Theorem ptclsg 19088

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 18431	. . . . . 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 18432	. . . . . . . 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 3389	. . . . . 6 |- ( ( ph /\ k e. A ) -> S C_ U. R )
9		eqid 2441	. . . . . . 7 |- U. R = U. R
10	9	clscld 18551	. . . . . 6 |- ( ( R e. Top /\ S C_ U. R ) -> ( ( cls ` R ) ` S ) e. ( Clsd ` R ) )
11	4, 8, 10	syl2anc 656	. . . . 5 |- ( ( ph /\ k e. A ) -> ( ( cls ` R ) ` S ) e. ( Clsd ` R ) )
12	1, 4, 11	ptcldmpt 19087	. . . 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 5691	. . . 4 |- ( Clsd ` J ) = ( Clsd ` ( Xt_ ` ( k e. A |-> R ) ) )
15	12, 14	syl6eleqr 2532	. . 3 |- ( ph -> X_ k e. A ( ( cls ` R ) ` S ) e. ( Clsd ` J ) )
16	9	sscls 18560	. . . . . 6 |- ( ( R e. Top /\ S C_ U. R ) -> S C_ ( ( cls ` R ) ` S ) )
17	4, 8, 16	syl2anc 656	. . . . 5 |- ( ( ph /\ k e. A ) -> S C_ ( ( cls ` R ) ` S ) )
18	17	ralrimiva 2797	. . . 4 |- ( ph -> A. k e. A S C_ ( ( cls ` R ) ` S ) )
19		ss2ixp 7272	. . . 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 2441	. . . 4 |- U. J = U. J
22	21	clsss2 18576	. . 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 656	. 2 |- ( ph -> ( ( cls ` J ) ` X_ k e. A S ) C_ X_ k e. A ( ( cls ` R ) ` S ) )
24		vex 2973	. . . . . . . 8 |- u e. _V
25		eqeq1 2447	. . . . . . . . . 10 |- ( x = u -> ( x = X_ y e. A ( g ` y ) <-> u = X_ y e. A ( g ` y ) ) )
26	25	anbi2d 698	. . . . . . . . 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 1685	. . . . . . . 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 3103	. . . . . . 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 5696	. . . . . . . . . . . . . . . . . 18 |- F/_ k ( ( k e. A |-> R ) ` y )
30	29	nfel2 2589	. . . . . . . . . . . . . . . . 17 |- F/ k ( g ` y ) e. ( ( k e. A |-> R ) ` y )
31		nfv 1678	. . . . . . . . . . . . . . . . 17 |- F/ y ( g ` k ) e. ( ( k e. A |-> R ) ` k )
32		fveq2 5688	. . . . . . . . . . . . . . . . . 18 |- ( y = k -> ( g ` y ) = ( g ` k ) )
33		fveq2 5688	. . . . . . . . . . . . . . . . . 18 |- ( y = k -> ( ( k e. A |-> R ) ` y ) = ( ( k e. A |-> R ) ` k ) )
34	32, 33	eleq12d 2509	. . . . . . . . . . . . . . . . 17 |- ( y = k -> ( ( g ` y ) e. ( ( k e. A |-> R ) ` y ) <-> ( g ` k ) e. ( ( k e. A |-> R ) ` k ) ) )
35	30, 31, 34	cbvral 2941	. . . . . . . . . . . . . . . 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 458	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ k e. A ) -> k e. A )
37		eqid 2441	. . . . . . . . . . . . . . . . . . . 20 |- ( k e. A |-> R ) = ( k e. A |-> R )
38	37	fvmpt2 5778	. . . . . . . . . . . . . . . . . . 19 |- ( ( k e. A /\ R e. (TopOn ` X ) ) -> ( ( k e. A |-> R ) ` k ) = R )
39	36, 2, 38	syl2anc 656	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ k e. A ) -> ( ( k e. A |-> R ) ` k ) = R )
40	39	eleq2d 2508	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ k e. A ) -> ( ( g ` k ) e. ( ( k e. A |-> R ) ` k ) <-> ( g ` k ) e. R ) )
41	40	ralbidva 2729	. . . . . . . . . . . . . . . 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 698	. . . . . . . . . . . . . 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 462	. . . . . . . . . . . . 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 481	. . . . . . . . . . . 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 720	. . . . . . . . . . . . . . 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 748	. . . . . . . . . . . . . . . . . . 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 2973	. . . . . . . . . . . . . . . . . . . . . 22 |- f e. _V
50	49	elixp 7266	. . . . . . . . . . . . . . . . . . . . 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 461	. . . . . . . . . . . . . . . . . . . 20 |- ( f e. X_ k e. A ( ( cls ` R ) ` S ) -> A. k e. A ( f ` k ) e. ( ( cls ` R ) ` S ) )
52	51	ad2antlr 721	. . . . . . . . . . . . . . . . . . 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 18579	. . . . . . . . . . . . . . . . . . . . . . 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 1184	. . . . . . . . . . . . . . . . . . . . 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 656	. . . . . . . . . . . . . . . . . . . 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 2792	. . . . . . . . . . . . . . . . . . 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 757	. . . . . . . . . . . . . . . . . . 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 751	. . . . . . . . . . . . . . . . . . . . 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 7277	. . . . . . . . . . . . . . . . . . . . 21 |- X_ y e. A ( g ` y ) = X_ k e. A ( g ` k )
62	60, 61	syl6eleq 2531	. . . . . . . . . . . . . . . . . . . 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 7266	. . . . . . . . . . . . . . . . . . . . 21 |- ( f e. X_ k e. A ( g ` k ) <-> ( f Fn A /\ A. k e. A ( f ` k ) e. ( g ` k ) ) )
64	63	simprbi 461	. . . . . . . . . . . . . . . . . . . 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 2847	. . . . . . . . . . . . . . . . . . 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 659	. . . . . . . . . . . . . . . . . 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 2785	. . . . . . . . . . . . . . . . . 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 3654	. . . . . . . . . . . . . . . . . . 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 3333	. . . . . . . . . . . . . . . . . . . . 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 3568	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( g ` k ) i^i S ) C_ S
73		ssiun2 4210	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( k e. A -> S C_ U_ k e. A S )
74	72, 73	syl5ss 3364	. . . . . . . . . . . . . . . . . . . . . 22 |- ( k e. A -> ( ( g ` k ) i^i S ) C_ U_ k e. A S )
75		dfss1 3552	. . . . . . . . . . . . . . . . . . . . . 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 2487	. . . . . . . . . . . . . . . . . . . 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 2619	. . . . . . . . . . . . . . . . . . 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 2745	. . . . . . . . . . . . . . . . 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 1678	. . . . . . . . . . . . . . . . 17 |- F/ y E. z e. U_ k e. A S z e. ( ( g ` k ) i^i S )
83		nfiu1 4197	. . . . . . . . . . . . . . . . . 18 |- F/_ k U_ k e. A S
84		nfcv 2577	. . . . . . . . . . . . . . . . . . . 20 |- F/_ k ( g ` y )
85		nfcsb1v 3301	. . . . . . . . . . . . . . . . . . . 20 |- F/_ k [_ y / k ]_ S
86	84, 85	nfin 3554	. . . . . . . . . . . . . . . . . . 19 |- F/_ k ( ( g ` y ) i^i [_ y / k ]_ S )
87	86	nfel2 2589	. . . . . . . . . . . . . . . . . 18 |- F/ k z e. ( ( g ` y ) i^i [_ y / k ]_ S )
88	83, 87	nfrex 2769	. . . . . . . . . . . . . . . . 17 |- F/ k E. z e. U_ k e. A S z e. ( ( g ` y ) i^i [_ y / k ]_ S )
89		fveq2 5688	. . . . . . . . . . . . . . . . . . . 20 |- ( k = y -> ( g ` k ) = ( g ` y ) )
90		csbeq1a 3294	. . . . . . . . . . . . . . . . . . . 20 |- ( k = y -> S = [_ y / k ]_ S )
91	89, 90	ineq12d 3550	. . . . . . . . . . . . . . . . . . 19 |- ( k = y -> ( ( g ` k ) i^i S ) = ( ( g ` y ) i^i [_ y / k ]_ S ) )
92	91	eleq2d 2508	. . . . . . . . . . . . . . . . . 18 |- ( k = y -> ( z e. ( ( g ` k ) i^i S ) <-> z e. ( ( g ` y ) i^i [_ y / k ]_ S ) ) )
93	92	rexbidv 2734	. . . . . . . . . . . . . . . . 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 2941	. . . . . . . . . . . . . . . 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 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 8213	. . . . . . . . . . . . . . 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 656	. . . . . . . . . . . . . 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 5556	. . . . . . . . . . . . . . . 16 |- ( h : A --> U_ k e. A S -> h Fn A )
100		nfv 1678	. . . . . . . . . . . . . . . . . 18 |- F/ y ( h ` k ) e. ( ( g ` k ) i^i S )
101	86	nfel2 2589	. . . . . . . . . . . . . . . . . 18 |- F/ k ( h ` y ) e. ( ( g ` y ) i^i [_ y / k ]_ S )
102		fveq2 5688	. . . . . . . . . . . . . . . . . . 19 |- ( k = y -> ( h ` k ) = ( h ` y ) )
103	102, 91	eleq12d 2509	. . . . . . . . . . . . . . . . . 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 2941	. . . . . . . . . . . . . . . . 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 3640	. . . . . . . . . . . . . . . . . 18 |- ( h e. X_ k e. A ( ( g ` k ) i^i S ) -> X_ k e. A ( ( g ` k ) i^i S ) =/= (/) )
106		vex 2973	. . . . . . . . . . . . . . . . . . 19 |- h e. _V
107	106	elixp 7266	. . . . . . . . . . . . . . . . . 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 7284	. . . . . . . . . . . . . . . . . . . 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 3545	. . . . . . . . . . . . . . . . . . . 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 2464	. . . . . . . . . . . . . . . . . . 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 2616	. . . . . . . . . . . . . . . . . 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 473	. . . . . . . . . . . . . . . 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 468	. . . . . . . . . . . . . . 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 1693	. . . . . . . . . . . . . 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 612	. . . . . . . . . . . 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 467	. . . . . . . . . . 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 1144	. . . . . . . . . 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 3542	. . . . . . . . . . . 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 2619	. . . . . . . . . . 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 600	. . . . . . . 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 1695	. . . . . . 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 2796	. . . . 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 5864	. . . . . . . . . 10 |- ( ph -> ( k e. A |-> R ) : A --> Top )
130		ffn 5556	. . . . . . . . . 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 2441	. . . . . . . . . 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 19043	. . . . . . . . 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 656	. . . . . . . 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 2485	. . . . . . 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 462	. . . . . 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 2797	. . . . . . . . 9 |- ( ph -> A. k e. A R e. (TopOn ` X ) )
138	13	pttopon 19069	. . . . . . . . 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 656	. . . . . . . 8 |- ( ph -> J e. (TopOn ` X_ k e. A X ) )
140		toponuni 18432	. . . . . . . 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 462	. . . . . 6 |- ( ( ph /\ f e. X_ k e. A ( ( cls ` R ) ` S ) ) -> X_ k e. A X = U. J )
143	132	ptbas 19052	. . . . . . . 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 656	. . . . . . 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 462	. . . . . 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 2797	. . . . . . . 8 |- ( ph -> A. k e. A S C_ X )
147		ss2ixp 7272	. . . . . . . 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 462	. . . . . 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 18563	. . . . . . . . . . 11 |- ( ( R e. Top /\ S C_ U. R ) -> ( ( cls ` R ) ` S ) C_ U. R )
151	4, 8, 150	syl2anc 656	. . . . . . . . . 10 |- ( ( ph /\ k e. A ) -> ( ( cls ` R ) ` S ) C_ U. R )
152	151, 7	sseqtr4d 3390	. . . . . . . . 9 |- ( ( ph /\ k e. A ) -> ( ( cls ` R ) ` S ) C_ X )
153	152	ralrimiva 2797	. . . . . . . 8 |- ( ph -> A. k e. A ( ( cls ` R ) ` S ) C_ X )
154		ss2ixp 7272	. . . . . . . 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 3353	. . . . . 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 18587	. . . . 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 3359	. 2 |- ( ph -> X_ k e. A ( ( cls ` R ) ` S ) C_ ( ( cls ` J ) ` X_ k e. A S ) )
161	23, 160	eqssd 3370	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 960   = wceq 1364   E.wex 1591   e. wcel 1761   {cab 2427   =/= wne 2604   A.wral 2713   E.wrex 2714   {crab 2717   [_csb 3285   \ cdif 3322   i^i cin 3324   C_ wss 3325   (/)c0 3634   U.cuni 4088   U_ciun 4168   e. cmpt 4347   Fn wfn 5410   -->wf 5411   ` cfv 5415   X_cixp 7259   Fincfn 7306  AC wacn 8104   topGenctg 14372   Xt_cpt 14373   Topctop 18398  TopOnctopon 18399   TopBasesctb 18402   Clsdccld 18520   clsccl 18522

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-8 1763  ax-9 1765  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422  ax-rep 4400  ax-sep 4410  ax-nul 4418  ax-pow 4467  ax-pr 4528  ax-un 6371

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 961  df-3an 962  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-eu 2263  df-mo 2264  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ne 2606  df-ral 2718  df-rex 2719  df-reu 2720  df-rab 2722  df-v 2972  df-sbc 3184  df-csb 3286  df-dif 3328  df-un 3330  df-in 3332  df-ss 3339  df-pss 3341  df-nul 3635  df-if 3789  df-pw 3859  df-sn 3875  df-pr 3877  df-tp 3879  df-op 3881  df-uni 4089  df-int 4126  df-iun 4170  df-iin 4171  df-br 4290  df-opab 4348  df-mpt 4349  df-tr 4383  df-eprel 4628  df-id 4632  df-po 4637  df-so 4638  df-fr 4675  df-we 4677  df-ord 4718  df-on 4719  df-lim 4720  df-suc 4721  df-xp 4842  df-rel 4843  df-cnv 4844  df-co 4845  df-dm 4846  df-rn 4847  df-res 4848  df-ima 4849  df-iota 5378  df-fun 5417  df-fn 5418  df-f 5419  df-f1 5420  df-fo 5421  df-f1o 5422  df-fv 5423  df-ov 6093  df-oprab 6094  df-mpt2 6095  df-om 6476  df-recs 6828  df-rdg 6862  df-1o 6916  df-oadd 6920  df-er 7097  df-map 7212  df-ixp 7260  df-en 7307  df-fin 7310  df-fi 7657  df-acn 8108  df-topgen 14378  df-pt 14379  df-top 18403  df-bases 18405  df-topon 18406  df-cld 18523  df-ntr 18524  df-cls 18525

This theorem is referenced by:  ptcls  19089  dfac14  19091