ptclsg

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)

	Ref	Expression
Hypotheses	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	ptclsg	\|- ( ph -> ( ( cls ` J ) ` X_ k e. A S ) = X_ k e. A ( ( cls ` R ) ` S ) )

Proof

Step	Hyp	Ref	Expression
1		ptcls.2	\|- J = ( Xt_ ` ( k e. A \|-> R ) )
2		ptcls.a	\|- ( ph -> A e. V )
3		ptcls.j	\|- ( ( ph /\ k e. A ) -> R e. ( TopOn ` X ) )
4		ptcls.c	\|- ( ( ph /\ k e. A ) -> S C_ X )
5		ptclsg.1	\|- ( ph -> U_ k e. A S e. AC_ A )
6		topontop	\|- ( R e. ( TopOn ` X ) -> R e. Top )
7	3 6	syl	\|- ( ( ph /\ k e. A ) -> R e. Top )
8		toponuni	\|- ( R e. ( TopOn ` X ) -> X = U. R )
9	3 8	syl	\|- ( ( ph /\ k e. A ) -> X = U. R )
10	4 9	sseqtrd	\|- ( ( ph /\ k e. A ) -> S C_ U. R )
11		eqid	\|- U. R = U. R
12	11	clscld	\|- ( ( R e. Top /\ S C_ U. R ) -> ( ( cls ` R ) ` S ) e. ( Clsd ` R ) )
13	7 10 12	syl2anc	\|- ( ( ph /\ k e. A ) -> ( ( cls ` R ) ` S ) e. ( Clsd ` R ) )
14	2 7 13	ptcldmpt	\|- ( ph -> X_ k e. A ( ( cls ` R ) ` S ) e. ( Clsd ` ( Xt_ ` ( k e. A \|-> R ) ) ) )
15	1	fveq2i	\|- ( Clsd ` J ) = ( Clsd ` ( Xt_ ` ( k e. A \|-> R ) ) )
16	14 15	eleqtrrdi	\|- ( ph -> X_ k e. A ( ( cls ` R ) ` S ) e. ( Clsd ` J ) )
17	11	sscls	\|- ( ( R e. Top /\ S C_ U. R ) -> S C_ ( ( cls ` R ) ` S ) )
18	7 10 17	syl2anc	\|- ( ( ph /\ k e. A ) -> S C_ ( ( cls ` R ) ` S ) )
19	18	ralrimiva	\|- ( ph -> A. k e. A S C_ ( ( cls ` R ) ` S ) )
20		ss2ixp	\|- ( A. k e. A S C_ ( ( cls ` R ) ` S ) -> X_ k e. A S C_ X_ k e. A ( ( cls ` R ) ` S ) )
21	19 20	syl	\|- ( ph -> X_ k e. A S C_ X_ k e. A ( ( cls ` R ) ` S ) )
22		eqid	\|- U. J = U. J
23	22	clsss2	\|- ( ( 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 ) )
24	16 21 23	syl2anc	\|- ( ph -> ( ( cls ` J ) ` X_ k e. A S ) C_ X_ k e. A ( ( cls ` R ) ` S ) )
25		vex	\|- u e. _V
26		eqeq1	\|- ( x = u -> ( x = X_ y e. A ( g ` y ) <-> u = X_ y e. A ( g ` y ) ) )
27	26	anbi2d	\|- ( 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 ) ) ) )
28	27	exbidv	\|- ( 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 ) ) ) )
29	25 28	elab	\|- ( 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 ) ) )
30		nffvmpt1	\|- F/_ k ( ( k e. A \|-> R ) ` y )
31	30	nfel2	\|- F/ k ( g ` y ) e. ( ( k e. A \|-> R ) ` y )
32		nfv	\|- F/ y ( g ` k ) e. ( ( k e. A \|-> R ) ` k )
33		fveq2	\|- ( y = k -> ( g ` y ) = ( g ` k ) )
34		fveq2	\|- ( y = k -> ( ( k e. A \|-> R ) ` y ) = ( ( k e. A \|-> R ) ` k ) )
35	33 34	eleq12d	\|- ( y = k -> ( ( g ` y ) e. ( ( k e. A \|-> R ) ` y ) <-> ( g ` k ) e. ( ( k e. A \|-> R ) ` k ) ) )
36	31 32 35	cbvralw	\|- ( A. y e. A ( g ` y ) e. ( ( k e. A \|-> R ) ` y ) <-> A. k e. A ( g ` k ) e. ( ( k e. A \|-> R ) ` k ) )
37		simpr	\|- ( ( ph /\ k e. A ) -> k e. A )
38		eqid	\|- ( k e. A \|-> R ) = ( k e. A \|-> R )
39	38	fvmpt2	\|- ( ( k e. A /\ R e. ( TopOn ` X ) ) -> ( ( k e. A \|-> R ) ` k ) = R )
40	37 3 39	syl2anc	\|- ( ( ph /\ k e. A ) -> ( ( k e. A \|-> R ) ` k ) = R )
41	40	eleq2d	\|- ( ( ph /\ k e. A ) -> ( ( g ` k ) e. ( ( k e. A \|-> R ) ` k ) <-> ( g ` k ) e. R ) )
42	41	ralbidva	\|- ( ph -> ( A. k e. A ( g ` k ) e. ( ( k e. A \|-> R ) ` k ) <-> A. k e. A ( g ` k ) e. R ) )
43	36 42	bitrid	\|- ( ph -> ( A. y e. A ( g ` y ) e. ( ( k e. A \|-> R ) ` y ) <-> A. k e. A ( g ` k ) e. R ) )
44	43	anbi2d	\|- ( 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 ) ) )
45	44	adantr	\|- ( ( 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	45	biimpa	\|- ( ( ( 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 ) )
47	5	ad2antrr	\|- ( ( ( 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	\|- ( ( ( 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	\|- f e. _V
50	49	elixp	\|- ( 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	\|- ( f e. X_ k e. A ( ( cls ` R ) ` S ) -> A. k e. A ( f ` k ) e. ( ( cls ` R ) ` S ) )
52	51	ad2antlr	\|- ( ( ( 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	11	clsndisj	\|- ( ( ( 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	\|- ( ( 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	\|- ( ( 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	7 10 55	syl2anc	\|- ( ( 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	\|- ( 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	\|- ( ( ( 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	\|- ( ( ( 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	\|- ( ( ( 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	33	cbvixpv	\|- X_ y e. A ( g ` y ) = X_ k e. A ( g ` k )
62	60 61	eleqtrdi	\|- ( ( ( 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	\|- ( f e. X_ k e. A ( g ` k ) <-> ( f Fn A /\ A. k e. A ( f ` k ) e. ( g ` k ) ) )
64	63	simprbi	\|- ( f e. X_ k e. A ( g ` k ) -> A. k e. A ( f ` k ) e. ( g ` k ) )
65	62 64	syl	\|- ( ( ( 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	\|- ( 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	\|- ( ( ( 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	\|- ( 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	\|- ( ( ( 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	\|- ( { 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	\|- ( 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	\|- ( ( g ` k ) i^i S ) C_ S
73		ssiun2	\|- ( k e. A -> S C_ U_ k e. A S )
74	72 73	sstrid	\|- ( k e. A -> ( ( g ` k ) i^i S ) C_ U_ k e. A S )
75		sseqin2	\|- ( ( ( 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	\|- ( k e. A -> ( U_ k e. A S i^i ( ( g ` k ) i^i S ) ) = ( ( g ` k ) i^i S ) )
77	71 76	eqtr3id	\|- ( 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	\|- ( 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	bitr3id	\|- ( 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	\|- ( 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	\|- ( ( ( 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	\|- F/ y E. z e. U_ k e. A S z e. ( ( g ` k ) i^i S )
83		nfiu1	\|- F/_ k U_ k e. A S
84		nfcv	\|- F/_ k ( g ` y )
85		nfcsb1v	\|- F/_ k [_ y / k ]_ S
86	84 85	nfin	\|- F/_ k ( ( g ` y ) i^i [_ y / k ]_ S )
87	86	nfel2	\|- F/ k z e. ( ( g ` y ) i^i [_ y / k ]_ S )
88	83 87	nfrexw	\|- F/ k E. z e. U_ k e. A S z e. ( ( g ` y ) i^i [_ y / k ]_ S )
89		fveq2	\|- ( k = y -> ( g ` k ) = ( g ` y ) )
90		csbeq1a	\|- ( k = y -> S = [_ y / k ]_ S )
91	89 90	ineq12d	\|- ( k = y -> ( ( g ` k ) i^i S ) = ( ( g ` y ) i^i [_ y / k ]_ S ) )
92	91	eleq2d	\|- ( k = y -> ( z e. ( ( g ` k ) i^i S ) <-> z e. ( ( g ` y ) i^i [_ y / k ]_ S ) ) )
93	92	rexbidv	\|- ( 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	cbvralw	\|- ( 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	\|- ( ( ( 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	\|- ( 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	\|- ( ( 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	\|- ( ( ( 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	\|- ( h : A --> U_ k e. A S -> h Fn A )
100		nfv	\|- F/ y ( h ` k ) e. ( ( g ` k ) i^i S )
101	86	nfel2	\|- F/ k ( h ` y ) e. ( ( g ` y ) i^i [_ y / k ]_ S )
102		fveq2	\|- ( k = y -> ( h ` k ) = ( h ` y ) )
103	102 91	eleq12d	\|- ( k = y -> ( ( h ` k ) e. ( ( g ` k ) i^i S ) <-> ( h ` y ) e. ( ( g ` y ) i^i [_ y / k ]_ S ) ) )
104	100 101 103	cbvralw	\|- ( 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	\|- ( h e. X_ k e. A ( ( g ` k ) i^i S ) -> X_ k e. A ( ( g ` k ) i^i S ) =/= (/) )
106		vex	\|- h e. _V
107	106	elixp	\|- ( 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	\|- 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	\|- ( 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	\|- 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	\|- ( 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	\|- ( ( 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	\|- ( ( 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	\|- ( ( 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	\|- ( 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	\|- ( ( ( 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	\|- ( ( ( 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	46 117	syldan	\|- ( ( ( 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	\|- ( ( ( 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	\|- ( u = X_ y e. A ( g ` y ) -> ( f e. u <-> f e. X_ y e. A ( g ` y ) ) )
121		ineq1	\|- ( 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	\|- ( 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	\|- ( 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	\|- ( ( ( 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	\|- ( ( 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	\|- ( ( 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	29 126	biimtrid	\|- ( ( 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	\|- ( ( 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	7	fmpttd	\|- ( ph -> ( k e. A \|-> R ) : A --> Top )
130	129	ffnd	\|- ( ph -> ( k e. A \|-> R ) Fn A )
131		eqid	\|- { 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 ) ) }
132	131	ptval	\|- ( ( 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 ) ) } ) )
133	2 130 132	syl2anc	\|- ( 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 ) ) } ) )
134	1 133	eqtrid	\|- ( 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 ) ) } ) )
135	134	adantr	\|- ( ( 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 ) ) } ) )
136	3	ralrimiva	\|- ( ph -> A. k e. A R e. ( TopOn ` X ) )
137	1	pttopon	\|- ( ( A e. V /\ A. k e. A R e. ( TopOn ` X ) ) -> J e. ( TopOn ` X_ k e. A X ) )
138	2 136 137	syl2anc	\|- ( ph -> J e. ( TopOn ` X_ k e. A X ) )
139		toponuni	\|- ( J e. ( TopOn ` X_ k e. A X ) -> X_ k e. A X = U. J )
140	138 139	syl	\|- ( ph -> X_ k e. A X = U. J )
141	140	adantr	\|- ( ( ph /\ f e. X_ k e. A ( ( cls ` R ) ` S ) ) -> X_ k e. A X = U. J )
142	131	ptbas	\|- ( ( 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 )
143	2 129 142	syl2anc	\|- ( 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 )
144	143	adantr	\|- ( ( 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 )
145	4	ralrimiva	\|- ( ph -> A. k e. A S C_ X )
146		ss2ixp	\|- ( A. k e. A S C_ X -> X_ k e. A S C_ X_ k e. A X )
147	145 146	syl	\|- ( ph -> X_ k e. A S C_ X_ k e. A X )
148	147	adantr	\|- ( ( ph /\ f e. X_ k e. A ( ( cls ` R ) ` S ) ) -> X_ k e. A S C_ X_ k e. A X )
149	11	clsss3	\|- ( ( R e. Top /\ S C_ U. R ) -> ( ( cls ` R ) ` S ) C_ U. R )
150	7 10 149	syl2anc	\|- ( ( ph /\ k e. A ) -> ( ( cls ` R ) ` S ) C_ U. R )
151	150 9	sseqtrrd	\|- ( ( ph /\ k e. A ) -> ( ( cls ` R ) ` S ) C_ X )
152	151	ralrimiva	\|- ( ph -> A. k e. A ( ( cls ` R ) ` S ) C_ X )
153		ss2ixp	\|- ( A. k e. A ( ( cls ` R ) ` S ) C_ X -> X_ k e. A ( ( cls ` R ) ` S ) C_ X_ k e. A X )
154	152 153	syl	\|- ( ph -> X_ k e. A ( ( cls ` R ) ` S ) C_ X_ k e. A X )
155	154	sselda	\|- ( ( ph /\ f e. X_ k e. A ( ( cls ` R ) ` S ) ) -> f e. X_ k e. A X )
156	135 141 144 148 155	elcls3	\|- ( ( 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 ) =/= (/) ) ) )
157	128 156	mpbird	\|- ( ( ph /\ f e. X_ k e. A ( ( cls ` R ) ` S ) ) -> f e. ( ( cls ` J ) ` X_ k e. A S ) )
158	24 157	eqelssd	\|- ( ph -> ( ( cls ` J ) ` X_ k e. A S ) = X_ k e. A ( ( cls ` R ) ` S ) )

Metamath Proof Explorer

Theorem ptclsg

Proof