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 syl5eq
 |-  ( 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 } ) ) ) ) )