MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  txkgen Structured version   Visualization version   GIF version

Theorem txkgen 22260
Description: The topological product of a locally compact space and a compactly generated Hausdorff space is compactly generated. (The condition on 𝑆 can also be replaced with either "compactly generated weak Hausdorff (CGWH)" or "compact Hausdorff-ly generated (CHG)", where WH means that all images of compact Hausdorff spaces are closed and CHG means that a set is open iff it is open in all compact Hausdorff spaces.) (Contributed by Mario Carneiro, 23-Mar-2015.)
Assertion
Ref Expression
txkgen ((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) → (𝑅 ×t 𝑆) ∈ ran 𝑘Gen)

Proof of Theorem txkgen
Dummy variables 𝑎 𝑏 𝑘 𝑠 𝑡 𝑢 𝑥 𝑦 𝑣 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nllytop 22081 . . 3 (𝑅 ∈ 𝑛-Locally Comp → 𝑅 ∈ Top)
2 elinel1 4125 . . . 4 (𝑆 ∈ (ran 𝑘Gen ∩ Haus) → 𝑆 ∈ ran 𝑘Gen)
3 kgentop 22150 . . . 4 (𝑆 ∈ ran 𝑘Gen → 𝑆 ∈ Top)
42, 3syl 17 . . 3 (𝑆 ∈ (ran 𝑘Gen ∩ Haus) → 𝑆 ∈ Top)
5 txtop 22177 . . 3 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑅 ×t 𝑆) ∈ Top)
61, 4, 5syl2an 598 . 2 ((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) → (𝑅 ×t 𝑆) ∈ Top)
7 simplll 774 . . . . . . . 8 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → 𝑅 ∈ 𝑛-Locally Comp)
8 eqid 2801 . . . . . . . . . 10 (𝑡 𝑅 ↦ ⟨𝑡, (2nd𝑦)⟩) = (𝑡 𝑅 ↦ ⟨𝑡, (2nd𝑦)⟩)
98mptpreima 6063 . . . . . . . . 9 ((𝑡 𝑅 ↦ ⟨𝑡, (2nd𝑦)⟩) “ 𝑥) = {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥}
101ad3antrrr 729 . . . . . . . . . . . . . 14 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → 𝑅 ∈ Top)
11 toptopon2 21526 . . . . . . . . . . . . . 14 (𝑅 ∈ Top ↔ 𝑅 ∈ (TopOn‘ 𝑅))
1210, 11sylib 221 . . . . . . . . . . . . 13 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → 𝑅 ∈ (TopOn‘ 𝑅))
13 idcn 21865 . . . . . . . . . . . . 13 (𝑅 ∈ (TopOn‘ 𝑅) → ( I ↾ 𝑅) ∈ (𝑅 Cn 𝑅))
1412, 13syl 17 . . . . . . . . . . . 12 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → ( I ↾ 𝑅) ∈ (𝑅 Cn 𝑅))
15 simpllr 775 . . . . . . . . . . . . . . 15 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → 𝑆 ∈ (ran 𝑘Gen ∩ Haus))
1615, 4syl 17 . . . . . . . . . . . . . 14 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → 𝑆 ∈ Top)
17 toptopon2 21526 . . . . . . . . . . . . . 14 (𝑆 ∈ Top ↔ 𝑆 ∈ (TopOn‘ 𝑆))
1816, 17sylib 221 . . . . . . . . . . . . 13 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → 𝑆 ∈ (TopOn‘ 𝑆))
19 simpr 488 . . . . . . . . . . . . . . . 16 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → 𝑦𝑥)
20 simplr 768 . . . . . . . . . . . . . . . 16 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆)))
21 elunii 4808 . . . . . . . . . . . . . . . 16 ((𝑦𝑥𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) → 𝑦 (𝑘Gen‘(𝑅 ×t 𝑆)))
2219, 20, 21syl2anc 587 . . . . . . . . . . . . . . 15 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → 𝑦 (𝑘Gen‘(𝑅 ×t 𝑆)))
23 eqid 2801 . . . . . . . . . . . . . . . . . 18 𝑅 = 𝑅
24 eqid 2801 . . . . . . . . . . . . . . . . . 18 𝑆 = 𝑆
2523, 24txuni 22200 . . . . . . . . . . . . . . . . 17 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → ( 𝑅 × 𝑆) = (𝑅 ×t 𝑆))
2610, 16, 25syl2anc 587 . . . . . . . . . . . . . . . 16 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → ( 𝑅 × 𝑆) = (𝑅 ×t 𝑆))
2710, 16, 5syl2anc 587 . . . . . . . . . . . . . . . . 17 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → (𝑅 ×t 𝑆) ∈ Top)
28 eqid 2801 . . . . . . . . . . . . . . . . . 18 (𝑅 ×t 𝑆) = (𝑅 ×t 𝑆)
2928kgenuni 22147 . . . . . . . . . . . . . . . . 17 ((𝑅 ×t 𝑆) ∈ Top → (𝑅 ×t 𝑆) = (𝑘Gen‘(𝑅 ×t 𝑆)))
3027, 29syl 17 . . . . . . . . . . . . . . . 16 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → (𝑅 ×t 𝑆) = (𝑘Gen‘(𝑅 ×t 𝑆)))
3126, 30eqtrd 2836 . . . . . . . . . . . . . . 15 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → ( 𝑅 × 𝑆) = (𝑘Gen‘(𝑅 ×t 𝑆)))
3222, 31eleqtrrd 2896 . . . . . . . . . . . . . 14 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → 𝑦 ∈ ( 𝑅 × 𝑆))
33 xp2nd 7708 . . . . . . . . . . . . . 14 (𝑦 ∈ ( 𝑅 × 𝑆) → (2nd𝑦) ∈ 𝑆)
3432, 33syl 17 . . . . . . . . . . . . 13 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → (2nd𝑦) ∈ 𝑆)
35 cnconst2 21891 . . . . . . . . . . . . 13 ((𝑅 ∈ (TopOn‘ 𝑅) ∧ 𝑆 ∈ (TopOn‘ 𝑆) ∧ (2nd𝑦) ∈ 𝑆) → ( 𝑅 × {(2nd𝑦)}) ∈ (𝑅 Cn 𝑆))
3612, 18, 34, 35syl3anc 1368 . . . . . . . . . . . 12 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → ( 𝑅 × {(2nd𝑦)}) ∈ (𝑅 Cn 𝑆))
37 fvresi 6916 . . . . . . . . . . . . . . . 16 (𝑡 𝑅 → (( I ↾ 𝑅)‘𝑡) = 𝑡)
38 fvex 6662 . . . . . . . . . . . . . . . . 17 (2nd𝑦) ∈ V
3938fvconst2 6947 . . . . . . . . . . . . . . . 16 (𝑡 𝑅 → (( 𝑅 × {(2nd𝑦)})‘𝑡) = (2nd𝑦))
4037, 39opeq12d 4776 . . . . . . . . . . . . . . 15 (𝑡 𝑅 → ⟨(( I ↾ 𝑅)‘𝑡), (( 𝑅 × {(2nd𝑦)})‘𝑡)⟩ = ⟨𝑡, (2nd𝑦)⟩)
4140mpteq2ia 5124 . . . . . . . . . . . . . 14 (𝑡 𝑅 ↦ ⟨(( I ↾ 𝑅)‘𝑡), (( 𝑅 × {(2nd𝑦)})‘𝑡)⟩) = (𝑡 𝑅 ↦ ⟨𝑡, (2nd𝑦)⟩)
4241eqcomi 2810 . . . . . . . . . . . . 13 (𝑡 𝑅 ↦ ⟨𝑡, (2nd𝑦)⟩) = (𝑡 𝑅 ↦ ⟨(( I ↾ 𝑅)‘𝑡), (( 𝑅 × {(2nd𝑦)})‘𝑡)⟩)
4323, 42txcnmpt 22232 . . . . . . . . . . . 12 ((( I ↾ 𝑅) ∈ (𝑅 Cn 𝑅) ∧ ( 𝑅 × {(2nd𝑦)}) ∈ (𝑅 Cn 𝑆)) → (𝑡 𝑅 ↦ ⟨𝑡, (2nd𝑦)⟩) ∈ (𝑅 Cn (𝑅 ×t 𝑆)))
4414, 36, 43syl2anc 587 . . . . . . . . . . 11 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → (𝑡 𝑅 ↦ ⟨𝑡, (2nd𝑦)⟩) ∈ (𝑅 Cn (𝑅 ×t 𝑆)))
45 llycmpkgen 22160 . . . . . . . . . . . . 13 (𝑅 ∈ 𝑛-Locally Comp → 𝑅 ∈ ran 𝑘Gen)
4645ad3antrrr 729 . . . . . . . . . . . 12 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → 𝑅 ∈ ran 𝑘Gen)
476ad2antrr 725 . . . . . . . . . . . 12 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → (𝑅 ×t 𝑆) ∈ Top)
48 kgencn3 22166 . . . . . . . . . . . 12 ((𝑅 ∈ ran 𝑘Gen ∧ (𝑅 ×t 𝑆) ∈ Top) → (𝑅 Cn (𝑅 ×t 𝑆)) = (𝑅 Cn (𝑘Gen‘(𝑅 ×t 𝑆))))
4946, 47, 48syl2anc 587 . . . . . . . . . . 11 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → (𝑅 Cn (𝑅 ×t 𝑆)) = (𝑅 Cn (𝑘Gen‘(𝑅 ×t 𝑆))))
5044, 49eleqtrd 2895 . . . . . . . . . 10 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → (𝑡 𝑅 ↦ ⟨𝑡, (2nd𝑦)⟩) ∈ (𝑅 Cn (𝑘Gen‘(𝑅 ×t 𝑆))))
51 cnima 21873 . . . . . . . . . 10 (((𝑡 𝑅 ↦ ⟨𝑡, (2nd𝑦)⟩) ∈ (𝑅 Cn (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) → ((𝑡 𝑅 ↦ ⟨𝑡, (2nd𝑦)⟩) “ 𝑥) ∈ 𝑅)
5250, 20, 51syl2anc 587 . . . . . . . . 9 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → ((𝑡 𝑅 ↦ ⟨𝑡, (2nd𝑦)⟩) “ 𝑥) ∈ 𝑅)
539, 52eqeltrrid 2898 . . . . . . . 8 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∈ 𝑅)
54 opeq1 4766 . . . . . . . . . 10 (𝑡 = (1st𝑦) → ⟨𝑡, (2nd𝑦)⟩ = ⟨(1st𝑦), (2nd𝑦)⟩)
5554eleq1d 2877 . . . . . . . . 9 (𝑡 = (1st𝑦) → (⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥 ↔ ⟨(1st𝑦), (2nd𝑦)⟩ ∈ 𝑥))
56 xp1st 7707 . . . . . . . . . 10 (𝑦 ∈ ( 𝑅 × 𝑆) → (1st𝑦) ∈ 𝑅)
5732, 56syl 17 . . . . . . . . 9 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → (1st𝑦) ∈ 𝑅)
58 1st2nd2 7714 . . . . . . . . . . 11 (𝑦 ∈ ( 𝑅 × 𝑆) → 𝑦 = ⟨(1st𝑦), (2nd𝑦)⟩)
5932, 58syl 17 . . . . . . . . . 10 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → 𝑦 = ⟨(1st𝑦), (2nd𝑦)⟩)
6059, 19eqeltrrd 2894 . . . . . . . . 9 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → ⟨(1st𝑦), (2nd𝑦)⟩ ∈ 𝑥)
6155, 57, 60elrabd 3633 . . . . . . . 8 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → (1st𝑦) ∈ {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥})
62 nlly2i 22084 . . . . . . . 8 ((𝑅 ∈ 𝑛-Locally Comp ∧ {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∈ 𝑅 ∧ (1st𝑦) ∈ {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥}) → ∃𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥}∃𝑢𝑅 ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))
637, 53, 61, 62syl3anc 1368 . . . . . . 7 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → ∃𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥}∃𝑢𝑅 ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))
6410adantr 484 . . . . . . . . . . 11 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → 𝑅 ∈ Top)
6516adantr 484 . . . . . . . . . . 11 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → 𝑆 ∈ Top)
66 simprlr 779 . . . . . . . . . . 11 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → 𝑢𝑅)
67 ssrab2 4010 . . . . . . . . . . . . . 14 {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ⊆ 𝑆
6867a1i 11 . . . . . . . . . . . . 13 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ⊆ 𝑆)
69 incom 4131 . . . . . . . . . . . . . . . 16 ({𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ∩ 𝑘) = (𝑘 ∩ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})
70 simprll 778 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → 𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥})
7170elpwid 4511 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → 𝑠 ⊆ {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥})
72 ssrab2 4010 . . . . . . . . . . . . . . . . . . . . . 22 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ⊆ 𝑅
7371, 72sstrdi 3930 . . . . . . . . . . . . . . . . . . . . 21 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → 𝑠 𝑅)
7473adantr 484 . . . . . . . . . . . . . . . . . . . 20 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → 𝑠 𝑅)
75 elpwi 4509 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 ∈ 𝒫 𝑆𝑘 𝑆)
7675ad2antrl 727 . . . . . . . . . . . . . . . . . . . 20 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → 𝑘 𝑆)
77 eldif 3894 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑡 ∈ ((𝑠 × 𝑘) ∖ 𝑥) ↔ (𝑡 ∈ (𝑠 × 𝑘) ∧ ¬ 𝑡𝑥))
7877anbi1i 626 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑡 ∈ ((𝑠 × 𝑘) ∖ 𝑥) ∧ ((2nd ↾ ( 𝑅 × 𝑆))‘𝑡) = 𝑏) ↔ ((𝑡 ∈ (𝑠 × 𝑘) ∧ ¬ 𝑡𝑥) ∧ ((2nd ↾ ( 𝑅 × 𝑆))‘𝑡) = 𝑏))
79 anass 472 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑡 ∈ (𝑠 × 𝑘) ∧ ¬ 𝑡𝑥) ∧ ((2nd ↾ ( 𝑅 × 𝑆))‘𝑡) = 𝑏) ↔ (𝑡 ∈ (𝑠 × 𝑘) ∧ (¬ 𝑡𝑥 ∧ ((2nd ↾ ( 𝑅 × 𝑆))‘𝑡) = 𝑏)))
8078, 79bitri 278 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑡 ∈ ((𝑠 × 𝑘) ∖ 𝑥) ∧ ((2nd ↾ ( 𝑅 × 𝑆))‘𝑡) = 𝑏) ↔ (𝑡 ∈ (𝑠 × 𝑘) ∧ (¬ 𝑡𝑥 ∧ ((2nd ↾ ( 𝑅 × 𝑆))‘𝑡) = 𝑏)))
8180rexbii2 3211 . . . . . . . . . . . . . . . . . . . . . . . 24 (∃𝑡 ∈ ((𝑠 × 𝑘) ∖ 𝑥)((2nd ↾ ( 𝑅 × 𝑆))‘𝑡) = 𝑏 ↔ ∃𝑡 ∈ (𝑠 × 𝑘)(¬ 𝑡𝑥 ∧ ((2nd ↾ ( 𝑅 × 𝑆))‘𝑡) = 𝑏))
82 ancom 464 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((¬ 𝑡𝑥 ∧ ((2nd ↾ ( 𝑅 × 𝑆))‘𝑡) = 𝑏) ↔ (((2nd ↾ ( 𝑅 × 𝑆))‘𝑡) = 𝑏 ∧ ¬ 𝑡𝑥))
83 fveqeq2 6658 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑡 = ⟨𝑎, 𝑢⟩ → (((2nd ↾ ( 𝑅 × 𝑆))‘𝑡) = 𝑏 ↔ ((2nd ↾ ( 𝑅 × 𝑆))‘⟨𝑎, 𝑢⟩) = 𝑏))
84 eleq1 2880 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑡 = ⟨𝑎, 𝑢⟩ → (𝑡𝑥 ↔ ⟨𝑎, 𝑢⟩ ∈ 𝑥))
8584notbid 321 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑡 = ⟨𝑎, 𝑢⟩ → (¬ 𝑡𝑥 ↔ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥))
8683, 85anbi12d 633 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑡 = ⟨𝑎, 𝑢⟩ → ((((2nd ↾ ( 𝑅 × 𝑆))‘𝑡) = 𝑏 ∧ ¬ 𝑡𝑥) ↔ (((2nd ↾ ( 𝑅 × 𝑆))‘⟨𝑎, 𝑢⟩) = 𝑏 ∧ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥)))
8782, 86syl5bb 286 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑡 = ⟨𝑎, 𝑢⟩ → ((¬ 𝑡𝑥 ∧ ((2nd ↾ ( 𝑅 × 𝑆))‘𝑡) = 𝑏) ↔ (((2nd ↾ ( 𝑅 × 𝑆))‘⟨𝑎, 𝑢⟩) = 𝑏 ∧ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥)))
8887rexxp 5681 . . . . . . . . . . . . . . . . . . . . . . . 24 (∃𝑡 ∈ (𝑠 × 𝑘)(¬ 𝑡𝑥 ∧ ((2nd ↾ ( 𝑅 × 𝑆))‘𝑡) = 𝑏) ↔ ∃𝑎𝑠𝑢𝑘 (((2nd ↾ ( 𝑅 × 𝑆))‘⟨𝑎, 𝑢⟩) = 𝑏 ∧ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥))
8981, 88bitri 278 . . . . . . . . . . . . . . . . . . . . . . 23 (∃𝑡 ∈ ((𝑠 × 𝑘) ∖ 𝑥)((2nd ↾ ( 𝑅 × 𝑆))‘𝑡) = 𝑏 ↔ ∃𝑎𝑠𝑢𝑘 (((2nd ↾ ( 𝑅 × 𝑆))‘⟨𝑎, 𝑢⟩) = 𝑏 ∧ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥))
90 simpl 486 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑠 𝑅𝑘 𝑆) → 𝑠 𝑅)
9190sselda 3918 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝑠 𝑅𝑘 𝑆) ∧ 𝑎𝑠) → 𝑎 𝑅)
9291adantr 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝑠 𝑅𝑘 𝑆) ∧ 𝑎𝑠) ∧ 𝑢𝑘) → 𝑎 𝑅)
93 simplr 768 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝑠 𝑅𝑘 𝑆) ∧ 𝑎𝑠) → 𝑘 𝑆)
9493sselda 3918 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝑠 𝑅𝑘 𝑆) ∧ 𝑎𝑠) ∧ 𝑢𝑘) → 𝑢 𝑆)
9592, 94opelxpd 5561 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝑠 𝑅𝑘 𝑆) ∧ 𝑎𝑠) ∧ 𝑢𝑘) → ⟨𝑎, 𝑢⟩ ∈ ( 𝑅 × 𝑆))
9695fvresd 6669 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝑠 𝑅𝑘 𝑆) ∧ 𝑎𝑠) ∧ 𝑢𝑘) → ((2nd ↾ ( 𝑅 × 𝑆))‘⟨𝑎, 𝑢⟩) = (2nd ‘⟨𝑎, 𝑢⟩))
97 vex 3447 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 𝑎 ∈ V
98 vex 3447 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 𝑢 ∈ V
9997, 98op2nd 7684 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (2nd ‘⟨𝑎, 𝑢⟩) = 𝑢
10096, 99eqtrdi 2852 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝑠 𝑅𝑘 𝑆) ∧ 𝑎𝑠) ∧ 𝑢𝑘) → ((2nd ↾ ( 𝑅 × 𝑆))‘⟨𝑎, 𝑢⟩) = 𝑢)
101100eqeq1d 2803 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝑠 𝑅𝑘 𝑆) ∧ 𝑎𝑠) ∧ 𝑢𝑘) → (((2nd ↾ ( 𝑅 × 𝑆))‘⟨𝑎, 𝑢⟩) = 𝑏𝑢 = 𝑏))
102101anbi1d 632 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝑠 𝑅𝑘 𝑆) ∧ 𝑎𝑠) ∧ 𝑢𝑘) → ((((2nd ↾ ( 𝑅 × 𝑆))‘⟨𝑎, 𝑢⟩) = 𝑏 ∧ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥) ↔ (𝑢 = 𝑏 ∧ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥)))
103102rexbidva 3258 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑠 𝑅𝑘 𝑆) ∧ 𝑎𝑠) → (∃𝑢𝑘 (((2nd ↾ ( 𝑅 × 𝑆))‘⟨𝑎, 𝑢⟩) = 𝑏 ∧ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥) ↔ ∃𝑢𝑘 (𝑢 = 𝑏 ∧ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥)))
104 opeq2 4768 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑢 = 𝑏 → ⟨𝑎, 𝑢⟩ = ⟨𝑎, 𝑏⟩)
105104eleq1d 2877 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑢 = 𝑏 → (⟨𝑎, 𝑢⟩ ∈ 𝑥 ↔ ⟨𝑎, 𝑏⟩ ∈ 𝑥))
106105notbid 321 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑢 = 𝑏 → (¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥 ↔ ¬ ⟨𝑎, 𝑏⟩ ∈ 𝑥))
107106ceqsrexbv 3601 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (∃𝑢𝑘 (𝑢 = 𝑏 ∧ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥) ↔ (𝑏𝑘 ∧ ¬ ⟨𝑎, 𝑏⟩ ∈ 𝑥))
108103, 107syl6bb 290 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑠 𝑅𝑘 𝑆) ∧ 𝑎𝑠) → (∃𝑢𝑘 (((2nd ↾ ( 𝑅 × 𝑆))‘⟨𝑎, 𝑢⟩) = 𝑏 ∧ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥) ↔ (𝑏𝑘 ∧ ¬ ⟨𝑎, 𝑏⟩ ∈ 𝑥)))
109108rexbidva 3258 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑠 𝑅𝑘 𝑆) → (∃𝑎𝑠𝑢𝑘 (((2nd ↾ ( 𝑅 × 𝑆))‘⟨𝑎, 𝑢⟩) = 𝑏 ∧ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥) ↔ ∃𝑎𝑠 (𝑏𝑘 ∧ ¬ ⟨𝑎, 𝑏⟩ ∈ 𝑥)))
110 r19.42v 3306 . . . . . . . . . . . . . . . . . . . . . . . 24 (∃𝑎𝑠 (𝑏𝑘 ∧ ¬ ⟨𝑎, 𝑏⟩ ∈ 𝑥) ↔ (𝑏𝑘 ∧ ∃𝑎𝑠 ¬ ⟨𝑎, 𝑏⟩ ∈ 𝑥))
111109, 110syl6bb 290 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑠 𝑅𝑘 𝑆) → (∃𝑎𝑠𝑢𝑘 (((2nd ↾ ( 𝑅 × 𝑆))‘⟨𝑎, 𝑢⟩) = 𝑏 ∧ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥) ↔ (𝑏𝑘 ∧ ∃𝑎𝑠 ¬ ⟨𝑎, 𝑏⟩ ∈ 𝑥)))
11289, 111syl5bb 286 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑠 𝑅𝑘 𝑆) → (∃𝑡 ∈ ((𝑠 × 𝑘) ∖ 𝑥)((2nd ↾ ( 𝑅 × 𝑆))‘𝑡) = 𝑏 ↔ (𝑏𝑘 ∧ ∃𝑎𝑠 ¬ ⟨𝑎, 𝑏⟩ ∈ 𝑥)))
113 f2ndres 7700 . . . . . . . . . . . . . . . . . . . . . . . 24 (2nd ↾ ( 𝑅 × 𝑆)):( 𝑅 × 𝑆)⟶ 𝑆
114 ffn 6491 . . . . . . . . . . . . . . . . . . . . . . . 24 ((2nd ↾ ( 𝑅 × 𝑆)):( 𝑅 × 𝑆)⟶ 𝑆 → (2nd ↾ ( 𝑅 × 𝑆)) Fn ( 𝑅 × 𝑆))
115113, 114ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . 23 (2nd ↾ ( 𝑅 × 𝑆)) Fn ( 𝑅 × 𝑆)
116 difss 4062 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑠 × 𝑘) ∖ 𝑥) ⊆ (𝑠 × 𝑘)
117 xpss12 5538 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑠 𝑅𝑘 𝑆) → (𝑠 × 𝑘) ⊆ ( 𝑅 × 𝑆))
118116, 117sstrid 3929 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑠 𝑅𝑘 𝑆) → ((𝑠 × 𝑘) ∖ 𝑥) ⊆ ( 𝑅 × 𝑆))
119 fvelimab 6716 . . . . . . . . . . . . . . . . . . . . . . 23 (((2nd ↾ ( 𝑅 × 𝑆)) Fn ( 𝑅 × 𝑆) ∧ ((𝑠 × 𝑘) ∖ 𝑥) ⊆ ( 𝑅 × 𝑆)) → (𝑏 ∈ ((2nd ↾ ( 𝑅 × 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ↔ ∃𝑡 ∈ ((𝑠 × 𝑘) ∖ 𝑥)((2nd ↾ ( 𝑅 × 𝑆))‘𝑡) = 𝑏))
120115, 118, 119sylancr 590 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑠 𝑅𝑘 𝑆) → (𝑏 ∈ ((2nd ↾ ( 𝑅 × 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ↔ ∃𝑡 ∈ ((𝑠 × 𝑘) ∖ 𝑥)((2nd ↾ ( 𝑅 × 𝑆))‘𝑡) = 𝑏))
121 eldif 3894 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑏 ∈ (𝑘 ∖ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ↔ (𝑏𝑘 ∧ ¬ 𝑏 ∈ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}))
122 simpr 488 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑠 𝑅𝑘 𝑆) → 𝑘 𝑆)
123122sselda 3918 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑠 𝑅𝑘 𝑆) ∧ 𝑏𝑘) → 𝑏 𝑆)
124 sneq 4538 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑣 = 𝑏 → {𝑣} = {𝑏})
125124xpeq2d 5553 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑣 = 𝑏 → (𝑠 × {𝑣}) = (𝑠 × {𝑏}))
126125sseq1d 3949 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑣 = 𝑏 → ((𝑠 × {𝑣}) ⊆ 𝑥 ↔ (𝑠 × {𝑏}) ⊆ 𝑥))
127 dfss3 3906 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑠 × {𝑏}) ⊆ 𝑥 ↔ ∀𝑘 ∈ (𝑠 × {𝑏})𝑘𝑥)
128 eleq1 2880 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑘 = ⟨𝑎, 𝑡⟩ → (𝑘𝑥 ↔ ⟨𝑎, 𝑡⟩ ∈ 𝑥))
129128ralxp 5680 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (∀𝑘 ∈ (𝑠 × {𝑏})𝑘𝑥 ↔ ∀𝑎𝑠𝑡 ∈ {𝑏}⟨𝑎, 𝑡⟩ ∈ 𝑥)
130 vex 3447 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 𝑏 ∈ V
131 opeq2 4768 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑡 = 𝑏 → ⟨𝑎, 𝑡⟩ = ⟨𝑎, 𝑏⟩)
132131eleq1d 2877 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑡 = 𝑏 → (⟨𝑎, 𝑡⟩ ∈ 𝑥 ↔ ⟨𝑎, 𝑏⟩ ∈ 𝑥))
133130, 132ralsn 4582 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (∀𝑡 ∈ {𝑏}⟨𝑎, 𝑡⟩ ∈ 𝑥 ↔ ⟨𝑎, 𝑏⟩ ∈ 𝑥)
134133ralbii 3136 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (∀𝑎𝑠𝑡 ∈ {𝑏}⟨𝑎, 𝑡⟩ ∈ 𝑥 ↔ ∀𝑎𝑠𝑎, 𝑏⟩ ∈ 𝑥)
135127, 129, 1343bitri 300 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑠 × {𝑏}) ⊆ 𝑥 ↔ ∀𝑎𝑠𝑎, 𝑏⟩ ∈ 𝑥)
136126, 135syl6bb 290 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑣 = 𝑏 → ((𝑠 × {𝑣}) ⊆ 𝑥 ↔ ∀𝑎𝑠𝑎, 𝑏⟩ ∈ 𝑥))
137136elrab3 3632 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑏 𝑆 → (𝑏 ∈ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ↔ ∀𝑎𝑠𝑎, 𝑏⟩ ∈ 𝑥))
138123, 137syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑠 𝑅𝑘 𝑆) ∧ 𝑏𝑘) → (𝑏 ∈ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ↔ ∀𝑎𝑠𝑎, 𝑏⟩ ∈ 𝑥))
139138notbid 321 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑠 𝑅𝑘 𝑆) ∧ 𝑏𝑘) → (¬ 𝑏 ∈ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ↔ ¬ ∀𝑎𝑠𝑎, 𝑏⟩ ∈ 𝑥))
140 rexnal 3204 . . . . . . . . . . . . . . . . . . . . . . . . 25 (∃𝑎𝑠 ¬ ⟨𝑎, 𝑏⟩ ∈ 𝑥 ↔ ¬ ∀𝑎𝑠𝑎, 𝑏⟩ ∈ 𝑥)
141139, 140syl6bbr 292 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑠 𝑅𝑘 𝑆) ∧ 𝑏𝑘) → (¬ 𝑏 ∈ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ↔ ∃𝑎𝑠 ¬ ⟨𝑎, 𝑏⟩ ∈ 𝑥))
142141pm5.32da 582 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑠 𝑅𝑘 𝑆) → ((𝑏𝑘 ∧ ¬ 𝑏 ∈ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ↔ (𝑏𝑘 ∧ ∃𝑎𝑠 ¬ ⟨𝑎, 𝑏⟩ ∈ 𝑥)))
143121, 142syl5bb 286 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑠 𝑅𝑘 𝑆) → (𝑏 ∈ (𝑘 ∖ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ↔ (𝑏𝑘 ∧ ∃𝑎𝑠 ¬ ⟨𝑎, 𝑏⟩ ∈ 𝑥)))
144112, 120, 1433bitr4d 314 . . . . . . . . . . . . . . . . . . . . 21 ((𝑠 𝑅𝑘 𝑆) → (𝑏 ∈ ((2nd ↾ ( 𝑅 × 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ↔ 𝑏 ∈ (𝑘 ∖ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})))
145144eqrdv 2799 . . . . . . . . . . . . . . . . . . . 20 ((𝑠 𝑅𝑘 𝑆) → ((2nd ↾ ( 𝑅 × 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) = (𝑘 ∖ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}))
14674, 76, 145syl2anc 587 . . . . . . . . . . . . . . . . . . 19 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → ((2nd ↾ ( 𝑅 × 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) = (𝑘 ∖ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}))
147 difin 4191 . . . . . . . . . . . . . . . . . . . 20 (𝑘 ∖ (𝑘 ∩ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})) = (𝑘 ∖ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})
14865adantr 484 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → 𝑆 ∈ Top)
14924restuni 21770 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑆 ∈ Top ∧ 𝑘 𝑆) → 𝑘 = (𝑆t 𝑘))
150148, 76, 149syl2anc 587 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → 𝑘 = (𝑆t 𝑘))
151150difeq1d 4052 . . . . . . . . . . . . . . . . . . . 20 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → (𝑘 ∖ (𝑘 ∩ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})) = ( (𝑆t 𝑘) ∖ (𝑘 ∩ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})))
152147, 151syl5eqr 2850 . . . . . . . . . . . . . . . . . . 19 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → (𝑘 ∖ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) = ( (𝑆t 𝑘) ∖ (𝑘 ∩ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})))
153146, 152eqtrd 2836 . . . . . . . . . . . . . . . . . 18 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → ((2nd ↾ ( 𝑅 × 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) = ( (𝑆t 𝑘) ∖ (𝑘 ∩ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})))
15415ad2antrr 725 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → 𝑆 ∈ (ran 𝑘Gen ∩ Haus))
155154elin2d 4129 . . . . . . . . . . . . . . . . . . . 20 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → 𝑆 ∈ Haus)
156 df-ima 5536 . . . . . . . . . . . . . . . . . . . . . . 23 ((2nd ↾ ( 𝑅 × 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) = ran ((2nd ↾ ( 𝑅 × 𝑆)) ↾ ((𝑠 × 𝑘) ∖ 𝑥))
157 resres 5835 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((2nd ↾ ( 𝑅 × 𝑆)) ↾ ((𝑠 × 𝑘) ∖ 𝑥)) = (2nd ↾ (( 𝑅 × 𝑆) ∩ ((𝑠 × 𝑘) ∖ 𝑥)))
158 inss2 4159 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (( 𝑅 × 𝑆) ∩ ((𝑠 × 𝑘) ∖ 𝑥)) ⊆ ((𝑠 × 𝑘) ∖ 𝑥)
159158, 116sstri 3927 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (( 𝑅 × 𝑆) ∩ ((𝑠 × 𝑘) ∖ 𝑥)) ⊆ (𝑠 × 𝑘)
160 ssres2 5850 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((( 𝑅 × 𝑆) ∩ ((𝑠 × 𝑘) ∖ 𝑥)) ⊆ (𝑠 × 𝑘) → (2nd ↾ (( 𝑅 × 𝑆) ∩ ((𝑠 × 𝑘) ∖ 𝑥))) ⊆ (2nd ↾ (𝑠 × 𝑘)))
161159, 160ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . 25 (2nd ↾ (( 𝑅 × 𝑆) ∩ ((𝑠 × 𝑘) ∖ 𝑥))) ⊆ (2nd ↾ (𝑠 × 𝑘))
162157, 161eqsstri 3952 . . . . . . . . . . . . . . . . . . . . . . . 24 ((2nd ↾ ( 𝑅 × 𝑆)) ↾ ((𝑠 × 𝑘) ∖ 𝑥)) ⊆ (2nd ↾ (𝑠 × 𝑘))
163162rnssi 5778 . . . . . . . . . . . . . . . . . . . . . . 23 ran ((2nd ↾ ( 𝑅 × 𝑆)) ↾ ((𝑠 × 𝑘) ∖ 𝑥)) ⊆ ran (2nd ↾ (𝑠 × 𝑘))
164156, 163eqsstri 3952 . . . . . . . . . . . . . . . . . . . . . 22 ((2nd ↾ ( 𝑅 × 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ⊆ ran (2nd ↾ (𝑠 × 𝑘))
165 f2ndres 7700 . . . . . . . . . . . . . . . . . . . . . . 23 (2nd ↾ (𝑠 × 𝑘)):(𝑠 × 𝑘)⟶𝑘
166 frn 6497 . . . . . . . . . . . . . . . . . . . . . . 23 ((2nd ↾ (𝑠 × 𝑘)):(𝑠 × 𝑘)⟶𝑘 → ran (2nd ↾ (𝑠 × 𝑘)) ⊆ 𝑘)
167165, 166ax-mp 5 . . . . . . . . . . . . . . . . . . . . . 22 ran (2nd ↾ (𝑠 × 𝑘)) ⊆ 𝑘
168164, 167sstri 3927 . . . . . . . . . . . . . . . . . . . . 21 ((2nd ↾ ( 𝑅 × 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ⊆ 𝑘
169168, 76sstrid 3929 . . . . . . . . . . . . . . . . . . . 20 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → ((2nd ↾ ( 𝑅 × 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ⊆ 𝑆)
17012ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → 𝑅 ∈ (TopOn‘ 𝑅))
171148, 17sylib 221 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → 𝑆 ∈ (TopOn‘ 𝑆))
172 tx2cn 22218 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑅 ∈ (TopOn‘ 𝑅) ∧ 𝑆 ∈ (TopOn‘ 𝑆)) → (2nd ↾ ( 𝑅 × 𝑆)) ∈ ((𝑅 ×t 𝑆) Cn 𝑆))
173170, 171, 172syl2anc 587 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → (2nd ↾ ( 𝑅 × 𝑆)) ∈ ((𝑅 ×t 𝑆) Cn 𝑆))
17427ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → (𝑅 ×t 𝑆) ∈ Top)
175116a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → ((𝑠 × 𝑘) ∖ 𝑥) ⊆ (𝑠 × 𝑘))
176 vex 3447 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑠 ∈ V
177 vex 3447 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑘 ∈ V
178176, 177xpex 7460 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑠 × 𝑘) ∈ V
179178a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → (𝑠 × 𝑘) ∈ V)
180 restabs 21773 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑅 ×t 𝑆) ∈ Top ∧ ((𝑠 × 𝑘) ∖ 𝑥) ⊆ (𝑠 × 𝑘) ∧ (𝑠 × 𝑘) ∈ V) → (((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ↾t ((𝑠 × 𝑘) ∖ 𝑥)) = ((𝑅 ×t 𝑆) ↾t ((𝑠 × 𝑘) ∖ 𝑥)))
181174, 175, 179, 180syl3anc 1368 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → (((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ↾t ((𝑠 × 𝑘) ∖ 𝑥)) = ((𝑅 ×t 𝑆) ↾t ((𝑠 × 𝑘) ∖ 𝑥)))
18264adantr 484 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → 𝑅 ∈ Top)
183154, 4syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → 𝑆 ∈ Top)
184176a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → 𝑠 ∈ V)
185 simprl 770 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → 𝑘 ∈ 𝒫 𝑆)
186 txrest 22239 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑠 ∈ V ∧ 𝑘 ∈ 𝒫 𝑆)) → ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) = ((𝑅t 𝑠) ×t (𝑆t 𝑘)))
187182, 183, 184, 185, 186syl22anc 837 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) = ((𝑅t 𝑠) ×t (𝑆t 𝑘)))
188 simprr3 1220 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → (𝑅t 𝑠) ∈ Comp)
189188adantr 484 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → (𝑅t 𝑠) ∈ Comp)
190 simprr 772 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → (𝑆t 𝑘) ∈ Comp)
191 txcmp 22251 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑅t 𝑠) ∈ Comp ∧ (𝑆t 𝑘) ∈ Comp) → ((𝑅t 𝑠) ×t (𝑆t 𝑘)) ∈ Comp)
192189, 190, 191syl2anc 587 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → ((𝑅t 𝑠) ×t (𝑆t 𝑘)) ∈ Comp)
193187, 192eqeltrd 2893 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ∈ Comp)
194 difin 4191 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑠 × 𝑘) ∖ ((𝑠 × 𝑘) ∩ 𝑥)) = ((𝑠 × 𝑘) ∖ 𝑥)
19574, 76, 117syl2anc 587 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → (𝑠 × 𝑘) ⊆ ( 𝑅 × 𝑆))
196182, 148, 25syl2anc 587 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → ( 𝑅 × 𝑆) = (𝑅 ×t 𝑆))
197195, 196sseqtrd 3958 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → (𝑠 × 𝑘) ⊆ (𝑅 ×t 𝑆))
19828restuni 21770 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑅 ×t 𝑆) ∈ Top ∧ (𝑠 × 𝑘) ⊆ (𝑅 ×t 𝑆)) → (𝑠 × 𝑘) = ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)))
199174, 197, 198syl2anc 587 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → (𝑠 × 𝑘) = ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)))
200199difeq1d 4052 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → ((𝑠 × 𝑘) ∖ ((𝑠 × 𝑘) ∩ 𝑥)) = ( ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ∖ ((𝑠 × 𝑘) ∩ 𝑥)))
201194, 200syl5eqr 2850 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → ((𝑠 × 𝑘) ∖ 𝑥) = ( ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ∖ ((𝑠 × 𝑘) ∩ 𝑥)))
202 resttop 21768 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑅 ×t 𝑆) ∈ Top ∧ (𝑠 × 𝑘) ∈ V) → ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ∈ Top)
203174, 178, 202sylancl 589 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ∈ Top)
204 incom 4131 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑠 × 𝑘) ∩ 𝑥) = (𝑥 ∩ (𝑠 × 𝑘))
20520ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆)))
206 kgeni 22145 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆)) ∧ ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ∈ Comp) → (𝑥 ∩ (𝑠 × 𝑘)) ∈ ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)))
207205, 193, 206syl2anc 587 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → (𝑥 ∩ (𝑠 × 𝑘)) ∈ ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)))
208204, 207eqeltrid 2897 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → ((𝑠 × 𝑘) ∩ 𝑥) ∈ ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)))
209 eqid 2801 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) = ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘))
210209opncld 21641 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ∈ Top ∧ ((𝑠 × 𝑘) ∩ 𝑥) ∈ ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘))) → ( ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ∖ ((𝑠 × 𝑘) ∩ 𝑥)) ∈ (Clsd‘((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘))))
211203, 208, 210syl2anc 587 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → ( ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ∖ ((𝑠 × 𝑘) ∩ 𝑥)) ∈ (Clsd‘((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘))))
212201, 211eqeltrd 2893 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → ((𝑠 × 𝑘) ∖ 𝑥) ∈ (Clsd‘((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘))))
213 cmpcld 22010 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ∈ Comp ∧ ((𝑠 × 𝑘) ∖ 𝑥) ∈ (Clsd‘((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)))) → (((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ↾t ((𝑠 × 𝑘) ∖ 𝑥)) ∈ Comp)
214193, 212, 213syl2anc 587 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → (((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ↾t ((𝑠 × 𝑘) ∖ 𝑥)) ∈ Comp)
215181, 214eqeltrrd 2894 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → ((𝑅 ×t 𝑆) ↾t ((𝑠 × 𝑘) ∖ 𝑥)) ∈ Comp)
216 imacmp 22005 . . . . . . . . . . . . . . . . . . . . 21 (((2nd ↾ ( 𝑅 × 𝑆)) ∈ ((𝑅 ×t 𝑆) Cn 𝑆) ∧ ((𝑅 ×t 𝑆) ↾t ((𝑠 × 𝑘) ∖ 𝑥)) ∈ Comp) → (𝑆t ((2nd ↾ ( 𝑅 × 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥))) ∈ Comp)
217173, 215, 216syl2anc 587 . . . . . . . . . . . . . . . . . . . 20 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → (𝑆t ((2nd ↾ ( 𝑅 × 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥))) ∈ Comp)
21824hauscmp 22015 . . . . . . . . . . . . . . . . . . . 20 ((𝑆 ∈ Haus ∧ ((2nd ↾ ( 𝑅 × 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ⊆ 𝑆 ∧ (𝑆t ((2nd ↾ ( 𝑅 × 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥))) ∈ Comp) → ((2nd ↾ ( 𝑅 × 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ∈ (Clsd‘𝑆))
219155, 169, 217, 218syl3anc 1368 . . . . . . . . . . . . . . . . . . 19 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → ((2nd ↾ ( 𝑅 × 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ∈ (Clsd‘𝑆))
220168a1i 11 . . . . . . . . . . . . . . . . . . 19 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → ((2nd ↾ ( 𝑅 × 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ⊆ 𝑘)
22124restcldi 21781 . . . . . . . . . . . . . . . . . . 19 ((𝑘 𝑆 ∧ ((2nd ↾ ( 𝑅 × 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ∈ (Clsd‘𝑆) ∧ ((2nd ↾ ( 𝑅 × 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ⊆ 𝑘) → ((2nd ↾ ( 𝑅 × 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ∈ (Clsd‘(𝑆t 𝑘)))
22276, 219, 220, 221syl3anc 1368 . . . . . . . . . . . . . . . . . 18 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → ((2nd ↾ ( 𝑅 × 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ∈ (Clsd‘(𝑆t 𝑘)))
223153, 222eqeltrrd 2894 . . . . . . . . . . . . . . . . 17 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → ( (𝑆t 𝑘) ∖ (𝑘 ∩ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})) ∈ (Clsd‘(𝑆t 𝑘)))
224 resttop 21768 . . . . . . . . . . . . . . . . . . 19 ((𝑆 ∈ Top ∧ 𝑘 ∈ 𝒫 𝑆) → (𝑆t 𝑘) ∈ Top)
225148, 185, 224syl2anc 587 . . . . . . . . . . . . . . . . . 18 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → (𝑆t 𝑘) ∈ Top)
226 inss1 4158 . . . . . . . . . . . . . . . . . . 19 (𝑘 ∩ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ⊆ 𝑘
227226, 150sseqtrid 3970 . . . . . . . . . . . . . . . . . 18 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → (𝑘 ∩ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ⊆ (𝑆t 𝑘))
228 eqid 2801 . . . . . . . . . . . . . . . . . . 19 (𝑆t 𝑘) = (𝑆t 𝑘)
229228isopn2 21640 . . . . . . . . . . . . . . . . . 18 (((𝑆t 𝑘) ∈ Top ∧ (𝑘 ∩ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ⊆ (𝑆t 𝑘)) → ((𝑘 ∩ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ∈ (𝑆t 𝑘) ↔ ( (𝑆t 𝑘) ∖ (𝑘 ∩ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})) ∈ (Clsd‘(𝑆t 𝑘))))
230225, 227, 229syl2anc 587 . . . . . . . . . . . . . . . . 17 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → ((𝑘 ∩ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ∈ (𝑆t 𝑘) ↔ ( (𝑆t 𝑘) ∖ (𝑘 ∩ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})) ∈ (Clsd‘(𝑆t 𝑘))))
231223, 230mpbird 260 . . . . . . . . . . . . . . . 16 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → (𝑘 ∩ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ∈ (𝑆t 𝑘))
23269, 231eqeltrid 2897 . . . . . . . . . . . . . . 15 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → ({𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ∩ 𝑘) ∈ (𝑆t 𝑘))
233232expr 460 . . . . . . . . . . . . . 14 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ 𝑘 ∈ 𝒫 𝑆) → ((𝑆t 𝑘) ∈ Comp → ({𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ∩ 𝑘) ∈ (𝑆t 𝑘)))
234233ralrimiva 3152 . . . . . . . . . . . . 13 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → ∀𝑘 ∈ 𝒫 𝑆((𝑆t 𝑘) ∈ Comp → ({𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ∩ 𝑘) ∈ (𝑆t 𝑘)))
23565, 17sylib 221 . . . . . . . . . . . . . 14 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → 𝑆 ∈ (TopOn‘ 𝑆))
236 elkgen 22144 . . . . . . . . . . . . . 14 (𝑆 ∈ (TopOn‘ 𝑆) → ({𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ∈ (𝑘Gen‘𝑆) ↔ ({𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ⊆ 𝑆 ∧ ∀𝑘 ∈ 𝒫 𝑆((𝑆t 𝑘) ∈ Comp → ({𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ∩ 𝑘) ∈ (𝑆t 𝑘)))))
237235, 236syl 17 . . . . . . . . . . . . 13 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → ({𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ∈ (𝑘Gen‘𝑆) ↔ ({𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ⊆ 𝑆 ∧ ∀𝑘 ∈ 𝒫 𝑆((𝑆t 𝑘) ∈ Comp → ({𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ∩ 𝑘) ∈ (𝑆t 𝑘)))))
23868, 234, 237mpbir2and 712 . . . . . . . . . . . 12 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ∈ (𝑘Gen‘𝑆))
23915adantr 484 . . . . . . . . . . . . . 14 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → 𝑆 ∈ (ran 𝑘Gen ∩ Haus))
240239, 2syl 17 . . . . . . . . . . . . 13 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → 𝑆 ∈ ran 𝑘Gen)
241 kgenidm 22155 . . . . . . . . . . . . 13 (𝑆 ∈ ran 𝑘Gen → (𝑘Gen‘𝑆) = 𝑆)
242240, 241syl 17 . . . . . . . . . . . 12 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → (𝑘Gen‘𝑆) = 𝑆)
243238, 242eleqtrd 2895 . . . . . . . . . . 11 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ∈ 𝑆)
244 txopn 22210 . . . . . . . . . . 11 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑢𝑅 ∧ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ∈ 𝑆)) → (𝑢 × {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ∈ (𝑅 ×t 𝑆))
24564, 65, 66, 243, 244syl22anc 837 . . . . . . . . . 10 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → (𝑢 × {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ∈ (𝑅 ×t 𝑆))
24659adantr 484 . . . . . . . . . . 11 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → 𝑦 = ⟨(1st𝑦), (2nd𝑦)⟩)
247 simprr1 1218 . . . . . . . . . . . 12 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → (1st𝑦) ∈ 𝑢)
248 sneq 4538 . . . . . . . . . . . . . . 15 (𝑣 = (2nd𝑦) → {𝑣} = {(2nd𝑦)})
249248xpeq2d 5553 . . . . . . . . . . . . . 14 (𝑣 = (2nd𝑦) → (𝑠 × {𝑣}) = (𝑠 × {(2nd𝑦)}))
250249sseq1d 3949 . . . . . . . . . . . . 13 (𝑣 = (2nd𝑦) → ((𝑠 × {𝑣}) ⊆ 𝑥 ↔ (𝑠 × {(2nd𝑦)}) ⊆ 𝑥))
25134adantr 484 . . . . . . . . . . . . 13 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → (2nd𝑦) ∈ 𝑆)
252 relxp 5541 . . . . . . . . . . . . . . 15 Rel (𝑠 × {(2nd𝑦)})
253252a1i 11 . . . . . . . . . . . . . 14 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → Rel (𝑠 × {(2nd𝑦)}))
254 opelxp 5559 . . . . . . . . . . . . . . 15 (⟨𝑎, 𝑏⟩ ∈ (𝑠 × {(2nd𝑦)}) ↔ (𝑎𝑠𝑏 ∈ {(2nd𝑦)}))
25571sselda 3918 . . . . . . . . . . . . . . . . . 18 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ 𝑎𝑠) → 𝑎 ∈ {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥})
256 opeq1 4766 . . . . . . . . . . . . . . . . . . . . 21 (𝑡 = 𝑎 → ⟨𝑡, (2nd𝑦)⟩ = ⟨𝑎, (2nd𝑦)⟩)
257256eleq1d 2877 . . . . . . . . . . . . . . . . . . . 20 (𝑡 = 𝑎 → (⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥 ↔ ⟨𝑎, (2nd𝑦)⟩ ∈ 𝑥))
258257elrab 3631 . . . . . . . . . . . . . . . . . . 19 (𝑎 ∈ {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ↔ (𝑎 𝑅 ∧ ⟨𝑎, (2nd𝑦)⟩ ∈ 𝑥))
259258simprbi 500 . . . . . . . . . . . . . . . . . 18 (𝑎 ∈ {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} → ⟨𝑎, (2nd𝑦)⟩ ∈ 𝑥)
260255, 259syl 17 . . . . . . . . . . . . . . . . 17 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ 𝑎𝑠) → ⟨𝑎, (2nd𝑦)⟩ ∈ 𝑥)
261 elsni 4545 . . . . . . . . . . . . . . . . . . 19 (𝑏 ∈ {(2nd𝑦)} → 𝑏 = (2nd𝑦))
262261opeq2d 4775 . . . . . . . . . . . . . . . . . 18 (𝑏 ∈ {(2nd𝑦)} → ⟨𝑎, 𝑏⟩ = ⟨𝑎, (2nd𝑦)⟩)
263262eleq1d 2877 . . . . . . . . . . . . . . . . 17 (𝑏 ∈ {(2nd𝑦)} → (⟨𝑎, 𝑏⟩ ∈ 𝑥 ↔ ⟨𝑎, (2nd𝑦)⟩ ∈ 𝑥))
264260, 263syl5ibrcom 250 . . . . . . . . . . . . . . . 16 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ 𝑎𝑠) → (𝑏 ∈ {(2nd𝑦)} → ⟨𝑎, 𝑏⟩ ∈ 𝑥))
265264expimpd 457 . . . . . . . . . . . . . . 15 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → ((𝑎𝑠𝑏 ∈ {(2nd𝑦)}) → ⟨𝑎, 𝑏⟩ ∈ 𝑥))
266254, 265syl5bi 245 . . . . . . . . . . . . . 14 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → (⟨𝑎, 𝑏⟩ ∈ (𝑠 × {(2nd𝑦)}) → ⟨𝑎, 𝑏⟩ ∈ 𝑥))
267253, 266relssdv 5629 . . . . . . . . . . . . 13 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → (𝑠 × {(2nd𝑦)}) ⊆ 𝑥)
268250, 251, 267elrabd 3633 . . . . . . . . . . . 12 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → (2nd𝑦) ∈ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})
269247, 268opelxpd 5561 . . . . . . . . . . 11 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → ⟨(1st𝑦), (2nd𝑦)⟩ ∈ (𝑢 × {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}))
270246, 269eqeltrd 2893 . . . . . . . . . 10 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → 𝑦 ∈ (𝑢 × {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}))
271 relxp 5541 . . . . . . . . . . . 12 Rel (𝑢 × {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})
272271a1i 11 . . . . . . . . . . 11 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → Rel (𝑢 × {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}))
273 opelxp 5559 . . . . . . . . . . . 12 (⟨𝑎, 𝑏⟩ ∈ (𝑢 × {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ↔ (𝑎𝑢𝑏 ∈ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}))
274126elrab 3631 . . . . . . . . . . . . . . 15 (𝑏 ∈ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ↔ (𝑏 𝑆 ∧ (𝑠 × {𝑏}) ⊆ 𝑥))
275274simprbi 500 . . . . . . . . . . . . . 14 (𝑏 ∈ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} → (𝑠 × {𝑏}) ⊆ 𝑥)
276 simprr2 1219 . . . . . . . . . . . . . . . 16 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → 𝑢𝑠)
277276sselda 3918 . . . . . . . . . . . . . . 15 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ 𝑎𝑢) → 𝑎𝑠)
278 vsnid 4565 . . . . . . . . . . . . . . 15 𝑏 ∈ {𝑏}
279 opelxpi 5560 . . . . . . . . . . . . . . 15 ((𝑎𝑠𝑏 ∈ {𝑏}) → ⟨𝑎, 𝑏⟩ ∈ (𝑠 × {𝑏}))
280277, 278, 279sylancl 589 . . . . . . . . . . . . . 14 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ 𝑎𝑢) → ⟨𝑎, 𝑏⟩ ∈ (𝑠 × {𝑏}))
281 ssel 3911 . . . . . . . . . . . . . 14 ((𝑠 × {𝑏}) ⊆ 𝑥 → (⟨𝑎, 𝑏⟩ ∈ (𝑠 × {𝑏}) → ⟨𝑎, 𝑏⟩ ∈ 𝑥))
282275, 280, 281syl2imc 41 . . . . . . . . . . . . 13 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ 𝑎𝑢) → (𝑏 ∈ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} → ⟨𝑎, 𝑏⟩ ∈ 𝑥))
283282expimpd 457 . . . . . . . . . . . 12 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → ((𝑎𝑢𝑏 ∈ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) → ⟨𝑎, 𝑏⟩ ∈ 𝑥))
284273, 283syl5bi 245 . . . . . . . . . . 11 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → (⟨𝑎, 𝑏⟩ ∈ (𝑢 × {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) → ⟨𝑎, 𝑏⟩ ∈ 𝑥))
285272, 284relssdv 5629 . . . . . . . . . 10 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → (𝑢 × {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ⊆ 𝑥)
286 eleq2 2881 . . . . . . . . . . . 12 (𝑡 = (𝑢 × {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) → (𝑦𝑡𝑦 ∈ (𝑢 × {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})))
287 sseq1 3943 . . . . . . . . . . . 12 (𝑡 = (𝑢 × {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) → (𝑡𝑥 ↔ (𝑢 × {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ⊆ 𝑥))
288286, 287anbi12d 633 . . . . . . . . . . 11 (𝑡 = (𝑢 × {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) → ((𝑦𝑡𝑡𝑥) ↔ (𝑦 ∈ (𝑢 × {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ∧ (𝑢 × {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ⊆ 𝑥)))
289288rspcev 3574 . . . . . . . . . 10 (((𝑢 × {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ∈ (𝑅 ×t 𝑆) ∧ (𝑦 ∈ (𝑢 × {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ∧ (𝑢 × {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ⊆ 𝑥)) → ∃𝑡 ∈ (𝑅 ×t 𝑆)(𝑦𝑡𝑡𝑥))
290245, 270, 285, 289syl12anc 835 . . . . . . . . 9 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → ∃𝑡 ∈ (𝑅 ×t 𝑆)(𝑦𝑡𝑡𝑥))
291290expr 460 . . . . . . . 8 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ (𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅)) → (((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp) → ∃𝑡 ∈ (𝑅 ×t 𝑆)(𝑦𝑡𝑡𝑥)))
292291rexlimdvva 3256 . . . . . . 7 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → (∃𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥}∃𝑢𝑅 ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp) → ∃𝑡 ∈ (𝑅 ×t 𝑆)(𝑦𝑡𝑡𝑥)))
29363, 292mpd 15 . . . . . 6 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → ∃𝑡 ∈ (𝑅 ×t 𝑆)(𝑦𝑡𝑡𝑥))
294293ralrimiva 3152 . . . . 5 (((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) → ∀𝑦𝑥𝑡 ∈ (𝑅 ×t 𝑆)(𝑦𝑡𝑡𝑥))
2956adantr 484 . . . . . 6 (((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) → (𝑅 ×t 𝑆) ∈ Top)
296 eltop2 21583 . . . . . 6 ((𝑅 ×t 𝑆) ∈ Top → (𝑥 ∈ (𝑅 ×t 𝑆) ↔ ∀𝑦𝑥𝑡 ∈ (𝑅 ×t 𝑆)(𝑦𝑡𝑡𝑥)))
297295, 296syl 17 . . . . 5 (((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) → (𝑥 ∈ (𝑅 ×t 𝑆) ↔ ∀𝑦𝑥𝑡 ∈ (𝑅 ×t 𝑆)(𝑦𝑡𝑡𝑥)))
298294, 297mpbird 260 . . . 4 (((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) → 𝑥 ∈ (𝑅 ×t 𝑆))
299298ex 416 . . 3 ((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) → (𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆)) → 𝑥 ∈ (𝑅 ×t 𝑆)))
300299ssrdv 3924 . 2 ((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) → (𝑘Gen‘(𝑅 ×t 𝑆)) ⊆ (𝑅 ×t 𝑆))
301 iskgen2 22156 . 2 ((𝑅 ×t 𝑆) ∈ ran 𝑘Gen ↔ ((𝑅 ×t 𝑆) ∈ Top ∧ (𝑘Gen‘(𝑅 ×t 𝑆)) ⊆ (𝑅 ×t 𝑆)))
3026, 300, 301sylanbrc 586 1 ((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) → (𝑅 ×t 𝑆) ∈ ran 𝑘Gen)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399  w3a 1084   = wceq 1538  wcel 2112  wral 3109  wrex 3110  {crab 3113  Vcvv 3444  cdif 3881  cin 3883  wss 3884  𝒫 cpw 4500  {csn 4528  cop 4534   cuni 4803  cmpt 5113   I cid 5427   × cxp 5521  ccnv 5522  ran crn 5524  cres 5525  cima 5526  Rel wrel 5528   Fn wfn 6323  wf 6324  cfv 6328  (class class class)co 7139  1st c1st 7673  2nd c2nd 7674  t crest 16689  Topctop 21501  TopOnctopon 21518  Clsdccld 21624   Cn ccn 21832  Hauscha 21916  Compccmp 21994  𝑛-Locally cnlly 22073  𝑘Genckgen 22141   ×t ctx 22168
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-rep 5157  ax-sep 5170  ax-nul 5177  ax-pow 5234  ax-pr 5298  ax-un 7445
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ne 2991  df-ral 3114  df-rex 3115  df-reu 3116  df-rab 3118  df-v 3446  df-sbc 3724  df-csb 3832  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-pss 3903  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-tp 4533  df-op 4535  df-uni 4804  df-int 4842  df-iun 4886  df-iin 4887  df-br 5034  df-opab 5096  df-mpt 5114  df-tr 5140  df-id 5428  df-eprel 5433  df-po 5442  df-so 5443  df-fr 5482  df-we 5484  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-pred 6120  df-ord 6166  df-on 6167  df-lim 6168  df-suc 6169  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-ov 7142  df-oprab 7143  df-mpo 7144  df-om 7565  df-1st 7675  df-2nd 7676  df-wrecs 7934  df-recs 7995  df-rdg 8033  df-1o 8089  df-oadd 8093  df-er 8276  df-map 8395  df-en 8497  df-dom 8498  df-fin 8500  df-fi 8863  df-rest 16691  df-topgen 16712  df-top 21502  df-topon 21519  df-bases 21554  df-cld 21627  df-ntr 21628  df-cls 21629  df-nei 21706  df-cn 21835  df-cnp 21836  df-haus 21923  df-cmp 21995  df-nlly 22075  df-kgen 22142  df-tx 22170
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator