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 
 |-  ( z = x -> ( z Ref y <-> x Ref y ) )
2 simplr 
 |-  ( ( ( ( ( j e. Top /\ y e. ~P j ) /\ U. j = U. y ) /\ x e. ( ~P y i^i Fin ) ) /\ U. j = U. x ) -> x e. ( ~P y i^i Fin ) )
3 2 elin1d 
 |-  ( ( ( ( ( j e. Top /\ y e. ~P j ) /\ U. j = U. y ) /\ x e. ( ~P y i^i Fin ) ) /\ U. j = U. x ) -> x e. ~P y )
4 3 elpwid 
 |-  ( ( ( ( ( j e. Top /\ y e. ~P j ) /\ U. j = U. y ) /\ x e. ( ~P y i^i Fin ) ) /\ U. j = U. x ) -> x C_ y )
5 elpwi 
 |-  ( y e. ~P j -> y C_ j )
6 5 ad4antlr 
 |-  ( ( ( ( ( j e. Top /\ y e. ~P j ) /\ U. j = U. y ) /\ x e. ( ~P y i^i Fin ) ) /\ U. j = U. x ) -> y C_ j )
7 4 6 sstrd 
 |-  ( ( ( ( ( j e. Top /\ y e. ~P j ) /\ U. j = U. y ) /\ x e. ( ~P y i^i Fin ) ) /\ U. j = U. x ) -> x C_ j )
8 velpw 
 |-  ( x e. ~P j <-> x C_ j )
9 7 8 sylibr 
 |-  ( ( ( ( ( j e. Top /\ y e. ~P j ) /\ U. j = U. y ) /\ x e. ( ~P y i^i Fin ) ) /\ U. j = U. x ) -> x e. ~P j )
10 2 elin2d 
 |-  ( ( ( ( ( j e. Top /\ y e. ~P j ) /\ U. j = U. y ) /\ x e. ( ~P y i^i Fin ) ) /\ U. j = U. x ) -> x e. Fin )
11 9 10 elind 
 |-  ( ( ( ( ( j e. Top /\ y e. ~P j ) /\ U. j = U. y ) /\ x e. ( ~P y i^i Fin ) ) /\ U. j = U. x ) -> x e. ( ~P j i^i Fin ) )
12 simpr 
 |-  ( ( ( ( ( j e. Top /\ y e. ~P j ) /\ U. j = U. y ) /\ x e. ( ~P y i^i Fin ) ) /\ U. j = U. x ) -> U. j = U. x )
13 simpllr 
 |-  ( ( ( ( ( j e. Top /\ y e. ~P j ) /\ U. j = U. y ) /\ x e. ( ~P y i^i Fin ) ) /\ U. j = U. x ) -> U. j = U. y )
14 12 13 eqtr3d 
 |-  ( ( ( ( ( j e. Top /\ y e. ~P j ) /\ U. j = U. y ) /\ x e. ( ~P y i^i Fin ) ) /\ U. j = U. x ) -> U. x = U. y )
15 eqid 
 |-  U. x = U. x
16 eqid 
 |-  U. y = U. y
17 15 16 ssref 
 |-  ( ( x e. ~P j /\ x C_ y /\ U. x = U. y ) -> x Ref y )
18 9 4 14 17 syl3anc 
 |-  ( ( ( ( ( j e. Top /\ y e. ~P j ) /\ U. j = U. y ) /\ x e. ( ~P y i^i Fin ) ) /\ U. j = U. x ) -> x Ref y )
19 1 11 18 rspcedvdw 
 |-  ( ( ( ( ( j e. Top /\ y e. ~P j ) /\ U. j = U. y ) /\ x e. ( ~P y i^i Fin ) ) /\ U. j = U. x ) -> E. z e. ( ~P j i^i Fin ) z Ref y )
20 19 r19.29an 
 |-  ( ( ( ( j e. Top /\ y e. ~P j ) /\ U. j = U. y ) /\ E. x e. ( ~P y i^i Fin ) U. j = U. x ) -> E. z e. ( ~P j i^i Fin ) z Ref y )
21 simplr 
 |-  ( ( ( ( ( j e. Top /\ y e. ~P j ) /\ U. j = U. y ) /\ z e. ( ~P j i^i Fin ) ) /\ z Ref y ) -> z e. ( ~P j i^i Fin ) )
22 vex 
 |-  y e. _V
23 22 a1i 
 |-  ( ( ( ( ( j e. Top /\ y e. ~P j ) /\ U. j = U. y ) /\ z e. ( ~P j i^i Fin ) ) /\ z Ref y ) -> y e. _V )
24 eqid 
 |-  U. z = U. z
25 24 16 isref 
 |-  ( z e. _V -> ( z Ref y <-> ( U. y = U. z /\ A. u e. z E. v e. y u C_ v ) ) )
