Theorem txkgen 23643

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 23464	. . 3 ⊢ (𝑅 ∈ 𝑛-Locally Comp → 𝑅 ∈ Top)
2		elinel1 4195	. . . 4 ⊢ (𝑆 ∈ (ran 𝑘Gen ∩ Haus) → 𝑆 ∈ ran 𝑘Gen)
3		kgentop 23533	. . . 4 ⊢ (𝑆 ∈ ran 𝑘Gen → 𝑆 ∈ Top)
4	2, 3	syl 17	. . 3 ⊢ (𝑆 ∈ (ran 𝑘Gen ∩ Haus) → 𝑆 ∈ Top)
5		txtop 23560	. . 3 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑅 ×t 𝑆) ∈ Top)
6	1, 4, 5	syl2an 594	. 2 ⊢ ((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) → (𝑅 ×t 𝑆) ∈ Top)
7		simplll 773	. . . . . . . 8 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → 𝑅 ∈ 𝑛-Locally Comp)
8		eqid 2726	. . . . . . . . . 10 ⊢ (𝑡 ∈ ∪ 𝑅 ↦ ⟨𝑡, (2nd ‘𝑦)⟩) = (𝑡 ∈ ∪ 𝑅 ↦ ⟨𝑡, (2nd ‘𝑦)⟩)
9	8	mptpreima 6241	. . . . . . . . 9 ⊢ (◡(𝑡 ∈ ∪ 𝑅 ↦ ⟨𝑡, (2nd ‘𝑦)⟩) “ 𝑥) = {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥}
10	1	ad3antrrr 728	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → 𝑅 ∈ Top)
11		toptopon2 22907	. . . . . . . . . . . . . 14 ⊢ (𝑅 ∈ Top ↔ 𝑅 ∈ (TopOn‘∪ 𝑅))
12	10, 11	sylib 217	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → 𝑅 ∈ (TopOn‘∪ 𝑅))
13		idcn 23248	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ (TopOn‘∪ 𝑅) → ( I ↾ ∪ 𝑅) ∈ (𝑅 Cn 𝑅))
14	12, 13	syl 17	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → ( I ↾ ∪ 𝑅) ∈ (𝑅 Cn 𝑅))
15		simpllr 774	. . . . . . . . . . . . . . 15 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → 𝑆 ∈ (ran 𝑘Gen ∩ Haus))
16	15, 4	syl 17	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → 𝑆 ∈ Top)
17		toptopon2 22907	. . . . . . . . . . . . . 14 ⊢ (𝑆 ∈ Top ↔ 𝑆 ∈ (TopOn‘∪ 𝑆))
18	16, 17	sylib 217	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → 𝑆 ∈ (TopOn‘∪ 𝑆))
19		simpr 483	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ 𝑥)
20		simplr 767	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆)))
21		elunii 4912	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) → 𝑦 ∈ ∪ (𝑘Gen‘(𝑅 ×t 𝑆)))
22	19, 20, 21	syl2anc 582	. . . . . . . . . . . . . . 15 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ ∪ (𝑘Gen‘(𝑅 ×t 𝑆)))
23		eqid 2726	. . . . . . . . . . . . . . . . . 18 ⊢ ∪ 𝑅 = ∪ 𝑅
24		eqid 2726	. . . . . . . . . . . . . . . . . 18 ⊢ ∪ 𝑆 = ∪ 𝑆
25	23, 24	txuni 23583	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (∪ 𝑅 × ∪ 𝑆) = ∪ (𝑅 ×t 𝑆))
26	10, 16, 25	syl2anc 582	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → (∪ 𝑅 × ∪ 𝑆) = ∪ (𝑅 ×t 𝑆))
27	10, 16, 5	syl2anc 582	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → (𝑅 ×t 𝑆) ∈ Top)
28		eqid 2726	. . . . . . . . . . . . . . . . . 18 ⊢ ∪ (𝑅 ×t 𝑆) = ∪ (𝑅 ×t 𝑆)
29	28	kgenuni 23530	. . . . . . . . . . . . . . . . 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 2766	. . . . . . . . . . . . . . 15 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → (∪ 𝑅 × ∪ 𝑆) = ∪ (𝑘Gen‘(𝑅 ×t 𝑆)))
32	22, 31	eleqtrrd 2829	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ (∪ 𝑅 × ∪ 𝑆))
33		xp2nd 8027	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ (∪ 𝑅 × ∪ 𝑆) → (2nd ‘𝑦) ∈ ∪ 𝑆)
34	32, 33	syl 17	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → (2nd ‘𝑦) ∈ ∪ 𝑆)
35		cnconst2 23274	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ (TopOn‘∪ 𝑅) ∧ 𝑆 ∈ (TopOn‘∪ 𝑆) ∧ (2nd ‘𝑦) ∈ ∪ 𝑆) → (∪ 𝑅 × {(2nd ‘𝑦)}) ∈ (𝑅 Cn 𝑆))
36	12, 18, 34, 35	syl3anc 1368	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → (∪ 𝑅 × {(2nd ‘𝑦)}) ∈ (𝑅 Cn 𝑆))
37		fvresi 7178	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 ∈ ∪ 𝑅 → (( I ↾ ∪ 𝑅)‘𝑡) = 𝑡)
38		fvex 6905	. . . . . . . . . . . . . . . . 17 ⊢ (2nd ‘𝑦) ∈ V
39	38	fvconst2 7212	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 ∈ ∪ 𝑅 → ((∪ 𝑅 × {(2nd ‘𝑦)})‘𝑡) = (2nd ‘𝑦))
40	37, 39	opeq12d 4881	. . . . . . . . . . . . . . 15 ⊢ (𝑡 ∈ ∪ 𝑅 → ⟨(( I ↾ ∪ 𝑅)‘𝑡), ((∪ 𝑅 × {(2nd ‘𝑦)})‘𝑡)⟩ = ⟨𝑡, (2nd ‘𝑦)⟩)
41	40	mpteq2ia 5248	. . . . . . . . . . . . . 14 ⊢ (𝑡 ∈ ∪ 𝑅 ↦ ⟨(( I ↾ ∪ 𝑅)‘𝑡), ((∪ 𝑅 × {(2nd ‘𝑦)})‘𝑡)⟩) = (𝑡 ∈ ∪ 𝑅 ↦ ⟨𝑡, (2nd ‘𝑦)⟩)
42	41	eqcomi 2735	. . . . . . . . . . . . 13 ⊢ (𝑡 ∈ ∪ 𝑅 ↦ ⟨𝑡, (2nd ‘𝑦)⟩) = (𝑡 ∈ ∪ 𝑅 ↦ ⟨(( I ↾ ∪ 𝑅)‘𝑡), ((∪ 𝑅 × {(2nd ‘𝑦)})‘𝑡)⟩)
43	23, 42	txcnmpt 23615	. . . . . . . . . . . 12 ⊢ ((( I ↾ ∪ 𝑅) ∈ (𝑅 Cn 𝑅) ∧ (∪ 𝑅 × {(2nd ‘𝑦)}) ∈ (𝑅 Cn 𝑆)) → (𝑡 ∈ ∪ 𝑅 ↦ ⟨𝑡, (2nd ‘𝑦)⟩) ∈ (𝑅 Cn (𝑅 ×t 𝑆)))
44	14, 36, 43	syl2anc 582	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → (𝑡 ∈ ∪ 𝑅 ↦ ⟨𝑡, (2nd ‘𝑦)⟩) ∈ (𝑅 Cn (𝑅 ×t 𝑆)))
45		llycmpkgen 23543	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ 𝑛-Locally Comp → 𝑅 ∈ ran 𝑘Gen)
46	45	ad3antrrr 728	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → 𝑅 ∈ ran 𝑘Gen)
47	6	ad2antrr 724	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → (𝑅 ×t 𝑆) ∈ Top)
48		kgencn3 23549	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ ran 𝑘Gen ∧ (𝑅 ×t 𝑆) ∈ Top) → (𝑅 Cn (𝑅 ×t 𝑆)) = (𝑅 Cn (𝑘Gen‘(𝑅 ×t 𝑆))))
49	46, 47, 48	syl2anc 582	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → (𝑅 Cn (𝑅 ×t 𝑆)) = (𝑅 Cn (𝑘Gen‘(𝑅 ×t 𝑆))))
50	44, 49	eleqtrd 2828	. . . . . . . . . 10 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → (𝑡 ∈ ∪ 𝑅 ↦ ⟨𝑡, (2nd ‘𝑦)⟩) ∈ (𝑅 Cn (𝑘Gen‘(𝑅 ×t 𝑆))))
51		cnima 23256	. . . . . . . . . 10 ⊢ (((𝑡 ∈ ∪ 𝑅 ↦ ⟨𝑡, (2nd ‘𝑦)⟩) ∈ (𝑅 Cn (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) → (◡(𝑡 ∈ ∪ 𝑅 ↦ ⟨𝑡, (2nd ‘𝑦)⟩) “ 𝑥) ∈ 𝑅)
52	50, 20, 51	syl2anc 582	. . . . . . . . 9 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → (◡(𝑡 ∈ ∪ 𝑅 ↦ ⟨𝑡, (2nd ‘𝑦)⟩) “ 𝑥) ∈ 𝑅)
53	9, 52	eqeltrrid 2831	. . . . . . . 8 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∈ 𝑅)
54		opeq1 4873	. . . . . . . . . 10 ⊢ (𝑡 = (1st ‘𝑦) → ⟨𝑡, (2nd ‘𝑦)⟩ = ⟨(1st ‘𝑦), (2nd ‘𝑦)⟩)
55	54	eleq1d 2811	. . . . . . . . 9 ⊢ (𝑡 = (1st ‘𝑦) → (⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥 ↔ ⟨(1st ‘𝑦), (2nd ‘𝑦)⟩ ∈ 𝑥))
56		xp1st 8026	. . . . . . . . . 10 ⊢ (𝑦 ∈ (∪ 𝑅 × ∪ 𝑆) → (1st ‘𝑦) ∈ ∪ 𝑅)
57	32, 56	syl 17	. . . . . . . . 9 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → (1st ‘𝑦) ∈ ∪ 𝑅)
58		1st2nd2 8033	. . . . . . . . . . 11 ⊢ (𝑦 ∈ (∪ 𝑅 × ∪ 𝑆) → 𝑦 = ⟨(1st ‘𝑦), (2nd ‘𝑦)⟩)
59	32, 58	syl 17	. . . . . . . . . 10 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → 𝑦 = ⟨(1st ‘𝑦), (2nd ‘𝑦)⟩)
60	59, 19	eqeltrrd 2827	. . . . . . . . 9 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → ⟨(1st ‘𝑦), (2nd ‘𝑦)⟩ ∈ 𝑥)
61	55, 57, 60	elrabd 3684	. . . . . . . 8 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → (1st ‘𝑦) ∈ {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥})
62		nlly2i 23467	. . . . . . . 8 ⊢ ((𝑅 ∈ 𝑛-Locally Comp ∧ {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∈ 𝑅 ∧ (1st ‘𝑦) ∈ {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥}) → ∃𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥}∃𝑢 ∈ 𝑅 ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))
63	7, 53, 61, 62	syl3anc 1368	. . . . . . 7 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → ∃𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥}∃𝑢 ∈ 𝑅 ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))
64	10	adantr 479	. . . . . . . . . . 11 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → 𝑅 ∈ Top)
65	16	adantr 479	. . . . . . . . . . 11 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → 𝑆 ∈ Top)
66		simprlr 778	. . . . . . . . . . 11 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → 𝑢 ∈ 𝑅)
67		ssrab2 4075	. . . . . . . . . . . . . 14 ⊢ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ⊆ ∪ 𝑆
68	67	a1i 11	. . . . . . . . . . . . 13 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ⊆ ∪ 𝑆)
69		incom 4201	. . . . . . . . . . . . . . . 16 ⊢ ({𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ∩ 𝑘) = (𝑘 ∩ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})
70		simprll 777	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → 𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥})
71	70	elpwid 4608	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → 𝑠 ⊆ {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥})
72		ssrab2 4075	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ⊆ ∪ 𝑅
73	71, 72	sstrdi 3993	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → 𝑠 ⊆ ∪ 𝑅)
74	73	adantr 479	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → 𝑠 ⊆ ∪ 𝑅)
75		elpwi 4606	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 ∈ 𝒫 ∪ 𝑆 → 𝑘 ⊆ ∪ 𝑆)
76	75	ad2antrl 726	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → 𝑘 ⊆ ∪ 𝑆)
77		eldif 3958	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑡 ∈ ((𝑠 × 𝑘) ∖ 𝑥) ↔ (𝑡 ∈ (𝑠 × 𝑘) ∧ ¬ 𝑡 ∈ 𝑥))
78	77	anbi1i 622	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑡 ∈ ((𝑠 × 𝑘) ∖ 𝑥) ∧ ((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘𝑡) = 𝑏) ↔ ((𝑡 ∈ (𝑠 × 𝑘) ∧ ¬ 𝑡 ∈ 𝑥) ∧ ((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘𝑡) = 𝑏))
79		anass 467	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑡 ∈ (𝑠 × 𝑘) ∧ ¬ 𝑡 ∈ 𝑥) ∧ ((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘𝑡) = 𝑏) ↔ (𝑡 ∈ (𝑠 × 𝑘) ∧ (¬ 𝑡 ∈ 𝑥 ∧ ((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘𝑡) = 𝑏)))
80	78, 79	bitri 274	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑡 ∈ ((𝑠 × 𝑘) ∖ 𝑥) ∧ ((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘𝑡) = 𝑏) ↔ (𝑡 ∈ (𝑠 × 𝑘) ∧ (¬ 𝑡 ∈ 𝑥 ∧ ((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘𝑡) = 𝑏)))
81	80	rexbii2 3080	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (∃𝑡 ∈ ((𝑠 × 𝑘) ∖ 𝑥)((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘𝑡) = 𝑏 ↔ ∃𝑡 ∈ (𝑠 × 𝑘)(¬ 𝑡 ∈ 𝑥 ∧ ((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘𝑡) = 𝑏))
82		ancom 459	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((¬ 𝑡 ∈ 𝑥 ∧ ((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘𝑡) = 𝑏) ↔ (((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘𝑡) = 𝑏 ∧ ¬ 𝑡 ∈ 𝑥))
83		fveqeq2 6901	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑡 = ⟨𝑎, 𝑢⟩ → (((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘𝑡) = 𝑏 ↔ ((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘⟨𝑎, 𝑢⟩) = 𝑏))
84		eleq1 2814	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑡 = ⟨𝑎, 𝑢⟩ → (𝑡 ∈ 𝑥 ↔ ⟨𝑎, 𝑢⟩ ∈ 𝑥))
85	84	notbid 317	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑡 = ⟨𝑎, 𝑢⟩ → (¬ 𝑡 ∈ 𝑥 ↔ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥))
86	83, 85	anbi12d 630	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑡 = ⟨𝑎, 𝑢⟩ → ((((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘𝑡) = 𝑏 ∧ ¬ 𝑡 ∈ 𝑥) ↔ (((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘⟨𝑎, 𝑢⟩) = 𝑏 ∧ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥)))
87	82, 86	bitrid 282	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑡 = ⟨𝑎, 𝑢⟩ → ((¬ 𝑡 ∈ 𝑥 ∧ ((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘𝑡) = 𝑏) ↔ (((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘⟨𝑎, 𝑢⟩) = 𝑏 ∧ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥)))
88	87	rexxp 5841	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (∃𝑡 ∈ (𝑠 × 𝑘)(¬ 𝑡 ∈ 𝑥 ∧ ((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘𝑡) = 𝑏) ↔ ∃𝑎 ∈ 𝑠 ∃𝑢 ∈ 𝑘 (((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘⟨𝑎, 𝑢⟩) = 𝑏 ∧ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥))
89	81, 88	bitri 274	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (∃𝑡 ∈ ((𝑠 × 𝑘) ∖ 𝑥)((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘𝑡) = 𝑏 ↔ ∃𝑎 ∈ 𝑠 ∃𝑢 ∈ 𝑘 (((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘⟨𝑎, 𝑢⟩) = 𝑏 ∧ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥))
90		simpl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) → 𝑠 ⊆ ∪ 𝑅)
91	90	sselda 3980	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) ∧ 𝑎 ∈ 𝑠) → 𝑎 ∈ ∪ 𝑅)
92	91	adantr 479	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) ∧ 𝑎 ∈ 𝑠) ∧ 𝑢 ∈ 𝑘) → 𝑎 ∈ ∪ 𝑅)
93		simplr 767	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) ∧ 𝑎 ∈ 𝑠) → 𝑘 ⊆ ∪ 𝑆)
94	93	sselda 3980	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) ∧ 𝑎 ∈ 𝑠) ∧ 𝑢 ∈ 𝑘) → 𝑢 ∈ ∪ 𝑆)
95	92, 94	opelxpd 5713	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) ∧ 𝑎 ∈ 𝑠) ∧ 𝑢 ∈ 𝑘) → ⟨𝑎, 𝑢⟩ ∈ (∪ 𝑅 × ∪ 𝑆))
96	95	fvresd 6912	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) ∧ 𝑎 ∈ 𝑠) ∧ 𝑢 ∈ 𝑘) → ((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘⟨𝑎, 𝑢⟩) = (2nd ‘⟨𝑎, 𝑢⟩))
97		vex 3468	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ 𝑎 ∈ V
98		vex 3468	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ 𝑢 ∈ V
99	97, 98	op2nd 8003	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (2nd ‘⟨𝑎, 𝑢⟩) = 𝑢
100	96, 99	eqtrdi 2782	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) ∧ 𝑎 ∈ 𝑠) ∧ 𝑢 ∈ 𝑘) → ((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘⟨𝑎, 𝑢⟩) = 𝑢)
101	100	eqeq1d 2728	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) ∧ 𝑎 ∈ 𝑠) ∧ 𝑢 ∈ 𝑘) → (((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘⟨𝑎, 𝑢⟩) = 𝑏 ↔ 𝑢 = 𝑏))
102	101	anbi1d 629	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) ∧ 𝑎 ∈ 𝑠) ∧ 𝑢 ∈ 𝑘) → ((((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘⟨𝑎, 𝑢⟩) = 𝑏 ∧ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥) ↔ (𝑢 = 𝑏 ∧ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥)))
103	102	rexbidva 3167	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) ∧ 𝑎 ∈ 𝑠) → (∃𝑢 ∈ 𝑘 (((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘⟨𝑎, 𝑢⟩) = 𝑏 ∧ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥) ↔ ∃𝑢 ∈ 𝑘 (𝑢 = 𝑏 ∧ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥)))
104		opeq2 4874	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑢 = 𝑏 → ⟨𝑎, 𝑢⟩ = ⟨𝑎, 𝑏⟩)
105	104	eleq1d 2811	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑢 = 𝑏 → (⟨𝑎, 𝑢⟩ ∈ 𝑥 ↔ ⟨𝑎, 𝑏⟩ ∈ 𝑥))
106	105	notbid 317	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑢 = 𝑏 → (¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥 ↔ ¬ ⟨𝑎, 𝑏⟩ ∈ 𝑥))
107	106	ceqsrexbv 3642	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (∃𝑢 ∈ 𝑘 (𝑢 = 𝑏 ∧ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥) ↔ (𝑏 ∈ 𝑘 ∧ ¬ ⟨𝑎, 𝑏⟩ ∈ 𝑥))
108	103, 107	bitrdi 286	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) ∧ 𝑎 ∈ 𝑠) → (∃𝑢 ∈ 𝑘 (((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘⟨𝑎, 𝑢⟩) = 𝑏 ∧ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥) ↔ (𝑏 ∈ 𝑘 ∧ ¬ ⟨𝑎, 𝑏⟩ ∈ 𝑥)))
109	108	rexbidva 3167	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) → (∃𝑎 ∈ 𝑠 ∃𝑢 ∈ 𝑘 (((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘⟨𝑎, 𝑢⟩) = 𝑏 ∧ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥) ↔ ∃𝑎 ∈ 𝑠 (𝑏 ∈ 𝑘 ∧ ¬ ⟨𝑎, 𝑏⟩ ∈ 𝑥)))
110		r19.42v 3181	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (∃𝑎 ∈ 𝑠 (𝑏 ∈ 𝑘 ∧ ¬ ⟨𝑎, 𝑏⟩ ∈ 𝑥) ↔ (𝑏 ∈ 𝑘 ∧ ∃𝑎 ∈ 𝑠 ¬ ⟨𝑎, 𝑏⟩ ∈ 𝑥))
111	109, 110	bitrdi 286	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) → (∃𝑎 ∈ 𝑠 ∃𝑢 ∈ 𝑘 (((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘⟨𝑎, 𝑢⟩) = 𝑏 ∧ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥) ↔ (𝑏 ∈ 𝑘 ∧ ∃𝑎 ∈ 𝑠 ¬ ⟨𝑎, 𝑏⟩ ∈ 𝑥)))
112	89, 111	bitrid 282	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) → (∃𝑡 ∈ ((𝑠 × 𝑘) ∖ 𝑥)((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘𝑡) = 𝑏 ↔ (𝑏 ∈ 𝑘 ∧ ∃𝑎 ∈ 𝑠 ¬ ⟨𝑎, 𝑏⟩ ∈ 𝑥)))
113		f2ndres 8019	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (2nd ↾ (∪ 𝑅 × ∪ 𝑆)):(∪ 𝑅 × ∪ 𝑆)⟶∪ 𝑆
114		ffn 6719	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)):(∪ 𝑅 × ∪ 𝑆)⟶∪ 𝑆 → (2nd ↾ (∪ 𝑅 × ∪ 𝑆)) Fn (∪ 𝑅 × ∪ 𝑆))
115	113, 114	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (2nd ↾ (∪ 𝑅 × ∪ 𝑆)) Fn (∪ 𝑅 × ∪ 𝑆)
116		difss 4130	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑠 × 𝑘) ∖ 𝑥) ⊆ (𝑠 × 𝑘)
117		xpss12 5689	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) → (𝑠 × 𝑘) ⊆ (∪ 𝑅 × ∪ 𝑆))
118	116, 117	sstrid 3992	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) → ((𝑠 × 𝑘) ∖ 𝑥) ⊆ (∪ 𝑅 × ∪ 𝑆))
119		fvelimab 6966	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) Fn (∪ 𝑅 × ∪ 𝑆) ∧ ((𝑠 × 𝑘) ∖ 𝑥) ⊆ (∪ 𝑅 × ∪ 𝑆)) → (𝑏 ∈ ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ↔ ∃𝑡 ∈ ((𝑠 × 𝑘) ∖ 𝑥)((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘𝑡) = 𝑏))
120	115, 118, 119	sylancr 585	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) → (𝑏 ∈ ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ↔ ∃𝑡 ∈ ((𝑠 × 𝑘) ∖ 𝑥)((2nd ↾ (∪ 𝑅 × ∪ 𝑆))‘𝑡) = 𝑏))
121		eldif 3958	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑏 ∈ (𝑘 ∖ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ↔ (𝑏 ∈ 𝑘 ∧ ¬ 𝑏 ∈ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}))
122		simpr 483	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) → 𝑘 ⊆ ∪ 𝑆)
123	122	sselda 3980	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) ∧ 𝑏 ∈ 𝑘) → 𝑏 ∈ ∪ 𝑆)
124		sneq 4635	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑣 = 𝑏 → {𝑣} = {𝑏})
125	124	xpeq2d 5704	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑣 = 𝑏 → (𝑠 × {𝑣}) = (𝑠 × {𝑏}))
126	125	sseq1d 4012	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑣 = 𝑏 → ((𝑠 × {𝑣}) ⊆ 𝑥 ↔ (𝑠 × {𝑏}) ⊆ 𝑥))
127		dfss3 3969	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑠 × {𝑏}) ⊆ 𝑥 ↔ ∀𝑘 ∈ (𝑠 × {𝑏})𝑘 ∈ 𝑥)
128		eleq1 2814	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑘 = ⟨𝑎, 𝑡⟩ → (𝑘 ∈ 𝑥 ↔ ⟨𝑎, 𝑡⟩ ∈ 𝑥))
129	128	ralxp 5840	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (∀𝑘 ∈ (𝑠 × {𝑏})𝑘 ∈ 𝑥 ↔ ∀𝑎 ∈ 𝑠 ∀𝑡 ∈ {𝑏}⟨𝑎, 𝑡⟩ ∈ 𝑥)
130		vex 3468	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ 𝑏 ∈ V
131		opeq2 4874	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑡 = 𝑏 → ⟨𝑎, 𝑡⟩ = ⟨𝑎, 𝑏⟩)
132	131	eleq1d 2811	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑡 = 𝑏 → (⟨𝑎, 𝑡⟩ ∈ 𝑥 ↔ ⟨𝑎, 𝑏⟩ ∈ 𝑥))
133	130, 132	ralsn 4682	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (∀𝑡 ∈ {𝑏}⟨𝑎, 𝑡⟩ ∈ 𝑥 ↔ ⟨𝑎, 𝑏⟩ ∈ 𝑥)
134	133	ralbii 3083	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (∀𝑎 ∈ 𝑠 ∀𝑡 ∈ {𝑏}⟨𝑎, 𝑡⟩ ∈ 𝑥 ↔ ∀𝑎 ∈ 𝑠 ⟨𝑎, 𝑏⟩ ∈ 𝑥)
135	127, 129, 134	3bitri 296	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑠 × {𝑏}) ⊆ 𝑥 ↔ ∀𝑎 ∈ 𝑠 ⟨𝑎, 𝑏⟩ ∈ 𝑥)
136	126, 135	bitrdi 286	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑣 = 𝑏 → ((𝑠 × {𝑣}) ⊆ 𝑥 ↔ ∀𝑎 ∈ 𝑠 ⟨𝑎, 𝑏⟩ ∈ 𝑥))
137	136	elrab3 3683	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑏 ∈ ∪ 𝑆 → (𝑏 ∈ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ↔ ∀𝑎 ∈ 𝑠 ⟨𝑎, 𝑏⟩ ∈ 𝑥))
138	123, 137	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) ∧ 𝑏 ∈ 𝑘) → (𝑏 ∈ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ↔ ∀𝑎 ∈ 𝑠 ⟨𝑎, 𝑏⟩ ∈ 𝑥))
139	138	notbid 317	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) ∧ 𝑏 ∈ 𝑘) → (¬ 𝑏 ∈ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ↔ ¬ ∀𝑎 ∈ 𝑠 ⟨𝑎, 𝑏⟩ ∈ 𝑥))
140		rexnal 3090	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (∃𝑎 ∈ 𝑠 ¬ ⟨𝑎, 𝑏⟩ ∈ 𝑥 ↔ ¬ ∀𝑎 ∈ 𝑠 ⟨𝑎, 𝑏⟩ ∈ 𝑥)
141	139, 140	bitr4di 288	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) ∧ 𝑏 ∈ 𝑘) → (¬ 𝑏 ∈ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ↔ ∃𝑎 ∈ 𝑠 ¬ ⟨𝑎, 𝑏⟩ ∈ 𝑥))
142	141	pm5.32da 577	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) → ((𝑏 ∈ 𝑘 ∧ ¬ 𝑏 ∈ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ↔ (𝑏 ∈ 𝑘 ∧ ∃𝑎 ∈ 𝑠 ¬ ⟨𝑎, 𝑏⟩ ∈ 𝑥)))
143	121, 142	bitrid 282	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) → (𝑏 ∈ (𝑘 ∖ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ↔ (𝑏 ∈ 𝑘 ∧ ∃𝑎 ∈ 𝑠 ¬ ⟨𝑎, 𝑏⟩ ∈ 𝑥)))
144	112, 120, 143	3bitr4d 310	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) → (𝑏 ∈ ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ↔ 𝑏 ∈ (𝑘 ∖ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})))
145	144	eqrdv 2724	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆) → ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) = (𝑘 ∖ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}))
146	74, 76, 145	syl2anc 582	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) = (𝑘 ∖ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}))
147		difin 4262	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∖ (𝑘 ∩ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})) = (𝑘 ∖ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})
148	65	adantr 479	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → 𝑆 ∈ Top)
149	24	restuni 23153	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑆 ∈ Top ∧ 𝑘 ⊆ ∪ 𝑆) → 𝑘 = ∪ (𝑆 ↾t 𝑘))
150	148, 76, 149	syl2anc 582	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → 𝑘 = ∪ (𝑆 ↾t 𝑘))
151	150	difeq1d 4119	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → (𝑘 ∖ (𝑘 ∩ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})) = (∪ (𝑆 ↾t 𝑘) ∖ (𝑘 ∩ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})))
152	147, 151	eqtr3id 2780	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → (𝑘 ∖ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) = (∪ (𝑆 ↾t 𝑘) ∖ (𝑘 ∩ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})))
153	146, 152	eqtrd 2766	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) = (∪ (𝑆 ↾t 𝑘) ∖ (𝑘 ∩ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})))
154	15	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → 𝑆 ∈ (ran 𝑘Gen ∩ Haus))
155	154	elin2d 4199	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → 𝑆 ∈ Haus)
156		df-ima 5687	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) = ran ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) ↾ ((𝑠 × 𝑘) ∖ 𝑥))
157		resres 5994	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) ↾ ((𝑠 × 𝑘) ∖ 𝑥)) = (2nd ↾ ((∪ 𝑅 × ∪ 𝑆) ∩ ((𝑠 × 𝑘) ∖ 𝑥)))
158		inss2 4230	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((∪ 𝑅 × ∪ 𝑆) ∩ ((𝑠 × 𝑘) ∖ 𝑥)) ⊆ ((𝑠 × 𝑘) ∖ 𝑥)
159	158, 116	sstri 3990	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((∪ 𝑅 × ∪ 𝑆) ∩ ((𝑠 × 𝑘) ∖ 𝑥)) ⊆ (𝑠 × 𝑘)
160		ssres2 6006	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((∪ 𝑅 × ∪ 𝑆) ∩ ((𝑠 × 𝑘) ∖ 𝑥)) ⊆ (𝑠 × 𝑘) → (2nd ↾ ((∪ 𝑅 × ∪ 𝑆) ∩ ((𝑠 × 𝑘) ∖ 𝑥))) ⊆ (2nd ↾ (𝑠 × 𝑘)))
161	159, 160	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (2nd ↾ ((∪ 𝑅 × ∪ 𝑆) ∩ ((𝑠 × 𝑘) ∖ 𝑥))) ⊆ (2nd ↾ (𝑠 × 𝑘))
162	157, 161	eqsstri 4015	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) ↾ ((𝑠 × 𝑘) ∖ 𝑥)) ⊆ (2nd ↾ (𝑠 × 𝑘))
163	162	rnssi 5938	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ran ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) ↾ ((𝑠 × 𝑘) ∖ 𝑥)) ⊆ ran (2nd ↾ (𝑠 × 𝑘))
164	156, 163	eqsstri 4015	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ⊆ ran (2nd ↾ (𝑠 × 𝑘))
165		f2ndres 8019	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (2nd ↾ (𝑠 × 𝑘)):(𝑠 × 𝑘)⟶𝑘
166		frn 6726	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((2nd ↾ (𝑠 × 𝑘)):(𝑠 × 𝑘)⟶𝑘 → ran (2nd ↾ (𝑠 × 𝑘)) ⊆ 𝑘)
167	165, 166	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ran (2nd ↾ (𝑠 × 𝑘)) ⊆ 𝑘
168	164, 167	sstri 3990	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ⊆ 𝑘
169	168, 76	sstrid 3992	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ⊆ ∪ 𝑆)
170	12	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → 𝑅 ∈ (TopOn‘∪ 𝑅))
171	148, 17	sylib 217	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → 𝑆 ∈ (TopOn‘∪ 𝑆))
172		tx2cn 23601	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑅 ∈ (TopOn‘∪ 𝑅) ∧ 𝑆 ∈ (TopOn‘∪ 𝑆)) → (2nd ↾ (∪ 𝑅 × ∪ 𝑆)) ∈ ((𝑅 ×t 𝑆) Cn 𝑆))
173	170, 171, 172	syl2anc 582	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → (2nd ↾ (∪ 𝑅 × ∪ 𝑆)) ∈ ((𝑅 ×t 𝑆) Cn 𝑆))
174	27	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . . 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 3468	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 𝑠 ∈ V
177		vex 3468	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 𝑘 ∈ V
178	176, 177	xpex 7752	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑠 × 𝑘) ∈ V
179	178	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → (𝑠 × 𝑘) ∈ V)
180		restabs 23156	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑅 ×t 𝑆) ∈ Top ∧ ((𝑠 × 𝑘) ∖ 𝑥) ⊆ (𝑠 × 𝑘) ∧ (𝑠 × 𝑘) ∈ V) → (((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ↾t ((𝑠 × 𝑘) ∖ 𝑥)) = ((𝑅 ×t 𝑆) ↾t ((𝑠 × 𝑘) ∖ 𝑥)))
181	174, 175, 179, 180	syl3anc 1368	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → (((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ↾t ((𝑠 × 𝑘) ∖ 𝑥)) = ((𝑅 ×t 𝑆) ↾t ((𝑠 × 𝑘) ∖ 𝑥)))
182	64	adantr 479	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → 𝑅 ∈ Top)
183	154, 4	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → 𝑆 ∈ Top)
184	176	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → 𝑠 ∈ V)
185		simprl 769	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → 𝑘 ∈ 𝒫 ∪ 𝑆)
186		txrest 23622	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑠 ∈ V ∧ 𝑘 ∈ 𝒫 ∪ 𝑆)) → ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) = ((𝑅 ↾t 𝑠) ×t (𝑆 ↾t 𝑘)))
187	182, 183, 184, 185, 186	syl22anc 837	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) = ((𝑅 ↾t 𝑠) ×t (𝑆 ↾t 𝑘)))
188		simprr3 1220	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → (𝑅 ↾t 𝑠) ∈ Comp)
189	188	adantr 479	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → (𝑅 ↾t 𝑠) ∈ Comp)
190		simprr 771	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → (𝑆 ↾t 𝑘) ∈ Comp)
191		txcmp 23634	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑅 ↾t 𝑠) ∈ Comp ∧ (𝑆 ↾t 𝑘) ∈ Comp) → ((𝑅 ↾t 𝑠) ×t (𝑆 ↾t 𝑘)) ∈ Comp)
192	189, 190, 191	syl2anc 582	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → ((𝑅 ↾t 𝑠) ×t (𝑆 ↾t 𝑘)) ∈ Comp)
193	187, 192	eqeltrd 2826	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ∈ Comp)
194		difin 4262	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑠 × 𝑘) ∖ ((𝑠 × 𝑘) ∩ 𝑥)) = ((𝑠 × 𝑘) ∖ 𝑥)
195	74, 76, 117	syl2anc 582	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → (𝑠 × 𝑘) ⊆ (∪ 𝑅 × ∪ 𝑆))
196	182, 148, 25	syl2anc 582	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → (∪ 𝑅 × ∪ 𝑆) = ∪ (𝑅 ×t 𝑆))
197	195, 196	sseqtrd 4021	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → (𝑠 × 𝑘) ⊆ ∪ (𝑅 ×t 𝑆))
198	28	restuni 23153	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑅 ×t 𝑆) ∈ Top ∧ (𝑠 × 𝑘) ⊆ ∪ (𝑅 ×t 𝑆)) → (𝑠 × 𝑘) = ∪ ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)))
199	174, 197, 198	syl2anc 582	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → (𝑠 × 𝑘) = ∪ ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)))
200	199	difeq1d 4119	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → ((𝑠 × 𝑘) ∖ ((𝑠 × 𝑘) ∩ 𝑥)) = (∪ ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ∖ ((𝑠 × 𝑘) ∩ 𝑥)))
201	194, 200	eqtr3id 2780	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → ((𝑠 × 𝑘) ∖ 𝑥) = (∪ ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ∖ ((𝑠 × 𝑘) ∩ 𝑥)))
202		resttop 23151	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑅 ×t 𝑆) ∈ Top ∧ (𝑠 × 𝑘) ∈ V) → ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ∈ Top)
203	174, 178, 202	sylancl 584	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ∈ Top)
204		incom 4201	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑠 × 𝑘) ∩ 𝑥) = (𝑥 ∩ (𝑠 × 𝑘))
205	20	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆)))
206		kgeni 23528	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆)) ∧ ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ∈ Comp) → (𝑥 ∩ (𝑠 × 𝑘)) ∈ ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)))
207	205, 193, 206	syl2anc 582	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → (𝑥 ∩ (𝑠 × 𝑘)) ∈ ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)))
208	204, 207	eqeltrid 2830	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → ((𝑠 × 𝑘) ∩ 𝑥) ∈ ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)))
209		eqid 2726	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ∪ ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) = ∪ ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘))
210	209	opncld 23024	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ∈ Top ∧ ((𝑠 × 𝑘) ∩ 𝑥) ∈ ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘))) → (∪ ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ∖ ((𝑠 × 𝑘) ∩ 𝑥)) ∈ (Clsd‘((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘))))
211	203, 208, 210	syl2anc 582	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → (∪ ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ∖ ((𝑠 × 𝑘) ∩ 𝑥)) ∈ (Clsd‘((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘))))
212	201, 211	eqeltrd 2826	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → ((𝑠 × 𝑘) ∖ 𝑥) ∈ (Clsd‘((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘))))
213		cmpcld 23393	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ∈ Comp ∧ ((𝑠 × 𝑘) ∖ 𝑥) ∈ (Clsd‘((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)))) → (((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ↾t ((𝑠 × 𝑘) ∖ 𝑥)) ∈ Comp)
214	193, 212, 213	syl2anc 582	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → (((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ↾t ((𝑠 × 𝑘) ∖ 𝑥)) ∈ Comp)
215	181, 214	eqeltrrd 2827	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → ((𝑅 ×t 𝑆) ↾t ((𝑠 × 𝑘) ∖ 𝑥)) ∈ Comp)
216		imacmp 23388	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) ∈ ((𝑅 ×t 𝑆) Cn 𝑆) ∧ ((𝑅 ×t 𝑆) ↾t ((𝑠 × 𝑘) ∖ 𝑥)) ∈ Comp) → (𝑆 ↾t ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥))) ∈ Comp)
217	173, 215, 216	syl2anc 582	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → (𝑆 ↾t ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥))) ∈ Comp)
218	24	hauscmp 23398	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑆 ∈ Haus ∧ ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ⊆ ∪ 𝑆 ∧ (𝑆 ↾t ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥))) ∈ Comp) → ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ∈ (Clsd‘𝑆))
219	155, 169, 217, 218	syl3anc 1368	. . . . . . . . . . . . . . . . . . 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 23164	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑘 ⊆ ∪ 𝑆 ∧ ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ∈ (Clsd‘𝑆) ∧ ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ⊆ 𝑘) → ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ∈ (Clsd‘(𝑆 ↾t 𝑘)))
222	76, 219, 220, 221	syl3anc 1368	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ∈ (Clsd‘(𝑆 ↾t 𝑘)))
223	153, 222	eqeltrrd 2827	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → (∪ (𝑆 ↾t 𝑘) ∖ (𝑘 ∩ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})) ∈ (Clsd‘(𝑆 ↾t 𝑘)))
224		resttop 23151	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑆 ∈ Top ∧ 𝑘 ∈ 𝒫 ∪ 𝑆) → (𝑆 ↾t 𝑘) ∈ Top)
225	148, 185, 224	syl2anc 582	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → (𝑆 ↾t 𝑘) ∈ Top)
226		inss1 4229	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 ∩ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ⊆ 𝑘
227	226, 150	sseqtrid 4033	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → (𝑘 ∩ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ⊆ ∪ (𝑆 ↾t 𝑘))
228		eqid 2726	. . . . . . . . . . . . . . . . . . 19 ⊢ ∪ (𝑆 ↾t 𝑘) = ∪ (𝑆 ↾t 𝑘)
229	228	isopn2 23023	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑆 ↾t 𝑘) ∈ Top ∧ (𝑘 ∩ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ⊆ ∪ (𝑆 ↾t 𝑘)) → ((𝑘 ∩ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ∈ (𝑆 ↾t 𝑘) ↔ (∪ (𝑆 ↾t 𝑘) ∖ (𝑘 ∩ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})) ∈ (Clsd‘(𝑆 ↾t 𝑘))))
230	225, 227, 229	syl2anc 582	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → ((𝑘 ∩ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ∈ (𝑆 ↾t 𝑘) ↔ (∪ (𝑆 ↾t 𝑘) ∖ (𝑘 ∩ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})) ∈ (Clsd‘(𝑆 ↾t 𝑘))))
231	223, 230	mpbird 256	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → (𝑘 ∩ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ∈ (𝑆 ↾t 𝑘))
232	69, 231	eqeltrid 2830	. . . . . . . . . . . . . . 15 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 ∪ 𝑆 ∧ (𝑆 ↾t 𝑘) ∈ Comp)) → ({𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ∩ 𝑘) ∈ (𝑆 ↾t 𝑘))
233	232	expr 455	. . . . . . . . . . . . . 14 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ 𝑘 ∈ 𝒫 ∪ 𝑆) → ((𝑆 ↾t 𝑘) ∈ Comp → ({𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ∩ 𝑘) ∈ (𝑆 ↾t 𝑘)))
234	233	ralrimiva 3136	. . . . . . . . . . . . 13 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → ∀𝑘 ∈ 𝒫 ∪ 𝑆((𝑆 ↾t 𝑘) ∈ Comp → ({𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ∩ 𝑘) ∈ (𝑆 ↾t 𝑘)))
235	65, 17	sylib 217	. . . . . . . . . . . . . 14 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → 𝑆 ∈ (TopOn‘∪ 𝑆))
236		elkgen 23527	. . . . . . . . . . . . . 14 ⊢ (𝑆 ∈ (TopOn‘∪ 𝑆) → ({𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ∈ (𝑘Gen‘𝑆) ↔ ({𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ⊆ ∪ 𝑆 ∧ ∀𝑘 ∈ 𝒫 ∪ 𝑆((𝑆 ↾t 𝑘) ∈ Comp → ({𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ∩ 𝑘) ∈ (𝑆 ↾t 𝑘)))))
237	235, 236	syl 17	. . . . . . . . . . . . 13 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → ({𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ∈ (𝑘Gen‘𝑆) ↔ ({𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ⊆ ∪ 𝑆 ∧ ∀𝑘 ∈ 𝒫 ∪ 𝑆((𝑆 ↾t 𝑘) ∈ Comp → ({𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ∩ 𝑘) ∈ (𝑆 ↾t 𝑘)))))
238	68, 234, 237	mpbir2and 711	. . . . . . . . . . . 12 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ∈ (𝑘Gen‘𝑆))
239	15	adantr 479	. . . . . . . . . . . . . 14 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → 𝑆 ∈ (ran 𝑘Gen ∩ Haus))
240	239, 2	syl 17	. . . . . . . . . . . . 13 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → 𝑆 ∈ ran 𝑘Gen)
241		kgenidm 23538	. . . . . . . . . . . . 13 ⊢ (𝑆 ∈ ran 𝑘Gen → (𝑘Gen‘𝑆) = 𝑆)
242	240, 241	syl 17	. . . . . . . . . . . 12 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → (𝑘Gen‘𝑆) = 𝑆)
243	238, 242	eleqtrd 2828	. . . . . . . . . . 11 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ∈ 𝑆)
244		txopn 23593	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑢 ∈ 𝑅 ∧ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ∈ 𝑆)) → (𝑢 × {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ∈ (𝑅 ×t 𝑆))
245	64, 65, 66, 243, 244	syl22anc 837	. . . . . . . . . 10 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → (𝑢 × {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ∈ (𝑅 ×t 𝑆))
246	59	adantr 479	. . . . . . . . . . 11 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → 𝑦 = ⟨(1st ‘𝑦), (2nd ‘𝑦)⟩)
247		simprr1 1218	. . . . . . . . . . . 12 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → (1st ‘𝑦) ∈ 𝑢)
248		sneq 4635	. . . . . . . . . . . . . . 15 ⊢ (𝑣 = (2nd ‘𝑦) → {𝑣} = {(2nd ‘𝑦)})
249	248	xpeq2d 5704	. . . . . . . . . . . . . 14 ⊢ (𝑣 = (2nd ‘𝑦) → (𝑠 × {𝑣}) = (𝑠 × {(2nd ‘𝑦)}))
250	249	sseq1d 4012	. . . . . . . . . . . . 13 ⊢ (𝑣 = (2nd ‘𝑦) → ((𝑠 × {𝑣}) ⊆ 𝑥 ↔ (𝑠 × {(2nd ‘𝑦)}) ⊆ 𝑥))
251	34	adantr 479	. . . . . . . . . . . . 13 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → (2nd ‘𝑦) ∈ ∪ 𝑆)
252		relxp 5692	. . . . . . . . . . . . . . 15 ⊢ Rel (𝑠 × {(2nd ‘𝑦)})
253	252	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → Rel (𝑠 × {(2nd ‘𝑦)}))
254		opelxp 5710	. . . . . . . . . . . . . . 15 ⊢ (⟨𝑎, 𝑏⟩ ∈ (𝑠 × {(2nd ‘𝑦)}) ↔ (𝑎 ∈ 𝑠 ∧ 𝑏 ∈ {(2nd ‘𝑦)}))
255	71	sselda 3980	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ 𝑎 ∈ 𝑠) → 𝑎 ∈ {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥})
256		opeq1 4873	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑡 = 𝑎 → ⟨𝑡, (2nd ‘𝑦)⟩ = ⟨𝑎, (2nd ‘𝑦)⟩)
257	256	eleq1d 2811	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 = 𝑎 → (⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥 ↔ ⟨𝑎, (2nd ‘𝑦)⟩ ∈ 𝑥))
258	257	elrab 3682	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 ∈ {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ↔ (𝑎 ∈ ∪ 𝑅 ∧ ⟨𝑎, (2nd ‘𝑦)⟩ ∈ 𝑥))
259	258	simprbi 495	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 ∈ {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} → ⟨𝑎, (2nd ‘𝑦)⟩ ∈ 𝑥)
260	255, 259	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ 𝑎 ∈ 𝑠) → ⟨𝑎, (2nd ‘𝑦)⟩ ∈ 𝑥)
261		elsni 4642	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 ∈ {(2nd ‘𝑦)} → 𝑏 = (2nd ‘𝑦))
262	261	opeq2d 4880	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 ∈ {(2nd ‘𝑦)} → ⟨𝑎, 𝑏⟩ = ⟨𝑎, (2nd ‘𝑦)⟩)
263	262	eleq1d 2811	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 ∈ {(2nd ‘𝑦)} → (⟨𝑎, 𝑏⟩ ∈ 𝑥 ↔ ⟨𝑎, (2nd ‘𝑦)⟩ ∈ 𝑥))
264	260, 263	syl5ibrcom 246	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ 𝑎 ∈ 𝑠) → (𝑏 ∈ {(2nd ‘𝑦)} → ⟨𝑎, 𝑏⟩ ∈ 𝑥))
265	264	expimpd 452	. . . . . . . . . . . . . . 15 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → ((𝑎 ∈ 𝑠 ∧ 𝑏 ∈ {(2nd ‘𝑦)}) → ⟨𝑎, 𝑏⟩ ∈ 𝑥))
266	254, 265	biimtrid 241	. . . . . . . . . . . . . 14 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → (⟨𝑎, 𝑏⟩ ∈ (𝑠 × {(2nd ‘𝑦)}) → ⟨𝑎, 𝑏⟩ ∈ 𝑥))
267	253, 266	relssdv 5786	. . . . . . . . . . . . 13 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → (𝑠 × {(2nd ‘𝑦)}) ⊆ 𝑥)
268	250, 251, 267	elrabd 3684	. . . . . . . . . . . 12 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → (2nd ‘𝑦) ∈ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})
269	247, 268	opelxpd 5713	. . . . . . . . . . 11 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → ⟨(1st ‘𝑦), (2nd ‘𝑦)⟩ ∈ (𝑢 × {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}))
270	246, 269	eqeltrd 2826	. . . . . . . . . 10 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → 𝑦 ∈ (𝑢 × {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}))
271		relxp 5692	. . . . . . . . . . . 12 ⊢ Rel (𝑢 × {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})
272	271	a1i 11	. . . . . . . . . . 11 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → Rel (𝑢 × {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}))
273		opelxp 5710	. . . . . . . . . . . 12 ⊢ (⟨𝑎, 𝑏⟩ ∈ (𝑢 × {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ↔ (𝑎 ∈ 𝑢 ∧ 𝑏 ∈ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}))
274	126	elrab 3682	. . . . . . . . . . . . . . 15 ⊢ (𝑏 ∈ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ↔ (𝑏 ∈ ∪ 𝑆 ∧ (𝑠 × {𝑏}) ⊆ 𝑥))
275	274	simprbi 495	. . . . . . . . . . . . . 14 ⊢ (𝑏 ∈ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} → (𝑠 × {𝑏}) ⊆ 𝑥)
276		simprr2 1219	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → 𝑢 ⊆ 𝑠)
277	276	sselda 3980	. . . . . . . . . . . . . . 15 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ 𝑎 ∈ 𝑢) → 𝑎 ∈ 𝑠)
278		vsnid 4662	. . . . . . . . . . . . . . 15 ⊢ 𝑏 ∈ {𝑏}
279		opelxpi 5711	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 ∈ 𝑠 ∧ 𝑏 ∈ {𝑏}) → ⟨𝑎, 𝑏⟩ ∈ (𝑠 × {𝑏}))
280	277, 278, 279	sylancl 584	. . . . . . . . . . . . . 14 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ 𝑎 ∈ 𝑢) → ⟨𝑎, 𝑏⟩ ∈ (𝑠 × {𝑏}))
281		ssel 3974	. . . . . . . . . . . . . 14 ⊢ ((𝑠 × {𝑏}) ⊆ 𝑥 → (⟨𝑎, 𝑏⟩ ∈ (𝑠 × {𝑏}) → ⟨𝑎, 𝑏⟩ ∈ 𝑥))
282	275, 280, 281	syl2imc 41	. . . . . . . . . . . . 13 ⊢ ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) ∧ 𝑎 ∈ 𝑢) → (𝑏 ∈ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} → ⟨𝑎, 𝑏⟩ ∈ 𝑥))
283	282	expimpd 452	. . . . . . . . . . . 12 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → ((𝑎 ∈ 𝑢 ∧ 𝑏 ∈ {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) → ⟨𝑎, 𝑏⟩ ∈ 𝑥))
284	273, 283	biimtrid 241	. . . . . . . . . . 11 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → (⟨𝑎, 𝑏⟩ ∈ (𝑢 × {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) → ⟨𝑎, 𝑏⟩ ∈ 𝑥))
285	272, 284	relssdv 5786	. . . . . . . . . 10 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → (𝑢 × {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ⊆ 𝑥)
286		eleq2 2815	. . . . . . . . . . . 12 ⊢ (𝑡 = (𝑢 × {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) → (𝑦 ∈ 𝑡 ↔ 𝑦 ∈ (𝑢 × {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})))
287		sseq1 4006	. . . . . . . . . . . 12 ⊢ (𝑡 = (𝑢 × {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) → (𝑡 ⊆ 𝑥 ↔ (𝑢 × {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ⊆ 𝑥))
288	286, 287	anbi12d 630	. . . . . . . . . . 11 ⊢ (𝑡 = (𝑢 × {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) → ((𝑦 ∈ 𝑡 ∧ 𝑡 ⊆ 𝑥) ↔ (𝑦 ∈ (𝑢 × {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ∧ (𝑢 × {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ⊆ 𝑥)))
289	288	rspcev 3609	. . . . . . . . . 10 ⊢ (((𝑢 × {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ∈ (𝑅 ×t 𝑆) ∧ (𝑦 ∈ (𝑢 × {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ∧ (𝑢 × {𝑣 ∈ ∪ 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ⊆ 𝑥)) → ∃𝑡 ∈ (𝑅 ×t 𝑆)(𝑦 ∈ 𝑡 ∧ 𝑡 ⊆ 𝑥))
290	245, 270, 285, 289	syl12anc 835	. . . . . . . . 9 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅) ∧ ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp))) → ∃𝑡 ∈ (𝑅 ×t 𝑆)(𝑦 ∈ 𝑡 ∧ 𝑡 ⊆ 𝑥))
291	290	expr 455	. . . . . . . 8 ⊢ (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) ∧ (𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥} ∧ 𝑢 ∈ 𝑅)) → (((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp) → ∃𝑡 ∈ (𝑅 ×t 𝑆)(𝑦 ∈ 𝑡 ∧ 𝑡 ⊆ 𝑥)))
292	291	rexlimdvva 3202	. . . . . . 7 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → (∃𝑠 ∈ 𝒫 {𝑡 ∈ ∪ 𝑅 ∣ ⟨𝑡, (2nd ‘𝑦)⟩ ∈ 𝑥}∃𝑢 ∈ 𝑅 ((1st ‘𝑦) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑅 ↾t 𝑠) ∈ Comp) → ∃𝑡 ∈ (𝑅 ×t 𝑆)(𝑦 ∈ 𝑡 ∧ 𝑡 ⊆ 𝑥)))
293	63, 292	mpd 15	. . . . . 6 ⊢ ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦 ∈ 𝑥) → ∃𝑡 ∈ (𝑅 ×t 𝑆)(𝑦 ∈ 𝑡 ∧ 𝑡 ⊆ 𝑥))
294	293	ralrimiva 3136	. . . . 5 ⊢ (((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) → ∀𝑦 ∈ 𝑥 ∃𝑡 ∈ (𝑅 ×t 𝑆)(𝑦 ∈ 𝑡 ∧ 𝑡 ⊆ 𝑥))
295	6	adantr 479	. . . . . 6 ⊢ (((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) → (𝑅 ×t 𝑆) ∈ Top)
296		eltop2 22965	. . . . . 6 ⊢ ((𝑅 ×t 𝑆) ∈ Top → (𝑥 ∈ (𝑅 ×t 𝑆) ↔ ∀𝑦 ∈ 𝑥 ∃𝑡 ∈ (𝑅 ×t 𝑆)(𝑦 ∈ 𝑡 ∧ 𝑡 ⊆ 𝑥)))
297	295, 296	syl 17	. . . . 5 ⊢ (((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) → (𝑥 ∈ (𝑅 ×t 𝑆) ↔ ∀𝑦 ∈ 𝑥 ∃𝑡 ∈ (𝑅 ×t 𝑆)(𝑦 ∈ 𝑡 ∧ 𝑡 ⊆ 𝑥)))
298	294, 297	mpbird 256	. . . 4 ⊢ (((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) → 𝑥 ∈ (𝑅 ×t 𝑆))
299	298	ex 411	. . 3 ⊢ ((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) → (𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆)) → 𝑥 ∈ (𝑅 ×t 𝑆)))
300	299	ssrdv 3986	. 2 ⊢ ((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) → (𝑘Gen‘(𝑅 ×t 𝑆)) ⊆ (𝑅 ×t 𝑆))
301		iskgen2 23539	. 2 ⊢ ((𝑅 ×t 𝑆) ∈ ran 𝑘Gen ↔ ((𝑅 ×t 𝑆) ∈ Top ∧ (𝑘Gen‘(𝑅 ×t 𝑆)) ⊆ (𝑅 ×t 𝑆)))
302	6, 300, 301	sylanbrc 581	1 ⊢ ((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) → (𝑅 ×t 𝑆) ∈ ran 𝑘Gen)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 394   ∧ w3a 1084   = wceq 1534   ∈ wcel 2099  ∀wral 3051  ∃wrex 3060  {crab 3420  Vcvv 3464   ∖ cdif 3945   ∩ cin 3947   ⊆ wss 3948  𝒫 cpw 4599  {csn 4625  ⟨cop 4631  ∪ cuni 4907   ↦ cmpt 5228   I cid 5571   × cxp 5672  ^◡ccnv 5673  ran crn 5675   ↾ cres 5676   “ cima 5677  Rel wrel 5679   Fn wfn 6540  ⟶wf 6541  ‘cfv 6545  (class class class)co 7415  1^st c1st 7992  2^nd c2nd 7993   ↾_t crest 17429  Topctop 22882  TopOnctopon 22899  Clsdccld 23007   Cn ccn 23215  Hauscha 23299  Compccmp 23377  𝑛-Locally cnlly 23456  𝑘Genckgen 23524   ×_t ctx 23551

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2697  ax-rep 5282  ax-sep 5296  ax-nul 5303  ax-pow 5361  ax-pr 5425  ax-un 7737

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2704  df-cleq 2718  df-clel 2803  df-nfc 2878  df-ne 2931  df-ral 3052  df-rex 3061  df-reu 3366  df-rab 3421  df-v 3466  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3968  df-nul 4325  df-if 4526  df-pw 4601  df-sn 4626  df-pr 4628  df-op 4632  df-uni 4908  df-int 4949  df-iun 4997  df-iin 4998  df-br 5146  df-opab 5208  df-mpt 5229  df-tr 5263  df-id 5572  df-eprel 5578  df-po 5586  df-so 5587  df-fr 5629  df-we 5631  df-xp 5680  df-rel 5681  df-cnv 5682  df-co 5683  df-dm 5684  df-rn 5685  df-res 5686  df-ima 5687  df-ord 6370  df-on 6371  df-lim 6372  df-suc 6373  df-iota 6497  df-fun 6547  df-fn 6548  df-f 6549  df-f1 6550  df-fo 6551  df-f1o 6552  df-fv 6553  df-ov 7418  df-oprab 7419  df-mpo 7420  df-om 7868  df-1st 7994  df-2nd 7995  df-1o 8487  df-2o 8488  df-map 8848  df-en 8966  df-dom 8967  df-fin 8969  df-fi 9446  df-rest 17431  df-topgen 17452  df-top 22883  df-topon 22900  df-bases 22936  df-cld 23010  df-ntr 23011  df-cls 23012  df-nei 23089  df-cn 23218  df-cnp 23219  df-haus 23306  df-cmp 23378  df-nlly 23458  df-kgen 23525  df-tx 23553

This theorem is referenced by: (None)