Metamath Proof Explorer

Theorem ptclsg

Description: The closure of a box in the product topology is the box formed from the closures of the factors. The proof uses the axiom of choice; the last hypothesis is the choice assumption. (Contributed by Mario Carneiro, 3-Sep-2015)

Ref Expression
Hypotheses ptcls.2 
|- J = ( Xt_ ` ( k e. A |-> R ) )
ptcls.a 
|- ( ph -> A e. V )
ptcls.j 
|- ( ( ph /\ k e. A ) -> R e. ( TopOn ` X ) )
ptcls.c 
|- ( ( ph /\ k e. A ) -> S C_ X )
ptclsg.1 
|- ( ph -> U_ k e. A S e. AC_ A )
Assertion ptclsg 
|- ( ph -> ( ( cls ` J ) ` X_ k e. A S ) = X_ k e. A ( ( cls ` R ) ` S ) )

Proof

Step Hyp Ref Expression
1 ptcls.2 
 |-  J = ( Xt_ ` ( k e. A |-> R ) )
2 ptcls.a 
 |-  ( ph -> A e. V )
3 ptcls.j 
 |-  ( ( ph /\ k e. A ) -> R e. ( TopOn ` X ) )
4 ptcls.c 
 |-  ( ( ph /\ k e. A ) -> S C_ X )
5 ptclsg.1 
 |-  ( ph -> U_ k e. A S e. AC_ A )
6 topontop 
 |-  ( R e. ( TopOn ` X ) -> R e. Top )
7 3 6 syl 
 |-  ( ( ph /\ k e. A ) -> R e. Top )
8 toponuni 
 |-  ( R e. ( TopOn ` X ) -> X = U. R )
9 3 8 syl 
 |-  ( ( ph /\ k e. A ) -> X = U. R )
10 4 9 sseqtrd 
 |-  ( ( ph /\ k e. A ) -> S C_ U. R )
11 eqid 
 |-  U. R = U. R
12 11 clscld 
 |-  ( ( R e. Top /\ S C_ U. R ) -> ( ( cls ` R ) ` S ) e. ( Clsd ` R ) )
13 7 10 12 syl2anc 
 |-  ( ( ph /\ k e. A ) -> ( ( cls ` R ) ` S ) e. ( Clsd ` R ) )
14 2 7 13 ptcldmpt 
 |-  ( ph -> X_ k e. A ( ( cls ` R ) ` S ) e. ( Clsd ` ( Xt_ ` ( k e. A |-> R ) ) ) )
15 1 fveq2i 
 |-  ( Clsd ` J ) = ( Clsd ` ( Xt_ ` ( k e. A |-> R ) ) )
16 14 15 eleqtrrdi 
 |-  ( ph -> X_ k e. A ( ( cls ` R ) ` S ) e. ( Clsd ` J ) )
17 11 sscls 
 |-  ( ( R e. Top /\ S C_ U. R ) -> S C_ ( ( cls ` R ) ` S ) )
18 7 10 17 syl2anc 
 |-  ( ( ph /\ k e. A ) -> S C_ ( ( cls ` R ) ` S ) )
19 18 ralrimiva 
 |-  ( ph -> A. k e. A S C_ ( ( cls ` R ) ` S ) )
20 ss2ixp 
 |-  ( A. k e. A S C_ ( ( cls ` R ) ` S ) -> X_ k e. A S C_ X_ k e. A ( ( cls ` R ) ` S ) )
21 19 20 syl 
 |-  ( ph -> X_ k e. A S C_ X_ k e. A ( ( cls ` R ) ` S ) )
22 eqid 
 |-  U. J = U. J
23 22 clsss2 
 |-  ( ( X_ k e. A ( ( cls ` R ) ` S ) e. ( Clsd ` J ) /\ X_ k e. A S C_ X_ k e. A ( ( cls ` R ) ` S ) ) -> ( ( cls ` J ) ` X_ k e. A S ) C_ X_ k e. A ( ( cls ` R ) ` S ) )
24 16 21 23 syl2anc 
 |-  ( ph -> ( ( cls ` J ) ` X_ k e. A S ) C_ X_ k e. A ( ( cls ` R ) ` S ) )
25 vex 
 |-  u e. _V
26 eqeq1 
 |-  ( x = u -> ( x = X_ y e. A ( g ` y ) <-> u = X_ y e. A ( g ` y ) ) )
27 26 anbi2d 
 |-  ( x = u -> ( ( ( g Fn A /\ A. y e. A ( g ` y ) e. ( ( k e. A |-> R ) ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( ( k e. A |-> R ) ` y ) ) /\ x = X_ y e. A ( g ` y ) ) <-> ( ( g Fn A /\ A. y e. A ( g ` y ) e. ( ( k e. A |-> R ) ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( ( k e. A |-> R ) ` y ) ) /\ u = X_ y e. A ( g ` y ) ) ) )
28 27 exbidv 
 |-  ( x = u -> ( E. g ( ( g Fn A /\ A. y e. A ( g ` y ) e. ( ( k e. A |-> R ) ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( ( k e. A |-> R ) ` y ) ) /\ x = X_ y e. A ( g ` y ) ) <-> E. g ( ( g Fn A /\ A. y e. A ( g ` y ) e. ( ( k e. A |-> R ) ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( ( k e. A |-> R ) ` y ) ) /\ u = X_ y e. A ( g ` y ) ) ) )
29 25 28 elab 
 |-  ( u e. { x | E. g ( ( g Fn A /\ A. y e. A ( g ` y ) e. ( ( k e. A |-> R ) ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( ( k e. A |-> R ) ` y ) ) /\ x = X_ y e. A ( g ` y ) ) } <-> E. g ( ( g Fn A /\ A. y e. A ( g ` y ) e. ( ( k e. A |-> R ) ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( ( k e. A |-> R ) ` y ) ) /\ u = X_ y e. A ( g ` y ) ) )
30 nffvmpt1 
 |-  F/_ k ( ( k e. A |-> R ) ` y )
31 30 nfel2 
 |-  F/ k ( g ` y ) e. ( ( k e. A |-> R ) ` y )
32 nfv 
 |-  F/ y ( g ` k ) e. ( ( k e. A |-> R ) ` k )
33 fveq2 
 |-  ( y = k -> ( g ` y ) = ( g ` k ) )
34 fveq2 
 |-  ( y = k -> ( ( k e. A |-> R ) ` y ) = ( ( k e. A |-> R ) ` k ) )
35 33 34 eleq12d 
 |-  ( y = k -> ( ( g ` y ) e. ( ( k e. A |-> R ) ` y ) <-> ( g ` k ) e. ( ( k e. A |-> R ) ` k ) ) )
36 31 32 35 cbvralw 
 |-  ( A. y e. A ( g ` y ) e. ( ( k e. A |-> R ) ` y ) <-> A. k e. A ( g ` k ) e. ( ( k e. A |-> R ) ` k ) )
37 simpr 
 |-  ( ( ph /\ k e. A ) -> k e. A )
38 eqid 
 |-  ( k e. A |-> R ) = ( k e. A |-> R )
39 38 fvmpt2 
 |-  ( ( k e. A /\ R e. ( TopOn ` X ) ) -> ( ( k e. A |-> R ) ` k ) = R )
40 37 3 39 syl2anc 
 |-  ( ( ph /\ k e. A ) -> ( ( k e. A |-> R ) ` k ) = R )
41 40 eleq2d 
 |-  ( ( ph /\ k e. A ) -> ( ( g ` k ) e. ( ( k e. A |-> R ) ` k ) <-> ( g ` k ) e. R ) )
42 41 ralbidva 
 |-  ( ph -> ( A. k e. A ( g ` k ) e. ( ( k e. A |-> R ) ` k ) <-> A. k e. A ( g ` k ) e. R ) )
43 36 42 syl5bb 
 |-  ( ph -> ( A. y e. A ( g ` y ) e. ( ( k e. A |-> R ) ` y ) <-> A. k e. A ( g ` k ) e. R ) )
44 43 anbi2d 
 |-  ( ph -> ( ( g Fn A /\ A. y e. A ( g ` y ) e. ( ( k e. A |-> R ) ` y ) ) <-> ( g Fn A /\ A. k e. A ( g ` k ) e. R ) ) )
45 44 adantr 
 |-  ( ( ph /\ f e. X_ k e. A ( ( cls ` R ) ` S ) ) -> ( ( g Fn A /\ A. y e. A ( g ` y ) e. ( ( k e. A |-> R ) ` y ) ) <-> ( g Fn A /\ A. k e. A ( g ` k ) e. R ) ) )
46 45 biimpa 
 |-  ( ( ( ph /\ f e. X_ k e. A ( ( cls ` R ) ` S ) ) /\ ( g Fn A /\ A. y e. A ( g ` y ) e. ( ( k e. A |-> R ) ` y ) ) ) -> ( g Fn A /\ A. k e. A ( g ` k ) e. R ) )
47 5 ad2antrr 
 |-  ( ( ( ph /\ f e. X_ k e. A ( ( cls ` R ) ` S ) ) /\ ( ( g Fn A /\ A. k e. A ( g ` k ) e. R ) /\ f e. X_ y e. A ( g ` y ) ) ) -> U_ k e. A S e. AC_ A )
48 simpll 
 |-  ( ( ( ph /\ f e. X_ k e. A ( ( cls ` R ) ` S ) ) /\ ( ( g Fn A /\ A. k e. A ( g ` k ) e. R ) /\ f e. X_ y e. A ( g ` y ) ) ) -> ph )
49 vex 
 |-  f e. _V
50 49 elixp 
 |-  ( f e. X_ k e. A ( ( cls ` R ) ` S ) <-> ( f Fn A /\ A. k e. A ( f ` k ) e. ( ( cls ` R ) ` S ) ) )
51 50 simprbi 
 |-  ( f e. X_ k e. A ( ( cls ` R ) ` S ) -> A. k e. A ( f ` k ) e. ( ( cls ` R ) ` S ) )
52 51 ad2antlr 
 |-  ( ( ( ph /\ f e. X_ k e. A ( ( cls ` R ) ` S ) ) /\ ( ( g Fn A /\ A. k e. A ( g ` k ) e. R ) /\ f e. X_ y e. A ( g ` y ) ) ) -> A. k e. A ( f ` k ) e. ( ( cls ` R ) ` S ) )
53 11 clsndisj 
 |-  ( ( ( R e. Top /\ S C_ U. R /\ ( f ` k ) e. ( ( cls ` R ) ` S ) ) /\ ( ( g ` k ) e. R /\ ( f ` k ) e. ( g ` k ) ) ) -> ( ( g ` k ) i^i S ) =/= (/) )
54 53 ex 
 |-  ( ( R e. Top /\ S C_ U. R /\ ( f ` k ) e. ( ( cls ` R ) ` S ) ) -> ( ( ( g ` k ) e. R /\ ( f ` k ) e. ( g ` k ) ) -> ( ( g ` k ) i^i S ) =/= (/) ) )
55 54 3expia 
 |-  ( ( R e. Top /\ S C_ U. R ) -> ( ( f ` k ) e. ( ( cls ` R ) ` S ) -> ( ( ( g ` k ) e. R /\ ( f ` k ) e. ( g ` k ) ) -> ( ( g ` k ) i^i S ) =/= (/) ) ) )
56 7 10 55 syl2anc 
 |-  ( ( ph /\ k e. A ) -> ( ( f ` k ) e. ( ( cls ` R ) ` S ) -> ( ( ( g ` k ) e. R /\ ( f ` k ) e. ( g ` k ) ) -> ( ( g ` k ) i^i S ) =/= (/) ) ) )
57 56 ralimdva 
 |-  ( ph -> ( A. k e. A ( f ` k ) e. ( ( cls ` R ) ` S ) -> A. k e. A ( ( ( g ` k ) e. R /\ ( f ` k ) e. ( g ` k ) ) -> ( ( g ` k ) i^i S ) =/= (/) ) ) )
58 48 52 57 sylc 
 |-  ( ( ( ph /\ f e. X_ k e. A ( ( cls ` R ) ` S ) ) /\ ( ( g Fn A /\ A. k e. A ( g ` k ) e. R ) /\ f e. X_ y e. A ( g ` y ) ) ) -> A. k e. A ( ( ( g ` k ) e. R /\ ( f ` k ) e. ( g ` k ) ) -> ( ( g ` k ) i^i S ) =/= (/) ) )
59 simprlr 
 |-  ( ( ( ph /\ f e. X_ k e. A ( ( cls ` R ) ` S ) ) /\ ( ( g Fn A /\ A. k e. A ( g ` k ) e. R ) /\ f e. X_ y e. A ( g ` y ) ) ) -> A. k e. A ( g ` k ) e. R )
60 simprr 
 |-  ( ( ( ph /\ f e. X_ k e. A ( ( cls ` R ) ` S ) ) /\ ( ( g Fn A /\ A. k e. A ( g ` k ) e. R ) /\ f e. X_ y e. A ( g ` y ) ) ) -> f e. X_ y e. A ( g ` y ) )
61 33 cbvixpv 
 |-  X_ y e. A ( g ` y ) = X_ k e. A ( g ` k )
62 60 61 eleqtrdi 
 |-  ( ( ( ph /\ f e. X_ k e. A ( ( cls ` R ) ` S ) ) /\ ( ( g Fn A /\ A. k e. A ( g ` k ) e. R ) /\ f e. X_ y e. A ( g ` y ) ) ) -> f e. X_ k e. A ( g ` k ) )
63 49 elixp 
 |-  ( f e. X_ k e. A ( g ` k ) <-> ( f Fn A /\ A. k e. A ( f ` k ) e. ( g ` k ) ) )
64 63 simprbi 
 |-  ( f e. X_ k e. A ( g ` k ) -> A. k e. A ( f ` k ) e. ( g ` k ) )
65 62 64 syl 
 |-  ( ( ( ph /\ f e. X_ k e. A ( ( cls ` R ) ` S ) ) /\ ( ( g Fn A /\ A. k e. A ( g ` k ) e. R ) /\ f e. X_ y e. A ( g ` y ) ) ) -> A. k e. A ( f ` k ) e. ( g ` k ) )
66 r19.26 
 |-  ( A. k e. A ( ( g ` k ) e. R /\ ( f ` k ) e. ( g ` k ) ) <-> ( A. k e. A ( g ` k ) e. R /\ A. k e. A ( f ` k ) e. ( g ` k ) ) )
67 59 65 66 sylanbrc 
 |-  ( ( ( ph /\ f e. X_ k e. A ( ( cls ` R ) ` S ) ) /\ ( ( g Fn A /\ A. k e. A ( g ` k ) e. R ) /\ f e. X_ y e. A ( g ` y ) ) ) -> A. k e. A ( ( g ` k ) e. R /\ ( f ` k ) e. ( g ` k ) ) )
68 ralim 
 |-  ( A. k e. A ( ( ( g ` k ) e. R /\ ( f ` k ) e. ( g ` k ) ) -> ( ( g ` k ) i^i S ) =/= (/) ) -> ( A. k e. A ( ( g ` k ) e. R /\ ( f ` k ) e. ( g ` k ) ) -> A. k e. A ( ( g ` k ) i^i S ) =/= (/) ) )
69 58 67 68 sylc 
 |-  ( ( ( ph /\ f e. X_ k e. A ( ( cls ` R ) ` S ) ) /\ ( ( g Fn A /\ A. k e. A ( g ` k ) e. R ) /\ f e. X_ y e. A ( g ` y ) ) ) -> A. k e. A ( ( g ` k ) i^i S ) =/= (/) )
70 rabn0 
 |-  ( { z e. U_ k e. A S | z e. ( ( g ` k ) i^i S ) } =/= (/) <-> E. z e. U_ k e. A S z e. ( ( g ` k ) i^i S ) )
71 dfin5 
 |-  ( U_ k e. A S i^i ( ( g ` k ) i^i S ) ) = { z e. U_ k e. A S | z e. ( ( g ` k ) i^i S ) }
72 inss2 
 |-  ( ( g ` k ) i^i S ) C_ S
73 ssiun2 
 |-  ( k e. A -> S C_ U_ k e. A S )
74 72 73 sstrid 
 |-  ( k e. A -> ( ( g ` k ) i^i S ) C_ U_ k e. A S )
75 sseqin2 
 |-  ( ( ( g ` k ) i^i S ) C_ U_ k e. A S <-> ( U_ k e. A S i^i ( ( g ` k ) i^i S ) ) = ( ( g ` k ) i^i S ) )
76 74 75 sylib 
 |-  ( k e. A -> ( U_ k e. A S i^i ( ( g ` k ) i^i S ) ) = ( ( g ` k ) i^i S ) )
77 71 76 syl5eqr 
 |-  ( k e. A -> { z e. U_ k e. A S | z e. ( ( g ` k ) i^i S ) } = ( ( g ` k ) i^i S ) )
78 77 neeq1d 
 |-  ( k e. A -> ( { z e. U_ k e. A S | z e. ( ( g ` k ) i^i S ) } =/= (/) <-> ( ( g ` k ) i^i S ) =/= (/) ) )
79 70 78 bitr3id 
 |-  ( k e. A -> ( E. z e. U_ k e. A S z e. ( ( g ` k ) i^i S ) <-> ( ( g ` k ) i^i S ) =/= (/) ) )
80 79 ralbiia 
 |-  ( A. k e. A E. z e. U_ k e. A S z e. ( ( g ` k ) i^i S ) <-> A. k e. A ( ( g ` k ) i^i S ) =/= (/) )
81 69 80 sylibr 
 |-  ( ( ( ph /\ f e. X_ k e. A ( ( cls ` R ) ` S ) ) /\ ( ( g Fn A /\ A. k e. A ( g ` k ) e. R ) /\ f e. X_ y e. A ( g ` y ) ) ) -> A. k e. A E. z e. U_ k e. A S z e. ( ( g ` k ) i^i S ) )
82 nfv 
 |-  F/ y E. z e. U_ k e. A S z e. ( ( g ` k ) i^i S )
83 nfiu1 
 |-  F/_ k U_ k e. A S
84 nfcv 
 |-  F/_ k ( g ` y )
85 nfcsb1v 
 |-  F/_ k [_ y / k ]_ S
86 84 85 nfin 
 |-  F/_ k ( ( g ` y ) i^i [_ y / k ]_ S )
87 86 nfel2 
 |-  F/ k z e. ( ( g ` y ) i^i [_ y / k ]_ S )
88 83 87 nfrex 
 |-  F/ k E. z e. U_ k e. A S z e. ( ( g ` y ) i^i [_ y / k ]_ S )
89 fveq2 
 |-  ( k = y -> ( g ` k ) = ( g ` y ) )
90 csbeq1a 
 |-  ( k = y -> S = [_ y / k ]_ S )
91 89 90 ineq12d 
 |-  ( k = y -> ( ( g ` k ) i^i S ) = ( ( g ` y ) i^i [_ y / k ]_ S ) )
92 91 eleq2d 
 |-  ( k = y -> ( z e. ( ( g ` k ) i^i S ) <-> z e. ( ( g ` y ) i^i [_ y / k ]_ S ) ) )
93 92 rexbidv 
 |-  ( k = y -> ( E. z e. U_ k e. A S z e. ( ( g ` k ) i^i S ) <-> E. z e. U_ k e. A S z e. ( ( g ` y ) i^i [_ y / k ]_ S ) ) )
94 82 88 93 cbvralw 
 |-  ( A. k e. A E. z e. U_ k e. A S z e. ( ( g ` k ) i^i S ) <-> A. y e. A E. z e. U_ k e. A S z e. ( ( g ` y ) i^i [_ y / k ]_ S ) )
95 81 94 sylib 
 |-  ( ( ( ph /\ f e. X_ k e. A ( ( cls ` R ) ` S ) ) /\ ( ( g Fn A /\ A. k e. A ( g ` k ) e. R ) /\ f e. X_ y e. A ( g ` y ) ) ) -> A. y e. A E. z e. U_ k e. A S z e. ( ( g ` y ) i^i [_ y / k ]_ S ) )
96 eleq1 
 |-  ( z = ( h ` y ) -> ( z e. ( ( g ` y ) i^i [_ y / k ]_ S ) <-> ( h ` y ) e. ( ( g ` y ) i^i [_ y / k ]_ S ) ) )
97 96 acni3 
 |-  ( ( U_ k e. A S e. AC_ A /\ A. y e. A E. z e. U_ k e. A S z e. ( ( g ` y ) i^i [_ y / k ]_ S ) ) -> E. h ( h : A --> U_ k e. A S /\ A. y e. A ( h ` y ) e. ( ( g ` y ) i^i [_ y / k ]_ S ) ) )
98 47 95 97 syl2anc 
 |-  ( ( ( ph /\ f e. X_ k e. A ( ( cls ` R ) ` S ) ) /\ ( ( g Fn A /\ A. k e. A ( g ` k ) e. R ) /\ f e. X_ y e. A ( g ` y ) ) ) -> E. h ( h : A --> U_ k e. A S /\ A. y e. A ( h ` y ) e. ( ( g ` y ) i^i [_ y / k ]_ S ) ) )
99 ffn 
 |-  ( h : A --> U_ k e. A S -> h Fn A )
100 nfv 
 |-  F/ y ( h ` k ) e. ( ( g ` k ) i^i S )
101 86 nfel2 
 |-  F/ k ( h ` y ) e. ( ( g ` y ) i^i [_ y / k ]_ S )
102 fveq2 
 |-  ( k = y -> ( h ` k ) = ( h ` y ) )
103 102 91 eleq12d 
 |-  ( k = y -> ( ( h ` k ) e. ( ( g ` k ) i^i S ) <-> ( h ` y ) e. ( ( g ` y ) i^i [_ y / k ]_ S ) ) )
104 100 101 103 cbvralw 
 |-  ( A. k e. A ( h ` k ) e. ( ( g ` k ) i^i S ) <-> A. y e. A ( h ` y ) e. ( ( g ` y ) i^i [_ y / k ]_ S ) )
105 ne0i 
 |-  ( h e. X_ k e. A ( ( g ` k ) i^i S ) -> X_ k e. A ( ( g ` k ) i^i S ) =/= (/) )
106 vex 
 |-  h e. _V
107 106 elixp 
 |-  ( h e. X_ k e. A ( ( g ` k ) i^i S ) <-> ( h Fn A /\ A. k e. A ( h ` k ) e. ( ( g ` k ) i^i S ) ) )
108 ixpin 
 |-  X_ k e. A ( ( g ` k ) i^i S ) = ( X_ k e. A ( g ` k ) i^i X_ k e. A S )
109 61 ineq1i 
 |-  ( X_ y e. A ( g ` y ) i^i X_ k e. A S ) = ( X_ k e. A ( g ` k ) i^i X_ k e. A S )
110 108 109 eqtr4i 
 |-  X_ k e. A ( ( g ` k ) i^i S ) = ( X_ y e. A ( g ` y ) i^i X_ k e. A S )
111 110 neeq1i 
 |-  ( X_ k e. A ( ( g ` k ) i^i S ) =/= (/) <-> ( X_ y e. A ( g ` y ) i^i X_ k e. A S ) =/= (/) )
112 105 107 111 3imtr3i 
 |-  ( ( h Fn A /\ A. k e. A ( h ` k ) e. ( ( g ` k ) i^i S ) ) -> ( X_ y e. A ( g ` y ) i^i X_ k e. A S ) =/= (/) )
113 104 112 sylan2br 
 |-  ( ( h Fn A /\ A. y e. A ( h ` y ) e. ( ( g ` y ) i^i [_ y / k ]_ S ) ) -> ( X_ y e. A ( g ` y ) i^i X_ k e. A S ) =/= (/) )
114 99 113 sylan 
 |-  ( ( h : A --> U_ k e. A S /\ A. y e. A ( h ` y ) e. ( ( g ` y ) i^i [_ y / k ]_ S ) ) -> ( X_ y e. A ( g ` y ) i^i X_ k e. A S ) =/= (/) )
115 114 exlimiv 
 |-  ( E. h ( h : A --> U_ k e. A S /\ A. y e. A ( h ` y ) e. ( ( g ` y ) i^i [_ y / k ]_ S ) ) -> ( X_ y e. A ( g ` y ) i^i X_ k e. A S ) =/= (/) )
116 98 115 syl 
 |-  ( ( ( ph /\ f e. X_ k e. A ( ( cls ` R ) ` S ) ) /\ ( ( g Fn A /\ A. k e. A ( g ` k ) e. R ) /\ f e. X_ y e. A ( g ` y ) ) ) -> ( X_ y e. A ( g ` y ) i^i X_ k e. A S ) =/= (/) )
117 116 expr 
 |-  ( ( ( ph /\ f e. X_ k e. A ( ( cls ` R ) ` S ) ) /\ ( g Fn A /\ A. k e. A ( g ` k ) e. R ) ) -> ( f e. X_ y e. A ( g ` y ) -> ( X_ y e. A ( g ` y ) i^i X_ k e. A S ) =/= (/) ) )
118 46 117 syldan 
 |-  ( ( ( ph /\ f e. X_ k e. A ( ( cls ` R ) ` S ) ) /\ ( g Fn A /\ A. y e. A ( g ` y ) e. ( ( k e. A |-> R ) ` y ) ) ) -> ( f e. X_ y e. A ( g ` y ) -> ( X_ y e. A ( g ` y ) i^i X_ k e. A S ) =/= (/) ) )
119 118 3adantr3 
 |-  ( ( ( ph /\ f e. X_ k e. A ( ( cls ` R ) ` S ) ) /\ ( g Fn A /\ A. y e. A ( g ` y ) e. ( ( k e. A |-> R ) ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( ( k e. A |-> R ) ` y ) ) ) -> ( f e. X_ y e. A ( g ` y ) -> ( X_ y e. A ( g ` y ) i^i X_ k e. A S ) =/= (/) ) )
120 eleq2 
 |-  ( u = X_ y e. A ( g ` y ) -> ( f e. u <-> f e. X_ y e. A ( g ` y ) ) )
121 ineq1 
 |-  ( u = X_ y e. A ( g ` y ) -> ( u i^i X_ k e. A S ) = ( X_ y e. A ( g ` y ) i^i X_ k e. A S ) )
122 121 neeq1d 
 |-  ( u = X_ y e. A ( g ` y ) -> ( ( u i^i X_ k e. A S ) =/= (/) <-> ( X_ y e. A ( g ` y ) i^i X_ k e. A S ) =/= (/) ) )
123 120 122 imbi12d 
 |-  ( u = X_ y e. A ( g ` y ) -> ( ( f e. u -> ( u i^i X_ k e. A S ) =/= (/) ) <-> ( f e. X_ y e. A ( g ` y ) -> ( X_ y e. A ( g ` y ) i^i X_ k e. A S ) =/= (/) ) ) )
124 119 123 syl5ibrcom 
 |-  ( ( ( ph /\ f e. X_ k e. A ( ( cls ` R ) ` S ) ) /\ ( g Fn A /\ A. y e. A ( g ` y ) e. ( ( k e. A |-> R ) ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( ( k e. A |-> R ) ` y ) ) ) -> ( u = X_ y e. A ( g ` y ) -> ( f e. u -> ( u i^i X_ k e. A S ) =/= (/) ) ) )
125 124 expimpd 
 |-  ( ( ph /\ f e. X_ k e. A ( ( cls ` R ) ` S ) ) -> ( ( ( g Fn A /\ A. y e. A ( g ` y ) e. ( ( k e. A |-> R ) ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( ( k e. A |-> R ) ` y ) ) /\ u = X_ y e. A ( g ` y ) ) -> ( f e. u -> ( u i^i X_ k e. A S ) =/= (/) ) ) )
126 125 exlimdv 
 |-  ( ( ph /\ f e. X_ k e. A ( ( cls ` R ) ` S ) ) -> ( E. g ( ( g Fn A /\ A. y e. A ( g ` y ) e. ( ( k e. A |-> R ) ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( ( k e. A |-> R ) ` y ) ) /\ u = X_ y e. A ( g ` y ) ) -> ( f e. u -> ( u i^i X_ k e. A S ) =/= (/) ) ) )
127 29 126 syl5bi 
 |-  ( ( ph /\ f e. X_ k e. A ( ( cls ` R ) ` S ) ) -> ( u e. { x | E. g ( ( g Fn A /\ A. y e. A ( g ` y ) e. ( ( k e. A |-> R ) ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( ( k e. A |-> R ) ` y ) ) /\ x = X_ y e. A ( g ` y ) ) } -> ( f e. u -> ( u i^i X_ k e. A S ) =/= (/) ) ) )
128 127 ralrimiv 
 |-  ( ( ph /\ f e. X_ k e. A ( ( cls ` R ) ` S ) ) -> A. u e. { x | E. g ( ( g Fn A /\ A. y e. A ( g ` y ) e. ( ( k e. A |-> R ) ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( ( k e. A |-> R ) ` y ) ) /\ x = X_ y e. A ( g ` y ) ) } ( f e. u -> ( u i^i X_ k e. A S ) =/= (/) ) )
129 7 fmpttd 
 |-  ( ph -> ( k e. A |-> R ) : A --> Top )
130 129 ffnd 
 |-  ( ph -> ( k e. A |-> R ) Fn A )
131 eqid 
 |-  { x | E. g ( ( g Fn A /\ A. y e. A ( g ` y ) e. ( ( k e. A |-> R ) ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( ( k e. A |-> R ) ` y ) ) /\ x = X_ y e. A ( g ` y ) ) } = { x | E. g ( ( g Fn A /\ A. y e. A ( g ` y ) e. ( ( k e. A |-> R ) ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( ( k e. A |-> R ) ` y ) ) /\ x = X_ y e. A ( g ` y ) ) }
132 131 ptval 
 |-  ( ( A e. V /\ ( k e. A |-> R ) Fn A ) -> ( Xt_ ` ( k e. A |-> R ) ) = ( topGen ` { x | E. g ( ( g Fn A /\ A. y e. A ( g ` y ) e. ( ( k e. A |-> R ) ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( ( k e. A |-> R ) ` y ) ) /\ x = X_ y e. A ( g ` y ) ) } ) )
133 2 130 132 syl2anc 
 |-  ( ph -> ( Xt_ ` ( k e. A |-> R ) ) = ( topGen ` { x | E. g ( ( g Fn A /\ A. y e. A ( g ` y ) e. ( ( k e. A |-> R ) ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( ( k e. A |-> R ) ` y ) ) /\ x = X_ y e. A ( g ` y ) ) } ) )
134 1 133 syl5eq 
 |-  ( ph -> J = ( topGen ` { x | E. g ( ( g Fn A /\ A. y e. A ( g ` y ) e. ( ( k e. A |-> R ) ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( ( k e. A |-> R ) ` y ) ) /\ x = X_ y e. A ( g ` y ) ) } ) )
135 134 adantr 
 |-  ( ( ph /\ f e. X_ k e. A ( ( cls ` R ) ` S ) ) -> J = ( topGen ` { x | E. g ( ( g Fn A /\ A. y e. A ( g ` y ) e. ( ( k e. A |-> R ) ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( ( k e. A |-> R ) ` y ) ) /\ x = X_ y e. A ( g ` y ) ) } ) )
136 3 ralrimiva 
 |-  ( ph -> A. k e. A R e. ( TopOn ` X ) )
137 1 pttopon 
 |-  ( ( A e. V /\ A. k e. A R e. ( TopOn ` X ) ) -> J e. ( TopOn ` X_ k e. A X ) )
138 2 136 137 syl2anc 
 |-  ( ph -> J e. ( TopOn ` X_ k e. A X ) )
139 toponuni 
 |-  ( J e. ( TopOn ` X_ k e. A X ) -> X_ k e. A X = U. J )
140 138 139 syl 
 |-  ( ph -> X_ k e. A X = U. J )
141 140 adantr 
 |-  ( ( ph /\ f e. X_ k e. A ( ( cls ` R ) ` S ) ) -> X_ k e. A X = U. J )
142 131 ptbas 
 |-  ( ( A e. V /\ ( k e. A |-> R ) : A --> Top ) -> { x | E. g ( ( g Fn A /\ A. y e. A ( g ` y ) e. ( ( k e. A |-> R ) ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( ( k e. A |-> R ) ` y ) ) /\ x = X_ y e. A ( g ` y ) ) } e. TopBases )
143 2 129 142 syl2anc 
 |-  ( ph -> { x | E. g ( ( g Fn A /\ A. y e. A ( g ` y ) e. ( ( k e. A |-> R ) ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( ( k e. A |-> R ) ` y ) ) /\ x = X_ y e. A ( g ` y ) ) } e. TopBases )
144 143 adantr 
 |-  ( ( ph /\ f e. X_ k e. A ( ( cls ` R ) ` S ) ) -> { x | E. g ( ( g Fn A /\ A. y e. A ( g ` y ) e. ( ( k e. A |-> R ) ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( ( k e. A |-> R ) ` y ) ) /\ x = X_ y e. A ( g ` y ) ) } e. TopBases )
145 4 ralrimiva 
 |-  ( ph -> A. k e. A S C_ X )
146 ss2ixp 
 |-  ( A. k e. A S C_ X -> X_ k e. A S C_ X_ k e. A X )
147 145 146 syl 
 |-  ( ph -> X_ k e. A S C_ X_ k e. A X )
148 147 adantr 
 |-  ( ( ph /\ f e. X_ k e. A ( ( cls ` R ) ` S ) ) -> X_ k e. A S C_ X_ k e. A X )
149 11 clsss3 
 |-  ( ( R e. Top /\ S C_ U. R ) -> ( ( cls ` R ) ` S ) C_ U. R )
150 7 10 149 syl2anc 
 |-  ( ( ph /\ k e. A ) -> ( ( cls ` R ) ` S ) C_ U. R )
151 150 9 sseqtrrd 
 |-  ( ( ph /\ k e. A ) -> ( ( cls ` R ) ` S ) C_ X )
152 151 ralrimiva 
 |-  ( ph -> A. k e. A ( ( cls ` R ) ` S ) C_ X )
153 ss2ixp 
 |-  ( A. k e. A ( ( cls ` R ) ` S ) C_ X -> X_ k e. A ( ( cls ` R ) ` S ) C_ X_ k e. A X )
154 152 153 syl 
 |-  ( ph -> X_ k e. A ( ( cls ` R ) ` S ) C_ X_ k e. A X )
155 154 sselda 
 |-  ( ( ph /\ f e. X_ k e. A ( ( cls ` R ) ` S ) ) -> f e. X_ k e. A X )
156 135 141 144 148 155 elcls3 
 |-  ( ( ph /\ f e. X_ k e. A ( ( cls ` R ) ` S ) ) -> ( f e. ( ( cls ` J ) ` X_ k e. A S ) <-> A. u e. { x | E. g ( ( g Fn A /\ A. y e. A ( g ` y ) e. ( ( k e. A |-> R ) ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( ( k e. A |-> R ) ` y ) ) /\ x = X_ y e. A ( g ` y ) ) } ( f e. u -> ( u i^i X_ k e. A S ) =/= (/) ) ) )
157 128 156 mpbird 
 |-  ( ( ph /\ f e. X_ k e. A ( ( cls ` R ) ` S ) ) -> f e. ( ( cls ` J ) ` X_ k e. A S ) )
158 24 157 eqelssd 
 |-  ( ph -> ( ( cls ` J ) ` X_ k e. A S ) = X_ k e. A ( ( cls ` R ) ` S ) )