Mathbox for Thierry Arnoux < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  cmpcref Structured version   Visualization version   GIF version

Theorem cmpcref 30248
 Description: Equivalent definition of compact space in terms of open cover refinements. Compact spaces are topologies with finite open cover refinements. (Contributed by Thierry Arnoux, 7-Jan-2020.)
Assertion
Ref Expression
cmpcref Comp = CovHasRefFin

Proof of Theorem cmpcref
Dummy variables 𝑓 𝑗 𝑢 𝑣 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simplr 809 . . . . . . . . . . . . . . 15 (((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑥 ∈ (𝒫 𝑦 ∩ Fin)) ∧ 𝑗 = 𝑥) → 𝑥 ∈ (𝒫 𝑦 ∩ Fin))
2 elin 3940 . . . . . . . . . . . . . . 15 (𝑥 ∈ (𝒫 𝑦 ∩ Fin) ↔ (𝑥 ∈ 𝒫 𝑦𝑥 ∈ Fin))
31, 2sylib 208 . . . . . . . . . . . . . 14 (((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑥 ∈ (𝒫 𝑦 ∩ Fin)) ∧ 𝑗 = 𝑥) → (𝑥 ∈ 𝒫 𝑦𝑥 ∈ Fin))
43simpld 477 . . . . . . . . . . . . 13 (((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑥 ∈ (𝒫 𝑦 ∩ Fin)) ∧ 𝑗 = 𝑥) → 𝑥 ∈ 𝒫 𝑦)
5 elpwi 4313 . . . . . . . . . . . . 13 (𝑥 ∈ 𝒫 𝑦𝑥𝑦)
64, 5syl 17 . . . . . . . . . . . 12 (((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑥 ∈ (𝒫 𝑦 ∩ Fin)) ∧ 𝑗 = 𝑥) → 𝑥𝑦)
7 elpwi 4313 . . . . . . . . . . . . 13 (𝑦 ∈ 𝒫 𝑗𝑦𝑗)
87ad4antlr 773 . . . . . . . . . . . 12 (((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑥 ∈ (𝒫 𝑦 ∩ Fin)) ∧ 𝑗 = 𝑥) → 𝑦𝑗)
96, 8sstrd 3755 . . . . . . . . . . 11 (((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑥 ∈ (𝒫 𝑦 ∩ Fin)) ∧ 𝑗 = 𝑥) → 𝑥𝑗)
10 selpw 4310 . . . . . . . . . . 11 (𝑥 ∈ 𝒫 𝑗𝑥𝑗)
119, 10sylibr 224 . . . . . . . . . 10 (((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑥 ∈ (𝒫 𝑦 ∩ Fin)) ∧ 𝑗 = 𝑥) → 𝑥 ∈ 𝒫 𝑗)
123simprd 482 . . . . . . . . . 10 (((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑥 ∈ (𝒫 𝑦 ∩ Fin)) ∧ 𝑗 = 𝑥) → 𝑥 ∈ Fin)
1311, 12elind 3942 . . . . . . . . 9 (((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑥 ∈ (𝒫 𝑦 ∩ Fin)) ∧ 𝑗 = 𝑥) → 𝑥 ∈ (𝒫 𝑗 ∩ Fin))
14 simpr 479 . . . . . . . . . . 11 (((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑥 ∈ (𝒫 𝑦 ∩ Fin)) ∧ 𝑗 = 𝑥) → 𝑗 = 𝑥)
15 simpllr 817 . . . . . . . . . . 11 (((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑥 ∈ (𝒫 𝑦 ∩ Fin)) ∧ 𝑗 = 𝑥) → 𝑗 = 𝑦)
1614, 15eqtr3d 2797 . . . . . . . . . 10 (((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑥 ∈ (𝒫 𝑦 ∩ Fin)) ∧ 𝑗 = 𝑥) → 𝑥 = 𝑦)
17 eqid 2761 . . . . . . . . . . 11 𝑥 = 𝑥
18 eqid 2761 . . . . . . . . . . 11 𝑦 = 𝑦
1917, 18ssref 21538 . . . . . . . . . 10 ((𝑥 ∈ 𝒫 𝑗𝑥𝑦 𝑥 = 𝑦) → 𝑥Ref𝑦)
2011, 6, 16, 19syl3anc 1477 . . . . . . . . 9 (((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑥 ∈ (𝒫 𝑦 ∩ Fin)) ∧ 𝑗 = 𝑥) → 𝑥Ref𝑦)
21 breq1 4808 . . . . . . . . . 10 (𝑧 = 𝑥 → (𝑧Ref𝑦𝑥Ref𝑦))
2221rspcev 3450 . . . . . . . . 9 ((𝑥 ∈ (𝒫 𝑗 ∩ Fin) ∧ 𝑥Ref𝑦) → ∃𝑧 ∈ (𝒫 𝑗 ∩ Fin)𝑧Ref𝑦)
2313, 20, 22syl2anc 696 . . . . . . . 8 (((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑥 ∈ (𝒫 𝑦 ∩ Fin)) ∧ 𝑗 = 𝑥) → ∃𝑧 ∈ (𝒫 𝑗 ∩ Fin)𝑧Ref𝑦)
2423r19.29an 3216 . . . . . . 7 ((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ ∃𝑥 ∈ (𝒫 𝑦 ∩ Fin) 𝑗 = 𝑥) → ∃𝑧 ∈ (𝒫 𝑗 ∩ Fin)𝑧Ref𝑦)
25 simplr 809 . . . . . . . . . 10 (((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) → 𝑧 ∈ (𝒫 𝑗 ∩ Fin))
26 vex 3344 . . . . . . . . . . . . 13 𝑧 ∈ V
27 eqid 2761 . . . . . . . . . . . . . 14 𝑧 = 𝑧
2827, 18isref 21535 . . . . . . . . . . . . 13 (𝑧 ∈ V → (𝑧Ref𝑦 ↔ ( 𝑦 = 𝑧 ∧ ∀𝑢𝑧𝑣𝑦 𝑢𝑣)))
2926, 28ax-mp 5 . . . . . . . . . . . 12 (𝑧Ref𝑦 ↔ ( 𝑦 = 𝑧 ∧ ∀𝑢𝑧𝑣𝑦 𝑢𝑣))
3029simprbi 483 . . . . . . . . . . 11 (𝑧Ref𝑦 → ∀𝑢𝑧𝑣𝑦 𝑢𝑣)
3130adantl 473 . . . . . . . . . 10 (((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) → ∀𝑢𝑧𝑣𝑦 𝑢𝑣)
32 sseq2 3769 . . . . . . . . . . 11 (𝑣 = (𝑓𝑢) → (𝑢𝑣𝑢 ⊆ (𝑓𝑢)))
3332ac6sg 9523 . . . . . . . . . 10 (𝑧 ∈ (𝒫 𝑗 ∩ Fin) → (∀𝑢𝑧𝑣𝑦 𝑢𝑣 → ∃𝑓(𝑓:𝑧𝑦 ∧ ∀𝑢𝑧 𝑢 ⊆ (𝑓𝑢))))
3425, 31, 33sylc 65 . . . . . . . . 9 (((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) → ∃𝑓(𝑓:𝑧𝑦 ∧ ∀𝑢𝑧 𝑢 ⊆ (𝑓𝑢)))
35 simplr 809 . . . . . . . . . . . . . . 15 (((((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) ∧ 𝑓:𝑧𝑦) ∧ ∀𝑢𝑧 𝑢 ⊆ (𝑓𝑢)) → 𝑓:𝑧𝑦)
36 frn 6215 . . . . . . . . . . . . . . 15 (𝑓:𝑧𝑦 → ran 𝑓𝑦)
3735, 36syl 17 . . . . . . . . . . . . . 14 (((((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) ∧ 𝑓:𝑧𝑦) ∧ ∀𝑢𝑧 𝑢 ⊆ (𝑓𝑢)) → ran 𝑓𝑦)
38 vex 3344 . . . . . . . . . . . . . . . 16 𝑓 ∈ V
3938rnex 7267 . . . . . . . . . . . . . . 15 ran 𝑓 ∈ V
4039elpw 4309 . . . . . . . . . . . . . 14 (ran 𝑓 ∈ 𝒫 𝑦 ↔ ran 𝑓𝑦)
4137, 40sylibr 224 . . . . . . . . . . . . 13 (((((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) ∧ 𝑓:𝑧𝑦) ∧ ∀𝑢𝑧 𝑢 ⊆ (𝑓𝑢)) → ran 𝑓 ∈ 𝒫 𝑦)
42 ffn 6207 . . . . . . . . . . . . . . . 16 (𝑓:𝑧𝑦𝑓 Fn 𝑧)
4335, 42syl 17 . . . . . . . . . . . . . . 15 (((((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) ∧ 𝑓:𝑧𝑦) ∧ ∀𝑢𝑧 𝑢 ⊆ (𝑓𝑢)) → 𝑓 Fn 𝑧)
44 elin 3940 . . . . . . . . . . . . . . . . 17 (𝑧 ∈ (𝒫 𝑗 ∩ Fin) ↔ (𝑧 ∈ 𝒫 𝑗𝑧 ∈ Fin))
4544simprbi 483 . . . . . . . . . . . . . . . 16 (𝑧 ∈ (𝒫 𝑗 ∩ Fin) → 𝑧 ∈ Fin)
4645ad4antlr 773 . . . . . . . . . . . . . . 15 (((((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) ∧ 𝑓:𝑧𝑦) ∧ ∀𝑢𝑧 𝑢 ⊆ (𝑓𝑢)) → 𝑧 ∈ Fin)
47 fnfi 8406 . . . . . . . . . . . . . . 15 ((𝑓 Fn 𝑧𝑧 ∈ Fin) → 𝑓 ∈ Fin)
4843, 46, 47syl2anc 696 . . . . . . . . . . . . . 14 (((((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) ∧ 𝑓:𝑧𝑦) ∧ ∀𝑢𝑧 𝑢 ⊆ (𝑓𝑢)) → 𝑓 ∈ Fin)
49 rnfi 8417 . . . . . . . . . . . . . 14 (𝑓 ∈ Fin → ran 𝑓 ∈ Fin)
5048, 49syl 17 . . . . . . . . . . . . 13 (((((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) ∧ 𝑓:𝑧𝑦) ∧ ∀𝑢𝑧 𝑢 ⊆ (𝑓𝑢)) → ran 𝑓 ∈ Fin)
5141, 50elind 3942 . . . . . . . . . . . 12 (((((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) ∧ 𝑓:𝑧𝑦) ∧ ∀𝑢𝑧 𝑢 ⊆ (𝑓𝑢)) → ran 𝑓 ∈ (𝒫 𝑦 ∩ Fin))
52 simp-5r 831 . . . . . . . . . . . . 13 (((((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) ∧ 𝑓:𝑧𝑦) ∧ ∀𝑢𝑧 𝑢 ⊆ (𝑓𝑢)) → 𝑗 = 𝑦)
5327, 18refbas 21536 . . . . . . . . . . . . . . . 16 (𝑧Ref𝑦 𝑦 = 𝑧)
5453ad3antlr 769 . . . . . . . . . . . . . . 15 (((((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) ∧ 𝑓:𝑧𝑦) ∧ ∀𝑢𝑧 𝑢 ⊆ (𝑓𝑢)) → 𝑦 = 𝑧)
55 nfv 1993 . . . . . . . . . . . . . . . . . . 19 𝑢(((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) ∧ 𝑓:𝑧𝑦)
56 nfra1 3080 . . . . . . . . . . . . . . . . . . 19 𝑢𝑢𝑧 𝑢 ⊆ (𝑓𝑢)
5755, 56nfan 1978 . . . . . . . . . . . . . . . . . 18 𝑢((((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) ∧ 𝑓:𝑧𝑦) ∧ ∀𝑢𝑧 𝑢 ⊆ (𝑓𝑢))
58 rspa 3069 . . . . . . . . . . . . . . . . . . . . 21 ((∀𝑢𝑧 𝑢 ⊆ (𝑓𝑢) ∧ 𝑢𝑧) → 𝑢 ⊆ (𝑓𝑢))
5958adantll 752 . . . . . . . . . . . . . . . . . . . 20 ((((((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) ∧ 𝑓:𝑧𝑦) ∧ ∀𝑢𝑧 𝑢 ⊆ (𝑓𝑢)) ∧ 𝑢𝑧) → 𝑢 ⊆ (𝑓𝑢))
6059sseld 3744 . . . . . . . . . . . . . . . . . . 19 ((((((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) ∧ 𝑓:𝑧𝑦) ∧ ∀𝑢𝑧 𝑢 ⊆ (𝑓𝑢)) ∧ 𝑢𝑧) → (𝑥𝑢𝑥 ∈ (𝑓𝑢)))
6160ex 449 . . . . . . . . . . . . . . . . . 18 (((((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) ∧ 𝑓:𝑧𝑦) ∧ ∀𝑢𝑧 𝑢 ⊆ (𝑓𝑢)) → (𝑢𝑧 → (𝑥𝑢𝑥 ∈ (𝑓𝑢))))
6257, 61reximdai 3151 . . . . . . . . . . . . . . . . 17 (((((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) ∧ 𝑓:𝑧𝑦) ∧ ∀𝑢𝑧 𝑢 ⊆ (𝑓𝑢)) → (∃𝑢𝑧 𝑥𝑢 → ∃𝑢𝑧 𝑥 ∈ (𝑓𝑢)))
63 eluni2 4593 . . . . . . . . . . . . . . . . . 18 (𝑥 𝑧 ↔ ∃𝑢𝑧 𝑥𝑢)
6463a1i 11 . . . . . . . . . . . . . . . . 17 (((((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) ∧ 𝑓:𝑧𝑦) ∧ ∀𝑢𝑧 𝑢 ⊆ (𝑓𝑢)) → (𝑥 𝑧 ↔ ∃𝑢𝑧 𝑥𝑢))
65 fnunirn 6676 . . . . . . . . . . . . . . . . . 18 (𝑓 Fn 𝑧 → (𝑥 ran 𝑓 ↔ ∃𝑢𝑧 𝑥 ∈ (𝑓𝑢)))
6643, 65syl 17 . . . . . . . . . . . . . . . . 17 (((((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) ∧ 𝑓:𝑧𝑦) ∧ ∀𝑢𝑧 𝑢 ⊆ (𝑓𝑢)) → (𝑥 ran 𝑓 ↔ ∃𝑢𝑧 𝑥 ∈ (𝑓𝑢)))
6762, 64, 663imtr4d 283 . . . . . . . . . . . . . . . 16 (((((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) ∧ 𝑓:𝑧𝑦) ∧ ∀𝑢𝑧 𝑢 ⊆ (𝑓𝑢)) → (𝑥 𝑧𝑥 ran 𝑓))
6867ssrdv 3751 . . . . . . . . . . . . . . 15 (((((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) ∧ 𝑓:𝑧𝑦) ∧ ∀𝑢𝑧 𝑢 ⊆ (𝑓𝑢)) → 𝑧 ran 𝑓)
6954, 68eqsstrd 3781 . . . . . . . . . . . . . 14 (((((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) ∧ 𝑓:𝑧𝑦) ∧ ∀𝑢𝑧 𝑢 ⊆ (𝑓𝑢)) → 𝑦 ran 𝑓)
7037unissd 4615 . . . . . . . . . . . . . 14 (((((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) ∧ 𝑓:𝑧𝑦) ∧ ∀𝑢𝑧 𝑢 ⊆ (𝑓𝑢)) → ran 𝑓 𝑦)
7169, 70eqssd 3762 . . . . . . . . . . . . 13 (((((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) ∧ 𝑓:𝑧𝑦) ∧ ∀𝑢𝑧 𝑢 ⊆ (𝑓𝑢)) → 𝑦 = ran 𝑓)
7252, 71eqtrd 2795 . . . . . . . . . . . 12 (((((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) ∧ 𝑓:𝑧𝑦) ∧ ∀𝑢𝑧 𝑢 ⊆ (𝑓𝑢)) → 𝑗 = ran 𝑓)
73 unieq 4597 . . . . . . . . . . . . . 14 (𝑥 = ran 𝑓 𝑥 = ran 𝑓)
7473eqeq2d 2771 . . . . . . . . . . . . 13 (𝑥 = ran 𝑓 → ( 𝑗 = 𝑥 𝑗 = ran 𝑓))
7574rspcev 3450 . . . . . . . . . . . 12 ((ran 𝑓 ∈ (𝒫 𝑦 ∩ Fin) ∧ 𝑗 = ran 𝑓) → ∃𝑥 ∈ (𝒫 𝑦 ∩ Fin) 𝑗 = 𝑥)
7651, 72, 75syl2anc 696 . . . . . . . . . . 11 (((((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) ∧ 𝑓:𝑧𝑦) ∧ ∀𝑢𝑧 𝑢 ⊆ (𝑓𝑢)) → ∃𝑥 ∈ (𝒫 𝑦 ∩ Fin) 𝑗 = 𝑥)
7776expl 649 . . . . . . . . . 10 (((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) → ((𝑓:𝑧𝑦 ∧ ∀𝑢𝑧 𝑢 ⊆ (𝑓𝑢)) → ∃𝑥 ∈ (𝒫 𝑦 ∩ Fin) 𝑗 = 𝑥))
7877exlimdv 2011 . . . . . . . . 9 (((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) → (∃𝑓(𝑓:𝑧𝑦 ∧ ∀𝑢𝑧 𝑢 ⊆ (𝑓𝑢)) → ∃𝑥 ∈ (𝒫 𝑦 ∩ Fin) 𝑗 = 𝑥))
7934, 78mpd 15 . . . . . . . 8 (((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) → ∃𝑥 ∈ (𝒫 𝑦 ∩ Fin) 𝑗 = 𝑥)
8079r19.29an 3216 . . . . . . 7 ((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ ∃𝑧 ∈ (𝒫 𝑗 ∩ Fin)𝑧Ref𝑦) → ∃𝑥 ∈ (𝒫 𝑦 ∩ Fin) 𝑗 = 𝑥)
8124, 80impbida 913 . . . . . 6 (((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) → (∃𝑥 ∈ (𝒫 𝑦 ∩ Fin) 𝑗 = 𝑥 ↔ ∃𝑧 ∈ (𝒫 𝑗 ∩ Fin)𝑧Ref𝑦))
8281pm5.74da 725 . . . . 5 ((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) → (( 𝑗 = 𝑦 → ∃𝑥 ∈ (𝒫 𝑦 ∩ Fin) 𝑗 = 𝑥) ↔ ( 𝑗 = 𝑦 → ∃𝑧 ∈ (𝒫 𝑗 ∩ Fin)𝑧Ref𝑦)))
8382ralbidva 3124 . . . 4 (𝑗 ∈ Top → (∀𝑦 ∈ 𝒫 𝑗( 𝑗 = 𝑦 → ∃𝑥 ∈ (𝒫 𝑦 ∩ Fin) 𝑗 = 𝑥) ↔ ∀𝑦 ∈ 𝒫 𝑗( 𝑗 = 𝑦 → ∃𝑧 ∈ (𝒫 𝑗 ∩ Fin)𝑧Ref𝑦)))
8483pm5.32i 672 . . 3 ((𝑗 ∈ Top ∧ ∀𝑦 ∈ 𝒫 𝑗( 𝑗 = 𝑦 → ∃𝑥 ∈ (𝒫 𝑦 ∩ Fin) 𝑗 = 𝑥)) ↔ (𝑗 ∈ Top ∧ ∀𝑦 ∈ 𝒫 𝑗( 𝑗 = 𝑦 → ∃𝑧 ∈ (𝒫 𝑗 ∩ Fin)𝑧Ref𝑦)))
85 eqid 2761 . . . 4 𝑗 = 𝑗
8685iscmp 21414 . . 3 (𝑗 ∈ Comp ↔ (𝑗 ∈ Top ∧ ∀𝑦 ∈ 𝒫 𝑗( 𝑗 = 𝑦 → ∃𝑥 ∈ (𝒫 𝑦 ∩ Fin) 𝑗 = 𝑥)))
8785iscref 30242 . . 3 (𝑗 ∈ CovHasRefFin ↔ (𝑗 ∈ Top ∧ ∀𝑦 ∈ 𝒫 𝑗( 𝑗 = 𝑦 → ∃𝑧 ∈ (𝒫 𝑗 ∩ Fin)𝑧Ref𝑦)))
8884, 86, 873bitr4i 292 . 2 (𝑗 ∈ Comp ↔ 𝑗 ∈ CovHasRefFin)
8988eqriv 2758 1 Comp = CovHasRefFin
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383   = wceq 1632  ∃wex 1853   ∈ wcel 2140  ∀wral 3051  ∃wrex 3052  Vcvv 3341   ∩ cin 3715   ⊆ wss 3716  𝒫 cpw 4303  ∪ cuni 4589   class class class wbr 4805  ran crn 5268   Fn wfn 6045  ⟶wf 6046  ‘cfv 6050  Fincfn 8124  Topctop 20921  Compccmp 21412  Refcref 21528  CovHasRefccref 30240 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1989  ax-6 2055  ax-7 2091  ax-8 2142  ax-9 2149  ax-10 2169  ax-11 2184  ax-12 2197  ax-13 2392  ax-ext 2741  ax-rep 4924  ax-sep 4934  ax-nul 4942  ax-pow 4993  ax-pr 5056  ax-un 7116  ax-reg 8665  ax-inf2 8714  ax-ac2 9498 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2048  df-eu 2612  df-mo 2613  df-clab 2748  df-cleq 2754  df-clel 2757  df-nfc 2892  df-ne 2934  df-ral 3056  df-rex 3057  df-reu 3058  df-rmo 3059  df-rab 3060  df-v 3343  df-sbc 3578  df-csb 3676  df-dif 3719  df-un 3721  df-in 3723  df-ss 3730  df-pss 3732  df-nul 4060  df-if 4232  df-pw 4305  df-sn 4323  df-pr 4325  df-tp 4327  df-op 4329  df-uni 4590  df-int 4629  df-iun 4675  df-iin 4676  df-br 4806  df-opab 4866  df-mpt 4883  df-tr 4906  df-id 5175  df-eprel 5180  df-po 5188  df-so 5189  df-fr 5226  df-se 5227  df-we 5228  df-xp 5273  df-rel 5274  df-cnv 5275  df-co 5276  df-dm 5277  df-rn 5278  df-res 5279  df-ima 5280  df-pred 5842  df-ord 5888  df-on 5889  df-lim 5890  df-suc 5891  df-iota 6013  df-fun 6052  df-fn 6053  df-f 6054  df-f1 6055  df-fo 6056  df-f1o 6057  df-fv 6058  df-isom 6059  df-riota 6776  df-ov 6818  df-oprab 6819  df-mpt2 6820  df-om 7233  df-1st 7335  df-2nd 7336  df-wrecs 7578  df-recs 7639  df-rdg 7677  df-1o 7731  df-oadd 7735  df-er 7914  df-en 8125  df-dom 8126  df-fin 8128  df-r1 8803  df-rank 8804  df-card 8976  df-ac 9150  df-cmp 21413  df-ref 21531  df-cref 30241 This theorem is referenced by:  cmpfiref  30249  cmppcmp  30256
 Copyright terms: Public domain W3C validator