Metamath Proof Explorer


Theorem ptbasfi

Description: The basis for the product topology can also be written as the set of finite intersections of "cylinder sets", the preimages of projections into one factor from open sets in the factor. (We have to add X itself to the list because if A is empty we get ( fi(/) ) = (/) while B = { (/) } .) (Contributed by Mario Carneiro, 3-Feb-2015)

Ref Expression
Hypotheses ptbas.1
|- B = { 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 ) ) }
ptbasfi.2
|- X = X_ n e. A U. ( F ` n )
Assertion ptbasfi
|- ( ( A e. V /\ F : A --> Top ) -> B = ( fi ` ( { X } u. ran ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) ) ) ) )

Proof

Step Hyp Ref Expression
1 ptbas.1
 |-  B = { 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 ) ) }
2 ptbasfi.2
 |-  X = X_ n e. A U. ( F ` n )
3 1 elpt
 |-  ( s e. B <-> E. h ( ( h Fn A /\ A. y e. A ( h ` y ) e. ( F ` y ) /\ E. m e. Fin A. y e. ( A \ m ) ( h ` y ) = U. ( F ` y ) ) /\ s = X_ y e. A ( h ` y ) ) )
4 df-3an
 |-  ( ( h Fn A /\ A. y e. A ( h ` y ) e. ( F ` y ) /\ E. m e. Fin A. y e. ( A \ m ) ( h ` y ) = U. ( F ` y ) ) <-> ( ( h Fn A /\ A. y e. A ( h ` y ) e. ( F ` y ) ) /\ E. m e. Fin A. y e. ( A \ m ) ( h ` y ) = U. ( F ` y ) ) )
5 simprr
 |-  ( ( ( ( A e. V /\ F : A --> Top ) /\ ( h Fn A /\ A. y e. A ( h ` y ) e. ( F ` y ) ) ) /\ ( m e. Fin /\ A. y e. ( A \ m ) ( h ` y ) = U. ( F ` y ) ) ) -> A. y e. ( A \ m ) ( h ` y ) = U. ( F ` y ) )
6 disjdif2
 |-  ( ( A i^i m ) = (/) -> ( A \ m ) = A )
7 6 raleqdv
 |-  ( ( A i^i m ) = (/) -> ( A. y e. ( A \ m ) ( h ` y ) = U. ( F ` y ) <-> A. y e. A ( h ` y ) = U. ( F ` y ) ) )
8 7 biimpac
 |-  ( ( A. y e. ( A \ m ) ( h ` y ) = U. ( F ` y ) /\ ( A i^i m ) = (/) ) -> A. y e. A ( h ` y ) = U. ( F ` y ) )
9 ixpeq2
 |-  ( A. y e. A ( h ` y ) = U. ( F ` y ) -> X_ y e. A ( h ` y ) = X_ y e. A U. ( F ` y ) )
10 8 9 syl
 |-  ( ( A. y e. ( A \ m ) ( h ` y ) = U. ( F ` y ) /\ ( A i^i m ) = (/) ) -> X_ y e. A ( h ` y ) = X_ y e. A U. ( F ` y ) )
11 fveq2
 |-  ( n = y -> ( F ` n ) = ( F ` y ) )
12 11 unieqd
 |-  ( n = y -> U. ( F ` n ) = U. ( F ` y ) )
13 12 cbvixpv
 |-  X_ n e. A U. ( F ` n ) = X_ y e. A U. ( F ` y )
14 2 13 eqtri
 |-  X = X_ y e. A U. ( F ` y )
15 10 14 eqtr4di
 |-  ( ( A. y e. ( A \ m ) ( h ` y ) = U. ( F ` y ) /\ ( A i^i m ) = (/) ) -> X_ y e. A ( h ` y ) = X )
16 5 15 sylan
 |-  ( ( ( ( ( A e. V /\ F : A --> Top ) /\ ( h Fn A /\ A. y e. A ( h ` y ) e. ( F ` y ) ) ) /\ ( m e. Fin /\ A. y e. ( A \ m ) ( h ` y ) = U. ( F ` y ) ) ) /\ ( A i^i m ) = (/) ) -> X_ y e. A ( h ` y ) = X )
17 ssv
 |-  X C_ _V
18 iineq1
 |-  ( ( A i^i m ) = (/) -> |^|_ n e. ( A i^i m ) ( `' ( w e. X |-> ( w ` n ) ) " ( h ` n ) ) = |^|_ n e. (/) ( `' ( w e. X |-> ( w ` n ) ) " ( h ` n ) ) )
19 0iin
 |-  |^|_ n e. (/) ( `' ( w e. X |-> ( w ` n ) ) " ( h ` n ) ) = _V
20 18 19 eqtrdi
 |-  ( ( A i^i m ) = (/) -> |^|_ n e. ( A i^i m ) ( `' ( w e. X |-> ( w ` n ) ) " ( h ` n ) ) = _V )
21 17 20 sseqtrrid
 |-  ( ( A i^i m ) = (/) -> X C_ |^|_ n e. ( A i^i m ) ( `' ( w e. X |-> ( w ` n ) ) " ( h ` n ) ) )
22 21 adantl
 |-  ( ( ( ( ( A e. V /\ F : A --> Top ) /\ ( h Fn A /\ A. y e. A ( h ` y ) e. ( F ` y ) ) ) /\ ( m e. Fin /\ A. y e. ( A \ m ) ( h ` y ) = U. ( F ` y ) ) ) /\ ( A i^i m ) = (/) ) -> X C_ |^|_ n e. ( A i^i m ) ( `' ( w e. X |-> ( w ` n ) ) " ( h ` n ) ) )
