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

Theorem utop2nei 24076
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 24060 . . . . . . . 8 (π‘ˆ ∈ (UnifOnβ€˜π‘‹) β†’ (unifTopβ€˜π‘ˆ) ∈ Top)
31, 2eqeltrid 2829 . . . . . . 7 (π‘ˆ ∈ (UnifOnβ€˜π‘‹) β†’ 𝐽 ∈ Top)
4 txtop 23394 . . . . . . 7 ((𝐽 ∈ Top ∧ 𝐽 ∈ Top) β†’ (𝐽 Γ—t 𝐽) ∈ Top)
53, 3, 4syl2anc 583 . . . . . 6 (π‘ˆ ∈ (UnifOnβ€˜π‘‹) β†’ (𝐽 Γ—t 𝐽) ∈ Top)
653ad2ant1 1130 . . . . 5 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) β†’ (𝐽 Γ—t 𝐽) ∈ Top)
76adantr 480 . . . 4 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ 𝑀 = βˆ…) β†’ (𝐽 Γ—t 𝐽) ∈ Top)
8 0nei 22953 . . . 4 ((𝐽 Γ—t 𝐽) ∈ Top β†’ βˆ… ∈ ((neiβ€˜(𝐽 Γ—t 𝐽))β€˜βˆ…))
97, 8syl 17 . . 3 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ 𝑀 = βˆ…) β†’ βˆ… ∈ ((neiβ€˜(𝐽 Γ—t 𝐽))β€˜βˆ…))
10 coeq1 5847 . . . . . . 7 (𝑀 = βˆ… β†’ (𝑀 ∘ 𝑉) = (βˆ… ∘ 𝑉))
11 co01 6250 . . . . . . 7 (βˆ… ∘ 𝑉) = βˆ…
1210, 11eqtrdi 2780 . . . . . 6 (𝑀 = βˆ… β†’ (𝑀 ∘ 𝑉) = βˆ…)
1312coeq2d 5852 . . . . 5 (𝑀 = βˆ… β†’ (𝑉 ∘ (𝑀 ∘ 𝑉)) = (𝑉 ∘ βˆ…))
14 co02 6249 . . . . 5 (𝑉 ∘ βˆ…) = βˆ…
1513, 14eqtrdi 2780 . . . 4 (𝑀 = βˆ… β†’ (𝑉 ∘ (𝑀 ∘ 𝑉)) = βˆ…)
1615adantl 481 . . 3 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ 𝑀 = βˆ…) β†’ (𝑉 ∘ (𝑀 ∘ 𝑉)) = βˆ…)
17 simpr 484 . . . 4 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ 𝑀 = βˆ…) β†’ 𝑀 = βˆ…)
1817fveq2d 6885 . . 3 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ 𝑀 = βˆ…) β†’ ((neiβ€˜(𝐽 Γ—t 𝐽))β€˜π‘€) = ((neiβ€˜(𝐽 Γ—t 𝐽))β€˜βˆ…))
199, 16, 183eltr4d 2840 . 2 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ 𝑀 = βˆ…) β†’ (𝑉 ∘ (𝑀 ∘ 𝑉)) ∈ ((neiβ€˜(𝐽 Γ—t 𝐽))β€˜π‘€))
206adantr 480 . . . . . 6 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ π‘Ÿ ∈ 𝑀) β†’ (𝐽 Γ—t 𝐽) ∈ Top)
21 simpl1 1188 . . . . . . . . . 10 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ π‘Ÿ ∈ 𝑀) β†’ π‘ˆ ∈ (UnifOnβ€˜π‘‹))
2221, 3syl 17 . . . . . . . . 9 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ π‘Ÿ ∈ 𝑀) β†’ 𝐽 ∈ Top)
23 simpl2l 1223 . . . . . . . . . 10 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ π‘Ÿ ∈ 𝑀) β†’ 𝑉 ∈ π‘ˆ)
24 simp3 1135 . . . . . . . . . . . 12 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) β†’ 𝑀 βŠ† (𝑋 Γ— 𝑋))
2524sselda 3974 . . . . . . . . . . 11 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ π‘Ÿ ∈ 𝑀) β†’ π‘Ÿ ∈ (𝑋 Γ— 𝑋))
26 xp1st 8000 . . . . . . . . . . 11 (π‘Ÿ ∈ (𝑋 Γ— 𝑋) β†’ (1st β€˜π‘Ÿ) ∈ 𝑋)
2725, 26syl 17 . . . . . . . . . 10 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ π‘Ÿ ∈ 𝑀) β†’ (1st β€˜π‘Ÿ) ∈ 𝑋)
281utopsnnei 24075 . . . . . . . . . 10 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑉 ∈ π‘ˆ ∧ (1st β€˜π‘Ÿ) ∈ 𝑋) β†’ (𝑉 β€œ {(1st β€˜π‘Ÿ)}) ∈ ((neiβ€˜π½)β€˜{(1st β€˜π‘Ÿ)}))
2921, 23, 27, 28syl3anc 1368 . . . . . . . . 9 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ π‘Ÿ ∈ 𝑀) β†’ (𝑉 β€œ {(1st β€˜π‘Ÿ)}) ∈ ((neiβ€˜π½)β€˜{(1st β€˜π‘Ÿ)}))
30 xp2nd 8001 . . . . . . . . . . 11 (π‘Ÿ ∈ (𝑋 Γ— 𝑋) β†’ (2nd β€˜π‘Ÿ) ∈ 𝑋)
3125, 30syl 17 . . . . . . . . . 10 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ π‘Ÿ ∈ 𝑀) β†’ (2nd β€˜π‘Ÿ) ∈ 𝑋)
321utopsnnei 24075 . . . . . . . . . 10 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑉 ∈ π‘ˆ ∧ (2nd β€˜π‘Ÿ) ∈ 𝑋) β†’ (𝑉 β€œ {(2nd β€˜π‘Ÿ)}) ∈ ((neiβ€˜π½)β€˜{(2nd β€˜π‘Ÿ)}))
3321, 23, 31, 32syl3anc 1368 . . . . . . . . 9 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ π‘Ÿ ∈ 𝑀) β†’ (𝑉 β€œ {(2nd β€˜π‘Ÿ)}) ∈ ((neiβ€˜π½)β€˜{(2nd β€˜π‘Ÿ)}))
34 eqid 2724 . . . . . . . . . 10 βˆͺ 𝐽 = βˆͺ 𝐽
3534, 34neitx 23432 . . . . . . . . 9 (((𝐽 ∈ Top ∧ 𝐽 ∈ Top) ∧ ((𝑉 β€œ {(1st β€˜π‘Ÿ)}) ∈ ((neiβ€˜π½)β€˜{(1st β€˜π‘Ÿ)}) ∧ (𝑉 β€œ {(2nd β€˜π‘Ÿ)}) ∈ ((neiβ€˜π½)β€˜{(2nd β€˜π‘Ÿ)}))) β†’ ((𝑉 β€œ {(1st β€˜π‘Ÿ)}) Γ— (𝑉 β€œ {(2nd β€˜π‘Ÿ)})) ∈ ((neiβ€˜(𝐽 Γ—t 𝐽))β€˜({(1st β€˜π‘Ÿ)} Γ— {(2nd β€˜π‘Ÿ)})))
3622, 22, 29, 33, 35syl22anc 836 . . . . . . . 8 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ π‘Ÿ ∈ 𝑀) β†’ ((𝑉 β€œ {(1st β€˜π‘Ÿ)}) Γ— (𝑉 β€œ {(2nd β€˜π‘Ÿ)})) ∈ ((neiβ€˜(𝐽 Γ—t 𝐽))β€˜({(1st β€˜π‘Ÿ)} Γ— {(2nd β€˜π‘Ÿ)})))
37 fvex 6894 . . . . . . . . . 10 (1st β€˜π‘Ÿ) ∈ V
38 fvex 6894 . . . . . . . . . 10 (2nd β€˜π‘Ÿ) ∈ V
3937, 38xpsn 7131 . . . . . . . . 9 ({(1st β€˜π‘Ÿ)} Γ— {(2nd β€˜π‘Ÿ)}) = {⟨(1st β€˜π‘Ÿ), (2nd β€˜π‘Ÿ)⟩}
4039fveq2i 6884 . . . . . . . 8 ((neiβ€˜(𝐽 Γ—t 𝐽))β€˜({(1st β€˜π‘Ÿ)} Γ— {(2nd β€˜π‘Ÿ)})) = ((neiβ€˜(𝐽 Γ—t 𝐽))β€˜{⟨(1st β€˜π‘Ÿ), (2nd β€˜π‘Ÿ)⟩})
4136, 40eleqtrdi 2835 . . . . . . 7 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ π‘Ÿ ∈ 𝑀) β†’ ((𝑉 β€œ {(1st β€˜π‘Ÿ)}) Γ— (𝑉 β€œ {(2nd β€˜π‘Ÿ)})) ∈ ((neiβ€˜(𝐽 Γ—t 𝐽))β€˜{⟨(1st β€˜π‘Ÿ), (2nd β€˜π‘Ÿ)⟩}))
4224adantr 480 . . . . . . . . . . 11 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ π‘Ÿ ∈ 𝑀) β†’ 𝑀 βŠ† (𝑋 Γ— 𝑋))
43 xpss 5682 . . . . . . . . . . . . 13 (𝑋 Γ— 𝑋) βŠ† (V Γ— V)
44 sstr 3982 . . . . . . . . . . . . 13 ((𝑀 βŠ† (𝑋 Γ— 𝑋) ∧ (𝑋 Γ— 𝑋) βŠ† (V Γ— V)) β†’ 𝑀 βŠ† (V Γ— V))
4543, 44mpan2 688 . . . . . . . . . . . 12 (𝑀 βŠ† (𝑋 Γ— 𝑋) β†’ 𝑀 βŠ† (V Γ— V))
46 df-rel 5673 . . . . . . . . . . . 12 (Rel 𝑀 ↔ 𝑀 βŠ† (V Γ— V))
4745, 46sylibr 233 . . . . . . . . . . 11 (𝑀 βŠ† (𝑋 Γ— 𝑋) β†’ Rel 𝑀)
4842, 47syl 17 . . . . . . . . . 10 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ π‘Ÿ ∈ 𝑀) β†’ Rel 𝑀)
49 1st2nd 8018 . . . . . . . . . 10 ((Rel 𝑀 ∧ π‘Ÿ ∈ 𝑀) β†’ π‘Ÿ = ⟨(1st β€˜π‘Ÿ), (2nd β€˜π‘Ÿ)⟩)
5048, 49sylancom 587 . . . . . . . . 9 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ π‘Ÿ ∈ 𝑀) β†’ π‘Ÿ = ⟨(1st β€˜π‘Ÿ), (2nd β€˜π‘Ÿ)⟩)
5150sneqd 4632 . . . . . . . 8 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ π‘Ÿ ∈ 𝑀) β†’ {π‘Ÿ} = {⟨(1st β€˜π‘Ÿ), (2nd β€˜π‘Ÿ)⟩})
5251fveq2d 6885 . . . . . . 7 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ π‘Ÿ ∈ 𝑀) β†’ ((neiβ€˜(𝐽 Γ—t 𝐽))β€˜{π‘Ÿ}) = ((neiβ€˜(𝐽 Γ—t 𝐽))β€˜{⟨(1st β€˜π‘Ÿ), (2nd β€˜π‘Ÿ)⟩}))
5341, 52eleqtrrd 2828 . . . . . 6 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ π‘Ÿ ∈ 𝑀) β†’ ((𝑉 β€œ {(1st β€˜π‘Ÿ)}) Γ— (𝑉 β€œ {(2nd β€˜π‘Ÿ)})) ∈ ((neiβ€˜(𝐽 Γ—t 𝐽))β€˜{π‘Ÿ}))
54 relxp 5684 . . . . . . . . . . 11 Rel ((𝑉 β€œ {(1st β€˜π‘Ÿ)}) Γ— (𝑉 β€œ {(2nd β€˜π‘Ÿ)}))
5554a1i 11 . . . . . . . . . 10 ((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ π‘Ÿ ∈ 𝑀) ∧ 𝑧 ∈ ((𝑉 β€œ {(1st β€˜π‘Ÿ)}) Γ— (𝑉 β€œ {(2nd β€˜π‘Ÿ)}))) β†’ Rel ((𝑉 β€œ {(1st β€˜π‘Ÿ)}) Γ— (𝑉 β€œ {(2nd β€˜π‘Ÿ)})))
56 1st2nd 8018 . . . . . . . . . 10 ((Rel ((𝑉 β€œ {(1st β€˜π‘Ÿ)}) Γ— (𝑉 β€œ {(2nd β€˜π‘Ÿ)})) ∧ 𝑧 ∈ ((𝑉 β€œ {(1st β€˜π‘Ÿ)}) Γ— (𝑉 β€œ {(2nd β€˜π‘Ÿ)}))) β†’ 𝑧 = ⟨(1st β€˜π‘§), (2nd β€˜π‘§)⟩)
5755, 56sylancom 587 . . . . . . . . 9 ((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ π‘Ÿ ∈ 𝑀) ∧ 𝑧 ∈ ((𝑉 β€œ {(1st β€˜π‘Ÿ)}) Γ— (𝑉 β€œ {(2nd β€˜π‘Ÿ)}))) β†’ 𝑧 = ⟨(1st β€˜π‘§), (2nd β€˜π‘§)⟩)
58 simpll2 1210 . . . . . . . . . . . . 13 ((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ π‘Ÿ ∈ 𝑀) ∧ 𝑧 ∈ ((𝑉 β€œ {(1st β€˜π‘Ÿ)}) Γ— (𝑉 β€œ {(2nd β€˜π‘Ÿ)}))) β†’ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉))
5958simprd 495 . . . . . . . . . . . 12 ((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ π‘Ÿ ∈ 𝑀) ∧ 𝑧 ∈ ((𝑉 β€œ {(1st β€˜π‘Ÿ)}) Γ— (𝑉 β€œ {(2nd β€˜π‘Ÿ)}))) β†’ ◑𝑉 = 𝑉)
60 simpll1 1209 . . . . . . . . . . . . . 14 ((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ π‘Ÿ ∈ 𝑀) ∧ 𝑧 ∈ ((𝑉 β€œ {(1st β€˜π‘Ÿ)}) Γ— (𝑉 β€œ {(2nd β€˜π‘Ÿ)}))) β†’ π‘ˆ ∈ (UnifOnβ€˜π‘‹))
6158simpld 494 . . . . . . . . . . . . . 14 ((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ π‘Ÿ ∈ 𝑀) ∧ 𝑧 ∈ ((𝑉 β€œ {(1st β€˜π‘Ÿ)}) Γ— (𝑉 β€œ {(2nd β€˜π‘Ÿ)}))) β†’ 𝑉 ∈ π‘ˆ)
62 ustrel 24037 . . . . . . . . . . . . . 14 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑉 ∈ π‘ˆ) β†’ Rel 𝑉)
6360, 61, 62syl2anc 583 . . . . . . . . . . . . 13 ((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ π‘Ÿ ∈ 𝑀) ∧ 𝑧 ∈ ((𝑉 β€œ {(1st β€˜π‘Ÿ)}) Γ— (𝑉 β€œ {(2nd β€˜π‘Ÿ)}))) β†’ Rel 𝑉)
64 xp1st 8000 . . . . . . . . . . . . . 14 (𝑧 ∈ ((𝑉 β€œ {(1st β€˜π‘Ÿ)}) Γ— (𝑉 β€œ {(2nd β€˜π‘Ÿ)})) β†’ (1st β€˜π‘§) ∈ (𝑉 β€œ {(1st β€˜π‘Ÿ)}))
6564adantl 481 . . . . . . . . . . . . 13 ((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ π‘Ÿ ∈ 𝑀) ∧ 𝑧 ∈ ((𝑉 β€œ {(1st β€˜π‘Ÿ)}) Γ— (𝑉 β€œ {(2nd β€˜π‘Ÿ)}))) β†’ (1st β€˜π‘§) ∈ (𝑉 β€œ {(1st β€˜π‘Ÿ)}))
66 elrelimasn 6074 . . . . . . . . . . . . . 14 (Rel 𝑉 β†’ ((1st β€˜π‘§) ∈ (𝑉 β€œ {(1st β€˜π‘Ÿ)}) ↔ (1st β€˜π‘Ÿ)𝑉(1st β€˜π‘§)))
6766biimpa 476 . . . . . . . . . . . . 13 ((Rel 𝑉 ∧ (1st β€˜π‘§) ∈ (𝑉 β€œ {(1st β€˜π‘Ÿ)})) β†’ (1st β€˜π‘Ÿ)𝑉(1st β€˜π‘§))
6863, 65, 67syl2anc 583 . . . . . . . . . . . 12 ((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ π‘Ÿ ∈ 𝑀) ∧ 𝑧 ∈ ((𝑉 β€œ {(1st β€˜π‘Ÿ)}) Γ— (𝑉 β€œ {(2nd β€˜π‘Ÿ)}))) β†’ (1st β€˜π‘Ÿ)𝑉(1st β€˜π‘§))
69 fvex 6894 . . . . . . . . . . . . . . 15 (1st β€˜π‘§) ∈ V
7037, 69brcnv 5872 . . . . . . . . . . . . . 14 ((1st β€˜π‘Ÿ)◑𝑉(1st β€˜π‘§) ↔ (1st β€˜π‘§)𝑉(1st β€˜π‘Ÿ))
71 breq 5140 . . . . . . . . . . . . . 14 (◑𝑉 = 𝑉 β†’ ((1st β€˜π‘Ÿ)◑𝑉(1st β€˜π‘§) ↔ (1st β€˜π‘Ÿ)𝑉(1st β€˜π‘§)))
7270, 71bitr3id 285 . . . . . . . . . . . . 13 (◑𝑉 = 𝑉 β†’ ((1st β€˜π‘§)𝑉(1st β€˜π‘Ÿ) ↔ (1st β€˜π‘Ÿ)𝑉(1st β€˜π‘§)))
7372biimpar 477 . . . . . . . . . . . 12 ((◑𝑉 = 𝑉 ∧ (1st β€˜π‘Ÿ)𝑉(1st β€˜π‘§)) β†’ (1st β€˜π‘§)𝑉(1st β€˜π‘Ÿ))
7459, 68, 73syl2anc 583 . . . . . . . . . . 11 ((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ π‘Ÿ ∈ 𝑀) ∧ 𝑧 ∈ ((𝑉 β€œ {(1st β€˜π‘Ÿ)}) Γ— (𝑉 β€œ {(2nd β€˜π‘Ÿ)}))) β†’ (1st β€˜π‘§)𝑉(1st β€˜π‘Ÿ))
75 simpll3 1211 . . . . . . . . . . . 12 ((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ π‘Ÿ ∈ 𝑀) ∧ 𝑧 ∈ ((𝑉 β€œ {(1st β€˜π‘Ÿ)}) Γ— (𝑉 β€œ {(2nd β€˜π‘Ÿ)}))) β†’ 𝑀 βŠ† (𝑋 Γ— 𝑋))
76 simplr 766 . . . . . . . . . . . 12 ((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ π‘Ÿ ∈ 𝑀) ∧ 𝑧 ∈ ((𝑉 β€œ {(1st β€˜π‘Ÿ)}) Γ— (𝑉 β€œ {(2nd β€˜π‘Ÿ)}))) β†’ π‘Ÿ ∈ 𝑀)
77 1st2ndbr 8021 . . . . . . . . . . . . 13 ((Rel 𝑀 ∧ π‘Ÿ ∈ 𝑀) β†’ (1st β€˜π‘Ÿ)𝑀(2nd β€˜π‘Ÿ))
7847, 77sylan 579 . . . . . . . . . . . 12 ((𝑀 βŠ† (𝑋 Γ— 𝑋) ∧ π‘Ÿ ∈ 𝑀) β†’ (1st β€˜π‘Ÿ)𝑀(2nd β€˜π‘Ÿ))
7975, 76, 78syl2anc 583 . . . . . . . . . . 11 ((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ π‘Ÿ ∈ 𝑀) ∧ 𝑧 ∈ ((𝑉 β€œ {(1st β€˜π‘Ÿ)}) Γ— (𝑉 β€œ {(2nd β€˜π‘Ÿ)}))) β†’ (1st β€˜π‘Ÿ)𝑀(2nd β€˜π‘Ÿ))
80 xp2nd 8001 . . . . . . . . . . . . 13 (𝑧 ∈ ((𝑉 β€œ {(1st β€˜π‘Ÿ)}) Γ— (𝑉 β€œ {(2nd β€˜π‘Ÿ)})) β†’ (2nd β€˜π‘§) ∈ (𝑉 β€œ {(2nd β€˜π‘Ÿ)}))
8180adantl 481 . . . . . . . . . . . 12 ((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ π‘Ÿ ∈ 𝑀) ∧ 𝑧 ∈ ((𝑉 β€œ {(1st β€˜π‘Ÿ)}) Γ— (𝑉 β€œ {(2nd β€˜π‘Ÿ)}))) β†’ (2nd β€˜π‘§) ∈ (𝑉 β€œ {(2nd β€˜π‘Ÿ)}))
82 elrelimasn 6074 . . . . . . . . . . . . 13 (Rel 𝑉 β†’ ((2nd β€˜π‘§) ∈ (𝑉 β€œ {(2nd β€˜π‘Ÿ)}) ↔ (2nd β€˜π‘Ÿ)𝑉(2nd β€˜π‘§)))
8382biimpa 476 . . . . . . . . . . . 12 ((Rel 𝑉 ∧ (2nd β€˜π‘§) ∈ (𝑉 β€œ {(2nd β€˜π‘Ÿ)})) β†’ (2nd β€˜π‘Ÿ)𝑉(2nd β€˜π‘§))
8463, 81, 83syl2anc 583 . . . . . . . . . . 11 ((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ π‘Ÿ ∈ 𝑀) ∧ 𝑧 ∈ ((𝑉 β€œ {(1st β€˜π‘Ÿ)}) Γ— (𝑉 β€œ {(2nd β€˜π‘Ÿ)}))) β†’ (2nd β€˜π‘Ÿ)𝑉(2nd β€˜π‘§))
8569, 38, 373pm3.2i 1336 . . . . . . . . . . . . 13 ((1st β€˜π‘§) ∈ V ∧ (2nd β€˜π‘Ÿ) ∈ V ∧ (1st β€˜π‘Ÿ) ∈ V)
86 brcogw 5858 . . . . . . . . . . . . 13 ((((1st β€˜π‘§) ∈ V ∧ (2nd β€˜π‘Ÿ) ∈ V ∧ (1st β€˜π‘Ÿ) ∈ V) ∧ ((1st β€˜π‘§)𝑉(1st β€˜π‘Ÿ) ∧ (1st β€˜π‘Ÿ)𝑀(2nd β€˜π‘Ÿ))) β†’ (1st β€˜π‘§)(𝑀 ∘ 𝑉)(2nd β€˜π‘Ÿ))
8785, 86mpan 687 . . . . . . . . . . . 12 (((1st β€˜π‘§)𝑉(1st β€˜π‘Ÿ) ∧ (1st β€˜π‘Ÿ)𝑀(2nd β€˜π‘Ÿ)) β†’ (1st β€˜π‘§)(𝑀 ∘ 𝑉)(2nd β€˜π‘Ÿ))
88 fvex 6894 . . . . . . . . . . . . . 14 (2nd β€˜π‘§) ∈ V
8969, 88, 383pm3.2i 1336 . . . . . . . . . . . . 13 ((1st β€˜π‘§) ∈ V ∧ (2nd β€˜π‘§) ∈ V ∧ (2nd β€˜π‘Ÿ) ∈ V)
90 brcogw 5858 . . . . . . . . . . . . 13 ((((1st β€˜π‘§) ∈ V ∧ (2nd β€˜π‘§) ∈ V ∧ (2nd β€˜π‘Ÿ) ∈ V) ∧ ((1st β€˜π‘§)(𝑀 ∘ 𝑉)(2nd β€˜π‘Ÿ) ∧ (2nd β€˜π‘Ÿ)𝑉(2nd β€˜π‘§))) β†’ (1st β€˜π‘§)(𝑉 ∘ (𝑀 ∘ 𝑉))(2nd β€˜π‘§))
9189, 90mpan 687 . . . . . . . . . . . 12 (((1st β€˜π‘§)(𝑀 ∘ 𝑉)(2nd β€˜π‘Ÿ) ∧ (2nd β€˜π‘Ÿ)𝑉(2nd β€˜π‘§)) β†’ (1st β€˜π‘§)(𝑉 ∘ (𝑀 ∘ 𝑉))(2nd β€˜π‘§))
9287, 91sylan 579 . . . . . . . . . . 11 ((((1st β€˜π‘§)𝑉(1st β€˜π‘Ÿ) ∧ (1st β€˜π‘Ÿ)𝑀(2nd β€˜π‘Ÿ)) ∧ (2nd β€˜π‘Ÿ)𝑉(2nd β€˜π‘§)) β†’ (1st β€˜π‘§)(𝑉 ∘ (𝑀 ∘ 𝑉))(2nd β€˜π‘§))
9374, 79, 84, 92syl21anc 835 . . . . . . . . . 10 ((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ π‘Ÿ ∈ 𝑀) ∧ 𝑧 ∈ ((𝑉 β€œ {(1st β€˜π‘Ÿ)}) Γ— (𝑉 β€œ {(2nd β€˜π‘Ÿ)}))) β†’ (1st β€˜π‘§)(𝑉 ∘ (𝑀 ∘ 𝑉))(2nd β€˜π‘§))
94 df-br 5139 . . . . . . . . . 10 ((1st β€˜π‘§)(𝑉 ∘ (𝑀 ∘ 𝑉))(2nd β€˜π‘§) ↔ ⟨(1st β€˜π‘§), (2nd β€˜π‘§)⟩ ∈ (𝑉 ∘ (𝑀 ∘ 𝑉)))
9593, 94sylib 217 . . . . . . . . 9 ((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ π‘Ÿ ∈ 𝑀) ∧ 𝑧 ∈ ((𝑉 β€œ {(1st β€˜π‘Ÿ)}) Γ— (𝑉 β€œ {(2nd β€˜π‘Ÿ)}))) β†’ ⟨(1st β€˜π‘§), (2nd β€˜π‘§)⟩ ∈ (𝑉 ∘ (𝑀 ∘ 𝑉)))
9657, 95eqeltrd 2825 . . . . . . . 8 ((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ π‘Ÿ ∈ 𝑀) ∧ 𝑧 ∈ ((𝑉 β€œ {(1st β€˜π‘Ÿ)}) Γ— (𝑉 β€œ {(2nd β€˜π‘Ÿ)}))) β†’ 𝑧 ∈ (𝑉 ∘ (𝑀 ∘ 𝑉)))
9796ex 412 . . . . . . 7 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ π‘Ÿ ∈ 𝑀) β†’ (𝑧 ∈ ((𝑉 β€œ {(1st β€˜π‘Ÿ)}) Γ— (𝑉 β€œ {(2nd β€˜π‘Ÿ)})) β†’ 𝑧 ∈ (𝑉 ∘ (𝑀 ∘ 𝑉))))
9897ssrdv 3980 . . . . . 6 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ π‘Ÿ ∈ 𝑀) β†’ ((𝑉 β€œ {(1st β€˜π‘Ÿ)}) Γ— (𝑉 β€œ {(2nd β€˜π‘Ÿ)})) βŠ† (𝑉 ∘ (𝑀 ∘ 𝑉)))
99 simp1 1133 . . . . . . . . . . 11 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) β†’ π‘ˆ ∈ (UnifOnβ€˜π‘‹))
100 simp2l 1196 . . . . . . . . . . 11 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) β†’ 𝑉 ∈ π‘ˆ)
101 ustssxp 24030 . . . . . . . . . . 11 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑉 ∈ π‘ˆ) β†’ 𝑉 βŠ† (𝑋 Γ— 𝑋))
10299, 100, 101syl2anc 583 . . . . . . . . . 10 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) β†’ 𝑉 βŠ† (𝑋 Γ— 𝑋))
103 coss1 5845 . . . . . . . . . 10 (𝑉 βŠ† (𝑋 Γ— 𝑋) β†’ (𝑉 ∘ (𝑀 ∘ 𝑉)) βŠ† ((𝑋 Γ— 𝑋) ∘ (𝑀 ∘ 𝑉)))
104102, 103syl 17 . . . . . . . . 9 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) β†’ (𝑉 ∘ (𝑀 ∘ 𝑉)) βŠ† ((𝑋 Γ— 𝑋) ∘ (𝑀 ∘ 𝑉)))
105 coss1 5845 . . . . . . . . . . . 12 (𝑀 βŠ† (𝑋 Γ— 𝑋) β†’ (𝑀 ∘ 𝑉) βŠ† ((𝑋 Γ— 𝑋) ∘ 𝑉))
10624, 105syl 17 . . . . . . . . . . 11 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) β†’ (𝑀 ∘ 𝑉) βŠ† ((𝑋 Γ— 𝑋) ∘ 𝑉))
107 coss2 5846 . . . . . . . . . . . . 13 (𝑉 βŠ† (𝑋 Γ— 𝑋) β†’ ((𝑋 Γ— 𝑋) ∘ 𝑉) βŠ† ((𝑋 Γ— 𝑋) ∘ (𝑋 Γ— 𝑋)))
108 xpcoid 6279 . . . . . . . . . . . . 13 ((𝑋 Γ— 𝑋) ∘ (𝑋 Γ— 𝑋)) = (𝑋 Γ— 𝑋)
109107, 108sseqtrdi 4024 . . . . . . . . . . . 12 (𝑉 βŠ† (𝑋 Γ— 𝑋) β†’ ((𝑋 Γ— 𝑋) ∘ 𝑉) βŠ† (𝑋 Γ— 𝑋))
110102, 109syl 17 . . . . . . . . . . 11 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) β†’ ((𝑋 Γ— 𝑋) ∘ 𝑉) βŠ† (𝑋 Γ— 𝑋))
111106, 110sstrd 3984 . . . . . . . . . 10 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) β†’ (𝑀 ∘ 𝑉) βŠ† (𝑋 Γ— 𝑋))
112 coss2 5846 . . . . . . . . . . 11 ((𝑀 ∘ 𝑉) βŠ† (𝑋 Γ— 𝑋) β†’ ((𝑋 Γ— 𝑋) ∘ (𝑀 ∘ 𝑉)) βŠ† ((𝑋 Γ— 𝑋) ∘ (𝑋 Γ— 𝑋)))
113112, 108sseqtrdi 4024 . . . . . . . . . 10 ((𝑀 ∘ 𝑉) βŠ† (𝑋 Γ— 𝑋) β†’ ((𝑋 Γ— 𝑋) ∘ (𝑀 ∘ 𝑉)) βŠ† (𝑋 Γ— 𝑋))
114111, 113syl 17 . . . . . . . . 9 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) β†’ ((𝑋 Γ— 𝑋) ∘ (𝑀 ∘ 𝑉)) βŠ† (𝑋 Γ— 𝑋))
115104, 114sstrd 3984 . . . . . . . 8 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) β†’ (𝑉 ∘ (𝑀 ∘ 𝑉)) βŠ† (𝑋 Γ— 𝑋))
116 utopbas 24061 . . . . . . . . . . . 12 (π‘ˆ ∈ (UnifOnβ€˜π‘‹) β†’ 𝑋 = βˆͺ (unifTopβ€˜π‘ˆ))
1171unieqi 4911 . . . . . . . . . . . 12 βˆͺ 𝐽 = βˆͺ (unifTopβ€˜π‘ˆ)
118116, 117eqtr4di 2782 . . . . . . . . . . 11 (π‘ˆ ∈ (UnifOnβ€˜π‘‹) β†’ 𝑋 = βˆͺ 𝐽)
119118sqxpeqd 5698 . . . . . . . . . 10 (π‘ˆ ∈ (UnifOnβ€˜π‘‹) β†’ (𝑋 Γ— 𝑋) = (βˆͺ 𝐽 Γ— βˆͺ 𝐽))
12034, 34txuni 23417 . . . . . . . . . . 11 ((𝐽 ∈ Top ∧ 𝐽 ∈ Top) β†’ (βˆͺ 𝐽 Γ— βˆͺ 𝐽) = βˆͺ (𝐽 Γ—t 𝐽))
1213, 3, 120syl2anc 583 . . . . . . . . . 10 (π‘ˆ ∈ (UnifOnβ€˜π‘‹) β†’ (βˆͺ 𝐽 Γ— βˆͺ 𝐽) = βˆͺ (𝐽 Γ—t 𝐽))
122119, 121eqtrd 2764 . . . . . . . . 9 (π‘ˆ ∈ (UnifOnβ€˜π‘‹) β†’ (𝑋 Γ— 𝑋) = βˆͺ (𝐽 Γ—t 𝐽))
1231223ad2ant1 1130 . . . . . . . 8 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) β†’ (𝑋 Γ— 𝑋) = βˆͺ (𝐽 Γ—t 𝐽))
124115, 123sseqtrd 4014 . . . . . . 7 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) β†’ (𝑉 ∘ (𝑀 ∘ 𝑉)) βŠ† βˆͺ (𝐽 Γ—t 𝐽))
125124adantr 480 . . . . . 6 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ π‘Ÿ ∈ 𝑀) β†’ (𝑉 ∘ (𝑀 ∘ 𝑉)) βŠ† βˆͺ (𝐽 Γ—t 𝐽))
126 eqid 2724 . . . . . . 7 βˆͺ (𝐽 Γ—t 𝐽) = βˆͺ (𝐽 Γ—t 𝐽)
127126ssnei2 22941 . . . . . 6 ((((𝐽 Γ—t 𝐽) ∈ Top ∧ ((𝑉 β€œ {(1st β€˜π‘Ÿ)}) Γ— (𝑉 β€œ {(2nd β€˜π‘Ÿ)})) ∈ ((neiβ€˜(𝐽 Γ—t 𝐽))β€˜{π‘Ÿ})) ∧ (((𝑉 β€œ {(1st β€˜π‘Ÿ)}) Γ— (𝑉 β€œ {(2nd β€˜π‘Ÿ)})) βŠ† (𝑉 ∘ (𝑀 ∘ 𝑉)) ∧ (𝑉 ∘ (𝑀 ∘ 𝑉)) βŠ† βˆͺ (𝐽 Γ—t 𝐽))) β†’ (𝑉 ∘ (𝑀 ∘ 𝑉)) ∈ ((neiβ€˜(𝐽 Γ—t 𝐽))β€˜{π‘Ÿ}))
12820, 53, 98, 125, 127syl22anc 836 . . . . 5 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ π‘Ÿ ∈ 𝑀) β†’ (𝑉 ∘ (𝑀 ∘ 𝑉)) ∈ ((neiβ€˜(𝐽 Γ—t 𝐽))β€˜{π‘Ÿ}))
129128ralrimiva 3138 . . . 4 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) β†’ βˆ€π‘Ÿ ∈ 𝑀 (𝑉 ∘ (𝑀 ∘ 𝑉)) ∈ ((neiβ€˜(𝐽 Γ—t 𝐽))β€˜{π‘Ÿ}))
130129adantr 480 . . 3 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ 𝑀 β‰  βˆ…) β†’ βˆ€π‘Ÿ ∈ 𝑀 (𝑉 ∘ (𝑀 ∘ 𝑉)) ∈ ((neiβ€˜(𝐽 Γ—t 𝐽))β€˜{π‘Ÿ}))
1316adantr 480 . . . 4 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ 𝑀 β‰  βˆ…) β†’ (𝐽 Γ—t 𝐽) ∈ Top)
13224, 123sseqtrd 4014 . . . . 5 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) β†’ 𝑀 βŠ† βˆͺ (𝐽 Γ—t 𝐽))
133132adantr 480 . . . 4 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ 𝑀 β‰  βˆ…) β†’ 𝑀 βŠ† βˆͺ (𝐽 Γ—t 𝐽))
134 simpr 484 . . . 4 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ 𝑀 β‰  βˆ…) β†’ 𝑀 β‰  βˆ…)
135126neips 22938 . . . 4 (((𝐽 Γ—t 𝐽) ∈ Top ∧ 𝑀 βŠ† βˆͺ (𝐽 Γ—t 𝐽) ∧ 𝑀 β‰  βˆ…) β†’ ((𝑉 ∘ (𝑀 ∘ 𝑉)) ∈ ((neiβ€˜(𝐽 Γ—t 𝐽))β€˜π‘€) ↔ βˆ€π‘Ÿ ∈ 𝑀 (𝑉 ∘ (𝑀 ∘ 𝑉)) ∈ ((neiβ€˜(𝐽 Γ—t 𝐽))β€˜{π‘Ÿ})))
136131, 133, 134, 135syl3anc 1368 . . 3 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ 𝑀 β‰  βˆ…) β†’ ((𝑉 ∘ (𝑀 ∘ 𝑉)) ∈ ((neiβ€˜(𝐽 Γ—t 𝐽))β€˜π‘€) ↔ βˆ€π‘Ÿ ∈ 𝑀 (𝑉 ∘ (𝑀 ∘ 𝑉)) ∈ ((neiβ€˜(𝐽 Γ—t 𝐽))β€˜{π‘Ÿ})))
137130, 136mpbird 257 . 2 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ 𝑀 β‰  βˆ…) β†’ (𝑉 ∘ (𝑀 ∘ 𝑉)) ∈ ((neiβ€˜(𝐽 Γ—t 𝐽))β€˜π‘€))
13819, 137pm2.61dane 3021 1 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) β†’ (𝑉 ∘ (𝑀 ∘ 𝑉)) ∈ ((neiβ€˜(𝐽 Γ—t 𝐽))β€˜π‘€))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 395   ∧ w3a 1084   = wceq 1533   ∈ wcel 2098   β‰  wne 2932  βˆ€wral 3053  Vcvv 3466   βŠ† wss 3940  βˆ…c0 4314  {csn 4620  βŸ¨cop 4626  βˆͺ cuni 4899   class class class wbr 5138   Γ— cxp 5664  β—‘ccnv 5665   β€œ cima 5669   ∘ ccom 5670  Rel wrel 5671  β€˜cfv 6533  (class class class)co 7401  1st c1st 7966  2nd c2nd 7967  Topctop 22716  neicnei 22922   Γ—t ctx 23385  UnifOncust 24025  unifTopcutop 24056
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-rep 5275  ax-sep 5289  ax-nul 5296  ax-pow 5353  ax-pr 5417  ax-un 7718
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-ral 3054  df-rex 3063  df-reu 3369  df-rab 3425  df-v 3468  df-sbc 3770  df-csb 3886  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-pss 3959  df-nul 4315  df-if 4521  df-pw 4596  df-sn 4621  df-pr 4623  df-op 4627  df-uni 4900  df-int 4941  df-iun 4989  df-br 5139  df-opab 5201  df-mpt 5222  df-tr 5256  df-id 5564  df-eprel 5570  df-po 5578  df-so 5579  df-fr 5621  df-we 5623  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-ord 6357  df-on 6358  df-lim 6359  df-suc 6360  df-iota 6485  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-ov 7404  df-oprab 7405  df-mpo 7406  df-om 7849  df-1st 7968  df-2nd 7969  df-1o 8461  df-er 8698  df-en 8935  df-fin 8938  df-fi 9401  df-topgen 17387  df-top 22717  df-topon 22734  df-bases 22770  df-nei 22923  df-tx 23387  df-ust 24026  df-utop 24057
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator