Metamath Proof Explorer

Theorem cmpcref

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)

Ref Expression
Assertion cmpcref Comp = CovHasRef Fin

Proof

Step Hyp Ref Expression
1 simplr ⊢ ( ( ( ( ( 𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗 ) ∧ ∪ 𝑗 = ∪ 𝑦 ) ∧ 𝑥 ∈ ( 𝒫 𝑦 ∩ Fin ) ) ∧ ∪ 𝑗 = ∪ 𝑥 ) → 𝑥 ∈ ( 𝒫 𝑦 ∩ Fin ) )
2 elin ⊢ ( 𝑥 ∈ ( 𝒫 𝑦 ∩ Fin ) ↔ ( 𝑥 ∈ 𝒫 𝑦 ∧ 𝑥 ∈ Fin ) )
3 1 2 sylib ⊢ ( ( ( ( ( 𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗 ) ∧ ∪ 𝑗 = ∪ 𝑦 ) ∧ 𝑥 ∈ ( 𝒫 𝑦 ∩ Fin ) ) ∧ ∪ 𝑗 = ∪ 𝑥 ) → ( 𝑥 ∈ 𝒫 𝑦 ∧ 𝑥 ∈ Fin ) )
4 3 simpld ⊢ ( ( ( ( ( 𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗 ) ∧ ∪ 𝑗 = ∪ 𝑦 ) ∧ 𝑥 ∈ ( 𝒫 𝑦 ∩ Fin ) ) ∧ ∪ 𝑗 = ∪ 𝑥 ) → 𝑥 ∈ 𝒫 𝑦 )
5 elpwi ⊢ ( 𝑥 ∈ 𝒫 𝑦 → 𝑥 ⊆ 𝑦 )
6 4 5 syl ⊢ ( ( ( ( ( 𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗 ) ∧ ∪ 𝑗 = ∪ 𝑦 ) ∧ 𝑥 ∈ ( 𝒫 𝑦 ∩ Fin ) ) ∧ ∪ 𝑗 = ∪ 𝑥 ) → 𝑥 ⊆ 𝑦 )
7 elpwi ⊢ ( 𝑦 ∈ 𝒫 𝑗 → 𝑦 ⊆ 𝑗 )
8 7 ad4antlr ⊢ ( ( ( ( ( 𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗 ) ∧ ∪ 𝑗 = ∪ 𝑦 ) ∧ 𝑥 ∈ ( 𝒫 𝑦 ∩ Fin ) ) ∧ ∪ 𝑗 = ∪ 𝑥 ) → 𝑦 ⊆ 𝑗 )
9 6 8 sstrd ⊢ ( ( ( ( ( 𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗 ) ∧ ∪ 𝑗 = ∪ 𝑦 ) ∧ 𝑥 ∈ ( 𝒫 𝑦 ∩ Fin ) ) ∧ ∪ 𝑗 = ∪ 𝑥 ) → 𝑥 ⊆ 𝑗 )
10 velpw ⊢ ( 𝑥 ∈ 𝒫 𝑗 ↔ 𝑥 ⊆ 𝑗 )
11 9 10 sylibr ⊢ ( ( ( ( ( 𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗 ) ∧ ∪ 𝑗 = ∪ 𝑦 ) ∧ 𝑥 ∈ ( 𝒫 𝑦 ∩ Fin ) ) ∧ ∪ 𝑗 = ∪ 𝑥 ) → 𝑥 ∈ 𝒫 𝑗 )
12 3 simprd ⊢ ( ( ( ( ( 𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗 ) ∧ ∪ 𝑗 = ∪ 𝑦 ) ∧ 𝑥 ∈ ( 𝒫 𝑦 ∩ Fin ) ) ∧ ∪ 𝑗 = ∪ 𝑥 ) → 𝑥 ∈ Fin )
13 11 12 elind ⊢ ( ( ( ( ( 𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗 ) ∧ ∪ 𝑗 = ∪ 𝑦 ) ∧ 𝑥 ∈ ( 𝒫 𝑦 ∩ Fin ) ) ∧ ∪ 𝑗 = ∪ 𝑥 ) → 𝑥 ∈ ( 𝒫 𝑗 ∩ Fin ) )
14 simpr ⊢ ( ( ( ( ( 𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗 ) ∧ ∪ 𝑗 = ∪ 𝑦 ) ∧ 𝑥 ∈ ( 𝒫 𝑦 ∩ Fin ) ) ∧ ∪ 𝑗 = ∪ 𝑥 ) → ∪ 𝑗 = ∪ 𝑥 )
15 simpllr ⊢ ( ( ( ( ( 𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗 ) ∧ ∪ 𝑗 = ∪ 𝑦 ) ∧ 𝑥 ∈ ( 𝒫 𝑦 ∩ Fin ) ) ∧ ∪ 𝑗 = ∪ 𝑥 ) → ∪ 𝑗 = ∪ 𝑦 )
16 14 15 eqtr3d ⊢ ( ( ( ( ( 𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗 ) ∧ ∪ 𝑗 = ∪ 𝑦 ) ∧ 𝑥 ∈ ( 𝒫 𝑦 ∩ Fin ) ) ∧ ∪ 𝑗 = ∪ 𝑥 ) → ∪ 𝑥 = ∪ 𝑦 )
17 eqid ⊢ ∪ 𝑥 = ∪ 𝑥
18 eqid ⊢ ∪ 𝑦 = ∪ 𝑦
19 17 18 ssref ⊢ ( ( 𝑥 ∈ 𝒫 𝑗 ∧ 𝑥 ⊆ 𝑦 ∧ ∪ 𝑥 = ∪ 𝑦 ) → 𝑥 Ref 𝑦 )
20 11 6 16 19 syl3anc ⊢ ( ( ( ( ( 𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗 ) ∧ ∪ 𝑗 = ∪ 𝑦 ) ∧ 𝑥 ∈ ( 𝒫 𝑦 ∩ Fin ) ) ∧ ∪ 𝑗 = ∪ 𝑥 ) → 𝑥 Ref 𝑦 )
21 breq1 ⊢ ( 𝑧 = 𝑥 → ( 𝑧 Ref 𝑦 ↔ 𝑥 Ref 𝑦 ) )
22 21 rspcev ⊢ ( ( 𝑥 ∈ ( 𝒫 𝑗 ∩ Fin ) ∧ 𝑥 Ref 𝑦 ) → ∃ 𝑧 ∈ ( 𝒫 𝑗 ∩ Fin ) 𝑧 Ref 𝑦 )
23 13 20 22 syl2anc ⊢ ( ( ( ( ( 𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗 ) ∧ ∪ 𝑗 = ∪ 𝑦 ) ∧ 𝑥 ∈ ( 𝒫 𝑦 ∩ Fin ) ) ∧ ∪ 𝑗 = ∪ 𝑥 ) → ∃ 𝑧 ∈ ( 𝒫 𝑗 ∩ Fin ) 𝑧 Ref 𝑦 )
24 23 r19.29an ⊢ ( ( ( ( 𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗 ) ∧ ∪ 𝑗 = ∪ 𝑦 ) ∧ ∃ 𝑥 ∈ ( 𝒫 𝑦 ∩ Fin ) ∪ 𝑗 = ∪ 𝑥 ) → ∃ 𝑧 ∈ ( 𝒫 𝑗 ∩ Fin ) 𝑧 Ref 𝑦 )
25 simplr ⊢ ( ( ( ( ( 𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗 ) ∧ ∪ 𝑗 = ∪ 𝑦 ) ∧ 𝑧 ∈ ( 𝒫 𝑗 ∩ Fin ) ) ∧ 𝑧 Ref 𝑦 ) → 𝑧 ∈ ( 𝒫 𝑗 ∩ Fin ) )
26 vex ⊢ 𝑧 ∈ V
27 eqid ⊢ ∪ 𝑧 = ∪ 𝑧
28 27 18 isref ⊢ ( 𝑧 ∈ V → ( 𝑧 Ref 𝑦 ↔ ( ∪ 𝑦 = ∪ 𝑧 ∧ ∀ 𝑢 ∈ 𝑧 ∃ 𝑣 ∈ 𝑦 𝑢 ⊆ 𝑣 ) ) )
29 26 28 ax-mp ⊢ ( 𝑧 Ref 𝑦 ↔ ( ∪ 𝑦 = ∪ 𝑧 ∧ ∀ 𝑢 ∈ 𝑧 ∃ 𝑣 ∈ 𝑦 𝑢 ⊆ 𝑣 ) )
30 29 simprbi ⊢ ( 𝑧 Ref 𝑦 → ∀ 𝑢 ∈ 𝑧 ∃ 𝑣 ∈ 𝑦 𝑢 ⊆ 𝑣 )
31 30 adantl ⊢ ( ( ( ( ( 𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗 ) ∧ ∪ 𝑗 = ∪ 𝑦 ) ∧ 𝑧 ∈ ( 𝒫 𝑗 ∩ Fin ) ) ∧ 𝑧 Ref 𝑦 ) → ∀ 𝑢 ∈ 𝑧 ∃ 𝑣 ∈ 𝑦 𝑢 ⊆ 𝑣 )
32 sseq2 ⊢ ( 𝑣 = ( 𝑓 ‘ 𝑢 ) → ( 𝑢 ⊆ 𝑣 ↔ 𝑢 ⊆ ( 𝑓 ‘ 𝑢 ) ) )
33 32 ac6sg ⊢ ( 𝑧 ∈ ( 𝒫 𝑗 ∩ Fin ) → ( ∀ 𝑢 ∈ 𝑧 ∃ 𝑣 ∈ 𝑦 𝑢 ⊆ 𝑣 → ∃ 𝑓 ( 𝑓 : 𝑧 ⟶ 𝑦 ∧ ∀ 𝑢 ∈ 𝑧 𝑢 ⊆ ( 𝑓 ‘ 𝑢 ) ) ) )
34 25 31 33 sylc ⊢ ( ( ( ( ( 𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗 ) ∧ ∪ 𝑗 = ∪ 𝑦 ) ∧ 𝑧 ∈ ( 𝒫 𝑗 ∩ Fin ) ) ∧ 𝑧 Ref 𝑦 ) → ∃ 𝑓 ( 𝑓 : 𝑧 ⟶ 𝑦 ∧ ∀ 𝑢 ∈ 𝑧 𝑢 ⊆ ( 𝑓 ‘ 𝑢 ) ) )
35 simplr ⊢ ( ( ( ( ( ( ( 𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗 ) ∧ ∪ 𝑗 = ∪ 𝑦 ) ∧ 𝑧 ∈ ( 𝒫 𝑗 ∩ Fin ) ) ∧ 𝑧 Ref 𝑦 ) ∧ 𝑓 : 𝑧 ⟶ 𝑦 ) ∧ ∀ 𝑢 ∈ 𝑧 𝑢 ⊆ ( 𝑓 ‘ 𝑢 ) ) → 𝑓 : 𝑧 ⟶ 𝑦 )
36 35 frnd ⊢ ( ( ( ( ( ( ( 𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗 ) ∧ ∪ 𝑗 = ∪ 𝑦 ) ∧ 𝑧 ∈ ( 𝒫 𝑗 ∩ Fin ) ) ∧ 𝑧 Ref 𝑦 ) ∧ 𝑓 : 𝑧 ⟶ 𝑦 ) ∧ ∀ 𝑢 ∈ 𝑧 𝑢 ⊆ ( 𝑓 ‘ 𝑢 ) ) → ran 𝑓 ⊆ 𝑦 )
37 vex ⊢ 𝑓 ∈ V
38 37 rnex ⊢ ran 𝑓 ∈ V
39 38 elpw ⊢ ( ran 𝑓 ∈ 𝒫 𝑦 ↔ ran 𝑓 ⊆ 𝑦 )
40 36 39 sylibr ⊢ ( ( ( ( ( ( ( 𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗 ) ∧ ∪ 𝑗 = ∪ 𝑦 ) ∧ 𝑧 ∈ ( 𝒫 𝑗 ∩ Fin ) ) ∧ 𝑧 Ref 𝑦 ) ∧ 𝑓 : 𝑧 ⟶ 𝑦 ) ∧ ∀ 𝑢 ∈ 𝑧 𝑢 ⊆ ( 𝑓 ‘ 𝑢 ) ) → ran 𝑓 ∈ 𝒫 𝑦 )
41 35 ffnd ⊢ ( ( ( ( ( ( ( 𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗 ) ∧ ∪ 𝑗 = ∪ 𝑦 ) ∧ 𝑧 ∈ ( 𝒫 𝑗 ∩ Fin ) ) ∧ 𝑧 Ref 𝑦 ) ∧ 𝑓 : 𝑧 ⟶ 𝑦 ) ∧ ∀ 𝑢 ∈ 𝑧 𝑢 ⊆ ( 𝑓 ‘ 𝑢 ) ) → 𝑓 Fn 𝑧 )
42 elin ⊢ ( 𝑧 ∈ ( 𝒫 𝑗 ∩ Fin ) ↔ ( 𝑧 ∈ 𝒫 𝑗 ∧ 𝑧 ∈ Fin ) )
43 42 simprbi ⊢ ( 𝑧 ∈ ( 𝒫 𝑗 ∩ Fin ) → 𝑧 ∈ Fin )
44 43 ad4antlr ⊢ ( ( ( ( ( ( ( 𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗 ) ∧ ∪ 𝑗 = ∪ 𝑦 ) ∧ 𝑧 ∈ ( 𝒫 𝑗 ∩ Fin ) ) ∧ 𝑧 Ref 𝑦 ) ∧ 𝑓 : 𝑧 ⟶ 𝑦 ) ∧ ∀ 𝑢 ∈ 𝑧 𝑢 ⊆ ( 𝑓 ‘ 𝑢 ) ) → 𝑧 ∈ Fin )
45 fnfi ⊢ ( ( 𝑓 Fn 𝑧 ∧ 𝑧 ∈ Fin ) → 𝑓 ∈ Fin )
46 41 44 45 syl2anc ⊢ ( ( ( ( ( ( ( 𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗 ) ∧ ∪ 𝑗 = ∪ 𝑦 ) ∧ 𝑧 ∈ ( 𝒫 𝑗 ∩ Fin ) ) ∧ 𝑧 Ref 𝑦 ) ∧ 𝑓 : 𝑧 ⟶ 𝑦 ) ∧ ∀ 𝑢 ∈ 𝑧 𝑢 ⊆ ( 𝑓 ‘ 𝑢 ) ) → 𝑓 ∈ Fin )
47 rnfi ⊢ ( 𝑓 ∈ Fin → ran 𝑓 ∈ Fin )
48 46 47 syl ⊢ ( ( ( ( ( ( ( 𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗 ) ∧ ∪ 𝑗 = ∪ 𝑦 ) ∧ 𝑧 ∈ ( 𝒫 𝑗 ∩ Fin ) ) ∧ 𝑧 Ref 𝑦 ) ∧ 𝑓 : 𝑧 ⟶ 𝑦 ) ∧ ∀ 𝑢 ∈ 𝑧 𝑢 ⊆ ( 𝑓 ‘ 𝑢 ) ) → ran 𝑓 ∈ Fin )
49 40 48 elind ⊢ ( ( ( ( ( ( ( 𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗 ) ∧ ∪ 𝑗 = ∪ 𝑦 ) ∧ 𝑧 ∈ ( 𝒫 𝑗 ∩ Fin ) ) ∧ 𝑧 Ref 𝑦 ) ∧ 𝑓 : 𝑧 ⟶ 𝑦 ) ∧ ∀ 𝑢 ∈ 𝑧 𝑢 ⊆ ( 𝑓 ‘ 𝑢 ) ) → ran 𝑓 ∈ ( 𝒫 𝑦 ∩ Fin ) )
50 simp-5r ⊢ ( ( ( ( ( ( ( 𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗 ) ∧ ∪ 𝑗 = ∪ 𝑦 ) ∧ 𝑧 ∈ ( 𝒫 𝑗 ∩ Fin ) ) ∧ 𝑧 Ref 𝑦 ) ∧ 𝑓 : 𝑧 ⟶ 𝑦 ) ∧ ∀ 𝑢 ∈ 𝑧 𝑢 ⊆ ( 𝑓 ‘ 𝑢 ) ) → ∪ 𝑗 = ∪ 𝑦 )
51 27 18 refbas ⊢ ( 𝑧 Ref 𝑦 → ∪ 𝑦 = ∪ 𝑧 )
52 51 ad3antlr ⊢ ( ( ( ( ( ( ( 𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗 ) ∧ ∪ 𝑗 = ∪ 𝑦 ) ∧ 𝑧 ∈ ( 𝒫 𝑗 ∩ Fin ) ) ∧ 𝑧 Ref 𝑦 ) ∧ 𝑓 : 𝑧 ⟶ 𝑦 ) ∧ ∀ 𝑢 ∈ 𝑧 𝑢 ⊆ ( 𝑓 ‘ 𝑢 ) ) → ∪ 𝑦 = ∪ 𝑧 )
53 nfv ⊢ Ⅎ 𝑢 ( ( ( ( ( 𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗 ) ∧ ∪ 𝑗 = ∪ 𝑦 ) ∧ 𝑧 ∈ ( 𝒫 𝑗 ∩ Fin ) ) ∧ 𝑧 Ref 𝑦 ) ∧ 𝑓 : 𝑧 ⟶ 𝑦 )
54 nfra1 ⊢ Ⅎ 𝑢 ∀ 𝑢 ∈ 𝑧 𝑢 ⊆ ( 𝑓 ‘ 𝑢 )
55 53 54 nfan ⊢ Ⅎ 𝑢 ( ( ( ( ( ( 𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗 ) ∧ ∪ 𝑗 = ∪ 𝑦 ) ∧ 𝑧 ∈ ( 𝒫 𝑗 ∩ Fin ) ) ∧ 𝑧 Ref 𝑦 ) ∧ 𝑓 : 𝑧 ⟶ 𝑦 ) ∧ ∀ 𝑢 ∈ 𝑧 𝑢 ⊆ ( 𝑓 ‘ 𝑢 ) )
56 rspa ⊢ ( ( ∀ 𝑢 ∈ 𝑧 𝑢 ⊆ ( 𝑓 ‘ 𝑢 ) ∧ 𝑢 ∈ 𝑧 ) → 𝑢 ⊆ ( 𝑓 ‘ 𝑢 ) )
57 56 adantll ⊢ ( ( ( ( ( ( ( ( 𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗 ) ∧ ∪ 𝑗 = ∪ 𝑦 ) ∧ 𝑧 ∈ ( 𝒫 𝑗 ∩ Fin ) ) ∧ 𝑧 Ref 𝑦 ) ∧ 𝑓 : 𝑧 ⟶ 𝑦 ) ∧ ∀ 𝑢 ∈ 𝑧 𝑢 ⊆ ( 𝑓 ‘ 𝑢 ) ) ∧ 𝑢 ∈ 𝑧 ) → 𝑢 ⊆ ( 𝑓 ‘ 𝑢 ) )
58 57 sseld ⊢ ( ( ( ( ( ( ( ( 𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗 ) ∧ ∪ 𝑗 = ∪ 𝑦 ) ∧ 𝑧 ∈ ( 𝒫 𝑗 ∩ Fin ) ) ∧ 𝑧 Ref 𝑦 ) ∧ 𝑓 : 𝑧 ⟶ 𝑦 ) ∧ ∀ 𝑢 ∈ 𝑧 𝑢 ⊆ ( 𝑓 ‘ 𝑢 ) ) ∧ 𝑢 ∈ 𝑧 ) → ( 𝑥 ∈ 𝑢 → 𝑥 ∈ ( 𝑓 ‘ 𝑢 ) ) )
59 58 ex ⊢ ( ( ( ( ( ( ( 𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗 ) ∧ ∪ 𝑗 = ∪ 𝑦 ) ∧ 𝑧 ∈ ( 𝒫 𝑗 ∩ Fin ) ) ∧ 𝑧 Ref 𝑦 ) ∧ 𝑓 : 𝑧 ⟶ 𝑦 ) ∧ ∀ 𝑢 ∈ 𝑧 𝑢 ⊆ ( 𝑓 ‘ 𝑢 ) ) → ( 𝑢 ∈ 𝑧 → ( 𝑥 ∈ 𝑢 → 𝑥 ∈ ( 𝑓 ‘ 𝑢 ) ) ) )
60 55 59 reximdai ⊢ ( ( ( ( ( ( ( 𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗 ) ∧ ∪ 𝑗 = ∪ 𝑦 ) ∧ 𝑧 ∈ ( 𝒫 𝑗 ∩ Fin ) ) ∧ 𝑧 Ref 𝑦 ) ∧ 𝑓 : 𝑧 ⟶ 𝑦 ) ∧ ∀ 𝑢 ∈ 𝑧 𝑢 ⊆ ( 𝑓 ‘ 𝑢 ) ) → ( ∃ 𝑢 ∈ 𝑧 𝑥 ∈ 𝑢 → ∃ 𝑢 ∈ 𝑧 𝑥 ∈ ( 𝑓 ‘ 𝑢 ) ) )
61 eluni2 ⊢ ( 𝑥 ∈ ∪ 𝑧 ↔ ∃ 𝑢 ∈ 𝑧 𝑥 ∈ 𝑢 )
62 61 a1i ⊢ ( ( ( ( ( ( ( 𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗 ) ∧ ∪ 𝑗 = ∪ 𝑦 ) ∧ 𝑧 ∈ ( 𝒫 𝑗 ∩ Fin ) ) ∧ 𝑧 Ref 𝑦 ) ∧ 𝑓 : 𝑧 ⟶ 𝑦 ) ∧ ∀ 𝑢 ∈ 𝑧 𝑢 ⊆ ( 𝑓 ‘ 𝑢 ) ) → ( 𝑥 ∈ ∪ 𝑧 ↔ ∃ 𝑢 ∈ 𝑧 𝑥 ∈ 𝑢 ) )
63 fnunirn ⊢ ( 𝑓 Fn 𝑧 → ( 𝑥 ∈ ∪ ran 𝑓 ↔ ∃ 𝑢 ∈ 𝑧 𝑥 ∈ ( 𝑓 ‘ 𝑢 ) ) )
64 41 63 syl ⊢ ( ( ( ( ( ( ( 𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗 ) ∧ ∪ 𝑗 = ∪ 𝑦 ) ∧ 𝑧 ∈ ( 𝒫 𝑗 ∩ Fin ) ) ∧ 𝑧 Ref 𝑦 ) ∧ 𝑓 : 𝑧 ⟶ 𝑦 ) ∧ ∀ 𝑢 ∈ 𝑧 𝑢 ⊆ ( 𝑓 ‘ 𝑢 ) ) → ( 𝑥 ∈ ∪ ran 𝑓 ↔ ∃ 𝑢 ∈ 𝑧 𝑥 ∈ ( 𝑓 ‘ 𝑢 ) ) )
65 60 62 64 3imtr4d ⊢ ( ( ( ( ( ( ( 𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗 ) ∧ ∪ 𝑗 = ∪ 𝑦 ) ∧ 𝑧 ∈ ( 𝒫 𝑗 ∩ Fin ) ) ∧ 𝑧 Ref 𝑦 ) ∧ 𝑓 : 𝑧 ⟶ 𝑦 ) ∧ ∀ 𝑢 ∈ 𝑧 𝑢 ⊆ ( 𝑓 ‘ 𝑢 ) ) → ( 𝑥 ∈ ∪ 𝑧 → 𝑥 ∈ ∪ ran 𝑓 ) )
66 65 ssrdv ⊢ ( ( ( ( ( ( ( 𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗 ) ∧ ∪ 𝑗 = ∪ 𝑦 ) ∧ 𝑧 ∈ ( 𝒫 𝑗 ∩ Fin ) ) ∧ 𝑧 Ref 𝑦 ) ∧ 𝑓 : 𝑧 ⟶ 𝑦 ) ∧ ∀ 𝑢 ∈ 𝑧 𝑢 ⊆ ( 𝑓 ‘ 𝑢 ) ) → ∪ 𝑧 ⊆ ∪ ran 𝑓 )
67 52 66 eqsstrd ⊢ ( ( ( ( ( ( ( 𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗 ) ∧ ∪ 𝑗 = ∪ 𝑦 ) ∧ 𝑧 ∈ ( 𝒫 𝑗 ∩ Fin ) ) ∧ 𝑧 Ref 𝑦 ) ∧ 𝑓 : 𝑧 ⟶ 𝑦 ) ∧ ∀ 𝑢 ∈ 𝑧 𝑢 ⊆ ( 𝑓 ‘ 𝑢 ) ) → ∪ 𝑦 ⊆ ∪ ran 𝑓 )
68 36 unissd ⊢ ( ( ( ( ( ( ( 𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗 ) ∧ ∪ 𝑗 = ∪ 𝑦 ) ∧ 𝑧 ∈ ( 𝒫 𝑗 ∩ Fin ) ) ∧ 𝑧 Ref 𝑦 ) ∧ 𝑓 : 𝑧 ⟶ 𝑦 ) ∧ ∀ 𝑢 ∈ 𝑧 𝑢 ⊆ ( 𝑓 ‘ 𝑢 ) ) → ∪ ran 𝑓 ⊆ ∪ 𝑦 )
69 67 68 eqssd ⊢ ( ( ( ( ( ( ( 𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗 ) ∧ ∪ 𝑗 = ∪ 𝑦 ) ∧ 𝑧 ∈ ( 𝒫 𝑗 ∩ Fin ) ) ∧ 𝑧 Ref 𝑦 ) ∧ 𝑓 : 𝑧 ⟶ 𝑦 ) ∧ ∀ 𝑢 ∈ 𝑧 𝑢 ⊆ ( 𝑓 ‘ 𝑢 ) ) → ∪ 𝑦 = ∪ ran 𝑓 )
70 50 69 eqtrd ⊢ ( ( ( ( ( ( ( 𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗 ) ∧ ∪ 𝑗 = ∪ 𝑦 ) ∧ 𝑧 ∈ ( 𝒫 𝑗 ∩ Fin ) ) ∧ 𝑧 Ref 𝑦 ) ∧ 𝑓 : 𝑧 ⟶ 𝑦 ) ∧ ∀ 𝑢 ∈ 𝑧 𝑢 ⊆ ( 𝑓 ‘ 𝑢 ) ) → ∪ 𝑗 = ∪ ran 𝑓 )
71 unieq ⊢ ( 𝑥 = ran 𝑓 → ∪ 𝑥 = ∪ ran 𝑓 )
72 71 rspceeqv ⊢ ( ( ran 𝑓 ∈ ( 𝒫 𝑦 ∩ Fin ) ∧ ∪ 𝑗 = ∪ ran 𝑓 ) → ∃ 𝑥 ∈ ( 𝒫 𝑦 ∩ Fin ) ∪ 𝑗 = ∪ 𝑥 )
73 49 70 72 syl2anc ⊢ ( ( ( ( ( ( ( 𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗 ) ∧ ∪ 𝑗 = ∪ 𝑦 ) ∧ 𝑧 ∈ ( 𝒫 𝑗 ∩ Fin ) ) ∧ 𝑧 Ref 𝑦 ) ∧ 𝑓 : 𝑧 ⟶ 𝑦 ) ∧ ∀ 𝑢 ∈ 𝑧 𝑢 ⊆ ( 𝑓 ‘ 𝑢 ) ) → ∃ 𝑥 ∈ ( 𝒫 𝑦 ∩ Fin ) ∪ 𝑗 = ∪ 𝑥 )
74 73 expl ⊢ ( ( ( ( ( 𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗 ) ∧ ∪ 𝑗 = ∪ 𝑦 ) ∧ 𝑧 ∈ ( 𝒫 𝑗 ∩ Fin ) ) ∧ 𝑧 Ref 𝑦 ) → ( ( 𝑓 : 𝑧 ⟶ 𝑦 ∧ ∀ 𝑢 ∈ 𝑧 𝑢 ⊆ ( 𝑓 ‘ 𝑢 ) ) → ∃ 𝑥 ∈ ( 𝒫 𝑦 ∩ Fin ) ∪ 𝑗 = ∪ 𝑥 ) )
75 74 exlimdv ⊢ ( ( ( ( ( 𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗 ) ∧ ∪ 𝑗 = ∪ 𝑦 ) ∧ 𝑧 ∈ ( 𝒫 𝑗 ∩ Fin ) ) ∧ 𝑧 Ref 𝑦 ) → ( ∃ 𝑓 ( 𝑓 : 𝑧 ⟶ 𝑦 ∧ ∀ 𝑢 ∈ 𝑧 𝑢 ⊆ ( 𝑓 ‘ 𝑢 ) ) → ∃ 𝑥 ∈ ( 𝒫 𝑦 ∩ Fin ) ∪ 𝑗 = ∪ 𝑥 ) )
76 34 75 mpd ⊢ ( ( ( ( ( 𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗 ) ∧ ∪ 𝑗 = ∪ 𝑦 ) ∧ 𝑧 ∈ ( 𝒫 𝑗 ∩ Fin ) ) ∧ 𝑧 Ref 𝑦 ) → ∃ 𝑥 ∈ ( 𝒫 𝑦 ∩ Fin ) ∪ 𝑗 = ∪ 𝑥 )
77 76 r19.29an ⊢ ( ( ( ( 𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗 ) ∧ ∪ 𝑗 = ∪ 𝑦 ) ∧ ∃ 𝑧 ∈ ( 𝒫 𝑗 ∩ Fin ) 𝑧 Ref 𝑦 ) → ∃ 𝑥 ∈ ( 𝒫 𝑦 ∩ Fin ) ∪ 𝑗 = ∪ 𝑥 )
78 24 77 impbida ⊢ ( ( ( 𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗 ) ∧ ∪ 𝑗 = ∪ 𝑦 ) → ( ∃ 𝑥 ∈ ( 𝒫 𝑦 ∩ Fin ) ∪ 𝑗 = ∪ 𝑥 ↔ ∃ 𝑧 ∈ ( 𝒫 𝑗 ∩ Fin ) 𝑧 Ref 𝑦 ) )
79 78 pm5.74da ⊢ ( ( 𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗 ) → ( ( ∪ 𝑗 = ∪ 𝑦 → ∃ 𝑥 ∈ ( 𝒫 𝑦 ∩ Fin ) ∪ 𝑗 = ∪ 𝑥 ) ↔ ( ∪ 𝑗 = ∪ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝑗 ∩ Fin ) 𝑧 Ref 𝑦 ) ) )
80 79 ralbidva ⊢ ( 𝑗 ∈ Top → ( ∀ 𝑦 ∈ 𝒫 𝑗 ( ∪ 𝑗 = ∪ 𝑦 → ∃ 𝑥 ∈ ( 𝒫 𝑦 ∩ Fin ) ∪ 𝑗 = ∪ 𝑥 ) ↔ ∀ 𝑦 ∈ 𝒫 𝑗 ( ∪ 𝑗 = ∪ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝑗 ∩ Fin ) 𝑧 Ref 𝑦 ) ) )
81 80 pm5.32i ⊢ ( ( 𝑗 ∈ Top ∧ ∀ 𝑦 ∈ 𝒫 𝑗 ( ∪ 𝑗 = ∪ 𝑦 → ∃ 𝑥 ∈ ( 𝒫 𝑦 ∩ Fin ) ∪ 𝑗 = ∪ 𝑥 ) ) ↔ ( 𝑗 ∈ Top ∧ ∀ 𝑦 ∈ 𝒫 𝑗 ( ∪ 𝑗 = ∪ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝑗 ∩ Fin ) 𝑧 Ref 𝑦 ) ) )
82 eqid ⊢ ∪ 𝑗 = ∪ 𝑗
83 82 iscmp ⊢ ( 𝑗 ∈ Comp ↔ ( 𝑗 ∈ Top ∧ ∀ 𝑦 ∈ 𝒫 𝑗 ( ∪ 𝑗 = ∪ 𝑦 → ∃ 𝑥 ∈ ( 𝒫 𝑦 ∩ Fin ) ∪ 𝑗 = ∪ 𝑥 ) ) )
84 82 iscref ⊢ ( 𝑗 ∈ CovHasRef Fin ↔ ( 𝑗 ∈ Top ∧ ∀ 𝑦 ∈ 𝒫 𝑗 ( ∪ 𝑗 = ∪ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝑗 ∩ Fin ) 𝑧 Ref 𝑦 ) ) )
85 81 83 84 3bitr4i ⊢ ( 𝑗 ∈ Comp ↔ 𝑗 ∈ CovHasRef Fin )
86 85 eqriv ⊢ Comp = CovHasRef Fin