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

Theorem txkgen 23026
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 22847 . . 3 (𝑅 ∈ 𝑛-Locally Comp β†’ 𝑅 ∈ Top)
2 elinel1 4159 . . . 4 (𝑆 ∈ (ran π‘˜Gen ∩ Haus) β†’ 𝑆 ∈ ran π‘˜Gen)
3 kgentop 22916 . . . 4 (𝑆 ∈ ran π‘˜Gen β†’ 𝑆 ∈ Top)
42, 3syl 17 . . 3 (𝑆 ∈ (ran π‘˜Gen ∩ Haus) β†’ 𝑆 ∈ Top)
5 txtop 22943 . . 3 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ (𝑅 Γ—t 𝑆) ∈ Top)
61, 4, 5syl2an 597 . 2 ((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) β†’ (𝑅 Γ—t 𝑆) ∈ Top)
7 simplll 774 . . . . . . . 8 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) β†’ 𝑅 ∈ 𝑛-Locally Comp)
8 eqid 2733 . . . . . . . . . 10 (𝑑 ∈ βˆͺ 𝑅 ↦ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩) = (𝑑 ∈ βˆͺ 𝑅 ↦ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩)
98mptpreima 6194 . . . . . . . . 9 (β—‘(𝑑 ∈ βˆͺ 𝑅 ↦ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩) β€œ π‘₯) = {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯}
101ad3antrrr 729 . . . . . . . . . . . . . 14 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) β†’ 𝑅 ∈ Top)
11 toptopon2 22290 . . . . . . . . . . . . . 14 (𝑅 ∈ Top ↔ 𝑅 ∈ (TopOnβ€˜βˆͺ 𝑅))
1210, 11sylib 217 . . . . . . . . . . . . 13 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) β†’ 𝑅 ∈ (TopOnβ€˜βˆͺ 𝑅))
13 idcn 22631 . . . . . . . . . . . . 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 22290 . . . . . . . . . . . . . 14 (𝑆 ∈ Top ↔ 𝑆 ∈ (TopOnβ€˜βˆͺ 𝑆))
1816, 17sylib 217 . . . . . . . . . . . . 13 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) β†’ 𝑆 ∈ (TopOnβ€˜βˆͺ 𝑆))
19 simpr 486 . . . . . . . . . . . . . . . 16 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) β†’ 𝑦 ∈ π‘₯)
20 simplr 768 . . . . . . . . . . . . . . . 16 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) β†’ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆)))
21 elunii 4874 . . . . . . . . . . . . . . . 16 ((𝑦 ∈ π‘₯ ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) β†’ 𝑦 ∈ βˆͺ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆)))
2219, 20, 21syl2anc 585 . . . . . . . . . . . . . . 15 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) β†’ 𝑦 ∈ βˆͺ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆)))
23 eqid 2733 . . . . . . . . . . . . . . . . . 18 βˆͺ 𝑅 = βˆͺ 𝑅
24 eqid 2733 . . . . . . . . . . . . . . . . . 18 βˆͺ 𝑆 = βˆͺ 𝑆
2523, 24txuni 22966 . . . . . . . . . . . . . . . . 17 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ (βˆͺ 𝑅 Γ— βˆͺ 𝑆) = βˆͺ (𝑅 Γ—t 𝑆))
2610, 16, 25syl2anc 585 . . . . . . . . . . . . . . . 16 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) β†’ (βˆͺ 𝑅 Γ— βˆͺ 𝑆) = βˆͺ (𝑅 Γ—t 𝑆))
2710, 16, 5syl2anc 585 . . . . . . . . . . . . . . . . 17 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) β†’ (𝑅 Γ—t 𝑆) ∈ Top)
28 eqid 2733 . . . . . . . . . . . . . . . . . 18 βˆͺ (𝑅 Γ—t 𝑆) = βˆͺ (𝑅 Γ—t 𝑆)
2928kgenuni 22913 . . . . . . . . . . . . . . . . 17 ((𝑅 Γ—t 𝑆) ∈ Top β†’ βˆͺ (𝑅 Γ—t 𝑆) = βˆͺ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆)))
3027, 29syl 17 . . . . . . . . . . . . . . . 16 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) β†’ βˆͺ (𝑅 Γ—t 𝑆) = βˆͺ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆)))
3126, 30eqtrd 2773 . . . . . . . . . . . . . . 15 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) β†’ (βˆͺ 𝑅 Γ— βˆͺ 𝑆) = βˆͺ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆)))
3222, 31eleqtrrd 2837 . . . . . . . . . . . . . 14 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) β†’ 𝑦 ∈ (βˆͺ 𝑅 Γ— βˆͺ 𝑆))
33 xp2nd 7958 . . . . . . . . . . . . . 14 (𝑦 ∈ (βˆͺ 𝑅 Γ— βˆͺ 𝑆) β†’ (2nd β€˜π‘¦) ∈ βˆͺ 𝑆)
3432, 33syl 17 . . . . . . . . . . . . 13 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) β†’ (2nd β€˜π‘¦) ∈ βˆͺ 𝑆)
35 cnconst2 22657 . . . . . . . . . . . . 13 ((𝑅 ∈ (TopOnβ€˜βˆͺ 𝑅) ∧ 𝑆 ∈ (TopOnβ€˜βˆͺ 𝑆) ∧ (2nd β€˜π‘¦) ∈ βˆͺ 𝑆) β†’ (βˆͺ 𝑅 Γ— {(2nd β€˜π‘¦)}) ∈ (𝑅 Cn 𝑆))
3612, 18, 34, 35syl3anc 1372 . . . . . . . . . . . 12 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) β†’ (βˆͺ 𝑅 Γ— {(2nd β€˜π‘¦)}) ∈ (𝑅 Cn 𝑆))
37 fvresi 7123 . . . . . . . . . . . . . . . 16 (𝑑 ∈ βˆͺ 𝑅 β†’ (( I β†Ύ βˆͺ 𝑅)β€˜π‘‘) = 𝑑)
38 fvex 6859 . . . . . . . . . . . . . . . . 17 (2nd β€˜π‘¦) ∈ V
3938fvconst2 7157 . . . . . . . . . . . . . . . 16 (𝑑 ∈ βˆͺ 𝑅 β†’ ((βˆͺ 𝑅 Γ— {(2nd β€˜π‘¦)})β€˜π‘‘) = (2nd β€˜π‘¦))
4037, 39opeq12d 4842 . . . . . . . . . . . . . . 15 (𝑑 ∈ βˆͺ 𝑅 β†’ ⟨(( I β†Ύ βˆͺ 𝑅)β€˜π‘‘), ((βˆͺ 𝑅 Γ— {(2nd β€˜π‘¦)})β€˜π‘‘)⟩ = βŸ¨π‘‘, (2nd β€˜π‘¦)⟩)
4140mpteq2ia 5212 . . . . . . . . . . . . . 14 (𝑑 ∈ βˆͺ 𝑅 ↦ ⟨(( I β†Ύ βˆͺ 𝑅)β€˜π‘‘), ((βˆͺ 𝑅 Γ— {(2nd β€˜π‘¦)})β€˜π‘‘)⟩) = (𝑑 ∈ βˆͺ 𝑅 ↦ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩)
4241eqcomi 2742 . . . . . . . . . . . . 13 (𝑑 ∈ βˆͺ 𝑅 ↦ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩) = (𝑑 ∈ βˆͺ 𝑅 ↦ ⟨(( I β†Ύ βˆͺ 𝑅)β€˜π‘‘), ((βˆͺ 𝑅 Γ— {(2nd β€˜π‘¦)})β€˜π‘‘)⟩)
4323, 42txcnmpt 22998 . . . . . . . . . . . 12 ((( I β†Ύ βˆͺ 𝑅) ∈ (𝑅 Cn 𝑅) ∧ (βˆͺ 𝑅 Γ— {(2nd β€˜π‘¦)}) ∈ (𝑅 Cn 𝑆)) β†’ (𝑑 ∈ βˆͺ 𝑅 ↦ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩) ∈ (𝑅 Cn (𝑅 Γ—t 𝑆)))
4414, 36, 43syl2anc 585 . . . . . . . . . . 11 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) β†’ (𝑑 ∈ βˆͺ 𝑅 ↦ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩) ∈ (𝑅 Cn (𝑅 Γ—t 𝑆)))
45 llycmpkgen 22926 . . . . . . . . . . . . 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 22932 . . . . . . . . . . . 12 ((𝑅 ∈ ran π‘˜Gen ∧ (𝑅 Γ—t 𝑆) ∈ Top) β†’ (𝑅 Cn (𝑅 Γ—t 𝑆)) = (𝑅 Cn (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))))
4946, 47, 48syl2anc 585 . . . . . . . . . . 11 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) β†’ (𝑅 Cn (𝑅 Γ—t 𝑆)) = (𝑅 Cn (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))))
5044, 49eleqtrd 2836 . . . . . . . . . 10 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) β†’ (𝑑 ∈ βˆͺ 𝑅 ↦ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩) ∈ (𝑅 Cn (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))))
51 cnima 22639 . . . . . . . . . 10 (((𝑑 ∈ βˆͺ 𝑅 ↦ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩) ∈ (𝑅 Cn (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) β†’ (β—‘(𝑑 ∈ βˆͺ 𝑅 ↦ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩) β€œ π‘₯) ∈ 𝑅)
5250, 20, 51syl2anc 585 . . . . . . . . 9 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) β†’ (β—‘(𝑑 ∈ βˆͺ 𝑅 ↦ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩) β€œ π‘₯) ∈ 𝑅)
539, 52eqeltrrid 2839 . . . . . . . 8 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) β†’ {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∈ 𝑅)
54 opeq1 4834 . . . . . . . . . 10 (𝑑 = (1st β€˜π‘¦) β†’ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ = ⟨(1st β€˜π‘¦), (2nd β€˜π‘¦)⟩)
5554eleq1d 2819 . . . . . . . . 9 (𝑑 = (1st β€˜π‘¦) β†’ (βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯ ↔ ⟨(1st β€˜π‘¦), (2nd β€˜π‘¦)⟩ ∈ π‘₯))
56 xp1st 7957 . . . . . . . . . 10 (𝑦 ∈ (βˆͺ 𝑅 Γ— βˆͺ 𝑆) β†’ (1st β€˜π‘¦) ∈ βˆͺ 𝑅)
5732, 56syl 17 . . . . . . . . 9 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) β†’ (1st β€˜π‘¦) ∈ βˆͺ 𝑅)
58 1st2nd2 7964 . . . . . . . . . . 11 (𝑦 ∈ (βˆͺ 𝑅 Γ— βˆͺ 𝑆) β†’ 𝑦 = ⟨(1st β€˜π‘¦), (2nd β€˜π‘¦)⟩)
5932, 58syl 17 . . . . . . . . . 10 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) β†’ 𝑦 = ⟨(1st β€˜π‘¦), (2nd β€˜π‘¦)⟩)
6059, 19eqeltrrd 2835 . . . . . . . . 9 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) β†’ ⟨(1st β€˜π‘¦), (2nd β€˜π‘¦)⟩ ∈ π‘₯)
6155, 57, 60elrabd 3651 . . . . . . . 8 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) β†’ (1st β€˜π‘¦) ∈ {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯})
62 nlly2i 22850 . . . . . . . 8 ((𝑅 ∈ 𝑛-Locally Comp ∧ {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∈ 𝑅 ∧ (1st β€˜π‘¦) ∈ {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯}) β†’ βˆƒπ‘  ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯}βˆƒπ‘’ ∈ 𝑅 ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))
637, 53, 61, 62syl3anc 1372 . . . . . . 7 ((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) β†’ βˆƒπ‘  ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯}βˆƒπ‘’ ∈ 𝑅 ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))
6410adantr 482 . . . . . . . . . . 11 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) β†’ 𝑅 ∈ Top)
6516adantr 482 . . . . . . . . . . 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 4041 . . . . . . . . . . . . . 14 {𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯} βŠ† βˆͺ 𝑆
6867a1i 11 . . . . . . . . . . . . 13 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) β†’ {𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯} βŠ† βˆͺ 𝑆)
69 incom 4165 . . . . . . . . . . . . . . . 16 ({𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯} ∩ π‘˜) = (π‘˜ ∩ {𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯})
70 simprll 778 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) β†’ 𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯})
7170elpwid 4573 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) β†’ 𝑠 βŠ† {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯})
72 ssrab2 4041 . . . . . . . . . . . . . . . . . . . . . 22 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} βŠ† βˆͺ 𝑅
7371, 72sstrdi 3960 . . . . . . . . . . . . . . . . . . . . 21 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) β†’ 𝑠 βŠ† βˆͺ 𝑅)
7473adantr 482 . . . . . . . . . . . . . . . . . . . 20 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) ∧ (π‘˜ ∈ 𝒫 βˆͺ 𝑆 ∧ (𝑆 β†Ύt π‘˜) ∈ Comp)) β†’ 𝑠 βŠ† βˆͺ 𝑅)
75 elpwi 4571 . . . . . . . . . . . . . . . . . . . . 21 (π‘˜ ∈ 𝒫 βˆͺ 𝑆 β†’ π‘˜ βŠ† βˆͺ 𝑆)
7675ad2antrl 727 . . . . . . . . . . . . . . . . . . . 20 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) ∧ (π‘˜ ∈ 𝒫 βˆͺ 𝑆 ∧ (𝑆 β†Ύt π‘˜) ∈ Comp)) β†’ π‘˜ βŠ† βˆͺ 𝑆)
77 eldif 3924 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑑 ∈ ((𝑠 Γ— π‘˜) βˆ– π‘₯) ↔ (𝑑 ∈ (𝑠 Γ— π‘˜) ∧ Β¬ 𝑑 ∈ π‘₯))
7877anbi1i 625 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑑 ∈ ((𝑠 Γ— π‘˜) βˆ– π‘₯) ∧ ((2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆))β€˜π‘‘) = 𝑏) ↔ ((𝑑 ∈ (𝑠 Γ— π‘˜) ∧ Β¬ 𝑑 ∈ π‘₯) ∧ ((2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆))β€˜π‘‘) = 𝑏))
79 anass 470 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑑 ∈ (𝑠 Γ— π‘˜) ∧ Β¬ 𝑑 ∈ π‘₯) ∧ ((2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆))β€˜π‘‘) = 𝑏) ↔ (𝑑 ∈ (𝑠 Γ— π‘˜) ∧ (Β¬ 𝑑 ∈ π‘₯ ∧ ((2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆))β€˜π‘‘) = 𝑏)))
8078, 79bitri 275 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑑 ∈ ((𝑠 Γ— π‘˜) βˆ– π‘₯) ∧ ((2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆))β€˜π‘‘) = 𝑏) ↔ (𝑑 ∈ (𝑠 Γ— π‘˜) ∧ (Β¬ 𝑑 ∈ π‘₯ ∧ ((2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆))β€˜π‘‘) = 𝑏)))
8180rexbii2 3090 . . . . . . . . . . . . . . . . . . . . . . . 24 (βˆƒπ‘‘ ∈ ((𝑠 Γ— π‘˜) βˆ– π‘₯)((2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆))β€˜π‘‘) = 𝑏 ↔ βˆƒπ‘‘ ∈ (𝑠 Γ— π‘˜)(Β¬ 𝑑 ∈ π‘₯ ∧ ((2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆))β€˜π‘‘) = 𝑏))
82 ancom 462 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((Β¬ 𝑑 ∈ π‘₯ ∧ ((2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆))β€˜π‘‘) = 𝑏) ↔ (((2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆))β€˜π‘‘) = 𝑏 ∧ Β¬ 𝑑 ∈ π‘₯))
83 fveqeq2 6855 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑑 = βŸ¨π‘Ž, π‘’βŸ© β†’ (((2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆))β€˜π‘‘) = 𝑏 ↔ ((2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆))β€˜βŸ¨π‘Ž, π‘’βŸ©) = 𝑏))
84 eleq1 2822 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑑 = βŸ¨π‘Ž, π‘’βŸ© β†’ (𝑑 ∈ π‘₯ ↔ βŸ¨π‘Ž, π‘’βŸ© ∈ π‘₯))
8584notbid 318 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑑 = βŸ¨π‘Ž, π‘’βŸ© β†’ (Β¬ 𝑑 ∈ π‘₯ ↔ Β¬ βŸ¨π‘Ž, π‘’βŸ© ∈ π‘₯))
8683, 85anbi12d 632 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑑 = βŸ¨π‘Ž, π‘’βŸ© β†’ ((((2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆))β€˜π‘‘) = 𝑏 ∧ Β¬ 𝑑 ∈ π‘₯) ↔ (((2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆))β€˜βŸ¨π‘Ž, π‘’βŸ©) = 𝑏 ∧ Β¬ βŸ¨π‘Ž, π‘’βŸ© ∈ π‘₯)))
8782, 86bitrid 283 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑑 = βŸ¨π‘Ž, π‘’βŸ© β†’ ((Β¬ 𝑑 ∈ π‘₯ ∧ ((2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆))β€˜π‘‘) = 𝑏) ↔ (((2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆))β€˜βŸ¨π‘Ž, π‘’βŸ©) = 𝑏 ∧ Β¬ βŸ¨π‘Ž, π‘’βŸ© ∈ π‘₯)))
8887rexxp 5802 . . . . . . . . . . . . . . . . . . . . . . . 24 (βˆƒπ‘‘ ∈ (𝑠 Γ— π‘˜)(Β¬ 𝑑 ∈ π‘₯ ∧ ((2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆))β€˜π‘‘) = 𝑏) ↔ βˆƒπ‘Ž ∈ 𝑠 βˆƒπ‘’ ∈ π‘˜ (((2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆))β€˜βŸ¨π‘Ž, π‘’βŸ©) = 𝑏 ∧ Β¬ βŸ¨π‘Ž, π‘’βŸ© ∈ π‘₯))
8981, 88bitri 275 . . . . . . . . . . . . . . . . . . . . . . 23 (βˆƒπ‘‘ ∈ ((𝑠 Γ— π‘˜) βˆ– π‘₯)((2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆))β€˜π‘‘) = 𝑏 ↔ βˆƒπ‘Ž ∈ 𝑠 βˆƒπ‘’ ∈ π‘˜ (((2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆))β€˜βŸ¨π‘Ž, π‘’βŸ©) = 𝑏 ∧ Β¬ βŸ¨π‘Ž, π‘’βŸ© ∈ π‘₯))
90 simpl 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑠 βŠ† βˆͺ 𝑅 ∧ π‘˜ βŠ† βˆͺ 𝑆) β†’ 𝑠 βŠ† βˆͺ 𝑅)
9190sselda 3948 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝑠 βŠ† βˆͺ 𝑅 ∧ π‘˜ βŠ† βˆͺ 𝑆) ∧ π‘Ž ∈ 𝑠) β†’ π‘Ž ∈ βˆͺ 𝑅)
9291adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝑠 βŠ† βˆͺ 𝑅 ∧ π‘˜ βŠ† βˆͺ 𝑆) ∧ π‘Ž ∈ 𝑠) ∧ 𝑒 ∈ π‘˜) β†’ π‘Ž ∈ βˆͺ 𝑅)
93 simplr 768 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝑠 βŠ† βˆͺ 𝑅 ∧ π‘˜ βŠ† βˆͺ 𝑆) ∧ π‘Ž ∈ 𝑠) β†’ π‘˜ βŠ† βˆͺ 𝑆)
9493sselda 3948 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝑠 βŠ† βˆͺ 𝑅 ∧ π‘˜ βŠ† βˆͺ 𝑆) ∧ π‘Ž ∈ 𝑠) ∧ 𝑒 ∈ π‘˜) β†’ 𝑒 ∈ βˆͺ 𝑆)
9592, 94opelxpd 5675 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝑠 βŠ† βˆͺ 𝑅 ∧ π‘˜ βŠ† βˆͺ 𝑆) ∧ π‘Ž ∈ 𝑠) ∧ 𝑒 ∈ π‘˜) β†’ βŸ¨π‘Ž, π‘’βŸ© ∈ (βˆͺ 𝑅 Γ— βˆͺ 𝑆))
9695fvresd 6866 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝑠 βŠ† βˆͺ 𝑅 ∧ π‘˜ βŠ† βˆͺ 𝑆) ∧ π‘Ž ∈ 𝑠) ∧ 𝑒 ∈ π‘˜) β†’ ((2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆))β€˜βŸ¨π‘Ž, π‘’βŸ©) = (2nd β€˜βŸ¨π‘Ž, π‘’βŸ©))
97 vex 3451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 π‘Ž ∈ V
98 vex 3451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 𝑒 ∈ V
9997, 98op2nd 7934 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (2nd β€˜βŸ¨π‘Ž, π‘’βŸ©) = 𝑒
10096, 99eqtrdi 2789 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝑠 βŠ† βˆͺ 𝑅 ∧ π‘˜ βŠ† βˆͺ 𝑆) ∧ π‘Ž ∈ 𝑠) ∧ 𝑒 ∈ π‘˜) β†’ ((2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆))β€˜βŸ¨π‘Ž, π‘’βŸ©) = 𝑒)
101100eqeq1d 2735 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝑠 βŠ† βˆͺ 𝑅 ∧ π‘˜ βŠ† βˆͺ 𝑆) ∧ π‘Ž ∈ 𝑠) ∧ 𝑒 ∈ π‘˜) β†’ (((2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆))β€˜βŸ¨π‘Ž, π‘’βŸ©) = 𝑏 ↔ 𝑒 = 𝑏))
102101anbi1d 631 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝑠 βŠ† βˆͺ 𝑅 ∧ π‘˜ βŠ† βˆͺ 𝑆) ∧ π‘Ž ∈ 𝑠) ∧ 𝑒 ∈ π‘˜) β†’ ((((2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆))β€˜βŸ¨π‘Ž, π‘’βŸ©) = 𝑏 ∧ Β¬ βŸ¨π‘Ž, π‘’βŸ© ∈ π‘₯) ↔ (𝑒 = 𝑏 ∧ Β¬ βŸ¨π‘Ž, π‘’βŸ© ∈ π‘₯)))
103102rexbidva 3170 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑠 βŠ† βˆͺ 𝑅 ∧ π‘˜ βŠ† βˆͺ 𝑆) ∧ π‘Ž ∈ 𝑠) β†’ (βˆƒπ‘’ ∈ π‘˜ (((2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆))β€˜βŸ¨π‘Ž, π‘’βŸ©) = 𝑏 ∧ Β¬ βŸ¨π‘Ž, π‘’βŸ© ∈ π‘₯) ↔ βˆƒπ‘’ ∈ π‘˜ (𝑒 = 𝑏 ∧ Β¬ βŸ¨π‘Ž, π‘’βŸ© ∈ π‘₯)))
104 opeq2 4835 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑒 = 𝑏 β†’ βŸ¨π‘Ž, π‘’βŸ© = βŸ¨π‘Ž, π‘βŸ©)
105104eleq1d 2819 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑒 = 𝑏 β†’ (βŸ¨π‘Ž, π‘’βŸ© ∈ π‘₯ ↔ βŸ¨π‘Ž, π‘βŸ© ∈ π‘₯))
106105notbid 318 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑒 = 𝑏 β†’ (Β¬ βŸ¨π‘Ž, π‘’βŸ© ∈ π‘₯ ↔ Β¬ βŸ¨π‘Ž, π‘βŸ© ∈ π‘₯))
107106ceqsrexbv 3610 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (βˆƒπ‘’ ∈ π‘˜ (𝑒 = 𝑏 ∧ Β¬ βŸ¨π‘Ž, π‘’βŸ© ∈ π‘₯) ↔ (𝑏 ∈ π‘˜ ∧ Β¬ βŸ¨π‘Ž, π‘βŸ© ∈ π‘₯))
108103, 107bitrdi 287 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑠 βŠ† βˆͺ 𝑅 ∧ π‘˜ βŠ† βˆͺ 𝑆) ∧ π‘Ž ∈ 𝑠) β†’ (βˆƒπ‘’ ∈ π‘˜ (((2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆))β€˜βŸ¨π‘Ž, π‘’βŸ©) = 𝑏 ∧ Β¬ βŸ¨π‘Ž, π‘’βŸ© ∈ π‘₯) ↔ (𝑏 ∈ π‘˜ ∧ Β¬ βŸ¨π‘Ž, π‘βŸ© ∈ π‘₯)))
109108rexbidva 3170 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑠 βŠ† βˆͺ 𝑅 ∧ π‘˜ βŠ† βˆͺ 𝑆) β†’ (βˆƒπ‘Ž ∈ 𝑠 βˆƒπ‘’ ∈ π‘˜ (((2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆))β€˜βŸ¨π‘Ž, π‘’βŸ©) = 𝑏 ∧ Β¬ βŸ¨π‘Ž, π‘’βŸ© ∈ π‘₯) ↔ βˆƒπ‘Ž ∈ 𝑠 (𝑏 ∈ π‘˜ ∧ Β¬ βŸ¨π‘Ž, π‘βŸ© ∈ π‘₯)))
110 r19.42v 3184 . . . . . . . . . . . . . . . . . . . . . . . 24 (βˆƒπ‘Ž ∈ 𝑠 (𝑏 ∈ π‘˜ ∧ Β¬ βŸ¨π‘Ž, π‘βŸ© ∈ π‘₯) ↔ (𝑏 ∈ π‘˜ ∧ βˆƒπ‘Ž ∈ 𝑠 Β¬ βŸ¨π‘Ž, π‘βŸ© ∈ π‘₯))
111109, 110bitrdi 287 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑠 βŠ† βˆͺ 𝑅 ∧ π‘˜ βŠ† βˆͺ 𝑆) β†’ (βˆƒπ‘Ž ∈ 𝑠 βˆƒπ‘’ ∈ π‘˜ (((2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆))β€˜βŸ¨π‘Ž, π‘’βŸ©) = 𝑏 ∧ Β¬ βŸ¨π‘Ž, π‘’βŸ© ∈ π‘₯) ↔ (𝑏 ∈ π‘˜ ∧ βˆƒπ‘Ž ∈ 𝑠 Β¬ βŸ¨π‘Ž, π‘βŸ© ∈ π‘₯)))
11289, 111bitrid 283 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑠 βŠ† βˆͺ 𝑅 ∧ π‘˜ βŠ† βˆͺ 𝑆) β†’ (βˆƒπ‘‘ ∈ ((𝑠 Γ— π‘˜) βˆ– π‘₯)((2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆))β€˜π‘‘) = 𝑏 ↔ (𝑏 ∈ π‘˜ ∧ βˆƒπ‘Ž ∈ 𝑠 Β¬ βŸ¨π‘Ž, π‘βŸ© ∈ π‘₯)))
113 f2ndres 7950 . . . . . . . . . . . . . . . . . . . . . . . 24 (2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆)):(βˆͺ 𝑅 Γ— βˆͺ 𝑆)⟢βˆͺ 𝑆
114 ffn 6672 . . . . . . . . . . . . . . . . . . . . . . . 24 ((2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆)):(βˆͺ 𝑅 Γ— βˆͺ 𝑆)⟢βˆͺ 𝑆 β†’ (2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆)) Fn (βˆͺ 𝑅 Γ— βˆͺ 𝑆))
115113, 114ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . 23 (2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆)) Fn (βˆͺ 𝑅 Γ— βˆͺ 𝑆)
116 difss 4095 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑠 Γ— π‘˜) βˆ– π‘₯) βŠ† (𝑠 Γ— π‘˜)
117 xpss12 5652 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑠 βŠ† βˆͺ 𝑅 ∧ π‘˜ βŠ† βˆͺ 𝑆) β†’ (𝑠 Γ— π‘˜) βŠ† (βˆͺ 𝑅 Γ— βˆͺ 𝑆))
118116, 117sstrid 3959 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑠 βŠ† βˆͺ 𝑅 ∧ π‘˜ βŠ† βˆͺ 𝑆) β†’ ((𝑠 Γ— π‘˜) βˆ– π‘₯) βŠ† (βˆͺ 𝑅 Γ— βˆͺ 𝑆))
119 fvelimab 6918 . . . . . . . . . . . . . . . . . . . . . . 23 (((2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆)) Fn (βˆͺ 𝑅 Γ— βˆͺ 𝑆) ∧ ((𝑠 Γ— π‘˜) βˆ– π‘₯) βŠ† (βˆͺ 𝑅 Γ— βˆͺ 𝑆)) β†’ (𝑏 ∈ ((2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆)) β€œ ((𝑠 Γ— π‘˜) βˆ– π‘₯)) ↔ βˆƒπ‘‘ ∈ ((𝑠 Γ— π‘˜) βˆ– π‘₯)((2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆))β€˜π‘‘) = 𝑏))
120115, 118, 119sylancr 588 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑠 βŠ† βˆͺ 𝑅 ∧ π‘˜ βŠ† βˆͺ 𝑆) β†’ (𝑏 ∈ ((2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆)) β€œ ((𝑠 Γ— π‘˜) βˆ– π‘₯)) ↔ βˆƒπ‘‘ ∈ ((𝑠 Γ— π‘˜) βˆ– π‘₯)((2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆))β€˜π‘‘) = 𝑏))
121 eldif 3924 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑏 ∈ (π‘˜ βˆ– {𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯}) ↔ (𝑏 ∈ π‘˜ ∧ Β¬ 𝑏 ∈ {𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯}))
122 simpr 486 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑠 βŠ† βˆͺ 𝑅 ∧ π‘˜ βŠ† βˆͺ 𝑆) β†’ π‘˜ βŠ† βˆͺ 𝑆)
123122sselda 3948 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑠 βŠ† βˆͺ 𝑅 ∧ π‘˜ βŠ† βˆͺ 𝑆) ∧ 𝑏 ∈ π‘˜) β†’ 𝑏 ∈ βˆͺ 𝑆)
124 sneq 4600 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑣 = 𝑏 β†’ {𝑣} = {𝑏})
125124xpeq2d 5667 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑣 = 𝑏 β†’ (𝑠 Γ— {𝑣}) = (𝑠 Γ— {𝑏}))
126125sseq1d 3979 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑣 = 𝑏 β†’ ((𝑠 Γ— {𝑣}) βŠ† π‘₯ ↔ (𝑠 Γ— {𝑏}) βŠ† π‘₯))
127 dfss3 3936 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑠 Γ— {𝑏}) βŠ† π‘₯ ↔ βˆ€π‘˜ ∈ (𝑠 Γ— {𝑏})π‘˜ ∈ π‘₯)
128 eleq1 2822 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (π‘˜ = βŸ¨π‘Ž, π‘‘βŸ© β†’ (π‘˜ ∈ π‘₯ ↔ βŸ¨π‘Ž, π‘‘βŸ© ∈ π‘₯))
129128ralxp 5801 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (βˆ€π‘˜ ∈ (𝑠 Γ— {𝑏})π‘˜ ∈ π‘₯ ↔ βˆ€π‘Ž ∈ 𝑠 βˆ€π‘‘ ∈ {𝑏}βŸ¨π‘Ž, π‘‘βŸ© ∈ π‘₯)
130 vex 3451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 𝑏 ∈ V
131 opeq2 4835 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑑 = 𝑏 β†’ βŸ¨π‘Ž, π‘‘βŸ© = βŸ¨π‘Ž, π‘βŸ©)
132131eleq1d 2819 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑑 = 𝑏 β†’ (βŸ¨π‘Ž, π‘‘βŸ© ∈ π‘₯ ↔ βŸ¨π‘Ž, π‘βŸ© ∈ π‘₯))
133130, 132ralsn 4646 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (βˆ€π‘‘ ∈ {𝑏}βŸ¨π‘Ž, π‘‘βŸ© ∈ π‘₯ ↔ βŸ¨π‘Ž, π‘βŸ© ∈ π‘₯)
134133ralbii 3093 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (βˆ€π‘Ž ∈ 𝑠 βˆ€π‘‘ ∈ {𝑏}βŸ¨π‘Ž, π‘‘βŸ© ∈ π‘₯ ↔ βˆ€π‘Ž ∈ 𝑠 βŸ¨π‘Ž, π‘βŸ© ∈ π‘₯)
135127, 129, 1343bitri 297 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑠 Γ— {𝑏}) βŠ† π‘₯ ↔ βˆ€π‘Ž ∈ 𝑠 βŸ¨π‘Ž, π‘βŸ© ∈ π‘₯)
136126, 135bitrdi 287 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑣 = 𝑏 β†’ ((𝑠 Γ— {𝑣}) βŠ† π‘₯ ↔ βˆ€π‘Ž ∈ 𝑠 βŸ¨π‘Ž, π‘βŸ© ∈ π‘₯))
137136elrab3 3650 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑏 ∈ βˆͺ 𝑆 β†’ (𝑏 ∈ {𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯} ↔ βˆ€π‘Ž ∈ 𝑠 βŸ¨π‘Ž, π‘βŸ© ∈ π‘₯))
138123, 137syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑠 βŠ† βˆͺ 𝑅 ∧ π‘˜ βŠ† βˆͺ 𝑆) ∧ 𝑏 ∈ π‘˜) β†’ (𝑏 ∈ {𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯} ↔ βˆ€π‘Ž ∈ 𝑠 βŸ¨π‘Ž, π‘βŸ© ∈ π‘₯))
139138notbid 318 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑠 βŠ† βˆͺ 𝑅 ∧ π‘˜ βŠ† βˆͺ 𝑆) ∧ 𝑏 ∈ π‘˜) β†’ (Β¬ 𝑏 ∈ {𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯} ↔ Β¬ βˆ€π‘Ž ∈ 𝑠 βŸ¨π‘Ž, π‘βŸ© ∈ π‘₯))
140 rexnal 3100 . . . . . . . . . . . . . . . . . . . . . . . . 25 (βˆƒπ‘Ž ∈ 𝑠 Β¬ βŸ¨π‘Ž, π‘βŸ© ∈ π‘₯ ↔ Β¬ βˆ€π‘Ž ∈ 𝑠 βŸ¨π‘Ž, π‘βŸ© ∈ π‘₯)
141139, 140bitr4di 289 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑠 βŠ† βˆͺ 𝑅 ∧ π‘˜ βŠ† βˆͺ 𝑆) ∧ 𝑏 ∈ π‘˜) β†’ (Β¬ 𝑏 ∈ {𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯} ↔ βˆƒπ‘Ž ∈ 𝑠 Β¬ βŸ¨π‘Ž, π‘βŸ© ∈ π‘₯))
142141pm5.32da 580 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑠 βŠ† βˆͺ 𝑅 ∧ π‘˜ βŠ† βˆͺ 𝑆) β†’ ((𝑏 ∈ π‘˜ ∧ Β¬ 𝑏 ∈ {𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯}) ↔ (𝑏 ∈ π‘˜ ∧ βˆƒπ‘Ž ∈ 𝑠 Β¬ βŸ¨π‘Ž, π‘βŸ© ∈ π‘₯)))
143121, 142bitrid 283 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑠 βŠ† βˆͺ 𝑅 ∧ π‘˜ βŠ† βˆͺ 𝑆) β†’ (𝑏 ∈ (π‘˜ βˆ– {𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯}) ↔ (𝑏 ∈ π‘˜ ∧ βˆƒπ‘Ž ∈ 𝑠 Β¬ βŸ¨π‘Ž, π‘βŸ© ∈ π‘₯)))
144112, 120, 1433bitr4d 311 . . . . . . . . . . . . . . . . . . . . 21 ((𝑠 βŠ† βˆͺ 𝑅 ∧ π‘˜ βŠ† βˆͺ 𝑆) β†’ (𝑏 ∈ ((2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆)) β€œ ((𝑠 Γ— π‘˜) βˆ– π‘₯)) ↔ 𝑏 ∈ (π‘˜ βˆ– {𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯})))
145144eqrdv 2731 . . . . . . . . . . . . . . . . . . . 20 ((𝑠 βŠ† βˆͺ 𝑅 ∧ π‘˜ βŠ† βˆͺ 𝑆) β†’ ((2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆)) β€œ ((𝑠 Γ— π‘˜) βˆ– π‘₯)) = (π‘˜ βˆ– {𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯}))
14674, 76, 145syl2anc 585 . . . . . . . . . . . . . . . . . . 19 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) ∧ (π‘˜ ∈ 𝒫 βˆͺ 𝑆 ∧ (𝑆 β†Ύt π‘˜) ∈ Comp)) β†’ ((2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆)) β€œ ((𝑠 Γ— π‘˜) βˆ– π‘₯)) = (π‘˜ βˆ– {𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯}))
147 difin 4225 . . . . . . . . . . . . . . . . . . . 20 (π‘˜ βˆ– (π‘˜ ∩ {𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯})) = (π‘˜ βˆ– {𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯})
14865adantr 482 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) ∧ (π‘˜ ∈ 𝒫 βˆͺ 𝑆 ∧ (𝑆 β†Ύt π‘˜) ∈ Comp)) β†’ 𝑆 ∈ Top)
14924restuni 22536 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑆 ∈ Top ∧ π‘˜ βŠ† βˆͺ 𝑆) β†’ π‘˜ = βˆͺ (𝑆 β†Ύt π‘˜))
150148, 76, 149syl2anc 585 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) ∧ (π‘˜ ∈ 𝒫 βˆͺ 𝑆 ∧ (𝑆 β†Ύt π‘˜) ∈ Comp)) β†’ π‘˜ = βˆͺ (𝑆 β†Ύt π‘˜))
151150difeq1d 4085 . . . . . . . . . . . . . . . . . . . 20 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) ∧ (π‘˜ ∈ 𝒫 βˆͺ 𝑆 ∧ (𝑆 β†Ύt π‘˜) ∈ Comp)) β†’ (π‘˜ βˆ– (π‘˜ ∩ {𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯})) = (βˆͺ (𝑆 β†Ύt π‘˜) βˆ– (π‘˜ ∩ {𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯})))
152147, 151eqtr3id 2787 . . . . . . . . . . . . . . . . . . 19 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) ∧ (π‘˜ ∈ 𝒫 βˆͺ 𝑆 ∧ (𝑆 β†Ύt π‘˜) ∈ Comp)) β†’ (π‘˜ βˆ– {𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯}) = (βˆͺ (𝑆 β†Ύt π‘˜) βˆ– (π‘˜ ∩ {𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯})))
153146, 152eqtrd 2773 . . . . . . . . . . . . . . . . . 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 4163 . . . . . . . . . . . . . . . . . . . 20 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) ∧ (π‘˜ ∈ 𝒫 βˆͺ 𝑆 ∧ (𝑆 β†Ύt π‘˜) ∈ Comp)) β†’ 𝑆 ∈ Haus)
156 df-ima 5650 . . . . . . . . . . . . . . . . . . . . . . 23 ((2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆)) β€œ ((𝑠 Γ— π‘˜) βˆ– π‘₯)) = ran ((2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆)) β†Ύ ((𝑠 Γ— π‘˜) βˆ– π‘₯))
157 resres 5954 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆)) β†Ύ ((𝑠 Γ— π‘˜) βˆ– π‘₯)) = (2nd β†Ύ ((βˆͺ 𝑅 Γ— βˆͺ 𝑆) ∩ ((𝑠 Γ— π‘˜) βˆ– π‘₯)))
158 inss2 4193 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((βˆͺ 𝑅 Γ— βˆͺ 𝑆) ∩ ((𝑠 Γ— π‘˜) βˆ– π‘₯)) βŠ† ((𝑠 Γ— π‘˜) βˆ– π‘₯)
159158, 116sstri 3957 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((βˆͺ 𝑅 Γ— βˆͺ 𝑆) ∩ ((𝑠 Γ— π‘˜) βˆ– π‘₯)) βŠ† (𝑠 Γ— π‘˜)
160 ssres2 5969 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((βˆͺ 𝑅 Γ— βˆͺ 𝑆) ∩ ((𝑠 Γ— π‘˜) βˆ– π‘₯)) βŠ† (𝑠 Γ— π‘˜) β†’ (2nd β†Ύ ((βˆͺ 𝑅 Γ— βˆͺ 𝑆) ∩ ((𝑠 Γ— π‘˜) βˆ– π‘₯))) βŠ† (2nd β†Ύ (𝑠 Γ— π‘˜)))
161159, 160ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . 25 (2nd β†Ύ ((βˆͺ 𝑅 Γ— βˆͺ 𝑆) ∩ ((𝑠 Γ— π‘˜) βˆ– π‘₯))) βŠ† (2nd β†Ύ (𝑠 Γ— π‘˜))
162157, 161eqsstri 3982 . . . . . . . . . . . . . . . . . . . . . . . 24 ((2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆)) β†Ύ ((𝑠 Γ— π‘˜) βˆ– π‘₯)) βŠ† (2nd β†Ύ (𝑠 Γ— π‘˜))
163162rnssi 5899 . . . . . . . . . . . . . . . . . . . . . . 23 ran ((2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆)) β†Ύ ((𝑠 Γ— π‘˜) βˆ– π‘₯)) βŠ† ran (2nd β†Ύ (𝑠 Γ— π‘˜))
164156, 163eqsstri 3982 . . . . . . . . . . . . . . . . . . . . . 22 ((2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆)) β€œ ((𝑠 Γ— π‘˜) βˆ– π‘₯)) βŠ† ran (2nd β†Ύ (𝑠 Γ— π‘˜))
165 f2ndres 7950 . . . . . . . . . . . . . . . . . . . . . . 23 (2nd β†Ύ (𝑠 Γ— π‘˜)):(𝑠 Γ— π‘˜)βŸΆπ‘˜
166 frn 6679 . . . . . . . . . . . . . . . . . . . . . . 23 ((2nd β†Ύ (𝑠 Γ— π‘˜)):(𝑠 Γ— π‘˜)βŸΆπ‘˜ β†’ ran (2nd β†Ύ (𝑠 Γ— π‘˜)) βŠ† π‘˜)
167165, 166ax-mp 5 . . . . . . . . . . . . . . . . . . . . . 22 ran (2nd β†Ύ (𝑠 Γ— π‘˜)) βŠ† π‘˜
168164, 167sstri 3957 . . . . . . . . . . . . . . . . . . . . 21 ((2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆)) β€œ ((𝑠 Γ— π‘˜) βˆ– π‘₯)) βŠ† π‘˜
169168, 76sstrid 3959 . . . . . . . . . . . . . . . . . . . 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 22984 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑅 ∈ (TopOnβ€˜βˆͺ 𝑅) ∧ 𝑆 ∈ (TopOnβ€˜βˆͺ 𝑆)) β†’ (2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆)) ∈ ((𝑅 Γ—t 𝑆) Cn 𝑆))
173170, 171, 172syl2anc 585 . . . . . . . . . . . . . . . . . . . . 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 3451 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑠 ∈ V
177 vex 3451 . . . . . . . . . . . . . . . . . . . . . . . . 25 π‘˜ ∈ V
178176, 177xpex 7691 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑠 Γ— π‘˜) ∈ V
179178a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) ∧ (π‘˜ ∈ 𝒫 βˆͺ 𝑆 ∧ (𝑆 β†Ύt π‘˜) ∈ Comp)) β†’ (𝑠 Γ— π‘˜) ∈ V)
180 restabs 22539 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑅 Γ—t 𝑆) ∈ Top ∧ ((𝑠 Γ— π‘˜) βˆ– π‘₯) βŠ† (𝑠 Γ— π‘˜) ∧ (𝑠 Γ— π‘˜) ∈ V) β†’ (((𝑅 Γ—t 𝑆) β†Ύt (𝑠 Γ— π‘˜)) β†Ύt ((𝑠 Γ— π‘˜) βˆ– π‘₯)) = ((𝑅 Γ—t 𝑆) β†Ύt ((𝑠 Γ— π‘˜) βˆ– π‘₯)))
181174, 175, 179, 180syl3anc 1372 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) ∧ (π‘˜ ∈ 𝒫 βˆͺ 𝑆 ∧ (𝑆 β†Ύt π‘˜) ∈ Comp)) β†’ (((𝑅 Γ—t 𝑆) β†Ύt (𝑠 Γ— π‘˜)) β†Ύt ((𝑠 Γ— π‘˜) βˆ– π‘₯)) = ((𝑅 Γ—t 𝑆) β†Ύt ((𝑠 Γ— π‘˜) βˆ– π‘₯)))
18264adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . 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 23005 . . . . . . . . . . . . . . . . . . . . . . . . 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 1224 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) β†’ (𝑅 β†Ύt 𝑠) ∈ Comp)
189188adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . 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 23017 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑅 β†Ύt 𝑠) ∈ Comp ∧ (𝑆 β†Ύt π‘˜) ∈ Comp) β†’ ((𝑅 β†Ύt 𝑠) Γ—t (𝑆 β†Ύt π‘˜)) ∈ Comp)
192189, 190, 191syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) ∧ (π‘˜ ∈ 𝒫 βˆͺ 𝑆 ∧ (𝑆 β†Ύt π‘˜) ∈ Comp)) β†’ ((𝑅 β†Ύt 𝑠) Γ—t (𝑆 β†Ύt π‘˜)) ∈ Comp)
193187, 192eqeltrd 2834 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) ∧ (π‘˜ ∈ 𝒫 βˆͺ 𝑆 ∧ (𝑆 β†Ύt π‘˜) ∈ Comp)) β†’ ((𝑅 Γ—t 𝑆) β†Ύt (𝑠 Γ— π‘˜)) ∈ Comp)
194 difin 4225 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑠 Γ— π‘˜) βˆ– ((𝑠 Γ— π‘˜) ∩ π‘₯)) = ((𝑠 Γ— π‘˜) βˆ– π‘₯)
19574, 76, 117syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) ∧ (π‘˜ ∈ 𝒫 βˆͺ 𝑆 ∧ (𝑆 β†Ύt π‘˜) ∈ Comp)) β†’ (𝑠 Γ— π‘˜) βŠ† (βˆͺ 𝑅 Γ— βˆͺ 𝑆))
196182, 148, 25syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) ∧ (π‘˜ ∈ 𝒫 βˆͺ 𝑆 ∧ (𝑆 β†Ύt π‘˜) ∈ Comp)) β†’ (βˆͺ 𝑅 Γ— βˆͺ 𝑆) = βˆͺ (𝑅 Γ—t 𝑆))
197195, 196sseqtrd 3988 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) ∧ (π‘˜ ∈ 𝒫 βˆͺ 𝑆 ∧ (𝑆 β†Ύt π‘˜) ∈ Comp)) β†’ (𝑠 Γ— π‘˜) βŠ† βˆͺ (𝑅 Γ—t 𝑆))
19828restuni 22536 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑅 Γ—t 𝑆) ∈ Top ∧ (𝑠 Γ— π‘˜) βŠ† βˆͺ (𝑅 Γ—t 𝑆)) β†’ (𝑠 Γ— π‘˜) = βˆͺ ((𝑅 Γ—t 𝑆) β†Ύt (𝑠 Γ— π‘˜)))
199174, 197, 198syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) ∧ (π‘˜ ∈ 𝒫 βˆͺ 𝑆 ∧ (𝑆 β†Ύt π‘˜) ∈ Comp)) β†’ (𝑠 Γ— π‘˜) = βˆͺ ((𝑅 Γ—t 𝑆) β†Ύt (𝑠 Γ— π‘˜)))
200199difeq1d 4085 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) ∧ (π‘˜ ∈ 𝒫 βˆͺ 𝑆 ∧ (𝑆 β†Ύt π‘˜) ∈ Comp)) β†’ ((𝑠 Γ— π‘˜) βˆ– ((𝑠 Γ— π‘˜) ∩ π‘₯)) = (βˆͺ ((𝑅 Γ—t 𝑆) β†Ύt (𝑠 Γ— π‘˜)) βˆ– ((𝑠 Γ— π‘˜) ∩ π‘₯)))
201194, 200eqtr3id 2787 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) ∧ (π‘˜ ∈ 𝒫 βˆͺ 𝑆 ∧ (𝑆 β†Ύt π‘˜) ∈ Comp)) β†’ ((𝑠 Γ— π‘˜) βˆ– π‘₯) = (βˆͺ ((𝑅 Γ—t 𝑆) β†Ύt (𝑠 Γ— π‘˜)) βˆ– ((𝑠 Γ— π‘˜) ∩ π‘₯)))
202 resttop 22534 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑅 Γ—t 𝑆) ∈ Top ∧ (𝑠 Γ— π‘˜) ∈ V) β†’ ((𝑅 Γ—t 𝑆) β†Ύt (𝑠 Γ— π‘˜)) ∈ Top)
203174, 178, 202sylancl 587 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) ∧ (π‘˜ ∈ 𝒫 βˆͺ 𝑆 ∧ (𝑆 β†Ύt π‘˜) ∈ Comp)) β†’ ((𝑅 Γ—t 𝑆) β†Ύt (𝑠 Γ— π‘˜)) ∈ Top)
204 incom 4165 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑠 Γ— π‘˜) ∩ π‘₯) = (π‘₯ ∩ (𝑠 Γ— π‘˜))
20520ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) ∧ (π‘˜ ∈ 𝒫 βˆͺ 𝑆 ∧ (𝑆 β†Ύt π‘˜) ∈ Comp)) β†’ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆)))
206 kgeni 22911 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆)) ∧ ((𝑅 Γ—t 𝑆) β†Ύt (𝑠 Γ— π‘˜)) ∈ Comp) β†’ (π‘₯ ∩ (𝑠 Γ— π‘˜)) ∈ ((𝑅 Γ—t 𝑆) β†Ύt (𝑠 Γ— π‘˜)))
207205, 193, 206syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) ∧ (π‘˜ ∈ 𝒫 βˆͺ 𝑆 ∧ (𝑆 β†Ύt π‘˜) ∈ Comp)) β†’ (π‘₯ ∩ (𝑠 Γ— π‘˜)) ∈ ((𝑅 Γ—t 𝑆) β†Ύt (𝑠 Γ— π‘˜)))
208204, 207eqeltrid 2838 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) ∧ (π‘˜ ∈ 𝒫 βˆͺ 𝑆 ∧ (𝑆 β†Ύt π‘˜) ∈ Comp)) β†’ ((𝑠 Γ— π‘˜) ∩ π‘₯) ∈ ((𝑅 Γ—t 𝑆) β†Ύt (𝑠 Γ— π‘˜)))
209 eqid 2733 . . . . . . . . . . . . . . . . . . . . . . . . . 26 βˆͺ ((𝑅 Γ—t 𝑆) β†Ύt (𝑠 Γ— π‘˜)) = βˆͺ ((𝑅 Γ—t 𝑆) β†Ύt (𝑠 Γ— π‘˜))
210209opncld 22407 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝑅 Γ—t 𝑆) β†Ύt (𝑠 Γ— π‘˜)) ∈ Top ∧ ((𝑠 Γ— π‘˜) ∩ π‘₯) ∈ ((𝑅 Γ—t 𝑆) β†Ύt (𝑠 Γ— π‘˜))) β†’ (βˆͺ ((𝑅 Γ—t 𝑆) β†Ύt (𝑠 Γ— π‘˜)) βˆ– ((𝑠 Γ— π‘˜) ∩ π‘₯)) ∈ (Clsdβ€˜((𝑅 Γ—t 𝑆) β†Ύt (𝑠 Γ— π‘˜))))
211203, 208, 210syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) ∧ (π‘˜ ∈ 𝒫 βˆͺ 𝑆 ∧ (𝑆 β†Ύt π‘˜) ∈ Comp)) β†’ (βˆͺ ((𝑅 Γ—t 𝑆) β†Ύt (𝑠 Γ— π‘˜)) βˆ– ((𝑠 Γ— π‘˜) ∩ π‘₯)) ∈ (Clsdβ€˜((𝑅 Γ—t 𝑆) β†Ύt (𝑠 Γ— π‘˜))))
212201, 211eqeltrd 2834 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) ∧ (π‘˜ ∈ 𝒫 βˆͺ 𝑆 ∧ (𝑆 β†Ύt π‘˜) ∈ Comp)) β†’ ((𝑠 Γ— π‘˜) βˆ– π‘₯) ∈ (Clsdβ€˜((𝑅 Γ—t 𝑆) β†Ύt (𝑠 Γ— π‘˜))))
213 cmpcld 22776 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑅 Γ—t 𝑆) β†Ύt (𝑠 Γ— π‘˜)) ∈ Comp ∧ ((𝑠 Γ— π‘˜) βˆ– π‘₯) ∈ (Clsdβ€˜((𝑅 Γ—t 𝑆) β†Ύt (𝑠 Γ— π‘˜)))) β†’ (((𝑅 Γ—t 𝑆) β†Ύt (𝑠 Γ— π‘˜)) β†Ύt ((𝑠 Γ— π‘˜) βˆ– π‘₯)) ∈ Comp)
214193, 212, 213syl2anc 585 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) ∧ (π‘˜ ∈ 𝒫 βˆͺ 𝑆 ∧ (𝑆 β†Ύt π‘˜) ∈ Comp)) β†’ (((𝑅 Γ—t 𝑆) β†Ύt (𝑠 Γ— π‘˜)) β†Ύt ((𝑠 Γ— π‘˜) βˆ– π‘₯)) ∈ Comp)
215181, 214eqeltrrd 2835 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) ∧ (π‘˜ ∈ 𝒫 βˆͺ 𝑆 ∧ (𝑆 β†Ύt π‘˜) ∈ Comp)) β†’ ((𝑅 Γ—t 𝑆) β†Ύt ((𝑠 Γ— π‘˜) βˆ– π‘₯)) ∈ Comp)
216 imacmp 22771 . . . . . . . . . . . . . . . . . . . . 21 (((2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆)) ∈ ((𝑅 Γ—t 𝑆) Cn 𝑆) ∧ ((𝑅 Γ—t 𝑆) β†Ύt ((𝑠 Γ— π‘˜) βˆ– π‘₯)) ∈ Comp) β†’ (𝑆 β†Ύt ((2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆)) β€œ ((𝑠 Γ— π‘˜) βˆ– π‘₯))) ∈ Comp)
217173, 215, 216syl2anc 585 . . . . . . . . . . . . . . . . . . . 20 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) ∧ (π‘˜ ∈ 𝒫 βˆͺ 𝑆 ∧ (𝑆 β†Ύt π‘˜) ∈ Comp)) β†’ (𝑆 β†Ύt ((2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆)) β€œ ((𝑠 Γ— π‘˜) βˆ– π‘₯))) ∈ Comp)
21824hauscmp 22781 . . . . . . . . . . . . . . . . . . . 20 ((𝑆 ∈ Haus ∧ ((2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆)) β€œ ((𝑠 Γ— π‘˜) βˆ– π‘₯)) βŠ† βˆͺ 𝑆 ∧ (𝑆 β†Ύt ((2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆)) β€œ ((𝑠 Γ— π‘˜) βˆ– π‘₯))) ∈ Comp) β†’ ((2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆)) β€œ ((𝑠 Γ— π‘˜) βˆ– π‘₯)) ∈ (Clsdβ€˜π‘†))
219155, 169, 217, 218syl3anc 1372 . . . . . . . . . . . . . . . . . . 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 22547 . . . . . . . . . . . . . . . . . . 19 ((π‘˜ βŠ† βˆͺ 𝑆 ∧ ((2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆)) β€œ ((𝑠 Γ— π‘˜) βˆ– π‘₯)) ∈ (Clsdβ€˜π‘†) ∧ ((2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆)) β€œ ((𝑠 Γ— π‘˜) βˆ– π‘₯)) βŠ† π‘˜) β†’ ((2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆)) β€œ ((𝑠 Γ— π‘˜) βˆ– π‘₯)) ∈ (Clsdβ€˜(𝑆 β†Ύt π‘˜)))
22276, 219, 220, 221syl3anc 1372 . . . . . . . . . . . . . . . . . 18 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) ∧ (π‘˜ ∈ 𝒫 βˆͺ 𝑆 ∧ (𝑆 β†Ύt π‘˜) ∈ Comp)) β†’ ((2nd β†Ύ (βˆͺ 𝑅 Γ— βˆͺ 𝑆)) β€œ ((𝑠 Γ— π‘˜) βˆ– π‘₯)) ∈ (Clsdβ€˜(𝑆 β†Ύt π‘˜)))
223153, 222eqeltrrd 2835 . . . . . . . . . . . . . . . . 17 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) ∧ (π‘˜ ∈ 𝒫 βˆͺ 𝑆 ∧ (𝑆 β†Ύt π‘˜) ∈ Comp)) β†’ (βˆͺ (𝑆 β†Ύt π‘˜) βˆ– (π‘˜ ∩ {𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯})) ∈ (Clsdβ€˜(𝑆 β†Ύt π‘˜)))
224 resttop 22534 . . . . . . . . . . . . . . . . . . 19 ((𝑆 ∈ Top ∧ π‘˜ ∈ 𝒫 βˆͺ 𝑆) β†’ (𝑆 β†Ύt π‘˜) ∈ Top)
225148, 185, 224syl2anc 585 . . . . . . . . . . . . . . . . . 18 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) ∧ (π‘˜ ∈ 𝒫 βˆͺ 𝑆 ∧ (𝑆 β†Ύt π‘˜) ∈ Comp)) β†’ (𝑆 β†Ύt π‘˜) ∈ Top)
226 inss1 4192 . . . . . . . . . . . . . . . . . . 19 (π‘˜ ∩ {𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯}) βŠ† π‘˜
227226, 150sseqtrid 4000 . . . . . . . . . . . . . . . . . 18 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) ∧ (π‘˜ ∈ 𝒫 βˆͺ 𝑆 ∧ (𝑆 β†Ύt π‘˜) ∈ Comp)) β†’ (π‘˜ ∩ {𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯}) βŠ† βˆͺ (𝑆 β†Ύt π‘˜))
228 eqid 2733 . . . . . . . . . . . . . . . . . . 19 βˆͺ (𝑆 β†Ύt π‘˜) = βˆͺ (𝑆 β†Ύt π‘˜)
229228isopn2 22406 . . . . . . . . . . . . . . . . . 18 (((𝑆 β†Ύt π‘˜) ∈ Top ∧ (π‘˜ ∩ {𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯}) βŠ† βˆͺ (𝑆 β†Ύt π‘˜)) β†’ ((π‘˜ ∩ {𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯}) ∈ (𝑆 β†Ύt π‘˜) ↔ (βˆͺ (𝑆 β†Ύt π‘˜) βˆ– (π‘˜ ∩ {𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯})) ∈ (Clsdβ€˜(𝑆 β†Ύt π‘˜))))
230225, 227, 229syl2anc 585 . . . . . . . . . . . . . . . . 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 2838 . . . . . . . . . . . . . . 15 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) ∧ (π‘˜ ∈ 𝒫 βˆͺ 𝑆 ∧ (𝑆 β†Ύt π‘˜) ∈ Comp)) β†’ ({𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯} ∩ π‘˜) ∈ (𝑆 β†Ύt π‘˜))
233232expr 458 . . . . . . . . . . . . . 14 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) ∧ π‘˜ ∈ 𝒫 βˆͺ 𝑆) β†’ ((𝑆 β†Ύt π‘˜) ∈ Comp β†’ ({𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯} ∩ π‘˜) ∈ (𝑆 β†Ύt π‘˜)))
234233ralrimiva 3140 . . . . . . . . . . . . 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 22910 . . . . . . . . . . . . . 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 482 . . . . . . . . . . . . . 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 22921 . . . . . . . . . . . . 13 (𝑆 ∈ ran π‘˜Gen β†’ (π‘˜Genβ€˜π‘†) = 𝑆)
242240, 241syl 17 . . . . . . . . . . . 12 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) β†’ (π‘˜Genβ€˜π‘†) = 𝑆)
243238, 242eleqtrd 2836 . . . . . . . . . . 11 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) β†’ {𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯} ∈ 𝑆)
244 txopn 22976 . . . . . . . . . . 11 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑒 ∈ 𝑅 ∧ {𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯} ∈ 𝑆)) β†’ (𝑒 Γ— {𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯}) ∈ (𝑅 Γ—t 𝑆))
24564, 65, 66, 243, 244syl22anc 838 . . . . . . . . . 10 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) β†’ (𝑒 Γ— {𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯}) ∈ (𝑅 Γ—t 𝑆))
24659adantr 482 . . . . . . . . . . 11 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) β†’ 𝑦 = ⟨(1st β€˜π‘¦), (2nd β€˜π‘¦)⟩)
247 simprr1 1222 . . . . . . . . . . . 12 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) β†’ (1st β€˜π‘¦) ∈ 𝑒)
248 sneq 4600 . . . . . . . . . . . . . . 15 (𝑣 = (2nd β€˜π‘¦) β†’ {𝑣} = {(2nd β€˜π‘¦)})
249248xpeq2d 5667 . . . . . . . . . . . . . 14 (𝑣 = (2nd β€˜π‘¦) β†’ (𝑠 Γ— {𝑣}) = (𝑠 Γ— {(2nd β€˜π‘¦)}))
250249sseq1d 3979 . . . . . . . . . . . . 13 (𝑣 = (2nd β€˜π‘¦) β†’ ((𝑠 Γ— {𝑣}) βŠ† π‘₯ ↔ (𝑠 Γ— {(2nd β€˜π‘¦)}) βŠ† π‘₯))
25134adantr 482 . . . . . . . . . . . . 13 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) β†’ (2nd β€˜π‘¦) ∈ βˆͺ 𝑆)
252 relxp 5655 . . . . . . . . . . . . . . 15 Rel (𝑠 Γ— {(2nd β€˜π‘¦)})
253252a1i 11 . . . . . . . . . . . . . 14 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) β†’ Rel (𝑠 Γ— {(2nd β€˜π‘¦)}))
254 opelxp 5673 . . . . . . . . . . . . . . 15 (βŸ¨π‘Ž, π‘βŸ© ∈ (𝑠 Γ— {(2nd β€˜π‘¦)}) ↔ (π‘Ž ∈ 𝑠 ∧ 𝑏 ∈ {(2nd β€˜π‘¦)}))
25571sselda 3948 . . . . . . . . . . . . . . . . . 18 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) ∧ π‘Ž ∈ 𝑠) β†’ π‘Ž ∈ {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯})
256 opeq1 4834 . . . . . . . . . . . . . . . . . . . . 21 (𝑑 = π‘Ž β†’ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ = βŸ¨π‘Ž, (2nd β€˜π‘¦)⟩)
257256eleq1d 2819 . . . . . . . . . . . . . . . . . . . 20 (𝑑 = π‘Ž β†’ (βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯ ↔ βŸ¨π‘Ž, (2nd β€˜π‘¦)⟩ ∈ π‘₯))
258257elrab 3649 . . . . . . . . . . . . . . . . . . 19 (π‘Ž ∈ {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ↔ (π‘Ž ∈ βˆͺ 𝑅 ∧ βŸ¨π‘Ž, (2nd β€˜π‘¦)⟩ ∈ π‘₯))
259258simprbi 498 . . . . . . . . . . . . . . . . . 18 (π‘Ž ∈ {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} β†’ βŸ¨π‘Ž, (2nd β€˜π‘¦)⟩ ∈ π‘₯)
260255, 259syl 17 . . . . . . . . . . . . . . . . 17 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) ∧ π‘Ž ∈ 𝑠) β†’ βŸ¨π‘Ž, (2nd β€˜π‘¦)⟩ ∈ π‘₯)
261 elsni 4607 . . . . . . . . . . . . . . . . . . 19 (𝑏 ∈ {(2nd β€˜π‘¦)} β†’ 𝑏 = (2nd β€˜π‘¦))
262261opeq2d 4841 . . . . . . . . . . . . . . . . . 18 (𝑏 ∈ {(2nd β€˜π‘¦)} β†’ βŸ¨π‘Ž, π‘βŸ© = βŸ¨π‘Ž, (2nd β€˜π‘¦)⟩)
263262eleq1d 2819 . . . . . . . . . . . . . . . . 17 (𝑏 ∈ {(2nd β€˜π‘¦)} β†’ (βŸ¨π‘Ž, π‘βŸ© ∈ π‘₯ ↔ βŸ¨π‘Ž, (2nd β€˜π‘¦)⟩ ∈ π‘₯))
264260, 263syl5ibrcom 247 . . . . . . . . . . . . . . . 16 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) ∧ π‘Ž ∈ 𝑠) β†’ (𝑏 ∈ {(2nd β€˜π‘¦)} β†’ βŸ¨π‘Ž, π‘βŸ© ∈ π‘₯))
265264expimpd 455 . . . . . . . . . . . . . . 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 5748 . . . . . . . . . . . . 13 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) β†’ (𝑠 Γ— {(2nd β€˜π‘¦)}) βŠ† π‘₯)
268250, 251, 267elrabd 3651 . . . . . . . . . . . 12 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) β†’ (2nd β€˜π‘¦) ∈ {𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯})
269247, 268opelxpd 5675 . . . . . . . . . . 11 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) β†’ ⟨(1st β€˜π‘¦), (2nd β€˜π‘¦)⟩ ∈ (𝑒 Γ— {𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯}))
270246, 269eqeltrd 2834 . . . . . . . . . 10 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) β†’ 𝑦 ∈ (𝑒 Γ— {𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯}))
271 relxp 5655 . . . . . . . . . . . 12 Rel (𝑒 Γ— {𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯})
272271a1i 11 . . . . . . . . . . 11 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) β†’ Rel (𝑒 Γ— {𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯}))
273 opelxp 5673 . . . . . . . . . . . 12 (βŸ¨π‘Ž, π‘βŸ© ∈ (𝑒 Γ— {𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯}) ↔ (π‘Ž ∈ 𝑒 ∧ 𝑏 ∈ {𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯}))
274126elrab 3649 . . . . . . . . . . . . . . 15 (𝑏 ∈ {𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯} ↔ (𝑏 ∈ βˆͺ 𝑆 ∧ (𝑠 Γ— {𝑏}) βŠ† π‘₯))
275274simprbi 498 . . . . . . . . . . . . . 14 (𝑏 ∈ {𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯} β†’ (𝑠 Γ— {𝑏}) βŠ† π‘₯)
276 simprr2 1223 . . . . . . . . . . . . . . . 16 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) β†’ 𝑒 βŠ† 𝑠)
277276sselda 3948 . . . . . . . . . . . . . . 15 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) ∧ π‘Ž ∈ 𝑒) β†’ π‘Ž ∈ 𝑠)
278 vsnid 4627 . . . . . . . . . . . . . . 15 𝑏 ∈ {𝑏}
279 opelxpi 5674 . . . . . . . . . . . . . . 15 ((π‘Ž ∈ 𝑠 ∧ 𝑏 ∈ {𝑏}) β†’ βŸ¨π‘Ž, π‘βŸ© ∈ (𝑠 Γ— {𝑏}))
280277, 278, 279sylancl 587 . . . . . . . . . . . . . 14 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) ∧ π‘Ž ∈ 𝑒) β†’ βŸ¨π‘Ž, π‘βŸ© ∈ (𝑠 Γ— {𝑏}))
281 ssel 3941 . . . . . . . . . . . . . 14 ((𝑠 Γ— {𝑏}) βŠ† π‘₯ β†’ (βŸ¨π‘Ž, π‘βŸ© ∈ (𝑠 Γ— {𝑏}) β†’ βŸ¨π‘Ž, π‘βŸ© ∈ π‘₯))
282275, 280, 281syl2imc 41 . . . . . . . . . . . . 13 ((((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) ∧ π‘Ž ∈ 𝑒) β†’ (𝑏 ∈ {𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯} β†’ βŸ¨π‘Ž, π‘βŸ© ∈ π‘₯))
283282expimpd 455 . . . . . . . . . . . 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 5748 . . . . . . . . . 10 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) β†’ (𝑒 Γ— {𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯}) βŠ† π‘₯)
286 eleq2 2823 . . . . . . . . . . . 12 (𝑑 = (𝑒 Γ— {𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯}) β†’ (𝑦 ∈ 𝑑 ↔ 𝑦 ∈ (𝑒 Γ— {𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯})))
287 sseq1 3973 . . . . . . . . . . . 12 (𝑑 = (𝑒 Γ— {𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯}) β†’ (𝑑 βŠ† π‘₯ ↔ (𝑒 Γ— {𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯}) βŠ† π‘₯))
288286, 287anbi12d 632 . . . . . . . . . . 11 (𝑑 = (𝑒 Γ— {𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯}) β†’ ((𝑦 ∈ 𝑑 ∧ 𝑑 βŠ† π‘₯) ↔ (𝑦 ∈ (𝑒 Γ— {𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯}) ∧ (𝑒 Γ— {𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯}) βŠ† π‘₯)))
289288rspcev 3583 . . . . . . . . . 10 (((𝑒 Γ— {𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯}) ∈ (𝑅 Γ—t 𝑆) ∧ (𝑦 ∈ (𝑒 Γ— {𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯}) ∧ (𝑒 Γ— {𝑣 ∈ βˆͺ 𝑆 ∣ (𝑠 Γ— {𝑣}) βŠ† π‘₯}) βŠ† π‘₯)) β†’ βˆƒπ‘‘ ∈ (𝑅 Γ—t 𝑆)(𝑦 ∈ 𝑑 ∧ 𝑑 βŠ† π‘₯))
290245, 270, 285, 289syl12anc 836 . . . . . . . . 9 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ ((𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅) ∧ ((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp))) β†’ βˆƒπ‘‘ ∈ (𝑅 Γ—t 𝑆)(𝑦 ∈ 𝑑 ∧ 𝑑 βŠ† π‘₯))
291290expr 458 . . . . . . . 8 (((((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) ∧ 𝑦 ∈ π‘₯) ∧ (𝑠 ∈ 𝒫 {𝑑 ∈ βˆͺ 𝑅 ∣ βŸ¨π‘‘, (2nd β€˜π‘¦)⟩ ∈ π‘₯} ∧ 𝑒 ∈ 𝑅)) β†’ (((1st β€˜π‘¦) ∈ 𝑒 ∧ 𝑒 βŠ† 𝑠 ∧ (𝑅 β†Ύt 𝑠) ∈ Comp) β†’ βˆƒπ‘‘ ∈ (𝑅 Γ—t 𝑆)(𝑦 ∈ 𝑑 ∧ 𝑑 βŠ† π‘₯)))
292291rexlimdvva 3202 . . . . . . 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 3140 . . . . 5 (((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) β†’ βˆ€π‘¦ ∈ π‘₯ βˆƒπ‘‘ ∈ (𝑅 Γ—t 𝑆)(𝑦 ∈ 𝑑 ∧ 𝑑 βŠ† π‘₯))
2956adantr 482 . . . . . 6 (((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) ∧ π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆))) β†’ (𝑅 Γ—t 𝑆) ∈ Top)
296 eltop2 22348 . . . . . 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 414 . . 3 ((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) β†’ (π‘₯ ∈ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆)) β†’ π‘₯ ∈ (𝑅 Γ—t 𝑆)))
300299ssrdv 3954 . 2 ((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) β†’ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆)) βŠ† (𝑅 Γ—t 𝑆))
301 iskgen2 22922 . 2 ((𝑅 Γ—t 𝑆) ∈ ran π‘˜Gen ↔ ((𝑅 Γ—t 𝑆) ∈ Top ∧ (π‘˜Genβ€˜(𝑅 Γ—t 𝑆)) βŠ† (𝑅 Γ—t 𝑆)))
3026, 300, 301sylanbrc 584 1 ((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran π‘˜Gen ∩ Haus)) β†’ (𝑅 Γ—t 𝑆) ∈ ran π‘˜Gen)
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 397   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107  βˆ€wral 3061  βˆƒwrex 3070  {crab 3406  Vcvv 3447   βˆ– cdif 3911   ∩ cin 3913   βŠ† wss 3914  π’« cpw 4564  {csn 4590  βŸ¨cop 4596  βˆͺ cuni 4869   ↦ cmpt 5192   I cid 5534   Γ— cxp 5635  β—‘ccnv 5636  ran crn 5638   β†Ύ cres 5639   β€œ cima 5640  Rel wrel 5642   Fn wfn 6495  βŸΆwf 6496  β€˜cfv 6500  (class class class)co 7361  1st c1st 7923  2nd c2nd 7924   β†Ύt crest 17310  Topctop 22265  TopOnctopon 22282  Clsdccld 22390   Cn ccn 22598  Hauscha 22682  Compccmp 22760  π‘›-Locally cnlly 22839  π‘˜Genckgen 22907   Γ—t ctx 22934
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5246  ax-sep 5260  ax-nul 5267  ax-pow 5324  ax-pr 5388  ax-un 7676
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3353  df-rab 3407  df-v 3449  df-sbc 3744  df-csb 3860  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-pss 3933  df-nul 4287  df-if 4491  df-pw 4566  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4870  df-int 4912  df-iun 4960  df-iin 4961  df-br 5110  df-opab 5172  df-mpt 5193  df-tr 5227  df-id 5535  df-eprel 5541  df-po 5549  df-so 5550  df-fr 5592  df-we 5594  df-xp 5643  df-rel 5644  df-cnv 5645  df-co 5646  df-dm 5647  df-rn 5648  df-res 5649  df-ima 5650  df-ord 6324  df-on 6325  df-lim 6326  df-suc 6327  df-iota 6452  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-ov 7364  df-oprab 7365  df-mpo 7366  df-om 7807  df-1st 7925  df-2nd 7926  df-1o 8416  df-er 8654  df-map 8773  df-en 8890  df-dom 8891  df-fin 8893  df-fi 9355  df-rest 17312  df-topgen 17333  df-top 22266  df-topon 22283  df-bases 22319  df-cld 22393  df-ntr 22394  df-cls 22395  df-nei 22472  df-cn 22601  df-cnp 22602  df-haus 22689  df-cmp 22761  df-nlly 22841  df-kgen 22908  df-tx 22936
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator