Theorem ptclsg 19188

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 18531	. . . . . 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 18532	. . . . . . . 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 3392	. . . . . 6 |- ( ( ph /\ k e. A ) -> S C_ U. R )
9		eqid 2443	. . . . . . 7 |- U. R = U. R
10	9	clscld 18651	. . . . . 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 19187	. . . 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 5694	. . . 4 |- ( Clsd ` J ) = ( Clsd ` ( Xt_ ` ( k e. A |-> R ) ) )
15	12, 14	syl6eleqr 2534	. . 3 |- ( ph -> X_ k e. A ( ( cls ` R ) ` S ) e. ( Clsd ` J ) )
16	9	sscls 18660	. . . . . 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 2799	. . . 4 |- ( ph -> A. k e. A S C_ ( ( cls ` R ) ` S ) )
19		ss2ixp 7276	. . . 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 2443	. . . 4 |- U. J = U. J
22	21	clsss2 18676	. . 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 2975	. . . . . . . 8 |- u e. _V
25		eqeq1 2449	. . . . . . . . . 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 1680	. . . . . . . 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 3106	. . . . . . 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 5699	. . . . . . . . . . . . . . . . . 18 |- F/_ k ( ( k e. A |-> R ) ` y )
30	29	nfel2 2591	. . . . . . . . . . . . . . . . 17 |- F/ k ( g ` y ) e. ( ( k e. A |-> R ) ` y )
31		nfv 1673	. . . . . . . . . . . . . . . . 17 |- F/ y ( g ` k ) e. ( ( k e. A |-> R ) ` k )
32		fveq2 5691	. . . . . . . . . . . . . . . . . 18 |- ( y = k -> ( g ` y ) = ( g ` k ) )
33		fveq2 5691	. . . . . . . . . . . . . . . . . 18 |- ( y = k -> ( ( k e. A |-> R ) ` y ) = ( ( k e. A |-> R ) ` k ) )
34	32, 33	eleq12d 2511	. . . . . . . . . . . . . . . . 17 |- ( y = k -> ( ( g ` y ) e. ( ( k e. A |-> R ) ` y ) <-> ( g ` k ) e. ( ( k e. A |-> R ) ` k ) ) )
35	30, 31, 34	cbvral 2943	. . . . . . . . . . . . . . . 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 2443	. . . . . . . . . . . . . . . . . . . 20 |- ( k e. A |-> R ) = ( k e. A |-> R )
38	37	fvmpt2 5781	. . . . . . . . . . . . . . . . . . 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 2510	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ k e. A ) -> ( ( g ` k ) e. ( ( k e. A |-> R ) ` k ) <-> ( g ` k ) e. R ) )
41	40	ralbidva 2731	. . . . . . . . . . . . . . . 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 2975	. . . . . . . . . . . . . . . . . . . . . 22 |- f e. _V
50	49	elixp 7270	. . . . . . . . . . . . . . . . . . . . 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 18679	. . . . . . . . . . . . . . . . . . . . . . 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 1189	. . . . . . . . . . . . . . . . . . . . 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 2794	. . . . . . . . . . . . . . . . . . 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 7281	. . . . . . . . . . . . . . . . . . . . 21 |- X_ y e. A ( g ` y ) = X_ k e. A ( g ` k )
62	60, 61	syl6eleq 2533	. . . . . . . . . . . . . . . . . . . 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 7270	. . . . . . . . . . . . . . . . . . . . 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 2849	. . . . . . . . . . . . . . . . . . 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 2787	. . . . . . . . . . . . . . . . . 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 3657	. . . . . . . . . . . . . . . . . . 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 3336	. . . . . . . . . . . . . . . . . . . . 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 3571	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( g ` k ) i^i S ) C_ S
73		ssiun2 4213	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( k e. A -> S C_ U_ k e. A S )
74	72, 73	syl5ss 3367	. . . . . . . . . . . . . . . . . . . . . 22 |- ( k e. A -> ( ( g ` k ) i^i S ) C_ U_ k e. A S )
75		dfss1 3555	. . . . . . . . . . . . . . . . . . . . . 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 2489	. . . . . . . . . . . . . . . . . . . 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 2621	. . . . . . . . . . . . . . . . . . 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 2747	. . . . . . . . . . . . . . . . 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 1673	. . . . . . . . . . . . . . . . 17 |- F/ y E. z e. U_ k e. A S z e. ( ( g ` k ) i^i S )
83		nfiu1 4200	. . . . . . . . . . . . . . . . . 18 |- F/_ k U_ k e. A S
84		nfcv 2579	. . . . . . . . . . . . . . . . . . . 20 |- F/_ k ( g ` y )
85		nfcsb1v 3304	. . . . . . . . . . . . . . . . . . . 20 |- F/_ k [_ y / k ]_ S
86	84, 85	nfin 3557	. . . . . . . . . . . . . . . . . . 19 |- F/_ k ( ( g ` y ) i^i [_ y / k ]_ S )
87	86	nfel2 2591	. . . . . . . . . . . . . . . . . 18 |- F/ k z e. ( ( g ` y ) i^i [_ y / k ]_ S )
88	83, 87	nfrex 2771	. . . . . . . . . . . . . . . . 17 |- F/ k E. z e. U_ k e. A S z e. ( ( g ` y ) i^i [_ y / k ]_ S )
89		fveq2 5691	. . . . . . . . . . . . . . . . . . . 20 |- ( k = y -> ( g ` k ) = ( g ` y ) )
90		csbeq1a 3297	. . . . . . . . . . . . . . . . . . . 20 |- ( k = y -> S = [_ y / k ]_ S )
91	89, 90	ineq12d 3553	. . . . . . . . . . . . . . . . . . 19 |- ( k = y -> ( ( g ` k ) i^i S ) = ( ( g ` y ) i^i [_ y / k ]_ S ) )
92	91	eleq2d 2510	. . . . . . . . . . . . . . . . . 18 |- ( k = y -> ( z e. ( ( g ` k ) i^i S ) <-> z e. ( ( g ` y ) i^i [_ y / k ]_ S ) ) )
93	92	rexbidv 2736	. . . . . . . . . . . . . . . . 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 2943	. . . . . . . . . . . . . . . 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 2503	. . . . . . . . . . . . . . . 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 8217	. . . . . . . . . . . . . . 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 5559	. . . . . . . . . . . . . . . 16 |- ( h : A --> U_ k e. A S -> h Fn A )
100		nfv 1673	. . . . . . . . . . . . . . . . . 18 |- F/ y ( h ` k ) e. ( ( g ` k ) i^i S )
101	86	nfel2 2591	. . . . . . . . . . . . . . . . . 18 |- F/ k ( h ` y ) e. ( ( g ` y ) i^i [_ y / k ]_ S )
102		fveq2 5691	. . . . . . . . . . . . . . . . . . 19 |- ( k = y -> ( h ` k ) = ( h ` y ) )
103	102, 91	eleq12d 2511	. . . . . . . . . . . . . . . . . 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 2943	. . . . . . . . . . . . . . . . 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 3643	. . . . . . . . . . . . . . . . . 18 |- ( h e. X_ k e. A ( ( g ` k ) i^i S ) -> X_ k e. A ( ( g ` k ) i^i S ) =/= (/) )
106		vex 2975	. . . . . . . . . . . . . . . . . . 19 |- h e. _V
107	106	elixp 7270	. . . . . . . . . . . . . . . . . 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 7288	. . . . . . . . . . . . . . . . . . . 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 3548	. . . . . . . . . . . . . . . . . . . 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 2466	. . . . . . . . . . . . . . . . . . 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 2618	. . . . . . . . . . . . . . . . . 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 1688	. . . . . . . . . . . . . 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 1149	. . . . . . . . . 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 2504	. . . . . . . . . . 11 |- ( u = X_ y e. A ( g ` y ) -> ( f e. u <-> f e. X_ y e. A ( g ` y ) ) )
121		ineq1 3545	. . . . . . . . . . . 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 2621	. . . . . . . . . . 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 1690	. . . . . . 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 2798	. . . . 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 5867	. . . . . . . . . 10 |- ( ph -> ( k e. A |-> R ) : A --> Top )
130		ffn 5559	. . . . . . . . . 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 2443	. . . . . . . . . 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 19143	. . . . . . . . 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 2487	. . . . . . 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 2799	. . . . . . . . 9 |- ( ph -> A. k e. A R e. (TopOn ` X ) )
138	13	pttopon 19169	. . . . . . . . 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 18532	. . . . . . . 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 19152	. . . . . . . 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 2799	. . . . . . . 8 |- ( ph -> A. k e. A S C_ X )
147		ss2ixp 7276	. . . . . . . 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 18663	. . . . . . . . . . 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 3393	. . . . . . . . 9 |- ( ( ph /\ k e. A ) -> ( ( cls ` R ) ` S ) C_ X )
153	152	ralrimiva 2799	. . . . . . . 8 |- ( ph -> A. k e. A ( ( cls ` R ) ` S ) C_ X )
154		ss2ixp 7276	. . . . . . . 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 3356	. . . . . 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 18687	. . . . 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 3362	. 2 |- ( ph -> X_ k e. A ( ( cls ` R ) ` S ) C_ ( ( cls ` J ) ` X_ k e. A S ) )
161	23, 160	eqssd 3373	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 965   = wceq 1369   E.wex 1586   e. wcel 1756   {cab 2429   =/= wne 2606   A.wral 2715   E.wrex 2716   {crab 2719   [_csb 3288   \ cdif 3325   i^i cin 3327   C_ wss 3328   (/)c0 3637   U.cuni 4091   U_ciun 4171   e. cmpt 4350   Fn wfn 5413   -->wf 5414   ` cfv 5418   X_cixp 7263   Fincfn 7310  AC wacn 8108   topGenctg 14376   Xt_cpt 14377   Topctop 18498  TopOnctopon 18499   TopBasesctb 18502   Clsdccld 18620   clsccl 18622

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-rep 4403  ax-sep 4413  ax-nul 4421  ax-pow 4470  ax-pr 4531  ax-un 6372

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-ne 2608  df-ral 2720  df-rex 2721  df-reu 2722  df-rab 2724  df-v 2974  df-sbc 3187  df-csb 3289  df-dif 3331  df-un 3333  df-in 3335  df-ss 3342  df-pss 3344  df-nul 3638  df-if 3792  df-pw 3862  df-sn 3878  df-pr 3880  df-tp 3882  df-op 3884  df-uni 4092  df-int 4129  df-iun 4173  df-iin 4174  df-br 4293  df-opab 4351  df-mpt 4352  df-tr 4386  df-eprel 4632  df-id 4636  df-po 4641  df-so 4642  df-fr 4679  df-we 4681  df-ord 4722  df-on 4723  df-lim 4724  df-suc 4725  df-xp 4846  df-rel 4847  df-cnv 4848  df-co 4849  df-dm 4850  df-rn 4851  df-res 4852  df-ima 4853  df-iota 5381  df-fun 5420  df-fn 5421  df-f 5422  df-f1 5423  df-fo 5424  df-f1o 5425  df-fv 5426  df-ov 6094  df-oprab 6095  df-mpt2 6096  df-om 6477  df-recs 6832  df-rdg 6866  df-1o 6920  df-oadd 6924  df-er 7101  df-map 7216  df-ixp 7264  df-en 7311  df-fin 7314  df-fi 7661  df-acn 8112  df-topgen 14382  df-pt 14383  df-top 18503  df-bases 18505  df-topon 18506  df-cld 18623  df-ntr 18624  df-cls 18625

This theorem is referenced by:  ptcls  19189  dfac14  19191