Theorem txkgen 23910

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 23731	. . 3 ⊢ (𝑅 ∈ 𝑛-Locally Comp → 𝑅 ∈ Top)
2		elinel1 4147	. . . 4 ⊢ (𝑆 ∈ (ran 𝑘Gen ∩ Haus) → 𝑆 ∈ ran 𝑘Gen)
3		kgentop 23800	. . . 4 ⊢ (𝑆 ∈ ran 𝑘Gen → 𝑆 ∈ Top)
4	2, 3	syl 18	. . 3 ⊢ (𝑆 ∈ (ran 𝑘Gen ∩ Haus) → 𝑆 ∈ Top)
5		txtop 23827	. . 3 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑅 ×t 𝑆) ∈ Top)
6	1, 4, 5	syl2an 608	. 2 ⊢ ((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) → (𝑅 ×t 𝑆) ∈ Top)
7		simplll 787	. . . . . . . 8 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → 𝑅 ∈ 𝑛-Locally Comp)
8		eqid 2760	. . . . . . . . . 10 ⊢ (𝑡 ∈ ∪ 𝑅 ↦ ⟨𝑡, (2nd ‘𝑦)⟩) = (𝑡 ∈ ∪ 𝑅 ↦ ⟨𝑡, (2nd ‘𝑦)⟩)
9	8	mptpreima 6236	. . . . . . . . 9 ⊢ (◡(𝑡 ∈ ∪ 𝑅 ↦ ⟨𝑡, (2nd ‘𝑦)⟩) “ 𝑥) = {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥}
10	1	ad3antrrr 743	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → 𝑅 ∈ Top)
11		toptopon2 23175	. . . . . . . . . . . . . 14 ⊢ (𝑅 ∈ Top ↔ 𝑅 ∈ (TopOn‘∪ 𝑅))
12	10, 11	sylib 221	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → 𝑅 ∈ (TopOn‘∪ 𝑅))
13		idcn 23514	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ (TopOn‘∪ 𝑅) → ( I ↾ ∪ 𝑅) ∈ (𝑅 Cn 𝑅))
14	12, 13	syl 18	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → ( I ↾ ∪ 𝑅) ∈ (𝑅 Cn 𝑅))
15		simpllr 788	. . . . . . . . . . . . . . 15 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → 𝑆 ∈ (ran 𝑘Gen ∩ Haus))
16	15, 4	syl 18	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → 𝑆 ∈ Top)
17		toptopon2 23175	. . . . . . . . . . . . . 14 ⊢ (𝑆 ∈ Top ↔ 𝑆 ∈ (TopOn‘∪ 𝑆))
18	16, 17	sylib 221	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → 𝑆 ∈ (TopOn‘∪ 𝑆))
19		simpr 490	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ 𝑥)
20		simplr 781	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆)))
21		elunii 4872	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) → 𝑦 ∈ ∪ (𝑘Gen‘(𝑅 ×t 𝑆)))
22	19, 20, 21	syl2anc 596	. . . . . . . . . . . . . . 15 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ ∪ (𝑘Gen‘(𝑅 ×t 𝑆)))
23		eqid 2760	. . . . . . . . . . . . . . . . . 18 ⊢ ∪ 𝑅 = ∪ 𝑅
24		eqid 2760	. . . . . . . . . . . . . . . . . 18 ⊢ ∪ 𝑆 = ∪ 𝑆
25	23, 24	txuni 23850	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (∪ 𝑅 × ∪ 𝑆) = ∪ (𝑅 ×t 𝑆))
26	10, 16, 25	syl2anc 596	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → (∪ 𝑅 × ∪ 𝑆) = ∪ (𝑅 ×t 𝑆))
27	10, 16, 5	syl2anc 596	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → (𝑅 ×t 𝑆) ∈ Top)
28		eqid 2760	. . . . . . . . . . . . . . . . . 18 ⊢ ∪ (𝑅 ×t 𝑆) = ∪ (𝑅 ×t 𝑆)
29	28	kgenuni 23797	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 ×t 𝑆) ∈ Top → ∪ (𝑅 ×t 𝑆) = ∪ (𝑘Gen‘(𝑅 ×t 𝑆)))
30	27, 29	syl 18	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → ∪ (𝑅 ×t 𝑆) = ∪ (𝑘Gen‘(𝑅 ×t 𝑆)))
31	26, 30	eqtrd 2795	. . . . . . . . . . . . . . 15 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → (∪ 𝑅 × ∪ 𝑆) = ∪ (𝑘Gen‘(𝑅 ×t 𝑆)))
32	22, 31	eleqtrrd 2863	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ (∪ 𝑅 × ∪ 𝑆))
33		xp2nd 8025	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ (∪ 𝑅 × ∪ 𝑆) → (2nd ‘𝑦) ∈ ∪ 𝑆)
34	32, 33	syl 18	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → (2nd ‘𝑦) ∈ ∪ 𝑆)
35		cnconst2 23540	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ (TopOn‘∪ 𝑅) ∧ 𝑆 ∈ (TopOn‘∪ 𝑆) ∧ (2nd ‘𝑦) ∈ ∪ 𝑆) → (∪ 𝑅 × {(2nd ‘𝑦)}) ∈ (𝑅 Cn 𝑆))
36	12, 18, 34, 35	syl3anc 1398	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → (∪ 𝑅 × {(2nd ‘𝑦)}) ∈ (𝑅 Cn 𝑆))
37		fvresi 7174	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 ∈ ∪ 𝑅 → (( I ↾ ∪ 𝑅)‘𝑡) = 𝑡)
38		fvex 6894	. . . . . . . . . . . . . . . . 17 ⊢ (2nd ‘𝑦) ∈ V
39	38	fvconst2 7206	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 ∈ ∪ 𝑅 → ((∪ 𝑅 × {(2nd ‘𝑦)})‘𝑡) = (2nd ‘𝑦))
40	37, 39	opeq12d 4841	. . . . . . . . . . . . . . 15 ⊢ (𝑡 ∈ ∪ 𝑅 → ⟨(( I ↾ ∪ 𝑅)‘𝑡), ((∪ 𝑅 × {(2nd ‘𝑦)})‘𝑡)⟩ = ⟨𝑡, (2nd ‘𝑦)⟩)
41	40	mpteq2ia 5200	. . . . . . . . . . . . . 14 ⊢ (𝑡 ∈ ∪ 𝑅 ↦ ⟨(( I ↾ ∪ 𝑅)‘𝑡), ((∪ 𝑅 × {(2nd ‘𝑦)})‘𝑡)⟩) = (𝑡 ∈ ∪ 𝑅 ↦ ⟨𝑡, (2nd ‘𝑦)⟩)
42	41	eqcomi 2769	. . . . . . . . . . . . 13 ⊢ (𝑡 ∈ ∪ 𝑅 ↦ ⟨𝑡, (2nd ‘𝑦)⟩) = (𝑡 ∈ ∪ 𝑅 ↦ ⟨(( I ↾ ∪ 𝑅)‘𝑡), ((∪ 𝑅 × {(2nd ‘𝑦)})‘𝑡)⟩)
43	23, 42	txcnmpt 23882	. . . . . . . . . . . 12 ⊢ ((( I ↾ ∪ 𝑅) ∈ (𝑅 Cn 𝑅) ∧ (∪ 𝑅 × {(2nd ‘𝑦)}) ∈ (𝑅 Cn 𝑆)) → (𝑡 ∈ ∪ 𝑅 ↦ ⟨𝑡, (2nd ‘𝑦)⟩) ∈ (𝑅 Cn (𝑅 ×t 𝑆)))
44	14, 36, 43	syl2anc 596	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → (𝑡 ∈ ∪ 𝑅 ↦ ⟨𝑡, (2nd ‘𝑦)⟩) ∈ (𝑅 Cn (𝑅 ×t 𝑆)))
45		llycmpkgen 23810	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ 𝑛-Locally Comp → 𝑅 ∈ ran 𝑘Gen)
46	45	ad3antrrr 743	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → 𝑅 ∈ ran 𝑘Gen)
47	6	ad2antrr 739	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → (𝑅 ×t 𝑆) ∈ Top)
48		kgencn3 23816	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ ran 𝑘Gen ∧ (𝑅 ×t 𝑆) ∈ Top) → (𝑅 Cn (𝑅 ×t 𝑆)) = (𝑅 Cn (𝑘Gen‘(𝑅 ×t 𝑆))))
49	46, 47, 48	syl2anc 596	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → (𝑅 Cn (𝑅 ×t 𝑆)) = (𝑅 Cn (𝑘Gen‘(𝑅 ×t 𝑆))))
50	44, 49	eleqtrd 2862	. . . . . . . . . 10 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → (𝑡 ∈ ∪ 𝑅 ↦ ⟨𝑡, (2nd ‘𝑦)⟩) ∈ (𝑅 Cn (𝑘Gen‘(𝑅 ×t 𝑆))))
51		cnima 23522	. . . . . . . . . 10 ⊢ (((𝑡 ∈ ∪ 𝑅 ↦ ⟨𝑡, (2nd ‘𝑦)⟩) ∈ (𝑅 Cn (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) → (◡(𝑡 ∈ ∪ 𝑅 ↦ ⟨𝑡, (2nd ‘𝑦)⟩) “ 𝑥) ∈ 𝑅)
52	50, 20, 51	syl2anc 596	. . . . . . . . 9 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → (◡(𝑡 ∈ ∪ 𝑅 ↦ ⟨𝑡, (2nd ‘𝑦)⟩) “ 𝑥) ∈ 𝑅)
53	9, 52	eqeltrrid 2865	. . . . . . . 8 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∈ 𝑅)
54		opeq1 4833	. . . . . . . . . 10 ⊢ (𝑡 = (1st ‘𝑦) → ⟨𝑡, (2nd ‘𝑦)⟩ = ⟨(1st ‘𝑦), (2nd ‘𝑦)⟩)
55	54	eleq1d 2845	. . . . . . . . 9 ⊢ (𝑡 = (1st ‘𝑦) → (⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥 ↔ ⟨(1st ‘𝑦), (2nd ‘𝑦)⟩ ∈ 𝑥))
56		xp1st 8024	. . . . . . . . . 10 ⊢ (𝑦 ∈ (∪ 𝑅 × ∪ 𝑆) → (1st ‘𝑦) ∈ ∪ 𝑅)
57	32, 56	syl 18	. . . . . . . . 9 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → (1st ‘𝑦) ∈ ∪ 𝑅)
58		1st2nd2 8031	. . . . . . . . . . 11 ⊢ (𝑦 ∈ (∪ 𝑅 × ∪ 𝑆) → 𝑦 = ⟨(1st ‘𝑦), (2nd ‘𝑦)⟩)
59	32, 58	syl 18	. . . . . . . . . 10 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → 𝑦 = ⟨(1st ‘𝑦), (2nd ‘𝑦)⟩)
60	59, 19	eqeltrrd 2861	. . . . . . . . 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 23734	. . . . . . . 8 ⊢ ((𝑅 ∈ 𝑛-Locally Comp ∧ {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∈ 𝑅 ∧ (1st ‘𝑦) ∈ {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥}) → ∃𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥}∃𝑢 ∈ 𝑅 ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))
63	7, 53, 61, 62	syl3anc 1398	. . . . . . 7 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → ∃𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥}∃𝑢 ∈ 𝑅 ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))
64	10	adantr 486	. . . . . . . . . . 11 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → 𝑅 ∈ Top)
65	16	adantr 486	. . . . . . . . . . 11 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → 𝑆 ∈ Top)
66		simprlr 792	. . . . . . . . . . 11 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → 𝑢 ∈ 𝑅)
67		ssrab2 4028	. . . . . . . . . . . . . 14 ⊢ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ⊆ ∪ 𝑆
68	67	a1i 11	. . . . . . . . . . . . 13 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ⊆ ∪ 𝑆)
69		incom 4155	. . . . . . . . . . . . . . . 16 ⊢ ({𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ∩ 𝑘) = (𝑘 ∩ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})
70		simprll 791	. . . . . . . . . . . . . . . . . . . . . . 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 4028	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ⊆ ∪ 𝑅
73	71, 72	sstrdi 3943	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → 𝑠 ⊆ ∪ 𝑅)
74	73	adantr 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → 𝑠 ⊆ ∪ 𝑅)
75		elpwi 4564	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 ∈ 𝒫 ∪ 𝑆 → 𝑘 ⊆ ∪ 𝑆)
76	75	ad2antrl 741	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → 𝑘 ⊆ ∪ 𝑆)
77		eldif 3909	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑡 ∈ ((𝑠 × 𝑘) ∖ 𝑥) ↔ (𝑡 ∈ (𝑠 × 𝑘) ∧ ¬ 𝑡 ∈ 𝑥))
78	77	anbi1i 636	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑡 ∈ ((𝑠 × 𝑘) ∖ 𝑥) ∧ ((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘𝑡) = 𝑏) ↔ ((𝑡 ∈ (𝑠 × 𝑘) ∧ ¬ 𝑡 ∈ 𝑥) ∧ ((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘𝑡) = 𝑏))
79		anass 474	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑡 ∈ (𝑠 × 𝑘) ∧ ¬ 𝑡 ∈ 𝑥) ∧ ((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘𝑡) = 𝑏) ↔ (𝑡 ∈ (𝑠 × 𝑘) ∧ (¬ 𝑡 ∈ 𝑥 ∧ ((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘𝑡) = 𝑏)))
80	78, 79	bitri 278	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑡 ∈ ((𝑠 × 𝑘) ∖ 𝑥) ∧ ((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘𝑡) = 𝑏) ↔ (𝑡 ∈ (𝑠 × 𝑘) ∧ (¬ 𝑡 ∈ 𝑥 ∧ ((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘𝑡) = 𝑏)))
81	80	rexbii2 3105	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (∃𝑡 ∈ ((𝑠 × 𝑘) ∖ 𝑥)((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘𝑡) = 𝑏 ↔ ∃𝑡 ∈ (𝑠 × 𝑘)(¬ 𝑡 ∈ 𝑥 ∧ ((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘𝑡) = 𝑏))
82		ancom 466	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((¬ 𝑡 ∈ 𝑥 ∧ ((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘𝑡) = 𝑏) ↔ (((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘𝑡) = 𝑏 ∧ ¬ 𝑡 ∈ 𝑥))
83		fveqeq2 6890	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑡 = ⟨𝑎, 𝑢⟩ → (((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘𝑡) = 𝑏 ↔ ((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘⟨𝑎, 𝑢⟩) = 𝑏))
84		eleq1 2848	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑡 = ⟨𝑎, 𝑢⟩ → (𝑡 ∈ 𝑥 ↔ ⟨𝑎, 𝑢⟩ ∈ 𝑥))
85	84	notbid 321	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑡 = ⟨𝑎, 𝑢⟩ → (¬ 𝑡 ∈ 𝑥 ↔ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥))
86	83, 85	anbi12d 644	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑡 = ⟨𝑎, 𝑢⟩ → ((((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘𝑡) = 𝑏 ∧ ¬ 𝑡 ∈ 𝑥) ↔ (((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘⟨𝑎, 𝑢⟩) = 𝑏 ∧ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥)))
87	82, 86	bitrid 286	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑡 = ⟨𝑎, 𝑢⟩ → ((¬ 𝑡 ∈ 𝑥 ∧ ((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘𝑡) = 𝑏) ↔ (((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘⟨𝑎, 𝑢⟩) = 𝑏 ∧ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥)))
88	87	rexxp 5823	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (∃𝑡 ∈ (𝑠 × 𝑘)(¬ 𝑡 ∈ 𝑥 ∧ ((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘𝑡) = 𝑏) ↔ ∃𝑎 ∈ 𝑠 ∃𝑢 ∈ 𝑘 (((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘⟨𝑎, 𝑢⟩) = 𝑏 ∧ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥))
89	81, 88	bitri 278	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (∃𝑡 ∈ ((𝑠 × 𝑘) ∖ 𝑥)((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘𝑡) = 𝑏 ↔ ∃𝑎 ∈ 𝑠 ∃𝑢 ∈ 𝑘 (((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘⟨𝑎, 𝑢⟩) = 𝑏 ∧ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥))
90		simpl 488	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) → 𝑠 ⊆ ∪ 𝑅)
91	90	sselda 3931	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) ∧ 𝑎 ∈ 𝑠) → 𝑎 ∈ ∪ 𝑅)
92	91	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) ∧ 𝑎 ∈ 𝑠) ∧ 𝑢 ∈ 𝑘) → 𝑎 ∈ ∪ 𝑅)
93		simplr 781	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) ∧ 𝑎 ∈ 𝑠) → 𝑘 ⊆ ∪ 𝑆)
94	93	sselda 3931	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) ∧ 𝑎 ∈ 𝑠) ∧ 𝑢 ∈ 𝑘) → 𝑢 ∈ ∪ 𝑆)
95	92, 94	opelxpd 5694	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) ∧ 𝑎 ∈ 𝑠) ∧ 𝑢 ∈ 𝑘) → ⟨𝑎, 𝑢⟩ ∈ (∪ 𝑅 × ∪ 𝑆))
96	95	fvresd 6901	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) ∧ 𝑎 ∈ 𝑠) ∧ 𝑢 ∈ 𝑘) → ((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘⟨𝑎, 𝑢⟩) = (2nd ‘⟨𝑎, 𝑢⟩))
97		vex 3454	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ 𝑎 ∈ V
98		vex 3454	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ 𝑢 ∈ V
99	97, 98	op2nd 8001	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (2nd ‘⟨𝑎, 𝑢⟩) = 𝑢
100	96, 99	eqtrdi 2811	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) ∧ 𝑎 ∈ 𝑠) ∧ 𝑢 ∈ 𝑘) → ((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘⟨𝑎, 𝑢⟩) = 𝑢)
101	100	eqeq1d 2762	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) ∧ 𝑎 ∈ 𝑠) ∧ 𝑢 ∈ 𝑘) → (((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘⟨𝑎, 𝑢⟩) = 𝑏 ↔ 𝑢 = 𝑏))
102	101	anbi1d 643	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) ∧ 𝑎 ∈ 𝑠) ∧ 𝑢 ∈ 𝑘) → ((((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘⟨𝑎, 𝑢⟩) = 𝑏 ∧ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥) ↔ (𝑢 = 𝑏 ∧ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥)))
103	102	rexbidva 3184	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) ∧ 𝑎 ∈ 𝑠) → (∃𝑢 ∈ 𝑘 (((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘⟨𝑎, 𝑢⟩) = 𝑏 ∧ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥) ↔ ∃𝑢 ∈ 𝑘 (𝑢 = 𝑏 ∧ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥)))
104		opeq2 4834	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑢 = 𝑏 → ⟨𝑎, 𝑢⟩ = ⟨𝑎, 𝑏⟩)
105	104	eleq1d 2845	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑢 = 𝑏 → (⟨𝑎, 𝑢⟩ ∈ 𝑥 ↔ ⟨𝑎, 𝑏⟩ ∈ 𝑥))
106	105	notbid 321	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑢 = 𝑏 → (¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥 ↔ ¬ ⟨𝑎, 𝑏⟩ ∈ 𝑥))
107	106	ceqsrexbv 3610	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (∃𝑢 ∈ 𝑘 (𝑢 = 𝑏 ∧ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥) ↔ (𝑏 ∈ 𝑘 ∧ ¬ ⟨𝑎, 𝑏⟩ ∈ 𝑥))
108	103, 107	bitrdi 290	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) ∧ 𝑎 ∈ 𝑠) → (∃𝑢 ∈ 𝑘 (((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘⟨𝑎, 𝑢⟩) = 𝑏 ∧ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥) ↔ (𝑏 ∈ 𝑘 ∧ ¬ ⟨𝑎, 𝑏⟩ ∈ 𝑥)))
109	108	rexbidva 3184	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) → (∃𝑎 ∈ 𝑠 ∃𝑢 ∈ 𝑘 (((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘⟨𝑎, 𝑢⟩) = 𝑏 ∧ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥) ↔ ∃𝑎 ∈ 𝑠 (𝑏 ∈ 𝑘 ∧ ¬ ⟨𝑎, 𝑏⟩ ∈ 𝑥)))
110		r19.42v 3194	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (∃𝑎 ∈ 𝑠 (𝑏 ∈ 𝑘 ∧ ¬ ⟨𝑎, 𝑏⟩ ∈ 𝑥) ↔ (𝑏 ∈ 𝑘 ∧ ∃𝑎 ∈ 𝑠 ¬ ⟨𝑎, 𝑏⟩ ∈ 𝑥))
111	109, 110	bitrdi 290	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) → (∃𝑎 ∈ 𝑠 ∃𝑢 ∈ 𝑘 (((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘⟨𝑎, 𝑢⟩) = 𝑏 ∧ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥) ↔ (𝑏 ∈ 𝑘 ∧ ∃𝑎 ∈ 𝑠 ¬ ⟨𝑎, 𝑏⟩ ∈ 𝑥)))
112	89, 111	bitrid 286	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) → (∃𝑡 ∈ ((𝑠 × 𝑘) ∖ 𝑥)((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘𝑡) = 𝑏 ↔ (𝑏 ∈ 𝑘 ∧ ∃𝑎 ∈ 𝑠 ¬ ⟨𝑎, 𝑏⟩ ∈ 𝑥)))
113		f2ndres 8017	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (2nd ↾ (∪ 𝑅 × ∪ 𝑆)):(∪ 𝑅 × ∪ 𝑆)⟶∪ 𝑆
114		ffn 6705	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)):(∪ 𝑅 × ∪ 𝑆)⟶∪ 𝑆 → (2nd ↾ (∪ 𝑅 × ∪ 𝑆)) Fn (∪ 𝑅 × ∪ 𝑆))
115	113, 114	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (2nd ↾ (∪ 𝑅 × ∪ 𝑆)) Fn (∪ 𝑅 × ∪ 𝑆)
116		difss 4083	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑠 × 𝑘) ∖ 𝑥) ⊆ (𝑠 × 𝑘)
117		xpss12 5670	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) → (𝑠 × 𝑘) ⊆ (∪ 𝑅 × ∪ 𝑆))
118	116, 117	sstrid 3942	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) → ((𝑠 × 𝑘) ∖ 𝑥) ⊆ (∪ 𝑅 × ∪ 𝑆))
119		fvelimab 6953	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) Fn (∪ 𝑅 × ∪ 𝑆) ∧ ((𝑠 × 𝑘) ∖ 𝑥) ⊆ (∪ 𝑅 × ∪ 𝑆)) → (𝑏 ∈ ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ↔ ∃𝑡 ∈ ((𝑠 × 𝑘) ∖ 𝑥)((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘𝑡) = 𝑏))
120	115, 118, 119	sylancr 599	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) → (𝑏 ∈ ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ↔ ∃𝑡 ∈ ((𝑠 × 𝑘) ∖ 𝑥)((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘𝑡) = 𝑏))
121		eldif 3909	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑏 ∈ (𝑘 ∖ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ↔ (𝑏 ∈ 𝑘 ∧ ¬ 𝑏 ∈ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}))
122		simpr 490	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) → 𝑘 ⊆ ∪ 𝑆)
123	122	sselda 3931	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) ∧ 𝑏 ∈ 𝑘) → 𝑏 ∈ ∪ 𝑆)
124		sneq 4594	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑣 = 𝑏 → {𝑣} = {𝑏})
125	124	xpeq2d 5685	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑣 = 𝑏 → (𝑠 × {𝑣}) = (𝑠 × {𝑏}))
126	125	sseq1d 3962	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑣 = 𝑏 → ((𝑠 × {𝑣}) ⊆ 𝑥 ↔ (𝑠 × {𝑏}) ⊆ 𝑥))
127		dfss3 3920	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑠 × {𝑏}) ⊆ 𝑥 ↔ ∀𝑘 ∈ (𝑠 × {𝑏})𝑘 ∈ 𝑥)
128		eleq1 2848	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑘 = ⟨𝑎, 𝑡⟩ → (𝑘 ∈ 𝑥 ↔ ⟨𝑎, 𝑡⟩ ∈ 𝑥))
129	128	ralxp 5822	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (∀𝑘 ∈ (𝑠 × {𝑏})𝑘 ∈ 𝑥 ↔ ∀𝑎 ∈ 𝑠 ∀𝑡 ∈ {𝑏}⟨𝑎, 𝑡⟩ ∈ 𝑥)
130		vex 3454	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ 𝑏 ∈ V
131		opeq2 4834	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑡 = 𝑏 → ⟨𝑎, 𝑡⟩ = ⟨𝑎, 𝑏⟩)
132	131	eleq1d 2845	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑡 = 𝑏 → (⟨𝑎, 𝑡⟩ ∈ 𝑥 ↔ ⟨𝑎, 𝑏⟩ ∈ 𝑥))
133	130, 132	ralsn 4642	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (∀𝑡 ∈ {𝑏}⟨𝑎, 𝑡⟩ ∈ 𝑥 ↔ ⟨𝑎, 𝑏⟩ ∈ 𝑥)
134	133	ralbii 3108	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (∀𝑎 ∈ 𝑠 ∀𝑡 ∈ {𝑏}⟨𝑎, 𝑡⟩ ∈ 𝑥 ↔ ∀𝑎 ∈ 𝑠 ⟨𝑎, 𝑏⟩ ∈ 𝑥)
135	127, 129, 134	3bitri 300	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑠 × {𝑏}) ⊆ 𝑥 ↔ ∀𝑎 ∈ 𝑠 ⟨𝑎, 𝑏⟩ ∈ 𝑥)
136	126, 135	bitrdi 290	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑣 = 𝑏 → ((𝑠 × {𝑣}) ⊆ 𝑥 ↔ ∀𝑎 ∈ 𝑠 ⟨𝑎, 𝑏⟩ ∈ 𝑥))
137	136	elrab3 3646	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑏 ∈ ∪ 𝑆 → (𝑏 ∈ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ↔ ∀𝑎 ∈ 𝑠 ⟨𝑎, 𝑏⟩ ∈ 𝑥))
138	123, 137	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) ∧ 𝑏 ∈ 𝑘) → (𝑏 ∈ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ↔ ∀𝑎 ∈ 𝑠 ⟨𝑎, 𝑏⟩ ∈ 𝑥))
139	138	notbid 321	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) ∧ 𝑏 ∈ 𝑘) → (¬ 𝑏 ∈ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ↔ ¬ ∀𝑎 ∈ 𝑠 ⟨𝑎, 𝑏⟩ ∈ 𝑥))
140		rexnal 3114	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (∃𝑎 ∈ 𝑠 ¬ ⟨𝑎, 𝑏⟩ ∈ 𝑥 ↔ ¬ ∀𝑎 ∈ 𝑠 ⟨𝑎, 𝑏⟩ ∈ 𝑥)
141	139, 140	bitr4di 292	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) ∧ 𝑏 ∈ 𝑘) → (¬ 𝑏 ∈ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ↔ ∃𝑎 ∈ 𝑠 ¬ ⟨𝑎, 𝑏⟩ ∈ 𝑥))
142	141	pm5.32da 590	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) → ((𝑏 ∈ 𝑘 ∧ ¬ 𝑏 ∈ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ↔ (𝑏 ∈ 𝑘 ∧ ∃𝑎 ∈ 𝑠 ¬ ⟨𝑎, 𝑏⟩ ∈ 𝑥)))
143	121, 142	bitrid 286	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) → (𝑏 ∈ (𝑘 ∖ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ↔ (𝑏 ∈ 𝑘 ∧ ∃𝑎 ∈ 𝑠 ¬ ⟨𝑎, 𝑏⟩ ∈ 𝑥)))
144	112, 120, 143	3bitr4d 314	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) → (𝑏 ∈ ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ↔ 𝑏 ∈ (𝑘 ∖ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})))
145	144	eqrdv 2758	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) → ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) = (𝑘 ∖ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}))
146	74, 76, 145	syl2anc 596	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) = (𝑘 ∖ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}))
147		difin 4218	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∖ (𝑘 ∩ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})) = (𝑘 ∖ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})
148	65	adantr 486	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → 𝑆 ∈ Top)
149	24	restuni 23419	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑆 ∈ Top ∧ 𝑘 ⊆ ∪ 𝑆) → 𝑘 = ∪ (𝑆 ↾t 𝑘))
150	148, 76, 149	syl2anc 596	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → 𝑘 = ∪ (𝑆 ↾t 𝑘))
151	150	difeq1d 4073	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → (𝑘 ∖ (𝑘 ∩ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})) = (∪ (𝑆 ↾t 𝑘) ∖ (𝑘 ∩ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})))
152	147, 151	eqtr3id 2809	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → (𝑘 ∖ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) = (∪ (𝑆 ↾t 𝑘) ∖ (𝑘 ∩ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})))
153	146, 152	eqtrd 2795	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) = (∪ (𝑆 ↾t 𝑘) ∖ (𝑘 ∩ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})))
154	15	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → 𝑆 ∈ (ran 𝑘Gen ∩ Haus))
155	154	elin2d 4151	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → 𝑆 ∈ Haus)
156		df-ima 5668	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) = ran ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) ↾ ((𝑠 × 𝑘) ∖ 𝑥))
157		resres 5987	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) ↾ ((𝑠 × 𝑘) ∖ 𝑥)) = (2nd ↾ ((∪ 𝑅 × ∪ 𝑆) ∩ ((𝑠 × 𝑘) ∖ 𝑥)))
158		inss2 4183	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((∪ 𝑅 × ∪ 𝑆) ∩ ((𝑠 × 𝑘) ∖ 𝑥)) ⊆ ((𝑠 × 𝑘) ∖ 𝑥)
159	158, 116	sstri 3940	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((∪ 𝑅 × ∪ 𝑆) ∩ ((𝑠 × 𝑘) ∖ 𝑥)) ⊆ (𝑠 × 𝑘)
160		ssres2 5999	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((∪ 𝑅 × ∪ 𝑆) ∩ ((𝑠 × 𝑘) ∖ 𝑥)) ⊆ (𝑠 × 𝑘) → (2nd ↾ ((∪ 𝑅 × ∪ 𝑆) ∩ ((𝑠 × 𝑘) ∖ 𝑥))) ⊆ (2nd ↾ (𝑠 × 𝑘)))
161	159, 160	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (2nd ↾ ((∪ 𝑅 × ∪ 𝑆) ∩ ((𝑠 × 𝑘) ∖ 𝑥))) ⊆ (2nd ↾ (𝑠 × 𝑘))
162	157, 161	eqsstri 3977	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) ↾ ((𝑠 × 𝑘) ∖ 𝑥)) ⊆ (2nd ↾ (𝑠 × 𝑘))
163	162	rnssi 5926	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ran ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) ↾ ((𝑠 × 𝑘) ∖ 𝑥)) ⊆ ran (2nd ↾ (𝑠 × 𝑘))
164	156, 163	eqsstri 3977	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ⊆ ran (2nd ↾ (𝑠 × 𝑘))
165		f2ndres 8017	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (2nd ↾ (𝑠 × 𝑘)):(𝑠 × 𝑘)⟶𝑘
166		frn 6713	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((2nd ↾ (𝑠 × 𝑘)):(𝑠 × 𝑘)⟶𝑘 → ran (2nd ↾ (𝑠 × 𝑘)) ⊆ 𝑘)
167	165, 166	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ran (2nd ↾ (𝑠 × 𝑘)) ⊆ 𝑘
168	164, 167	sstri 3940	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ⊆ 𝑘
169	168, 76	sstrid 3942	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ⊆ ∪ 𝑆)
170	12	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → 𝑅 ∈ (TopOn‘∪ 𝑅))
171	148, 17	sylib 221	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → 𝑆 ∈ (TopOn‘∪ 𝑆))
172		tx2cn 23868	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑅 ∈ (TopOn‘∪ 𝑅) ∧ 𝑆 ∈ (TopOn‘∪ 𝑆)) → (2nd ↾ (∪ 𝑅 × ∪ 𝑆)) ∈ ((𝑅 ×t 𝑆) Cn 𝑆))
173	170, 171, 172	syl2anc 596	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → (2nd ↾ (∪ 𝑅 × ∪ 𝑆)) ∈ ((𝑅 ×t 𝑆) Cn 𝑆))
174	27	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . . 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 3454	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 𝑠 ∈ V
177		vex 3454	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 𝑘 ∈ V
178	176, 177	xpex 7758	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑠 × 𝑘) ∈ V
179	178	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → (𝑠 × 𝑘) ∈ V)
180		restabs 23422	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑅 ×t 𝑆) ∈ Top ∧ ((𝑠 × 𝑘) ∖ 𝑥) ⊆ (𝑠 × 𝑘) ∧ (𝑠 × 𝑘) ∈ V) → (((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ↾t ((𝑠 × 𝑘) ∖ 𝑥)) = ((𝑅 ×t 𝑆) ↾t ((𝑠 × 𝑘) ∖ 𝑥)))
181	174, 175, 179, 180	syl3anc 1398	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → (((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ↾t ((𝑠 × 𝑘) ∖ 𝑥)) = ((𝑅 ×t 𝑆) ↾t ((𝑠 × 𝑘) ∖ 𝑥)))
182	64	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → 𝑅 ∈ Top)
183	154, 4	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . 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 783	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → 𝑘 ∈ 𝒫 ∪ 𝑆)
186		txrest 23889	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑠 ∈ V ∧ 𝑘 ∈ 𝒫 ∪ 𝑆)) → ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) = ((𝑅 ↾t 𝑠) ×t (𝑆 ↾t 𝑘)))
187	182, 183, 184, 185, 186	syl22anc 852	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) = ((𝑅 ↾t 𝑠) ×t (𝑆 ↾t 𝑘)))
188		simprr3 1242	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → (𝑅 ↾t 𝑠) ∈ Comp)
189	188	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → (𝑅 ↾t 𝑠) ∈ Comp)
190		simprr 785	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → (𝑆 ↾t 𝑘) ∈ Comp)
191		txcmp 23901	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑅 ↾t 𝑠) ∈ Comp ∧ (𝑆 ↾t 𝑘) ∈ Comp) → ((𝑅 ↾t 𝑠) ×t (𝑆 ↾t 𝑘)) ∈ Comp)
192	189, 190, 191	syl2anc 596	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → ((𝑅 ↾t 𝑠) ×t (𝑆 ↾t 𝑘)) ∈ Comp)
193	187, 192	eqeltrd 2860	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ∈ Comp)
194		difin 4218	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑠 × 𝑘) ∖ ((𝑠 × 𝑘) ∩ 𝑥)) = ((𝑠 × 𝑘) ∖ 𝑥)
195	74, 76, 117	syl2anc 596	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → (𝑠 × 𝑘) ⊆ (∪ 𝑅 × ∪ 𝑆))
196	182, 148, 25	syl2anc 596	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → (∪ 𝑅 × ∪ 𝑆) = ∪ (𝑅 ×t 𝑆))
197	195, 196	sseqtrd 3967	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → (𝑠 × 𝑘) ⊆ ∪ (𝑅 ×t 𝑆))
198	28	restuni 23419	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑅 ×t 𝑆) ∈ Top ∧ (𝑠 × 𝑘) ⊆ ∪ (𝑅 ×t 𝑆)) → (𝑠 × 𝑘) = ∪ ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)))
199	174, 197, 198	syl2anc 596	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → (𝑠 × 𝑘) = ∪ ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)))
200	199	difeq1d 4073	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → ((𝑠 × 𝑘) ∖ ((𝑠 × 𝑘) ∩ 𝑥)) = (∪ ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ∖ ((𝑠 × 𝑘) ∩ 𝑥)))
201	194, 200	eqtr3id 2809	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → ((𝑠 × 𝑘) ∖ 𝑥) = (∪ ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ∖ ((𝑠 × 𝑘) ∩ 𝑥)))
202		resttop 23417	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑅 ×t 𝑆) ∈ Top ∧ (𝑠 × 𝑘) ∈ V) → ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ∈ Top)
203	174, 178, 202	sylancl 598	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ∈ Top)
204		incom 4155	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑠 × 𝑘) ∩ 𝑥) = (𝑥 ∩ (𝑠 × 𝑘))
205	20	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆)))
206		kgeni 23795	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆)) ∧ ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ∈ Comp) → (𝑥 ∩ (𝑠 × 𝑘)) ∈ ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)))
207	205, 193, 206	syl2anc 596	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → (𝑥 ∩ (𝑠 × 𝑘)) ∈ ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)))
208	204, 207	eqeltrid 2864	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → ((𝑠 × 𝑘) ∩ 𝑥) ∈ ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)))
209		eqid 2760	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ∪ ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) = ∪ ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘))
210	209	opncld 23290	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ∈ Top ∧ ((𝑠 × 𝑘) ∩ 𝑥) ∈ ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘))) → (∪ ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ∖ ((𝑠 × 𝑘) ∩ 𝑥)) ∈ (Clsd‘((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘))))
211	203, 208, 210	syl2anc 596	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → (∪ ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ∖ ((𝑠 × 𝑘) ∩ 𝑥)) ∈ (Clsd‘((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘))))
212	201, 211	eqeltrd 2860	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → ((𝑠 × 𝑘) ∖ 𝑥) ∈ (Clsd‘((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘))))
213		cmpcld 23659	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ∈ Comp ∧ ((𝑠 × 𝑘) ∖ 𝑥) ∈ (Clsd‘((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)))) → (((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ↾t ((𝑠 × 𝑘) ∖ 𝑥)) ∈ Comp)
214	193, 212, 213	syl2anc 596	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → (((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ↾t ((𝑠 × 𝑘) ∖ 𝑥)) ∈ Comp)
215	181, 214	eqeltrrd 2861	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → ((𝑅 ×t 𝑆) ↾t ((𝑠 × 𝑘) ∖ 𝑥)) ∈ Comp)
216		imacmp 23654	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) ∈ ((𝑅 ×t 𝑆) Cn 𝑆) ∧ ((𝑅 ×t 𝑆) ↾t ((𝑠 × 𝑘) ∖ 𝑥)) ∈ Comp) → (𝑆 ↾t ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥))) ∈ Comp)
217	173, 215, 216	syl2anc 596	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → (𝑆 ↾t ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥))) ∈ Comp)
218	24	hauscmp 23664	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑆 ∈ Haus ∧ ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ⊆ ∪ 𝑆 ∧ (𝑆 ↾t ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥))) ∈ Comp) → ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ∈ (Clsd‘𝑆))
219	155, 169, 217, 218	syl3anc 1398	. . . . . . . . . . . . . . . . . . 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 23430	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑘 ⊆ ∪ 𝑆 ∧ ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ∈ (Clsd‘𝑆) ∧ ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ⊆ 𝑘) → ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ∈ (Clsd‘(𝑆 ↾t 𝑘)))
222	76, 219, 220, 221	syl3anc 1398	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ∈ (Clsd‘(𝑆 ↾t 𝑘)))
223	153, 222	eqeltrrd 2861	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → (∪ (𝑆 ↾t 𝑘) ∖ (𝑘 ∩ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})) ∈ (Clsd‘(𝑆 ↾t 𝑘)))
224		resttop 23417	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑆 ∈ Top ∧ 𝑘 ∈ 𝒫 ∪ 𝑆) → (𝑆 ↾t 𝑘) ∈ Top)
225	148, 185, 224	syl2anc 596	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → (𝑆 ↾t 𝑘) ∈ Top)
226		inss1 4182	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 ∩ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ⊆ 𝑘
227	226, 150	sseqtrid 3973	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → (𝑘 ∩ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ⊆ ∪ (𝑆 ↾t 𝑘))
228		eqid 2760	. . . . . . . . . . . . . . . . . . 19 ⊢ ∪ (𝑆 ↾t 𝑘) = ∪ (𝑆 ↾t 𝑘)
229	228	isopn2 23289	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑆 ↾t 𝑘) ∈ Top ∧ (𝑘 ∩ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ⊆ ∪ (𝑆 ↾t 𝑘)) → ((𝑘 ∩ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ∈ (𝑆 ↾t 𝑘) ↔ (∪ (𝑆 ↾t 𝑘) ∖ (𝑘 ∩ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})) ∈ (Clsd‘(𝑆 ↾t 𝑘))))
230	225, 227, 229	syl2anc 596	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → ((𝑘 ∩ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ∈ (𝑆 ↾t 𝑘) ↔ (∪ (𝑆 ↾t 𝑘) ∖ (𝑘 ∩ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})) ∈ (Clsd‘(𝑆 ↾t 𝑘))))
231	223, 230	mpbird 260	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → (𝑘 ∩ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ∈ (𝑆 ↾t 𝑘))
232	69, 231	eqeltrid 2864	. . . . . . . . . . . . . . 15 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → ({𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ∩ 𝑘) ∈ (𝑆 ↾t 𝑘))
233	232	expr 462	. . . . . . . . . . . . . 14 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ 𝑘 ∈ 𝒫 ∪ 𝑆) → ((𝑆 ↾t 𝑘) ∈ Comp → ({𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ∩ 𝑘) ∈ (𝑆 ↾t 𝑘)))
234	233	ralrimiva 3154	. . . . . . . . . . . . 13 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → ∀𝑘 ∈ 𝒫 ∪ 𝑆((𝑆 ↾t 𝑘) ∈ Comp → ({𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ∩ 𝑘) ∈ (𝑆 ↾t 𝑘)))
235	65, 17	sylib 221	. . . . . . . . . . . . . 14 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → 𝑆 ∈ (TopOn‘∪ 𝑆))
236		elkgen 23794	. . . . . . . . . . . . . 14 ⊢ (𝑆 ∈ (TopOn‘∪ 𝑆) → ({𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ∈ (𝑘Gen‘𝑆) ↔ ({𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ⊆ ∪ 𝑆 ∧ ∀𝑘 ∈ 𝒫 ∪ 𝑆((𝑆 ↾t 𝑘) ∈ Comp → ({𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ∩ 𝑘) ∈ (𝑆 ↾t 𝑘)))))
237	235, 236	syl 18	. . . . . . . . . . . . 13 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → ({𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ∈ (𝑘Gen‘𝑆) ↔ ({𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ⊆ ∪ 𝑆 ∧ ∀𝑘 ∈ 𝒫 ∪ 𝑆((𝑆 ↾t 𝑘) ∈ Comp → ({𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ∩ 𝑘) ∈ (𝑆 ↾t 𝑘)))))
238	68, 234, 237	mpbir2and 726	. . . . . . . . . . . 12 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ∈ (𝑘Gen‘𝑆))
239	15	adantr 486	. . . . . . . . . . . . . 14 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → 𝑆 ∈ (ran 𝑘Gen ∩ Haus))
240	239, 2	syl 18	. . . . . . . . . . . . 13 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → 𝑆 ∈ ran 𝑘Gen)
241		kgenidm 23805	. . . . . . . . . . . . 13 ⊢ (𝑆 ∈ ran 𝑘Gen → (𝑘Gen‘𝑆) = 𝑆)
242	240, 241	syl 18	. . . . . . . . . . . 12 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → (𝑘Gen‘𝑆) = 𝑆)
243	238, 242	eleqtrd 2862	. . . . . . . . . . 11 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ∈ 𝑆)
244		txopn 23860	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑢 ∈ 𝑅 ∧ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ∈ 𝑆)) → (𝑢 × {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ∈ (𝑅 ×t 𝑆))
245	64, 65, 66, 243, 244	syl22anc 852	. . . . . . . . . 10 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → (𝑢 × {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ∈ (𝑅 ×t 𝑆))
246	59	adantr 486	. . . . . . . . . . 11 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → 𝑦 = ⟨(1st ‘𝑦), (2nd ‘𝑦)⟩)
247		simprr1 1240	. . . . . . . . . . . 12 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → (1st ‘𝑦) ∈ 𝑢)
248		sneq 4594	. . . . . . . . . . . . . . 15 ⊢ (𝑣 = (2nd ‘𝑦) → {𝑣} = {(2nd ‘𝑦)})
249	248	xpeq2d 5685	. . . . . . . . . . . . . 14 ⊢ (𝑣 = (2nd ‘𝑦) → (𝑠 × {𝑣}) = (𝑠 × {(2nd ‘𝑦)}))
250	249	sseq1d 3962	. . . . . . . . . . . . 13 ⊢ (𝑣 = (2nd ‘𝑦) → ((𝑠 × {𝑣}) ⊆ 𝑥 ↔ (𝑠 × {(2nd ‘𝑦)}) ⊆ 𝑥))
251	34	adantr 486	. . . . . . . . . . . . 13 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → (2nd ‘𝑦) ∈ ∪ 𝑆)
252		relxp 5673	. . . . . . . . . . . . . . 15 ⊢ Rel (𝑠 × {(2nd ‘𝑦)})
253	252	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → Rel (𝑠 × {(2nd ‘𝑦)}))
254		opelxp 5691	. . . . . . . . . . . . . . 15 ⊢ (⟨𝑎, 𝑏⟩ ∈ (𝑠 × {(2nd ‘𝑦)}) ↔ (𝑎 ∈ 𝑠 ∧ 𝑏 ∈ {(2nd ‘𝑦)}))
255	71	sselda 3931	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ 𝑎 ∈ 𝑠) → 𝑎 ∈ {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥})
256		opeq1 4833	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑡 = 𝑎 → ⟨𝑡, (2nd ‘𝑦)⟩ = ⟨𝑎, (2nd ‘𝑦)⟩)
257	256	eleq1d 2845	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 = 𝑎 → (⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥 ↔ ⟨𝑎, (2nd ‘𝑦)⟩ ∈ 𝑥))
258	257	elrab 3645	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 ∈ {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ↔ (𝑎 ∈ ∪ 𝑅 ∧ ⟨𝑎, (2nd ‘𝑦)⟩ ∈ 𝑥))
259	258	simprbi 503	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 ∈ {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} → ⟨𝑎, (2nd ‘𝑦)⟩ ∈ 𝑥)
260	255, 259	syl 18	. . . . . . . . . . . . . . . . 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 2845	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 ∈ {(2nd ‘𝑦)} → (⟨𝑎, 𝑏⟩ ∈ 𝑥 ↔ ⟨𝑎, (2nd ‘𝑦)⟩ ∈ 𝑥))
264	260, 263	syl5ibrcom 250	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ 𝑎 ∈ 𝑠) → (𝑏 ∈ {(2nd ‘𝑦)} → ⟨𝑎, 𝑏⟩ ∈ 𝑥))
265	264	expimpd 459	. . . . . . . . . . . . . . 15 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → ((𝑎 ∈ 𝑠 ∧ 𝑏 ∈ {(2nd ‘𝑦)}) → ⟨𝑎, 𝑏⟩ ∈ 𝑥))
266	254, 265	biimtrid 245	. . . . . . . . . . . . . 14 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → (⟨𝑎, 𝑏⟩ ∈ (𝑠 × {(2nd ‘𝑦)}) → ⟨𝑎, 𝑏⟩ ∈ 𝑥))
267	253, 266	relssdv 5768	. . . . . . . . . . . . 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 5694	. . . . . . . . . . 11 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → ⟨(1st ‘𝑦), (2nd ‘𝑦)⟩ ∈ (𝑢 × {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}))
270	246, 269	eqeltrd 2860	. . . . . . . . . 10 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → 𝑦 ∈ (𝑢 × {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}))
271		relxp 5673	. . . . . . . . . . . 12 ⊢ Rel (𝑢 × {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})
272	271	a1i 11	. . . . . . . . . . 11 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → Rel (𝑢 × {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}))
273		opelxp 5691	. . . . . . . . . . . 12 ⊢ (⟨𝑎, 𝑏⟩ ∈ (𝑢 × {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ↔ (𝑎 ∈ 𝑢 ∧ 𝑏 ∈ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}))
274	126	elrab 3645	. . . . . . . . . . . . . . 15 ⊢ (𝑏 ∈ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ↔ (𝑏 ∈ ∪ 𝑆 ∧ (𝑠 × {𝑏}) ⊆ 𝑥))
275	274	simprbi 503	. . . . . . . . . . . . . 14 ⊢ (𝑏 ∈ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} → (𝑠 × {𝑏}) ⊆ 𝑥)
276		simprr2 1241	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → 𝑢 ⊆ 𝑠)
277	276	sselda 3931	. . . . . . . . . . . . . . 15 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ 𝑎 ∈ 𝑢) → 𝑎 ∈ 𝑠)
278		vsnid 4624	. . . . . . . . . . . . . . 15 ⊢ 𝑏 ∈ {𝑏}
279		opelxpi 5692	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 ∈ 𝑠 ∧ 𝑏 ∈ {𝑏}) → ⟨𝑎, 𝑏⟩ ∈ (𝑠 × {𝑏}))
280	277, 278, 279	sylancl 598	. . . . . . . . . . . . . 14 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ 𝑎 ∈ 𝑢) → ⟨𝑎, 𝑏⟩ ∈ (𝑠 × {𝑏}))
281		ssel 3925	. . . . . . . . . . . . . 14 ⊢ ((𝑠 × {𝑏}) ⊆ 𝑥 → (⟨𝑎, 𝑏⟩ ∈ (𝑠 × {𝑏}) → ⟨𝑎, 𝑏⟩ ∈ 𝑥))
282	275, 280, 281	syl2imc 42	. . . . . . . . . . . . 13 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ 𝑎 ∈ 𝑢) → (𝑏 ∈ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} → ⟨𝑎, 𝑏⟩ ∈ 𝑥))
283	282	expimpd 459	. . . . . . . . . . . 12 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → ((𝑎 ∈ 𝑢 ∧ 𝑏 ∈ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) → ⟨𝑎, 𝑏⟩ ∈ 𝑥))
284	273, 283	biimtrid 245	. . . . . . . . . . 11 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → (⟨𝑎, 𝑏⟩ ∈ (𝑢 × {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) → ⟨𝑎, 𝑏⟩ ∈ 𝑥))
285	272, 284	relssdv 5768	. . . . . . . . . 10 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → (𝑢 × {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ⊆ 𝑥)
286		eleq2 2849	. . . . . . . . . . . 12 ⊢ (𝑡 = (𝑢 × {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) → (𝑦 ∈ 𝑡 ↔ 𝑦 ∈ (𝑢 × {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})))
287		sseq1 3956	. . . . . . . . . . . 12 ⊢ (𝑡 = (𝑢 × {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) → (𝑡 ⊆ 𝑥 ↔ (𝑢 × {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ⊆ 𝑥))
288	286, 287	anbi12d 644	. . . . . . . . . . 11 ⊢ (𝑡 = (𝑢 × {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) → ((𝑦 ∈ 𝑡 ∧ 𝑡 ⊆ 𝑥) ↔ (𝑦 ∈ (𝑢 × {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ∧ (𝑢 × {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ⊆ 𝑥)))
289	288	rspcev 3576	. . . . . . . . . 10 ⊢ (((𝑢 × {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ∈ (𝑅 ×t 𝑆) ∧ (𝑦 ∈ (𝑢 × {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ∧ (𝑢 × {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ⊆ 𝑥)) → ∃𝑡 ∈ (𝑅 ×t 𝑆)(𝑦 ∈ 𝑡 ∧ 𝑡 ⊆ 𝑥))
290	245, 270, 285, 289	syl12anc 850	. . . . . . . . 9 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → ∃𝑡 ∈ (𝑅 ×t 𝑆)(𝑦 ∈ 𝑡 ∧ 𝑡 ⊆ 𝑥))
291	290	expr 462	. . . . . . . 8 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ (𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅)) → (((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp) → ∃𝑡 ∈ (𝑅 ×t 𝑆)(𝑦 ∈ 𝑡 ∧ 𝑡 ⊆ 𝑥)))
292	291	rexlimdvva 3219	. . . . . . 7 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → (∃𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥}∃𝑢 ∈ 𝑅 ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp) → ∃𝑡 ∈ (𝑅 ×t 𝑆)(𝑦 ∈ 𝑡 ∧ 𝑡 ⊆ 𝑥)))
293	63, 292	mpd 16	. . . . . 6 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → ∃𝑡 ∈ (𝑅 ×t 𝑆)(𝑦 ∈ 𝑡 ∧ 𝑡 ⊆ 𝑥))
294	293	ralrimiva 3154	. . . . 5 ⊢ (((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) → ∀𝑦 ∈ 𝑥 ∃𝑡 ∈ (𝑅 ×t 𝑆)(𝑦 ∈ 𝑡 ∧ 𝑡 ⊆ 𝑥))
295	6	adantr 486	. . . . . 6 ⊢ (((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) → (𝑅 ×t 𝑆) ∈ Top)
296		eltop2 23232	. . . . . 6 ⊢ ((𝑅 ×t 𝑆) ∈ Top → (𝑥 ∈ (𝑅 ×t 𝑆) ↔ ∀𝑦 ∈ 𝑥 ∃𝑡 ∈ (𝑅 ×t 𝑆)(𝑦 ∈ 𝑡 ∧ 𝑡 ⊆ 𝑥)))
297	295, 296	syl 18	. . . . 5 ⊢ (((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) → (𝑥 ∈ (𝑅 ×t 𝑆) ↔ ∀𝑦 ∈ 𝑥 ∃𝑡 ∈ (𝑅 ×t 𝑆)(𝑦 ∈ 𝑡 ∧ 𝑡 ⊆ 𝑥)))
298	294, 297	mpbird 260	. . . 4 ⊢ (((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) → 𝑥 ∈ (𝑅 ×t 𝑆))
299	298	ex 418	. . 3 ⊢ ((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) → (𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆)) → 𝑥 ∈ (𝑅 ×t 𝑆)))
300	299	ssrdv 3937	. 2 ⊢ ((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) → (𝑘Gen‘(𝑅 ×t 𝑆)) ⊆ (𝑅 ×t 𝑆))
301		iskgen2 23806	. 2 ⊢ ((𝑅 ×t 𝑆) ∈ ran 𝑘Gen ↔ ((𝑅 ×t 𝑆) ∈ Top ∧ (𝑘Gen‘(𝑅 ×t 𝑆)) ⊆ (𝑅 ×t 𝑆)))
302	6, 300, 301	sylanbrc 595	1 ⊢ ((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) → (𝑅 ×t 𝑆) ∈ ran 𝑘Gen)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∧ w3a 1103   = wceq 1570   ∈ wcel 2145  ∀wral 3076  ∃wrex 3086  {crab 3412  Vcvv 3450   ∖ cdif 3896   ∩ cin 3898   ⊆ wss 3899  𝒫 cpw 4557  {csn 4584  ⟨cop 4590  ∪ cuni 4867   ↦ cmpt 5186   I cid 5549   × cxp 5653  ^◡ccnv 5654  ran crn 5656   ↾ cres 5657   “ cima 5658  Rel wrel 5660   Fn wfn 6530  ⟶wf 6531  ‘cfv 6535  (class class class)co 7416  1^st c1st 7990  2^nd c2nd 7991   ↾_t crest 17530  Topctop 23150  TopOnctopon 23167  Clsdccld 23273   Cn ccn 23481  Hauscha 23565  Compccmp 23643  𝑛-Locally cnlly 23723  𝑘Genckgen 23791   ×_t ctx 23818

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-rep 5232  ax-sep 5251  ax-nul 5263  ax-pow 5330  ax-pr 5398  ax-un 7742

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  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 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5550  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-we 5610  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-ord 6362  df-on 6363  df-lim 6364  df-suc 6365  df-iota 6491  df-fun 6537  df-fn 6538  df-f 6539  df-f1 6540  df-fo 6541  df-f1o 6542  df-fv 6543  df-ov 7419  df-oprab 7420  df-mpo 7421  df-om 7869  df-1st 7992  df-2nd 7993  df-1o 8462  df-2o 8463  df-map 8835  df-en 8960  df-dom 8961  df-fin 8963  df-fi 9388  df-rest 17532  df-topgen 17553  df-top 23151  df-topon 23168  df-bases 23203  df-cld 23276  df-ntr 23277  df-cls 23278  df-nei 23355  df-cn 23484  df-cnp 23485  df-haus 23572  df-cmp 23644  df-nlly 23725  df-kgen 23792  df-tx 23820

This theorem is used by: (None)