Theorem txkgen 23598

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 23419	. . 3 ⊢ (𝑅 ∈ 𝑛-Locally Comp → 𝑅 ∈ Top)
2		elinel1 4152	. . . 4 ⊢ (𝑆 ∈ (ran 𝑘Gen ∩ Haus) → 𝑆 ∈ ran 𝑘Gen)
3		kgentop 23488	. . . 4 ⊢ (𝑆 ∈ ran 𝑘Gen → 𝑆 ∈ Top)
4	2, 3	syl 17	. . 3 ⊢ (𝑆 ∈ (ran 𝑘Gen ∩ Haus) → 𝑆 ∈ Top)
5		txtop 23515	. . 3 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑅 ×t 𝑆) ∈ Top)
6	1, 4, 5	syl2an 597	. 2 ⊢ ((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) → (𝑅 ×t 𝑆) ∈ Top)
7		simplll 775	. . . . . . . 8 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → 𝑅 ∈ 𝑛-Locally Comp)
8		eqid 2735	. . . . . . . . . 10 ⊢ (𝑡 ∈ ∪ 𝑅 ↦ ⟨𝑡, (2nd ‘𝑦)⟩) = (𝑡 ∈ ∪ 𝑅 ↦ ⟨𝑡, (2nd ‘𝑦)⟩)
9	8	mptpreima 6195	. . . . . . . . 9 ⊢ (◡(𝑡 ∈ ∪ 𝑅 ↦ ⟨𝑡, (2nd ‘𝑦)⟩) “ 𝑥) = {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥}
10	1	ad3antrrr 731	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → 𝑅 ∈ Top)
11		toptopon2 22864	. . . . . . . . . . . . . 14 ⊢ (𝑅 ∈ Top ↔ 𝑅 ∈ (TopOn‘∪ 𝑅))
12	10, 11	sylib 218	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → 𝑅 ∈ (TopOn‘∪ 𝑅))
13		idcn 23203	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ (TopOn‘∪ 𝑅) → ( I ↾ ∪ 𝑅) ∈ (𝑅 Cn 𝑅))
14	12, 13	syl 17	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → ( I ↾ ∪ 𝑅) ∈ (𝑅 Cn 𝑅))
15		simpllr 776	. . . . . . . . . . . . . . 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 22864	. . . . . . . . . . . . . 14 ⊢ (𝑆 ∈ Top ↔ 𝑆 ∈ (TopOn‘∪ 𝑆))
18	16, 17	sylib 218	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → 𝑆 ∈ (TopOn‘∪ 𝑆))
19		simpr 484	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ 𝑥)
20		simplr 769	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆)))
21		elunii 4867	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) → 𝑦 ∈ ∪ (𝑘Gen‘(𝑅 ×t 𝑆)))
22	19, 20, 21	syl2anc 585	. . . . . . . . . . . . . . 15 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ ∪ (𝑘Gen‘(𝑅 ×t 𝑆)))
23		eqid 2735	. . . . . . . . . . . . . . . . . 18 ⊢ ∪ 𝑅 = ∪ 𝑅
24		eqid 2735	. . . . . . . . . . . . . . . . . 18 ⊢ ∪ 𝑆 = ∪ 𝑆
25	23, 24	txuni 23538	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (∪ 𝑅 × ∪ 𝑆) = ∪ (𝑅 ×t 𝑆))
26	10, 16, 25	syl2anc 585	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → (∪ 𝑅 × ∪ 𝑆) = ∪ (𝑅 ×t 𝑆))
27	10, 16, 5	syl2anc 585	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → (𝑅 ×t 𝑆) ∈ Top)
28		eqid 2735	. . . . . . . . . . . . . . . . . 18 ⊢ ∪ (𝑅 ×t 𝑆) = ∪ (𝑅 ×t 𝑆)
29	28	kgenuni 23485	. . . . . . . . . . . . . . . . 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 2770	. . . . . . . . . . . . . . 15 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → (∪ 𝑅 × ∪ 𝑆) = ∪ (𝑘Gen‘(𝑅 ×t 𝑆)))
32	22, 31	eleqtrrd 2838	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ (∪ 𝑅 × ∪ 𝑆))
33		xp2nd 7966	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ (∪ 𝑅 × ∪ 𝑆) → (2nd ‘𝑦) ∈ ∪ 𝑆)
34	32, 33	syl 17	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → (2nd ‘𝑦) ∈ ∪ 𝑆)
35		cnconst2 23229	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ (TopOn‘∪ 𝑅) ∧ 𝑆 ∈ (TopOn‘∪ 𝑆) ∧ (2nd ‘𝑦) ∈ ∪ 𝑆) → (∪ 𝑅 × {(2nd ‘𝑦)}) ∈ (𝑅 Cn 𝑆))
36	12, 18, 34, 35	syl3anc 1374	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → (∪ 𝑅 × {(2nd ‘𝑦)}) ∈ (𝑅 Cn 𝑆))
37		fvresi 7119	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 ∈ ∪ 𝑅 → (( I ↾ ∪ 𝑅)‘𝑡) = 𝑡)
38		fvex 6846	. . . . . . . . . . . . . . . . 17 ⊢ (2nd ‘𝑦) ∈ V
39	38	fvconst2 7150	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 ∈ ∪ 𝑅 → ((∪ 𝑅 × {(2nd ‘𝑦)})‘𝑡) = (2nd ‘𝑦))
40	37, 39	opeq12d 4836	. . . . . . . . . . . . . . 15 ⊢ (𝑡 ∈ ∪ 𝑅 → ⟨(( I ↾ ∪ 𝑅)‘𝑡), ((∪ 𝑅 × {(2nd ‘𝑦)})‘𝑡)⟩ = ⟨𝑡, (2nd ‘𝑦)⟩)
41	40	mpteq2ia 5192	. . . . . . . . . . . . . 14 ⊢ (𝑡 ∈ ∪ 𝑅 ↦ ⟨(( I ↾ ∪ 𝑅)‘𝑡), ((∪ 𝑅 × {(2nd ‘𝑦)})‘𝑡)⟩) = (𝑡 ∈ ∪ 𝑅 ↦ ⟨𝑡, (2nd ‘𝑦)⟩)
42	41	eqcomi 2744	. . . . . . . . . . . . 13 ⊢ (𝑡 ∈ ∪ 𝑅 ↦ ⟨𝑡, (2nd ‘𝑦)⟩) = (𝑡 ∈ ∪ 𝑅 ↦ ⟨(( I ↾ ∪ 𝑅)‘𝑡), ((∪ 𝑅 × {(2nd ‘𝑦)})‘𝑡)⟩)
43	23, 42	txcnmpt 23570	. . . . . . . . . . . 12 ⊢ ((( I ↾ ∪ 𝑅) ∈ (𝑅 Cn 𝑅) ∧ (∪ 𝑅 × {(2nd ‘𝑦)}) ∈ (𝑅 Cn 𝑆)) → (𝑡 ∈ ∪ 𝑅 ↦ ⟨𝑡, (2nd ‘𝑦)⟩) ∈ (𝑅 Cn (𝑅 ×t 𝑆)))
44	14, 36, 43	syl2anc 585	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → (𝑡 ∈ ∪ 𝑅 ↦ ⟨𝑡, (2nd ‘𝑦)⟩) ∈ (𝑅 Cn (𝑅 ×t 𝑆)))
45		llycmpkgen 23498	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ 𝑛-Locally Comp → 𝑅 ∈ ran 𝑘Gen)
46	45	ad3antrrr 731	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → 𝑅 ∈ ran 𝑘Gen)
47	6	ad2antrr 727	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → (𝑅 ×t 𝑆) ∈ Top)
48		kgencn3 23504	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ ran 𝑘Gen ∧ (𝑅 ×t 𝑆) ∈ Top) → (𝑅 Cn (𝑅 ×t 𝑆)) = (𝑅 Cn (𝑘Gen‘(𝑅 ×t 𝑆))))
49	46, 47, 48	syl2anc 585	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → (𝑅 Cn (𝑅 ×t 𝑆)) = (𝑅 Cn (𝑘Gen‘(𝑅 ×t 𝑆))))
50	44, 49	eleqtrd 2837	. . . . . . . . . 10 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → (𝑡 ∈ ∪ 𝑅 ↦ ⟨𝑡, (2nd ‘𝑦)⟩) ∈ (𝑅 Cn (𝑘Gen‘(𝑅 ×t 𝑆))))
51		cnima 23211	. . . . . . . . . 10 ⊢ (((𝑡 ∈ ∪ 𝑅 ↦ ⟨𝑡, (2nd ‘𝑦)⟩) ∈ (𝑅 Cn (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) → (◡(𝑡 ∈ ∪ 𝑅 ↦ ⟨𝑡, (2nd ‘𝑦)⟩) “ 𝑥) ∈ 𝑅)
52	50, 20, 51	syl2anc 585	. . . . . . . . 9 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → (◡(𝑡 ∈ ∪ 𝑅 ↦ ⟨𝑡, (2nd ‘𝑦)⟩) “ 𝑥) ∈ 𝑅)
53	9, 52	eqeltrrid 2840	. . . . . . . 8 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∈ 𝑅)
54		opeq1 4828	. . . . . . . . . 10 ⊢ (𝑡 = (1st ‘𝑦) → ⟨𝑡, (2nd ‘𝑦)⟩ = ⟨(1st ‘𝑦), (2nd ‘𝑦)⟩)
55	54	eleq1d 2820	. . . . . . . . 9 ⊢ (𝑡 = (1st ‘𝑦) → (⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥 ↔ ⟨(1st ‘𝑦), (2nd ‘𝑦)⟩ ∈ 𝑥))
56		xp1st 7965	. . . . . . . . . 10 ⊢ (𝑦 ∈ (∪ 𝑅 × ∪ 𝑆) → (1st ‘𝑦) ∈ ∪ 𝑅)
57	32, 56	syl 17	. . . . . . . . 9 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → (1st ‘𝑦) ∈ ∪ 𝑅)
58		1st2nd2 7972	. . . . . . . . . . 11 ⊢ (𝑦 ∈ (∪ 𝑅 × ∪ 𝑆) → 𝑦 = ⟨(1st ‘𝑦), (2nd ‘𝑦)⟩)
59	32, 58	syl 17	. . . . . . . . . 10 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → 𝑦 = ⟨(1st ‘𝑦), (2nd ‘𝑦)⟩)
60	59, 19	eqeltrrd 2836	. . . . . . . . 9 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → ⟨(1st ‘𝑦), (2nd ‘𝑦)⟩ ∈ 𝑥)
61	55, 57, 60	elrabd 3647	. . . . . . . 8 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → (1st ‘𝑦) ∈ {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥})
62		nlly2i 23422	. . . . . . . 8 ⊢ ((𝑅 ∈ 𝑛-Locally Comp ∧ {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∈ 𝑅 ∧ (1st ‘𝑦) ∈ {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥}) → ∃𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥}∃𝑢 ∈ 𝑅 ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))
63	7, 53, 61, 62	syl3anc 1374	. . . . . . 7 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → ∃𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥}∃𝑢 ∈ 𝑅 ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))
64	10	adantr 480	. . . . . . . . . . 11 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → 𝑅 ∈ Top)
65	16	adantr 480	. . . . . . . . . . 11 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → 𝑆 ∈ Top)
66		simprlr 780	. . . . . . . . . . 11 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → 𝑢 ∈ 𝑅)
67		ssrab2 4031	. . . . . . . . . . . . . 14 ⊢ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ⊆ ∪ 𝑆
68	67	a1i 11	. . . . . . . . . . . . 13 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ⊆ ∪ 𝑆)
69		incom 4160	. . . . . . . . . . . . . . . 16 ⊢ ({𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ∩ 𝑘) = (𝑘 ∩ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})
70		simprll 779	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → 𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥})
71	70	elpwid 4562	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → 𝑠 ⊆ {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥})
72		ssrab2 4031	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ⊆ ∪ 𝑅
73	71, 72	sstrdi 3945	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → 𝑠 ⊆ ∪ 𝑅)
74	73	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → 𝑠 ⊆ ∪ 𝑅)
75		elpwi 4560	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 ∈ 𝒫 ∪ 𝑆 → 𝑘 ⊆ ∪ 𝑆)
76	75	ad2antrl 729	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → 𝑘 ⊆ ∪ 𝑆)
77		eldif 3910	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑡 ∈ ((𝑠 × 𝑘) ∖ 𝑥) ↔ (𝑡 ∈ (𝑠 × 𝑘) ∧ ¬ 𝑡 ∈ 𝑥))
78	77	anbi1i 625	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑡 ∈ ((𝑠 × 𝑘) ∖ 𝑥) ∧ ((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘𝑡) = 𝑏) ↔ ((𝑡 ∈ (𝑠 × 𝑘) ∧ ¬ 𝑡 ∈ 𝑥) ∧ ((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘𝑡) = 𝑏))
79		anass 468	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑡 ∈ (𝑠 × 𝑘) ∧ ¬ 𝑡 ∈ 𝑥) ∧ ((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘𝑡) = 𝑏) ↔ (𝑡 ∈ (𝑠 × 𝑘) ∧ (¬ 𝑡 ∈ 𝑥 ∧ ((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘𝑡) = 𝑏)))
80	78, 79	bitri 275	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑡 ∈ ((𝑠 × 𝑘) ∖ 𝑥) ∧ ((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘𝑡) = 𝑏) ↔ (𝑡 ∈ (𝑠 × 𝑘) ∧ (¬ 𝑡 ∈ 𝑥 ∧ ((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘𝑡) = 𝑏)))
81	80	rexbii2 3078	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (∃𝑡 ∈ ((𝑠 × 𝑘) ∖ 𝑥)((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘𝑡) = 𝑏 ↔ ∃𝑡 ∈ (𝑠 × 𝑘)(¬ 𝑡 ∈ 𝑥 ∧ ((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘𝑡) = 𝑏))
82		ancom 460	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((¬ 𝑡 ∈ 𝑥 ∧ ((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘𝑡) = 𝑏) ↔ (((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘𝑡) = 𝑏 ∧ ¬ 𝑡 ∈ 𝑥))
83		fveqeq2 6842	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑡 = ⟨𝑎, 𝑢⟩ → (((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘𝑡) = 𝑏 ↔ ((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘⟨𝑎, 𝑢⟩) = 𝑏))
84		eleq1 2823	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑡 = ⟨𝑎, 𝑢⟩ → (𝑡 ∈ 𝑥 ↔ ⟨𝑎, 𝑢⟩ ∈ 𝑥))
85	84	notbid 318	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑡 = ⟨𝑎, 𝑢⟩ → (¬ 𝑡 ∈ 𝑥 ↔ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥))
86	83, 85	anbi12d 633	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑡 = ⟨𝑎, 𝑢⟩ → ((((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘𝑡) = 𝑏 ∧ ¬ 𝑡 ∈ 𝑥) ↔ (((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘⟨𝑎, 𝑢⟩) = 𝑏 ∧ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥)))
87	82, 86	bitrid 283	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑡 = ⟨𝑎, 𝑢⟩ → ((¬ 𝑡 ∈ 𝑥 ∧ ((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘𝑡) = 𝑏) ↔ (((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘⟨𝑎, 𝑢⟩) = 𝑏 ∧ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥)))
88	87	rexxp 5790	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (∃𝑡 ∈ (𝑠 × 𝑘)(¬ 𝑡 ∈ 𝑥 ∧ ((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘𝑡) = 𝑏) ↔ ∃𝑎 ∈ 𝑠 ∃𝑢 ∈ 𝑘 (((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘⟨𝑎, 𝑢⟩) = 𝑏 ∧ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥))
89	81, 88	bitri 275	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (∃𝑡 ∈ ((𝑠 × 𝑘) ∖ 𝑥)((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘𝑡) = 𝑏 ↔ ∃𝑎 ∈ 𝑠 ∃𝑢 ∈ 𝑘 (((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘⟨𝑎, 𝑢⟩) = 𝑏 ∧ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥))
90		simpl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) → 𝑠 ⊆ ∪ 𝑅)
91	90	sselda 3932	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) ∧ 𝑎 ∈ 𝑠) → 𝑎 ∈ ∪ 𝑅)
92	91	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) ∧ 𝑎 ∈ 𝑠) ∧ 𝑢 ∈ 𝑘) → 𝑎 ∈ ∪ 𝑅)
93		simplr 769	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) ∧ 𝑎 ∈ 𝑠) → 𝑘 ⊆ ∪ 𝑆)
94	93	sselda 3932	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) ∧ 𝑎 ∈ 𝑠) ∧ 𝑢 ∈ 𝑘) → 𝑢 ∈ ∪ 𝑆)
95	92, 94	opelxpd 5662	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) ∧ 𝑎 ∈ 𝑠) ∧ 𝑢 ∈ 𝑘) → ⟨𝑎, 𝑢⟩ ∈ (∪ 𝑅 × ∪ 𝑆))
96	95	fvresd 6853	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) ∧ 𝑎 ∈ 𝑠) ∧ 𝑢 ∈ 𝑘) → ((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘⟨𝑎, 𝑢⟩) = (2nd ‘⟨𝑎, 𝑢⟩))
97		vex 3443	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ 𝑎 ∈ V
98		vex 3443	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ 𝑢 ∈ V
99	97, 98	op2nd 7942	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (2nd ‘⟨𝑎, 𝑢⟩) = 𝑢
100	96, 99	eqtrdi 2786	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) ∧ 𝑎 ∈ 𝑠) ∧ 𝑢 ∈ 𝑘) → ((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘⟨𝑎, 𝑢⟩) = 𝑢)
101	100	eqeq1d 2737	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) ∧ 𝑎 ∈ 𝑠) ∧ 𝑢 ∈ 𝑘) → (((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘⟨𝑎, 𝑢⟩) = 𝑏 ↔ 𝑢 = 𝑏))
102	101	anbi1d 632	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) ∧ 𝑎 ∈ 𝑠) ∧ 𝑢 ∈ 𝑘) → ((((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘⟨𝑎, 𝑢⟩) = 𝑏 ∧ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥) ↔ (𝑢 = 𝑏 ∧ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥)))
103	102	rexbidva 3157	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) ∧ 𝑎 ∈ 𝑠) → (∃𝑢 ∈ 𝑘 (((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘⟨𝑎, 𝑢⟩) = 𝑏 ∧ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥) ↔ ∃𝑢 ∈ 𝑘 (𝑢 = 𝑏 ∧ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥)))
104		opeq2 4829	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑢 = 𝑏 → ⟨𝑎, 𝑢⟩ = ⟨𝑎, 𝑏⟩)
105	104	eleq1d 2820	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑢 = 𝑏 → (⟨𝑎, 𝑢⟩ ∈ 𝑥 ↔ ⟨𝑎, 𝑏⟩ ∈ 𝑥))
106	105	notbid 318	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑢 = 𝑏 → (¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥 ↔ ¬ ⟨𝑎, 𝑏⟩ ∈ 𝑥))
107	106	ceqsrexbv 3609	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (∃𝑢 ∈ 𝑘 (𝑢 = 𝑏 ∧ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥) ↔ (𝑏 ∈ 𝑘 ∧ ¬ ⟨𝑎, 𝑏⟩ ∈ 𝑥))
108	103, 107	bitrdi 287	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) ∧ 𝑎 ∈ 𝑠) → (∃𝑢 ∈ 𝑘 (((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘⟨𝑎, 𝑢⟩) = 𝑏 ∧ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥) ↔ (𝑏 ∈ 𝑘 ∧ ¬ ⟨𝑎, 𝑏⟩ ∈ 𝑥)))
109	108	rexbidva 3157	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) → (∃𝑎 ∈ 𝑠 ∃𝑢 ∈ 𝑘 (((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘⟨𝑎, 𝑢⟩) = 𝑏 ∧ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥) ↔ ∃𝑎 ∈ 𝑠 (𝑏 ∈ 𝑘 ∧ ¬ ⟨𝑎, 𝑏⟩ ∈ 𝑥)))
110		r19.42v 3167	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (∃𝑎 ∈ 𝑠 (𝑏 ∈ 𝑘 ∧ ¬ ⟨𝑎, 𝑏⟩ ∈ 𝑥) ↔ (𝑏 ∈ 𝑘 ∧ ∃𝑎 ∈ 𝑠 ¬ ⟨𝑎, 𝑏⟩ ∈ 𝑥))
111	109, 110	bitrdi 287	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) → (∃𝑎 ∈ 𝑠 ∃𝑢 ∈ 𝑘 (((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘⟨𝑎, 𝑢⟩) = 𝑏 ∧ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥) ↔ (𝑏 ∈ 𝑘 ∧ ∃𝑎 ∈ 𝑠 ¬ ⟨𝑎, 𝑏⟩ ∈ 𝑥)))
112	89, 111	bitrid 283	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) → (∃𝑡 ∈ ((𝑠 × 𝑘) ∖ 𝑥)((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘𝑡) = 𝑏 ↔ (𝑏 ∈ 𝑘 ∧ ∃𝑎 ∈ 𝑠 ¬ ⟨𝑎, 𝑏⟩ ∈ 𝑥)))
113		f2ndres 7958	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (2nd ↾ (∪ 𝑅 × ∪ 𝑆)):(∪ 𝑅 × ∪ 𝑆)⟶∪ 𝑆
114		ffn 6661	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)):(∪ 𝑅 × ∪ 𝑆)⟶∪ 𝑆 → (2nd ↾ (∪ 𝑅 × ∪ 𝑆)) Fn (∪ 𝑅 × ∪ 𝑆))
115	113, 114	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (2nd ↾ (∪ 𝑅 × ∪ 𝑆)) Fn (∪ 𝑅 × ∪ 𝑆)
116		difss 4087	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑠 × 𝑘) ∖ 𝑥) ⊆ (𝑠 × 𝑘)
117		xpss12 5638	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) → (𝑠 × 𝑘) ⊆ (∪ 𝑅 × ∪ 𝑆))
118	116, 117	sstrid 3944	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) → ((𝑠 × 𝑘) ∖ 𝑥) ⊆ (∪ 𝑅 × ∪ 𝑆))
119		fvelimab 6905	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) Fn (∪ 𝑅 × ∪ 𝑆) ∧ ((𝑠 × 𝑘) ∖ 𝑥) ⊆ (∪ 𝑅 × ∪ 𝑆)) → (𝑏 ∈ ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ↔ ∃𝑡 ∈ ((𝑠 × 𝑘) ∖ 𝑥)((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘𝑡) = 𝑏))
120	115, 118, 119	sylancr 588	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) → (𝑏 ∈ ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ↔ ∃𝑡 ∈ ((𝑠 × 𝑘) ∖ 𝑥)((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘𝑡) = 𝑏))
121		eldif 3910	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑏 ∈ (𝑘 ∖ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ↔ (𝑏 ∈ 𝑘 ∧ ¬ 𝑏 ∈ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}))
122		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) → 𝑘 ⊆ ∪ 𝑆)
123	122	sselda 3932	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) ∧ 𝑏 ∈ 𝑘) → 𝑏 ∈ ∪ 𝑆)
124		sneq 4589	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑣 = 𝑏 → {𝑣} = {𝑏})
125	124	xpeq2d 5653	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑣 = 𝑏 → (𝑠 × {𝑣}) = (𝑠 × {𝑏}))
126	125	sseq1d 3964	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑣 = 𝑏 → ((𝑠 × {𝑣}) ⊆ 𝑥 ↔ (𝑠 × {𝑏}) ⊆ 𝑥))
127		dfss3 3921	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑠 × {𝑏}) ⊆ 𝑥 ↔ ∀𝑘 ∈ (𝑠 × {𝑏})𝑘 ∈ 𝑥)
128		eleq1 2823	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑘 = ⟨𝑎, 𝑡⟩ → (𝑘 ∈ 𝑥 ↔ ⟨𝑎, 𝑡⟩ ∈ 𝑥))
129	128	ralxp 5789	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (∀𝑘 ∈ (𝑠 × {𝑏})𝑘 ∈ 𝑥 ↔ ∀𝑎 ∈ 𝑠 ∀𝑡 ∈ {𝑏}⟨𝑎, 𝑡⟩ ∈ 𝑥)
130		vex 3443	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ 𝑏 ∈ V
131		opeq2 4829	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑡 = 𝑏 → ⟨𝑎, 𝑡⟩ = ⟨𝑎, 𝑏⟩)
132	131	eleq1d 2820	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑡 = 𝑏 → (⟨𝑎, 𝑡⟩ ∈ 𝑥 ↔ ⟨𝑎, 𝑏⟩ ∈ 𝑥))
133	130, 132	ralsn 4637	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (∀𝑡 ∈ {𝑏}⟨𝑎, 𝑡⟩ ∈ 𝑥 ↔ ⟨𝑎, 𝑏⟩ ∈ 𝑥)
134	133	ralbii 3081	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (∀𝑎 ∈ 𝑠 ∀𝑡 ∈ {𝑏}⟨𝑎, 𝑡⟩ ∈ 𝑥 ↔ ∀𝑎 ∈ 𝑠 ⟨𝑎, 𝑏⟩ ∈ 𝑥)
135	127, 129, 134	3bitri 297	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑠 × {𝑏}) ⊆ 𝑥 ↔ ∀𝑎 ∈ 𝑠 ⟨𝑎, 𝑏⟩ ∈ 𝑥)
136	126, 135	bitrdi 287	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑣 = 𝑏 → ((𝑠 × {𝑣}) ⊆ 𝑥 ↔ ∀𝑎 ∈ 𝑠 ⟨𝑎, 𝑏⟩ ∈ 𝑥))
137	136	elrab3 3646	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑏 ∈ ∪ 𝑆 → (𝑏 ∈ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ↔ ∀𝑎 ∈ 𝑠 ⟨𝑎, 𝑏⟩ ∈ 𝑥))
138	123, 137	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) ∧ 𝑏 ∈ 𝑘) → (𝑏 ∈ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ↔ ∀𝑎 ∈ 𝑠 ⟨𝑎, 𝑏⟩ ∈ 𝑥))
139	138	notbid 318	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) ∧ 𝑏 ∈ 𝑘) → (¬ 𝑏 ∈ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ↔ ¬ ∀𝑎 ∈ 𝑠 ⟨𝑎, 𝑏⟩ ∈ 𝑥))
140		rexnal 3087	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (∃𝑎 ∈ 𝑠 ¬ ⟨𝑎, 𝑏⟩ ∈ 𝑥 ↔ ¬ ∀𝑎 ∈ 𝑠 ⟨𝑎, 𝑏⟩ ∈ 𝑥)
141	139, 140	bitr4di 289	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) ∧ 𝑏 ∈ 𝑘) → (¬ 𝑏 ∈ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ↔ ∃𝑎 ∈ 𝑠 ¬ ⟨𝑎, 𝑏⟩ ∈ 𝑥))
142	141	pm5.32da 579	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) → ((𝑏 ∈ 𝑘 ∧ ¬ 𝑏 ∈ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ↔ (𝑏 ∈ 𝑘 ∧ ∃𝑎 ∈ 𝑠 ¬ ⟨𝑎, 𝑏⟩ ∈ 𝑥)))
143	121, 142	bitrid 283	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) → (𝑏 ∈ (𝑘 ∖ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ↔ (𝑏 ∈ 𝑘 ∧ ∃𝑎 ∈ 𝑠 ¬ ⟨𝑎, 𝑏⟩ ∈ 𝑥)))
144	112, 120, 143	3bitr4d 311	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) → (𝑏 ∈ ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ↔ 𝑏 ∈ (𝑘 ∖ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})))
145	144	eqrdv 2733	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) → ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) = (𝑘 ∖ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}))
146	74, 76, 145	syl2anc 585	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) = (𝑘 ∖ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}))
147		difin 4223	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∖ (𝑘 ∩ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})) = (𝑘 ∖ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})
148	65	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → 𝑆 ∈ Top)
149	24	restuni 23108	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑆 ∈ Top ∧ 𝑘 ⊆ ∪ 𝑆) → 𝑘 = ∪ (𝑆 ↾t 𝑘))
150	148, 76, 149	syl2anc 585	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → 𝑘 = ∪ (𝑆 ↾t 𝑘))
151	150	difeq1d 4076	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → (𝑘 ∖ (𝑘 ∩ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})) = (∪ (𝑆 ↾t 𝑘) ∖ (𝑘 ∩ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})))
152	147, 151	eqtr3id 2784	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → (𝑘 ∖ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) = (∪ (𝑆 ↾t 𝑘) ∖ (𝑘 ∩ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})))
153	146, 152	eqtrd 2770	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) = (∪ (𝑆 ↾t 𝑘) ∖ (𝑘 ∩ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})))
154	15	ad2antrr 727	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → 𝑆 ∈ (ran 𝑘Gen ∩ Haus))
155	154	elin2d 4156	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → 𝑆 ∈ Haus)
156		df-ima 5636	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) = ran ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) ↾ ((𝑠 × 𝑘) ∖ 𝑥))
157		resres 5950	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) ↾ ((𝑠 × 𝑘) ∖ 𝑥)) = (2nd ↾ ((∪ 𝑅 × ∪ 𝑆) ∩ ((𝑠 × 𝑘) ∖ 𝑥)))
158		inss2 4189	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((∪ 𝑅 × ∪ 𝑆) ∩ ((𝑠 × 𝑘) ∖ 𝑥)) ⊆ ((𝑠 × 𝑘) ∖ 𝑥)
159	158, 116	sstri 3942	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((∪ 𝑅 × ∪ 𝑆) ∩ ((𝑠 × 𝑘) ∖ 𝑥)) ⊆ (𝑠 × 𝑘)
160		ssres2 5962	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((∪ 𝑅 × ∪ 𝑆) ∩ ((𝑠 × 𝑘) ∖ 𝑥)) ⊆ (𝑠 × 𝑘) → (2nd ↾ ((∪ 𝑅 × ∪ 𝑆) ∩ ((𝑠 × 𝑘) ∖ 𝑥))) ⊆ (2nd ↾ (𝑠 × 𝑘)))
161	159, 160	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (2nd ↾ ((∪ 𝑅 × ∪ 𝑆) ∩ ((𝑠 × 𝑘) ∖ 𝑥))) ⊆ (2nd ↾ (𝑠 × 𝑘))
162	157, 161	eqsstri 3979	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) ↾ ((𝑠 × 𝑘) ∖ 𝑥)) ⊆ (2nd ↾ (𝑠 × 𝑘))
163	162	rnssi 5888	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ran ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) ↾ ((𝑠 × 𝑘) ∖ 𝑥)) ⊆ ran (2nd ↾ (𝑠 × 𝑘))
164	156, 163	eqsstri 3979	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ⊆ ran (2nd ↾ (𝑠 × 𝑘))
165		f2ndres 7958	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (2nd ↾ (𝑠 × 𝑘)):(𝑠 × 𝑘)⟶𝑘
166		frn 6668	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((2nd ↾ (𝑠 × 𝑘)):(𝑠 × 𝑘)⟶𝑘 → ran (2nd ↾ (𝑠 × 𝑘)) ⊆ 𝑘)
167	165, 166	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ran (2nd ↾ (𝑠 × 𝑘)) ⊆ 𝑘
168	164, 167	sstri 3942	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ⊆ 𝑘
169	168, 76	sstrid 3944	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ⊆ ∪ 𝑆)
170	12	ad2antrr 727	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → 𝑅 ∈ (TopOn‘∪ 𝑅))
171	148, 17	sylib 218	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → 𝑆 ∈ (TopOn‘∪ 𝑆))
172		tx2cn 23556	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑅 ∈ (TopOn‘∪ 𝑅) ∧ 𝑆 ∈ (TopOn‘∪ 𝑆)) → (2nd ↾ (∪ 𝑅 × ∪ 𝑆)) ∈ ((𝑅 ×t 𝑆) Cn 𝑆))
173	170, 171, 172	syl2anc 585	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → (2nd ↾ (∪ 𝑅 × ∪ 𝑆)) ∈ ((𝑅 ×t 𝑆) Cn 𝑆))
174	27	ad2antrr 727	. . . . . . . . . . . . . . . . . . . . . . 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 3443	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 𝑠 ∈ V
177		vex 3443	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 𝑘 ∈ V
178	176, 177	xpex 7698	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑠 × 𝑘) ∈ V
179	178	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → (𝑠 × 𝑘) ∈ V)
180		restabs 23111	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑅 ×t 𝑆) ∈ Top ∧ ((𝑠 × 𝑘) ∖ 𝑥) ⊆ (𝑠 × 𝑘) ∧ (𝑠 × 𝑘) ∈ V) → (((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ↾t ((𝑠 × 𝑘) ∖ 𝑥)) = ((𝑅 ×t 𝑆) ↾t ((𝑠 × 𝑘) ∖ 𝑥)))
181	174, 175, 179, 180	syl3anc 1374	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → (((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ↾t ((𝑠 × 𝑘) ∖ 𝑥)) = ((𝑅 ×t 𝑆) ↾t ((𝑠 × 𝑘) ∖ 𝑥)))
182	64	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . 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 771	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → 𝑘 ∈ 𝒫 ∪ 𝑆)
186		txrest 23577	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑠 ∈ V ∧ 𝑘 ∈ 𝒫 ∪ 𝑆)) → ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) = ((𝑅 ↾t 𝑠) ×t (𝑆 ↾t 𝑘)))
187	182, 183, 184, 185, 186	syl22anc 839	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) = ((𝑅 ↾t 𝑠) ×t (𝑆 ↾t 𝑘)))
188		simprr3 1225	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → (𝑅 ↾t 𝑠) ∈ Comp)
189	188	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → (𝑅 ↾t 𝑠) ∈ Comp)
190		simprr 773	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → (𝑆 ↾t 𝑘) ∈ Comp)
191		txcmp 23589	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑅 ↾t 𝑠) ∈ Comp ∧ (𝑆 ↾t 𝑘) ∈ Comp) → ((𝑅 ↾t 𝑠) ×t (𝑆 ↾t 𝑘)) ∈ Comp)
192	189, 190, 191	syl2anc 585	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → ((𝑅 ↾t 𝑠) ×t (𝑆 ↾t 𝑘)) ∈ Comp)
193	187, 192	eqeltrd 2835	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ∈ Comp)
194		difin 4223	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑠 × 𝑘) ∖ ((𝑠 × 𝑘) ∩ 𝑥)) = ((𝑠 × 𝑘) ∖ 𝑥)
195	74, 76, 117	syl2anc 585	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → (𝑠 × 𝑘) ⊆ (∪ 𝑅 × ∪ 𝑆))
196	182, 148, 25	syl2anc 585	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → (∪ 𝑅 × ∪ 𝑆) = ∪ (𝑅 ×t 𝑆))
197	195, 196	sseqtrd 3969	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → (𝑠 × 𝑘) ⊆ ∪ (𝑅 ×t 𝑆))
198	28	restuni 23108	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑅 ×t 𝑆) ∈ Top ∧ (𝑠 × 𝑘) ⊆ ∪ (𝑅 ×t 𝑆)) → (𝑠 × 𝑘) = ∪ ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)))
199	174, 197, 198	syl2anc 585	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → (𝑠 × 𝑘) = ∪ ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)))
200	199	difeq1d 4076	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → ((𝑠 × 𝑘) ∖ ((𝑠 × 𝑘) ∩ 𝑥)) = (∪ ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ∖ ((𝑠 × 𝑘) ∩ 𝑥)))
201	194, 200	eqtr3id 2784	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → ((𝑠 × 𝑘) ∖ 𝑥) = (∪ ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ∖ ((𝑠 × 𝑘) ∩ 𝑥)))
202		resttop 23106	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑅 ×t 𝑆) ∈ Top ∧ (𝑠 × 𝑘) ∈ V) → ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ∈ Top)
203	174, 178, 202	sylancl 587	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ∈ Top)
204		incom 4160	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑠 × 𝑘) ∩ 𝑥) = (𝑥 ∩ (𝑠 × 𝑘))
205	20	ad2antrr 727	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆)))
206		kgeni 23483	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆)) ∧ ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ∈ Comp) → (𝑥 ∩ (𝑠 × 𝑘)) ∈ ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)))
207	205, 193, 206	syl2anc 585	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → (𝑥 ∩ (𝑠 × 𝑘)) ∈ ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)))
208	204, 207	eqeltrid 2839	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → ((𝑠 × 𝑘) ∩ 𝑥) ∈ ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)))
209		eqid 2735	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ∪ ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) = ∪ ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘))
210	209	opncld 22979	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ∈ Top ∧ ((𝑠 × 𝑘) ∩ 𝑥) ∈ ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘))) → (∪ ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ∖ ((𝑠 × 𝑘) ∩ 𝑥)) ∈ (Clsd‘((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘))))
211	203, 208, 210	syl2anc 585	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → (∪ ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ∖ ((𝑠 × 𝑘) ∩ 𝑥)) ∈ (Clsd‘((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘))))
212	201, 211	eqeltrd 2835	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → ((𝑠 × 𝑘) ∖ 𝑥) ∈ (Clsd‘((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘))))
213		cmpcld 23348	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ∈ Comp ∧ ((𝑠 × 𝑘) ∖ 𝑥) ∈ (Clsd‘((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)))) → (((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ↾t ((𝑠 × 𝑘) ∖ 𝑥)) ∈ Comp)
214	193, 212, 213	syl2anc 585	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → (((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ↾t ((𝑠 × 𝑘) ∖ 𝑥)) ∈ Comp)
215	181, 214	eqeltrrd 2836	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → ((𝑅 ×t 𝑆) ↾t ((𝑠 × 𝑘) ∖ 𝑥)) ∈ Comp)
216		imacmp 23343	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) ∈ ((𝑅 ×t 𝑆) Cn 𝑆) ∧ ((𝑅 ×t 𝑆) ↾t ((𝑠 × 𝑘) ∖ 𝑥)) ∈ Comp) → (𝑆 ↾t ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥))) ∈ Comp)
217	173, 215, 216	syl2anc 585	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → (𝑆 ↾t ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥))) ∈ Comp)
218	24	hauscmp 23353	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑆 ∈ Haus ∧ ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ⊆ ∪ 𝑆 ∧ (𝑆 ↾t ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥))) ∈ Comp) → ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ∈ (Clsd‘𝑆))
219	155, 169, 217, 218	syl3anc 1374	. . . . . . . . . . . . . . . . . . 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 23119	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑘 ⊆ ∪ 𝑆 ∧ ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ∈ (Clsd‘𝑆) ∧ ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ⊆ 𝑘) → ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ∈ (Clsd‘(𝑆 ↾t 𝑘)))
222	76, 219, 220, 221	syl3anc 1374	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ∈ (Clsd‘(𝑆 ↾t 𝑘)))
223	153, 222	eqeltrrd 2836	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → (∪ (𝑆 ↾t 𝑘) ∖ (𝑘 ∩ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})) ∈ (Clsd‘(𝑆 ↾t 𝑘)))
224		resttop 23106	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑆 ∈ Top ∧ 𝑘 ∈ 𝒫 ∪ 𝑆) → (𝑆 ↾t 𝑘) ∈ Top)
225	148, 185, 224	syl2anc 585	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → (𝑆 ↾t 𝑘) ∈ Top)
226		inss1 4188	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 ∩ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ⊆ 𝑘
227	226, 150	sseqtrid 3975	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → (𝑘 ∩ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ⊆ ∪ (𝑆 ↾t 𝑘))
228		eqid 2735	. . . . . . . . . . . . . . . . . . 19 ⊢ ∪ (𝑆 ↾t 𝑘) = ∪ (𝑆 ↾t 𝑘)
229	228	isopn2 22978	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑆 ↾t 𝑘) ∈ Top ∧ (𝑘 ∩ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ⊆ ∪ (𝑆 ↾t 𝑘)) → ((𝑘 ∩ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ∈ (𝑆 ↾t 𝑘) ↔ (∪ (𝑆 ↾t 𝑘) ∖ (𝑘 ∩ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})) ∈ (Clsd‘(𝑆 ↾t 𝑘))))
230	225, 227, 229	syl2anc 585	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → ((𝑘 ∩ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ∈ (𝑆 ↾t 𝑘) ↔ (∪ (𝑆 ↾t 𝑘) ∖ (𝑘 ∩ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})) ∈ (Clsd‘(𝑆 ↾t 𝑘))))
231	223, 230	mpbird 257	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → (𝑘 ∩ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ∈ (𝑆 ↾t 𝑘))
232	69, 231	eqeltrid 2839	. . . . . . . . . . . . . . 15 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → ({𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ∩ 𝑘) ∈ (𝑆 ↾t 𝑘))
233	232	expr 456	. . . . . . . . . . . . . 14 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ 𝑘 ∈ 𝒫 ∪ 𝑆) → ((𝑆 ↾t 𝑘) ∈ Comp → ({𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ∩ 𝑘) ∈ (𝑆 ↾t 𝑘)))
234	233	ralrimiva 3127	. . . . . . . . . . . . 13 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → ∀𝑘 ∈ 𝒫 ∪ 𝑆((𝑆 ↾t 𝑘) ∈ Comp → ({𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ∩ 𝑘) ∈ (𝑆 ↾t 𝑘)))
235	65, 17	sylib 218	. . . . . . . . . . . . . 14 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → 𝑆 ∈ (TopOn‘∪ 𝑆))
236		elkgen 23482	. . . . . . . . . . . . . 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 714	. . . . . . . . . . . 12 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ∈ (𝑘Gen‘𝑆))
239	15	adantr 480	. . . . . . . . . . . . . 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 23493	. . . . . . . . . . . . 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 2837	. . . . . . . . . . 11 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ∈ 𝑆)
244		txopn 23548	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑢 ∈ 𝑅 ∧ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ∈ 𝑆)) → (𝑢 × {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ∈ (𝑅 ×t 𝑆))
245	64, 65, 66, 243, 244	syl22anc 839	. . . . . . . . . 10 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → (𝑢 × {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ∈ (𝑅 ×t 𝑆))
246	59	adantr 480	. . . . . . . . . . 11 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → 𝑦 = ⟨(1st ‘𝑦), (2nd ‘𝑦)⟩)
247		simprr1 1223	. . . . . . . . . . . 12 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → (1st ‘𝑦) ∈ 𝑢)
248		sneq 4589	. . . . . . . . . . . . . . 15 ⊢ (𝑣 = (2nd ‘𝑦) → {𝑣} = {(2nd ‘𝑦)})
249	248	xpeq2d 5653	. . . . . . . . . . . . . 14 ⊢ (𝑣 = (2nd ‘𝑦) → (𝑠 × {𝑣}) = (𝑠 × {(2nd ‘𝑦)}))
250	249	sseq1d 3964	. . . . . . . . . . . . 13 ⊢ (𝑣 = (2nd ‘𝑦) → ((𝑠 × {𝑣}) ⊆ 𝑥 ↔ (𝑠 × {(2nd ‘𝑦)}) ⊆ 𝑥))
251	34	adantr 480	. . . . . . . . . . . . 13 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → (2nd ‘𝑦) ∈ ∪ 𝑆)
252		relxp 5641	. . . . . . . . . . . . . . 15 ⊢ Rel (𝑠 × {(2nd ‘𝑦)})
253	252	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → Rel (𝑠 × {(2nd ‘𝑦)}))
254		opelxp 5659	. . . . . . . . . . . . . . 15 ⊢ (⟨𝑎, 𝑏⟩ ∈ (𝑠 × {(2nd ‘𝑦)}) ↔ (𝑎 ∈ 𝑠 ∧ 𝑏 ∈ {(2nd ‘𝑦)}))
255	71	sselda 3932	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ 𝑎 ∈ 𝑠) → 𝑎 ∈ {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥})
256		opeq1 4828	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑡 = 𝑎 → ⟨𝑡, (2nd ‘𝑦)⟩ = ⟨𝑎, (2nd ‘𝑦)⟩)
257	256	eleq1d 2820	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 = 𝑎 → (⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥 ↔ ⟨𝑎, (2nd ‘𝑦)⟩ ∈ 𝑥))
258	257	elrab 3645	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 ∈ {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ↔ (𝑎 ∈ ∪ 𝑅 ∧ ⟨𝑎, (2nd ‘𝑦)⟩ ∈ 𝑥))
259	258	simprbi 496	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 ∈ {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} → ⟨𝑎, (2nd ‘𝑦)⟩ ∈ 𝑥)
260	255, 259	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ 𝑎 ∈ 𝑠) → ⟨𝑎, (2nd ‘𝑦)⟩ ∈ 𝑥)
261		elsni 4596	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 ∈ {(2nd ‘𝑦)} → 𝑏 = (2nd ‘𝑦))
262	261	opeq2d 4835	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 ∈ {(2nd ‘𝑦)} → ⟨𝑎, 𝑏⟩ = ⟨𝑎, (2nd ‘𝑦)⟩)
263	262	eleq1d 2820	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 ∈ {(2nd ‘𝑦)} → (⟨𝑎, 𝑏⟩ ∈ 𝑥 ↔ ⟨𝑎, (2nd ‘𝑦)⟩ ∈ 𝑥))
264	260, 263	syl5ibrcom 247	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ 𝑎 ∈ 𝑠) → (𝑏 ∈ {(2nd ‘𝑦)} → ⟨𝑎, 𝑏⟩ ∈ 𝑥))
265	264	expimpd 453	. . . . . . . . . . . . . . 15 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → ((𝑎 ∈ 𝑠 ∧ 𝑏 ∈ {(2nd ‘𝑦)}) → ⟨𝑎, 𝑏⟩ ∈ 𝑥))
266	254, 265	biimtrid 242	. . . . . . . . . . . . . 14 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → (⟨𝑎, 𝑏⟩ ∈ (𝑠 × {(2nd ‘𝑦)}) → ⟨𝑎, 𝑏⟩ ∈ 𝑥))
267	253, 266	relssdv 5736	. . . . . . . . . . . . 13 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → (𝑠 × {(2nd ‘𝑦)}) ⊆ 𝑥)
268	250, 251, 267	elrabd 3647	. . . . . . . . . . . 12 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → (2nd ‘𝑦) ∈ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})
269	247, 268	opelxpd 5662	. . . . . . . . . . 11 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → ⟨(1st ‘𝑦), (2nd ‘𝑦)⟩ ∈ (𝑢 × {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}))
270	246, 269	eqeltrd 2835	. . . . . . . . . 10 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → 𝑦 ∈ (𝑢 × {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}))
271		relxp 5641	. . . . . . . . . . . 12 ⊢ Rel (𝑢 × {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})
272	271	a1i 11	. . . . . . . . . . 11 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → Rel (𝑢 × {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}))
273		opelxp 5659	. . . . . . . . . . . 12 ⊢ (⟨𝑎, 𝑏⟩ ∈ (𝑢 × {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ↔ (𝑎 ∈ 𝑢 ∧ 𝑏 ∈ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}))
274	126	elrab 3645	. . . . . . . . . . . . . . 15 ⊢ (𝑏 ∈ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ↔ (𝑏 ∈ ∪ 𝑆 ∧ (𝑠 × {𝑏}) ⊆ 𝑥))
275	274	simprbi 496	. . . . . . . . . . . . . 14 ⊢ (𝑏 ∈ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} → (𝑠 × {𝑏}) ⊆ 𝑥)
276		simprr2 1224	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → 𝑢 ⊆ 𝑠)
277	276	sselda 3932	. . . . . . . . . . . . . . 15 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ 𝑎 ∈ 𝑢) → 𝑎 ∈ 𝑠)
278		vsnid 4619	. . . . . . . . . . . . . . 15 ⊢ 𝑏 ∈ {𝑏}
279		opelxpi 5660	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 ∈ 𝑠 ∧ 𝑏 ∈ {𝑏}) → ⟨𝑎, 𝑏⟩ ∈ (𝑠 × {𝑏}))
280	277, 278, 279	sylancl 587	. . . . . . . . . . . . . 14 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ 𝑎 ∈ 𝑢) → ⟨𝑎, 𝑏⟩ ∈ (𝑠 × {𝑏}))
281		ssel 3926	. . . . . . . . . . . . . 14 ⊢ ((𝑠 × {𝑏}) ⊆ 𝑥 → (⟨𝑎, 𝑏⟩ ∈ (𝑠 × {𝑏}) → ⟨𝑎, 𝑏⟩ ∈ 𝑥))
282	275, 280, 281	syl2imc 41	. . . . . . . . . . . . 13 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ 𝑎 ∈ 𝑢) → (𝑏 ∈ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} → ⟨𝑎, 𝑏⟩ ∈ 𝑥))
283	282	expimpd 453	. . . . . . . . . . . 12 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → ((𝑎 ∈ 𝑢 ∧ 𝑏 ∈ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) → ⟨𝑎, 𝑏⟩ ∈ 𝑥))
284	273, 283	biimtrid 242	. . . . . . . . . . 11 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → (⟨𝑎, 𝑏⟩ ∈ (𝑢 × {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) → ⟨𝑎, 𝑏⟩ ∈ 𝑥))
285	272, 284	relssdv 5736	. . . . . . . . . 10 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → (𝑢 × {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ⊆ 𝑥)
286		eleq2 2824	. . . . . . . . . . . 12 ⊢ (𝑡 = (𝑢 × {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) → (𝑦 ∈ 𝑡 ↔ 𝑦 ∈ (𝑢 × {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})))
287		sseq1 3958	. . . . . . . . . . . 12 ⊢ (𝑡 = (𝑢 × {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) → (𝑡 ⊆ 𝑥 ↔ (𝑢 × {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ⊆ 𝑥))
288	286, 287	anbi12d 633	. . . . . . . . . . 11 ⊢ (𝑡 = (𝑢 × {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) → ((𝑦 ∈ 𝑡 ∧ 𝑡 ⊆ 𝑥) ↔ (𝑦 ∈ (𝑢 × {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ∧ (𝑢 × {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ⊆ 𝑥)))
289	288	rspcev 3575	. . . . . . . . . 10 ⊢ (((𝑢 × {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ∈ (𝑅 ×t 𝑆) ∧ (𝑦 ∈ (𝑢 × {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ∧ (𝑢 × {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ⊆ 𝑥)) → ∃𝑡 ∈ (𝑅 ×t 𝑆)(𝑦 ∈ 𝑡 ∧ 𝑡 ⊆ 𝑥))
290	245, 270, 285, 289	syl12anc 837	. . . . . . . . 9 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → ∃𝑡 ∈ (𝑅 ×t 𝑆)(𝑦 ∈ 𝑡 ∧ 𝑡 ⊆ 𝑥))
291	290	expr 456	. . . . . . . 8 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ (𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅)) → (((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp) → ∃𝑡 ∈ (𝑅 ×t 𝑆)(𝑦 ∈ 𝑡 ∧ 𝑡 ⊆ 𝑥)))
292	291	rexlimdvva 3192	. . . . . . 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 3127	. . . . 5 ⊢ (((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) → ∀𝑦 ∈ 𝑥 ∃𝑡 ∈ (𝑅 ×t 𝑆)(𝑦 ∈ 𝑡 ∧ 𝑡 ⊆ 𝑥))
295	6	adantr 480	. . . . . 6 ⊢ (((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) → (𝑅 ×t 𝑆) ∈ Top)
296		eltop2 22921	. . . . . 6 ⊢ ((𝑅 ×t 𝑆) ∈ Top → (𝑥 ∈ (𝑅 ×t 𝑆) ↔ ∀𝑦 ∈ 𝑥 ∃𝑡 ∈ (𝑅 ×t 𝑆)(𝑦 ∈ 𝑡 ∧ 𝑡 ⊆ 𝑥)))
297	295, 296	syl 17	. . . . 5 ⊢ (((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) → (𝑥 ∈ (𝑅 ×t 𝑆) ↔ ∀𝑦 ∈ 𝑥 ∃𝑡 ∈ (𝑅 ×t 𝑆)(𝑦 ∈ 𝑡 ∧ 𝑡 ⊆ 𝑥)))
298	294, 297	mpbird 257	. . . 4 ⊢ (((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) → 𝑥 ∈ (𝑅 ×t 𝑆))
299	298	ex 412	. . 3 ⊢ ((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) → (𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆)) → 𝑥 ∈ (𝑅 ×t 𝑆)))
300	299	ssrdv 3938	. 2 ⊢ ((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) → (𝑘Gen‘(𝑅 ×t 𝑆)) ⊆ (𝑅 ×t 𝑆))
301		iskgen2 23494	. 2 ⊢ ((𝑅 ×t 𝑆) ∈ ran 𝑘Gen ↔ ((𝑅 ×t 𝑆) ∈ Top ∧ (𝑘Gen‘(𝑅 ×t 𝑆)) ⊆ (𝑅 ×t 𝑆)))
302	6, 300, 301	sylanbrc 584	1 ⊢ ((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) → (𝑅 ×t 𝑆) ∈ ran 𝑘Gen)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114  ∀wral 3050  ∃wrex 3059  {crab 3398  Vcvv 3439   ∖ cdif 3897   ∩ cin 3899   ⊆ wss 3900  𝒫 cpw 4553  {csn 4579  ⟨cop 4585  ∪ cuni 4862   ↦ cmpt 5178   I cid 5517   × cxp 5621  ^◡ccnv 5622  ran crn 5624   ↾ cres 5625   “ cima 5626  Rel wrel 5628   Fn wfn 6486  ⟶wf 6487  ‘cfv 6491  (class class class)co 7358  1^st c1st 7931  2^nd c2nd 7932   ↾_t crest 17342  Topctop 22839  TopOnctopon 22856  Clsdccld 22962   Cn ccn 23170  Hauscha 23254  Compccmp 23332  𝑛-Locally cnlly 23411  𝑘Genckgen 23479   ×_t ctx 23506

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2183  ax-ext 2707  ax-rep 5223  ax-sep 5240  ax-nul 5250  ax-pow 5309  ax-pr 5376  ax-un 7680

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2538  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2810  df-nfc 2884  df-ne 2932  df-ral 3051  df-rex 3060  df-reu 3350  df-rab 3399  df-v 3441  df-sbc 3740  df-csb 3849  df-dif 3903  df-un 3905  df-in 3907  df-ss 3917  df-pss 3920  df-nul 4285  df-if 4479  df-pw 4555  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-int 4902  df-iun 4947  df-iin 4948  df-br 5098  df-opab 5160  df-mpt 5179  df-tr 5205  df-id 5518  df-eprel 5523  df-po 5531  df-so 5532  df-fr 5576  df-we 5578  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634  df-res 5635  df-ima 5636  df-ord 6319  df-on 6320  df-lim 6321  df-suc 6322  df-iota 6447  df-fun 6493  df-fn 6494  df-f 6495  df-f1 6496  df-fo 6497  df-f1o 6498  df-fv 6499  df-ov 7361  df-oprab 7362  df-mpo 7363  df-om 7809  df-1st 7933  df-2nd 7934  df-1o 8397  df-2o 8398  df-map 8767  df-en 8886  df-dom 8887  df-fin 8889  df-fi 9316  df-rest 17344  df-topgen 17365  df-top 22840  df-topon 22857  df-bases 22892  df-cld 22965  df-ntr 22966  df-cls 22967  df-nei 23044  df-cn 23173  df-cnp 23174  df-haus 23261  df-cmp 23333  df-nlly 23413  df-kgen 23480  df-tx 23508

This theorem is referenced by: (None)