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

Theorem txkgen 23660
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 23481 . . 3 (𝑅 ∈ 𝑛-Locally Comp → 𝑅 ∈ Top)
2 elinel1 4201 . . . 4 (𝑆 ∈ (ran 𝑘Gen ∩ Haus) → 𝑆 ∈ ran 𝑘Gen)
3 kgentop 23550 . . . 4 (𝑆 ∈ ran 𝑘Gen → 𝑆 ∈ Top)
42, 3syl 17 . . 3 (𝑆 ∈ (ran 𝑘Gen ∩ Haus) → 𝑆 ∈ Top)
5 txtop 23577 . . 3 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑅 ×t 𝑆) ∈ Top)
61, 4, 5syl2an 596 . 2 ((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) → (𝑅 ×t 𝑆) ∈ Top)
7 simplll 775 . . . . . . . 8 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → 𝑅 ∈ 𝑛-Locally Comp)
8 eqid 2737 . . . . . . . . . 10 (𝑡 𝑅 ↦ ⟨𝑡, (2nd𝑦)⟩) = (𝑡 𝑅 ↦ ⟨𝑡, (2nd𝑦)⟩)
98mptpreima 6258 . . . . . . . . 9 ((𝑡 𝑅 ↦ ⟨𝑡, (2nd𝑦)⟩) “ 𝑥) = {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥}
101ad3antrrr 730 . . . . . . . . . . . . . 14 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → 𝑅 ∈ Top)
11 toptopon2 22924 . . . . . . . . . . . . . 14 (𝑅 ∈ Top ↔ 𝑅 ∈ (TopOn‘ 𝑅))
1210, 11sylib 218 . . . . . . . . . . . . 13 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → 𝑅 ∈ (TopOn‘ 𝑅))
13 idcn 23265 . . . . . . . . . . . . 13 (𝑅 ∈ (TopOn‘ 𝑅) → ( I ↾ 𝑅) ∈ (𝑅 Cn 𝑅))
1412, 13syl 17 . . . . . . . . . . . 12 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → ( I ↾ 𝑅) ∈ (𝑅 Cn 𝑅))
15 simpllr 776 . . . . . . . . . . . . . . 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 22924 . . . . . . . . . . . . . 14 (𝑆 ∈ Top ↔ 𝑆 ∈ (TopOn‘ 𝑆))
1816, 17sylib 218 . . . . . . . . . . . . 13 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → 𝑆 ∈ (TopOn‘ 𝑆))
19 simpr 484 . . . . . . . . . . . . . . . 16 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → 𝑦𝑥)
20 simplr 769 . . . . . . . . . . . . . . . 16 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆)))
21 elunii 4912 . . . . . . . . . . . . . . . 16 ((𝑦𝑥𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) → 𝑦 (𝑘Gen‘(𝑅 ×t 𝑆)))
2219, 20, 21syl2anc 584 . . . . . . . . . . . . . . 15 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → 𝑦 (𝑘Gen‘(𝑅 ×t 𝑆)))
23 eqid 2737 . . . . . . . . . . . . . . . . . 18 𝑅 = 𝑅
24 eqid 2737 . . . . . . . . . . . . . . . . . 18 𝑆 = 𝑆
2523, 24txuni 23600 . . . . . . . . . . . . . . . . 17 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → ( 𝑅 × 𝑆) = (𝑅 ×t 𝑆))
2610, 16, 25syl2anc 584 . . . . . . . . . . . . . . . 16 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → ( 𝑅 × 𝑆) = (𝑅 ×t 𝑆))
2710, 16, 5syl2anc 584 . . . . . . . . . . . . . . . . 17 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → (𝑅 ×t 𝑆) ∈ Top)
28 eqid 2737 . . . . . . . . . . . . . . . . . 18 (𝑅 ×t 𝑆) = (𝑅 ×t 𝑆)
2928kgenuni 23547 . . . . . . . . . . . . . . . . 17 ((𝑅 ×t 𝑆) ∈ Top → (𝑅 ×t 𝑆) = (𝑘Gen‘(𝑅 ×t 𝑆)))
3027, 29syl 17 . . . . . . . . . . . . . . . 16 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → (𝑅 ×t 𝑆) = (𝑘Gen‘(𝑅 ×t 𝑆)))
3126, 30eqtrd 2777 . . . . . . . . . . . . . . 15 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → ( 𝑅 × 𝑆) = (𝑘Gen‘(𝑅 ×t 𝑆)))
3222, 31eleqtrrd 2844 . . . . . . . . . . . . . 14 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → 𝑦 ∈ ( 𝑅 × 𝑆))
33 xp2nd 8047 . . . . . . . . . . . . . 14 (𝑦 ∈ ( 𝑅 × 𝑆) → (2nd𝑦) ∈ 𝑆)
3432, 33syl 17 . . . . . . . . . . . . 13 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → (2nd𝑦) ∈ 𝑆)
35 cnconst2 23291 . . . . . . . . . . . . 13 ((𝑅 ∈ (TopOn‘ 𝑅) ∧ 𝑆 ∈ (TopOn‘ 𝑆) ∧ (2nd𝑦) ∈ 𝑆) → ( 𝑅 × {(2nd𝑦)}) ∈ (𝑅 Cn 𝑆))
3612, 18, 34, 35syl3anc 1373 . . . . . . . . . . . 12 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → ( 𝑅 × {(2nd𝑦)}) ∈ (𝑅 Cn 𝑆))
37 fvresi 7193 . . . . . . . . . . . . . . . 16 (𝑡 𝑅 → (( I ↾ 𝑅)‘𝑡) = 𝑡)
38 fvex 6919 . . . . . . . . . . . . . . . . 17 (2nd𝑦) ∈ V
3938fvconst2 7224 . . . . . . . . . . . . . . . 16 (𝑡 𝑅 → (( 𝑅 × {(2nd𝑦)})‘𝑡) = (2nd𝑦))
4037, 39opeq12d 4881 . . . . . . . . . . . . . . 15 (𝑡 𝑅 → ⟨(( I ↾ 𝑅)‘𝑡), (( 𝑅 × {(2nd𝑦)})‘𝑡)⟩ = ⟨𝑡, (2nd𝑦)⟩)
4140mpteq2ia 5245 . . . . . . . . . . . . . 14 (𝑡 𝑅 ↦ ⟨(( I ↾ 𝑅)‘𝑡), (( 𝑅 × {(2nd𝑦)})‘𝑡)⟩) = (𝑡 𝑅 ↦ ⟨𝑡, (2nd𝑦)⟩)
4241eqcomi 2746 . . . . . . . . . . . . 13 (𝑡 𝑅 ↦ ⟨𝑡, (2nd𝑦)⟩) = (𝑡 𝑅 ↦ ⟨(( I ↾ 𝑅)‘𝑡), (( 𝑅 × {(2nd𝑦)})‘𝑡)⟩)
4323, 42txcnmpt 23632 . . . . . . . . . . . 12 ((( I ↾ 𝑅) ∈ (𝑅 Cn 𝑅) ∧ ( 𝑅 × {(2nd𝑦)}) ∈ (𝑅 Cn 𝑆)) → (𝑡 𝑅 ↦ ⟨𝑡, (2nd𝑦)⟩) ∈ (𝑅 Cn (𝑅 ×t 𝑆)))
4414, 36, 43syl2anc 584 . . . . . . . . . . 11 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → (𝑡 𝑅 ↦ ⟨𝑡, (2nd𝑦)⟩) ∈ (𝑅 Cn (𝑅 ×t 𝑆)))
45 llycmpkgen 23560 . . . . . . . . . . . . 13 (𝑅 ∈ 𝑛-Locally Comp → 𝑅 ∈ ran 𝑘Gen)
4645ad3antrrr 730 . . . . . . . . . . . 12 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → 𝑅 ∈ ran 𝑘Gen)
476ad2antrr 726 . . . . . . . . . . . 12 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → (𝑅 ×t 𝑆) ∈ Top)
48 kgencn3 23566 . . . . . . . . . . . 12 ((𝑅 ∈ ran 𝑘Gen ∧ (𝑅 ×t 𝑆) ∈ Top) → (𝑅 Cn (𝑅 ×t 𝑆)) = (𝑅 Cn (𝑘Gen‘(𝑅 ×t 𝑆))))
4946, 47, 48syl2anc 584 . . . . . . . . . . 11 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → (𝑅 Cn (𝑅 ×t 𝑆)) = (𝑅 Cn (𝑘Gen‘(𝑅 ×t 𝑆))))
5044, 49eleqtrd 2843 . . . . . . . . . 10 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → (𝑡 𝑅 ↦ ⟨𝑡, (2nd𝑦)⟩) ∈ (𝑅 Cn (𝑘Gen‘(𝑅 ×t 𝑆))))
51 cnima 23273 . . . . . . . . . 10 (((𝑡 𝑅 ↦ ⟨𝑡, (2nd𝑦)⟩) ∈ (𝑅 Cn (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) → ((𝑡 𝑅 ↦ ⟨𝑡, (2nd𝑦)⟩) “ 𝑥) ∈ 𝑅)
5250, 20, 51syl2anc 584 . . . . . . . . 9 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → ((𝑡 𝑅 ↦ ⟨𝑡, (2nd𝑦)⟩) “ 𝑥) ∈ 𝑅)
539, 52eqeltrrid 2846 . . . . . . . 8 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∈ 𝑅)
54 opeq1 4873 . . . . . . . . . 10 (𝑡 = (1st𝑦) → ⟨𝑡, (2nd𝑦)⟩ = ⟨(1st𝑦), (2nd𝑦)⟩)
5554eleq1d 2826 . . . . . . . . 9 (𝑡 = (1st𝑦) → (⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥 ↔ ⟨(1st𝑦), (2nd𝑦)⟩ ∈ 𝑥))
56 xp1st 8046 . . . . . . . . . 10 (𝑦 ∈ ( 𝑅 × 𝑆) → (1st𝑦) ∈ 𝑅)
5732, 56syl 17 . . . . . . . . 9 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → (1st𝑦) ∈ 𝑅)
58 1st2nd2 8053 . . . . . . . . . . 11 (𝑦 ∈ ( 𝑅 × 𝑆) → 𝑦 = ⟨(1st𝑦), (2nd𝑦)⟩)
5932, 58syl 17 . . . . . . . . . 10 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → 𝑦 = ⟨(1st𝑦), (2nd𝑦)⟩)
6059, 19eqeltrrd 2842 . . . . . . . . 9 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → ⟨(1st𝑦), (2nd𝑦)⟩ ∈ 𝑥)
6155, 57, 60elrabd 3694 . . . . . . . 8 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → (1st𝑦) ∈ {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥})
62 nlly2i 23484 . . . . . . . 8 ((𝑅 ∈ 𝑛-Locally Comp ∧ {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∈ 𝑅 ∧ (1st𝑦) ∈ {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥}) → ∃𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥}∃𝑢𝑅 ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))
637, 53, 61, 62syl3anc 1373 . . . . . . 7 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → ∃𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥}∃𝑢𝑅 ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))
6410adantr 480 . . . . . . . . . . 11 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → 𝑅 ∈ Top)
6516adantr 480 . . . . . . . . . . 11 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → 𝑆 ∈ Top)
66 simprlr 780 . . . . . . . . . . 11 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → 𝑢𝑅)
67 ssrab2 4080 . . . . . . . . . . . . . 14 {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ⊆ 𝑆
6867a1i 11 . . . . . . . . . . . . 13 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ⊆ 𝑆)
69 incom 4209 . . . . . . . . . . . . . . . 16 ({𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ∩ 𝑘) = (𝑘 ∩ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})
70 simprll 779 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → 𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥})
7170elpwid 4609 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → 𝑠 ⊆ {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥})
72 ssrab2 4080 . . . . . . . . . . . . . . . . . . . . . 22 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ⊆ 𝑅
7371, 72sstrdi 3996 . . . . . . . . . . . . . . . . . . . . 21 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → 𝑠 𝑅)
7473adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → 𝑠 𝑅)
75 elpwi 4607 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 ∈ 𝒫 𝑆𝑘 𝑆)
7675ad2antrl 728 . . . . . . . . . . . . . . . . . . . 20 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → 𝑘 𝑆)
77 eldif 3961 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑡 ∈ ((𝑠 × 𝑘) ∖ 𝑥) ↔ (𝑡 ∈ (𝑠 × 𝑘) ∧ ¬ 𝑡𝑥))
7877anbi1i 624 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑡 ∈ ((𝑠 × 𝑘) ∖ 𝑥) ∧ ((2nd ↾ ( 𝑅 × 𝑆))‘𝑡) = 𝑏) ↔ ((𝑡 ∈ (𝑠 × 𝑘) ∧ ¬ 𝑡𝑥) ∧ ((2nd ↾ ( 𝑅 × 𝑆))‘𝑡) = 𝑏))
79 anass 468 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑡 ∈ (𝑠 × 𝑘) ∧ ¬ 𝑡𝑥) ∧ ((2nd ↾ ( 𝑅 × 𝑆))‘𝑡) = 𝑏) ↔ (𝑡 ∈ (𝑠 × 𝑘) ∧ (¬ 𝑡𝑥 ∧ ((2nd ↾ ( 𝑅 × 𝑆))‘𝑡) = 𝑏)))
8078, 79bitri 275 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑡 ∈ ((𝑠 × 𝑘) ∖ 𝑥) ∧ ((2nd ↾ ( 𝑅 × 𝑆))‘𝑡) = 𝑏) ↔ (𝑡 ∈ (𝑠 × 𝑘) ∧ (¬ 𝑡𝑥 ∧ ((2nd ↾ ( 𝑅 × 𝑆))‘𝑡) = 𝑏)))
8180rexbii2 3090 . . . . . . . . . . . . . . . . . . . . . . . 24 (∃𝑡 ∈ ((𝑠 × 𝑘) ∖ 𝑥)((2nd ↾ ( 𝑅 × 𝑆))‘𝑡) = 𝑏 ↔ ∃𝑡 ∈ (𝑠 × 𝑘)(¬ 𝑡𝑥 ∧ ((2nd ↾ ( 𝑅 × 𝑆))‘𝑡) = 𝑏))
82 ancom 460 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((¬ 𝑡𝑥 ∧ ((2nd ↾ ( 𝑅 × 𝑆))‘𝑡) = 𝑏) ↔ (((2nd ↾ ( 𝑅 × 𝑆))‘𝑡) = 𝑏 ∧ ¬ 𝑡𝑥))
83 fveqeq2 6915 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑡 = ⟨𝑎, 𝑢⟩ → (((2nd ↾ ( 𝑅 × 𝑆))‘𝑡) = 𝑏 ↔ ((2nd ↾ ( 𝑅 × 𝑆))‘⟨𝑎, 𝑢⟩) = 𝑏))
84 eleq1 2829 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑡 = ⟨𝑎, 𝑢⟩ → (𝑡𝑥 ↔ ⟨𝑎, 𝑢⟩ ∈ 𝑥))
8584notbid 318 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑡 = ⟨𝑎, 𝑢⟩ → (¬ 𝑡𝑥 ↔ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥))
8683, 85anbi12d 632 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑡 = ⟨𝑎, 𝑢⟩ → ((((2nd ↾ ( 𝑅 × 𝑆))‘𝑡) = 𝑏 ∧ ¬ 𝑡𝑥) ↔ (((2nd ↾ ( 𝑅 × 𝑆))‘⟨𝑎, 𝑢⟩) = 𝑏 ∧ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥)))
8782, 86bitrid 283 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑡 = ⟨𝑎, 𝑢⟩ → ((¬ 𝑡𝑥 ∧ ((2nd ↾ ( 𝑅 × 𝑆))‘𝑡) = 𝑏) ↔ (((2nd ↾ ( 𝑅 × 𝑆))‘⟨𝑎, 𝑢⟩) = 𝑏 ∧ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥)))
8887rexxp 5853 . . . . . . . . . . . . . . . . . . . . . . . 24 (∃𝑡 ∈ (𝑠 × 𝑘)(¬ 𝑡𝑥 ∧ ((2nd ↾ ( 𝑅 × 𝑆))‘𝑡) = 𝑏) ↔ ∃𝑎𝑠𝑢𝑘 (((2nd ↾ ( 𝑅 × 𝑆))‘⟨𝑎, 𝑢⟩) = 𝑏 ∧ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥))
8981, 88bitri 275 . . . . . . . . . . . . . . . . . . . . . . 23 (∃𝑡 ∈ ((𝑠 × 𝑘) ∖ 𝑥)((2nd ↾ ( 𝑅 × 𝑆))‘𝑡) = 𝑏 ↔ ∃𝑎𝑠𝑢𝑘 (((2nd ↾ ( 𝑅 × 𝑆))‘⟨𝑎, 𝑢⟩) = 𝑏 ∧ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥))
90 simpl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑠 𝑅𝑘 𝑆) → 𝑠 𝑅)
9190sselda 3983 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝑠 𝑅𝑘 𝑆) ∧ 𝑎𝑠) → 𝑎 𝑅)
9291adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝑠 𝑅𝑘 𝑆) ∧ 𝑎𝑠) ∧ 𝑢𝑘) → 𝑎 𝑅)
93 simplr 769 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝑠 𝑅𝑘 𝑆) ∧ 𝑎𝑠) → 𝑘 𝑆)
9493sselda 3983 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝑠 𝑅𝑘 𝑆) ∧ 𝑎𝑠) ∧ 𝑢𝑘) → 𝑢 𝑆)
9592, 94opelxpd 5724 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝑠 𝑅𝑘 𝑆) ∧ 𝑎𝑠) ∧ 𝑢𝑘) → ⟨𝑎, 𝑢⟩ ∈ ( 𝑅 × 𝑆))
9695fvresd 6926 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝑠 𝑅𝑘 𝑆) ∧ 𝑎𝑠) ∧ 𝑢𝑘) → ((2nd ↾ ( 𝑅 × 𝑆))‘⟨𝑎, 𝑢⟩) = (2nd ‘⟨𝑎, 𝑢⟩))
97 vex 3484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 𝑎 ∈ V
98 vex 3484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 𝑢 ∈ V
9997, 98op2nd 8023 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (2nd ‘⟨𝑎, 𝑢⟩) = 𝑢
10096, 99eqtrdi 2793 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝑠 𝑅𝑘 𝑆) ∧ 𝑎𝑠) ∧ 𝑢𝑘) → ((2nd ↾ ( 𝑅 × 𝑆))‘⟨𝑎, 𝑢⟩) = 𝑢)
101100eqeq1d 2739 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝑠 𝑅𝑘 𝑆) ∧ 𝑎𝑠) ∧ 𝑢𝑘) → (((2nd ↾ ( 𝑅 × 𝑆))‘⟨𝑎, 𝑢⟩) = 𝑏𝑢 = 𝑏))
102101anbi1d 631 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝑠 𝑅𝑘 𝑆) ∧ 𝑎𝑠) ∧ 𝑢𝑘) → ((((2nd ↾ ( 𝑅 × 𝑆))‘⟨𝑎, 𝑢⟩) = 𝑏 ∧ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥) ↔ (𝑢 = 𝑏 ∧ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥)))
103102rexbidva 3177 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑠 𝑅𝑘 𝑆) ∧ 𝑎𝑠) → (∃𝑢𝑘 (((2nd ↾ ( 𝑅 × 𝑆))‘⟨𝑎, 𝑢⟩) = 𝑏 ∧ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥) ↔ ∃𝑢𝑘 (𝑢 = 𝑏 ∧ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥)))
104 opeq2 4874 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑢 = 𝑏 → ⟨𝑎, 𝑢⟩ = ⟨𝑎, 𝑏⟩)
105104eleq1d 2826 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑢 = 𝑏 → (⟨𝑎, 𝑢⟩ ∈ 𝑥 ↔ ⟨𝑎, 𝑏⟩ ∈ 𝑥))
106105notbid 318 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑢 = 𝑏 → (¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥 ↔ ¬ ⟨𝑎, 𝑏⟩ ∈ 𝑥))
107106ceqsrexbv 3656 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (∃𝑢𝑘 (𝑢 = 𝑏 ∧ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥) ↔ (𝑏𝑘 ∧ ¬ ⟨𝑎, 𝑏⟩ ∈ 𝑥))
108103, 107bitrdi 287 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑠 𝑅𝑘 𝑆) ∧ 𝑎𝑠) → (∃𝑢𝑘 (((2nd ↾ ( 𝑅 × 𝑆))‘⟨𝑎, 𝑢⟩) = 𝑏 ∧ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥) ↔ (𝑏𝑘 ∧ ¬ ⟨𝑎, 𝑏⟩ ∈ 𝑥)))
109108rexbidva 3177 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑠 𝑅𝑘 𝑆) → (∃𝑎𝑠𝑢𝑘 (((2nd ↾ ( 𝑅 × 𝑆))‘⟨𝑎, 𝑢⟩) = 𝑏 ∧ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥) ↔ ∃𝑎𝑠 (𝑏𝑘 ∧ ¬ ⟨𝑎, 𝑏⟩ ∈ 𝑥)))
110 r19.42v 3191 . . . . . . . . . . . . . . . . . . . . . . . 24 (∃𝑎𝑠 (𝑏𝑘 ∧ ¬ ⟨𝑎, 𝑏⟩ ∈ 𝑥) ↔ (𝑏𝑘 ∧ ∃𝑎𝑠 ¬ ⟨𝑎, 𝑏⟩ ∈ 𝑥))
111109, 110bitrdi 287 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑠 𝑅𝑘 𝑆) → (∃𝑎𝑠𝑢𝑘 (((2nd ↾ ( 𝑅 × 𝑆))‘⟨𝑎, 𝑢⟩) = 𝑏 ∧ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥) ↔ (𝑏𝑘 ∧ ∃𝑎𝑠 ¬ ⟨𝑎, 𝑏⟩ ∈ 𝑥)))
11289, 111bitrid 283 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑠 𝑅𝑘 𝑆) → (∃𝑡 ∈ ((𝑠 × 𝑘) ∖ 𝑥)((2nd ↾ ( 𝑅 × 𝑆))‘𝑡) = 𝑏 ↔ (𝑏𝑘 ∧ ∃𝑎𝑠 ¬ ⟨𝑎, 𝑏⟩ ∈ 𝑥)))
113 f2ndres 8039 . . . . . . . . . . . . . . . . . . . . . . . 24 (2nd ↾ ( 𝑅 × 𝑆)):( 𝑅 × 𝑆)⟶ 𝑆
114 ffn 6736 . . . . . . . . . . . . . . . . . . . . . . . 24 ((2nd ↾ ( 𝑅 × 𝑆)):( 𝑅 × 𝑆)⟶ 𝑆 → (2nd ↾ ( 𝑅 × 𝑆)) Fn ( 𝑅 × 𝑆))
115113, 114ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . 23 (2nd ↾ ( 𝑅 × 𝑆)) Fn ( 𝑅 × 𝑆)
116 difss 4136 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑠 × 𝑘) ∖ 𝑥) ⊆ (𝑠 × 𝑘)
117 xpss12 5700 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑠 𝑅𝑘 𝑆) → (𝑠 × 𝑘) ⊆ ( 𝑅 × 𝑆))
118116, 117sstrid 3995 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑠 𝑅𝑘 𝑆) → ((𝑠 × 𝑘) ∖ 𝑥) ⊆ ( 𝑅 × 𝑆))
119 fvelimab 6981 . . . . . . . . . . . . . . . . . . . . . . 23 (((2nd ↾ ( 𝑅 × 𝑆)) Fn ( 𝑅 × 𝑆) ∧ ((𝑠 × 𝑘) ∖ 𝑥) ⊆ ( 𝑅 × 𝑆)) → (𝑏 ∈ ((2nd ↾ ( 𝑅 × 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ↔ ∃𝑡 ∈ ((𝑠 × 𝑘) ∖ 𝑥)((2nd ↾ ( 𝑅 × 𝑆))‘𝑡) = 𝑏))
120115, 118, 119sylancr 587 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑠 𝑅𝑘 𝑆) → (𝑏 ∈ ((2nd ↾ ( 𝑅 × 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ↔ ∃𝑡 ∈ ((𝑠 × 𝑘) ∖ 𝑥)((2nd ↾ ( 𝑅 × 𝑆))‘𝑡) = 𝑏))
121 eldif 3961 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑏 ∈ (𝑘 ∖ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ↔ (𝑏𝑘 ∧ ¬ 𝑏 ∈ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}))
122 simpr 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑠 𝑅𝑘 𝑆) → 𝑘 𝑆)
123122sselda 3983 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑠 𝑅𝑘 𝑆) ∧ 𝑏𝑘) → 𝑏 𝑆)
124 sneq 4636 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑣 = 𝑏 → {𝑣} = {𝑏})
125124xpeq2d 5715 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑣 = 𝑏 → (𝑠 × {𝑣}) = (𝑠 × {𝑏}))
126125sseq1d 4015 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑣 = 𝑏 → ((𝑠 × {𝑣}) ⊆ 𝑥 ↔ (𝑠 × {𝑏}) ⊆ 𝑥))
127 dfss3 3972 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑠 × {𝑏}) ⊆ 𝑥 ↔ ∀𝑘 ∈ (𝑠 × {𝑏})𝑘𝑥)
128 eleq1 2829 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑘 = ⟨𝑎, 𝑡⟩ → (𝑘𝑥 ↔ ⟨𝑎, 𝑡⟩ ∈ 𝑥))
129128ralxp 5852 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (∀𝑘 ∈ (𝑠 × {𝑏})𝑘𝑥 ↔ ∀𝑎𝑠𝑡 ∈ {𝑏}⟨𝑎, 𝑡⟩ ∈ 𝑥)
130 vex 3484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 𝑏 ∈ V
131 opeq2 4874 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑡 = 𝑏 → ⟨𝑎, 𝑡⟩ = ⟨𝑎, 𝑏⟩)
132131eleq1d 2826 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑡 = 𝑏 → (⟨𝑎, 𝑡⟩ ∈ 𝑥 ↔ ⟨𝑎, 𝑏⟩ ∈ 𝑥))
133130, 132ralsn 4681 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (∀𝑡 ∈ {𝑏}⟨𝑎, 𝑡⟩ ∈ 𝑥 ↔ ⟨𝑎, 𝑏⟩ ∈ 𝑥)
134133ralbii 3093 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (∀𝑎𝑠𝑡 ∈ {𝑏}⟨𝑎, 𝑡⟩ ∈ 𝑥 ↔ ∀𝑎𝑠𝑎, 𝑏⟩ ∈ 𝑥)
135127, 129, 1343bitri 297 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑠 × {𝑏}) ⊆ 𝑥 ↔ ∀𝑎𝑠𝑎, 𝑏⟩ ∈ 𝑥)
136126, 135bitrdi 287 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑣 = 𝑏 → ((𝑠 × {𝑣}) ⊆ 𝑥 ↔ ∀𝑎𝑠𝑎, 𝑏⟩ ∈ 𝑥))
137136elrab3 3693 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑏 𝑆 → (𝑏 ∈ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ↔ ∀𝑎𝑠𝑎, 𝑏⟩ ∈ 𝑥))
138123, 137syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑠 𝑅𝑘 𝑆) ∧ 𝑏𝑘) → (𝑏 ∈ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ↔ ∀𝑎𝑠𝑎, 𝑏⟩ ∈ 𝑥))
139138notbid 318 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑠 𝑅𝑘 𝑆) ∧ 𝑏𝑘) → (¬ 𝑏 ∈ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ↔ ¬ ∀𝑎𝑠𝑎, 𝑏⟩ ∈ 𝑥))
140 rexnal 3100 . . . . . . . . . . . . . . . . . . . . . . . . 25 (∃𝑎𝑠 ¬ ⟨𝑎, 𝑏⟩ ∈ 𝑥 ↔ ¬ ∀𝑎𝑠𝑎, 𝑏⟩ ∈ 𝑥)
141139, 140bitr4di 289 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑠 𝑅𝑘 𝑆) ∧ 𝑏𝑘) → (¬ 𝑏 ∈ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ↔ ∃𝑎𝑠 ¬ ⟨𝑎, 𝑏⟩ ∈ 𝑥))
142141pm5.32da 579 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑠 𝑅𝑘 𝑆) → ((𝑏𝑘 ∧ ¬ 𝑏 ∈ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ↔ (𝑏𝑘 ∧ ∃𝑎𝑠 ¬ ⟨𝑎, 𝑏⟩ ∈ 𝑥)))
143121, 142bitrid 283 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑠 𝑅𝑘 𝑆) → (𝑏 ∈ (𝑘 ∖ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ↔ (𝑏𝑘 ∧ ∃𝑎𝑠 ¬ ⟨𝑎, 𝑏⟩ ∈ 𝑥)))
144112, 120, 1433bitr4d 311 . . . . . . . . . . . . . . . . . . . . 21 ((𝑠 𝑅𝑘 𝑆) → (𝑏 ∈ ((2nd ↾ ( 𝑅 × 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ↔ 𝑏 ∈ (𝑘 ∖ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})))
145144eqrdv 2735 . . . . . . . . . . . . . . . . . . . 20 ((𝑠 𝑅𝑘 𝑆) → ((2nd ↾ ( 𝑅 × 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) = (𝑘 ∖ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}))
14674, 76, 145syl2anc 584 . . . . . . . . . . . . . . . . . . 19 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → ((2nd ↾ ( 𝑅 × 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) = (𝑘 ∖ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}))
147 difin 4272 . . . . . . . . . . . . . . . . . . . 20 (𝑘 ∖ (𝑘 ∩ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})) = (𝑘 ∖ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})
14865adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → 𝑆 ∈ Top)
14924restuni 23170 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑆 ∈ Top ∧ 𝑘 𝑆) → 𝑘 = (𝑆t 𝑘))
150148, 76, 149syl2anc 584 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → 𝑘 = (𝑆t 𝑘))
151150difeq1d 4125 . . . . . . . . . . . . . . . . . . . 20 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → (𝑘 ∖ (𝑘 ∩ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})) = ( (𝑆t 𝑘) ∖ (𝑘 ∩ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})))
152147, 151eqtr3id 2791 . . . . . . . . . . . . . . . . . . 19 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → (𝑘 ∖ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) = ( (𝑆t 𝑘) ∖ (𝑘 ∩ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})))
153146, 152eqtrd 2777 . . . . . . . . . . . . . . . . . 18 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → ((2nd ↾ ( 𝑅 × 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) = ( (𝑆t 𝑘) ∖ (𝑘 ∩ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})))
15415ad2antrr 726 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → 𝑆 ∈ (ran 𝑘Gen ∩ Haus))
155154elin2d 4205 . . . . . . . . . . . . . . . . . . . 20 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → 𝑆 ∈ Haus)
156 df-ima 5698 . . . . . . . . . . . . . . . . . . . . . . 23 ((2nd ↾ ( 𝑅 × 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) = ran ((2nd ↾ ( 𝑅 × 𝑆)) ↾ ((𝑠 × 𝑘) ∖ 𝑥))
157 resres 6010 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((2nd ↾ ( 𝑅 × 𝑆)) ↾ ((𝑠 × 𝑘) ∖ 𝑥)) = (2nd ↾ (( 𝑅 × 𝑆) ∩ ((𝑠 × 𝑘) ∖ 𝑥)))
158 inss2 4238 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (( 𝑅 × 𝑆) ∩ ((𝑠 × 𝑘) ∖ 𝑥)) ⊆ ((𝑠 × 𝑘) ∖ 𝑥)
159158, 116sstri 3993 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (( 𝑅 × 𝑆) ∩ ((𝑠 × 𝑘) ∖ 𝑥)) ⊆ (𝑠 × 𝑘)
160 ssres2 6022 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((( 𝑅 × 𝑆) ∩ ((𝑠 × 𝑘) ∖ 𝑥)) ⊆ (𝑠 × 𝑘) → (2nd ↾ (( 𝑅 × 𝑆) ∩ ((𝑠 × 𝑘) ∖ 𝑥))) ⊆ (2nd ↾ (𝑠 × 𝑘)))
161159, 160ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . 25 (2nd ↾ (( 𝑅 × 𝑆) ∩ ((𝑠 × 𝑘) ∖ 𝑥))) ⊆ (2nd ↾ (𝑠 × 𝑘))
162157, 161eqsstri 4030 . . . . . . . . . . . . . . . . . . . . . . . 24 ((2nd ↾ ( 𝑅 × 𝑆)) ↾ ((𝑠 × 𝑘) ∖ 𝑥)) ⊆ (2nd ↾ (𝑠 × 𝑘))
163162rnssi 5951 . . . . . . . . . . . . . . . . . . . . . . 23 ran ((2nd ↾ ( 𝑅 × 𝑆)) ↾ ((𝑠 × 𝑘) ∖ 𝑥)) ⊆ ran (2nd ↾ (𝑠 × 𝑘))
164156, 163eqsstri 4030 . . . . . . . . . . . . . . . . . . . . . 22 ((2nd ↾ ( 𝑅 × 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ⊆ ran (2nd ↾ (𝑠 × 𝑘))
165 f2ndres 8039 . . . . . . . . . . . . . . . . . . . . . . 23 (2nd ↾ (𝑠 × 𝑘)):(𝑠 × 𝑘)⟶𝑘
166 frn 6743 . . . . . . . . . . . . . . . . . . . . . . 23 ((2nd ↾ (𝑠 × 𝑘)):(𝑠 × 𝑘)⟶𝑘 → ran (2nd ↾ (𝑠 × 𝑘)) ⊆ 𝑘)
167165, 166ax-mp 5 . . . . . . . . . . . . . . . . . . . . . 22 ran (2nd ↾ (𝑠 × 𝑘)) ⊆ 𝑘
168164, 167sstri 3993 . . . . . . . . . . . . . . . . . . . . 21 ((2nd ↾ ( 𝑅 × 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ⊆ 𝑘
169168, 76sstrid 3995 . . . . . . . . . . . . . . . . . . . 20 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → ((2nd ↾ ( 𝑅 × 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ⊆ 𝑆)
17012ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → 𝑅 ∈ (TopOn‘ 𝑅))
171148, 17sylib 218 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → 𝑆 ∈ (TopOn‘ 𝑆))
172 tx2cn 23618 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑅 ∈ (TopOn‘ 𝑅) ∧ 𝑆 ∈ (TopOn‘ 𝑆)) → (2nd ↾ ( 𝑅 × 𝑆)) ∈ ((𝑅 ×t 𝑆) Cn 𝑆))
173170, 171, 172syl2anc 584 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → (2nd ↾ ( 𝑅 × 𝑆)) ∈ ((𝑅 ×t 𝑆) Cn 𝑆))
17427ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . . 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 3484 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑠 ∈ V
177 vex 3484 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑘 ∈ V
178176, 177xpex 7773 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑠 × 𝑘) ∈ V
179178a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → (𝑠 × 𝑘) ∈ V)
180 restabs 23173 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑅 ×t 𝑆) ∈ Top ∧ ((𝑠 × 𝑘) ∖ 𝑥) ⊆ (𝑠 × 𝑘) ∧ (𝑠 × 𝑘) ∈ V) → (((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ↾t ((𝑠 × 𝑘) ∖ 𝑥)) = ((𝑅 ×t 𝑆) ↾t ((𝑠 × 𝑘) ∖ 𝑥)))
181174, 175, 179, 180syl3anc 1373 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → (((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ↾t ((𝑠 × 𝑘) ∖ 𝑥)) = ((𝑅 ×t 𝑆) ↾t ((𝑠 × 𝑘) ∖ 𝑥)))
18264adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 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 771 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → 𝑘 ∈ 𝒫 𝑆)
186 txrest 23639 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑠 ∈ V ∧ 𝑘 ∈ 𝒫 𝑆)) → ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) = ((𝑅t 𝑠) ×t (𝑆t 𝑘)))
187182, 183, 184, 185, 186syl22anc 839 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) = ((𝑅t 𝑠) ×t (𝑆t 𝑘)))
188 simprr3 1224 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → (𝑅t 𝑠) ∈ Comp)
189188adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → (𝑅t 𝑠) ∈ Comp)
190 simprr 773 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → (𝑆t 𝑘) ∈ Comp)
191 txcmp 23651 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑅t 𝑠) ∈ Comp ∧ (𝑆t 𝑘) ∈ Comp) → ((𝑅t 𝑠) ×t (𝑆t 𝑘)) ∈ Comp)
192189, 190, 191syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → ((𝑅t 𝑠) ×t (𝑆t 𝑘)) ∈ Comp)
193187, 192eqeltrd 2841 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ∈ Comp)
194 difin 4272 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑠 × 𝑘) ∖ ((𝑠 × 𝑘) ∩ 𝑥)) = ((𝑠 × 𝑘) ∖ 𝑥)
19574, 76, 117syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → (𝑠 × 𝑘) ⊆ ( 𝑅 × 𝑆))
196182, 148, 25syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → ( 𝑅 × 𝑆) = (𝑅 ×t 𝑆))
197195, 196sseqtrd 4020 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → (𝑠 × 𝑘) ⊆ (𝑅 ×t 𝑆))
19828restuni 23170 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑅 ×t 𝑆) ∈ Top ∧ (𝑠 × 𝑘) ⊆ (𝑅 ×t 𝑆)) → (𝑠 × 𝑘) = ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)))
199174, 197, 198syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → (𝑠 × 𝑘) = ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)))
200199difeq1d 4125 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → ((𝑠 × 𝑘) ∖ ((𝑠 × 𝑘) ∩ 𝑥)) = ( ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ∖ ((𝑠 × 𝑘) ∩ 𝑥)))
201194, 200eqtr3id 2791 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → ((𝑠 × 𝑘) ∖ 𝑥) = ( ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ∖ ((𝑠 × 𝑘) ∩ 𝑥)))
202 resttop 23168 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑅 ×t 𝑆) ∈ Top ∧ (𝑠 × 𝑘) ∈ V) → ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ∈ Top)
203174, 178, 202sylancl 586 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ∈ Top)
204 incom 4209 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑠 × 𝑘) ∩ 𝑥) = (𝑥 ∩ (𝑠 × 𝑘))
20520ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆)))
206 kgeni 23545 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆)) ∧ ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ∈ Comp) → (𝑥 ∩ (𝑠 × 𝑘)) ∈ ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)))
207205, 193, 206syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → (𝑥 ∩ (𝑠 × 𝑘)) ∈ ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)))
208204, 207eqeltrid 2845 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → ((𝑠 × 𝑘) ∩ 𝑥) ∈ ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)))
209 eqid 2737 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) = ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘))
210209opncld 23041 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ∈ Top ∧ ((𝑠 × 𝑘) ∩ 𝑥) ∈ ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘))) → ( ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ∖ ((𝑠 × 𝑘) ∩ 𝑥)) ∈ (Clsd‘((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘))))
211203, 208, 210syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → ( ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ∖ ((𝑠 × 𝑘) ∩ 𝑥)) ∈ (Clsd‘((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘))))
212201, 211eqeltrd 2841 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → ((𝑠 × 𝑘) ∖ 𝑥) ∈ (Clsd‘((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘))))
213 cmpcld 23410 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ∈ Comp ∧ ((𝑠 × 𝑘) ∖ 𝑥) ∈ (Clsd‘((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)))) → (((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ↾t ((𝑠 × 𝑘) ∖ 𝑥)) ∈ Comp)
214193, 212, 213syl2anc 584 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → (((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ↾t ((𝑠 × 𝑘) ∖ 𝑥)) ∈ Comp)
215181, 214eqeltrrd 2842 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → ((𝑅 ×t 𝑆) ↾t ((𝑠 × 𝑘) ∖ 𝑥)) ∈ Comp)
216 imacmp 23405 . . . . . . . . . . . . . . . . . . . . 21 (((2nd ↾ ( 𝑅 × 𝑆)) ∈ ((𝑅 ×t 𝑆) Cn 𝑆) ∧ ((𝑅 ×t 𝑆) ↾t ((𝑠 × 𝑘) ∖ 𝑥)) ∈ Comp) → (𝑆t ((2nd ↾ ( 𝑅 × 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥))) ∈ Comp)
217173, 215, 216syl2anc 584 . . . . . . . . . . . . . . . . . . . 20 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → (𝑆t ((2nd ↾ ( 𝑅 × 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥))) ∈ Comp)
21824hauscmp 23415 . . . . . . . . . . . . . . . . . . . 20 ((𝑆 ∈ Haus ∧ ((2nd ↾ ( 𝑅 × 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ⊆ 𝑆 ∧ (𝑆t ((2nd ↾ ( 𝑅 × 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥))) ∈ Comp) → ((2nd ↾ ( 𝑅 × 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ∈ (Clsd‘𝑆))
219155, 169, 217, 218syl3anc 1373 . . . . . . . . . . . . . . . . . . 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 23181 . . . . . . . . . . . . . . . . . . 19 ((𝑘 𝑆 ∧ ((2nd ↾ ( 𝑅 × 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ∈ (Clsd‘𝑆) ∧ ((2nd ↾ ( 𝑅 × 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ⊆ 𝑘) → ((2nd ↾ ( 𝑅 × 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ∈ (Clsd‘(𝑆t 𝑘)))
22276, 219, 220, 221syl3anc 1373 . . . . . . . . . . . . . . . . . 18 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → ((2nd ↾ ( 𝑅 × 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ∈ (Clsd‘(𝑆t 𝑘)))
223153, 222eqeltrrd 2842 . . . . . . . . . . . . . . . . 17 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → ( (𝑆t 𝑘) ∖ (𝑘 ∩ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})) ∈ (Clsd‘(𝑆t 𝑘)))
224 resttop 23168 . . . . . . . . . . . . . . . . . . 19 ((𝑆 ∈ Top ∧ 𝑘 ∈ 𝒫 𝑆) → (𝑆t 𝑘) ∈ Top)
225148, 185, 224syl2anc 584 . . . . . . . . . . . . . . . . . 18 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → (𝑆t 𝑘) ∈ Top)
226 inss1 4237 . . . . . . . . . . . . . . . . . . 19 (𝑘 ∩ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ⊆ 𝑘
227226, 150sseqtrid 4026 . . . . . . . . . . . . . . . . . 18 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → (𝑘 ∩ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ⊆ (𝑆t 𝑘))
228 eqid 2737 . . . . . . . . . . . . . . . . . . 19 (𝑆t 𝑘) = (𝑆t 𝑘)
229228isopn2 23040 . . . . . . . . . . . . . . . . . 18 (((𝑆t 𝑘) ∈ Top ∧ (𝑘 ∩ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ⊆ (𝑆t 𝑘)) → ((𝑘 ∩ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ∈ (𝑆t 𝑘) ↔ ( (𝑆t 𝑘) ∖ (𝑘 ∩ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})) ∈ (Clsd‘(𝑆t 𝑘))))
230225, 227, 229syl2anc 584 . . . . . . . . . . . . . . . . 17 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → ((𝑘 ∩ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ∈ (𝑆t 𝑘) ↔ ( (𝑆t 𝑘) ∖ (𝑘 ∩ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})) ∈ (Clsd‘(𝑆t 𝑘))))
231223, 230mpbird 257 . . . . . . . . . . . . . . . 16 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → (𝑘 ∩ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ∈ (𝑆t 𝑘))
23269, 231eqeltrid 2845 . . . . . . . . . . . . . . 15 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → ({𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ∩ 𝑘) ∈ (𝑆t 𝑘))
233232expr 456 . . . . . . . . . . . . . 14 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ 𝑘 ∈ 𝒫 𝑆) → ((𝑆t 𝑘) ∈ Comp → ({𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ∩ 𝑘) ∈ (𝑆t 𝑘)))
234233ralrimiva 3146 . . . . . . . . . . . . 13 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → ∀𝑘 ∈ 𝒫 𝑆((𝑆t 𝑘) ∈ Comp → ({𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ∩ 𝑘) ∈ (𝑆t 𝑘)))
23565, 17sylib 218 . . . . . . . . . . . . . 14 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → 𝑆 ∈ (TopOn‘ 𝑆))
236 elkgen 23544 . . . . . . . . . . . . . 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 713 . . . . . . . . . . . 12 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ∈ (𝑘Gen‘𝑆))
23915adantr 480 . . . . . . . . . . . . . 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 23555 . . . . . . . . . . . . 13 (𝑆 ∈ ran 𝑘Gen → (𝑘Gen‘𝑆) = 𝑆)
242240, 241syl 17 . . . . . . . . . . . 12 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → (𝑘Gen‘𝑆) = 𝑆)
243238, 242eleqtrd 2843 . . . . . . . . . . 11 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ∈ 𝑆)
244 txopn 23610 . . . . . . . . . . 11 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑢𝑅 ∧ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ∈ 𝑆)) → (𝑢 × {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ∈ (𝑅 ×t 𝑆))
24564, 65, 66, 243, 244syl22anc 839 . . . . . . . . . 10 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → (𝑢 × {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ∈ (𝑅 ×t 𝑆))
24659adantr 480 . . . . . . . . . . 11 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → 𝑦 = ⟨(1st𝑦), (2nd𝑦)⟩)
247 simprr1 1222 . . . . . . . . . . . 12 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → (1st𝑦) ∈ 𝑢)
248 sneq 4636 . . . . . . . . . . . . . . 15 (𝑣 = (2nd𝑦) → {𝑣} = {(2nd𝑦)})
249248xpeq2d 5715 . . . . . . . . . . . . . 14 (𝑣 = (2nd𝑦) → (𝑠 × {𝑣}) = (𝑠 × {(2nd𝑦)}))
250249sseq1d 4015 . . . . . . . . . . . . 13 (𝑣 = (2nd𝑦) → ((𝑠 × {𝑣}) ⊆ 𝑥 ↔ (𝑠 × {(2nd𝑦)}) ⊆ 𝑥))
25134adantr 480 . . . . . . . . . . . . 13 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → (2nd𝑦) ∈ 𝑆)
252 relxp 5703 . . . . . . . . . . . . . . 15 Rel (𝑠 × {(2nd𝑦)})
253252a1i 11 . . . . . . . . . . . . . 14 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → Rel (𝑠 × {(2nd𝑦)}))
254 opelxp 5721 . . . . . . . . . . . . . . 15 (⟨𝑎, 𝑏⟩ ∈ (𝑠 × {(2nd𝑦)}) ↔ (𝑎𝑠𝑏 ∈ {(2nd𝑦)}))
25571sselda 3983 . . . . . . . . . . . . . . . . . 18 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ 𝑎𝑠) → 𝑎 ∈ {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥})
256 opeq1 4873 . . . . . . . . . . . . . . . . . . . . 21 (𝑡 = 𝑎 → ⟨𝑡, (2nd𝑦)⟩ = ⟨𝑎, (2nd𝑦)⟩)
257256eleq1d 2826 . . . . . . . . . . . . . . . . . . . 20 (𝑡 = 𝑎 → (⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥 ↔ ⟨𝑎, (2nd𝑦)⟩ ∈ 𝑥))
258257elrab 3692 . . . . . . . . . . . . . . . . . . 19 (𝑎 ∈ {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ↔ (𝑎 𝑅 ∧ ⟨𝑎, (2nd𝑦)⟩ ∈ 𝑥))
259258simprbi 496 . . . . . . . . . . . . . . . . . 18 (𝑎 ∈ {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} → ⟨𝑎, (2nd𝑦)⟩ ∈ 𝑥)
260255, 259syl 17 . . . . . . . . . . . . . . . . 17 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ 𝑎𝑠) → ⟨𝑎, (2nd𝑦)⟩ ∈ 𝑥)
261 elsni 4643 . . . . . . . . . . . . . . . . . . 19 (𝑏 ∈ {(2nd𝑦)} → 𝑏 = (2nd𝑦))
262261opeq2d 4880 . . . . . . . . . . . . . . . . . 18 (𝑏 ∈ {(2nd𝑦)} → ⟨𝑎, 𝑏⟩ = ⟨𝑎, (2nd𝑦)⟩)
263262eleq1d 2826 . . . . . . . . . . . . . . . . 17 (𝑏 ∈ {(2nd𝑦)} → (⟨𝑎, 𝑏⟩ ∈ 𝑥 ↔ ⟨𝑎, (2nd𝑦)⟩ ∈ 𝑥))
264260, 263syl5ibrcom 247 . . . . . . . . . . . . . . . 16 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ 𝑎𝑠) → (𝑏 ∈ {(2nd𝑦)} → ⟨𝑎, 𝑏⟩ ∈ 𝑥))
265264expimpd 453 . . . . . . . . . . . . . . 15 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → ((𝑎𝑠𝑏 ∈ {(2nd𝑦)}) → ⟨𝑎, 𝑏⟩ ∈ 𝑥))
266254, 265biimtrid 242 . . . . . . . . . . . . . 14 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → (⟨𝑎, 𝑏⟩ ∈ (𝑠 × {(2nd𝑦)}) → ⟨𝑎, 𝑏⟩ ∈ 𝑥))
267253, 266relssdv 5798 . . . . . . . . . . . . 13 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → (𝑠 × {(2nd𝑦)}) ⊆ 𝑥)
268250, 251, 267elrabd 3694 . . . . . . . . . . . 12 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → (2nd𝑦) ∈ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})
269247, 268opelxpd 5724 . . . . . . . . . . 11 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → ⟨(1st𝑦), (2nd𝑦)⟩ ∈ (𝑢 × {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}))
270246, 269eqeltrd 2841 . . . . . . . . . 10 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → 𝑦 ∈ (𝑢 × {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}))
271 relxp 5703 . . . . . . . . . . . 12 Rel (𝑢 × {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})
272271a1i 11 . . . . . . . . . . 11 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → Rel (𝑢 × {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}))
273 opelxp 5721 . . . . . . . . . . . 12 (⟨𝑎, 𝑏⟩ ∈ (𝑢 × {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ↔ (𝑎𝑢𝑏 ∈ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}))
274126elrab 3692 . . . . . . . . . . . . . . 15 (𝑏 ∈ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ↔ (𝑏 𝑆 ∧ (𝑠 × {𝑏}) ⊆ 𝑥))
275274simprbi 496 . . . . . . . . . . . . . 14 (𝑏 ∈ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} → (𝑠 × {𝑏}) ⊆ 𝑥)
276 simprr2 1223 . . . . . . . . . . . . . . . 16 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → 𝑢𝑠)
277276sselda 3983 . . . . . . . . . . . . . . 15 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ 𝑎𝑢) → 𝑎𝑠)
278 vsnid 4663 . . . . . . . . . . . . . . 15 𝑏 ∈ {𝑏}
279 opelxpi 5722 . . . . . . . . . . . . . . 15 ((𝑎𝑠𝑏 ∈ {𝑏}) → ⟨𝑎, 𝑏⟩ ∈ (𝑠 × {𝑏}))
280277, 278, 279sylancl 586 . . . . . . . . . . . . . 14 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ 𝑎𝑢) → ⟨𝑎, 𝑏⟩ ∈ (𝑠 × {𝑏}))
281 ssel 3977 . . . . . . . . . . . . . 14 ((𝑠 × {𝑏}) ⊆ 𝑥 → (⟨𝑎, 𝑏⟩ ∈ (𝑠 × {𝑏}) → ⟨𝑎, 𝑏⟩ ∈ 𝑥))
282275, 280, 281syl2imc 41 . . . . . . . . . . . . 13 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ 𝑎𝑢) → (𝑏 ∈ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} → ⟨𝑎, 𝑏⟩ ∈ 𝑥))
283282expimpd 453 . . . . . . . . . . . 12 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → ((𝑎𝑢𝑏 ∈ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) → ⟨𝑎, 𝑏⟩ ∈ 𝑥))
284273, 283biimtrid 242 . . . . . . . . . . 11 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → (⟨𝑎, 𝑏⟩ ∈ (𝑢 × {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) → ⟨𝑎, 𝑏⟩ ∈ 𝑥))
285272, 284relssdv 5798 . . . . . . . . . 10 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → (𝑢 × {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ⊆ 𝑥)
286 eleq2 2830 . . . . . . . . . . . 12 (𝑡 = (𝑢 × {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) → (𝑦𝑡𝑦 ∈ (𝑢 × {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})))
287 sseq1 4009 . . . . . . . . . . . 12 (𝑡 = (𝑢 × {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) → (𝑡𝑥 ↔ (𝑢 × {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ⊆ 𝑥))
288286, 287anbi12d 632 . . . . . . . . . . 11 (𝑡 = (𝑢 × {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) → ((𝑦𝑡𝑡𝑥) ↔ (𝑦 ∈ (𝑢 × {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ∧ (𝑢 × {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ⊆ 𝑥)))
289288rspcev 3622 . . . . . . . . . 10 (((𝑢 × {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ∈ (𝑅 ×t 𝑆) ∧ (𝑦 ∈ (𝑢 × {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ∧ (𝑢 × {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ⊆ 𝑥)) → ∃𝑡 ∈ (𝑅 ×t 𝑆)(𝑦𝑡𝑡𝑥))
290245, 270, 285, 289syl12anc 837 . . . . . . . . 9 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → ∃𝑡 ∈ (𝑅 ×t 𝑆)(𝑦𝑡𝑡𝑥))
291290expr 456 . . . . . . . 8 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ (𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅)) → (((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp) → ∃𝑡 ∈ (𝑅 ×t 𝑆)(𝑦𝑡𝑡𝑥)))
292291rexlimdvva 3213 . . . . . . 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 3146 . . . . 5 (((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) → ∀𝑦𝑥𝑡 ∈ (𝑅 ×t 𝑆)(𝑦𝑡𝑡𝑥))
2956adantr 480 . . . . . 6 (((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) → (𝑅 ×t 𝑆) ∈ Top)
296 eltop2 22982 . . . . . 6 ((𝑅 ×t 𝑆) ∈ Top → (𝑥 ∈ (𝑅 ×t 𝑆) ↔ ∀𝑦𝑥𝑡 ∈ (𝑅 ×t 𝑆)(𝑦𝑡𝑡𝑥)))
297295, 296syl 17 . . . . 5 (((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) → (𝑥 ∈ (𝑅 ×t 𝑆) ↔ ∀𝑦𝑥𝑡 ∈ (𝑅 ×t 𝑆)(𝑦𝑡𝑡𝑥)))
298294, 297mpbird 257 . . . 4 (((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) → 𝑥 ∈ (𝑅 ×t 𝑆))
299298ex 412 . . 3 ((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) → (𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆)) → 𝑥 ∈ (𝑅 ×t 𝑆)))
300299ssrdv 3989 . 2 ((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) → (𝑘Gen‘(𝑅 ×t 𝑆)) ⊆ (𝑅 ×t 𝑆))
301 iskgen2 23556 . 2 ((𝑅 ×t 𝑆) ∈ ran 𝑘Gen ↔ ((𝑅 ×t 𝑆) ∈ Top ∧ (𝑘Gen‘(𝑅 ×t 𝑆)) ⊆ (𝑅 ×t 𝑆)))
3026, 300, 301sylanbrc 583 1 ((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) → (𝑅 ×t 𝑆) ∈ ran 𝑘Gen)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  w3a 1087   = wceq 1540  wcel 2108  wral 3061  wrex 3070  {crab 3436  Vcvv 3480  cdif 3948  cin 3950  wss 3951  𝒫 cpw 4600  {csn 4626  cop 4632   cuni 4907  cmpt 5225   I cid 5577   × cxp 5683  ccnv 5684  ran crn 5686  cres 5687  cima 5688  Rel wrel 5690   Fn wfn 6556  wf 6557  cfv 6561  (class class class)co 7431  1st c1st 8012  2nd c2nd 8013  t crest 17465  Topctop 22899  TopOnctopon 22916  Clsdccld 23024   Cn ccn 23232  Hauscha 23316  Compccmp 23394  𝑛-Locally cnlly 23473  𝑘Genckgen 23541   ×t ctx 23568
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-int 4947  df-iun 4993  df-iin 4994  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-1st 8014  df-2nd 8015  df-1o 8506  df-2o 8507  df-map 8868  df-en 8986  df-dom 8987  df-fin 8989  df-fi 9451  df-rest 17467  df-topgen 17488  df-top 22900  df-topon 22917  df-bases 22953  df-cld 23027  df-ntr 23028  df-cls 23029  df-nei 23106  df-cn 23235  df-cnp 23236  df-haus 23323  df-cmp 23395  df-nlly 23475  df-kgen 23542  df-tx 23570
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator