Theorem ptclsg 21418

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 20718	. . . . . 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 20719	. . . . . . . 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 3641	. . . . . 6 |- ( ( ph /\ k e. A ) -> S C_ U. R )
9		eqid 2622	. . . . . . 7 |- U. R = U. R
10	9	clscld 20851	. . . . . 6 |- ( ( R e. Top /\ S C_ U. R ) -> ( ( cls ` R ) ` S ) e. ( Clsd ` R ) )
11	4, 8, 10	syl2anc 693	. . . . 5 |- ( ( ph /\ k e. A ) -> ( ( cls ` R ) ` S ) e. ( Clsd ` R ) )
12	1, 4, 11	ptcldmpt 21417	. . . 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 6194	. . . 4 |- ( Clsd ` J ) = ( Clsd ` ( Xt_ ` ( k e. A |-> R ) ) )
15	12, 14	syl6eleqr 2712	. . 3 |- ( ph -> X_ k e. A ( ( cls ` R ) ` S ) e. ( Clsd ` J ) )
16	9	sscls 20860	. . . . . 6 |- ( ( R e. Top /\ S C_ U. R ) -> S C_ ( ( cls ` R ) ` S ) )
17	4, 8, 16	syl2anc 693	. . . . 5 |- ( ( ph /\ k e. A ) -> S C_ ( ( cls ` R ) ` S ) )
18	17	ralrimiva 2966	. . . 4 |- ( ph -> A. k e. A S C_ ( ( cls ` R ) ` S ) )
19		ss2ixp 7921	. . . 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 2622	. . . 4 |- U. J = U. J
22	21	clsss2 20876	. . 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 693	. 2 |- ( ph -> ( ( cls ` J ) ` X_ k e. A S ) C_ X_ k e. A ( ( cls ` R ) ` S ) )
24		vex 3203	. . . . . . . 8 |- u e. _V
25		eqeq1 2626	. . . . . . . . . 10 |- ( x = u -> ( x = X_ y e. A ( g ` y ) <-> u = X_ y e. A ( g ` y ) ) )
26	25	anbi2d 740	. . . . . . . . 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 1850	. . . . . . . 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 3350	. . . . . . 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 6199	. . . . . . . . . . . . . . . . . 18 |- F/_ k ( ( k e. A |-> R ) ` y )
30	29	nfel2 2781	. . . . . . . . . . . . . . . . 17 |- F/ k ( g ` y ) e. ( ( k e. A |-> R ) ` y )
31		nfv 1843	. . . . . . . . . . . . . . . . 17 |- F/ y ( g ` k ) e. ( ( k e. A |-> R ) ` k )
32		fveq2 6191	. . . . . . . . . . . . . . . . . 18 |- ( y = k -> ( g ` y ) = ( g ` k ) )
33		fveq2 6191	. . . . . . . . . . . . . . . . . 18 |- ( y = k -> ( ( k e. A |-> R ) ` y ) = ( ( k e. A |-> R ) ` k ) )
34	32, 33	eleq12d 2695	. . . . . . . . . . . . . . . . 17 |- ( y = k -> ( ( g ` y ) e. ( ( k e. A |-> R ) ` y ) <-> ( g ` k ) e. ( ( k e. A |-> R ) ` k ) ) )
35	30, 31, 34	cbvral 3167	. . . . . . . . . . . . . . . 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 477	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ k e. A ) -> k e. A )
37		eqid 2622	. . . . . . . . . . . . . . . . . . . 20 |- ( k e. A |-> R ) = ( k e. A |-> R )
38	37	fvmpt2 6291	. . . . . . . . . . . . . . . . . . 19 |- ( ( k e. A /\ R e. (TopOn ` X ) ) -> ( ( k e. A |-> R ) ` k ) = R )
39	36, 2, 38	syl2anc 693	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ k e. A ) -> ( ( k e. A |-> R ) ` k ) = R )
40	39	eleq2d 2687	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ k e. A ) -> ( ( g ` k ) e. ( ( k e. A |-> R ) ` k ) <-> ( g ` k ) e. R ) )
41	40	ralbidva 2985	. . . . . . . . . . . . . . . 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 272	. . . . . . . . . . . . . . 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 740	. . . . . . . . . . . . . 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 481	. . . . . . . . . . . . 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 501	. . . . . . . . . . . 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 762	. . . . . . . . . . . . . . 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 790	. . . . . . . . . . . . . . . . . . 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 3203	. . . . . . . . . . . . . . . . . . . . . 22 |- f e. _V
50	49	elixp 7915	. . . . . . . . . . . . . . . . . . . . 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 480	. . . . . . . . . . . . . . . . . . . 20 |- ( f e. X_ k e. A ( ( cls ` R ) ` S ) -> A. k e. A ( f ` k ) e. ( ( cls ` R ) ` S ) )
52	51	ad2antlr 763	. . . . . . . . . . . . . . . . . . 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 20879	. . . . . . . . . . . . . . . . . . . . . . 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 450	. . . . . . . . . . . . . . . . . . . . . 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 1267	. . . . . . . . . . . . . . . . . . . . 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 693	. . . . . . . . . . . . . . . . . . . 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 2962	. . . . . . . . . . . . . . . . . . 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 65	. . . . . . . . . . . . . . . . . 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 803	. . . . . . . . . . . . . . . . . . 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 796	. . . . . . . . . . . . . . . . . . . . 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 7926	. . . . . . . . . . . . . . . . . . . . 21 |- X_ y e. A ( g ` y ) = X_ k e. A ( g ` k )
62	60, 61	syl6eleq 2711	. . . . . . . . . . . . . . . . . . . 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 7915	. . . . . . . . . . . . . . . . . . . . 21 |- ( f e. X_ k e. A ( g ` k ) <-> ( f Fn A /\ A. k e. A ( f ` k ) e. ( g ` k ) ) )
64	63	simprbi 480	. . . . . . . . . . . . . . . . . . . 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 3064	. . . . . . . . . . . . . . . . . . 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 698	. . . . . . . . . . . . . . . . . 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 2948	. . . . . . . . . . . . . . . . . 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 65	. . . . . . . . . . . . . . . . 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 3958	. . . . . . . . . . . . . . . . . . 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 3582	. . . . . . . . . . . . . . . . . . . . 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 3834	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( g ` k ) i^i S ) C_ S
73		ssiun2 4563	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( k e. A -> S C_ U_ k e. A S )
74	72, 73	syl5ss 3614	. . . . . . . . . . . . . . . . . . . . . 22 |- ( k e. A -> ( ( g ` k ) i^i S ) C_ U_ k e. A S )
75		sseqin2 3817	. . . . . . . . . . . . . . . . . . . . . 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 208	. . . . . . . . . . . . . . . . . . . . 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 2670	. . . . . . . . . . . . . . . . . . . 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 2853	. . . . . . . . . . . . . . . . . . 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 274	. . . . . . . . . . . . . . . . . 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 2979	. . . . . . . . . . . . . . . . 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 224	. . . . . . . . . . . . . . . 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 1843	. . . . . . . . . . . . . . . . 17 |- F/ y E. z e. U_ k e. A S z e. ( ( g ` k ) i^i S )
83		nfiu1 4550	. . . . . . . . . . . . . . . . . 18 |- F/_ k U_ k e. A S
84		nfcv 2764	. . . . . . . . . . . . . . . . . . . 20 |- F/_ k ( g ` y )
85		nfcsb1v 3549	. . . . . . . . . . . . . . . . . . . 20 |- F/_ k [_ y / k ]_ S
86	84, 85	nfin 3820	. . . . . . . . . . . . . . . . . . 19 |- F/_ k ( ( g ` y ) i^i [_ y / k ]_ S )
87	86	nfel2 2781	. . . . . . . . . . . . . . . . . 18 |- F/ k z e. ( ( g ` y ) i^i [_ y / k ]_ S )
88	83, 87	nfrex 3007	. . . . . . . . . . . . . . . . 17 |- F/ k E. z e. U_ k e. A S z e. ( ( g ` y ) i^i [_ y / k ]_ S )
89		fveq2 6191	. . . . . . . . . . . . . . . . . . . 20 |- ( k = y -> ( g ` k ) = ( g ` y ) )
90		csbeq1a 3542	. . . . . . . . . . . . . . . . . . . 20 |- ( k = y -> S = [_ y / k ]_ S )
91	89, 90	ineq12d 3815	. . . . . . . . . . . . . . . . . . 19 |- ( k = y -> ( ( g ` k ) i^i S ) = ( ( g ` y ) i^i [_ y / k ]_ S ) )
92	91	eleq2d 2687	. . . . . . . . . . . . . . . . . 18 |- ( k = y -> ( z e. ( ( g ` k ) i^i S ) <-> z e. ( ( g ` y ) i^i [_ y / k ]_ S ) ) )
93	92	rexbidv 3052	. . . . . . . . . . . . . . . . 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 3167	. . . . . . . . . . . . . . . 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 208	. . . . . . . . . . . . . . 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 2689	. . . . . . . . . . . . . . . 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 8870	. . . . . . . . . . . . . . 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 693	. . . . . . . . . . . . . 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 6045	. . . . . . . . . . . . . . . 16 |- ( h : A --> U_ k e. A S -> h Fn A )
100		nfv 1843	. . . . . . . . . . . . . . . . . 18 |- F/ y ( h ` k ) e. ( ( g ` k ) i^i S )
101	86	nfel2 2781	. . . . . . . . . . . . . . . . . 18 |- F/ k ( h ` y ) e. ( ( g ` y ) i^i [_ y / k ]_ S )
102		fveq2 6191	. . . . . . . . . . . . . . . . . . 19 |- ( k = y -> ( h ` k ) = ( h ` y ) )
103	102, 91	eleq12d 2695	. . . . . . . . . . . . . . . . . 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 3167	. . . . . . . . . . . . . . . . 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 3921	. . . . . . . . . . . . . . . . . 18 |- ( h e. X_ k e. A ( ( g ` k ) i^i S ) -> X_ k e. A ( ( g ` k ) i^i S ) =/= (/) )
106		vex 3203	. . . . . . . . . . . . . . . . . . 19 |- h e. _V
107	106	elixp 7915	. . . . . . . . . . . . . . . . . 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 7933	. . . . . . . . . . . . . . . . . . . 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 3810	. . . . . . . . . . . . . . . . . . . 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 2647	. . . . . . . . . . . . . . . . . . 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 2858	. . . . . . . . . . . . . . . . . 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 280	. . . . . . . . . . . . . . . . 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 493	. . . . . . . . . . . . . . . 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 488	. . . . . . . . . . . . . . 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 1858	. . . . . . . . . . . . . 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 643	. . . . . . . . . . . 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 487	. . . . . . . . . . 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 1222	. . . . . . . . . 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 2690	. . . . . . . . . . 11 |- ( u = X_ y e. A ( g ` y ) -> ( f e. u <-> f e. X_ y e. A ( g ` y ) ) )
121		ineq1 3807	. . . . . . . . . . . 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 2853	. . . . . . . . . . 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 334	. . . . . . . . . 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 237	. . . . . . . . 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 629	. . . . . . . 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 1861	. . . . . . 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 232	. . . . . 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 2965	. . . . 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 6385	. . . . . . . . . 10 |- ( ph -> ( k e. A |-> R ) : A --> Top )
130		ffn 6045	. . . . . . . . . 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 2622	. . . . . . . . . 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 21373	. . . . . . . . 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 693	. . . . . . . 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 2668	. . . . . . 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 481	. . . . . 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 2966	. . . . . . . . 9 |- ( ph -> A. k e. A R e. (TopOn ` X ) )
138	13	pttopon 21399	. . . . . . . . 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 693	. . . . . . . 8 |- ( ph -> J e. (TopOn ` X_ k e. A X ) )
140		toponuni 20719	. . . . . . . 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 481	. . . . . 6 |- ( ( ph /\ f e. X_ k e. A ( ( cls ` R ) ` S ) ) -> X_ k e. A X = U. J )
143	132	ptbas 21382	. . . . . . . 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 693	. . . . . . 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 481	. . . . . 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 2966	. . . . . . . 8 |- ( ph -> A. k e. A S C_ X )
147		ss2ixp 7921	. . . . . . . 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 481	. . . . . 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 20863	. . . . . . . . . . 11 |- ( ( R e. Top /\ S C_ U. R ) -> ( ( cls ` R ) ` S ) C_ U. R )
151	4, 8, 150	syl2anc 693	. . . . . . . . . 10 |- ( ( ph /\ k e. A ) -> ( ( cls ` R ) ` S ) C_ U. R )
152	151, 7	sseqtr4d 3642	. . . . . . . . 9 |- ( ( ph /\ k e. A ) -> ( ( cls ` R ) ` S ) C_ X )
153	152	ralrimiva 2966	. . . . . . . 8 |- ( ph -> A. k e. A ( ( cls ` R ) ` S ) C_ X )
154		ss2ixp 7921	. . . . . . . 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 3603	. . . . . 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 20887	. . . . 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 247	. . . 4 |- ( ( ph /\ f e. X_ k e. A ( ( cls ` R ) ` S ) ) -> f e. ( ( cls ` J ) ` X_ k e. A S ) )
159	158	ex 450	. . 3 |- ( ph -> ( f e. X_ k e. A ( ( cls ` R ) ` S ) -> f e. ( ( cls ` J ) ` X_ k e. A S ) ) )
160	159	ssrdv 3609	. 2 |- ( ph -> X_ k e. A ( ( cls ` R ) ` S ) C_ ( ( cls ` J ) ` X_ k e. A S ) )
161	23, 160	eqssd 3620	1 |- ( ph -> ( ( cls ` J ) ` X_ k e. A S ) = X_ k e. A ( ( cls ` R ) ` S ) )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   /\ w3a 1037   = wceq 1483   E.wex 1704   e. wcel 1990   {cab 2608   =/= wne 2794   A.wral 2912   E.wrex 2913   {crab 2916   [_csb 3533   \ cdif 3571   i^i cin 3573   C_ wss 3574   (/)c0 3915   U.cuni 4436   U_ciun 4520   |-> cmpt 4729   Fn wfn 5883   -->wf 5884   ` cfv 5888   X_cixp 7908   Fincfn 7955  AC wacn 8764   topGenctg 16098   Xt_cpt 16099   Topctop 20698  TopOnctopon 20715   TopBasesctb 20749   Clsdccld 20820   clsccl 20822

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-reu 2919  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-int 4476  df-iun 4522  df-iin 4523  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-om 7066  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-1o 7560  df-oadd 7564  df-er 7742  df-map 7859  df-ixp 7909  df-en 7956  df-fin 7959  df-fi 8317  df-acn 8768  df-topgen 16104  df-pt 16105  df-top 20699  df-topon 20716  df-bases 20750  df-cld 20823  df-ntr 20824  df-cls 20825

This theorem is referenced by:  ptcls  21419  dfac14  21421