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

Theorem txkgen 21365
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 21186 . . 3 (𝑅 ∈ 𝑛-Locally Comp → 𝑅 ∈ Top)
2 elinel1 3777 . . . 4 (𝑆 ∈ (ran 𝑘Gen ∩ Haus) → 𝑆 ∈ ran 𝑘Gen)
3 kgentop 21255 . . . 4 (𝑆 ∈ ran 𝑘Gen → 𝑆 ∈ Top)
42, 3syl 17 . . 3 (𝑆 ∈ (ran 𝑘Gen ∩ Haus) → 𝑆 ∈ Top)
5 txtop 21282 . . 3 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑅 ×t 𝑆) ∈ Top)
61, 4, 5syl2an 494 . 2 ((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) → (𝑅 ×t 𝑆) ∈ Top)
7 simplll 797 . . . . . . . 8 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → 𝑅 ∈ 𝑛-Locally Comp)
8 eqid 2621 . . . . . . . . . 10 (𝑡 𝑅 ↦ ⟨𝑡, (2nd𝑦)⟩) = (𝑡 𝑅 ↦ ⟨𝑡, (2nd𝑦)⟩)
98mptpreima 5587 . . . . . . . . 9 ((𝑡 𝑅 ↦ ⟨𝑡, (2nd𝑦)⟩) “ 𝑥) = {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥}
101ad3antrrr 765 . . . . . . . . . . . . . 14 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → 𝑅 ∈ Top)
11 eqid 2621 . . . . . . . . . . . . . . 15 𝑅 = 𝑅
1211toptopon 20648 . . . . . . . . . . . . . 14 (𝑅 ∈ Top ↔ 𝑅 ∈ (TopOn‘ 𝑅))
1310, 12sylib 208 . . . . . . . . . . . . 13 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → 𝑅 ∈ (TopOn‘ 𝑅))
14 idcn 20971 . . . . . . . . . . . . 13 (𝑅 ∈ (TopOn‘ 𝑅) → ( I ↾ 𝑅) ∈ (𝑅 Cn 𝑅))
1513, 14syl 17 . . . . . . . . . . . 12 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → ( I ↾ 𝑅) ∈ (𝑅 Cn 𝑅))
16 simpllr 798 . . . . . . . . . . . . . . 15 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → 𝑆 ∈ (ran 𝑘Gen ∩ Haus))
1716, 4syl 17 . . . . . . . . . . . . . 14 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → 𝑆 ∈ Top)
18 eqid 2621 . . . . . . . . . . . . . . 15 𝑆 = 𝑆
1918toptopon 20648 . . . . . . . . . . . . . 14 (𝑆 ∈ Top ↔ 𝑆 ∈ (TopOn‘ 𝑆))
2017, 19sylib 208 . . . . . . . . . . . . 13 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → 𝑆 ∈ (TopOn‘ 𝑆))
21 simpr 477 . . . . . . . . . . . . . . . 16 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → 𝑦𝑥)
22 simplr 791 . . . . . . . . . . . . . . . 16 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆)))
23 elunii 4407 . . . . . . . . . . . . . . . 16 ((𝑦𝑥𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) → 𝑦 (𝑘Gen‘(𝑅 ×t 𝑆)))
2421, 22, 23syl2anc 692 . . . . . . . . . . . . . . 15 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → 𝑦 (𝑘Gen‘(𝑅 ×t 𝑆)))
2511, 18txuni 21305 . . . . . . . . . . . . . . . . 17 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → ( 𝑅 × 𝑆) = (𝑅 ×t 𝑆))
2610, 17, 25syl2anc 692 . . . . . . . . . . . . . . . 16 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → ( 𝑅 × 𝑆) = (𝑅 ×t 𝑆))
2710, 17, 5syl2anc 692 . . . . . . . . . . . . . . . . 17 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → (𝑅 ×t 𝑆) ∈ Top)
28 eqid 2621 . . . . . . . . . . . . . . . . . 18 (𝑅 ×t 𝑆) = (𝑅 ×t 𝑆)
2928kgenuni 21252 . . . . . . . . . . . . . . . . 17 ((𝑅 ×t 𝑆) ∈ Top → (𝑅 ×t 𝑆) = (𝑘Gen‘(𝑅 ×t 𝑆)))
3027, 29syl 17 . . . . . . . . . . . . . . . 16 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → (𝑅 ×t 𝑆) = (𝑘Gen‘(𝑅 ×t 𝑆)))
3126, 30eqtrd 2655 . . . . . . . . . . . . . . 15 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → ( 𝑅 × 𝑆) = (𝑘Gen‘(𝑅 ×t 𝑆)))
3224, 31eleqtrrd 2701 . . . . . . . . . . . . . 14 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → 𝑦 ∈ ( 𝑅 × 𝑆))
33 xp2nd 7144 . . . . . . . . . . . . . 14 (𝑦 ∈ ( 𝑅 × 𝑆) → (2nd𝑦) ∈ 𝑆)
3432, 33syl 17 . . . . . . . . . . . . 13 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → (2nd𝑦) ∈ 𝑆)
35 cnconst2 20997 . . . . . . . . . . . . 13 ((𝑅 ∈ (TopOn‘ 𝑅) ∧ 𝑆 ∈ (TopOn‘ 𝑆) ∧ (2nd𝑦) ∈ 𝑆) → ( 𝑅 × {(2nd𝑦)}) ∈ (𝑅 Cn 𝑆))
3613, 20, 34, 35syl3anc 1323 . . . . . . . . . . . 12 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → ( 𝑅 × {(2nd𝑦)}) ∈ (𝑅 Cn 𝑆))
37 fvresi 6393 . . . . . . . . . . . . . . . 16 (𝑡 𝑅 → (( I ↾ 𝑅)‘𝑡) = 𝑡)
38 fvex 6158 . . . . . . . . . . . . . . . . 17 (2nd𝑦) ∈ V
3938fvconst2 6423 . . . . . . . . . . . . . . . 16 (𝑡 𝑅 → (( 𝑅 × {(2nd𝑦)})‘𝑡) = (2nd𝑦))
4037, 39opeq12d 4378 . . . . . . . . . . . . . . 15 (𝑡 𝑅 → ⟨(( I ↾ 𝑅)‘𝑡), (( 𝑅 × {(2nd𝑦)})‘𝑡)⟩ = ⟨𝑡, (2nd𝑦)⟩)
4140mpteq2ia 4700 . . . . . . . . . . . . . 14 (𝑡 𝑅 ↦ ⟨(( I ↾ 𝑅)‘𝑡), (( 𝑅 × {(2nd𝑦)})‘𝑡)⟩) = (𝑡 𝑅 ↦ ⟨𝑡, (2nd𝑦)⟩)
4241eqcomi 2630 . . . . . . . . . . . . 13 (𝑡 𝑅 ↦ ⟨𝑡, (2nd𝑦)⟩) = (𝑡 𝑅 ↦ ⟨(( I ↾ 𝑅)‘𝑡), (( 𝑅 × {(2nd𝑦)})‘𝑡)⟩)
4311, 42txcnmpt 21337 . . . . . . . . . . . 12 ((( I ↾ 𝑅) ∈ (𝑅 Cn 𝑅) ∧ ( 𝑅 × {(2nd𝑦)}) ∈ (𝑅 Cn 𝑆)) → (𝑡 𝑅 ↦ ⟨𝑡, (2nd𝑦)⟩) ∈ (𝑅 Cn (𝑅 ×t 𝑆)))
4415, 36, 43syl2anc 692 . . . . . . . . . . 11 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → (𝑡 𝑅 ↦ ⟨𝑡, (2nd𝑦)⟩) ∈ (𝑅 Cn (𝑅 ×t 𝑆)))
45 llycmpkgen 21265 . . . . . . . . . . . . 13 (𝑅 ∈ 𝑛-Locally Comp → 𝑅 ∈ ran 𝑘Gen)
4645ad3antrrr 765 . . . . . . . . . . . 12 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → 𝑅 ∈ ran 𝑘Gen)
476ad2antrr 761 . . . . . . . . . . . 12 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → (𝑅 ×t 𝑆) ∈ Top)
48 kgencn3 21271 . . . . . . . . . . . 12 ((𝑅 ∈ ran 𝑘Gen ∧ (𝑅 ×t 𝑆) ∈ Top) → (𝑅 Cn (𝑅 ×t 𝑆)) = (𝑅 Cn (𝑘Gen‘(𝑅 ×t 𝑆))))
4946, 47, 48syl2anc 692 . . . . . . . . . . 11 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → (𝑅 Cn (𝑅 ×t 𝑆)) = (𝑅 Cn (𝑘Gen‘(𝑅 ×t 𝑆))))
5044, 49eleqtrd 2700 . . . . . . . . . 10 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → (𝑡 𝑅 ↦ ⟨𝑡, (2nd𝑦)⟩) ∈ (𝑅 Cn (𝑘Gen‘(𝑅 ×t 𝑆))))
51 cnima 20979 . . . . . . . . . 10 (((𝑡 𝑅 ↦ ⟨𝑡, (2nd𝑦)⟩) ∈ (𝑅 Cn (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) → ((𝑡 𝑅 ↦ ⟨𝑡, (2nd𝑦)⟩) “ 𝑥) ∈ 𝑅)
5250, 22, 51syl2anc 692 . . . . . . . . 9 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → ((𝑡 𝑅 ↦ ⟨𝑡, (2nd𝑦)⟩) “ 𝑥) ∈ 𝑅)
539, 52syl5eqelr 2703 . . . . . . . 8 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∈ 𝑅)
54 xp1st 7143 . . . . . . . . . 10 (𝑦 ∈ ( 𝑅 × 𝑆) → (1st𝑦) ∈ 𝑅)
5532, 54syl 17 . . . . . . . . 9 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → (1st𝑦) ∈ 𝑅)
56 1st2nd2 7150 . . . . . . . . . . 11 (𝑦 ∈ ( 𝑅 × 𝑆) → 𝑦 = ⟨(1st𝑦), (2nd𝑦)⟩)
5732, 56syl 17 . . . . . . . . . 10 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → 𝑦 = ⟨(1st𝑦), (2nd𝑦)⟩)
5857, 21eqeltrrd 2699 . . . . . . . . 9 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → ⟨(1st𝑦), (2nd𝑦)⟩ ∈ 𝑥)
59 opeq1 4370 . . . . . . . . . . 11 (𝑡 = (1st𝑦) → ⟨𝑡, (2nd𝑦)⟩ = ⟨(1st𝑦), (2nd𝑦)⟩)
6059eleq1d 2683 . . . . . . . . . 10 (𝑡 = (1st𝑦) → (⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥 ↔ ⟨(1st𝑦), (2nd𝑦)⟩ ∈ 𝑥))
6160elrab 3346 . . . . . . . . 9 ((1st𝑦) ∈ {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ↔ ((1st𝑦) ∈ 𝑅 ∧ ⟨(1st𝑦), (2nd𝑦)⟩ ∈ 𝑥))
6255, 58, 61sylanbrc 697 . . . . . . . 8 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → (1st𝑦) ∈ {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥})
63 nlly2i 21189 . . . . . . . 8 ((𝑅 ∈ 𝑛-Locally Comp ∧ {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∈ 𝑅 ∧ (1st𝑦) ∈ {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥}) → ∃𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥}∃𝑢𝑅 ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))
647, 53, 62, 63syl3anc 1323 . . . . . . 7 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → ∃𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥}∃𝑢𝑅 ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))
6510adantr 481 . . . . . . . . . . 11 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → 𝑅 ∈ Top)
6617adantr 481 . . . . . . . . . . 11 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → 𝑆 ∈ Top)
67 simprlr 802 . . . . . . . . . . 11 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → 𝑢𝑅)
68 ssrab2 3666 . . . . . . . . . . . . . 14 {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ⊆ 𝑆
6968a1i 11 . . . . . . . . . . . . 13 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ⊆ 𝑆)
70 incom 3783 . . . . . . . . . . . . . . . 16 ({𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ∩ 𝑘) = (𝑘 ∩ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})
71 simprll 801 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → 𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥})
7271elpwid 4141 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → 𝑠 ⊆ {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥})
73 ssrab2 3666 . . . . . . . . . . . . . . . . . . . . . 22 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ⊆ 𝑅
7472, 73syl6ss 3595 . . . . . . . . . . . . . . . . . . . . 21 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → 𝑠 𝑅)
7574adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → 𝑠 𝑅)
76 elpwi 4140 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 ∈ 𝒫 𝑆𝑘 𝑆)
7776ad2antrl 763 . . . . . . . . . . . . . . . . . . . 20 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → 𝑘 𝑆)
78 eldif 3565 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑡 ∈ ((𝑠 × 𝑘) ∖ 𝑥) ↔ (𝑡 ∈ (𝑠 × 𝑘) ∧ ¬ 𝑡𝑥))
7978anbi1i 730 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑡 ∈ ((𝑠 × 𝑘) ∖ 𝑥) ∧ ((2nd ↾ ( 𝑅 × 𝑆))‘𝑡) = 𝑏) ↔ ((𝑡 ∈ (𝑠 × 𝑘) ∧ ¬ 𝑡𝑥) ∧ ((2nd ↾ ( 𝑅 × 𝑆))‘𝑡) = 𝑏))
80 anass 680 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑡 ∈ (𝑠 × 𝑘) ∧ ¬ 𝑡𝑥) ∧ ((2nd ↾ ( 𝑅 × 𝑆))‘𝑡) = 𝑏) ↔ (𝑡 ∈ (𝑠 × 𝑘) ∧ (¬ 𝑡𝑥 ∧ ((2nd ↾ ( 𝑅 × 𝑆))‘𝑡) = 𝑏)))
8179, 80bitri 264 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑡 ∈ ((𝑠 × 𝑘) ∖ 𝑥) ∧ ((2nd ↾ ( 𝑅 × 𝑆))‘𝑡) = 𝑏) ↔ (𝑡 ∈ (𝑠 × 𝑘) ∧ (¬ 𝑡𝑥 ∧ ((2nd ↾ ( 𝑅 × 𝑆))‘𝑡) = 𝑏)))
8281rexbii2 3032 . . . . . . . . . . . . . . . . . . . . . . . 24 (∃𝑡 ∈ ((𝑠 × 𝑘) ∖ 𝑥)((2nd ↾ ( 𝑅 × 𝑆))‘𝑡) = 𝑏 ↔ ∃𝑡 ∈ (𝑠 × 𝑘)(¬ 𝑡𝑥 ∧ ((2nd ↾ ( 𝑅 × 𝑆))‘𝑡) = 𝑏))
83 ancom 466 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((¬ 𝑡𝑥 ∧ ((2nd ↾ ( 𝑅 × 𝑆))‘𝑡) = 𝑏) ↔ (((2nd ↾ ( 𝑅 × 𝑆))‘𝑡) = 𝑏 ∧ ¬ 𝑡𝑥))
84 fveq2 6148 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑡 = ⟨𝑎, 𝑢⟩ → ((2nd ↾ ( 𝑅 × 𝑆))‘𝑡) = ((2nd ↾ ( 𝑅 × 𝑆))‘⟨𝑎, 𝑢⟩))
8584eqeq1d 2623 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑡 = ⟨𝑎, 𝑢⟩ → (((2nd ↾ ( 𝑅 × 𝑆))‘𝑡) = 𝑏 ↔ ((2nd ↾ ( 𝑅 × 𝑆))‘⟨𝑎, 𝑢⟩) = 𝑏))
86 eleq1 2686 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑡 = ⟨𝑎, 𝑢⟩ → (𝑡𝑥 ↔ ⟨𝑎, 𝑢⟩ ∈ 𝑥))
8786notbid 308 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑡 = ⟨𝑎, 𝑢⟩ → (¬ 𝑡𝑥 ↔ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥))
8885, 87anbi12d 746 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑡 = ⟨𝑎, 𝑢⟩ → ((((2nd ↾ ( 𝑅 × 𝑆))‘𝑡) = 𝑏 ∧ ¬ 𝑡𝑥) ↔ (((2nd ↾ ( 𝑅 × 𝑆))‘⟨𝑎, 𝑢⟩) = 𝑏 ∧ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥)))
8983, 88syl5bb 272 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑡 = ⟨𝑎, 𝑢⟩ → ((¬ 𝑡𝑥 ∧ ((2nd ↾ ( 𝑅 × 𝑆))‘𝑡) = 𝑏) ↔ (((2nd ↾ ( 𝑅 × 𝑆))‘⟨𝑎, 𝑢⟩) = 𝑏 ∧ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥)))
9089rexxp 5224 . . . . . . . . . . . . . . . . . . . . . . . 24 (∃𝑡 ∈ (𝑠 × 𝑘)(¬ 𝑡𝑥 ∧ ((2nd ↾ ( 𝑅 × 𝑆))‘𝑡) = 𝑏) ↔ ∃𝑎𝑠𝑢𝑘 (((2nd ↾ ( 𝑅 × 𝑆))‘⟨𝑎, 𝑢⟩) = 𝑏 ∧ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥))
9182, 90bitri 264 . . . . . . . . . . . . . . . . . . . . . . 23 (∃𝑡 ∈ ((𝑠 × 𝑘) ∖ 𝑥)((2nd ↾ ( 𝑅 × 𝑆))‘𝑡) = 𝑏 ↔ ∃𝑎𝑠𝑢𝑘 (((2nd ↾ ( 𝑅 × 𝑆))‘⟨𝑎, 𝑢⟩) = 𝑏 ∧ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥))
92 simpl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑠 𝑅𝑘 𝑆) → 𝑠 𝑅)
9392sselda 3583 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝑠 𝑅𝑘 𝑆) ∧ 𝑎𝑠) → 𝑎 𝑅)
9493adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝑠 𝑅𝑘 𝑆) ∧ 𝑎𝑠) ∧ 𝑢𝑘) → 𝑎 𝑅)
95 simplr 791 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝑠 𝑅𝑘 𝑆) ∧ 𝑎𝑠) → 𝑘 𝑆)
9695sselda 3583 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝑠 𝑅𝑘 𝑆) ∧ 𝑎𝑠) ∧ 𝑢𝑘) → 𝑢 𝑆)
9794, 96opelxpd 5109 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝑠 𝑅𝑘 𝑆) ∧ 𝑎𝑠) ∧ 𝑢𝑘) → ⟨𝑎, 𝑢⟩ ∈ ( 𝑅 × 𝑆))
9897fvresd 6165 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝑠 𝑅𝑘 𝑆) ∧ 𝑎𝑠) ∧ 𝑢𝑘) → ((2nd ↾ ( 𝑅 × 𝑆))‘⟨𝑎, 𝑢⟩) = (2nd ‘⟨𝑎, 𝑢⟩))
99 vex 3189 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 𝑎 ∈ V
100 vex 3189 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 𝑢 ∈ V
10199, 100op2nd 7122 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (2nd ‘⟨𝑎, 𝑢⟩) = 𝑢
10298, 101syl6eq 2671 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝑠 𝑅𝑘 𝑆) ∧ 𝑎𝑠) ∧ 𝑢𝑘) → ((2nd ↾ ( 𝑅 × 𝑆))‘⟨𝑎, 𝑢⟩) = 𝑢)
103102eqeq1d 2623 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝑠 𝑅𝑘 𝑆) ∧ 𝑎𝑠) ∧ 𝑢𝑘) → (((2nd ↾ ( 𝑅 × 𝑆))‘⟨𝑎, 𝑢⟩) = 𝑏𝑢 = 𝑏))
104103anbi1d 740 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝑠 𝑅𝑘 𝑆) ∧ 𝑎𝑠) ∧ 𝑢𝑘) → ((((2nd ↾ ( 𝑅 × 𝑆))‘⟨𝑎, 𝑢⟩) = 𝑏 ∧ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥) ↔ (𝑢 = 𝑏 ∧ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥)))
105104rexbidva 3042 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑠 𝑅𝑘 𝑆) ∧ 𝑎𝑠) → (∃𝑢𝑘 (((2nd ↾ ( 𝑅 × 𝑆))‘⟨𝑎, 𝑢⟩) = 𝑏 ∧ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥) ↔ ∃𝑢𝑘 (𝑢 = 𝑏 ∧ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥)))
106 opeq2 4371 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑢 = 𝑏 → ⟨𝑎, 𝑢⟩ = ⟨𝑎, 𝑏⟩)
107106eleq1d 2683 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑢 = 𝑏 → (⟨𝑎, 𝑢⟩ ∈ 𝑥 ↔ ⟨𝑎, 𝑏⟩ ∈ 𝑥))
108107notbid 308 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑢 = 𝑏 → (¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥 ↔ ¬ ⟨𝑎, 𝑏⟩ ∈ 𝑥))
109108ceqsrexbv 3320 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (∃𝑢𝑘 (𝑢 = 𝑏 ∧ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥) ↔ (𝑏𝑘 ∧ ¬ ⟨𝑎, 𝑏⟩ ∈ 𝑥))
110105, 109syl6bb 276 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑠 𝑅𝑘 𝑆) ∧ 𝑎𝑠) → (∃𝑢𝑘 (((2nd ↾ ( 𝑅 × 𝑆))‘⟨𝑎, 𝑢⟩) = 𝑏 ∧ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥) ↔ (𝑏𝑘 ∧ ¬ ⟨𝑎, 𝑏⟩ ∈ 𝑥)))
111110rexbidva 3042 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑠 𝑅𝑘 𝑆) → (∃𝑎𝑠𝑢𝑘 (((2nd ↾ ( 𝑅 × 𝑆))‘⟨𝑎, 𝑢⟩) = 𝑏 ∧ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥) ↔ ∃𝑎𝑠 (𝑏𝑘 ∧ ¬ ⟨𝑎, 𝑏⟩ ∈ 𝑥)))
112 r19.42v 3084 . . . . . . . . . . . . . . . . . . . . . . . 24 (∃𝑎𝑠 (𝑏𝑘 ∧ ¬ ⟨𝑎, 𝑏⟩ ∈ 𝑥) ↔ (𝑏𝑘 ∧ ∃𝑎𝑠 ¬ ⟨𝑎, 𝑏⟩ ∈ 𝑥))
113111, 112syl6bb 276 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑠 𝑅𝑘 𝑆) → (∃𝑎𝑠𝑢𝑘 (((2nd ↾ ( 𝑅 × 𝑆))‘⟨𝑎, 𝑢⟩) = 𝑏 ∧ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥) ↔ (𝑏𝑘 ∧ ∃𝑎𝑠 ¬ ⟨𝑎, 𝑏⟩ ∈ 𝑥)))
11491, 113syl5bb 272 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑠 𝑅𝑘 𝑆) → (∃𝑡 ∈ ((𝑠 × 𝑘) ∖ 𝑥)((2nd ↾ ( 𝑅 × 𝑆))‘𝑡) = 𝑏 ↔ (𝑏𝑘 ∧ ∃𝑎𝑠 ¬ ⟨𝑎, 𝑏⟩ ∈ 𝑥)))
115 f2ndres 7136 . . . . . . . . . . . . . . . . . . . . . . . 24 (2nd ↾ ( 𝑅 × 𝑆)):( 𝑅 × 𝑆)⟶ 𝑆
116 ffn 6002 . . . . . . . . . . . . . . . . . . . . . . . 24 ((2nd ↾ ( 𝑅 × 𝑆)):( 𝑅 × 𝑆)⟶ 𝑆 → (2nd ↾ ( 𝑅 × 𝑆)) Fn ( 𝑅 × 𝑆))
117115, 116ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . 23 (2nd ↾ ( 𝑅 × 𝑆)) Fn ( 𝑅 × 𝑆)
118 difss 3715 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑠 × 𝑘) ∖ 𝑥) ⊆ (𝑠 × 𝑘)
119 xpss12 5186 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑠 𝑅𝑘 𝑆) → (𝑠 × 𝑘) ⊆ ( 𝑅 × 𝑆))
120118, 119syl5ss 3594 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑠 𝑅𝑘 𝑆) → ((𝑠 × 𝑘) ∖ 𝑥) ⊆ ( 𝑅 × 𝑆))
121 fvelimab 6210 . . . . . . . . . . . . . . . . . . . . . . 23 (((2nd ↾ ( 𝑅 × 𝑆)) Fn ( 𝑅 × 𝑆) ∧ ((𝑠 × 𝑘) ∖ 𝑥) ⊆ ( 𝑅 × 𝑆)) → (𝑏 ∈ ((2nd ↾ ( 𝑅 × 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ↔ ∃𝑡 ∈ ((𝑠 × 𝑘) ∖ 𝑥)((2nd ↾ ( 𝑅 × 𝑆))‘𝑡) = 𝑏))
122117, 120, 121sylancr 694 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑠 𝑅𝑘 𝑆) → (𝑏 ∈ ((2nd ↾ ( 𝑅 × 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ↔ ∃𝑡 ∈ ((𝑠 × 𝑘) ∖ 𝑥)((2nd ↾ ( 𝑅 × 𝑆))‘𝑡) = 𝑏))
123 eldif 3565 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑏 ∈ (𝑘 ∖ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ↔ (𝑏𝑘 ∧ ¬ 𝑏 ∈ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}))
124 simpr 477 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑠 𝑅𝑘 𝑆) → 𝑘 𝑆)
125124sselda 3583 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑠 𝑅𝑘 𝑆) ∧ 𝑏𝑘) → 𝑏 𝑆)
126 sneq 4158 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑣 = 𝑏 → {𝑣} = {𝑏})
127126xpeq2d 5099 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑣 = 𝑏 → (𝑠 × {𝑣}) = (𝑠 × {𝑏}))
128127sseq1d 3611 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑣 = 𝑏 → ((𝑠 × {𝑣}) ⊆ 𝑥 ↔ (𝑠 × {𝑏}) ⊆ 𝑥))
129 dfss3 3573 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑠 × {𝑏}) ⊆ 𝑥 ↔ ∀𝑘 ∈ (𝑠 × {𝑏})𝑘𝑥)
130 eleq1 2686 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑘 = ⟨𝑎, 𝑡⟩ → (𝑘𝑥 ↔ ⟨𝑎, 𝑡⟩ ∈ 𝑥))
131130ralxp 5223 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (∀𝑘 ∈ (𝑠 × {𝑏})𝑘𝑥 ↔ ∀𝑎𝑠𝑡 ∈ {𝑏}⟨𝑎, 𝑡⟩ ∈ 𝑥)
132 vex 3189 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 𝑏 ∈ V
133 opeq2 4371 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑡 = 𝑏 → ⟨𝑎, 𝑡⟩ = ⟨𝑎, 𝑏⟩)
134133eleq1d 2683 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑡 = 𝑏 → (⟨𝑎, 𝑡⟩ ∈ 𝑥 ↔ ⟨𝑎, 𝑏⟩ ∈ 𝑥))
135132, 134ralsn 4193 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (∀𝑡 ∈ {𝑏}⟨𝑎, 𝑡⟩ ∈ 𝑥 ↔ ⟨𝑎, 𝑏⟩ ∈ 𝑥)
136135ralbii 2974 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (∀𝑎𝑠𝑡 ∈ {𝑏}⟨𝑎, 𝑡⟩ ∈ 𝑥 ↔ ∀𝑎𝑠𝑎, 𝑏⟩ ∈ 𝑥)
137129, 131, 1363bitri 286 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑠 × {𝑏}) ⊆ 𝑥 ↔ ∀𝑎𝑠𝑎, 𝑏⟩ ∈ 𝑥)
138128, 137syl6bb 276 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑣 = 𝑏 → ((𝑠 × {𝑣}) ⊆ 𝑥 ↔ ∀𝑎𝑠𝑎, 𝑏⟩ ∈ 𝑥))
139138elrab3 3347 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑏 𝑆 → (𝑏 ∈ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ↔ ∀𝑎𝑠𝑎, 𝑏⟩ ∈ 𝑥))
140125, 139syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑠 𝑅𝑘 𝑆) ∧ 𝑏𝑘) → (𝑏 ∈ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ↔ ∀𝑎𝑠𝑎, 𝑏⟩ ∈ 𝑥))
141140notbid 308 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑠 𝑅𝑘 𝑆) ∧ 𝑏𝑘) → (¬ 𝑏 ∈ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ↔ ¬ ∀𝑎𝑠𝑎, 𝑏⟩ ∈ 𝑥))
142 rexnal 2989 . . . . . . . . . . . . . . . . . . . . . . . . 25 (∃𝑎𝑠 ¬ ⟨𝑎, 𝑏⟩ ∈ 𝑥 ↔ ¬ ∀𝑎𝑠𝑎, 𝑏⟩ ∈ 𝑥)
143141, 142syl6bbr 278 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑠 𝑅𝑘 𝑆) ∧ 𝑏𝑘) → (¬ 𝑏 ∈ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ↔ ∃𝑎𝑠 ¬ ⟨𝑎, 𝑏⟩ ∈ 𝑥))
144143pm5.32da 672 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑠 𝑅𝑘 𝑆) → ((𝑏𝑘 ∧ ¬ 𝑏 ∈ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ↔ (𝑏𝑘 ∧ ∃𝑎𝑠 ¬ ⟨𝑎, 𝑏⟩ ∈ 𝑥)))
145123, 144syl5bb 272 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑠 𝑅𝑘 𝑆) → (𝑏 ∈ (𝑘 ∖ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ↔ (𝑏𝑘 ∧ ∃𝑎𝑠 ¬ ⟨𝑎, 𝑏⟩ ∈ 𝑥)))
146114, 122, 1453bitr4d 300 . . . . . . . . . . . . . . . . . . . . 21 ((𝑠 𝑅𝑘 𝑆) → (𝑏 ∈ ((2nd ↾ ( 𝑅 × 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ↔ 𝑏 ∈ (𝑘 ∖ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})))
147146eqrdv 2619 . . . . . . . . . . . . . . . . . . . 20 ((𝑠 𝑅𝑘 𝑆) → ((2nd ↾ ( 𝑅 × 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) = (𝑘 ∖ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}))
14875, 77, 147syl2anc 692 . . . . . . . . . . . . . . . . . . 19 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → ((2nd ↾ ( 𝑅 × 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) = (𝑘 ∖ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}))
149 difin 3839 . . . . . . . . . . . . . . . . . . . 20 (𝑘 ∖ (𝑘 ∩ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})) = (𝑘 ∖ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})
15066adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → 𝑆 ∈ Top)
15118restuni 20876 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑆 ∈ Top ∧ 𝑘 𝑆) → 𝑘 = (𝑆t 𝑘))
152150, 77, 151syl2anc 692 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → 𝑘 = (𝑆t 𝑘))
153152difeq1d 3705 . . . . . . . . . . . . . . . . . . . 20 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → (𝑘 ∖ (𝑘 ∩ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})) = ( (𝑆t 𝑘) ∖ (𝑘 ∩ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})))
154149, 153syl5eqr 2669 . . . . . . . . . . . . . . . . . . 19 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → (𝑘 ∖ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) = ( (𝑆t 𝑘) ∖ (𝑘 ∩ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})))
155148, 154eqtrd 2655 . . . . . . . . . . . . . . . . . 18 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → ((2nd ↾ ( 𝑅 × 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) = ( (𝑆t 𝑘) ∖ (𝑘 ∩ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})))
15616ad2antrr 761 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → 𝑆 ∈ (ran 𝑘Gen ∩ Haus))
157156elin2d 3781 . . . . . . . . . . . . . . . . . . . 20 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → 𝑆 ∈ Haus)
158 df-ima 5087 . . . . . . . . . . . . . . . . . . . . . . 23 ((2nd ↾ ( 𝑅 × 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) = ran ((2nd ↾ ( 𝑅 × 𝑆)) ↾ ((𝑠 × 𝑘) ∖ 𝑥))
159 resres 5368 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((2nd ↾ ( 𝑅 × 𝑆)) ↾ ((𝑠 × 𝑘) ∖ 𝑥)) = (2nd ↾ (( 𝑅 × 𝑆) ∩ ((𝑠 × 𝑘) ∖ 𝑥)))
160 inss2 3812 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (( 𝑅 × 𝑆) ∩ ((𝑠 × 𝑘) ∖ 𝑥)) ⊆ ((𝑠 × 𝑘) ∖ 𝑥)
161160, 118sstri 3592 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (( 𝑅 × 𝑆) ∩ ((𝑠 × 𝑘) ∖ 𝑥)) ⊆ (𝑠 × 𝑘)
162 ssres2 5384 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((( 𝑅 × 𝑆) ∩ ((𝑠 × 𝑘) ∖ 𝑥)) ⊆ (𝑠 × 𝑘) → (2nd ↾ (( 𝑅 × 𝑆) ∩ ((𝑠 × 𝑘) ∖ 𝑥))) ⊆ (2nd ↾ (𝑠 × 𝑘)))
163161, 162ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . 25 (2nd ↾ (( 𝑅 × 𝑆) ∩ ((𝑠 × 𝑘) ∖ 𝑥))) ⊆ (2nd ↾ (𝑠 × 𝑘))
164159, 163eqsstri 3614 . . . . . . . . . . . . . . . . . . . . . . . 24 ((2nd ↾ ( 𝑅 × 𝑆)) ↾ ((𝑠 × 𝑘) ∖ 𝑥)) ⊆ (2nd ↾ (𝑠 × 𝑘))
165 rnss 5314 . . . . . . . . . . . . . . . . . . . . . . . 24 (((2nd ↾ ( 𝑅 × 𝑆)) ↾ ((𝑠 × 𝑘) ∖ 𝑥)) ⊆ (2nd ↾ (𝑠 × 𝑘)) → ran ((2nd ↾ ( 𝑅 × 𝑆)) ↾ ((𝑠 × 𝑘) ∖ 𝑥)) ⊆ ran (2nd ↾ (𝑠 × 𝑘)))
166164, 165ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . 23 ran ((2nd ↾ ( 𝑅 × 𝑆)) ↾ ((𝑠 × 𝑘) ∖ 𝑥)) ⊆ ran (2nd ↾ (𝑠 × 𝑘))
167158, 166eqsstri 3614 . . . . . . . . . . . . . . . . . . . . . 22 ((2nd ↾ ( 𝑅 × 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ⊆ ran (2nd ↾ (𝑠 × 𝑘))
168 f2ndres 7136 . . . . . . . . . . . . . . . . . . . . . . 23 (2nd ↾ (𝑠 × 𝑘)):(𝑠 × 𝑘)⟶𝑘
169 frn 6010 . . . . . . . . . . . . . . . . . . . . . . 23 ((2nd ↾ (𝑠 × 𝑘)):(𝑠 × 𝑘)⟶𝑘 → ran (2nd ↾ (𝑠 × 𝑘)) ⊆ 𝑘)
170168, 169ax-mp 5 . . . . . . . . . . . . . . . . . . . . . 22 ran (2nd ↾ (𝑠 × 𝑘)) ⊆ 𝑘
171167, 170sstri 3592 . . . . . . . . . . . . . . . . . . . . 21 ((2nd ↾ ( 𝑅 × 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ⊆ 𝑘
172171, 77syl5ss 3594 . . . . . . . . . . . . . . . . . . . 20 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → ((2nd ↾ ( 𝑅 × 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ⊆ 𝑆)
17313ad2antrr 761 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → 𝑅 ∈ (TopOn‘ 𝑅))
174150, 19sylib 208 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → 𝑆 ∈ (TopOn‘ 𝑆))
175 tx2cn 21323 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑅 ∈ (TopOn‘ 𝑅) ∧ 𝑆 ∈ (TopOn‘ 𝑆)) → (2nd ↾ ( 𝑅 × 𝑆)) ∈ ((𝑅 ×t 𝑆) Cn 𝑆))
176173, 174, 175syl2anc 692 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → (2nd ↾ ( 𝑅 × 𝑆)) ∈ ((𝑅 ×t 𝑆) Cn 𝑆))
17727ad2antrr 761 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → (𝑅 ×t 𝑆) ∈ Top)
178118a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → ((𝑠 × 𝑘) ∖ 𝑥) ⊆ (𝑠 × 𝑘))
179 vex 3189 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑠 ∈ V
180 vex 3189 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑘 ∈ V
181179, 180xpex 6915 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑠 × 𝑘) ∈ V
182181a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → (𝑠 × 𝑘) ∈ V)
183 restabs 20879 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑅 ×t 𝑆) ∈ Top ∧ ((𝑠 × 𝑘) ∖ 𝑥) ⊆ (𝑠 × 𝑘) ∧ (𝑠 × 𝑘) ∈ V) → (((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ↾t ((𝑠 × 𝑘) ∖ 𝑥)) = ((𝑅 ×t 𝑆) ↾t ((𝑠 × 𝑘) ∖ 𝑥)))
184177, 178, 182, 183syl3anc 1323 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → (((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ↾t ((𝑠 × 𝑘) ∖ 𝑥)) = ((𝑅 ×t 𝑆) ↾t ((𝑠 × 𝑘) ∖ 𝑥)))
18565adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → 𝑅 ∈ Top)
186156, 4syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → 𝑆 ∈ Top)
187179a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → 𝑠 ∈ V)
188 simprl 793 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → 𝑘 ∈ 𝒫 𝑆)
189 txrest 21344 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑠 ∈ V ∧ 𝑘 ∈ 𝒫 𝑆)) → ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) = ((𝑅t 𝑠) ×t (𝑆t 𝑘)))
190185, 186, 187, 188, 189syl22anc 1324 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) = ((𝑅t 𝑠) ×t (𝑆t 𝑘)))
191 simprr3 1109 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → (𝑅t 𝑠) ∈ Comp)
192191adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → (𝑅t 𝑠) ∈ Comp)
193 simprr 795 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → (𝑆t 𝑘) ∈ Comp)
194 txcmp 21356 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑅t 𝑠) ∈ Comp ∧ (𝑆t 𝑘) ∈ Comp) → ((𝑅t 𝑠) ×t (𝑆t 𝑘)) ∈ Comp)
195192, 193, 194syl2anc 692 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → ((𝑅t 𝑠) ×t (𝑆t 𝑘)) ∈ Comp)
196190, 195eqeltrd 2698 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ∈ Comp)
197 difin 3839 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑠 × 𝑘) ∖ ((𝑠 × 𝑘) ∩ 𝑥)) = ((𝑠 × 𝑘) ∖ 𝑥)
19875, 77, 119syl2anc 692 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → (𝑠 × 𝑘) ⊆ ( 𝑅 × 𝑆))
199185, 150, 25syl2anc 692 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → ( 𝑅 × 𝑆) = (𝑅 ×t 𝑆))
200198, 199sseqtrd 3620 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → (𝑠 × 𝑘) ⊆ (𝑅 ×t 𝑆))
20128restuni 20876 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑅 ×t 𝑆) ∈ Top ∧ (𝑠 × 𝑘) ⊆ (𝑅 ×t 𝑆)) → (𝑠 × 𝑘) = ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)))
202177, 200, 201syl2anc 692 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → (𝑠 × 𝑘) = ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)))
203202difeq1d 3705 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → ((𝑠 × 𝑘) ∖ ((𝑠 × 𝑘) ∩ 𝑥)) = ( ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ∖ ((𝑠 × 𝑘) ∩ 𝑥)))
204197, 203syl5eqr 2669 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → ((𝑠 × 𝑘) ∖ 𝑥) = ( ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ∖ ((𝑠 × 𝑘) ∩ 𝑥)))
205 resttop 20874 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑅 ×t 𝑆) ∈ Top ∧ (𝑠 × 𝑘) ∈ V) → ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ∈ Top)
206177, 181, 205sylancl 693 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ∈ Top)
207 incom 3783 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑠 × 𝑘) ∩ 𝑥) = (𝑥 ∩ (𝑠 × 𝑘))
20822ad2antrr 761 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆)))
209 kgeni 21250 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆)) ∧ ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ∈ Comp) → (𝑥 ∩ (𝑠 × 𝑘)) ∈ ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)))
210208, 196, 209syl2anc 692 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → (𝑥 ∩ (𝑠 × 𝑘)) ∈ ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)))
211207, 210syl5eqel 2702 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → ((𝑠 × 𝑘) ∩ 𝑥) ∈ ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)))
212 eqid 2621 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) = ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘))
213212opncld 20747 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ∈ Top ∧ ((𝑠 × 𝑘) ∩ 𝑥) ∈ ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘))) → ( ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ∖ ((𝑠 × 𝑘) ∩ 𝑥)) ∈ (Clsd‘((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘))))
214206, 211, 213syl2anc 692 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → ( ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ∖ ((𝑠 × 𝑘) ∩ 𝑥)) ∈ (Clsd‘((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘))))
215204, 214eqeltrd 2698 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → ((𝑠 × 𝑘) ∖ 𝑥) ∈ (Clsd‘((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘))))
216 cmpcld 21115 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ∈ Comp ∧ ((𝑠 × 𝑘) ∖ 𝑥) ∈ (Clsd‘((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)))) → (((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ↾t ((𝑠 × 𝑘) ∖ 𝑥)) ∈ Comp)
217196, 215, 216syl2anc 692 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → (((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ↾t ((𝑠 × 𝑘) ∖ 𝑥)) ∈ Comp)
218184, 217eqeltrrd 2699 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → ((𝑅 ×t 𝑆) ↾t ((𝑠 × 𝑘) ∖ 𝑥)) ∈ Comp)
219 imacmp 21110 . . . . . . . . . . . . . . . . . . . . 21 (((2nd ↾ ( 𝑅 × 𝑆)) ∈ ((𝑅 ×t 𝑆) Cn 𝑆) ∧ ((𝑅 ×t 𝑆) ↾t ((𝑠 × 𝑘) ∖ 𝑥)) ∈ Comp) → (𝑆t ((2nd ↾ ( 𝑅 × 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥))) ∈ Comp)
220176, 218, 219syl2anc 692 . . . . . . . . . . . . . . . . . . . 20 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → (𝑆t ((2nd ↾ ( 𝑅 × 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥))) ∈ Comp)
22118hauscmp 21120 . . . . . . . . . . . . . . . . . . . 20 ((𝑆 ∈ Haus ∧ ((2nd ↾ ( 𝑅 × 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ⊆ 𝑆 ∧ (𝑆t ((2nd ↾ ( 𝑅 × 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥))) ∈ Comp) → ((2nd ↾ ( 𝑅 × 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ∈ (Clsd‘𝑆))
222157, 172, 220, 221syl3anc 1323 . . . . . . . . . . . . . . . . . . 19 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → ((2nd ↾ ( 𝑅 × 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ∈ (Clsd‘𝑆))
223171a1i 11 . . . . . . . . . . . . . . . . . . 19 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → ((2nd ↾ ( 𝑅 × 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ⊆ 𝑘)
22418restcldi 20887 . . . . . . . . . . . . . . . . . . 19 ((𝑘 𝑆 ∧ ((2nd ↾ ( 𝑅 × 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ∈ (Clsd‘𝑆) ∧ ((2nd ↾ ( 𝑅 × 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ⊆ 𝑘) → ((2nd ↾ ( 𝑅 × 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ∈ (Clsd‘(𝑆t 𝑘)))
22577, 222, 223, 224syl3anc 1323 . . . . . . . . . . . . . . . . . 18 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → ((2nd ↾ ( 𝑅 × 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ∈ (Clsd‘(𝑆t 𝑘)))
226155, 225eqeltrrd 2699 . . . . . . . . . . . . . . . . 17 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → ( (𝑆t 𝑘) ∖ (𝑘 ∩ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})) ∈ (Clsd‘(𝑆t 𝑘)))
227 resttop 20874 . . . . . . . . . . . . . . . . . . 19 ((𝑆 ∈ Top ∧ 𝑘 ∈ 𝒫 𝑆) → (𝑆t 𝑘) ∈ Top)
228150, 188, 227syl2anc 692 . . . . . . . . . . . . . . . . . 18 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → (𝑆t 𝑘) ∈ Top)
229 inss1 3811 . . . . . . . . . . . . . . . . . . 19 (𝑘 ∩ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ⊆ 𝑘
230229, 152syl5sseq 3632 . . . . . . . . . . . . . . . . . 18 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → (𝑘 ∩ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ⊆ (𝑆t 𝑘))
231 eqid 2621 . . . . . . . . . . . . . . . . . . 19 (𝑆t 𝑘) = (𝑆t 𝑘)
232231isopn2 20746 . . . . . . . . . . . . . . . . . 18 (((𝑆t 𝑘) ∈ Top ∧ (𝑘 ∩ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ⊆ (𝑆t 𝑘)) → ((𝑘 ∩ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ∈ (𝑆t 𝑘) ↔ ( (𝑆t 𝑘) ∖ (𝑘 ∩ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})) ∈ (Clsd‘(𝑆t 𝑘))))
233228, 230, 232syl2anc 692 . . . . . . . . . . . . . . . . 17 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → ((𝑘 ∩ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ∈ (𝑆t 𝑘) ↔ ( (𝑆t 𝑘) ∖ (𝑘 ∩ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})) ∈ (Clsd‘(𝑆t 𝑘))))
234226, 233mpbird 247 . . . . . . . . . . . . . . . 16 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → (𝑘 ∩ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ∈ (𝑆t 𝑘))
23570, 234syl5eqel 2702 . . . . . . . . . . . . . . 15 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → ({𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ∩ 𝑘) ∈ (𝑆t 𝑘))
236235expr 642 . . . . . . . . . . . . . 14 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ 𝑘 ∈ 𝒫 𝑆) → ((𝑆t 𝑘) ∈ Comp → ({𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ∩ 𝑘) ∈ (𝑆t 𝑘)))
237236ralrimiva 2960 . . . . . . . . . . . . 13 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → ∀𝑘 ∈ 𝒫 𝑆((𝑆t 𝑘) ∈ Comp → ({𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ∩ 𝑘) ∈ (𝑆t 𝑘)))
23866, 19sylib 208 . . . . . . . . . . . . . 14 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → 𝑆 ∈ (TopOn‘ 𝑆))
239 elkgen 21249 . . . . . . . . . . . . . 14 (𝑆 ∈ (TopOn‘ 𝑆) → ({𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ∈ (𝑘Gen‘𝑆) ↔ ({𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ⊆ 𝑆 ∧ ∀𝑘 ∈ 𝒫 𝑆((𝑆t 𝑘) ∈ Comp → ({𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ∩ 𝑘) ∈ (𝑆t 𝑘)))))
240238, 239syl 17 . . . . . . . . . . . . 13 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → ({𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ∈ (𝑘Gen‘𝑆) ↔ ({𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ⊆ 𝑆 ∧ ∀𝑘 ∈ 𝒫 𝑆((𝑆t 𝑘) ∈ Comp → ({𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ∩ 𝑘) ∈ (𝑆t 𝑘)))))
24169, 237, 240mpbir2and 956 . . . . . . . . . . . 12 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ∈ (𝑘Gen‘𝑆))
24216adantr 481 . . . . . . . . . . . . . 14 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → 𝑆 ∈ (ran 𝑘Gen ∩ Haus))
243242, 2syl 17 . . . . . . . . . . . . 13 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → 𝑆 ∈ ran 𝑘Gen)
244 kgenidm 21260 . . . . . . . . . . . . 13 (𝑆 ∈ ran 𝑘Gen → (𝑘Gen‘𝑆) = 𝑆)
245243, 244syl 17 . . . . . . . . . . . 12 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → (𝑘Gen‘𝑆) = 𝑆)
246241, 245eleqtrd 2700 . . . . . . . . . . 11 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ∈ 𝑆)
247 txopn 21315 . . . . . . . . . . 11 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑢𝑅 ∧ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ∈ 𝑆)) → (𝑢 × {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ∈ (𝑅 ×t 𝑆))
24865, 66, 67, 246, 247syl22anc 1324 . . . . . . . . . 10 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → (𝑢 × {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ∈ (𝑅 ×t 𝑆))
24957adantr 481 . . . . . . . . . . 11 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → 𝑦 = ⟨(1st𝑦), (2nd𝑦)⟩)
250 simprr1 1107 . . . . . . . . . . . 12 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → (1st𝑦) ∈ 𝑢)
25134adantr 481 . . . . . . . . . . . . 13 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → (2nd𝑦) ∈ 𝑆)
252 relxp 5188 . . . . . . . . . . . . . . 15 Rel (𝑠 × {(2nd𝑦)})
253252a1i 11 . . . . . . . . . . . . . 14 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → Rel (𝑠 × {(2nd𝑦)}))
254 opelxp 5106 . . . . . . . . . . . . . . 15 (⟨𝑎, 𝑏⟩ ∈ (𝑠 × {(2nd𝑦)}) ↔ (𝑎𝑠𝑏 ∈ {(2nd𝑦)}))
25572sselda 3583 . . . . . . . . . . . . . . . . . 18 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ 𝑎𝑠) → 𝑎 ∈ {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥})
256 opeq1 4370 . . . . . . . . . . . . . . . . . . . . 21 (𝑡 = 𝑎 → ⟨𝑡, (2nd𝑦)⟩ = ⟨𝑎, (2nd𝑦)⟩)
257256eleq1d 2683 . . . . . . . . . . . . . . . . . . . 20 (𝑡 = 𝑎 → (⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥 ↔ ⟨𝑎, (2nd𝑦)⟩ ∈ 𝑥))
258257elrab 3346 . . . . . . . . . . . . . . . . . . 19 (𝑎 ∈ {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ↔ (𝑎 𝑅 ∧ ⟨𝑎, (2nd𝑦)⟩ ∈ 𝑥))
259258simprbi 480 . . . . . . . . . . . . . . . . . 18 (𝑎 ∈ {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} → ⟨𝑎, (2nd𝑦)⟩ ∈ 𝑥)
260255, 259syl 17 . . . . . . . . . . . . . . . . 17 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ 𝑎𝑠) → ⟨𝑎, (2nd𝑦)⟩ ∈ 𝑥)
261 elsni 4165 . . . . . . . . . . . . . . . . . . 19 (𝑏 ∈ {(2nd𝑦)} → 𝑏 = (2nd𝑦))
262261opeq2d 4377 . . . . . . . . . . . . . . . . . 18 (𝑏 ∈ {(2nd𝑦)} → ⟨𝑎, 𝑏⟩ = ⟨𝑎, (2nd𝑦)⟩)
263262eleq1d 2683 . . . . . . . . . . . . . . . . 17 (𝑏 ∈ {(2nd𝑦)} → (⟨𝑎, 𝑏⟩ ∈ 𝑥 ↔ ⟨𝑎, (2nd𝑦)⟩ ∈ 𝑥))
264260, 263syl5ibrcom 237 . . . . . . . . . . . . . . . 16 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ 𝑎𝑠) → (𝑏 ∈ {(2nd𝑦)} → ⟨𝑎, 𝑏⟩ ∈ 𝑥))
265264expimpd 628 . . . . . . . . . . . . . . 15 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → ((𝑎𝑠𝑏 ∈ {(2nd𝑦)}) → ⟨𝑎, 𝑏⟩ ∈ 𝑥))
266254, 265syl5bi 232 . . . . . . . . . . . . . 14 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → (⟨𝑎, 𝑏⟩ ∈ (𝑠 × {(2nd𝑦)}) → ⟨𝑎, 𝑏⟩ ∈ 𝑥))
267253, 266relssdv 5173 . . . . . . . . . . . . 13 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → (𝑠 × {(2nd𝑦)}) ⊆ 𝑥)
268 sneq 4158 . . . . . . . . . . . . . . . 16 (𝑣 = (2nd𝑦) → {𝑣} = {(2nd𝑦)})
269268xpeq2d 5099 . . . . . . . . . . . . . . 15 (𝑣 = (2nd𝑦) → (𝑠 × {𝑣}) = (𝑠 × {(2nd𝑦)}))
270269sseq1d 3611 . . . . . . . . . . . . . 14 (𝑣 = (2nd𝑦) → ((𝑠 × {𝑣}) ⊆ 𝑥 ↔ (𝑠 × {(2nd𝑦)}) ⊆ 𝑥))
271270elrab 3346 . . . . . . . . . . . . 13 ((2nd𝑦) ∈ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ↔ ((2nd𝑦) ∈ 𝑆 ∧ (𝑠 × {(2nd𝑦)}) ⊆ 𝑥))
272251, 267, 271sylanbrc 697 . . . . . . . . . . . 12 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → (2nd𝑦) ∈ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})
273250, 272opelxpd 5109 . . . . . . . . . . 11 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → ⟨(1st𝑦), (2nd𝑦)⟩ ∈ (𝑢 × {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}))
274249, 273eqeltrd 2698 . . . . . . . . . 10 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → 𝑦 ∈ (𝑢 × {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}))
275 relxp 5188 . . . . . . . . . . . 12 Rel (𝑢 × {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})
276275a1i 11 . . . . . . . . . . 11 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → Rel (𝑢 × {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}))
277 opelxp 5106 . . . . . . . . . . . 12 (⟨𝑎, 𝑏⟩ ∈ (𝑢 × {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ↔ (𝑎𝑢𝑏 ∈ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}))
278128elrab 3346 . . . . . . . . . . . . . . 15 (𝑏 ∈ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ↔ (𝑏 𝑆 ∧ (𝑠 × {𝑏}) ⊆ 𝑥))
279278simprbi 480 . . . . . . . . . . . . . 14 (𝑏 ∈ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} → (𝑠 × {𝑏}) ⊆ 𝑥)
280 simprr2 1108 . . . . . . . . . . . . . . . 16 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → 𝑢𝑠)
281280sselda 3583 . . . . . . . . . . . . . . 15 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ 𝑎𝑢) → 𝑎𝑠)
282 vsnid 4180 . . . . . . . . . . . . . . 15 𝑏 ∈ {𝑏}
283 opelxpi 5108 . . . . . . . . . . . . . . 15 ((𝑎𝑠𝑏 ∈ {𝑏}) → ⟨𝑎, 𝑏⟩ ∈ (𝑠 × {𝑏}))
284281, 282, 283sylancl 693 . . . . . . . . . . . . . 14 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ 𝑎𝑢) → ⟨𝑎, 𝑏⟩ ∈ (𝑠 × {𝑏}))
285 ssel 3577 . . . . . . . . . . . . . 14 ((𝑠 × {𝑏}) ⊆ 𝑥 → (⟨𝑎, 𝑏⟩ ∈ (𝑠 × {𝑏}) → ⟨𝑎, 𝑏⟩ ∈ 𝑥))
286279, 284, 285syl2imc 41 . . . . . . . . . . . . 13 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ 𝑎𝑢) → (𝑏 ∈ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} → ⟨𝑎, 𝑏⟩ ∈ 𝑥))
287286expimpd 628 . . . . . . . . . . . 12 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → ((𝑎𝑢𝑏 ∈ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) → ⟨𝑎, 𝑏⟩ ∈ 𝑥))
288277, 287syl5bi 232 . . . . . . . . . . 11 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → (⟨𝑎, 𝑏⟩ ∈ (𝑢 × {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) → ⟨𝑎, 𝑏⟩ ∈ 𝑥))
289276, 288relssdv 5173 . . . . . . . . . 10 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → (𝑢 × {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ⊆ 𝑥)
290 eleq2 2687 . . . . . . . . . . . 12 (𝑡 = (𝑢 × {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) → (𝑦𝑡𝑦 ∈ (𝑢 × {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})))
291 sseq1 3605 . . . . . . . . . . . 12 (𝑡 = (𝑢 × {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) → (𝑡𝑥 ↔ (𝑢 × {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ⊆ 𝑥))
292290, 291anbi12d 746 . . . . . . . . . . 11 (𝑡 = (𝑢 × {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) → ((𝑦𝑡𝑡𝑥) ↔ (𝑦 ∈ (𝑢 × {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ∧ (𝑢 × {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ⊆ 𝑥)))
293292rspcev 3295 . . . . . . . . . 10 (((𝑢 × {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ∈ (𝑅 ×t 𝑆) ∧ (𝑦 ∈ (𝑢 × {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ∧ (𝑢 × {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ⊆ 𝑥)) → ∃𝑡 ∈ (𝑅 ×t 𝑆)(𝑦𝑡𝑡𝑥))
294248, 274, 289, 293syl12anc 1321 . . . . . . . . 9 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → ∃𝑡 ∈ (𝑅 ×t 𝑆)(𝑦𝑡𝑡𝑥))
295294expr 642 . . . . . . . 8 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ (𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅)) → (((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp) → ∃𝑡 ∈ (𝑅 ×t 𝑆)(𝑦𝑡𝑡𝑥)))
296295rexlimdvva 3031 . . . . . . 7 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → (∃𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥}∃𝑢𝑅 ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp) → ∃𝑡 ∈ (𝑅 ×t 𝑆)(𝑦𝑡𝑡𝑥)))
29764, 296mpd 15 . . . . . 6 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → ∃𝑡 ∈ (𝑅 ×t 𝑆)(𝑦𝑡𝑡𝑥))
298297ralrimiva 2960 . . . . 5 (((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) → ∀𝑦𝑥𝑡 ∈ (𝑅 ×t 𝑆)(𝑦𝑡𝑡𝑥))
2996adantr 481 . . . . . 6 (((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) → (𝑅 ×t 𝑆) ∈ Top)
300 eltop2 20690 . . . . . 6 ((𝑅 ×t 𝑆) ∈ Top → (𝑥 ∈ (𝑅 ×t 𝑆) ↔ ∀𝑦𝑥𝑡 ∈ (𝑅 ×t 𝑆)(𝑦𝑡𝑡𝑥)))
301299, 300syl 17 . . . . 5 (((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) → (𝑥 ∈ (𝑅 ×t 𝑆) ↔ ∀𝑦𝑥𝑡 ∈ (𝑅 ×t 𝑆)(𝑦𝑡𝑡𝑥)))
302298, 301mpbird 247 . . . 4 (((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) → 𝑥 ∈ (𝑅 ×t 𝑆))
303302ex 450 . . 3 ((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) → (𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆)) → 𝑥 ∈ (𝑅 ×t 𝑆)))
304303ssrdv 3589 . 2 ((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) → (𝑘Gen‘(𝑅 ×t 𝑆)) ⊆ (𝑅 ×t 𝑆))
305 iskgen2 21261 . 2 ((𝑅 ×t 𝑆) ∈ ran 𝑘Gen ↔ ((𝑅 ×t 𝑆) ∈ Top ∧ (𝑘Gen‘(𝑅 ×t 𝑆)) ⊆ (𝑅 ×t 𝑆)))
3066, 304, 305sylanbrc 697 1 ((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) → (𝑅 ×t 𝑆) ∈ ran 𝑘Gen)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 384  w3a 1036   = wceq 1480  wcel 1987  wral 2907  wrex 2908  {crab 2911  Vcvv 3186  cdif 3552  cin 3554  wss 3555  𝒫 cpw 4130  {csn 4148  cop 4154   cuni 4402  cmpt 4673   I cid 4984   × cxp 5072  ccnv 5073  ran crn 5075  cres 5076  cima 5077  Rel wrel 5079   Fn wfn 5842  wf 5843  cfv 5847  (class class class)co 6604  1st c1st 7111  2nd c2nd 7112  t crest 16002  Topctop 20617  TopOnctopon 20618  Clsdccld 20730   Cn ccn 20938  Hauscha 21022  Compccmp 21099  𝑛-Locally cnlly 21178  𝑘Genckgen 21246   ×t ctx 21273
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4731  ax-sep 4741  ax-nul 4749  ax-pow 4803  ax-pr 4867  ax-un 6902
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-reu 2914  df-rab 2916  df-v 3188  df-sbc 3418  df-csb 3515  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-pss 3571  df-nul 3892  df-if 4059  df-pw 4132  df-sn 4149  df-pr 4151  df-tp 4153  df-op 4155  df-uni 4403  df-int 4441  df-iun 4487  df-iin 4488  df-br 4614  df-opab 4674  df-mpt 4675  df-tr 4713  df-eprel 4985  df-id 4989  df-po 4995  df-so 4996  df-fr 5033  df-we 5035  df-xp 5080  df-rel 5081  df-cnv 5082  df-co 5083  df-dm 5084  df-rn 5085  df-res 5086  df-ima 5087  df-pred 5639  df-ord 5685  df-on 5686  df-lim 5687  df-suc 5688  df-iota 5810  df-fun 5849  df-fn 5850  df-f 5851  df-f1 5852  df-fo 5853  df-f1o 5854  df-fv 5855  df-ov 6607  df-oprab 6608  df-mpt2 6609  df-om 7013  df-1st 7113  df-2nd 7114  df-wrecs 7352  df-recs 7413  df-rdg 7451  df-1o 7505  df-oadd 7509  df-er 7687  df-map 7804  df-en 7900  df-dom 7901  df-fin 7903  df-fi 8261  df-rest 16004  df-topgen 16025  df-top 20621  df-bases 20622  df-topon 20623  df-cld 20733  df-ntr 20734  df-cls 20735  df-nei 20812  df-cn 20941  df-cnp 20942  df-haus 21029  df-cmp 21100  df-nlly 21180  df-kgen 21247  df-tx 21275
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator