Theorem ptclsg 20561

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 19872	. . . . . 6 |- ( R e. (TopOn ` X ) -> R e. Top )
4	2, 3	syl 17	. . . . 5 |- ( ( ph /\ k e. A ) -> R e. Top )
5		ptcls.c	. . . . . . 7 |- ( ( ph /\ k e. A ) -> S C_ X )
6		toponuni 19873	. . . . . . . 8 |- ( R e. (TopOn ` X ) -> X = U. R )
7	2, 6	syl 17	. . . . . . 7 |- ( ( ph /\ k e. A ) -> X = U. R )
8	5, 7	sseqtrd 3506	. . . . . 6 |- ( ( ph /\ k e. A ) -> S C_ U. R )
9		eqid 2429	. . . . . . 7 |- U. R = U. R
10	9	clscld 19993	. . . . . 6 |- ( ( R e. Top /\ S C_ U. R ) -> ( ( cls ` R ) ` S ) e. ( Clsd ` R ) )
11	4, 8, 10	syl2anc 665	. . . . 5 |- ( ( ph /\ k e. A ) -> ( ( cls ` R ) ` S ) e. ( Clsd ` R ) )
12	1, 4, 11	ptcldmpt 20560	. . . 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 5884	. . . 4 |- ( Clsd ` J ) = ( Clsd ` ( Xt_ ` ( k e. A |-> R ) ) )
15	12, 14	syl6eleqr 2528	. . 3 |- ( ph -> X_ k e. A ( ( cls ` R ) ` S ) e. ( Clsd ` J ) )
16	9	sscls 20002	. . . . . 6 |- ( ( R e. Top /\ S C_ U. R ) -> S C_ ( ( cls ` R ) ` S ) )
17	4, 8, 16	syl2anc 665	. . . . 5 |- ( ( ph /\ k e. A ) -> S C_ ( ( cls ` R ) ` S ) )
18	17	ralrimiva 2846	. . . 4 |- ( ph -> A. k e. A S C_ ( ( cls ` R ) ` S ) )
19		ss2ixp 7543	. . . 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 17	. . 3 |- ( ph -> X_ k e. A S C_ X_ k e. A ( ( cls ` R ) ` S ) )
21		eqid 2429	. . . 4 |- U. J = U. J
22	21	clsss2 20019	. . 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 665	. 2 |- ( ph -> ( ( cls ` J ) ` X_ k e. A S ) C_ X_ k e. A ( ( cls ` R ) ` S ) )
24		vex 3090	. . . . . . . 8 |- u e. _V
25		eqeq1 2433	. . . . . . . . . 10 |- ( x = u -> ( x = X_ y e. A ( g ` y ) <-> u = X_ y e. A ( g ` y ) ) )
26	25	anbi2d 708	. . . . . . . . 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 1761	. . . . . . . 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 3224	. . . . . . 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 5889	. . . . . . . . . . . . . . . . . 18 |- F/_ k ( ( k e. A |-> R ) ` y )
30	29	nfel2 2609	. . . . . . . . . . . . . . . . 17 |- F/ k ( g ` y ) e. ( ( k e. A |-> R ) ` y )
31		nfv 1754	. . . . . . . . . . . . . . . . 17 |- F/ y ( g ` k ) e. ( ( k e. A |-> R ) ` k )
32		fveq2 5881	. . . . . . . . . . . . . . . . . 18 |- ( y = k -> ( g ` y ) = ( g ` k ) )
33		fveq2 5881	. . . . . . . . . . . . . . . . . 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 3058	. . . . . . . . . . . . . . . 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 462	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ k e. A ) -> k e. A )
37		eqid 2429	. . . . . . . . . . . . . . . . . . . 20 |- ( k e. A |-> R ) = ( k e. A |-> R )
38	37	fvmpt2 5973	. . . . . . . . . . . . . . . . . . 19 |- ( ( k e. A /\ R e. (TopOn ` X ) ) -> ( ( k e. A |-> R ) ` k ) = R )
39	36, 2, 38	syl2anc 665	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ k e. A ) -> ( ( k e. A |-> R ) ` k ) = R )
40	39	eleq2d 2499	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ k e. A ) -> ( ( g ` k ) e. ( ( k e. A |-> R ) ` k ) <-> ( g ` k ) e. R ) )
41	40	ralbidva 2868	. . . . . . . . . . . . . . . 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 260	. . . . . . . . . . . . . . 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 708	. . . . . . . . . . . . . 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 466	. . . . . . . . . . . . 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 486	. . . . . . . . . . . 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 730	. . . . . . . . . . . . . . 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 758	. . . . . . . . . . . . . . . . . . 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 3090	. . . . . . . . . . . . . . . . . . . . . 22 |- f e. _V
50	49	elixp 7537	. . . . . . . . . . . . . . . . . . . . 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 465	. . . . . . . . . . . . . . . . . . . 20 |- ( f e. X_ k e. A ( ( cls ` R ) ` S ) -> A. k e. A ( f ` k ) e. ( ( cls ` R ) ` S ) )
52	51	ad2antlr 731	. . . . . . . . . . . . . . . . . . 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 20022	. . . . . . . . . . . . . . . . . . . . . . 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 435	. . . . . . . . . . . . . . . . . . . . . 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 1207	. . . . . . . . . . . . . . . . . . . . 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 665	. . . . . . . . . . . . . . . . . . . 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 2840	. . . . . . . . . . . . . . . . . . 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 62	. . . . . . . . . . . . . . . . . 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 771	. . . . . . . . . . . . . . . . . . 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 764	. . . . . . . . . . . . . . . . . . . . 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 7548	. . . . . . . . . . . . . . . . . . . . 21 |- X_ y e. A ( g ` y ) = X_ k e. A ( g ` k )
62	60, 61	syl6eleq 2527	. . . . . . . . . . . . . . . . . . . 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 7537	. . . . . . . . . . . . . . . . . . . . 21 |- ( f e. X_ k e. A ( g ` k ) <-> ( f Fn A /\ A. k e. A ( f ` k ) e. ( g ` k ) ) )
64	63	simprbi 465	. . . . . . . . . . . . . . . . . . . 20 |- ( f e. X_ k e. A ( g ` k ) -> A. k e. A ( f ` k ) e. ( g ` k ) )
65	62, 64	syl 17	. . . . . . . . . . . . . . . . . . 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 2962	. . . . . . . . . . . . . . . . . . 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 668	. . . . . . . . . . . . . . . . . 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 2821	. . . . . . . . . . . . . . . . . 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 62	. . . . . . . . . . . . . . . . 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 3788	. . . . . . . . . . . . . . . . . . 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 3450	. . . . . . . . . . . . . . . . . . . . 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 3689	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( g ` k ) i^i S ) C_ S
73		ssiun2 4345	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( k e. A -> S C_ U_ k e. A S )
74	72, 73	syl5ss 3481	. . . . . . . . . . . . . . . . . . . . . 22 |- ( k e. A -> ( ( g ` k ) i^i S ) C_ U_ k e. A S )
75		dfss1 3673	. . . . . . . . . . . . . . . . . . . . . 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 199	. . . . . . . . . . . . . . . . . . . . 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 2484	. . . . . . . . . . . . . . . . . . . 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 2708	. . . . . . . . . . . . . . . . . . 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 262	. . . . . . . . . . . . . . . . . 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 2862	. . . . . . . . . . . . . . . . 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 215	. . . . . . . . . . . . . . . 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 1754	. . . . . . . . . . . . . . . . 17 |- F/ y E. z e. U_ k e. A S z e. ( ( g ` k ) i^i S )
83		nfiu1 4332	. . . . . . . . . . . . . . . . . 18 |- F/_ k U_ k e. A S
84		nfcv 2591	. . . . . . . . . . . . . . . . . . . 20 |- F/_ k ( g ` y )
85		nfcsb1v 3417	. . . . . . . . . . . . . . . . . . . 20 |- F/_ k [_ y / k ]_ S
86	84, 85	nfin 3675	. . . . . . . . . . . . . . . . . . 19 |- F/_ k ( ( g ` y ) i^i [_ y / k ]_ S )
87	86	nfel2 2609	. . . . . . . . . . . . . . . . . 18 |- F/ k z e. ( ( g ` y ) i^i [_ y / k ]_ S )
88	83, 87	nfrex 2895	. . . . . . . . . . . . . . . . 17 |- F/ k E. z e. U_ k e. A S z e. ( ( g ` y ) i^i [_ y / k ]_ S )
89		fveq2 5881	. . . . . . . . . . . . . . . . . . . 20 |- ( k = y -> ( g ` k ) = ( g ` y ) )
90		csbeq1a 3410	. . . . . . . . . . . . . . . . . . . 20 |- ( k = y -> S = [_ y / k ]_ S )
91	89, 90	ineq12d 3671	. . . . . . . . . . . . . . . . . . 19 |- ( k = y -> ( ( g ` k ) i^i S ) = ( ( g ` y ) i^i [_ y / k ]_ S ) )
92	91	eleq2d 2499	. . . . . . . . . . . . . . . . . 18 |- ( k = y -> ( z e. ( ( g ` k ) i^i S ) <-> z e. ( ( g ` y ) i^i [_ y / k ]_ S ) ) )
93	92	rexbidv 2946	. . . . . . . . . . . . . . . . 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 3058	. . . . . . . . . . . . . . . 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 199	. . . . . . . . . . . . . . 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 2501	. . . . . . . . . . . . . . . 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 8476	. . . . . . . . . . . . . . 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 665	. . . . . . . . . . . . . 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 5746	. . . . . . . . . . . . . . . 16 |- ( h : A --> U_ k e. A S -> h Fn A )
100		nfv 1754	. . . . . . . . . . . . . . . . . 18 |- F/ y ( h ` k ) e. ( ( g ` k ) i^i S )
101	86	nfel2 2609	. . . . . . . . . . . . . . . . . 18 |- F/ k ( h ` y ) e. ( ( g ` y ) i^i [_ y / k ]_ S )
102		fveq2 5881	. . . . . . . . . . . . . . . . . . 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 3058	. . . . . . . . . . . . . . . . 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 3773	. . . . . . . . . . . . . . . . . 18 |- ( h e. X_ k e. A ( ( g ` k ) i^i S ) -> X_ k e. A ( ( g ` k ) i^i S ) =/= (/) )
106		vex 3090	. . . . . . . . . . . . . . . . . . 19 |- h e. _V
107	106	elixp 7537	. . . . . . . . . . . . . . . . . 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 7555	. . . . . . . . . . . . . . . . . . . 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 3666	. . . . . . . . . . . . . . . . . . . 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 2461	. . . . . . . . . . . . . . . . . . 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 2716	. . . . . . . . . . . . . . . . . 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 268	. . . . . . . . . . . . . . . . 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 478	. . . . . . . . . . . . . . . 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 473	. . . . . . . . . . . . . . 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 1769	. . . . . . . . . . . . . 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 17	. . . . . . . . . . . . 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 618	. . . . . . . . . . . 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 472	. . . . . . . . . . 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 1166	. . . . . . . . . 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 2502	. . . . . . . . . . 11 |- ( u = X_ y e. A ( g ` y ) -> ( f e. u <-> f e. X_ y e. A ( g ` y ) ) )
121		ineq1 3663	. . . . . . . . . . . 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 2708	. . . . . . . . . . 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 321	. . . . . . . . . 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 225	. . . . . . . . 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 606	. . . . . . . 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 1771	. . . . . . 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 220	. . . . . 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 2844	. . . . 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 6061	. . . . . . . . . 10 |- ( ph -> ( k e. A |-> R ) : A --> Top )
130		ffn 5746	. . . . . . . . . 10 |- ( ( k e. A |-> R ) : A --> Top -> ( k e. A |-> R ) Fn A )
131	129, 130	syl 17	. . . . . . . . 9 |- ( ph -> ( k e. A |-> R ) Fn A )
132		eqid 2429	. . . . . . . . . 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 20516	. . . . . . . . 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 665	. . . . . . . 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 2482	. . . . . . 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 466	. . . . . 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 2846	. . . . . . . . 9 |- ( ph -> A. k e. A R e. (TopOn ` X ) )
138	13	pttopon 20542	. . . . . . . . 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 665	. . . . . . . 8 |- ( ph -> J e. (TopOn ` X_ k e. A X ) )
140		toponuni 19873	. . . . . . . 8 |- ( J e. (TopOn ` X_ k e. A X ) -> X_ k e. A X = U. J )
141	139, 140	syl 17	. . . . . . 7 |- ( ph -> X_ k e. A X = U. J )
142	141	adantr 466	. . . . . 6 |- ( ( ph /\ f e. X_ k e. A ( ( cls ` R ) ` S ) ) -> X_ k e. A X = U. J )
143	132	ptbas 20525	. . . . . . . 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 665	. . . . . . 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 466	. . . . . 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 2846	. . . . . . . 8 |- ( ph -> A. k e. A S C_ X )
147		ss2ixp 7543	. . . . . . . 8 |- ( A. k e. A S C_ X -> X_ k e. A S C_ X_ k e. A X )
148	146, 147	syl 17	. . . . . . 7 |- ( ph -> X_ k e. A S C_ X_ k e. A X )
149	148	adantr 466	. . . . . 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 20005	. . . . . . . . . . 11 |- ( ( R e. Top /\ S C_ U. R ) -> ( ( cls ` R ) ` S ) C_ U. R )
151	4, 8, 150	syl2anc 665	. . . . . . . . . 10 |- ( ( ph /\ k e. A ) -> ( ( cls ` R ) ` S ) C_ U. R )
152	151, 7	sseqtr4d 3507	. . . . . . . . 9 |- ( ( ph /\ k e. A ) -> ( ( cls ` R ) ` S ) C_ X )
153	152	ralrimiva 2846	. . . . . . . 8 |- ( ph -> A. k e. A ( ( cls ` R ) ` S ) C_ X )
154		ss2ixp 7543	. . . . . . . 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 17	. . . . . . 7 |- ( ph -> X_ k e. A ( ( cls ` R ) ` S ) C_ X_ k e. A X )
156	155	sselda 3470	. . . . . 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 20030	. . . . 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 235	. . . 4 |- ( ( ph /\ f e. X_ k e. A ( ( cls ` R ) ` S ) ) -> f e. ( ( cls ` J ) ` X_ k e. A S ) )
159	158	ex 435	. . 3 |- ( ph -> ( f e. X_ k e. A ( ( cls ` R ) ` S ) -> f e. ( ( cls ` J ) ` X_ k e. A S ) ) )
160	159	ssrdv 3476	. 2 |- ( ph -> X_ k e. A ( ( cls ` R ) ` S ) C_ ( ( cls ` J ) ` X_ k e. A S ) )
161	23, 160	eqssd 3487	1 |- ( ph -> ( ( cls ` J ) ` X_ k e. A S ) = X_ k e. A ( ( cls ` R ) ` S ) )

Syntax hints:   -> wi 4   <-> wb 187   /\ wa 370   /\ w3a 982   = wceq 1437   E.wex 1659   e. wcel 1870   {cab 2414   =/= wne 2625   A.wral 2782   E.wrex 2783   {crab 2786   [_csb 3401   \ cdif 3439   i^i cin 3441   C_ wss 3442   (/)c0 3767   U.cuni 4222   U_ciun 4302   |-> cmpt 4484   Fn wfn 5596   -->wf 5597   ` cfv 5601   X_cixp 7530   Fincfn 7577  AC wacn 8371   topGenctg 15295   Xt_cpt 15296   Topctop 19848  TopOnctopon 19849   TopBasesctb 19851   Clsdccld 19962   clsccl 19964

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-8 1872  ax-9 1874  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407  ax-rep 4538  ax-sep 4548  ax-nul 4556  ax-pow 4603  ax-pr 4661  ax-un 6597

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-eu 2270  df-mo 2271  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-ne 2627  df-ral 2787  df-rex 2788  df-reu 2789  df-rab 2791  df-v 3089  df-sbc 3306  df-csb 3402  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-pss 3458  df-nul 3768  df-if 3916  df-pw 3987  df-sn 4003  df-pr 4005  df-tp 4007  df-op 4009  df-uni 4223  df-int 4259  df-iun 4304  df-iin 4305  df-br 4427  df-opab 4485  df-mpt 4486  df-tr 4521  df-eprel 4765  df-id 4769  df-po 4775  df-so 4776  df-fr 4813  df-we 4815  df-xp 4860  df-rel 4861  df-cnv 4862  df-co 4863  df-dm 4864  df-rn 4865  df-res 4866  df-ima 4867  df-pred 5399  df-ord 5445  df-on 5446  df-lim 5447  df-suc 5448  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-ov 6308  df-oprab 6309  df-mpt2 6310  df-om 6707  df-wrecs 7036  df-recs 7098  df-rdg 7136  df-1o 7190  df-oadd 7194  df-er 7371  df-map 7482  df-ixp 7531  df-en 7578  df-fin 7581  df-fi 7931  df-acn 8375  df-topgen 15301  df-pt 15302  df-top 19852  df-bases 19853  df-topon 19854  df-cld 19965  df-ntr 19966  df-cls 19967

This theorem is referenced by:  ptcls  20562  dfac14  20564