23 df-ss
 |-  ( X C_ |^|_ n e. ( A i^i m ) ( `' ( w e. X |-> ( w ` n ) ) " ( h ` n ) ) <-> ( X i^i |^|_ n e. ( A i^i m ) ( `' ( w e. X |-> ( w ` n ) ) " ( h ` n ) ) ) = X )
24 22 23 sylib
 |-  ( ( ( ( ( A e. V /\ F : A --> Top ) /\ ( h Fn A /\ A. y e. A ( h ` y ) e. ( F ` y ) ) ) /\ ( m e. Fin /\ A. y e. ( A \ m ) ( h ` y ) = U. ( F ` y ) ) ) /\ ( A i^i m ) = (/) ) -> ( X i^i |^|_ n e. ( A i^i m ) ( `' ( w e. X |-> ( w ` n ) ) " ( h ` n ) ) ) = X )
25 16 24 eqtr4d
 |-  ( ( ( ( ( A e. V /\ F : A --> Top ) /\ ( h Fn A /\ A. y e. A ( h ` y ) e. ( F ` y ) ) ) /\ ( m e. Fin /\ A. y e. ( A \ m ) ( h ` y ) = U. ( F ` y ) ) ) /\ ( A i^i m ) = (/) ) -> X_ y e. A ( h ` y ) = ( X i^i |^|_ n e. ( A i^i m ) ( `' ( w e. X |-> ( w ` n ) ) " ( h ` n ) ) ) )
26 simplll
 |-  ( ( ( ( ( A e. V /\ F : A --> Top ) /\ ( h Fn A /\ A. y e. A ( h ` y ) e. ( F ` y ) ) ) /\ ( m e. Fin /\ A. y e. ( A \ m ) ( h ` y ) = U. ( F ` y ) ) ) /\ n e. ( A i^i m ) ) -> ( A e. V /\ F : A --> Top ) )
27 inss1
 |-  ( A i^i m ) C_ A
28 simpr
 |-  ( ( ( ( ( A e. V /\ F : A --> Top ) /\ ( h Fn A /\ A. y e. A ( h ` y ) e. ( F ` y ) ) ) /\ ( m e. Fin /\ A. y e. ( A \ m ) ( h ` y ) = U. ( F ` y ) ) ) /\ n e. ( A i^i m ) ) -> n e. ( A i^i m ) )
29 27 28 sselid
 |-  ( ( ( ( ( A e. V /\ F : A --> Top ) /\ ( h Fn A /\ A. y e. A ( h ` y ) e. ( F ` y ) ) ) /\ ( m e. Fin /\ A. y e. ( A \ m ) ( h ` y ) = U. ( F ` y ) ) ) /\ n e. ( A i^i m ) ) -> n e. A )
30 fveq2
 |-  ( y = n -> ( h ` y ) = ( h ` n ) )
31 fveq2
 |-  ( y = n -> ( F ` y ) = ( F ` n ) )
32 30 31 eleq12d
 |-  ( y = n -> ( ( h ` y ) e. ( F ` y ) <-> ( h ` n ) e. ( F ` n ) ) )
33 simprr
 |-  ( ( ( A e. V /\ F : A --> Top ) /\ ( h Fn A /\ A. y e. A ( h ` y ) e. ( F ` y ) ) ) -> A. y e. A ( h ` y ) e. ( F ` y ) )
34 33 ad2antrr
 |-  ( ( ( ( ( A e. V /\ F : A --> Top ) /\ ( h Fn A /\ A. y e. A ( h ` y ) e. ( F ` y ) ) ) /\ ( m e. Fin /\ A. y e. ( A \ m ) ( h ` y ) = U. ( F ` y ) ) ) /\ n e. ( A i^i m ) ) -> A. y e. A ( h ` y ) e. ( F ` y ) )
35 32 34 29 rspcdva
 |-  ( ( ( ( ( A e. V /\ F : A --> Top ) /\ ( h Fn A /\ A. y e. A ( h ` y ) e. ( F ` y ) ) ) /\ ( m e. Fin /\ A. y e. ( A \ m ) ( h ` y ) = U. ( F ` y ) ) ) /\ n e. ( A i^i m ) ) -> ( h ` n ) e. ( F ` n ) )
36 14 ptpjpre1
 |-  ( ( ( A e. V /\ F : A --> Top ) /\ ( n e. A /\ ( h ` n ) e. ( F ` n ) ) ) -> ( `' ( w e. X |-> ( w ` n ) ) " ( h ` n ) ) = X_ y e. A if ( y = n , ( h ` n ) , U. ( F ` y ) ) )
37 26 29 35 36 syl12anc
 |-  ( ( ( ( ( A e. V /\ F : A --> Top ) /\ ( h Fn A /\ A. y e. A ( h ` y ) e. ( F ` y ) ) ) /\ ( m e. Fin /\ A. y e. ( A \ m ) ( h ` y ) = U. ( F ` y ) ) ) /\ n e. ( A i^i m ) ) -> ( `' ( w e. X |-> ( w ` n ) ) " ( h ` n ) ) = X_ y e. A if ( y = n , ( h ` n ) , U. ( F ` y ) ) )
38 37 adantlr
 |-  ( ( ( ( ( ( A e. V /\ F : A --> Top ) /\ ( h Fn A /\ A. y e. A ( h ` y ) e. ( F ` y ) ) ) /\ ( m e. Fin /\ A. y e. ( A \ m ) ( h ` y ) = U. ( F ` y ) ) ) /\ ( A i^i m ) =/= (/) ) /\ n e. ( A i^i m ) ) -> ( `' ( w e. X |-> ( w ` n ) ) " ( h ` n ) ) = X_ y e. A if ( y = n , ( h ` n ) , U. ( F ` y ) ) )
39 38 iineq2dv
 |-  ( ( ( ( ( A e. V /\ F : A --> Top ) /\ ( h Fn A /\ A. y e. A ( h ` y ) e. ( F ` y ) ) ) /\ ( m e. Fin /\ A. y e. ( A \ m ) ( h ` y ) = U. ( F ` y ) ) ) /\ ( A i^i m ) =/= (/) ) -> |^|_ n e. ( A i^i m ) ( `' ( w e. X |-> ( w ` n ) ) " ( h ` n ) ) = |^|_ n e. ( A i^i m ) X_ y e. A if ( y = n , ( h ` n ) , U. ( F ` y ) ) )
40 simpr
 |-  ( ( ( ( ( A e. V /\ F : A --> Top ) /\ ( h Fn A /\ A. y e. A ( h ` y ) e. ( F ` y ) ) ) /\ ( m e. Fin /\ A. y e. ( A \ m ) ( h ` y ) = U. ( F ` y ) ) ) /\ ( A i^i m ) =/= (/) ) -> ( A i^i m ) =/= (/) )
41 cnvimass
 |-  ( `' ( w e. X |-> ( w ` n ) ) " ( h ` n ) ) C_ dom ( w e. X |-> ( w ` n ) )
42 eqid
 |-  ( w e. X |-> ( w ` n ) ) = ( w e. X |-> ( w ` n ) )
43 42 dmmptss
 |-  dom ( w e. X |-> ( w ` n ) ) C_ X
44 41 43 sstri
 |-  ( `' ( w e. X |-> ( w ` n ) ) " ( h ` n ) ) C_ X
45 44 14 sseqtri
 |-  ( `' ( w e. X |-> ( w ` n ) ) " ( h ` n ) ) C_ X_ y e. A U. ( F ` y )
46 45 rgenw
 |-  A. n e. ( A i^i m ) ( `' ( w e. X |-> ( w ` n ) ) " ( h ` n ) ) C_ X_ y e. A U. ( F ` y )
47 r19.2z
 |-  ( ( ( A i^i m ) =/= (/) /\ A. n e. ( A i^i m ) ( `' ( w e. X |-> ( w ` n ) ) " ( h ` n ) ) C_ X_ y e. A U. ( F ` y ) ) -> E. n e. ( A i^i m ) ( `' ( w e. X |-> ( w ` n ) ) " ( h ` n ) ) C_ X_ y e. A U. ( F ` y ) )
48 40 46 47 sylancl
 |-  ( ( ( ( ( A e. V /\ F : A --> Top ) /\ ( h Fn A /\ A. y e. A ( h ` y ) e. ( F ` y ) ) ) /\ ( m e. Fin /\ A. y e. ( A \ m ) ( h ` y ) = U. ( F ` y ) ) ) /\ ( A i^i m ) =/= (/) ) -> E. n e. ( A i^i m ) ( `' ( w e. X |-> ( w ` n ) ) " ( h ` n ) ) C_ X_ y e. A U. ( F ` y ) )
49 iinss
 |-  ( E. n e. ( A i^i m ) ( `' ( w e. X |-> ( w ` n ) ) " ( h ` n ) ) C_ X_ y e. A U. ( F ` y ) -> |^|_ n e. ( A i^i m ) ( `' ( w e. X |-> ( w ` n ) ) " ( h ` n ) ) C_ X_ y e. A U. ( F ` y ) )
50 48 49 syl
 |-  ( ( ( ( ( A e. V /\ F : A --> Top ) /\ ( h Fn A /\ A. y e. A ( h ` y ) e. ( F ` y ) ) ) /\ ( m e. Fin /\ A. y e. ( A \ m ) ( h ` y ) = U. ( F ` y ) ) ) /\ ( A i^i m ) =/= (/) ) -> |^|_ n e. ( A i^i m ) ( `' ( w e. X |-> ( w ` n ) ) " ( h ` n ) ) C_ X_ y e. A U. ( F ` y ) )
51 50 14 sseqtrrdi
 |-  ( ( ( ( ( A e. V /\ F : A --> Top ) /\ ( h Fn A /\ A. y e. A ( h ` y ) e. ( F ` y ) ) ) /\ ( m e. Fin /\ A. y e. ( A \ m ) ( h ` y ) = U. ( F ` y ) ) ) /\ ( A i^i m ) =/= (/) ) -> |^|_ n e. ( A i^i m ) ( `' ( w e. X |-> ( w ` n ) ) " ( h ` n ) ) C_ X )
52 sseqin2
 |-  ( |^|_ n e. ( A i^i m ) ( `' ( w e. X |-> ( w ` n ) ) " ( h ` n ) ) C_ X <-> ( X i^i |^|_ n e. ( A i^i m ) ( `' ( w e. X |-> ( w ` n ) ) " ( h ` n ) ) ) = |^|_ n e. ( A i^i m ) ( `' ( w e. X |-> ( w ` n ) ) " ( h ` n ) ) )
53 51 52 sylib
 |-  ( ( ( ( ( A e. V /\ F : A --> Top ) /\ ( h Fn A /\ A. y e. A ( h ` y ) e. ( F ` y ) ) ) /\ ( m e. Fin /\ A. y e. ( A \ m ) ( h ` y ) = U. ( F ` y ) ) ) /\ ( A i^i m ) =/= (/) ) -> ( X i^i |^|_ n e. ( A i^i m ) ( `' ( w e. X |-> ( w ` n ) ) " ( h ` n ) ) ) = |^|_ n e. ( A i^i m ) ( `' ( w e. X |-> ( w ` n ) ) " ( h ` n ) ) )
54 33 ad2antrr
 |-  ( ( ( ( ( A e. V /\ F : A --> Top ) /\ ( h Fn A /\ A. y e. A ( h ` y ) e. ( F ` y ) ) ) /\ ( m e. Fin /\ A. y e. ( A \ m ) ( h ` y ) = U. ( F ` y ) ) ) /\ ( A i^i m ) =/= (/) ) -> A. y e. A ( h ` y ) e. ( F ` y ) )
55 ssralv
 |-  ( ( A i^i m ) C_ A -> ( A. y e. A ( h ` y ) e. ( F ` y ) -> A. y e. ( A i^i m ) ( h ` y ) e. ( F ` y ) ) )
56 27 55 ax-mp
 |-  ( A. y e. A ( h ` y ) e. ( F ` y ) -> A. y e. ( A i^i m ) ( h ` y ) e. ( F ` y ) )
57 elssuni
 |-  ( ( h ` y ) e. ( F ` y ) -> ( h ` y ) C_ U. ( F ` y ) )
58 iffalse
 |-  ( -. y = n -> if ( y = n , ( h ` n ) , U. ( F ` y ) ) = U. ( F ` y ) )
59 58 sseq2d
 |-  ( -. y = n -> ( ( h ` y ) C_ if ( y = n , ( h ` n ) , U. ( F ` y ) ) <-> ( h ` y ) C_ U. ( F ` y ) ) )
60 57 59 syl5ibrcom
 |-  ( ( h ` y ) e. ( F ` y ) -> ( -. y = n -> ( h ` y ) C_ if ( y = n , ( h ` n ) , U. ( F ` y ) ) ) )
61 ssid
 |-  ( h ` y ) C_ ( h ` y )
62 iftrue
 |-  ( y = n -> if ( y = n , ( h ` n ) , U. ( F ` y ) ) = ( h ` n ) )
63 62 30 eqtr4d
 |-  ( y = n -> if ( y = n , ( h ` n ) , U. ( F ` y ) ) = ( h ` y ) )
64 61 63 sseqtrrid
 |-  ( y = n -> ( h ` y ) C_ if ( y = n , ( h ` n ) , U. ( F ` y ) ) )
65 60 64 pm2.61d2
 |-  ( ( h ` y ) e. ( F ` y ) -> ( h ` y ) C_ if ( y = n , ( h ` n ) , U. ( F ` y ) ) )
66 65 ralrimivw
 |-  ( ( h ` y ) e. ( F ` y ) -> A. n e. ( A i^i m ) ( h ` y ) C_ if ( y = n , ( h ` n ) , U. ( F ` y ) ) )
67 ssiin
 |-  ( ( h ` y ) C_ |^|_ n e. ( A i^i m ) if ( y = n , ( h ` n ) , U. ( F ` y ) ) <-> A. n e. ( A i^i m ) ( h ` y ) C_ if ( y = n , ( h ` n ) , U. ( F ` y ) ) )
68 66 67 sylibr
 |-  ( ( h ` y ) e. ( F ` y ) -> ( h ` y ) C_ |^|_ n e. ( A i^i m ) if ( y = n , ( h ` n ) , U. ( F ` y ) ) )
69 68 adantl
 |-  ( ( y e. ( A i^i m ) /\ ( h ` y ) e. ( F ` y ) ) -> ( h ` y ) C_ |^|_ n e. ( A i^i m ) if ( y = n , ( h ` n ) , U. ( F ` y ) ) )
70 62 equcoms
 |-  ( n = y -> if ( y = n , ( h ` n ) , U. ( F ` y ) ) = ( h ` n ) )
71 fveq2
 |-  ( n = y -> ( h ` n ) = ( h ` y ) )
72 70 71 eqtrd
 |-  ( n = y -> if ( y = n , ( h ` n ) , U. ( F ` y ) ) = ( h ` y ) )
73 72 sseq1d
 |-  ( n = y -> ( if ( y = n , ( h ` n ) , U. ( F ` y ) ) C_ ( h ` y ) <-> ( h ` y ) C_ ( h ` y ) ) )
74 73 rspcev
 |-  ( ( y e. ( A i^i m ) /\ ( h ` y ) C_ ( h ` y ) ) -> E. n e. ( A i^i m ) if ( y = n , ( h ` n ) , U. ( F ` y ) ) C_ ( h ` y ) )
75 61 74 mpan2
 |-  ( y e. ( A i^i m ) -> E. n e. ( A i^i m ) if ( y = n , ( h ` n ) , U. ( F ` y ) ) C_ ( h ` y ) )
76 iinss
 |-  ( E. n e. ( A i^i m ) if ( y = n , ( h ` n ) , U. ( F ` y ) ) C_ ( h ` y ) -> |^|_ n e. ( A i^i m ) if ( y = n , ( h ` n ) , U. ( F ` y ) ) C_ ( h ` y ) )
77 75 76 syl
 |-  ( y e. ( A i^i m ) -> |^|_ n e. ( A i^i m ) if ( y = n , ( h ` n ) , U. ( F ` y ) ) C_ ( h ` y ) )
78 77 adantr
 |-  ( ( y e. ( A i^i m ) /\ ( h ` y ) e. ( F ` y ) ) -> |^|_ n e. ( A i^i m ) if ( y = n , ( h ` n ) , U. ( F ` y ) ) C_ ( h ` y ) )
79 69 78 eqssd
 |-  ( ( y e. ( A i^i m ) /\ ( h ` y ) e. ( F ` y ) ) -> ( h ` y ) = |^|_ n e. ( A i^i m ) if ( y = n , ( h ` n ) , U. ( F ` y ) ) )
80 79 ralimiaa
 |-  ( A. y e. ( A i^i m ) ( h ` y ) e. ( F ` y ) -> A. y e. ( A i^i m ) ( h ` y ) = |^|_ n e. ( A i^i m ) if ( y = n , ( h ` n ) , U. ( F ` y ) ) )
81 54 56 80 3syl
 |-  ( ( ( ( ( A e. V /\ F : A --> Top ) /\ ( h Fn A /\ A. y e. A ( h ` y ) e. ( F ` y ) ) ) /\ ( m e. Fin /\ A. y e. ( A \ m ) ( h ` y ) = U. ( F ` y ) ) ) /\ ( A i^i m ) =/= (/) ) -> A. y e. ( A i^i m ) ( h ` y ) = |^|_ n e. ( A i^i m ) if ( y = n , ( h ` n ) , U. ( F ` y ) ) )
82 eldifn
 |-  ( y e. ( A \ m ) -> -. y e. m )
83 82 ad2antlr
 |-  ( ( ( ( A i^i m ) =/= (/) /\ y e. ( A \ m ) ) /\ n e. ( A i^i m ) ) -> -. y e. m )
84 inss2
 |-  ( A i^i m ) C_ m
85 simpr
 |-  ( ( ( ( A i^i m ) =/= (/) /\ y e. ( A \ m ) ) /\ n e. ( A i^i m ) ) -> n e. ( A i^i m ) )
86 84 85 sselid
 |-  ( ( ( ( A i^i m ) =/= (/) /\ y e. ( A \ m ) ) /\ n e. ( A i^i m ) ) -> n e. m )
87 eleq1
 |-  ( y = n -> ( y e. m <-> n e. m ) )
88 86 87 syl5ibrcom
 |-  ( ( ( ( A i^i m ) =/= (/) /\ y e. ( A \ m ) ) /\ n e. ( A i^i m ) ) -> ( y = n -> y e. m ) )
89 83 88 mtod
 |-  ( ( ( ( A i^i m ) =/= (/) /\ y e. ( A \ m ) ) /\ n e. ( A i^i m ) ) -> -. y = n )
90 89 58 syl
 |-  ( ( ( ( A i^i m ) =/= (/) /\ y e. ( A \ m ) ) /\ n e. ( A i^i m ) ) -> if ( y = n , ( h ` n ) , U. ( F ` y ) ) = U. ( F ` y ) )
91 90 iineq2dv
 |-  ( ( ( A i^i m ) =/= (/) /\ y e. ( A \ m ) ) -> |^|_ n e. ( A i^i m ) if ( y = n , ( h ` n ) , U. ( F ` y ) ) = |^|_ n e. ( A i^i m ) U. ( F ` y ) )
92 iinconst
 |-  ( ( A i^i m ) =/= (/) -> |^|_ n e. ( A i^i m ) U. ( F ` y ) = U. ( F ` y ) )
93 92 adantr
 |-  ( ( ( A i^i m ) =/= (/) /\ y e. ( A \ m ) ) -> |^|_ n e. ( A i^i m ) U. ( F ` y ) = U. ( F ` y ) )
94 91 93 eqtr2d
 |-  ( ( ( A i^i m ) =/= (/) /\ y e. ( A \ m ) ) -> U. ( F ` y ) = |^|_ n e. ( A i^i m ) if ( y = n , ( h ` n ) , U. ( F ` y ) ) )
95 eqeq1
 |-  ( ( h ` y ) = U. ( F ` y ) -> ( ( h ` y ) = |^|_ n e. ( A i^i m ) if ( y = n , ( h ` n ) , U. ( F ` y ) ) <-> U. ( F ` y ) = |^|_ n e. ( A i^i m ) if ( y = n , ( h ` n ) , U. ( F ` y ) ) ) )
96 94 95 syl5ibrcom
 |-  ( ( ( A i^i m ) =/= (/) /\ y e. ( A \ m ) ) -> ( ( h ` y ) = U. ( F ` y ) -> ( h ` y ) = |^|_ n e. ( A i^i m ) if ( y = n , ( h ` n ) , U. ( F ` y ) ) ) )
97 96 ralimdva
 |-  ( ( A i^i m ) =/= (/) -> ( A. y e. ( A \ m ) ( h ` y ) = U. ( F ` y ) -> A. y e. ( A \ m ) ( h ` y ) = |^|_ n e. ( A i^i m ) if ( y = n , ( h ` n ) , U. ( F ` y ) ) ) )
98 5 97 mpan9
 |-  ( ( ( ( ( A e. V /\ F : A --> Top ) /\ ( h Fn A /\ A. y e. A ( h ` y ) e. ( F ` y ) ) ) /\ ( m e. Fin /\ A. y e. ( A \ m ) ( h ` y ) = U. ( F ` y ) ) ) /\ ( A i^i m ) =/= (/) ) -> A. y e. ( A \ m ) ( h ` y ) = |^|_ n e. ( A i^i m ) if ( y = n , ( h ` n ) , U. ( F ` y ) ) )
99 inundif
 |-  ( ( A i^i m ) u. ( A \ m ) ) = A
100 99 raleqi
 |-  ( A. y e. ( ( A i^i m ) u. ( A \ m ) ) ( h ` y ) = |^|_ n e. ( A i^i m ) if ( y = n , ( h ` n ) , U. ( F ` y ) ) <-> A. y e. A ( h ` y ) = |^|_ n e. ( A i^i m ) if ( y = n , ( h ` n ) , U. ( F ` y ) ) )
101 ralunb
 |-  ( A. y e. ( ( A i^i m ) u. ( A \ m ) ) ( h ` y ) = |^|_ n e. ( A i^i m ) if ( y = n , ( h ` n ) , U. ( F ` y ) ) <-> ( A. y e. ( A i^i m ) ( h ` y ) = |^|_ n e. ( A i^i m ) if ( y = n , ( h ` n ) , U. ( F ` y ) ) /\ A. y e. ( A \ m ) ( h ` y ) = |^|_ n e. ( A i^i m ) if ( y = n , ( h ` n ) , U. ( F ` y ) ) ) )
102 100 101 bitr3i
 |-  ( A. y e. A ( h ` y ) = |^|_ n e. ( A i^i m ) if ( y = n , ( h ` n ) , U. ( F ` y ) ) <-> ( A. y e. ( A i^i m ) ( h ` y ) = |^|_ n e. ( A i^i m ) if ( y = n , ( h ` n ) , U. ( F ` y ) ) /\ A. y e. ( A \ m ) ( h ` y ) = |^|_ n e. ( A i^i m ) if ( y = n , ( h ` n ) , U. ( F ` y ) ) ) )
103 81 98 102 sylanbrc
 |-  ( ( ( ( ( A e. V /\ F : A --> Top ) /\ ( h Fn A /\ A. y e. A ( h ` y ) e. ( F ` y ) ) ) /\ ( m e. Fin /\ A. y e. ( A \ m ) ( h ` y ) = U. ( F ` y ) ) ) /\ ( A i^i m ) =/= (/) ) -> A. y e. A ( h ` y ) = |^|_ n e. ( A i^i m ) if ( y = n , ( h ` n ) , U. ( F ` y ) ) )
104 ixpeq2
 |-  ( A. y e. A ( h ` y ) = |^|_ n e. ( A i^i m ) if ( y = n , ( h ` n ) , U. ( F ` y ) ) -> X_ y e. A ( h ` y ) = X_ y e. A |^|_ n e. ( A i^i m ) if ( y = n , ( h ` n ) , U. ( F ` y ) ) )
105 103 104 syl
 |-  ( ( ( ( ( A e. V /\ F : A --> Top ) /\ ( h Fn A /\ A. y e. A ( h ` y ) e. ( F ` y ) ) ) /\ ( m e. Fin /\ A. y e. ( A \ m ) ( h ` y ) = U. ( F ` y ) ) ) /\ ( A i^i m ) =/= (/) ) -> X_ y e. A ( h ` y ) = X_ y e. A |^|_ n e. ( A i^i m ) if ( y = n , ( h ` n ) , U. ( F ` y ) ) )
106 ixpiin
 |-  ( ( A i^i m ) =/= (/) -> X_ y e. A |^|_ n e. ( A i^i m ) if ( y = n , ( h ` n ) , U. ( F ` y ) ) = |^|_ n e. ( A i^i m ) X_ y e. A if ( y = n , ( h ` n ) , U. ( F ` y ) ) )
107 106 adantl
 |-  ( ( ( ( ( A e. V /\ F : A --> Top ) /\ ( h Fn A /\ A. y e. A ( h ` y ) e. ( F ` y ) ) ) /\ ( m e. Fin /\ A. y e. ( A \ m ) ( h ` y ) = U. ( F ` y ) ) ) /\ ( A i^i m ) =/= (/) ) -> X_ y e. A |^|_ n e. ( A i^i m ) if ( y = n , ( h ` n ) , U. ( F ` y ) ) = |^|_ n e. ( A i^i m ) X_ y e. A if ( y = n , ( h ` n ) , U. ( F ` y ) ) )
108 105 107 eqtrd
 |-  ( ( ( ( ( A e. V /\ F : A --> Top ) /\ ( h Fn A /\ A. y e. A ( h ` y ) e. ( F ` y ) ) ) /\ ( m e. Fin /\ A. y e. ( A \ m ) ( h ` y ) = U. ( F ` y ) ) ) /\ ( A i^i m ) =/= (/) ) -> X_ y e. A ( h ` y ) = |^|_ n e. ( A i^i m ) X_ y e. A if ( y = n , ( h ` n ) , U. ( F ` y ) ) )
109 39 53 108 3eqtr4rd
 |-  ( ( ( ( ( A e. V /\ F : A --> Top ) /\ ( h Fn A /\ A. y e. A ( h ` y ) e. ( F ` y ) ) ) /\ ( m e. Fin /\ A. y e. ( A \ m ) ( h ` y ) = U. ( F ` y ) ) ) /\ ( A i^i m ) =/= (/) ) -> X_ y e. A ( h ` y ) = ( X i^i |^|_ n e. ( A i^i m ) ( `' ( w e. X |-> ( w ` n ) ) " ( h ` n ) ) ) )
110 25 109 pm2.61dane
 |-  ( ( ( ( A e. V /\ F : A --> Top ) /\ ( h Fn A /\ A. y e. A ( h ` y ) e. ( F ` y ) ) ) /\ ( m e. Fin /\ A. y e. ( A \ m ) ( h ` y ) = U. ( F ` y ) ) ) -> X_ y e. A ( h ` y ) = ( X i^i |^|_ n e. ( A i^i m ) ( `' ( w e. X |-> ( w ` n ) ) " ( h ` n ) ) ) )
111 ixpexg
 |-  ( A. n e. A U. ( F ` n ) e. _V -> X_ n e. A U. ( F ` n ) e. _V )
112 fvex
 |-  ( F ` n ) e. _V
113 112 uniex
 |-  U. ( F ` n ) e. _V
114 113 a1i
 |-  ( n e. A -> U. ( F ` n ) e. _V )
115 111 114 mprg
 |-  X_ n e. A U. ( F ` n ) e. _V
116 2 115 eqeltri
 |-  X e. _V
117 116 mptex
 |-  ( w e. X |-> ( w ` n ) ) e. _V
118 117 cnvex
 |-  `' ( w e. X |-> ( w ` n ) ) e. _V
119 118 imaex
 |-  ( `' ( w e. X |-> ( w ` n ) ) " ( h ` n ) ) e. _V
120 119 dfiin2
 |-  |^|_ n e. ( A i^i m ) ( `' ( w e. X |-> ( w ` n ) ) " ( h ` n ) ) = |^| { z | E. n e. ( A i^i m ) z = ( `' ( w e. X |-> ( w ` n ) ) " ( h ` n ) ) }
121 inteq
 |-  ( { z | E. n e. ( A i^i m ) z = ( `' ( w e. X |-> ( w ` n ) ) " ( h ` n ) ) } = (/) -> |^| { z | E. n e. ( A i^i m ) z = ( `' ( w e. X |-> ( w ` n ) ) " ( h ` n ) ) } = |^| (/) )
122 120 121 eqtrid
 |-  ( { z | E. n e. ( A i^i m ) z = ( `' ( w e. X |-> ( w ` n ) ) " ( h ` n ) ) } = (/) -> |^|_ n e. ( A i^i m ) ( `' ( w e. X |-> ( w ` n ) ) " ( h ` n ) ) = |^| (/) )
123 int0
 |-  |^| (/) = _V
124 122 123 eqtrdi
 |-  ( { z | E. n e. ( A i^i m ) z = ( `' ( w e. X |-> ( w ` n ) ) " ( h ` n ) ) } = (/) -> |^|_ n e. ( A i^i m ) ( `' ( w e. X |-> ( w ` n ) ) " ( h ` n ) ) = _V )
125 124 ineq2d
 |-  ( { z | E. n e. ( A i^i m ) z = ( `' ( w e. X |-> ( w ` n ) ) " ( h ` n ) ) } = (/) -> ( X i^i |^|_ n e. ( A i^i m ) ( `' ( w e. X |-> ( w ` n ) ) " ( h ` n ) ) ) = ( X i^i _V ) )
126 inv1
 |-  ( X i^i _V ) = X
127 125 126 eqtrdi
 |-  ( { z | E. n e. ( A i^i m ) z = ( `' ( w e. X |-> ( w ` n ) ) " ( h ` n ) ) } = (/) -> ( X i^i |^|_ n e. ( A i^i m ) ( `' ( w e. X |-> ( w ` n ) ) " ( h ` n ) ) ) = X )
128 127 adantl
 |-  ( ( ( ( ( A e. V /\ F : A --> Top ) /\ ( h Fn A /\ A. y e. A ( h ` y ) e. ( F ` y ) ) ) /\ ( m e. Fin /\ A. y e. ( A \ m ) ( h ` y ) = U. ( F ` y ) ) ) /\ { z | E. n e. ( A i^i m ) z = ( `' ( w e. X |-> ( w ` n ) ) " ( h ` n ) ) } = (/) ) -> ( X i^i |^|_ n e. ( A i^i m ) ( `' ( w e. X |-> ( w ` n ) ) " ( h ` n ) ) ) = X )
129 snex
 |-  { X } e. _V
130 1 ptbas
 |-  ( ( A e. V /\ F : A --> Top ) -> B e. TopBases )
131 1 2 ptpjpre2
 |-  ( ( ( A e. V /\ F : A --> Top ) /\ ( k e. A /\ u e. ( F ` k ) ) ) -> ( `' ( w e. X |-> ( w ` k ) ) " u ) e. B )
132 131 ralrimivva
 |-  ( ( A e. V /\ F : A --> Top ) -> A. k e. A A. u e. ( F ` k ) ( `' ( w e. X |-> ( w ` k ) ) " u ) e. B )
133 eqid
 |-  ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) ) = ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) )
134 133 fmpox
 |-  ( A. k e. A A. u e. ( F ` k ) ( `' ( w e. X |-> ( w ` k ) ) " u ) e. B <-> ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) ) : U_ k e. A ( { k } X. ( F ` k ) ) --> B )
135 132 134 sylib
 |-  ( ( A e. V /\ F : A --> Top ) -> ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) ) : U_ k e. A ( { k } X. ( F ` k ) ) --> B )
136 135 frnd
 |-  ( ( A e. V /\ F : A --> Top ) -> ran ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) ) C_ B )
137 130 136 ssexd
 |-  ( ( A e. V /\ F : A --> Top ) -> ran ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) ) e. _V )
138 unexg
 |-  ( ( { X } e. _V /\ ran ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) ) e. _V ) -> ( { X } u. ran ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) ) ) e. _V )
139 129 137 138 sylancr
 |-  ( ( A e. V /\ F : A --> Top ) -> ( { X } u. ran ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) ) ) e. _V )
140 ssfii
 |-  ( ( { X } u. ran ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) ) ) e. _V -> ( { X } u. ran ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) ) ) C_ ( fi ` ( { X } u. ran ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) ) ) ) )
141 139 140 syl
 |-  ( ( A e. V /\ F : A --> Top ) -> ( { X } u. ran ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) ) ) C_ ( fi ` ( { X } u. ran ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) ) ) ) )
142 141 ad2antrr
 |-  ( ( ( ( A e. V /\ F : A --> Top ) /\ ( h Fn A /\ A. y e. A ( h ` y ) e. ( F ` y ) ) ) /\ ( m e. Fin /\ A. y e. ( A \ m ) ( h ` y ) = U. ( F ` y ) ) ) -> ( { X } u. ran ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) ) ) C_ ( fi ` ( { X } u. ran ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) ) ) ) )
143 ssun1
 |-  { X } C_ ( { X } u. ran ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) ) )
144 116 snss
 |-  ( X e. ( { X } u. ran ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) ) ) <-> { X } C_ ( { X } u. ran ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) ) ) )
145 143 144 mpbir
 |-  X e. ( { X } u. ran ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) ) )
146 145 a1i
 |-  ( ( ( ( A e. V /\ F : A --> Top ) /\ ( h Fn A /\ A. y e. A ( h ` y ) e. ( F ` y ) ) ) /\ ( m e. Fin /\ A. y e. ( A \ m ) ( h ` y ) = U. ( F ` y ) ) ) -> X e. ( { X } u. ran ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) ) ) )
147 142 146 sseldd
 |-  ( ( ( ( A e. V /\ F : A --> Top ) /\ ( h Fn A /\ A. y e. A ( h ` y ) e. ( F ` y ) ) ) /\ ( m e. Fin /\ A. y e. ( A \ m ) ( h ` y ) = U. ( F ` y ) ) ) -> X e. ( fi ` ( { X } u. ran ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) ) ) ) )
148 147 adantr
 |-  ( ( ( ( ( A e. V /\ F : A --> Top ) /\ ( h Fn A /\ A. y e. A ( h ` y ) e. ( F ` y ) ) ) /\ ( m e. Fin /\ A. y e. ( A \ m ) ( h ` y ) = U. ( F ` y ) ) ) /\ { z | E. n e. ( A i^i m ) z = ( `' ( w e. X |-> ( w ` n ) ) " ( h ` n ) ) } = (/) ) -> X e. ( fi ` ( { X } u. ran ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) ) ) ) )
149 128 148 eqeltrd
 |-  ( ( ( ( ( A e. V /\ F : A --> Top ) /\ ( h Fn A /\ A. y e. A ( h ` y ) e. ( F ` y ) ) ) /\ ( m e. Fin /\ A. y e. ( A \ m ) ( h ` y ) = U. ( F ` y ) ) ) /\ { z | E. n e. ( A i^i m ) z = ( `' ( w e. X |-> ( w ` n ) ) " ( h ` n ) ) } = (/) ) -> ( X i^i |^|_ n e. ( A i^i m ) ( `' ( w e. X |-> ( w ` n ) ) " ( h ` n ) ) ) e. ( fi ` ( { X } u. ran ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) ) ) ) )
150 139 ad3antrrr
 |-  ( ( ( ( ( A e. V /\ F : A --> Top ) /\ ( h Fn A /\ A. y e. A ( h ` y ) e. ( F ` y ) ) ) /\ ( m e. Fin /\ A. y e. ( A \ m ) ( h ` y ) = U. ( F ` y ) ) ) /\ { z | E. n e. ( A i^i m ) z = ( `' ( w e. X |-> ( w ` n ) ) " ( h ` n ) ) } =/= (/) ) -> ( { X } u. ran ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) ) ) e. _V )
151 nfv
 |-  F/ n ( ( ( A e. V /\ F : A --> Top ) /\ ( h Fn A /\ A. y e. A ( h ` y ) e. ( F ` y ) ) ) /\ ( m e. Fin /\ A. y e. ( A \ m ) ( h ` y ) = U. ( F ` y ) ) )
152 nfcv
 |-  F/_ n A
153 nfcv
 |-  F/_ n ( F ` k )
154 nfixp1
 |-  F/_ n X_ n e. A U. ( F ` n )
155 2 154 nfcxfr
 |-  F/_ n X
156 nfcv
 |-  F/_ n ( w ` k )
157 155 156 nfmpt
 |-  F/_ n ( w e. X |-> ( w ` k ) )
158 157 nfcnv
 |-  F/_ n `' ( w e. X |-> ( w ` k ) )
159 nfcv
 |-  F/_ n u
160 158 159 nfima
 |-  F/_ n ( `' ( w e. X |-> ( w ` k ) ) " u )
161 152 153 160 nfmpo
 |-  F/_ n ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) )
162 161 nfrn
 |-  F/_ n ran ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) )
163 162 nfcri
 |-  F/ n z e. ran ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) )
164 df-ov
 |-  ( n ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) ) ( h ` n ) ) = ( ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) ) ` <. n , ( h ` n ) >. )
165 119 a1i
 |-  ( ( ( ( ( A e. V /\ F : A --> Top ) /\ ( h Fn A /\ A. y e. A ( h ` y ) e. ( F ` y ) ) ) /\ ( m e. Fin /\ A. y e. ( A \ m ) ( h ` y ) = U. ( F ` y ) ) ) /\ n e. ( A i^i m ) ) -> ( `' ( w e. X |-> ( w ` n ) ) " ( h ` n ) ) e. _V )
166 fveq2
 |-  ( k = n -> ( w ` k ) = ( w ` n ) )
167 166 mpteq2dv
 |-  ( k = n -> ( w e. X |-> ( w ` k ) ) = ( w e. X |-> ( w ` n ) ) )
168 167 cnveqd
 |-  ( k = n -> `' ( w e. X |-> ( w ` k ) ) = `' ( w e. X |-> ( w ` n ) ) )
169 168 imaeq1d
 |-  ( k = n -> ( `' ( w e. X |-> ( w ` k ) ) " u ) = ( `' ( w e. X |-> ( w ` n ) ) " u ) )
170 imaeq2
 |-  ( u = ( h ` n ) -> ( `' ( w e. X |-> ( w ` n ) ) " u ) = ( `' ( w e. X |-> ( w ` n ) ) " ( h ` n ) ) )
171 169 170 sylan9eq
 |-  ( ( k = n /\ u = ( h ` n ) ) -> ( `' ( w e. X |-> ( w ` k ) ) " u ) = ( `' ( w e. X |-> ( w ` n ) ) " ( h ` n ) ) )
172 fveq2
 |-  ( k = n -> ( F ` k ) = ( F ` n ) )
173 171 172 133 ovmpox
 |-  ( ( n e. A /\ ( h ` n ) e. ( F ` n ) /\ ( `' ( w e. X |-> ( w ` n ) ) " ( h ` n ) ) e. _V ) -> ( n ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) ) ( h ` n ) ) = ( `' ( w e. X |-> ( w ` n ) ) " ( h ` n ) ) )
174 29 35 165 173 syl3anc
 |-  ( ( ( ( ( A e. V /\ F : A --> Top ) /\ ( h Fn A /\ A. y e. A ( h ` y ) e. ( F ` y ) ) ) /\ ( m e. Fin /\ A. y e. ( A \ m ) ( h ` y ) = U. ( F ` y ) ) ) /\ n e. ( A i^i m ) ) -> ( n ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) ) ( h ` n ) ) = ( `' ( w e. X |-> ( w ` n ) ) " ( h ` n ) ) )
175 164 174 eqtr3id
 |-  ( ( ( ( ( A e. V /\ F : A --> Top ) /\ ( h Fn A /\ A. y e. A ( h ` y ) e. ( F ` y ) ) ) /\ ( m e. Fin /\ A. y e. ( A \ m ) ( h ` y ) = U. ( F ` y ) ) ) /\ n e. ( A i^i m ) ) -> ( ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) ) ` <. n , ( h ` n ) >. ) = ( `' ( w e. X |-> ( w ` n ) ) " ( h ` n ) ) )
176 135 ad3antrrr
 |-  ( ( ( ( ( A e. V /\ F : A --> Top ) /\ ( h Fn A /\ A. y e. A ( h ` y ) e. ( F ` y ) ) ) /\ ( m e. Fin /\ A. y e. ( A \ m ) ( h ` y ) = U. ( F ` y ) ) ) /\ n e. ( A i^i m ) ) -> ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) ) : U_ k e. A ( { k } X. ( F ` k ) ) --> B )
177 176 ffnd
 |-  ( ( ( ( ( A e. V /\ F : A --> Top ) /\ ( h Fn A /\ A. y e. A ( h ` y ) e. ( F ` y ) ) ) /\ ( m e. Fin /\ A. y e. ( A \ m ) ( h ` y ) = U. ( F ` y ) ) ) /\ n e. ( A i^i m ) ) -> ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) ) Fn U_ k e. A ( { k } X. ( F ` k ) ) )
178 opeliunxp
 |-  ( <. n , ( h ` n ) >. e. U_ n e. A ( { n } X. ( F ` n ) ) <-> ( n e. A /\ ( h ` n ) e. ( F ` n ) ) )
179 29 35 178 sylanbrc
 |-  ( ( ( ( ( A e. V /\ F : A --> Top ) /\ ( h Fn A /\ A. y e. A ( h ` y ) e. ( F ` y ) ) ) /\ ( m e. Fin /\ A. y e. ( A \ m ) ( h ` y ) = U. ( F ` y ) ) ) /\ n e. ( A i^i m ) ) -> <. n , ( h ` n ) >. e. U_ n e. A ( { n } X. ( F ` n ) ) )
180 sneq
 |-  ( n = k -> { n } = { k } )
181 fveq2
 |-  ( n = k -> ( F ` n ) = ( F ` k ) )
182 180 181 xpeq12d
 |-  ( n = k -> ( { n } X. ( F ` n ) ) = ( { k } X. ( F ` k ) ) )
183 182 cbviunv
 |-  U_ n e. A ( { n } X. ( F ` n ) ) = U_ k e. A ( { k } X. ( F ` k ) )
184 179 183 eleqtrdi
 |-  ( ( ( ( ( A e. V /\ F : A --> Top ) /\ ( h Fn A /\ A. y e. A ( h ` y ) e. ( F ` y ) ) ) /\ ( m e. Fin /\ A. y e. ( A \ m ) ( h ` y ) = U. ( F ` y ) ) ) /\ n e. ( A i^i m ) ) -> <. n , ( h ` n ) >. e. U_ k e. A ( { k } X. ( F ` k ) ) )
185 fnfvelrn
 |-  ( ( ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) ) Fn U_ k e. A ( { k } X. ( F ` k ) ) /\ <. n , ( h ` n ) >. e. U_ k e. A ( { k } X. ( F ` k ) ) ) -> ( ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) ) ` <. n , ( h ` n ) >. ) e. ran ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) ) )
186 177 184 185 syl2anc
 |-  ( ( ( ( ( A e. V /\ F : A --> Top ) /\ ( h Fn A /\ A. y e. A ( h ` y ) e. ( F ` y ) ) ) /\ ( m e. Fin /\ A. y e. ( A \ m ) ( h ` y ) = U. ( F ` y ) ) ) /\ n e. ( A i^i m ) ) -> ( ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) ) ` <. n , ( h ` n ) >. ) e. ran ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) ) )
187 175 186 eqeltrrd
 |-  ( ( ( ( ( A e. V /\ F : A --> Top ) /\ ( h Fn A /\ A. y e. A ( h ` y ) e. ( F ` y ) ) ) /\ ( m e. Fin /\ A. y e. ( A \ m ) ( h ` y ) = U. ( F ` y ) ) ) /\ n e. ( A i^i m ) ) -> ( `' ( w e. X |-> ( w ` n ) ) " ( h ` n ) ) e. ran ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) ) )
188 eleq1
 |-  ( z = ( `' ( w e. X |-> ( w ` n ) ) " ( h ` n ) ) -> ( z e. ran ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) ) <-> ( `' ( w e. X |-> ( w ` n ) ) " ( h ` n ) ) e. ran ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) ) ) )
189 187 188 syl5ibrcom
 |-  ( ( ( ( ( A e. V /\ F : A --> Top ) /\ ( h Fn A /\ A. y e. A ( h ` y ) e. ( F ` y ) ) ) /\ ( m e. Fin /\ A. y e. ( A \ m ) ( h ` y ) = U. ( F ` y ) ) ) /\ n e. ( A i^i m ) ) -> ( z = ( `' ( w e. X |-> ( w ` n ) ) " ( h ` n ) ) -> z e. ran ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) ) ) )
190 189 ex
 |-  ( ( ( ( A e. V /\ F : A --> Top ) /\ ( h Fn A /\ A. y e. A ( h ` y ) e. ( F ` y ) ) ) /\ ( m e. Fin /\ A. y e. ( A \ m ) ( h ` y ) = U. ( F ` y ) ) ) -> ( n e. ( A i^i m ) -> ( z = ( `' ( w e. X |-> ( w ` n ) ) " ( h ` n ) ) -> z e. ran ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) ) ) ) )
191 151 163 190 rexlimd
 |-  ( ( ( ( A e. V /\ F : A --> Top ) /\ ( h Fn A /\ A. y e. A ( h ` y ) e. ( F ` y ) ) ) /\ ( m e. Fin /\ A. y e. ( A \ m ) ( h ` y ) = U. ( F ` y ) ) ) -> ( E. n e. ( A i^i m ) z = ( `' ( w e. X |-> ( w ` n ) ) " ( h ` n ) ) -> z e. ran ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) ) ) )
192 191 abssdv
 |-  ( ( ( ( A e. V /\ F : A --> Top ) /\ ( h Fn A /\ A. y e. A ( h ` y ) e. ( F ` y ) ) ) /\ ( m e. Fin /\ A. y e. ( A \ m ) ( h ` y ) = U. ( F ` y ) ) ) -> { z | E. n e. ( A i^i m ) z = ( `' ( w e. X |-> ( w ` n ) ) " ( h ` n ) ) } C_ ran ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) ) )
193 ssun2
 |-  ran ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) ) C_ ( { X } u. ran ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) ) )
194 192 193 sstrdi
 |-  ( ( ( ( A e. V /\ F : A --> Top ) /\ ( h Fn A /\ A. y e. A ( h ` y ) e. ( F ` y ) ) ) /\ ( m e. Fin /\ A. y e. ( A \ m ) ( h ` y ) = U. ( F ` y ) ) ) -> { z | E. n e. ( A i^i m ) z = ( `' ( w e. X |-> ( w ` n ) ) " ( h ` n ) ) } C_ ( { X } u. ran ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) ) ) )
195 194 adantr
 |-  ( ( ( ( ( A e. V /\ F : A --> Top ) /\ ( h Fn A /\ A. y e. A ( h ` y ) e. ( F ` y ) ) ) /\ ( m e. Fin /\ A. y e. ( A \ m ) ( h ` y ) = U. ( F ` y ) ) ) /\ { z | E. n e. ( A i^i m ) z = ( `' ( w e. X |-> ( w ` n ) ) " ( h ` n ) ) } =/= (/) ) -> { z | E. n e. ( A i^i m ) z = ( `' ( w e. X |-> ( w ` n ) ) " ( h ` n ) ) } C_ ( { X } u. ran ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) ) ) )
196 simpr
 |-  ( ( ( ( ( A e. V /\ F : A --> Top ) /\ ( h Fn A /\ A. y e. A ( h ` y ) e. ( F ` y ) ) ) /\ ( m e. Fin /\ A. y e. ( A \ m ) ( h ` y ) = U. ( F ` y ) ) ) /\ { z | E. n e. ( A i^i m ) z = ( `' ( w e. X |-> ( w ` n ) ) " ( h ` n ) ) } =/= (/) ) -> { z | E. n e. ( A i^i m ) z = ( `' ( w e. X |-> ( w ` n ) ) " ( h ` n ) ) } =/= (/) )
197 simplrl
 |-  ( ( ( ( ( A e. V /\ F : A --> Top ) /\ ( h Fn A /\ A. y e. A ( h ` y ) e. ( F ` y ) ) ) /\ ( m e. Fin /\ A. y e. ( A \ m ) ( h ` y ) = U. ( F ` y ) ) ) /\ { z | E. n e. ( A i^i m ) z = ( `' ( w e. X |-> ( w ` n ) ) " ( h ` n ) ) } =/= (/) ) -> m e. Fin )
198 ssfi
 |-  ( ( m e. Fin /\ ( A i^i m ) C_ m ) -> ( A i^i m ) e. Fin )
199 197 84 198 sylancl
 |-  ( ( ( ( ( A e. V /\ F : A --> Top ) /\ ( h Fn A /\ A. y e. A ( h ` y ) e. ( F ` y ) ) ) /\ ( m e. Fin /\ A. y e. ( A \ m ) ( h ` y ) = U. ( F ` y ) ) ) /\ { z | E. n e. ( A i^i m ) z = ( `' ( w e. X |-> ( w ` n ) ) " ( h ` n ) ) } =/= (/) ) -> ( A i^i m ) e. Fin )
200 abrexfi
 |-  ( ( A i^i m ) e. Fin -> { z | E. n e. ( A i^i m ) z = ( `' ( w e. X |-> ( w ` n ) ) " ( h ` n ) ) } e. Fin )
201 199 200 syl
 |-  ( ( ( ( ( A e. V /\ F : A --> Top ) /\ ( h Fn A /\ A. y e. A ( h ` y ) e. ( F ` y ) ) ) /\ ( m e. Fin /\ A. y e. ( A \ m ) ( h ` y ) = U. ( F ` y ) ) ) /\ { z | E. n e. ( A i^i m ) z = ( `' ( w e. X |-> ( w ` n ) ) " ( h ` n ) ) } =/= (/) ) -> { z | E. n e. ( A i^i m ) z = ( `' ( w e. X |-> ( w ` n ) ) " ( h ` n ) ) } e. Fin )
202 elfir
 |-  ( ( ( { X } u. ran ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) ) ) e. _V /\ ( { z | E. n e. ( A i^i m ) z = ( `' ( w e. X |-> ( w ` n ) ) " ( h ` n ) ) } C_ ( { X } u. ran ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) ) ) /\ { z | E. n e. ( A i^i m ) z = ( `' ( w e. X |-> ( w ` n ) ) " ( h ` n ) ) } =/= (/) /\ { z | E. n e. ( A i^i m ) z = ( `' ( w e. X |-> ( w ` n ) ) " ( h ` n ) ) } e. Fin ) ) -> |^| { z | E. n e. ( A i^i m ) z = ( `' ( w e. X |-> ( w ` n ) ) " ( h ` n ) ) } e. ( fi ` ( { X } u. ran ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) ) ) ) )
203 150 195 196 201 202 syl13anc
 |-  ( ( ( ( ( A e. V /\ F : A --> Top ) /\ ( h Fn A /\ A. y e. A ( h ` y ) e. ( F ` y ) ) ) /\ ( m e. Fin /\ A. y e. ( A \ m ) ( h ` y ) = U. ( F ` y ) ) ) /\ { z | E. n e. ( A i^i m ) z = ( `' ( w e. X |-> ( w ` n ) ) " ( h ` n ) ) } =/= (/) ) -> |^| { z | E. n e. ( A i^i m ) z = ( `' ( w e. X |-> ( w ` n ) ) " ( h ` n ) ) } e. ( fi ` ( { X } u. ran ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) ) ) ) )
204 120 203 eqeltrid
 |-  ( ( ( ( ( A e. V /\ F : A --> Top ) /\ ( h Fn A /\ A. y e. A ( h ` y ) e. ( F ` y ) ) ) /\ ( m e. Fin /\ A. y e. ( A \ m ) ( h ` y ) = U. ( F ` y ) ) ) /\ { z | E. n e. ( A i^i m ) z = ( `' ( w e. X |-> ( w ` n ) ) " ( h ` n ) ) } =/= (/) ) -> |^|_ n e. ( A i^i m ) ( `' ( w e. X |-> ( w ` n ) ) " ( h ` n ) ) e. ( fi ` ( { X } u. ran ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) ) ) ) )
205 elssuni
 |-  ( |^|_ n e. ( A i^i m ) ( `' ( w e. X |-> ( w ` n ) ) " ( h ` n ) ) e. ( fi ` ( { X } u. ran ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) ) ) ) -> |^|_ n e. ( A i^i m ) ( `' ( w e. X |-> ( w ` n ) ) " ( h ` n ) ) C_ U. ( fi ` ( { X } u. ran ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) ) ) ) )
206 204 205 syl
 |-  ( ( ( ( ( A e. V /\ F : A --> Top ) /\ ( h Fn A /\ A. y e. A ( h ` y ) e. ( F ` y ) ) ) /\ ( m e. Fin /\ A. y e. ( A \ m ) ( h ` y ) = U. ( F ` y ) ) ) /\ { z | E. n e. ( A i^i m ) z = ( `' ( w e. X |-> ( w ` n ) ) " ( h ` n ) ) } =/= (/) ) -> |^|_ n e. ( A i^i m ) ( `' ( w e. X |-> ( w ` n ) ) " ( h ` n ) ) C_ U. ( fi ` ( { X } u. ran ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) ) ) ) )
207 fiuni
 |-  ( ( { X } u. ran ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) ) ) e. _V -> U. ( { X } u. ran ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) ) ) = U. ( fi ` ( { X } u. ran ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) ) ) ) )
208 139 207 syl
 |-  ( ( A e. V /\ F : A --> Top ) -> U. ( { X } u. ran ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) ) ) = U. ( fi ` ( { X } u. ran ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) ) ) ) )
209 116 pwid
 |-  X e. ~P X
210 209 a1i
 |-  ( ( A e. V /\ F : A --> Top ) -> X e. ~P X )
211 210 snssd
 |-  ( ( A e. V /\ F : A --> Top ) -> { X } C_ ~P X )
212 1 ptuni2
 |-  ( ( A e. V /\ F : A --> Top ) -> X_ n e. A U. ( F ` n ) = U. B )
213 2 212 eqtrid
 |-  ( ( A e. V /\ F : A --> Top ) -> X = U. B )
214 eqimss2
 |-  ( X = U. B -> U. B C_ X )
215 213 214 syl
 |-  ( ( A e. V /\ F : A --> Top ) -> U. B C_ X )
216 sspwuni
 |-  ( B C_ ~P X <-> U. B C_ X )
217 215 216 sylibr
 |-  ( ( A e. V /\ F : A --> Top ) -> B C_ ~P X )
218 136 217 sstrd
 |-  ( ( A e. V /\ F : A --> Top ) -> ran ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) ) C_ ~P X )
219 211 218 unssd
 |-  ( ( A e. V /\ F : A --> Top ) -> ( { X } u. ran ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) ) ) C_ ~P X )
220 sspwuni
 |-  ( ( { X } u. ran ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) ) ) C_ ~P X <-> U. ( { X } u. ran ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) ) ) C_ X )
221 219 220 sylib
 |-  ( ( A e. V /\ F : A --> Top ) -> U. ( { X } u. ran ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) ) ) C_ X )
222 elssuni
 |-  ( X e. ( { X } u. ran ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) ) ) -> X C_ U. ( { X } u. ran ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) ) ) )
223 145 222 mp1i
 |-  ( ( A e. V /\ F : A --> Top ) -> X C_ U. ( { X } u. ran ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) ) ) )
224 221 223 eqssd
 |-  ( ( A e. V /\ F : A --> Top ) -> U. ( { X } u. ran ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) ) ) = X )
225 208 224 eqtr3d
 |-  ( ( A e. V /\ F : A --> Top ) -> U. ( fi ` ( { X } u. ran ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) ) ) ) = X )
226 225 ad3antrrr
 |-  ( ( ( ( ( A e. V /\ F : A --> Top ) /\ ( h Fn A /\ A. y e. A ( h ` y ) e. ( F ` y ) ) ) /\ ( m e. Fin /\ A. y e. ( A \ m ) ( h ` y ) = U. ( F ` y ) ) ) /\ { z | E. n e. ( A i^i m ) z = ( `' ( w e. X |-> ( w ` n ) ) " ( h ` n ) ) } =/= (/) ) -> U. ( fi ` ( { X } u. ran ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) ) ) ) = X )
227 206 226 sseqtrd
 |-  ( ( ( ( ( A e. V /\ F : A --> Top ) /\ ( h Fn A /\ A. y e. A ( h ` y ) e. ( F ` y ) ) ) /\ ( m e. Fin /\ A. y e. ( A \ m ) ( h ` y ) = U. ( F ` y ) ) ) /\ { z | E. n e. ( A i^i m ) z = ( `' ( w e. X |-> ( w ` n ) ) " ( h ` n ) ) } =/= (/) ) -> |^|_ n e. ( A i^i m ) ( `' ( w e. X |-> ( w ` n ) ) " ( h ` n ) ) C_ X )
228 227 52 sylib
 |-  ( ( ( ( ( A e. V /\ F : A --> Top ) /\ ( h Fn A /\ A. y e. A ( h ` y ) e. ( F ` y ) ) ) /\ ( m e. Fin /\ A. y e. ( A \ m ) ( h ` y ) = U. ( F ` y ) ) ) /\ { z | E. n e. ( A i^i m ) z = ( `' ( w e. X |-> ( w ` n ) ) " ( h ` n ) ) } =/= (/) ) -> ( X i^i |^|_ n e. ( A i^i m ) ( `' ( w e. X |-> ( w ` n ) ) " ( h ` n ) ) ) = |^|_ n e. ( A i^i m ) ( `' ( w e. X |-> ( w ` n ) ) " ( h ` n ) ) )
229 228 204 eqeltrd
 |-  ( ( ( ( ( A e. V /\ F : A --> Top ) /\ ( h Fn A /\ A. y e. A ( h ` y ) e. ( F ` y ) ) ) /\ ( m e. Fin /\ A. y e. ( A \ m ) ( h ` y ) = U. ( F ` y ) ) ) /\ { z | E. n e. ( A i^i m ) z = ( `' ( w e. X |-> ( w ` n ) ) " ( h ` n ) ) } =/= (/) ) -> ( X i^i |^|_ n e. ( A i^i m ) ( `' ( w e. X |-> ( w ` n ) ) " ( h ` n ) ) ) e. ( fi ` ( { X } u. ran ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) ) ) ) )
230 149 229 pm2.61dane
 |-  ( ( ( ( A e. V /\ F : A --> Top ) /\ ( h Fn A /\ A. y e. A ( h ` y ) e. ( F ` y ) ) ) /\ ( m e. Fin /\ A. y e. ( A \ m ) ( h ` y ) = U. ( F ` y ) ) ) -> ( X i^i |^|_ n e. ( A i^i m ) ( `' ( w e. X |-> ( w ` n ) ) " ( h ` n ) ) ) e. ( fi ` ( { X } u. ran ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) ) ) ) )
231 110 230 eqeltrd
 |-  ( ( ( ( A e. V /\ F : A --> Top ) /\ ( h Fn A /\ A. y e. A ( h ` y ) e. ( F ` y ) ) ) /\ ( m e. Fin /\ A. y e. ( A \ m ) ( h ` y ) = U. ( F ` y ) ) ) -> X_ y e. A ( h ` y ) e. ( fi ` ( { X } u. ran ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) ) ) ) )
232 231 rexlimdvaa
 |-  ( ( ( A e. V /\ F : A --> Top ) /\ ( h Fn A /\ A. y e. A ( h ` y ) e. ( F ` y ) ) ) -> ( E. m e. Fin A. y e. ( A \ m ) ( h ` y ) = U. ( F ` y ) -> X_ y e. A ( h ` y ) e. ( fi ` ( { X } u. ran ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) ) ) ) ) )
233 232 impr
 |-  ( ( ( A e. V /\ F : A --> Top ) /\ ( ( h Fn A /\ A. y e. A ( h ` y ) e. ( F ` y ) ) /\ E. m e. Fin A. y e. ( A \ m ) ( h ` y ) = U. ( F ` y ) ) ) -> X_ y e. A ( h ` y ) e. ( fi ` ( { X } u. ran ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) ) ) ) )
234 4 233 sylan2b
 |-  ( ( ( A e. V /\ F : A --> Top ) /\ ( h Fn A /\ A. y e. A ( h ` y ) e. ( F ` y ) /\ E. m e. Fin A. y e. ( A \ m ) ( h ` y ) = U. ( F ` y ) ) ) -> X_ y e. A ( h ` y ) e. ( fi ` ( { X } u. ran ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) ) ) ) )
235 eleq1
 |-  ( s = X_ y e. A ( h ` y ) -> ( s e. ( fi ` ( { X } u. ran ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) ) ) ) <-> X_ y e. A ( h ` y ) e. ( fi ` ( { X } u. ran ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) ) ) ) ) )
236 234 235 syl5ibrcom
 |-  ( ( ( A e. V /\ F : A --> Top ) /\ ( h Fn A /\ A. y e. A ( h ` y ) e. ( F ` y ) /\ E. m e. Fin A. y e. ( A \ m ) ( h ` y ) = U. ( F ` y ) ) ) -> ( s = X_ y e. A ( h ` y ) -> s e. ( fi ` ( { X } u. ran ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) ) ) ) ) )
237 236 expimpd
 |-  ( ( A e. V /\ F : A --> Top ) -> ( ( ( h Fn A /\ A. y e. A ( h ` y ) e. ( F ` y ) /\ E. m e. Fin A. y e. ( A \ m ) ( h ` y ) = U. ( F ` y ) ) /\ s = X_ y e. A ( h ` y ) ) -> s e. ( fi ` ( { X } u. ran ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) ) ) ) ) )
238 237 exlimdv
 |-  ( ( A e. V /\ F : A --> Top ) -> ( E. h ( ( h Fn A /\ A. y e. A ( h ` y ) e. ( F ` y ) /\ E. m e. Fin A. y e. ( A \ m ) ( h ` y ) = U. ( F ` y ) ) /\ s = X_ y e. A ( h ` y ) ) -> s e. ( fi ` ( { X } u. ran ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) ) ) ) ) )
239 3 238 syl5bi
 |-  ( ( A e. V /\ F : A --> Top ) -> ( s e. B -> s e. ( fi ` ( { X } u. ran ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) ) ) ) ) )
240 239 ssrdv
 |-  ( ( A e. V /\ F : A --> Top ) -> B C_ ( fi ` ( { X } u. ran ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) ) ) ) )
241 1 ptbasid
 |-  ( ( A e. V /\ F : A --> Top ) -> X_ n e. A U. ( F ` n ) e. B )
242 2 241 eqeltrid
 |-  ( ( A e. V /\ F : A --> Top ) -> X e. B )
243 242 snssd
 |-  ( ( A e. V /\ F : A --> Top ) -> { X } C_ B )
244 243 136 unssd
 |-  ( ( A e. V /\ F : A --> Top ) -> ( { X } u. ran ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) ) ) C_ B )
245 fiss
 |-  ( ( B e. TopBases /\ ( { X } u. ran ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) ) ) C_ B ) -> ( fi ` ( { X } u. ran ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) ) ) ) C_ ( fi ` B ) )
246 130 244 245 syl2anc
 |-  ( ( A e. V /\ F : A --> Top ) -> ( fi ` ( { X } u. ran ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) ) ) ) C_ ( fi ` B ) )
247 1 ptbasin2
 |-  ( ( A e. V /\ F : A --> Top ) -> ( fi ` B ) = B )
248 246 247 sseqtrd
 |-  ( ( A e. V /\ F : A --> Top ) -> ( fi ` ( { X } u. ran ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) ) ) ) C_ B )
249 240 248 eqssd
 |-  ( ( A e. V /\ F : A --> Top ) -> B = ( fi ` ( { X } u. ran ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) ) ) ) )