# Metamath Proof Explorer

## Theorem utop2nei

Description: For any symmetrical entourage V and any relation M , build a neighborhood of M . First part of proposition 2 of BourbakiTop1 p. II.4. (Contributed by Thierry Arnoux, 14-Jan-2018)

Ref Expression
Hypothesis utoptop.1 ${⊢}{J}=\mathrm{unifTop}\left({U}\right)$
Assertion utop2nei ${⊢}\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge \left({V}\in {U}\wedge {{V}}^{-1}={V}\right)\wedge {M}\subseteq {X}×{X}\right)\to {V}\circ \left({M}\circ {V}\right)\in \mathrm{nei}\left({J}{×}_{t}{J}\right)\left({M}\right)$

### Proof

Step Hyp Ref Expression
1 utoptop.1 ${⊢}{J}=\mathrm{unifTop}\left({U}\right)$
2 utoptop ${⊢}{U}\in \mathrm{UnifOn}\left({X}\right)\to \mathrm{unifTop}\left({U}\right)\in \mathrm{Top}$
3 1 2 eqeltrid ${⊢}{U}\in \mathrm{UnifOn}\left({X}\right)\to {J}\in \mathrm{Top}$
4 txtop ${⊢}\left({J}\in \mathrm{Top}\wedge {J}\in \mathrm{Top}\right)\to {J}{×}_{t}{J}\in \mathrm{Top}$
5 3 3 4 syl2anc ${⊢}{U}\in \mathrm{UnifOn}\left({X}\right)\to {J}{×}_{t}{J}\in \mathrm{Top}$
6 5 3ad2ant1 ${⊢}\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge \left({V}\in {U}\wedge {{V}}^{-1}={V}\right)\wedge {M}\subseteq {X}×{X}\right)\to {J}{×}_{t}{J}\in \mathrm{Top}$
7 6 adantr ${⊢}\left(\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge \left({V}\in {U}\wedge {{V}}^{-1}={V}\right)\wedge {M}\subseteq {X}×{X}\right)\wedge {M}=\varnothing \right)\to {J}{×}_{t}{J}\in \mathrm{Top}$
8 0nei ${⊢}{J}{×}_{t}{J}\in \mathrm{Top}\to \varnothing \in \mathrm{nei}\left({J}{×}_{t}{J}\right)\left(\varnothing \right)$
9 7 8 syl ${⊢}\left(\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge \left({V}\in {U}\wedge {{V}}^{-1}={V}\right)\wedge {M}\subseteq {X}×{X}\right)\wedge {M}=\varnothing \right)\to \varnothing \in \mathrm{nei}\left({J}{×}_{t}{J}\right)\left(\varnothing \right)$
10 coeq1 ${⊢}{M}=\varnothing \to {M}\circ {V}=\varnothing \circ {V}$
11 co01 ${⊢}\varnothing \circ {V}=\varnothing$
12 10 11 syl6eq ${⊢}{M}=\varnothing \to {M}\circ {V}=\varnothing$
13 12 coeq2d ${⊢}{M}=\varnothing \to {V}\circ \left({M}\circ {V}\right)={V}\circ \varnothing$
14 co02 ${⊢}{V}\circ \varnothing =\varnothing$
15 13 14 syl6eq ${⊢}{M}=\varnothing \to {V}\circ \left({M}\circ {V}\right)=\varnothing$
16 15 adantl ${⊢}\left(\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge \left({V}\in {U}\wedge {{V}}^{-1}={V}\right)\wedge {M}\subseteq {X}×{X}\right)\wedge {M}=\varnothing \right)\to {V}\circ \left({M}\circ {V}\right)=\varnothing$
17 simpr ${⊢}\left(\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge \left({V}\in {U}\wedge {{V}}^{-1}={V}\right)\wedge {M}\subseteq {X}×{X}\right)\wedge {M}=\varnothing \right)\to {M}=\varnothing$
18 17 fveq2d ${⊢}\left(\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge \left({V}\in {U}\wedge {{V}}^{-1}={V}\right)\wedge {M}\subseteq {X}×{X}\right)\wedge {M}=\varnothing \right)\to \mathrm{nei}\left({J}{×}_{t}{J}\right)\left({M}\right)=\mathrm{nei}\left({J}{×}_{t}{J}\right)\left(\varnothing \right)$
19 9 16 18 3eltr4d ${⊢}\left(\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge \left({V}\in {U}\wedge {{V}}^{-1}={V}\right)\wedge {M}\subseteq {X}×{X}\right)\wedge {M}=\varnothing \right)\to {V}\circ \left({M}\circ {V}\right)\in \mathrm{nei}\left({J}{×}_{t}{J}\right)\left({M}\right)$
20 6 adantr ${⊢}\left(\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge \left({V}\in {U}\wedge {{V}}^{-1}={V}\right)\wedge {M}\subseteq {X}×{X}\right)\wedge {r}\in {M}\right)\to {J}{×}_{t}{J}\in \mathrm{Top}$
21 simpl1 ${⊢}\left(\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge \left({V}\in {U}\wedge {{V}}^{-1}={V}\right)\wedge {M}\subseteq {X}×{X}\right)\wedge {r}\in {M}\right)\to {U}\in \mathrm{UnifOn}\left({X}\right)$
22 21 3 syl ${⊢}\left(\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge \left({V}\in {U}\wedge {{V}}^{-1}={V}\right)\wedge {M}\subseteq {X}×{X}\right)\wedge {r}\in {M}\right)\to {J}\in \mathrm{Top}$
23 simpl2l ${⊢}\left(\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge \left({V}\in {U}\wedge {{V}}^{-1}={V}\right)\wedge {M}\subseteq {X}×{X}\right)\wedge {r}\in {M}\right)\to {V}\in {U}$
24 simp3 ${⊢}\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge \left({V}\in {U}\wedge {{V}}^{-1}={V}\right)\wedge {M}\subseteq {X}×{X}\right)\to {M}\subseteq {X}×{X}$
25 24 sselda ${⊢}\left(\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge \left({V}\in {U}\wedge {{V}}^{-1}={V}\right)\wedge {M}\subseteq {X}×{X}\right)\wedge {r}\in {M}\right)\to {r}\in \left({X}×{X}\right)$
26 xp1st ${⊢}{r}\in \left({X}×{X}\right)\to {1}^{st}\left({r}\right)\in {X}$
27 25 26 syl ${⊢}\left(\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge \left({V}\in {U}\wedge {{V}}^{-1}={V}\right)\wedge {M}\subseteq {X}×{X}\right)\wedge {r}\in {M}\right)\to {1}^{st}\left({r}\right)\in {X}$
28 1 utopsnnei ${⊢}\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge {V}\in {U}\wedge {1}^{st}\left({r}\right)\in {X}\right)\to {V}\left[\left\{{1}^{st}\left({r}\right)\right\}\right]\in \mathrm{nei}\left({J}\right)\left(\left\{{1}^{st}\left({r}\right)\right\}\right)$
29 21 23 27 28 syl3anc ${⊢}\left(\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge \left({V}\in {U}\wedge {{V}}^{-1}={V}\right)\wedge {M}\subseteq {X}×{X}\right)\wedge {r}\in {M}\right)\to {V}\left[\left\{{1}^{st}\left({r}\right)\right\}\right]\in \mathrm{nei}\left({J}\right)\left(\left\{{1}^{st}\left({r}\right)\right\}\right)$
30 xp2nd ${⊢}{r}\in \left({X}×{X}\right)\to {2}^{nd}\left({r}\right)\in {X}$
31 25 30 syl ${⊢}\left(\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge \left({V}\in {U}\wedge {{V}}^{-1}={V}\right)\wedge {M}\subseteq {X}×{X}\right)\wedge {r}\in {M}\right)\to {2}^{nd}\left({r}\right)\in {X}$
32 1 utopsnnei ${⊢}\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge {V}\in {U}\wedge {2}^{nd}\left({r}\right)\in {X}\right)\to {V}\left[\left\{{2}^{nd}\left({r}\right)\right\}\right]\in \mathrm{nei}\left({J}\right)\left(\left\{{2}^{nd}\left({r}\right)\right\}\right)$
33 21 23 31 32 syl3anc ${⊢}\left(\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge \left({V}\in {U}\wedge {{V}}^{-1}={V}\right)\wedge {M}\subseteq {X}×{X}\right)\wedge {r}\in {M}\right)\to {V}\left[\left\{{2}^{nd}\left({r}\right)\right\}\right]\in \mathrm{nei}\left({J}\right)\left(\left\{{2}^{nd}\left({r}\right)\right\}\right)$
34 eqid ${⊢}\bigcup {J}=\bigcup {J}$
35 34 34 neitx ${⊢}\left(\left({J}\in \mathrm{Top}\wedge {J}\in \mathrm{Top}\right)\wedge \left({V}\left[\left\{{1}^{st}\left({r}\right)\right\}\right]\in \mathrm{nei}\left({J}\right)\left(\left\{{1}^{st}\left({r}\right)\right\}\right)\wedge {V}\left[\left\{{2}^{nd}\left({r}\right)\right\}\right]\in \mathrm{nei}\left({J}\right)\left(\left\{{2}^{nd}\left({r}\right)\right\}\right)\right)\right)\to {V}\left[\left\{{1}^{st}\left({r}\right)\right\}\right]×{V}\left[\left\{{2}^{nd}\left({r}\right)\right\}\right]\in \mathrm{nei}\left({J}{×}_{t}{J}\right)\left(\left\{{1}^{st}\left({r}\right)\right\}×\left\{{2}^{nd}\left({r}\right)\right\}\right)$
36 22 22 29 33 35 syl22anc ${⊢}\left(\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge \left({V}\in {U}\wedge {{V}}^{-1}={V}\right)\wedge {M}\subseteq {X}×{X}\right)\wedge {r}\in {M}\right)\to {V}\left[\left\{{1}^{st}\left({r}\right)\right\}\right]×{V}\left[\left\{{2}^{nd}\left({r}\right)\right\}\right]\in \mathrm{nei}\left({J}{×}_{t}{J}\right)\left(\left\{{1}^{st}\left({r}\right)\right\}×\left\{{2}^{nd}\left({r}\right)\right\}\right)$
37 fvex ${⊢}{1}^{st}\left({r}\right)\in \mathrm{V}$
38 fvex ${⊢}{2}^{nd}\left({r}\right)\in \mathrm{V}$
39 37 38 xpsn ${⊢}\left\{{1}^{st}\left({r}\right)\right\}×\left\{{2}^{nd}\left({r}\right)\right\}=\left\{⟨{1}^{st}\left({r}\right),{2}^{nd}\left({r}\right)⟩\right\}$
40 39 fveq2i ${⊢}\mathrm{nei}\left({J}{×}_{t}{J}\right)\left(\left\{{1}^{st}\left({r}\right)\right\}×\left\{{2}^{nd}\left({r}\right)\right\}\right)=\mathrm{nei}\left({J}{×}_{t}{J}\right)\left(\left\{⟨{1}^{st}\left({r}\right),{2}^{nd}\left({r}\right)⟩\right\}\right)$
41 36 40 syl6eleq ${⊢}\left(\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge \left({V}\in {U}\wedge {{V}}^{-1}={V}\right)\wedge {M}\subseteq {X}×{X}\right)\wedge {r}\in {M}\right)\to {V}\left[\left\{{1}^{st}\left({r}\right)\right\}\right]×{V}\left[\left\{{2}^{nd}\left({r}\right)\right\}\right]\in \mathrm{nei}\left({J}{×}_{t}{J}\right)\left(\left\{⟨{1}^{st}\left({r}\right),{2}^{nd}\left({r}\right)⟩\right\}\right)$
42 24 adantr ${⊢}\left(\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge \left({V}\in {U}\wedge {{V}}^{-1}={V}\right)\wedge {M}\subseteq {X}×{X}\right)\wedge {r}\in {M}\right)\to {M}\subseteq {X}×{X}$
43 xpss ${⊢}{X}×{X}\subseteq \mathrm{V}×\mathrm{V}$
44 sstr ${⊢}\left({M}\subseteq {X}×{X}\wedge {X}×{X}\subseteq \mathrm{V}×\mathrm{V}\right)\to {M}\subseteq \mathrm{V}×\mathrm{V}$
45 43 44 mpan2 ${⊢}{M}\subseteq {X}×{X}\to {M}\subseteq \mathrm{V}×\mathrm{V}$
46 df-rel ${⊢}\mathrm{Rel}{M}↔{M}\subseteq \mathrm{V}×\mathrm{V}$
47 45 46 sylibr ${⊢}{M}\subseteq {X}×{X}\to \mathrm{Rel}{M}$
48 42 47 syl ${⊢}\left(\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge \left({V}\in {U}\wedge {{V}}^{-1}={V}\right)\wedge {M}\subseteq {X}×{X}\right)\wedge {r}\in {M}\right)\to \mathrm{Rel}{M}$
49 1st2nd ${⊢}\left(\mathrm{Rel}{M}\wedge {r}\in {M}\right)\to {r}=⟨{1}^{st}\left({r}\right),{2}^{nd}\left({r}\right)⟩$
50 48 49 sylancom ${⊢}\left(\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge \left({V}\in {U}\wedge {{V}}^{-1}={V}\right)\wedge {M}\subseteq {X}×{X}\right)\wedge {r}\in {M}\right)\to {r}=⟨{1}^{st}\left({r}\right),{2}^{nd}\left({r}\right)⟩$
51 50 sneqd ${⊢}\left(\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge \left({V}\in {U}\wedge {{V}}^{-1}={V}\right)\wedge {M}\subseteq {X}×{X}\right)\wedge {r}\in {M}\right)\to \left\{{r}\right\}=\left\{⟨{1}^{st}\left({r}\right),{2}^{nd}\left({r}\right)⟩\right\}$
52 51 fveq2d ${⊢}\left(\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge \left({V}\in {U}\wedge {{V}}^{-1}={V}\right)\wedge {M}\subseteq {X}×{X}\right)\wedge {r}\in {M}\right)\to \mathrm{nei}\left({J}{×}_{t}{J}\right)\left(\left\{{r}\right\}\right)=\mathrm{nei}\left({J}{×}_{t}{J}\right)\left(\left\{⟨{1}^{st}\left({r}\right),{2}^{nd}\left({r}\right)⟩\right\}\right)$
53 41 52 eleqtrrd ${⊢}\left(\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge \left({V}\in {U}\wedge {{V}}^{-1}={V}\right)\wedge {M}\subseteq {X}×{X}\right)\wedge {r}\in {M}\right)\to {V}\left[\left\{{1}^{st}\left({r}\right)\right\}\right]×{V}\left[\left\{{2}^{nd}\left({r}\right)\right\}\right]\in \mathrm{nei}\left({J}{×}_{t}{J}\right)\left(\left\{{r}\right\}\right)$
54 relxp ${⊢}\mathrm{Rel}\left({V}\left[\left\{{1}^{st}\left({r}\right)\right\}\right]×{V}\left[\left\{{2}^{nd}\left({r}\right)\right\}\right]\right)$
55 54 a1i ${⊢}\left(\left(\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge \left({V}\in {U}\wedge {{V}}^{-1}={V}\right)\wedge {M}\subseteq {X}×{X}\right)\wedge {r}\in {M}\right)\wedge {z}\in \left({V}\left[\left\{{1}^{st}\left({r}\right)\right\}\right]×{V}\left[\left\{{2}^{nd}\left({r}\right)\right\}\right]\right)\right)\to \mathrm{Rel}\left({V}\left[\left\{{1}^{st}\left({r}\right)\right\}\right]×{V}\left[\left\{{2}^{nd}\left({r}\right)\right\}\right]\right)$
56 1st2nd ${⊢}\left(\mathrm{Rel}\left({V}\left[\left\{{1}^{st}\left({r}\right)\right\}\right]×{V}\left[\left\{{2}^{nd}\left({r}\right)\right\}\right]\right)\wedge {z}\in \left({V}\left[\left\{{1}^{st}\left({r}\right)\right\}\right]×{V}\left[\left\{{2}^{nd}\left({r}\right)\right\}\right]\right)\right)\to {z}=⟨{1}^{st}\left({z}\right),{2}^{nd}\left({z}\right)⟩$
57 55 56 sylancom ${⊢}\left(\left(\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge \left({V}\in {U}\wedge {{V}}^{-1}={V}\right)\wedge {M}\subseteq {X}×{X}\right)\wedge {r}\in {M}\right)\wedge {z}\in \left({V}\left[\left\{{1}^{st}\left({r}\right)\right\}\right]×{V}\left[\left\{{2}^{nd}\left({r}\right)\right\}\right]\right)\right)\to {z}=⟨{1}^{st}\left({z}\right),{2}^{nd}\left({z}\right)⟩$
58 simpll2 ${⊢}\left(\left(\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge \left({V}\in {U}\wedge {{V}}^{-1}={V}\right)\wedge {M}\subseteq {X}×{X}\right)\wedge {r}\in {M}\right)\wedge {z}\in \left({V}\left[\left\{{1}^{st}\left({r}\right)\right\}\right]×{V}\left[\left\{{2}^{nd}\left({r}\right)\right\}\right]\right)\right)\to \left({V}\in {U}\wedge {{V}}^{-1}={V}\right)$
59 58 simprd ${⊢}\left(\left(\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge \left({V}\in {U}\wedge {{V}}^{-1}={V}\right)\wedge {M}\subseteq {X}×{X}\right)\wedge {r}\in {M}\right)\wedge {z}\in \left({V}\left[\left\{{1}^{st}\left({r}\right)\right\}\right]×{V}\left[\left\{{2}^{nd}\left({r}\right)\right\}\right]\right)\right)\to {{V}}^{-1}={V}$
60 simpll1 ${⊢}\left(\left(\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge \left({V}\in {U}\wedge {{V}}^{-1}={V}\right)\wedge {M}\subseteq {X}×{X}\right)\wedge {r}\in {M}\right)\wedge {z}\in \left({V}\left[\left\{{1}^{st}\left({r}\right)\right\}\right]×{V}\left[\left\{{2}^{nd}\left({r}\right)\right\}\right]\right)\right)\to {U}\in \mathrm{UnifOn}\left({X}\right)$
61 58 simpld ${⊢}\left(\left(\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge \left({V}\in {U}\wedge {{V}}^{-1}={V}\right)\wedge {M}\subseteq {X}×{X}\right)\wedge {r}\in {M}\right)\wedge {z}\in \left({V}\left[\left\{{1}^{st}\left({r}\right)\right\}\right]×{V}\left[\left\{{2}^{nd}\left({r}\right)\right\}\right]\right)\right)\to {V}\in {U}$
62 ustrel ${⊢}\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge {V}\in {U}\right)\to \mathrm{Rel}{V}$
63 60 61 62 syl2anc ${⊢}\left(\left(\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge \left({V}\in {U}\wedge {{V}}^{-1}={V}\right)\wedge {M}\subseteq {X}×{X}\right)\wedge {r}\in {M}\right)\wedge {z}\in \left({V}\left[\left\{{1}^{st}\left({r}\right)\right\}\right]×{V}\left[\left\{{2}^{nd}\left({r}\right)\right\}\right]\right)\right)\to \mathrm{Rel}{V}$
64 xp1st ${⊢}{z}\in \left({V}\left[\left\{{1}^{st}\left({r}\right)\right\}\right]×{V}\left[\left\{{2}^{nd}\left({r}\right)\right\}\right]\right)\to {1}^{st}\left({z}\right)\in {V}\left[\left\{{1}^{st}\left({r}\right)\right\}\right]$
65 64 adantl ${⊢}\left(\left(\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge \left({V}\in {U}\wedge {{V}}^{-1}={V}\right)\wedge {M}\subseteq {X}×{X}\right)\wedge {r}\in {M}\right)\wedge {z}\in \left({V}\left[\left\{{1}^{st}\left({r}\right)\right\}\right]×{V}\left[\left\{{2}^{nd}\left({r}\right)\right\}\right]\right)\right)\to {1}^{st}\left({z}\right)\in {V}\left[\left\{{1}^{st}\left({r}\right)\right\}\right]$
66 elrelimasn ${⊢}\mathrm{Rel}{V}\to \left({1}^{st}\left({z}\right)\in {V}\left[\left\{{1}^{st}\left({r}\right)\right\}\right]↔{1}^{st}\left({r}\right){V}{1}^{st}\left({z}\right)\right)$
67 66 biimpa ${⊢}\left(\mathrm{Rel}{V}\wedge {1}^{st}\left({z}\right)\in {V}\left[\left\{{1}^{st}\left({r}\right)\right\}\right]\right)\to {1}^{st}\left({r}\right){V}{1}^{st}\left({z}\right)$
68 63 65 67 syl2anc ${⊢}\left(\left(\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge \left({V}\in {U}\wedge {{V}}^{-1}={V}\right)\wedge {M}\subseteq {X}×{X}\right)\wedge {r}\in {M}\right)\wedge {z}\in \left({V}\left[\left\{{1}^{st}\left({r}\right)\right\}\right]×{V}\left[\left\{{2}^{nd}\left({r}\right)\right\}\right]\right)\right)\to {1}^{st}\left({r}\right){V}{1}^{st}\left({z}\right)$
69 fvex ${⊢}{1}^{st}\left({z}\right)\in \mathrm{V}$
70 37 69 brcnv ${⊢}{1}^{st}\left({r}\right){{V}}^{-1}{1}^{st}\left({z}\right)↔{1}^{st}\left({z}\right){V}{1}^{st}\left({r}\right)$
71 breq ${⊢}{{V}}^{-1}={V}\to \left({1}^{st}\left({r}\right){{V}}^{-1}{1}^{st}\left({z}\right)↔{1}^{st}\left({r}\right){V}{1}^{st}\left({z}\right)\right)$
72 70 71 syl5bbr ${⊢}{{V}}^{-1}={V}\to \left({1}^{st}\left({z}\right){V}{1}^{st}\left({r}\right)↔{1}^{st}\left({r}\right){V}{1}^{st}\left({z}\right)\right)$
73 72 biimpar ${⊢}\left({{V}}^{-1}={V}\wedge {1}^{st}\left({r}\right){V}{1}^{st}\left({z}\right)\right)\to {1}^{st}\left({z}\right){V}{1}^{st}\left({r}\right)$
74 59 68 73 syl2anc ${⊢}\left(\left(\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge \left({V}\in {U}\wedge {{V}}^{-1}={V}\right)\wedge {M}\subseteq {X}×{X}\right)\wedge {r}\in {M}\right)\wedge {z}\in \left({V}\left[\left\{{1}^{st}\left({r}\right)\right\}\right]×{V}\left[\left\{{2}^{nd}\left({r}\right)\right\}\right]\right)\right)\to {1}^{st}\left({z}\right){V}{1}^{st}\left({r}\right)$
75 simpll3 ${⊢}\left(\left(\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge \left({V}\in {U}\wedge {{V}}^{-1}={V}\right)\wedge {M}\subseteq {X}×{X}\right)\wedge {r}\in {M}\right)\wedge {z}\in \left({V}\left[\left\{{1}^{st}\left({r}\right)\right\}\right]×{V}\left[\left\{{2}^{nd}\left({r}\right)\right\}\right]\right)\right)\to {M}\subseteq {X}×{X}$
76 simplr ${⊢}\left(\left(\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge \left({V}\in {U}\wedge {{V}}^{-1}={V}\right)\wedge {M}\subseteq {X}×{X}\right)\wedge {r}\in {M}\right)\wedge {z}\in \left({V}\left[\left\{{1}^{st}\left({r}\right)\right\}\right]×{V}\left[\left\{{2}^{nd}\left({r}\right)\right\}\right]\right)\right)\to {r}\in {M}$
77 1st2ndbr ${⊢}\left(\mathrm{Rel}{M}\wedge {r}\in {M}\right)\to {1}^{st}\left({r}\right){M}{2}^{nd}\left({r}\right)$
78 47 77 sylan ${⊢}\left({M}\subseteq {X}×{X}\wedge {r}\in {M}\right)\to {1}^{st}\left({r}\right){M}{2}^{nd}\left({r}\right)$
79 75 76 78 syl2anc ${⊢}\left(\left(\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge \left({V}\in {U}\wedge {{V}}^{-1}={V}\right)\wedge {M}\subseteq {X}×{X}\right)\wedge {r}\in {M}\right)\wedge {z}\in \left({V}\left[\left\{{1}^{st}\left({r}\right)\right\}\right]×{V}\left[\left\{{2}^{nd}\left({r}\right)\right\}\right]\right)\right)\to {1}^{st}\left({r}\right){M}{2}^{nd}\left({r}\right)$
80 xp2nd ${⊢}{z}\in \left({V}\left[\left\{{1}^{st}\left({r}\right)\right\}\right]×{V}\left[\left\{{2}^{nd}\left({r}\right)\right\}\right]\right)\to {2}^{nd}\left({z}\right)\in {V}\left[\left\{{2}^{nd}\left({r}\right)\right\}\right]$
81 80 adantl ${⊢}\left(\left(\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge \left({V}\in {U}\wedge {{V}}^{-1}={V}\right)\wedge {M}\subseteq {X}×{X}\right)\wedge {r}\in {M}\right)\wedge {z}\in \left({V}\left[\left\{{1}^{st}\left({r}\right)\right\}\right]×{V}\left[\left\{{2}^{nd}\left({r}\right)\right\}\right]\right)\right)\to {2}^{nd}\left({z}\right)\in {V}\left[\left\{{2}^{nd}\left({r}\right)\right\}\right]$
82 elrelimasn ${⊢}\mathrm{Rel}{V}\to \left({2}^{nd}\left({z}\right)\in {V}\left[\left\{{2}^{nd}\left({r}\right)\right\}\right]↔{2}^{nd}\left({r}\right){V}{2}^{nd}\left({z}\right)\right)$
83 82 biimpa ${⊢}\left(\mathrm{Rel}{V}\wedge {2}^{nd}\left({z}\right)\in {V}\left[\left\{{2}^{nd}\left({r}\right)\right\}\right]\right)\to {2}^{nd}\left({r}\right){V}{2}^{nd}\left({z}\right)$
84 63 81 83 syl2anc ${⊢}\left(\left(\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge \left({V}\in {U}\wedge {{V}}^{-1}={V}\right)\wedge {M}\subseteq {X}×{X}\right)\wedge {r}\in {M}\right)\wedge {z}\in \left({V}\left[\left\{{1}^{st}\left({r}\right)\right\}\right]×{V}\left[\left\{{2}^{nd}\left({r}\right)\right\}\right]\right)\right)\to {2}^{nd}\left({r}\right){V}{2}^{nd}\left({z}\right)$
85 69 38 37 3pm3.2i ${⊢}\left({1}^{st}\left({z}\right)\in \mathrm{V}\wedge {2}^{nd}\left({r}\right)\in \mathrm{V}\wedge {1}^{st}\left({r}\right)\in \mathrm{V}\right)$
86 brcogw ${⊢}\left(\left({1}^{st}\left({z}\right)\in \mathrm{V}\wedge {2}^{nd}\left({r}\right)\in \mathrm{V}\wedge {1}^{st}\left({r}\right)\in \mathrm{V}\right)\wedge \left({1}^{st}\left({z}\right){V}{1}^{st}\left({r}\right)\wedge {1}^{st}\left({r}\right){M}{2}^{nd}\left({r}\right)\right)\right)\to {1}^{st}\left({z}\right)\left({M}\circ {V}\right){2}^{nd}\left({r}\right)$
87 85 86 mpan ${⊢}\left({1}^{st}\left({z}\right){V}{1}^{st}\left({r}\right)\wedge {1}^{st}\left({r}\right){M}{2}^{nd}\left({r}\right)\right)\to {1}^{st}\left({z}\right)\left({M}\circ {V}\right){2}^{nd}\left({r}\right)$
88 fvex ${⊢}{2}^{nd}\left({z}\right)\in \mathrm{V}$
89 69 88 38 3pm3.2i ${⊢}\left({1}^{st}\left({z}\right)\in \mathrm{V}\wedge {2}^{nd}\left({z}\right)\in \mathrm{V}\wedge {2}^{nd}\left({r}\right)\in \mathrm{V}\right)$
90 brcogw ${⊢}\left(\left({1}^{st}\left({z}\right)\in \mathrm{V}\wedge {2}^{nd}\left({z}\right)\in \mathrm{V}\wedge {2}^{nd}\left({r}\right)\in \mathrm{V}\right)\wedge \left({1}^{st}\left({z}\right)\left({M}\circ {V}\right){2}^{nd}\left({r}\right)\wedge {2}^{nd}\left({r}\right){V}{2}^{nd}\left({z}\right)\right)\right)\to {1}^{st}\left({z}\right)\left({V}\circ \left({M}\circ {V}\right)\right){2}^{nd}\left({z}\right)$
91 89 90 mpan ${⊢}\left({1}^{st}\left({z}\right)\left({M}\circ {V}\right){2}^{nd}\left({r}\right)\wedge {2}^{nd}\left({r}\right){V}{2}^{nd}\left({z}\right)\right)\to {1}^{st}\left({z}\right)\left({V}\circ \left({M}\circ {V}\right)\right){2}^{nd}\left({z}\right)$
92 87 91 sylan ${⊢}\left(\left({1}^{st}\left({z}\right){V}{1}^{st}\left({r}\right)\wedge {1}^{st}\left({r}\right){M}{2}^{nd}\left({r}\right)\right)\wedge {2}^{nd}\left({r}\right){V}{2}^{nd}\left({z}\right)\right)\to {1}^{st}\left({z}\right)\left({V}\circ \left({M}\circ {V}\right)\right){2}^{nd}\left({z}\right)$
93 74 79 84 92 syl21anc ${⊢}\left(\left(\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge \left({V}\in {U}\wedge {{V}}^{-1}={V}\right)\wedge {M}\subseteq {X}×{X}\right)\wedge {r}\in {M}\right)\wedge {z}\in \left({V}\left[\left\{{1}^{st}\left({r}\right)\right\}\right]×{V}\left[\left\{{2}^{nd}\left({r}\right)\right\}\right]\right)\right)\to {1}^{st}\left({z}\right)\left({V}\circ \left({M}\circ {V}\right)\right){2}^{nd}\left({z}\right)$
94 df-br ${⊢}{1}^{st}\left({z}\right)\left({V}\circ \left({M}\circ {V}\right)\right){2}^{nd}\left({z}\right)↔⟨{1}^{st}\left({z}\right),{2}^{nd}\left({z}\right)⟩\in \left({V}\circ \left({M}\circ {V}\right)\right)$
95 93 94 sylib ${⊢}\left(\left(\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge \left({V}\in {U}\wedge {{V}}^{-1}={V}\right)\wedge {M}\subseteq {X}×{X}\right)\wedge {r}\in {M}\right)\wedge {z}\in \left({V}\left[\left\{{1}^{st}\left({r}\right)\right\}\right]×{V}\left[\left\{{2}^{nd}\left({r}\right)\right\}\right]\right)\right)\to ⟨{1}^{st}\left({z}\right),{2}^{nd}\left({z}\right)⟩\in \left({V}\circ \left({M}\circ {V}\right)\right)$
96 57 95 eqeltrd ${⊢}\left(\left(\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge \left({V}\in {U}\wedge {{V}}^{-1}={V}\right)\wedge {M}\subseteq {X}×{X}\right)\wedge {r}\in {M}\right)\wedge {z}\in \left({V}\left[\left\{{1}^{st}\left({r}\right)\right\}\right]×{V}\left[\left\{{2}^{nd}\left({r}\right)\right\}\right]\right)\right)\to {z}\in \left({V}\circ \left({M}\circ {V}\right)\right)$
97 96 ex ${⊢}\left(\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge \left({V}\in {U}\wedge {{V}}^{-1}={V}\right)\wedge {M}\subseteq {X}×{X}\right)\wedge {r}\in {M}\right)\to \left({z}\in \left({V}\left[\left\{{1}^{st}\left({r}\right)\right\}\right]×{V}\left[\left\{{2}^{nd}\left({r}\right)\right\}\right]\right)\to {z}\in \left({V}\circ \left({M}\circ {V}\right)\right)\right)$
98 97 ssrdv ${⊢}\left(\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge \left({V}\in {U}\wedge {{V}}^{-1}={V}\right)\wedge {M}\subseteq {X}×{X}\right)\wedge {r}\in {M}\right)\to {V}\left[\left\{{1}^{st}\left({r}\right)\right\}\right]×{V}\left[\left\{{2}^{nd}\left({r}\right)\right\}\right]\subseteq {V}\circ \left({M}\circ {V}\right)$
99 simp1 ${⊢}\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge \left({V}\in {U}\wedge {{V}}^{-1}={V}\right)\wedge {M}\subseteq {X}×{X}\right)\to {U}\in \mathrm{UnifOn}\left({X}\right)$
100 simp2l ${⊢}\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge \left({V}\in {U}\wedge {{V}}^{-1}={V}\right)\wedge {M}\subseteq {X}×{X}\right)\to {V}\in {U}$
101 ustssxp ${⊢}\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge {V}\in {U}\right)\to {V}\subseteq {X}×{X}$
102 99 100 101 syl2anc ${⊢}\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge \left({V}\in {U}\wedge {{V}}^{-1}={V}\right)\wedge {M}\subseteq {X}×{X}\right)\to {V}\subseteq {X}×{X}$
103 coss1 ${⊢}{V}\subseteq {X}×{X}\to {V}\circ \left({M}\circ {V}\right)\subseteq \left({X}×{X}\right)\circ \left({M}\circ {V}\right)$
104 102 103 syl ${⊢}\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge \left({V}\in {U}\wedge {{V}}^{-1}={V}\right)\wedge {M}\subseteq {X}×{X}\right)\to {V}\circ \left({M}\circ {V}\right)\subseteq \left({X}×{X}\right)\circ \left({M}\circ {V}\right)$
105 coss1 ${⊢}{M}\subseteq {X}×{X}\to {M}\circ {V}\subseteq \left({X}×{X}\right)\circ {V}$
106 24 105 syl ${⊢}\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge \left({V}\in {U}\wedge {{V}}^{-1}={V}\right)\wedge {M}\subseteq {X}×{X}\right)\to {M}\circ {V}\subseteq \left({X}×{X}\right)\circ {V}$
107 coss2 ${⊢}{V}\subseteq {X}×{X}\to \left({X}×{X}\right)\circ {V}\subseteq \left({X}×{X}\right)\circ \left({X}×{X}\right)$
108 xpcoid ${⊢}\left({X}×{X}\right)\circ \left({X}×{X}\right)={X}×{X}$
109 107 108 sseqtrdi ${⊢}{V}\subseteq {X}×{X}\to \left({X}×{X}\right)\circ {V}\subseteq {X}×{X}$
110 102 109 syl ${⊢}\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge \left({V}\in {U}\wedge {{V}}^{-1}={V}\right)\wedge {M}\subseteq {X}×{X}\right)\to \left({X}×{X}\right)\circ {V}\subseteq {X}×{X}$
111 106 110 sstrd ${⊢}\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge \left({V}\in {U}\wedge {{V}}^{-1}={V}\right)\wedge {M}\subseteq {X}×{X}\right)\to {M}\circ {V}\subseteq {X}×{X}$
112 coss2 ${⊢}{M}\circ {V}\subseteq {X}×{X}\to \left({X}×{X}\right)\circ \left({M}\circ {V}\right)\subseteq \left({X}×{X}\right)\circ \left({X}×{X}\right)$
113 112 108 sseqtrdi ${⊢}{M}\circ {V}\subseteq {X}×{X}\to \left({X}×{X}\right)\circ \left({M}\circ {V}\right)\subseteq {X}×{X}$
114 111 113 syl ${⊢}\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge \left({V}\in {U}\wedge {{V}}^{-1}={V}\right)\wedge {M}\subseteq {X}×{X}\right)\to \left({X}×{X}\right)\circ \left({M}\circ {V}\right)\subseteq {X}×{X}$
115 104 114 sstrd ${⊢}\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge \left({V}\in {U}\wedge {{V}}^{-1}={V}\right)\wedge {M}\subseteq {X}×{X}\right)\to {V}\circ \left({M}\circ {V}\right)\subseteq {X}×{X}$
116 utopbas ${⊢}{U}\in \mathrm{UnifOn}\left({X}\right)\to {X}=\bigcup \mathrm{unifTop}\left({U}\right)$
117 1 unieqi ${⊢}\bigcup {J}=\bigcup \mathrm{unifTop}\left({U}\right)$
118 116 117 syl6eqr ${⊢}{U}\in \mathrm{UnifOn}\left({X}\right)\to {X}=\bigcup {J}$
119 118 sqxpeqd ${⊢}{U}\in \mathrm{UnifOn}\left({X}\right)\to {X}×{X}=\bigcup {J}×\bigcup {J}$
120 34 34 txuni ${⊢}\left({J}\in \mathrm{Top}\wedge {J}\in \mathrm{Top}\right)\to \bigcup {J}×\bigcup {J}=\bigcup \left({J}{×}_{t}{J}\right)$
121 3 3 120 syl2anc ${⊢}{U}\in \mathrm{UnifOn}\left({X}\right)\to \bigcup {J}×\bigcup {J}=\bigcup \left({J}{×}_{t}{J}\right)$
122 119 121 eqtrd ${⊢}{U}\in \mathrm{UnifOn}\left({X}\right)\to {X}×{X}=\bigcup \left({J}{×}_{t}{J}\right)$
123 122 3ad2ant1 ${⊢}\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge \left({V}\in {U}\wedge {{V}}^{-1}={V}\right)\wedge {M}\subseteq {X}×{X}\right)\to {X}×{X}=\bigcup \left({J}{×}_{t}{J}\right)$
124 115 123 sseqtrd ${⊢}\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge \left({V}\in {U}\wedge {{V}}^{-1}={V}\right)\wedge {M}\subseteq {X}×{X}\right)\to {V}\circ \left({M}\circ {V}\right)\subseteq \bigcup \left({J}{×}_{t}{J}\right)$
125 124 adantr ${⊢}\left(\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge \left({V}\in {U}\wedge {{V}}^{-1}={V}\right)\wedge {M}\subseteq {X}×{X}\right)\wedge {r}\in {M}\right)\to {V}\circ \left({M}\circ {V}\right)\subseteq \bigcup \left({J}{×}_{t}{J}\right)$
126 eqid ${⊢}\bigcup \left({J}{×}_{t}{J}\right)=\bigcup \left({J}{×}_{t}{J}\right)$
127 126 ssnei2 ${⊢}\left(\left({J}{×}_{t}{J}\in \mathrm{Top}\wedge {V}\left[\left\{{1}^{st}\left({r}\right)\right\}\right]×{V}\left[\left\{{2}^{nd}\left({r}\right)\right\}\right]\in \mathrm{nei}\left({J}{×}_{t}{J}\right)\left(\left\{{r}\right\}\right)\right)\wedge \left({V}\left[\left\{{1}^{st}\left({r}\right)\right\}\right]×{V}\left[\left\{{2}^{nd}\left({r}\right)\right\}\right]\subseteq {V}\circ \left({M}\circ {V}\right)\wedge {V}\circ \left({M}\circ {V}\right)\subseteq \bigcup \left({J}{×}_{t}{J}\right)\right)\right)\to {V}\circ \left({M}\circ {V}\right)\in \mathrm{nei}\left({J}{×}_{t}{J}\right)\left(\left\{{r}\right\}\right)$
128 20 53 98 125 127 syl22anc ${⊢}\left(\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge \left({V}\in {U}\wedge {{V}}^{-1}={V}\right)\wedge {M}\subseteq {X}×{X}\right)\wedge {r}\in {M}\right)\to {V}\circ \left({M}\circ {V}\right)\in \mathrm{nei}\left({J}{×}_{t}{J}\right)\left(\left\{{r}\right\}\right)$
129 128 ralrimiva ${⊢}\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge \left({V}\in {U}\wedge {{V}}^{-1}={V}\right)\wedge {M}\subseteq {X}×{X}\right)\to \forall {r}\in {M}\phantom{\rule{.4em}{0ex}}{V}\circ \left({M}\circ {V}\right)\in \mathrm{nei}\left({J}{×}_{t}{J}\right)\left(\left\{{r}\right\}\right)$
130 129 adantr ${⊢}\left(\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge \left({V}\in {U}\wedge {{V}}^{-1}={V}\right)\wedge {M}\subseteq {X}×{X}\right)\wedge {M}\ne \varnothing \right)\to \forall {r}\in {M}\phantom{\rule{.4em}{0ex}}{V}\circ \left({M}\circ {V}\right)\in \mathrm{nei}\left({J}{×}_{t}{J}\right)\left(\left\{{r}\right\}\right)$
131 6 adantr ${⊢}\left(\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge \left({V}\in {U}\wedge {{V}}^{-1}={V}\right)\wedge {M}\subseteq {X}×{X}\right)\wedge {M}\ne \varnothing \right)\to {J}{×}_{t}{J}\in \mathrm{Top}$
132 24 123 sseqtrd ${⊢}\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge \left({V}\in {U}\wedge {{V}}^{-1}={V}\right)\wedge {M}\subseteq {X}×{X}\right)\to {M}\subseteq \bigcup \left({J}{×}_{t}{J}\right)$
133 132 adantr ${⊢}\left(\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge \left({V}\in {U}\wedge {{V}}^{-1}={V}\right)\wedge {M}\subseteq {X}×{X}\right)\wedge {M}\ne \varnothing \right)\to {M}\subseteq \bigcup \left({J}{×}_{t}{J}\right)$
134 simpr ${⊢}\left(\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge \left({V}\in {U}\wedge {{V}}^{-1}={V}\right)\wedge {M}\subseteq {X}×{X}\right)\wedge {M}\ne \varnothing \right)\to {M}\ne \varnothing$
135 126 neips ${⊢}\left({J}{×}_{t}{J}\in \mathrm{Top}\wedge {M}\subseteq \bigcup \left({J}{×}_{t}{J}\right)\wedge {M}\ne \varnothing \right)\to \left({V}\circ \left({M}\circ {V}\right)\in \mathrm{nei}\left({J}{×}_{t}{J}\right)\left({M}\right)↔\forall {r}\in {M}\phantom{\rule{.4em}{0ex}}{V}\circ \left({M}\circ {V}\right)\in \mathrm{nei}\left({J}{×}_{t}{J}\right)\left(\left\{{r}\right\}\right)\right)$
136 131 133 134 135 syl3anc ${⊢}\left(\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge \left({V}\in {U}\wedge {{V}}^{-1}={V}\right)\wedge {M}\subseteq {X}×{X}\right)\wedge {M}\ne \varnothing \right)\to \left({V}\circ \left({M}\circ {V}\right)\in \mathrm{nei}\left({J}{×}_{t}{J}\right)\left({M}\right)↔\forall {r}\in {M}\phantom{\rule{.4em}{0ex}}{V}\circ \left({M}\circ {V}\right)\in \mathrm{nei}\left({J}{×}_{t}{J}\right)\left(\left\{{r}\right\}\right)\right)$
137 130 136 mpbird ${⊢}\left(\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge \left({V}\in {U}\wedge {{V}}^{-1}={V}\right)\wedge {M}\subseteq {X}×{X}\right)\wedge {M}\ne \varnothing \right)\to {V}\circ \left({M}\circ {V}\right)\in \mathrm{nei}\left({J}{×}_{t}{J}\right)\left({M}\right)$
138 19 137 pm2.61dane ${⊢}\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge \left({V}\in {U}\wedge {{V}}^{-1}={V}\right)\wedge {M}\subseteq {X}×{X}\right)\to {V}\circ \left({M}\circ {V}\right)\in \mathrm{nei}\left({J}{×}_{t}{J}\right)\left({M}\right)$