MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  utop2nei Structured version   Visualization version   GIF version
Theorem utop2nei 23975
Description: For any symmetrical entourage 𝑉 and any relation 𝑀, build a neighborhood of 𝑀. First part of proposition 2 of [BourbakiTop1] p. II.4. (Contributed by Thierry Arnoux, 14-Jan-2018.)
Hypothesis
Ref Expression
utoptop.1 𝐽 = (unifTopβ€˜π‘ˆ)
Assertion
Ref Expression
utop2nei ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) β†’ (𝑉 ∘ (𝑀 ∘ 𝑉)) ∈ ((neiβ€˜(𝐽 Γ—t 𝐽))β€˜π‘€))
Proof of Theorem utop2nei
Dummy variables π‘Ÿ 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 utoptop.1 . . . . . . . 8 𝐽 = (unifTopβ€˜π‘ˆ)
2 utoptop 23959 . . . . . . . 8 (π‘ˆ ∈ (UnifOnβ€˜π‘‹) β†’ (unifTopβ€˜π‘ˆ) ∈ Top)
31, 2eqeltrid 2835 . . . . . . 7 (π‘ˆ ∈ (UnifOnβ€˜π‘‹) β†’ 𝐽 ∈ Top)
4 txtop 23293 . . . . . . 7 ((𝐽 ∈ Top ∧ 𝐽 ∈ Top) β†’ (𝐽 Γ—t 𝐽) ∈ Top)
53, 3, 4syl2anc 582 . . . . . 6 (π‘ˆ ∈ (UnifOnβ€˜π‘‹) β†’ (𝐽 Γ—t 𝐽) ∈ Top)
653ad2ant1 1131 . . . . 5 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) β†’ (𝐽 Γ—t 𝐽) ∈ Top)
76adantr 479 . . . 4 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ 𝑀 = βˆ…) β†’ (𝐽 Γ—t 𝐽) ∈ Top)
8 0nei 22852 . . . 4 ((𝐽 Γ—t 𝐽) ∈ Top β†’ βˆ… ∈ ((neiβ€˜(𝐽 Γ—t 𝐽))β€˜βˆ…))
97, 8syl 17 . . 3 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ 𝑀 = βˆ…) β†’ βˆ… ∈ ((neiβ€˜(𝐽 Γ—t 𝐽))β€˜βˆ…))
10 coeq1 5856 . . . . . . 7 (𝑀 = βˆ… β†’ (𝑀 ∘ 𝑉) = (βˆ… ∘ 𝑉))
11 co01 6259 . . . . . . 7 (βˆ… ∘ 𝑉) = βˆ…
1210, 11eqtrdi 2786 . . . . . 6 (𝑀 = βˆ… β†’ (𝑀 ∘ 𝑉) = βˆ…)
1312coeq2d 5861 . . . . 5 (𝑀 = βˆ… β†’ (𝑉 ∘ (𝑀 ∘ 𝑉)) = (𝑉 ∘ βˆ…))
14 co02 6258 . . . . 5 (𝑉 ∘ βˆ…) = βˆ…
1513, 14eqtrdi 2786 . . . 4 (𝑀 = βˆ… β†’ (𝑉 ∘ (𝑀 ∘ 𝑉)) = βˆ…)
1615adantl 480 . . 3 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ 𝑀 = βˆ…) β†’ (𝑉 ∘ (𝑀 ∘ 𝑉)) = βˆ…)
17 simpr 483 . . . 4 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ 𝑀 = βˆ…) β†’ 𝑀 = βˆ…)
1817fveq2d 6894 . . 3 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ 𝑀 = βˆ…) β†’ ((neiβ€˜(𝐽 Γ—t 𝐽))β€˜π‘€) = ((neiβ€˜(𝐽 Γ—t 𝐽))β€˜βˆ…))
199, 16, 183eltr4d 2846 . 2 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ 𝑀 = βˆ…) β†’ (𝑉 ∘ (𝑀 ∘ 𝑉)) ∈ ((neiβ€˜(𝐽 Γ—t 𝐽))β€˜π‘€))
206adantr 479 . . . . . 6 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ π‘Ÿ ∈ 𝑀) β†’ (𝐽 Γ—t 𝐽) ∈ Top)
21 simpl1 1189 . . . . . . . . . 10 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ π‘Ÿ ∈ 𝑀) β†’ π‘ˆ ∈ (UnifOnβ€˜π‘‹))
2221, 3syl 17 . . . . . . . . 9 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ π‘Ÿ ∈ 𝑀) β†’ 𝐽 ∈ Top)
23 simpl2l 1224 . . . . . . . . . 10 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ π‘Ÿ ∈ 𝑀) β†’ 𝑉 ∈ π‘ˆ)
24 simp3 1136 . . . . . . . . . . . 12 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) β†’ 𝑀 βŠ† (𝑋 Γ— 𝑋))
2524sselda 3981 . . . . . . . . . . 11 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ π‘Ÿ ∈ 𝑀) β†’ π‘Ÿ ∈ (𝑋 Γ— 𝑋))
26 xp1st 8009 . . . . . . . . . . 11 (π‘Ÿ ∈ (𝑋 Γ— 𝑋) β†’ (1st β€˜π‘Ÿ) ∈ 𝑋)
2725, 26syl 17 . . . . . . . . . 10 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ π‘Ÿ ∈ 𝑀) β†’ (1st β€˜π‘Ÿ) ∈ 𝑋)
281utopsnnei 23974 . . . . . . . . . 10 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑉 ∈ π‘ˆ ∧ (1st β€˜π‘Ÿ) ∈ 𝑋) β†’ (𝑉 β€œ {(1st β€˜π‘Ÿ)}) ∈ ((neiβ€˜π½)β€˜{(1st β€˜π‘Ÿ)}))
2921, 23, 27, 28syl3anc 1369 . . . . . . . . 9 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ π‘Ÿ ∈ 𝑀) β†’ (𝑉 β€œ {(1st β€˜π‘Ÿ)}) ∈ ((neiβ€˜π½)β€˜{(1st β€˜π‘Ÿ)}))
30 xp2nd 8010 . . . . . . . . . . 11 (π‘Ÿ ∈ (𝑋 Γ— 𝑋) β†’ (2nd β€˜π‘Ÿ) ∈ 𝑋)
3125, 30syl 17 . . . . . . . . . 10 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ π‘Ÿ ∈ 𝑀) β†’ (2nd β€˜π‘Ÿ) ∈ 𝑋)
321utopsnnei 23974 . . . . . . . . . 10 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑉 ∈ π‘ˆ ∧ (2nd β€˜π‘Ÿ) ∈ 𝑋) β†’ (𝑉 β€œ {(2nd β€˜π‘Ÿ)}) ∈ ((neiβ€˜π½)β€˜{(2nd β€˜π‘Ÿ)}))
3321, 23, 31, 32syl3anc 1369 . . . . . . . . 9 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ π‘Ÿ ∈ 𝑀) β†’ (𝑉 β€œ {(2nd β€˜π‘Ÿ)}) ∈ ((neiβ€˜π½)β€˜{(2nd β€˜π‘Ÿ)}))
34 eqid 2730 . . . . . . . . . 10 βˆͺ 𝐽 = βˆͺ 𝐽
3534, 34neitx 23331 . . . . . . . . 9 (((𝐽 ∈ Top ∧ 𝐽 ∈ Top) ∧ ((𝑉 β€œ {(1st β€˜π‘Ÿ)}) ∈ ((neiβ€˜π½)β€˜{(1st β€˜π‘Ÿ)}) ∧ (𝑉 β€œ {(2nd β€˜π‘Ÿ)}) ∈ ((neiβ€˜π½)β€˜{(2nd β€˜π‘Ÿ)}))) β†’ ((𝑉 β€œ {(1st β€˜π‘Ÿ)}) Γ— (𝑉 β€œ {(2nd β€˜π‘Ÿ)})) ∈ ((neiβ€˜(𝐽 Γ—t 𝐽))β€˜({(1st β€˜π‘Ÿ)} Γ— {(2nd β€˜π‘Ÿ)})))
3622, 22, 29, 33, 35syl22anc 835 . . . . . . . 8 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ π‘Ÿ ∈ 𝑀) β†’ ((𝑉 β€œ {(1st β€˜π‘Ÿ)}) Γ— (𝑉 β€œ {(2nd β€˜π‘Ÿ)})) ∈ ((neiβ€˜(𝐽 Γ—t 𝐽))β€˜({(1st β€˜π‘Ÿ)} Γ— {(2nd β€˜π‘Ÿ)})))
37 fvex 6903 . . . . . . . . . 10 (1st β€˜π‘Ÿ) ∈ V
38 fvex 6903 . . . . . . . . . 10 (2nd β€˜π‘Ÿ) ∈ V
3937, 38xpsn 7140 . . . . . . . . 9 ({(1st β€˜π‘Ÿ)} Γ— {(2nd β€˜π‘Ÿ)}) = {⟨(1st β€˜π‘Ÿ), (2nd β€˜π‘Ÿ)⟩}
4039fveq2i 6893 . . . . . . . 8 ((neiβ€˜(𝐽 Γ—t 𝐽))β€˜({(1st β€˜π‘Ÿ)} Γ— {(2nd β€˜π‘Ÿ)})) = ((neiβ€˜(𝐽 Γ—t 𝐽))β€˜{⟨(1st β€˜π‘Ÿ), (2nd β€˜π‘Ÿ)⟩})
4136, 40eleqtrdi 2841 . . . . . . 7 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ π‘Ÿ ∈ 𝑀) β†’ ((𝑉 β€œ {(1st β€˜π‘Ÿ)}) Γ— (𝑉 β€œ {(2nd β€˜π‘Ÿ)})) ∈ ((neiβ€˜(𝐽 Γ—t 𝐽))β€˜{⟨(1st β€˜π‘Ÿ), (2nd β€˜π‘Ÿ)⟩}))
4224adantr 479 . . . . . . . . . . 11 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ π‘Ÿ ∈ 𝑀) β†’ 𝑀 βŠ† (𝑋 Γ— 𝑋))
43 xpss 5691 . . . . . . . . . . . . 13 (𝑋 Γ— 𝑋) βŠ† (V Γ— V)
44 sstr 3989 . . . . . . . . . . . . 13 ((𝑀 βŠ† (𝑋 Γ— 𝑋) ∧ (𝑋 Γ— 𝑋) βŠ† (V Γ— V)) β†’ 𝑀 βŠ† (V Γ— V))
4543, 44mpan2 687 . . . . . . . . . . . 12 (𝑀 βŠ† (𝑋 Γ— 𝑋) β†’ 𝑀 βŠ† (V Γ— V))
46 df-rel 5682 . . . . . . . . . . . 12 (Rel 𝑀 ↔ 𝑀 βŠ† (V Γ— V))
4745, 46sylibr 233 . . . . . . . . . . 11 (𝑀 βŠ† (𝑋 Γ— 𝑋) β†’ Rel 𝑀)
4842, 47syl 17 . . . . . . . . . 10 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ π‘Ÿ ∈ 𝑀) β†’ Rel 𝑀)
49 1st2nd 8027 . . . . . . . . . 10 ((Rel 𝑀 ∧ π‘Ÿ ∈ 𝑀) β†’ π‘Ÿ = ⟨(1st β€˜π‘Ÿ), (2nd β€˜π‘Ÿ)⟩)
5048, 49sylancom 586 . . . . . . . . 9 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ π‘Ÿ ∈ 𝑀) β†’ π‘Ÿ = ⟨(1st β€˜π‘Ÿ), (2nd β€˜π‘Ÿ)⟩)
5150sneqd 4639 . . . . . . . 8 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ π‘Ÿ ∈ 𝑀) β†’ {π‘Ÿ} = {⟨(1st β€˜π‘Ÿ), (2nd β€˜π‘Ÿ)⟩})
5251fveq2d 6894 . . . . . . 7 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ π‘Ÿ ∈ 𝑀) β†’ ((neiβ€˜(𝐽 Γ—t 𝐽))β€˜{π‘Ÿ}) = ((neiβ€˜(𝐽 Γ—t 𝐽))β€˜{⟨(1st β€˜π‘Ÿ), (2nd β€˜π‘Ÿ)⟩}))
5341, 52eleqtrrd 2834 . . . . . 6 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ π‘Ÿ ∈ 𝑀) β†’ ((𝑉 β€œ {(1st β€˜π‘Ÿ)}) Γ— (𝑉 β€œ {(2nd β€˜π‘Ÿ)})) ∈ ((neiβ€˜(𝐽 Γ—t 𝐽))β€˜{π‘Ÿ}))
54 relxp 5693 . . . . . . . . . . 11 Rel ((𝑉 β€œ {(1st β€˜π‘Ÿ)}) Γ— (𝑉 β€œ {(2nd β€˜π‘Ÿ)}))
5554a1i 11 . . . . . . . . . 10 ((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ π‘Ÿ ∈ 𝑀) ∧ 𝑧 ∈ ((𝑉 β€œ {(1st β€˜π‘Ÿ)}) Γ— (𝑉 β€œ {(2nd β€˜π‘Ÿ)}))) β†’ Rel ((𝑉 β€œ {(1st β€˜π‘Ÿ)}) Γ— (𝑉 β€œ {(2nd β€˜π‘Ÿ)})))
56 1st2nd 8027 . . . . . . . . . 10 ((Rel ((𝑉 β€œ {(1st β€˜π‘Ÿ)}) Γ— (𝑉 β€œ {(2nd β€˜π‘Ÿ)})) ∧ 𝑧 ∈ ((𝑉 β€œ {(1st β€˜π‘Ÿ)}) Γ— (𝑉 β€œ {(2nd β€˜π‘Ÿ)}))) β†’ 𝑧 = ⟨(1st β€˜π‘§), (2nd β€˜π‘§)⟩)
5755, 56sylancom 586 . . . . . . . . 9 ((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ π‘Ÿ ∈ 𝑀) ∧ 𝑧 ∈ ((𝑉 β€œ {(1st β€˜π‘Ÿ)}) Γ— (𝑉 β€œ {(2nd β€˜π‘Ÿ)}))) β†’ 𝑧 = ⟨(1st β€˜π‘§), (2nd β€˜π‘§)⟩)
58 simpll2 1211 . . . . . . . . . . . . 13 ((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ π‘Ÿ ∈ 𝑀) ∧ 𝑧 ∈ ((𝑉 β€œ {(1st β€˜π‘Ÿ)}) Γ— (𝑉 β€œ {(2nd β€˜π‘Ÿ)}))) β†’ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉))
5958simprd 494 . . . . . . . . . . . 12 ((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ π‘Ÿ ∈ 𝑀) ∧ 𝑧 ∈ ((𝑉 β€œ {(1st β€˜π‘Ÿ)}) Γ— (𝑉 β€œ {(2nd β€˜π‘Ÿ)}))) β†’ ◑𝑉 = 𝑉)
60 simpll1 1210 . . . . . . . . . . . . . 14 ((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ π‘Ÿ ∈ 𝑀) ∧ 𝑧 ∈ ((𝑉 β€œ {(1st β€˜π‘Ÿ)}) Γ— (𝑉 β€œ {(2nd β€˜π‘Ÿ)}))) β†’ π‘ˆ ∈ (UnifOnβ€˜π‘‹))
6158simpld 493 . . . . . . . . . . . . . 14 ((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ π‘Ÿ ∈ 𝑀) ∧ 𝑧 ∈ ((𝑉 β€œ {(1st β€˜π‘Ÿ)}) Γ— (𝑉 β€œ {(2nd β€˜π‘Ÿ)}))) β†’ 𝑉 ∈ π‘ˆ)
62 ustrel 23936 . . . . . . . . . . . . . 14 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑉 ∈ π‘ˆ) β†’ Rel 𝑉)
6360, 61, 62syl2anc 582 . . . . . . . . . . . . 13 ((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ π‘Ÿ ∈ 𝑀) ∧ 𝑧 ∈ ((𝑉 β€œ {(1st β€˜π‘Ÿ)}) Γ— (𝑉 β€œ {(2nd β€˜π‘Ÿ)}))) β†’ Rel 𝑉)
64 xp1st 8009 . . . . . . . . . . . . . 14 (𝑧 ∈ ((𝑉 β€œ {(1st β€˜π‘Ÿ)}) Γ— (𝑉 β€œ {(2nd β€˜π‘Ÿ)})) β†’ (1st β€˜π‘§) ∈ (𝑉 β€œ {(1st β€˜π‘Ÿ)}))
6564adantl 480 . . . . . . . . . . . . 13 ((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ π‘Ÿ ∈ 𝑀) ∧ 𝑧 ∈ ((𝑉 β€œ {(1st β€˜π‘Ÿ)}) Γ— (𝑉 β€œ {(2nd β€˜π‘Ÿ)}))) β†’ (1st β€˜π‘§) ∈ (𝑉 β€œ {(1st β€˜π‘Ÿ)}))
66 elrelimasn 6083 . . . . . . . . . . . . . 14 (Rel 𝑉 β†’ ((1st β€˜π‘§) ∈ (𝑉 β€œ {(1st β€˜π‘Ÿ)}) ↔ (1st β€˜π‘Ÿ)𝑉(1st β€˜π‘§)))
6766biimpa 475 . . . . . . . . . . . . 13 ((Rel 𝑉 ∧ (1st β€˜π‘§) ∈ (𝑉 β€œ {(1st β€˜π‘Ÿ)})) β†’ (1st β€˜π‘Ÿ)𝑉(1st β€˜π‘§))
6863, 65, 67syl2anc 582 . . . . . . . . . . . 12 ((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ π‘Ÿ ∈ 𝑀) ∧ 𝑧 ∈ ((𝑉 β€œ {(1st β€˜π‘Ÿ)}) Γ— (𝑉 β€œ {(2nd β€˜π‘Ÿ)}))) β†’ (1st β€˜π‘Ÿ)𝑉(1st β€˜π‘§))
69 fvex 6903 . . . . . . . . . . . . . . 15 (1st β€˜π‘§) ∈ V
7037, 69brcnv 5881 . . . . . . . . . . . . . 14 ((1st β€˜π‘Ÿ)◑𝑉(1st β€˜π‘§) ↔ (1st β€˜π‘§)𝑉(1st β€˜π‘Ÿ))
71 breq 5149 . . . . . . . . . . . . . 14 (◑𝑉 = 𝑉 β†’ ((1st β€˜π‘Ÿ)◑𝑉(1st β€˜π‘§) ↔ (1st β€˜π‘Ÿ)𝑉(1st β€˜π‘§)))
7270, 71bitr3id 284 . . . . . . . . . . . . 13 (◑𝑉 = 𝑉 β†’ ((1st β€˜π‘§)𝑉(1st β€˜π‘Ÿ) ↔ (1st β€˜π‘Ÿ)𝑉(1st β€˜π‘§)))
7372biimpar 476 . . . . . . . . . . . 12 ((◑𝑉 = 𝑉 ∧ (1st β€˜π‘Ÿ)𝑉(1st β€˜π‘§)) β†’ (1st β€˜π‘§)𝑉(1st β€˜π‘Ÿ))
7459, 68, 73syl2anc 582 . . . . . . . . . . 11 ((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ π‘Ÿ ∈ 𝑀) ∧ 𝑧 ∈ ((𝑉 β€œ {(1st β€˜π‘Ÿ)}) Γ— (𝑉 β€œ {(2nd β€˜π‘Ÿ)}))) β†’ (1st β€˜π‘§)𝑉(1st β€˜π‘Ÿ))
75 simpll3 1212 . . . . . . . . . . . 12 ((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ π‘Ÿ ∈ 𝑀) ∧ 𝑧 ∈ ((𝑉 β€œ {(1st β€˜π‘Ÿ)}) Γ— (𝑉 β€œ {(2nd β€˜π‘Ÿ)}))) β†’ 𝑀 βŠ† (𝑋 Γ— 𝑋))
76 simplr 765 . . . . . . . . . . . 12 ((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ π‘Ÿ ∈ 𝑀) ∧ 𝑧 ∈ ((𝑉 β€œ {(1st β€˜π‘Ÿ)}) Γ— (𝑉 β€œ {(2nd β€˜π‘Ÿ)}))) β†’ π‘Ÿ ∈ 𝑀)
77 1st2ndbr 8030 . . . . . . . . . . . . 13 ((Rel 𝑀 ∧ π‘Ÿ ∈ 𝑀) β†’ (1st β€˜π‘Ÿ)𝑀(2nd β€˜π‘Ÿ))
7847, 77sylan 578 . . . . . . . . . . . 12 ((𝑀 βŠ† (𝑋 Γ— 𝑋) ∧ π‘Ÿ ∈ 𝑀) β†’ (1st β€˜π‘Ÿ)𝑀(2nd β€˜π‘Ÿ))
7975, 76, 78syl2anc 582 . . . . . . . . . . 11 ((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ π‘Ÿ ∈ 𝑀) ∧ 𝑧 ∈ ((𝑉 β€œ {(1st β€˜π‘Ÿ)}) Γ— (𝑉 β€œ {(2nd β€˜π‘Ÿ)}))) β†’ (1st β€˜π‘Ÿ)𝑀(2nd β€˜π‘Ÿ))
80 xp2nd 8010 . . . . . . . . . . . . 13 (𝑧 ∈ ((𝑉 β€œ {(1st β€˜π‘Ÿ)}) Γ— (𝑉 β€œ {(2nd β€˜π‘Ÿ)})) β†’ (2nd β€˜π‘§) ∈ (𝑉 β€œ {(2nd β€˜π‘Ÿ)}))
8180adantl 480 . . . . . . . . . . . 12 ((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ π‘Ÿ ∈ 𝑀) ∧ 𝑧 ∈ ((𝑉 β€œ {(1st β€˜π‘Ÿ)}) Γ— (𝑉 β€œ {(2nd β€˜π‘Ÿ)}))) β†’ (2nd β€˜π‘§) ∈ (𝑉 β€œ {(2nd β€˜π‘Ÿ)}))
82 elrelimasn 6083 . . . . . . . . . . . . 13 (Rel 𝑉 β†’ ((2nd β€˜π‘§) ∈ (𝑉 β€œ {(2nd β€˜π‘Ÿ)}) ↔ (2nd β€˜π‘Ÿ)𝑉(2nd β€˜π‘§)))
8382biimpa 475 . . . . . . . . . . . 12 ((Rel 𝑉 ∧ (2nd β€˜π‘§) ∈ (𝑉 β€œ {(2nd β€˜π‘Ÿ)})) β†’ (2nd β€˜π‘Ÿ)𝑉(2nd β€˜π‘§))
8463, 81, 83syl2anc 582 . . . . . . . . . . 11 ((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ π‘Ÿ ∈ 𝑀) ∧ 𝑧 ∈ ((𝑉 β€œ {(1st β€˜π‘Ÿ)}) Γ— (𝑉 β€œ {(2nd β€˜π‘Ÿ)}))) β†’ (2nd β€˜π‘Ÿ)𝑉(2nd β€˜π‘§))
8569, 38, 373pm3.2i 1337 . . . . . . . . . . . . 13 ((1st β€˜π‘§) ∈ V ∧ (2nd β€˜π‘Ÿ) ∈ V ∧ (1st β€˜π‘Ÿ) ∈ V)
86 brcogw 5867 . . . . . . . . . . . . 13 ((((1st β€˜π‘§) ∈ V ∧ (2nd β€˜π‘Ÿ) ∈ V ∧ (1st β€˜π‘Ÿ) ∈ V) ∧ ((1st β€˜π‘§)𝑉(1st β€˜π‘Ÿ) ∧ (1st β€˜π‘Ÿ)𝑀(2nd β€˜π‘Ÿ))) β†’ (1st β€˜π‘§)(𝑀 ∘ 𝑉)(2nd β€˜π‘Ÿ))
8785, 86mpan 686 . . . . . . . . . . . 12 (((1st β€˜π‘§)𝑉(1st β€˜π‘Ÿ) ∧ (1st β€˜π‘Ÿ)𝑀(2nd β€˜π‘Ÿ)) β†’ (1st β€˜π‘§)(𝑀 ∘ 𝑉)(2nd β€˜π‘Ÿ))
88 fvex 6903 . . . . . . . . . . . . . 14 (2nd β€˜π‘§) ∈ V
8969, 88, 383pm3.2i 1337 . . . . . . . . . . . . 13 ((1st β€˜π‘§) ∈ V ∧ (2nd β€˜π‘§) ∈ V ∧ (2nd β€˜π‘Ÿ) ∈ V)
90 brcogw 5867 . . . . . . . . . . . . 13 ((((1st β€˜π‘§) ∈ V ∧ (2nd β€˜π‘§) ∈ V ∧ (2nd β€˜π‘Ÿ) ∈ V) ∧ ((1st β€˜π‘§)(𝑀 ∘ 𝑉)(2nd β€˜π‘Ÿ) ∧ (2nd β€˜π‘Ÿ)𝑉(2nd β€˜π‘§))) β†’ (1st β€˜π‘§)(𝑉 ∘ (𝑀 ∘ 𝑉))(2nd β€˜π‘§))
9189, 90mpan 686 . . . . . . . . . . . 12 (((1st β€˜π‘§)(𝑀 ∘ 𝑉)(2nd β€˜π‘Ÿ) ∧ (2nd β€˜π‘Ÿ)𝑉(2nd β€˜π‘§)) β†’ (1st β€˜π‘§)(𝑉 ∘ (𝑀 ∘ 𝑉))(2nd β€˜π‘§))
9287, 91sylan 578 . . . . . . . . . . 11 ((((1st β€˜π‘§)𝑉(1st β€˜π‘Ÿ) ∧ (1st β€˜π‘Ÿ)𝑀(2nd β€˜π‘Ÿ)) ∧ (2nd β€˜π‘Ÿ)𝑉(2nd β€˜π‘§)) β†’ (1st β€˜π‘§)(𝑉 ∘ (𝑀 ∘ 𝑉))(2nd β€˜π‘§))
9374, 79, 84, 92syl21anc 834 . . . . . . . . . 10 ((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ π‘Ÿ ∈ 𝑀) ∧ 𝑧 ∈ ((𝑉 β€œ {(1st β€˜π‘Ÿ)}) Γ— (𝑉 β€œ {(2nd β€˜π‘Ÿ)}))) β†’ (1st β€˜π‘§)(𝑉 ∘ (𝑀 ∘ 𝑉))(2nd β€˜π‘§))
94 df-br 5148 . . . . . . . . . 10 ((1st β€˜π‘§)(𝑉 ∘ (𝑀 ∘ 𝑉))(2nd β€˜π‘§) ↔ ⟨(1st β€˜π‘§), (2nd β€˜π‘§)⟩ ∈ (𝑉 ∘ (𝑀 ∘ 𝑉)))
9593, 94sylib 217 . . . . . . . . 9 ((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ π‘Ÿ ∈ 𝑀) ∧ 𝑧 ∈ ((𝑉 β€œ {(1st β€˜π‘Ÿ)}) Γ— (𝑉 β€œ {(2nd β€˜π‘Ÿ)}))) β†’ ⟨(1st β€˜π‘§), (2nd β€˜π‘§)⟩ ∈ (𝑉 ∘ (𝑀 ∘ 𝑉)))
9657, 95eqeltrd 2831 . . . . . . . 8 ((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ π‘Ÿ ∈ 𝑀) ∧ 𝑧 ∈ ((𝑉 β€œ {(1st β€˜π‘Ÿ)}) Γ— (𝑉 β€œ {(2nd β€˜π‘Ÿ)}))) β†’ 𝑧 ∈ (𝑉 ∘ (𝑀 ∘ 𝑉)))
9796ex 411 . . . . . . 7 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ π‘Ÿ ∈ 𝑀) β†’ (𝑧 ∈ ((𝑉 β€œ {(1st β€˜π‘Ÿ)}) Γ— (𝑉 β€œ {(2nd β€˜π‘Ÿ)})) β†’ 𝑧 ∈ (𝑉 ∘ (𝑀 ∘ 𝑉))))
9897ssrdv 3987 . . . . . 6 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ π‘Ÿ ∈ 𝑀) β†’ ((𝑉 β€œ {(1st β€˜π‘Ÿ)}) Γ— (𝑉 β€œ {(2nd β€˜π‘Ÿ)})) βŠ† (𝑉 ∘ (𝑀 ∘ 𝑉)))
99 simp1 1134 . . . . . . . . . . 11 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) β†’ π‘ˆ ∈ (UnifOnβ€˜π‘‹))
100 simp2l 1197 . . . . . . . . . . 11 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) β†’ 𝑉 ∈ π‘ˆ)
101 ustssxp 23929 . . . . . . . . . . 11 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑉 ∈ π‘ˆ) β†’ 𝑉 βŠ† (𝑋 Γ— 𝑋))
10299, 100, 101syl2anc 582 . . . . . . . . . 10 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) β†’ 𝑉 βŠ† (𝑋 Γ— 𝑋))
103 coss1 5854 . . . . . . . . . 10 (𝑉 βŠ† (𝑋 Γ— 𝑋) β†’ (𝑉 ∘ (𝑀 ∘ 𝑉)) βŠ† ((𝑋 Γ— 𝑋) ∘ (𝑀 ∘ 𝑉)))
104102, 103syl 17 . . . . . . . . 9 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) β†’ (𝑉 ∘ (𝑀 ∘ 𝑉)) βŠ† ((𝑋 Γ— 𝑋) ∘ (𝑀 ∘ 𝑉)))
105 coss1 5854 . . . . . . . . . . . 12 (𝑀 βŠ† (𝑋 Γ— 𝑋) β†’ (𝑀 ∘ 𝑉) βŠ† ((𝑋 Γ— 𝑋) ∘ 𝑉))
10624, 105syl 17 . . . . . . . . . . 11 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) β†’ (𝑀 ∘ 𝑉) βŠ† ((𝑋 Γ— 𝑋) ∘ 𝑉))
107 coss2 5855 . . . . . . . . . . . . 13 (𝑉 βŠ† (𝑋 Γ— 𝑋) β†’ ((𝑋 Γ— 𝑋) ∘ 𝑉) βŠ† ((𝑋 Γ— 𝑋) ∘ (𝑋 Γ— 𝑋)))
108 xpcoid 6288 . . . . . . . . . . . . 13 ((𝑋 Γ— 𝑋) ∘ (𝑋 Γ— 𝑋)) = (𝑋 Γ— 𝑋)
109107, 108sseqtrdi 4031 . . . . . . . . . . . 12 (𝑉 βŠ† (𝑋 Γ— 𝑋) β†’ ((𝑋 Γ— 𝑋) ∘ 𝑉) βŠ† (𝑋 Γ— 𝑋))
110102, 109syl 17 . . . . . . . . . . 11 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) β†’ ((𝑋 Γ— 𝑋) ∘ 𝑉) βŠ† (𝑋 Γ— 𝑋))
111106, 110sstrd 3991 . . . . . . . . . 10 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) β†’ (𝑀 ∘ 𝑉) βŠ† (𝑋 Γ— 𝑋))
112 coss2 5855 . . . . . . . . . . 11 ((𝑀 ∘ 𝑉) βŠ† (𝑋 Γ— 𝑋) β†’ ((𝑋 Γ— 𝑋) ∘ (𝑀 ∘ 𝑉)) βŠ† ((𝑋 Γ— 𝑋) ∘ (𝑋 Γ— 𝑋)))
113112, 108sseqtrdi 4031 . . . . . . . . . 10 ((𝑀 ∘ 𝑉) βŠ† (𝑋 Γ— 𝑋) β†’ ((𝑋 Γ— 𝑋) ∘ (𝑀 ∘ 𝑉)) βŠ† (𝑋 Γ— 𝑋))
114111, 113syl 17 . . . . . . . . 9 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) β†’ ((𝑋 Γ— 𝑋) ∘ (𝑀 ∘ 𝑉)) βŠ† (𝑋 Γ— 𝑋))
115104, 114sstrd 3991 . . . . . . . 8 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) β†’ (𝑉 ∘ (𝑀 ∘ 𝑉)) βŠ† (𝑋 Γ— 𝑋))
116 utopbas 23960 . . . . . . . . . . . 12 (π‘ˆ ∈ (UnifOnβ€˜π‘‹) β†’ 𝑋 = βˆͺ (unifTopβ€˜π‘ˆ))
1171unieqi 4920 . . . . . . . . . . . 12 βˆͺ 𝐽 = βˆͺ (unifTopβ€˜π‘ˆ)
118116, 117eqtr4di 2788 . . . . . . . . . . 11 (π‘ˆ ∈ (UnifOnβ€˜π‘‹) β†’ 𝑋 = βˆͺ 𝐽)
119118sqxpeqd 5707 . . . . . . . . . 10 (π‘ˆ ∈ (UnifOnβ€˜π‘‹) β†’ (𝑋 Γ— 𝑋) = (βˆͺ 𝐽 Γ— βˆͺ 𝐽))
12034, 34txuni 23316 . . . . . . . . . . 11 ((𝐽 ∈ Top ∧ 𝐽 ∈ Top) β†’ (βˆͺ 𝐽 Γ— βˆͺ 𝐽) = βˆͺ (𝐽 Γ—t 𝐽))
1213, 3, 120syl2anc 582 . . . . . . . . . 10 (π‘ˆ ∈ (UnifOnβ€˜π‘‹) β†’ (βˆͺ 𝐽 Γ— βˆͺ 𝐽) = βˆͺ (𝐽 Γ—t 𝐽))
122119, 121eqtrd 2770 . . . . . . . . 9 (π‘ˆ ∈ (UnifOnβ€˜π‘‹) β†’ (𝑋 Γ— 𝑋) = βˆͺ (𝐽 Γ—t 𝐽))
1231223ad2ant1 1131 . . . . . . . 8 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) β†’ (𝑋 Γ— 𝑋) = βˆͺ (𝐽 Γ—t 𝐽))
124115, 123sseqtrd 4021 . . . . . . 7 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) β†’ (𝑉 ∘ (𝑀 ∘ 𝑉)) βŠ† βˆͺ (𝐽 Γ—t 𝐽))
125124adantr 479 . . . . . 6 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ π‘Ÿ ∈ 𝑀) β†’ (𝑉 ∘ (𝑀 ∘ 𝑉)) βŠ† βˆͺ (𝐽 Γ—t 𝐽))
126 eqid 2730 . . . . . . 7 βˆͺ (𝐽 Γ—t 𝐽) = βˆͺ (𝐽 Γ—t 𝐽)
127126ssnei2 22840 . . . . . 6 ((((𝐽 Γ—t 𝐽) ∈ Top ∧ ((𝑉 β€œ {(1st β€˜π‘Ÿ)}) Γ— (𝑉 β€œ {(2nd β€˜π‘Ÿ)})) ∈ ((neiβ€˜(𝐽 Γ—t 𝐽))β€˜{π‘Ÿ})) ∧ (((𝑉 β€œ {(1st β€˜π‘Ÿ)}) Γ— (𝑉 β€œ {(2nd β€˜π‘Ÿ)})) βŠ† (𝑉 ∘ (𝑀 ∘ 𝑉)) ∧ (𝑉 ∘ (𝑀 ∘ 𝑉)) βŠ† βˆͺ (𝐽 Γ—t 𝐽))) β†’ (𝑉 ∘ (𝑀 ∘ 𝑉)) ∈ ((neiβ€˜(𝐽 Γ—t 𝐽))β€˜{π‘Ÿ}))
12820, 53, 98, 125, 127syl22anc 835 . . . . 5 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ π‘Ÿ ∈ 𝑀) β†’ (𝑉 ∘ (𝑀 ∘ 𝑉)) ∈ ((neiβ€˜(𝐽 Γ—t 𝐽))β€˜{π‘Ÿ}))
129128ralrimiva 3144 . . . 4 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) β†’ βˆ€π‘Ÿ ∈ 𝑀 (𝑉 ∘ (𝑀 ∘ 𝑉)) ∈ ((neiβ€˜(𝐽 Γ—t 𝐽))β€˜{π‘Ÿ}))
130129adantr 479 . . 3 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ 𝑀 β‰  βˆ…) β†’ βˆ€π‘Ÿ ∈ 𝑀 (𝑉 ∘ (𝑀 ∘ 𝑉)) ∈ ((neiβ€˜(𝐽 Γ—t 𝐽))β€˜{π‘Ÿ}))
1316adantr 479 . . . 4 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ 𝑀 β‰  βˆ…) β†’ (𝐽 Γ—t 𝐽) ∈ Top)
13224, 123sseqtrd 4021 . . . . 5 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) β†’ 𝑀 βŠ† βˆͺ (𝐽 Γ—t 𝐽))
133132adantr 479 . . . 4 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ 𝑀 β‰  βˆ…) β†’ 𝑀 βŠ† βˆͺ (𝐽 Γ—t 𝐽))
134 simpr 483 . . . 4 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ 𝑀 β‰  βˆ…) β†’ 𝑀 β‰  βˆ…)
135126neips 22837 . . . 4 (((𝐽 Γ—t 𝐽) ∈ Top ∧ 𝑀 βŠ† βˆͺ (𝐽 Γ—t 𝐽) ∧ 𝑀 β‰  βˆ…) β†’ ((𝑉 ∘ (𝑀 ∘ 𝑉)) ∈ ((neiβ€˜(𝐽 Γ—t 𝐽))β€˜π‘€) ↔ βˆ€π‘Ÿ ∈ 𝑀 (𝑉 ∘ (𝑀 ∘ 𝑉)) ∈ ((neiβ€˜(𝐽 Γ—t 𝐽))β€˜{π‘Ÿ})))
136131, 133, 134, 135syl3anc 1369 . . 3 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ 𝑀 β‰  βˆ…) β†’ ((𝑉 ∘ (𝑀 ∘ 𝑉)) ∈ ((neiβ€˜(𝐽 Γ—t 𝐽))β€˜π‘€) ↔ βˆ€π‘Ÿ ∈ 𝑀 (𝑉 ∘ (𝑀 ∘ 𝑉)) ∈ ((neiβ€˜(𝐽 Γ—t 𝐽))β€˜{π‘Ÿ})))
137130, 136mpbird 256 . 2 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ 𝑀 β‰  βˆ…) β†’ (𝑉 ∘ (𝑀 ∘ 𝑉)) ∈ ((neiβ€˜(𝐽 Γ—t 𝐽))β€˜π‘€))
13819, 137pm2.61dane 3027 1 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) β†’ (𝑉 ∘ (𝑀 ∘ 𝑉)) ∈ ((neiβ€˜(𝐽 Γ—t 𝐽))β€˜π‘€))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 394   ∧ w3a 1085   = wceq 1539   ∈ wcel 2104   β‰  wne 2938  βˆ€wral 3059  Vcvv 3472   βŠ† wss 3947  βˆ…c0 4321  {csn 4627  βŸ¨cop 4633  βˆͺ cuni 4907   class class class wbr 5147   Γ— cxp 5673  β—‘ccnv 5674   β€œ cima 5678   ∘ ccom 5679  Rel wrel 5680  β€˜cfv 6542  (class class class)co 7411  1st c1st 7975  2nd c2nd 7976  Topctop 22615  neicnei 22821   Γ—t ctx 23284  UnifOncust 23924  unifTopcutop 23955
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7727
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-ral 3060  df-rex 3069  df-reu 3375  df-rab 3431  df-v 3474  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-int 4950  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-ov 7414  df-oprab 7415  df-mpo 7416  df-om 7858  df-1st 7977  df-2nd 7978  df-1o 8468  df-er 8705  df-en 8942  df-fin 8945  df-fi 9408  df-topgen 17393  df-top 22616  df-topon 22633  df-bases 22669  df-nei 22822  df-tx 23286  df-ust 23925  df-utop 23956
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator