Metamath Proof Explorer

Theorem ptcmpg

Description: Tychonoff's theorem: The product of compact spaces is compact. The choice principles needed are encoded in the last hypothesis: the base set of the product must be well-orderable and satisfy the ultrafilter lemma. Both these assumptions are satisfied if ~P ~P X is well-orderable, so if we assume the Axiom of Choice we can eliminate them (see ptcmp ). (Contributed by Mario Carneiro, 27-Aug-2015)

Ref Expression
Hypotheses ptcmpg.1 
|- J = ( Xt_ ` F )
ptcmpg.2 
|- X = U. J
Assertion ptcmpg 
|- ( ( A e. V /\ F : A --> Comp /\ X e. ( UFL i^i dom card ) ) -> J e. Comp )

Proof

Step Hyp Ref Expression
1 ptcmpg.1 
 |-  J = ( Xt_ ` F )
2 ptcmpg.2 
 |-  X = U. J
3 nfcv 
 |-  F/_ k ( F ` a )
4 nfcv 
 |-  F/_ a ( F ` k )
5 nfcv 
 |-  F/_ k ( `' ( w e. X_ n e. A U. ( F ` n ) |-> ( w ` a ) ) " b )
6 nfcv 
 |-  F/_ u ( `' ( w e. X_ n e. A U. ( F ` n ) |-> ( w ` a ) ) " b )
7 nfcv 
 |-  F/_ a ( `' ( w e. X_ n e. A U. ( F ` n ) |-> ( w ` k ) ) " u )
8 nfcv 
 |-  F/_ b ( `' ( w e. X_ n e. A U. ( F ` n ) |-> ( w ` k ) ) " u )
9 fveq2 
 |-  ( a = k -> ( F ` a ) = ( F ` k ) )
10 fveq2 
 |-  ( a = k -> ( w ` a ) = ( w ` k ) )
11 10 mpteq2dv 
 |-  ( a = k -> ( w e. X_ n e. A U. ( F ` n ) |-> ( w ` a ) ) = ( w e. X_ n e. A U. ( F ` n ) |-> ( w ` k ) ) )
12 11 cnveqd 
 |-  ( a = k -> `' ( w e. X_ n e. A U. ( F ` n ) |-> ( w ` a ) ) = `' ( w e. X_ n e. A U. ( F ` n ) |-> ( w ` k ) ) )
13 12 imaeq1d 
 |-  ( a = k -> ( `' ( w e. X_ n e. A U. ( F ` n ) |-> ( w ` a ) ) " b ) = ( `' ( w e. X_ n e. A U. ( F ` n ) |-> ( w ` k ) ) " b ) )
14 imaeq2 
 |-  ( b = u -> ( `' ( w e. X_ n e. A U. ( F ` n ) |-> ( w ` k ) ) " b ) = ( `' ( w e. X_ n e. A U. ( F ` n ) |-> ( w ` k ) ) " u ) )
15 13 14 sylan9eq 
 |-  ( ( a = k /\ b = u ) -> ( `' ( w e. X_ n e. A U. ( F ` n ) |-> ( w ` a ) ) " b ) = ( `' ( w e. X_ n e. A U. ( F ` n ) |-> ( w ` k ) ) " u ) )
16 3 4 5 6 7 8 9 15 cbvmpox 
 |-  ( a e. A , b e. ( F ` a ) |-> ( `' ( w e. X_ n e. A U. ( F ` n ) |-> ( w ` a ) ) " b ) ) = ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X_ n e. A U. ( F ` n ) |-> ( w ` k ) ) " u ) )
17 fveq2 
 |-  ( n = m -> ( F ` n ) = ( F ` m ) )
18 17 unieqd 
 |-  ( n = m -> U. ( F ` n ) = U. ( F ` m ) )
19 18 cbvixpv 
 |-  X_ n e. A U. ( F ` n ) = X_ m e. A U. ( F ` m )
20 simp1 
 |-  ( ( A e. V /\ F : A --> Comp /\ X e. ( UFL i^i dom card ) ) -> A e. V )
21 simp2 
 |-  ( ( A e. V /\ F : A --> Comp /\ X e. ( UFL i^i dom card ) ) -> F : A --> Comp )
22 cmptop 
 |-  ( k e. Comp -> k e. Top )
23 22 ssriv 
 |-  Comp C_ Top
24 fss 
 |-  ( ( F : A --> Comp /\ Comp C_ Top ) -> F : A --> Top )
25 21 23 24 sylancl 
 |-  ( ( A e. V /\ F : A --> Comp /\ X e. ( UFL i^i dom card ) ) -> F : A --> Top )
26 1 ptuni 
 |-  ( ( A e. V /\ F : A --> Top ) -> X_ n e. A U. ( F ` n ) = U. J )
27 20 25 26 syl2anc 
 |-  ( ( A e. V /\ F : A --> Comp /\ X e. ( UFL i^i dom card ) ) -> X_ n e. A U. ( F ` n ) = U. J )
28 27 2 eqtr4di 
 |-  ( ( A e. V /\ F : A --> Comp /\ X e. ( UFL i^i dom card ) ) -> X_ n e. A U. ( F ` n ) = X )
29 simp3 
 |-  ( ( A e. V /\ F : A --> Comp /\ X e. ( UFL i^i dom card ) ) -> X e. ( UFL i^i dom card ) )
30 28 29 eqeltrd 
 |-  ( ( A e. V /\ F : A --> Comp /\ X e. ( UFL i^i dom card ) ) -> X_ n e. A U. ( F ` n ) e. ( UFL i^i dom card ) )
31 16 19 20 21 30 ptcmplem5 
 |-  ( ( A e. V /\ F : A --> Comp /\ X e. ( UFL i^i dom card ) ) -> ( Xt_ ` F ) e. Comp )
32 1 31 eqeltrid 
 |-  ( ( A e. V /\ F : A --> Comp /\ X e. ( UFL i^i dom card ) ) -> J e. Comp )