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

Theorem txkgen 23569
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 23390 . . 3 (𝑅 ∈ 𝑛-Locally Comp β†’ 𝑅 ∈ Top)
2 elinel1 4195 . . . 4 (𝑆 ∈ (ran π‘˜Gen ∩ Haus) β†’ 𝑆 ∈ ran π‘˜Gen)
3 kgentop 23459 . . . 4 (𝑆 ∈ ran π‘˜Gen β†’ 𝑆 ∈ Top)
42, 3syl 17 . . 3 (𝑆 ∈ (ran π‘˜Gen ∩ Haus) β†’ 𝑆 ∈ Top)
5 txtop 23486 . . 3 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ (𝑅 Γ—t 𝑆) ∈ Top)
61, 4, 5syl2an 595 . 2 ((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) β†’ (𝑅 Γ—t 𝑆) ∈ Top)
7 simplll 774 . . . . . . . 8 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) β†’ 𝑅 ∈ 𝑛-Locally Comp)
8 eqid 2728 . . . . . . . . . 10 (𝑑 ∈ βˆͺ 𝑅 ↦ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩) = (𝑑 ∈ βˆͺ 𝑅 ↦ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩)
98mptpreima 6242 . . . . . . . . 9 (β—‘(𝑑 ∈ βˆͺ 𝑅 ↦ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩) β€œ π‘₯) = {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯}
101ad3antrrr 729 . . . . . . . . . . . . . 14 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) β†’ 𝑅 ∈ Top)
11 toptopon2 22833 . . . . . . . . . . . . . 14 (𝑅 ∈ Top ↔ 𝑅 ∈ (TopOnβ€˜βˆͺ 𝑅))
1210, 11sylib 217 . . . . . . . . . . . . 13 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) β†’ 𝑅 ∈ (TopOnβ€˜βˆͺ 𝑅))
13 idcn 23174 . . . . . . . . . . . . 13 (𝑅 ∈ (TopOnβ€˜βˆͺ 𝑅) β†’ ( I β†Ύ βˆͺ 𝑅) ∈ (𝑅 Cn 𝑅))
1412, 13syl 17 . . . . . . . . . . . 12 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) β†’ ( I β†Ύ βˆͺ 𝑅) ∈ (𝑅 Cn 𝑅))
15 simpllr 775 . . . . . . . . . . . . . . 15 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) β†’ 𝑆 ∈ (ran π‘˜Gen ∩ Haus))
1615, 4syl 17 . . . . . . . . . . . . . 14 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) β†’ 𝑆 ∈ Top)
17 toptopon2 22833 . . . . . . . . . . . . . 14 (𝑆 ∈ Top ↔ 𝑆 ∈ (TopOnβ€˜βˆͺ 𝑆))
1816, 17sylib 217 . . . . . . . . . . . . 13 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) β†’ 𝑆 ∈ (TopOnβ€˜βˆͺ 𝑆))
19 simpr 484 . . . . . . . . . . . . . . . 16 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) β†’ 𝑦 ∈ π‘₯)
20 simplr 768 . . . . . . . . . . . . . . . 16 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) β†’ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆)))
21 elunii 4913 . . . . . . . . . . . . . . . 16 ((𝑦 ∈ π‘₯ ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) β†’ 𝑦 ∈ βˆͺ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆)))
2219, 20, 21syl2anc 583 . . . . . . . . . . . . . . 15 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) β†’ 𝑦 ∈ βˆͺ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆)))
23 eqid 2728 . . . . . . . . . . . . . . . . . 18 βˆͺ 𝑅 = βˆͺ 𝑅
24 eqid 2728 . . . . . . . . . . . . . . . . . 18 βˆͺ 𝑆 = βˆͺ 𝑆
2523, 24txuni 23509 . . . . . . . . . . . . . . . . 17 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ (βˆͺ 𝑅 Γ— βˆͺ 𝑆) = βˆͺ (𝑅 Γ—t 𝑆))
2610, 16, 25syl2anc 583 . . . . . . . . . . . . . . . 16 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) β†’ (βˆͺ 𝑅 Γ— βˆͺ 𝑆) = βˆͺ (𝑅 Γ—t 𝑆))
2710, 16, 5syl2anc 583 . . . . . . . . . . . . . . . . 17 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) β†’ (𝑅 Γ—t 𝑆) ∈ Top)
28 eqid 2728 . . . . . . . . . . . . . . . . . 18 βˆͺ (𝑅 Γ—t 𝑆) = βˆͺ (𝑅 Γ—t 𝑆)
2928kgenuni 23456 . . . . . . . . . . . . . . . . 17 ((𝑅 Γ—t 𝑆) ∈ Top β†’ βˆͺ (𝑅 Γ—t 𝑆) = βˆͺ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆)))
3027, 29syl 17 . . . . . . . . . . . . . . . 16 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) β†’ βˆͺ (𝑅 Γ—t 𝑆) = βˆͺ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆)))
3126, 30eqtrd 2768 . . . . . . . . . . . . . . 15 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) β†’ (βˆͺ 𝑅 Γ— βˆͺ 𝑆) = βˆͺ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆)))
3222, 31eleqtrrd 2832 . . . . . . . . . . . . . 14 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) β†’ 𝑦 ∈ (βˆͺ 𝑅 Γ— βˆͺ 𝑆))
33 xp2nd 8026 . . . . . . . . . . . . . 14 (𝑦 ∈ (βˆͺ 𝑅 Γ— βˆͺ 𝑆) β†’ (2nd β€˜π‘¦) ∈ βˆͺ 𝑆)
3432, 33syl 17 . . . . . . . . . . . . 13 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) β†’ (2nd β€˜π‘¦) ∈ βˆͺ 𝑆)
35 cnconst2 23200 . . . . . . . . . . . . 13 ((𝑅 ∈ (TopOnβ€˜βˆͺ 𝑅) ∧ 𝑆 ∈ (TopOnβ€˜βˆͺ 𝑆) ∧ (2nd β€˜π‘¦) ∈ βˆͺ 𝑆) β†’ (βˆͺ 𝑅 Γ— {(2nd β€˜π‘¦)}) ∈ (𝑅 Cn 𝑆))
3612, 18, 34, 35syl3anc 1369 . . . . . . . . . . . 12 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) β†’ (βˆͺ 𝑅 Γ— {(2nd β€˜π‘¦)}) ∈ (𝑅 Cn 𝑆))
37 fvresi 7182 . . . . . . . . . . . . . . . 16 (𝑑 ∈ βˆͺ 𝑅 β†’ (( I β†Ύ βˆͺ 𝑅)β€˜π‘‘) = 𝑑)
38 fvex 6910 . . . . . . . . . . . . . . . . 17 (2nd β€˜π‘¦) ∈ V
3938fvconst2 7216 . . . . . . . . . . . . . . . 16 (𝑑 ∈ βˆͺ 𝑅 β†’ ((βˆͺ 𝑅 Γ— {(2nd β€˜π‘¦)})β€˜π‘‘) = (2nd β€˜π‘¦))
4037, 39opeq12d 4882 . . . . . . . . . . . . . . 15 (𝑑 ∈ βˆͺ 𝑅 β†’ ⟨(( I β†Ύ βˆͺ 𝑅)β€˜π‘‘), ((βˆͺ 𝑅 Γ— {(2nd β€˜π‘¦)})β€˜π‘‘)⟩ = βŸ¨π‘‘, (2nd β€˜π‘¦)⟩)
4140mpteq2ia 5251 . . . . . . . . . . . . . 14 (𝑑 ∈ βˆͺ 𝑅 ↦ ⟨(( I β†Ύ βˆͺ 𝑅)β€˜π‘‘), ((βˆͺ 𝑅 Γ— {(2nd β€˜π‘¦)})β€˜π‘‘)⟩) = (𝑑 ∈ βˆͺ 𝑅 ↦ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩)
4241eqcomi 2737 . . . . . . . . . . . . 13 (𝑑 ∈ βˆͺ 𝑅 ↦ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩) = (𝑑 ∈ βˆͺ 𝑅 ↦ ⟨(( I β†Ύ βˆͺ 𝑅)β€˜π‘‘), ((βˆͺ 𝑅 Γ— {(2nd β€˜π‘¦)})β€˜π‘‘)⟩)
4323, 42txcnmpt 23541 . . . . . . . . . . . 12 ((( I β†Ύ βˆͺ 𝑅) ∈ (𝑅 Cn 𝑅) ∧ (βˆͺ 𝑅 Γ— {(2nd β€˜π‘¦)}) ∈ (𝑅 Cn 𝑆)) β†’ (𝑑 ∈ βˆͺ 𝑅 ↦ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩) ∈ (𝑅 Cn (𝑅 Γ—t 𝑆)))
4414, 36, 43syl2anc 583 . . . . . . . . . . 11 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) β†’ (𝑑 ∈ βˆͺ 𝑅 ↦ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩) ∈ (𝑅 Cn (𝑅 Γ—t 𝑆)))
45 llycmpkgen 23469 . . . . . . . . . . . . 13 (𝑅 ∈ 𝑛-Locally Comp β†’ 𝑅 ∈ ran π‘˜Gen)
4645ad3antrrr 729 . . . . . . . . . . . 12 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) β†’ 𝑅 ∈ ran π‘˜Gen)
476ad2antrr 725 . . . . . . . . . . . 12 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) β†’ (𝑅 Γ—t 𝑆) ∈ Top)
48 kgencn3 23475 . . . . . . . . . . . 12 ((𝑅 ∈ ran π‘˜Gen ∧ (𝑅 Γ—t 𝑆) ∈ Top) β†’ (𝑅 Cn (𝑅 Γ—t 𝑆)) = (𝑅 Cn (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))))
4946, 47, 48syl2anc 583 . . . . . . . . . . 11 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) β†’ (𝑅 Cn (𝑅 Γ—t 𝑆)) = (𝑅 Cn (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))))
5044, 49eleqtrd 2831 . . . . . . . . . 10 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) β†’ (𝑑 ∈ βˆͺ 𝑅 ↦ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩) ∈ (𝑅 Cn (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))))
51 cnima 23182 . . . . . . . . . 10 (((𝑑 ∈ βˆͺ 𝑅 ↦ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩) ∈ (𝑅 Cn (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) β†’ (β—‘(𝑑 ∈ βˆͺ 𝑅 ↦ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩) β€œ π‘₯) ∈ 𝑅)
5250, 20, 51syl2anc 583 . . . . . . . . 9 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) β†’ (β—‘(𝑑 ∈ βˆͺ 𝑅 ↦ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩) β€œ π‘₯) ∈ 𝑅)
539, 52eqeltrrid 2834 . . . . . . . 8 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) β†’ {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∈ 𝑅)
54 opeq1 4874 . . . . . . . . . 10 (𝑑 = (1st β€˜π‘¦) β†’ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ = ⟨(1st β€˜π‘¦), (2nd β€˜π‘¦)⟩)
5554eleq1d 2814 . . . . . . . . 9 (𝑑 = (1st β€˜π‘¦) β†’ (βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯ ↔ ⟨(1st β€˜π‘¦), (2nd β€˜π‘¦)⟩ ∈ π‘₯))
56 xp1st 8025 . . . . . . . . . 10 (𝑦 ∈ (βˆͺ 𝑅 Γ— βˆͺ 𝑆) β†’ (1st β€˜π‘¦) ∈ βˆͺ 𝑅)
5732, 56syl 17 . . . . . . . . 9 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) β†’ (1st β€˜π‘¦) ∈ βˆͺ 𝑅)
58 1st2nd2 8032 . . . . . . . . . . 11 (𝑦 ∈ (βˆͺ 𝑅 Γ— βˆͺ 𝑆) β†’ 𝑦 = ⟨(1st β€˜π‘¦), (2nd β€˜π‘¦)⟩)
5932, 58syl 17 . . . . . . . . . 10 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) β†’ 𝑦 = ⟨(1st β€˜π‘¦), (2nd β€˜π‘¦)⟩)
6059, 19eqeltrrd 2830 . . . . . . . . 9 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) β†’ ⟨(1st β€˜π‘¦), (2nd β€˜π‘¦)⟩ ∈ π‘₯)
6155, 57, 60elrabd 3684 . . . . . . . 8 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) β†’ (1st β€˜π‘¦) ∈ {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯})
62 nlly2i 23393 . . . . . . . 8 ((𝑅 ∈ 𝑛-Locally Comp ∧ {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∈ 𝑅 ∧ (1st β€˜π‘¦) ∈ {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯}) β†’ βˆƒπ‘  ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯}βˆƒπ‘’ ∈ 𝑅 ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))
637, 53, 61, 62syl3anc 1369 . . . . . . 7 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) β†’ βˆƒπ‘  ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯}βˆƒπ‘’ ∈ 𝑅 ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))
6410adantr 480 . . . . . . . . . . 11 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) β†’ 𝑅 ∈ Top)
6516adantr 480 . . . . . . . . . . 11 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) β†’ 𝑆 ∈ Top)
66 simprlr 779 . . . . . . . . . . 11 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) β†’ 𝑒 ∈ 𝑅)
67 ssrab2 4075 . . . . . . . . . . . . . 14 {𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯} βŠ† βˆͺ 𝑆
6867a1i 11 . . . . . . . . . . . . 13 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) β†’ {𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯} βŠ† βˆͺ 𝑆)
69 incom 4201 . . . . . . . . . . . . . . . 16 ({𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯} ∩ π‘˜) = (π‘˜ ∩ {𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯})
70 simprll 778 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) β†’ 𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯})
7170elpwid 4612 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) β†’ 𝑠 βŠ† {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯})
72 ssrab2 4075 . . . . . . . . . . . . . . . . . . . . . 22 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} βŠ† βˆͺ 𝑅
7371, 72sstrdi 3992 . . . . . . . . . . . . . . . . . . . . 21 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) β†’ 𝑠 βŠ† βˆͺ 𝑅)
7473adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) ∧ (π‘˜ ∈ 𝒫 βˆͺ 𝑆 ∧ (𝑆 β†Ύt π‘˜) ∈ Comp)) β†’ 𝑠 βŠ† βˆͺ 𝑅)
75 elpwi 4610 . . . . . . . . . . . . . . . . . . . . 21 (π‘˜ ∈ 𝒫 βˆͺ 𝑆 β†’ π‘˜ βŠ† βˆͺ 𝑆)
7675ad2antrl 727 . . . . . . . . . . . . . . . . . . . 20 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) ∧ (π‘˜ ∈ 𝒫 βˆͺ 𝑆 ∧ (𝑆 β†Ύt π‘˜) ∈ Comp)) β†’ π‘˜ βŠ† βˆͺ 𝑆)
77 eldif 3957 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑑 ∈ ((𝑠 Γ— π‘˜) βˆ– π‘₯) ↔ (𝑑 ∈ (𝑠 Γ— π‘˜) ∧ Β¬ 𝑑 ∈ π‘₯))
7877anbi1i 623 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑑 ∈ ((𝑠 Γ— π‘˜) βˆ– π‘₯) ∧ ((2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆))β€˜π‘‘) = 𝑏) ↔ ((𝑑 ∈ (𝑠 Γ— π‘˜) ∧ Β¬ 𝑑 ∈ π‘₯) ∧ ((2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆))β€˜π‘‘) = 𝑏))
79 anass 468 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑑 ∈ (𝑠 Γ— π‘˜) ∧ Β¬ 𝑑 ∈ π‘₯) ∧ ((2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆))β€˜π‘‘) = 𝑏) ↔ (𝑑 ∈ (𝑠 Γ— π‘˜) ∧ (Β¬ 𝑑 ∈ π‘₯ ∧ ((2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆))β€˜π‘‘) = 𝑏)))
8078, 79bitri 275 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑑 ∈ ((𝑠 Γ— π‘˜) βˆ– π‘₯) ∧ ((2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆))β€˜π‘‘) = 𝑏) ↔ (𝑑 ∈ (𝑠 Γ— π‘˜) ∧ (Β¬ 𝑑 ∈ π‘₯ ∧ ((2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆))β€˜π‘‘) = 𝑏)))
8180rexbii2 3087 . . . . . . . . . . . . . . . . . . . . . . . 24 (βˆƒπ‘‘ ∈ ((𝑠 Γ— π‘˜) βˆ– π‘₯)((2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆))β€˜π‘‘) = 𝑏 ↔ βˆƒπ‘‘ ∈ (𝑠 Γ— π‘˜)(Β¬ 𝑑 ∈ π‘₯ ∧ ((2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆))β€˜π‘‘) = 𝑏))
82 ancom 460 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((Β¬ 𝑑 ∈ π‘₯ ∧ ((2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆))β€˜π‘‘) = 𝑏) ↔ (((2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆))β€˜π‘‘) = 𝑏 ∧ Β¬ 𝑑 ∈ π‘₯))
83 fveqeq2 6906 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑑 = βŸ¨π‘Ž, π‘’βŸ© β†’ (((2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆))β€˜π‘‘) = 𝑏 ↔ ((2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆))β€˜βŸ¨π‘Ž, π‘’βŸ©) = 𝑏))
84 eleq1 2817 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑑 = βŸ¨π‘Ž, π‘’βŸ© β†’ (𝑑 ∈ π‘₯ ↔ βŸ¨π‘Ž, π‘’βŸ© ∈ π‘₯))
8584notbid 318 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑑 = βŸ¨π‘Ž, π‘’βŸ© β†’ (Β¬ 𝑑 ∈ π‘₯ ↔ Β¬ βŸ¨π‘Ž, π‘’βŸ© ∈ π‘₯))
8683, 85anbi12d 631 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑑 = βŸ¨π‘Ž, π‘’βŸ© β†’ ((((2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆))β€˜π‘‘) = 𝑏 ∧ Β¬ 𝑑 ∈ π‘₯) ↔ (((2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆))β€˜βŸ¨π‘Ž, π‘’βŸ©) = 𝑏 ∧ Β¬ βŸ¨π‘Ž, π‘’βŸ© ∈ π‘₯)))
8782, 86bitrid 283 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑑 = βŸ¨π‘Ž, π‘’βŸ© β†’ ((Β¬ 𝑑 ∈ π‘₯ ∧ ((2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆))β€˜π‘‘) = 𝑏) ↔ (((2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆))β€˜βŸ¨π‘Ž, π‘’βŸ©) = 𝑏 ∧ Β¬ βŸ¨π‘Ž, π‘’βŸ© ∈ π‘₯)))
8887rexxp 5845 . . . . . . . . . . . . . . . . . . . . . . . 24 (βˆƒπ‘‘ ∈ (𝑠 Γ— π‘˜)(Β¬ 𝑑 ∈ π‘₯ ∧ ((2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆))β€˜π‘‘) = 𝑏) ↔ βˆƒπ‘Ž ∈ 𝑠 βˆƒπ‘’ ∈ π‘˜ (((2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆))β€˜βŸ¨π‘Ž, π‘’βŸ©) = 𝑏 ∧ Β¬ βŸ¨π‘Ž, π‘’βŸ© ∈ π‘₯))
8981, 88bitri 275 . . . . . . . . . . . . . . . . . . . . . . 23 (βˆƒπ‘‘ ∈ ((𝑠 Γ— π‘˜) βˆ– π‘₯)((2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆))β€˜π‘‘) = 𝑏 ↔ βˆƒπ‘Ž ∈ 𝑠 βˆƒπ‘’ ∈ π‘˜ (((2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆))β€˜βŸ¨π‘Ž, π‘’βŸ©) = 𝑏 ∧ Β¬ βŸ¨π‘Ž, π‘’βŸ© ∈ π‘₯))
90 simpl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑠 βŠ† βˆͺ 𝑅 ∧ π‘˜ βŠ† βˆͺ 𝑆) β†’ 𝑠 βŠ† βˆͺ 𝑅)
9190sselda 3980 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝑠 βŠ† βˆͺ 𝑅 ∧ π‘˜ βŠ† βˆͺ 𝑆) ∧ π‘Ž ∈ 𝑠) β†’ π‘Ž ∈ βˆͺ 𝑅)
9291adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝑠 βŠ† βˆͺ 𝑅 ∧ π‘˜ βŠ† βˆͺ 𝑆) ∧ π‘Ž ∈ 𝑠) ∧ 𝑒 ∈ π‘˜) β†’ π‘Ž ∈ βˆͺ 𝑅)
93 simplr 768 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝑠 βŠ† βˆͺ 𝑅 ∧ π‘˜ βŠ† βˆͺ 𝑆) ∧ π‘Ž ∈ 𝑠) β†’ π‘˜ βŠ† βˆͺ 𝑆)
9493sselda 3980 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝑠 βŠ† βˆͺ 𝑅 ∧ π‘˜ βŠ† βˆͺ 𝑆) ∧ π‘Ž ∈ 𝑠) ∧ 𝑒 ∈ π‘˜) β†’ 𝑒 ∈ βˆͺ 𝑆)
9592, 94opelxpd 5717 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝑠 βŠ† βˆͺ 𝑅 ∧ π‘˜ βŠ† βˆͺ 𝑆) ∧ π‘Ž ∈ 𝑠) ∧ 𝑒 ∈ π‘˜) β†’ βŸ¨π‘Ž, π‘’βŸ© ∈ (βˆͺ 𝑅 Γ— βˆͺ 𝑆))
9695fvresd 6917 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝑠 βŠ† βˆͺ 𝑅 ∧ π‘˜ βŠ† βˆͺ 𝑆) ∧ π‘Ž ∈ 𝑠) ∧ 𝑒 ∈ π‘˜) β†’ ((2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆))β€˜βŸ¨π‘Ž, π‘’βŸ©) = (2nd β€˜βŸ¨π‘Ž, π‘’βŸ©))
97 vex 3475 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 π‘Ž ∈ V
98 vex 3475 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 𝑒 ∈ V
9997, 98op2nd 8002 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (2nd β€˜βŸ¨π‘Ž, π‘’βŸ©) = 𝑒
10096, 99eqtrdi 2784 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝑠 βŠ† βˆͺ 𝑅 ∧ π‘˜ βŠ† βˆͺ 𝑆) ∧ π‘Ž ∈ 𝑠) ∧ 𝑒 ∈ π‘˜) β†’ ((2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆))β€˜βŸ¨π‘Ž, π‘’βŸ©) = 𝑒)
101100eqeq1d 2730 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝑠 βŠ† βˆͺ 𝑅 ∧ π‘˜ βŠ† βˆͺ 𝑆) ∧ π‘Ž ∈ 𝑠) ∧ 𝑒 ∈ π‘˜) β†’ (((2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆))β€˜βŸ¨π‘Ž, π‘’βŸ©) = 𝑏 ↔ 𝑒 = 𝑏))
102101anbi1d 630 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝑠 βŠ† βˆͺ 𝑅 ∧ π‘˜ βŠ† βˆͺ 𝑆) ∧ π‘Ž ∈ 𝑠) ∧ 𝑒 ∈ π‘˜) β†’ ((((2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆))β€˜βŸ¨π‘Ž, π‘’βŸ©) = 𝑏 ∧ Β¬ βŸ¨π‘Ž, π‘’βŸ© ∈ π‘₯) ↔ (𝑒 = 𝑏 ∧ Β¬ βŸ¨π‘Ž, π‘’βŸ© ∈ π‘₯)))
103102rexbidva 3173 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑠 βŠ† βˆͺ 𝑅 ∧ π‘˜ βŠ† βˆͺ 𝑆) ∧ π‘Ž ∈ 𝑠) β†’ (βˆƒπ‘’ ∈ π‘˜ (((2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆))β€˜βŸ¨π‘Ž, π‘’βŸ©) = 𝑏 ∧ Β¬ βŸ¨π‘Ž, π‘’βŸ© ∈ π‘₯) ↔ βˆƒπ‘’ ∈ π‘˜ (𝑒 = 𝑏 ∧ Β¬ βŸ¨π‘Ž, π‘’βŸ© ∈ π‘₯)))
104 opeq2 4875 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑒 = 𝑏 β†’ βŸ¨π‘Ž, π‘’βŸ© = βŸ¨π‘Ž, π‘βŸ©)
105104eleq1d 2814 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑒 = 𝑏 β†’ (βŸ¨π‘Ž, π‘’βŸ© ∈ π‘₯ ↔ βŸ¨π‘Ž, π‘βŸ© ∈ π‘₯))
106105notbid 318 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑒 = 𝑏 β†’ (Β¬ βŸ¨π‘Ž, π‘’βŸ© ∈ π‘₯ ↔ Β¬ βŸ¨π‘Ž, π‘βŸ© ∈ π‘₯))
107106ceqsrexbv 3642 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (βˆƒπ‘’ ∈ π‘˜ (𝑒 = 𝑏 ∧ Β¬ βŸ¨π‘Ž, π‘’βŸ© ∈ π‘₯) ↔ (𝑏 ∈ π‘˜ ∧ Β¬ βŸ¨π‘Ž, π‘βŸ© ∈ π‘₯))
108103, 107bitrdi 287 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑠 βŠ† βˆͺ 𝑅 ∧ π‘˜ βŠ† βˆͺ 𝑆) ∧ π‘Ž ∈ 𝑠) β†’ (βˆƒπ‘’ ∈ π‘˜ (((2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆))β€˜βŸ¨π‘Ž, π‘’βŸ©) = 𝑏 ∧ Β¬ βŸ¨π‘Ž, π‘’βŸ© ∈ π‘₯) ↔ (𝑏 ∈ π‘˜ ∧ Β¬ βŸ¨π‘Ž, π‘βŸ© ∈ π‘₯)))
109108rexbidva 3173 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑠 βŠ† βˆͺ 𝑅 ∧ π‘˜ βŠ† βˆͺ 𝑆) β†’ (βˆƒπ‘Ž ∈ 𝑠 βˆƒπ‘’ ∈ π‘˜ (((2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆))β€˜βŸ¨π‘Ž, π‘’βŸ©) = 𝑏 ∧ Β¬ βŸ¨π‘Ž, π‘’βŸ© ∈ π‘₯) ↔ βˆƒπ‘Ž ∈ 𝑠 (𝑏 ∈ π‘˜ ∧ Β¬ βŸ¨π‘Ž, π‘βŸ© ∈ π‘₯)))
110 r19.42v 3187 . . . . . . . . . . . . . . . . . . . . . . . 24 (βˆƒπ‘Ž ∈ 𝑠 (𝑏 ∈ π‘˜ ∧ Β¬ βŸ¨π‘Ž, π‘βŸ© ∈ π‘₯) ↔ (𝑏 ∈ π‘˜ ∧ βˆƒπ‘Ž ∈ 𝑠 Β¬ βŸ¨π‘Ž, π‘βŸ© ∈ π‘₯))
111109, 110bitrdi 287 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑠 βŠ† βˆͺ 𝑅 ∧ π‘˜ βŠ† βˆͺ 𝑆) β†’ (βˆƒπ‘Ž ∈ 𝑠 βˆƒπ‘’ ∈ π‘˜ (((2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆))β€˜βŸ¨π‘Ž, π‘’βŸ©) = 𝑏 ∧ Β¬ βŸ¨π‘Ž, π‘’βŸ© ∈ π‘₯) ↔ (𝑏 ∈ π‘˜ ∧ βˆƒπ‘Ž ∈ 𝑠 Β¬ βŸ¨π‘Ž, π‘βŸ© ∈ π‘₯)))
11289, 111bitrid 283 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑠 βŠ† βˆͺ 𝑅 ∧ π‘˜ βŠ† βˆͺ 𝑆) β†’ (βˆƒπ‘‘ ∈ ((𝑠 Γ— π‘˜) βˆ– π‘₯)((2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆))β€˜π‘‘) = 𝑏 ↔ (𝑏 ∈ π‘˜ ∧ βˆƒπ‘Ž ∈ 𝑠 Β¬ βŸ¨π‘Ž, π‘βŸ© ∈ π‘₯)))
113 f2ndres 8018 . . . . . . . . . . . . . . . . . . . . . . . 24 (2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆)):(βˆͺ 𝑅 Γ— βˆͺ 𝑆)⟢βˆͺ 𝑆
114 ffn 6722 . . . . . . . . . . . . . . . . . . . . . . . 24 ((2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆)):(βˆͺ 𝑅 Γ— βˆͺ 𝑆)⟢βˆͺ 𝑆 β†’ (2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆)) Fn (βˆͺ 𝑅 Γ— βˆͺ 𝑆))
115113, 114ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . 23 (2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆)) Fn (βˆͺ 𝑅 Γ— βˆͺ 𝑆)
116 difss 4130 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑠 Γ— π‘˜) βˆ– π‘₯) βŠ† (𝑠 Γ— π‘˜)
117 xpss12 5693 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑠 βŠ† βˆͺ 𝑅 ∧ π‘˜ βŠ† βˆͺ 𝑆) β†’ (𝑠 Γ— π‘˜) βŠ† (βˆͺ 𝑅 Γ— βˆͺ 𝑆))
118116, 117sstrid 3991 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑠 βŠ† βˆͺ 𝑅 ∧ π‘˜ βŠ† βˆͺ 𝑆) β†’ ((𝑠 Γ— π‘˜) βˆ– π‘₯) βŠ† (βˆͺ 𝑅 Γ— βˆͺ 𝑆))
119 fvelimab 6971 . . . . . . . . . . . . . . . . . . . . . . 23 (((2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆)) Fn (βˆͺ 𝑅 Γ— βˆͺ 𝑆) ∧ ((𝑠 Γ— π‘˜) βˆ– π‘₯) βŠ† (βˆͺ 𝑅 Γ— βˆͺ 𝑆)) β†’ (𝑏 ∈ ((2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆)) β€œ ((𝑠 Γ— π‘˜) βˆ– π‘₯)) ↔ βˆƒπ‘‘ ∈ ((𝑠 Γ— π‘˜) βˆ– π‘₯)((2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆))β€˜π‘‘) = 𝑏))
120115, 118, 119sylancr 586 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑠 βŠ† βˆͺ 𝑅 ∧ π‘˜ βŠ† βˆͺ 𝑆) β†’ (𝑏 ∈ ((2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆)) β€œ ((𝑠 Γ— π‘˜) βˆ– π‘₯)) ↔ βˆƒπ‘‘ ∈ ((𝑠 Γ— π‘˜) βˆ– π‘₯)((2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆))β€˜π‘‘) = 𝑏))
121 eldif 3957 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑏 ∈ (π‘˜ βˆ– {𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯}) ↔ (𝑏 ∈ π‘˜ ∧ Β¬ 𝑏 ∈ {𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯}))
122 simpr 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑠 βŠ† βˆͺ 𝑅 ∧ π‘˜ βŠ† βˆͺ 𝑆) β†’ π‘˜ βŠ† βˆͺ 𝑆)
123122sselda 3980 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑠 βŠ† βˆͺ 𝑅 ∧ π‘˜ βŠ† βˆͺ 𝑆) ∧ 𝑏 ∈ π‘˜) β†’ 𝑏 ∈ βˆͺ 𝑆)
124 sneq 4639 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑣 = 𝑏 β†’ {𝑣} = {𝑏})
125124xpeq2d 5708 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑣 = 𝑏 β†’ (𝑠 Γ— {𝑣}) = (𝑠 Γ— {𝑏}))
126125sseq1d 4011 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑣 = 𝑏 β†’ ((𝑠 Γ— {𝑣}) βŠ† π‘₯ ↔ (𝑠 Γ— {𝑏}) βŠ† π‘₯))
127 dfss3 3968 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑠 Γ— {𝑏}) βŠ† π‘₯ ↔ βˆ€π‘˜ ∈ (𝑠 Γ— {𝑏})π‘˜ ∈ π‘₯)
128 eleq1 2817 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (π‘˜ = βŸ¨π‘Ž, π‘‘βŸ© β†’ (π‘˜ ∈ π‘₯ ↔ βŸ¨π‘Ž, π‘‘βŸ© ∈ π‘₯))
129128ralxp 5844 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (βˆ€π‘˜ ∈ (𝑠 Γ— {𝑏})π‘˜ ∈ π‘₯ ↔ βˆ€π‘Ž ∈ 𝑠 βˆ€π‘‘ ∈ {𝑏}βŸ¨π‘Ž, π‘‘βŸ© ∈ π‘₯)
130 vex 3475 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 𝑏 ∈ V
131 opeq2 4875 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑑 = 𝑏 β†’ βŸ¨π‘Ž, π‘‘βŸ© = βŸ¨π‘Ž, π‘βŸ©)
132131eleq1d 2814 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑑 = 𝑏 β†’ (βŸ¨π‘Ž, π‘‘βŸ© ∈ π‘₯ ↔ βŸ¨π‘Ž, π‘βŸ© ∈ π‘₯))
133130, 132ralsn 4686 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (βˆ€π‘‘ ∈ {𝑏}βŸ¨π‘Ž, π‘‘βŸ© ∈ π‘₯ ↔ βŸ¨π‘Ž, π‘βŸ© ∈ π‘₯)
134133ralbii 3090 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (βˆ€π‘Ž ∈ 𝑠 βˆ€π‘‘ ∈ {𝑏}βŸ¨π‘Ž, π‘‘βŸ© ∈ π‘₯ ↔ βˆ€π‘Ž ∈ 𝑠 βŸ¨π‘Ž, π‘βŸ© ∈ π‘₯)
135127, 129, 1343bitri 297 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑠 Γ— {𝑏}) βŠ† π‘₯ ↔ βˆ€π‘Ž ∈ 𝑠 βŸ¨π‘Ž, π‘βŸ© ∈ π‘₯)
136126, 135bitrdi 287 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑣 = 𝑏 β†’ ((𝑠 Γ— {𝑣}) βŠ† π‘₯ ↔ βˆ€π‘Ž ∈ 𝑠 βŸ¨π‘Ž, π‘βŸ© ∈ π‘₯))
137136elrab3 3683 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑏 ∈ βˆͺ 𝑆 β†’ (𝑏 ∈ {𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯} ↔ βˆ€π‘Ž ∈ 𝑠 βŸ¨π‘Ž, π‘βŸ© ∈ π‘₯))
138123, 137syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑠 βŠ† βˆͺ 𝑅 ∧ π‘˜ βŠ† βˆͺ 𝑆) ∧ 𝑏 ∈ π‘˜) β†’ (𝑏 ∈ {𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯} ↔ βˆ€π‘Ž ∈ 𝑠 βŸ¨π‘Ž, π‘βŸ© ∈ π‘₯))
139138notbid 318 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑠 βŠ† βˆͺ 𝑅 ∧ π‘˜ βŠ† βˆͺ 𝑆) ∧ 𝑏 ∈ π‘˜) β†’ (Β¬ 𝑏 ∈ {𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯} ↔ Β¬ βˆ€π‘Ž ∈ 𝑠 βŸ¨π‘Ž, π‘βŸ© ∈ π‘₯))
140 rexnal 3097 . . . . . . . . . . . . . . . . . . . . . . . . 25 (βˆƒπ‘Ž ∈ 𝑠 Β¬ βŸ¨π‘Ž, π‘βŸ© ∈ π‘₯ ↔ Β¬ βˆ€π‘Ž ∈ 𝑠 βŸ¨π‘Ž, π‘βŸ© ∈ π‘₯)
141139, 140bitr4di 289 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑠 βŠ† βˆͺ 𝑅 ∧ π‘˜ βŠ† βˆͺ 𝑆) ∧ 𝑏 ∈ π‘˜) β†’ (Β¬ 𝑏 ∈ {𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯} ↔ βˆƒπ‘Ž ∈ 𝑠 Β¬ βŸ¨π‘Ž, π‘βŸ© ∈ π‘₯))
142141pm5.32da 578 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑠 βŠ† βˆͺ 𝑅 ∧ π‘˜ βŠ† βˆͺ 𝑆) β†’ ((𝑏 ∈ π‘˜ ∧ Β¬ 𝑏 ∈ {𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯}) ↔ (𝑏 ∈ π‘˜ ∧ βˆƒπ‘Ž ∈ 𝑠 Β¬ βŸ¨π‘Ž, π‘βŸ© ∈ π‘₯)))
143121, 142bitrid 283 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑠 βŠ† βˆͺ 𝑅 ∧ π‘˜ βŠ† βˆͺ 𝑆) β†’ (𝑏 ∈ (π‘˜ βˆ– {𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯}) ↔ (𝑏 ∈ π‘˜ ∧ βˆƒπ‘Ž ∈ 𝑠 Β¬ βŸ¨π‘Ž, π‘βŸ© ∈ π‘₯)))
144112, 120, 1433bitr4d 311 . . . . . . . . . . . . . . . . . . . . 21 ((𝑠 βŠ† βˆͺ 𝑅 ∧ π‘˜ βŠ† βˆͺ 𝑆) β†’ (𝑏 ∈ ((2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆)) β€œ ((𝑠 Γ— π‘˜) βˆ– π‘₯)) ↔ 𝑏 ∈ (π‘˜ βˆ– {𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯})))
145144eqrdv 2726 . . . . . . . . . . . . . . . . . . . 20 ((𝑠 βŠ† βˆͺ 𝑅 ∧ π‘˜ βŠ† βˆͺ 𝑆) β†’ ((2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆)) β€œ ((𝑠 Γ— π‘˜) βˆ– π‘₯)) = (π‘˜ βˆ– {𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯}))
14674, 76, 145syl2anc 583 . . . . . . . . . . . . . . . . . . 19 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) ∧ (π‘˜ ∈ 𝒫 βˆͺ 𝑆 ∧ (𝑆 β†Ύt π‘˜) ∈ Comp)) β†’ ((2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆)) β€œ ((𝑠 Γ— π‘˜) βˆ– π‘₯)) = (π‘˜ βˆ– {𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯}))
147 difin 4262 . . . . . . . . . . . . . . . . . . . 20 (π‘˜ βˆ– (π‘˜ ∩ {𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯})) = (π‘˜ βˆ– {𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯})
14865adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) ∧ (π‘˜ ∈ 𝒫 βˆͺ 𝑆 ∧ (𝑆 β†Ύt π‘˜) ∈ Comp)) β†’ 𝑆 ∈ Top)
14924restuni 23079 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑆 ∈ Top ∧ π‘˜ βŠ† βˆͺ 𝑆) β†’ π‘˜ = βˆͺ (𝑆 β†Ύt π‘˜))
150148, 76, 149syl2anc 583 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) ∧ (π‘˜ ∈ 𝒫 βˆͺ 𝑆 ∧ (𝑆 β†Ύt π‘˜) ∈ Comp)) β†’ π‘˜ = βˆͺ (𝑆 β†Ύt π‘˜))
151150difeq1d 4119 . . . . . . . . . . . . . . . . . . . 20 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) ∧ (π‘˜ ∈ 𝒫 βˆͺ 𝑆 ∧ (𝑆 β†Ύt π‘˜) ∈ Comp)) β†’ (π‘˜ βˆ– (π‘˜ ∩ {𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯})) = (βˆͺ (𝑆 β†Ύt π‘˜) βˆ– (π‘˜ ∩ {𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯})))
152147, 151eqtr3id 2782 . . . . . . . . . . . . . . . . . . 19 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) ∧ (π‘˜ ∈ 𝒫 βˆͺ 𝑆 ∧ (𝑆 β†Ύt π‘˜) ∈ Comp)) β†’ (π‘˜ βˆ– {𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯}) = (βˆͺ (𝑆 β†Ύt π‘˜) βˆ– (π‘˜ ∩ {𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯})))
153146, 152eqtrd 2768 . . . . . . . . . . . . . . . . . 18 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) ∧ (π‘˜ ∈ 𝒫 βˆͺ 𝑆 ∧ (𝑆 β†Ύt π‘˜) ∈ Comp)) β†’ ((2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆)) β€œ ((𝑠 Γ— π‘˜) βˆ– π‘₯)) = (βˆͺ (𝑆 β†Ύt π‘˜) βˆ– (π‘˜ ∩ {𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯})))
15415ad2antrr 725 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) ∧ (π‘˜ ∈ 𝒫 βˆͺ 𝑆 ∧ (𝑆 β†Ύt π‘˜) ∈ Comp)) β†’ 𝑆 ∈ (ran π‘˜Gen ∩ Haus))
155154elin2d 4199 . . . . . . . . . . . . . . . . . . . 20 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) ∧ (π‘˜ ∈ 𝒫 βˆͺ 𝑆 ∧ (𝑆 β†Ύt π‘˜) ∈ Comp)) β†’ 𝑆 ∈ Haus)
156 df-ima 5691 . . . . . . . . . . . . . . . . . . . . . . 23 ((2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆)) β€œ ((𝑠 Γ— π‘˜) βˆ– π‘₯)) = ran ((2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆)) β†Ύ ((𝑠 Γ— π‘˜) βˆ– π‘₯))
157 resres 5998 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆)) β†Ύ ((𝑠 Γ— π‘˜) βˆ– π‘₯)) = (2nd β†Ύ ((βˆͺ 𝑅 Γ— βˆͺ 𝑆) ∩ ((𝑠 Γ— π‘˜) βˆ– π‘₯)))
158 inss2 4230 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((βˆͺ 𝑅 Γ— βˆͺ 𝑆) ∩ ((𝑠 Γ— π‘˜) βˆ– π‘₯)) βŠ† ((𝑠 Γ— π‘˜) βˆ– π‘₯)
159158, 116sstri 3989 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((βˆͺ 𝑅 Γ— βˆͺ 𝑆) ∩ ((𝑠 Γ— π‘˜) βˆ– π‘₯)) βŠ† (𝑠 Γ— π‘˜)
160 ssres2 6013 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((βˆͺ 𝑅 Γ— βˆͺ 𝑆) ∩ ((𝑠 Γ— π‘˜) βˆ– π‘₯)) βŠ† (𝑠 Γ— π‘˜) β†’ (2nd β†Ύ ((βˆͺ 𝑅 Γ— βˆͺ 𝑆) ∩ ((𝑠 Γ— π‘˜) βˆ– π‘₯))) βŠ† (2nd β†Ύ (𝑠 Γ— π‘˜)))
161159, 160ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . 25 (2nd β†Ύ ((βˆͺ 𝑅 Γ— βˆͺ 𝑆) ∩ ((𝑠 Γ— π‘˜) βˆ– π‘₯))) βŠ† (2nd β†Ύ (𝑠 Γ— π‘˜))
162157, 161eqsstri 4014 . . . . . . . . . . . . . . . . . . . . . . . 24 ((2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆)) β†Ύ ((𝑠 Γ— π‘˜) βˆ– π‘₯)) βŠ† (2nd β†Ύ (𝑠 Γ— π‘˜))
163162rnssi 5942 . . . . . . . . . . . . . . . . . . . . . . 23 ran ((2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆)) β†Ύ ((𝑠 Γ— π‘˜) βˆ– π‘₯)) βŠ† ran (2nd β†Ύ (𝑠 Γ— π‘˜))
164156, 163eqsstri 4014 . . . . . . . . . . . . . . . . . . . . . 22 ((2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆)) β€œ ((𝑠 Γ— π‘˜) βˆ– π‘₯)) βŠ† ran (2nd β†Ύ (𝑠 Γ— π‘˜))
165 f2ndres 8018 . . . . . . . . . . . . . . . . . . . . . . 23 (2nd β†Ύ (𝑠 Γ— π‘˜)):(𝑠 Γ— π‘˜)βŸΆπ‘˜
166 frn 6729 . . . . . . . . . . . . . . . . . . . . . . 23 ((2nd β†Ύ (𝑠 Γ— π‘˜)):(𝑠 Γ— π‘˜)βŸΆπ‘˜ β†’ ran (2nd β†Ύ (𝑠 Γ— π‘˜)) βŠ† π‘˜)
167165, 166ax-mp 5 . . . . . . . . . . . . . . . . . . . . . 22 ran (2nd β†Ύ (𝑠 Γ— π‘˜)) βŠ† π‘˜
168164, 167sstri 3989 . . . . . . . . . . . . . . . . . . . . 21 ((2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆)) β€œ ((𝑠 Γ— π‘˜) βˆ– π‘₯)) βŠ† π‘˜
169168, 76sstrid 3991 . . . . . . . . . . . . . . . . . . . 20 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) ∧ (π‘˜ ∈ 𝒫 βˆͺ 𝑆 ∧ (𝑆 β†Ύt π‘˜) ∈ Comp)) β†’ ((2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆)) β€œ ((𝑠 Γ— π‘˜) βˆ– π‘₯)) βŠ† βˆͺ 𝑆)
17012ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) ∧ (π‘˜ ∈ 𝒫 βˆͺ 𝑆 ∧ (𝑆 β†Ύt π‘˜) ∈ Comp)) β†’ 𝑅 ∈ (TopOnβ€˜βˆͺ 𝑅))
171148, 17sylib 217 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) ∧ (π‘˜ ∈ 𝒫 βˆͺ 𝑆 ∧ (𝑆 β†Ύt π‘˜) ∈ Comp)) β†’ 𝑆 ∈ (TopOnβ€˜βˆͺ 𝑆))
172 tx2cn 23527 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑅 ∈ (TopOnβ€˜βˆͺ 𝑅) ∧ 𝑆 ∈ (TopOnβ€˜βˆͺ 𝑆)) β†’ (2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆)) ∈ ((𝑅 Γ—t 𝑆) Cn 𝑆))
173170, 171, 172syl2anc 583 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) ∧ (π‘˜ ∈ 𝒫 βˆͺ 𝑆 ∧ (𝑆 β†Ύt π‘˜) ∈ Comp)) β†’ (2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆)) ∈ ((𝑅 Γ—t 𝑆) Cn 𝑆))
17427ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) ∧ (π‘˜ ∈ 𝒫 βˆͺ 𝑆 ∧ (𝑆 β†Ύt π‘˜) ∈ Comp)) β†’ (𝑅 Γ—t 𝑆) ∈ Top)
175116a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) ∧ (π‘˜ ∈ 𝒫 βˆͺ 𝑆 ∧ (𝑆 β†Ύt π‘˜) ∈ Comp)) β†’ ((𝑠 Γ— π‘˜) βˆ– π‘₯) βŠ† (𝑠 Γ— π‘˜))
176 vex 3475 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑠 ∈ V
177 vex 3475 . . . . . . . . . . . . . . . . . . . . . . . . 25 π‘˜ ∈ V
178176, 177xpex 7755 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑠 Γ— π‘˜) ∈ V
179178a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) ∧ (π‘˜ ∈ 𝒫 βˆͺ 𝑆 ∧ (𝑆 β†Ύt π‘˜) ∈ Comp)) β†’ (𝑠 Γ— π‘˜) ∈ V)
180 restabs 23082 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑅 Γ—t 𝑆) ∈ Top ∧ ((𝑠 Γ— π‘˜) βˆ– π‘₯) βŠ† (𝑠 Γ— π‘˜) ∧ (𝑠 Γ— π‘˜) ∈ V) β†’ (((𝑅 Γ—t 𝑆) β†Ύt (𝑠 Γ— π‘˜)) β†Ύt ((𝑠 Γ— π‘˜) βˆ– π‘₯)) = ((𝑅 Γ—t 𝑆) β†Ύt ((𝑠 Γ— π‘˜) βˆ– π‘₯)))
181174, 175, 179, 180syl3anc 1369 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) ∧ (π‘˜ ∈ 𝒫 βˆͺ 𝑆 ∧ (𝑆 β†Ύt π‘˜) ∈ Comp)) β†’ (((𝑅 Γ—t 𝑆) β†Ύt (𝑠 Γ— π‘˜)) β†Ύt ((𝑠 Γ— π‘˜) βˆ– π‘₯)) = ((𝑅 Γ—t 𝑆) β†Ύt ((𝑠 Γ— π‘˜) βˆ– π‘₯)))
18264adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) ∧ (π‘˜ ∈ 𝒫 βˆͺ 𝑆 ∧ (𝑆 β†Ύt π‘˜) ∈ Comp)) β†’ 𝑅 ∈ Top)
183154, 4syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) ∧ (π‘˜ ∈ 𝒫 βˆͺ 𝑆 ∧ (𝑆 β†Ύt π‘˜) ∈ Comp)) β†’ 𝑆 ∈ Top)
184176a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) ∧ (π‘˜ ∈ 𝒫 βˆͺ 𝑆 ∧ (𝑆 β†Ύt π‘˜) ∈ Comp)) β†’ 𝑠 ∈ V)
185 simprl 770 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) ∧ (π‘˜ ∈ 𝒫 βˆͺ 𝑆 ∧ (𝑆 β†Ύt π‘˜) ∈ Comp)) β†’ π‘˜ ∈ 𝒫 βˆͺ 𝑆)
186 txrest 23548 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑠 ∈ V ∧ π‘˜ ∈ 𝒫 βˆͺ 𝑆)) β†’ ((𝑅 Γ—t 𝑆) β†Ύt (𝑠 Γ— π‘˜)) = ((𝑅 β†Ύt 𝑠) Γ—t (𝑆 β†Ύt π‘˜)))
187182, 183, 184, 185, 186syl22anc 838 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) ∧ (π‘˜ ∈ 𝒫 βˆͺ 𝑆 ∧ (𝑆 β†Ύt π‘˜) ∈ Comp)) β†’ ((𝑅 Γ—t 𝑆) β†Ύt (𝑠 Γ— π‘˜)) = ((𝑅 β†Ύt 𝑠) Γ—t (𝑆 β†Ύt π‘˜)))
188 simprr3 1221 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) β†’ (𝑅 β†Ύt 𝑠) ∈ Comp)
189188adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) ∧ (π‘˜ ∈ 𝒫 βˆͺ 𝑆 ∧ (𝑆 β†Ύt π‘˜) ∈ Comp)) β†’ (𝑅 β†Ύt 𝑠) ∈ Comp)
190 simprr 772 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) ∧ (π‘˜ ∈ 𝒫 βˆͺ 𝑆 ∧ (𝑆 β†Ύt π‘˜) ∈ Comp)) β†’ (𝑆 β†Ύt π‘˜) ∈ Comp)
191 txcmp 23560 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑅 β†Ύt 𝑠) ∈ Comp ∧ (𝑆 β†Ύt π‘˜) ∈ Comp) β†’ ((𝑅 β†Ύt 𝑠) Γ—t (𝑆 β†Ύt π‘˜)) ∈ Comp)
192189, 190, 191syl2anc 583 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) ∧ (π‘˜ ∈ 𝒫 βˆͺ 𝑆 ∧ (𝑆 β†Ύt π‘˜) ∈ Comp)) β†’ ((𝑅 β†Ύt 𝑠) Γ—t (𝑆 β†Ύt π‘˜)) ∈ Comp)
193187, 192eqeltrd 2829 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) ∧ (π‘˜ ∈ 𝒫 βˆͺ 𝑆 ∧ (𝑆 β†Ύt π‘˜) ∈ Comp)) β†’ ((𝑅 Γ—t 𝑆) β†Ύt (𝑠 Γ— π‘˜)) ∈ Comp)
194 difin 4262 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑠 Γ— π‘˜) βˆ– ((𝑠 Γ— π‘˜) ∩ π‘₯)) = ((𝑠 Γ— π‘˜) βˆ– π‘₯)
19574, 76, 117syl2anc 583 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) ∧ (π‘˜ ∈ 𝒫 βˆͺ 𝑆 ∧ (𝑆 β†Ύt π‘˜) ∈ Comp)) β†’ (𝑠 Γ— π‘˜) βŠ† (βˆͺ 𝑅 Γ— βˆͺ 𝑆))
196182, 148, 25syl2anc 583 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) ∧ (π‘˜ ∈ 𝒫 βˆͺ 𝑆 ∧ (𝑆 β†Ύt π‘˜) ∈ Comp)) β†’ (βˆͺ 𝑅 Γ— βˆͺ 𝑆) = βˆͺ (𝑅 Γ—t 𝑆))
197195, 196sseqtrd 4020 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) ∧ (π‘˜ ∈ 𝒫 βˆͺ 𝑆 ∧ (𝑆 β†Ύt π‘˜) ∈ Comp)) β†’ (𝑠 Γ— π‘˜) βŠ† βˆͺ (𝑅 Γ—t 𝑆))
19828restuni 23079 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑅 Γ—t 𝑆) ∈ Top ∧ (𝑠 Γ— π‘˜) βŠ† βˆͺ (𝑅 Γ—t 𝑆)) β†’ (𝑠 Γ— π‘˜) = βˆͺ ((𝑅 Γ—t 𝑆) β†Ύt (𝑠 Γ— π‘˜)))
199174, 197, 198syl2anc 583 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) ∧ (π‘˜ ∈ 𝒫 βˆͺ 𝑆 ∧ (𝑆 β†Ύt π‘˜) ∈ Comp)) β†’ (𝑠 Γ— π‘˜) = βˆͺ ((𝑅 Γ—t 𝑆) β†Ύt (𝑠 Γ— π‘˜)))
200199difeq1d 4119 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) ∧ (π‘˜ ∈ 𝒫 βˆͺ 𝑆 ∧ (𝑆 β†Ύt π‘˜) ∈ Comp)) β†’ ((𝑠 Γ— π‘˜) βˆ– ((𝑠 Γ— π‘˜) ∩ π‘₯)) = (βˆͺ ((𝑅 Γ—t 𝑆) β†Ύt (𝑠 Γ— π‘˜)) βˆ– ((𝑠 Γ— π‘˜) ∩ π‘₯)))
201194, 200eqtr3id 2782 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) ∧ (π‘˜ ∈ 𝒫 βˆͺ 𝑆 ∧ (𝑆 β†Ύt π‘˜) ∈ Comp)) β†’ ((𝑠 Γ— π‘˜) βˆ– π‘₯) = (βˆͺ ((𝑅 Γ—t 𝑆) β†Ύt (𝑠 Γ— π‘˜)) βˆ– ((𝑠 Γ— π‘˜) ∩ π‘₯)))
202 resttop 23077 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑅 Γ—t 𝑆) ∈ Top ∧ (𝑠 Γ— π‘˜) ∈ V) β†’ ((𝑅 Γ—t 𝑆) β†Ύt (𝑠 Γ— π‘˜)) ∈ Top)
203174, 178, 202sylancl 585 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) ∧ (π‘˜ ∈ 𝒫 βˆͺ 𝑆 ∧ (𝑆 β†Ύt π‘˜) ∈ Comp)) β†’ ((𝑅 Γ—t 𝑆) β†Ύt (𝑠 Γ— π‘˜)) ∈ Top)
204 incom 4201 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑠 Γ— π‘˜) ∩ π‘₯) = (π‘₯ ∩ (𝑠 Γ— π‘˜))
20520ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) ∧ (π‘˜ ∈ 𝒫 βˆͺ 𝑆 ∧ (𝑆 β†Ύt π‘˜) ∈ Comp)) β†’ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆)))
206 kgeni 23454 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆)) ∧ ((𝑅 Γ—t 𝑆) β†Ύt (𝑠 Γ— π‘˜)) ∈ Comp) β†’ (π‘₯ ∩ (𝑠 Γ— π‘˜)) ∈ ((𝑅 Γ—t 𝑆) β†Ύt (𝑠 Γ— π‘˜)))
207205, 193, 206syl2anc 583 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) ∧ (π‘˜ ∈ 𝒫 βˆͺ 𝑆 ∧ (𝑆 β†Ύt π‘˜) ∈ Comp)) β†’ (π‘₯ ∩ (𝑠 Γ— π‘˜)) ∈ ((𝑅 Γ—t 𝑆) β†Ύt (𝑠 Γ— π‘˜)))
208204, 207eqeltrid 2833 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) ∧ (π‘˜ ∈ 𝒫 βˆͺ 𝑆 ∧ (𝑆 β†Ύt π‘˜) ∈ Comp)) β†’ ((𝑠 Γ— π‘˜) ∩ π‘₯) ∈ ((𝑅 Γ—t 𝑆) β†Ύt (𝑠 Γ— π‘˜)))
209 eqid 2728 . . . . . . . . . . . . . . . . . . . . . . . . . 26 βˆͺ ((𝑅 Γ—t 𝑆) β†Ύt (𝑠 Γ— π‘˜)) = βˆͺ ((𝑅 Γ—t 𝑆) β†Ύt (𝑠 Γ— π‘˜))
210209opncld 22950 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝑅 Γ—t 𝑆) β†Ύt (𝑠 Γ— π‘˜)) ∈ Top ∧ ((𝑠 Γ— π‘˜) ∩ π‘₯) ∈ ((𝑅 Γ—t 𝑆) β†Ύt (𝑠 Γ— π‘˜))) β†’ (βˆͺ ((𝑅 Γ—t 𝑆) β†Ύt (𝑠 Γ— π‘˜)) βˆ– ((𝑠 Γ— π‘˜) ∩ π‘₯)) ∈ (Clsdβ€˜((𝑅 Γ—t 𝑆) β†Ύt (𝑠 Γ— π‘˜))))
211203, 208, 210syl2anc 583 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) ∧ (π‘˜ ∈ 𝒫 βˆͺ 𝑆 ∧ (𝑆 β†Ύt π‘˜) ∈ Comp)) β†’ (βˆͺ ((𝑅 Γ—t 𝑆) β†Ύt (𝑠 Γ— π‘˜)) βˆ– ((𝑠 Γ— π‘˜) ∩ π‘₯)) ∈ (Clsdβ€˜((𝑅 Γ—t 𝑆) β†Ύt (𝑠 Γ— π‘˜))))
212201, 211eqeltrd 2829 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) ∧ (π‘˜ ∈ 𝒫 βˆͺ 𝑆 ∧ (𝑆 β†Ύt π‘˜) ∈ Comp)) β†’ ((𝑠 Γ— π‘˜) βˆ– π‘₯) ∈ (Clsdβ€˜((𝑅 Γ—t 𝑆) β†Ύt (𝑠 Γ— π‘˜))))
213 cmpcld 23319 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑅 Γ—t 𝑆) β†Ύt (𝑠 Γ— π‘˜)) ∈ Comp ∧ ((𝑠 Γ— π‘˜) βˆ– π‘₯) ∈ (Clsdβ€˜((𝑅 Γ—t 𝑆) β†Ύt (𝑠 Γ— π‘˜)))) β†’ (((𝑅 Γ—t 𝑆) β†Ύt (𝑠 Γ— π‘˜)) β†Ύt ((𝑠 Γ— π‘˜) βˆ– π‘₯)) ∈ Comp)
214193, 212, 213syl2anc 583 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) ∧ (π‘˜ ∈ 𝒫 βˆͺ 𝑆 ∧ (𝑆 β†Ύt π‘˜) ∈ Comp)) β†’ (((𝑅 Γ—t 𝑆) β†Ύt (𝑠 Γ— π‘˜)) β†Ύt ((𝑠 Γ— π‘˜) βˆ– π‘₯)) ∈ Comp)
215181, 214eqeltrrd 2830 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) ∧ (π‘˜ ∈ 𝒫 βˆͺ 𝑆 ∧ (𝑆 β†Ύt π‘˜) ∈ Comp)) β†’ ((𝑅 Γ—t 𝑆) β†Ύt ((𝑠 Γ— π‘˜) βˆ– π‘₯)) ∈ Comp)
216 imacmp 23314 . . . . . . . . . . . . . . . . . . . . 21 (((2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆)) ∈ ((𝑅 Γ—t 𝑆) Cn 𝑆) ∧ ((𝑅 Γ—t 𝑆) β†Ύt ((𝑠 Γ— π‘˜) βˆ– π‘₯)) ∈ Comp) β†’ (𝑆 β†Ύt ((2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆)) β€œ ((𝑠 Γ— π‘˜) βˆ– π‘₯))) ∈ Comp)
217173, 215, 216syl2anc 583 . . . . . . . . . . . . . . . . . . . 20 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) ∧ (π‘˜ ∈ 𝒫 βˆͺ 𝑆 ∧ (𝑆 β†Ύt π‘˜) ∈ Comp)) β†’ (𝑆 β†Ύt ((2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆)) β€œ ((𝑠 Γ— π‘˜) βˆ– π‘₯))) ∈ Comp)
21824hauscmp 23324 . . . . . . . . . . . . . . . . . . . 20 ((𝑆 ∈ Haus ∧ ((2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆)) β€œ ((𝑠 Γ— π‘˜) βˆ– π‘₯)) βŠ† βˆͺ 𝑆 ∧ (𝑆 β†Ύt ((2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆)) β€œ ((𝑠 Γ— π‘˜) βˆ– π‘₯))) ∈ Comp) β†’ ((2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆)) β€œ ((𝑠 Γ— π‘˜) βˆ– π‘₯)) ∈ (Clsdβ€˜π‘†))
219155, 169, 217, 218syl3anc 1369 . . . . . . . . . . . . . . . . . . 19 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) ∧ (π‘˜ ∈ 𝒫 βˆͺ 𝑆 ∧ (𝑆 β†Ύt π‘˜) ∈ Comp)) β†’ ((2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆)) β€œ ((𝑠 Γ— π‘˜) βˆ– π‘₯)) ∈ (Clsdβ€˜π‘†))
220168a1i 11 . . . . . . . . . . . . . . . . . . 19 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) ∧ (π‘˜ ∈ 𝒫 βˆͺ 𝑆 ∧ (𝑆 β†Ύt π‘˜) ∈ Comp)) β†’ ((2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆)) β€œ ((𝑠 Γ— π‘˜) βˆ– π‘₯)) βŠ† π‘˜)
22124restcldi 23090 . . . . . . . . . . . . . . . . . . 19 ((π‘˜ βŠ† βˆͺ 𝑆 ∧ ((2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆)) β€œ ((𝑠 Γ— π‘˜) βˆ– π‘₯)) ∈ (Clsdβ€˜π‘†) ∧ ((2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆)) β€œ ((𝑠 Γ— π‘˜) βˆ– π‘₯)) βŠ† π‘˜) β†’ ((2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆)) β€œ ((𝑠 Γ— π‘˜) βˆ– π‘₯)) ∈ (Clsdβ€˜(𝑆 β†Ύt π‘˜)))
22276, 219, 220, 221syl3anc 1369 . . . . . . . . . . . . . . . . . 18 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) ∧ (π‘˜ ∈ 𝒫 βˆͺ 𝑆 ∧ (𝑆 β†Ύt π‘˜) ∈ Comp)) β†’ ((2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆)) β€œ ((𝑠 Γ— π‘˜) βˆ– π‘₯)) ∈ (Clsdβ€˜(𝑆 β†Ύt π‘˜)))
223153, 222eqeltrrd 2830 . . . . . . . . . . . . . . . . 17 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) ∧ (π‘˜ ∈ 𝒫 βˆͺ 𝑆 ∧ (𝑆 β†Ύt π‘˜) ∈ Comp)) β†’ (βˆͺ (𝑆 β†Ύt π‘˜) βˆ– (π‘˜ ∩ {𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯})) ∈ (Clsdβ€˜(𝑆 β†Ύt π‘˜)))
224 resttop 23077 . . . . . . . . . . . . . . . . . . 19 ((𝑆 ∈ Top ∧ π‘˜ ∈ 𝒫 βˆͺ 𝑆) β†’ (𝑆 β†Ύt π‘˜) ∈ Top)
225148, 185, 224syl2anc 583 . . . . . . . . . . . . . . . . . 18 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) ∧ (π‘˜ ∈ 𝒫 βˆͺ 𝑆 ∧ (𝑆 β†Ύt π‘˜) ∈ Comp)) β†’ (𝑆 β†Ύt π‘˜) ∈ Top)
226 inss1 4229 . . . . . . . . . . . . . . . . . . 19 (π‘˜ ∩ {𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯}) βŠ† π‘˜
227226, 150sseqtrid 4032 . . . . . . . . . . . . . . . . . 18 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) ∧ (π‘˜ ∈ 𝒫 βˆͺ 𝑆 ∧ (𝑆 β†Ύt π‘˜) ∈ Comp)) β†’ (π‘˜ ∩ {𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯}) βŠ† βˆͺ (𝑆 β†Ύt π‘˜))
228 eqid 2728 . . . . . . . . . . . . . . . . . . 19 βˆͺ (𝑆 β†Ύt π‘˜) = βˆͺ (𝑆 β†Ύt π‘˜)
229228isopn2 22949 . . . . . . . . . . . . . . . . . 18 (((𝑆 β†Ύt π‘˜) ∈ Top ∧ (π‘˜ ∩ {𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯}) βŠ† βˆͺ (𝑆 β†Ύt π‘˜)) β†’ ((π‘˜ ∩ {𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯}) ∈ (𝑆 β†Ύt π‘˜) ↔ (βˆͺ (𝑆 β†Ύt π‘˜) βˆ– (π‘˜ ∩ {𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯})) ∈ (Clsdβ€˜(𝑆 β†Ύt π‘˜))))
230225, 227, 229syl2anc 583 . . . . . . . . . . . . . . . . 17 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) ∧ (π‘˜ ∈ 𝒫 βˆͺ 𝑆 ∧ (𝑆 β†Ύt π‘˜) ∈ Comp)) β†’ ((π‘˜ ∩ {𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯}) ∈ (𝑆 β†Ύt π‘˜) ↔ (βˆͺ (𝑆 β†Ύt π‘˜) βˆ– (π‘˜ ∩ {𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯})) ∈ (Clsdβ€˜(𝑆 β†Ύt π‘˜))))
231223, 230mpbird 257 . . . . . . . . . . . . . . . 16 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) ∧ (π‘˜ ∈ 𝒫 βˆͺ 𝑆 ∧ (𝑆 β†Ύt π‘˜) ∈ Comp)) β†’ (π‘˜ ∩ {𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯}) ∈ (𝑆 β†Ύt π‘˜))
23269, 231eqeltrid 2833 . . . . . . . . . . . . . . 15 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) ∧ (π‘˜ ∈ 𝒫 βˆͺ 𝑆 ∧ (𝑆 β†Ύt π‘˜) ∈ Comp)) β†’ ({𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯} ∩ π‘˜) ∈ (𝑆 β†Ύt π‘˜))
233232expr 456 . . . . . . . . . . . . . 14 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) ∧ π‘˜ ∈ 𝒫 βˆͺ 𝑆) β†’ ((𝑆 β†Ύt π‘˜) ∈ Comp β†’ ({𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯} ∩ π‘˜) ∈ (𝑆 β†Ύt π‘˜)))
234233ralrimiva 3143 . . . . . . . . . . . . 13 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) β†’ βˆ€π‘˜ ∈ 𝒫 βˆͺ 𝑆((𝑆 β†Ύt π‘˜) ∈ Comp β†’ ({𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯} ∩ π‘˜) ∈ (𝑆 β†Ύt π‘˜)))
23565, 17sylib 217 . . . . . . . . . . . . . 14 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) β†’ 𝑆 ∈ (TopOnβ€˜βˆͺ 𝑆))
236 elkgen 23453 . . . . . . . . . . . . . 14 (𝑆 ∈ (TopOnβ€˜βˆͺ 𝑆) β†’ ({𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯} ∈ (π‘˜Genβ€˜π‘†) ↔ ({𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯} βŠ† βˆͺ 𝑆 ∧ βˆ€π‘˜ ∈ 𝒫 βˆͺ 𝑆((𝑆 β†Ύt π‘˜) ∈ Comp β†’ ({𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯} ∩ π‘˜) ∈ (𝑆 β†Ύt π‘˜)))))
237235, 236syl 17 . . . . . . . . . . . . 13 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) β†’ ({𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯} ∈ (π‘˜Genβ€˜π‘†) ↔ ({𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯} βŠ† βˆͺ 𝑆 ∧ βˆ€π‘˜ ∈ 𝒫 βˆͺ 𝑆((𝑆 β†Ύt π‘˜) ∈ Comp β†’ ({𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯} ∩ π‘˜) ∈ (𝑆 β†Ύt π‘˜)))))
23868, 234, 237mpbir2and 712 . . . . . . . . . . . 12 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) β†’ {𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯} ∈ (π‘˜Genβ€˜π‘†))
23915adantr 480 . . . . . . . . . . . . . 14 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) β†’ 𝑆 ∈ (ran π‘˜Gen ∩ Haus))
240239, 2syl 17 . . . . . . . . . . . . 13 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) β†’ 𝑆 ∈ ran π‘˜Gen)
241 kgenidm 23464 . . . . . . . . . . . . 13 (𝑆 ∈ ran π‘˜Gen β†’ (π‘˜Genβ€˜π‘†) = 𝑆)
242240, 241syl 17 . . . . . . . . . . . 12 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) β†’ (π‘˜Genβ€˜π‘†) = 𝑆)
243238, 242eleqtrd 2831 . . . . . . . . . . 11 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) β†’ {𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯} ∈ 𝑆)
244 txopn 23519 . . . . . . . . . . 11 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑒 ∈ 𝑅 ∧ {𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯} ∈ 𝑆)) β†’ (𝑒 Γ— {𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯}) ∈ (𝑅 Γ—t 𝑆))
24564, 65, 66, 243, 244syl22anc 838 . . . . . . . . . 10 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) β†’ (𝑒 Γ— {𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯}) ∈ (𝑅 Γ—t 𝑆))
24659adantr 480 . . . . . . . . . . 11 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) β†’ 𝑦 = ⟨(1st β€˜π‘¦), (2nd β€˜π‘¦)⟩)
247 simprr1 1219 . . . . . . . . . . . 12 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) β†’ (1st β€˜π‘¦) ∈ 𝑒)
248 sneq 4639 . . . . . . . . . . . . . . 15 (𝑣 = (2nd β€˜π‘¦) β†’ {𝑣} = {(2nd β€˜π‘¦)})
249248xpeq2d 5708 . . . . . . . . . . . . . 14 (𝑣 = (2nd β€˜π‘¦) β†’ (𝑠 Γ— {𝑣}) = (𝑠 Γ— {(2nd β€˜π‘¦)}))
250249sseq1d 4011 . . . . . . . . . . . . 13 (𝑣 = (2nd β€˜π‘¦) β†’ ((𝑠 Γ— {𝑣}) βŠ† π‘₯ ↔ (𝑠 Γ— {(2nd β€˜π‘¦)}) βŠ† π‘₯))
25134adantr 480 . . . . . . . . . . . . 13 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) β†’ (2nd β€˜π‘¦) ∈ βˆͺ 𝑆)
252 relxp 5696 . . . . . . . . . . . . . . 15 Rel (𝑠 Γ— {(2nd β€˜π‘¦)})
253252a1i 11 . . . . . . . . . . . . . 14 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) β†’ Rel (𝑠 Γ— {(2nd β€˜π‘¦)}))
254 opelxp 5714 . . . . . . . . . . . . . . 15 (βŸ¨π‘Ž, π‘βŸ© ∈ (𝑠 Γ— {(2nd β€˜π‘¦)}) ↔ (π‘Ž ∈ 𝑠 ∧ 𝑏 ∈ {(2nd β€˜π‘¦)}))
25571sselda 3980 . . . . . . . . . . . . . . . . . 18 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) ∧ π‘Ž ∈ 𝑠) β†’ π‘Ž ∈ {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯})
256 opeq1 4874 . . . . . . . . . . . . . . . . . . . . 21 (𝑑 = π‘Ž β†’ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ = βŸ¨π‘Ž, (2nd β€˜π‘¦)⟩)
257256eleq1d 2814 . . . . . . . . . . . . . . . . . . . 20 (𝑑 = π‘Ž β†’ (βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯ ↔ βŸ¨π‘Ž, (2nd β€˜π‘¦)⟩ ∈ π‘₯))
258257elrab 3682 . . . . . . . . . . . . . . . . . . 19 (π‘Ž ∈ {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ↔ (π‘Ž ∈ βˆͺ 𝑅 ∧ βŸ¨π‘Ž, (2nd β€˜π‘¦)⟩ ∈ π‘₯))
259258simprbi 496 . . . . . . . . . . . . . . . . . 18 (π‘Ž ∈ {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} β†’ βŸ¨π‘Ž, (2nd β€˜π‘¦)⟩ ∈ π‘₯)
260255, 259syl 17 . . . . . . . . . . . . . . . . 17 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) ∧ π‘Ž ∈ 𝑠) β†’ βŸ¨π‘Ž, (2nd β€˜π‘¦)⟩ ∈ π‘₯)
261 elsni 4646 . . . . . . . . . . . . . . . . . . 19 (𝑏 ∈ {(2nd β€˜π‘¦)} β†’ 𝑏 = (2nd β€˜π‘¦))
262261opeq2d 4881 . . . . . . . . . . . . . . . . . 18 (𝑏 ∈ {(2nd β€˜π‘¦)} β†’ βŸ¨π‘Ž, π‘βŸ© = βŸ¨π‘Ž, (2nd β€˜π‘¦)⟩)
263262eleq1d 2814 . . . . . . . . . . . . . . . . 17 (𝑏 ∈ {(2nd β€˜π‘¦)} β†’ (βŸ¨π‘Ž, π‘βŸ© ∈ π‘₯ ↔ βŸ¨π‘Ž, (2nd β€˜π‘¦)⟩ ∈ π‘₯))
264260, 263syl5ibrcom 246 . . . . . . . . . . . . . . . 16 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) ∧ π‘Ž ∈ 𝑠) β†’ (𝑏 ∈ {(2nd β€˜π‘¦)} β†’ βŸ¨π‘Ž, π‘βŸ© ∈ π‘₯))
265264expimpd 453 . . . . . . . . . . . . . . 15 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) β†’ ((π‘Ž ∈ 𝑠 ∧ 𝑏 ∈ {(2nd β€˜π‘¦)}) β†’ βŸ¨π‘Ž, π‘βŸ© ∈ π‘₯))
266254, 265biimtrid 241 . . . . . . . . . . . . . 14 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) β†’ (βŸ¨π‘Ž, π‘βŸ© ∈ (𝑠 Γ— {(2nd β€˜π‘¦)}) β†’ βŸ¨π‘Ž, π‘βŸ© ∈ π‘₯))
267253, 266relssdv 5790 . . . . . . . . . . . . 13 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) β†’ (𝑠 Γ— {(2nd β€˜π‘¦)}) βŠ† π‘₯)
268250, 251, 267elrabd 3684 . . . . . . . . . . . 12 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) β†’ (2nd β€˜π‘¦) ∈ {𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯})
269247, 268opelxpd 5717 . . . . . . . . . . 11 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) β†’ ⟨(1st β€˜π‘¦), (2nd β€˜π‘¦)⟩ ∈ (𝑒 Γ— {𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯}))
270246, 269eqeltrd 2829 . . . . . . . . . 10 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) β†’ 𝑦 ∈ (𝑒 Γ— {𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯}))
271 relxp 5696 . . . . . . . . . . . 12 Rel (𝑒 Γ— {𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯})
272271a1i 11 . . . . . . . . . . 11 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) β†’ Rel (𝑒 Γ— {𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯}))
273 opelxp 5714 . . . . . . . . . . . 12 (βŸ¨π‘Ž, π‘βŸ© ∈ (𝑒 Γ— {𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯}) ↔ (π‘Ž ∈ 𝑒 ∧ 𝑏 ∈ {𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯}))
274126elrab 3682 . . . . . . . . . . . . . . 15 (𝑏 ∈ {𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯} ↔ (𝑏 ∈ βˆͺ 𝑆 ∧ (𝑠 Γ— {𝑏}) βŠ† π‘₯))
275274simprbi 496 . . . . . . . . . . . . . 14 (𝑏 ∈ {𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯} β†’ (𝑠 Γ— {𝑏}) βŠ† π‘₯)
276 simprr2 1220 . . . . . . . . . . . . . . . 16 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) β†’ 𝑒 βŠ† 𝑠)
277276sselda 3980 . . . . . . . . . . . . . . 15 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) ∧ π‘Ž ∈ 𝑒) β†’ π‘Ž ∈ 𝑠)
278 vsnid 4666 . . . . . . . . . . . . . . 15 𝑏 ∈ {𝑏}
279 opelxpi 5715 . . . . . . . . . . . . . . 15 ((π‘Ž ∈ 𝑠 ∧ 𝑏 ∈ {𝑏}) β†’ βŸ¨π‘Ž, π‘βŸ© ∈ (𝑠 Γ— {𝑏}))
280277, 278, 279sylancl 585 . . . . . . . . . . . . . 14 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) ∧ π‘Ž ∈ 𝑒) β†’ βŸ¨π‘Ž, π‘βŸ© ∈ (𝑠 Γ— {𝑏}))
281 ssel 3973 . . . . . . . . . . . . . 14 ((𝑠 Γ— {𝑏}) βŠ† π‘₯ β†’ (βŸ¨π‘Ž, π‘βŸ© ∈ (𝑠 Γ— {𝑏}) β†’ βŸ¨π‘Ž, π‘βŸ© ∈ π‘₯))
282275, 280, 281syl2imc 41 . . . . . . . . . . . . 13 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) ∧ π‘Ž ∈ 𝑒) β†’ (𝑏 ∈ {𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯} β†’ βŸ¨π‘Ž, π‘βŸ© ∈ π‘₯))
283282expimpd 453 . . . . . . . . . . . 12 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) β†’ ((π‘Ž ∈ 𝑒 ∧ 𝑏 ∈ {𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯}) β†’ βŸ¨π‘Ž, π‘βŸ© ∈ π‘₯))
284273, 283biimtrid 241 . . . . . . . . . . 11 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) β†’ (βŸ¨π‘Ž, π‘βŸ© ∈ (𝑒 Γ— {𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯}) β†’ βŸ¨π‘Ž, π‘βŸ© ∈ π‘₯))
285272, 284relssdv 5790 . . . . . . . . . 10 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) β†’ (𝑒 Γ— {𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯}) βŠ† π‘₯)
286 eleq2 2818 . . . . . . . . . . . 12 (𝑑 = (𝑒 Γ— {𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯}) β†’ (𝑦 ∈ 𝑑 ↔ 𝑦 ∈ (𝑒 Γ— {𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯})))
287 sseq1 4005 . . . . . . . . . . . 12 (𝑑 = (𝑒 Γ— {𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯}) β†’ (𝑑 βŠ† π‘₯ ↔ (𝑒 Γ— {𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯}) βŠ† π‘₯))
288286, 287anbi12d 631 . . . . . . . . . . 11 (𝑑 = (𝑒 Γ— {𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯}) β†’ ((𝑦 ∈ 𝑑 ∧ 𝑑 βŠ† π‘₯) ↔ (𝑦 ∈ (𝑒 Γ— {𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯}) ∧ (𝑒 Γ— {𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯}) βŠ† π‘₯)))
289288rspcev 3609 . . . . . . . . . 10 (((𝑒 Γ— {𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯}) ∈ (𝑅 Γ—t 𝑆) ∧ (𝑦 ∈ (𝑒 Γ— {𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯}) ∧ (𝑒 Γ— {𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯}) βŠ† π‘₯)) β†’ βˆƒπ‘‘ ∈ (𝑅 Γ—t 𝑆)(𝑦 ∈ 𝑑 ∧ 𝑑 βŠ† π‘₯))
290245, 270, 285, 289syl12anc 836 . . . . . . . . 9 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) β†’ βˆƒπ‘‘ ∈ (𝑅 Γ—t 𝑆)(𝑦 ∈ 𝑑 ∧ 𝑑 βŠ† π‘₯))
291290expr 456 . . . . . . . 8 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ (𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅)) β†’ (((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp) β†’ βˆƒπ‘‘ ∈ (𝑅 Γ—t 𝑆)(𝑦 ∈ 𝑑 ∧ 𝑑 βŠ† π‘₯)))
292291rexlimdvva 3208 . . . . . . 7 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) β†’ (βˆƒπ‘  ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯}βˆƒπ‘’ ∈ 𝑅 ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp) β†’ βˆƒπ‘‘ ∈ (𝑅 Γ—t 𝑆)(𝑦 ∈ 𝑑 ∧ 𝑑 βŠ† π‘₯)))
29363, 292mpd 15 . . . . . 6 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) β†’ βˆƒπ‘‘ ∈ (𝑅 Γ—t 𝑆)(𝑦 ∈ 𝑑 ∧ 𝑑 βŠ† π‘₯))
294293ralrimiva 3143 . . . . 5 (((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) β†’ βˆ€π‘¦ ∈ π‘₯ βˆƒπ‘‘ ∈ (𝑅 Γ—t 𝑆)(𝑦 ∈ 𝑑 ∧ 𝑑 βŠ† π‘₯))
2956adantr 480 . . . . . 6 (((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) β†’ (𝑅 Γ—t 𝑆) ∈ Top)
296 eltop2 22891 . . . . . 6 ((𝑅 Γ—t 𝑆) ∈ Top β†’ (π‘₯ ∈ (𝑅 Γ—t 𝑆) ↔ βˆ€π‘¦ ∈ π‘₯ βˆƒπ‘‘ ∈ (𝑅 Γ—t 𝑆)(𝑦 ∈ 𝑑 ∧ 𝑑 βŠ† π‘₯)))
297295, 296syl 17 . . . . 5 (((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) β†’ (π‘₯ ∈ (𝑅 Γ—t 𝑆) ↔ βˆ€π‘¦ ∈ π‘₯ βˆƒπ‘‘ ∈ (𝑅 Γ—t 𝑆)(𝑦 ∈ 𝑑 ∧ 𝑑 βŠ† π‘₯)))
298294, 297mpbird 257 . . . 4 (((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) β†’ π‘₯ ∈ (𝑅 Γ—t 𝑆))
299298ex 412 . . 3 ((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) β†’ (π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆)) β†’ π‘₯ ∈ (𝑅 Γ—t 𝑆)))
300299ssrdv 3986 . 2 ((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) β†’ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆)) βŠ† (𝑅 Γ—t 𝑆))
301 iskgen2 23465 . 2 ((𝑅 Γ—t 𝑆) ∈ ran π‘˜Gen ↔ ((𝑅 Γ—t 𝑆) ∈ Top ∧ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆)) βŠ† (𝑅 Γ—t 𝑆)))
3026, 300, 301sylanbrc 582 1 ((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) β†’ (𝑅 Γ—t 𝑆) ∈ ran π‘˜Gen)
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 395   ∧ w3a 1085   = wceq 1534   ∈ wcel 2099  βˆ€wral 3058  βˆƒwrex 3067  {crab 3429  Vcvv 3471   βˆ– cdif 3944   ∩ cin 3946   βŠ† wss 3947  π’« cpw 4603  {csn 4629  βŸ¨cop 4635  βˆͺ cuni 4908   ↦ cmpt 5231   I cid 5575   Γ— cxp 5676  β—‘ccnv 5677  ran crn 5679   β†Ύ cres 5680   β€œ cima 5681  Rel wrel 5683   Fn wfn 6543  βŸΆwf 6544  β€˜cfv 6548  (class class class)co 7420  1st c1st 7991  2nd c2nd 7992   β†Ύt crest 17402  Topctop 22808  TopOnctopon 22825  Clsdccld 22933   Cn ccn 23141  Hauscha 23225  Compccmp 23303  π‘›-Locally cnlly 23382  π‘˜Genckgen 23450   Γ—t ctx 23477
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2699  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5365  ax-pr 5429  ax-un 7740
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2530  df-eu 2559  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2938  df-ral 3059  df-rex 3068  df-reu 3374  df-rab 3430  df-v 3473  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4909  df-int 4950  df-iun 4998  df-iin 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5576  df-eprel 5582  df-po 5590  df-so 5591  df-fr 5633  df-we 5635  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-ord 6372  df-on 6373  df-lim 6374  df-suc 6375  df-iota 6500  df-fun 6550  df-fn 6551  df-f 6552  df-f1 6553  df-fo 6554  df-f1o 6555  df-fv 6556  df-ov 7423  df-oprab 7424  df-mpo 7425  df-om 7871  df-1st 7993  df-2nd 7994  df-1o 8487  df-er 8725  df-map 8847  df-en 8965  df-dom 8966  df-fin 8968  df-fi 9435  df-rest 17404  df-topgen 17425  df-top 22809  df-topon 22826  df-bases 22862  df-cld 22936  df-ntr 22937  df-cls 22938  df-nei 23015  df-cn 23144  df-cnp 23145  df-haus 23232  df-cmp 23304  df-nlly 23384  df-kgen 23451  df-tx 23479
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator