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) Remove dependency on ax-reg and ax-inf2 . (Revised by Timothy J. O'Malley, 15-Oct-2026)

Ref Expression
Assertion cmpcref Comp = CovHasRef Fin

Proof

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