# Metamath Proof Explorer

## Theorem ucnima

Description: An equivalent statement of the definition of uniformly continuous function. (Contributed by Thierry Arnoux, 19-Nov-2017)

Ref Expression
Hypotheses ucnprima.1 ${⊢}{\phi }\to {U}\in \mathrm{UnifOn}\left({X}\right)$
ucnprima.2 ${⊢}{\phi }\to {V}\in \mathrm{UnifOn}\left({Y}\right)$
ucnprima.3 ${⊢}{\phi }\to {F}\in \left({U}\mathrm{uCn}{V}\right)$
ucnprima.4 ${⊢}{\phi }\to {W}\in {V}$
ucnprima.5 ${⊢}{G}=\left({x}\in {X},{y}\in {X}⟼⟨{F}\left({x}\right),{F}\left({y}\right)⟩\right)$
Assertion ucnima ${⊢}{\phi }\to \exists {r}\in {U}\phantom{\rule{.4em}{0ex}}{G}\left[{r}\right]\subseteq {W}$

### Proof

Step Hyp Ref Expression
1 ucnprima.1 ${⊢}{\phi }\to {U}\in \mathrm{UnifOn}\left({X}\right)$
2 ucnprima.2 ${⊢}{\phi }\to {V}\in \mathrm{UnifOn}\left({Y}\right)$
3 ucnprima.3 ${⊢}{\phi }\to {F}\in \left({U}\mathrm{uCn}{V}\right)$
4 ucnprima.4 ${⊢}{\phi }\to {W}\in {V}$
5 ucnprima.5 ${⊢}{G}=\left({x}\in {X},{y}\in {X}⟼⟨{F}\left({x}\right),{F}\left({y}\right)⟩\right)$
6 breq ${⊢}{w}={W}\to \left({F}\left({x}\right){w}{F}\left({y}\right)↔{F}\left({x}\right){W}{F}\left({y}\right)\right)$
7 6 imbi2d ${⊢}{w}={W}\to \left(\left({x}{r}{y}\to {F}\left({x}\right){w}{F}\left({y}\right)\right)↔\left({x}{r}{y}\to {F}\left({x}\right){W}{F}\left({y}\right)\right)\right)$
8 7 ralbidv ${⊢}{w}={W}\to \left(\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{r}{y}\to {F}\left({x}\right){w}{F}\left({y}\right)\right)↔\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{r}{y}\to {F}\left({x}\right){W}{F}\left({y}\right)\right)\right)$
9 8 rexralbidv ${⊢}{w}={W}\to \left(\exists {r}\in {U}\phantom{\rule{.4em}{0ex}}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{r}{y}\to {F}\left({x}\right){w}{F}\left({y}\right)\right)↔\exists {r}\in {U}\phantom{\rule{.4em}{0ex}}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{r}{y}\to {F}\left({x}\right){W}{F}\left({y}\right)\right)\right)$
10 isucn ${⊢}\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge {V}\in \mathrm{UnifOn}\left({Y}\right)\right)\to \left({F}\in \left({U}\mathrm{uCn}{V}\right)↔\left({F}:{X}⟶{Y}\wedge \forall {w}\in {V}\phantom{\rule{.4em}{0ex}}\exists {r}\in {U}\phantom{\rule{.4em}{0ex}}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{r}{y}\to {F}\left({x}\right){w}{F}\left({y}\right)\right)\right)\right)$
11 1 2 10 syl2anc ${⊢}{\phi }\to \left({F}\in \left({U}\mathrm{uCn}{V}\right)↔\left({F}:{X}⟶{Y}\wedge \forall {w}\in {V}\phantom{\rule{.4em}{0ex}}\exists {r}\in {U}\phantom{\rule{.4em}{0ex}}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{r}{y}\to {F}\left({x}\right){w}{F}\left({y}\right)\right)\right)\right)$
12 3 11 mpbid ${⊢}{\phi }\to \left({F}:{X}⟶{Y}\wedge \forall {w}\in {V}\phantom{\rule{.4em}{0ex}}\exists {r}\in {U}\phantom{\rule{.4em}{0ex}}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{r}{y}\to {F}\left({x}\right){w}{F}\left({y}\right)\right)\right)$
13 12 simprd ${⊢}{\phi }\to \forall {w}\in {V}\phantom{\rule{.4em}{0ex}}\exists {r}\in {U}\phantom{\rule{.4em}{0ex}}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{r}{y}\to {F}\left({x}\right){w}{F}\left({y}\right)\right)$
14 9 13 4 rspcdva ${⊢}{\phi }\to \exists {r}\in {U}\phantom{\rule{.4em}{0ex}}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{r}{y}\to {F}\left({x}\right){W}{F}\left({y}\right)\right)$
15 simplll ${⊢}\left(\left(\left({\phi }\wedge {r}\in {U}\right)\wedge \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{r}{y}\to {F}\left({x}\right){W}{F}\left({y}\right)\right)\right)\wedge {p}\in {r}\right)\to {\phi }$
16 simplr ${⊢}\left(\left(\left({\phi }\wedge {r}\in {U}\right)\wedge \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{r}{y}\to {F}\left({x}\right){W}{F}\left({y}\right)\right)\right)\wedge {p}\in {r}\right)\to \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{r}{y}\to {F}\left({x}\right){W}{F}\left({y}\right)\right)$
17 ustssxp ${⊢}\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge {r}\in {U}\right)\to {r}\subseteq {X}×{X}$
18 1 17 sylan ${⊢}\left({\phi }\wedge {r}\in {U}\right)\to {r}\subseteq {X}×{X}$
19 18 sselda ${⊢}\left(\left({\phi }\wedge {r}\in {U}\right)\wedge {p}\in {r}\right)\to {p}\in \left({X}×{X}\right)$
20 19 adantlr ${⊢}\left(\left(\left({\phi }\wedge {r}\in {U}\right)\wedge \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{r}{y}\to {F}\left({x}\right){W}{F}\left({y}\right)\right)\right)\wedge {p}\in {r}\right)\to {p}\in \left({X}×{X}\right)$
21 simpr ${⊢}\left(\left(\left({\phi }\wedge {r}\in {U}\right)\wedge \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{r}{y}\to {F}\left({x}\right){W}{F}\left({y}\right)\right)\right)\wedge {p}\in {r}\right)\to {p}\in {r}$
22 simplr ${⊢}\left(\left({\phi }\wedge \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{r}{y}\to {F}\left({x}\right){W}{F}\left({y}\right)\right)\right)\wedge {p}\in \left({X}×{X}\right)\right)\to \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{r}{y}\to {F}\left({x}\right){W}{F}\left({y}\right)\right)$
23 simpr ${⊢}\left({\phi }\wedge {p}\in \left({X}×{X}\right)\right)\to {p}\in \left({X}×{X}\right)$
24 elxp2 ${⊢}{p}\in \left({X}×{X}\right)↔\exists {x}\in {X}\phantom{\rule{.4em}{0ex}}\exists {y}\in {X}\phantom{\rule{.4em}{0ex}}{p}=⟨{x},{y}⟩$
25 23 24 sylib ${⊢}\left({\phi }\wedge {p}\in \left({X}×{X}\right)\right)\to \exists {x}\in {X}\phantom{\rule{.4em}{0ex}}\exists {y}\in {X}\phantom{\rule{.4em}{0ex}}{p}=⟨{x},{y}⟩$
26 simpr ${⊢}\left({\phi }\wedge {p}=⟨{x},{y}⟩\right)\to {p}=⟨{x},{y}⟩$
27 26 eleq1d ${⊢}\left({\phi }\wedge {p}=⟨{x},{y}⟩\right)\to \left({p}\in {r}↔⟨{x},{y}⟩\in {r}\right)$
28 27 adantlr ${⊢}\left(\left({\phi }\wedge {p}\in \left({X}×{X}\right)\right)\wedge {p}=⟨{x},{y}⟩\right)\to \left({p}\in {r}↔⟨{x},{y}⟩\in {r}\right)$
29 df-br ${⊢}{x}{r}{y}↔⟨{x},{y}⟩\in {r}$
30 28 29 syl6bbr ${⊢}\left(\left({\phi }\wedge {p}\in \left({X}×{X}\right)\right)\wedge {p}=⟨{x},{y}⟩\right)\to \left({p}\in {r}↔{x}{r}{y}\right)$
31 simplr ${⊢}\left(\left({\phi }\wedge {p}\in \left({X}×{X}\right)\right)\wedge {p}=⟨{x},{y}⟩\right)\to {p}\in \left({X}×{X}\right)$
32 opex ${⊢}⟨{F}\left({1}^{st}\left({p}\right)\right),{F}\left({2}^{nd}\left({p}\right)\right)⟩\in \mathrm{V}$
33 1 2 3 4 5 ucnimalem ${⊢}{G}=\left({p}\in \left({X}×{X}\right)⟼⟨{F}\left({1}^{st}\left({p}\right)\right),{F}\left({2}^{nd}\left({p}\right)\right)⟩\right)$
34 33 fvmpt2 ${⊢}\left({p}\in \left({X}×{X}\right)\wedge ⟨{F}\left({1}^{st}\left({p}\right)\right),{F}\left({2}^{nd}\left({p}\right)\right)⟩\in \mathrm{V}\right)\to {G}\left({p}\right)=⟨{F}\left({1}^{st}\left({p}\right)\right),{F}\left({2}^{nd}\left({p}\right)\right)⟩$
35 31 32 34 sylancl ${⊢}\left(\left({\phi }\wedge {p}\in \left({X}×{X}\right)\right)\wedge {p}=⟨{x},{y}⟩\right)\to {G}\left({p}\right)=⟨{F}\left({1}^{st}\left({p}\right)\right),{F}\left({2}^{nd}\left({p}\right)\right)⟩$
36 simpr ${⊢}\left(\left({\phi }\wedge {p}\in \left({X}×{X}\right)\right)\wedge {p}=⟨{x},{y}⟩\right)\to {p}=⟨{x},{y}⟩$
37 1st2nd2 ${⊢}{p}\in \left({X}×{X}\right)\to {p}=⟨{1}^{st}\left({p}\right),{2}^{nd}\left({p}\right)⟩$
38 31 37 syl ${⊢}\left(\left({\phi }\wedge {p}\in \left({X}×{X}\right)\right)\wedge {p}=⟨{x},{y}⟩\right)\to {p}=⟨{1}^{st}\left({p}\right),{2}^{nd}\left({p}\right)⟩$
39 36 38 eqtr3d ${⊢}\left(\left({\phi }\wedge {p}\in \left({X}×{X}\right)\right)\wedge {p}=⟨{x},{y}⟩\right)\to ⟨{x},{y}⟩=⟨{1}^{st}\left({p}\right),{2}^{nd}\left({p}\right)⟩$
40 vex ${⊢}{x}\in \mathrm{V}$
41 vex ${⊢}{y}\in \mathrm{V}$
42 40 41 opth ${⊢}⟨{x},{y}⟩=⟨{1}^{st}\left({p}\right),{2}^{nd}\left({p}\right)⟩↔\left({x}={1}^{st}\left({p}\right)\wedge {y}={2}^{nd}\left({p}\right)\right)$
43 39 42 sylib ${⊢}\left(\left({\phi }\wedge {p}\in \left({X}×{X}\right)\right)\wedge {p}=⟨{x},{y}⟩\right)\to \left({x}={1}^{st}\left({p}\right)\wedge {y}={2}^{nd}\left({p}\right)\right)$
44 43 simpld ${⊢}\left(\left({\phi }\wedge {p}\in \left({X}×{X}\right)\right)\wedge {p}=⟨{x},{y}⟩\right)\to {x}={1}^{st}\left({p}\right)$
45 44 fveq2d ${⊢}\left(\left({\phi }\wedge {p}\in \left({X}×{X}\right)\right)\wedge {p}=⟨{x},{y}⟩\right)\to {F}\left({x}\right)={F}\left({1}^{st}\left({p}\right)\right)$
46 43 simprd ${⊢}\left(\left({\phi }\wedge {p}\in \left({X}×{X}\right)\right)\wedge {p}=⟨{x},{y}⟩\right)\to {y}={2}^{nd}\left({p}\right)$
47 46 fveq2d ${⊢}\left(\left({\phi }\wedge {p}\in \left({X}×{X}\right)\right)\wedge {p}=⟨{x},{y}⟩\right)\to {F}\left({y}\right)={F}\left({2}^{nd}\left({p}\right)\right)$
48 45 47 opeq12d ${⊢}\left(\left({\phi }\wedge {p}\in \left({X}×{X}\right)\right)\wedge {p}=⟨{x},{y}⟩\right)\to ⟨{F}\left({x}\right),{F}\left({y}\right)⟩=⟨{F}\left({1}^{st}\left({p}\right)\right),{F}\left({2}^{nd}\left({p}\right)\right)⟩$
49 35 48 eqtr4d ${⊢}\left(\left({\phi }\wedge {p}\in \left({X}×{X}\right)\right)\wedge {p}=⟨{x},{y}⟩\right)\to {G}\left({p}\right)=⟨{F}\left({x}\right),{F}\left({y}\right)⟩$
50 49 eleq1d ${⊢}\left(\left({\phi }\wedge {p}\in \left({X}×{X}\right)\right)\wedge {p}=⟨{x},{y}⟩\right)\to \left({G}\left({p}\right)\in {W}↔⟨{F}\left({x}\right),{F}\left({y}\right)⟩\in {W}\right)$
51 df-br ${⊢}{F}\left({x}\right){W}{F}\left({y}\right)↔⟨{F}\left({x}\right),{F}\left({y}\right)⟩\in {W}$
52 50 51 syl6bbr ${⊢}\left(\left({\phi }\wedge {p}\in \left({X}×{X}\right)\right)\wedge {p}=⟨{x},{y}⟩\right)\to \left({G}\left({p}\right)\in {W}↔{F}\left({x}\right){W}{F}\left({y}\right)\right)$
53 30 52 imbi12d ${⊢}\left(\left({\phi }\wedge {p}\in \left({X}×{X}\right)\right)\wedge {p}=⟨{x},{y}⟩\right)\to \left(\left({p}\in {r}\to {G}\left({p}\right)\in {W}\right)↔\left({x}{r}{y}\to {F}\left({x}\right){W}{F}\left({y}\right)\right)\right)$
54 53 exbiri ${⊢}\left({\phi }\wedge {p}\in \left({X}×{X}\right)\right)\to \left({p}=⟨{x},{y}⟩\to \left(\left({x}{r}{y}\to {F}\left({x}\right){W}{F}\left({y}\right)\right)\to \left({p}\in {r}\to {G}\left({p}\right)\in {W}\right)\right)\right)$
55 54 reximdv ${⊢}\left({\phi }\wedge {p}\in \left({X}×{X}\right)\right)\to \left(\exists {y}\in {X}\phantom{\rule{.4em}{0ex}}{p}=⟨{x},{y}⟩\to \exists {y}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left({x}{r}{y}\to {F}\left({x}\right){W}{F}\left({y}\right)\right)\to \left({p}\in {r}\to {G}\left({p}\right)\in {W}\right)\right)\right)$
56 55 reximdv ${⊢}\left({\phi }\wedge {p}\in \left({X}×{X}\right)\right)\to \left(\exists {x}\in {X}\phantom{\rule{.4em}{0ex}}\exists {y}\in {X}\phantom{\rule{.4em}{0ex}}{p}=⟨{x},{y}⟩\to \exists {x}\in {X}\phantom{\rule{.4em}{0ex}}\exists {y}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left({x}{r}{y}\to {F}\left({x}\right){W}{F}\left({y}\right)\right)\to \left({p}\in {r}\to {G}\left({p}\right)\in {W}\right)\right)\right)$
57 25 56 mpd ${⊢}\left({\phi }\wedge {p}\in \left({X}×{X}\right)\right)\to \exists {x}\in {X}\phantom{\rule{.4em}{0ex}}\exists {y}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left({x}{r}{y}\to {F}\left({x}\right){W}{F}\left({y}\right)\right)\to \left({p}\in {r}\to {G}\left({p}\right)\in {W}\right)\right)$
58 57 adantlr ${⊢}\left(\left({\phi }\wedge \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{r}{y}\to {F}\left({x}\right){W}{F}\left({y}\right)\right)\right)\wedge {p}\in \left({X}×{X}\right)\right)\to \exists {x}\in {X}\phantom{\rule{.4em}{0ex}}\exists {y}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left({x}{r}{y}\to {F}\left({x}\right){W}{F}\left({y}\right)\right)\to \left({p}\in {r}\to {G}\left({p}\right)\in {W}\right)\right)$
59 22 58 r19.29d2r ${⊢}\left(\left({\phi }\wedge \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{r}{y}\to {F}\left({x}\right){W}{F}\left({y}\right)\right)\right)\wedge {p}\in \left({X}×{X}\right)\right)\to \exists {x}\in {X}\phantom{\rule{.4em}{0ex}}\exists {y}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left({x}{r}{y}\to {F}\left({x}\right){W}{F}\left({y}\right)\right)\wedge \left(\left({x}{r}{y}\to {F}\left({x}\right){W}{F}\left({y}\right)\right)\to \left({p}\in {r}\to {G}\left({p}\right)\in {W}\right)\right)\right)$
60 pm3.35 ${⊢}\left(\left({x}{r}{y}\to {F}\left({x}\right){W}{F}\left({y}\right)\right)\wedge \left(\left({x}{r}{y}\to {F}\left({x}\right){W}{F}\left({y}\right)\right)\to \left({p}\in {r}\to {G}\left({p}\right)\in {W}\right)\right)\right)\to \left({p}\in {r}\to {G}\left({p}\right)\in {W}\right)$
61 60 rexlimivw ${⊢}\exists {y}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left({x}{r}{y}\to {F}\left({x}\right){W}{F}\left({y}\right)\right)\wedge \left(\left({x}{r}{y}\to {F}\left({x}\right){W}{F}\left({y}\right)\right)\to \left({p}\in {r}\to {G}\left({p}\right)\in {W}\right)\right)\right)\to \left({p}\in {r}\to {G}\left({p}\right)\in {W}\right)$
62 61 rexlimivw ${⊢}\exists {x}\in {X}\phantom{\rule{.4em}{0ex}}\exists {y}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left({x}{r}{y}\to {F}\left({x}\right){W}{F}\left({y}\right)\right)\wedge \left(\left({x}{r}{y}\to {F}\left({x}\right){W}{F}\left({y}\right)\right)\to \left({p}\in {r}\to {G}\left({p}\right)\in {W}\right)\right)\right)\to \left({p}\in {r}\to {G}\left({p}\right)\in {W}\right)$
63 59 62 syl ${⊢}\left(\left({\phi }\wedge \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{r}{y}\to {F}\left({x}\right){W}{F}\left({y}\right)\right)\right)\wedge {p}\in \left({X}×{X}\right)\right)\to \left({p}\in {r}\to {G}\left({p}\right)\in {W}\right)$
64 63 imp ${⊢}\left(\left(\left({\phi }\wedge \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{r}{y}\to {F}\left({x}\right){W}{F}\left({y}\right)\right)\right)\wedge {p}\in \left({X}×{X}\right)\right)\wedge {p}\in {r}\right)\to {G}\left({p}\right)\in {W}$
65 15 16 20 21 64 syl1111anc ${⊢}\left(\left(\left({\phi }\wedge {r}\in {U}\right)\wedge \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{r}{y}\to {F}\left({x}\right){W}{F}\left({y}\right)\right)\right)\wedge {p}\in {r}\right)\to {G}\left({p}\right)\in {W}$
66 65 ralrimiva ${⊢}\left(\left({\phi }\wedge {r}\in {U}\right)\wedge \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{r}{y}\to {F}\left({x}\right){W}{F}\left({y}\right)\right)\right)\to \forall {p}\in {r}\phantom{\rule{.4em}{0ex}}{G}\left({p}\right)\in {W}$
67 66 ex ${⊢}\left({\phi }\wedge {r}\in {U}\right)\to \left(\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{r}{y}\to {F}\left({x}\right){W}{F}\left({y}\right)\right)\to \forall {p}\in {r}\phantom{\rule{.4em}{0ex}}{G}\left({p}\right)\in {W}\right)$
68 67 reximdva ${⊢}{\phi }\to \left(\exists {r}\in {U}\phantom{\rule{.4em}{0ex}}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{r}{y}\to {F}\left({x}\right){W}{F}\left({y}\right)\right)\to \exists {r}\in {U}\phantom{\rule{.4em}{0ex}}\forall {p}\in {r}\phantom{\rule{.4em}{0ex}}{G}\left({p}\right)\in {W}\right)$
69 14 68 mpd ${⊢}{\phi }\to \exists {r}\in {U}\phantom{\rule{.4em}{0ex}}\forall {p}\in {r}\phantom{\rule{.4em}{0ex}}{G}\left({p}\right)\in {W}$
70 5 mpofun ${⊢}\mathrm{Fun}{G}$
71 opex ${⊢}⟨{F}\left({x}\right),{F}\left({y}\right)⟩\in \mathrm{V}$
72 5 71 dmmpo ${⊢}\mathrm{dom}{G}={X}×{X}$
73 18 72 sseqtrrdi ${⊢}\left({\phi }\wedge {r}\in {U}\right)\to {r}\subseteq \mathrm{dom}{G}$
74 funimass4 ${⊢}\left(\mathrm{Fun}{G}\wedge {r}\subseteq \mathrm{dom}{G}\right)\to \left({G}\left[{r}\right]\subseteq {W}↔\forall {p}\in {r}\phantom{\rule{.4em}{0ex}}{G}\left({p}\right)\in {W}\right)$
75 70 73 74 sylancr ${⊢}\left({\phi }\wedge {r}\in {U}\right)\to \left({G}\left[{r}\right]\subseteq {W}↔\forall {p}\in {r}\phantom{\rule{.4em}{0ex}}{G}\left({p}\right)\in {W}\right)$
76 75 biimprd ${⊢}\left({\phi }\wedge {r}\in {U}\right)\to \left(\forall {p}\in {r}\phantom{\rule{.4em}{0ex}}{G}\left({p}\right)\in {W}\to {G}\left[{r}\right]\subseteq {W}\right)$
77 76 ralrimiva ${⊢}{\phi }\to \forall {r}\in {U}\phantom{\rule{.4em}{0ex}}\left(\forall {p}\in {r}\phantom{\rule{.4em}{0ex}}{G}\left({p}\right)\in {W}\to {G}\left[{r}\right]\subseteq {W}\right)$
78 r19.29r ${⊢}\left(\exists {r}\in {U}\phantom{\rule{.4em}{0ex}}\forall {p}\in {r}\phantom{\rule{.4em}{0ex}}{G}\left({p}\right)\in {W}\wedge \forall {r}\in {U}\phantom{\rule{.4em}{0ex}}\left(\forall {p}\in {r}\phantom{\rule{.4em}{0ex}}{G}\left({p}\right)\in {W}\to {G}\left[{r}\right]\subseteq {W}\right)\right)\to \exists {r}\in {U}\phantom{\rule{.4em}{0ex}}\left(\forall {p}\in {r}\phantom{\rule{.4em}{0ex}}{G}\left({p}\right)\in {W}\wedge \left(\forall {p}\in {r}\phantom{\rule{.4em}{0ex}}{G}\left({p}\right)\in {W}\to {G}\left[{r}\right]\subseteq {W}\right)\right)$
79 69 77 78 syl2anc ${⊢}{\phi }\to \exists {r}\in {U}\phantom{\rule{.4em}{0ex}}\left(\forall {p}\in {r}\phantom{\rule{.4em}{0ex}}{G}\left({p}\right)\in {W}\wedge \left(\forall {p}\in {r}\phantom{\rule{.4em}{0ex}}{G}\left({p}\right)\in {W}\to {G}\left[{r}\right]\subseteq {W}\right)\right)$
80 pm3.35 ${⊢}\left(\forall {p}\in {r}\phantom{\rule{.4em}{0ex}}{G}\left({p}\right)\in {W}\wedge \left(\forall {p}\in {r}\phantom{\rule{.4em}{0ex}}{G}\left({p}\right)\in {W}\to {G}\left[{r}\right]\subseteq {W}\right)\right)\to {G}\left[{r}\right]\subseteq {W}$
81 80 reximi ${⊢}\exists {r}\in {U}\phantom{\rule{.4em}{0ex}}\left(\forall {p}\in {r}\phantom{\rule{.4em}{0ex}}{G}\left({p}\right)\in {W}\wedge \left(\forall {p}\in {r}\phantom{\rule{.4em}{0ex}}{G}\left({p}\right)\in {W}\to {G}\left[{r}\right]\subseteq {W}\right)\right)\to \exists {r}\in {U}\phantom{\rule{.4em}{0ex}}{G}\left[{r}\right]\subseteq {W}$
82 79 81 syl ${⊢}{\phi }\to \exists {r}\in {U}\phantom{\rule{.4em}{0ex}}{G}\left[{r}\right]\subseteq {W}$