This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ptcmplem1

Description: Lemma for ptcmp . (Contributed by Mario Carneiro, 26-Aug-2015)

Ref Expression
Hypotheses ptcmp.1 
|- S = ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) )
ptcmp.2 
|- X = X_ n e. A U. ( F ` n )
ptcmp.3 
|- ( ph -> A e. V )
ptcmp.4 
|- ( ph -> F : A --> Comp )
ptcmp.5 
|- ( ph -> X e. ( UFL i^i dom card ) )
Assertion ptcmplem1 
|- ( ph -> ( X = U. ( ran S u. { X } ) /\ ( Xt_ ` F ) = ( topGen ` ( fi ` ( ran S u. { X } ) ) ) ) )

Proof

Step Hyp Ref Expression
1 ptcmp.1 
 |-  S = ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) )
2 ptcmp.2 
 |-  X = X_ n e. A U. ( F ` n )
3 ptcmp.3 
 |-  ( ph -> A e. V )
4 ptcmp.4 
 |-  ( ph -> F : A --> Comp )
5 ptcmp.5 
 |-  ( ph -> X e. ( UFL i^i dom card ) )
6 4 ffnd 
 |-  ( ph -> F Fn A )
7 eqid 
 |-  { x | E. g ( ( g Fn A /\ A. y e. A ( g ` y ) e. ( F ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( F ` y ) ) /\ x = X_ y e. A ( g ` y ) ) } = { x | E. g ( ( g Fn A /\ A. y e. A ( g ` y ) e. ( F ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( F ` y ) ) /\ x = X_ y e. A ( g ` y ) ) }
8 7 ptval 
 |-  ( ( A e. V /\ F Fn A ) -> ( Xt_ ` F ) = ( topGen ` { x | E. g ( ( g Fn A /\ A. y e. A ( g ` y ) e. ( F ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( F ` y ) ) /\ x = X_ y e. A ( g ` y ) ) } ) )
