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

Theorem cmpcref 32431
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 767 . . . . . . . . . . . . . . 15 (((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑥 ∈ (𝒫 𝑦 ∩ Fin)) ∧ 𝑗 = 𝑥) → 𝑥 ∈ (𝒫 𝑦 ∩ Fin))
2 elin 3926 . . . . . . . . . . . . . . 15 (𝑥 ∈ (𝒫 𝑦 ∩ Fin) ↔ (𝑥 ∈ 𝒫 𝑦𝑥 ∈ Fin))
31, 2sylib 217 . . . . . . . . . . . . . 14 (((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑥 ∈ (𝒫 𝑦 ∩ Fin)) ∧ 𝑗 = 𝑥) → (𝑥 ∈ 𝒫 𝑦𝑥 ∈ Fin))
43simpld 495 . . . . . . . . . . . . 13 (((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑥 ∈ (𝒫 𝑦 ∩ Fin)) ∧ 𝑗 = 𝑥) → 𝑥 ∈ 𝒫 𝑦)
5 elpwi 4567 . . . . . . . . . . . . 13 (𝑥 ∈ 𝒫 𝑦𝑥𝑦)
64, 5syl 17 . . . . . . . . . . . 12 (((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑥 ∈ (𝒫 𝑦 ∩ Fin)) ∧ 𝑗 = 𝑥) → 𝑥𝑦)
7 elpwi 4567 . . . . . . . . . . . . 13 (𝑦 ∈ 𝒫 𝑗𝑦𝑗)
87ad4antlr 731 . . . . . . . . . . . 12 (((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑥 ∈ (𝒫 𝑦 ∩ Fin)) ∧ 𝑗 = 𝑥) → 𝑦𝑗)
96, 8sstrd 3954 . . . . . . . . . . 11 (((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑥 ∈ (𝒫 𝑦 ∩ Fin)) ∧ 𝑗 = 𝑥) → 𝑥𝑗)
10 velpw 4565 . . . . . . . . . . 11 (𝑥 ∈ 𝒫 𝑗𝑥𝑗)
119, 10sylibr 233 . . . . . . . . . 10 (((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑥 ∈ (𝒫 𝑦 ∩ Fin)) ∧ 𝑗 = 𝑥) → 𝑥 ∈ 𝒫 𝑗)
123simprd 496 . . . . . . . . . 10 (((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑥 ∈ (𝒫 𝑦 ∩ Fin)) ∧ 𝑗 = 𝑥) → 𝑥 ∈ Fin)
1311, 12elind 4154 . . . . . . . . 9 (((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑥 ∈ (𝒫 𝑦 ∩ Fin)) ∧ 𝑗 = 𝑥) → 𝑥 ∈ (𝒫 𝑗 ∩ Fin))
14 simpr 485 . . . . . . . . . . 11 (((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑥 ∈ (𝒫 𝑦 ∩ Fin)) ∧ 𝑗 = 𝑥) → 𝑗 = 𝑥)
15 simpllr 774 . . . . . . . . . . 11 (((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑥 ∈ (𝒫 𝑦 ∩ Fin)) ∧ 𝑗 = 𝑥) → 𝑗 = 𝑦)
1614, 15eqtr3d 2778 . . . . . . . . . 10 (((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑥 ∈ (𝒫 𝑦 ∩ Fin)) ∧ 𝑗 = 𝑥) → 𝑥 = 𝑦)
17 eqid 2736 . . . . . . . . . . 11 𝑥 = 𝑥
18 eqid 2736 . . . . . . . . . . 11 𝑦 = 𝑦
1917, 18ssref 22863 . . . . . . . . . 10 ((𝑥 ∈ 𝒫 𝑗𝑥𝑦 𝑥 = 𝑦) → 𝑥Ref𝑦)
2011, 6, 16, 19syl3anc 1371 . . . . . . . . 9 (((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑥 ∈ (𝒫 𝑦 ∩ Fin)) ∧ 𝑗 = 𝑥) → 𝑥Ref𝑦)
21 breq1 5108 . . . . . . . . . 10 (𝑧 = 𝑥 → (𝑧Ref𝑦𝑥Ref𝑦))
2221rspcev 3581 . . . . . . . . 9 ((𝑥 ∈ (𝒫 𝑗 ∩ Fin) ∧ 𝑥Ref𝑦) → ∃𝑧 ∈ (𝒫 𝑗 ∩ Fin)𝑧Ref𝑦)
2313, 20, 22syl2anc 584 . . . . . . . 8 (((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑥 ∈ (𝒫 𝑦 ∩ Fin)) ∧ 𝑗 = 𝑥) → ∃𝑧 ∈ (𝒫 𝑗 ∩ Fin)𝑧Ref𝑦)
2423r19.29an 3155 . . . . . . 7 ((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ ∃𝑥 ∈ (𝒫 𝑦 ∩ Fin) 𝑗 = 𝑥) → ∃𝑧 ∈ (𝒫 𝑗 ∩ Fin)𝑧Ref𝑦)
25 simplr 767 . . . . . . . . . 10 (((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) → 𝑧 ∈ (𝒫 𝑗 ∩ Fin))
26 vex 3449 . . . . . . . . . . . . 13 𝑧 ∈ V
27 eqid 2736 . . . . . . . . . . . . . 14 𝑧 = 𝑧
2827, 18isref 22860 . . . . . . . . . . . . 13 (𝑧 ∈ V → (𝑧Ref𝑦 ↔ ( 𝑦 = 𝑧 ∧ ∀𝑢𝑧𝑣𝑦 𝑢𝑣)))
2926, 28ax-mp 5 . . . . . . . . . . . 12 (𝑧Ref𝑦 ↔ ( 𝑦 = 𝑧 ∧ ∀𝑢𝑧𝑣𝑦 𝑢𝑣))
3029simprbi 497 . . . . . . . . . . 11 (𝑧Ref𝑦 → ∀𝑢𝑧𝑣𝑦 𝑢𝑣)
3130adantl 482 . . . . . . . . . 10 (((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) → ∀𝑢𝑧𝑣𝑦 𝑢𝑣)
32 sseq2 3970 . . . . . . . . . . 11 (𝑣 = (𝑓𝑢) → (𝑢𝑣𝑢 ⊆ (𝑓𝑢)))
3332ac6sg 10424 . . . . . . . . . 10 (𝑧 ∈ (𝒫 𝑗 ∩ Fin) → (∀𝑢𝑧𝑣𝑦 𝑢𝑣 → ∃𝑓(𝑓:𝑧𝑦 ∧ ∀𝑢𝑧 𝑢 ⊆ (𝑓𝑢))))
3425, 31, 33sylc 65 . . . . . . . . 9 (((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) → ∃𝑓(𝑓:𝑧𝑦 ∧ ∀𝑢𝑧 𝑢 ⊆ (𝑓𝑢)))
35 simplr 767 . . . . . . . . . . . . . . 15 (((((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) ∧ 𝑓:𝑧𝑦) ∧ ∀𝑢𝑧 𝑢 ⊆ (𝑓𝑢)) → 𝑓:𝑧𝑦)
3635frnd 6676 . . . . . . . . . . . . . 14 (((((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) ∧ 𝑓:𝑧𝑦) ∧ ∀𝑢𝑧 𝑢 ⊆ (𝑓𝑢)) → ran 𝑓𝑦)
37 vex 3449 . . . . . . . . . . . . . . . 16 𝑓 ∈ V
3837rnex 7849 . . . . . . . . . . . . . . 15 ran 𝑓 ∈ V
3938elpw 4564 . . . . . . . . . . . . . 14 (ran 𝑓 ∈ 𝒫 𝑦 ↔ ran 𝑓𝑦)
4036, 39sylibr 233 . . . . . . . . . . . . 13 (((((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) ∧ 𝑓:𝑧𝑦) ∧ ∀𝑢𝑧 𝑢 ⊆ (𝑓𝑢)) → ran 𝑓 ∈ 𝒫 𝑦)
4135ffnd 6669 . . . . . . . . . . . . . . 15 (((((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) ∧ 𝑓:𝑧𝑦) ∧ ∀𝑢𝑧 𝑢 ⊆ (𝑓𝑢)) → 𝑓 Fn 𝑧)
42 elin 3926 . . . . . . . . . . . . . . . . 17 (𝑧 ∈ (𝒫 𝑗 ∩ Fin) ↔ (𝑧 ∈ 𝒫 𝑗𝑧 ∈ Fin))
4342simprbi 497 . . . . . . . . . . . . . . . 16 (𝑧 ∈ (𝒫 𝑗 ∩ Fin) → 𝑧 ∈ Fin)
4443ad4antlr 731 . . . . . . . . . . . . . . 15 (((((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) ∧ 𝑓:𝑧𝑦) ∧ ∀𝑢𝑧 𝑢 ⊆ (𝑓𝑢)) → 𝑧 ∈ Fin)
45 fnfi 9125 . . . . . . . . . . . . . . 15 ((𝑓 Fn 𝑧𝑧 ∈ Fin) → 𝑓 ∈ Fin)
4641, 44, 45syl2anc 584 . . . . . . . . . . . . . 14 (((((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) ∧ 𝑓:𝑧𝑦) ∧ ∀𝑢𝑧 𝑢 ⊆ (𝑓𝑢)) → 𝑓 ∈ Fin)
47 rnfi 9279 . . . . . . . . . . . . . 14 (𝑓 ∈ Fin → ran 𝑓 ∈ Fin)
4846, 47syl 17 . . . . . . . . . . . . 13 (((((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) ∧ 𝑓:𝑧𝑦) ∧ ∀𝑢𝑧 𝑢 ⊆ (𝑓𝑢)) → ran 𝑓 ∈ Fin)
4940, 48elind 4154 . . . . . . . . . . . 12 (((((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) ∧ 𝑓:𝑧𝑦) ∧ ∀𝑢𝑧 𝑢 ⊆ (𝑓𝑢)) → ran 𝑓 ∈ (𝒫 𝑦 ∩ Fin))
50 simp-5r 784 . . . . . . . . . . . . 13 (((((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) ∧ 𝑓:𝑧𝑦) ∧ ∀𝑢𝑧 𝑢 ⊆ (𝑓𝑢)) → 𝑗 = 𝑦)
5127, 18refbas 22861 . . . . . . . . . . . . . . . 16 (𝑧Ref𝑦 𝑦 = 𝑧)
5251ad3antlr 729 . . . . . . . . . . . . . . 15 (((((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) ∧ 𝑓:𝑧𝑦) ∧ ∀𝑢𝑧 𝑢 ⊆ (𝑓𝑢)) → 𝑦 = 𝑧)
53 nfv 1917 . . . . . . . . . . . . . . . . . . 19 𝑢(((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) ∧ 𝑓:𝑧𝑦)
54 nfra1 3267 . . . . . . . . . . . . . . . . . . 19 𝑢𝑢𝑧 𝑢 ⊆ (𝑓𝑢)
5553, 54nfan 1902 . . . . . . . . . . . . . . . . . 18 𝑢((((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) ∧ 𝑓:𝑧𝑦) ∧ ∀𝑢𝑧 𝑢 ⊆ (𝑓𝑢))
56 rspa 3231 . . . . . . . . . . . . . . . . . . . . 21 ((∀𝑢𝑧 𝑢 ⊆ (𝑓𝑢) ∧ 𝑢𝑧) → 𝑢 ⊆ (𝑓𝑢))
5756adantll 712 . . . . . . . . . . . . . . . . . . . 20 ((((((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) ∧ 𝑓:𝑧𝑦) ∧ ∀𝑢𝑧 𝑢 ⊆ (𝑓𝑢)) ∧ 𝑢𝑧) → 𝑢 ⊆ (𝑓𝑢))
5857sseld 3943 . . . . . . . . . . . . . . . . . . 19 ((((((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) ∧ 𝑓:𝑧𝑦) ∧ ∀𝑢𝑧 𝑢 ⊆ (𝑓𝑢)) ∧ 𝑢𝑧) → (𝑥𝑢𝑥 ∈ (𝑓𝑢)))
5958ex 413 . . . . . . . . . . . . . . . . . 18 (((((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) ∧ 𝑓:𝑧𝑦) ∧ ∀𝑢𝑧 𝑢 ⊆ (𝑓𝑢)) → (𝑢𝑧 → (𝑥𝑢𝑥 ∈ (𝑓𝑢))))
6055, 59reximdai 3244 . . . . . . . . . . . . . . . . 17 (((((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) ∧ 𝑓:𝑧𝑦) ∧ ∀𝑢𝑧 𝑢 ⊆ (𝑓𝑢)) → (∃𝑢𝑧 𝑥𝑢 → ∃𝑢𝑧 𝑥 ∈ (𝑓𝑢)))
61 eluni2 4869 . . . . . . . . . . . . . . . . . 18 (𝑥 𝑧 ↔ ∃𝑢𝑧 𝑥𝑢)
6261a1i 11 . . . . . . . . . . . . . . . . 17 (((((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) ∧ 𝑓:𝑧𝑦) ∧ ∀𝑢𝑧 𝑢 ⊆ (𝑓𝑢)) → (𝑥 𝑧 ↔ ∃𝑢𝑧 𝑥𝑢))
63 fnunirn 7201 . . . . . . . . . . . . . . . . . 18 (𝑓 Fn 𝑧 → (𝑥 ran 𝑓 ↔ ∃𝑢𝑧 𝑥 ∈ (𝑓𝑢)))
6441, 63syl 17 . . . . . . . . . . . . . . . . 17 (((((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) ∧ 𝑓:𝑧𝑦) ∧ ∀𝑢𝑧 𝑢 ⊆ (𝑓𝑢)) → (𝑥 ran 𝑓 ↔ ∃𝑢𝑧 𝑥 ∈ (𝑓𝑢)))
6560, 62, 643imtr4d 293 . . . . . . . . . . . . . . . 16 (((((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) ∧ 𝑓:𝑧𝑦) ∧ ∀𝑢𝑧 𝑢 ⊆ (𝑓𝑢)) → (𝑥 𝑧𝑥 ran 𝑓))
6665ssrdv 3950 . . . . . . . . . . . . . . 15 (((((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) ∧ 𝑓:𝑧𝑦) ∧ ∀𝑢𝑧 𝑢 ⊆ (𝑓𝑢)) → 𝑧 ran 𝑓)
6752, 66eqsstrd 3982 . . . . . . . . . . . . . 14 (((((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) ∧ 𝑓:𝑧𝑦) ∧ ∀𝑢𝑧 𝑢 ⊆ (𝑓𝑢)) → 𝑦 ran 𝑓)
6836unissd 4875 . . . . . . . . . . . . . 14 (((((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) ∧ 𝑓:𝑧𝑦) ∧ ∀𝑢𝑧 𝑢 ⊆ (𝑓𝑢)) → ran 𝑓 𝑦)
6967, 68eqssd 3961 . . . . . . . . . . . . 13 (((((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) ∧ 𝑓:𝑧𝑦) ∧ ∀𝑢𝑧 𝑢 ⊆ (𝑓𝑢)) → 𝑦 = ran 𝑓)
7050, 69eqtrd 2776 . . . . . . . . . . . 12 (((((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) ∧ 𝑓:𝑧𝑦) ∧ ∀𝑢𝑧 𝑢 ⊆ (𝑓𝑢)) → 𝑗 = ran 𝑓)
71 unieq 4876 . . . . . . . . . . . . 13 (𝑥 = ran 𝑓 𝑥 = ran 𝑓)
7271rspceeqv 3595 . . . . . . . . . . . 12 ((ran 𝑓 ∈ (𝒫 𝑦 ∩ Fin) ∧ 𝑗 = ran 𝑓) → ∃𝑥 ∈ (𝒫 𝑦 ∩ Fin) 𝑗 = 𝑥)
7349, 70, 72syl2anc 584 . . . . . . . . . . 11 (((((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) ∧ 𝑓:𝑧𝑦) ∧ ∀𝑢𝑧 𝑢 ⊆ (𝑓𝑢)) → ∃𝑥 ∈ (𝒫 𝑦 ∩ Fin) 𝑗 = 𝑥)
7473expl 458 . . . . . . . . . 10 (((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) → ((𝑓:𝑧𝑦 ∧ ∀𝑢𝑧 𝑢 ⊆ (𝑓𝑢)) → ∃𝑥 ∈ (𝒫 𝑦 ∩ Fin) 𝑗 = 𝑥))
7574exlimdv 1936 . . . . . . . . 9 (((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) → (∃𝑓(𝑓:𝑧𝑦 ∧ ∀𝑢𝑧 𝑢 ⊆ (𝑓𝑢)) → ∃𝑥 ∈ (𝒫 𝑦 ∩ Fin) 𝑗 = 𝑥))
7634, 75mpd 15 . . . . . . . 8 (((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) → ∃𝑥 ∈ (𝒫 𝑦 ∩ Fin) 𝑗 = 𝑥)
7776r19.29an 3155 . . . . . . 7 ((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ ∃𝑧 ∈ (𝒫 𝑗 ∩ Fin)𝑧Ref𝑦) → ∃𝑥 ∈ (𝒫 𝑦 ∩ Fin) 𝑗 = 𝑥)
7824, 77impbida 799 . . . . . 6 (((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) → (∃𝑥 ∈ (𝒫 𝑦 ∩ Fin) 𝑗 = 𝑥 ↔ ∃𝑧 ∈ (𝒫 𝑗 ∩ Fin)𝑧Ref𝑦))
7978pm5.74da 802 . . . . 5 ((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) → (( 𝑗 = 𝑦 → ∃𝑥 ∈ (𝒫 𝑦 ∩ Fin) 𝑗 = 𝑥) ↔ ( 𝑗 = 𝑦 → ∃𝑧 ∈ (𝒫 𝑗 ∩ Fin)𝑧Ref𝑦)))
8079ralbidva 3172 . . . 4 (𝑗 ∈ Top → (∀𝑦 ∈ 𝒫 𝑗( 𝑗 = 𝑦 → ∃𝑥 ∈ (𝒫 𝑦 ∩ Fin) 𝑗 = 𝑥) ↔ ∀𝑦 ∈ 𝒫 𝑗( 𝑗 = 𝑦 → ∃𝑧 ∈ (𝒫 𝑗 ∩ Fin)𝑧Ref𝑦)))
8180pm5.32i 575 . . 3 ((𝑗 ∈ Top ∧ ∀𝑦 ∈ 𝒫 𝑗( 𝑗 = 𝑦 → ∃𝑥 ∈ (𝒫 𝑦 ∩ Fin) 𝑗 = 𝑥)) ↔ (𝑗 ∈ Top ∧ ∀𝑦 ∈ 𝒫 𝑗( 𝑗 = 𝑦 → ∃𝑧 ∈ (𝒫 𝑗 ∩ Fin)𝑧Ref𝑦)))
82 eqid 2736 . . . 4 𝑗 = 𝑗
8382iscmp 22739 . . 3 (𝑗 ∈ Comp ↔ (𝑗 ∈ Top ∧ ∀𝑦 ∈ 𝒫 𝑗( 𝑗 = 𝑦 → ∃𝑥 ∈ (𝒫 𝑦 ∩ Fin) 𝑗 = 𝑥)))
8482iscref 32425 . . 3 (𝑗 ∈ CovHasRefFin ↔ (𝑗 ∈ Top ∧ ∀𝑦 ∈ 𝒫 𝑗( 𝑗 = 𝑦 → ∃𝑧 ∈ (𝒫 𝑗 ∩ Fin)𝑧Ref𝑦)))
8581, 83, 843bitr4i 302 . 2 (𝑗 ∈ Comp ↔ 𝑗 ∈ CovHasRefFin)
8685eqriv 2733 1 Comp = CovHasRefFin
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396   = wceq 1541  wex 1781  wcel 2106  wral 3064  wrex 3073  Vcvv 3445  cin 3909  wss 3910  𝒫 cpw 4560   cuni 4865   class class class wbr 5105  ran crn 5634   Fn wfn 6491  wf 6492  cfv 6496  Fincfn 8883  Topctop 22242  Compccmp 22737  Refcref 22853  CovHasRefccref 32423
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-reg 9528  ax-inf2 9577  ax-ac2 10399
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-int 4908  df-iun 4956  df-iin 4957  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-se 5589  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-isom 6505  df-riota 7313  df-ov 7360  df-om 7803  df-1st 7921  df-2nd 7922  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-1o 8412  df-er 8648  df-en 8884  df-dom 8885  df-fin 8887  df-r1 9700  df-rank 9701  df-card 9875  df-ac 10052  df-cmp 22738  df-ref 22856  df-cref 32424
This theorem is referenced by:  cmpfiref  32432  cmppcmp  32439
  Copyright terms: Public domain W3C validator