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 
 |-  ( ( ( ( ( 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 ) )
2 elin 
 |-  ( x e. ( ~P y i^i Fin ) <-> ( x e. ~P y /\ x e. Fin ) )
3 1 2 sylib 
 |-  ( ( ( ( ( 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 /\ x e. Fin ) )
4 3 simpld 
 |-  ( ( ( ( ( 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 )
5 elpwi 
 |-  ( x e. ~P y -> x C_ y )
6 4 5 syl 
 |-  ( ( ( ( ( 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 )
7 elpwi 
 |-  ( y e. ~P j -> y C_ j )
8 7 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 )
9 6 8 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 )
10 velpw 
 |-  ( x e. ~P j <-> x C_ j )
11 9 10 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 )
12 3 simprd 
 |-  ( ( ( ( ( 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 )
13 11 12 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 ) )
14 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 )
15 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 )
16 14 15 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 )
17 eqid 
 |-  U. x = U. x
18 eqid 
 |-  U. y = U. y
19 17 18 ssref 
 |-  ( ( x e. ~P j /\ x C_ y /\ U. x = U. y ) -> x Ref y )
20 11 6 16 19 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 )
21 breq1 
 |-  ( z = x -> ( z Ref y <-> x Ref y ) )
22 21 rspcev 
 |-  ( ( x e. ( ~P j i^i Fin ) /\ x Ref y ) -> E. z e. ( ~P j i^i Fin ) z Ref y )
23 13 20 22 syl2anc 
 |-  ( ( ( ( ( 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 )
24 23 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 )
25 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 ) )
26 vex 
 |-  z e. _V
27 eqid 
 |-  U. z = U. z
28 27 18 isref 
 |-  ( z e. _V -> ( z Ref y <-> ( U. y = U. z /\ A. u e. z E. v e. y u C_ v ) ) )
29 26 28 ax-mp 
 |-  ( z Ref y <-> ( U. y = U. z /\ A. u e. z E. v e. y u C_ v ) )
30 29 simprbi 
 |-  ( z Ref y -> A. u e. z E. v e. y u C_ v )
31 30 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 )
32 sseq2 
 |-  ( v = ( f ` u ) -> ( u C_ v <-> u C_ ( f ` u ) ) )
33 32 ac6sg 
 |-  ( z e. ( ~P j i^i Fin ) -> ( A. u e. z E. v e. y u C_ v -> E. f ( f : z --> y /\ A. u e. z u C_ ( f ` u ) ) ) )
34 25 31 33 sylc 
 |-  ( ( ( ( ( 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 ) ) )
35 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 )
36 35 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 )
37 vex 
 |-  f e. _V
38 37 rnex 
 |-  ran f e. _V
39 38 elpw 
 |-  ( ran f e. ~P y <-> ran f C_ y )
40 36 39 sylibr 
 |-  ( ( ( ( ( ( ( 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 )
41 35 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 )
42 elin 
 |-  ( z e. ( ~P j i^i Fin ) <-> ( z e. ~P j /\ z e. Fin ) )
43 42 simprbi 
 |-  ( z e. ( ~P j i^i Fin ) -> z e. Fin )
44 43 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 )
45 fnfi 
 |-  ( ( f Fn z /\ z e. Fin ) -> f e. Fin )
46 41 44 45 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 )
47 rnfi 
 |-  ( f e. Fin -> ran f e. Fin )
48 46 47 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 )
49 40 48 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 ) )
50 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 )
51 27 18 refbas 
 |-  ( z Ref y -> U. y = U. z )
52 51 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 )
53 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 )
54 nfra1 
 |-  F/ u A. u e. z u C_ ( f ` u )
55 53 54 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 ) )
56 rspa 
 |-  ( ( A. u e. z u C_ ( f ` u ) /\ u e. z ) -> u C_ ( f ` u ) )
57 56 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 ) )
58 57 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 ) ) )
59 58 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 ) ) ) )
60 55 59 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 ) ) )
61 eluni2 
 |-  ( x e. U. z <-> E. u e. z x e. u )
62 61 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 ) )
63 fnunirn 
 |-  ( f Fn z -> ( x e. U. ran f <-> E. u e. z x e. ( f ` u ) ) )
64 41 63 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 ) ) )
65 60 62 64 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 ) )
66 65 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 )
67 52 66 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 )
68 36 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 )
69 67 68 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 )
70 50 69 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 )
71 unieq 
 |-  ( x = ran f -> U. x = U. ran f )
72 71 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 )
73 49 70 72 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 )
74 73 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 ) )
75 74 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 ) )
76 34 75 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 )
77 76 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 )
78 24 77 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 ) )
79 78 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 ) ) )
80 79 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 ) ) )
81 80 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 ) ) )
82 eqid 
 |-  U. j = U. j
83 82 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 ) ) )
84 82 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 ) ) )
85 81 83 84 3bitr4i 
 |-  ( j e. Comp <-> j e. CovHasRef Fin )
86 85 eqriv 
 |-  Comp = CovHasRef Fin