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 )