26 25 elv 
 |-  ( z Ref y <-> ( U. y = U. z /\ A. u e. z E. v e. y u C_ v ) )
27 26 simprbi 
 |-  ( z Ref y -> A. u e. z E. v e. y u C_ v )
28 27 adantl 
 |-  ( ( ( ( ( j e. Top /\ y e. ~P j ) /\ U. j = U. y ) /\ z e. ( ~P j i^i Fin ) ) /\ z Ref y ) -> A. u e. z E. v e. y u C_ v )
29 sseq2 
 |-  ( v = ( f ` u ) -> ( u C_ v <-> u C_ ( f ` u ) ) )
30 29 ac6 
 |-  ( ( z e. ( ~P j i^i Fin ) /\ y e. _V /\ A. u e. z E. v e. y u C_ v ) -> E. f ( f : z --> y /\ A. u e. z u C_ ( f ` u ) ) )
31 21 23 28 30 syl3anc 
 |-  ( ( ( ( ( j e. Top /\ y e. ~P j ) /\ U. j = U. y ) /\ z e. ( ~P j i^i Fin ) ) /\ z Ref y ) -> E. f ( f : z --> y /\ A. u e. z u C_ ( f ` u ) ) )
32 simplr 
 |-  ( ( ( ( ( ( ( j e. Top /\ y e. ~P j ) /\ U. j = U. y ) /\ z e. ( ~P j i^i Fin ) ) /\ z Ref y ) /\ f : z --> y ) /\ A. u e. z u C_ ( f ` u ) ) -> f : z --> y )
33 32 ffnd 
 |-  ( ( ( ( ( ( ( j e. Top /\ y e. ~P j ) /\ U. j = U. y ) /\ z e. ( ~P j i^i Fin ) ) /\ z Ref y ) /\ f : z --> y ) /\ A. u e. z u C_ ( f ` u ) ) -> f Fn z )
34 elinel2 
 |-  ( z e. ( ~P j i^i Fin ) -> z e. Fin )
35 34 ad4antlr 
 |-  ( ( ( ( ( ( ( j e. Top /\ y e. ~P j ) /\ U. j = U. y ) /\ z e. ( ~P j i^i Fin ) ) /\ z Ref y ) /\ f : z --> y ) /\ A. u e. z u C_ ( f ` u ) ) -> z e. Fin )
36 fnfi 
 |-  ( ( f Fn z /\ z e. Fin ) -> f e. Fin )
37 33 35 36 syl2anc 
 |-  ( ( ( ( ( ( ( j e. Top /\ y e. ~P j ) /\ U. j = U. y ) /\ z e. ( ~P j i^i Fin ) ) /\ z Ref y ) /\ f : z --> y ) /\ A. u e. z u C_ ( f ` u ) ) -> f e. Fin )
38 rnfi 
 |-  ( f e. Fin -> ran f e. Fin )
39 37 38 syl 
 |-  ( ( ( ( ( ( ( j e. Top /\ y e. ~P j ) /\ U. j = U. y ) /\ z e. ( ~P j i^i Fin ) ) /\ z Ref y ) /\ f : z --> y ) /\ A. u e. z u C_ ( f ` u ) ) -> ran f e. Fin )
40 32 frnd 
 |-  ( ( ( ( ( ( ( j e. Top /\ y e. ~P j ) /\ U. j = U. y ) /\ z e. ( ~P j i^i Fin ) ) /\ z Ref y ) /\ f : z --> y ) /\ A. u e. z u C_ ( f ` u ) ) -> ran f C_ y )
41 39 40 elpwd 
 |-  ( ( ( ( ( ( ( j e. Top /\ y e. ~P j ) /\ U. j = U. y ) /\ z e. ( ~P j i^i Fin ) ) /\ z Ref y ) /\ f : z --> y ) /\ A. u e. z u C_ ( f ` u ) ) -> ran f e. ~P y )
42 41 39 elind 
 |-  ( ( ( ( ( ( ( j e. Top /\ y e. ~P j ) /\ U. j = U. y ) /\ z e. ( ~P j i^i Fin ) ) /\ z Ref y ) /\ f : z --> y ) /\ A. u e. z u C_ ( f ` u ) ) -> ran f e. ( ~P y i^i Fin ) )
43 simp-5r 
 |-  ( ( ( ( ( ( ( j e. Top /\ y e. ~P j ) /\ U. j = U. y ) /\ z e. ( ~P j i^i Fin ) ) /\ z Ref y ) /\ f : z --> y ) /\ A. u e. z u C_ ( f ` u ) ) -> U. j = U. y )
44 24 16 refbas 
 |-  ( z Ref y -> U. y = U. z )
45 44 ad3antlr 
 |-  ( ( ( ( ( ( ( j e. Top /\ y e. ~P j ) /\ U. j = U. y ) /\ z e. ( ~P j i^i Fin ) ) /\ z Ref y ) /\ f : z --> y ) /\ A. u e. z u C_ ( f ` u ) ) -> U. y = U. z )
