txkgen

Description: The topological product of a locally compact space and a compactly generated Hausdorff space is compactly generated. (The condition on S can also be replaced with either "compactly generated weak Hausdorff (CGWH)" or "compact Hausdorff-ly generated (CHG)", where WH means that all images of compact Hausdorff spaces are closed and CHG means that a set is open iff it is open in all compact Hausdorff spaces.) (Contributed by Mario Carneiro, 23-Mar-2015)

		Ref	Expression
	Assertion	txkgen	$⊢ (R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\toR \times_{t} S \in ran 𝑘Gen)$

Proof

Step	Hyp	Ref	Expression
1		nllytop	$⊢ R \in N-LocallyComp\toR \in Top$
2		elinel1	$⊢ S \in (ran 𝑘Gen \cap Haus) \to S \in ran 𝑘Gen$
3		kgentop	$⊢ S \in ran 𝑘Gen \to S \in Top$
4	2 3	syl	$⊢ S \in (ran 𝑘Gen \cap Haus) \to S \in Top$
5		txtop	$⊢ (R \in Top \land S \in Top) \to R \times_{t} S \in Top$
6	1 4 5	syl2an	$⊢ (R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\toR \times_{t} S \in Top)$
7		simplll	$⊢ (((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\toR \in N-LocallyComp)))$
8		eqid	$⊢ (t \in ⋃ R ⟼ ⟨t, 2^{nd} (y)⟩) = (t \in ⋃ R ⟼ ⟨t, 2^{nd} (y)⟩)$
9	8	mptpreima	$⊢ {(t \in ⋃ R ⟼ ⟨t, 2^{nd} (y)⟩)}^{-1} [x] = \{t \in ⋃ R \| ⟨t, 2^{nd} (y)⟩ \in x\}$
10	1	ad3antrrr	$⊢ (((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\toR \in Top)))$
11		toptopon2	$⊢ R \in Top \leftrightarrow R \in TopOn (⋃ R)$
12	10 11	sylib	$⊢ (((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\toR \in TopOn (⋃ R))))$
13		idcn	$⊢ R \in TopOn (⋃ R) \to {I ↾}_{⋃ R} \in (R Cn R)$
14	12 13	syl	$⊢ (((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\to{I ↾}_{⋃ R} \in (R Cn R))))$
15		simpllr	$⊢ (((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\toS \in (ran 𝑘Gen \cap Haus))))$
16	15 4	syl	$⊢ (((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\toS \in Top)))$
17		toptopon2	$⊢ S \in Top \leftrightarrow S \in TopOn (⋃ S)$
18	16 17	sylib	$⊢ (((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\toS \in TopOn (⋃ S))))$
19		simpr	$⊢ (((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\toy \in x)))$
20		simplr	$⊢ (((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\tox \in 𝑘Gen (R \times_{t} S))))$
21		elunii	$⊢ (y \in x \land x \in 𝑘Gen (R \times_{t} S)) \to y \in ⋃ 𝑘Gen (R \times_{t} S)$
22	19 20 21	syl2anc	$⊢ (((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\toy \in ⋃ 𝑘Gen (R \times_{t} S))))$
23		eqid	$⊢ ⋃ R = ⋃ R$
24		eqid	$⊢ ⋃ S = ⋃ S$
25	23 24	txuni	$⊢ (R \in Top \land S \in Top) \to ⋃ R \times ⋃ S = ⋃ (R \times_{t} S)$
26	10 16 25	syl2anc	$⊢ (((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\to⋃ R \times ⋃ S = ⋃ (R \times_{t} S))))$
27	10 16 5	syl2anc	$⊢ (((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\toR \times_{t} S \in Top)))$
28		eqid	$⊢ ⋃ (R \times_{t} S) = ⋃ (R \times_{t} S)$
29	28	kgenuni	$⊢ R \times_{t} S \in Top \to ⋃ (R \times_{t} S) = ⋃ 𝑘Gen (R \times_{t} S)$
30	27 29	syl	$⊢ (((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\to⋃ (R \times_{t} S) = ⋃ 𝑘Gen (R \times_{t} S))))$
31	26 30	eqtrd	$⊢ (((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\to⋃ R \times ⋃ S = ⋃ 𝑘Gen (R \times_{t} S))))$
32	22 31	eleqtrrd	$⊢ (((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\toy \in (⋃ R \times ⋃ S))))$
33		xp2nd	$⊢ y \in (⋃ R \times ⋃ S) \to 2^{nd} (y) \in ⋃ S$
34	32 33	syl	$⊢ (((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\to2^{nd} (y) \in ⋃ S)))$
35		cnconst2	$⊢ (R \in TopOn (⋃ R) \land S \in TopOn (⋃ S) \land 2^{nd} (y) \in ⋃ S) \to ⋃ R \times \{2^{nd} (y)\} \in (R Cn S)$
36	12 18 34 35	syl3anc	$⊢ (((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\to⋃ R \times \{2^{nd} (y)\} \in (R Cn S))))$
37		fvresi	$⊢ t \in ⋃ R \to ({I ↾}_{⋃ R}) (t) = t$
38		fvex	$⊢ 2^{nd} (y) \in V$
39	38	fvconst2	$⊢ t \in ⋃ R \to (⋃ R \times \{2^{nd} (y)\}) (t) = 2^{nd} (y)$
40	37 39	opeq12d	$⊢ t \in ⋃ R \to ⟨({I ↾}_{⋃ R}) (t), (⋃ R \times \{2^{nd} (y)\}) (t)⟩ = ⟨t, 2^{nd} (y)⟩$
41	40	mpteq2ia	$⊢ (t \in ⋃ R ⟼ ⟨({I ↾}_{⋃ R}) (t), (⋃ R \times \{2^{nd} (y)\}) (t)⟩) = (t \in ⋃ R ⟼ ⟨t, 2^{nd} (y)⟩)$
42	41	eqcomi	$⊢ (t \in ⋃ R ⟼ ⟨t, 2^{nd} (y)⟩) = (t \in ⋃ R ⟼ ⟨({I ↾}_{⋃ R}) (t), (⋃ R \times \{2^{nd} (y)\}) (t)⟩)$
43	23 42	txcnmpt	$⊢ ({I ↾}_{⋃ R} \in (R Cn R) \land ⋃ R \times \{2^{nd} (y)\} \in (R Cn S)) \to (t \in ⋃ R ⟼ ⟨t, 2^{nd} (y)⟩) \in (R Cn (R \times_{t} S))$
44	14 36 43	syl2anc	$⊢ (((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\to(t \in ⋃ R ⟼ ⟨t, 2^{nd} (y)⟩) \in (R Cn (R \times_{t} S)))))$
45		llycmpkgen	$⊢ R \in N-LocallyComp\toR \in ran 𝑘Gen$
46	45	ad3antrrr	$⊢ (((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\toR \in ran 𝑘Gen)))$
47	6	ad2antrr	$⊢ (((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\toR \times_{t} S \in Top)))$
48		kgencn3	$⊢ (R \in ran 𝑘Gen \land R \times_{t} S \in Top) \to R Cn (R \times_{t} S) = R Cn 𝑘Gen (R \times_{t} S)$
49	46 47 48	syl2anc	$⊢ (((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\toR Cn (R \times_{t} S) = R Cn 𝑘Gen (R \times_{t} S))))$
50	44 49	eleqtrd	$⊢ (((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\to(t \in ⋃ R ⟼ ⟨t, 2^{nd} (y)⟩) \in (R Cn 𝑘Gen (R \times_{t} S)))))$
51		cnima	$⊢ ((t \in ⋃ R ⟼ ⟨t, 2^{nd} (y)⟩) \in (R Cn 𝑘Gen (R \times_{t} S)) \land x \in 𝑘Gen (R \times_{t} S)) \to {(t \in ⋃ R ⟼ ⟨t, 2^{nd} (y)⟩)}^{-1} [x] \in R$
52	50 20 51	syl2anc	$⊢ (((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\to{(t \in ⋃ R ⟼ ⟨t, 2^{nd} (y)⟩)}^{-1} [x] \in R)))$
53	9 52	eqeltrrid	$⊢ (((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\to\{t \in ⋃ R \| ⟨t, 2^{nd} (y)⟩ \in x\} \in R)))$
54		opeq1	$⊢ t = 1^{st} (y) \to ⟨t, 2^{nd} (y)⟩ = ⟨1^{st} (y), 2^{nd} (y)⟩$
55	54	eleq1d	$⊢ t = 1^{st} (y) \to (⟨t, 2^{nd} (y)⟩ \in x \leftrightarrow ⟨1^{st} (y), 2^{nd} (y)⟩ \in x)$
56		xp1st	$⊢ y \in (⋃ R \times ⋃ S) \to 1^{st} (y) \in ⋃ R$
57	32 56	syl	$⊢ (((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\to1^{st} (y) \in ⋃ R)))$
58		1st2nd2	$⊢ y \in (⋃ R \times ⋃ S) \to y = ⟨1^{st} (y), 2^{nd} (y)⟩$
59	32 58	syl	$⊢ (((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\toy = ⟨1^{st} (y), 2^{nd} (y)⟩)))$
60	59 19	eqeltrrd	$⊢ (((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\to⟨1^{st} (y), 2^{nd} (y)⟩ \in x)))$
61	55 57 60	elrabd	$⊢ (((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\to1^{st} (y) \in \{t \in ⋃ R \| ⟨t, 2^{nd} (y)⟩ \in x\})))$
62		nlly2i	$⊢ (R \in N-LocallyComp\land\{t \in ⋃ R \| ⟨t, 2^{nd} (y)⟩ \in x\} \in R\land1^{st} (y) \in \{t \in ⋃ R \| ⟨t, 2^{nd} (y)⟩ \in x\}\to\exists s \in 𝒫 \{t \in ⋃ R \| ⟨t, 2^{nd} (y)⟩ \in x\})$
63	7 53 61 62	syl3anc	$⊢ (((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\to\exists s \in 𝒫 \{t \in ⋃ R \| ⟨t, 2^{nd} (y)⟩ \in x\})))$
64	10	adantr	$⊢ ((((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\land((s \in 𝒫 \{t \in ⋃ R \| ⟨t, 2^{nd} (y)⟩ \in x\} \land u \in R) \land (1^{st} (y) \in u \land u \subseteq s \land R ↾_{𝑡} s \in Comp))\toR \in Top))))$
65	16	adantr	$⊢ ((((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\land((s \in 𝒫 \{t \in ⋃ R \| ⟨t, 2^{nd} (y)⟩ \in x\} \land u \in R) \land (1^{st} (y) \in u \land u \subseteq s \land R ↾_{𝑡} s \in Comp))\toS \in Top))))$
66		simprlr	$⊢ ((((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\land((s \in 𝒫 \{t \in ⋃ R \| ⟨t, 2^{nd} (y)⟩ \in x\} \land u \in R) \land (1^{st} (y) \in u \land u \subseteq s \land R ↾_{𝑡} s \in Comp))\tou \in R))))$
67		ssrab2	$⊢ \{v \in ⋃ S \| s \times \{v\} \subseteq x\} \subseteq ⋃ S$
68	67	a1i	$⊢ ((((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\land((s \in 𝒫 \{t \in ⋃ R \| ⟨t, 2^{nd} (y)⟩ \in x\} \land u \in R) \land (1^{st} (y) \in u \land u \subseteq s \land R ↾_{𝑡} s \in Comp))\to\{v \in ⋃ S \| s \times \{v\} \subseteq x\} \subseteq ⋃ S))))$
69		incom	$⊢ \{v \in ⋃ S \| s \times \{v\} \subseteq x\} \cap k = k \cap \{v \in ⋃ S \| s \times \{v\} \subseteq x\}$
70		simprll	$⊢ ((((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\land((s \in 𝒫 \{t \in ⋃ R \| ⟨t, 2^{nd} (y)⟩ \in x\} \land u \in R) \land (1^{st} (y) \in u \land u \subseteq s \land R ↾_{𝑡} s \in Comp))\tos \in 𝒫 \{t \in ⋃ R \| ⟨t, 2^{nd} (y)⟩ \in x\}))))$
71	70	elpwid	$⊢ ((((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\land((s \in 𝒫 \{t \in ⋃ R \| ⟨t, 2^{nd} (y)⟩ \in x\} \land u \in R) \land (1^{st} (y) \in u \land u \subseteq s \land R ↾_{𝑡} s \in Comp))\tos \subseteq \{t \in ⋃ R \| ⟨t, 2^{nd} (y)⟩ \in x\}))))$
72		ssrab2	$⊢ \{t \in ⋃ R \| ⟨t, 2^{nd} (y)⟩ \in x\} \subseteq ⋃ R$
73	71 72	sstrdi	$⊢ ((((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\land((s \in 𝒫 \{t \in ⋃ R \| ⟨t, 2^{nd} (y)⟩ \in x\} \land u \in R) \land (1^{st} (y) \in u \land u \subseteq s \land R ↾_{𝑡} s \in Comp))\tos \subseteq ⋃ R))))$
74	73	adantr	$⊢ (((((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\land((s \in 𝒫 \{t \in ⋃ R \| ⟨t, 2^{nd} (y)⟩ \in x\} \land u \in R) \land (1^{st} (y) \in u \land u \subseteq s \land R ↾_{𝑡} s \in Comp))\land(k \in 𝒫 ⋃ S \land S ↾_{𝑡} k \in Comp)\tos \subseteq ⋃ R)))))$
75		elpwi	$⊢ k \in 𝒫 ⋃ S \to k \subseteq ⋃ S$
76	75	ad2antrl	$⊢ (((((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\land((s \in 𝒫 \{t \in ⋃ R \| ⟨t, 2^{nd} (y)⟩ \in x\} \land u \in R) \land (1^{st} (y) \in u \land u \subseteq s \land R ↾_{𝑡} s \in Comp))\land(k \in 𝒫 ⋃ S \land S ↾_{𝑡} k \in Comp)\tok \subseteq ⋃ S)))))$
77		eldif	$⊢ t \in ((s \times k) ∖ x) \leftrightarrow (t \in (s \times k) \land \neg t \in x)$
78	77	anbi1i	$⊢ (t \in ((s \times k) ∖ x) \land ({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) (t) = b) \leftrightarrow ((t \in (s \times k) \land \neg t \in x) \land ({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) (t) = b)$
79		anass	$⊢ ((t \in (s \times k) \land \neg t \in x) \land ({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) (t) = b) \leftrightarrow (t \in (s \times k) \land (\neg t \in x \land ({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) (t) = b))$
80	78 79	bitri	$⊢ (t \in ((s \times k) ∖ x) \land ({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) (t) = b) \leftrightarrow (t \in (s \times k) \land (\neg t \in x \land ({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) (t) = b))$
81	80	rexbii2	$⊢ \exists t \in ((s \times k) ∖ x) ({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) (t) = b \leftrightarrow \exists t \in (s \times k) (\neg t \in x \land ({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) (t) = b)$
82		ancom	$⊢ (\neg t \in x \land ({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) (t) = b) \leftrightarrow (({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) (t) = b \land \neg t \in x)$
83		fveqeq2	$⊢ t = ⟨a, u⟩ \to (({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) (t) = b \leftrightarrow ({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) (⟨a, u⟩) = b)$
84		eleq1	$⊢ t = ⟨a, u⟩ \to (t \in x \leftrightarrow ⟨a, u⟩ \in x)$
85	84	notbid	$⊢ t = ⟨a, u⟩ \to (\neg t \in x \leftrightarrow \neg ⟨a, u⟩ \in x)$
86	83 85	anbi12d	$⊢ t = ⟨a, u⟩ \to ((({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) (t) = b \land \neg t \in x) \leftrightarrow (({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) (⟨a, u⟩) = b \land \neg ⟨a, u⟩ \in x))$
87	82 86	syl5bb	$⊢ t = ⟨a, u⟩ \to ((\neg t \in x \land ({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) (t) = b) \leftrightarrow (({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) (⟨a, u⟩) = b \land \neg ⟨a, u⟩ \in x))$
88	87	rexxp	$⊢ \exists t \in (s \times k) (\neg t \in x \land ({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) (t) = b) \leftrightarrow \exists a \in s \exists u \in k (({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) (⟨a, u⟩) = b \land \neg ⟨a, u⟩ \in x)$
89	81 88	bitri	$⊢ \exists t \in ((s \times k) ∖ x) ({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) (t) = b \leftrightarrow \exists a \in s \exists u \in k (({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) (⟨a, u⟩) = b \land \neg ⟨a, u⟩ \in x)$
90		simpl	$⊢ (s \subseteq ⋃ R \land k \subseteq ⋃ S) \to s \subseteq ⋃ R$
91	90	sselda	$⊢ ((s \subseteq ⋃ R \land k \subseteq ⋃ S) \land a \in s) \to a \in ⋃ R$
92	91	adantr	$⊢ (((s \subseteq ⋃ R \land k \subseteq ⋃ S) \land a \in s) \land u \in k) \to a \in ⋃ R$
93		simplr	$⊢ ((s \subseteq ⋃ R \land k \subseteq ⋃ S) \land a \in s) \to k \subseteq ⋃ S$
94	93	sselda	$⊢ (((s \subseteq ⋃ R \land k \subseteq ⋃ S) \land a \in s) \land u \in k) \to u \in ⋃ S$
95	92 94	opelxpd	$⊢ (((s \subseteq ⋃ R \land k \subseteq ⋃ S) \land a \in s) \land u \in k) \to ⟨a, u⟩ \in (⋃ R \times ⋃ S)$
96	95	fvresd	$⊢ (((s \subseteq ⋃ R \land k \subseteq ⋃ S) \land a \in s) \land u \in k) \to ({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) (⟨a, u⟩) = 2^{nd} (⟨a, u⟩)$
97		vex	$⊢ a \in V$
98		vex	$⊢ u \in V$
99	97 98	op2nd	$⊢ 2^{nd} (⟨a, u⟩) = u$
100	96 99	eqtrdi	$⊢ (((s \subseteq ⋃ R \land k \subseteq ⋃ S) \land a \in s) \land u \in k) \to ({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) (⟨a, u⟩) = u$
101	100	eqeq1d	$⊢ (((s \subseteq ⋃ R \land k \subseteq ⋃ S) \land a \in s) \land u \in k) \to (({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) (⟨a, u⟩) = b \leftrightarrow u = b)$
102	101	anbi1d	$⊢ (((s \subseteq ⋃ R \land k \subseteq ⋃ S) \land a \in s) \land u \in k) \to ((({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) (⟨a, u⟩) = b \land \neg ⟨a, u⟩ \in x) \leftrightarrow (u = b \land \neg ⟨a, u⟩ \in x))$
103	102	rexbidva	$⊢ ((s \subseteq ⋃ R \land k \subseteq ⋃ S) \land a \in s) \to (\exists u \in k (({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) (⟨a, u⟩) = b \land \neg ⟨a, u⟩ \in x) \leftrightarrow \exists u \in k (u = b \land \neg ⟨a, u⟩ \in x))$
104		opeq2	$⊢ u = b \to ⟨a, u⟩ = ⟨a, b⟩$
105	104	eleq1d	$⊢ u = b \to (⟨a, u⟩ \in x \leftrightarrow ⟨a, b⟩ \in x)$
106	105	notbid	$⊢ u = b \to (\neg ⟨a, u⟩ \in x \leftrightarrow \neg ⟨a, b⟩ \in x)$
107	106	ceqsrexbv	$⊢ \exists u \in k (u = b \land \neg ⟨a, u⟩ \in x) \leftrightarrow (b \in k \land \neg ⟨a, b⟩ \in x)$
108	103 107	bitrdi	$⊢ ((s \subseteq ⋃ R \land k \subseteq ⋃ S) \land a \in s) \to (\exists u \in k (({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) (⟨a, u⟩) = b \land \neg ⟨a, u⟩ \in x) \leftrightarrow (b \in k \land \neg ⟨a, b⟩ \in x))$
109	108	rexbidva	$⊢ (s \subseteq ⋃ R \land k \subseteq ⋃ S) \to (\exists a \in s \exists u \in k (({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) (⟨a, u⟩) = b \land \neg ⟨a, u⟩ \in x) \leftrightarrow \exists a \in s (b \in k \land \neg ⟨a, b⟩ \in x))$
110		r19.42v	$⊢ \exists a \in s (b \in k \land \neg ⟨a, b⟩ \in x) \leftrightarrow (b \in k \land \exists a \in s \neg ⟨a, b⟩ \in x)$
111	109 110	bitrdi	$⊢ (s \subseteq ⋃ R \land k \subseteq ⋃ S) \to (\exists a \in s \exists u \in k (({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) (⟨a, u⟩) = b \land \neg ⟨a, u⟩ \in x) \leftrightarrow (b \in k \land \exists a \in s \neg ⟨a, b⟩ \in x))$
112	89 111	syl5bb	$⊢ (s \subseteq ⋃ R \land k \subseteq ⋃ S) \to (\exists t \in ((s \times k) ∖ x) ({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) (t) = b \leftrightarrow (b \in k \land \exists a \in s \neg ⟨a, b⟩ \in x))$
113		f2ndres	$⊢ ({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) : ⋃ R \times ⋃ S ⟶ ⋃ S$
114		ffn	$⊢ ({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) : ⋃ R \times ⋃ S ⟶ ⋃ S \to ({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) Fn (⋃ R \times ⋃ S)$
115	113 114	ax-mp	$⊢ ({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) Fn (⋃ R \times ⋃ S)$
116		difss	$⊢ (s \times k) ∖ x \subseteq s \times k$
117		xpss12	$⊢ (s \subseteq ⋃ R \land k \subseteq ⋃ S) \to s \times k \subseteq ⋃ R \times ⋃ S$
118	116 117	sstrid	$⊢ (s \subseteq ⋃ R \land k \subseteq ⋃ S) \to (s \times k) ∖ x \subseteq ⋃ R \times ⋃ S$
119		fvelimab	$⊢ (({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) Fn (⋃ R \times ⋃ S) \land (s \times k) ∖ x \subseteq ⋃ R \times ⋃ S) \to (b \in ({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) [(s \times k) ∖ x] \leftrightarrow \exists t \in ((s \times k) ∖ x) ({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) (t) = b)$
120	115 118 119	sylancr	$⊢ (s \subseteq ⋃ R \land k \subseteq ⋃ S) \to (b \in ({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) [(s \times k) ∖ x] \leftrightarrow \exists t \in ((s \times k) ∖ x) ({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) (t) = b)$
121		eldif	$⊢ b \in (k ∖ \{v \in ⋃ S \| s \times \{v\} \subseteq x\}) \leftrightarrow (b \in k \land \neg b \in \{v \in ⋃ S \| s \times \{v\} \subseteq x\})$
122		simpr	$⊢ (s \subseteq ⋃ R \land k \subseteq ⋃ S) \to k \subseteq ⋃ S$
123	122	sselda	$⊢ ((s \subseteq ⋃ R \land k \subseteq ⋃ S) \land b \in k) \to b \in ⋃ S$
124		sneq	$⊢ v = b \to \{v\} = \{b\}$
125	124	xpeq2d	$⊢ v = b \to s \times \{v\} = s \times \{b\}$
126	125	sseq1d	$⊢ v = b \to (s \times \{v\} \subseteq x \leftrightarrow s \times \{b\} \subseteq x)$
127		dfss3	$⊢ s \times \{b\} \subseteq x \leftrightarrow \forall k \in (s \times \{b\}) k \in x$
128		eleq1	$⊢ k = ⟨a, t⟩ \to (k \in x \leftrightarrow ⟨a, t⟩ \in x)$
129	128	ralxp	$⊢ \forall k \in (s \times \{b\}) k \in x \leftrightarrow \forall a \in s \forall t \in \{b\} ⟨a, t⟩ \in x$
130		vex	$⊢ b \in V$
131		opeq2	$⊢ t = b \to ⟨a, t⟩ = ⟨a, b⟩$
132	131	eleq1d	$⊢ t = b \to (⟨a, t⟩ \in x \leftrightarrow ⟨a, b⟩ \in x)$
133	130 132	ralsn	$⊢ \forall t \in \{b\} ⟨a, t⟩ \in x \leftrightarrow ⟨a, b⟩ \in x$
134	133	ralbii	$⊢ \forall a \in s \forall t \in \{b\} ⟨a, t⟩ \in x \leftrightarrow \forall a \in s ⟨a, b⟩ \in x$
135	127 129 134	3bitri	$⊢ s \times \{b\} \subseteq x \leftrightarrow \forall a \in s ⟨a, b⟩ \in x$
136	126 135	bitrdi	$⊢ v = b \to (s \times \{v\} \subseteq x \leftrightarrow \forall a \in s ⟨a, b⟩ \in x)$
137	136	elrab3	$⊢ b \in ⋃ S \to (b \in \{v \in ⋃ S \| s \times \{v\} \subseteq x\} \leftrightarrow \forall a \in s ⟨a, b⟩ \in x)$
138	123 137	syl	$⊢ ((s \subseteq ⋃ R \land k \subseteq ⋃ S) \land b \in k) \to (b \in \{v \in ⋃ S \| s \times \{v\} \subseteq x\} \leftrightarrow \forall a \in s ⟨a, b⟩ \in x)$
139	138	notbid	$⊢ ((s \subseteq ⋃ R \land k \subseteq ⋃ S) \land b \in k) \to (\neg b \in \{v \in ⋃ S \| s \times \{v\} \subseteq x\} \leftrightarrow \neg \forall a \in s ⟨a, b⟩ \in x)$
140		rexnal	$⊢ \exists a \in s \neg ⟨a, b⟩ \in x \leftrightarrow \neg \forall a \in s ⟨a, b⟩ \in x$
141	139 140	bitr4di	$⊢ ((s \subseteq ⋃ R \land k \subseteq ⋃ S) \land b \in k) \to (\neg b \in \{v \in ⋃ S \| s \times \{v\} \subseteq x\} \leftrightarrow \exists a \in s \neg ⟨a, b⟩ \in x)$
142	141	pm5.32da	$⊢ (s \subseteq ⋃ R \land k \subseteq ⋃ S) \to ((b \in k \land \neg b \in \{v \in ⋃ S \| s \times \{v\} \subseteq x\}) \leftrightarrow (b \in k \land \exists a \in s \neg ⟨a, b⟩ \in x))$
143	121 142	syl5bb	$⊢ (s \subseteq ⋃ R \land k \subseteq ⋃ S) \to (b \in (k ∖ \{v \in ⋃ S \| s \times \{v\} \subseteq x\}) \leftrightarrow (b \in k \land \exists a \in s \neg ⟨a, b⟩ \in x))$
144	112 120 143	3bitr4d	$⊢ (s \subseteq ⋃ R \land k \subseteq ⋃ S) \to (b \in ({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) [(s \times k) ∖ x] \leftrightarrow b \in (k ∖ \{v \in ⋃ S \| s \times \{v\} \subseteq x\}))$
145	144	eqrdv	$⊢ (s \subseteq ⋃ R \land k \subseteq ⋃ S) \to ({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) [(s \times k) ∖ x] = k ∖ \{v \in ⋃ S \| s \times \{v\} \subseteq x\}$
146	74 76 145	syl2anc	$⊢ (((((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\land((s \in 𝒫 \{t \in ⋃ R \| ⟨t, 2^{nd} (y)⟩ \in x\} \land u \in R) \land (1^{st} (y) \in u \land u \subseteq s \land R ↾_{𝑡} s \in Comp))\land(k \in 𝒫 ⋃ S \land S ↾_{𝑡} k \in Comp)\to({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) [(s \times k) ∖ x] = k ∖ \{v \in ⋃ S \| s \times \{v\} \subseteq x\})))))$
147		difin	$⊢ k ∖ (k \cap \{v \in ⋃ S \| s \times \{v\} \subseteq x\}) = k ∖ \{v \in ⋃ S \| s \times \{v\} \subseteq x\}$
148	65	adantr	$⊢ (((((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\land((s \in 𝒫 \{t \in ⋃ R \| ⟨t, 2^{nd} (y)⟩ \in x\} \land u \in R) \land (1^{st} (y) \in u \land u \subseteq s \land R ↾_{𝑡} s \in Comp))\land(k \in 𝒫 ⋃ S \land S ↾_{𝑡} k \in Comp)\toS \in Top)))))$
149	24	restuni	$⊢ (S \in Top \land k \subseteq ⋃ S) \to k = ⋃ (S ↾_{𝑡} k)$
150	148 76 149	syl2anc	$⊢ (((((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\land((s \in 𝒫 \{t \in ⋃ R \| ⟨t, 2^{nd} (y)⟩ \in x\} \land u \in R) \land (1^{st} (y) \in u \land u \subseteq s \land R ↾_{𝑡} s \in Comp))\land(k \in 𝒫 ⋃ S \land S ↾_{𝑡} k \in Comp)\tok = ⋃ (S ↾_{𝑡} k))))))$
151	150	difeq1d	$⊢ (((((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\land((s \in 𝒫 \{t \in ⋃ R \| ⟨t, 2^{nd} (y)⟩ \in x\} \land u \in R) \land (1^{st} (y) \in u \land u \subseteq s \land R ↾_{𝑡} s \in Comp))\land(k \in 𝒫 ⋃ S \land S ↾_{𝑡} k \in Comp)\tok ∖ (k \cap \{v \in ⋃ S \| s \times \{v\} \subseteq x\}) = ⋃ (S ↾_{𝑡} k) ∖ (k \cap \{v \in ⋃ S \| s \times \{v\} \subseteq x\}))))))$
152	147 151	syl5eqr	$⊢ (((((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\land((s \in 𝒫 \{t \in ⋃ R \| ⟨t, 2^{nd} (y)⟩ \in x\} \land u \in R) \land (1^{st} (y) \in u \land u \subseteq s \land R ↾_{𝑡} s \in Comp))\land(k \in 𝒫 ⋃ S \land S ↾_{𝑡} k \in Comp)\tok ∖ \{v \in ⋃ S \| s \times \{v\} \subseteq x\} = ⋃ (S ↾_{𝑡} k) ∖ (k \cap \{v \in ⋃ S \| s \times \{v\} \subseteq x\}))))))$
153	146 152	eqtrd	$⊢ (((((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\land((s \in 𝒫 \{t \in ⋃ R \| ⟨t, 2^{nd} (y)⟩ \in x\} \land u \in R) \land (1^{st} (y) \in u \land u \subseteq s \land R ↾_{𝑡} s \in Comp))\land(k \in 𝒫 ⋃ S \land S ↾_{𝑡} k \in Comp)\to({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) [(s \times k) ∖ x] = ⋃ (S ↾_{𝑡} k) ∖ (k \cap \{v \in ⋃ S \| s \times \{v\} \subseteq x\}))))))$
154	15	ad2antrr	$⊢ (((((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\land((s \in 𝒫 \{t \in ⋃ R \| ⟨t, 2^{nd} (y)⟩ \in x\} \land u \in R) \land (1^{st} (y) \in u \land u \subseteq s \land R ↾_{𝑡} s \in Comp))\land(k \in 𝒫 ⋃ S \land S ↾_{𝑡} k \in Comp)\toS \in (ran 𝑘Gen \cap Haus))))))$
155	154	elin2d	$⊢ (((((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\land((s \in 𝒫 \{t \in ⋃ R \| ⟨t, 2^{nd} (y)⟩ \in x\} \land u \in R) \land (1^{st} (y) \in u \land u \subseteq s \land R ↾_{𝑡} s \in Comp))\land(k \in 𝒫 ⋃ S \land S ↾_{𝑡} k \in Comp)\toS \in Haus)))))$
156		df-ima	$⊢ ({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) [(s \times k) ∖ x] = ran ({({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) ↾}_{((s \times k) ∖ x)})$
157		resres	$⊢ {({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) ↾}_{((s \times k) ∖ x)} = {2^{nd} ↾}_{((⋃ R \times ⋃ S) \cap ((s \times k) ∖ x))}$
158		inss2	$⊢ (⋃ R \times ⋃ S) \cap ((s \times k) ∖ x) \subseteq (s \times k) ∖ x$
159	158 116	sstri	$⊢ (⋃ R \times ⋃ S) \cap ((s \times k) ∖ x) \subseteq s \times k$
160		ssres2	$⊢ (⋃ R \times ⋃ S) \cap ((s \times k) ∖ x) \subseteq s \times k \to {2^{nd} ↾}_{((⋃ R \times ⋃ S) \cap ((s \times k) ∖ x))} \subseteq {2^{nd} ↾}_{(s \times k)}$
161	159 160	ax-mp	$⊢ {2^{nd} ↾}_{((⋃ R \times ⋃ S) \cap ((s \times k) ∖ x))} \subseteq {2^{nd} ↾}_{(s \times k)}$
162	157 161	eqsstri	$⊢ {({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) ↾}_{((s \times k) ∖ x)} \subseteq {2^{nd} ↾}_{(s \times k)}$
163	162	rnssi	$⊢ ran ({({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) ↾}_{((s \times k) ∖ x)}) \subseteq ran ({2^{nd} ↾}_{(s \times k)})$
164	156 163	eqsstri	$⊢ ({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) [(s \times k) ∖ x] \subseteq ran ({2^{nd} ↾}_{(s \times k)})$
165		f2ndres	$⊢ ({2^{nd} ↾}_{(s \times k)}) : s \times k ⟶ k$
166		frn	$⊢ ({2^{nd} ↾}_{(s \times k)}) : s \times k ⟶ k \to ran ({2^{nd} ↾}_{(s \times k)}) \subseteq k$
167	165 166	ax-mp	$⊢ ran ({2^{nd} ↾}_{(s \times k)}) \subseteq k$
168	164 167	sstri	$⊢ ({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) [(s \times k) ∖ x] \subseteq k$
169	168 76	sstrid	$⊢ (((((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\land((s \in 𝒫 \{t \in ⋃ R \| ⟨t, 2^{nd} (y)⟩ \in x\} \land u \in R) \land (1^{st} (y) \in u \land u \subseteq s \land R ↾_{𝑡} s \in Comp))\land(k \in 𝒫 ⋃ S \land S ↾_{𝑡} k \in Comp)\to({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) [(s \times k) ∖ x] \subseteq ⋃ S)))))$
170	12	ad2antrr	$⊢ (((((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\land((s \in 𝒫 \{t \in ⋃ R \| ⟨t, 2^{nd} (y)⟩ \in x\} \land u \in R) \land (1^{st} (y) \in u \land u \subseteq s \land R ↾_{𝑡} s \in Comp))\land(k \in 𝒫 ⋃ S \land S ↾_{𝑡} k \in Comp)\toR \in TopOn (⋃ R))))))$
171	148 17	sylib	$⊢ (((((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\land((s \in 𝒫 \{t \in ⋃ R \| ⟨t, 2^{nd} (y)⟩ \in x\} \land u \in R) \land (1^{st} (y) \in u \land u \subseteq s \land R ↾_{𝑡} s \in Comp))\land(k \in 𝒫 ⋃ S \land S ↾_{𝑡} k \in Comp)\toS \in TopOn (⋃ S))))))$
172		tx2cn	$⊢ (R \in TopOn (⋃ R) \land S \in TopOn (⋃ S)) \to {2^{nd} ↾}_{(⋃ R \times ⋃ S)} \in ((R \times_{t} S) Cn S)$
173	170 171 172	syl2anc	$⊢ (((((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\land((s \in 𝒫 \{t \in ⋃ R \| ⟨t, 2^{nd} (y)⟩ \in x\} \land u \in R) \land (1^{st} (y) \in u \land u \subseteq s \land R ↾_{𝑡} s \in Comp))\land(k \in 𝒫 ⋃ S \land S ↾_{𝑡} k \in Comp)\to{2^{nd} ↾}_{(⋃ R \times ⋃ S)} \in ((R \times_{t} S) Cn S))))))$
174	27	ad2antrr	$⊢ (((((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\land((s \in 𝒫 \{t \in ⋃ R \| ⟨t, 2^{nd} (y)⟩ \in x\} \land u \in R) \land (1^{st} (y) \in u \land u \subseteq s \land R ↾_{𝑡} s \in Comp))\land(k \in 𝒫 ⋃ S \land S ↾_{𝑡} k \in Comp)\toR \times_{t} S \in Top)))))$
175	116	a1i	$⊢ (((((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\land((s \in 𝒫 \{t \in ⋃ R \| ⟨t, 2^{nd} (y)⟩ \in x\} \land u \in R) \land (1^{st} (y) \in u \land u \subseteq s \land R ↾_{𝑡} s \in Comp))\land(k \in 𝒫 ⋃ S \land S ↾_{𝑡} k \in Comp)\to(s \times k) ∖ x \subseteq s \times k)))))$
176		vex	$⊢ s \in V$
177		vex	$⊢ k \in V$
178	176 177	xpex	$⊢ s \times k \in V$
179	178	a1i	$⊢ (((((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\land((s \in 𝒫 \{t \in ⋃ R \| ⟨t, 2^{nd} (y)⟩ \in x\} \land u \in R) \land (1^{st} (y) \in u \land u \subseteq s \land R ↾_{𝑡} s \in Comp))\land(k \in 𝒫 ⋃ S \land S ↾_{𝑡} k \in Comp)\tos \times k \in V)))))$
180		restabs	$⊢ (R \times_{t} S \in Top \land (s \times k) ∖ x \subseteq s \times k \land s \times k \in V) \to ((R \times_{t} S) ↾_{𝑡} (s \times k)) ↾_{𝑡} ((s \times k) ∖ x) = (R \times_{t} S) ↾_{𝑡} ((s \times k) ∖ x)$
181	174 175 179 180	syl3anc	$⊢ (((((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\land((s \in 𝒫 \{t \in ⋃ R \| ⟨t, 2^{nd} (y)⟩ \in x\} \land u \in R) \land (1^{st} (y) \in u \land u \subseteq s \land R ↾_{𝑡} s \in Comp))\land(k \in 𝒫 ⋃ S \land S ↾_{𝑡} k \in Comp)\to((R \times_{t} S) ↾_{𝑡} (s \times k)) ↾_{𝑡} ((s \times k) ∖ x) = (R \times_{t} S) ↾_{𝑡} ((s \times k) ∖ x))))))$
182	64	adantr	$⊢ (((((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\land((s \in 𝒫 \{t \in ⋃ R \| ⟨t, 2^{nd} (y)⟩ \in x\} \land u \in R) \land (1^{st} (y) \in u \land u \subseteq s \land R ↾_{𝑡} s \in Comp))\land(k \in 𝒫 ⋃ S \land S ↾_{𝑡} k \in Comp)\toR \in Top)))))$
183	154 4	syl	$⊢ (((((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\land((s \in 𝒫 \{t \in ⋃ R \| ⟨t, 2^{nd} (y)⟩ \in x\} \land u \in R) \land (1^{st} (y) \in u \land u \subseteq s \land R ↾_{𝑡} s \in Comp))\land(k \in 𝒫 ⋃ S \land S ↾_{𝑡} k \in Comp)\toS \in Top)))))$
184	176	a1i	$⊢ (((((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\land((s \in 𝒫 \{t \in ⋃ R \| ⟨t, 2^{nd} (y)⟩ \in x\} \land u \in R) \land (1^{st} (y) \in u \land u \subseteq s \land R ↾_{𝑡} s \in Comp))\land(k \in 𝒫 ⋃ S \land S ↾_{𝑡} k \in Comp)\tos \in V)))))$
185		simprl	$⊢ (((((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\land((s \in 𝒫 \{t \in ⋃ R \| ⟨t, 2^{nd} (y)⟩ \in x\} \land u \in R) \land (1^{st} (y) \in u \land u \subseteq s \land R ↾_{𝑡} s \in Comp))\land(k \in 𝒫 ⋃ S \land S ↾_{𝑡} k \in Comp)\tok \in 𝒫 ⋃ S)))))$
186		txrest	$⊢ ((R \in Top \land S \in Top) \land (s \in V \land k \in 𝒫 ⋃ S)) \to (R \times_{t} S) ↾_{𝑡} (s \times k) = (R ↾_{𝑡} s) \times_{t} (S ↾_{𝑡} k)$
187	182 183 184 185 186	syl22anc	$⊢ (((((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\land((s \in 𝒫 \{t \in ⋃ R \| ⟨t, 2^{nd} (y)⟩ \in x\} \land u \in R) \land (1^{st} (y) \in u \land u \subseteq s \land R ↾_{𝑡} s \in Comp))\land(k \in 𝒫 ⋃ S \land S ↾_{𝑡} k \in Comp)\to(R \times_{t} S) ↾_{𝑡} (s \times k) = (R ↾_{𝑡} s) \times_{t} (S ↾_{𝑡} k))))))$
188		simprr3	$⊢ ((((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\land((s \in 𝒫 \{t \in ⋃ R \| ⟨t, 2^{nd} (y)⟩ \in x\} \land u \in R) \land (1^{st} (y) \in u \land u \subseteq s \land R ↾_{𝑡} s \in Comp))\toR ↾_{𝑡} s \in Comp))))$
189	188	adantr	$⊢ (((((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\land((s \in 𝒫 \{t \in ⋃ R \| ⟨t, 2^{nd} (y)⟩ \in x\} \land u \in R) \land (1^{st} (y) \in u \land u \subseteq s \land R ↾_{𝑡} s \in Comp))\land(k \in 𝒫 ⋃ S \land S ↾_{𝑡} k \in Comp)\toR ↾_{𝑡} s \in Comp)))))$
190		simprr	$⊢ (((((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\land((s \in 𝒫 \{t \in ⋃ R \| ⟨t, 2^{nd} (y)⟩ \in x\} \land u \in R) \land (1^{st} (y) \in u \land u \subseteq s \land R ↾_{𝑡} s \in Comp))\land(k \in 𝒫 ⋃ S \land S ↾_{𝑡} k \in Comp)\toS ↾_{𝑡} k \in Comp)))))$
191		txcmp	$⊢ (R ↾_{𝑡} s \in Comp \land S ↾_{𝑡} k \in Comp) \to (R ↾_{𝑡} s) \times_{t} (S ↾_{𝑡} k) \in Comp$
192	189 190 191	syl2anc	$⊢ (((((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\land((s \in 𝒫 \{t \in ⋃ R \| ⟨t, 2^{nd} (y)⟩ \in x\} \land u \in R) \land (1^{st} (y) \in u \land u \subseteq s \land R ↾_{𝑡} s \in Comp))\land(k \in 𝒫 ⋃ S \land S ↾_{𝑡} k \in Comp)\to(R ↾_{𝑡} s) \times_{t} (S ↾_{𝑡} k) \in Comp)))))$
193	187 192	eqeltrd	$⊢ (((((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\land((s \in 𝒫 \{t \in ⋃ R \| ⟨t, 2^{nd} (y)⟩ \in x\} \land u \in R) \land (1^{st} (y) \in u \land u \subseteq s \land R ↾_{𝑡} s \in Comp))\land(k \in 𝒫 ⋃ S \land S ↾_{𝑡} k \in Comp)\to(R \times_{t} S) ↾_{𝑡} (s \times k) \in Comp)))))$
194		difin	$⊢ (s \times k) ∖ ((s \times k) \cap x) = (s \times k) ∖ x$
195	74 76 117	syl2anc	$⊢ (((((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\land((s \in 𝒫 \{t \in ⋃ R \| ⟨t, 2^{nd} (y)⟩ \in x\} \land u \in R) \land (1^{st} (y) \in u \land u \subseteq s \land R ↾_{𝑡} s \in Comp))\land(k \in 𝒫 ⋃ S \land S ↾_{𝑡} k \in Comp)\tos \times k \subseteq ⋃ R \times ⋃ S)))))$
196	182 148 25	syl2anc	$⊢ (((((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\land((s \in 𝒫 \{t \in ⋃ R \| ⟨t, 2^{nd} (y)⟩ \in x\} \land u \in R) \land (1^{st} (y) \in u \land u \subseteq s \land R ↾_{𝑡} s \in Comp))\land(k \in 𝒫 ⋃ S \land S ↾_{𝑡} k \in Comp)\to⋃ R \times ⋃ S = ⋃ (R \times_{t} S))))))$
197	195 196	sseqtrd	$⊢ (((((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\land((s \in 𝒫 \{t \in ⋃ R \| ⟨t, 2^{nd} (y)⟩ \in x\} \land u \in R) \land (1^{st} (y) \in u \land u \subseteq s \land R ↾_{𝑡} s \in Comp))\land(k \in 𝒫 ⋃ S \land S ↾_{𝑡} k \in Comp)\tos \times k \subseteq ⋃ (R \times_{t} S))))))$
198	28	restuni	$⊢ (R \times_{t} S \in Top \land s \times k \subseteq ⋃ (R \times_{t} S)) \to s \times k = ⋃ ((R \times_{t} S) ↾_{𝑡} (s \times k))$
199	174 197 198	syl2anc	$⊢ (((((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\land((s \in 𝒫 \{t \in ⋃ R \| ⟨t, 2^{nd} (y)⟩ \in x\} \land u \in R) \land (1^{st} (y) \in u \land u \subseteq s \land R ↾_{𝑡} s \in Comp))\land(k \in 𝒫 ⋃ S \land S ↾_{𝑡} k \in Comp)\tos \times k = ⋃ ((R \times_{t} S) ↾_{𝑡} (s \times k)))))))$
200	199	difeq1d	$⊢ (((((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\land((s \in 𝒫 \{t \in ⋃ R \| ⟨t, 2^{nd} (y)⟩ \in x\} \land u \in R) \land (1^{st} (y) \in u \land u \subseteq s \land R ↾_{𝑡} s \in Comp))\land(k \in 𝒫 ⋃ S \land S ↾_{𝑡} k \in Comp)\to(s \times k) ∖ ((s \times k) \cap x) = ⋃ ((R \times_{t} S) ↾_{𝑡} (s \times k)) ∖ ((s \times k) \cap x))))))$
201	194 200	syl5eqr	$⊢ (((((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\land((s \in 𝒫 \{t \in ⋃ R \| ⟨t, 2^{nd} (y)⟩ \in x\} \land u \in R) \land (1^{st} (y) \in u \land u \subseteq s \land R ↾_{𝑡} s \in Comp))\land(k \in 𝒫 ⋃ S \land S ↾_{𝑡} k \in Comp)\to(s \times k) ∖ x = ⋃ ((R \times_{t} S) ↾_{𝑡} (s \times k)) ∖ ((s \times k) \cap x))))))$
202		resttop	$⊢ (R \times_{t} S \in Top \land s \times k \in V) \to (R \times_{t} S) ↾_{𝑡} (s \times k) \in Top$
203	174 178 202	sylancl	$⊢ (((((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\land((s \in 𝒫 \{t \in ⋃ R \| ⟨t, 2^{nd} (y)⟩ \in x\} \land u \in R) \land (1^{st} (y) \in u \land u \subseteq s \land R ↾_{𝑡} s \in Comp))\land(k \in 𝒫 ⋃ S \land S ↾_{𝑡} k \in Comp)\to(R \times_{t} S) ↾_{𝑡} (s \times k) \in Top)))))$
204		incom	$⊢ (s \times k) \cap x = x \cap (s \times k)$
205	20	ad2antrr	$⊢ (((((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\land((s \in 𝒫 \{t \in ⋃ R \| ⟨t, 2^{nd} (y)⟩ \in x\} \land u \in R) \land (1^{st} (y) \in u \land u \subseteq s \land R ↾_{𝑡} s \in Comp))\land(k \in 𝒫 ⋃ S \land S ↾_{𝑡} k \in Comp)\tox \in 𝑘Gen (R \times_{t} S))))))$
206		kgeni	$⊢ (x \in 𝑘Gen (R \times_{t} S) \land (R \times_{t} S) ↾_{𝑡} (s \times k) \in Comp) \to x \cap (s \times k) \in ((R \times_{t} S) ↾_{𝑡} (s \times k))$
207	205 193 206	syl2anc	$⊢ (((((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\land((s \in 𝒫 \{t \in ⋃ R \| ⟨t, 2^{nd} (y)⟩ \in x\} \land u \in R) \land (1^{st} (y) \in u \land u \subseteq s \land R ↾_{𝑡} s \in Comp))\land(k \in 𝒫 ⋃ S \land S ↾_{𝑡} k \in Comp)\tox \cap (s \times k) \in ((R \times_{t} S) ↾_{𝑡} (s \times k)))))))$
208	204 207	eqeltrid	$⊢ (((((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\land((s \in 𝒫 \{t \in ⋃ R \| ⟨t, 2^{nd} (y)⟩ \in x\} \land u \in R) \land (1^{st} (y) \in u \land u \subseteq s \land R ↾_{𝑡} s \in Comp))\land(k \in 𝒫 ⋃ S \land S ↾_{𝑡} k \in Comp)\to(s \times k) \cap x \in ((R \times_{t} S) ↾_{𝑡} (s \times k)))))))$
209		eqid	$⊢ ⋃ ((R \times_{t} S) ↾_{𝑡} (s \times k)) = ⋃ ((R \times_{t} S) ↾_{𝑡} (s \times k))$
210	209	opncld	$⊢ ((R \times_{t} S) ↾_{𝑡} (s \times k) \in Top \land (s \times k) \cap x \in ((R \times_{t} S) ↾_{𝑡} (s \times k))) \to ⋃ ((R \times_{t} S) ↾_{𝑡} (s \times k)) ∖ ((s \times k) \cap x) \in Clsd ((R \times_{t} S) ↾_{𝑡} (s \times k))$
211	203 208 210	syl2anc	$⊢ (((((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\land((s \in 𝒫 \{t \in ⋃ R \| ⟨t, 2^{nd} (y)⟩ \in x\} \land u \in R) \land (1^{st} (y) \in u \land u \subseteq s \land R ↾_{𝑡} s \in Comp))\land(k \in 𝒫 ⋃ S \land S ↾_{𝑡} k \in Comp)\to⋃ ((R \times_{t} S) ↾_{𝑡} (s \times k)) ∖ ((s \times k) \cap x) \in Clsd ((R \times_{t} S) ↾_{𝑡} (s \times k)))))))$
212	201 211	eqeltrd	$⊢ (((((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\land((s \in 𝒫 \{t \in ⋃ R \| ⟨t, 2^{nd} (y)⟩ \in x\} \land u \in R) \land (1^{st} (y) \in u \land u \subseteq s \land R ↾_{𝑡} s \in Comp))\land(k \in 𝒫 ⋃ S \land S ↾_{𝑡} k \in Comp)\to(s \times k) ∖ x \in Clsd ((R \times_{t} S) ↾_{𝑡} (s \times k)))))))$
213		cmpcld	$⊢ ((R \times_{t} S) ↾_{𝑡} (s \times k) \in Comp \land (s \times k) ∖ x \in Clsd ((R \times_{t} S) ↾_{𝑡} (s \times k))) \to ((R \times_{t} S) ↾_{𝑡} (s \times k)) ↾_{𝑡} ((s \times k) ∖ x) \in Comp$
214	193 212 213	syl2anc	$⊢ (((((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\land((s \in 𝒫 \{t \in ⋃ R \| ⟨t, 2^{nd} (y)⟩ \in x\} \land u \in R) \land (1^{st} (y) \in u \land u \subseteq s \land R ↾_{𝑡} s \in Comp))\land(k \in 𝒫 ⋃ S \land S ↾_{𝑡} k \in Comp)\to((R \times_{t} S) ↾_{𝑡} (s \times k)) ↾_{𝑡} ((s \times k) ∖ x) \in Comp)))))$
215	181 214	eqeltrrd	$⊢ (((((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\land((s \in 𝒫 \{t \in ⋃ R \| ⟨t, 2^{nd} (y)⟩ \in x\} \land u \in R) \land (1^{st} (y) \in u \land u \subseteq s \land R ↾_{𝑡} s \in Comp))\land(k \in 𝒫 ⋃ S \land S ↾_{𝑡} k \in Comp)\to(R \times_{t} S) ↾_{𝑡} ((s \times k) ∖ x) \in Comp)))))$
216		imacmp	$⊢ ({2^{nd} ↾}_{(⋃ R \times ⋃ S)} \in ((R \times_{t} S) Cn S) \land (R \times_{t} S) ↾_{𝑡} ((s \times k) ∖ x) \in Comp) \to S ↾_{𝑡} ({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) [(s \times k) ∖ x] \in Comp$
217	173 215 216	syl2anc	$⊢ (((((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\land((s \in 𝒫 \{t \in ⋃ R \| ⟨t, 2^{nd} (y)⟩ \in x\} \land u \in R) \land (1^{st} (y) \in u \land u \subseteq s \land R ↾_{𝑡} s \in Comp))\land(k \in 𝒫 ⋃ S \land S ↾_{𝑡} k \in Comp)\toS ↾_{𝑡} ({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) [(s \times k) ∖ x] \in Comp)))))$
218	24	hauscmp	$⊢ (S \in Haus \land ({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) [(s \times k) ∖ x] \subseteq ⋃ S \land S ↾_{𝑡} ({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) [(s \times k) ∖ x] \in Comp) \to ({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) [(s \times k) ∖ x] \in Clsd (S)$
219	155 169 217 218	syl3anc	$⊢ (((((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\land((s \in 𝒫 \{t \in ⋃ R \| ⟨t, 2^{nd} (y)⟩ \in x\} \land u \in R) \land (1^{st} (y) \in u \land u \subseteq s \land R ↾_{𝑡} s \in Comp))\land(k \in 𝒫 ⋃ S \land S ↾_{𝑡} k \in Comp)\to({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) [(s \times k) ∖ x] \in Clsd (S))))))$
220	168	a1i	$⊢ (((((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\land((s \in 𝒫 \{t \in ⋃ R \| ⟨t, 2^{nd} (y)⟩ \in x\} \land u \in R) \land (1^{st} (y) \in u \land u \subseteq s \land R ↾_{𝑡} s \in Comp))\land(k \in 𝒫 ⋃ S \land S ↾_{𝑡} k \in Comp)\to({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) [(s \times k) ∖ x] \subseteq k)))))$
221	24	restcldi	$⊢ (k \subseteq ⋃ S \land ({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) [(s \times k) ∖ x] \in Clsd (S) \land ({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) [(s \times k) ∖ x] \subseteq k) \to ({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) [(s \times k) ∖ x] \in Clsd (S ↾_{𝑡} k)$
222	76 219 220 221	syl3anc	$⊢ (((((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\land((s \in 𝒫 \{t \in ⋃ R \| ⟨t, 2^{nd} (y)⟩ \in x\} \land u \in R) \land (1^{st} (y) \in u \land u \subseteq s \land R ↾_{𝑡} s \in Comp))\land(k \in 𝒫 ⋃ S \land S ↾_{𝑡} k \in Comp)\to({2^{nd} ↾}_{(⋃ R \times ⋃ S)}) [(s \times k) ∖ x] \in Clsd (S ↾_{𝑡} k))))))$
223	153 222	eqeltrrd	$⊢ (((((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\land((s \in 𝒫 \{t \in ⋃ R \| ⟨t, 2^{nd} (y)⟩ \in x\} \land u \in R) \land (1^{st} (y) \in u \land u \subseteq s \land R ↾_{𝑡} s \in Comp))\land(k \in 𝒫 ⋃ S \land S ↾_{𝑡} k \in Comp)\to⋃ (S ↾_{𝑡} k) ∖ (k \cap \{v \in ⋃ S \| s \times \{v\} \subseteq x\}) \in Clsd (S ↾_{𝑡} k))))))$
224		resttop	$⊢ (S \in Top \land k \in 𝒫 ⋃ S) \to S ↾_{𝑡} k \in Top$
225	148 185 224	syl2anc	$⊢ (((((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\land((s \in 𝒫 \{t \in ⋃ R \| ⟨t, 2^{nd} (y)⟩ \in x\} \land u \in R) \land (1^{st} (y) \in u \land u \subseteq s \land R ↾_{𝑡} s \in Comp))\land(k \in 𝒫 ⋃ S \land S ↾_{𝑡} k \in Comp)\toS ↾_{𝑡} k \in Top)))))$
226		inss1	$⊢ k \cap \{v \in ⋃ S \| s \times \{v\} \subseteq x\} \subseteq k$
227	226 150	sseqtrid	$⊢ (((((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\land((s \in 𝒫 \{t \in ⋃ R \| ⟨t, 2^{nd} (y)⟩ \in x\} \land u \in R) \land (1^{st} (y) \in u \land u \subseteq s \land R ↾_{𝑡} s \in Comp))\land(k \in 𝒫 ⋃ S \land S ↾_{𝑡} k \in Comp)\tok \cap \{v \in ⋃ S \| s \times \{v\} \subseteq x\} \subseteq ⋃ (S ↾_{𝑡} k))))))$
228		eqid	$⊢ ⋃ (S ↾_{𝑡} k) = ⋃ (S ↾_{𝑡} k)$
229	228	isopn2	$⊢ (S ↾_{𝑡} k \in Top \land k \cap \{v \in ⋃ S \| s \times \{v\} \subseteq x\} \subseteq ⋃ (S ↾_{𝑡} k)) \to (k \cap \{v \in ⋃ S \| s \times \{v\} \subseteq x\} \in (S ↾_{𝑡} k) \leftrightarrow ⋃ (S ↾_{𝑡} k) ∖ (k \cap \{v \in ⋃ S \| s \times \{v\} \subseteq x\}) \in Clsd (S ↾_{𝑡} k))$
230	225 227 229	syl2anc	$⊢ (((((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\land((s \in 𝒫 \{t \in ⋃ R \| ⟨t, 2^{nd} (y)⟩ \in x\} \land u \in R) \land (1^{st} (y) \in u \land u \subseteq s \land R ↾_{𝑡} s \in Comp))\land(k \in 𝒫 ⋃ S \land S ↾_{𝑡} k \in Comp)\to(k \cap \{v \in ⋃ S \| s \times \{v\} \subseteq x\} \in (S ↾_{𝑡} k) \leftrightarrow ⋃ (S ↾_{𝑡} k) ∖ (k \cap \{v \in ⋃ S \| s \times \{v\} \subseteq x\}) \in Clsd (S ↾_{𝑡} k)))))))$
231	223 230	mpbird	$⊢ (((((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\land((s \in 𝒫 \{t \in ⋃ R \| ⟨t, 2^{nd} (y)⟩ \in x\} \land u \in R) \land (1^{st} (y) \in u \land u \subseteq s \land R ↾_{𝑡} s \in Comp))\land(k \in 𝒫 ⋃ S \land S ↾_{𝑡} k \in Comp)\tok \cap \{v \in ⋃ S \| s \times \{v\} \subseteq x\} \in (S ↾_{𝑡} k))))))$
232	69 231	eqeltrid	$⊢ (((((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\land((s \in 𝒫 \{t \in ⋃ R \| ⟨t, 2^{nd} (y)⟩ \in x\} \land u \in R) \land (1^{st} (y) \in u \land u \subseteq s \land R ↾_{𝑡} s \in Comp))\land(k \in 𝒫 ⋃ S \land S ↾_{𝑡} k \in Comp)\to\{v \in ⋃ S \| s \times \{v\} \subseteq x\} \cap k \in (S ↾_{𝑡} k))))))$
233	232	expr	$⊢ (((((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\land((s \in 𝒫 \{t \in ⋃ R \| ⟨t, 2^{nd} (y)⟩ \in x\} \land u \in R) \land (1^{st} (y) \in u \land u \subseteq s \land R ↾_{𝑡} s \in Comp))\landk \in 𝒫 ⋃ S\to(S ↾_{𝑡} k \in Comp \to \{v \in ⋃ S \| s \times \{v\} \subseteq x\} \cap k \in (S ↾_{𝑡} k)))))))$
234	233	ralrimiva	$⊢ ((((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\land((s \in 𝒫 \{t \in ⋃ R \| ⟨t, 2^{nd} (y)⟩ \in x\} \land u \in R) \land (1^{st} (y) \in u \land u \subseteq s \land R ↾_{𝑡} s \in Comp))\to\forall k \in 𝒫 ⋃ S))))$
235	65 17	sylib	$⊢ ((((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\land((s \in 𝒫 \{t \in ⋃ R \| ⟨t, 2^{nd} (y)⟩ \in x\} \land u \in R) \land (1^{st} (y) \in u \land u \subseteq s \land R ↾_{𝑡} s \in Comp))\toS \in TopOn (⋃ S)))))$
236		elkgen	$⊢ S \in TopOn (⋃ S) \to (\{v \in ⋃ S \| s \times \{v\} \subseteq x\} \in 𝑘Gen (S) \leftrightarrow (\{v \in ⋃ S \| s \times \{v\} \subseteq x\} \subseteq ⋃ S \land \forall k \in 𝒫 ⋃ S (S ↾_{𝑡} k \in Comp \to \{v \in ⋃ S \| s \times \{v\} \subseteq x\} \cap k \in (S ↾_{𝑡} k))))$
237	235 236	syl	$⊢ ((((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\land((s \in 𝒫 \{t \in ⋃ R \| ⟨t, 2^{nd} (y)⟩ \in x\} \land u \in R) \land (1^{st} (y) \in u \land u \subseteq s \land R ↾_{𝑡} s \in Comp))\to(\{v \in ⋃ S \| s \times \{v\} \subseteq x\} \in 𝑘Gen (S) \leftrightarrow (\{v \in ⋃ S \| s \times \{v\} \subseteq x\} \subseteq ⋃ S \land \forall k \in 𝒫 ⋃ S))))))$
238	68 234 237	mpbir2and	$⊢ ((((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\land((s \in 𝒫 \{t \in ⋃ R \| ⟨t, 2^{nd} (y)⟩ \in x\} \land u \in R) \land (1^{st} (y) \in u \land u \subseteq s \land R ↾_{𝑡} s \in Comp))\to\{v \in ⋃ S \| s \times \{v\} \subseteq x\} \in 𝑘Gen (S)))))$
239	15	adantr	$⊢ ((((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\land((s \in 𝒫 \{t \in ⋃ R \| ⟨t, 2^{nd} (y)⟩ \in x\} \land u \in R) \land (1^{st} (y) \in u \land u \subseteq s \land R ↾_{𝑡} s \in Comp))\toS \in (ran 𝑘Gen \cap Haus)))))$
240	239 2	syl	$⊢ ((((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\land((s \in 𝒫 \{t \in ⋃ R \| ⟨t, 2^{nd} (y)⟩ \in x\} \land u \in R) \land (1^{st} (y) \in u \land u \subseteq s \land R ↾_{𝑡} s \in Comp))\toS \in ran 𝑘Gen))))$
241		kgenidm	$⊢ S \in ran 𝑘Gen \to 𝑘Gen (S) = S$
242	240 241	syl	$⊢ ((((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\land((s \in 𝒫 \{t \in ⋃ R \| ⟨t, 2^{nd} (y)⟩ \in x\} \land u \in R) \land (1^{st} (y) \in u \land u \subseteq s \land R ↾_{𝑡} s \in Comp))\to𝑘Gen (S) = S))))$
243	238 242	eleqtrd	$⊢ ((((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\land((s \in 𝒫 \{t \in ⋃ R \| ⟨t, 2^{nd} (y)⟩ \in x\} \land u \in R) \land (1^{st} (y) \in u \land u \subseteq s \land R ↾_{𝑡} s \in Comp))\to\{v \in ⋃ S \| s \times \{v\} \subseteq x\} \in S))))$
244		txopn	$⊢ ((R \in Top \land S \in Top) \land (u \in R \land \{v \in ⋃ S \| s \times \{v\} \subseteq x\} \in S)) \to u \times \{v \in ⋃ S \| s \times \{v\} \subseteq x\} \in (R \times_{t} S)$
245	64 65 66 243 244	syl22anc	$⊢ ((((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\land((s \in 𝒫 \{t \in ⋃ R \| ⟨t, 2^{nd} (y)⟩ \in x\} \land u \in R) \land (1^{st} (y) \in u \land u \subseteq s \land R ↾_{𝑡} s \in Comp))\tou \times \{v \in ⋃ S \| s \times \{v\} \subseteq x\} \in (R \times_{t} S)))))$
246	59	adantr	$⊢ ((((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\land((s \in 𝒫 \{t \in ⋃ R \| ⟨t, 2^{nd} (y)⟩ \in x\} \land u \in R) \land (1^{st} (y) \in u \land u \subseteq s \land R ↾_{𝑡} s \in Comp))\toy = ⟨1^{st} (y), 2^{nd} (y)⟩))))$
247		simprr1	$⊢ ((((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\land((s \in 𝒫 \{t \in ⋃ R \| ⟨t, 2^{nd} (y)⟩ \in x\} \land u \in R) \land (1^{st} (y) \in u \land u \subseteq s \land R ↾_{𝑡} s \in Comp))\to1^{st} (y) \in u))))$
248		sneq	$⊢ v = 2^{nd} (y) \to \{v\} = \{2^{nd} (y)\}$
249	248	xpeq2d	$⊢ v = 2^{nd} (y) \to s \times \{v\} = s \times \{2^{nd} (y)\}$
250	249	sseq1d	$⊢ v = 2^{nd} (y) \to (s \times \{v\} \subseteq x \leftrightarrow s \times \{2^{nd} (y)\} \subseteq x)$
251	34	adantr	$⊢ ((((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\land((s \in 𝒫 \{t \in ⋃ R \| ⟨t, 2^{nd} (y)⟩ \in x\} \land u \in R) \land (1^{st} (y) \in u \land u \subseteq s \land R ↾_{𝑡} s \in Comp))\to2^{nd} (y) \in ⋃ S))))$
252		relxp	$⊢ Rel (s \times \{2^{nd} (y)\})$
253	252	a1i	$⊢ ((((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\land((s \in 𝒫 \{t \in ⋃ R \| ⟨t, 2^{nd} (y)⟩ \in x\} \land u \in R) \land (1^{st} (y) \in u \land u \subseteq s \land R ↾_{𝑡} s \in Comp))\toRel (s \times \{2^{nd} (y)\})))))$
254		opelxp	$⊢ ⟨a, b⟩ \in (s \times \{2^{nd} (y)\}) \leftrightarrow (a \in s \land b \in \{2^{nd} (y)\})$
255	71	sselda	$⊢ (((((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\land((s \in 𝒫 \{t \in ⋃ R \| ⟨t, 2^{nd} (y)⟩ \in x\} \land u \in R) \land (1^{st} (y) \in u \land u \subseteq s \land R ↾_{𝑡} s \in Comp))\landa \in s\toa \in \{t \in ⋃ R \| ⟨t, 2^{nd} (y)⟩ \in x\})))))$
256		opeq1	$⊢ t = a \to ⟨t, 2^{nd} (y)⟩ = ⟨a, 2^{nd} (y)⟩$
257	256	eleq1d	$⊢ t = a \to (⟨t, 2^{nd} (y)⟩ \in x \leftrightarrow ⟨a, 2^{nd} (y)⟩ \in x)$
258	257	elrab	$⊢ a \in \{t \in ⋃ R \| ⟨t, 2^{nd} (y)⟩ \in x\} \leftrightarrow (a \in ⋃ R \land ⟨a, 2^{nd} (y)⟩ \in x)$
259	258	simprbi	$⊢ a \in \{t \in ⋃ R \| ⟨t, 2^{nd} (y)⟩ \in x\} \to ⟨a, 2^{nd} (y)⟩ \in x$
260	255 259	syl	$⊢ (((((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\land((s \in 𝒫 \{t \in ⋃ R \| ⟨t, 2^{nd} (y)⟩ \in x\} \land u \in R) \land (1^{st} (y) \in u \land u \subseteq s \land R ↾_{𝑡} s \in Comp))\landa \in s\to⟨a, 2^{nd} (y)⟩ \in x)))))$
261		elsni	$⊢ b \in \{2^{nd} (y)\} \to b = 2^{nd} (y)$
262	261	opeq2d	$⊢ b \in \{2^{nd} (y)\} \to ⟨a, b⟩ = ⟨a, 2^{nd} (y)⟩$
263	262	eleq1d	$⊢ b \in \{2^{nd} (y)\} \to (⟨a, b⟩ \in x \leftrightarrow ⟨a, 2^{nd} (y)⟩ \in x)$
264	260 263	syl5ibrcom	$⊢ (((((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\land((s \in 𝒫 \{t \in ⋃ R \| ⟨t, 2^{nd} (y)⟩ \in x\} \land u \in R) \land (1^{st} (y) \in u \land u \subseteq s \land R ↾_{𝑡} s \in Comp))\landa \in s\to(b \in \{2^{nd} (y)\} \to ⟨a, b⟩ \in x))))))$
265	264	expimpd	$⊢ ((((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\land((s \in 𝒫 \{t \in ⋃ R \| ⟨t, 2^{nd} (y)⟩ \in x\} \land u \in R) \land (1^{st} (y) \in u \land u \subseteq s \land R ↾_{𝑡} s \in Comp))\to((a \in s \land b \in \{2^{nd} (y)\}) \to ⟨a, b⟩ \in x)))))$
266	254 265	syl5bi	$⊢ ((((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\land((s \in 𝒫 \{t \in ⋃ R \| ⟨t, 2^{nd} (y)⟩ \in x\} \land u \in R) \land (1^{st} (y) \in u \land u \subseteq s \land R ↾_{𝑡} s \in Comp))\to(⟨a, b⟩ \in (s \times \{2^{nd} (y)\}) \to ⟨a, b⟩ \in x)))))$
267	253 266	relssdv	$⊢ ((((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\land((s \in 𝒫 \{t \in ⋃ R \| ⟨t, 2^{nd} (y)⟩ \in x\} \land u \in R) \land (1^{st} (y) \in u \land u \subseteq s \land R ↾_{𝑡} s \in Comp))\tos \times \{2^{nd} (y)\} \subseteq x))))$
268	250 251 267	elrabd	$⊢ ((((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\land((s \in 𝒫 \{t \in ⋃ R \| ⟨t, 2^{nd} (y)⟩ \in x\} \land u \in R) \land (1^{st} (y) \in u \land u \subseteq s \land R ↾_{𝑡} s \in Comp))\to2^{nd} (y) \in \{v \in ⋃ S \| s \times \{v\} \subseteq x\}))))$
269	247 268	opelxpd	$⊢ ((((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\land((s \in 𝒫 \{t \in ⋃ R \| ⟨t, 2^{nd} (y)⟩ \in x\} \land u \in R) \land (1^{st} (y) \in u \land u \subseteq s \land R ↾_{𝑡} s \in Comp))\to⟨1^{st} (y), 2^{nd} (y)⟩ \in (u \times \{v \in ⋃ S \| s \times \{v\} \subseteq x\})))))$
270	246 269	eqeltrd	$⊢ ((((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\land((s \in 𝒫 \{t \in ⋃ R \| ⟨t, 2^{nd} (y)⟩ \in x\} \land u \in R) \land (1^{st} (y) \in u \land u \subseteq s \land R ↾_{𝑡} s \in Comp))\toy \in (u \times \{v \in ⋃ S \| s \times \{v\} \subseteq x\})))))$
271		relxp	$⊢ Rel (u \times \{v \in ⋃ S \| s \times \{v\} \subseteq x\})$
272	271	a1i	$⊢ ((((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\land((s \in 𝒫 \{t \in ⋃ R \| ⟨t, 2^{nd} (y)⟩ \in x\} \land u \in R) \land (1^{st} (y) \in u \land u \subseteq s \land R ↾_{𝑡} s \in Comp))\toRel (u \times \{v \in ⋃ S \| s \times \{v\} \subseteq x\})))))$
273		opelxp	$⊢ ⟨a, b⟩ \in (u \times \{v \in ⋃ S \| s \times \{v\} \subseteq x\}) \leftrightarrow (a \in u \land b \in \{v \in ⋃ S \| s \times \{v\} \subseteq x\})$
274	126	elrab	$⊢ b \in \{v \in ⋃ S \| s \times \{v\} \subseteq x\} \leftrightarrow (b \in ⋃ S \land s \times \{b\} \subseteq x)$
275	274	simprbi	$⊢ b \in \{v \in ⋃ S \| s \times \{v\} \subseteq x\} \to s \times \{b\} \subseteq x$
276		simprr2	$⊢ ((((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\land((s \in 𝒫 \{t \in ⋃ R \| ⟨t, 2^{nd} (y)⟩ \in x\} \land u \in R) \land (1^{st} (y) \in u \land u \subseteq s \land R ↾_{𝑡} s \in Comp))\tou \subseteq s))))$
277	276	sselda	$⊢ (((((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\land((s \in 𝒫 \{t \in ⋃ R \| ⟨t, 2^{nd} (y)⟩ \in x\} \land u \in R) \land (1^{st} (y) \in u \land u \subseteq s \land R ↾_{𝑡} s \in Comp))\landa \in u\toa \in s)))))$
278		vsnid	$⊢ b \in \{b\}$
279		opelxpi	$⊢ (a \in s \land b \in \{b\}) \to ⟨a, b⟩ \in (s \times \{b\})$
280	277 278 279	sylancl	$⊢ (((((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\land((s \in 𝒫 \{t \in ⋃ R \| ⟨t, 2^{nd} (y)⟩ \in x\} \land u \in R) \land (1^{st} (y) \in u \land u \subseteq s \land R ↾_{𝑡} s \in Comp))\landa \in u\to⟨a, b⟩ \in (s \times \{b\}))))))$
281		ssel	$⊢ s \times \{b\} \subseteq x \to (⟨a, b⟩ \in (s \times \{b\}) \to ⟨a, b⟩ \in x)$
282	275 280 281	syl2imc	$⊢ (((((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\land((s \in 𝒫 \{t \in ⋃ R \| ⟨t, 2^{nd} (y)⟩ \in x\} \land u \in R) \land (1^{st} (y) \in u \land u \subseteq s \land R ↾_{𝑡} s \in Comp))\landa \in u\to(b \in \{v \in ⋃ S \| s \times \{v\} \subseteq x\} \to ⟨a, b⟩ \in x))))))$
283	282	expimpd	$⊢ ((((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\land((s \in 𝒫 \{t \in ⋃ R \| ⟨t, 2^{nd} (y)⟩ \in x\} \land u \in R) \land (1^{st} (y) \in u \land u \subseteq s \land R ↾_{𝑡} s \in Comp))\to((a \in u \land b \in \{v \in ⋃ S \| s \times \{v\} \subseteq x\}) \to ⟨a, b⟩ \in x)))))$
284	273 283	syl5bi	$⊢ ((((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\land((s \in 𝒫 \{t \in ⋃ R \| ⟨t, 2^{nd} (y)⟩ \in x\} \land u \in R) \land (1^{st} (y) \in u \land u \subseteq s \land R ↾_{𝑡} s \in Comp))\to(⟨a, b⟩ \in (u \times \{v \in ⋃ S \| s \times \{v\} \subseteq x\}) \to ⟨a, b⟩ \in x)))))$
285	272 284	relssdv	$⊢ ((((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\land((s \in 𝒫 \{t \in ⋃ R \| ⟨t, 2^{nd} (y)⟩ \in x\} \land u \in R) \land (1^{st} (y) \in u \land u \subseteq s \land R ↾_{𝑡} s \in Comp))\tou \times \{v \in ⋃ S \| s \times \{v\} \subseteq x\} \subseteq x))))$
286		eleq2	$⊢ t = u \times \{v \in ⋃ S \| s \times \{v\} \subseteq x\} \to (y \in t \leftrightarrow y \in (u \times \{v \in ⋃ S \| s \times \{v\} \subseteq x\}))$
287		sseq1	$⊢ t = u \times \{v \in ⋃ S \| s \times \{v\} \subseteq x\} \to (t \subseteq x \leftrightarrow u \times \{v \in ⋃ S \| s \times \{v\} \subseteq x\} \subseteq x)$
288	286 287	anbi12d	$⊢ t = u \times \{v \in ⋃ S \| s \times \{v\} \subseteq x\} \to ((y \in t \land t \subseteq x) \leftrightarrow (y \in (u \times \{v \in ⋃ S \| s \times \{v\} \subseteq x\}) \land u \times \{v \in ⋃ S \| s \times \{v\} \subseteq x\} \subseteq x))$
289	288	rspcev	$⊢ (u \times \{v \in ⋃ S \| s \times \{v\} \subseteq x\} \in (R \times_{t} S) \land (y \in (u \times \{v \in ⋃ S \| s \times \{v\} \subseteq x\}) \land u \times \{v \in ⋃ S \| s \times \{v\} \subseteq x\} \subseteq x)) \to \exists t \in (R \times_{t} S) (y \in t \land t \subseteq x)$
290	245 270 285 289	syl12anc	$⊢ ((((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\land((s \in 𝒫 \{t \in ⋃ R \| ⟨t, 2^{nd} (y)⟩ \in x\} \land u \in R) \land (1^{st} (y) \in u \land u \subseteq s \land R ↾_{𝑡} s \in Comp))\to\exists t \in (R \times_{t} S)))))$
291	290	expr	$⊢ ((((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\land(s \in 𝒫 \{t \in ⋃ R \| ⟨t, 2^{nd} (y)⟩ \in x\} \land u \in R)\to((1^{st} (y) \in u \land u \subseteq s \land R ↾_{𝑡} s \in Comp) \to \exists t \in (R \times_{t} S))))))$
292	291	rexlimdvva	$⊢ (((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\to(\exists s \in 𝒫 \{t \in ⋃ R \| ⟨t, 2^{nd} (y)⟩ \in x\} \to \exists t \in (R \times_{t} S)))))$
293	63 292	mpd	$⊢ (((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\landy \in x\to\exists t \in (R \times_{t} S))))$
294	293	ralrimiva	$⊢ ((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\to\forall y \in x))$
295	6	adantr	$⊢ ((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\toR \times_{t} S \in Top))$
296		eltop2	$⊢ R \times_{t} S \in Top \to (x \in (R \times_{t} S) \leftrightarrow \forall y \in x \exists t \in (R \times_{t} S) (y \in t \land t \subseteq x))$
297	295 296	syl	$⊢ ((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\to(x \in (R \times_{t} S) \leftrightarrow \forall y \in x)))$
298	294 297	mpbird	$⊢ ((R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\landx \in 𝑘Gen (R \times_{t} S)\tox \in (R \times_{t} S)))$
299	298	ex	$⊢ (R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\to(x \in 𝑘Gen (R \times_{t} S) \to x \in (R \times_{t} S)))$
300	299	ssrdv	$⊢ (R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\to𝑘Gen (R \times_{t} S) \subseteq R \times_{t} S)$
301		iskgen2	$⊢ R \times_{t} S \in ran 𝑘Gen \leftrightarrow (R \times_{t} S \in Top \land 𝑘Gen (R \times_{t} S) \subseteq R \times_{t} S)$
302	6 300 301	sylanbrc	$⊢ (R \in N-LocallyComp\landS \in (ran 𝑘Gen \cap Haus)\toR \times_{t} S \in ran 𝑘Gen)$

Metamath Proof Explorer

Theorem txkgen

Proof