Theorem txkgen 23714

Description: The topological product of a locally compact space and a compactly generated Hausdorff space is compactly generated. (The condition on 𝑆 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.)

Assertion

Ref	Expression
txkgen	⊢ ((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) → (𝑅 ×t 𝑆) ∈ ran 𝑘Gen)

Proof of Theorem txkgen

Dummy variables 𝑎 𝑏 𝑘 𝑠 𝑡 𝑢 𝑥 𝑦 𝑣 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		nllytop 23535	. . 3 ⊢ (𝑅 ∈ 𝑛-Locally Comp → 𝑅 ∈ Top)
2		elinel1 4155	. . . 4 ⊢ (𝑆 ∈ (ran 𝑘Gen ∩ Haus) → 𝑆 ∈ ran 𝑘Gen)
3		kgentop 23604	. . . 4 ⊢ (𝑆 ∈ ran 𝑘Gen → 𝑆 ∈ Top)
4	2, 3	syl 17	. . 3 ⊢ (𝑆 ∈ (ran 𝑘Gen ∩ Haus) → 𝑆 ∈ Top)
5		txtop 23631	. . 3 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑅 ×t 𝑆) ∈ Top)
6	1, 4, 5	syl2an 605	. 2 ⊢ ((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) → (𝑅 ×t 𝑆) ∈ Top)
7		simplll 784	. . . . . . . 8 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → 𝑅 ∈ 𝑛-Locally Comp)
8		eqid 2764	. . . . . . . . . 10 ⊢ (𝑡 ∈ ∪ 𝑅 ↦ ⟨𝑡, (2nd ‘𝑦)⟩) = (𝑡 ∈ ∪ 𝑅 ↦ ⟨𝑡, (2nd ‘𝑦)⟩)
9	8	mptpreima 6227	. . . . . . . . 9 ⊢ (◡(𝑡 ∈ ∪ 𝑅 ↦ ⟨𝑡, (2nd ‘𝑦)⟩) “ 𝑥) = {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥}
10	1	ad3antrrr 740	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → 𝑅 ∈ Top)
11		toptopon2 22980	. . . . . . . . . . . . . 14 ⊢ (𝑅 ∈ Top ↔ 𝑅 ∈ (TopOn‘∪ 𝑅))
12	10, 11	sylib 220	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → 𝑅 ∈ (TopOn‘∪ 𝑅))
13		idcn 23319	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ (TopOn‘∪ 𝑅) → ( I ↾ ∪ 𝑅) ∈ (𝑅 Cn 𝑅))
14	12, 13	syl 17	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → ( I ↾ ∪ 𝑅) ∈ (𝑅 Cn 𝑅))
15		simpllr 785	. . . . . . . . . . . . . . 15 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → 𝑆 ∈ (ran 𝑘Gen ∩ Haus))
16	15, 4	syl 17	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → 𝑆 ∈ Top)
17		toptopon2 22980	. . . . . . . . . . . . . 14 ⊢ (𝑆 ∈ Top ↔ 𝑆 ∈ (TopOn‘∪ 𝑆))
18	16, 17	sylib 220	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → 𝑆 ∈ (TopOn‘∪ 𝑆))
19		simpr 488	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ 𝑥)
20		simplr 778	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆)))
21		elunii 4872	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) → 𝑦 ∈ ∪ (𝑘Gen‘(𝑅 ×t 𝑆)))
22	19, 20, 21	syl2anc 593	. . . . . . . . . . . . . . 15 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ ∪ (𝑘Gen‘(𝑅 ×t 𝑆)))
23		eqid 2764	. . . . . . . . . . . . . . . . . 18 ⊢ ∪ 𝑅 = ∪ 𝑅
24		eqid 2764	. . . . . . . . . . . . . . . . . 18 ⊢ ∪ 𝑆 = ∪ 𝑆
25	23, 24	txuni 23654	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (∪ 𝑅 × ∪ 𝑆) = ∪ (𝑅 ×t 𝑆))
26	10, 16, 25	syl2anc 593	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → (∪ 𝑅 × ∪ 𝑆) = ∪ (𝑅 ×t 𝑆))
27	10, 16, 5	syl2anc 593	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → (𝑅 ×t 𝑆) ∈ Top)
28		eqid 2764	. . . . . . . . . . . . . . . . . 18 ⊢ ∪ (𝑅 ×t 𝑆) = ∪ (𝑅 ×t 𝑆)
29	28	kgenuni 23601	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 ×t 𝑆) ∈ Top → ∪ (𝑅 ×t 𝑆) = ∪ (𝑘Gen‘(𝑅 ×t 𝑆)))
30	27, 29	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → ∪ (𝑅 ×t 𝑆) = ∪ (𝑘Gen‘(𝑅 ×t 𝑆)))
31	26, 30	eqtrd 2799	. . . . . . . . . . . . . . 15 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → (∪ 𝑅 × ∪ 𝑆) = ∪ (𝑘Gen‘(𝑅 ×t 𝑆)))
32	22, 31	eleqtrrd 2867	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ (∪ 𝑅 × ∪ 𝑆))
33		xp2nd 8005	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ (∪ 𝑅 × ∪ 𝑆) → (2nd ‘𝑦) ∈ ∪ 𝑆)
34	32, 33	syl 17	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → (2nd ‘𝑦) ∈ ∪ 𝑆)
35		cnconst2 23345	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ (TopOn‘∪ 𝑅) ∧ 𝑆 ∈ (TopOn‘∪ 𝑆) ∧ (2nd ‘𝑦) ∈ ∪ 𝑆) → (∪ 𝑅 × {(2nd ‘𝑦)}) ∈ (𝑅 Cn 𝑆))
36	12, 18, 34, 35	syl3anc 1392	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → (∪ 𝑅 × {(2nd ‘𝑦)}) ∈ (𝑅 Cn 𝑆))
37		fvresi 7159	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 ∈ ∪ 𝑅 → (( I ↾ ∪ 𝑅)‘𝑡) = 𝑡)
38		fvex 6882	. . . . . . . . . . . . . . . . 17 ⊢ (2nd ‘𝑦) ∈ V
39	38	fvconst2 7190	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 ∈ ∪ 𝑅 → ((∪ 𝑅 × {(2nd ‘𝑦)})‘𝑡) = (2nd ‘𝑦))
40	37, 39	opeq12d 4841	. . . . . . . . . . . . . . 15 ⊢ (𝑡 ∈ ∪ 𝑅 → ⟨(( I ↾ ∪ 𝑅)‘𝑡), ((∪ 𝑅 × {(2nd ‘𝑦)})‘𝑡)⟩ = ⟨𝑡, (2nd ‘𝑦)⟩)
41	40	mpteq2ia 5197	. . . . . . . . . . . . . 14 ⊢ (𝑡 ∈ ∪ 𝑅 ↦ ⟨(( I ↾ ∪ 𝑅)‘𝑡), ((∪ 𝑅 × {(2nd ‘𝑦)})‘𝑡)⟩) = (𝑡 ∈ ∪ 𝑅 ↦ ⟨𝑡, (2nd ‘𝑦)⟩)
42	41	eqcomi 2773	. . . . . . . . . . . . 13 ⊢ (𝑡 ∈ ∪ 𝑅 ↦ ⟨𝑡, (2nd ‘𝑦)⟩) = (𝑡 ∈ ∪ 𝑅 ↦ ⟨(( I ↾ ∪ 𝑅)‘𝑡), ((∪ 𝑅 × {(2nd ‘𝑦)})‘𝑡)⟩)
43	23, 42	txcnmpt 23686	. . . . . . . . . . . 12 ⊢ ((( I ↾ ∪ 𝑅) ∈ (𝑅 Cn 𝑅) ∧ (∪ 𝑅 × {(2nd ‘𝑦)}) ∈ (𝑅 Cn 𝑆)) → (𝑡 ∈ ∪ 𝑅 ↦ ⟨𝑡, (2nd ‘𝑦)⟩) ∈ (𝑅 Cn (𝑅 ×t 𝑆)))
44	14, 36, 43	syl2anc 593	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → (𝑡 ∈ ∪ 𝑅 ↦ ⟨𝑡, (2nd ‘𝑦)⟩) ∈ (𝑅 Cn (𝑅 ×t 𝑆)))
45		llycmpkgen 23614	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ 𝑛-Locally Comp → 𝑅 ∈ ran 𝑘Gen)
46	45	ad3antrrr 740	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → 𝑅 ∈ ran 𝑘Gen)
47	6	ad2antrr 736	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → (𝑅 ×t 𝑆) ∈ Top)
48		kgencn3 23620	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ ran 𝑘Gen ∧ (𝑅 ×t 𝑆) ∈ Top) → (𝑅 Cn (𝑅 ×t 𝑆)) = (𝑅 Cn (𝑘Gen‘(𝑅 ×t 𝑆))))
49	46, 47, 48	syl2anc 593	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → (𝑅 Cn (𝑅 ×t 𝑆)) = (𝑅 Cn (𝑘Gen‘(𝑅 ×t 𝑆))))
50	44, 49	eleqtrd 2866	. . . . . . . . . 10 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → (𝑡 ∈ ∪ 𝑅 ↦ ⟨𝑡, (2nd ‘𝑦)⟩) ∈ (𝑅 Cn (𝑘Gen‘(𝑅 ×t 𝑆))))
51		cnima 23327	. . . . . . . . . 10 ⊢ (((𝑡 ∈ ∪ 𝑅 ↦ ⟨𝑡, (2nd ‘𝑦)⟩) ∈ (𝑅 Cn (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) → (◡(𝑡 ∈ ∪ 𝑅 ↦ ⟨𝑡, (2nd ‘𝑦)⟩) “ 𝑥) ∈ 𝑅)
52	50, 20, 51	syl2anc 593	. . . . . . . . 9 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → (◡(𝑡 ∈ ∪ 𝑅 ↦ ⟨𝑡, (2nd ‘𝑦)⟩) “ 𝑥) ∈ 𝑅)
53	9, 52	eqeltrrid 2869	. . . . . . . 8 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∈ 𝑅)
54		opeq1 4833	. . . . . . . . . 10 ⊢ (𝑡 = (1st ‘𝑦) → ⟨𝑡, (2nd ‘𝑦)⟩ = ⟨(1st ‘𝑦), (2nd ‘𝑦)⟩)
55	54	eleq1d 2849	. . . . . . . . 9 ⊢ (𝑡 = (1st ‘𝑦) → (⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥 ↔ ⟨(1st ‘𝑦), (2nd ‘𝑦)⟩ ∈ 𝑥))
56		xp1st 8004	. . . . . . . . . 10 ⊢ (𝑦 ∈ (∪ 𝑅 × ∪ 𝑆) → (1st ‘𝑦) ∈ ∪ 𝑅)
57	32, 56	syl 17	. . . . . . . . 9 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → (1st ‘𝑦) ∈ ∪ 𝑅)
58		1st2nd2 8011	. . . . . . . . . . 11 ⊢ (𝑦 ∈ (∪ 𝑅 × ∪ 𝑆) → 𝑦 = ⟨(1st ‘𝑦), (2nd ‘𝑦)⟩)
59	32, 58	syl 17	. . . . . . . . . 10 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → 𝑦 = ⟨(1st ‘𝑦), (2nd ‘𝑦)⟩)
60	59, 19	eqeltrrd 2865	. . . . . . . . 9 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → ⟨(1st ‘𝑦), (2nd ‘𝑦)⟩ ∈ 𝑥)
61	55, 57, 60	elrabd 3654	. . . . . . . 8 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → (1st ‘𝑦) ∈ {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥})
62		nlly2i 23538	. . . . . . . 8 ⊢ ((𝑅 ∈ 𝑛-Locally Comp ∧ {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∈ 𝑅 ∧ (1st ‘𝑦) ∈ {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥}) → ∃𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥}∃𝑢 ∈ 𝑅 ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))
63	7, 53, 61, 62	syl3anc 1392	. . . . . . 7 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → ∃𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥}∃𝑢 ∈ 𝑅 ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))
64	10	adantr 484	. . . . . . . . . . 11 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → 𝑅 ∈ Top)
65	16	adantr 484	. . . . . . . . . . 11 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → 𝑆 ∈ Top)
66		simprlr 789	. . . . . . . . . . 11 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → 𝑢 ∈ 𝑅)
67		ssrab2 4035	. . . . . . . . . . . . . 14 ⊢ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ⊆ ∪ 𝑆
68	67	a1i 11	. . . . . . . . . . . . 13 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ⊆ ∪ 𝑆)
69		incom 4163	. . . . . . . . . . . . . . . 16 ⊢ ({𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ∩ 𝑘) = (𝑘 ∩ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})
70		simprll 788	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → 𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥})
71	70	elpwid 4566	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → 𝑠 ⊆ {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥})
72		ssrab2 4035	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ⊆ ∪ 𝑅
73	71, 72	sstrdi 3950	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → 𝑠 ⊆ ∪ 𝑅)
74	73	adantr 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → 𝑠 ⊆ ∪ 𝑅)
75		elpwi 4564	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 ∈ 𝒫 ∪ 𝑆 → 𝑘 ⊆ ∪ 𝑆)
76	75	ad2antrl 738	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → 𝑘 ⊆ ∪ 𝑆)
77		eldif 3916	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑡 ∈ ((𝑠 × 𝑘) ∖ 𝑥) ↔ (𝑡 ∈ (𝑠 × 𝑘) ∧ ¬ 𝑡 ∈ 𝑥))
78	77	anbi1i 633	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑡 ∈ ((𝑠 × 𝑘) ∖ 𝑥) ∧ ((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘𝑡) = 𝑏) ↔ ((𝑡 ∈ (𝑠 × 𝑘) ∧ ¬ 𝑡 ∈ 𝑥) ∧ ((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘𝑡) = 𝑏))
79		anass 472	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑡 ∈ (𝑠 × 𝑘) ∧ ¬ 𝑡 ∈ 𝑥) ∧ ((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘𝑡) = 𝑏) ↔ (𝑡 ∈ (𝑠 × 𝑘) ∧ (¬ 𝑡 ∈ 𝑥 ∧ ((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘𝑡) = 𝑏)))
80	78, 79	bitri 277	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑡 ∈ ((𝑠 × 𝑘) ∖ 𝑥) ∧ ((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘𝑡) = 𝑏) ↔ (𝑡 ∈ (𝑠 × 𝑘) ∧ (¬ 𝑡 ∈ 𝑥 ∧ ((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘𝑡) = 𝑏)))
81	80	rexbii2 3107	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (∃𝑡 ∈ ((𝑠 × 𝑘) ∖ 𝑥)((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘𝑡) = 𝑏 ↔ ∃𝑡 ∈ (𝑠 × 𝑘)(¬ 𝑡 ∈ 𝑥 ∧ ((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘𝑡) = 𝑏))
82		ancom 464	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((¬ 𝑡 ∈ 𝑥 ∧ ((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘𝑡) = 𝑏) ↔ (((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘𝑡) = 𝑏 ∧ ¬ 𝑡 ∈ 𝑥))
83		fveqeq2 6878	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑡 = ⟨𝑎, 𝑢⟩ → (((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘𝑡) = 𝑏 ↔ ((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘⟨𝑎, 𝑢⟩) = 𝑏))
84		eleq1 2852	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑡 = ⟨𝑎, 𝑢⟩ → (𝑡 ∈ 𝑥 ↔ ⟨𝑎, 𝑢⟩ ∈ 𝑥))
85	84	notbid 320	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑡 = ⟨𝑎, 𝑢⟩ → (¬ 𝑡 ∈ 𝑥 ↔ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥))
86	83, 85	anbi12d 641	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑡 = ⟨𝑎, 𝑢⟩ → ((((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘𝑡) = 𝑏 ∧ ¬ 𝑡 ∈ 𝑥) ↔ (((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘⟨𝑎, 𝑢⟩) = 𝑏 ∧ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥)))
87	82, 86	bitrid 285	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑡 = ⟨𝑎, 𝑢⟩ → ((¬ 𝑡 ∈ 𝑥 ∧ ((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘𝑡) = 𝑏) ↔ (((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘⟨𝑎, 𝑢⟩) = 𝑏 ∧ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥)))
88	87	rexxp 5816	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (∃𝑡 ∈ (𝑠 × 𝑘)(¬ 𝑡 ∈ 𝑥 ∧ ((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘𝑡) = 𝑏) ↔ ∃𝑎 ∈ 𝑠 ∃𝑢 ∈ 𝑘 (((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘⟨𝑎, 𝑢⟩) = 𝑏 ∧ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥))
89	81, 88	bitri 277	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (∃𝑡 ∈ ((𝑠 × 𝑘) ∖ 𝑥)((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘𝑡) = 𝑏 ↔ ∃𝑎 ∈ 𝑠 ∃𝑢 ∈ 𝑘 (((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘⟨𝑎, 𝑢⟩) = 𝑏 ∧ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥))
90		simpl 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) → 𝑠 ⊆ ∪ 𝑅)
91	90	sselda 3938	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) ∧ 𝑎 ∈ 𝑠) → 𝑎 ∈ ∪ 𝑅)
92	91	adantr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) ∧ 𝑎 ∈ 𝑠) ∧ 𝑢 ∈ 𝑘) → 𝑎 ∈ ∪ 𝑅)
93		simplr 778	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) ∧ 𝑎 ∈ 𝑠) → 𝑘 ⊆ ∪ 𝑆)
94	93	sselda 3938	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) ∧ 𝑎 ∈ 𝑠) ∧ 𝑢 ∈ 𝑘) → 𝑢 ∈ ∪ 𝑆)
95	92, 94	opelxpd 5688	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) ∧ 𝑎 ∈ 𝑠) ∧ 𝑢 ∈ 𝑘) → ⟨𝑎, 𝑢⟩ ∈ (∪ 𝑅 × ∪ 𝑆))
96	95	fvresd 6889	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) ∧ 𝑎 ∈ 𝑠) ∧ 𝑢 ∈ 𝑘) → ((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘⟨𝑎, 𝑢⟩) = (2nd ‘⟨𝑎, 𝑢⟩))
97		vex 3460	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ 𝑎 ∈ V
98		vex 3460	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ 𝑢 ∈ V
99	97, 98	op2nd 7981	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (2nd ‘⟨𝑎, 𝑢⟩) = 𝑢
100	96, 99	eqtrdi 2815	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) ∧ 𝑎 ∈ 𝑠) ∧ 𝑢 ∈ 𝑘) → ((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘⟨𝑎, 𝑢⟩) = 𝑢)
101	100	eqeq1d 2766	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) ∧ 𝑎 ∈ 𝑠) ∧ 𝑢 ∈ 𝑘) → (((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘⟨𝑎, 𝑢⟩) = 𝑏 ↔ 𝑢 = 𝑏))
102	101	anbi1d 640	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) ∧ 𝑎 ∈ 𝑠) ∧ 𝑢 ∈ 𝑘) → ((((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘⟨𝑎, 𝑢⟩) = 𝑏 ∧ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥) ↔ (𝑢 = 𝑏 ∧ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥)))
103	102	rexbidva 3186	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) ∧ 𝑎 ∈ 𝑠) → (∃𝑢 ∈ 𝑘 (((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘⟨𝑎, 𝑢⟩) = 𝑏 ∧ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥) ↔ ∃𝑢 ∈ 𝑘 (𝑢 = 𝑏 ∧ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥)))
104		opeq2 4834	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑢 = 𝑏 → ⟨𝑎, 𝑢⟩ = ⟨𝑎, 𝑏⟩)
105	104	eleq1d 2849	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑢 = 𝑏 → (⟨𝑎, 𝑢⟩ ∈ 𝑥 ↔ ⟨𝑎, 𝑏⟩ ∈ 𝑥))
106	105	notbid 320	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑢 = 𝑏 → (¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥 ↔ ¬ ⟨𝑎, 𝑏⟩ ∈ 𝑥))
107	106	ceqsrexbv 3617	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (∃𝑢 ∈ 𝑘 (𝑢 = 𝑏 ∧ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥) ↔ (𝑏 ∈ 𝑘 ∧ ¬ ⟨𝑎, 𝑏⟩ ∈ 𝑥))
108	103, 107	bitrdi 289	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) ∧ 𝑎 ∈ 𝑠) → (∃𝑢 ∈ 𝑘 (((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘⟨𝑎, 𝑢⟩) = 𝑏 ∧ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥) ↔ (𝑏 ∈ 𝑘 ∧ ¬ ⟨𝑎, 𝑏⟩ ∈ 𝑥)))
109	108	rexbidva 3186	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) → (∃𝑎 ∈ 𝑠 ∃𝑢 ∈ 𝑘 (((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘⟨𝑎, 𝑢⟩) = 𝑏 ∧ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥) ↔ ∃𝑎 ∈ 𝑠 (𝑏 ∈ 𝑘 ∧ ¬ ⟨𝑎, 𝑏⟩ ∈ 𝑥)))
110		r19.42v 3196	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (∃𝑎 ∈ 𝑠 (𝑏 ∈ 𝑘 ∧ ¬ ⟨𝑎, 𝑏⟩ ∈ 𝑥) ↔ (𝑏 ∈ 𝑘 ∧ ∃𝑎 ∈ 𝑠 ¬ ⟨𝑎, 𝑏⟩ ∈ 𝑥))
111	109, 110	bitrdi 289	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) → (∃𝑎 ∈ 𝑠 ∃𝑢 ∈ 𝑘 (((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘⟨𝑎, 𝑢⟩) = 𝑏 ∧ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥) ↔ (𝑏 ∈ 𝑘 ∧ ∃𝑎 ∈ 𝑠 ¬ ⟨𝑎, 𝑏⟩ ∈ 𝑥)))
112	89, 111	bitrid 285	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) → (∃𝑡 ∈ ((𝑠 × 𝑘) ∖ 𝑥)((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘𝑡) = 𝑏 ↔ (𝑏 ∈ 𝑘 ∧ ∃𝑎 ∈ 𝑠 ¬ ⟨𝑎, 𝑏⟩ ∈ 𝑥)))
113		f2ndres 7997	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (2nd ↾ (∪ 𝑅 × ∪ 𝑆)):(∪ 𝑅 × ∪ 𝑆)⟶∪ 𝑆
114		ffn 6693	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)):(∪ 𝑅 × ∪ 𝑆)⟶∪ 𝑆 → (2nd ↾ (∪ 𝑅 × ∪ 𝑆)) Fn (∪ 𝑅 × ∪ 𝑆))
115	113, 114	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (2nd ↾ (∪ 𝑅 × ∪ 𝑆)) Fn (∪ 𝑅 × ∪ 𝑆)
116		difss 4091	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑠 × 𝑘) ∖ 𝑥) ⊆ (𝑠 × 𝑘)
117		xpss12 5664	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) → (𝑠 × 𝑘) ⊆ (∪ 𝑅 × ∪ 𝑆))
118	116, 117	sstrid 3949	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) → ((𝑠 × 𝑘) ∖ 𝑥) ⊆ (∪ 𝑅 × ∪ 𝑆))
119		fvelimab 6941	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) Fn (∪ 𝑅 × ∪ 𝑆) ∧ ((𝑠 × 𝑘) ∖ 𝑥) ⊆ (∪ 𝑅 × ∪ 𝑆)) → (𝑏 ∈ ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ↔ ∃𝑡 ∈ ((𝑠 × 𝑘) ∖ 𝑥)((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘𝑡) = 𝑏))
120	115, 118, 119	sylancr 596	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) → (𝑏 ∈ ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ↔ ∃𝑡 ∈ ((𝑠 × 𝑘) ∖ 𝑥)((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘𝑡) = 𝑏))
121		eldif 3916	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑏 ∈ (𝑘 ∖ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ↔ (𝑏 ∈ 𝑘 ∧ ¬ 𝑏 ∈ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}))
122		simpr 488	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) → 𝑘 ⊆ ∪ 𝑆)
123	122	sselda 3938	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) ∧ 𝑏 ∈ 𝑘) → 𝑏 ∈ ∪ 𝑆)
124		sneq 4594	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑣 = 𝑏 → {𝑣} = {𝑏})
125	124	xpeq2d 5679	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑣 = 𝑏 → (𝑠 × {𝑣}) = (𝑠 × {𝑏}))
126	125	sseq1d 3969	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑣 = 𝑏 → ((𝑠 × {𝑣}) ⊆ 𝑥 ↔ (𝑠 × {𝑏}) ⊆ 𝑥))
127		dfss3 3927	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑠 × {𝑏}) ⊆ 𝑥 ↔ ∀𝑘 ∈ (𝑠 × {𝑏})𝑘 ∈ 𝑥)
128		eleq1 2852	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑘 = ⟨𝑎, 𝑡⟩ → (𝑘 ∈ 𝑥 ↔ ⟨𝑎, 𝑡⟩ ∈ 𝑥))
129	128	ralxp 5815	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (∀𝑘 ∈ (𝑠 × {𝑏})𝑘 ∈ 𝑥 ↔ ∀𝑎 ∈ 𝑠 ∀𝑡 ∈ {𝑏}⟨𝑎, 𝑡⟩ ∈ 𝑥)
130		vex 3460	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ 𝑏 ∈ V
131		opeq2 4834	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑡 = 𝑏 → ⟨𝑎, 𝑡⟩ = ⟨𝑎, 𝑏⟩)
132	131	eleq1d 2849	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑡 = 𝑏 → (⟨𝑎, 𝑡⟩ ∈ 𝑥 ↔ ⟨𝑎, 𝑏⟩ ∈ 𝑥))
133	130, 132	ralsn 4642	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (∀𝑡 ∈ {𝑏}⟨𝑎, 𝑡⟩ ∈ 𝑥 ↔ ⟨𝑎, 𝑏⟩ ∈ 𝑥)
134	133	ralbii 3110	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (∀𝑎 ∈ 𝑠 ∀𝑡 ∈ {𝑏}⟨𝑎, 𝑡⟩ ∈ 𝑥 ↔ ∀𝑎 ∈ 𝑠 ⟨𝑎, 𝑏⟩ ∈ 𝑥)
135	127, 129, 134	3bitri 299	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑠 × {𝑏}) ⊆ 𝑥 ↔ ∀𝑎 ∈ 𝑠 ⟨𝑎, 𝑏⟩ ∈ 𝑥)
136	126, 135	bitrdi 289	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑣 = 𝑏 → ((𝑠 × {𝑣}) ⊆ 𝑥 ↔ ∀𝑎 ∈ 𝑠 ⟨𝑎, 𝑏⟩ ∈ 𝑥))
137	136	elrab3 3653	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑏 ∈ ∪ 𝑆 → (𝑏 ∈ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ↔ ∀𝑎 ∈ 𝑠 ⟨𝑎, 𝑏⟩ ∈ 𝑥))
138	123, 137	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) ∧ 𝑏 ∈ 𝑘) → (𝑏 ∈ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ↔ ∀𝑎 ∈ 𝑠 ⟨𝑎, 𝑏⟩ ∈ 𝑥))
139	138	notbid 320	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) ∧ 𝑏 ∈ 𝑘) → (¬ 𝑏 ∈ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ↔ ¬ ∀𝑎 ∈ 𝑠 ⟨𝑎, 𝑏⟩ ∈ 𝑥))
140		rexnal 3116	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (∃𝑎 ∈ 𝑠 ¬ ⟨𝑎, 𝑏⟩ ∈ 𝑥 ↔ ¬ ∀𝑎 ∈ 𝑠 ⟨𝑎, 𝑏⟩ ∈ 𝑥)
141	139, 140	bitr4di 291	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) ∧ 𝑏 ∈ 𝑘) → (¬ 𝑏 ∈ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ↔ ∃𝑎 ∈ 𝑠 ¬ ⟨𝑎, 𝑏⟩ ∈ 𝑥))
142	141	pm5.32da 587	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) → ((𝑏 ∈ 𝑘 ∧ ¬ 𝑏 ∈ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ↔ (𝑏 ∈ 𝑘 ∧ ∃𝑎 ∈ 𝑠 ¬ ⟨𝑎, 𝑏⟩ ∈ 𝑥)))
143	121, 142	bitrid 285	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) → (𝑏 ∈ (𝑘 ∖ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ↔ (𝑏 ∈ 𝑘 ∧ ∃𝑎 ∈ 𝑠 ¬ ⟨𝑎, 𝑏⟩ ∈ 𝑥)))
144	112, 120, 143	3bitr4d 313	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) → (𝑏 ∈ ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ↔ 𝑏 ∈ (𝑘 ∖ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})))
145	144	eqrdv 2762	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) → ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) = (𝑘 ∖ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}))
146	74, 76, 145	syl2anc 593	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) = (𝑘 ∖ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}))
147		difin 4226	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∖ (𝑘 ∩ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})) = (𝑘 ∖ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})
148	65	adantr 484	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → 𝑆 ∈ Top)
149	24	restuni 23224	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑆 ∈ Top ∧ 𝑘 ⊆ ∪ 𝑆) → 𝑘 = ∪ (𝑆 ↾t 𝑘))
150	148, 76, 149	syl2anc 593	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → 𝑘 = ∪ (𝑆 ↾t 𝑘))
151	150	difeq1d 4081	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → (𝑘 ∖ (𝑘 ∩ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})) = (∪ (𝑆 ↾t 𝑘) ∖ (𝑘 ∩ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})))
152	147, 151	eqtr3id 2813	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → (𝑘 ∖ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) = (∪ (𝑆 ↾t 𝑘) ∖ (𝑘 ∩ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})))
153	146, 152	eqtrd 2799	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) = (∪ (𝑆 ↾t 𝑘) ∖ (𝑘 ∩ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})))
154	15	ad2antrr 736	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → 𝑆 ∈ (ran 𝑘Gen ∩ Haus))
155	154	elin2d 4159	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → 𝑆 ∈ Haus)
156		df-ima 5662	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) = ran ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) ↾ ((𝑠 × 𝑘) ∖ 𝑥))
157		resres 5980	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) ↾ ((𝑠 × 𝑘) ∖ 𝑥)) = (2nd ↾ ((∪ 𝑅 × ∪ 𝑆) ∩ ((𝑠 × 𝑘) ∖ 𝑥)))
158		inss2 4191	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((∪ 𝑅 × ∪ 𝑆) ∩ ((𝑠 × 𝑘) ∖ 𝑥)) ⊆ ((𝑠 × 𝑘) ∖ 𝑥)
159	158, 116	sstri 3947	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((∪ 𝑅 × ∪ 𝑆) ∩ ((𝑠 × 𝑘) ∖ 𝑥)) ⊆ (𝑠 × 𝑘)
160		ssres2 5992	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((∪ 𝑅 × ∪ 𝑆) ∩ ((𝑠 × 𝑘) ∖ 𝑥)) ⊆ (𝑠 × 𝑘) → (2nd ↾ ((∪ 𝑅 × ∪ 𝑆) ∩ ((𝑠 × 𝑘) ∖ 𝑥))) ⊆ (2nd ↾ (𝑠 × 𝑘)))
161	159, 160	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (2nd ↾ ((∪ 𝑅 × ∪ 𝑆) ∩ ((𝑠 × 𝑘) ∖ 𝑥))) ⊆ (2nd ↾ (𝑠 × 𝑘))
162	157, 161	eqsstri 3984	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) ↾ ((𝑠 × 𝑘) ∖ 𝑥)) ⊆ (2nd ↾ (𝑠 × 𝑘))
163	162	rnssi 5918	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ran ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) ↾ ((𝑠 × 𝑘) ∖ 𝑥)) ⊆ ran (2nd ↾ (𝑠 × 𝑘))
164	156, 163	eqsstri 3984	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ⊆ ran (2nd ↾ (𝑠 × 𝑘))
165		f2ndres 7997	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (2nd ↾ (𝑠 × 𝑘)):(𝑠 × 𝑘)⟶𝑘
166		frn 6701	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((2nd ↾ (𝑠 × 𝑘)):(𝑠 × 𝑘)⟶𝑘 → ran (2nd ↾ (𝑠 × 𝑘)) ⊆ 𝑘)
167	165, 166	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ran (2nd ↾ (𝑠 × 𝑘)) ⊆ 𝑘
168	164, 167	sstri 3947	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ⊆ 𝑘
169	168, 76	sstrid 3949	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ⊆ ∪ 𝑆)
170	12	ad2antrr 736	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → 𝑅 ∈ (TopOn‘∪ 𝑅))
171	148, 17	sylib 220	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → 𝑆 ∈ (TopOn‘∪ 𝑆))
172		tx2cn 23672	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑅 ∈ (TopOn‘∪ 𝑅) ∧ 𝑆 ∈ (TopOn‘∪ 𝑆)) → (2nd ↾ (∪ 𝑅 × ∪ 𝑆)) ∈ ((𝑅 ×t 𝑆) Cn 𝑆))
173	170, 171, 172	syl2anc 593	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → (2nd ↾ (∪ 𝑅 × ∪ 𝑆)) ∈ ((𝑅 ×t 𝑆) Cn 𝑆))
174	27	ad2antrr 736	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → (𝑅 ×t 𝑆) ∈ Top)
175	116	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → ((𝑠 × 𝑘) ∖ 𝑥) ⊆ (𝑠 × 𝑘))
176		vex 3460	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 𝑠 ∈ V
177		vex 3460	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 𝑘 ∈ V
178	176, 177	xpex 7738	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑠 × 𝑘) ∈ V
179	178	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → (𝑠 × 𝑘) ∈ V)
180		restabs 23227	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑅 ×t 𝑆) ∈ Top ∧ ((𝑠 × 𝑘) ∖ 𝑥) ⊆ (𝑠 × 𝑘) ∧ (𝑠 × 𝑘) ∈ V) → (((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ↾t ((𝑠 × 𝑘) ∖ 𝑥)) = ((𝑅 ×t 𝑆) ↾t ((𝑠 × 𝑘) ∖ 𝑥)))
181	174, 175, 179, 180	syl3anc 1392	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → (((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ↾t ((𝑠 × 𝑘) ∖ 𝑥)) = ((𝑅 ×t 𝑆) ↾t ((𝑠 × 𝑘) ∖ 𝑥)))
182	64	adantr 484	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → 𝑅 ∈ Top)
183	154, 4	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → 𝑆 ∈ Top)
184	176	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → 𝑠 ∈ V)
185		simprl 780	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → 𝑘 ∈ 𝒫 ∪ 𝑆)
186		txrest 23693	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑠 ∈ V ∧ 𝑘 ∈ 𝒫 ∪ 𝑆)) → ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) = ((𝑅 ↾t 𝑠) ×t (𝑆 ↾t 𝑘)))
187	182, 183, 184, 185, 186	syl22anc 849	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) = ((𝑅 ↾t 𝑠) ×t (𝑆 ↾t 𝑘)))
188		simprr3 1238	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → (𝑅 ↾t 𝑠) ∈ Comp)
189	188	adantr 484	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → (𝑅 ↾t 𝑠) ∈ Comp)
190		simprr 782	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → (𝑆 ↾t 𝑘) ∈ Comp)
191		txcmp 23705	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑅 ↾t 𝑠) ∈ Comp ∧ (𝑆 ↾t 𝑘) ∈ Comp) → ((𝑅 ↾t 𝑠) ×t (𝑆 ↾t 𝑘)) ∈ Comp)
192	189, 190, 191	syl2anc 593	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → ((𝑅 ↾t 𝑠) ×t (𝑆 ↾t 𝑘)) ∈ Comp)
193	187, 192	eqeltrd 2864	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ∈ Comp)
194		difin 4226	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑠 × 𝑘) ∖ ((𝑠 × 𝑘) ∩ 𝑥)) = ((𝑠 × 𝑘) ∖ 𝑥)
195	74, 76, 117	syl2anc 593	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → (𝑠 × 𝑘) ⊆ (∪ 𝑅 × ∪ 𝑆))
196	182, 148, 25	syl2anc 593	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → (∪ 𝑅 × ∪ 𝑆) = ∪ (𝑅 ×t 𝑆))
197	195, 196	sseqtrd 3974	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → (𝑠 × 𝑘) ⊆ ∪ (𝑅 ×t 𝑆))
198	28	restuni 23224	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑅 ×t 𝑆) ∈ Top ∧ (𝑠 × 𝑘) ⊆ ∪ (𝑅 ×t 𝑆)) → (𝑠 × 𝑘) = ∪ ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)))
199	174, 197, 198	syl2anc 593	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → (𝑠 × 𝑘) = ∪ ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)))
200	199	difeq1d 4081	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → ((𝑠 × 𝑘) ∖ ((𝑠 × 𝑘) ∩ 𝑥)) = (∪ ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ∖ ((𝑠 × 𝑘) ∩ 𝑥)))
201	194, 200	eqtr3id 2813	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → ((𝑠 × 𝑘) ∖ 𝑥) = (∪ ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ∖ ((𝑠 × 𝑘) ∩ 𝑥)))
202		resttop 23222	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑅 ×t 𝑆) ∈ Top ∧ (𝑠 × 𝑘) ∈ V) → ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ∈ Top)
203	174, 178, 202	sylancl 595	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ∈ Top)
204		incom 4163	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑠 × 𝑘) ∩ 𝑥) = (𝑥 ∩ (𝑠 × 𝑘))
205	20	ad2antrr 736	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆)))
206		kgeni 23599	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆)) ∧ ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ∈ Comp) → (𝑥 ∩ (𝑠 × 𝑘)) ∈ ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)))
207	205, 193, 206	syl2anc 593	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → (𝑥 ∩ (𝑠 × 𝑘)) ∈ ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)))
208	204, 207	eqeltrid 2868	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → ((𝑠 × 𝑘) ∩ 𝑥) ∈ ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)))
209		eqid 2764	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ∪ ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) = ∪ ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘))
210	209	opncld 23095	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ∈ Top ∧ ((𝑠 × 𝑘) ∩ 𝑥) ∈ ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘))) → (∪ ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ∖ ((𝑠 × 𝑘) ∩ 𝑥)) ∈ (Clsd‘((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘))))
211	203, 208, 210	syl2anc 593	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → (∪ ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ∖ ((𝑠 × 𝑘) ∩ 𝑥)) ∈ (Clsd‘((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘))))
212	201, 211	eqeltrd 2864	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → ((𝑠 × 𝑘) ∖ 𝑥) ∈ (Clsd‘((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘))))
213		cmpcld 23464	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ∈ Comp ∧ ((𝑠 × 𝑘) ∖ 𝑥) ∈ (Clsd‘((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)))) → (((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ↾t ((𝑠 × 𝑘) ∖ 𝑥)) ∈ Comp)
214	193, 212, 213	syl2anc 593	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → (((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ↾t ((𝑠 × 𝑘) ∖ 𝑥)) ∈ Comp)
215	181, 214	eqeltrrd 2865	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → ((𝑅 ×t 𝑆) ↾t ((𝑠 × 𝑘) ∖ 𝑥)) ∈ Comp)
216		imacmp 23459	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) ∈ ((𝑅 ×t 𝑆) Cn 𝑆) ∧ ((𝑅 ×t 𝑆) ↾t ((𝑠 × 𝑘) ∖ 𝑥)) ∈ Comp) → (𝑆 ↾t ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥))) ∈ Comp)
217	173, 215, 216	syl2anc 593	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → (𝑆 ↾t ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥))) ∈ Comp)
218	24	hauscmp 23469	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑆 ∈ Haus ∧ ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ⊆ ∪ 𝑆 ∧ (𝑆 ↾t ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥))) ∈ Comp) → ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ∈ (Clsd‘𝑆))
219	155, 169, 217, 218	syl3anc 1392	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ∈ (Clsd‘𝑆))
220	168	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ⊆ 𝑘)
221	24	restcldi 23235	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑘 ⊆ ∪ 𝑆 ∧ ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ∈ (Clsd‘𝑆) ∧ ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ⊆ 𝑘) → ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ∈ (Clsd‘(𝑆 ↾t 𝑘)))
222	76, 219, 220, 221	syl3anc 1392	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ∈ (Clsd‘(𝑆 ↾t 𝑘)))
223	153, 222	eqeltrrd 2865	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → (∪ (𝑆 ↾t 𝑘) ∖ (𝑘 ∩ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})) ∈ (Clsd‘(𝑆 ↾t 𝑘)))
224		resttop 23222	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑆 ∈ Top ∧ 𝑘 ∈ 𝒫 ∪ 𝑆) → (𝑆 ↾t 𝑘) ∈ Top)
225	148, 185, 224	syl2anc 593	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → (𝑆 ↾t 𝑘) ∈ Top)
226		inss1 4190	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 ∩ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ⊆ 𝑘
227	226, 150	sseqtrid 3980	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → (𝑘 ∩ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ⊆ ∪ (𝑆 ↾t 𝑘))
228		eqid 2764	. . . . . . . . . . . . . . . . . . 19 ⊢ ∪ (𝑆 ↾t 𝑘) = ∪ (𝑆 ↾t 𝑘)
229	228	isopn2 23094	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑆 ↾t 𝑘) ∈ Top ∧ (𝑘 ∩ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ⊆ ∪ (𝑆 ↾t 𝑘)) → ((𝑘 ∩ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ∈ (𝑆 ↾t 𝑘) ↔ (∪ (𝑆 ↾t 𝑘) ∖ (𝑘 ∩ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})) ∈ (Clsd‘(𝑆 ↾t 𝑘))))
230	225, 227, 229	syl2anc 593	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → ((𝑘 ∩ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ∈ (𝑆 ↾t 𝑘) ↔ (∪ (𝑆 ↾t 𝑘) ∖ (𝑘 ∩ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})) ∈ (Clsd‘(𝑆 ↾t 𝑘))))
231	223, 230	mpbird 259	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → (𝑘 ∩ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ∈ (𝑆 ↾t 𝑘))
232	69, 231	eqeltrid 2868	. . . . . . . . . . . . . . 15 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → ({𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ∩ 𝑘) ∈ (𝑆 ↾t 𝑘))
233	232	expr 460	. . . . . . . . . . . . . 14 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ 𝑘 ∈ 𝒫 ∪ 𝑆) → ((𝑆 ↾t 𝑘) ∈ Comp → ({𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ∩ 𝑘) ∈ (𝑆 ↾t 𝑘)))
234	233	ralrimiva 3156	. . . . . . . . . . . . 13 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → ∀𝑘 ∈ 𝒫 ∪ 𝑆((𝑆 ↾t 𝑘) ∈ Comp → ({𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ∩ 𝑘) ∈ (𝑆 ↾t 𝑘)))
235	65, 17	sylib 220	. . . . . . . . . . . . . 14 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → 𝑆 ∈ (TopOn‘∪ 𝑆))
236		elkgen 23598	. . . . . . . . . . . . . 14 ⊢ (𝑆 ∈ (TopOn‘∪ 𝑆) → ({𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ∈ (𝑘Gen‘𝑆) ↔ ({𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ⊆ ∪ 𝑆 ∧ ∀𝑘 ∈ 𝒫 ∪ 𝑆((𝑆 ↾t 𝑘) ∈ Comp → ({𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ∩ 𝑘) ∈ (𝑆 ↾t 𝑘)))))
237	235, 236	syl 17	. . . . . . . . . . . . 13 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → ({𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ∈ (𝑘Gen‘𝑆) ↔ ({𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ⊆ ∪ 𝑆 ∧ ∀𝑘 ∈ 𝒫 ∪ 𝑆((𝑆 ↾t 𝑘) ∈ Comp → ({𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ∩ 𝑘) ∈ (𝑆 ↾t 𝑘)))))
238	68, 234, 237	mpbir2and 723	. . . . . . . . . . . 12 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ∈ (𝑘Gen‘𝑆))
239	15	adantr 484	. . . . . . . . . . . . . 14 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → 𝑆 ∈ (ran 𝑘Gen ∩ Haus))
240	239, 2	syl 17	. . . . . . . . . . . . 13 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → 𝑆 ∈ ran 𝑘Gen)
241		kgenidm 23609	. . . . . . . . . . . . 13 ⊢ (𝑆 ∈ ran 𝑘Gen → (𝑘Gen‘𝑆) = 𝑆)
242	240, 241	syl 17	. . . . . . . . . . . 12 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → (𝑘Gen‘𝑆) = 𝑆)
243	238, 242	eleqtrd 2866	. . . . . . . . . . 11 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ∈ 𝑆)
244		txopn 23664	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑢 ∈ 𝑅 ∧ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ∈ 𝑆)) → (𝑢 × {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ∈ (𝑅 ×t 𝑆))
245	64, 65, 66, 243, 244	syl22anc 849	. . . . . . . . . 10 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → (𝑢 × {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ∈ (𝑅 ×t 𝑆))
246	59	adantr 484	. . . . . . . . . . 11 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → 𝑦 = ⟨(1st ‘𝑦), (2nd ‘𝑦)⟩)
247		simprr1 1236	. . . . . . . . . . . 12 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → (1st ‘𝑦) ∈ 𝑢)
248		sneq 4594	. . . . . . . . . . . . . . 15 ⊢ (𝑣 = (2nd ‘𝑦) → {𝑣} = {(2nd ‘𝑦)})
249	248	xpeq2d 5679	. . . . . . . . . . . . . 14 ⊢ (𝑣 = (2nd ‘𝑦) → (𝑠 × {𝑣}) = (𝑠 × {(2nd ‘𝑦)}))
250	249	sseq1d 3969	. . . . . . . . . . . . 13 ⊢ (𝑣 = (2nd ‘𝑦) → ((𝑠 × {𝑣}) ⊆ 𝑥 ↔ (𝑠 × {(2nd ‘𝑦)}) ⊆ 𝑥))
251	34	adantr 484	. . . . . . . . . . . . 13 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → (2nd ‘𝑦) ∈ ∪ 𝑆)
252		relxp 5667	. . . . . . . . . . . . . . 15 ⊢ Rel (𝑠 × {(2nd ‘𝑦)})
253	252	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → Rel (𝑠 × {(2nd ‘𝑦)}))
254		opelxp 5685	. . . . . . . . . . . . . . 15 ⊢ (⟨𝑎, 𝑏⟩ ∈ (𝑠 × {(2nd ‘𝑦)}) ↔ (𝑎 ∈ 𝑠 ∧ 𝑏 ∈ {(2nd ‘𝑦)}))
255	71	sselda 3938	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ 𝑎 ∈ 𝑠) → 𝑎 ∈ {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥})
256		opeq1 4833	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑡 = 𝑎 → ⟨𝑡, (2nd ‘𝑦)⟩ = ⟨𝑎, (2nd ‘𝑦)⟩)
257	256	eleq1d 2849	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 = 𝑎 → (⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥 ↔ ⟨𝑎, (2nd ‘𝑦)⟩ ∈ 𝑥))
258	257	elrab 3652	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 ∈ {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ↔ (𝑎 ∈ ∪ 𝑅 ∧ ⟨𝑎, (2nd ‘𝑦)⟩ ∈ 𝑥))
259	258	simprbi 501	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 ∈ {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} → ⟨𝑎, (2nd ‘𝑦)⟩ ∈ 𝑥)
260	255, 259	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ 𝑎 ∈ 𝑠) → ⟨𝑎, (2nd ‘𝑦)⟩ ∈ 𝑥)
261		elsni 4601	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 ∈ {(2nd ‘𝑦)} → 𝑏 = (2nd ‘𝑦))
262	261	opeq2d 4840	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 ∈ {(2nd ‘𝑦)} → ⟨𝑎, 𝑏⟩ = ⟨𝑎, (2nd ‘𝑦)⟩)
263	262	eleq1d 2849	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 ∈ {(2nd ‘𝑦)} → (⟨𝑎, 𝑏⟩ ∈ 𝑥 ↔ ⟨𝑎, (2nd ‘𝑦)⟩ ∈ 𝑥))
264	260, 263	syl5ibrcom 249	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ 𝑎 ∈ 𝑠) → (𝑏 ∈ {(2nd ‘𝑦)} → ⟨𝑎, 𝑏⟩ ∈ 𝑥))
265	264	expimpd 457	. . . . . . . . . . . . . . 15 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → ((𝑎 ∈ 𝑠 ∧ 𝑏 ∈ {(2nd ‘𝑦)}) → ⟨𝑎, 𝑏⟩ ∈ 𝑥))
266	254, 265	biimtrid 244	. . . . . . . . . . . . . 14 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → (⟨𝑎, 𝑏⟩ ∈ (𝑠 × {(2nd ‘𝑦)}) → ⟨𝑎, 𝑏⟩ ∈ 𝑥))
267	253, 266	relssdv 5762	. . . . . . . . . . . . 13 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → (𝑠 × {(2nd ‘𝑦)}) ⊆ 𝑥)
268	250, 251, 267	elrabd 3654	. . . . . . . . . . . 12 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → (2nd ‘𝑦) ∈ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})
269	247, 268	opelxpd 5688	. . . . . . . . . . 11 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → ⟨(1st ‘𝑦), (2nd ‘𝑦)⟩ ∈ (𝑢 × {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}))
270	246, 269	eqeltrd 2864	. . . . . . . . . 10 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → 𝑦 ∈ (𝑢 × {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}))
271		relxp 5667	. . . . . . . . . . . 12 ⊢ Rel (𝑢 × {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})
272	271	a1i 11	. . . . . . . . . . 11 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → Rel (𝑢 × {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}))
273		opelxp 5685	. . . . . . . . . . . 12 ⊢ (⟨𝑎, 𝑏⟩ ∈ (𝑢 × {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ↔ (𝑎 ∈ 𝑢 ∧ 𝑏 ∈ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}))
274	126	elrab 3652	. . . . . . . . . . . . . . 15 ⊢ (𝑏 ∈ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ↔ (𝑏 ∈ ∪ 𝑆 ∧ (𝑠 × {𝑏}) ⊆ 𝑥))
275	274	simprbi 501	. . . . . . . . . . . . . 14 ⊢ (𝑏 ∈ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} → (𝑠 × {𝑏}) ⊆ 𝑥)
276		simprr2 1237	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → 𝑢 ⊆ 𝑠)
277	276	sselda 3938	. . . . . . . . . . . . . . 15 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ 𝑎 ∈ 𝑢) → 𝑎 ∈ 𝑠)
278		vsnid 4624	. . . . . . . . . . . . . . 15 ⊢ 𝑏 ∈ {𝑏}
279		opelxpi 5686	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 ∈ 𝑠 ∧ 𝑏 ∈ {𝑏}) → ⟨𝑎, 𝑏⟩ ∈ (𝑠 × {𝑏}))
280	277, 278, 279	sylancl 595	. . . . . . . . . . . . . 14 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ 𝑎 ∈ 𝑢) → ⟨𝑎, 𝑏⟩ ∈ (𝑠 × {𝑏}))
281		ssel 3932	. . . . . . . . . . . . . 14 ⊢ ((𝑠 × {𝑏}) ⊆ 𝑥 → (⟨𝑎, 𝑏⟩ ∈ (𝑠 × {𝑏}) → ⟨𝑎, 𝑏⟩ ∈ 𝑥))
282	275, 280, 281	syl2imc 41	. . . . . . . . . . . . 13 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ 𝑎 ∈ 𝑢) → (𝑏 ∈ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} → ⟨𝑎, 𝑏⟩ ∈ 𝑥))
283	282	expimpd 457	. . . . . . . . . . . 12 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → ((𝑎 ∈ 𝑢 ∧ 𝑏 ∈ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) → ⟨𝑎, 𝑏⟩ ∈ 𝑥))
284	273, 283	biimtrid 244	. . . . . . . . . . 11 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → (⟨𝑎, 𝑏⟩ ∈ (𝑢 × {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) → ⟨𝑎, 𝑏⟩ ∈ 𝑥))
285	272, 284	relssdv 5762	. . . . . . . . . 10 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → (𝑢 × {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ⊆ 𝑥)
286		eleq2 2853	. . . . . . . . . . . 12 ⊢ (𝑡 = (𝑢 × {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) → (𝑦 ∈ 𝑡 ↔ 𝑦 ∈ (𝑢 × {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})))
287		sseq1 3963	. . . . . . . . . . . 12 ⊢ (𝑡 = (𝑢 × {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) → (𝑡 ⊆ 𝑥 ↔ (𝑢 × {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ⊆ 𝑥))
288	286, 287	anbi12d 641	. . . . . . . . . . 11 ⊢ (𝑡 = (𝑢 × {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) → ((𝑦 ∈ 𝑡 ∧ 𝑡 ⊆ 𝑥) ↔ (𝑦 ∈ (𝑢 × {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ∧ (𝑢 × {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ⊆ 𝑥)))
289	288	rspcev 3583	. . . . . . . . . 10 ⊢ (((𝑢 × {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ∈ (𝑅 ×t 𝑆) ∧ (𝑦 ∈ (𝑢 × {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ∧ (𝑢 × {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ⊆ 𝑥)) → ∃𝑡 ∈ (𝑅 ×t 𝑆)(𝑦 ∈ 𝑡 ∧ 𝑡 ⊆ 𝑥))
290	245, 270, 285, 289	syl12anc 847	. . . . . . . . 9 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → ∃𝑡 ∈ (𝑅 ×t 𝑆)(𝑦 ∈ 𝑡 ∧ 𝑡 ⊆ 𝑥))
291	290	expr 460	. . . . . . . 8 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ (𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅)) → (((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp) → ∃𝑡 ∈ (𝑅 ×t 𝑆)(𝑦 ∈ 𝑡 ∧ 𝑡 ⊆ 𝑥)))
292	291	rexlimdvva 3221	. . . . . . 7 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → (∃𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥}∃𝑢 ∈ 𝑅 ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp) → ∃𝑡 ∈ (𝑅 ×t 𝑆)(𝑦 ∈ 𝑡 ∧ 𝑡 ⊆ 𝑥)))
293	63, 292	mpd 15	. . . . . 6 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → ∃𝑡 ∈ (𝑅 ×t 𝑆)(𝑦 ∈ 𝑡 ∧ 𝑡 ⊆ 𝑥))
294	293	ralrimiva 3156	. . . . 5 ⊢ (((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) → ∀𝑦 ∈ 𝑥 ∃𝑡 ∈ (𝑅 ×t 𝑆)(𝑦 ∈ 𝑡 ∧ 𝑡 ⊆ 𝑥))
295	6	adantr 484	. . . . . 6 ⊢ (((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) → (𝑅 ×t 𝑆) ∈ Top)
296		eltop2 23037	. . . . . 6 ⊢ ((𝑅 ×t 𝑆) ∈ Top → (𝑥 ∈ (𝑅 ×t 𝑆) ↔ ∀𝑦 ∈ 𝑥 ∃𝑡 ∈ (𝑅 ×t 𝑆)(𝑦 ∈ 𝑡 ∧ 𝑡 ⊆ 𝑥)))
297	295, 296	syl 17	. . . . 5 ⊢ (((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) → (𝑥 ∈ (𝑅 ×t 𝑆) ↔ ∀𝑦 ∈ 𝑥 ∃𝑡 ∈ (𝑅 ×t 𝑆)(𝑦 ∈ 𝑡 ∧ 𝑡 ⊆ 𝑥)))
298	294, 297	mpbird 259	. . . 4 ⊢ (((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) → 𝑥 ∈ (𝑅 ×t 𝑆))
299	298	ex 416	. . 3 ⊢ ((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) → (𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆)) → 𝑥 ∈ (𝑅 ×t 𝑆)))
300	299	ssrdv 3944	. 2 ⊢ ((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) → (𝑘Gen‘(𝑅 ×t 𝑆)) ⊆ (𝑅 ×t 𝑆))
301		iskgen2 23610	. 2 ⊢ ((𝑅 ×t 𝑆) ∈ ran 𝑘Gen ↔ ((𝑅 ×t 𝑆) ∈ Top ∧ (𝑘Gen‘(𝑅 ×t 𝑆)) ⊆ (𝑅 ×t 𝑆)))
302	6, 300, 301	sylanbrc 592	1 ⊢ ((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) → (𝑅 ×t 𝑆) ∈ ran 𝑘Gen)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 399   ∧ w3a 1099   = wceq 1562   ∈ wcel 2144  ∀wral 3078  ∃wrex 3088  {crab 3416  Vcvv 3456   ∖ cdif 3903   ∩ cin 3905   ⊆ wss 3906  𝒫 cpw 4557  {csn 4584  ⟨cop 4590  ∪ cuni 4867   ↦ cmpt 5183   I cid 5543   × cxp 5647  ^◡ccnv 5648  ran crn 5650   ↾ cres 5651   “ cima 5652  Rel wrel 5654   Fn wfn 6518  ⟶wf 6519  ‘cfv 6523  (class class class)co 7398  1^st c1st 7970  2^nd c2nd 7971   ↾_t crest 17451  Topctop 22955  TopOnctopon 22972  Clsdccld 23078   Cn ccn 23286  Hauscha 23370  Compccmp 23448  𝑛-Locally cnlly 23527  𝑘Genckgen 23595   ×_t ctx 23622

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2214  ax-ext 2736  ax-rep 5229  ax-sep 5248  ax-nul 5258  ax-pow 5324  ax-pr 5392  ax-un 7720

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1100  df-3an 1101  df-tru 1565  df-fal 1575  df-ex 1802  df-nf 1806  df-sb 2093  df-mo 2568  df-eu 2598  df-clab 2743  df-cleq 2756  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3079  df-rex 3089  df-reu 3370  df-rab 3417  df-v 3458  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4288  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-int 4908  df-iun 4953  df-iin 4954  df-br 5103  df-opab 5165  df-mpt 5184  df-tr 5210  df-id 5544  df-eprel 5549  df-po 5557  df-so 5558  df-fr 5602  df-we 5604  df-xp 5655  df-rel 5656  df-cnv 5657  df-co 5658  df-dm 5659  df-rn 5660  df-res 5661  df-ima 5662  df-ord 6351  df-on 6352  df-lim 6353  df-suc 6354  df-iota 6479  df-fun 6525  df-fn 6526  df-f 6527  df-f1 6528  df-fo 6529  df-f1o 6530  df-fv 6531  df-ov 7401  df-oprab 7402  df-mpo 7403  df-om 7849  df-1st 7972  df-2nd 7973  df-1o 8439  df-2o 8440  df-map 8812  df-en 8930  df-dom 8931  df-fin 8933  df-fi 9359  df-rest 17453  df-topgen 17474  df-top 22956  df-topon 22973  df-bases 23008  df-cld 23081  df-ntr 23082  df-cls 23083  df-nei 23160  df-cn 23289  df-cnp 23290  df-haus 23377  df-cmp 23449  df-nlly 23529  df-kgen 23596  df-tx 23624

This theorem is referenced by: (None)