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

Theorem txkgen 21677
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 21498 . . 3 (𝑅 ∈ 𝑛-Locally Comp → 𝑅 ∈ Top)
2 elinel1 3942 . . . 4 (𝑆 ∈ (ran 𝑘Gen ∩ Haus) → 𝑆 ∈ ran 𝑘Gen)
3 kgentop 21567 . . . 4 (𝑆 ∈ ran 𝑘Gen → 𝑆 ∈ Top)
42, 3syl 17 . . 3 (𝑆 ∈ (ran 𝑘Gen ∩ Haus) → 𝑆 ∈ Top)
5 txtop 21594 . . 3 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑅 ×t 𝑆) ∈ Top)
61, 4, 5syl2an 495 . 2 ((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) → (𝑅 ×t 𝑆) ∈ Top)
7 simplll 815 . . . . . . . 8 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → 𝑅 ∈ 𝑛-Locally Comp)
8 eqid 2760 . . . . . . . . . 10 (𝑡 𝑅 ↦ ⟨𝑡, (2nd𝑦)⟩) = (𝑡 𝑅 ↦ ⟨𝑡, (2nd𝑦)⟩)
98mptpreima 5789 . . . . . . . . 9 ((𝑡 𝑅 ↦ ⟨𝑡, (2nd𝑦)⟩) “ 𝑥) = {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥}
101ad3antrrr 768 . . . . . . . . . . . . . 14 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → 𝑅 ∈ Top)
11 eqid 2760 . . . . . . . . . . . . . . 15 𝑅 = 𝑅
1211toptopon 20944 . . . . . . . . . . . . . 14 (𝑅 ∈ Top ↔ 𝑅 ∈ (TopOn‘ 𝑅))
1310, 12sylib 208 . . . . . . . . . . . . 13 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → 𝑅 ∈ (TopOn‘ 𝑅))
14 idcn 21283 . . . . . . . . . . . . 13 (𝑅 ∈ (TopOn‘ 𝑅) → ( I ↾ 𝑅) ∈ (𝑅 Cn 𝑅))
1513, 14syl 17 . . . . . . . . . . . 12 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → ( I ↾ 𝑅) ∈ (𝑅 Cn 𝑅))
16 simpllr 817 . . . . . . . . . . . . . . 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 2760 . . . . . . . . . . . . . . 15 𝑆 = 𝑆
1918toptopon 20944 . . . . . . . . . . . . . 14 (𝑆 ∈ Top ↔ 𝑆 ∈ (TopOn‘ 𝑆))
2017, 19sylib 208 . . . . . . . . . . . . 13 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → 𝑆 ∈ (TopOn‘ 𝑆))
21 simpr 479 . . . . . . . . . . . . . . . 16 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → 𝑦𝑥)
22 simplr 809 . . . . . . . . . . . . . . . 16 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆)))
23 elunii 4593 . . . . . . . . . . . . . . . 16 ((𝑦𝑥𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) → 𝑦 (𝑘Gen‘(𝑅 ×t 𝑆)))
2421, 22, 23syl2anc 696 . . . . . . . . . . . . . . 15 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → 𝑦 (𝑘Gen‘(𝑅 ×t 𝑆)))
2511, 18txuni 21617 . . . . . . . . . . . . . . . . 17 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → ( 𝑅 × 𝑆) = (𝑅 ×t 𝑆))
2610, 17, 25syl2anc 696 . . . . . . . . . . . . . . . 16 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → ( 𝑅 × 𝑆) = (𝑅 ×t 𝑆))
2710, 17, 5syl2anc 696 . . . . . . . . . . . . . . . . 17 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → (𝑅 ×t 𝑆) ∈ Top)
28 eqid 2760 . . . . . . . . . . . . . . . . . 18 (𝑅 ×t 𝑆) = (𝑅 ×t 𝑆)
2928kgenuni 21564 . . . . . . . . . . . . . . . . 17 ((𝑅 ×t 𝑆) ∈ Top → (𝑅 ×t 𝑆) = (𝑘Gen‘(𝑅 ×t 𝑆)))
3027, 29syl 17 . . . . . . . . . . . . . . . 16 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → (𝑅 ×t 𝑆) = (𝑘Gen‘(𝑅 ×t 𝑆)))
3126, 30eqtrd 2794 . . . . . . . . . . . . . . 15 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → ( 𝑅 × 𝑆) = (𝑘Gen‘(𝑅 ×t 𝑆)))
3224, 31eleqtrrd 2842 . . . . . . . . . . . . . 14 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → 𝑦 ∈ ( 𝑅 × 𝑆))
33 xp2nd 7367 . . . . . . . . . . . . . 14 (𝑦 ∈ ( 𝑅 × 𝑆) → (2nd𝑦) ∈ 𝑆)
3432, 33syl 17 . . . . . . . . . . . . 13 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → (2nd𝑦) ∈ 𝑆)
35 cnconst2 21309 . . . . . . . . . . . . 13 ((𝑅 ∈ (TopOn‘ 𝑅) ∧ 𝑆 ∈ (TopOn‘ 𝑆) ∧ (2nd𝑦) ∈ 𝑆) → ( 𝑅 × {(2nd𝑦)}) ∈ (𝑅 Cn 𝑆))
3613, 20, 34, 35syl3anc 1477 . . . . . . . . . . . 12 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → ( 𝑅 × {(2nd𝑦)}) ∈ (𝑅 Cn 𝑆))
37 fvresi 6604 . . . . . . . . . . . . . . . 16 (𝑡 𝑅 → (( I ↾ 𝑅)‘𝑡) = 𝑡)
38 fvex 6363 . . . . . . . . . . . . . . . . 17 (2nd𝑦) ∈ V
3938fvconst2 6634 . . . . . . . . . . . . . . . 16 (𝑡 𝑅 → (( 𝑅 × {(2nd𝑦)})‘𝑡) = (2nd𝑦))
4037, 39opeq12d 4561 . . . . . . . . . . . . . . 15 (𝑡 𝑅 → ⟨(( I ↾ 𝑅)‘𝑡), (( 𝑅 × {(2nd𝑦)})‘𝑡)⟩ = ⟨𝑡, (2nd𝑦)⟩)
4140mpteq2ia 4892 . . . . . . . . . . . . . 14 (𝑡 𝑅 ↦ ⟨(( I ↾ 𝑅)‘𝑡), (( 𝑅 × {(2nd𝑦)})‘𝑡)⟩) = (𝑡 𝑅 ↦ ⟨𝑡, (2nd𝑦)⟩)
4241eqcomi 2769 . . . . . . . . . . . . 13 (𝑡 𝑅 ↦ ⟨𝑡, (2nd𝑦)⟩) = (𝑡 𝑅 ↦ ⟨(( I ↾ 𝑅)‘𝑡), (( 𝑅 × {(2nd𝑦)})‘𝑡)⟩)
4311, 42txcnmpt 21649 . . . . . . . . . . . 12 ((( I ↾ 𝑅) ∈ (𝑅 Cn 𝑅) ∧ ( 𝑅 × {(2nd𝑦)}) ∈ (𝑅 Cn 𝑆)) → (𝑡 𝑅 ↦ ⟨𝑡, (2nd𝑦)⟩) ∈ (𝑅 Cn (𝑅 ×t 𝑆)))
4415, 36, 43syl2anc 696 . . . . . . . . . . 11 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → (𝑡 𝑅 ↦ ⟨𝑡, (2nd𝑦)⟩) ∈ (𝑅 Cn (𝑅 ×t 𝑆)))
45 llycmpkgen 21577 . . . . . . . . . . . . 13 (𝑅 ∈ 𝑛-Locally Comp → 𝑅 ∈ ran 𝑘Gen)
4645ad3antrrr 768 . . . . . . . . . . . 12 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → 𝑅 ∈ ran 𝑘Gen)
476ad2antrr 764 . . . . . . . . . . . 12 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → (𝑅 ×t 𝑆) ∈ Top)
48 kgencn3 21583 . . . . . . . . . . . 12 ((𝑅 ∈ ran 𝑘Gen ∧ (𝑅 ×t 𝑆) ∈ Top) → (𝑅 Cn (𝑅 ×t 𝑆)) = (𝑅 Cn (𝑘Gen‘(𝑅 ×t 𝑆))))
4946, 47, 48syl2anc 696 . . . . . . . . . . 11 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → (𝑅 Cn (𝑅 ×t 𝑆)) = (𝑅 Cn (𝑘Gen‘(𝑅 ×t 𝑆))))
5044, 49eleqtrd 2841 . . . . . . . . . 10 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → (𝑡 𝑅 ↦ ⟨𝑡, (2nd𝑦)⟩) ∈ (𝑅 Cn (𝑘Gen‘(𝑅 ×t 𝑆))))
51 cnima 21291 . . . . . . . . . 10 (((𝑡 𝑅 ↦ ⟨𝑡, (2nd𝑦)⟩) ∈ (𝑅 Cn (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) → ((𝑡 𝑅 ↦ ⟨𝑡, (2nd𝑦)⟩) “ 𝑥) ∈ 𝑅)
5250, 22, 51syl2anc 696 . . . . . . . . 9 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → ((𝑡 𝑅 ↦ ⟨𝑡, (2nd𝑦)⟩) “ 𝑥) ∈ 𝑅)
539, 52syl5eqelr 2844 . . . . . . . 8 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∈ 𝑅)
54 xp1st 7366 . . . . . . . . . 10 (𝑦 ∈ ( 𝑅 × 𝑆) → (1st𝑦) ∈ 𝑅)
5532, 54syl 17 . . . . . . . . 9 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → (1st𝑦) ∈ 𝑅)
56 1st2nd2 7373 . . . . . . . . . . 11 (𝑦 ∈ ( 𝑅 × 𝑆) → 𝑦 = ⟨(1st𝑦), (2nd𝑦)⟩)
5732, 56syl 17 . . . . . . . . . 10 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → 𝑦 = ⟨(1st𝑦), (2nd𝑦)⟩)
5857, 21eqeltrrd 2840 . . . . . . . . 9 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → ⟨(1st𝑦), (2nd𝑦)⟩ ∈ 𝑥)
59 opeq1 4553 . . . . . . . . . . 11 (𝑡 = (1st𝑦) → ⟨𝑡, (2nd𝑦)⟩ = ⟨(1st𝑦), (2nd𝑦)⟩)
6059eleq1d 2824 . . . . . . . . . 10 (𝑡 = (1st𝑦) → (⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥 ↔ ⟨(1st𝑦), (2nd𝑦)⟩ ∈ 𝑥))
6160elrab 3504 . . . . . . . . 9 ((1st𝑦) ∈ {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ↔ ((1st𝑦) ∈ 𝑅 ∧ ⟨(1st𝑦), (2nd𝑦)⟩ ∈ 𝑥))
6255, 58, 61sylanbrc 701 . . . . . . . 8 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → (1st𝑦) ∈ {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥})
63 nlly2i 21501 . . . . . . . 8 ((𝑅 ∈ 𝑛-Locally Comp ∧ {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∈ 𝑅 ∧ (1st𝑦) ∈ {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥}) → ∃𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥}∃𝑢𝑅 ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))
647, 53, 62, 63syl3anc 1477 . . . . . . 7 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → ∃𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥}∃𝑢𝑅 ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))
6510adantr 472 . . . . . . . . . . 11 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → 𝑅 ∈ Top)
6617adantr 472 . . . . . . . . . . 11 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → 𝑆 ∈ Top)
67 simprlr 822 . . . . . . . . . . 11 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → 𝑢𝑅)
68 ssrab2 3828 . . . . . . . . . . . . . 14 {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ⊆ 𝑆
6968a1i 11 . . . . . . . . . . . . 13 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ⊆ 𝑆)
70 incom 3948 . . . . . . . . . . . . . . . 16 ({𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ∩ 𝑘) = (𝑘 ∩ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})
71 simprll 821 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → 𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥})
7271elpwid 4314 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → 𝑠 ⊆ {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥})
73 ssrab2 3828 . . . . . . . . . . . . . . . . . . . . . 22 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ⊆ 𝑅
7472, 73syl6ss 3756 . . . . . . . . . . . . . . . . . . . . 21 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → 𝑠 𝑅)
7574adantr 472 . . . . . . . . . . . . . . . . . . . 20 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → 𝑠 𝑅)
76 elpwi 4312 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 ∈ 𝒫 𝑆𝑘 𝑆)
7776ad2antrl 766 . . . . . . . . . . . . . . . . . . . 20 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → 𝑘 𝑆)
78 eldif 3725 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑡 ∈ ((𝑠 × 𝑘) ∖ 𝑥) ↔ (𝑡 ∈ (𝑠 × 𝑘) ∧ ¬ 𝑡𝑥))
7978anbi1i 733 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑡 ∈ ((𝑠 × 𝑘) ∖ 𝑥) ∧ ((2nd ↾ ( 𝑅 × 𝑆))‘𝑡) = 𝑏) ↔ ((𝑡 ∈ (𝑠 × 𝑘) ∧ ¬ 𝑡𝑥) ∧ ((2nd ↾ ( 𝑅 × 𝑆))‘𝑡) = 𝑏))
80 anass 684 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑡 ∈ (𝑠 × 𝑘) ∧ ¬ 𝑡𝑥) ∧ ((2nd ↾ ( 𝑅 × 𝑆))‘𝑡) = 𝑏) ↔ (𝑡 ∈ (𝑠 × 𝑘) ∧ (¬ 𝑡𝑥 ∧ ((2nd ↾ ( 𝑅 × 𝑆))‘𝑡) = 𝑏)))
8179, 80bitri 264 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑡 ∈ ((𝑠 × 𝑘) ∖ 𝑥) ∧ ((2nd ↾ ( 𝑅 × 𝑆))‘𝑡) = 𝑏) ↔ (𝑡 ∈ (𝑠 × 𝑘) ∧ (¬ 𝑡𝑥 ∧ ((2nd ↾ ( 𝑅 × 𝑆))‘𝑡) = 𝑏)))
8281rexbii2 3177 . . . . . . . . . . . . . . . . . . . . . . . 24 (∃𝑡 ∈ ((𝑠 × 𝑘) ∖ 𝑥)((2nd ↾ ( 𝑅 × 𝑆))‘𝑡) = 𝑏 ↔ ∃𝑡 ∈ (𝑠 × 𝑘)(¬ 𝑡𝑥 ∧ ((2nd ↾ ( 𝑅 × 𝑆))‘𝑡) = 𝑏))
83 ancom 465 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((¬ 𝑡𝑥 ∧ ((2nd ↾ ( 𝑅 × 𝑆))‘𝑡) = 𝑏) ↔ (((2nd ↾ ( 𝑅 × 𝑆))‘𝑡) = 𝑏 ∧ ¬ 𝑡𝑥))
84 fveq2 6353 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑡 = ⟨𝑎, 𝑢⟩ → ((2nd ↾ ( 𝑅 × 𝑆))‘𝑡) = ((2nd ↾ ( 𝑅 × 𝑆))‘⟨𝑎, 𝑢⟩))
8584eqeq1d 2762 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑡 = ⟨𝑎, 𝑢⟩ → (((2nd ↾ ( 𝑅 × 𝑆))‘𝑡) = 𝑏 ↔ ((2nd ↾ ( 𝑅 × 𝑆))‘⟨𝑎, 𝑢⟩) = 𝑏))
86 eleq1 2827 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑡 = ⟨𝑎, 𝑢⟩ → (𝑡𝑥 ↔ ⟨𝑎, 𝑢⟩ ∈ 𝑥))
8786notbid 307 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑡 = ⟨𝑎, 𝑢⟩ → (¬ 𝑡𝑥 ↔ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥))
8885, 87anbi12d 749 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑡 = ⟨𝑎, 𝑢⟩ → ((((2nd ↾ ( 𝑅 × 𝑆))‘𝑡) = 𝑏 ∧ ¬ 𝑡𝑥) ↔ (((2nd ↾ ( 𝑅 × 𝑆))‘⟨𝑎, 𝑢⟩) = 𝑏 ∧ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥)))
8983, 88syl5bb 272 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑡 = ⟨𝑎, 𝑢⟩ → ((¬ 𝑡𝑥 ∧ ((2nd ↾ ( 𝑅 × 𝑆))‘𝑡) = 𝑏) ↔ (((2nd ↾ ( 𝑅 × 𝑆))‘⟨𝑎, 𝑢⟩) = 𝑏 ∧ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥)))
9089rexxp 5420 . . . . . . . . . . . . . . . . . . . . . . . 24 (∃𝑡 ∈ (𝑠 × 𝑘)(¬ 𝑡𝑥 ∧ ((2nd ↾ ( 𝑅 × 𝑆))‘𝑡) = 𝑏) ↔ ∃𝑎𝑠𝑢𝑘 (((2nd ↾ ( 𝑅 × 𝑆))‘⟨𝑎, 𝑢⟩) = 𝑏 ∧ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥))
9182, 90bitri 264 . . . . . . . . . . . . . . . . . . . . . . 23 (∃𝑡 ∈ ((𝑠 × 𝑘) ∖ 𝑥)((2nd ↾ ( 𝑅 × 𝑆))‘𝑡) = 𝑏 ↔ ∃𝑎𝑠𝑢𝑘 (((2nd ↾ ( 𝑅 × 𝑆))‘⟨𝑎, 𝑢⟩) = 𝑏 ∧ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥))
92 simpl 474 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑠 𝑅𝑘 𝑆) → 𝑠 𝑅)
9392sselda 3744 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝑠 𝑅𝑘 𝑆) ∧ 𝑎𝑠) → 𝑎 𝑅)
9493adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝑠 𝑅𝑘 𝑆) ∧ 𝑎𝑠) ∧ 𝑢𝑘) → 𝑎 𝑅)
95 simplr 809 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝑠 𝑅𝑘 𝑆) ∧ 𝑎𝑠) → 𝑘 𝑆)
9695sselda 3744 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝑠 𝑅𝑘 𝑆) ∧ 𝑎𝑠) ∧ 𝑢𝑘) → 𝑢 𝑆)
9794, 96opelxpd 5306 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝑠 𝑅𝑘 𝑆) ∧ 𝑎𝑠) ∧ 𝑢𝑘) → ⟨𝑎, 𝑢⟩ ∈ ( 𝑅 × 𝑆))
9897fvresd 6370 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝑠 𝑅𝑘 𝑆) ∧ 𝑎𝑠) ∧ 𝑢𝑘) → ((2nd ↾ ( 𝑅 × 𝑆))‘⟨𝑎, 𝑢⟩) = (2nd ‘⟨𝑎, 𝑢⟩))
99 vex 3343 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 𝑎 ∈ V
100 vex 3343 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 𝑢 ∈ V
10199, 100op2nd 7343 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (2nd ‘⟨𝑎, 𝑢⟩) = 𝑢
10298, 101syl6eq 2810 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝑠 𝑅𝑘 𝑆) ∧ 𝑎𝑠) ∧ 𝑢𝑘) → ((2nd ↾ ( 𝑅 × 𝑆))‘⟨𝑎, 𝑢⟩) = 𝑢)
103102eqeq1d 2762 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝑠 𝑅𝑘 𝑆) ∧ 𝑎𝑠) ∧ 𝑢𝑘) → (((2nd ↾ ( 𝑅 × 𝑆))‘⟨𝑎, 𝑢⟩) = 𝑏𝑢 = 𝑏))
104103anbi1d 743 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝑠 𝑅𝑘 𝑆) ∧ 𝑎𝑠) ∧ 𝑢𝑘) → ((((2nd ↾ ( 𝑅 × 𝑆))‘⟨𝑎, 𝑢⟩) = 𝑏 ∧ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥) ↔ (𝑢 = 𝑏 ∧ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥)))
105104rexbidva 3187 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑠 𝑅𝑘 𝑆) ∧ 𝑎𝑠) → (∃𝑢𝑘 (((2nd ↾ ( 𝑅 × 𝑆))‘⟨𝑎, 𝑢⟩) = 𝑏 ∧ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥) ↔ ∃𝑢𝑘 (𝑢 = 𝑏 ∧ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥)))
106 opeq2 4554 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑢 = 𝑏 → ⟨𝑎, 𝑢⟩ = ⟨𝑎, 𝑏⟩)
107106eleq1d 2824 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑢 = 𝑏 → (⟨𝑎, 𝑢⟩ ∈ 𝑥 ↔ ⟨𝑎, 𝑏⟩ ∈ 𝑥))
108107notbid 307 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑢 = 𝑏 → (¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥 ↔ ¬ ⟨𝑎, 𝑏⟩ ∈ 𝑥))
109108ceqsrexbv 3476 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (∃𝑢𝑘 (𝑢 = 𝑏 ∧ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥) ↔ (𝑏𝑘 ∧ ¬ ⟨𝑎, 𝑏⟩ ∈ 𝑥))
110105, 109syl6bb 276 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑠 𝑅𝑘 𝑆) ∧ 𝑎𝑠) → (∃𝑢𝑘 (((2nd ↾ ( 𝑅 × 𝑆))‘⟨𝑎, 𝑢⟩) = 𝑏 ∧ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥) ↔ (𝑏𝑘 ∧ ¬ ⟨𝑎, 𝑏⟩ ∈ 𝑥)))
111110rexbidva 3187 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑠 𝑅𝑘 𝑆) → (∃𝑎𝑠𝑢𝑘 (((2nd ↾ ( 𝑅 × 𝑆))‘⟨𝑎, 𝑢⟩) = 𝑏 ∧ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥) ↔ ∃𝑎𝑠 (𝑏𝑘 ∧ ¬ ⟨𝑎, 𝑏⟩ ∈ 𝑥)))
112 r19.42v 3230 . . . . . . . . . . . . . . . . . . . . . . . 24 (∃𝑎𝑠 (𝑏𝑘 ∧ ¬ ⟨𝑎, 𝑏⟩ ∈ 𝑥) ↔ (𝑏𝑘 ∧ ∃𝑎𝑠 ¬ ⟨𝑎, 𝑏⟩ ∈ 𝑥))
113111, 112syl6bb 276 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑠 𝑅𝑘 𝑆) → (∃𝑎𝑠𝑢𝑘 (((2nd ↾ ( 𝑅 × 𝑆))‘⟨𝑎, 𝑢⟩) = 𝑏 ∧ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥) ↔ (𝑏𝑘 ∧ ∃𝑎𝑠 ¬ ⟨𝑎, 𝑏⟩ ∈ 𝑥)))
11491, 113syl5bb 272 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑠 𝑅𝑘 𝑆) → (∃𝑡 ∈ ((𝑠 × 𝑘) ∖ 𝑥)((2nd ↾ ( 𝑅 × 𝑆))‘𝑡) = 𝑏 ↔ (𝑏𝑘 ∧ ∃𝑎𝑠 ¬ ⟨𝑎, 𝑏⟩ ∈ 𝑥)))
115 f2ndres 7359 . . . . . . . . . . . . . . . . . . . . . . . 24 (2nd ↾ ( 𝑅 × 𝑆)):( 𝑅 × 𝑆)⟶ 𝑆
116 ffn 6206 . . . . . . . . . . . . . . . . . . . . . . . 24 ((2nd ↾ ( 𝑅 × 𝑆)):( 𝑅 × 𝑆)⟶ 𝑆 → (2nd ↾ ( 𝑅 × 𝑆)) Fn ( 𝑅 × 𝑆))
117115, 116ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . 23 (2nd ↾ ( 𝑅 × 𝑆)) Fn ( 𝑅 × 𝑆)
118 difss 3880 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑠 × 𝑘) ∖ 𝑥) ⊆ (𝑠 × 𝑘)
119 xpss12 5281 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑠 𝑅𝑘 𝑆) → (𝑠 × 𝑘) ⊆ ( 𝑅 × 𝑆))
120118, 119syl5ss 3755 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑠 𝑅𝑘 𝑆) → ((𝑠 × 𝑘) ∖ 𝑥) ⊆ ( 𝑅 × 𝑆))
121 fvelimab 6416 . . . . . . . . . . . . . . . . . . . . . . 23 (((2nd ↾ ( 𝑅 × 𝑆)) Fn ( 𝑅 × 𝑆) ∧ ((𝑠 × 𝑘) ∖ 𝑥) ⊆ ( 𝑅 × 𝑆)) → (𝑏 ∈ ((2nd ↾ ( 𝑅 × 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ↔ ∃𝑡 ∈ ((𝑠 × 𝑘) ∖ 𝑥)((2nd ↾ ( 𝑅 × 𝑆))‘𝑡) = 𝑏))
122117, 120, 121sylancr 698 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑠 𝑅𝑘 𝑆) → (𝑏 ∈ ((2nd ↾ ( 𝑅 × 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ↔ ∃𝑡 ∈ ((𝑠 × 𝑘) ∖ 𝑥)((2nd ↾ ( 𝑅 × 𝑆))‘𝑡) = 𝑏))
123 eldif 3725 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑏 ∈ (𝑘 ∖ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ↔ (𝑏𝑘 ∧ ¬ 𝑏 ∈ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}))
124 simpr 479 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑠 𝑅𝑘 𝑆) → 𝑘 𝑆)
125124sselda 3744 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑠 𝑅𝑘 𝑆) ∧ 𝑏𝑘) → 𝑏 𝑆)
126 sneq 4331 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑣 = 𝑏 → {𝑣} = {𝑏})
127126xpeq2d 5296 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑣 = 𝑏 → (𝑠 × {𝑣}) = (𝑠 × {𝑏}))
128127sseq1d 3773 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑣 = 𝑏 → ((𝑠 × {𝑣}) ⊆ 𝑥 ↔ (𝑠 × {𝑏}) ⊆ 𝑥))
129 dfss3 3733 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑠 × {𝑏}) ⊆ 𝑥 ↔ ∀𝑘 ∈ (𝑠 × {𝑏})𝑘𝑥)
130 eleq1 2827 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑘 = ⟨𝑎, 𝑡⟩ → (𝑘𝑥 ↔ ⟨𝑎, 𝑡⟩ ∈ 𝑥))
131130ralxp 5419 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (∀𝑘 ∈ (𝑠 × {𝑏})𝑘𝑥 ↔ ∀𝑎𝑠𝑡 ∈ {𝑏}⟨𝑎, 𝑡⟩ ∈ 𝑥)
132 vex 3343 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 𝑏 ∈ V
133 opeq2 4554 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑡 = 𝑏 → ⟨𝑎, 𝑡⟩ = ⟨𝑎, 𝑏⟩)
134133eleq1d 2824 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑡 = 𝑏 → (⟨𝑎, 𝑡⟩ ∈ 𝑥 ↔ ⟨𝑎, 𝑏⟩ ∈ 𝑥))
135132, 134ralsn 4366 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (∀𝑡 ∈ {𝑏}⟨𝑎, 𝑡⟩ ∈ 𝑥 ↔ ⟨𝑎, 𝑏⟩ ∈ 𝑥)
136135ralbii 3118 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (∀𝑎𝑠𝑡 ∈ {𝑏}⟨𝑎, 𝑡⟩ ∈ 𝑥 ↔ ∀𝑎𝑠𝑎, 𝑏⟩ ∈ 𝑥)
137129, 131, 1363bitri 286 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑠 × {𝑏}) ⊆ 𝑥 ↔ ∀𝑎𝑠𝑎, 𝑏⟩ ∈ 𝑥)
138128, 137syl6bb 276 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑣 = 𝑏 → ((𝑠 × {𝑣}) ⊆ 𝑥 ↔ ∀𝑎𝑠𝑎, 𝑏⟩ ∈ 𝑥))
139138elrab3 3505 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑏 𝑆 → (𝑏 ∈ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ↔ ∀𝑎𝑠𝑎, 𝑏⟩ ∈ 𝑥))
140125, 139syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑠 𝑅𝑘 𝑆) ∧ 𝑏𝑘) → (𝑏 ∈ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ↔ ∀𝑎𝑠𝑎, 𝑏⟩ ∈ 𝑥))
141140notbid 307 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑠 𝑅𝑘 𝑆) ∧ 𝑏𝑘) → (¬ 𝑏 ∈ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ↔ ¬ ∀𝑎𝑠𝑎, 𝑏⟩ ∈ 𝑥))
142 rexnal 3133 . . . . . . . . . . . . . . . . . . . . . . . . 25 (∃𝑎𝑠 ¬ ⟨𝑎, 𝑏⟩ ∈ 𝑥 ↔ ¬ ∀𝑎𝑠𝑎, 𝑏⟩ ∈ 𝑥)
143141, 142syl6bbr 278 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑠 𝑅𝑘 𝑆) ∧ 𝑏𝑘) → (¬ 𝑏 ∈ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ↔ ∃𝑎𝑠 ¬ ⟨𝑎, 𝑏⟩ ∈ 𝑥))
144143pm5.32da 676 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑠 𝑅𝑘 𝑆) → ((𝑏𝑘 ∧ ¬ 𝑏 ∈ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ↔ (𝑏𝑘 ∧ ∃𝑎𝑠 ¬ ⟨𝑎, 𝑏⟩ ∈ 𝑥)))
145123, 144syl5bb 272 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑠 𝑅𝑘 𝑆) → (𝑏 ∈ (𝑘 ∖ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ↔ (𝑏𝑘 ∧ ∃𝑎𝑠 ¬ ⟨𝑎, 𝑏⟩ ∈ 𝑥)))
146114, 122, 1453bitr4d 300 . . . . . . . . . . . . . . . . . . . . 21 ((𝑠 𝑅𝑘 𝑆) → (𝑏 ∈ ((2nd ↾ ( 𝑅 × 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ↔ 𝑏 ∈ (𝑘 ∖ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})))
147146eqrdv 2758 . . . . . . . . . . . . . . . . . . . 20 ((𝑠 𝑅𝑘 𝑆) → ((2nd ↾ ( 𝑅 × 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) = (𝑘 ∖ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}))
14875, 77, 147syl2anc 696 . . . . . . . . . . . . . . . . . . 19 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → ((2nd ↾ ( 𝑅 × 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) = (𝑘 ∖ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}))
149 difin 4004 . . . . . . . . . . . . . . . . . . . 20 (𝑘 ∖ (𝑘 ∩ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})) = (𝑘 ∖ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})
15066adantr 472 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → 𝑆 ∈ Top)
15118restuni 21188 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑆 ∈ Top ∧ 𝑘 𝑆) → 𝑘 = (𝑆t 𝑘))
152150, 77, 151syl2anc 696 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → 𝑘 = (𝑆t 𝑘))
153152difeq1d 3870 . . . . . . . . . . . . . . . . . . . 20 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → (𝑘 ∖ (𝑘 ∩ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})) = ( (𝑆t 𝑘) ∖ (𝑘 ∩ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})))
154149, 153syl5eqr 2808 . . . . . . . . . . . . . . . . . . 19 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → (𝑘 ∖ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) = ( (𝑆t 𝑘) ∖ (𝑘 ∩ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})))
155148, 154eqtrd 2794 . . . . . . . . . . . . . . . . . 18 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → ((2nd ↾ ( 𝑅 × 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) = ( (𝑆t 𝑘) ∖ (𝑘 ∩ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})))
15616ad2antrr 764 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → 𝑆 ∈ (ran 𝑘Gen ∩ Haus))
157156elin2d 3946 . . . . . . . . . . . . . . . . . . . 20 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → 𝑆 ∈ Haus)
158 df-ima 5279 . . . . . . . . . . . . . . . . . . . . . . 23 ((2nd ↾ ( 𝑅 × 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) = ran ((2nd ↾ ( 𝑅 × 𝑆)) ↾ ((𝑠 × 𝑘) ∖ 𝑥))
159 resres 5567 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((2nd ↾ ( 𝑅 × 𝑆)) ↾ ((𝑠 × 𝑘) ∖ 𝑥)) = (2nd ↾ (( 𝑅 × 𝑆) ∩ ((𝑠 × 𝑘) ∖ 𝑥)))
160 inss2 3977 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (( 𝑅 × 𝑆) ∩ ((𝑠 × 𝑘) ∖ 𝑥)) ⊆ ((𝑠 × 𝑘) ∖ 𝑥)
161160, 118sstri 3753 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (( 𝑅 × 𝑆) ∩ ((𝑠 × 𝑘) ∖ 𝑥)) ⊆ (𝑠 × 𝑘)
162 ssres2 5583 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((( 𝑅 × 𝑆) ∩ ((𝑠 × 𝑘) ∖ 𝑥)) ⊆ (𝑠 × 𝑘) → (2nd ↾ (( 𝑅 × 𝑆) ∩ ((𝑠 × 𝑘) ∖ 𝑥))) ⊆ (2nd ↾ (𝑠 × 𝑘)))
163161, 162ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . 25 (2nd ↾ (( 𝑅 × 𝑆) ∩ ((𝑠 × 𝑘) ∖ 𝑥))) ⊆ (2nd ↾ (𝑠 × 𝑘))
164159, 163eqsstri 3776 . . . . . . . . . . . . . . . . . . . . . . . 24 ((2nd ↾ ( 𝑅 × 𝑆)) ↾ ((𝑠 × 𝑘) ∖ 𝑥)) ⊆ (2nd ↾ (𝑠 × 𝑘))
165 rnss 5509 . . . . . . . . . . . . . . . . . . . . . . . 24 (((2nd ↾ ( 𝑅 × 𝑆)) ↾ ((𝑠 × 𝑘) ∖ 𝑥)) ⊆ (2nd ↾ (𝑠 × 𝑘)) → ran ((2nd ↾ ( 𝑅 × 𝑆)) ↾ ((𝑠 × 𝑘) ∖ 𝑥)) ⊆ ran (2nd ↾ (𝑠 × 𝑘)))
166164, 165ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . 23 ran ((2nd ↾ ( 𝑅 × 𝑆)) ↾ ((𝑠 × 𝑘) ∖ 𝑥)) ⊆ ran (2nd ↾ (𝑠 × 𝑘))
167158, 166eqsstri 3776 . . . . . . . . . . . . . . . . . . . . . 22 ((2nd ↾ ( 𝑅 × 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ⊆ ran (2nd ↾ (𝑠 × 𝑘))
168 f2ndres 7359 . . . . . . . . . . . . . . . . . . . . . . 23 (2nd ↾ (𝑠 × 𝑘)):(𝑠 × 𝑘)⟶𝑘
169 frn 6214 . . . . . . . . . . . . . . . . . . . . . . 23 ((2nd ↾ (𝑠 × 𝑘)):(𝑠 × 𝑘)⟶𝑘 → ran (2nd ↾ (𝑠 × 𝑘)) ⊆ 𝑘)
170168, 169ax-mp 5 . . . . . . . . . . . . . . . . . . . . . 22 ran (2nd ↾ (𝑠 × 𝑘)) ⊆ 𝑘
171167, 170sstri 3753 . . . . . . . . . . . . . . . . . . . . 21 ((2nd ↾ ( 𝑅 × 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ⊆ 𝑘
172171, 77syl5ss 3755 . . . . . . . . . . . . . . . . . . . 20 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → ((2nd ↾ ( 𝑅 × 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ⊆ 𝑆)
17313ad2antrr 764 . . . . . . . . . . . . . . . . . . . . . 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 21635 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑅 ∈ (TopOn‘ 𝑅) ∧ 𝑆 ∈ (TopOn‘ 𝑆)) → (2nd ↾ ( 𝑅 × 𝑆)) ∈ ((𝑅 ×t 𝑆) Cn 𝑆))
176173, 174, 175syl2anc 696 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → (2nd ↾ ( 𝑅 × 𝑆)) ∈ ((𝑅 ×t 𝑆) Cn 𝑆))
17727ad2antrr 764 . . . . . . . . . . . . . . . . . . . . . . 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 3343 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑠 ∈ V
180 vex 3343 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑘 ∈ V
181179, 180xpex 7128 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑠 × 𝑘) ∈ V
182181a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → (𝑠 × 𝑘) ∈ V)
183 restabs 21191 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑅 ×t 𝑆) ∈ Top ∧ ((𝑠 × 𝑘) ∖ 𝑥) ⊆ (𝑠 × 𝑘) ∧ (𝑠 × 𝑘) ∈ V) → (((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ↾t ((𝑠 × 𝑘) ∖ 𝑥)) = ((𝑅 ×t 𝑆) ↾t ((𝑠 × 𝑘) ∖ 𝑥)))
184177, 178, 182, 183syl3anc 1477 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → (((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ↾t ((𝑠 × 𝑘) ∖ 𝑥)) = ((𝑅 ×t 𝑆) ↾t ((𝑠 × 𝑘) ∖ 𝑥)))
18565adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . 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 811 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → 𝑘 ∈ 𝒫 𝑆)
189 txrest 21656 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑠 ∈ V ∧ 𝑘 ∈ 𝒫 𝑆)) → ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) = ((𝑅t 𝑠) ×t (𝑆t 𝑘)))
190185, 186, 187, 188, 189syl22anc 1478 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) = ((𝑅t 𝑠) ×t (𝑆t 𝑘)))
191 simprr3 1277 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → (𝑅t 𝑠) ∈ Comp)
192191adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → (𝑅t 𝑠) ∈ Comp)
193 simprr 813 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → (𝑆t 𝑘) ∈ Comp)
194 txcmp 21668 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑅t 𝑠) ∈ Comp ∧ (𝑆t 𝑘) ∈ Comp) → ((𝑅t 𝑠) ×t (𝑆t 𝑘)) ∈ Comp)
195192, 193, 194syl2anc 696 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → ((𝑅t 𝑠) ×t (𝑆t 𝑘)) ∈ Comp)
196190, 195eqeltrd 2839 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ∈ Comp)
197 difin 4004 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑠 × 𝑘) ∖ ((𝑠 × 𝑘) ∩ 𝑥)) = ((𝑠 × 𝑘) ∖ 𝑥)
19875, 77, 119syl2anc 696 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → (𝑠 × 𝑘) ⊆ ( 𝑅 × 𝑆))
199185, 150, 25syl2anc 696 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → ( 𝑅 × 𝑆) = (𝑅 ×t 𝑆))
200198, 199sseqtrd 3782 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → (𝑠 × 𝑘) ⊆ (𝑅 ×t 𝑆))
20128restuni 21188 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑅 ×t 𝑆) ∈ Top ∧ (𝑠 × 𝑘) ⊆ (𝑅 ×t 𝑆)) → (𝑠 × 𝑘) = ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)))
202177, 200, 201syl2anc 696 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → (𝑠 × 𝑘) = ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)))
203202difeq1d 3870 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → ((𝑠 × 𝑘) ∖ ((𝑠 × 𝑘) ∩ 𝑥)) = ( ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ∖ ((𝑠 × 𝑘) ∩ 𝑥)))
204197, 203syl5eqr 2808 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → ((𝑠 × 𝑘) ∖ 𝑥) = ( ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ∖ ((𝑠 × 𝑘) ∩ 𝑥)))
205 resttop 21186 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑅 ×t 𝑆) ∈ Top ∧ (𝑠 × 𝑘) ∈ V) → ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ∈ Top)
206177, 181, 205sylancl 697 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ∈ Top)
207 incom 3948 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑠 × 𝑘) ∩ 𝑥) = (𝑥 ∩ (𝑠 × 𝑘))
20822ad2antrr 764 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆)))
209 kgeni 21562 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆)) ∧ ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ∈ Comp) → (𝑥 ∩ (𝑠 × 𝑘)) ∈ ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)))
210208, 196, 209syl2anc 696 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → (𝑥 ∩ (𝑠 × 𝑘)) ∈ ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)))
211207, 210syl5eqel 2843 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → ((𝑠 × 𝑘) ∩ 𝑥) ∈ ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)))
212 eqid 2760 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) = ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘))
213212opncld 21059 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ∈ Top ∧ ((𝑠 × 𝑘) ∩ 𝑥) ∈ ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘))) → ( ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ∖ ((𝑠 × 𝑘) ∩ 𝑥)) ∈ (Clsd‘((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘))))
214206, 211, 213syl2anc 696 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → ( ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ∖ ((𝑠 × 𝑘) ∩ 𝑥)) ∈ (Clsd‘((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘))))
215204, 214eqeltrd 2839 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → ((𝑠 × 𝑘) ∖ 𝑥) ∈ (Clsd‘((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘))))
216 cmpcld 21427 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ∈ Comp ∧ ((𝑠 × 𝑘) ∖ 𝑥) ∈ (Clsd‘((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)))) → (((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ↾t ((𝑠 × 𝑘) ∖ 𝑥)) ∈ Comp)
217196, 215, 216syl2anc 696 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → (((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ↾t ((𝑠 × 𝑘) ∖ 𝑥)) ∈ Comp)
218184, 217eqeltrrd 2840 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → ((𝑅 ×t 𝑆) ↾t ((𝑠 × 𝑘) ∖ 𝑥)) ∈ Comp)
219 imacmp 21422 . . . . . . . . . . . . . . . . . . . . 21 (((2nd ↾ ( 𝑅 × 𝑆)) ∈ ((𝑅 ×t 𝑆) Cn 𝑆) ∧ ((𝑅 ×t 𝑆) ↾t ((𝑠 × 𝑘) ∖ 𝑥)) ∈ Comp) → (𝑆t ((2nd ↾ ( 𝑅 × 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥))) ∈ Comp)
220176, 218, 219syl2anc 696 . . . . . . . . . . . . . . . . . . . 20 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → (𝑆t ((2nd ↾ ( 𝑅 × 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥))) ∈ Comp)
22118hauscmp 21432 . . . . . . . . . . . . . . . . . . . 20 ((𝑆 ∈ Haus ∧ ((2nd ↾ ( 𝑅 × 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ⊆ 𝑆 ∧ (𝑆t ((2nd ↾ ( 𝑅 × 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥))) ∈ Comp) → ((2nd ↾ ( 𝑅 × 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ∈ (Clsd‘𝑆))
222157, 172, 220, 221syl3anc 1477 . . . . . . . . . . . . . . . . . . 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 21199 . . . . . . . . . . . . . . . . . . 19 ((𝑘 𝑆 ∧ ((2nd ↾ ( 𝑅 × 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ∈ (Clsd‘𝑆) ∧ ((2nd ↾ ( 𝑅 × 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ⊆ 𝑘) → ((2nd ↾ ( 𝑅 × 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ∈ (Clsd‘(𝑆t 𝑘)))
22577, 222, 223, 224syl3anc 1477 . . . . . . . . . . . . . . . . . 18 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → ((2nd ↾ ( 𝑅 × 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ∈ (Clsd‘(𝑆t 𝑘)))
226155, 225eqeltrrd 2840 . . . . . . . . . . . . . . . . 17 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → ( (𝑆t 𝑘) ∖ (𝑘 ∩ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})) ∈ (Clsd‘(𝑆t 𝑘)))
227 resttop 21186 . . . . . . . . . . . . . . . . . . 19 ((𝑆 ∈ Top ∧ 𝑘 ∈ 𝒫 𝑆) → (𝑆t 𝑘) ∈ Top)
228150, 188, 227syl2anc 696 . . . . . . . . . . . . . . . . . 18 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → (𝑆t 𝑘) ∈ Top)
229 inss1 3976 . . . . . . . . . . . . . . . . . . 19 (𝑘 ∩ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ⊆ 𝑘
230229, 152syl5sseq 3794 . . . . . . . . . . . . . . . . . 18 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → (𝑘 ∩ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ⊆ (𝑆t 𝑘))
231 eqid 2760 . . . . . . . . . . . . . . . . . . 19 (𝑆t 𝑘) = (𝑆t 𝑘)
232231isopn2 21058 . . . . . . . . . . . . . . . . . 18 (((𝑆t 𝑘) ∈ Top ∧ (𝑘 ∩ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ⊆ (𝑆t 𝑘)) → ((𝑘 ∩ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ∈ (𝑆t 𝑘) ↔ ( (𝑆t 𝑘) ∖ (𝑘 ∩ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})) ∈ (Clsd‘(𝑆t 𝑘))))
233228, 230, 232syl2anc 696 . . . . . . . . . . . . . . . . 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 2843 . . . . . . . . . . . . . . 15 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → ({𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ∩ 𝑘) ∈ (𝑆t 𝑘))
236235expr 644 . . . . . . . . . . . . . 14 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ 𝑘 ∈ 𝒫 𝑆) → ((𝑆t 𝑘) ∈ Comp → ({𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ∩ 𝑘) ∈ (𝑆t 𝑘)))
237236ralrimiva 3104 . . . . . . . . . . . . 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 21561 . . . . . . . . . . . . . 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 995 . . . . . . . . . . . 12 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ∈ (𝑘Gen‘𝑆))
24216adantr 472 . . . . . . . . . . . . . 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 21572 . . . . . . . . . . . . 13 (𝑆 ∈ ran 𝑘Gen → (𝑘Gen‘𝑆) = 𝑆)
245243, 244syl 17 . . . . . . . . . . . 12 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → (𝑘Gen‘𝑆) = 𝑆)
246241, 245eleqtrd 2841 . . . . . . . . . . 11 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ∈ 𝑆)
247 txopn 21627 . . . . . . . . . . 11 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑢𝑅 ∧ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ∈ 𝑆)) → (𝑢 × {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ∈ (𝑅 ×t 𝑆))
24865, 66, 67, 246, 247syl22anc 1478 . . . . . . . . . 10 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → (𝑢 × {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ∈ (𝑅 ×t 𝑆))
24957adantr 472 . . . . . . . . . . 11 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → 𝑦 = ⟨(1st𝑦), (2nd𝑦)⟩)
250 simprr1 1273 . . . . . . . . . . . 12 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → (1st𝑦) ∈ 𝑢)
25134adantr 472 . . . . . . . . . . . . 13 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → (2nd𝑦) ∈ 𝑆)
252 relxp 5283 . . . . . . . . . . . . . . 15 Rel (𝑠 × {(2nd𝑦)})
253252a1i 11 . . . . . . . . . . . . . 14 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → Rel (𝑠 × {(2nd𝑦)}))
254 opelxp 5303 . . . . . . . . . . . . . . 15 (⟨𝑎, 𝑏⟩ ∈ (𝑠 × {(2nd𝑦)}) ↔ (𝑎𝑠𝑏 ∈ {(2nd𝑦)}))
25572sselda 3744 . . . . . . . . . . . . . . . . . 18 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ 𝑎𝑠) → 𝑎 ∈ {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥})
256 opeq1 4553 . . . . . . . . . . . . . . . . . . . . 21 (𝑡 = 𝑎 → ⟨𝑡, (2nd𝑦)⟩ = ⟨𝑎, (2nd𝑦)⟩)
257256eleq1d 2824 . . . . . . . . . . . . . . . . . . . 20 (𝑡 = 𝑎 → (⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥 ↔ ⟨𝑎, (2nd𝑦)⟩ ∈ 𝑥))
258257elrab 3504 . . . . . . . . . . . . . . . . . . 19 (𝑎 ∈ {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ↔ (𝑎 𝑅 ∧ ⟨𝑎, (2nd𝑦)⟩ ∈ 𝑥))
259258simprbi 483 . . . . . . . . . . . . . . . . . 18 (𝑎 ∈ {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} → ⟨𝑎, (2nd𝑦)⟩ ∈ 𝑥)
260255, 259syl 17 . . . . . . . . . . . . . . . . 17 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ 𝑎𝑠) → ⟨𝑎, (2nd𝑦)⟩ ∈ 𝑥)
261 elsni 4338 . . . . . . . . . . . . . . . . . . 19 (𝑏 ∈ {(2nd𝑦)} → 𝑏 = (2nd𝑦))
262261opeq2d 4560 . . . . . . . . . . . . . . . . . 18 (𝑏 ∈ {(2nd𝑦)} → ⟨𝑎, 𝑏⟩ = ⟨𝑎, (2nd𝑦)⟩)
263262eleq1d 2824 . . . . . . . . . . . . . . . . 17 (𝑏 ∈ {(2nd𝑦)} → (⟨𝑎, 𝑏⟩ ∈ 𝑥 ↔ ⟨𝑎, (2nd𝑦)⟩ ∈ 𝑥))
264260, 263syl5ibrcom 237 . . . . . . . . . . . . . . . 16 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ 𝑎𝑠) → (𝑏 ∈ {(2nd𝑦)} → ⟨𝑎, 𝑏⟩ ∈ 𝑥))
265264expimpd 630 . . . . . . . . . . . . . . 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 5369 . . . . . . . . . . . . 13 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → (𝑠 × {(2nd𝑦)}) ⊆ 𝑥)
268 sneq 4331 . . . . . . . . . . . . . . . 16 (𝑣 = (2nd𝑦) → {𝑣} = {(2nd𝑦)})
269268xpeq2d 5296 . . . . . . . . . . . . . . 15 (𝑣 = (2nd𝑦) → (𝑠 × {𝑣}) = (𝑠 × {(2nd𝑦)}))
270269sseq1d 3773 . . . . . . . . . . . . . 14 (𝑣 = (2nd𝑦) → ((𝑠 × {𝑣}) ⊆ 𝑥 ↔ (𝑠 × {(2nd𝑦)}) ⊆ 𝑥))
271270elrab 3504 . . . . . . . . . . . . 13 ((2nd𝑦) ∈ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ↔ ((2nd𝑦) ∈ 𝑆 ∧ (𝑠 × {(2nd𝑦)}) ⊆ 𝑥))
272251, 267, 271sylanbrc 701 . . . . . . . . . . . 12 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → (2nd𝑦) ∈ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})
273250, 272opelxpd 5306 . . . . . . . . . . 11 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → ⟨(1st𝑦), (2nd𝑦)⟩ ∈ (𝑢 × {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}))
274249, 273eqeltrd 2839 . . . . . . . . . 10 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → 𝑦 ∈ (𝑢 × {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}))
275 relxp 5283 . . . . . . . . . . . 12 Rel (𝑢 × {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})
276275a1i 11 . . . . . . . . . . 11 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → Rel (𝑢 × {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}))
277 opelxp 5303 . . . . . . . . . . . 12 (⟨𝑎, 𝑏⟩ ∈ (𝑢 × {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ↔ (𝑎𝑢𝑏 ∈ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}))
278128elrab 3504 . . . . . . . . . . . . . . 15 (𝑏 ∈ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ↔ (𝑏 𝑆 ∧ (𝑠 × {𝑏}) ⊆ 𝑥))
279278simprbi 483 . . . . . . . . . . . . . 14 (𝑏 ∈ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} → (𝑠 × {𝑏}) ⊆ 𝑥)
280 simprr2 1275 . . . . . . . . . . . . . . . 16 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → 𝑢𝑠)
281280sselda 3744 . . . . . . . . . . . . . . 15 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ 𝑎𝑢) → 𝑎𝑠)
282 vsnid 4354 . . . . . . . . . . . . . . 15 𝑏 ∈ {𝑏}
283 opelxpi 5305 . . . . . . . . . . . . . . 15 ((𝑎𝑠𝑏 ∈ {𝑏}) → ⟨𝑎, 𝑏⟩ ∈ (𝑠 × {𝑏}))
284281, 282, 283sylancl 697 . . . . . . . . . . . . . 14 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ 𝑎𝑢) → ⟨𝑎, 𝑏⟩ ∈ (𝑠 × {𝑏}))
285 ssel 3738 . . . . . . . . . . . . . 14 ((𝑠 × {𝑏}) ⊆ 𝑥 → (⟨𝑎, 𝑏⟩ ∈ (𝑠 × {𝑏}) → ⟨𝑎, 𝑏⟩ ∈ 𝑥))
286279, 284, 285syl2imc 41 . . . . . . . . . . . . 13 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ 𝑎𝑢) → (𝑏 ∈ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} → ⟨𝑎, 𝑏⟩ ∈ 𝑥))
287286expimpd 630 . . . . . . . . . . . 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 5369 . . . . . . . . . 10 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → (𝑢 × {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ⊆ 𝑥)
290 eleq2 2828 . . . . . . . . . . . 12 (𝑡 = (𝑢 × {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) → (𝑦𝑡𝑦 ∈ (𝑢 × {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})))
291 sseq1 3767 . . . . . . . . . . . 12 (𝑡 = (𝑢 × {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) → (𝑡𝑥 ↔ (𝑢 × {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ⊆ 𝑥))
292290, 291anbi12d 749 . . . . . . . . . . 11 (𝑡 = (𝑢 × {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) → ((𝑦𝑡𝑡𝑥) ↔ (𝑦 ∈ (𝑢 × {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ∧ (𝑢 × {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ⊆ 𝑥)))
293292rspcev 3449 . . . . . . . . . 10 (((𝑢 × {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ∈ (𝑅 ×t 𝑆) ∧ (𝑦 ∈ (𝑢 × {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ∧ (𝑢 × {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ⊆ 𝑥)) → ∃𝑡 ∈ (𝑅 ×t 𝑆)(𝑦𝑡𝑡𝑥))
294248, 274, 289, 293syl12anc 1475 . . . . . . . . 9 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → ∃𝑡 ∈ (𝑅 ×t 𝑆)(𝑦𝑡𝑡𝑥))
295294expr 644 . . . . . . . 8 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ (𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅)) → (((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp) → ∃𝑡 ∈ (𝑅 ×t 𝑆)(𝑦𝑡𝑡𝑥)))
296295rexlimdvva 3176 . . . . . . 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 3104 . . . . 5 (((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) → ∀𝑦𝑥𝑡 ∈ (𝑅 ×t 𝑆)(𝑦𝑡𝑡𝑥))
2996adantr 472 . . . . . 6 (((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) → (𝑅 ×t 𝑆) ∈ Top)
300 eltop2 21001 . . . . . 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 449 . . 3 ((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) → (𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆)) → 𝑥 ∈ (𝑅 ×t 𝑆)))
304303ssrdv 3750 . 2 ((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) → (𝑘Gen‘(𝑅 ×t 𝑆)) ⊆ (𝑅 ×t 𝑆))
305 iskgen2 21573 . 2 ((𝑅 ×t 𝑆) ∈ ran 𝑘Gen ↔ ((𝑅 ×t 𝑆) ∈ Top ∧ (𝑘Gen‘(𝑅 ×t 𝑆)) ⊆ (𝑅 ×t 𝑆)))
3066, 304, 305sylanbrc 701 1 ((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) → (𝑅 ×t 𝑆) ∈ ran 𝑘Gen)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 383  w3a 1072   = wceq 1632  wcel 2139  wral 3050  wrex 3051  {crab 3054  Vcvv 3340  cdif 3712  cin 3714  wss 3715  𝒫 cpw 4302  {csn 4321  cop 4327   cuni 4588  cmpt 4881   I cid 5173   × cxp 5264  ccnv 5265  ran crn 5267  cres 5268  cima 5269  Rel wrel 5271   Fn wfn 6044  wf 6045  cfv 6049  (class class class)co 6814  1st c1st 7332  2nd c2nd 7333  t crest 16303  Topctop 20920  TopOnctopon 20937  Clsdccld 21042   Cn ccn 21250  Hauscha 21334  Compccmp 21411  𝑛-Locally cnlly 21490  𝑘Genckgen 21558   ×t ctx 21585
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-rep 4923  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7115
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-ral 3055  df-rex 3056  df-reu 3057  df-rab 3059  df-v 3342  df-sbc 3577  df-csb 3675  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-pss 3731  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-tp 4326  df-op 4328  df-uni 4589  df-int 4628  df-iun 4674  df-iin 4675  df-br 4805  df-opab 4865  df-mpt 4882  df-tr 4905  df-id 5174  df-eprel 5179  df-po 5187  df-so 5188  df-fr 5225  df-we 5227  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-pred 5841  df-ord 5887  df-on 5888  df-lim 5889  df-suc 5890  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056  df-fv 6057  df-ov 6817  df-oprab 6818  df-mpt2 6819  df-om 7232  df-1st 7334  df-2nd 7335  df-wrecs 7577  df-recs 7638  df-rdg 7676  df-1o 7730  df-oadd 7734  df-er 7913  df-map 8027  df-en 8124  df-dom 8125  df-fin 8127  df-fi 8484  df-rest 16305  df-topgen 16326  df-top 20921  df-topon 20938  df-bases 20972  df-cld 21045  df-ntr 21046  df-cls 21047  df-nei 21124  df-cn 21253  df-cnp 21254  df-haus 21341  df-cmp 21412  df-nlly 21492  df-kgen 21559  df-tx 21587
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator