Theorem txkgen 21455

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 21276	. . 3 ⊢ (𝑅 ∈ 𝑛-Locally Comp → 𝑅 ∈ Top)
2		elinel1 3799	. . . 4 ⊢ (𝑆 ∈ (ran 𝑘Gen ∩ Haus) → 𝑆 ∈ ran 𝑘Gen)
3		kgentop 21345	. . . 4 ⊢ (𝑆 ∈ ran 𝑘Gen → 𝑆 ∈ Top)
4	2, 3	syl 17	. . 3 ⊢ (𝑆 ∈ (ran 𝑘Gen ∩ Haus) → 𝑆 ∈ Top)
5		txtop 21372	. . 3 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑅 ×t 𝑆) ∈ Top)
6	1, 4, 5	syl2an 494	. 2 ⊢ ((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) → (𝑅 ×t 𝑆) ∈ Top)
7		simplll 798	. . . . . . . 8 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → 𝑅 ∈ 𝑛-Locally Comp)
8		eqid 2622	. . . . . . . . . 10 ⊢ (𝑡 ∈ ∪ 𝑅 ↦ ⟨𝑡, (2nd ‘𝑦)⟩) = (𝑡 ∈ ∪ 𝑅 ↦ ⟨𝑡, (2nd ‘𝑦)⟩)
9	8	mptpreima 5628	. . . . . . . . 9 ⊢ (◡(𝑡 ∈ ∪ 𝑅 ↦ ⟨𝑡, (2nd ‘𝑦)⟩) “ 𝑥) = {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥}
10	1	ad3antrrr 766	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → 𝑅 ∈ Top)
11		eqid 2622	. . . . . . . . . . . . . . 15 ⊢ ∪ 𝑅 = ∪ 𝑅
12	11	toptopon 20722	. . . . . . . . . . . . . 14 ⊢ (𝑅 ∈ Top ↔ 𝑅 ∈ (TopOn‘∪ 𝑅))
13	10, 12	sylib 208	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → 𝑅 ∈ (TopOn‘∪ 𝑅))
14		idcn 21061	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ (TopOn‘∪ 𝑅) → ( I ↾ ∪ 𝑅) ∈ (𝑅 Cn 𝑅))
15	13, 14	syl 17	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → ( I ↾ ∪ 𝑅) ∈ (𝑅 Cn 𝑅))
16		simpllr 799	. . . . . . . . . . . . . . 15 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → 𝑆 ∈ (ran 𝑘Gen ∩ Haus))
17	16, 4	syl 17	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → 𝑆 ∈ Top)
18		eqid 2622	. . . . . . . . . . . . . . 15 ⊢ ∪ 𝑆 = ∪ 𝑆
19	18	toptopon 20722	. . . . . . . . . . . . . 14 ⊢ (𝑆 ∈ Top ↔ 𝑆 ∈ (TopOn‘∪ 𝑆))
20	17, 19	sylib 208	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → 𝑆 ∈ (TopOn‘∪ 𝑆))
21		simpr 477	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ 𝑥)
22		simplr 792	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆)))
23		elunii 4441	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) → 𝑦 ∈ ∪ (𝑘Gen‘(𝑅 ×t 𝑆)))
24	21, 22, 23	syl2anc 693	. . . . . . . . . . . . . . 15 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ ∪ (𝑘Gen‘(𝑅 ×t 𝑆)))
25	11, 18	txuni 21395	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (∪ 𝑅 × ∪ 𝑆) = ∪ (𝑅 ×t 𝑆))
26	10, 17, 25	syl2anc 693	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → (∪ 𝑅 × ∪ 𝑆) = ∪ (𝑅 ×t 𝑆))
27	10, 17, 5	syl2anc 693	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → (𝑅 ×t 𝑆) ∈ Top)
28		eqid 2622	. . . . . . . . . . . . . . . . . 18 ⊢ ∪ (𝑅 ×t 𝑆) = ∪ (𝑅 ×t 𝑆)
29	28	kgenuni 21342	. . . . . . . . . . . . . . . . 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 2656	. . . . . . . . . . . . . . 15 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → (∪ 𝑅 × ∪ 𝑆) = ∪ (𝑘Gen‘(𝑅 ×t 𝑆)))
32	24, 31	eleqtrrd 2704	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ (∪ 𝑅 × ∪ 𝑆))
33		xp2nd 7199	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ (∪ 𝑅 × ∪ 𝑆) → (2nd ‘𝑦) ∈ ∪ 𝑆)
34	32, 33	syl 17	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → (2nd ‘𝑦) ∈ ∪ 𝑆)
35		cnconst2 21087	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ (TopOn‘∪ 𝑅) ∧ 𝑆 ∈ (TopOn‘∪ 𝑆) ∧ (2nd ‘𝑦) ∈ ∪ 𝑆) → (∪ 𝑅 × {(2nd ‘𝑦)}) ∈ (𝑅 Cn 𝑆))
36	13, 20, 34, 35	syl3anc 1326	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → (∪ 𝑅 × {(2nd ‘𝑦)}) ∈ (𝑅 Cn 𝑆))
37		fvresi 6439	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 ∈ ∪ 𝑅 → (( I ↾ ∪ 𝑅)‘𝑡) = 𝑡)
38		fvex 6201	. . . . . . . . . . . . . . . . 17 ⊢ (2nd ‘𝑦) ∈ V
39	38	fvconst2 6469	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 ∈ ∪ 𝑅 → ((∪ 𝑅 × {(2nd ‘𝑦)})‘𝑡) = (2nd ‘𝑦))
40	37, 39	opeq12d 4410	. . . . . . . . . . . . . . 15 ⊢ (𝑡 ∈ ∪ 𝑅 → ⟨(( I ↾ ∪ 𝑅)‘𝑡), ((∪ 𝑅 × {(2nd ‘𝑦)})‘𝑡)⟩ = ⟨𝑡, (2nd ‘𝑦)⟩)
41	40	mpteq2ia 4740	. . . . . . . . . . . . . 14 ⊢ (𝑡 ∈ ∪ 𝑅 ↦ ⟨(( I ↾ ∪ 𝑅)‘𝑡), ((∪ 𝑅 × {(2nd ‘𝑦)})‘𝑡)⟩) = (𝑡 ∈ ∪ 𝑅 ↦ ⟨𝑡, (2nd ‘𝑦)⟩)
42	41	eqcomi 2631	. . . . . . . . . . . . 13 ⊢ (𝑡 ∈ ∪ 𝑅 ↦ ⟨𝑡, (2nd ‘𝑦)⟩) = (𝑡 ∈ ∪ 𝑅 ↦ ⟨(( I ↾ ∪ 𝑅)‘𝑡), ((∪ 𝑅 × {(2nd ‘𝑦)})‘𝑡)⟩)
43	11, 42	txcnmpt 21427	. . . . . . . . . . . 12 ⊢ ((( I ↾ ∪ 𝑅) ∈ (𝑅 Cn 𝑅) ∧ (∪ 𝑅 × {(2nd ‘𝑦)}) ∈ (𝑅 Cn 𝑆)) → (𝑡 ∈ ∪ 𝑅 ↦ ⟨𝑡, (2nd ‘𝑦)⟩) ∈ (𝑅 Cn (𝑅 ×t 𝑆)))
44	15, 36, 43	syl2anc 693	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → (𝑡 ∈ ∪ 𝑅 ↦ ⟨𝑡, (2nd ‘𝑦)⟩) ∈ (𝑅 Cn (𝑅 ×t 𝑆)))
45		llycmpkgen 21355	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ 𝑛-Locally Comp → 𝑅 ∈ ran 𝑘Gen)
46	45	ad3antrrr 766	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → 𝑅 ∈ ran 𝑘Gen)
47	6	ad2antrr 762	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → (𝑅 ×t 𝑆) ∈ Top)
48		kgencn3 21361	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ ran 𝑘Gen ∧ (𝑅 ×t 𝑆) ∈ Top) → (𝑅 Cn (𝑅 ×t 𝑆)) = (𝑅 Cn (𝑘Gen‘(𝑅 ×t 𝑆))))
49	46, 47, 48	syl2anc 693	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → (𝑅 Cn (𝑅 ×t 𝑆)) = (𝑅 Cn (𝑘Gen‘(𝑅 ×t 𝑆))))
50	44, 49	eleqtrd 2703	. . . . . . . . . 10 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → (𝑡 ∈ ∪ 𝑅 ↦ ⟨𝑡, (2nd ‘𝑦)⟩) ∈ (𝑅 Cn (𝑘Gen‘(𝑅 ×t 𝑆))))
51		cnima 21069	. . . . . . . . . 10 ⊢ (((𝑡 ∈ ∪ 𝑅 ↦ ⟨𝑡, (2nd ‘𝑦)⟩) ∈ (𝑅 Cn (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) → (◡(𝑡 ∈ ∪ 𝑅 ↦ ⟨𝑡, (2nd ‘𝑦)⟩) “ 𝑥) ∈ 𝑅)
52	50, 22, 51	syl2anc 693	. . . . . . . . 9 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → (◡(𝑡 ∈ ∪ 𝑅 ↦ ⟨𝑡, (2nd ‘𝑦)⟩) “ 𝑥) ∈ 𝑅)
53	9, 52	syl5eqelr 2706	. . . . . . . 8 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∈ 𝑅)
54		xp1st 7198	. . . . . . . . . 10 ⊢ (𝑦 ∈ (∪ 𝑅 × ∪ 𝑆) → (1st ‘𝑦) ∈ ∪ 𝑅)
55	32, 54	syl 17	. . . . . . . . 9 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → (1st ‘𝑦) ∈ ∪ 𝑅)
56		1st2nd2 7205	. . . . . . . . . . 11 ⊢ (𝑦 ∈ (∪ 𝑅 × ∪ 𝑆) → 𝑦 = ⟨(1st ‘𝑦), (2nd ‘𝑦)⟩)
57	32, 56	syl 17	. . . . . . . . . 10 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → 𝑦 = ⟨(1st ‘𝑦), (2nd ‘𝑦)⟩)
58	57, 21	eqeltrrd 2702	. . . . . . . . 9 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → ⟨(1st ‘𝑦), (2nd ‘𝑦)⟩ ∈ 𝑥)
59		opeq1 4402	. . . . . . . . . . 11 ⊢ (𝑡 = (1st ‘𝑦) → ⟨𝑡, (2nd ‘𝑦)⟩ = ⟨(1st ‘𝑦), (2nd ‘𝑦)⟩)
60	59	eleq1d 2686	. . . . . . . . . 10 ⊢ (𝑡 = (1st ‘𝑦) → (⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥 ↔ ⟨(1st ‘𝑦), (2nd ‘𝑦)⟩ ∈ 𝑥))
61	60	elrab 3363	. . . . . . . . 9 ⊢ ((1st ‘𝑦) ∈ {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ↔ ((1st ‘𝑦) ∈ ∪ 𝑅 ∧ ⟨(1st ‘𝑦), (2nd ‘𝑦)⟩ ∈ 𝑥))
62	55, 58, 61	sylanbrc 698	. . . . . . . 8 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → (1st ‘𝑦) ∈ {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥})
63		nlly2i 21279	. . . . . . . 8 ⊢ ((𝑅 ∈ 𝑛-Locally Comp ∧ {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∈ 𝑅 ∧ (1st ‘𝑦) ∈ {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥}) → ∃𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥}∃𝑢 ∈ 𝑅 ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))
64	7, 53, 62, 63	syl3anc 1326	. . . . . . 7 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → ∃𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥}∃𝑢 ∈ 𝑅 ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))
65	10	adantr 481	. . . . . . . . . . 11 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → 𝑅 ∈ Top)
66	17	adantr 481	. . . . . . . . . . 11 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → 𝑆 ∈ Top)
67		simprlr 803	. . . . . . . . . . 11 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → 𝑢 ∈ 𝑅)
68		ssrab2 3687	. . . . . . . . . . . . . 14 ⊢ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ⊆ ∪ 𝑆
69	68	a1i 11	. . . . . . . . . . . . 13 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ⊆ ∪ 𝑆)
70		incom 3805	. . . . . . . . . . . . . . . 16 ⊢ ({𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ∩ 𝑘) = (𝑘 ∩ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})
71		simprll 802	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → 𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥})
72	71	elpwid 4170	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → 𝑠 ⊆ {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥})
73		ssrab2 3687	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ⊆ ∪ 𝑅
74	72, 73	syl6ss 3615	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → 𝑠 ⊆ ∪ 𝑅)
75	74	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → 𝑠 ⊆ ∪ 𝑅)
76		elpwi 4168	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 ∈ 𝒫 ∪ 𝑆 → 𝑘 ⊆ ∪ 𝑆)
77	76	ad2antrl 764	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → 𝑘 ⊆ ∪ 𝑆)
78		eldif 3584	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑡 ∈ ((𝑠 × 𝑘) ∖ 𝑥) ↔ (𝑡 ∈ (𝑠 × 𝑘) ∧ ¬ 𝑡 ∈ 𝑥))
79	78	anbi1i 731	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑡 ∈ ((𝑠 × 𝑘) ∖ 𝑥) ∧ ((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘𝑡) = 𝑏) ↔ ((𝑡 ∈ (𝑠 × 𝑘) ∧ ¬ 𝑡 ∈ 𝑥) ∧ ((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘𝑡) = 𝑏))
80		anass 681	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑡 ∈ (𝑠 × 𝑘) ∧ ¬ 𝑡 ∈ 𝑥) ∧ ((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘𝑡) = 𝑏) ↔ (𝑡 ∈ (𝑠 × 𝑘) ∧ (¬ 𝑡 ∈ 𝑥 ∧ ((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘𝑡) = 𝑏)))
81	79, 80	bitri 264	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑡 ∈ ((𝑠 × 𝑘) ∖ 𝑥) ∧ ((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘𝑡) = 𝑏) ↔ (𝑡 ∈ (𝑠 × 𝑘) ∧ (¬ 𝑡 ∈ 𝑥 ∧ ((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘𝑡) = 𝑏)))
82	81	rexbii2 3039	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (∃𝑡 ∈ ((𝑠 × 𝑘) ∖ 𝑥)((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘𝑡) = 𝑏 ↔ ∃𝑡 ∈ (𝑠 × 𝑘)(¬ 𝑡 ∈ 𝑥 ∧ ((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘𝑡) = 𝑏))
83		ancom 466	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((¬ 𝑡 ∈ 𝑥 ∧ ((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘𝑡) = 𝑏) ↔ (((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘𝑡) = 𝑏 ∧ ¬ 𝑡 ∈ 𝑥))
84		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑡 = ⟨𝑎, 𝑢⟩ → ((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘𝑡) = ((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘⟨𝑎, 𝑢⟩))
85	84	eqeq1d 2624	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑡 = ⟨𝑎, 𝑢⟩ → (((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘𝑡) = 𝑏 ↔ ((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘⟨𝑎, 𝑢⟩) = 𝑏))
86		eleq1 2689	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑡 = ⟨𝑎, 𝑢⟩ → (𝑡 ∈ 𝑥 ↔ ⟨𝑎, 𝑢⟩ ∈ 𝑥))
87	86	notbid 308	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑡 = ⟨𝑎, 𝑢⟩ → (¬ 𝑡 ∈ 𝑥 ↔ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥))
88	85, 87	anbi12d 747	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑡 = ⟨𝑎, 𝑢⟩ → ((((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘𝑡) = 𝑏 ∧ ¬ 𝑡 ∈ 𝑥) ↔ (((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘⟨𝑎, 𝑢⟩) = 𝑏 ∧ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥)))
89	83, 88	syl5bb 272	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑡 = ⟨𝑎, 𝑢⟩ → ((¬ 𝑡 ∈ 𝑥 ∧ ((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘𝑡) = 𝑏) ↔ (((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘⟨𝑎, 𝑢⟩) = 𝑏 ∧ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥)))
90	89	rexxp 5264	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (∃𝑡 ∈ (𝑠 × 𝑘)(¬ 𝑡 ∈ 𝑥 ∧ ((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘𝑡) = 𝑏) ↔ ∃𝑎 ∈ 𝑠 ∃𝑢 ∈ 𝑘 (((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘⟨𝑎, 𝑢⟩) = 𝑏 ∧ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥))
91	82, 90	bitri 264	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (∃𝑡 ∈ ((𝑠 × 𝑘) ∖ 𝑥)((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘𝑡) = 𝑏 ↔ ∃𝑎 ∈ 𝑠 ∃𝑢 ∈ 𝑘 (((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘⟨𝑎, 𝑢⟩) = 𝑏 ∧ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥))
92		simpl 473	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) → 𝑠 ⊆ ∪ 𝑅)
93	92	sselda 3603	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) ∧ 𝑎 ∈ 𝑠) → 𝑎 ∈ ∪ 𝑅)
94	93	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) ∧ 𝑎 ∈ 𝑠) ∧ 𝑢 ∈ 𝑘) → 𝑎 ∈ ∪ 𝑅)
95		simplr 792	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) ∧ 𝑎 ∈ 𝑠) → 𝑘 ⊆ ∪ 𝑆)
96	95	sselda 3603	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) ∧ 𝑎 ∈ 𝑠) ∧ 𝑢 ∈ 𝑘) → 𝑢 ∈ ∪ 𝑆)
97	94, 96	opelxpd 5149	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) ∧ 𝑎 ∈ 𝑠) ∧ 𝑢 ∈ 𝑘) → ⟨𝑎, 𝑢⟩ ∈ (∪ 𝑅 × ∪ 𝑆))
98	97	fvresd 6208	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) ∧ 𝑎 ∈ 𝑠) ∧ 𝑢 ∈ 𝑘) → ((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘⟨𝑎, 𝑢⟩) = (2nd ‘⟨𝑎, 𝑢⟩))
99		vex 3203	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ 𝑎 ∈ V
100		vex 3203	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ 𝑢 ∈ V
101	99, 100	op2nd 7177	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (2nd ‘⟨𝑎, 𝑢⟩) = 𝑢
102	98, 101	syl6eq 2672	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) ∧ 𝑎 ∈ 𝑠) ∧ 𝑢 ∈ 𝑘) → ((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘⟨𝑎, 𝑢⟩) = 𝑢)
103	102	eqeq1d 2624	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) ∧ 𝑎 ∈ 𝑠) ∧ 𝑢 ∈ 𝑘) → (((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘⟨𝑎, 𝑢⟩) = 𝑏 ↔ 𝑢 = 𝑏))
104	103	anbi1d 741	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) ∧ 𝑎 ∈ 𝑠) ∧ 𝑢 ∈ 𝑘) → ((((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘⟨𝑎, 𝑢⟩) = 𝑏 ∧ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥) ↔ (𝑢 = 𝑏 ∧ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥)))
105	104	rexbidva 3049	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) ∧ 𝑎 ∈ 𝑠) → (∃𝑢 ∈ 𝑘 (((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘⟨𝑎, 𝑢⟩) = 𝑏 ∧ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥) ↔ ∃𝑢 ∈ 𝑘 (𝑢 = 𝑏 ∧ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥)))
106		opeq2 4403	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑢 = 𝑏 → ⟨𝑎, 𝑢⟩ = ⟨𝑎, 𝑏⟩)
107	106	eleq1d 2686	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑢 = 𝑏 → (⟨𝑎, 𝑢⟩ ∈ 𝑥 ↔ ⟨𝑎, 𝑏⟩ ∈ 𝑥))
108	107	notbid 308	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑢 = 𝑏 → (¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥 ↔ ¬ ⟨𝑎, 𝑏⟩ ∈ 𝑥))
109	108	ceqsrexbv 3337	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (∃𝑢 ∈ 𝑘 (𝑢 = 𝑏 ∧ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥) ↔ (𝑏 ∈ 𝑘 ∧ ¬ ⟨𝑎, 𝑏⟩ ∈ 𝑥))
110	105, 109	syl6bb 276	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) ∧ 𝑎 ∈ 𝑠) → (∃𝑢 ∈ 𝑘 (((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘⟨𝑎, 𝑢⟩) = 𝑏 ∧ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥) ↔ (𝑏 ∈ 𝑘 ∧ ¬ ⟨𝑎, 𝑏⟩ ∈ 𝑥)))
111	110	rexbidva 3049	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) → (∃𝑎 ∈ 𝑠 ∃𝑢 ∈ 𝑘 (((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘⟨𝑎, 𝑢⟩) = 𝑏 ∧ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥) ↔ ∃𝑎 ∈ 𝑠 (𝑏 ∈ 𝑘 ∧ ¬ ⟨𝑎, 𝑏⟩ ∈ 𝑥)))
112		r19.42v 3092	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (∃𝑎 ∈ 𝑠 (𝑏 ∈ 𝑘 ∧ ¬ ⟨𝑎, 𝑏⟩ ∈ 𝑥) ↔ (𝑏 ∈ 𝑘 ∧ ∃𝑎 ∈ 𝑠 ¬ ⟨𝑎, 𝑏⟩ ∈ 𝑥))
113	111, 112	syl6bb 276	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) → (∃𝑎 ∈ 𝑠 ∃𝑢 ∈ 𝑘 (((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘⟨𝑎, 𝑢⟩) = 𝑏 ∧ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥) ↔ (𝑏 ∈ 𝑘 ∧ ∃𝑎 ∈ 𝑠 ¬ ⟨𝑎, 𝑏⟩ ∈ 𝑥)))
114	91, 113	syl5bb 272	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) → (∃𝑡 ∈ ((𝑠 × 𝑘) ∖ 𝑥)((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘𝑡) = 𝑏 ↔ (𝑏 ∈ 𝑘 ∧ ∃𝑎 ∈ 𝑠 ¬ ⟨𝑎, 𝑏⟩ ∈ 𝑥)))
115		f2ndres 7191	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (2nd ↾ (∪ 𝑅 × ∪ 𝑆)):(∪ 𝑅 × ∪ 𝑆)⟶∪ 𝑆
116		ffn 6045	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)):(∪ 𝑅 × ∪ 𝑆)⟶∪ 𝑆 → (2nd ↾ (∪ 𝑅 × ∪ 𝑆)) Fn (∪ 𝑅 × ∪ 𝑆))
117	115, 116	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (2nd ↾ (∪ 𝑅 × ∪ 𝑆)) Fn (∪ 𝑅 × ∪ 𝑆)
118		difss 3737	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑠 × 𝑘) ∖ 𝑥) ⊆ (𝑠 × 𝑘)
119		xpss12 5225	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) → (𝑠 × 𝑘) ⊆ (∪ 𝑅 × ∪ 𝑆))
120	118, 119	syl5ss 3614	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) → ((𝑠 × 𝑘) ∖ 𝑥) ⊆ (∪ 𝑅 × ∪ 𝑆))
121		fvelimab 6253	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) Fn (∪ 𝑅 × ∪ 𝑆) ∧ ((𝑠 × 𝑘) ∖ 𝑥) ⊆ (∪ 𝑅 × ∪ 𝑆)) → (𝑏 ∈ ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ↔ ∃𝑡 ∈ ((𝑠 × 𝑘) ∖ 𝑥)((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘𝑡) = 𝑏))
122	117, 120, 121	sylancr 695	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) → (𝑏 ∈ ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ↔ ∃𝑡 ∈ ((𝑠 × 𝑘) ∖ 𝑥)((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘𝑡) = 𝑏))
123		eldif 3584	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑏 ∈ (𝑘 ∖ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ↔ (𝑏 ∈ 𝑘 ∧ ¬ 𝑏 ∈ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}))
124		simpr 477	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) → 𝑘 ⊆ ∪ 𝑆)
125	124	sselda 3603	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) ∧ 𝑏 ∈ 𝑘) → 𝑏 ∈ ∪ 𝑆)
126		sneq 4187	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑣 = 𝑏 → {𝑣} = {𝑏})
127	126	xpeq2d 5139	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑣 = 𝑏 → (𝑠 × {𝑣}) = (𝑠 × {𝑏}))
128	127	sseq1d 3632	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑣 = 𝑏 → ((𝑠 × {𝑣}) ⊆ 𝑥 ↔ (𝑠 × {𝑏}) ⊆ 𝑥))
129		dfss3 3592	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑠 × {𝑏}) ⊆ 𝑥 ↔ ∀𝑘 ∈ (𝑠 × {𝑏})𝑘 ∈ 𝑥)
130		eleq1 2689	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑘 = ⟨𝑎, 𝑡⟩ → (𝑘 ∈ 𝑥 ↔ ⟨𝑎, 𝑡⟩ ∈ 𝑥))
131	130	ralxp 5263	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (∀𝑘 ∈ (𝑠 × {𝑏})𝑘 ∈ 𝑥 ↔ ∀𝑎 ∈ 𝑠 ∀𝑡 ∈ {𝑏}⟨𝑎, 𝑡⟩ ∈ 𝑥)
132		vex 3203	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ 𝑏 ∈ V
133		opeq2 4403	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑡 = 𝑏 → ⟨𝑎, 𝑡⟩ = ⟨𝑎, 𝑏⟩)
134	133	eleq1d 2686	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑡 = 𝑏 → (⟨𝑎, 𝑡⟩ ∈ 𝑥 ↔ ⟨𝑎, 𝑏⟩ ∈ 𝑥))
135	132, 134	ralsn 4222	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (∀𝑡 ∈ {𝑏}⟨𝑎, 𝑡⟩ ∈ 𝑥 ↔ ⟨𝑎, 𝑏⟩ ∈ 𝑥)
136	135	ralbii 2980	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (∀𝑎 ∈ 𝑠 ∀𝑡 ∈ {𝑏}⟨𝑎, 𝑡⟩ ∈ 𝑥 ↔ ∀𝑎 ∈ 𝑠 ⟨𝑎, 𝑏⟩ ∈ 𝑥)
137	129, 131, 136	3bitri 286	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑠 × {𝑏}) ⊆ 𝑥 ↔ ∀𝑎 ∈ 𝑠 ⟨𝑎, 𝑏⟩ ∈ 𝑥)
138	128, 137	syl6bb 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑣 = 𝑏 → ((𝑠 × {𝑣}) ⊆ 𝑥 ↔ ∀𝑎 ∈ 𝑠 ⟨𝑎, 𝑏⟩ ∈ 𝑥))
139	138	elrab3 3364	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑏 ∈ ∪ 𝑆 → (𝑏 ∈ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ↔ ∀𝑎 ∈ 𝑠 ⟨𝑎, 𝑏⟩ ∈ 𝑥))
140	125, 139	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) ∧ 𝑏 ∈ 𝑘) → (𝑏 ∈ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ↔ ∀𝑎 ∈ 𝑠 ⟨𝑎, 𝑏⟩ ∈ 𝑥))
141	140	notbid 308	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) ∧ 𝑏 ∈ 𝑘) → (¬ 𝑏 ∈ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ↔ ¬ ∀𝑎 ∈ 𝑠 ⟨𝑎, 𝑏⟩ ∈ 𝑥))
142		rexnal 2995	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (∃𝑎 ∈ 𝑠 ¬ ⟨𝑎, 𝑏⟩ ∈ 𝑥 ↔ ¬ ∀𝑎 ∈ 𝑠 ⟨𝑎, 𝑏⟩ ∈ 𝑥)
143	141, 142	syl6bbr 278	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) ∧ 𝑏 ∈ 𝑘) → (¬ 𝑏 ∈ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ↔ ∃𝑎 ∈ 𝑠 ¬ ⟨𝑎, 𝑏⟩ ∈ 𝑥))
144	143	pm5.32da 673	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) → ((𝑏 ∈ 𝑘 ∧ ¬ 𝑏 ∈ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ↔ (𝑏 ∈ 𝑘 ∧ ∃𝑎 ∈ 𝑠 ¬ ⟨𝑎, 𝑏⟩ ∈ 𝑥)))
145	123, 144	syl5bb 272	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) → (𝑏 ∈ (𝑘 ∖ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ↔ (𝑏 ∈ 𝑘 ∧ ∃𝑎 ∈ 𝑠 ¬ ⟨𝑎, 𝑏⟩ ∈ 𝑥)))
146	114, 122, 145	3bitr4d 300	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) → (𝑏 ∈ ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ↔ 𝑏 ∈ (𝑘 ∖ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})))
147	146	eqrdv 2620	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) → ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) = (𝑘 ∖ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}))
148	75, 77, 147	syl2anc 693	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) = (𝑘 ∖ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}))
149		difin 3861	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∖ (𝑘 ∩ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})) = (𝑘 ∖ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})
150	66	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → 𝑆 ∈ Top)
151	18	restuni 20966	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑆 ∈ Top ∧ 𝑘 ⊆ ∪ 𝑆) → 𝑘 = ∪ (𝑆 ↾t 𝑘))
152	150, 77, 151	syl2anc 693	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → 𝑘 = ∪ (𝑆 ↾t 𝑘))
153	152	difeq1d 3727	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → (𝑘 ∖ (𝑘 ∩ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})) = (∪ (𝑆 ↾t 𝑘) ∖ (𝑘 ∩ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})))
154	149, 153	syl5eqr 2670	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → (𝑘 ∖ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) = (∪ (𝑆 ↾t 𝑘) ∖ (𝑘 ∩ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})))
155	148, 154	eqtrd 2656	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) = (∪ (𝑆 ↾t 𝑘) ∖ (𝑘 ∩ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})))
156	16	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → 𝑆 ∈ (ran 𝑘Gen ∩ Haus))
157	156	elin2d 3803	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → 𝑆 ∈ Haus)
158		df-ima 5127	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) = ran ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) ↾ ((𝑠 × 𝑘) ∖ 𝑥))
159		resres 5409	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) ↾ ((𝑠 × 𝑘) ∖ 𝑥)) = (2nd ↾ ((∪ 𝑅 × ∪ 𝑆) ∩ ((𝑠 × 𝑘) ∖ 𝑥)))
160		inss2 3834	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((∪ 𝑅 × ∪ 𝑆) ∩ ((𝑠 × 𝑘) ∖ 𝑥)) ⊆ ((𝑠 × 𝑘) ∖ 𝑥)
161	160, 118	sstri 3612	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((∪ 𝑅 × ∪ 𝑆) ∩ ((𝑠 × 𝑘) ∖ 𝑥)) ⊆ (𝑠 × 𝑘)
162		ssres2 5425	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((∪ 𝑅 × ∪ 𝑆) ∩ ((𝑠 × 𝑘) ∖ 𝑥)) ⊆ (𝑠 × 𝑘) → (2nd ↾ ((∪ 𝑅 × ∪ 𝑆) ∩ ((𝑠 × 𝑘) ∖ 𝑥))) ⊆ (2nd ↾ (𝑠 × 𝑘)))
163	161, 162	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (2nd ↾ ((∪ 𝑅 × ∪ 𝑆) ∩ ((𝑠 × 𝑘) ∖ 𝑥))) ⊆ (2nd ↾ (𝑠 × 𝑘))
164	159, 163	eqsstri 3635	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) ↾ ((𝑠 × 𝑘) ∖ 𝑥)) ⊆ (2nd ↾ (𝑠 × 𝑘))
165		rnss 5354	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) ↾ ((𝑠 × 𝑘) ∖ 𝑥)) ⊆ (2nd ↾ (𝑠 × 𝑘)) → ran ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) ↾ ((𝑠 × 𝑘) ∖ 𝑥)) ⊆ ran (2nd ↾ (𝑠 × 𝑘)))
166	164, 165	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ran ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) ↾ ((𝑠 × 𝑘) ∖ 𝑥)) ⊆ ran (2nd ↾ (𝑠 × 𝑘))
167	158, 166	eqsstri 3635	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ⊆ ran (2nd ↾ (𝑠 × 𝑘))
168		f2ndres 7191	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (2nd ↾ (𝑠 × 𝑘)):(𝑠 × 𝑘)⟶𝑘
169		frn 6053	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((2nd ↾ (𝑠 × 𝑘)):(𝑠 × 𝑘)⟶𝑘 → ran (2nd ↾ (𝑠 × 𝑘)) ⊆ 𝑘)
170	168, 169	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ran (2nd ↾ (𝑠 × 𝑘)) ⊆ 𝑘
171	167, 170	sstri 3612	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ⊆ 𝑘
172	171, 77	syl5ss 3614	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ⊆ ∪ 𝑆)
173	13	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → 𝑅 ∈ (TopOn‘∪ 𝑅))
174	150, 19	sylib 208	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → 𝑆 ∈ (TopOn‘∪ 𝑆))
175		tx2cn 21413	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑅 ∈ (TopOn‘∪ 𝑅) ∧ 𝑆 ∈ (TopOn‘∪ 𝑆)) → (2nd ↾ (∪ 𝑅 × ∪ 𝑆)) ∈ ((𝑅 ×t 𝑆) Cn 𝑆))
176	173, 174, 175	syl2anc 693	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → (2nd ↾ (∪ 𝑅 × ∪ 𝑆)) ∈ ((𝑅 ×t 𝑆) Cn 𝑆))
177	27	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → (𝑅 ×t 𝑆) ∈ Top)
178	118	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → ((𝑠 × 𝑘) ∖ 𝑥) ⊆ (𝑠 × 𝑘))
179		vex 3203	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 𝑠 ∈ V
180		vex 3203	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 𝑘 ∈ V
181	179, 180	xpex 6962	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑠 × 𝑘) ∈ V
182	181	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → (𝑠 × 𝑘) ∈ V)
183		restabs 20969	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑅 ×t 𝑆) ∈ Top ∧ ((𝑠 × 𝑘) ∖ 𝑥) ⊆ (𝑠 × 𝑘) ∧ (𝑠 × 𝑘) ∈ V) → (((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ↾t ((𝑠 × 𝑘) ∖ 𝑥)) = ((𝑅 ×t 𝑆) ↾t ((𝑠 × 𝑘) ∖ 𝑥)))
184	177, 178, 182, 183	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → (((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ↾t ((𝑠 × 𝑘) ∖ 𝑥)) = ((𝑅 ×t 𝑆) ↾t ((𝑠 × 𝑘) ∖ 𝑥)))
185	65	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → 𝑅 ∈ Top)
186	156, 4	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → 𝑆 ∈ Top)
187	179	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → 𝑠 ∈ V)
188		simprl 794	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → 𝑘 ∈ 𝒫 ∪ 𝑆)
189		txrest 21434	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑠 ∈ V ∧ 𝑘 ∈ 𝒫 ∪ 𝑆)) → ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) = ((𝑅 ↾t 𝑠) ×t (𝑆 ↾t 𝑘)))
190	185, 186, 187, 188, 189	syl22anc 1327	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) = ((𝑅 ↾t 𝑠) ×t (𝑆 ↾t 𝑘)))
191		simprr3 1111	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → (𝑅 ↾t 𝑠) ∈ Comp)
192	191	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → (𝑅 ↾t 𝑠) ∈ Comp)
193		simprr 796	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → (𝑆 ↾t 𝑘) ∈ Comp)
194		txcmp 21446	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑅 ↾t 𝑠) ∈ Comp ∧ (𝑆 ↾t 𝑘) ∈ Comp) → ((𝑅 ↾t 𝑠) ×t (𝑆 ↾t 𝑘)) ∈ Comp)
195	192, 193, 194	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → ((𝑅 ↾t 𝑠) ×t (𝑆 ↾t 𝑘)) ∈ Comp)
196	190, 195	eqeltrd 2701	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ∈ Comp)
197		difin 3861	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑠 × 𝑘) ∖ ((𝑠 × 𝑘) ∩ 𝑥)) = ((𝑠 × 𝑘) ∖ 𝑥)
198	75, 77, 119	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → (𝑠 × 𝑘) ⊆ (∪ 𝑅 × ∪ 𝑆))
199	185, 150, 25	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → (∪ 𝑅 × ∪ 𝑆) = ∪ (𝑅 ×t 𝑆))
200	198, 199	sseqtrd 3641	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → (𝑠 × 𝑘) ⊆ ∪ (𝑅 ×t 𝑆))
201	28	restuni 20966	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑅 ×t 𝑆) ∈ Top ∧ (𝑠 × 𝑘) ⊆ ∪ (𝑅 ×t 𝑆)) → (𝑠 × 𝑘) = ∪ ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)))
202	177, 200, 201	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → (𝑠 × 𝑘) = ∪ ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)))
203	202	difeq1d 3727	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → ((𝑠 × 𝑘) ∖ ((𝑠 × 𝑘) ∩ 𝑥)) = (∪ ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ∖ ((𝑠 × 𝑘) ∩ 𝑥)))
204	197, 203	syl5eqr 2670	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → ((𝑠 × 𝑘) ∖ 𝑥) = (∪ ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ∖ ((𝑠 × 𝑘) ∩ 𝑥)))
205		resttop 20964	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑅 ×t 𝑆) ∈ Top ∧ (𝑠 × 𝑘) ∈ V) → ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ∈ Top)
206	177, 181, 205	sylancl 694	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ∈ Top)
207		incom 3805	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑠 × 𝑘) ∩ 𝑥) = (𝑥 ∩ (𝑠 × 𝑘))
208	22	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆)))
209		kgeni 21340	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆)) ∧ ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ∈ Comp) → (𝑥 ∩ (𝑠 × 𝑘)) ∈ ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)))
210	208, 196, 209	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → (𝑥 ∩ (𝑠 × 𝑘)) ∈ ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)))
211	207, 210	syl5eqel 2705	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → ((𝑠 × 𝑘) ∩ 𝑥) ∈ ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)))
212		eqid 2622	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ∪ ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) = ∪ ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘))
213	212	opncld 20837	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ∈ Top ∧ ((𝑠 × 𝑘) ∩ 𝑥) ∈ ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘))) → (∪ ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ∖ ((𝑠 × 𝑘) ∩ 𝑥)) ∈ (Clsd‘((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘))))
214	206, 211, 213	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → (∪ ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ∖ ((𝑠 × 𝑘) ∩ 𝑥)) ∈ (Clsd‘((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘))))
215	204, 214	eqeltrd 2701	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → ((𝑠 × 𝑘) ∖ 𝑥) ∈ (Clsd‘((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘))))
216		cmpcld 21205	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ∈ Comp ∧ ((𝑠 × 𝑘) ∖ 𝑥) ∈ (Clsd‘((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)))) → (((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ↾t ((𝑠 × 𝑘) ∖ 𝑥)) ∈ Comp)
217	196, 215, 216	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → (((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ↾t ((𝑠 × 𝑘) ∖ 𝑥)) ∈ Comp)
218	184, 217	eqeltrrd 2702	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → ((𝑅 ×t 𝑆) ↾t ((𝑠 × 𝑘) ∖ 𝑥)) ∈ Comp)
219		imacmp 21200	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) ∈ ((𝑅 ×t 𝑆) Cn 𝑆) ∧ ((𝑅 ×t 𝑆) ↾t ((𝑠 × 𝑘) ∖ 𝑥)) ∈ Comp) → (𝑆 ↾t ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥))) ∈ Comp)
220	176, 218, 219	syl2anc 693	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → (𝑆 ↾t ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥))) ∈ Comp)
221	18	hauscmp 21210	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑆 ∈ Haus ∧ ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ⊆ ∪ 𝑆 ∧ (𝑆 ↾t ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥))) ∈ Comp) → ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ∈ (Clsd‘𝑆))
222	157, 172, 220, 221	syl3anc 1326	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ∈ (Clsd‘𝑆))
223	171	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ⊆ 𝑘)
224	18	restcldi 20977	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑘 ⊆ ∪ 𝑆 ∧ ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ∈ (Clsd‘𝑆) ∧ ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ⊆ 𝑘) → ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ∈ (Clsd‘(𝑆 ↾t 𝑘)))
225	77, 222, 223, 224	syl3anc 1326	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ∈ (Clsd‘(𝑆 ↾t 𝑘)))
226	155, 225	eqeltrrd 2702	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → (∪ (𝑆 ↾t 𝑘) ∖ (𝑘 ∩ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})) ∈ (Clsd‘(𝑆 ↾t 𝑘)))
227		resttop 20964	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑆 ∈ Top ∧ 𝑘 ∈ 𝒫 ∪ 𝑆) → (𝑆 ↾t 𝑘) ∈ Top)
228	150, 188, 227	syl2anc 693	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → (𝑆 ↾t 𝑘) ∈ Top)
229		inss1 3833	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 ∩ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ⊆ 𝑘
230	229, 152	syl5sseq 3653	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → (𝑘 ∩ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ⊆ ∪ (𝑆 ↾t 𝑘))
231		eqid 2622	. . . . . . . . . . . . . . . . . . 19 ⊢ ∪ (𝑆 ↾t 𝑘) = ∪ (𝑆 ↾t 𝑘)
232	231	isopn2 20836	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑆 ↾t 𝑘) ∈ Top ∧ (𝑘 ∩ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ⊆ ∪ (𝑆 ↾t 𝑘)) → ((𝑘 ∩ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ∈ (𝑆 ↾t 𝑘) ↔ (∪ (𝑆 ↾t 𝑘) ∖ (𝑘 ∩ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})) ∈ (Clsd‘(𝑆 ↾t 𝑘))))
233	228, 230, 232	syl2anc 693	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → ((𝑘 ∩ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ∈ (𝑆 ↾t 𝑘) ↔ (∪ (𝑆 ↾t 𝑘) ∖ (𝑘 ∩ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})) ∈ (Clsd‘(𝑆 ↾t 𝑘))))
234	226, 233	mpbird 247	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → (𝑘 ∩ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ∈ (𝑆 ↾t 𝑘))
235	70, 234	syl5eqel 2705	. . . . . . . . . . . . . . 15 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → ({𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ∩ 𝑘) ∈ (𝑆 ↾t 𝑘))
236	235	expr 643	. . . . . . . . . . . . . 14 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ 𝑘 ∈ 𝒫 ∪ 𝑆) → ((𝑆 ↾t 𝑘) ∈ Comp → ({𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ∩ 𝑘) ∈ (𝑆 ↾t 𝑘)))
237	236	ralrimiva 2966	. . . . . . . . . . . . 13 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → ∀𝑘 ∈ 𝒫 ∪ 𝑆((𝑆 ↾t 𝑘) ∈ Comp → ({𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ∩ 𝑘) ∈ (𝑆 ↾t 𝑘)))
238	66, 19	sylib 208	. . . . . . . . . . . . . 14 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → 𝑆 ∈ (TopOn‘∪ 𝑆))
239		elkgen 21339	. . . . . . . . . . . . . 14 ⊢ (𝑆 ∈ (TopOn‘∪ 𝑆) → ({𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ∈ (𝑘Gen‘𝑆) ↔ ({𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ⊆ ∪ 𝑆 ∧ ∀𝑘 ∈ 𝒫 ∪ 𝑆((𝑆 ↾t 𝑘) ∈ Comp → ({𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ∩ 𝑘) ∈ (𝑆 ↾t 𝑘)))))
240	238, 239	syl 17	. . . . . . . . . . . . 13 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → ({𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ∈ (𝑘Gen‘𝑆) ↔ ({𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ⊆ ∪ 𝑆 ∧ ∀𝑘 ∈ 𝒫 ∪ 𝑆((𝑆 ↾t 𝑘) ∈ Comp → ({𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ∩ 𝑘) ∈ (𝑆 ↾t 𝑘)))))
241	69, 237, 240	mpbir2and 957	. . . . . . . . . . . 12 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ∈ (𝑘Gen‘𝑆))
242	16	adantr 481	. . . . . . . . . . . . . 14 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → 𝑆 ∈ (ran 𝑘Gen ∩ Haus))
243	242, 2	syl 17	. . . . . . . . . . . . 13 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → 𝑆 ∈ ran 𝑘Gen)
244		kgenidm 21350	. . . . . . . . . . . . 13 ⊢ (𝑆 ∈ ran 𝑘Gen → (𝑘Gen‘𝑆) = 𝑆)
245	243, 244	syl 17	. . . . . . . . . . . 12 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → (𝑘Gen‘𝑆) = 𝑆)
246	241, 245	eleqtrd 2703	. . . . . . . . . . 11 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ∈ 𝑆)
247		txopn 21405	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑢 ∈ 𝑅 ∧ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ∈ 𝑆)) → (𝑢 × {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ∈ (𝑅 ×t 𝑆))
248	65, 66, 67, 246, 247	syl22anc 1327	. . . . . . . . . 10 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → (𝑢 × {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ∈ (𝑅 ×t 𝑆))
249	57	adantr 481	. . . . . . . . . . 11 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → 𝑦 = ⟨(1st ‘𝑦), (2nd ‘𝑦)⟩)
250		simprr1 1109	. . . . . . . . . . . 12 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → (1st ‘𝑦) ∈ 𝑢)
251	34	adantr 481	. . . . . . . . . . . . 13 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → (2nd ‘𝑦) ∈ ∪ 𝑆)
252		relxp 5227	. . . . . . . . . . . . . . 15 ⊢ Rel (𝑠 × {(2nd ‘𝑦)})
253	252	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → Rel (𝑠 × {(2nd ‘𝑦)}))
254		opelxp 5146	. . . . . . . . . . . . . . 15 ⊢ (⟨𝑎, 𝑏⟩ ∈ (𝑠 × {(2nd ‘𝑦)}) ↔ (𝑎 ∈ 𝑠 ∧ 𝑏 ∈ {(2nd ‘𝑦)}))
255	72	sselda 3603	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ 𝑎 ∈ 𝑠) → 𝑎 ∈ {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥})
256		opeq1 4402	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑡 = 𝑎 → ⟨𝑡, (2nd ‘𝑦)⟩ = ⟨𝑎, (2nd ‘𝑦)⟩)
257	256	eleq1d 2686	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 = 𝑎 → (⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥 ↔ ⟨𝑎, (2nd ‘𝑦)⟩ ∈ 𝑥))
258	257	elrab 3363	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 ∈ {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ↔ (𝑎 ∈ ∪ 𝑅 ∧ ⟨𝑎, (2nd ‘𝑦)⟩ ∈ 𝑥))
259	258	simprbi 480	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 ∈ {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} → ⟨𝑎, (2nd ‘𝑦)⟩ ∈ 𝑥)
260	255, 259	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ 𝑎 ∈ 𝑠) → ⟨𝑎, (2nd ‘𝑦)⟩ ∈ 𝑥)
261		elsni 4194	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 ∈ {(2nd ‘𝑦)} → 𝑏 = (2nd ‘𝑦))
262	261	opeq2d 4409	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 ∈ {(2nd ‘𝑦)} → ⟨𝑎, 𝑏⟩ = ⟨𝑎, (2nd ‘𝑦)⟩)
263	262	eleq1d 2686	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 ∈ {(2nd ‘𝑦)} → (⟨𝑎, 𝑏⟩ ∈ 𝑥 ↔ ⟨𝑎, (2nd ‘𝑦)⟩ ∈ 𝑥))
264	260, 263	syl5ibrcom 237	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ 𝑎 ∈ 𝑠) → (𝑏 ∈ {(2nd ‘𝑦)} → ⟨𝑎, 𝑏⟩ ∈ 𝑥))
265	264	expimpd 629	. . . . . . . . . . . . . . 15 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → ((𝑎 ∈ 𝑠 ∧ 𝑏 ∈ {(2nd ‘𝑦)}) → ⟨𝑎, 𝑏⟩ ∈ 𝑥))
266	254, 265	syl5bi 232	. . . . . . . . . . . . . 14 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → (⟨𝑎, 𝑏⟩ ∈ (𝑠 × {(2nd ‘𝑦)}) → ⟨𝑎, 𝑏⟩ ∈ 𝑥))
267	253, 266	relssdv 5212	. . . . . . . . . . . . 13 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → (𝑠 × {(2nd ‘𝑦)}) ⊆ 𝑥)
268		sneq 4187	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 = (2nd ‘𝑦) → {𝑣} = {(2nd ‘𝑦)})
269	268	xpeq2d 5139	. . . . . . . . . . . . . . 15 ⊢ (𝑣 = (2nd ‘𝑦) → (𝑠 × {𝑣}) = (𝑠 × {(2nd ‘𝑦)}))
270	269	sseq1d 3632	. . . . . . . . . . . . . 14 ⊢ (𝑣 = (2nd ‘𝑦) → ((𝑠 × {𝑣}) ⊆ 𝑥 ↔ (𝑠 × {(2nd ‘𝑦)}) ⊆ 𝑥))
271	270	elrab 3363	. . . . . . . . . . . . 13 ⊢ ((2nd ‘𝑦) ∈ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ↔ ((2nd ‘𝑦) ∈ ∪ 𝑆 ∧ (𝑠 × {(2nd ‘𝑦)}) ⊆ 𝑥))
272	251, 267, 271	sylanbrc 698	. . . . . . . . . . . 12 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → (2nd ‘𝑦) ∈ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})
273	250, 272	opelxpd 5149	. . . . . . . . . . 11 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → ⟨(1st ‘𝑦), (2nd ‘𝑦)⟩ ∈ (𝑢 × {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}))
274	249, 273	eqeltrd 2701	. . . . . . . . . 10 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → 𝑦 ∈ (𝑢 × {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}))
275		relxp 5227	. . . . . . . . . . . 12 ⊢ Rel (𝑢 × {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})
276	275	a1i 11	. . . . . . . . . . 11 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → Rel (𝑢 × {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}))
277		opelxp 5146	. . . . . . . . . . . 12 ⊢ (⟨𝑎, 𝑏⟩ ∈ (𝑢 × {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ↔ (𝑎 ∈ 𝑢 ∧ 𝑏 ∈ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}))
278	128	elrab 3363	. . . . . . . . . . . . . . 15 ⊢ (𝑏 ∈ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ↔ (𝑏 ∈ ∪ 𝑆 ∧ (𝑠 × {𝑏}) ⊆ 𝑥))
279	278	simprbi 480	. . . . . . . . . . . . . 14 ⊢ (𝑏 ∈ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} → (𝑠 × {𝑏}) ⊆ 𝑥)
280		simprr2 1110	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → 𝑢 ⊆ 𝑠)
281	280	sselda 3603	. . . . . . . . . . . . . . 15 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ 𝑎 ∈ 𝑢) → 𝑎 ∈ 𝑠)
282		vsnid 4209	. . . . . . . . . . . . . . 15 ⊢ 𝑏 ∈ {𝑏}
283		opelxpi 5148	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 ∈ 𝑠 ∧ 𝑏 ∈ {𝑏}) → ⟨𝑎, 𝑏⟩ ∈ (𝑠 × {𝑏}))
284	281, 282, 283	sylancl 694	. . . . . . . . . . . . . 14 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ 𝑎 ∈ 𝑢) → ⟨𝑎, 𝑏⟩ ∈ (𝑠 × {𝑏}))
285		ssel 3597	. . . . . . . . . . . . . 14 ⊢ ((𝑠 × {𝑏}) ⊆ 𝑥 → (⟨𝑎, 𝑏⟩ ∈ (𝑠 × {𝑏}) → ⟨𝑎, 𝑏⟩ ∈ 𝑥))
286	279, 284, 285	syl2imc 41	. . . . . . . . . . . . 13 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ 𝑎 ∈ 𝑢) → (𝑏 ∈ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} → ⟨𝑎, 𝑏⟩ ∈ 𝑥))
287	286	expimpd 629	. . . . . . . . . . . 12 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → ((𝑎 ∈ 𝑢 ∧ 𝑏 ∈ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) → ⟨𝑎, 𝑏⟩ ∈ 𝑥))
288	277, 287	syl5bi 232	. . . . . . . . . . 11 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → (⟨𝑎, 𝑏⟩ ∈ (𝑢 × {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) → ⟨𝑎, 𝑏⟩ ∈ 𝑥))
289	276, 288	relssdv 5212	. . . . . . . . . 10 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → (𝑢 × {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ⊆ 𝑥)
290		eleq2 2690	. . . . . . . . . . . 12 ⊢ (𝑡 = (𝑢 × {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) → (𝑦 ∈ 𝑡 ↔ 𝑦 ∈ (𝑢 × {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})))
291		sseq1 3626	. . . . . . . . . . . 12 ⊢ (𝑡 = (𝑢 × {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) → (𝑡 ⊆ 𝑥 ↔ (𝑢 × {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ⊆ 𝑥))
292	290, 291	anbi12d 747	. . . . . . . . . . 11 ⊢ (𝑡 = (𝑢 × {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) → ((𝑦 ∈ 𝑡 ∧ 𝑡 ⊆ 𝑥) ↔ (𝑦 ∈ (𝑢 × {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ∧ (𝑢 × {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ⊆ 𝑥)))
293	292	rspcev 3309	. . . . . . . . . 10 ⊢ (((𝑢 × {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ∈ (𝑅 ×t 𝑆) ∧ (𝑦 ∈ (𝑢 × {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ∧ (𝑢 × {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ⊆ 𝑥)) → ∃𝑡 ∈ (𝑅 ×t 𝑆)(𝑦 ∈ 𝑡 ∧ 𝑡 ⊆ 𝑥))
294	248, 274, 289, 293	syl12anc 1324	. . . . . . . . 9 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → ∃𝑡 ∈ (𝑅 ×t 𝑆)(𝑦 ∈ 𝑡 ∧ 𝑡 ⊆ 𝑥))
295	294	expr 643	. . . . . . . 8 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ (𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅)) → (((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp) → ∃𝑡 ∈ (𝑅 ×t 𝑆)(𝑦 ∈ 𝑡 ∧ 𝑡 ⊆ 𝑥)))
296	295	rexlimdvva 3038	. . . . . . 7 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → (∃𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥}∃𝑢 ∈ 𝑅 ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp) → ∃𝑡 ∈ (𝑅 ×t 𝑆)(𝑦 ∈ 𝑡 ∧ 𝑡 ⊆ 𝑥)))
297	64, 296	mpd 15	. . . . . 6 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → ∃𝑡 ∈ (𝑅 ×t 𝑆)(𝑦 ∈ 𝑡 ∧ 𝑡 ⊆ 𝑥))
298	297	ralrimiva 2966	. . . . 5 ⊢ (((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) → ∀𝑦 ∈ 𝑥 ∃𝑡 ∈ (𝑅 ×t 𝑆)(𝑦 ∈ 𝑡 ∧ 𝑡 ⊆ 𝑥))
299	6	adantr 481	. . . . . 6 ⊢ (((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) → (𝑅 ×t 𝑆) ∈ Top)
300		eltop2 20779	. . . . . 6 ⊢ ((𝑅 ×t 𝑆) ∈ Top → (𝑥 ∈ (𝑅 ×t 𝑆) ↔ ∀𝑦 ∈ 𝑥 ∃𝑡 ∈ (𝑅 ×t 𝑆)(𝑦 ∈ 𝑡 ∧ 𝑡 ⊆ 𝑥)))
301	299, 300	syl 17	. . . . 5 ⊢ (((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) → (𝑥 ∈ (𝑅 ×t 𝑆) ↔ ∀𝑦 ∈ 𝑥 ∃𝑡 ∈ (𝑅 ×t 𝑆)(𝑦 ∈ 𝑡 ∧ 𝑡 ⊆ 𝑥)))
302	298, 301	mpbird 247	. . . 4 ⊢ (((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) → 𝑥 ∈ (𝑅 ×t 𝑆))
303	302	ex 450	. . 3 ⊢ ((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) → (𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆)) → 𝑥 ∈ (𝑅 ×t 𝑆)))
304	303	ssrdv 3609	. 2 ⊢ ((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) → (𝑘Gen‘(𝑅 ×t 𝑆)) ⊆ (𝑅 ×t 𝑆))
305		iskgen2 21351	. 2 ⊢ ((𝑅 ×t 𝑆) ∈ ran 𝑘Gen ↔ ((𝑅 ×t 𝑆) ∈ Top ∧ (𝑘Gen‘(𝑅 ×t 𝑆)) ⊆ (𝑅 ×t 𝑆)))
306	6, 304, 305	sylanbrc 698	1 ⊢ ((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) → (𝑅 ×t 𝑆) ∈ ran 𝑘Gen)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∧ wa 384   ∧ w3a 1037   = wceq 1483   ∈ wcel 1990  ∀wral 2912  ∃wrex 2913  {crab 2916  Vcvv 3200   ∖ cdif 3571   ∩ cin 3573   ⊆ wss 3574  𝒫 cpw 4158  {csn 4177  ⟨cop 4183  ∪ cuni 4436   ↦ cmpt 4729   I cid 5023   × cxp 5112  ^◡ccnv 5113  ran crn 5115   ↾ cres 5116   “ cima 5117  Rel wrel 5119   Fn wfn 5883  ⟶wf 5884  ‘cfv 5888  (class class class)co 6650  1^st c1st 7166  2^nd c2nd 7167   ↾_t crest 16081  Topctop 20698  TopOnctopon 20715  Clsdccld 20820   Cn ccn 21028  Hauscha 21112  Compccmp 21189  𝑛-Locally cnlly 21268  𝑘Genckgen 21336   ×_t ctx 21363

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-reu 2919  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-int 4476  df-iun 4522  df-iin 4523  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-om 7066  df-1st 7168  df-2nd 7169  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-1o 7560  df-oadd 7564  df-er 7742  df-map 7859  df-en 7956  df-dom 7957  df-fin 7959  df-fi 8317  df-rest 16083  df-topgen 16104  df-top 20699  df-topon 20716  df-bases 20750  df-cld 20823  df-ntr 20824  df-cls 20825  df-nei 20902  df-cn 21031  df-cnp 21032  df-haus 21119  df-cmp 21190  df-nlly 21270  df-kgen 21337  df-tx 21365

This theorem is referenced by: (None)