MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  utop2nei Structured version   Visualization version   GIF version
Theorem utop2nei 23737
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 23721 . . . . . . . 8 (π‘ˆ ∈ (UnifOnβ€˜π‘‹) β†’ (unifTopβ€˜π‘ˆ) ∈ Top)
31, 2eqeltrid 2838 . . . . . . 7 (π‘ˆ ∈ (UnifOnβ€˜π‘‹) β†’ 𝐽 ∈ Top)
4 txtop 23055 . . . . . . 7 ((𝐽 ∈ Top ∧ 𝐽 ∈ Top) β†’ (𝐽 Γ—t 𝐽) ∈ Top)
53, 3, 4syl2anc 585 . . . . . 6 (π‘ˆ ∈ (UnifOnβ€˜π‘‹) β†’ (𝐽 Γ—t 𝐽) ∈ Top)
653ad2ant1 1134 . . . . 5 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) β†’ (𝐽 Γ—t 𝐽) ∈ Top)
76adantr 482 . . . 4 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ 𝑀 = βˆ…) β†’ (𝐽 Γ—t 𝐽) ∈ Top)
8 0nei 22614 . . . 4 ((𝐽 Γ—t 𝐽) ∈ Top β†’ βˆ… ∈ ((neiβ€˜(𝐽 Γ—t 𝐽))β€˜βˆ…))
97, 8syl 17 . . 3 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ 𝑀 = βˆ…) β†’ βˆ… ∈ ((neiβ€˜(𝐽 Γ—t 𝐽))β€˜βˆ…))
10 coeq1 5855 . . . . . . 7 (𝑀 = βˆ… β†’ (𝑀 ∘ 𝑉) = (βˆ… ∘ 𝑉))
11 co01 6257 . . . . . . 7 (βˆ… ∘ 𝑉) = βˆ…
1210, 11eqtrdi 2789 . . . . . 6 (𝑀 = βˆ… β†’ (𝑀 ∘ 𝑉) = βˆ…)
1312coeq2d 5860 . . . . 5 (𝑀 = βˆ… β†’ (𝑉 ∘ (𝑀 ∘ 𝑉)) = (𝑉 ∘ βˆ…))
14 co02 6256 . . . . 5 (𝑉 ∘ βˆ…) = βˆ…
1513, 14eqtrdi 2789 . . . 4 (𝑀 = βˆ… β†’ (𝑉 ∘ (𝑀 ∘ 𝑉)) = βˆ…)
1615adantl 483 . . 3 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ 𝑀 = βˆ…) β†’ (𝑉 ∘ (𝑀 ∘ 𝑉)) = βˆ…)
17 simpr 486 . . . 4 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ 𝑀 = βˆ…) β†’ 𝑀 = βˆ…)
1817fveq2d 6892 . . 3 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ 𝑀 = βˆ…) β†’ ((neiβ€˜(𝐽 Γ—t 𝐽))β€˜π‘€) = ((neiβ€˜(𝐽 Γ—t 𝐽))β€˜βˆ…))
199, 16, 183eltr4d 2849 . 2 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ 𝑀 = βˆ…) β†’ (𝑉 ∘ (𝑀 ∘ 𝑉)) ∈ ((neiβ€˜(𝐽 Γ—t 𝐽))β€˜π‘€))
206adantr 482 . . . . . 6 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ π‘Ÿ ∈ 𝑀) β†’ (𝐽 Γ—t 𝐽) ∈ Top)
21 simpl1 1192 . . . . . . . . . 10 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ π‘Ÿ ∈ 𝑀) β†’ π‘ˆ ∈ (UnifOnβ€˜π‘‹))
2221, 3syl 17 . . . . . . . . 9 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ π‘Ÿ ∈ 𝑀) β†’ 𝐽 ∈ Top)
23 simpl2l 1227 . . . . . . . . . 10 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ π‘Ÿ ∈ 𝑀) β†’ 𝑉 ∈ π‘ˆ)
24 simp3 1139 . . . . . . . . . . . 12 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) β†’ 𝑀 βŠ† (𝑋 Γ— 𝑋))
2524sselda 3981 . . . . . . . . . . 11 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ π‘Ÿ ∈ 𝑀) β†’ π‘Ÿ ∈ (𝑋 Γ— 𝑋))
26 xp1st 8002 . . . . . . . . . . 11 (π‘Ÿ ∈ (𝑋 Γ— 𝑋) β†’ (1st β€˜π‘Ÿ) ∈ 𝑋)
2725, 26syl 17 . . . . . . . . . 10 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ π‘Ÿ ∈ 𝑀) β†’ (1st β€˜π‘Ÿ) ∈ 𝑋)
281utopsnnei 23736 . . . . . . . . . 10 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑉 ∈ π‘ˆ ∧ (1st β€˜π‘Ÿ) ∈ 𝑋) β†’ (𝑉 β€œ {(1st β€˜π‘Ÿ)}) ∈ ((neiβ€˜π½)β€˜{(1st β€˜π‘Ÿ)}))
2921, 23, 27, 28syl3anc 1372 . . . . . . . . 9 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ π‘Ÿ ∈ 𝑀) β†’ (𝑉 β€œ {(1st β€˜π‘Ÿ)}) ∈ ((neiβ€˜π½)β€˜{(1st β€˜π‘Ÿ)}))
30 xp2nd 8003 . . . . . . . . . . 11 (π‘Ÿ ∈ (𝑋 Γ— 𝑋) β†’ (2nd β€˜π‘Ÿ) ∈ 𝑋)
3125, 30syl 17 . . . . . . . . . 10 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ π‘Ÿ ∈ 𝑀) β†’ (2nd β€˜π‘Ÿ) ∈ 𝑋)
321utopsnnei 23736 . . . . . . . . . 10 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑉 ∈ π‘ˆ ∧ (2nd β€˜π‘Ÿ) ∈ 𝑋) β†’ (𝑉 β€œ {(2nd β€˜π‘Ÿ)}) ∈ ((neiβ€˜π½)β€˜{(2nd β€˜π‘Ÿ)}))
3321, 23, 31, 32syl3anc 1372 . . . . . . . . 9 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ π‘Ÿ ∈ 𝑀) β†’ (𝑉 β€œ {(2nd β€˜π‘Ÿ)}) ∈ ((neiβ€˜π½)β€˜{(2nd β€˜π‘Ÿ)}))
34 eqid 2733 . . . . . . . . . 10 βˆͺ 𝐽 = βˆͺ 𝐽
3534, 34neitx 23093 . . . . . . . . 9 (((𝐽 ∈ Top ∧ 𝐽 ∈ Top) ∧ ((𝑉 β€œ {(1st β€˜π‘Ÿ)}) ∈ ((neiβ€˜π½)β€˜{(1st β€˜π‘Ÿ)}) ∧ (𝑉 β€œ {(2nd β€˜π‘Ÿ)}) ∈ ((neiβ€˜π½)β€˜{(2nd β€˜π‘Ÿ)}))) β†’ ((𝑉 β€œ {(1st β€˜π‘Ÿ)}) Γ— (𝑉 β€œ {(2nd β€˜π‘Ÿ)})) ∈ ((neiβ€˜(𝐽 Γ—t 𝐽))β€˜({(1st β€˜π‘Ÿ)} Γ— {(2nd β€˜π‘Ÿ)})))
3622, 22, 29, 33, 35syl22anc 838 . . . . . . . 8 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ π‘Ÿ ∈ 𝑀) β†’ ((𝑉 β€œ {(1st β€˜π‘Ÿ)}) Γ— (𝑉 β€œ {(2nd β€˜π‘Ÿ)})) ∈ ((neiβ€˜(𝐽 Γ—t 𝐽))β€˜({(1st β€˜π‘Ÿ)} Γ— {(2nd β€˜π‘Ÿ)})))
37 fvex 6901 . . . . . . . . . 10 (1st β€˜π‘Ÿ) ∈ V
38 fvex 6901 . . . . . . . . . 10 (2nd β€˜π‘Ÿ) ∈ V
3937, 38xpsn 7134 . . . . . . . . 9 ({(1st β€˜π‘Ÿ)} Γ— {(2nd β€˜π‘Ÿ)}) = {⟨(1st β€˜π‘Ÿ), (2nd β€˜π‘Ÿ)⟩}
4039fveq2i 6891 . . . . . . . 8 ((neiβ€˜(𝐽 Γ—t 𝐽))β€˜({(1st β€˜π‘Ÿ)} Γ— {(2nd β€˜π‘Ÿ)})) = ((neiβ€˜(𝐽 Γ—t 𝐽))β€˜{⟨(1st β€˜π‘Ÿ), (2nd β€˜π‘Ÿ)⟩})
4136, 40eleqtrdi 2844 . . . . . . 7 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ π‘Ÿ ∈ 𝑀) β†’ ((𝑉 β€œ {(1st β€˜π‘Ÿ)}) Γ— (𝑉 β€œ {(2nd β€˜π‘Ÿ)})) ∈ ((neiβ€˜(𝐽 Γ—t 𝐽))β€˜{⟨(1st β€˜π‘Ÿ), (2nd β€˜π‘Ÿ)⟩}))
4224adantr 482 . . . . . . . . . . 11 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ π‘Ÿ ∈ 𝑀) β†’ 𝑀 βŠ† (𝑋 Γ— 𝑋))
43 xpss 5691 . . . . . . . . . . . . 13 (𝑋 Γ— 𝑋) βŠ† (V Γ— V)
44 sstr 3989 . . . . . . . . . . . . 13 ((𝑀 βŠ† (𝑋 Γ— 𝑋) ∧ (𝑋 Γ— 𝑋) βŠ† (V Γ— V)) β†’ 𝑀 βŠ† (V Γ— V))
4543, 44mpan2 690 . . . . . . . . . . . 12 (𝑀 βŠ† (𝑋 Γ— 𝑋) β†’ 𝑀 βŠ† (V Γ— V))
46 df-rel 5682 . . . . . . . . . . . 12 (Rel 𝑀 ↔ 𝑀 βŠ† (V Γ— V))
4745, 46sylibr 233 . . . . . . . . . . 11 (𝑀 βŠ† (𝑋 Γ— 𝑋) β†’ Rel 𝑀)
4842, 47syl 17 . . . . . . . . . 10 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ π‘Ÿ ∈ 𝑀) β†’ Rel 𝑀)
49 1st2nd 8020 . . . . . . . . . 10 ((Rel 𝑀 ∧ π‘Ÿ ∈ 𝑀) β†’ π‘Ÿ = ⟨(1st β€˜π‘Ÿ), (2nd β€˜π‘Ÿ)⟩)
5048, 49sylancom 589 . . . . . . . . 9 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ π‘Ÿ ∈ 𝑀) β†’ π‘Ÿ = ⟨(1st β€˜π‘Ÿ), (2nd β€˜π‘Ÿ)⟩)
5150sneqd 4639 . . . . . . . 8 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ π‘Ÿ ∈ 𝑀) β†’ {π‘Ÿ} = {⟨(1st β€˜π‘Ÿ), (2nd β€˜π‘Ÿ)⟩})
5251fveq2d 6892 . . . . . . 7 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ π‘Ÿ ∈ 𝑀) β†’ ((neiβ€˜(𝐽 Γ—t 𝐽))β€˜{π‘Ÿ}) = ((neiβ€˜(𝐽 Γ—t 𝐽))β€˜{⟨(1st β€˜π‘Ÿ), (2nd β€˜π‘Ÿ)⟩}))
5341, 52eleqtrrd 2837 . . . . . 6 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ π‘Ÿ ∈ 𝑀) β†’ ((𝑉 β€œ {(1st β€˜π‘Ÿ)}) Γ— (𝑉 β€œ {(2nd β€˜π‘Ÿ)})) ∈ ((neiβ€˜(𝐽 Γ—t 𝐽))β€˜{π‘Ÿ}))
54 relxp 5693 . . . . . . . . . . 11 Rel ((𝑉 β€œ {(1st β€˜π‘Ÿ)}) Γ— (𝑉 β€œ {(2nd β€˜π‘Ÿ)}))
5554a1i 11 . . . . . . . . . 10 ((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ π‘Ÿ ∈ 𝑀) ∧ 𝑧 ∈ ((𝑉 β€œ {(1st β€˜π‘Ÿ)}) Γ— (𝑉 β€œ {(2nd β€˜π‘Ÿ)}))) β†’ Rel ((𝑉 β€œ {(1st β€˜π‘Ÿ)}) Γ— (𝑉 β€œ {(2nd β€˜π‘Ÿ)})))
56 1st2nd 8020 . . . . . . . . . 10 ((Rel ((𝑉 β€œ {(1st β€˜π‘Ÿ)}) Γ— (𝑉 β€œ {(2nd β€˜π‘Ÿ)})) ∧ 𝑧 ∈ ((𝑉 β€œ {(1st β€˜π‘Ÿ)}) Γ— (𝑉 β€œ {(2nd β€˜π‘Ÿ)}))) β†’ 𝑧 = ⟨(1st β€˜π‘§), (2nd β€˜π‘§)⟩)
5755, 56sylancom 589 . . . . . . . . 9 ((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ π‘Ÿ ∈ 𝑀) ∧ 𝑧 ∈ ((𝑉 β€œ {(1st β€˜π‘Ÿ)}) Γ— (𝑉 β€œ {(2nd β€˜π‘Ÿ)}))) β†’ 𝑧 = ⟨(1st β€˜π‘§), (2nd β€˜π‘§)⟩)
58 simpll2 1214 . . . . . . . . . . . . 13 ((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ π‘Ÿ ∈ 𝑀) ∧ 𝑧 ∈ ((𝑉 β€œ {(1st β€˜π‘Ÿ)}) Γ— (𝑉 β€œ {(2nd β€˜π‘Ÿ)}))) β†’ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉))
5958simprd 497 . . . . . . . . . . . 12 ((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ π‘Ÿ ∈ 𝑀) ∧ 𝑧 ∈ ((𝑉 β€œ {(1st β€˜π‘Ÿ)}) Γ— (𝑉 β€œ {(2nd β€˜π‘Ÿ)}))) β†’ ◑𝑉 = 𝑉)
60 simpll1 1213 . . . . . . . . . . . . . 14 ((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ π‘Ÿ ∈ 𝑀) ∧ 𝑧 ∈ ((𝑉 β€œ {(1st β€˜π‘Ÿ)}) Γ— (𝑉 β€œ {(2nd β€˜π‘Ÿ)}))) β†’ π‘ˆ ∈ (UnifOnβ€˜π‘‹))
6158simpld 496 . . . . . . . . . . . . . 14 ((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ π‘Ÿ ∈ 𝑀) ∧ 𝑧 ∈ ((𝑉 β€œ {(1st β€˜π‘Ÿ)}) Γ— (𝑉 β€œ {(2nd β€˜π‘Ÿ)}))) β†’ 𝑉 ∈ π‘ˆ)
62 ustrel 23698 . . . . . . . . . . . . . 14 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑉 ∈ π‘ˆ) β†’ Rel 𝑉)
6360, 61, 62syl2anc 585 . . . . . . . . . . . . 13 ((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ π‘Ÿ ∈ 𝑀) ∧ 𝑧 ∈ ((𝑉 β€œ {(1st β€˜π‘Ÿ)}) Γ— (𝑉 β€œ {(2nd β€˜π‘Ÿ)}))) β†’ Rel 𝑉)
64 xp1st 8002 . . . . . . . . . . . . . 14 (𝑧 ∈ ((𝑉 β€œ {(1st β€˜π‘Ÿ)}) Γ— (𝑉 β€œ {(2nd β€˜π‘Ÿ)})) β†’ (1st β€˜π‘§) ∈ (𝑉 β€œ {(1st β€˜π‘Ÿ)}))
6564adantl 483 . . . . . . . . . . . . 13 ((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ π‘Ÿ ∈ 𝑀) ∧ 𝑧 ∈ ((𝑉 β€œ {(1st β€˜π‘Ÿ)}) Γ— (𝑉 β€œ {(2nd β€˜π‘Ÿ)}))) β†’ (1st β€˜π‘§) ∈ (𝑉 β€œ {(1st β€˜π‘Ÿ)}))
66 elrelimasn 6081 . . . . . . . . . . . . . 14 (Rel 𝑉 β†’ ((1st β€˜π‘§) ∈ (𝑉 β€œ {(1st β€˜π‘Ÿ)}) ↔ (1st β€˜π‘Ÿ)𝑉(1st β€˜π‘§)))
6766biimpa 478 . . . . . . . . . . . . 13 ((Rel 𝑉 ∧ (1st β€˜π‘§) ∈ (𝑉 β€œ {(1st β€˜π‘Ÿ)})) β†’ (1st β€˜π‘Ÿ)𝑉(1st β€˜π‘§))
6863, 65, 67syl2anc 585 . . . . . . . . . . . 12 ((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ π‘Ÿ ∈ 𝑀) ∧ 𝑧 ∈ ((𝑉 β€œ {(1st β€˜π‘Ÿ)}) Γ— (𝑉 β€œ {(2nd β€˜π‘Ÿ)}))) β†’ (1st β€˜π‘Ÿ)𝑉(1st β€˜π‘§))
69 fvex 6901 . . . . . . . . . . . . . . 15 (1st β€˜π‘§) ∈ V
7037, 69brcnv 5880 . . . . . . . . . . . . . 14 ((1st β€˜π‘Ÿ)◑𝑉(1st β€˜π‘§) ↔ (1st β€˜π‘§)𝑉(1st β€˜π‘Ÿ))
71 breq 5149 . . . . . . . . . . . . . 14 (◑𝑉 = 𝑉 β†’ ((1st β€˜π‘Ÿ)◑𝑉(1st β€˜π‘§) ↔ (1st β€˜π‘Ÿ)𝑉(1st β€˜π‘§)))
7270, 71bitr3id 285 . . . . . . . . . . . . 13 (◑𝑉 = 𝑉 β†’ ((1st β€˜π‘§)𝑉(1st β€˜π‘Ÿ) ↔ (1st β€˜π‘Ÿ)𝑉(1st β€˜π‘§)))
7372biimpar 479 . . . . . . . . . . . 12 ((◑𝑉 = 𝑉 ∧ (1st β€˜π‘Ÿ)𝑉(1st β€˜π‘§)) β†’ (1st β€˜π‘§)𝑉(1st β€˜π‘Ÿ))
7459, 68, 73syl2anc 585 . . . . . . . . . . 11 ((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ π‘Ÿ ∈ 𝑀) ∧ 𝑧 ∈ ((𝑉 β€œ {(1st β€˜π‘Ÿ)}) Γ— (𝑉 β€œ {(2nd β€˜π‘Ÿ)}))) β†’ (1st β€˜π‘§)𝑉(1st β€˜π‘Ÿ))
75 simpll3 1215 . . . . . . . . . . . 12 ((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ π‘Ÿ ∈ 𝑀) ∧ 𝑧 ∈ ((𝑉 β€œ {(1st β€˜π‘Ÿ)}) Γ— (𝑉 β€œ {(2nd β€˜π‘Ÿ)}))) β†’ 𝑀 βŠ† (𝑋 Γ— 𝑋))
76 simplr 768 . . . . . . . . . . . 12 ((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ π‘Ÿ ∈ 𝑀) ∧ 𝑧 ∈ ((𝑉 β€œ {(1st β€˜π‘Ÿ)}) Γ— (𝑉 β€œ {(2nd β€˜π‘Ÿ)}))) β†’ π‘Ÿ ∈ 𝑀)
77 1st2ndbr 8023 . . . . . . . . . . . . 13 ((Rel 𝑀 ∧ π‘Ÿ ∈ 𝑀) β†’ (1st β€˜π‘Ÿ)𝑀(2nd β€˜π‘Ÿ))
7847, 77sylan 581 . . . . . . . . . . . 12 ((𝑀 βŠ† (𝑋 Γ— 𝑋) ∧ π‘Ÿ ∈ 𝑀) β†’ (1st β€˜π‘Ÿ)𝑀(2nd β€˜π‘Ÿ))
7975, 76, 78syl2anc 585 . . . . . . . . . . 11 ((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ π‘Ÿ ∈ 𝑀) ∧ 𝑧 ∈ ((𝑉 β€œ {(1st β€˜π‘Ÿ)}) Γ— (𝑉 β€œ {(2nd β€˜π‘Ÿ)}))) β†’ (1st β€˜π‘Ÿ)𝑀(2nd β€˜π‘Ÿ))
80 xp2nd 8003 . . . . . . . . . . . . 13 (𝑧 ∈ ((𝑉 β€œ {(1st β€˜π‘Ÿ)}) Γ— (𝑉 β€œ {(2nd β€˜π‘Ÿ)})) β†’ (2nd β€˜π‘§) ∈ (𝑉 β€œ {(2nd β€˜π‘Ÿ)}))
8180adantl 483 . . . . . . . . . . . 12 ((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ π‘Ÿ ∈ 𝑀) ∧ 𝑧 ∈ ((𝑉 β€œ {(1st β€˜π‘Ÿ)}) Γ— (𝑉 β€œ {(2nd β€˜π‘Ÿ)}))) β†’ (2nd β€˜π‘§) ∈ (𝑉 β€œ {(2nd β€˜π‘Ÿ)}))
82 elrelimasn 6081 . . . . . . . . . . . . 13 (Rel 𝑉 β†’ ((2nd β€˜π‘§) ∈ (𝑉 β€œ {(2nd β€˜π‘Ÿ)}) ↔ (2nd β€˜π‘Ÿ)𝑉(2nd β€˜π‘§)))
8382biimpa 478 . . . . . . . . . . . 12 ((Rel 𝑉 ∧ (2nd β€˜π‘§) ∈ (𝑉 β€œ {(2nd β€˜π‘Ÿ)})) β†’ (2nd β€˜π‘Ÿ)𝑉(2nd β€˜π‘§))
8463, 81, 83syl2anc 585 . . . . . . . . . . 11 ((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ π‘Ÿ ∈ 𝑀) ∧ 𝑧 ∈ ((𝑉 β€œ {(1st β€˜π‘Ÿ)}) Γ— (𝑉 β€œ {(2nd β€˜π‘Ÿ)}))) β†’ (2nd β€˜π‘Ÿ)𝑉(2nd β€˜π‘§))
8569, 38, 373pm3.2i 1340 . . . . . . . . . . . . 13 ((1st β€˜π‘§) ∈ V ∧ (2nd β€˜π‘Ÿ) ∈ V ∧ (1st β€˜π‘Ÿ) ∈ V)
86 brcogw 5866 . . . . . . . . . . . . 13 ((((1st β€˜π‘§) ∈ V ∧ (2nd β€˜π‘Ÿ) ∈ V ∧ (1st β€˜π‘Ÿ) ∈ V) ∧ ((1st β€˜π‘§)𝑉(1st β€˜π‘Ÿ) ∧ (1st β€˜π‘Ÿ)𝑀(2nd β€˜π‘Ÿ))) β†’ (1st β€˜π‘§)(𝑀 ∘ 𝑉)(2nd β€˜π‘Ÿ))
8785, 86mpan 689 . . . . . . . . . . . 12 (((1st β€˜π‘§)𝑉(1st β€˜π‘Ÿ) ∧ (1st β€˜π‘Ÿ)𝑀(2nd β€˜π‘Ÿ)) β†’ (1st β€˜π‘§)(𝑀 ∘ 𝑉)(2nd β€˜π‘Ÿ))
88 fvex 6901 . . . . . . . . . . . . . 14 (2nd β€˜π‘§) ∈ V
8969, 88, 383pm3.2i 1340 . . . . . . . . . . . . 13 ((1st β€˜π‘§) ∈ V ∧ (2nd β€˜π‘§) ∈ V ∧ (2nd β€˜π‘Ÿ) ∈ V)
90 brcogw 5866 . . . . . . . . . . . . 13 ((((1st β€˜π‘§) ∈ V ∧ (2nd β€˜π‘§) ∈ V ∧ (2nd β€˜π‘Ÿ) ∈ V) ∧ ((1st β€˜π‘§)(𝑀 ∘ 𝑉)(2nd β€˜π‘Ÿ) ∧ (2nd β€˜π‘Ÿ)𝑉(2nd β€˜π‘§))) β†’ (1st β€˜π‘§)(𝑉 ∘ (𝑀 ∘ 𝑉))(2nd β€˜π‘§))
9189, 90mpan 689 . . . . . . . . . . . 12 (((1st β€˜π‘§)(𝑀 ∘ 𝑉)(2nd β€˜π‘Ÿ) ∧ (2nd β€˜π‘Ÿ)𝑉(2nd β€˜π‘§)) β†’ (1st β€˜π‘§)(𝑉 ∘ (𝑀 ∘ 𝑉))(2nd β€˜π‘§))
9287, 91sylan 581 . . . . . . . . . . 11 ((((1st β€˜π‘§)𝑉(1st β€˜π‘Ÿ) ∧ (1st β€˜π‘Ÿ)𝑀(2nd β€˜π‘Ÿ)) ∧ (2nd β€˜π‘Ÿ)𝑉(2nd β€˜π‘§)) β†’ (1st β€˜π‘§)(𝑉 ∘ (𝑀 ∘ 𝑉))(2nd β€˜π‘§))
9374, 79, 84, 92syl21anc 837 . . . . . . . . . 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 2834 . . . . . . . 8 ((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ π‘Ÿ ∈ 𝑀) ∧ 𝑧 ∈ ((𝑉 β€œ {(1st β€˜π‘Ÿ)}) Γ— (𝑉 β€œ {(2nd β€˜π‘Ÿ)}))) β†’ 𝑧 ∈ (𝑉 ∘ (𝑀 ∘ 𝑉)))
9796ex 414 . . . . . . 7 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ π‘Ÿ ∈ 𝑀) β†’ (𝑧 ∈ ((𝑉 β€œ {(1st β€˜π‘Ÿ)}) Γ— (𝑉 β€œ {(2nd β€˜π‘Ÿ)})) β†’ 𝑧 ∈ (𝑉 ∘ (𝑀 ∘ 𝑉))))
9897ssrdv 3987 . . . . . 6 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ π‘Ÿ ∈ 𝑀) β†’ ((𝑉 β€œ {(1st β€˜π‘Ÿ)}) Γ— (𝑉 β€œ {(2nd β€˜π‘Ÿ)})) βŠ† (𝑉 ∘ (𝑀 ∘ 𝑉)))
99 simp1 1137 . . . . . . . . . . 11 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) β†’ π‘ˆ ∈ (UnifOnβ€˜π‘‹))
100 simp2l 1200 . . . . . . . . . . 11 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) β†’ 𝑉 ∈ π‘ˆ)
101 ustssxp 23691 . . . . . . . . . . 11 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑉 ∈ π‘ˆ) β†’ 𝑉 βŠ† (𝑋 Γ— 𝑋))
10299, 100, 101syl2anc 585 . . . . . . . . . 10 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) β†’ 𝑉 βŠ† (𝑋 Γ— 𝑋))
103 coss1 5853 . . . . . . . . . 10 (𝑉 βŠ† (𝑋 Γ— 𝑋) β†’ (𝑉 ∘ (𝑀 ∘ 𝑉)) βŠ† ((𝑋 Γ— 𝑋) ∘ (𝑀 ∘ 𝑉)))
104102, 103syl 17 . . . . . . . . 9 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) β†’ (𝑉 ∘ (𝑀 ∘ 𝑉)) βŠ† ((𝑋 Γ— 𝑋) ∘ (𝑀 ∘ 𝑉)))
105 coss1 5853 . . . . . . . . . . . 12 (𝑀 βŠ† (𝑋 Γ— 𝑋) β†’ (𝑀 ∘ 𝑉) βŠ† ((𝑋 Γ— 𝑋) ∘ 𝑉))
10624, 105syl 17 . . . . . . . . . . 11 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) β†’ (𝑀 ∘ 𝑉) βŠ† ((𝑋 Γ— 𝑋) ∘ 𝑉))
107 coss2 5854 . . . . . . . . . . . . 13 (𝑉 βŠ† (𝑋 Γ— 𝑋) β†’ ((𝑋 Γ— 𝑋) ∘ 𝑉) βŠ† ((𝑋 Γ— 𝑋) ∘ (𝑋 Γ— 𝑋)))
108 xpcoid 6286 . . . . . . . . . . . . 13 ((𝑋 Γ— 𝑋) ∘ (𝑋 Γ— 𝑋)) = (𝑋 Γ— 𝑋)
109107, 108sseqtrdi 4031 . . . . . . . . . . . 12 (𝑉 βŠ† (𝑋 Γ— 𝑋) β†’ ((𝑋 Γ— 𝑋) ∘ 𝑉) βŠ† (𝑋 Γ— 𝑋))
110102, 109syl 17 . . . . . . . . . . 11 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) β†’ ((𝑋 Γ— 𝑋) ∘ 𝑉) βŠ† (𝑋 Γ— 𝑋))
111106, 110sstrd 3991 . . . . . . . . . 10 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) β†’ (𝑀 ∘ 𝑉) βŠ† (𝑋 Γ— 𝑋))
112 coss2 5854 . . . . . . . . . . 11 ((𝑀 ∘ 𝑉) βŠ† (𝑋 Γ— 𝑋) β†’ ((𝑋 Γ— 𝑋) ∘ (𝑀 ∘ 𝑉)) βŠ† ((𝑋 Γ— 𝑋) ∘ (𝑋 Γ— 𝑋)))
113112, 108sseqtrdi 4031 . . . . . . . . . 10 ((𝑀 ∘ 𝑉) βŠ† (𝑋 Γ— 𝑋) β†’ ((𝑋 Γ— 𝑋) ∘ (𝑀 ∘ 𝑉)) βŠ† (𝑋 Γ— 𝑋))
114111, 113syl 17 . . . . . . . . 9 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) β†’ ((𝑋 Γ— 𝑋) ∘ (𝑀 ∘ 𝑉)) βŠ† (𝑋 Γ— 𝑋))
115104, 114sstrd 3991 . . . . . . . 8 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) β†’ (𝑉 ∘ (𝑀 ∘ 𝑉)) βŠ† (𝑋 Γ— 𝑋))
116 utopbas 23722 . . . . . . . . . . . 12 (π‘ˆ ∈ (UnifOnβ€˜π‘‹) β†’ 𝑋 = βˆͺ (unifTopβ€˜π‘ˆ))
1171unieqi 4920 . . . . . . . . . . . 12 βˆͺ 𝐽 = βˆͺ (unifTopβ€˜π‘ˆ)
118116, 117eqtr4di 2791 . . . . . . . . . . 11 (π‘ˆ ∈ (UnifOnβ€˜π‘‹) β†’ 𝑋 = βˆͺ 𝐽)
119118sqxpeqd 5707 . . . . . . . . . 10 (π‘ˆ ∈ (UnifOnβ€˜π‘‹) β†’ (𝑋 Γ— 𝑋) = (βˆͺ 𝐽 Γ— βˆͺ 𝐽))
12034, 34txuni 23078 . . . . . . . . . . 11 ((𝐽 ∈ Top ∧ 𝐽 ∈ Top) β†’ (βˆͺ 𝐽 Γ— βˆͺ 𝐽) = βˆͺ (𝐽 Γ—t 𝐽))
1213, 3, 120syl2anc 585 . . . . . . . . . 10 (π‘ˆ ∈ (UnifOnβ€˜π‘‹) β†’ (βˆͺ 𝐽 Γ— βˆͺ 𝐽) = βˆͺ (𝐽 Γ—t 𝐽))
122119, 121eqtrd 2773 . . . . . . . . 9 (π‘ˆ ∈ (UnifOnβ€˜π‘‹) β†’ (𝑋 Γ— 𝑋) = βˆͺ (𝐽 Γ—t 𝐽))
1231223ad2ant1 1134 . . . . . . . 8 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) β†’ (𝑋 Γ— 𝑋) = βˆͺ (𝐽 Γ—t 𝐽))
124115, 123sseqtrd 4021 . . . . . . 7 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) β†’ (𝑉 ∘ (𝑀 ∘ 𝑉)) βŠ† βˆͺ (𝐽 Γ—t 𝐽))
125124adantr 482 . . . . . 6 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ π‘Ÿ ∈ 𝑀) β†’ (𝑉 ∘ (𝑀 ∘ 𝑉)) βŠ† βˆͺ (𝐽 Γ—t 𝐽))
126 eqid 2733 . . . . . . 7 βˆͺ (𝐽 Γ—t 𝐽) = βˆͺ (𝐽 Γ—t 𝐽)
127126ssnei2 22602 . . . . . 6 ((((𝐽 Γ—t 𝐽) ∈ Top ∧ ((𝑉 β€œ {(1st β€˜π‘Ÿ)}) Γ— (𝑉 β€œ {(2nd β€˜π‘Ÿ)})) ∈ ((neiβ€˜(𝐽 Γ—t 𝐽))β€˜{π‘Ÿ})) ∧ (((𝑉 β€œ {(1st β€˜π‘Ÿ)}) Γ— (𝑉 β€œ {(2nd β€˜π‘Ÿ)})) βŠ† (𝑉 ∘ (𝑀 ∘ 𝑉)) ∧ (𝑉 ∘ (𝑀 ∘ 𝑉)) βŠ† βˆͺ (𝐽 Γ—t 𝐽))) β†’ (𝑉 ∘ (𝑀 ∘ 𝑉)) ∈ ((neiβ€˜(𝐽 Γ—t 𝐽))β€˜{π‘Ÿ}))
12820, 53, 98, 125, 127syl22anc 838 . . . . 5 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ π‘Ÿ ∈ 𝑀) β†’ (𝑉 ∘ (𝑀 ∘ 𝑉)) ∈ ((neiβ€˜(𝐽 Γ—t 𝐽))β€˜{π‘Ÿ}))
129128ralrimiva 3147 . . . 4 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) β†’ βˆ€π‘Ÿ ∈ 𝑀 (𝑉 ∘ (𝑀 ∘ 𝑉)) ∈ ((neiβ€˜(𝐽 Γ—t 𝐽))β€˜{π‘Ÿ}))
130129adantr 482 . . 3 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ 𝑀 β‰  βˆ…) β†’ βˆ€π‘Ÿ ∈ 𝑀 (𝑉 ∘ (𝑀 ∘ 𝑉)) ∈ ((neiβ€˜(𝐽 Γ—t 𝐽))β€˜{π‘Ÿ}))
1316adantr 482 . . . 4 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ 𝑀 β‰  βˆ…) β†’ (𝐽 Γ—t 𝐽) ∈ Top)
13224, 123sseqtrd 4021 . . . . 5 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) β†’ 𝑀 βŠ† βˆͺ (𝐽 Γ—t 𝐽))
133132adantr 482 . . . 4 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ 𝑀 β‰  βˆ…) β†’ 𝑀 βŠ† βˆͺ (𝐽 Γ—t 𝐽))
134 simpr 486 . . . 4 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ 𝑀 β‰  βˆ…) β†’ 𝑀 β‰  βˆ…)
135126neips 22599 . . . 4 (((𝐽 Γ—t 𝐽) ∈ Top ∧ 𝑀 βŠ† βˆͺ (𝐽 Γ—t 𝐽) ∧ 𝑀 β‰  βˆ…) β†’ ((𝑉 ∘ (𝑀 ∘ 𝑉)) ∈ ((neiβ€˜(𝐽 Γ—t 𝐽))β€˜π‘€) ↔ βˆ€π‘Ÿ ∈ 𝑀 (𝑉 ∘ (𝑀 ∘ 𝑉)) ∈ ((neiβ€˜(𝐽 Γ—t 𝐽))β€˜{π‘Ÿ})))
136131, 133, 134, 135syl3anc 1372 . . 3 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ 𝑀 β‰  βˆ…) β†’ ((𝑉 ∘ (𝑀 ∘ 𝑉)) ∈ ((neiβ€˜(𝐽 Γ—t 𝐽))β€˜π‘€) ↔ βˆ€π‘Ÿ ∈ 𝑀 (𝑉 ∘ (𝑀 ∘ 𝑉)) ∈ ((neiβ€˜(𝐽 Γ—t 𝐽))β€˜{π‘Ÿ})))
137130, 136mpbird 257 . 2 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ 𝑀 β‰  βˆ…) β†’ (𝑉 ∘ (𝑀 ∘ 𝑉)) ∈ ((neiβ€˜(𝐽 Γ—t 𝐽))β€˜π‘€))
13819, 137pm2.61dane 3030 1 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) β†’ (𝑉 ∘ (𝑀 ∘ 𝑉)) ∈ ((neiβ€˜(𝐽 Γ—t 𝐽))β€˜π‘€))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 397   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107   β‰  wne 2941  βˆ€wral 3062  Vcvv 3475   βŠ† 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 6540  (class class class)co 7404  1st c1st 7968  2nd c2nd 7969  Topctop 22377  neicnei 22583   Γ—t ctx 23046  UnifOncust 23686  unifTopcutop 23717
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 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7720
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 2942  df-ral 3063  df-rex 3072  df-reu 3378  df-rab 3434  df-v 3477  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 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-ov 7407  df-oprab 7408  df-mpo 7409  df-om 7851  df-1st 7970  df-2nd 7971  df-1o 8461  df-er 8699  df-en 8936  df-fin 8939  df-fi 9402  df-topgen 17385  df-top 22378  df-topon 22395  df-bases 22431  df-nei 22584  df-tx 23048  df-ust 23687  df-utop 23718
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator