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