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 33796
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 768 . . . . . . . . . . . . . . 15 (((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑥 ∈ (𝒫 𝑦 ∩ Fin)) ∧ 𝑗 = 𝑥) → 𝑥 ∈ (𝒫 𝑦 ∩ Fin))
2 elin 3992 . . . . . . . . . . . . . . 15 (𝑥 ∈ (𝒫 𝑦 ∩ Fin) ↔ (𝑥 ∈ 𝒫 𝑦𝑥 ∈ Fin))
31, 2sylib 218 . . . . . . . . . . . . . 14 (((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑥 ∈ (𝒫 𝑦 ∩ Fin)) ∧ 𝑗 = 𝑥) → (𝑥 ∈ 𝒫 𝑦𝑥 ∈ Fin))
43simpld 494 . . . . . . . . . . . . 13 (((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑥 ∈ (𝒫 𝑦 ∩ Fin)) ∧ 𝑗 = 𝑥) → 𝑥 ∈ 𝒫 𝑦)
5 elpwi 4629 . . . . . . . . . . . . 13 (𝑥 ∈ 𝒫 𝑦𝑥𝑦)
64, 5syl 17 . . . . . . . . . . . 12 (((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑥 ∈ (𝒫 𝑦 ∩ Fin)) ∧ 𝑗 = 𝑥) → 𝑥𝑦)
7 elpwi 4629 . . . . . . . . . . . . 13 (𝑦 ∈ 𝒫 𝑗𝑦𝑗)
87ad4antlr 732 . . . . . . . . . . . 12 (((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑥 ∈ (𝒫 𝑦 ∩ Fin)) ∧ 𝑗 = 𝑥) → 𝑦𝑗)
96, 8sstrd 4019 . . . . . . . . . . 11 (((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑥 ∈ (𝒫 𝑦 ∩ Fin)) ∧ 𝑗 = 𝑥) → 𝑥𝑗)
10 velpw 4627 . . . . . . . . . . 11 (𝑥 ∈ 𝒫 𝑗𝑥𝑗)
119, 10sylibr 234 . . . . . . . . . 10 (((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑥 ∈ (𝒫 𝑦 ∩ Fin)) ∧ 𝑗 = 𝑥) → 𝑥 ∈ 𝒫 𝑗)
123simprd 495 . . . . . . . . . 10 (((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑥 ∈ (𝒫 𝑦 ∩ Fin)) ∧ 𝑗 = 𝑥) → 𝑥 ∈ Fin)
1311, 12elind 4223 . . . . . . . . 9 (((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑥 ∈ (𝒫 𝑦 ∩ Fin)) ∧ 𝑗 = 𝑥) → 𝑥 ∈ (𝒫 𝑗 ∩ Fin))
14 simpr 484 . . . . . . . . . . 11 (((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑥 ∈ (𝒫 𝑦 ∩ Fin)) ∧ 𝑗 = 𝑥) → 𝑗 = 𝑥)
15 simpllr 775 . . . . . . . . . . 11 (((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑥 ∈ (𝒫 𝑦 ∩ Fin)) ∧ 𝑗 = 𝑥) → 𝑗 = 𝑦)
1614, 15eqtr3d 2782 . . . . . . . . . 10 (((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑥 ∈ (𝒫 𝑦 ∩ Fin)) ∧ 𝑗 = 𝑥) → 𝑥 = 𝑦)
17 eqid 2740 . . . . . . . . . . 11 𝑥 = 𝑥
18 eqid 2740 . . . . . . . . . . 11 𝑦 = 𝑦
1917, 18ssref 23541 . . . . . . . . . 10 ((𝑥 ∈ 𝒫 𝑗𝑥𝑦 𝑥 = 𝑦) → 𝑥Ref𝑦)
2011, 6, 16, 19syl3anc 1371 . . . . . . . . 9 (((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑥 ∈ (𝒫 𝑦 ∩ Fin)) ∧ 𝑗 = 𝑥) → 𝑥Ref𝑦)
21 breq1 5169 . . . . . . . . . 10 (𝑧 = 𝑥 → (𝑧Ref𝑦𝑥Ref𝑦))
2221rspcev 3635 . . . . . . . . 9 ((𝑥 ∈ (𝒫 𝑗 ∩ Fin) ∧ 𝑥Ref𝑦) → ∃𝑧 ∈ (𝒫 𝑗 ∩ Fin)𝑧Ref𝑦)
2313, 20, 22syl2anc 583 . . . . . . . 8 (((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑥 ∈ (𝒫 𝑦 ∩ Fin)) ∧ 𝑗 = 𝑥) → ∃𝑧 ∈ (𝒫 𝑗 ∩ Fin)𝑧Ref𝑦)
2423r19.29an 3164 . . . . . . 7 ((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ ∃𝑥 ∈ (𝒫 𝑦 ∩ Fin) 𝑗 = 𝑥) → ∃𝑧 ∈ (𝒫 𝑗 ∩ Fin)𝑧Ref𝑦)
25 simplr 768 . . . . . . . . . 10 (((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) → 𝑧 ∈ (𝒫 𝑗 ∩ Fin))
26 vex 3492 . . . . . . . . . . . . 13 𝑧 ∈ V
27 eqid 2740 . . . . . . . . . . . . . 14 𝑧 = 𝑧
2827, 18isref 23538 . . . . . . . . . . . . 13 (𝑧 ∈ V → (𝑧Ref𝑦 ↔ ( 𝑦 = 𝑧 ∧ ∀𝑢𝑧𝑣𝑦 𝑢𝑣)))
2926, 28ax-mp 5 . . . . . . . . . . . 12 (𝑧Ref𝑦 ↔ ( 𝑦 = 𝑧 ∧ ∀𝑢𝑧𝑣𝑦 𝑢𝑣))
3029simprbi 496 . . . . . . . . . . 11 (𝑧Ref𝑦 → ∀𝑢𝑧𝑣𝑦 𝑢𝑣)
3130adantl 481 . . . . . . . . . 10 (((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) → ∀𝑢𝑧𝑣𝑦 𝑢𝑣)
32 sseq2 4035 . . . . . . . . . . 11 (𝑣 = (𝑓𝑢) → (𝑢𝑣𝑢 ⊆ (𝑓𝑢)))
3332ac6sg 10557 . . . . . . . . . 10 (𝑧 ∈ (𝒫 𝑗 ∩ Fin) → (∀𝑢𝑧𝑣𝑦 𝑢𝑣 → ∃𝑓(𝑓:𝑧𝑦 ∧ ∀𝑢𝑧 𝑢 ⊆ (𝑓𝑢))))
3425, 31, 33sylc 65 . . . . . . . . 9 (((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) → ∃𝑓(𝑓:𝑧𝑦 ∧ ∀𝑢𝑧 𝑢 ⊆ (𝑓𝑢)))
35 simplr 768 . . . . . . . . . . . . . . 15 (((((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) ∧ 𝑓:𝑧𝑦) ∧ ∀𝑢𝑧 𝑢 ⊆ (𝑓𝑢)) → 𝑓:𝑧𝑦)
3635frnd 6755 . . . . . . . . . . . . . 14 (((((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) ∧ 𝑓:𝑧𝑦) ∧ ∀𝑢𝑧 𝑢 ⊆ (𝑓𝑢)) → ran 𝑓𝑦)
37 vex 3492 . . . . . . . . . . . . . . . 16 𝑓 ∈ V
3837rnex 7950 . . . . . . . . . . . . . . 15 ran 𝑓 ∈ V
3938elpw 4626 . . . . . . . . . . . . . 14 (ran 𝑓 ∈ 𝒫 𝑦 ↔ ran 𝑓𝑦)
4036, 39sylibr 234 . . . . . . . . . . . . 13 (((((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) ∧ 𝑓:𝑧𝑦) ∧ ∀𝑢𝑧 𝑢 ⊆ (𝑓𝑢)) → ran 𝑓 ∈ 𝒫 𝑦)
4135ffnd 6748 . . . . . . . . . . . . . . 15 (((((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) ∧ 𝑓:𝑧𝑦) ∧ ∀𝑢𝑧 𝑢 ⊆ (𝑓𝑢)) → 𝑓 Fn 𝑧)
42 elin 3992 . . . . . . . . . . . . . . . . 17 (𝑧 ∈ (𝒫 𝑗 ∩ Fin) ↔ (𝑧 ∈ 𝒫 𝑗𝑧 ∈ Fin))
4342simprbi 496 . . . . . . . . . . . . . . . 16 (𝑧 ∈ (𝒫 𝑗 ∩ Fin) → 𝑧 ∈ Fin)
4443ad4antlr 732 . . . . . . . . . . . . . . 15 (((((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) ∧ 𝑓:𝑧𝑦) ∧ ∀𝑢𝑧 𝑢 ⊆ (𝑓𝑢)) → 𝑧 ∈ Fin)
45 fnfi 9244 . . . . . . . . . . . . . . 15 ((𝑓 Fn 𝑧𝑧 ∈ Fin) → 𝑓 ∈ Fin)
4641, 44, 45syl2anc 583 . . . . . . . . . . . . . 14 (((((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) ∧ 𝑓:𝑧𝑦) ∧ ∀𝑢𝑧 𝑢 ⊆ (𝑓𝑢)) → 𝑓 ∈ Fin)
47 rnfi 9408 . . . . . . . . . . . . . 14 (𝑓 ∈ Fin → ran 𝑓 ∈ Fin)
4846, 47syl 17 . . . . . . . . . . . . 13 (((((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) ∧ 𝑓:𝑧𝑦) ∧ ∀𝑢𝑧 𝑢 ⊆ (𝑓𝑢)) → ran 𝑓 ∈ Fin)
4940, 48elind 4223 . . . . . . . . . . . 12 (((((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) ∧ 𝑓:𝑧𝑦) ∧ ∀𝑢𝑧 𝑢 ⊆ (𝑓𝑢)) → ran 𝑓 ∈ (𝒫 𝑦 ∩ Fin))
50 simp-5r 785 . . . . . . . . . . . . 13 (((((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) ∧ 𝑓:𝑧𝑦) ∧ ∀𝑢𝑧 𝑢 ⊆ (𝑓𝑢)) → 𝑗 = 𝑦)
5127, 18refbas 23539 . . . . . . . . . . . . . . . 16 (𝑧Ref𝑦 𝑦 = 𝑧)
5251ad3antlr 730 . . . . . . . . . . . . . . 15 (((((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) ∧ 𝑓:𝑧𝑦) ∧ ∀𝑢𝑧 𝑢 ⊆ (𝑓𝑢)) → 𝑦 = 𝑧)
53 nfv 1913 . . . . . . . . . . . . . . . . . . 19 𝑢(((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) ∧ 𝑓:𝑧𝑦)
54 nfra1 3290 . . . . . . . . . . . . . . . . . . 19 𝑢𝑢𝑧 𝑢 ⊆ (𝑓𝑢)
5553, 54nfan 1898 . . . . . . . . . . . . . . . . . 18 𝑢((((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) ∧ 𝑓:𝑧𝑦) ∧ ∀𝑢𝑧 𝑢 ⊆ (𝑓𝑢))
56 rspa 3254 . . . . . . . . . . . . . . . . . . . . 21 ((∀𝑢𝑧 𝑢 ⊆ (𝑓𝑢) ∧ 𝑢𝑧) → 𝑢 ⊆ (𝑓𝑢))
5756adantll 713 . . . . . . . . . . . . . . . . . . . 20 ((((((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) ∧ 𝑓:𝑧𝑦) ∧ ∀𝑢𝑧 𝑢 ⊆ (𝑓𝑢)) ∧ 𝑢𝑧) → 𝑢 ⊆ (𝑓𝑢))
5857sseld 4007 . . . . . . . . . . . . . . . . . . 19 ((((((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) ∧ 𝑓:𝑧𝑦) ∧ ∀𝑢𝑧 𝑢 ⊆ (𝑓𝑢)) ∧ 𝑢𝑧) → (𝑥𝑢𝑥 ∈ (𝑓𝑢)))
5958ex 412 . . . . . . . . . . . . . . . . . 18 (((((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) ∧ 𝑓:𝑧𝑦) ∧ ∀𝑢𝑧 𝑢 ⊆ (𝑓𝑢)) → (𝑢𝑧 → (𝑥𝑢𝑥 ∈ (𝑓𝑢))))
6055, 59reximdai 3267 . . . . . . . . . . . . . . . . 17 (((((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) ∧ 𝑓:𝑧𝑦) ∧ ∀𝑢𝑧 𝑢 ⊆ (𝑓𝑢)) → (∃𝑢𝑧 𝑥𝑢 → ∃𝑢𝑧 𝑥 ∈ (𝑓𝑢)))
61 eluni2 4935 . . . . . . . . . . . . . . . . . 18 (𝑥 𝑧 ↔ ∃𝑢𝑧 𝑥𝑢)
6261a1i 11 . . . . . . . . . . . . . . . . 17 (((((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) ∧ 𝑓:𝑧𝑦) ∧ ∀𝑢𝑧 𝑢 ⊆ (𝑓𝑢)) → (𝑥 𝑧 ↔ ∃𝑢𝑧 𝑥𝑢))
63 fnunirn 7291 . . . . . . . . . . . . . . . . . 18 (𝑓 Fn 𝑧 → (𝑥 ran 𝑓 ↔ ∃𝑢𝑧 𝑥 ∈ (𝑓𝑢)))
6441, 63syl 17 . . . . . . . . . . . . . . . . 17 (((((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) ∧ 𝑓:𝑧𝑦) ∧ ∀𝑢𝑧 𝑢 ⊆ (𝑓𝑢)) → (𝑥 ran 𝑓 ↔ ∃𝑢𝑧 𝑥 ∈ (𝑓𝑢)))
6560, 62, 643imtr4d 294 . . . . . . . . . . . . . . . 16 (((((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) ∧ 𝑓:𝑧𝑦) ∧ ∀𝑢𝑧 𝑢 ⊆ (𝑓𝑢)) → (𝑥 𝑧𝑥 ran 𝑓))
6665ssrdv 4014 . . . . . . . . . . . . . . 15 (((((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) ∧ 𝑓:𝑧𝑦) ∧ ∀𝑢𝑧 𝑢 ⊆ (𝑓𝑢)) → 𝑧 ran 𝑓)
6752, 66eqsstrd 4047 . . . . . . . . . . . . . 14 (((((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) ∧ 𝑓:𝑧𝑦) ∧ ∀𝑢𝑧 𝑢 ⊆ (𝑓𝑢)) → 𝑦 ran 𝑓)
6836unissd 4941 . . . . . . . . . . . . . 14 (((((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) ∧ 𝑓:𝑧𝑦) ∧ ∀𝑢𝑧 𝑢 ⊆ (𝑓𝑢)) → ran 𝑓 𝑦)
6967, 68eqssd 4026 . . . . . . . . . . . . 13 (((((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) ∧ 𝑓:𝑧𝑦) ∧ ∀𝑢𝑧 𝑢 ⊆ (𝑓𝑢)) → 𝑦 = ran 𝑓)
7050, 69eqtrd 2780 . . . . . . . . . . . 12 (((((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) ∧ 𝑓:𝑧𝑦) ∧ ∀𝑢𝑧 𝑢 ⊆ (𝑓𝑢)) → 𝑗 = ran 𝑓)
71 unieq 4942 . . . . . . . . . . . . 13 (𝑥 = ran 𝑓 𝑥 = ran 𝑓)
7271rspceeqv 3658 . . . . . . . . . . . 12 ((ran 𝑓 ∈ (𝒫 𝑦 ∩ Fin) ∧ 𝑗 = ran 𝑓) → ∃𝑥 ∈ (𝒫 𝑦 ∩ Fin) 𝑗 = 𝑥)
7349, 70, 72syl2anc 583 . . . . . . . . . . 11 (((((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) ∧ 𝑓:𝑧𝑦) ∧ ∀𝑢𝑧 𝑢 ⊆ (𝑓𝑢)) → ∃𝑥 ∈ (𝒫 𝑦 ∩ Fin) 𝑗 = 𝑥)
7473expl 457 . . . . . . . . . 10 (((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) → ((𝑓:𝑧𝑦 ∧ ∀𝑢𝑧 𝑢 ⊆ (𝑓𝑢)) → ∃𝑥 ∈ (𝒫 𝑦 ∩ Fin) 𝑗 = 𝑥))
7574exlimdv 1932 . . . . . . . . 9 (((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) → (∃𝑓(𝑓:𝑧𝑦 ∧ ∀𝑢𝑧 𝑢 ⊆ (𝑓𝑢)) → ∃𝑥 ∈ (𝒫 𝑦 ∩ Fin) 𝑗 = 𝑥))
7634, 75mpd 15 . . . . . . . 8 (((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) → ∃𝑥 ∈ (𝒫 𝑦 ∩ Fin) 𝑗 = 𝑥)
7776r19.29an 3164 . . . . . . 7 ((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) ∧ ∃𝑧 ∈ (𝒫 𝑗 ∩ Fin)𝑧Ref𝑦) → ∃𝑥 ∈ (𝒫 𝑦 ∩ Fin) 𝑗 = 𝑥)
7824, 77impbida 800 . . . . . 6 (((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ 𝑗 = 𝑦) → (∃𝑥 ∈ (𝒫 𝑦 ∩ Fin) 𝑗 = 𝑥 ↔ ∃𝑧 ∈ (𝒫 𝑗 ∩ Fin)𝑧Ref𝑦))
7978pm5.74da 803 . . . . 5 ((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) → (( 𝑗 = 𝑦 → ∃𝑥 ∈ (𝒫 𝑦 ∩ Fin) 𝑗 = 𝑥) ↔ ( 𝑗 = 𝑦 → ∃𝑧 ∈ (𝒫 𝑗 ∩ Fin)𝑧Ref𝑦)))
8079ralbidva 3182 . . . 4 (𝑗 ∈ Top → (∀𝑦 ∈ 𝒫 𝑗( 𝑗 = 𝑦 → ∃𝑥 ∈ (𝒫 𝑦 ∩ Fin) 𝑗 = 𝑥) ↔ ∀𝑦 ∈ 𝒫 𝑗( 𝑗 = 𝑦 → ∃𝑧 ∈ (𝒫 𝑗 ∩ Fin)𝑧Ref𝑦)))
8180pm5.32i 574 . . 3 ((𝑗 ∈ Top ∧ ∀𝑦 ∈ 𝒫 𝑗( 𝑗 = 𝑦 → ∃𝑥 ∈ (𝒫 𝑦 ∩ Fin) 𝑗 = 𝑥)) ↔ (𝑗 ∈ Top ∧ ∀𝑦 ∈ 𝒫 𝑗( 𝑗 = 𝑦 → ∃𝑧 ∈ (𝒫 𝑗 ∩ Fin)𝑧Ref𝑦)))
82 eqid 2740 . . . 4 𝑗 = 𝑗
8382iscmp 23417 . . 3 (𝑗 ∈ Comp ↔ (𝑗 ∈ Top ∧ ∀𝑦 ∈ 𝒫 𝑗( 𝑗 = 𝑦 → ∃𝑥 ∈ (𝒫 𝑦 ∩ Fin) 𝑗 = 𝑥)))
8482iscref 33790 . . 3 (𝑗 ∈ CovHasRefFin ↔ (𝑗 ∈ Top ∧ ∀𝑦 ∈ 𝒫 𝑗( 𝑗 = 𝑦 → ∃𝑧 ∈ (𝒫 𝑗 ∩ Fin)𝑧Ref𝑦)))
8581, 83, 843bitr4i 303 . 2 (𝑗 ∈ Comp ↔ 𝑗 ∈ CovHasRefFin)
8685eqriv 2737 1 Comp = CovHasRefFin
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395   = wceq 1537  wex 1777  wcel 2108  wral 3067  wrex 3076  Vcvv 3488  cin 3975  wss 3976  𝒫 cpw 4622   cuni 4931   class class class wbr 5166  ran crn 5701   Fn wfn 6568  wf 6569  cfv 6573  Fincfn 9003  Topctop 22920  Compccmp 23415  Refcref 23531  CovHasRefccref 33788
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-rep 5303  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447  ax-un 7770  ax-reg 9661  ax-inf2 9710  ax-ac2 10532
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-ral 3068  df-rex 3077  df-rmo 3388  df-reu 3389  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-pss 3996  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-int 4971  df-iun 5017  df-iin 5018  df-br 5167  df-opab 5229  df-mpt 5250  df-tr 5284  df-id 5593  df-eprel 5599  df-po 5607  df-so 5608  df-fr 5652  df-se 5653  df-we 5654  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-pred 6332  df-ord 6398  df-on 6399  df-lim 6400  df-suc 6401  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-fv 6581  df-isom 6582  df-riota 7404  df-ov 7451  df-om 7904  df-1st 8030  df-2nd 8031  df-frecs 8322  df-wrecs 8353  df-recs 8427  df-rdg 8466  df-1o 8522  df-en 9004  df-dom 9005  df-fin 9007  df-r1 9833  df-rank 9834  df-card 10008  df-ac 10185  df-cmp 23416  df-ref 23534  df-cref 33789
This theorem is referenced by:  cmpfiref  33797  cmppcmp  33804
  Copyright terms: Public domain W3C validator