9 3 6 8 syl2anc 
 |-  ( ph -> ( Xt_ ` F ) = ( topGen ` { x | E. g ( ( g Fn A /\ A. y e. A ( g ` y ) e. ( F ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( F ` y ) ) /\ x = X_ y e. A ( g ` y ) ) } ) )
10 cmptop 
 |-  ( x e. Comp -> x e. Top )
11 10 ssriv 
 |-  Comp C_ Top
12 fss 
 |-  ( ( F : A --> Comp /\ Comp C_ Top ) -> F : A --> Top )
13 4 11 12 sylancl 
 |-  ( ph -> F : A --> Top )
14 7 2 ptbasfi 
 |-  ( ( A e. V /\ F : A --> Top ) -> { x | E. g ( ( g Fn A /\ A. y e. A ( g ` y ) e. ( F ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( F ` y ) ) /\ x = X_ y e. A ( g ` y ) ) } = ( fi ` ( { X } u. ran ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) ) ) ) )
15 3 13 14 syl2anc 
 |-  ( ph -> { x | E. g ( ( g Fn A /\ A. y e. A ( g ` y ) e. ( F ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( F ` y ) ) /\ x = X_ y e. A ( g ` y ) ) } = ( fi ` ( { X } u. ran ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) ) ) ) )
16 uncom 
 |-  ( ran S u. { X } ) = ( { X } u. ran S )
17 1 rneqi 
 |-  ran S = ran ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) )
18 17 uneq2i 
 |-  ( { X } u. ran S ) = ( { X } u. ran ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) ) )
19 16 18 eqtri 
 |-  ( ran S u. { X } ) = ( { X } u. ran ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) ) )
20 19 fveq2i 
 |-  ( fi ` ( ran S u. { X } ) ) = ( fi ` ( { X } u. ran ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) ) ) )
21 15 20 eqtr4di 
 |-  ( ph -> { x | E. g ( ( g Fn A /\ A. y e. A ( g ` y ) e. ( F ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( F ` y ) ) /\ x = X_ y e. A ( g ` y ) ) } = ( fi ` ( ran S u. { X } ) ) )
22 21 fveq2d 
 |-  ( ph -> ( topGen ` { x | E. g ( ( g Fn A /\ A. y e. A ( g ` y ) e. ( F ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( F ` y ) ) /\ x = X_ y e. A ( g ` y ) ) } ) = ( topGen ` ( fi ` ( ran S u. { X } ) ) ) )
23 9 22 eqtrd 
 |-  ( ph -> ( Xt_ ` F ) = ( topGen ` ( fi ` ( ran S u. { X } ) ) ) )
24 23 unieqd 
 |-  ( ph -> U. ( Xt_ ` F ) = U. ( topGen ` ( fi ` ( ran S u. { X } ) ) ) )
25 fibas 
 |-  ( fi ` ( ran S u. { X } ) ) e. TopBases
26 unitg 
 |-  ( ( fi ` ( ran S u. { X } ) ) e. TopBases -> U. ( topGen ` ( fi ` ( ran S u. { X } ) ) ) = U. ( fi ` ( ran S u. { X } ) ) )
27 25 26 ax-mp 
 |-  U. ( topGen ` ( fi ` ( ran S u. { X } ) ) ) = U. ( fi ` ( ran S u. { X } ) )
28 24 27 eqtrdi 
 |-  ( ph -> U. ( Xt_ ` F ) = U. ( fi ` ( ran S u. { X } ) ) )
29 eqid 
 |-  ( Xt_ ` F ) = ( Xt_ ` F )
30 29 ptuni 
 |-  ( ( A e. V /\ F : A --> Top ) -> X_ n e. A U. ( F ` n ) = U. ( Xt_ ` F ) )
31 3 13 30 syl2anc 
 |-  ( ph -> X_ n e. A U. ( F ` n ) = U. ( Xt_ ` F ) )
32 2 31 eqtrid 
 |-  ( ph -> X = U. ( Xt_ ` F ) )
33 5 pwexd 
 |-  ( ph -> ~P X e. _V )
34 eqid 
 |-  ( w e. X |-> ( w ` k ) ) = ( w e. X |-> ( w ` k ) )
35 34 mptpreima 
 |-  ( `' ( w e. X |-> ( w ` k ) ) " u ) = { w e. X | ( w ` k ) e. u }
36 35 ssrab3 
 |-  ( `' ( w e. X |-> ( w ` k ) ) " u ) C_ X
37 5 adantr 
 |-  ( ( ph /\ ( k e. A /\ u e. ( F ` k ) ) ) -> X e. ( UFL i^i dom card ) )
38 elpw2g 
 |-  ( X e. ( UFL i^i dom card ) -> ( ( `' ( w e. X |-> ( w ` k ) ) " u ) e. ~P X <-> ( `' ( w e. X |-> ( w ` k ) ) " u ) C_ X ) )
39 37 38 syl 
 |-  ( ( ph /\ ( k e. A /\ u e. ( F ` k ) ) ) -> ( ( `' ( w e. X |-> ( w ` k ) ) " u ) e. ~P X <-> ( `' ( w e. X |-> ( w ` k ) ) " u ) C_ X ) )
40 36 39 mpbiri 
 |-  ( ( ph /\ ( k e. A /\ u e. ( F ` k ) ) ) -> ( `' ( w e. X |-> ( w ` k ) ) " u ) e. ~P X )
41 40 ralrimivva 
 |-  ( ph -> A. k e. A A. u e. ( F ` k ) ( `' ( w e. X |-> ( w ` k ) ) " u ) e. ~P X )
42 1 fmpox 
 |-  ( A. k e. A A. u e. ( F ` k ) ( `' ( w e. X |-> ( w ` k ) ) " u ) e. ~P X <-> S : U_ k e. A ( { k } X. ( F ` k ) ) --> ~P X )
43 41 42 sylib 
 |-  ( ph -> S : U_ k e. A ( { k } X. ( F ` k ) ) --> ~P X )
44 43 frnd 
 |-  ( ph -> ran S C_ ~P X )
45 33 44 ssexd 
 |-  ( ph -> ran S e. _V )
46 snex 
 |-  { X } e. _V
47 unexg 
 |-  ( ( ran S e. _V /\ { X } e. _V ) -> ( ran S u. { X } ) e. _V )
48 45 46 47 sylancl 
 |-  ( ph -> ( ran S u. { X } ) e. _V )
49 fiuni 
 |-  ( ( ran S u. { X } ) e. _V -> U. ( ran S u. { X } ) = U. ( fi ` ( ran S u. { X } ) ) )
50 48 49 syl 
 |-  ( ph -> U. ( ran S u. { X } ) = U. ( fi ` ( ran S u. { X } ) ) )
51 28 32 50 3eqtr4d 
 |-  ( ph -> X = U. ( ran S u. { X } ) )
52 51 23 jca 
 |-  ( ph -> ( X = U. ( ran S u. { X } ) /\ ( Xt_ ` F ) = ( topGen ` ( fi ` ( ran S u. { X } ) ) ) ) )