Metamath Proof Explorer

Theorem txkgen

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

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

Proof

Step Hyp Ref Expression
1 nllytop ⊢ ( 𝑅 ∈ 𝑛-Locally Comp → 𝑅 ∈ Top )
2 elinel1 ⊢ ( 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) → 𝑆 ∈ ran 𝑘Gen )
3 kgentop ⊢ ( 𝑆 ∈ ran 𝑘Gen → 𝑆 ∈ Top )
4 2 3 syl ⊢ ( 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) → 𝑆 ∈ Top )
5 txtop ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → ( 𝑅 ×t 𝑆 ) ∈ Top )
6 1 4 5 syl2an ⊢ ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) → ( 𝑅 ×t 𝑆 ) ∈ Top )
7 simplll ⊢ ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) → 𝑅 ∈ 𝑛-Locally Comp )
8 eqid ⊢ ( 𝑡 ∈ ∪ 𝑅 ↦ ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ ) = ( 𝑡 ∈ ∪ 𝑅 ↦ ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ )
9 8 mptpreima ⊢ ( ◡ ( 𝑡 ∈ ∪ 𝑅 ↦ ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ ) “ 𝑥 ) = { 𝑡 ∈ ∪ 𝑅 ∣ ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ ∈ 𝑥 }
10 1 ad3antrrr ⊢ ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) → 𝑅 ∈ Top )
11 toptopon2 ⊢ ( 𝑅 ∈ Top ↔ 𝑅 ∈ ( TopOn ‘ ∪ 𝑅 ) )
12 10 11 sylib ⊢ ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) → 𝑅 ∈ ( TopOn ‘ ∪ 𝑅 ) )
13 idcn ⊢ ( 𝑅 ∈ ( TopOn ‘ ∪ 𝑅 ) → ( I ↾ ∪ 𝑅 ) ∈ ( 𝑅 Cn 𝑅 ) )
14 12 13 syl ⊢ ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) → ( I ↾ ∪ 𝑅 ) ∈ ( 𝑅 Cn 𝑅 ) )
15 simpllr ⊢ ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) → 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) )
16 15 4 syl ⊢ ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) → 𝑆 ∈ Top )
17 toptopon2 ⊢ ( 𝑆 ∈ Top ↔ 𝑆 ∈ ( TopOn ‘ ∪ 𝑆 ) )
18 16 17 sylib ⊢ ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) → 𝑆 ∈ ( TopOn ‘ ∪ 𝑆 ) )
19 simpr ⊢ ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ∈ 𝑥 )
20 simplr ⊢ ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) → 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) )
21 elunii ⊢ ( ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) → 𝑦 ∈ ∪ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) )
22 19 20 21 syl2anc ⊢ ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ∈ ∪ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) )
23 eqid ⊢ ∪ 𝑅 = ∪ 𝑅
24 eqid ⊢ ∪ 𝑆 = ∪ 𝑆
25 23 24 txuni ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → ( ∪ 𝑅 × ∪ 𝑆 ) = ∪ ( 𝑅 ×t 𝑆 ) )
26 10 16 25 syl2anc ⊢ ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) → ( ∪ 𝑅 × ∪ 𝑆 ) = ∪ ( 𝑅 ×t 𝑆 ) )
27 10 16 5 syl2anc ⊢ ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) → ( 𝑅 ×t 𝑆 ) ∈ Top )
28 eqid ⊢ ∪ ( 𝑅 ×t 𝑆 ) = ∪ ( 𝑅 ×t 𝑆 )
29 28 kgenuni ⊢ ( ( 𝑅 ×t 𝑆 ) ∈ Top → ∪ ( 𝑅 ×t 𝑆 ) = ∪ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) )
30 27 29 syl ⊢ ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) → ∪ ( 𝑅 ×t 𝑆 ) = ∪ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) )
31 26 30 eqtrd ⊢ ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) → ( ∪ 𝑅 × ∪ 𝑆 ) = ∪ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) )
32 22 31 eleqtrrd ⊢ ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) )
33 xp2nd ⊢ ( 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) → ( 2nd ‘ 𝑦 ) ∈ ∪ 𝑆 )
34 32 33 syl ⊢ ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) → ( 2nd ‘ 𝑦 ) ∈ ∪ 𝑆 )
35 cnconst2 ⊢ ( ( 𝑅 ∈ ( TopOn ‘ ∪ 𝑅 ) ∧ 𝑆 ∈ ( TopOn ‘ ∪ 𝑆 ) ∧ ( 2nd ‘ 𝑦 ) ∈ ∪ 𝑆 ) → ( ∪ 𝑅 × { ( 2nd ‘ 𝑦 ) } ) ∈ ( 𝑅 Cn 𝑆 ) )
36 12 18 34 35 syl3anc ⊢ ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) → ( ∪ 𝑅 × { ( 2nd ‘ 𝑦 ) } ) ∈ ( 𝑅 Cn 𝑆 ) )
37 fvresi ⊢ ( 𝑡 ∈ ∪ 𝑅 → ( ( I ↾ ∪ 𝑅 ) ‘ 𝑡 ) = 𝑡 )
38 fvex ⊢ ( 2nd ‘ 𝑦 ) ∈ V
39 38 fvconst2 ⊢ ( 𝑡 ∈ ∪ 𝑅 → ( ( ∪ 𝑅 × { ( 2nd ‘ 𝑦 ) } ) ‘ 𝑡 ) = ( 2nd ‘ 𝑦 ) )
40 37 39 opeq12d ⊢ ( 𝑡 ∈ ∪ 𝑅 → ⟨ ( ( I ↾ ∪ 𝑅 ) ‘ 𝑡 ) , ( ( ∪ 𝑅 × { ( 2nd ‘ 𝑦 ) } ) ‘ 𝑡 ) ⟩ = ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ )
41 40 mpteq2ia ⊢ ( 𝑡 ∈ ∪ 𝑅 ↦ ⟨ ( ( I ↾ ∪ 𝑅 ) ‘ 𝑡 ) , ( ( ∪ 𝑅 × { ( 2nd ‘ 𝑦 ) } ) ‘ 𝑡 ) ⟩ ) = ( 𝑡 ∈ ∪ 𝑅 ↦ ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ )
42 41 eqcomi ⊢ ( 𝑡 ∈ ∪ 𝑅 ↦ ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ ) = ( 𝑡 ∈ ∪ 𝑅 ↦ ⟨ ( ( I ↾ ∪ 𝑅 ) ‘ 𝑡 ) , ( ( ∪ 𝑅 × { ( 2nd ‘ 𝑦 ) } ) ‘ 𝑡 ) ⟩ )
43 23 42 txcnmpt ⊢ ( ( ( I ↾ ∪ 𝑅 ) ∈ ( 𝑅 Cn 𝑅 ) ∧ ( ∪ 𝑅 × { ( 2nd ‘ 𝑦 ) } ) ∈ ( 𝑅 Cn 𝑆 ) ) → ( 𝑡 ∈ ∪ 𝑅 ↦ ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ ) ∈ ( 𝑅 Cn ( 𝑅 ×t 𝑆 ) ) )
44 14 36 43 syl2anc ⊢ ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) → ( 𝑡 ∈ ∪ 𝑅 ↦ ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ ) ∈ ( 𝑅 Cn ( 𝑅 ×t 𝑆 ) ) )
45 llycmpkgen ⊢ ( 𝑅 ∈ 𝑛-Locally Comp → 𝑅 ∈ ran 𝑘Gen )
46 45 ad3antrrr ⊢ ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) → 𝑅 ∈ ran 𝑘Gen )
47 6 ad2antrr ⊢ ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) → ( 𝑅 ×t 𝑆 ) ∈ Top )
48 kgencn3 ⊢ ( ( 𝑅 ∈ ran 𝑘Gen ∧ ( 𝑅 ×t 𝑆 ) ∈ Top ) → ( 𝑅 Cn ( 𝑅 ×t 𝑆 ) ) = ( 𝑅 Cn ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) )
49 46 47 48 syl2anc ⊢ ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) → ( 𝑅 Cn ( 𝑅 ×t 𝑆 ) ) = ( 𝑅 Cn ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) )
50 44 49 eleqtrd ⊢ ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) → ( 𝑡 ∈ ∪ 𝑅 ↦ ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ ) ∈ ( 𝑅 Cn ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) )
51 cnima ⊢ ( ( ( 𝑡 ∈ ∪ 𝑅 ↦ ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ ) ∈ ( 𝑅 Cn ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) → ( ◡ ( 𝑡 ∈ ∪ 𝑅 ↦ ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ ) “ 𝑥 ) ∈ 𝑅 )
52 50 20 51 syl2anc ⊢ ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) → ( ◡ ( 𝑡 ∈ ∪ 𝑅 ↦ ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ ) “ 𝑥 ) ∈ 𝑅 )
53 9 52 eqeltrrid ⊢ ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) → { 𝑡 ∈ ∪ 𝑅 ∣ ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ ∈ 𝑥 } ∈ 𝑅 )
54 opeq1 ⊢ ( 𝑡 = ( 1st ‘ 𝑦 ) → ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ = ⟨ ( 1st ‘ 𝑦 ) , ( 2nd ‘ 𝑦 ) ⟩ )
55 54 eleq1d ⊢ ( 𝑡 = ( 1st ‘ 𝑦 ) → ( ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ ∈ 𝑥 ↔ ⟨ ( 1st ‘ 𝑦 ) , ( 2nd ‘ 𝑦 ) ⟩ ∈ 𝑥 ) )
56 xp1st ⊢ ( 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) → ( 1st ‘ 𝑦 ) ∈ ∪ 𝑅 )
57 32 56 syl ⊢ ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) → ( 1st ‘ 𝑦 ) ∈ ∪ 𝑅 )
58 1st2nd2 ⊢ ( 𝑦 ∈ ( ∪ 𝑅 × ∪ 𝑆 ) → 𝑦 = ⟨ ( 1st ‘ 𝑦 ) , ( 2nd ‘ 𝑦 ) ⟩ )
59 32 58 syl ⊢ ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) → 𝑦 = ⟨ ( 1st ‘ 𝑦 ) , ( 2nd ‘ 𝑦 ) ⟩ )
60 59 19 eqeltrrd ⊢ ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) → ⟨ ( 1st ‘ 𝑦 ) , ( 2nd ‘ 𝑦 ) ⟩ ∈ 𝑥 )
61 55 57 60 elrabd ⊢ ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) → ( 1st ‘ 𝑦 ) ∈ { 𝑡 ∈ ∪ 𝑅 ∣ ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ ∈ 𝑥 } )
62 nlly2i ⊢ ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ { 𝑡 ∈ ∪ 𝑅 ∣ ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ ∈ 𝑥 } ∈ 𝑅 ∧ ( 1st ‘ 𝑦 ) ∈ { 𝑡 ∈ ∪ 𝑅 ∣ ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ ∈ 𝑥 } ) → ∃ 𝑠 ∈ 𝒫 { 𝑡 ∈ ∪ 𝑅 ∣ ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ ∈ 𝑥 } ∃ 𝑢 ∈ 𝑅 ( ( 1st ‘ 𝑦 ) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝑅 ↾t 𝑠 ) ∈ Comp ) )
63 7 53 61 62 syl3anc ⊢ ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) → ∃ 𝑠 ∈ 𝒫 { 𝑡 ∈ ∪ 𝑅 ∣ ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ ∈ 𝑥 } ∃ 𝑢 ∈ 𝑅 ( ( 1st ‘ 𝑦 ) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝑅 ↾t 𝑠 ) ∈ Comp ) )
64 10 adantr ⊢ ( ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( ( 𝑠 ∈ 𝒫 { 𝑡 ∈ ∪ 𝑅 ∣ ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ ∈ 𝑥 } ∧ 𝑢 ∈ 𝑅 ) ∧ ( ( 1st ‘ 𝑦 ) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝑅 ↾t 𝑠 ) ∈ Comp ) ) ) → 𝑅 ∈ Top )
65 16 adantr ⊢ ( ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( ( 𝑠 ∈ 𝒫 { 𝑡 ∈ ∪ 𝑅 ∣ ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ ∈ 𝑥 } ∧ 𝑢 ∈ 𝑅 ) ∧ ( ( 1st ‘ 𝑦 ) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝑅 ↾t 𝑠 ) ∈ Comp ) ) ) → 𝑆 ∈ Top )
66 simprlr ⊢ ( ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( ( 𝑠 ∈ 𝒫 { 𝑡 ∈ ∪ 𝑅 ∣ ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ ∈ 𝑥 } ∧ 𝑢 ∈ 𝑅 ) ∧ ( ( 1st ‘ 𝑦 ) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝑅 ↾t 𝑠 ) ∈ Comp ) ) ) → 𝑢 ∈ 𝑅 )
67 ssrab2 ⊢ { 𝑣 ∈ ∪ 𝑆 ∣ ( 𝑠 × { 𝑣 } ) ⊆ 𝑥 } ⊆ ∪ 𝑆
68 67 a1i ⊢ ( ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( ( 𝑠 ∈ 𝒫 { 𝑡 ∈ ∪ 𝑅 ∣ ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ ∈ 𝑥 } ∧ 𝑢 ∈ 𝑅 ) ∧ ( ( 1st ‘ 𝑦 ) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝑅 ↾t 𝑠 ) ∈ Comp ) ) ) → { 𝑣 ∈ ∪ 𝑆 ∣ ( 𝑠 × { 𝑣 } ) ⊆ 𝑥 } ⊆ ∪ 𝑆 )
69 incom ⊢ ( { 𝑣 ∈ ∪ 𝑆 ∣ ( 𝑠 × { 𝑣 } ) ⊆ 𝑥 } ∩ 𝑘 ) = ( 𝑘 ∩ { 𝑣 ∈ ∪ 𝑆 ∣ ( 𝑠 × { 𝑣 } ) ⊆ 𝑥 } )
70 simprll ⊢ ( ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( ( 𝑠 ∈ 𝒫 { 𝑡 ∈ ∪ 𝑅 ∣ ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ ∈ 𝑥 } ∧ 𝑢 ∈ 𝑅 ) ∧ ( ( 1st ‘ 𝑦 ) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝑅 ↾t 𝑠 ) ∈ Comp ) ) ) → 𝑠 ∈ 𝒫 { 𝑡 ∈ ∪ 𝑅 ∣ ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ ∈ 𝑥 } )
71 70 elpwid ⊢ ( ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( ( 𝑠 ∈ 𝒫 { 𝑡 ∈ ∪ 𝑅 ∣ ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ ∈ 𝑥 } ∧ 𝑢 ∈ 𝑅 ) ∧ ( ( 1st ‘ 𝑦 ) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝑅 ↾t 𝑠 ) ∈ Comp ) ) ) → 𝑠 ⊆ { 𝑡 ∈ ∪ 𝑅 ∣ ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ ∈ 𝑥 } )
72 ssrab2 ⊢ { 𝑡 ∈ ∪ 𝑅 ∣ ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ ∈ 𝑥 } ⊆ ∪ 𝑅
73 71 72 sstrdi ⊢ ( ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( ( 𝑠 ∈ 𝒫 { 𝑡 ∈ ∪ 𝑅 ∣ ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ ∈ 𝑥 } ∧ 𝑢 ∈ 𝑅 ) ∧ ( ( 1st ‘ 𝑦 ) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝑅 ↾t 𝑠 ) ∈ Comp ) ) ) → 𝑠 ⊆ ∪ 𝑅 )
74 73 adantr ⊢ ( ( ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( ( 𝑠 ∈ 𝒫 { 𝑡 ∈ ∪ 𝑅 ∣ ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ ∈ 𝑥 } ∧ 𝑢 ∈ 𝑅 ) ∧ ( ( 1st ‘ 𝑦 ) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝑅 ↾t 𝑠 ) ∈ Comp ) ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ ( 𝑆 ↾t 𝑘 ) ∈ Comp ) ) → 𝑠 ⊆ ∪ 𝑅 )
75 elpwi ⊢ ( 𝑘 ∈ 𝒫 ∪ 𝑆 → 𝑘 ⊆ ∪ 𝑆 )
76 75 ad2antrl ⊢ ( ( ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( ( 𝑠 ∈ 𝒫 { 𝑡 ∈ ∪ 𝑅 ∣ ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ ∈ 𝑥 } ∧ 𝑢 ∈ 𝑅 ) ∧ ( ( 1st ‘ 𝑦 ) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝑅 ↾t 𝑠 ) ∈ Comp ) ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ ( 𝑆 ↾t 𝑘 ) ∈ Comp ) ) → 𝑘 ⊆ ∪ 𝑆 )
77 eldif ⊢ ( 𝑡 ∈ ( ( 𝑠 × 𝑘 ) ∖ 𝑥 ) ↔ ( 𝑡 ∈ ( 𝑠 × 𝑘 ) ∧ ¬ 𝑡 ∈ 𝑥 ) )
78 77 anbi1i ⊢ ( ( 𝑡 ∈ ( ( 𝑠 × 𝑘 ) ∖ 𝑥 ) ∧ ( ( 2nd ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) ‘ 𝑡 ) = 𝑏 ) ↔ ( ( 𝑡 ∈ ( 𝑠 × 𝑘 ) ∧ ¬ 𝑡 ∈ 𝑥 ) ∧ ( ( 2nd ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) ‘ 𝑡 ) = 𝑏 ) )
79 anass ⊢ ( ( ( 𝑡 ∈ ( 𝑠 × 𝑘 ) ∧ ¬ 𝑡 ∈ 𝑥 ) ∧ ( ( 2nd ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) ‘ 𝑡 ) = 𝑏 ) ↔ ( 𝑡 ∈ ( 𝑠 × 𝑘 ) ∧ ( ¬ 𝑡 ∈ 𝑥 ∧ ( ( 2nd ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) ‘ 𝑡 ) = 𝑏 ) ) )
80 78 79 bitri ⊢ ( ( 𝑡 ∈ ( ( 𝑠 × 𝑘 ) ∖ 𝑥 ) ∧ ( ( 2nd ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) ‘ 𝑡 ) = 𝑏 ) ↔ ( 𝑡 ∈ ( 𝑠 × 𝑘 ) ∧ ( ¬ 𝑡 ∈ 𝑥 ∧ ( ( 2nd ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) ‘ 𝑡 ) = 𝑏 ) ) )
81 80 rexbii2 ⊢ ( ∃ 𝑡 ∈ ( ( 𝑠 × 𝑘 ) ∖ 𝑥 ) ( ( 2nd ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) ‘ 𝑡 ) = 𝑏 ↔ ∃ 𝑡 ∈ ( 𝑠 × 𝑘 ) ( ¬ 𝑡 ∈ 𝑥 ∧ ( ( 2nd ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) ‘ 𝑡 ) = 𝑏 ) )
82 ancom ⊢ ( ( ¬ 𝑡 ∈ 𝑥 ∧ ( ( 2nd ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) ‘ 𝑡 ) = 𝑏 ) ↔ ( ( ( 2nd ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) ‘ 𝑡 ) = 𝑏 ∧ ¬ 𝑡 ∈ 𝑥 ) )
83 fveqeq2 ⊢ ( 𝑡 = ⟨ 𝑎 , 𝑢 ⟩ → ( ( ( 2nd ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) ‘ 𝑡 ) = 𝑏 ↔ ( ( 2nd ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) ‘ ⟨ 𝑎 , 𝑢 ⟩ ) = 𝑏 ) )
84 eleq1 ⊢ ( 𝑡 = ⟨ 𝑎 , 𝑢 ⟩ → ( 𝑡 ∈ 𝑥 ↔ ⟨ 𝑎 , 𝑢 ⟩ ∈ 𝑥 ) )
85 84 notbid ⊢ ( 𝑡 = ⟨ 𝑎 , 𝑢 ⟩ → ( ¬ 𝑡 ∈ 𝑥 ↔ ¬ ⟨ 𝑎 , 𝑢 ⟩ ∈ 𝑥 ) )
86 83 85 anbi12d ⊢ ( 𝑡 = ⟨ 𝑎 , 𝑢 ⟩ → ( ( ( ( 2nd ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) ‘ 𝑡 ) = 𝑏 ∧ ¬ 𝑡 ∈ 𝑥 ) ↔ ( ( ( 2nd ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) ‘ ⟨ 𝑎 , 𝑢 ⟩ ) = 𝑏 ∧ ¬ ⟨ 𝑎 , 𝑢 ⟩ ∈ 𝑥 ) ) )
87 82 86 syl5bb ⊢ ( 𝑡 = ⟨ 𝑎 , 𝑢 ⟩ → ( ( ¬ 𝑡 ∈ 𝑥 ∧ ( ( 2nd ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) ‘ 𝑡 ) = 𝑏 ) ↔ ( ( ( 2nd ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) ‘ ⟨ 𝑎 , 𝑢 ⟩ ) = 𝑏 ∧ ¬ ⟨ 𝑎 , 𝑢 ⟩ ∈ 𝑥 ) ) )
88 87 rexxp ⊢ ( ∃ 𝑡 ∈ ( 𝑠 × 𝑘 ) ( ¬ 𝑡 ∈ 𝑥 ∧ ( ( 2nd ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) ‘ 𝑡 ) = 𝑏 ) ↔ ∃ 𝑎 ∈ 𝑠 ∃ 𝑢 ∈ 𝑘 ( ( ( 2nd ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) ‘ ⟨ 𝑎 , 𝑢 ⟩ ) = 𝑏 ∧ ¬ ⟨ 𝑎 , 𝑢 ⟩ ∈ 𝑥 ) )
89 81 88 bitri ⊢ ( ∃ 𝑡 ∈ ( ( 𝑠 × 𝑘 ) ∖ 𝑥 ) ( ( 2nd ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) ‘ 𝑡 ) = 𝑏 ↔ ∃ 𝑎 ∈ 𝑠 ∃ 𝑢 ∈ 𝑘 ( ( ( 2nd ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) ‘ ⟨ 𝑎 , 𝑢 ⟩ ) = 𝑏 ∧ ¬ ⟨ 𝑎 , 𝑢 ⟩ ∈ 𝑥 ) )
90 simpl ⊢ ( ( 𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆 ) → 𝑠 ⊆ ∪ 𝑅 )
91 90 sselda ⊢ ( ( ( 𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆 ) ∧ 𝑎 ∈ 𝑠 ) → 𝑎 ∈ ∪ 𝑅 )
92 91 adantr ⊢ ( ( ( ( 𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆 ) ∧ 𝑎 ∈ 𝑠 ) ∧ 𝑢 ∈ 𝑘 ) → 𝑎 ∈ ∪ 𝑅 )
93 simplr ⊢ ( ( ( 𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆 ) ∧ 𝑎 ∈ 𝑠 ) → 𝑘 ⊆ ∪ 𝑆 )
94 93 sselda ⊢ ( ( ( ( 𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆 ) ∧ 𝑎 ∈ 𝑠 ) ∧ 𝑢 ∈ 𝑘 ) → 𝑢 ∈ ∪ 𝑆 )
95 92 94 opelxpd ⊢ ( ( ( ( 𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆 ) ∧ 𝑎 ∈ 𝑠 ) ∧ 𝑢 ∈ 𝑘 ) → ⟨ 𝑎 , 𝑢 ⟩ ∈ ( ∪ 𝑅 × ∪ 𝑆 ) )
96 95 fvresd ⊢ ( ( ( ( 𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆 ) ∧ 𝑎 ∈ 𝑠 ) ∧ 𝑢 ∈ 𝑘 ) → ( ( 2nd ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) ‘ ⟨ 𝑎 , 𝑢 ⟩ ) = ( 2nd ‘ ⟨ 𝑎 , 𝑢 ⟩ ) )
97 vex ⊢ 𝑎 ∈ V
98 vex ⊢ 𝑢 ∈ V
99 97 98 op2nd ⊢ ( 2nd ‘ ⟨ 𝑎 , 𝑢 ⟩ ) = 𝑢
100 96 99 eqtrdi ⊢ ( ( ( ( 𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆 ) ∧ 𝑎 ∈ 𝑠 ) ∧ 𝑢 ∈ 𝑘 ) → ( ( 2nd ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) ‘ ⟨ 𝑎 , 𝑢 ⟩ ) = 𝑢 )
101 100 eqeq1d ⊢ ( ( ( ( 𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆 ) ∧ 𝑎 ∈ 𝑠 ) ∧ 𝑢 ∈ 𝑘 ) → ( ( ( 2nd ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) ‘ ⟨ 𝑎 , 𝑢 ⟩ ) = 𝑏 ↔ 𝑢 = 𝑏 ) )
102 101 anbi1d ⊢ ( ( ( ( 𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆 ) ∧ 𝑎 ∈ 𝑠 ) ∧ 𝑢 ∈ 𝑘 ) → ( ( ( ( 2nd ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) ‘ ⟨ 𝑎 , 𝑢 ⟩ ) = 𝑏 ∧ ¬ ⟨ 𝑎 , 𝑢 ⟩ ∈ 𝑥 ) ↔ ( 𝑢 = 𝑏 ∧ ¬ ⟨ 𝑎 , 𝑢 ⟩ ∈ 𝑥 ) ) )
103 102 rexbidva ⊢ ( ( ( 𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆 ) ∧ 𝑎 ∈ 𝑠 ) → ( ∃ 𝑢 ∈ 𝑘 ( ( ( 2nd ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) ‘ ⟨ 𝑎 , 𝑢 ⟩ ) = 𝑏 ∧ ¬ ⟨ 𝑎 , 𝑢 ⟩ ∈ 𝑥 ) ↔ ∃ 𝑢 ∈ 𝑘 ( 𝑢 = 𝑏 ∧ ¬ ⟨ 𝑎 , 𝑢 ⟩ ∈ 𝑥 ) ) )
104 opeq2 ⊢ ( 𝑢 = 𝑏 → ⟨ 𝑎 , 𝑢 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ )
105 104 eleq1d ⊢ ( 𝑢 = 𝑏 → ( ⟨ 𝑎 , 𝑢 ⟩ ∈ 𝑥 ↔ ⟨ 𝑎 , 𝑏 ⟩ ∈ 𝑥 ) )
106 105 notbid ⊢ ( 𝑢 = 𝑏 → ( ¬ ⟨ 𝑎 , 𝑢 ⟩ ∈ 𝑥 ↔ ¬ ⟨ 𝑎 , 𝑏 ⟩ ∈ 𝑥 ) )
107 106 ceqsrexbv ⊢ ( ∃ 𝑢 ∈ 𝑘 ( 𝑢 = 𝑏 ∧ ¬ ⟨ 𝑎 , 𝑢 ⟩ ∈ 𝑥 ) ↔ ( 𝑏 ∈ 𝑘 ∧ ¬ ⟨ 𝑎 , 𝑏 ⟩ ∈ 𝑥 ) )
108 103 107 bitrdi ⊢ ( ( ( 𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆 ) ∧ 𝑎 ∈ 𝑠 ) → ( ∃ 𝑢 ∈ 𝑘 ( ( ( 2nd ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) ‘ ⟨ 𝑎 , 𝑢 ⟩ ) = 𝑏 ∧ ¬ ⟨ 𝑎 , 𝑢 ⟩ ∈ 𝑥 ) ↔ ( 𝑏 ∈ 𝑘 ∧ ¬ ⟨ 𝑎 , 𝑏 ⟩ ∈ 𝑥 ) ) )
109 108 rexbidva ⊢ ( ( 𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆 ) → ( ∃ 𝑎 ∈ 𝑠 ∃ 𝑢 ∈ 𝑘 ( ( ( 2nd ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) ‘ ⟨ 𝑎 , 𝑢 ⟩ ) = 𝑏 ∧ ¬ ⟨ 𝑎 , 𝑢 ⟩ ∈ 𝑥 ) ↔ ∃ 𝑎 ∈ 𝑠 ( 𝑏 ∈ 𝑘 ∧ ¬ ⟨ 𝑎 , 𝑏 ⟩ ∈ 𝑥 ) ) )
110 r19.42v ⊢ ( ∃ 𝑎 ∈ 𝑠 ( 𝑏 ∈ 𝑘 ∧ ¬ ⟨ 𝑎 , 𝑏 ⟩ ∈ 𝑥 ) ↔ ( 𝑏 ∈ 𝑘 ∧ ∃ 𝑎 ∈ 𝑠 ¬ ⟨ 𝑎 , 𝑏 ⟩ ∈ 𝑥 ) )
111 109 110 bitrdi ⊢ ( ( 𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆 ) → ( ∃ 𝑎 ∈ 𝑠 ∃ 𝑢 ∈ 𝑘 ( ( ( 2nd ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) ‘ ⟨ 𝑎 , 𝑢 ⟩ ) = 𝑏 ∧ ¬ ⟨ 𝑎 , 𝑢 ⟩ ∈ 𝑥 ) ↔ ( 𝑏 ∈ 𝑘 ∧ ∃ 𝑎 ∈ 𝑠 ¬ ⟨ 𝑎 , 𝑏 ⟩ ∈ 𝑥 ) ) )
112 89 111 syl5bb ⊢ ( ( 𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆 ) → ( ∃ 𝑡 ∈ ( ( 𝑠 × 𝑘 ) ∖ 𝑥 ) ( ( 2nd ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) ‘ 𝑡 ) = 𝑏 ↔ ( 𝑏 ∈ 𝑘 ∧ ∃ 𝑎 ∈ 𝑠 ¬ ⟨ 𝑎 , 𝑏 ⟩ ∈ 𝑥 ) ) )
113 f2ndres ⊢ ( 2nd ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) : ( ∪ 𝑅 × ∪ 𝑆 ) ⟶ ∪ 𝑆
114 ffn ⊢ ( ( 2nd ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) : ( ∪ 𝑅 × ∪ 𝑆 ) ⟶ ∪ 𝑆 → ( 2nd ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) Fn ( ∪ 𝑅 × ∪ 𝑆 ) )
115 113 114 ax-mp ⊢ ( 2nd ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) Fn ( ∪ 𝑅 × ∪ 𝑆 )
116 difss ⊢ ( ( 𝑠 × 𝑘 ) ∖ 𝑥 ) ⊆ ( 𝑠 × 𝑘 )
117 xpss12 ⊢ ( ( 𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆 ) → ( 𝑠 × 𝑘 ) ⊆ ( ∪ 𝑅 × ∪ 𝑆 ) )
118 116 117 sstrid ⊢ ( ( 𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆 ) → ( ( 𝑠 × 𝑘 ) ∖ 𝑥 ) ⊆ ( ∪ 𝑅 × ∪ 𝑆 ) )
119 fvelimab ⊢ ( ( ( 2nd ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) Fn ( ∪ 𝑅 × ∪ 𝑆 ) ∧ ( ( 𝑠 × 𝑘 ) ∖ 𝑥 ) ⊆ ( ∪ 𝑅 × ∪ 𝑆 ) ) → ( 𝑏 ∈ ( ( 2nd ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) “ ( ( 𝑠 × 𝑘 ) ∖ 𝑥 ) ) ↔ ∃ 𝑡 ∈ ( ( 𝑠 × 𝑘 ) ∖ 𝑥 ) ( ( 2nd ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) ‘ 𝑡 ) = 𝑏 ) )
120 115 118 119 sylancr ⊢ ( ( 𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆 ) → ( 𝑏 ∈ ( ( 2nd ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) “ ( ( 𝑠 × 𝑘 ) ∖ 𝑥 ) ) ↔ ∃ 𝑡 ∈ ( ( 𝑠 × 𝑘 ) ∖ 𝑥 ) ( ( 2nd ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) ‘ 𝑡 ) = 𝑏 ) )
121 eldif ⊢ ( 𝑏 ∈ ( 𝑘 ∖ { 𝑣 ∈ ∪ 𝑆 ∣ ( 𝑠 × { 𝑣 } ) ⊆ 𝑥 } ) ↔ ( 𝑏 ∈ 𝑘 ∧ ¬ 𝑏 ∈ { 𝑣 ∈ ∪ 𝑆 ∣ ( 𝑠 × { 𝑣 } ) ⊆ 𝑥 } ) )
122 simpr ⊢ ( ( 𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆 ) → 𝑘 ⊆ ∪ 𝑆 )
123 122 sselda ⊢ ( ( ( 𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆 ) ∧ 𝑏 ∈ 𝑘 ) → 𝑏 ∈ ∪ 𝑆 )
124 sneq ⊢ ( 𝑣 = 𝑏 → { 𝑣 } = { 𝑏 } )
125 124 xpeq2d ⊢ ( 𝑣 = 𝑏 → ( 𝑠 × { 𝑣 } ) = ( 𝑠 × { 𝑏 } ) )
126 125 sseq1d ⊢ ( 𝑣 = 𝑏 → ( ( 𝑠 × { 𝑣 } ) ⊆ 𝑥 ↔ ( 𝑠 × { 𝑏 } ) ⊆ 𝑥 ) )
127 dfss3 ⊢ ( ( 𝑠 × { 𝑏 } ) ⊆ 𝑥 ↔ ∀ 𝑘 ∈ ( 𝑠 × { 𝑏 } ) 𝑘 ∈ 𝑥 )
128 eleq1 ⊢ ( 𝑘 = ⟨ 𝑎 , 𝑡 ⟩ → ( 𝑘 ∈ 𝑥 ↔ ⟨ 𝑎 , 𝑡 ⟩ ∈ 𝑥 ) )
129 128 ralxp ⊢ ( ∀ 𝑘 ∈ ( 𝑠 × { 𝑏 } ) 𝑘 ∈ 𝑥 ↔ ∀ 𝑎 ∈ 𝑠 ∀ 𝑡 ∈ { 𝑏 } ⟨ 𝑎 , 𝑡 ⟩ ∈ 𝑥 )
130 vex ⊢ 𝑏 ∈ V
131 opeq2 ⊢ ( 𝑡 = 𝑏 → ⟨ 𝑎 , 𝑡 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ )
132 131 eleq1d ⊢ ( 𝑡 = 𝑏 → ( ⟨ 𝑎 , 𝑡 ⟩ ∈ 𝑥 ↔ ⟨ 𝑎 , 𝑏 ⟩ ∈ 𝑥 ) )
133 130 132 ralsn ⊢ ( ∀ 𝑡 ∈ { 𝑏 } ⟨ 𝑎 , 𝑡 ⟩ ∈ 𝑥 ↔ ⟨ 𝑎 , 𝑏 ⟩ ∈ 𝑥 )
134 133 ralbii ⊢ ( ∀ 𝑎 ∈ 𝑠 ∀ 𝑡 ∈ { 𝑏 } ⟨ 𝑎 , 𝑡 ⟩ ∈ 𝑥 ↔ ∀ 𝑎 ∈ 𝑠 ⟨ 𝑎 , 𝑏 ⟩ ∈ 𝑥 )
135 127 129 134 3bitri ⊢ ( ( 𝑠 × { 𝑏 } ) ⊆ 𝑥 ↔ ∀ 𝑎 ∈ 𝑠 ⟨ 𝑎 , 𝑏 ⟩ ∈ 𝑥 )
136 126 135 bitrdi ⊢ ( 𝑣 = 𝑏 → ( ( 𝑠 × { 𝑣 } ) ⊆ 𝑥 ↔ ∀ 𝑎 ∈ 𝑠 ⟨ 𝑎 , 𝑏 ⟩ ∈ 𝑥 ) )
137 136 elrab3 ⊢ ( 𝑏 ∈ ∪ 𝑆 → ( 𝑏 ∈ { 𝑣 ∈ ∪ 𝑆 ∣ ( 𝑠 × { 𝑣 } ) ⊆ 𝑥 } ↔ ∀ 𝑎 ∈ 𝑠 ⟨ 𝑎 , 𝑏 ⟩ ∈ 𝑥 ) )
138 123 137 syl ⊢ ( ( ( 𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆 ) ∧ 𝑏 ∈ 𝑘 ) → ( 𝑏 ∈ { 𝑣 ∈ ∪ 𝑆 ∣ ( 𝑠 × { 𝑣 } ) ⊆ 𝑥 } ↔ ∀ 𝑎 ∈ 𝑠 ⟨ 𝑎 , 𝑏 ⟩ ∈ 𝑥 ) )
139 138 notbid ⊢ ( ( ( 𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆 ) ∧ 𝑏 ∈ 𝑘 ) → ( ¬ 𝑏 ∈ { 𝑣 ∈ ∪ 𝑆 ∣ ( 𝑠 × { 𝑣 } ) ⊆ 𝑥 } ↔ ¬ ∀ 𝑎 ∈ 𝑠 ⟨ 𝑎 , 𝑏 ⟩ ∈ 𝑥 ) )
140 rexnal ⊢ ( ∃ 𝑎 ∈ 𝑠 ¬ ⟨ 𝑎 , 𝑏 ⟩ ∈ 𝑥 ↔ ¬ ∀ 𝑎 ∈ 𝑠 ⟨ 𝑎 , 𝑏 ⟩ ∈ 𝑥 )
141 139 140 bitr4di ⊢ ( ( ( 𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆 ) ∧ 𝑏 ∈ 𝑘 ) → ( ¬ 𝑏 ∈ { 𝑣 ∈ ∪ 𝑆 ∣ ( 𝑠 × { 𝑣 } ) ⊆ 𝑥 } ↔ ∃ 𝑎 ∈ 𝑠 ¬ ⟨ 𝑎 , 𝑏 ⟩ ∈ 𝑥 ) )
142 141 pm5.32da ⊢ ( ( 𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆 ) → ( ( 𝑏 ∈ 𝑘 ∧ ¬ 𝑏 ∈ { 𝑣 ∈ ∪ 𝑆 ∣ ( 𝑠 × { 𝑣 } ) ⊆ 𝑥 } ) ↔ ( 𝑏 ∈ 𝑘 ∧ ∃ 𝑎 ∈ 𝑠 ¬ ⟨ 𝑎 , 𝑏 ⟩ ∈ 𝑥 ) ) )
143 121 142 syl5bb ⊢ ( ( 𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆 ) → ( 𝑏 ∈ ( 𝑘 ∖ { 𝑣 ∈ ∪ 𝑆 ∣ ( 𝑠 × { 𝑣 } ) ⊆ 𝑥 } ) ↔ ( 𝑏 ∈ 𝑘 ∧ ∃ 𝑎 ∈ 𝑠 ¬ ⟨ 𝑎 , 𝑏 ⟩ ∈ 𝑥 ) ) )
144 112 120 143 3bitr4d ⊢ ( ( 𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆 ) → ( 𝑏 ∈ ( ( 2nd ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) “ ( ( 𝑠 × 𝑘 ) ∖ 𝑥 ) ) ↔ 𝑏 ∈ ( 𝑘 ∖ { 𝑣 ∈ ∪ 𝑆 ∣ ( 𝑠 × { 𝑣 } ) ⊆ 𝑥 } ) ) )
145 144 eqrdv ⊢ ( ( 𝑠 ⊆ ∪ 𝑅 ∧ 𝑘 ⊆ ∪ 𝑆 ) → ( ( 2nd ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) “ ( ( 𝑠 × 𝑘 ) ∖ 𝑥 ) ) = ( 𝑘 ∖ { 𝑣 ∈ ∪ 𝑆 ∣ ( 𝑠 × { 𝑣 } ) ⊆ 𝑥 } ) )
146 74 76 145 syl2anc ⊢ ( ( ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( ( 𝑠 ∈ 𝒫 { 𝑡 ∈ ∪ 𝑅 ∣ ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ ∈ 𝑥 } ∧ 𝑢 ∈ 𝑅 ) ∧ ( ( 1st ‘ 𝑦 ) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝑅 ↾t 𝑠 ) ∈ Comp ) ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ ( 𝑆 ↾t 𝑘 ) ∈ Comp ) ) → ( ( 2nd ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) “ ( ( 𝑠 × 𝑘 ) ∖ 𝑥 ) ) = ( 𝑘 ∖ { 𝑣 ∈ ∪ 𝑆 ∣ ( 𝑠 × { 𝑣 } ) ⊆ 𝑥 } ) )
147 difin ⊢ ( 𝑘 ∖ ( 𝑘 ∩ { 𝑣 ∈ ∪ 𝑆 ∣ ( 𝑠 × { 𝑣 } ) ⊆ 𝑥 } ) ) = ( 𝑘 ∖ { 𝑣 ∈ ∪ 𝑆 ∣ ( 𝑠 × { 𝑣 } ) ⊆ 𝑥 } )
148 65 adantr ⊢ ( ( ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( ( 𝑠 ∈ 𝒫 { 𝑡 ∈ ∪ 𝑅 ∣ ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ ∈ 𝑥 } ∧ 𝑢 ∈ 𝑅 ) ∧ ( ( 1st ‘ 𝑦 ) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝑅 ↾t 𝑠 ) ∈ Comp ) ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ ( 𝑆 ↾t 𝑘 ) ∈ Comp ) ) → 𝑆 ∈ Top )
149 24 restuni ⊢ ( ( 𝑆 ∈ Top ∧ 𝑘 ⊆ ∪ 𝑆 ) → 𝑘 = ∪ ( 𝑆 ↾t 𝑘 ) )
150 148 76 149 syl2anc ⊢ ( ( ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( ( 𝑠 ∈ 𝒫 { 𝑡 ∈ ∪ 𝑅 ∣ ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ ∈ 𝑥 } ∧ 𝑢 ∈ 𝑅 ) ∧ ( ( 1st ‘ 𝑦 ) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝑅 ↾t 𝑠 ) ∈ Comp ) ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ ( 𝑆 ↾t 𝑘 ) ∈ Comp ) ) → 𝑘 = ∪ ( 𝑆 ↾t 𝑘 ) )
151 150 difeq1d ⊢ ( ( ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( ( 𝑠 ∈ 𝒫 { 𝑡 ∈ ∪ 𝑅 ∣ ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ ∈ 𝑥 } ∧ 𝑢 ∈ 𝑅 ) ∧ ( ( 1st ‘ 𝑦 ) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝑅 ↾t 𝑠 ) ∈ Comp ) ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ ( 𝑆 ↾t 𝑘 ) ∈ Comp ) ) → ( 𝑘 ∖ ( 𝑘 ∩ { 𝑣 ∈ ∪ 𝑆 ∣ ( 𝑠 × { 𝑣 } ) ⊆ 𝑥 } ) ) = ( ∪ ( 𝑆 ↾t 𝑘 ) ∖ ( 𝑘 ∩ { 𝑣 ∈ ∪ 𝑆 ∣ ( 𝑠 × { 𝑣 } ) ⊆ 𝑥 } ) ) )
152 147 151 eqtr3id ⊢ ( ( ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( ( 𝑠 ∈ 𝒫 { 𝑡 ∈ ∪ 𝑅 ∣ ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ ∈ 𝑥 } ∧ 𝑢 ∈ 𝑅 ) ∧ ( ( 1st ‘ 𝑦 ) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝑅 ↾t 𝑠 ) ∈ Comp ) ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ ( 𝑆 ↾t 𝑘 ) ∈ Comp ) ) → ( 𝑘 ∖ { 𝑣 ∈ ∪ 𝑆 ∣ ( 𝑠 × { 𝑣 } ) ⊆ 𝑥 } ) = ( ∪ ( 𝑆 ↾t 𝑘 ) ∖ ( 𝑘 ∩ { 𝑣 ∈ ∪ 𝑆 ∣ ( 𝑠 × { 𝑣 } ) ⊆ 𝑥 } ) ) )
153 146 152 eqtrd ⊢ ( ( ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( ( 𝑠 ∈ 𝒫 { 𝑡 ∈ ∪ 𝑅 ∣ ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ ∈ 𝑥 } ∧ 𝑢 ∈ 𝑅 ) ∧ ( ( 1st ‘ 𝑦 ) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝑅 ↾t 𝑠 ) ∈ Comp ) ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ ( 𝑆 ↾t 𝑘 ) ∈ Comp ) ) → ( ( 2nd ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) “ ( ( 𝑠 × 𝑘 ) ∖ 𝑥 ) ) = ( ∪ ( 𝑆 ↾t 𝑘 ) ∖ ( 𝑘 ∩ { 𝑣 ∈ ∪ 𝑆 ∣ ( 𝑠 × { 𝑣 } ) ⊆ 𝑥 } ) ) )
154 15 ad2antrr ⊢ ( ( ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( ( 𝑠 ∈ 𝒫 { 𝑡 ∈ ∪ 𝑅 ∣ ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ ∈ 𝑥 } ∧ 𝑢 ∈ 𝑅 ) ∧ ( ( 1st ‘ 𝑦 ) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝑅 ↾t 𝑠 ) ∈ Comp ) ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ ( 𝑆 ↾t 𝑘 ) ∈ Comp ) ) → 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) )
155 154 elin2d ⊢ ( ( ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( ( 𝑠 ∈ 𝒫 { 𝑡 ∈ ∪ 𝑅 ∣ ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ ∈ 𝑥 } ∧ 𝑢 ∈ 𝑅 ) ∧ ( ( 1st ‘ 𝑦 ) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝑅 ↾t 𝑠 ) ∈ Comp ) ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ ( 𝑆 ↾t 𝑘 ) ∈ Comp ) ) → 𝑆 ∈ Haus )
156 df-ima ⊢ ( ( 2nd ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) “ ( ( 𝑠 × 𝑘 ) ∖ 𝑥 ) ) = ran ( ( 2nd ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) ↾ ( ( 𝑠 × 𝑘 ) ∖ 𝑥 ) )
157 resres ⊢ ( ( 2nd ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) ↾ ( ( 𝑠 × 𝑘 ) ∖ 𝑥 ) ) = ( 2nd ↾ ( ( ∪ 𝑅 × ∪ 𝑆 ) ∩ ( ( 𝑠 × 𝑘 ) ∖ 𝑥 ) ) )
158 inss2 ⊢ ( ( ∪ 𝑅 × ∪ 𝑆 ) ∩ ( ( 𝑠 × 𝑘 ) ∖ 𝑥 ) ) ⊆ ( ( 𝑠 × 𝑘 ) ∖ 𝑥 )
159 158 116 sstri ⊢ ( ( ∪ 𝑅 × ∪ 𝑆 ) ∩ ( ( 𝑠 × 𝑘 ) ∖ 𝑥 ) ) ⊆ ( 𝑠 × 𝑘 )
160 ssres2 ⊢ ( ( ( ∪ 𝑅 × ∪ 𝑆 ) ∩ ( ( 𝑠 × 𝑘 ) ∖ 𝑥 ) ) ⊆ ( 𝑠 × 𝑘 ) → ( 2nd ↾ ( ( ∪ 𝑅 × ∪ 𝑆 ) ∩ ( ( 𝑠 × 𝑘 ) ∖ 𝑥 ) ) ) ⊆ ( 2nd ↾ ( 𝑠 × 𝑘 ) ) )
161 159 160 ax-mp ⊢ ( 2nd ↾ ( ( ∪ 𝑅 × ∪ 𝑆 ) ∩ ( ( 𝑠 × 𝑘 ) ∖ 𝑥 ) ) ) ⊆ ( 2nd ↾ ( 𝑠 × 𝑘 ) )
162 157 161 eqsstri ⊢ ( ( 2nd ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) ↾ ( ( 𝑠 × 𝑘 ) ∖ 𝑥 ) ) ⊆ ( 2nd ↾ ( 𝑠 × 𝑘 ) )
163 162 rnssi ⊢ ran ( ( 2nd ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) ↾ ( ( 𝑠 × 𝑘 ) ∖ 𝑥 ) ) ⊆ ran ( 2nd ↾ ( 𝑠 × 𝑘 ) )
164 156 163 eqsstri ⊢ ( ( 2nd ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) “ ( ( 𝑠 × 𝑘 ) ∖ 𝑥 ) ) ⊆ ran ( 2nd ↾ ( 𝑠 × 𝑘 ) )
165 f2ndres ⊢ ( 2nd ↾ ( 𝑠 × 𝑘 ) ) : ( 𝑠 × 𝑘 ) ⟶ 𝑘
166 frn ⊢ ( ( 2nd ↾ ( 𝑠 × 𝑘 ) ) : ( 𝑠 × 𝑘 ) ⟶ 𝑘 → ran ( 2nd ↾ ( 𝑠 × 𝑘 ) ) ⊆ 𝑘 )
167 165 166 ax-mp ⊢ ran ( 2nd ↾ ( 𝑠 × 𝑘 ) ) ⊆ 𝑘
168 164 167 sstri ⊢ ( ( 2nd ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) “ ( ( 𝑠 × 𝑘 ) ∖ 𝑥 ) ) ⊆ 𝑘
169 168 76 sstrid ⊢ ( ( ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( ( 𝑠 ∈ 𝒫 { 𝑡 ∈ ∪ 𝑅 ∣ ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ ∈ 𝑥 } ∧ 𝑢 ∈ 𝑅 ) ∧ ( ( 1st ‘ 𝑦 ) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝑅 ↾t 𝑠 ) ∈ Comp ) ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ ( 𝑆 ↾t 𝑘 ) ∈ Comp ) ) → ( ( 2nd ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) “ ( ( 𝑠 × 𝑘 ) ∖ 𝑥 ) ) ⊆ ∪ 𝑆 )
170 12 ad2antrr ⊢ ( ( ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( ( 𝑠 ∈ 𝒫 { 𝑡 ∈ ∪ 𝑅 ∣ ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ ∈ 𝑥 } ∧ 𝑢 ∈ 𝑅 ) ∧ ( ( 1st ‘ 𝑦 ) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝑅 ↾t 𝑠 ) ∈ Comp ) ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ ( 𝑆 ↾t 𝑘 ) ∈ Comp ) ) → 𝑅 ∈ ( TopOn ‘ ∪ 𝑅 ) )
171 148 17 sylib ⊢ ( ( ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( ( 𝑠 ∈ 𝒫 { 𝑡 ∈ ∪ 𝑅 ∣ ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ ∈ 𝑥 } ∧ 𝑢 ∈ 𝑅 ) ∧ ( ( 1st ‘ 𝑦 ) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝑅 ↾t 𝑠 ) ∈ Comp ) ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ ( 𝑆 ↾t 𝑘 ) ∈ Comp ) ) → 𝑆 ∈ ( TopOn ‘ ∪ 𝑆 ) )
172 tx2cn ⊢ ( ( 𝑅 ∈ ( TopOn ‘ ∪ 𝑅 ) ∧ 𝑆 ∈ ( TopOn ‘ ∪ 𝑆 ) ) → ( 2nd ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) ∈ ( ( 𝑅 ×t 𝑆 ) Cn 𝑆 ) )
173 170 171 172 syl2anc ⊢ ( ( ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( ( 𝑠 ∈ 𝒫 { 𝑡 ∈ ∪ 𝑅 ∣ ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ ∈ 𝑥 } ∧ 𝑢 ∈ 𝑅 ) ∧ ( ( 1st ‘ 𝑦 ) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝑅 ↾t 𝑠 ) ∈ Comp ) ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ ( 𝑆 ↾t 𝑘 ) ∈ Comp ) ) → ( 2nd ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) ∈ ( ( 𝑅 ×t 𝑆 ) Cn 𝑆 ) )
174 27 ad2antrr ⊢ ( ( ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( ( 𝑠 ∈ 𝒫 { 𝑡 ∈ ∪ 𝑅 ∣ ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ ∈ 𝑥 } ∧ 𝑢 ∈ 𝑅 ) ∧ ( ( 1st ‘ 𝑦 ) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝑅 ↾t 𝑠 ) ∈ Comp ) ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ ( 𝑆 ↾t 𝑘 ) ∈ Comp ) ) → ( 𝑅 ×t 𝑆 ) ∈ Top )
175 116 a1i ⊢ ( ( ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( ( 𝑠 ∈ 𝒫 { 𝑡 ∈ ∪ 𝑅 ∣ ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ ∈ 𝑥 } ∧ 𝑢 ∈ 𝑅 ) ∧ ( ( 1st ‘ 𝑦 ) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝑅 ↾t 𝑠 ) ∈ Comp ) ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ ( 𝑆 ↾t 𝑘 ) ∈ Comp ) ) → ( ( 𝑠 × 𝑘 ) ∖ 𝑥 ) ⊆ ( 𝑠 × 𝑘 ) )
176 vex ⊢ 𝑠 ∈ V
177 vex ⊢ 𝑘 ∈ V
178 176 177 xpex ⊢ ( 𝑠 × 𝑘 ) ∈ V
179 178 a1i ⊢ ( ( ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( ( 𝑠 ∈ 𝒫 { 𝑡 ∈ ∪ 𝑅 ∣ ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ ∈ 𝑥 } ∧ 𝑢 ∈ 𝑅 ) ∧ ( ( 1st ‘ 𝑦 ) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝑅 ↾t 𝑠 ) ∈ Comp ) ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ ( 𝑆 ↾t 𝑘 ) ∈ Comp ) ) → ( 𝑠 × 𝑘 ) ∈ V )
180 restabs ⊢ ( ( ( 𝑅 ×t 𝑆 ) ∈ Top ∧ ( ( 𝑠 × 𝑘 ) ∖ 𝑥 ) ⊆ ( 𝑠 × 𝑘 ) ∧ ( 𝑠 × 𝑘 ) ∈ V ) → ( ( ( 𝑅 ×t 𝑆 ) ↾t ( 𝑠 × 𝑘 ) ) ↾t ( ( 𝑠 × 𝑘 ) ∖ 𝑥 ) ) = ( ( 𝑅 ×t 𝑆 ) ↾t ( ( 𝑠 × 𝑘 ) ∖ 𝑥 ) ) )
181 174 175 179 180 syl3anc ⊢ ( ( ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( ( 𝑠 ∈ 𝒫 { 𝑡 ∈ ∪ 𝑅 ∣ ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ ∈ 𝑥 } ∧ 𝑢 ∈ 𝑅 ) ∧ ( ( 1st ‘ 𝑦 ) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝑅 ↾t 𝑠 ) ∈ Comp ) ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ ( 𝑆 ↾t 𝑘 ) ∈ Comp ) ) → ( ( ( 𝑅 ×t 𝑆 ) ↾t ( 𝑠 × 𝑘 ) ) ↾t ( ( 𝑠 × 𝑘 ) ∖ 𝑥 ) ) = ( ( 𝑅 ×t 𝑆 ) ↾t ( ( 𝑠 × 𝑘 ) ∖ 𝑥 ) ) )
182 64 adantr ⊢ ( ( ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( ( 𝑠 ∈ 𝒫 { 𝑡 ∈ ∪ 𝑅 ∣ ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ ∈ 𝑥 } ∧ 𝑢 ∈ 𝑅 ) ∧ ( ( 1st ‘ 𝑦 ) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝑅 ↾t 𝑠 ) ∈ Comp ) ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ ( 𝑆 ↾t 𝑘 ) ∈ Comp ) ) → 𝑅 ∈ Top )
183 154 4 syl ⊢ ( ( ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( ( 𝑠 ∈ 𝒫 { 𝑡 ∈ ∪ 𝑅 ∣ ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ ∈ 𝑥 } ∧ 𝑢 ∈ 𝑅 ) ∧ ( ( 1st ‘ 𝑦 ) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝑅 ↾t 𝑠 ) ∈ Comp ) ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ ( 𝑆 ↾t 𝑘 ) ∈ Comp ) ) → 𝑆 ∈ Top )
184 176 a1i ⊢ ( ( ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( ( 𝑠 ∈ 𝒫 { 𝑡 ∈ ∪ 𝑅 ∣ ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ ∈ 𝑥 } ∧ 𝑢 ∈ 𝑅 ) ∧ ( ( 1st ‘ 𝑦 ) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝑅 ↾t 𝑠 ) ∈ Comp ) ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ ( 𝑆 ↾t 𝑘 ) ∈ Comp ) ) → 𝑠 ∈ V )
185 simprl ⊢ ( ( ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( ( 𝑠 ∈ 𝒫 { 𝑡 ∈ ∪ 𝑅 ∣ ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ ∈ 𝑥 } ∧ 𝑢 ∈ 𝑅 ) ∧ ( ( 1st ‘ 𝑦 ) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝑅 ↾t 𝑠 ) ∈ Comp ) ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ ( 𝑆 ↾t 𝑘 ) ∈ Comp ) ) → 𝑘 ∈ 𝒫 ∪ 𝑆 )
186 txrest ⊢ ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) ∧ ( 𝑠 ∈ V ∧ 𝑘 ∈ 𝒫 ∪ 𝑆 ) ) → ( ( 𝑅 ×t 𝑆 ) ↾t ( 𝑠 × 𝑘 ) ) = ( ( 𝑅 ↾t 𝑠 ) ×t ( 𝑆 ↾t 𝑘 ) ) )
187 182 183 184 185 186 syl22anc ⊢ ( ( ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( ( 𝑠 ∈ 𝒫 { 𝑡 ∈ ∪ 𝑅 ∣ ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ ∈ 𝑥 } ∧ 𝑢 ∈ 𝑅 ) ∧ ( ( 1st ‘ 𝑦 ) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝑅 ↾t 𝑠 ) ∈ Comp ) ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ ( 𝑆 ↾t 𝑘 ) ∈ Comp ) ) → ( ( 𝑅 ×t 𝑆 ) ↾t ( 𝑠 × 𝑘 ) ) = ( ( 𝑅 ↾t 𝑠 ) ×t ( 𝑆 ↾t 𝑘 ) ) )
188 simprr3 ⊢ ( ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( ( 𝑠 ∈ 𝒫 { 𝑡 ∈ ∪ 𝑅 ∣ ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ ∈ 𝑥 } ∧ 𝑢 ∈ 𝑅 ) ∧ ( ( 1st ‘ 𝑦 ) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝑅 ↾t 𝑠 ) ∈ Comp ) ) ) → ( 𝑅 ↾t 𝑠 ) ∈ Comp )
189 188 adantr ⊢ ( ( ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( ( 𝑠 ∈ 𝒫 { 𝑡 ∈ ∪ 𝑅 ∣ ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ ∈ 𝑥 } ∧ 𝑢 ∈ 𝑅 ) ∧ ( ( 1st ‘ 𝑦 ) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝑅 ↾t 𝑠 ) ∈ Comp ) ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ ( 𝑆 ↾t 𝑘 ) ∈ Comp ) ) → ( 𝑅 ↾t 𝑠 ) ∈ Comp )
190 simprr ⊢ ( ( ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( ( 𝑠 ∈ 𝒫 { 𝑡 ∈ ∪ 𝑅 ∣ ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ ∈ 𝑥 } ∧ 𝑢 ∈ 𝑅 ) ∧ ( ( 1st ‘ 𝑦 ) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝑅 ↾t 𝑠 ) ∈ Comp ) ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ ( 𝑆 ↾t 𝑘 ) ∈ Comp ) ) → ( 𝑆 ↾t 𝑘 ) ∈ Comp )
191 txcmp ⊢ ( ( ( 𝑅 ↾t 𝑠 ) ∈ Comp ∧ ( 𝑆 ↾t 𝑘 ) ∈ Comp ) → ( ( 𝑅 ↾t 𝑠 ) ×t ( 𝑆 ↾t 𝑘 ) ) ∈ Comp )
192 189 190 191 syl2anc ⊢ ( ( ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( ( 𝑠 ∈ 𝒫 { 𝑡 ∈ ∪ 𝑅 ∣ ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ ∈ 𝑥 } ∧ 𝑢 ∈ 𝑅 ) ∧ ( ( 1st ‘ 𝑦 ) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝑅 ↾t 𝑠 ) ∈ Comp ) ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ ( 𝑆 ↾t 𝑘 ) ∈ Comp ) ) → ( ( 𝑅 ↾t 𝑠 ) ×t ( 𝑆 ↾t 𝑘 ) ) ∈ Comp )
193 187 192 eqeltrd ⊢ ( ( ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( ( 𝑠 ∈ 𝒫 { 𝑡 ∈ ∪ 𝑅 ∣ ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ ∈ 𝑥 } ∧ 𝑢 ∈ 𝑅 ) ∧ ( ( 1st ‘ 𝑦 ) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝑅 ↾t 𝑠 ) ∈ Comp ) ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ ( 𝑆 ↾t 𝑘 ) ∈ Comp ) ) → ( ( 𝑅 ×t 𝑆 ) ↾t ( 𝑠 × 𝑘 ) ) ∈ Comp )
194 difin ⊢ ( ( 𝑠 × 𝑘 ) ∖ ( ( 𝑠 × 𝑘 ) ∩ 𝑥 ) ) = ( ( 𝑠 × 𝑘 ) ∖ 𝑥 )
195 74 76 117 syl2anc ⊢ ( ( ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( ( 𝑠 ∈ 𝒫 { 𝑡 ∈ ∪ 𝑅 ∣ ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ ∈ 𝑥 } ∧ 𝑢 ∈ 𝑅 ) ∧ ( ( 1st ‘ 𝑦 ) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝑅 ↾t 𝑠 ) ∈ Comp ) ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ ( 𝑆 ↾t 𝑘 ) ∈ Comp ) ) → ( 𝑠 × 𝑘 ) ⊆ ( ∪ 𝑅 × ∪ 𝑆 ) )
196 182 148 25 syl2anc ⊢ ( ( ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( ( 𝑠 ∈ 𝒫 { 𝑡 ∈ ∪ 𝑅 ∣ ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ ∈ 𝑥 } ∧ 𝑢 ∈ 𝑅 ) ∧ ( ( 1st ‘ 𝑦 ) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝑅 ↾t 𝑠 ) ∈ Comp ) ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ ( 𝑆 ↾t 𝑘 ) ∈ Comp ) ) → ( ∪ 𝑅 × ∪ 𝑆 ) = ∪ ( 𝑅 ×t 𝑆 ) )
197 195 196 sseqtrd ⊢ ( ( ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( ( 𝑠 ∈ 𝒫 { 𝑡 ∈ ∪ 𝑅 ∣ ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ ∈ 𝑥 } ∧ 𝑢 ∈ 𝑅 ) ∧ ( ( 1st ‘ 𝑦 ) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝑅 ↾t 𝑠 ) ∈ Comp ) ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ ( 𝑆 ↾t 𝑘 ) ∈ Comp ) ) → ( 𝑠 × 𝑘 ) ⊆ ∪ ( 𝑅 ×t 𝑆 ) )
198 28 restuni ⊢ ( ( ( 𝑅 ×t 𝑆 ) ∈ Top ∧ ( 𝑠 × 𝑘 ) ⊆ ∪ ( 𝑅 ×t 𝑆 ) ) → ( 𝑠 × 𝑘 ) = ∪ ( ( 𝑅 ×t 𝑆 ) ↾t ( 𝑠 × 𝑘 ) ) )
199 174 197 198 syl2anc ⊢ ( ( ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( ( 𝑠 ∈ 𝒫 { 𝑡 ∈ ∪ 𝑅 ∣ ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ ∈ 𝑥 } ∧ 𝑢 ∈ 𝑅 ) ∧ ( ( 1st ‘ 𝑦 ) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝑅 ↾t 𝑠 ) ∈ Comp ) ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ ( 𝑆 ↾t 𝑘 ) ∈ Comp ) ) → ( 𝑠 × 𝑘 ) = ∪ ( ( 𝑅 ×t 𝑆 ) ↾t ( 𝑠 × 𝑘 ) ) )
200 199 difeq1d ⊢ ( ( ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( ( 𝑠 ∈ 𝒫 { 𝑡 ∈ ∪ 𝑅 ∣ ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ ∈ 𝑥 } ∧ 𝑢 ∈ 𝑅 ) ∧ ( ( 1st ‘ 𝑦 ) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝑅 ↾t 𝑠 ) ∈ Comp ) ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ ( 𝑆 ↾t 𝑘 ) ∈ Comp ) ) → ( ( 𝑠 × 𝑘 ) ∖ ( ( 𝑠 × 𝑘 ) ∩ 𝑥 ) ) = ( ∪ ( ( 𝑅 ×t 𝑆 ) ↾t ( 𝑠 × 𝑘 ) ) ∖ ( ( 𝑠 × 𝑘 ) ∩ 𝑥 ) ) )
201 194 200 eqtr3id ⊢ ( ( ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( ( 𝑠 ∈ 𝒫 { 𝑡 ∈ ∪ 𝑅 ∣ ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ ∈ 𝑥 } ∧ 𝑢 ∈ 𝑅 ) ∧ ( ( 1st ‘ 𝑦 ) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝑅 ↾t 𝑠 ) ∈ Comp ) ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ ( 𝑆 ↾t 𝑘 ) ∈ Comp ) ) → ( ( 𝑠 × 𝑘 ) ∖ 𝑥 ) = ( ∪ ( ( 𝑅 ×t 𝑆 ) ↾t ( 𝑠 × 𝑘 ) ) ∖ ( ( 𝑠 × 𝑘 ) ∩ 𝑥 ) ) )
202 resttop ⊢ ( ( ( 𝑅 ×t 𝑆 ) ∈ Top ∧ ( 𝑠 × 𝑘 ) ∈ V ) → ( ( 𝑅 ×t 𝑆 ) ↾t ( 𝑠 × 𝑘 ) ) ∈ Top )
203 174 178 202 sylancl ⊢ ( ( ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( ( 𝑠 ∈ 𝒫 { 𝑡 ∈ ∪ 𝑅 ∣ ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ ∈ 𝑥 } ∧ 𝑢 ∈ 𝑅 ) ∧ ( ( 1st ‘ 𝑦 ) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝑅 ↾t 𝑠 ) ∈ Comp ) ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ ( 𝑆 ↾t 𝑘 ) ∈ Comp ) ) → ( ( 𝑅 ×t 𝑆 ) ↾t ( 𝑠 × 𝑘 ) ) ∈ Top )
204 incom ⊢ ( ( 𝑠 × 𝑘 ) ∩ 𝑥 ) = ( 𝑥 ∩ ( 𝑠 × 𝑘 ) )
205 20 ad2antrr ⊢ ( ( ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( ( 𝑠 ∈ 𝒫 { 𝑡 ∈ ∪ 𝑅 ∣ ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ ∈ 𝑥 } ∧ 𝑢 ∈ 𝑅 ) ∧ ( ( 1st ‘ 𝑦 ) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝑅 ↾t 𝑠 ) ∈ Comp ) ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ ( 𝑆 ↾t 𝑘 ) ∈ Comp ) ) → 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) )
206 kgeni ⊢ ( ( 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ∧ ( ( 𝑅 ×t 𝑆 ) ↾t ( 𝑠 × 𝑘 ) ) ∈ Comp ) → ( 𝑥 ∩ ( 𝑠 × 𝑘 ) ) ∈ ( ( 𝑅 ×t 𝑆 ) ↾t ( 𝑠 × 𝑘 ) ) )
207 205 193 206 syl2anc ⊢ ( ( ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( ( 𝑠 ∈ 𝒫 { 𝑡 ∈ ∪ 𝑅 ∣ ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ ∈ 𝑥 } ∧ 𝑢 ∈ 𝑅 ) ∧ ( ( 1st ‘ 𝑦 ) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝑅 ↾t 𝑠 ) ∈ Comp ) ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ ( 𝑆 ↾t 𝑘 ) ∈ Comp ) ) → ( 𝑥 ∩ ( 𝑠 × 𝑘 ) ) ∈ ( ( 𝑅 ×t 𝑆 ) ↾t ( 𝑠 × 𝑘 ) ) )
208 204 207 eqeltrid ⊢ ( ( ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( ( 𝑠 ∈ 𝒫 { 𝑡 ∈ ∪ 𝑅 ∣ ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ ∈ 𝑥 } ∧ 𝑢 ∈ 𝑅 ) ∧ ( ( 1st ‘ 𝑦 ) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝑅 ↾t 𝑠 ) ∈ Comp ) ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ ( 𝑆 ↾t 𝑘 ) ∈ Comp ) ) → ( ( 𝑠 × 𝑘 ) ∩ 𝑥 ) ∈ ( ( 𝑅 ×t 𝑆 ) ↾t ( 𝑠 × 𝑘 ) ) )
209 eqid ⊢ ∪ ( ( 𝑅 ×t 𝑆 ) ↾t ( 𝑠 × 𝑘 ) ) = ∪ ( ( 𝑅 ×t 𝑆 ) ↾t ( 𝑠 × 𝑘 ) )
210 209 opncld ⊢ ( ( ( ( 𝑅 ×t 𝑆 ) ↾t ( 𝑠 × 𝑘 ) ) ∈ Top ∧ ( ( 𝑠 × 𝑘 ) ∩ 𝑥 ) ∈ ( ( 𝑅 ×t 𝑆 ) ↾t ( 𝑠 × 𝑘 ) ) ) → ( ∪ ( ( 𝑅 ×t 𝑆 ) ↾t ( 𝑠 × 𝑘 ) ) ∖ ( ( 𝑠 × 𝑘 ) ∩ 𝑥 ) ) ∈ ( Clsd ‘ ( ( 𝑅 ×t 𝑆 ) ↾t ( 𝑠 × 𝑘 ) ) ) )
211 203 208 210 syl2anc ⊢ ( ( ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( ( 𝑠 ∈ 𝒫 { 𝑡 ∈ ∪ 𝑅 ∣ ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ ∈ 𝑥 } ∧ 𝑢 ∈ 𝑅 ) ∧ ( ( 1st ‘ 𝑦 ) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝑅 ↾t 𝑠 ) ∈ Comp ) ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ ( 𝑆 ↾t 𝑘 ) ∈ Comp ) ) → ( ∪ ( ( 𝑅 ×t 𝑆 ) ↾t ( 𝑠 × 𝑘 ) ) ∖ ( ( 𝑠 × 𝑘 ) ∩ 𝑥 ) ) ∈ ( Clsd ‘ ( ( 𝑅 ×t 𝑆 ) ↾t ( 𝑠 × 𝑘 ) ) ) )
212 201 211 eqeltrd ⊢ ( ( ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( ( 𝑠 ∈ 𝒫 { 𝑡 ∈ ∪ 𝑅 ∣ ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ ∈ 𝑥 } ∧ 𝑢 ∈ 𝑅 ) ∧ ( ( 1st ‘ 𝑦 ) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝑅 ↾t 𝑠 ) ∈ Comp ) ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ ( 𝑆 ↾t 𝑘 ) ∈ Comp ) ) → ( ( 𝑠 × 𝑘 ) ∖ 𝑥 ) ∈ ( Clsd ‘ ( ( 𝑅 ×t 𝑆 ) ↾t ( 𝑠 × 𝑘 ) ) ) )
213 cmpcld ⊢ ( ( ( ( 𝑅 ×t 𝑆 ) ↾t ( 𝑠 × 𝑘 ) ) ∈ Comp ∧ ( ( 𝑠 × 𝑘 ) ∖ 𝑥 ) ∈ ( Clsd ‘ ( ( 𝑅 ×t 𝑆 ) ↾t ( 𝑠 × 𝑘 ) ) ) ) → ( ( ( 𝑅 ×t 𝑆 ) ↾t ( 𝑠 × 𝑘 ) ) ↾t ( ( 𝑠 × 𝑘 ) ∖ 𝑥 ) ) ∈ Comp )
214 193 212 213 syl2anc ⊢ ( ( ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( ( 𝑠 ∈ 𝒫 { 𝑡 ∈ ∪ 𝑅 ∣ ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ ∈ 𝑥 } ∧ 𝑢 ∈ 𝑅 ) ∧ ( ( 1st ‘ 𝑦 ) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝑅 ↾t 𝑠 ) ∈ Comp ) ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ ( 𝑆 ↾t 𝑘 ) ∈ Comp ) ) → ( ( ( 𝑅 ×t 𝑆 ) ↾t ( 𝑠 × 𝑘 ) ) ↾t ( ( 𝑠 × 𝑘 ) ∖ 𝑥 ) ) ∈ Comp )
215 181 214 eqeltrrd ⊢ ( ( ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( ( 𝑠 ∈ 𝒫 { 𝑡 ∈ ∪ 𝑅 ∣ ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ ∈ 𝑥 } ∧ 𝑢 ∈ 𝑅 ) ∧ ( ( 1st ‘ 𝑦 ) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝑅 ↾t 𝑠 ) ∈ Comp ) ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ ( 𝑆 ↾t 𝑘 ) ∈ Comp ) ) → ( ( 𝑅 ×t 𝑆 ) ↾t ( ( 𝑠 × 𝑘 ) ∖ 𝑥 ) ) ∈ Comp )
216 imacmp ⊢ ( ( ( 2nd ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) ∈ ( ( 𝑅 ×t 𝑆 ) Cn 𝑆 ) ∧ ( ( 𝑅 ×t 𝑆 ) ↾t ( ( 𝑠 × 𝑘 ) ∖ 𝑥 ) ) ∈ Comp ) → ( 𝑆 ↾t ( ( 2nd ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) “ ( ( 𝑠 × 𝑘 ) ∖ 𝑥 ) ) ) ∈ Comp )
217 173 215 216 syl2anc ⊢ ( ( ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( ( 𝑠 ∈ 𝒫 { 𝑡 ∈ ∪ 𝑅 ∣ ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ ∈ 𝑥 } ∧ 𝑢 ∈ 𝑅 ) ∧ ( ( 1st ‘ 𝑦 ) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝑅 ↾t 𝑠 ) ∈ Comp ) ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ ( 𝑆 ↾t 𝑘 ) ∈ Comp ) ) → ( 𝑆 ↾t ( ( 2nd ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) “ ( ( 𝑠 × 𝑘 ) ∖ 𝑥 ) ) ) ∈ Comp )
218 24 hauscmp ⊢ ( ( 𝑆 ∈ Haus ∧ ( ( 2nd ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) “ ( ( 𝑠 × 𝑘 ) ∖ 𝑥 ) ) ⊆ ∪ 𝑆 ∧ ( 𝑆 ↾t ( ( 2nd ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) “ ( ( 𝑠 × 𝑘 ) ∖ 𝑥 ) ) ) ∈ Comp ) → ( ( 2nd ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) “ ( ( 𝑠 × 𝑘 ) ∖ 𝑥 ) ) ∈ ( Clsd ‘ 𝑆 ) )
219 155 169 217 218 syl3anc ⊢ ( ( ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( ( 𝑠 ∈ 𝒫 { 𝑡 ∈ ∪ 𝑅 ∣ ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ ∈ 𝑥 } ∧ 𝑢 ∈ 𝑅 ) ∧ ( ( 1st ‘ 𝑦 ) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝑅 ↾t 𝑠 ) ∈ Comp ) ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ ( 𝑆 ↾t 𝑘 ) ∈ Comp ) ) → ( ( 2nd ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) “ ( ( 𝑠 × 𝑘 ) ∖ 𝑥 ) ) ∈ ( Clsd ‘ 𝑆 ) )
220 168 a1i ⊢ ( ( ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( ( 𝑠 ∈ 𝒫 { 𝑡 ∈ ∪ 𝑅 ∣ ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ ∈ 𝑥 } ∧ 𝑢 ∈ 𝑅 ) ∧ ( ( 1st ‘ 𝑦 ) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝑅 ↾t 𝑠 ) ∈ Comp ) ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ ( 𝑆 ↾t 𝑘 ) ∈ Comp ) ) → ( ( 2nd ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) “ ( ( 𝑠 × 𝑘 ) ∖ 𝑥 ) ) ⊆ 𝑘 )
221 24 restcldi ⊢ ( ( 𝑘 ⊆ ∪ 𝑆 ∧ ( ( 2nd ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) “ ( ( 𝑠 × 𝑘 ) ∖ 𝑥 ) ) ∈ ( Clsd ‘ 𝑆 ) ∧ ( ( 2nd ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) “ ( ( 𝑠 × 𝑘 ) ∖ 𝑥 ) ) ⊆ 𝑘 ) → ( ( 2nd ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) “ ( ( 𝑠 × 𝑘 ) ∖ 𝑥 ) ) ∈ ( Clsd ‘ ( 𝑆 ↾t 𝑘 ) ) )
222 76 219 220 221 syl3anc ⊢ ( ( ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( ( 𝑠 ∈ 𝒫 { 𝑡 ∈ ∪ 𝑅 ∣ ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ ∈ 𝑥 } ∧ 𝑢 ∈ 𝑅 ) ∧ ( ( 1st ‘ 𝑦 ) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝑅 ↾t 𝑠 ) ∈ Comp ) ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ ( 𝑆 ↾t 𝑘 ) ∈ Comp ) ) → ( ( 2nd ↾ ( ∪ 𝑅 × ∪ 𝑆 ) ) “ ( ( 𝑠 × 𝑘 ) ∖ 𝑥 ) ) ∈ ( Clsd ‘ ( 𝑆 ↾t 𝑘 ) ) )
223 153 222 eqeltrrd ⊢ ( ( ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( ( 𝑠 ∈ 𝒫 { 𝑡 ∈ ∪ 𝑅 ∣ ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ ∈ 𝑥 } ∧ 𝑢 ∈ 𝑅 ) ∧ ( ( 1st ‘ 𝑦 ) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝑅 ↾t 𝑠 ) ∈ Comp ) ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ ( 𝑆 ↾t 𝑘 ) ∈ Comp ) ) → ( ∪ ( 𝑆 ↾t 𝑘 ) ∖ ( 𝑘 ∩ { 𝑣 ∈ ∪ 𝑆 ∣ ( 𝑠 × { 𝑣 } ) ⊆ 𝑥 } ) ) ∈ ( Clsd ‘ ( 𝑆 ↾t 𝑘 ) ) )
224 resttop ⊢ ( ( 𝑆 ∈ Top ∧ 𝑘 ∈ 𝒫 ∪ 𝑆 ) → ( 𝑆 ↾t 𝑘 ) ∈ Top )
225 148 185 224 syl2anc ⊢ ( ( ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( ( 𝑠 ∈ 𝒫 { 𝑡 ∈ ∪ 𝑅 ∣ ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ ∈ 𝑥 } ∧ 𝑢 ∈ 𝑅 ) ∧ ( ( 1st ‘ 𝑦 ) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝑅 ↾t 𝑠 ) ∈ Comp ) ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ ( 𝑆 ↾t 𝑘 ) ∈ Comp ) ) → ( 𝑆 ↾t 𝑘 ) ∈ Top )
226 inss1 ⊢ ( 𝑘 ∩ { 𝑣 ∈ ∪ 𝑆 ∣ ( 𝑠 × { 𝑣 } ) ⊆ 𝑥 } ) ⊆ 𝑘
227 226 150 sseqtrid ⊢ ( ( ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( ( 𝑠 ∈ 𝒫 { 𝑡 ∈ ∪ 𝑅 ∣ ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ ∈ 𝑥 } ∧ 𝑢 ∈ 𝑅 ) ∧ ( ( 1st ‘ 𝑦 ) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝑅 ↾t 𝑠 ) ∈ Comp ) ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ ( 𝑆 ↾t 𝑘 ) ∈ Comp ) ) → ( 𝑘 ∩ { 𝑣 ∈ ∪ 𝑆 ∣ ( 𝑠 × { 𝑣 } ) ⊆ 𝑥 } ) ⊆ ∪ ( 𝑆 ↾t 𝑘 ) )
228 eqid ⊢ ∪ ( 𝑆 ↾t 𝑘 ) = ∪ ( 𝑆 ↾t 𝑘 )
229 228 isopn2 ⊢ ( ( ( 𝑆 ↾t 𝑘 ) ∈ Top ∧ ( 𝑘 ∩ { 𝑣 ∈ ∪ 𝑆 ∣ ( 𝑠 × { 𝑣 } ) ⊆ 𝑥 } ) ⊆ ∪ ( 𝑆 ↾t 𝑘 ) ) → ( ( 𝑘 ∩ { 𝑣 ∈ ∪ 𝑆 ∣ ( 𝑠 × { 𝑣 } ) ⊆ 𝑥 } ) ∈ ( 𝑆 ↾t 𝑘 ) ↔ ( ∪ ( 𝑆 ↾t 𝑘 ) ∖ ( 𝑘 ∩ { 𝑣 ∈ ∪ 𝑆 ∣ ( 𝑠 × { 𝑣 } ) ⊆ 𝑥 } ) ) ∈ ( Clsd ‘ ( 𝑆 ↾t 𝑘 ) ) ) )
230 225 227 229 syl2anc ⊢ ( ( ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( ( 𝑠 ∈ 𝒫 { 𝑡 ∈ ∪ 𝑅 ∣ ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ ∈ 𝑥 } ∧ 𝑢 ∈ 𝑅 ) ∧ ( ( 1st ‘ 𝑦 ) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝑅 ↾t 𝑠 ) ∈ Comp ) ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ ( 𝑆 ↾t 𝑘 ) ∈ Comp ) ) → ( ( 𝑘 ∩ { 𝑣 ∈ ∪ 𝑆 ∣ ( 𝑠 × { 𝑣 } ) ⊆ 𝑥 } ) ∈ ( 𝑆 ↾t 𝑘 ) ↔ ( ∪ ( 𝑆 ↾t 𝑘 ) ∖ ( 𝑘 ∩ { 𝑣 ∈ ∪ 𝑆 ∣ ( 𝑠 × { 𝑣 } ) ⊆ 𝑥 } ) ) ∈ ( Clsd ‘ ( 𝑆 ↾t 𝑘 ) ) ) )
231 223 230 mpbird ⊢ ( ( ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( ( 𝑠 ∈ 𝒫 { 𝑡 ∈ ∪ 𝑅 ∣ ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ ∈ 𝑥 } ∧ 𝑢 ∈ 𝑅 ) ∧ ( ( 1st ‘ 𝑦 ) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝑅 ↾t 𝑠 ) ∈ Comp ) ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ ( 𝑆 ↾t 𝑘 ) ∈ Comp ) ) → ( 𝑘 ∩ { 𝑣 ∈ ∪ 𝑆 ∣ ( 𝑠 × { 𝑣 } ) ⊆ 𝑥 } ) ∈ ( 𝑆 ↾t 𝑘 ) )
232 69 231 eqeltrid ⊢ ( ( ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( ( 𝑠 ∈ 𝒫 { 𝑡 ∈ ∪ 𝑅 ∣ ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ ∈ 𝑥 } ∧ 𝑢 ∈ 𝑅 ) ∧ ( ( 1st ‘ 𝑦 ) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝑅 ↾t 𝑠 ) ∈ Comp ) ) ) ∧ ( 𝑘 ∈ 𝒫 ∪ 𝑆 ∧ ( 𝑆 ↾t 𝑘 ) ∈ Comp ) ) → ( { 𝑣 ∈ ∪ 𝑆 ∣ ( 𝑠 × { 𝑣 } ) ⊆ 𝑥 } ∩ 𝑘 ) ∈ ( 𝑆 ↾t 𝑘 ) )
233 232 expr ⊢ ( ( ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( ( 𝑠 ∈ 𝒫 { 𝑡 ∈ ∪ 𝑅 ∣ ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ ∈ 𝑥 } ∧ 𝑢 ∈ 𝑅 ) ∧ ( ( 1st ‘ 𝑦 ) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝑅 ↾t 𝑠 ) ∈ Comp ) ) ) ∧ 𝑘 ∈ 𝒫 ∪ 𝑆 ) → ( ( 𝑆 ↾t 𝑘 ) ∈ Comp → ( { 𝑣 ∈ ∪ 𝑆 ∣ ( 𝑠 × { 𝑣 } ) ⊆ 𝑥 } ∩ 𝑘 ) ∈ ( 𝑆 ↾t 𝑘 ) ) )
234 233 ralrimiva ⊢ ( ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( ( 𝑠 ∈ 𝒫 { 𝑡 ∈ ∪ 𝑅 ∣ ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ ∈ 𝑥 } ∧ 𝑢 ∈ 𝑅 ) ∧ ( ( 1st ‘ 𝑦 ) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝑅 ↾t 𝑠 ) ∈ Comp ) ) ) → ∀ 𝑘 ∈ 𝒫 ∪ 𝑆 ( ( 𝑆 ↾t 𝑘 ) ∈ Comp → ( { 𝑣 ∈ ∪ 𝑆 ∣ ( 𝑠 × { 𝑣 } ) ⊆ 𝑥 } ∩ 𝑘 ) ∈ ( 𝑆 ↾t 𝑘 ) ) )
235 65 17 sylib ⊢ ( ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( ( 𝑠 ∈ 𝒫 { 𝑡 ∈ ∪ 𝑅 ∣ ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ ∈ 𝑥 } ∧ 𝑢 ∈ 𝑅 ) ∧ ( ( 1st ‘ 𝑦 ) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝑅 ↾t 𝑠 ) ∈ Comp ) ) ) → 𝑆 ∈ ( TopOn ‘ ∪ 𝑆 ) )
236 elkgen ⊢ ( 𝑆 ∈ ( TopOn ‘ ∪ 𝑆 ) → ( { 𝑣 ∈ ∪ 𝑆 ∣ ( 𝑠 × { 𝑣 } ) ⊆ 𝑥 } ∈ ( 𝑘Gen ‘ 𝑆 ) ↔ ( { 𝑣 ∈ ∪ 𝑆 ∣ ( 𝑠 × { 𝑣 } ) ⊆ 𝑥 } ⊆ ∪ 𝑆 ∧ ∀ 𝑘 ∈ 𝒫 ∪ 𝑆 ( ( 𝑆 ↾t 𝑘 ) ∈ Comp → ( { 𝑣 ∈ ∪ 𝑆 ∣ ( 𝑠 × { 𝑣 } ) ⊆ 𝑥 } ∩ 𝑘 ) ∈ ( 𝑆 ↾t 𝑘 ) ) ) ) )
237 235 236 syl ⊢ ( ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( ( 𝑠 ∈ 𝒫 { 𝑡 ∈ ∪ 𝑅 ∣ ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ ∈ 𝑥 } ∧ 𝑢 ∈ 𝑅 ) ∧ ( ( 1st ‘ 𝑦 ) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝑅 ↾t 𝑠 ) ∈ Comp ) ) ) → ( { 𝑣 ∈ ∪ 𝑆 ∣ ( 𝑠 × { 𝑣 } ) ⊆ 𝑥 } ∈ ( 𝑘Gen ‘ 𝑆 ) ↔ ( { 𝑣 ∈ ∪ 𝑆 ∣ ( 𝑠 × { 𝑣 } ) ⊆ 𝑥 } ⊆ ∪ 𝑆 ∧ ∀ 𝑘 ∈ 𝒫 ∪ 𝑆 ( ( 𝑆 ↾t 𝑘 ) ∈ Comp → ( { 𝑣 ∈ ∪ 𝑆 ∣ ( 𝑠 × { 𝑣 } ) ⊆ 𝑥 } ∩ 𝑘 ) ∈ ( 𝑆 ↾t 𝑘 ) ) ) ) )
238 68 234 237 mpbir2and ⊢ ( ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( ( 𝑠 ∈ 𝒫 { 𝑡 ∈ ∪ 𝑅 ∣ ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ ∈ 𝑥 } ∧ 𝑢 ∈ 𝑅 ) ∧ ( ( 1st ‘ 𝑦 ) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝑅 ↾t 𝑠 ) ∈ Comp ) ) ) → { 𝑣 ∈ ∪ 𝑆 ∣ ( 𝑠 × { 𝑣 } ) ⊆ 𝑥 } ∈ ( 𝑘Gen ‘ 𝑆 ) )
239 15 adantr ⊢ ( ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( ( 𝑠 ∈ 𝒫 { 𝑡 ∈ ∪ 𝑅 ∣ ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ ∈ 𝑥 } ∧ 𝑢 ∈ 𝑅 ) ∧ ( ( 1st ‘ 𝑦 ) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝑅 ↾t 𝑠 ) ∈ Comp ) ) ) → 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) )
240 239 2 syl ⊢ ( ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( ( 𝑠 ∈ 𝒫 { 𝑡 ∈ ∪ 𝑅 ∣ ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ ∈ 𝑥 } ∧ 𝑢 ∈ 𝑅 ) ∧ ( ( 1st ‘ 𝑦 ) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝑅 ↾t 𝑠 ) ∈ Comp ) ) ) → 𝑆 ∈ ran 𝑘Gen )
241 kgenidm ⊢ ( 𝑆 ∈ ran 𝑘Gen → ( 𝑘Gen ‘ 𝑆 ) = 𝑆 )
242 240 241 syl ⊢ ( ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( ( 𝑠 ∈ 𝒫 { 𝑡 ∈ ∪ 𝑅 ∣ ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ ∈ 𝑥 } ∧ 𝑢 ∈ 𝑅 ) ∧ ( ( 1st ‘ 𝑦 ) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝑅 ↾t 𝑠 ) ∈ Comp ) ) ) → ( 𝑘Gen ‘ 𝑆 ) = 𝑆 )
243 238 242 eleqtrd ⊢ ( ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( ( 𝑠 ∈ 𝒫 { 𝑡 ∈ ∪ 𝑅 ∣ ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ ∈ 𝑥 } ∧ 𝑢 ∈ 𝑅 ) ∧ ( ( 1st ‘ 𝑦 ) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝑅 ↾t 𝑠 ) ∈ Comp ) ) ) → { 𝑣 ∈ ∪ 𝑆 ∣ ( 𝑠 × { 𝑣 } ) ⊆ 𝑥 } ∈ 𝑆 )
244 txopn ⊢ ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) ∧ ( 𝑢 ∈ 𝑅 ∧ { 𝑣 ∈ ∪ 𝑆 ∣ ( 𝑠 × { 𝑣 } ) ⊆ 𝑥 } ∈ 𝑆 ) ) → ( 𝑢 × { 𝑣 ∈ ∪ 𝑆 ∣ ( 𝑠 × { 𝑣 } ) ⊆ 𝑥 } ) ∈ ( 𝑅 ×t 𝑆 ) )
245 64 65 66 243 244 syl22anc ⊢ ( ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( ( 𝑠 ∈ 𝒫 { 𝑡 ∈ ∪ 𝑅 ∣ ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ ∈ 𝑥 } ∧ 𝑢 ∈ 𝑅 ) ∧ ( ( 1st ‘ 𝑦 ) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝑅 ↾t 𝑠 ) ∈ Comp ) ) ) → ( 𝑢 × { 𝑣 ∈ ∪ 𝑆 ∣ ( 𝑠 × { 𝑣 } ) ⊆ 𝑥 } ) ∈ ( 𝑅 ×t 𝑆 ) )
246 59 adantr ⊢ ( ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( ( 𝑠 ∈ 𝒫 { 𝑡 ∈ ∪ 𝑅 ∣ ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ ∈ 𝑥 } ∧ 𝑢 ∈ 𝑅 ) ∧ ( ( 1st ‘ 𝑦 ) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝑅 ↾t 𝑠 ) ∈ Comp ) ) ) → 𝑦 = ⟨ ( 1st ‘ 𝑦 ) , ( 2nd ‘ 𝑦 ) ⟩ )
247 simprr1 ⊢ ( ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( ( 𝑠 ∈ 𝒫 { 𝑡 ∈ ∪ 𝑅 ∣ ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ ∈ 𝑥 } ∧ 𝑢 ∈ 𝑅 ) ∧ ( ( 1st ‘ 𝑦 ) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝑅 ↾t 𝑠 ) ∈ Comp ) ) ) → ( 1st ‘ 𝑦 ) ∈ 𝑢 )
248 sneq ⊢ ( 𝑣 = ( 2nd ‘ 𝑦 ) → { 𝑣 } = { ( 2nd ‘ 𝑦 ) } )
249 248 xpeq2d ⊢ ( 𝑣 = ( 2nd ‘ 𝑦 ) → ( 𝑠 × { 𝑣 } ) = ( 𝑠 × { ( 2nd ‘ 𝑦 ) } ) )
250 249 sseq1d ⊢ ( 𝑣 = ( 2nd ‘ 𝑦 ) → ( ( 𝑠 × { 𝑣 } ) ⊆ 𝑥 ↔ ( 𝑠 × { ( 2nd ‘ 𝑦 ) } ) ⊆ 𝑥 ) )
251 34 adantr ⊢ ( ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( ( 𝑠 ∈ 𝒫 { 𝑡 ∈ ∪ 𝑅 ∣ ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ ∈ 𝑥 } ∧ 𝑢 ∈ 𝑅 ) ∧ ( ( 1st ‘ 𝑦 ) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝑅 ↾t 𝑠 ) ∈ Comp ) ) ) → ( 2nd ‘ 𝑦 ) ∈ ∪ 𝑆 )
252 relxp ⊢ Rel ( 𝑠 × { ( 2nd ‘ 𝑦 ) } )
253 252 a1i ⊢ ( ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( ( 𝑠 ∈ 𝒫 { 𝑡 ∈ ∪ 𝑅 ∣ ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ ∈ 𝑥 } ∧ 𝑢 ∈ 𝑅 ) ∧ ( ( 1st ‘ 𝑦 ) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝑅 ↾t 𝑠 ) ∈ Comp ) ) ) → Rel ( 𝑠 × { ( 2nd ‘ 𝑦 ) } ) )
254 opelxp ⊢ ( ⟨ 𝑎 , 𝑏 ⟩ ∈ ( 𝑠 × { ( 2nd ‘ 𝑦 ) } ) ↔ ( 𝑎 ∈ 𝑠 ∧ 𝑏 ∈ { ( 2nd ‘ 𝑦 ) } ) )
255 71 sselda ⊢ ( ( ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( ( 𝑠 ∈ 𝒫 { 𝑡 ∈ ∪ 𝑅 ∣ ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ ∈ 𝑥 } ∧ 𝑢 ∈ 𝑅 ) ∧ ( ( 1st ‘ 𝑦 ) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝑅 ↾t 𝑠 ) ∈ Comp ) ) ) ∧ 𝑎 ∈ 𝑠 ) → 𝑎 ∈ { 𝑡 ∈ ∪ 𝑅 ∣ ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ ∈ 𝑥 } )
256 opeq1 ⊢ ( 𝑡 = 𝑎 → ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ = ⟨ 𝑎 , ( 2nd ‘ 𝑦 ) ⟩ )
257 256 eleq1d ⊢ ( 𝑡 = 𝑎 → ( ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ ∈ 𝑥 ↔ ⟨ 𝑎 , ( 2nd ‘ 𝑦 ) ⟩ ∈ 𝑥 ) )
258 257 elrab ⊢ ( 𝑎 ∈ { 𝑡 ∈ ∪ 𝑅 ∣ ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ ∈ 𝑥 } ↔ ( 𝑎 ∈ ∪ 𝑅 ∧ ⟨ 𝑎 , ( 2nd ‘ 𝑦 ) ⟩ ∈ 𝑥 ) )
259 258 simprbi ⊢ ( 𝑎 ∈ { 𝑡 ∈ ∪ 𝑅 ∣ ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ ∈ 𝑥 } → ⟨ 𝑎 , ( 2nd ‘ 𝑦 ) ⟩ ∈ 𝑥 )
260 255 259 syl ⊢ ( ( ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( ( 𝑠 ∈ 𝒫 { 𝑡 ∈ ∪ 𝑅 ∣ ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ ∈ 𝑥 } ∧ 𝑢 ∈ 𝑅 ) ∧ ( ( 1st ‘ 𝑦 ) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝑅 ↾t 𝑠 ) ∈ Comp ) ) ) ∧ 𝑎 ∈ 𝑠 ) → ⟨ 𝑎 , ( 2nd ‘ 𝑦 ) ⟩ ∈ 𝑥 )
261 elsni ⊢ ( 𝑏 ∈ { ( 2nd ‘ 𝑦 ) } → 𝑏 = ( 2nd ‘ 𝑦 ) )
262 261 opeq2d ⊢ ( 𝑏 ∈ { ( 2nd ‘ 𝑦 ) } → ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝑎 , ( 2nd ‘ 𝑦 ) ⟩ )
263 262 eleq1d ⊢ ( 𝑏 ∈ { ( 2nd ‘ 𝑦 ) } → ( ⟨ 𝑎 , 𝑏 ⟩ ∈ 𝑥 ↔ ⟨ 𝑎 , ( 2nd ‘ 𝑦 ) ⟩ ∈ 𝑥 ) )
264 260 263 syl5ibrcom ⊢ ( ( ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( ( 𝑠 ∈ 𝒫 { 𝑡 ∈ ∪ 𝑅 ∣ ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ ∈ 𝑥 } ∧ 𝑢 ∈ 𝑅 ) ∧ ( ( 1st ‘ 𝑦 ) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝑅 ↾t 𝑠 ) ∈ Comp ) ) ) ∧ 𝑎 ∈ 𝑠 ) → ( 𝑏 ∈ { ( 2nd ‘ 𝑦 ) } → ⟨ 𝑎 , 𝑏 ⟩ ∈ 𝑥 ) )
265 264 expimpd ⊢ ( ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( ( 𝑠 ∈ 𝒫 { 𝑡 ∈ ∪ 𝑅 ∣ ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ ∈ 𝑥 } ∧ 𝑢 ∈ 𝑅 ) ∧ ( ( 1st ‘ 𝑦 ) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝑅 ↾t 𝑠 ) ∈ Comp ) ) ) → ( ( 𝑎 ∈ 𝑠 ∧ 𝑏 ∈ { ( 2nd ‘ 𝑦 ) } ) → ⟨ 𝑎 , 𝑏 ⟩ ∈ 𝑥 ) )
266 254 265 syl5bi ⊢ ( ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( ( 𝑠 ∈ 𝒫 { 𝑡 ∈ ∪ 𝑅 ∣ ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ ∈ 𝑥 } ∧ 𝑢 ∈ 𝑅 ) ∧ ( ( 1st ‘ 𝑦 ) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝑅 ↾t 𝑠 ) ∈ Comp ) ) ) → ( ⟨ 𝑎 , 𝑏 ⟩ ∈ ( 𝑠 × { ( 2nd ‘ 𝑦 ) } ) → ⟨ 𝑎 , 𝑏 ⟩ ∈ 𝑥 ) )
267 253 266 relssdv ⊢ ( ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( ( 𝑠 ∈ 𝒫 { 𝑡 ∈ ∪ 𝑅 ∣ ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ ∈ 𝑥 } ∧ 𝑢 ∈ 𝑅 ) ∧ ( ( 1st ‘ 𝑦 ) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝑅 ↾t 𝑠 ) ∈ Comp ) ) ) → ( 𝑠 × { ( 2nd ‘ 𝑦 ) } ) ⊆ 𝑥 )
268 250 251 267 elrabd ⊢ ( ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( ( 𝑠 ∈ 𝒫 { 𝑡 ∈ ∪ 𝑅 ∣ ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ ∈ 𝑥 } ∧ 𝑢 ∈ 𝑅 ) ∧ ( ( 1st ‘ 𝑦 ) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝑅 ↾t 𝑠 ) ∈ Comp ) ) ) → ( 2nd ‘ 𝑦 ) ∈ { 𝑣 ∈ ∪ 𝑆 ∣ ( 𝑠 × { 𝑣 } ) ⊆ 𝑥 } )
269 247 268 opelxpd ⊢ ( ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( ( 𝑠 ∈ 𝒫 { 𝑡 ∈ ∪ 𝑅 ∣ ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ ∈ 𝑥 } ∧ 𝑢 ∈ 𝑅 ) ∧ ( ( 1st ‘ 𝑦 ) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝑅 ↾t 𝑠 ) ∈ Comp ) ) ) → ⟨ ( 1st ‘ 𝑦 ) , ( 2nd ‘ 𝑦 ) ⟩ ∈ ( 𝑢 × { 𝑣 ∈ ∪ 𝑆 ∣ ( 𝑠 × { 𝑣 } ) ⊆ 𝑥 } ) )
270 246 269 eqeltrd ⊢ ( ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( ( 𝑠 ∈ 𝒫 { 𝑡 ∈ ∪ 𝑅 ∣ ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ ∈ 𝑥 } ∧ 𝑢 ∈ 𝑅 ) ∧ ( ( 1st ‘ 𝑦 ) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝑅 ↾t 𝑠 ) ∈ Comp ) ) ) → 𝑦 ∈ ( 𝑢 × { 𝑣 ∈ ∪ 𝑆 ∣ ( 𝑠 × { 𝑣 } ) ⊆ 𝑥 } ) )
271 relxp ⊢ Rel ( 𝑢 × { 𝑣 ∈ ∪ 𝑆 ∣ ( 𝑠 × { 𝑣 } ) ⊆ 𝑥 } )
272 271 a1i ⊢ ( ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( ( 𝑠 ∈ 𝒫 { 𝑡 ∈ ∪ 𝑅 ∣ ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ ∈ 𝑥 } ∧ 𝑢 ∈ 𝑅 ) ∧ ( ( 1st ‘ 𝑦 ) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝑅 ↾t 𝑠 ) ∈ Comp ) ) ) → Rel ( 𝑢 × { 𝑣 ∈ ∪ 𝑆 ∣ ( 𝑠 × { 𝑣 } ) ⊆ 𝑥 } ) )
273 opelxp ⊢ ( ⟨ 𝑎 , 𝑏 ⟩ ∈ ( 𝑢 × { 𝑣 ∈ ∪ 𝑆 ∣ ( 𝑠 × { 𝑣 } ) ⊆ 𝑥 } ) ↔ ( 𝑎 ∈ 𝑢 ∧ 𝑏 ∈ { 𝑣 ∈ ∪ 𝑆 ∣ ( 𝑠 × { 𝑣 } ) ⊆ 𝑥 } ) )
274 126 elrab ⊢ ( 𝑏 ∈ { 𝑣 ∈ ∪ 𝑆 ∣ ( 𝑠 × { 𝑣 } ) ⊆ 𝑥 } ↔ ( 𝑏 ∈ ∪ 𝑆 ∧ ( 𝑠 × { 𝑏 } ) ⊆ 𝑥 ) )
275 274 simprbi ⊢ ( 𝑏 ∈ { 𝑣 ∈ ∪ 𝑆 ∣ ( 𝑠 × { 𝑣 } ) ⊆ 𝑥 } → ( 𝑠 × { 𝑏 } ) ⊆ 𝑥 )
276 simprr2 ⊢ ( ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( ( 𝑠 ∈ 𝒫 { 𝑡 ∈ ∪ 𝑅 ∣ ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ ∈ 𝑥 } ∧ 𝑢 ∈ 𝑅 ) ∧ ( ( 1st ‘ 𝑦 ) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝑅 ↾t 𝑠 ) ∈ Comp ) ) ) → 𝑢 ⊆ 𝑠 )
277 276 sselda ⊢ ( ( ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( ( 𝑠 ∈ 𝒫 { 𝑡 ∈ ∪ 𝑅 ∣ ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ ∈ 𝑥 } ∧ 𝑢 ∈ 𝑅 ) ∧ ( ( 1st ‘ 𝑦 ) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝑅 ↾t 𝑠 ) ∈ Comp ) ) ) ∧ 𝑎 ∈ 𝑢 ) → 𝑎 ∈ 𝑠 )
278 vsnid ⊢ 𝑏 ∈ { 𝑏 }
279 opelxpi ⊢ ( ( 𝑎 ∈ 𝑠 ∧ 𝑏 ∈ { 𝑏 } ) → ⟨ 𝑎 , 𝑏 ⟩ ∈ ( 𝑠 × { 𝑏 } ) )
280 277 278 279 sylancl ⊢ ( ( ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( ( 𝑠 ∈ 𝒫 { 𝑡 ∈ ∪ 𝑅 ∣ ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ ∈ 𝑥 } ∧ 𝑢 ∈ 𝑅 ) ∧ ( ( 1st ‘ 𝑦 ) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝑅 ↾t 𝑠 ) ∈ Comp ) ) ) ∧ 𝑎 ∈ 𝑢 ) → ⟨ 𝑎 , 𝑏 ⟩ ∈ ( 𝑠 × { 𝑏 } ) )
281 ssel ⊢ ( ( 𝑠 × { 𝑏 } ) ⊆ 𝑥 → ( ⟨ 𝑎 , 𝑏 ⟩ ∈ ( 𝑠 × { 𝑏 } ) → ⟨ 𝑎 , 𝑏 ⟩ ∈ 𝑥 ) )
282 275 280 281 syl2imc ⊢ ( ( ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( ( 𝑠 ∈ 𝒫 { 𝑡 ∈ ∪ 𝑅 ∣ ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ ∈ 𝑥 } ∧ 𝑢 ∈ 𝑅 ) ∧ ( ( 1st ‘ 𝑦 ) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝑅 ↾t 𝑠 ) ∈ Comp ) ) ) ∧ 𝑎 ∈ 𝑢 ) → ( 𝑏 ∈ { 𝑣 ∈ ∪ 𝑆 ∣ ( 𝑠 × { 𝑣 } ) ⊆ 𝑥 } → ⟨ 𝑎 , 𝑏 ⟩ ∈ 𝑥 ) )
283 282 expimpd ⊢ ( ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( ( 𝑠 ∈ 𝒫 { 𝑡 ∈ ∪ 𝑅 ∣ ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ ∈ 𝑥 } ∧ 𝑢 ∈ 𝑅 ) ∧ ( ( 1st ‘ 𝑦 ) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝑅 ↾t 𝑠 ) ∈ Comp ) ) ) → ( ( 𝑎 ∈ 𝑢 ∧ 𝑏 ∈ { 𝑣 ∈ ∪ 𝑆 ∣ ( 𝑠 × { 𝑣 } ) ⊆ 𝑥 } ) → ⟨ 𝑎 , 𝑏 ⟩ ∈ 𝑥 ) )
284 273 283 syl5bi ⊢ ( ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( ( 𝑠 ∈ 𝒫 { 𝑡 ∈ ∪ 𝑅 ∣ ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ ∈ 𝑥 } ∧ 𝑢 ∈ 𝑅 ) ∧ ( ( 1st ‘ 𝑦 ) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝑅 ↾t 𝑠 ) ∈ Comp ) ) ) → ( ⟨ 𝑎 , 𝑏 ⟩ ∈ ( 𝑢 × { 𝑣 ∈ ∪ 𝑆 ∣ ( 𝑠 × { 𝑣 } ) ⊆ 𝑥 } ) → ⟨ 𝑎 , 𝑏 ⟩ ∈ 𝑥 ) )
285 272 284 relssdv ⊢ ( ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( ( 𝑠 ∈ 𝒫 { 𝑡 ∈ ∪ 𝑅 ∣ ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ ∈ 𝑥 } ∧ 𝑢 ∈ 𝑅 ) ∧ ( ( 1st ‘ 𝑦 ) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝑅 ↾t 𝑠 ) ∈ Comp ) ) ) → ( 𝑢 × { 𝑣 ∈ ∪ 𝑆 ∣ ( 𝑠 × { 𝑣 } ) ⊆ 𝑥 } ) ⊆ 𝑥 )
286 eleq2 ⊢ ( 𝑡 = ( 𝑢 × { 𝑣 ∈ ∪ 𝑆 ∣ ( 𝑠 × { 𝑣 } ) ⊆ 𝑥 } ) → ( 𝑦 ∈ 𝑡 ↔ 𝑦 ∈ ( 𝑢 × { 𝑣 ∈ ∪ 𝑆 ∣ ( 𝑠 × { 𝑣 } ) ⊆ 𝑥 } ) ) )
287 sseq1 ⊢ ( 𝑡 = ( 𝑢 × { 𝑣 ∈ ∪ 𝑆 ∣ ( 𝑠 × { 𝑣 } ) ⊆ 𝑥 } ) → ( 𝑡 ⊆ 𝑥 ↔ ( 𝑢 × { 𝑣 ∈ ∪ 𝑆 ∣ ( 𝑠 × { 𝑣 } ) ⊆ 𝑥 } ) ⊆ 𝑥 ) )
288 286 287 anbi12d ⊢ ( 𝑡 = ( 𝑢 × { 𝑣 ∈ ∪ 𝑆 ∣ ( 𝑠 × { 𝑣 } ) ⊆ 𝑥 } ) → ( ( 𝑦 ∈ 𝑡 ∧ 𝑡 ⊆ 𝑥 ) ↔ ( 𝑦 ∈ ( 𝑢 × { 𝑣 ∈ ∪ 𝑆 ∣ ( 𝑠 × { 𝑣 } ) ⊆ 𝑥 } ) ∧ ( 𝑢 × { 𝑣 ∈ ∪ 𝑆 ∣ ( 𝑠 × { 𝑣 } ) ⊆ 𝑥 } ) ⊆ 𝑥 ) ) )
289 288 rspcev ⊢ ( ( ( 𝑢 × { 𝑣 ∈ ∪ 𝑆 ∣ ( 𝑠 × { 𝑣 } ) ⊆ 𝑥 } ) ∈ ( 𝑅 ×t 𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × { 𝑣 ∈ ∪ 𝑆 ∣ ( 𝑠 × { 𝑣 } ) ⊆ 𝑥 } ) ∧ ( 𝑢 × { 𝑣 ∈ ∪ 𝑆 ∣ ( 𝑠 × { 𝑣 } ) ⊆ 𝑥 } ) ⊆ 𝑥 ) ) → ∃ 𝑡 ∈ ( 𝑅 ×t 𝑆 ) ( 𝑦 ∈ 𝑡 ∧ 𝑡 ⊆ 𝑥 ) )
290 245 270 285 289 syl12anc ⊢ ( ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( ( 𝑠 ∈ 𝒫 { 𝑡 ∈ ∪ 𝑅 ∣ ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ ∈ 𝑥 } ∧ 𝑢 ∈ 𝑅 ) ∧ ( ( 1st ‘ 𝑦 ) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝑅 ↾t 𝑠 ) ∈ Comp ) ) ) → ∃ 𝑡 ∈ ( 𝑅 ×t 𝑆 ) ( 𝑦 ∈ 𝑡 ∧ 𝑡 ⊆ 𝑥 ) )
291 290 expr ⊢ ( ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑠 ∈ 𝒫 { 𝑡 ∈ ∪ 𝑅 ∣ ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ ∈ 𝑥 } ∧ 𝑢 ∈ 𝑅 ) ) → ( ( ( 1st ‘ 𝑦 ) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝑅 ↾t 𝑠 ) ∈ Comp ) → ∃ 𝑡 ∈ ( 𝑅 ×t 𝑆 ) ( 𝑦 ∈ 𝑡 ∧ 𝑡 ⊆ 𝑥 ) ) )
292 291 rexlimdvva ⊢ ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) → ( ∃ 𝑠 ∈ 𝒫 { 𝑡 ∈ ∪ 𝑅 ∣ ⟨ 𝑡 , ( 2nd ‘ 𝑦 ) ⟩ ∈ 𝑥 } ∃ 𝑢 ∈ 𝑅 ( ( 1st ‘ 𝑦 ) ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝑅 ↾t 𝑠 ) ∈ Comp ) → ∃ 𝑡 ∈ ( 𝑅 ×t 𝑆 ) ( 𝑦 ∈ 𝑡 ∧ 𝑡 ⊆ 𝑥 ) ) )
293 63 292 mpd ⊢ ( ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) ∧ 𝑦 ∈ 𝑥 ) → ∃ 𝑡 ∈ ( 𝑅 ×t 𝑆 ) ( 𝑦 ∈ 𝑡 ∧ 𝑡 ⊆ 𝑥 ) )
294 293 ralrimiva ⊢ ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) → ∀ 𝑦 ∈ 𝑥 ∃ 𝑡 ∈ ( 𝑅 ×t 𝑆 ) ( 𝑦 ∈ 𝑡 ∧ 𝑡 ⊆ 𝑥 ) )
295 6 adantr ⊢ ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) → ( 𝑅 ×t 𝑆 ) ∈ Top )
296 eltop2 ⊢ ( ( 𝑅 ×t 𝑆 ) ∈ Top → ( 𝑥 ∈ ( 𝑅 ×t 𝑆 ) ↔ ∀ 𝑦 ∈ 𝑥 ∃ 𝑡 ∈ ( 𝑅 ×t 𝑆 ) ( 𝑦 ∈ 𝑡 ∧ 𝑡 ⊆ 𝑥 ) ) )
297 295 296 syl ⊢ ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) → ( 𝑥 ∈ ( 𝑅 ×t 𝑆 ) ↔ ∀ 𝑦 ∈ 𝑥 ∃ 𝑡 ∈ ( 𝑅 ×t 𝑆 ) ( 𝑦 ∈ 𝑡 ∧ 𝑡 ⊆ 𝑥 ) ) )
298 294 297 mpbird ⊢ ( ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) ∧ 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ) → 𝑥 ∈ ( 𝑅 ×t 𝑆 ) )
299 298 ex ⊢ ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) → ( 𝑥 ∈ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) → 𝑥 ∈ ( 𝑅 ×t 𝑆 ) ) )
300 299 ssrdv ⊢ ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) → ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ⊆ ( 𝑅 ×t 𝑆 ) )
301 iskgen2 ⊢ ( ( 𝑅 ×t 𝑆 ) ∈ ran 𝑘Gen ↔ ( ( 𝑅 ×t 𝑆 ) ∈ Top ∧ ( 𝑘Gen ‘ ( 𝑅 ×t 𝑆 ) ) ⊆ ( 𝑅 ×t 𝑆 ) ) )
302 6 300 301 sylanbrc ⊢ ( ( 𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ ( ran 𝑘Gen ∩ Haus ) ) → ( 𝑅 ×t 𝑆 ) ∈ ran 𝑘Gen )