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

Theorem txkgen 21503
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 21324 . . 3 (𝑅 ∈ 𝑛-Locally Comp → 𝑅 ∈ Top)
2 elinel1 3832 . . . 4 (𝑆 ∈ (ran 𝑘Gen ∩ Haus) → 𝑆 ∈ ran 𝑘Gen)
3 kgentop 21393 . . . 4 (𝑆 ∈ ran 𝑘Gen → 𝑆 ∈ Top)
42, 3syl 17 . . 3 (𝑆 ∈ (ran 𝑘Gen ∩ Haus) → 𝑆 ∈ Top)
5 txtop 21420 . . 3 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑅 ×t 𝑆) ∈ Top)
61, 4, 5syl2an 493 . 2 ((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) → (𝑅 ×t 𝑆) ∈ Top)
7 simplll 813 . . . . . . . 8 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → 𝑅 ∈ 𝑛-Locally Comp)
8 eqid 2651 . . . . . . . . . 10 (𝑡 𝑅 ↦ ⟨𝑡, (2nd𝑦)⟩) = (𝑡 𝑅 ↦ ⟨𝑡, (2nd𝑦)⟩)
98mptpreima 5666 . . . . . . . . 9 ((𝑡 𝑅 ↦ ⟨𝑡, (2nd𝑦)⟩) “ 𝑥) = {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥}
101ad3antrrr 766 . . . . . . . . . . . . . 14 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → 𝑅 ∈ Top)
11 eqid 2651 . . . . . . . . . . . . . . 15 𝑅 = 𝑅
1211toptopon 20770 . . . . . . . . . . . . . 14 (𝑅 ∈ Top ↔ 𝑅 ∈ (TopOn‘ 𝑅))
1310, 12sylib 208 . . . . . . . . . . . . 13 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → 𝑅 ∈ (TopOn‘ 𝑅))
14 idcn 21109 . . . . . . . . . . . . 13 (𝑅 ∈ (TopOn‘ 𝑅) → ( I ↾ 𝑅) ∈ (𝑅 Cn 𝑅))
1513, 14syl 17 . . . . . . . . . . . 12 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → ( I ↾ 𝑅) ∈ (𝑅 Cn 𝑅))
16 simpllr 815 . . . . . . . . . . . . . . 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 2651 . . . . . . . . . . . . . . 15 𝑆 = 𝑆
1918toptopon 20770 . . . . . . . . . . . . . 14 (𝑆 ∈ Top ↔ 𝑆 ∈ (TopOn‘ 𝑆))
2017, 19sylib 208 . . . . . . . . . . . . 13 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → 𝑆 ∈ (TopOn‘ 𝑆))
21 simpr 476 . . . . . . . . . . . . . . . 16 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → 𝑦𝑥)
22 simplr 807 . . . . . . . . . . . . . . . 16 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆)))
23 elunii 4473 . . . . . . . . . . . . . . . 16 ((𝑦𝑥𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) → 𝑦 (𝑘Gen‘(𝑅 ×t 𝑆)))
2421, 22, 23syl2anc 694 . . . . . . . . . . . . . . 15 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → 𝑦 (𝑘Gen‘(𝑅 ×t 𝑆)))
2511, 18txuni 21443 . . . . . . . . . . . . . . . . 17 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → ( 𝑅 × 𝑆) = (𝑅 ×t 𝑆))
2610, 17, 25syl2anc 694 . . . . . . . . . . . . . . . 16 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → ( 𝑅 × 𝑆) = (𝑅 ×t 𝑆))
2710, 17, 5syl2anc 694 . . . . . . . . . . . . . . . . 17 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → (𝑅 ×t 𝑆) ∈ Top)
28 eqid 2651 . . . . . . . . . . . . . . . . . 18 (𝑅 ×t 𝑆) = (𝑅 ×t 𝑆)
2928kgenuni 21390 . . . . . . . . . . . . . . . . 17 ((𝑅 ×t 𝑆) ∈ Top → (𝑅 ×t 𝑆) = (𝑘Gen‘(𝑅 ×t 𝑆)))
3027, 29syl 17 . . . . . . . . . . . . . . . 16 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → (𝑅 ×t 𝑆) = (𝑘Gen‘(𝑅 ×t 𝑆)))
3126, 30eqtrd 2685 . . . . . . . . . . . . . . 15 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → ( 𝑅 × 𝑆) = (𝑘Gen‘(𝑅 ×t 𝑆)))
3224, 31eleqtrrd 2733 . . . . . . . . . . . . . 14 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → 𝑦 ∈ ( 𝑅 × 𝑆))
33 xp2nd 7243 . . . . . . . . . . . . . 14 (𝑦 ∈ ( 𝑅 × 𝑆) → (2nd𝑦) ∈ 𝑆)
3432, 33syl 17 . . . . . . . . . . . . 13 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → (2nd𝑦) ∈ 𝑆)
35 cnconst2 21135 . . . . . . . . . . . . 13 ((𝑅 ∈ (TopOn‘ 𝑅) ∧ 𝑆 ∈ (TopOn‘ 𝑆) ∧ (2nd𝑦) ∈ 𝑆) → ( 𝑅 × {(2nd𝑦)}) ∈ (𝑅 Cn 𝑆))
3613, 20, 34, 35syl3anc 1366 . . . . . . . . . . . 12 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → ( 𝑅 × {(2nd𝑦)}) ∈ (𝑅 Cn 𝑆))
37 fvresi 6480 . . . . . . . . . . . . . . . 16 (𝑡 𝑅 → (( I ↾ 𝑅)‘𝑡) = 𝑡)
38 fvex 6239 . . . . . . . . . . . . . . . . 17 (2nd𝑦) ∈ V
3938fvconst2 6510 . . . . . . . . . . . . . . . 16 (𝑡 𝑅 → (( 𝑅 × {(2nd𝑦)})‘𝑡) = (2nd𝑦))
4037, 39opeq12d 4441 . . . . . . . . . . . . . . 15 (𝑡 𝑅 → ⟨(( I ↾ 𝑅)‘𝑡), (( 𝑅 × {(2nd𝑦)})‘𝑡)⟩ = ⟨𝑡, (2nd𝑦)⟩)
4140mpteq2ia 4773 . . . . . . . . . . . . . 14 (𝑡 𝑅 ↦ ⟨(( I ↾ 𝑅)‘𝑡), (( 𝑅 × {(2nd𝑦)})‘𝑡)⟩) = (𝑡 𝑅 ↦ ⟨𝑡, (2nd𝑦)⟩)
4241eqcomi 2660 . . . . . . . . . . . . 13 (𝑡 𝑅 ↦ ⟨𝑡, (2nd𝑦)⟩) = (𝑡 𝑅 ↦ ⟨(( I ↾ 𝑅)‘𝑡), (( 𝑅 × {(2nd𝑦)})‘𝑡)⟩)
4311, 42txcnmpt 21475 . . . . . . . . . . . 12 ((( I ↾ 𝑅) ∈ (𝑅 Cn 𝑅) ∧ ( 𝑅 × {(2nd𝑦)}) ∈ (𝑅 Cn 𝑆)) → (𝑡 𝑅 ↦ ⟨𝑡, (2nd𝑦)⟩) ∈ (𝑅 Cn (𝑅 ×t 𝑆)))
4415, 36, 43syl2anc 694 . . . . . . . . . . 11 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → (𝑡 𝑅 ↦ ⟨𝑡, (2nd𝑦)⟩) ∈ (𝑅 Cn (𝑅 ×t 𝑆)))
45 llycmpkgen 21403 . . . . . . . . . . . . 13 (𝑅 ∈ 𝑛-Locally Comp → 𝑅 ∈ ran 𝑘Gen)
4645ad3antrrr 766 . . . . . . . . . . . 12 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → 𝑅 ∈ ran 𝑘Gen)
476ad2antrr 762 . . . . . . . . . . . 12 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → (𝑅 ×t 𝑆) ∈ Top)
48 kgencn3 21409 . . . . . . . . . . . 12 ((𝑅 ∈ ran 𝑘Gen ∧ (𝑅 ×t 𝑆) ∈ Top) → (𝑅 Cn (𝑅 ×t 𝑆)) = (𝑅 Cn (𝑘Gen‘(𝑅 ×t 𝑆))))
4946, 47, 48syl2anc 694 . . . . . . . . . . 11 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → (𝑅 Cn (𝑅 ×t 𝑆)) = (𝑅 Cn (𝑘Gen‘(𝑅 ×t 𝑆))))
5044, 49eleqtrd 2732 . . . . . . . . . 10 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → (𝑡 𝑅 ↦ ⟨𝑡, (2nd𝑦)⟩) ∈ (𝑅 Cn (𝑘Gen‘(𝑅 ×t 𝑆))))
51 cnima 21117 . . . . . . . . . 10 (((𝑡 𝑅 ↦ ⟨𝑡, (2nd𝑦)⟩) ∈ (𝑅 Cn (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) → ((𝑡 𝑅 ↦ ⟨𝑡, (2nd𝑦)⟩) “ 𝑥) ∈ 𝑅)
5250, 22, 51syl2anc 694 . . . . . . . . 9 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → ((𝑡 𝑅 ↦ ⟨𝑡, (2nd𝑦)⟩) “ 𝑥) ∈ 𝑅)
539, 52syl5eqelr 2735 . . . . . . . 8 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∈ 𝑅)
54 xp1st 7242 . . . . . . . . . 10 (𝑦 ∈ ( 𝑅 × 𝑆) → (1st𝑦) ∈ 𝑅)
5532, 54syl 17 . . . . . . . . 9 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → (1st𝑦) ∈ 𝑅)
56 1st2nd2 7249 . . . . . . . . . . 11 (𝑦 ∈ ( 𝑅 × 𝑆) → 𝑦 = ⟨(1st𝑦), (2nd𝑦)⟩)
5732, 56syl 17 . . . . . . . . . 10 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → 𝑦 = ⟨(1st𝑦), (2nd𝑦)⟩)
5857, 21eqeltrrd 2731 . . . . . . . . 9 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → ⟨(1st𝑦), (2nd𝑦)⟩ ∈ 𝑥)
59 opeq1 4433 . . . . . . . . . . 11 (𝑡 = (1st𝑦) → ⟨𝑡, (2nd𝑦)⟩ = ⟨(1st𝑦), (2nd𝑦)⟩)
6059eleq1d 2715 . . . . . . . . . 10 (𝑡 = (1st𝑦) → (⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥 ↔ ⟨(1st𝑦), (2nd𝑦)⟩ ∈ 𝑥))
6160elrab 3396 . . . . . . . . 9 ((1st𝑦) ∈ {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ↔ ((1st𝑦) ∈ 𝑅 ∧ ⟨(1st𝑦), (2nd𝑦)⟩ ∈ 𝑥))
6255, 58, 61sylanbrc 699 . . . . . . . 8 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → (1st𝑦) ∈ {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥})
63 nlly2i 21327 . . . . . . . 8 ((𝑅 ∈ 𝑛-Locally Comp ∧ {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∈ 𝑅 ∧ (1st𝑦) ∈ {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥}) → ∃𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥}∃𝑢𝑅 ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))
647, 53, 62, 63syl3anc 1366 . . . . . . 7 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) → ∃𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥}∃𝑢𝑅 ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))
6510adantr 480 . . . . . . . . . . 11 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → 𝑅 ∈ Top)
6617adantr 480 . . . . . . . . . . 11 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → 𝑆 ∈ Top)
67 simprlr 820 . . . . . . . . . . 11 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → 𝑢𝑅)
68 ssrab2 3720 . . . . . . . . . . . . . 14 {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ⊆ 𝑆
6968a1i 11 . . . . . . . . . . . . 13 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ⊆ 𝑆)
70 incom 3838 . . . . . . . . . . . . . . . 16 ({𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ∩ 𝑘) = (𝑘 ∩ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})
71 simprll 819 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → 𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥})
7271elpwid 4203 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → 𝑠 ⊆ {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥})
73 ssrab2 3720 . . . . . . . . . . . . . . . . . . . . . 22 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ⊆ 𝑅
7472, 73syl6ss 3648 . . . . . . . . . . . . . . . . . . . . 21 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → 𝑠 𝑅)
7574adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → 𝑠 𝑅)
76 elpwi 4201 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 ∈ 𝒫 𝑆𝑘 𝑆)
7776ad2antrl 764 . . . . . . . . . . . . . . . . . . . 20 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → 𝑘 𝑆)
78 eldif 3617 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑡 ∈ ((𝑠 × 𝑘) ∖ 𝑥) ↔ (𝑡 ∈ (𝑠 × 𝑘) ∧ ¬ 𝑡𝑥))
7978anbi1i 731 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑡 ∈ ((𝑠 × 𝑘) ∖ 𝑥) ∧ ((2nd ↾ ( 𝑅 × 𝑆))‘𝑡) = 𝑏) ↔ ((𝑡 ∈ (𝑠 × 𝑘) ∧ ¬ 𝑡𝑥) ∧ ((2nd ↾ ( 𝑅 × 𝑆))‘𝑡) = 𝑏))
80 anass 682 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑡 ∈ (𝑠 × 𝑘) ∧ ¬ 𝑡𝑥) ∧ ((2nd ↾ ( 𝑅 × 𝑆))‘𝑡) = 𝑏) ↔ (𝑡 ∈ (𝑠 × 𝑘) ∧ (¬ 𝑡𝑥 ∧ ((2nd ↾ ( 𝑅 × 𝑆))‘𝑡) = 𝑏)))
8179, 80bitri 264 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑡 ∈ ((𝑠 × 𝑘) ∖ 𝑥) ∧ ((2nd ↾ ( 𝑅 × 𝑆))‘𝑡) = 𝑏) ↔ (𝑡 ∈ (𝑠 × 𝑘) ∧ (¬ 𝑡𝑥 ∧ ((2nd ↾ ( 𝑅 × 𝑆))‘𝑡) = 𝑏)))
8281rexbii2 3068 . . . . . . . . . . . . . . . . . . . . . . . 24 (∃𝑡 ∈ ((𝑠 × 𝑘) ∖ 𝑥)((2nd ↾ ( 𝑅 × 𝑆))‘𝑡) = 𝑏 ↔ ∃𝑡 ∈ (𝑠 × 𝑘)(¬ 𝑡𝑥 ∧ ((2nd ↾ ( 𝑅 × 𝑆))‘𝑡) = 𝑏))
83 ancom 465 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((¬ 𝑡𝑥 ∧ ((2nd ↾ ( 𝑅 × 𝑆))‘𝑡) = 𝑏) ↔ (((2nd ↾ ( 𝑅 × 𝑆))‘𝑡) = 𝑏 ∧ ¬ 𝑡𝑥))
84 fveq2 6229 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑡 = ⟨𝑎, 𝑢⟩ → ((2nd ↾ ( 𝑅 × 𝑆))‘𝑡) = ((2nd ↾ ( 𝑅 × 𝑆))‘⟨𝑎, 𝑢⟩))
8584eqeq1d 2653 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑡 = ⟨𝑎, 𝑢⟩ → (((2nd ↾ ( 𝑅 × 𝑆))‘𝑡) = 𝑏 ↔ ((2nd ↾ ( 𝑅 × 𝑆))‘⟨𝑎, 𝑢⟩) = 𝑏))
86 eleq1 2718 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑡 = ⟨𝑎, 𝑢⟩ → (𝑡𝑥 ↔ ⟨𝑎, 𝑢⟩ ∈ 𝑥))
8786notbid 307 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑡 = ⟨𝑎, 𝑢⟩ → (¬ 𝑡𝑥 ↔ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥))
8885, 87anbi12d 747 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑡 = ⟨𝑎, 𝑢⟩ → ((((2nd ↾ ( 𝑅 × 𝑆))‘𝑡) = 𝑏 ∧ ¬ 𝑡𝑥) ↔ (((2nd ↾ ( 𝑅 × 𝑆))‘⟨𝑎, 𝑢⟩) = 𝑏 ∧ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥)))
8983, 88syl5bb 272 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑡 = ⟨𝑎, 𝑢⟩ → ((¬ 𝑡𝑥 ∧ ((2nd ↾ ( 𝑅 × 𝑆))‘𝑡) = 𝑏) ↔ (((2nd ↾ ( 𝑅 × 𝑆))‘⟨𝑎, 𝑢⟩) = 𝑏 ∧ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥)))
9089rexxp 5297 . . . . . . . . . . . . . . . . . . . . . . . 24 (∃𝑡 ∈ (𝑠 × 𝑘)(¬ 𝑡𝑥 ∧ ((2nd ↾ ( 𝑅 × 𝑆))‘𝑡) = 𝑏) ↔ ∃𝑎𝑠𝑢𝑘 (((2nd ↾ ( 𝑅 × 𝑆))‘⟨𝑎, 𝑢⟩) = 𝑏 ∧ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥))
9182, 90bitri 264 . . . . . . . . . . . . . . . . . . . . . . 23 (∃𝑡 ∈ ((𝑠 × 𝑘) ∖ 𝑥)((2nd ↾ ( 𝑅 × 𝑆))‘𝑡) = 𝑏 ↔ ∃𝑎𝑠𝑢𝑘 (((2nd ↾ ( 𝑅 × 𝑆))‘⟨𝑎, 𝑢⟩) = 𝑏 ∧ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥))
92 simpl 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑠 𝑅𝑘 𝑆) → 𝑠 𝑅)
9392sselda 3636 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝑠 𝑅𝑘 𝑆) ∧ 𝑎𝑠) → 𝑎 𝑅)
9493adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝑠 𝑅𝑘 𝑆) ∧ 𝑎𝑠) ∧ 𝑢𝑘) → 𝑎 𝑅)
95 simplr 807 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝑠 𝑅𝑘 𝑆) ∧ 𝑎𝑠) → 𝑘 𝑆)
9695sselda 3636 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝑠 𝑅𝑘 𝑆) ∧ 𝑎𝑠) ∧ 𝑢𝑘) → 𝑢 𝑆)
9794, 96opelxpd 5183 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝑠 𝑅𝑘 𝑆) ∧ 𝑎𝑠) ∧ 𝑢𝑘) → ⟨𝑎, 𝑢⟩ ∈ ( 𝑅 × 𝑆))
9897fvresd 6246 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝑠 𝑅𝑘 𝑆) ∧ 𝑎𝑠) ∧ 𝑢𝑘) → ((2nd ↾ ( 𝑅 × 𝑆))‘⟨𝑎, 𝑢⟩) = (2nd ‘⟨𝑎, 𝑢⟩))
99 vex 3234 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 𝑎 ∈ V
100 vex 3234 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 𝑢 ∈ V
10199, 100op2nd 7219 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (2nd ‘⟨𝑎, 𝑢⟩) = 𝑢
10298, 101syl6eq 2701 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝑠 𝑅𝑘 𝑆) ∧ 𝑎𝑠) ∧ 𝑢𝑘) → ((2nd ↾ ( 𝑅 × 𝑆))‘⟨𝑎, 𝑢⟩) = 𝑢)
103102eqeq1d 2653 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝑠 𝑅𝑘 𝑆) ∧ 𝑎𝑠) ∧ 𝑢𝑘) → (((2nd ↾ ( 𝑅 × 𝑆))‘⟨𝑎, 𝑢⟩) = 𝑏𝑢 = 𝑏))
104103anbi1d 741 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝑠 𝑅𝑘 𝑆) ∧ 𝑎𝑠) ∧ 𝑢𝑘) → ((((2nd ↾ ( 𝑅 × 𝑆))‘⟨𝑎, 𝑢⟩) = 𝑏 ∧ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥) ↔ (𝑢 = 𝑏 ∧ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥)))
105104rexbidva 3078 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑠 𝑅𝑘 𝑆) ∧ 𝑎𝑠) → (∃𝑢𝑘 (((2nd ↾ ( 𝑅 × 𝑆))‘⟨𝑎, 𝑢⟩) = 𝑏 ∧ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥) ↔ ∃𝑢𝑘 (𝑢 = 𝑏 ∧ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥)))
106 opeq2 4434 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑢 = 𝑏 → ⟨𝑎, 𝑢⟩ = ⟨𝑎, 𝑏⟩)
107106eleq1d 2715 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑢 = 𝑏 → (⟨𝑎, 𝑢⟩ ∈ 𝑥 ↔ ⟨𝑎, 𝑏⟩ ∈ 𝑥))
108107notbid 307 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑢 = 𝑏 → (¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥 ↔ ¬ ⟨𝑎, 𝑏⟩ ∈ 𝑥))
109108ceqsrexbv 3368 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (∃𝑢𝑘 (𝑢 = 𝑏 ∧ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥) ↔ (𝑏𝑘 ∧ ¬ ⟨𝑎, 𝑏⟩ ∈ 𝑥))
110105, 109syl6bb 276 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑠 𝑅𝑘 𝑆) ∧ 𝑎𝑠) → (∃𝑢𝑘 (((2nd ↾ ( 𝑅 × 𝑆))‘⟨𝑎, 𝑢⟩) = 𝑏 ∧ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥) ↔ (𝑏𝑘 ∧ ¬ ⟨𝑎, 𝑏⟩ ∈ 𝑥)))
111110rexbidva 3078 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑠 𝑅𝑘 𝑆) → (∃𝑎𝑠𝑢𝑘 (((2nd ↾ ( 𝑅 × 𝑆))‘⟨𝑎, 𝑢⟩) = 𝑏 ∧ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥) ↔ ∃𝑎𝑠 (𝑏𝑘 ∧ ¬ ⟨𝑎, 𝑏⟩ ∈ 𝑥)))
112 r19.42v 3121 . . . . . . . . . . . . . . . . . . . . . . . 24 (∃𝑎𝑠 (𝑏𝑘 ∧ ¬ ⟨𝑎, 𝑏⟩ ∈ 𝑥) ↔ (𝑏𝑘 ∧ ∃𝑎𝑠 ¬ ⟨𝑎, 𝑏⟩ ∈ 𝑥))
113111, 112syl6bb 276 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑠 𝑅𝑘 𝑆) → (∃𝑎𝑠𝑢𝑘 (((2nd ↾ ( 𝑅 × 𝑆))‘⟨𝑎, 𝑢⟩) = 𝑏 ∧ ¬ ⟨𝑎, 𝑢⟩ ∈ 𝑥) ↔ (𝑏𝑘 ∧ ∃𝑎𝑠 ¬ ⟨𝑎, 𝑏⟩ ∈ 𝑥)))
11491, 113syl5bb 272 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑠 𝑅𝑘 𝑆) → (∃𝑡 ∈ ((𝑠 × 𝑘) ∖ 𝑥)((2nd ↾ ( 𝑅 × 𝑆))‘𝑡) = 𝑏 ↔ (𝑏𝑘 ∧ ∃𝑎𝑠 ¬ ⟨𝑎, 𝑏⟩ ∈ 𝑥)))
115 f2ndres 7235 . . . . . . . . . . . . . . . . . . . . . . . 24 (2nd ↾ ( 𝑅 × 𝑆)):( 𝑅 × 𝑆)⟶ 𝑆
116 ffn 6083 . . . . . . . . . . . . . . . . . . . . . . . 24 ((2nd ↾ ( 𝑅 × 𝑆)):( 𝑅 × 𝑆)⟶ 𝑆 → (2nd ↾ ( 𝑅 × 𝑆)) Fn ( 𝑅 × 𝑆))
117115, 116ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . 23 (2nd ↾ ( 𝑅 × 𝑆)) Fn ( 𝑅 × 𝑆)
118 difss 3770 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑠 × 𝑘) ∖ 𝑥) ⊆ (𝑠 × 𝑘)
119 xpss12 5158 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑠 𝑅𝑘 𝑆) → (𝑠 × 𝑘) ⊆ ( 𝑅 × 𝑆))
120118, 119syl5ss 3647 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑠 𝑅𝑘 𝑆) → ((𝑠 × 𝑘) ∖ 𝑥) ⊆ ( 𝑅 × 𝑆))
121 fvelimab 6292 . . . . . . . . . . . . . . . . . . . . . . 23 (((2nd ↾ ( 𝑅 × 𝑆)) Fn ( 𝑅 × 𝑆) ∧ ((𝑠 × 𝑘) ∖ 𝑥) ⊆ ( 𝑅 × 𝑆)) → (𝑏 ∈ ((2nd ↾ ( 𝑅 × 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ↔ ∃𝑡 ∈ ((𝑠 × 𝑘) ∖ 𝑥)((2nd ↾ ( 𝑅 × 𝑆))‘𝑡) = 𝑏))
122117, 120, 121sylancr 696 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑠 𝑅𝑘 𝑆) → (𝑏 ∈ ((2nd ↾ ( 𝑅 × 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ↔ ∃𝑡 ∈ ((𝑠 × 𝑘) ∖ 𝑥)((2nd ↾ ( 𝑅 × 𝑆))‘𝑡) = 𝑏))
123 eldif 3617 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑏 ∈ (𝑘 ∖ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ↔ (𝑏𝑘 ∧ ¬ 𝑏 ∈ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}))
124 simpr 476 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑠 𝑅𝑘 𝑆) → 𝑘 𝑆)
125124sselda 3636 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑠 𝑅𝑘 𝑆) ∧ 𝑏𝑘) → 𝑏 𝑆)
126 sneq 4220 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑣 = 𝑏 → {𝑣} = {𝑏})
127126xpeq2d 5173 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑣 = 𝑏 → (𝑠 × {𝑣}) = (𝑠 × {𝑏}))
128127sseq1d 3665 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑣 = 𝑏 → ((𝑠 × {𝑣}) ⊆ 𝑥 ↔ (𝑠 × {𝑏}) ⊆ 𝑥))
129 dfss3 3625 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑠 × {𝑏}) ⊆ 𝑥 ↔ ∀𝑘 ∈ (𝑠 × {𝑏})𝑘𝑥)
130 eleq1 2718 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑘 = ⟨𝑎, 𝑡⟩ → (𝑘𝑥 ↔ ⟨𝑎, 𝑡⟩ ∈ 𝑥))
131130ralxp 5296 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (∀𝑘 ∈ (𝑠 × {𝑏})𝑘𝑥 ↔ ∀𝑎𝑠𝑡 ∈ {𝑏}⟨𝑎, 𝑡⟩ ∈ 𝑥)
132 vex 3234 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 𝑏 ∈ V
133 opeq2 4434 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑡 = 𝑏 → ⟨𝑎, 𝑡⟩ = ⟨𝑎, 𝑏⟩)
134133eleq1d 2715 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑡 = 𝑏 → (⟨𝑎, 𝑡⟩ ∈ 𝑥 ↔ ⟨𝑎, 𝑏⟩ ∈ 𝑥))
135132, 134ralsn 4254 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (∀𝑡 ∈ {𝑏}⟨𝑎, 𝑡⟩ ∈ 𝑥 ↔ ⟨𝑎, 𝑏⟩ ∈ 𝑥)
136135ralbii 3009 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (∀𝑎𝑠𝑡 ∈ {𝑏}⟨𝑎, 𝑡⟩ ∈ 𝑥 ↔ ∀𝑎𝑠𝑎, 𝑏⟩ ∈ 𝑥)
137129, 131, 1363bitri 286 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑠 × {𝑏}) ⊆ 𝑥 ↔ ∀𝑎𝑠𝑎, 𝑏⟩ ∈ 𝑥)
138128, 137syl6bb 276 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑣 = 𝑏 → ((𝑠 × {𝑣}) ⊆ 𝑥 ↔ ∀𝑎𝑠𝑎, 𝑏⟩ ∈ 𝑥))
139138elrab3 3397 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑏 𝑆 → (𝑏 ∈ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ↔ ∀𝑎𝑠𝑎, 𝑏⟩ ∈ 𝑥))
140125, 139syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑠 𝑅𝑘 𝑆) ∧ 𝑏𝑘) → (𝑏 ∈ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ↔ ∀𝑎𝑠𝑎, 𝑏⟩ ∈ 𝑥))
141140notbid 307 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑠 𝑅𝑘 𝑆) ∧ 𝑏𝑘) → (¬ 𝑏 ∈ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ↔ ¬ ∀𝑎𝑠𝑎, 𝑏⟩ ∈ 𝑥))
142 rexnal 3024 . . . . . . . . . . . . . . . . . . . . . . . . 25 (∃𝑎𝑠 ¬ ⟨𝑎, 𝑏⟩ ∈ 𝑥 ↔ ¬ ∀𝑎𝑠𝑎, 𝑏⟩ ∈ 𝑥)
143141, 142syl6bbr 278 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑠 𝑅𝑘 𝑆) ∧ 𝑏𝑘) → (¬ 𝑏 ∈ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ↔ ∃𝑎𝑠 ¬ ⟨𝑎, 𝑏⟩ ∈ 𝑥))
144143pm5.32da 674 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑠 𝑅𝑘 𝑆) → ((𝑏𝑘 ∧ ¬ 𝑏 ∈ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ↔ (𝑏𝑘 ∧ ∃𝑎𝑠 ¬ ⟨𝑎, 𝑏⟩ ∈ 𝑥)))
145123, 144syl5bb 272 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑠 𝑅𝑘 𝑆) → (𝑏 ∈ (𝑘 ∖ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ↔ (𝑏𝑘 ∧ ∃𝑎𝑠 ¬ ⟨𝑎, 𝑏⟩ ∈ 𝑥)))
146114, 122, 1453bitr4d 300 . . . . . . . . . . . . . . . . . . . . 21 ((𝑠 𝑅𝑘 𝑆) → (𝑏 ∈ ((2nd ↾ ( 𝑅 × 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ↔ 𝑏 ∈ (𝑘 ∖ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})))
147146eqrdv 2649 . . . . . . . . . . . . . . . . . . . 20 ((𝑠 𝑅𝑘 𝑆) → ((2nd ↾ ( 𝑅 × 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) = (𝑘 ∖ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}))
14875, 77, 147syl2anc 694 . . . . . . . . . . . . . . . . . . 19 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → ((2nd ↾ ( 𝑅 × 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) = (𝑘 ∖ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}))
149 difin 3894 . . . . . . . . . . . . . . . . . . . 20 (𝑘 ∖ (𝑘 ∩ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})) = (𝑘 ∖ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})
15066adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → 𝑆 ∈ Top)
15118restuni 21014 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑆 ∈ Top ∧ 𝑘 𝑆) → 𝑘 = (𝑆t 𝑘))
152150, 77, 151syl2anc 694 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → 𝑘 = (𝑆t 𝑘))
153152difeq1d 3760 . . . . . . . . . . . . . . . . . . . 20 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → (𝑘 ∖ (𝑘 ∩ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})) = ( (𝑆t 𝑘) ∖ (𝑘 ∩ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})))
154149, 153syl5eqr 2699 . . . . . . . . . . . . . . . . . . 19 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → (𝑘 ∖ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) = ( (𝑆t 𝑘) ∖ (𝑘 ∩ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})))
155148, 154eqtrd 2685 . . . . . . . . . . . . . . . . . 18 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → ((2nd ↾ ( 𝑅 × 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) = ( (𝑆t 𝑘) ∖ (𝑘 ∩ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})))
15616ad2antrr 762 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → 𝑆 ∈ (ran 𝑘Gen ∩ Haus))
157156elin2d 3836 . . . . . . . . . . . . . . . . . . . 20 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → 𝑆 ∈ Haus)
158 df-ima 5156 . . . . . . . . . . . . . . . . . . . . . . 23 ((2nd ↾ ( 𝑅 × 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) = ran ((2nd ↾ ( 𝑅 × 𝑆)) ↾ ((𝑠 × 𝑘) ∖ 𝑥))
159 resres 5444 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((2nd ↾ ( 𝑅 × 𝑆)) ↾ ((𝑠 × 𝑘) ∖ 𝑥)) = (2nd ↾ (( 𝑅 × 𝑆) ∩ ((𝑠 × 𝑘) ∖ 𝑥)))
160 inss2 3867 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (( 𝑅 × 𝑆) ∩ ((𝑠 × 𝑘) ∖ 𝑥)) ⊆ ((𝑠 × 𝑘) ∖ 𝑥)
161160, 118sstri 3645 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (( 𝑅 × 𝑆) ∩ ((𝑠 × 𝑘) ∖ 𝑥)) ⊆ (𝑠 × 𝑘)
162 ssres2 5460 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((( 𝑅 × 𝑆) ∩ ((𝑠 × 𝑘) ∖ 𝑥)) ⊆ (𝑠 × 𝑘) → (2nd ↾ (( 𝑅 × 𝑆) ∩ ((𝑠 × 𝑘) ∖ 𝑥))) ⊆ (2nd ↾ (𝑠 × 𝑘)))
163161, 162ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . 25 (2nd ↾ (( 𝑅 × 𝑆) ∩ ((𝑠 × 𝑘) ∖ 𝑥))) ⊆ (2nd ↾ (𝑠 × 𝑘))
164159, 163eqsstri 3668 . . . . . . . . . . . . . . . . . . . . . . . 24 ((2nd ↾ ( 𝑅 × 𝑆)) ↾ ((𝑠 × 𝑘) ∖ 𝑥)) ⊆ (2nd ↾ (𝑠 × 𝑘))
165 rnss 5386 . . . . . . . . . . . . . . . . . . . . . . . 24 (((2nd ↾ ( 𝑅 × 𝑆)) ↾ ((𝑠 × 𝑘) ∖ 𝑥)) ⊆ (2nd ↾ (𝑠 × 𝑘)) → ran ((2nd ↾ ( 𝑅 × 𝑆)) ↾ ((𝑠 × 𝑘) ∖ 𝑥)) ⊆ ran (2nd ↾ (𝑠 × 𝑘)))
166164, 165ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . 23 ran ((2nd ↾ ( 𝑅 × 𝑆)) ↾ ((𝑠 × 𝑘) ∖ 𝑥)) ⊆ ran (2nd ↾ (𝑠 × 𝑘))
167158, 166eqsstri 3668 . . . . . . . . . . . . . . . . . . . . . 22 ((2nd ↾ ( 𝑅 × 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ⊆ ran (2nd ↾ (𝑠 × 𝑘))
168 f2ndres 7235 . . . . . . . . . . . . . . . . . . . . . . 23 (2nd ↾ (𝑠 × 𝑘)):(𝑠 × 𝑘)⟶𝑘
169 frn 6091 . . . . . . . . . . . . . . . . . . . . . . 23 ((2nd ↾ (𝑠 × 𝑘)):(𝑠 × 𝑘)⟶𝑘 → ran (2nd ↾ (𝑠 × 𝑘)) ⊆ 𝑘)
170168, 169ax-mp 5 . . . . . . . . . . . . . . . . . . . . . 22 ran (2nd ↾ (𝑠 × 𝑘)) ⊆ 𝑘
171167, 170sstri 3645 . . . . . . . . . . . . . . . . . . . . 21 ((2nd ↾ ( 𝑅 × 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ⊆ 𝑘
172171, 77syl5ss 3647 . . . . . . . . . . . . . . . . . . . 20 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → ((2nd ↾ ( 𝑅 × 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ⊆ 𝑆)
17313ad2antrr 762 . . . . . . . . . . . . . . . . . . . . . 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 21461 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑅 ∈ (TopOn‘ 𝑅) ∧ 𝑆 ∈ (TopOn‘ 𝑆)) → (2nd ↾ ( 𝑅 × 𝑆)) ∈ ((𝑅 ×t 𝑆) Cn 𝑆))
176173, 174, 175syl2anc 694 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → (2nd ↾ ( 𝑅 × 𝑆)) ∈ ((𝑅 ×t 𝑆) Cn 𝑆))
17727ad2antrr 762 . . . . . . . . . . . . . . . . . . . . . . 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 3234 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑠 ∈ V
180 vex 3234 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑘 ∈ V
181179, 180xpex 7004 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑠 × 𝑘) ∈ V
182181a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → (𝑠 × 𝑘) ∈ V)
183 restabs 21017 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑅 ×t 𝑆) ∈ Top ∧ ((𝑠 × 𝑘) ∖ 𝑥) ⊆ (𝑠 × 𝑘) ∧ (𝑠 × 𝑘) ∈ V) → (((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ↾t ((𝑠 × 𝑘) ∖ 𝑥)) = ((𝑅 ×t 𝑆) ↾t ((𝑠 × 𝑘) ∖ 𝑥)))
184177, 178, 182, 183syl3anc 1366 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → (((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ↾t ((𝑠 × 𝑘) ∖ 𝑥)) = ((𝑅 ×t 𝑆) ↾t ((𝑠 × 𝑘) ∖ 𝑥)))
18565adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 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 809 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → 𝑘 ∈ 𝒫 𝑆)
189 txrest 21482 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑠 ∈ V ∧ 𝑘 ∈ 𝒫 𝑆)) → ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) = ((𝑅t 𝑠) ×t (𝑆t 𝑘)))
190185, 186, 187, 188, 189syl22anc 1367 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) = ((𝑅t 𝑠) ×t (𝑆t 𝑘)))
191 simprr3 1131 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → (𝑅t 𝑠) ∈ Comp)
192191adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → (𝑅t 𝑠) ∈ Comp)
193 simprr 811 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → (𝑆t 𝑘) ∈ Comp)
194 txcmp 21494 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑅t 𝑠) ∈ Comp ∧ (𝑆t 𝑘) ∈ Comp) → ((𝑅t 𝑠) ×t (𝑆t 𝑘)) ∈ Comp)
195192, 193, 194syl2anc 694 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → ((𝑅t 𝑠) ×t (𝑆t 𝑘)) ∈ Comp)
196190, 195eqeltrd 2730 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ∈ Comp)
197 difin 3894 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑠 × 𝑘) ∖ ((𝑠 × 𝑘) ∩ 𝑥)) = ((𝑠 × 𝑘) ∖ 𝑥)
19875, 77, 119syl2anc 694 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → (𝑠 × 𝑘) ⊆ ( 𝑅 × 𝑆))
199185, 150, 25syl2anc 694 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → ( 𝑅 × 𝑆) = (𝑅 ×t 𝑆))
200198, 199sseqtrd 3674 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → (𝑠 × 𝑘) ⊆ (𝑅 ×t 𝑆))
20128restuni 21014 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑅 ×t 𝑆) ∈ Top ∧ (𝑠 × 𝑘) ⊆ (𝑅 ×t 𝑆)) → (𝑠 × 𝑘) = ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)))
202177, 200, 201syl2anc 694 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → (𝑠 × 𝑘) = ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)))
203202difeq1d 3760 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → ((𝑠 × 𝑘) ∖ ((𝑠 × 𝑘) ∩ 𝑥)) = ( ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ∖ ((𝑠 × 𝑘) ∩ 𝑥)))
204197, 203syl5eqr 2699 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → ((𝑠 × 𝑘) ∖ 𝑥) = ( ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ∖ ((𝑠 × 𝑘) ∩ 𝑥)))
205 resttop 21012 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑅 ×t 𝑆) ∈ Top ∧ (𝑠 × 𝑘) ∈ V) → ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ∈ Top)
206177, 181, 205sylancl 695 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ∈ Top)
207 incom 3838 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑠 × 𝑘) ∩ 𝑥) = (𝑥 ∩ (𝑠 × 𝑘))
20822ad2antrr 762 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆)))
209 kgeni 21388 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆)) ∧ ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ∈ Comp) → (𝑥 ∩ (𝑠 × 𝑘)) ∈ ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)))
210208, 196, 209syl2anc 694 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → (𝑥 ∩ (𝑠 × 𝑘)) ∈ ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)))
211207, 210syl5eqel 2734 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → ((𝑠 × 𝑘) ∩ 𝑥) ∈ ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)))
212 eqid 2651 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) = ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘))
213212opncld 20885 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ∈ Top ∧ ((𝑠 × 𝑘) ∩ 𝑥) ∈ ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘))) → ( ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ∖ ((𝑠 × 𝑘) ∩ 𝑥)) ∈ (Clsd‘((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘))))
214206, 211, 213syl2anc 694 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → ( ((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ∖ ((𝑠 × 𝑘) ∩ 𝑥)) ∈ (Clsd‘((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘))))
215204, 214eqeltrd 2730 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → ((𝑠 × 𝑘) ∖ 𝑥) ∈ (Clsd‘((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘))))
216 cmpcld 21253 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ∈ Comp ∧ ((𝑠 × 𝑘) ∖ 𝑥) ∈ (Clsd‘((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)))) → (((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ↾t ((𝑠 × 𝑘) ∖ 𝑥)) ∈ Comp)
217196, 215, 216syl2anc 694 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → (((𝑅 ×t 𝑆) ↾t (𝑠 × 𝑘)) ↾t ((𝑠 × 𝑘) ∖ 𝑥)) ∈ Comp)
218184, 217eqeltrrd 2731 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → ((𝑅 ×t 𝑆) ↾t ((𝑠 × 𝑘) ∖ 𝑥)) ∈ Comp)
219 imacmp 21248 . . . . . . . . . . . . . . . . . . . . 21 (((2nd ↾ ( 𝑅 × 𝑆)) ∈ ((𝑅 ×t 𝑆) Cn 𝑆) ∧ ((𝑅 ×t 𝑆) ↾t ((𝑠 × 𝑘) ∖ 𝑥)) ∈ Comp) → (𝑆t ((2nd ↾ ( 𝑅 × 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥))) ∈ Comp)
220176, 218, 219syl2anc 694 . . . . . . . . . . . . . . . . . . . 20 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → (𝑆t ((2nd ↾ ( 𝑅 × 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥))) ∈ Comp)
22118hauscmp 21258 . . . . . . . . . . . . . . . . . . . 20 ((𝑆 ∈ Haus ∧ ((2nd ↾ ( 𝑅 × 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ⊆ 𝑆 ∧ (𝑆t ((2nd ↾ ( 𝑅 × 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥))) ∈ Comp) → ((2nd ↾ ( 𝑅 × 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ∈ (Clsd‘𝑆))
222157, 172, 220, 221syl3anc 1366 . . . . . . . . . . . . . . . . . . 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 21025 . . . . . . . . . . . . . . . . . . 19 ((𝑘 𝑆 ∧ ((2nd ↾ ( 𝑅 × 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ∈ (Clsd‘𝑆) ∧ ((2nd ↾ ( 𝑅 × 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ⊆ 𝑘) → ((2nd ↾ ( 𝑅 × 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ∈ (Clsd‘(𝑆t 𝑘)))
22577, 222, 223, 224syl3anc 1366 . . . . . . . . . . . . . . . . . 18 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → ((2nd ↾ ( 𝑅 × 𝑆)) “ ((𝑠 × 𝑘) ∖ 𝑥)) ∈ (Clsd‘(𝑆t 𝑘)))
226155, 225eqeltrrd 2731 . . . . . . . . . . . . . . . . 17 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → ( (𝑆t 𝑘) ∖ (𝑘 ∩ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})) ∈ (Clsd‘(𝑆t 𝑘)))
227 resttop 21012 . . . . . . . . . . . . . . . . . . 19 ((𝑆 ∈ Top ∧ 𝑘 ∈ 𝒫 𝑆) → (𝑆t 𝑘) ∈ Top)
228150, 188, 227syl2anc 694 . . . . . . . . . . . . . . . . . 18 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → (𝑆t 𝑘) ∈ Top)
229 inss1 3866 . . . . . . . . . . . . . . . . . . 19 (𝑘 ∩ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ⊆ 𝑘
230229, 152syl5sseq 3686 . . . . . . . . . . . . . . . . . 18 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ (𝑘 ∈ 𝒫 𝑆 ∧ (𝑆t 𝑘) ∈ Comp)) → (𝑘 ∩ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ⊆ (𝑆t 𝑘))
231 eqid 2651 . . . . . . . . . . . . . . . . . . 19 (𝑆t 𝑘) = (𝑆t 𝑘)
232231isopn2 20884 . . . . . . . . . . . . . . . . . 18 (((𝑆t 𝑘) ∈ Top ∧ (𝑘 ∩ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ⊆ (𝑆t 𝑘)) → ((𝑘 ∩ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ∈ (𝑆t 𝑘) ↔ ( (𝑆t 𝑘) ∖ (𝑘 ∩ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})) ∈ (Clsd‘(𝑆t 𝑘))))
233228, 230, 232syl2anc 694 . . . . . . . . . . . . . . . . 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 2734 . . . . . . . . . . . . . . 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 2995 . . . . . . . . . . . . 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 21387 . . . . . . . . . . . . . 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 977 . . . . . . . . . . . 12 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ∈ (𝑘Gen‘𝑆))
24216adantr 480 . . . . . . . . . . . . . 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 21398 . . . . . . . . . . . . 13 (𝑆 ∈ ran 𝑘Gen → (𝑘Gen‘𝑆) = 𝑆)
245243, 244syl 17 . . . . . . . . . . . 12 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → (𝑘Gen‘𝑆) = 𝑆)
246241, 245eleqtrd 2732 . . . . . . . . . . 11 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ∈ 𝑆)
247 txopn 21453 . . . . . . . . . . 11 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑢𝑅 ∧ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ∈ 𝑆)) → (𝑢 × {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ∈ (𝑅 ×t 𝑆))
24865, 66, 67, 246, 247syl22anc 1367 . . . . . . . . . 10 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → (𝑢 × {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ∈ (𝑅 ×t 𝑆))
24957adantr 480 . . . . . . . . . . 11 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → 𝑦 = ⟨(1st𝑦), (2nd𝑦)⟩)
250 simprr1 1129 . . . . . . . . . . . 12 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → (1st𝑦) ∈ 𝑢)
25134adantr 480 . . . . . . . . . . . . 13 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → (2nd𝑦) ∈ 𝑆)
252 relxp 5160 . . . . . . . . . . . . . . 15 Rel (𝑠 × {(2nd𝑦)})
253252a1i 11 . . . . . . . . . . . . . 14 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → Rel (𝑠 × {(2nd𝑦)}))
254 opelxp 5180 . . . . . . . . . . . . . . 15 (⟨𝑎, 𝑏⟩ ∈ (𝑠 × {(2nd𝑦)}) ↔ (𝑎𝑠𝑏 ∈ {(2nd𝑦)}))
25572sselda 3636 . . . . . . . . . . . . . . . . . 18 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ 𝑎𝑠) → 𝑎 ∈ {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥})
256 opeq1 4433 . . . . . . . . . . . . . . . . . . . . 21 (𝑡 = 𝑎 → ⟨𝑡, (2nd𝑦)⟩ = ⟨𝑎, (2nd𝑦)⟩)
257256eleq1d 2715 . . . . . . . . . . . . . . . . . . . 20 (𝑡 = 𝑎 → (⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥 ↔ ⟨𝑎, (2nd𝑦)⟩ ∈ 𝑥))
258257elrab 3396 . . . . . . . . . . . . . . . . . . 19 (𝑎 ∈ {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ↔ (𝑎 𝑅 ∧ ⟨𝑎, (2nd𝑦)⟩ ∈ 𝑥))
259258simprbi 479 . . . . . . . . . . . . . . . . . 18 (𝑎 ∈ {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} → ⟨𝑎, (2nd𝑦)⟩ ∈ 𝑥)
260255, 259syl 17 . . . . . . . . . . . . . . . . 17 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ 𝑎𝑠) → ⟨𝑎, (2nd𝑦)⟩ ∈ 𝑥)
261 elsni 4227 . . . . . . . . . . . . . . . . . . 19 (𝑏 ∈ {(2nd𝑦)} → 𝑏 = (2nd𝑦))
262261opeq2d 4440 . . . . . . . . . . . . . . . . . 18 (𝑏 ∈ {(2nd𝑦)} → ⟨𝑎, 𝑏⟩ = ⟨𝑎, (2nd𝑦)⟩)
263262eleq1d 2715 . . . . . . . . . . . . . . . . 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 5246 . . . . . . . . . . . . 13 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → (𝑠 × {(2nd𝑦)}) ⊆ 𝑥)
268 sneq 4220 . . . . . . . . . . . . . . . 16 (𝑣 = (2nd𝑦) → {𝑣} = {(2nd𝑦)})
269268xpeq2d 5173 . . . . . . . . . . . . . . 15 (𝑣 = (2nd𝑦) → (𝑠 × {𝑣}) = (𝑠 × {(2nd𝑦)}))
270269sseq1d 3665 . . . . . . . . . . . . . 14 (𝑣 = (2nd𝑦) → ((𝑠 × {𝑣}) ⊆ 𝑥 ↔ (𝑠 × {(2nd𝑦)}) ⊆ 𝑥))
271270elrab 3396 . . . . . . . . . . . . 13 ((2nd𝑦) ∈ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ↔ ((2nd𝑦) ∈ 𝑆 ∧ (𝑠 × {(2nd𝑦)}) ⊆ 𝑥))
272251, 267, 271sylanbrc 699 . . . . . . . . . . . 12 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → (2nd𝑦) ∈ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})
273250, 272opelxpd 5183 . . . . . . . . . . 11 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → ⟨(1st𝑦), (2nd𝑦)⟩ ∈ (𝑢 × {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}))
274249, 273eqeltrd 2730 . . . . . . . . . 10 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → 𝑦 ∈ (𝑢 × {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}))
275 relxp 5160 . . . . . . . . . . . 12 Rel (𝑢 × {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})
276275a1i 11 . . . . . . . . . . 11 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → Rel (𝑢 × {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}))
277 opelxp 5180 . . . . . . . . . . . 12 (⟨𝑎, 𝑏⟩ ∈ (𝑢 × {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ↔ (𝑎𝑢𝑏 ∈ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}))
278128elrab 3396 . . . . . . . . . . . . . . 15 (𝑏 ∈ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} ↔ (𝑏 𝑆 ∧ (𝑠 × {𝑏}) ⊆ 𝑥))
279278simprbi 479 . . . . . . . . . . . . . 14 (𝑏 ∈ {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥} → (𝑠 × {𝑏}) ⊆ 𝑥)
280 simprr2 1130 . . . . . . . . . . . . . . . 16 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → 𝑢𝑠)
281280sselda 3636 . . . . . . . . . . . . . . 15 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ 𝑎𝑢) → 𝑎𝑠)
282 vsnid 4242 . . . . . . . . . . . . . . 15 𝑏 ∈ {𝑏}
283 opelxpi 5182 . . . . . . . . . . . . . . 15 ((𝑎𝑠𝑏 ∈ {𝑏}) → ⟨𝑎, 𝑏⟩ ∈ (𝑠 × {𝑏}))
284281, 282, 283sylancl 695 . . . . . . . . . . . . . 14 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) ∧ 𝑎𝑢) → ⟨𝑎, 𝑏⟩ ∈ (𝑠 × {𝑏}))
285 ssel 3630 . . . . . . . . . . . . . 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 5246 . . . . . . . . . 10 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) ∧ 𝑦𝑥) ∧ ((𝑠 ∈ 𝒫 {𝑡 𝑅 ∣ ⟨𝑡, (2nd𝑦)⟩ ∈ 𝑥} ∧ 𝑢𝑅) ∧ ((1st𝑦) ∈ 𝑢𝑢𝑠 ∧ (𝑅t 𝑠) ∈ Comp))) → (𝑢 × {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ⊆ 𝑥)
290 eleq2 2719 . . . . . . . . . . . 12 (𝑡 = (𝑢 × {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) → (𝑦𝑡𝑦 ∈ (𝑢 × {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥})))
291 sseq1 3659 . . . . . . . . . . . 12 (𝑡 = (𝑢 × {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) → (𝑡𝑥 ↔ (𝑢 × {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ⊆ 𝑥))
292290, 291anbi12d 747 . . . . . . . . . . 11 (𝑡 = (𝑢 × {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) → ((𝑦𝑡𝑡𝑥) ↔ (𝑦 ∈ (𝑢 × {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ∧ (𝑢 × {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ⊆ 𝑥)))
293292rspcev 3340 . . . . . . . . . 10 (((𝑢 × {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ∈ (𝑅 ×t 𝑆) ∧ (𝑦 ∈ (𝑢 × {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ∧ (𝑢 × {𝑣 𝑆 ∣ (𝑠 × {𝑣}) ⊆ 𝑥}) ⊆ 𝑥)) → ∃𝑡 ∈ (𝑅 ×t 𝑆)(𝑦𝑡𝑡𝑥))
294248, 274, 289, 293syl12anc 1364 . . . . . . . . 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 3067 . . . . . . 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 2995 . . . . 5 (((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) → ∀𝑦𝑥𝑡 ∈ (𝑅 ×t 𝑆)(𝑦𝑡𝑡𝑥))
2996adantr 480 . . . . . 6 (((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) ∧ 𝑥 ∈ (𝑘Gen‘(𝑅 ×t 𝑆))) → (𝑅 ×t 𝑆) ∈ Top)
300 eltop2 20827 . . . . . 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 3642 . 2 ((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) → (𝑘Gen‘(𝑅 ×t 𝑆)) ⊆ (𝑅 ×t 𝑆))
305 iskgen2 21399 . 2 ((𝑅 ×t 𝑆) ∈ ran 𝑘Gen ↔ ((𝑅 ×t 𝑆) ∈ Top ∧ (𝑘Gen‘(𝑅 ×t 𝑆)) ⊆ (𝑅 ×t 𝑆)))
3066, 304, 305sylanbrc 699 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 1054   = wceq 1523  wcel 2030  wral 2941  wrex 2942  {crab 2945  Vcvv 3231  cdif 3604  cin 3606  wss 3607  𝒫 cpw 4191  {csn 4210  cop 4216   cuni 4468  cmpt 4762   I cid 5052   × cxp 5141  ccnv 5142  ran crn 5144  cres 5145  cima 5146  Rel wrel 5148   Fn wfn 5921  wf 5922  cfv 5926  (class class class)co 6690  1st c1st 7208  2nd c2nd 7209  t crest 16128  Topctop 20746  TopOnctopon 20763  Clsdccld 20868   Cn ccn 21076  Hauscha 21160  Compccmp 21237  𝑛-Locally cnlly 21316  𝑘Genckgen 21384   ×t ctx 21411
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-reu 2948  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-iin 4555  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-oadd 7609  df-er 7787  df-map 7901  df-en 7998  df-dom 7999  df-fin 8001  df-fi 8358  df-rest 16130  df-topgen 16151  df-top 20747  df-topon 20764  df-bases 20798  df-cld 20871  df-ntr 20872  df-cls 20873  df-nei 20950  df-cn 21079  df-cnp 21080  df-haus 21167  df-cmp 21238  df-nlly 21318  df-kgen 21385  df-tx 21413
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator