Theorem ptclsg 19879

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.)

Hypotheses

Ref	Expression
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

Ref	Expression
ptclsg	|- ( ph -> ( ( cls ` J ) ` X_ k e. A S ) = X_ k e. A ( ( cls ` R ) ` S ) )

Distinct variable groups:   ph, k   A, k

Allowed substitution hints:   R( k)   S( k)   J( k)   V( k)   X( k)

Proof of Theorem ptclsg

Dummy variables f g u x y z h are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ptcls.a	. . . . 5 |- ( ph -> A e. V )
2		ptcls.j	. . . . . 6 |- ( ( ph /\ k e. A ) -> R e. (TopOn ` X ) )
3		topontop 19222	. . . . . 6 |- ( R e. (TopOn ` X ) -> R e. Top )
4	2, 3	syl 16	. . . . 5 |- ( ( ph /\ k e. A ) -> R e. Top )
5		ptcls.c	. . . . . . 7 |- ( ( ph /\ k e. A ) -> S C_ X )
6		toponuni 19223	. . . . . . . 8 |- ( R e. (TopOn ` X ) -> X = U. R )
7	2, 6	syl 16	. . . . . . 7 |- ( ( ph /\ k e. A ) -> X = U. R )
8	5, 7	sseqtrd 3540	. . . . . 6 |- ( ( ph /\ k e. A ) -> S C_ U. R )
9		eqid 2467	. . . . . . 7 |- U. R = U. R
10	9	clscld 19342	. . . . . 6 |- ( ( R e. Top /\ S C_ U. R ) -> ( ( cls ` R ) ` S ) e. ( Clsd ` R ) )
11	4, 8, 10	syl2anc 661	. . . . 5 |- ( ( ph /\ k e. A ) -> ( ( cls ` R ) ` S ) e. ( Clsd ` R ) )
12	1, 4, 11	ptcldmpt 19878	. . . 4 |- ( ph -> X_ k e. A ( ( cls ` R ) ` S ) e. ( Clsd ` ( Xt_ ` ( k e. A |-> R ) ) ) )
13		ptcls.2	. . . . 5 |- J = ( Xt_ ` ( k e. A |-> R ) )
14	13	fveq2i 5869	. . . 4 |- ( Clsd ` J ) = ( Clsd ` ( Xt_ ` ( k e. A |-> R ) ) )
15	12, 14	syl6eleqr 2566	. . 3 |- ( ph -> X_ k e. A ( ( cls ` R ) ` S ) e. ( Clsd ` J ) )
16	9	sscls 19351	. . . . . 6 |- ( ( R e. Top /\ S C_ U. R ) -> S C_ ( ( cls ` R ) ` S ) )
17	4, 8, 16	syl2anc 661	. . . . 5 |- ( ( ph /\ k e. A ) -> S C_ ( ( cls ` R ) ` S ) )
18	17	ralrimiva 2878	. . . 4 |- ( ph -> A. k e. A S C_ ( ( cls ` R ) ` S ) )
19		ss2ixp 7482	. . . 4 |- ( A. k e. A S C_ ( ( cls ` R ) ` S ) -> X_ k e. A S C_ X_ k e. A ( ( cls ` R ) ` S ) )
20	18, 19	syl 16	. . 3 |- ( ph -> X_ k e. A S C_ X_ k e. A ( ( cls ` R ) ` S ) )
21		eqid 2467	. . . 4 |- U. J = U. J
22	21	clsss2 19367	. . 3 |- ( ( 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 ) )
23	15, 20, 22	syl2anc 661	. 2 |- ( ph -> ( ( cls ` J ) ` X_ k e. A S ) C_ X_ k e. A ( ( cls ` R ) ` S ) )
24		vex 3116	. . . . . . . 8 |- u e. _V
25		eqeq1 2471	. . . . . . . . . 10 |- ( x = u -> ( x = X_ y e. A ( g ` y ) <-> u = X_ y e. A ( g ` y ) ) )
26	25	anbi2d 703	. . . . . . . . 9 |- ( 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 ) ) ) )
27	26	exbidv 1690	. . . . . . . 8 |- ( 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 ) ) ) )
28	24, 27	elab 3250	. . . . . . 7 |- ( 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 ) ) )
29		nffvmpt1 5874	. . . . . . . . . . . . . . . . . 18 |- F/_ k ( ( k e. A |-> R ) ` y )
30	29	nfel2 2647	. . . . . . . . . . . . . . . . 17 |- F/ k ( g ` y ) e. ( ( k e. A |-> R ) ` y )
31		nfv 1683	. . . . . . . . . . . . . . . . 17 |- F/ y ( g ` k ) e. ( ( k e. A |-> R ) ` k )
32		fveq2 5866	. . . . . . . . . . . . . . . . . 18 |- ( y = k -> ( g ` y ) = ( g ` k ) )
33		fveq2 5866	. . . . . . . . . . . . . . . . . 18 |- ( y = k -> ( ( k e. A |-> R ) ` y ) = ( ( k e. A |-> R ) ` k ) )
34	32, 33	eleq12d 2549	. . . . . . . . . . . . . . . . 17 |- ( y = k -> ( ( g ` y ) e. ( ( k e. A |-> R ) ` y ) <-> ( g ` k ) e. ( ( k e. A |-> R ) ` k ) ) )
35	30, 31, 34	cbvral 3084	. . . . . . . . . . . . . . . 16 |- ( A. y e. A ( g ` y ) e. ( ( k e. A |-> R ) ` y ) <-> A. k e. A ( g ` k ) e. ( ( k e. A |-> R ) ` k ) )
36		simpr 461	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ k e. A ) -> k e. A )
37		eqid 2467	. . . . . . . . . . . . . . . . . . . 20 |- ( k e. A |-> R ) = ( k e. A |-> R )
38	37	fvmpt2 5957	. . . . . . . . . . . . . . . . . . 19 |- ( ( k e. A /\ R e. (TopOn ` X ) ) -> ( ( k e. A |-> R ) ` k ) = R )
39	36, 2, 38	syl2anc 661	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ k e. A ) -> ( ( k e. A |-> R ) ` k ) = R )
40	39	eleq2d 2537	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ k e. A ) -> ( ( g ` k ) e. ( ( k e. A |-> R ) ` k ) <-> ( g ` k ) e. R ) )
41	40	ralbidva 2900	. . . . . . . . . . . . . . . 16 |- ( ph -> ( A. k e. A ( g ` k ) e. ( ( k e. A |-> R ) ` k ) <-> A. k e. A ( g ` k ) e. R ) )
42	35, 41	syl5bb 257	. . . . . . . . . . . . . . 15 |- ( ph -> ( A. y e. A ( g ` y ) e. ( ( k e. A |-> R ) ` y ) <-> A. k e. A ( g ` k ) e. R ) )
43	42	anbi2d 703	. . . . . . . . . . . . . 14 |- ( 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 ) ) )
44	43	adantr 465	. . . . . . . . . . . . 13 |- ( ( 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 ) ) )
45	44	biimpa 484	. . . . . . . . . . . 12 |- ( ( ( 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		ptclsg.1	. . . . . . . . . . . . . . . 16 |- ( ph -> U_ k e. A S e. AC A )
47	46	ad2antrr 725	. . . . . . . . . . . . . . 15 |- ( ( ( 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 753	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( 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 3116	. . . . . . . . . . . . . . . . . . . . . 22 |- f e. _V
50	49	elixp 7476	. . . . . . . . . . . . . . . . . . . . 21 |- ( 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 464	. . . . . . . . . . . . . . . . . . . 20 |- ( f e. X_ k e. A ( ( cls ` R ) ` S ) -> A. k e. A ( f ` k ) e. ( ( cls ` R ) ` S ) )
52	51	ad2antlr 726	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( 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	9	clsndisj 19370	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( 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 434	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( 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 1198	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( 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	4, 8, 55	syl2anc 661	. . . . . . . . . . . . . . . . . . . 20 |- ( ( 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 2872	. . . . . . . . . . . . . . . . . . 19 |- ( 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 60	. . . . . . . . . . . . . . . . . 18 |- ( ( ( 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 762	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( 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 756	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( 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	32	cbvixpv 7487	. . . . . . . . . . . . . . . . . . . . 21 |- X_ y e. A ( g ` y ) = X_ k e. A ( g ` k )
62	60, 61	syl6eleq 2565	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( 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 7476	. . . . . . . . . . . . . . . . . . . . 21 |- ( f e. X_ k e. A ( g ` k ) <-> ( f Fn A /\ A. k e. A ( f ` k ) e. ( g ` k ) ) )
64	63	simprbi 464	. . . . . . . . . . . . . . . . . . . 20 |- ( f e. X_ k e. A ( g ` k ) -> A. k e. A ( f ` k ) e. ( g ` k ) )
65	62, 64	syl 16	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( 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 2989	. . . . . . . . . . . . . . . . . . 19 |- ( 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 664	. . . . . . . . . . . . . . . . . 18 |- ( ( ( 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 2853	. . . . . . . . . . . . . . . . . 18 |- ( 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 60	. . . . . . . . . . . . . . . . 17 |- ( ( ( 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 3805	. . . . . . . . . . . . . . . . . . 19 |- ( { 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 3484	. . . . . . . . . . . . . . . . . . . . 21 |- ( 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 3719	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( g ` k ) i^i S ) C_ S
73		ssiun2 4368	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( k e. A -> S C_ U_ k e. A S )
74	72, 73	syl5ss 3515	. . . . . . . . . . . . . . . . . . . . . 22 |- ( k e. A -> ( ( g ` k ) i^i S ) C_ U_ k e. A S )
75		dfss1 3703	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( 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 196	. . . . . . . . . . . . . . . . . . . . 21 |- ( k e. A -> ( U_ k e. A S i^i ( ( g ` k ) i^i S ) ) = ( ( g ` k ) i^i S ) )
77	71, 76	syl5eqr 2522	. . . . . . . . . . . . . . . . . . . 20 |- ( 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 2744	. . . . . . . . . . . . . . . . . . 19 |- ( 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	syl5bbr 259	. . . . . . . . . . . . . . . . . 18 |- ( 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 2894	. . . . . . . . . . . . . . . . 17 |- ( 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 212	. . . . . . . . . . . . . . . 16 |- ( ( ( 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 1683	. . . . . . . . . . . . . . . . 17 |- F/ y E. z e. U_ k e. A S z e. ( ( g ` k ) i^i S )
83		nfiu1 4355	. . . . . . . . . . . . . . . . . 18 |- F/_ k U_ k e. A S
84		nfcv 2629	. . . . . . . . . . . . . . . . . . . 20 |- F/_ k ( g ` y )
85		nfcsb1v 3451	. . . . . . . . . . . . . . . . . . . 20 |- F/_ k [_ y / k ]_ S
86	84, 85	nfin 3705	. . . . . . . . . . . . . . . . . . 19 |- F/_ k ( ( g ` y ) i^i [_ y / k ]_ S )
87	86	nfel2 2647	. . . . . . . . . . . . . . . . . 18 |- F/ k z e. ( ( g ` y ) i^i [_ y / k ]_ S )
88	83, 87	nfrex 2927	. . . . . . . . . . . . . . . . 17 |- F/ k E. z e. U_ k e. A S z e. ( ( g ` y ) i^i [_ y / k ]_ S )
89		fveq2 5866	. . . . . . . . . . . . . . . . . . . 20 |- ( k = y -> ( g ` k ) = ( g ` y ) )
90		csbeq1a 3444	. . . . . . . . . . . . . . . . . . . 20 |- ( k = y -> S = [_ y / k ]_ S )
91	89, 90	ineq12d 3701	. . . . . . . . . . . . . . . . . . 19 |- ( k = y -> ( ( g ` k ) i^i S ) = ( ( g ` y ) i^i [_ y / k ]_ S ) )
92	91	eleq2d 2537	. . . . . . . . . . . . . . . . . 18 |- ( k = y -> ( z e. ( ( g ` k ) i^i S ) <-> z e. ( ( g ` y ) i^i [_ y / k ]_ S ) ) )
93	92	rexbidv 2973	. . . . . . . . . . . . . . . . 17 |- ( 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	cbvral 3084	. . . . . . . . . . . . . . . 16 |- ( 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 196	. . . . . . . . . . . . . . 15 |- ( ( ( 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 2539	. . . . . . . . . . . . . . . 16 |- ( 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 8428	. . . . . . . . . . . . . . 15 |- ( ( 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 661	. . . . . . . . . . . . . 14 |- ( ( ( 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 5731	. . . . . . . . . . . . . . . 16 |- ( h : A --> U_ k e. A S -> h Fn A )
100		nfv 1683	. . . . . . . . . . . . . . . . . 18 |- F/ y ( h ` k ) e. ( ( g ` k ) i^i S )
101	86	nfel2 2647	. . . . . . . . . . . . . . . . . 18 |- F/ k ( h ` y ) e. ( ( g ` y ) i^i [_ y / k ]_ S )
102		fveq2 5866	. . . . . . . . . . . . . . . . . . 19 |- ( k = y -> ( h ` k ) = ( h ` y ) )
103	102, 91	eleq12d 2549	. . . . . . . . . . . . . . . . . 18 |- ( k = y -> ( ( h ` k ) e. ( ( g ` k ) i^i S ) <-> ( h ` y ) e. ( ( g ` y ) i^i [_ y / k ]_ S ) ) )
104	100, 101, 103	cbvral 3084	. . . . . . . . . . . . . . . . 17 |- ( 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 3791	. . . . . . . . . . . . . . . . . 18 |- ( h e. X_ k e. A ( ( g ` k ) i^i S ) -> X_ k e. A ( ( g ` k ) i^i S ) =/= (/) )
106		vex 3116	. . . . . . . . . . . . . . . . . . 19 |- h e. _V
107	106	elixp 7476	. . . . . . . . . . . . . . . . . 18 |- ( 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 7494	. . . . . . . . . . . . . . . . . . . 20 |- 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 3696	. . . . . . . . . . . . . . . . . . . 20 |- ( 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 2499	. . . . . . . . . . . . . . . . . . 19 |- 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 2752	. . . . . . . . . . . . . . . . . 18 |- ( 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 265	. . . . . . . . . . . . . . . . 17 |- ( ( 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 476	. . . . . . . . . . . . . . . 16 |- ( ( 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 471	. . . . . . . . . . . . . . 15 |- ( ( 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 1698	. . . . . . . . . . . . . 14 |- ( 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 16	. . . . . . . . . . . . 13 |- ( ( ( 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 615	. . . . . . . . . . . 12 |- ( ( ( 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	45, 117	syldan 470	. . . . . . . . . . 11 |- ( ( ( 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 1157	. . . . . . . . . 10 |- ( ( ( 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 2540	. . . . . . . . . . 11 |- ( u = X_ y e. A ( g ` y ) -> ( f e. u <-> f e. X_ y e. A ( g ` y ) ) )
121		ineq1 3693	. . . . . . . . . . . 12 |- ( 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 2744	. . . . . . . . . . 11 |- ( 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 320	. . . . . . . . . 10 |- ( 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 222	. . . . . . . . 9 |- ( ( ( 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 603	. . . . . . . 8 |- ( ( 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 1700	. . . . . . 7 |- ( ( 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	28, 126	syl5bi 217	. . . . . 6 |- ( ( 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 2876	. . . . 5 |- ( ( 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	4, 37	fmptd 6045	. . . . . . . . . 10 |- ( ph -> ( k e. A |-> R ) : A --> Top )
130		ffn 5731	. . . . . . . . . 10 |- ( ( k e. A |-> R ) : A --> Top -> ( k e. A |-> R ) Fn A )
131	129, 130	syl 16	. . . . . . . . 9 |- ( ph -> ( k e. A |-> R ) Fn A )
132		eqid 2467	. . . . . . . . . 10 |- { 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 ) ) }
133	132	ptval 19834	. . . . . . . . 9 |- ( ( 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 ) ) } ) )
134	1, 131, 133	syl2anc 661	. . . . . . . 8 |- ( 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 ) ) } ) )
135	13, 134	syl5eq 2520	. . . . . . 7 |- ( 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 ) ) } ) )
136	135	adantr 465	. . . . . 6 |- ( ( 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 ) ) } ) )
137	2	ralrimiva 2878	. . . . . . . . 9 |- ( ph -> A. k e. A R e. (TopOn ` X ) )
138	13	pttopon 19860	. . . . . . . . 9 |- ( ( A e. V /\ A. k e. A R e. (TopOn ` X ) ) -> J e. (TopOn ` X_ k e. A X ) )
139	1, 137, 138	syl2anc 661	. . . . . . . 8 |- ( ph -> J e. (TopOn ` X_ k e. A X ) )
140		toponuni 19223	. . . . . . . 8 |- ( J e. (TopOn ` X_ k e. A X ) -> X_ k e. A X = U. J )
141	139, 140	syl 16	. . . . . . 7 |- ( ph -> X_ k e. A X = U. J )
142	141	adantr 465	. . . . . 6 |- ( ( ph /\ f e. X_ k e. A ( ( cls ` R ) ` S ) ) -> X_ k e. A X = U. J )
143	132	ptbas 19843	. . . . . . . 8 |- ( ( 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 )
144	1, 129, 143	syl2anc 661	. . . . . . 7 |- ( 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 )
145	144	adantr 465	. . . . . 6 |- ( ( 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 )
146	5	ralrimiva 2878	. . . . . . . 8 |- ( ph -> A. k e. A S C_ X )
147		ss2ixp 7482	. . . . . . . 8 |- ( A. k e. A S C_ X -> X_ k e. A S C_ X_ k e. A X )
148	146, 147	syl 16	. . . . . . 7 |- ( ph -> X_ k e. A S C_ X_ k e. A X )
149	148	adantr 465	. . . . . 6 |- ( ( ph /\ f e. X_ k e. A ( ( cls ` R ) ` S ) ) -> X_ k e. A S C_ X_ k e. A X )
150	9	clsss3 19354	. . . . . . . . . . 11 |- ( ( R e. Top /\ S C_ U. R ) -> ( ( cls ` R ) ` S ) C_ U. R )
151	4, 8, 150	syl2anc 661	. . . . . . . . . 10 |- ( ( ph /\ k e. A ) -> ( ( cls ` R ) ` S ) C_ U. R )
152	151, 7	sseqtr4d 3541	. . . . . . . . 9 |- ( ( ph /\ k e. A ) -> ( ( cls ` R ) ` S ) C_ X )
153	152	ralrimiva 2878	. . . . . . . 8 |- ( ph -> A. k e. A ( ( cls ` R ) ` S ) C_ X )
154		ss2ixp 7482	. . . . . . . 8 |- ( A. k e. A ( ( cls ` R ) ` S ) C_ X -> X_ k e. A ( ( cls ` R ) ` S ) C_ X_ k e. A X )
155	153, 154	syl 16	. . . . . . 7 |- ( ph -> X_ k e. A ( ( cls ` R ) ` S ) C_ X_ k e. A X )
156	155	sselda 3504	. . . . . 6 |- ( ( ph /\ f e. X_ k e. A ( ( cls ` R ) ` S ) ) -> f e. X_ k e. A X )
157	136, 142, 145, 149, 156	elcls3 19378	. . . . 5 |- ( ( 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 ) =/= (/) ) ) )
158	128, 157	mpbird 232	. . . 4 |- ( ( ph /\ f e. X_ k e. A ( ( cls ` R ) ` S ) ) -> f e. ( ( cls ` J ) ` X_ k e. A S ) )
159	158	ex 434	. . 3 |- ( ph -> ( f e. X_ k e. A ( ( cls ` R ) ` S ) -> f e. ( ( cls ` J ) ` X_ k e. A S ) ) )
160	159	ssrdv 3510	. 2 |- ( ph -> X_ k e. A ( ( cls ` R ) ` S ) C_ ( ( cls ` J ) ` X_ k e. A S ) )
161	23, 160	eqssd 3521	1 |- ( ph -> ( ( cls ` J ) ` X_ k e. A S ) = X_ k e. A ( ( cls ` R ) ` S ) )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369   /\ w3a 973   = wceq 1379   E.wex 1596   e. wcel 1767   {cab 2452   =/= wne 2662   A.wral 2814   E.wrex 2815   {crab 2818   [_csb 3435   \ cdif 3473   i^i cin 3475   C_ wss 3476   (/)c0 3785   U.cuni 4245   U_ciun 4325   |-> cmpt 4505   Fn wfn 5583   -->wf 5584   ` cfv 5588   X_cixp 7469   Fincfn 7516  AC wacn 8319   topGenctg 14693   Xt_cpt 14694   Topctop 19189  TopOnctopon 19190   TopBasesctb 19193   Clsdccld 19311   clsccl 19313

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-rep 4558  ax-sep 4568  ax-nul 4576  ax-pow 4625  ax-pr 4686  ax-un 6576

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2819  df-rex 2820  df-reu 2821  df-rab 2823  df-v 3115  df-sbc 3332  df-csb 3436  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-pss 3492  df-nul 3786  df-if 3940  df-pw 4012  df-sn 4028  df-pr 4030  df-tp 4032  df-op 4034  df-uni 4246  df-int 4283  df-iun 4327  df-iin 4328  df-br 4448  df-opab 4506  df-mpt 4507  df-tr 4541  df-eprel 4791  df-id 4795  df-po 4800  df-so 4801  df-fr 4838  df-we 4840  df-ord 4881  df-on 4882  df-lim 4883  df-suc 4884  df-xp 5005  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-rn 5010  df-res 5011  df-ima 5012  df-iota 5551  df-fun 5590  df-fn 5591  df-f 5592  df-f1 5593  df-fo 5594  df-f1o 5595  df-fv 5596  df-ov 6287  df-oprab 6288  df-mpt2 6289  df-om 6685  df-recs 7042  df-rdg 7076  df-1o 7130  df-oadd 7134  df-er 7311  df-map 7422  df-ixp 7470  df-en 7517  df-fin 7520  df-fi 7871  df-acn 8323  df-topgen 14699  df-pt 14700  df-top 19194  df-bases 19196  df-topon 19197  df-cld 19314  df-ntr 19315  df-cls 19316

This theorem is referenced by:  ptcls  19880  dfac14  19882