46 nfv 
 |-  F/ u ( ( ( ( ( j e. Top /\ y e. ~P j ) /\ U. j = U. y ) /\ z e. ( ~P j i^i Fin ) ) /\ z Ref y ) /\ f : z --> y )
47 nfra1 
 |-  F/ u A. u e. z u C_ ( f ` u )
48 46 47 nfan 
 |-  F/ u ( ( ( ( ( ( j e. Top /\ y e. ~P j ) /\ U. j = U. y ) /\ z e. ( ~P j i^i Fin ) ) /\ z Ref y ) /\ f : z --> y ) /\ A. u e. z u C_ ( f ` u ) )
49 rspa 
 |-  ( ( A. u e. z u C_ ( f ` u ) /\ u e. z ) -> u C_ ( f ` u ) )
50 49 adantll 
 |-  ( ( ( ( ( ( ( ( j e. Top /\ y e. ~P j ) /\ U. j = U. y ) /\ z e. ( ~P j i^i Fin ) ) /\ z Ref y ) /\ f : z --> y ) /\ A. u e. z u C_ ( f ` u ) ) /\ u e. z ) -> u C_ ( f ` u ) )
51 50 sseld 
 |-  ( ( ( ( ( ( ( ( j e. Top /\ y e. ~P j ) /\ U. j = U. y ) /\ z e. ( ~P j i^i Fin ) ) /\ z Ref y ) /\ f : z --> y ) /\ A. u e. z u C_ ( f ` u ) ) /\ u e. z ) -> ( x e. u -> x e. ( f ` u ) ) )
52 51 ex 
 |-  ( ( ( ( ( ( ( j e. Top /\ y e. ~P j ) /\ U. j = U. y ) /\ z e. ( ~P j i^i Fin ) ) /\ z Ref y ) /\ f : z --> y ) /\ A. u e. z u C_ ( f ` u ) ) -> ( u e. z -> ( x e. u -> x e. ( f ` u ) ) ) )
53 48 52 reximdai 
 |-  ( ( ( ( ( ( ( j e. Top /\ y e. ~P j ) /\ U. j = U. y ) /\ z e. ( ~P j i^i Fin ) ) /\ z Ref y ) /\ f : z --> y ) /\ A. u e. z u C_ ( f ` u ) ) -> ( E. u e. z x e. u -> E. u e. z x e. ( f ` u ) ) )
54 eluni2 
 |-  ( x e. U. z <-> E. u e. z x e. u )
55 54 a1i 
 |-  ( ( ( ( ( ( ( j e. Top /\ y e. ~P j ) /\ U. j = U. y ) /\ z e. ( ~P j i^i Fin ) ) /\ z Ref y ) /\ f : z --> y ) /\ A. u e. z u C_ ( f ` u ) ) -> ( x e. U. z <-> E. u e. z x e. u ) )
56 fnunirn 
 |-  ( f Fn z -> ( x e. U. ran f <-> E. u e. z x e. ( f ` u ) ) )
57 33 56 syl 
 |-  ( ( ( ( ( ( ( j e. Top /\ y e. ~P j ) /\ U. j = U. y ) /\ z e. ( ~P j i^i Fin ) ) /\ z Ref y ) /\ f : z --> y ) /\ A. u e. z u C_ ( f ` u ) ) -> ( x e. U. ran f <-> E. u e. z x e. ( f ` u ) ) )
58 53 55 57 3imtr4d 
 |-  ( ( ( ( ( ( ( j e. Top /\ y e. ~P j ) /\ U. j = U. y ) /\ z e. ( ~P j i^i Fin ) ) /\ z Ref y ) /\ f : z --> y ) /\ A. u e. z u C_ ( f ` u ) ) -> ( x e. U. z -> x e. U. ran f ) )
59 58 ssrdv 
 |-  ( ( ( ( ( ( ( j e. Top /\ y e. ~P j ) /\ U. j = U. y ) /\ z e. ( ~P j i^i Fin ) ) /\ z Ref y ) /\ f : z --> y ) /\ A. u e. z u C_ ( f ` u ) ) -> U. z C_ U. ran f )
60 45 59 eqsstrd 
 |-  ( ( ( ( ( ( ( j e. Top /\ y e. ~P j ) /\ U. j = U. y ) /\ z e. ( ~P j i^i Fin ) ) /\ z Ref y ) /\ f : z --> y ) /\ A. u e. z u C_ ( f ` u ) ) -> U. y C_ U. ran f )
61 40 unissd 
 |-  ( ( ( ( ( ( ( j e. Top /\ y e. ~P j ) /\ U. j = U. y ) /\ z e. ( ~P j i^i Fin ) ) /\ z Ref y ) /\ f : z --> y ) /\ A. u e. z u C_ ( f ` u ) ) -> U. ran f C_ U. y )
62 60 61 eqssd 
 |-  ( ( ( ( ( ( ( j e. Top /\ y e. ~P j ) /\ U. j = U. y ) /\ z e. ( ~P j i^i Fin ) ) /\ z Ref y ) /\ f : z --> y ) /\ A. u e. z u C_ ( f ` u ) ) -> U. y = U. ran f )
63 43 62 eqtrd 
 |-  ( ( ( ( ( ( ( j e. Top /\ y e. ~P j ) /\ U. j = U. y ) /\ z e. ( ~P j i^i Fin ) ) /\ z Ref y ) /\ f : z --> y ) /\ A. u e. z u C_ ( f ` u ) ) -> U. j = U. ran f )
64 unieq 
 |-  ( x = ran f -> U. x = U. ran f )
65 64 rspceeqv 
 |-  ( ( ran f e. ( ~P y i^i Fin ) /\ U. j = U. ran f ) -> E. x e. ( ~P y i^i Fin ) U. j = U. x )
66 42 63 65 syl2anc 
 |-  ( ( ( ( ( ( ( j e. Top /\ y e. ~P j ) /\ U. j = U. y ) /\ z e. ( ~P j i^i Fin ) ) /\ z Ref y ) /\ f : z --> y ) /\ A. u e. z u C_ ( f ` u ) ) -> E. x e. ( ~P y i^i Fin ) U. j = U. x )
67 66 expl 
 |-  ( ( ( ( ( j e. Top /\ y e. ~P j ) /\ U. j = U. y ) /\ z e. ( ~P j i^i Fin ) ) /\ z Ref y ) -> ( ( f : z --> y /\ A. u e. z u C_ ( f ` u ) ) -> E. x e. ( ~P y i^i Fin ) U. j = U. x ) )
68 67 exlimdv 
 |-  ( ( ( ( ( j e. Top /\ y e. ~P j ) /\ U. j = U. y ) /\ z e. ( ~P j i^i Fin ) ) /\ z Ref y ) -> ( E. f ( f : z --> y /\ A. u e. z u C_ ( f ` u ) ) -> E. x e. ( ~P y i^i Fin ) U. j = U. x ) )
69 31 68 mpd 
 |-  ( ( ( ( ( j e. Top /\ y e. ~P j ) /\ U. j = U. y ) /\ z e. ( ~P j i^i Fin ) ) /\ z Ref y ) -> E. x e. ( ~P y i^i Fin ) U. j = U. x )
70 69 r19.29an 
 |-  ( ( ( ( j e. Top /\ y e. ~P j ) /\ U. j = U. y ) /\ E. z e. ( ~P j i^i Fin ) z Ref y ) -> E. x e. ( ~P y i^i Fin ) U. j = U. x )
71 20 70 impbida 
 |-  ( ( ( j e. Top /\ y e. ~P j ) /\ U. j = U. y ) -> ( E. x e. ( ~P y i^i Fin ) U. j = U. x <-> E. z e. ( ~P j i^i Fin ) z Ref y ) )
72 71 pm5.74da 
 |-  ( ( j e. Top /\ y e. ~P j ) -> ( ( U. j = U. y -> E. x e. ( ~P y i^i Fin ) U. j = U. x ) <-> ( U. j = U. y -> E. z e. ( ~P j i^i Fin ) z Ref y ) ) )
73 72 ralbidva 
 |-  ( j e. Top -> ( A. y e. ~P j ( U. j = U. y -> E. x e. ( ~P y i^i Fin ) U. j = U. x ) <-> A. y e. ~P j ( U. j = U. y -> E. z e. ( ~P j i^i Fin ) z Ref y ) ) )
74 73 pm5.32i 
 |-  ( ( j e. Top /\ A. y e. ~P j ( U. j = U. y -> E. x e. ( ~P y i^i Fin ) U. j = U. x ) ) <-> ( j e. Top /\ A. y e. ~P j ( U. j = U. y -> E. z e. ( ~P j i^i Fin ) z Ref y ) ) )
75 eqid 
 |-  U. j = U. j
76 75 iscmp 
 |-  ( j e. Comp <-> ( j e. Top /\ A. y e. ~P j ( U. j = U. y -> E. x e. ( ~P y i^i Fin ) U. j = U. x ) ) )
77 75 iscref 
 |-  ( j e. CovHasRef Fin <-> ( j e. Top /\ A. y e. ~P j ( U. j = U. y -> E. z e. ( ~P j i^i Fin ) z Ref y ) ) )
78 74 76 77 3bitr4i 
 |-  ( j e. Comp <-> j e. CovHasRef Fin )
79 78 eqriv 
 |-  Comp = CovHasRef Fin