Metamath Proof Explorer

Theorem 3vfriswmgrlem

Description: Lemma for 3vfriswmgr . (Contributed by Alexander van der Vekens, 6-Oct-2017) (Revised by AV, 31-Mar-2021)

Ref Expression
Hypotheses 3vfriswmgr.v ${⊢}{V}=\mathrm{Vtx}\left({G}\right)$
3vfriswmgr.e ${⊢}{E}=\mathrm{Edg}\left({G}\right)$
Assertion 3vfriswmgrlem ${⊢}\left(\left({A}\in {X}\wedge {B}\in {Y}\wedge {A}\ne {B}\right)\wedge \left({V}=\left\{{A},{B},{C}\right\}\wedge {G}\in \mathrm{USGraph}\right)\right)\to \left(\left\{{A},{B}\right\}\in {E}\to \exists !{w}\in \left\{{A},{B}\right\}\phantom{\rule{.4em}{0ex}}\left\{{A},{w}\right\}\in {E}\right)$

Proof

Step Hyp Ref Expression
1 3vfriswmgr.v ${⊢}{V}=\mathrm{Vtx}\left({G}\right)$
2 3vfriswmgr.e ${⊢}{E}=\mathrm{Edg}\left({G}\right)$
3 animorr ${⊢}\left(\left(\left({A}\in {X}\wedge {B}\in {Y}\wedge {A}\ne {B}\right)\wedge \left({V}=\left\{{A},{B},{C}\right\}\wedge {G}\in \mathrm{USGraph}\right)\right)\wedge \left\{{A},{B}\right\}\in {E}\right)\to \left(\left\{{A},{A}\right\}\in {E}\vee \left\{{A},{B}\right\}\in {E}\right)$
4 preq2 ${⊢}{w}={A}\to \left\{{A},{w}\right\}=\left\{{A},{A}\right\}$
5 4 eleq1d ${⊢}{w}={A}\to \left(\left\{{A},{w}\right\}\in {E}↔\left\{{A},{A}\right\}\in {E}\right)$
6 preq2 ${⊢}{w}={B}\to \left\{{A},{w}\right\}=\left\{{A},{B}\right\}$
7 6 eleq1d ${⊢}{w}={B}\to \left(\left\{{A},{w}\right\}\in {E}↔\left\{{A},{B}\right\}\in {E}\right)$
8 5 7 rexprg ${⊢}\left({A}\in {X}\wedge {B}\in {Y}\right)\to \left(\exists {w}\in \left\{{A},{B}\right\}\phantom{\rule{.4em}{0ex}}\left\{{A},{w}\right\}\in {E}↔\left(\left\{{A},{A}\right\}\in {E}\vee \left\{{A},{B}\right\}\in {E}\right)\right)$
9 8 3adant3 ${⊢}\left({A}\in {X}\wedge {B}\in {Y}\wedge {A}\ne {B}\right)\to \left(\exists {w}\in \left\{{A},{B}\right\}\phantom{\rule{.4em}{0ex}}\left\{{A},{w}\right\}\in {E}↔\left(\left\{{A},{A}\right\}\in {E}\vee \left\{{A},{B}\right\}\in {E}\right)\right)$
10 9 ad2antrr ${⊢}\left(\left(\left({A}\in {X}\wedge {B}\in {Y}\wedge {A}\ne {B}\right)\wedge \left({V}=\left\{{A},{B},{C}\right\}\wedge {G}\in \mathrm{USGraph}\right)\right)\wedge \left\{{A},{B}\right\}\in {E}\right)\to \left(\exists {w}\in \left\{{A},{B}\right\}\phantom{\rule{.4em}{0ex}}\left\{{A},{w}\right\}\in {E}↔\left(\left\{{A},{A}\right\}\in {E}\vee \left\{{A},{B}\right\}\in {E}\right)\right)$
11 3 10 mpbird ${⊢}\left(\left(\left({A}\in {X}\wedge {B}\in {Y}\wedge {A}\ne {B}\right)\wedge \left({V}=\left\{{A},{B},{C}\right\}\wedge {G}\in \mathrm{USGraph}\right)\right)\wedge \left\{{A},{B}\right\}\in {E}\right)\to \exists {w}\in \left\{{A},{B}\right\}\phantom{\rule{.4em}{0ex}}\left\{{A},{w}\right\}\in {E}$
12 df-rex ${⊢}\exists {w}\in \left\{{A},{B}\right\}\phantom{\rule{.4em}{0ex}}\left\{{A},{w}\right\}\in {E}↔\exists {w}\phantom{\rule{.4em}{0ex}}\left({w}\in \left\{{A},{B}\right\}\wedge \left\{{A},{w}\right\}\in {E}\right)$
13 11 12 sylib ${⊢}\left(\left(\left({A}\in {X}\wedge {B}\in {Y}\wedge {A}\ne {B}\right)\wedge \left({V}=\left\{{A},{B},{C}\right\}\wedge {G}\in \mathrm{USGraph}\right)\right)\wedge \left\{{A},{B}\right\}\in {E}\right)\to \exists {w}\phantom{\rule{.4em}{0ex}}\left({w}\in \left\{{A},{B}\right\}\wedge \left\{{A},{w}\right\}\in {E}\right)$
14 vex ${⊢}{w}\in \mathrm{V}$
15 14 elpr ${⊢}{w}\in \left\{{A},{B}\right\}↔\left({w}={A}\vee {w}={B}\right)$
16 vex ${⊢}{y}\in \mathrm{V}$
17 16 elpr ${⊢}{y}\in \left\{{A},{B}\right\}↔\left({y}={A}\vee {y}={B}\right)$
18 eqidd ${⊢}\left(\left(\left({A}\in {X}\wedge {B}\in {Y}\wedge {A}\ne {B}\right)\wedge \left({V}=\left\{{A},{B},{C}\right\}\wedge {G}\in \mathrm{USGraph}\right)\right)\wedge \left\{{A},{B}\right\}\in {E}\right)\to {A}={A}$
19 18 a1i ${⊢}\left\{{A},{A}\right\}\in {E}\to \left(\left(\left(\left({A}\in {X}\wedge {B}\in {Y}\wedge {A}\ne {B}\right)\wedge \left({V}=\left\{{A},{B},{C}\right\}\wedge {G}\in \mathrm{USGraph}\right)\right)\wedge \left\{{A},{B}\right\}\in {E}\right)\to {A}={A}\right)$
20 19 a1i13 ${⊢}{y}={A}\to \left(\left\{{A},{A}\right\}\in {E}\to \left(\left\{{A},{A}\right\}\in {E}\to \left(\left(\left(\left({A}\in {X}\wedge {B}\in {Y}\wedge {A}\ne {B}\right)\wedge \left({V}=\left\{{A},{B},{C}\right\}\wedge {G}\in \mathrm{USGraph}\right)\right)\wedge \left\{{A},{B}\right\}\in {E}\right)\to {A}={A}\right)\right)\right)$
21 preq2 ${⊢}{y}={A}\to \left\{{A},{y}\right\}=\left\{{A},{A}\right\}$
22 21 eleq1d ${⊢}{y}={A}\to \left(\left\{{A},{y}\right\}\in {E}↔\left\{{A},{A}\right\}\in {E}\right)$
23 eqeq2 ${⊢}{y}={A}\to \left({A}={y}↔{A}={A}\right)$
24 23 imbi2d ${⊢}{y}={A}\to \left(\left(\left(\left(\left({A}\in {X}\wedge {B}\in {Y}\wedge {A}\ne {B}\right)\wedge \left({V}=\left\{{A},{B},{C}\right\}\wedge {G}\in \mathrm{USGraph}\right)\right)\wedge \left\{{A},{B}\right\}\in {E}\right)\to {A}={y}\right)↔\left(\left(\left(\left({A}\in {X}\wedge {B}\in {Y}\wedge {A}\ne {B}\right)\wedge \left({V}=\left\{{A},{B},{C}\right\}\wedge {G}\in \mathrm{USGraph}\right)\right)\wedge \left\{{A},{B}\right\}\in {E}\right)\to {A}={A}\right)\right)$
25 24 imbi2d ${⊢}{y}={A}\to \left(\left(\left\{{A},{A}\right\}\in {E}\to \left(\left(\left(\left({A}\in {X}\wedge {B}\in {Y}\wedge {A}\ne {B}\right)\wedge \left({V}=\left\{{A},{B},{C}\right\}\wedge {G}\in \mathrm{USGraph}\right)\right)\wedge \left\{{A},{B}\right\}\in {E}\right)\to {A}={y}\right)\right)↔\left(\left\{{A},{A}\right\}\in {E}\to \left(\left(\left(\left({A}\in {X}\wedge {B}\in {Y}\wedge {A}\ne {B}\right)\wedge \left({V}=\left\{{A},{B},{C}\right\}\wedge {G}\in \mathrm{USGraph}\right)\right)\wedge \left\{{A},{B}\right\}\in {E}\right)\to {A}={A}\right)\right)\right)$
26 20 22 25 3imtr4d ${⊢}{y}={A}\to \left(\left\{{A},{y}\right\}\in {E}\to \left(\left\{{A},{A}\right\}\in {E}\to \left(\left(\left(\left({A}\in {X}\wedge {B}\in {Y}\wedge {A}\ne {B}\right)\wedge \left({V}=\left\{{A},{B},{C}\right\}\wedge {G}\in \mathrm{USGraph}\right)\right)\wedge \left\{{A},{B}\right\}\in {E}\right)\to {A}={y}\right)\right)\right)$
27 2 usgredgne ${⊢}\left({G}\in \mathrm{USGraph}\wedge \left\{{A},{A}\right\}\in {E}\right)\to {A}\ne {A}$
28 27 adantll ${⊢}\left(\left({V}=\left\{{A},{B},{C}\right\}\wedge {G}\in \mathrm{USGraph}\right)\wedge \left\{{A},{A}\right\}\in {E}\right)\to {A}\ne {A}$
29 df-ne ${⊢}{A}\ne {A}↔¬{A}={A}$
30 eqid ${⊢}{A}={A}$
31 30 pm2.24i ${⊢}¬{A}={A}\to {A}={B}$
32 29 31 sylbi ${⊢}{A}\ne {A}\to {A}={B}$
33 28 32 syl ${⊢}\left(\left({V}=\left\{{A},{B},{C}\right\}\wedge {G}\in \mathrm{USGraph}\right)\wedge \left\{{A},{A}\right\}\in {E}\right)\to {A}={B}$
34 33 ex ${⊢}\left({V}=\left\{{A},{B},{C}\right\}\wedge {G}\in \mathrm{USGraph}\right)\to \left(\left\{{A},{A}\right\}\in {E}\to {A}={B}\right)$
35 34 ad2antlr ${⊢}\left(\left(\left({A}\in {X}\wedge {B}\in {Y}\wedge {A}\ne {B}\right)\wedge \left({V}=\left\{{A},{B},{C}\right\}\wedge {G}\in \mathrm{USGraph}\right)\right)\wedge \left\{{A},{B}\right\}\in {E}\right)\to \left(\left\{{A},{A}\right\}\in {E}\to {A}={B}\right)$
36 35 com12 ${⊢}\left\{{A},{A}\right\}\in {E}\to \left(\left(\left(\left({A}\in {X}\wedge {B}\in {Y}\wedge {A}\ne {B}\right)\wedge \left({V}=\left\{{A},{B},{C}\right\}\wedge {G}\in \mathrm{USGraph}\right)\right)\wedge \left\{{A},{B}\right\}\in {E}\right)\to {A}={B}\right)$
37 36 2a1i ${⊢}{y}={B}\to \left(\left\{{A},{B}\right\}\in {E}\to \left(\left\{{A},{A}\right\}\in {E}\to \left(\left(\left(\left({A}\in {X}\wedge {B}\in {Y}\wedge {A}\ne {B}\right)\wedge \left({V}=\left\{{A},{B},{C}\right\}\wedge {G}\in \mathrm{USGraph}\right)\right)\wedge \left\{{A},{B}\right\}\in {E}\right)\to {A}={B}\right)\right)\right)$
38 preq2 ${⊢}{y}={B}\to \left\{{A},{y}\right\}=\left\{{A},{B}\right\}$
39 38 eleq1d ${⊢}{y}={B}\to \left(\left\{{A},{y}\right\}\in {E}↔\left\{{A},{B}\right\}\in {E}\right)$
40 eqeq2 ${⊢}{y}={B}\to \left({A}={y}↔{A}={B}\right)$
41 40 imbi2d ${⊢}{y}={B}\to \left(\left(\left(\left(\left({A}\in {X}\wedge {B}\in {Y}\wedge {A}\ne {B}\right)\wedge \left({V}=\left\{{A},{B},{C}\right\}\wedge {G}\in \mathrm{USGraph}\right)\right)\wedge \left\{{A},{B}\right\}\in {E}\right)\to {A}={y}\right)↔\left(\left(\left(\left({A}\in {X}\wedge {B}\in {Y}\wedge {A}\ne {B}\right)\wedge \left({V}=\left\{{A},{B},{C}\right\}\wedge {G}\in \mathrm{USGraph}\right)\right)\wedge \left\{{A},{B}\right\}\in {E}\right)\to {A}={B}\right)\right)$
42 41 imbi2d ${⊢}{y}={B}\to \left(\left(\left\{{A},{A}\right\}\in {E}\to \left(\left(\left(\left({A}\in {X}\wedge {B}\in {Y}\wedge {A}\ne {B}\right)\wedge \left({V}=\left\{{A},{B},{C}\right\}\wedge {G}\in \mathrm{USGraph}\right)\right)\wedge \left\{{A},{B}\right\}\in {E}\right)\to {A}={y}\right)\right)↔\left(\left\{{A},{A}\right\}\in {E}\to \left(\left(\left(\left({A}\in {X}\wedge {B}\in {Y}\wedge {A}\ne {B}\right)\wedge \left({V}=\left\{{A},{B},{C}\right\}\wedge {G}\in \mathrm{USGraph}\right)\right)\wedge \left\{{A},{B}\right\}\in {E}\right)\to {A}={B}\right)\right)\right)$
43 37 39 42 3imtr4d ${⊢}{y}={B}\to \left(\left\{{A},{y}\right\}\in {E}\to \left(\left\{{A},{A}\right\}\in {E}\to \left(\left(\left(\left({A}\in {X}\wedge {B}\in {Y}\wedge {A}\ne {B}\right)\wedge \left({V}=\left\{{A},{B},{C}\right\}\wedge {G}\in \mathrm{USGraph}\right)\right)\wedge \left\{{A},{B}\right\}\in {E}\right)\to {A}={y}\right)\right)\right)$
44 26 43 jaoi ${⊢}\left({y}={A}\vee {y}={B}\right)\to \left(\left\{{A},{y}\right\}\in {E}\to \left(\left\{{A},{A}\right\}\in {E}\to \left(\left(\left(\left({A}\in {X}\wedge {B}\in {Y}\wedge {A}\ne {B}\right)\wedge \left({V}=\left\{{A},{B},{C}\right\}\wedge {G}\in \mathrm{USGraph}\right)\right)\wedge \left\{{A},{B}\right\}\in {E}\right)\to {A}={y}\right)\right)\right)$
45 eqeq1 ${⊢}{w}={A}\to \left({w}={y}↔{A}={y}\right)$
46 45 imbi2d ${⊢}{w}={A}\to \left(\left(\left(\left(\left({A}\in {X}\wedge {B}\in {Y}\wedge {A}\ne {B}\right)\wedge \left({V}=\left\{{A},{B},{C}\right\}\wedge {G}\in \mathrm{USGraph}\right)\right)\wedge \left\{{A},{B}\right\}\in {E}\right)\to {w}={y}\right)↔\left(\left(\left(\left({A}\in {X}\wedge {B}\in {Y}\wedge {A}\ne {B}\right)\wedge \left({V}=\left\{{A},{B},{C}\right\}\wedge {G}\in \mathrm{USGraph}\right)\right)\wedge \left\{{A},{B}\right\}\in {E}\right)\to {A}={y}\right)\right)$
47 5 46 imbi12d ${⊢}{w}={A}\to \left(\left(\left\{{A},{w}\right\}\in {E}\to \left(\left(\left(\left({A}\in {X}\wedge {B}\in {Y}\wedge {A}\ne {B}\right)\wedge \left({V}=\left\{{A},{B},{C}\right\}\wedge {G}\in \mathrm{USGraph}\right)\right)\wedge \left\{{A},{B}\right\}\in {E}\right)\to {w}={y}\right)\right)↔\left(\left\{{A},{A}\right\}\in {E}\to \left(\left(\left(\left({A}\in {X}\wedge {B}\in {Y}\wedge {A}\ne {B}\right)\wedge \left({V}=\left\{{A},{B},{C}\right\}\wedge {G}\in \mathrm{USGraph}\right)\right)\wedge \left\{{A},{B}\right\}\in {E}\right)\to {A}={y}\right)\right)\right)$
48 47 imbi2d ${⊢}{w}={A}\to \left(\left(\left\{{A},{y}\right\}\in {E}\to \left(\left\{{A},{w}\right\}\in {E}\to \left(\left(\left(\left({A}\in {X}\wedge {B}\in {Y}\wedge {A}\ne {B}\right)\wedge \left({V}=\left\{{A},{B},{C}\right\}\wedge {G}\in \mathrm{USGraph}\right)\right)\wedge \left\{{A},{B}\right\}\in {E}\right)\to {w}={y}\right)\right)\right)↔\left(\left\{{A},{y}\right\}\in {E}\to \left(\left\{{A},{A}\right\}\in {E}\to \left(\left(\left(\left({A}\in {X}\wedge {B}\in {Y}\wedge {A}\ne {B}\right)\wedge \left({V}=\left\{{A},{B},{C}\right\}\wedge {G}\in \mathrm{USGraph}\right)\right)\wedge \left\{{A},{B}\right\}\in {E}\right)\to {A}={y}\right)\right)\right)\right)$
49 44 48 syl5ibr ${⊢}{w}={A}\to \left(\left({y}={A}\vee {y}={B}\right)\to \left(\left\{{A},{y}\right\}\in {E}\to \left(\left\{{A},{w}\right\}\in {E}\to \left(\left(\left(\left({A}\in {X}\wedge {B}\in {Y}\wedge {A}\ne {B}\right)\wedge \left({V}=\left\{{A},{B},{C}\right\}\wedge {G}\in \mathrm{USGraph}\right)\right)\wedge \left\{{A},{B}\right\}\in {E}\right)\to {w}={y}\right)\right)\right)\right)$
50 30 pm2.24i ${⊢}¬{A}={A}\to {B}={A}$
51 29 50 sylbi ${⊢}{A}\ne {A}\to {B}={A}$
52 28 51 syl ${⊢}\left(\left({V}=\left\{{A},{B},{C}\right\}\wedge {G}\in \mathrm{USGraph}\right)\wedge \left\{{A},{A}\right\}\in {E}\right)\to {B}={A}$
53 52 ex ${⊢}\left({V}=\left\{{A},{B},{C}\right\}\wedge {G}\in \mathrm{USGraph}\right)\to \left(\left\{{A},{A}\right\}\in {E}\to {B}={A}\right)$
54 53 ad2antlr ${⊢}\left(\left(\left({A}\in {X}\wedge {B}\in {Y}\wedge {A}\ne {B}\right)\wedge \left({V}=\left\{{A},{B},{C}\right\}\wedge {G}\in \mathrm{USGraph}\right)\right)\wedge \left\{{A},{B}\right\}\in {E}\right)\to \left(\left\{{A},{A}\right\}\in {E}\to {B}={A}\right)$
55 54 com12 ${⊢}\left\{{A},{A}\right\}\in {E}\to \left(\left(\left(\left({A}\in {X}\wedge {B}\in {Y}\wedge {A}\ne {B}\right)\wedge \left({V}=\left\{{A},{B},{C}\right\}\wedge {G}\in \mathrm{USGraph}\right)\right)\wedge \left\{{A},{B}\right\}\in {E}\right)\to {B}={A}\right)$
56 55 a1i13 ${⊢}{y}={A}\to \left(\left\{{A},{A}\right\}\in {E}\to \left(\left\{{A},{B}\right\}\in {E}\to \left(\left(\left(\left({A}\in {X}\wedge {B}\in {Y}\wedge {A}\ne {B}\right)\wedge \left({V}=\left\{{A},{B},{C}\right\}\wedge {G}\in \mathrm{USGraph}\right)\right)\wedge \left\{{A},{B}\right\}\in {E}\right)\to {B}={A}\right)\right)\right)$
57 eqeq2 ${⊢}{y}={A}\to \left({B}={y}↔{B}={A}\right)$
58 57 imbi2d ${⊢}{y}={A}\to \left(\left(\left(\left(\left({A}\in {X}\wedge {B}\in {Y}\wedge {A}\ne {B}\right)\wedge \left({V}=\left\{{A},{B},{C}\right\}\wedge {G}\in \mathrm{USGraph}\right)\right)\wedge \left\{{A},{B}\right\}\in {E}\right)\to {B}={y}\right)↔\left(\left(\left(\left({A}\in {X}\wedge {B}\in {Y}\wedge {A}\ne {B}\right)\wedge \left({V}=\left\{{A},{B},{C}\right\}\wedge {G}\in \mathrm{USGraph}\right)\right)\wedge \left\{{A},{B}\right\}\in {E}\right)\to {B}={A}\right)\right)$
59 58 imbi2d ${⊢}{y}={A}\to \left(\left(\left\{{A},{B}\right\}\in {E}\to \left(\left(\left(\left({A}\in {X}\wedge {B}\in {Y}\wedge {A}\ne {B}\right)\wedge \left({V}=\left\{{A},{B},{C}\right\}\wedge {G}\in \mathrm{USGraph}\right)\right)\wedge \left\{{A},{B}\right\}\in {E}\right)\to {B}={y}\right)\right)↔\left(\left\{{A},{B}\right\}\in {E}\to \left(\left(\left(\left({A}\in {X}\wedge {B}\in {Y}\wedge {A}\ne {B}\right)\wedge \left({V}=\left\{{A},{B},{C}\right\}\wedge {G}\in \mathrm{USGraph}\right)\right)\wedge \left\{{A},{B}\right\}\in {E}\right)\to {B}={A}\right)\right)\right)$
60 56 22 59 3imtr4d ${⊢}{y}={A}\to \left(\left\{{A},{y}\right\}\in {E}\to \left(\left\{{A},{B}\right\}\in {E}\to \left(\left(\left(\left({A}\in {X}\wedge {B}\in {Y}\wedge {A}\ne {B}\right)\wedge \left({V}=\left\{{A},{B},{C}\right\}\wedge {G}\in \mathrm{USGraph}\right)\right)\wedge \left\{{A},{B}\right\}\in {E}\right)\to {B}={y}\right)\right)\right)$
61 eqidd ${⊢}\left(\left(\left({A}\in {X}\wedge {B}\in {Y}\wedge {A}\ne {B}\right)\wedge \left({V}=\left\{{A},{B},{C}\right\}\wedge {G}\in \mathrm{USGraph}\right)\right)\wedge \left\{{A},{B}\right\}\in {E}\right)\to {B}={B}$
62 61 a1i ${⊢}\left\{{A},{B}\right\}\in {E}\to \left(\left(\left(\left({A}\in {X}\wedge {B}\in {Y}\wedge {A}\ne {B}\right)\wedge \left({V}=\left\{{A},{B},{C}\right\}\wedge {G}\in \mathrm{USGraph}\right)\right)\wedge \left\{{A},{B}\right\}\in {E}\right)\to {B}={B}\right)$
63 62 a1i13 ${⊢}{y}={B}\to \left(\left\{{A},{B}\right\}\in {E}\to \left(\left\{{A},{B}\right\}\in {E}\to \left(\left(\left(\left({A}\in {X}\wedge {B}\in {Y}\wedge {A}\ne {B}\right)\wedge \left({V}=\left\{{A},{B},{C}\right\}\wedge {G}\in \mathrm{USGraph}\right)\right)\wedge \left\{{A},{B}\right\}\in {E}\right)\to {B}={B}\right)\right)\right)$
64 eqeq2 ${⊢}{y}={B}\to \left({B}={y}↔{B}={B}\right)$
65 64 imbi2d ${⊢}{y}={B}\to \left(\left(\left(\left(\left({A}\in {X}\wedge {B}\in {Y}\wedge {A}\ne {B}\right)\wedge \left({V}=\left\{{A},{B},{C}\right\}\wedge {G}\in \mathrm{USGraph}\right)\right)\wedge \left\{{A},{B}\right\}\in {E}\right)\to {B}={y}\right)↔\left(\left(\left(\left({A}\in {X}\wedge {B}\in {Y}\wedge {A}\ne {B}\right)\wedge \left({V}=\left\{{A},{B},{C}\right\}\wedge {G}\in \mathrm{USGraph}\right)\right)\wedge \left\{{A},{B}\right\}\in {E}\right)\to {B}={B}\right)\right)$
66 65 imbi2d ${⊢}{y}={B}\to \left(\left(\left\{{A},{B}\right\}\in {E}\to \left(\left(\left(\left({A}\in {X}\wedge {B}\in {Y}\wedge {A}\ne {B}\right)\wedge \left({V}=\left\{{A},{B},{C}\right\}\wedge {G}\in \mathrm{USGraph}\right)\right)\wedge \left\{{A},{B}\right\}\in {E}\right)\to {B}={y}\right)\right)↔\left(\left\{{A},{B}\right\}\in {E}\to \left(\left(\left(\left({A}\in {X}\wedge {B}\in {Y}\wedge {A}\ne {B}\right)\wedge \left({V}=\left\{{A},{B},{C}\right\}\wedge {G}\in \mathrm{USGraph}\right)\right)\wedge \left\{{A},{B}\right\}\in {E}\right)\to {B}={B}\right)\right)\right)$
67 63 39 66 3imtr4d ${⊢}{y}={B}\to \left(\left\{{A},{y}\right\}\in {E}\to \left(\left\{{A},{B}\right\}\in {E}\to \left(\left(\left(\left({A}\in {X}\wedge {B}\in {Y}\wedge {A}\ne {B}\right)\wedge \left({V}=\left\{{A},{B},{C}\right\}\wedge {G}\in \mathrm{USGraph}\right)\right)\wedge \left\{{A},{B}\right\}\in {E}\right)\to {B}={y}\right)\right)\right)$
68 60 67 jaoi ${⊢}\left({y}={A}\vee {y}={B}\right)\to \left(\left\{{A},{y}\right\}\in {E}\to \left(\left\{{A},{B}\right\}\in {E}\to \left(\left(\left(\left({A}\in {X}\wedge {B}\in {Y}\wedge {A}\ne {B}\right)\wedge \left({V}=\left\{{A},{B},{C}\right\}\wedge {G}\in \mathrm{USGraph}\right)\right)\wedge \left\{{A},{B}\right\}\in {E}\right)\to {B}={y}\right)\right)\right)$
69 eqeq1 ${⊢}{w}={B}\to \left({w}={y}↔{B}={y}\right)$
70 69 imbi2d ${⊢}{w}={B}\to \left(\left(\left(\left(\left({A}\in {X}\wedge {B}\in {Y}\wedge {A}\ne {B}\right)\wedge \left({V}=\left\{{A},{B},{C}\right\}\wedge {G}\in \mathrm{USGraph}\right)\right)\wedge \left\{{A},{B}\right\}\in {E}\right)\to {w}={y}\right)↔\left(\left(\left(\left({A}\in {X}\wedge {B}\in {Y}\wedge {A}\ne {B}\right)\wedge \left({V}=\left\{{A},{B},{C}\right\}\wedge {G}\in \mathrm{USGraph}\right)\right)\wedge \left\{{A},{B}\right\}\in {E}\right)\to {B}={y}\right)\right)$
71 7 70 imbi12d ${⊢}{w}={B}\to \left(\left(\left\{{A},{w}\right\}\in {E}\to \left(\left(\left(\left({A}\in {X}\wedge {B}\in {Y}\wedge {A}\ne {B}\right)\wedge \left({V}=\left\{{A},{B},{C}\right\}\wedge {G}\in \mathrm{USGraph}\right)\right)\wedge \left\{{A},{B}\right\}\in {E}\right)\to {w}={y}\right)\right)↔\left(\left\{{A},{B}\right\}\in {E}\to \left(\left(\left(\left({A}\in {X}\wedge {B}\in {Y}\wedge {A}\ne {B}\right)\wedge \left({V}=\left\{{A},{B},{C}\right\}\wedge {G}\in \mathrm{USGraph}\right)\right)\wedge \left\{{A},{B}\right\}\in {E}\right)\to {B}={y}\right)\right)\right)$
72 71 imbi2d ${⊢}{w}={B}\to \left(\left(\left\{{A},{y}\right\}\in {E}\to \left(\left\{{A},{w}\right\}\in {E}\to \left(\left(\left(\left({A}\in {X}\wedge {B}\in {Y}\wedge {A}\ne {B}\right)\wedge \left({V}=\left\{{A},{B},{C}\right\}\wedge {G}\in \mathrm{USGraph}\right)\right)\wedge \left\{{A},{B}\right\}\in {E}\right)\to {w}={y}\right)\right)\right)↔\left(\left\{{A},{y}\right\}\in {E}\to \left(\left\{{A},{B}\right\}\in {E}\to \left(\left(\left(\left({A}\in {X}\wedge {B}\in {Y}\wedge {A}\ne {B}\right)\wedge \left({V}=\left\{{A},{B},{C}\right\}\wedge {G}\in \mathrm{USGraph}\right)\right)\wedge \left\{{A},{B}\right\}\in {E}\right)\to {B}={y}\right)\right)\right)\right)$
73 68 72 syl5ibr ${⊢}{w}={B}\to \left(\left({y}={A}\vee {y}={B}\right)\to \left(\left\{{A},{y}\right\}\in {E}\to \left(\left\{{A},{w}\right\}\in {E}\to \left(\left(\left(\left({A}\in {X}\wedge {B}\in {Y}\wedge {A}\ne {B}\right)\wedge \left({V}=\left\{{A},{B},{C}\right\}\wedge {G}\in \mathrm{USGraph}\right)\right)\wedge \left\{{A},{B}\right\}\in {E}\right)\to {w}={y}\right)\right)\right)\right)$
74 49 73 jaoi ${⊢}\left({w}={A}\vee {w}={B}\right)\to \left(\left({y}={A}\vee {y}={B}\right)\to \left(\left\{{A},{y}\right\}\in {E}\to \left(\left\{{A},{w}\right\}\in {E}\to \left(\left(\left(\left({A}\in {X}\wedge {B}\in {Y}\wedge {A}\ne {B}\right)\wedge \left({V}=\left\{{A},{B},{C}\right\}\wedge {G}\in \mathrm{USGraph}\right)\right)\wedge \left\{{A},{B}\right\}\in {E}\right)\to {w}={y}\right)\right)\right)\right)$
75 74 com3l ${⊢}\left({y}={A}\vee {y}={B}\right)\to \left(\left\{{A},{y}\right\}\in {E}\to \left(\left({w}={A}\vee {w}={B}\right)\to \left(\left\{{A},{w}\right\}\in {E}\to \left(\left(\left(\left({A}\in {X}\wedge {B}\in {Y}\wedge {A}\ne {B}\right)\wedge \left({V}=\left\{{A},{B},{C}\right\}\wedge {G}\in \mathrm{USGraph}\right)\right)\wedge \left\{{A},{B}\right\}\in {E}\right)\to {w}={y}\right)\right)\right)\right)$
76 17 75 sylbi ${⊢}{y}\in \left\{{A},{B}\right\}\to \left(\left\{{A},{y}\right\}\in {E}\to \left(\left({w}={A}\vee {w}={B}\right)\to \left(\left\{{A},{w}\right\}\in {E}\to \left(\left(\left(\left({A}\in {X}\wedge {B}\in {Y}\wedge {A}\ne {B}\right)\wedge \left({V}=\left\{{A},{B},{C}\right\}\wedge {G}\in \mathrm{USGraph}\right)\right)\wedge \left\{{A},{B}\right\}\in {E}\right)\to {w}={y}\right)\right)\right)\right)$
77 76 imp ${⊢}\left({y}\in \left\{{A},{B}\right\}\wedge \left\{{A},{y}\right\}\in {E}\right)\to \left(\left({w}={A}\vee {w}={B}\right)\to \left(\left\{{A},{w}\right\}\in {E}\to \left(\left(\left(\left({A}\in {X}\wedge {B}\in {Y}\wedge {A}\ne {B}\right)\wedge \left({V}=\left\{{A},{B},{C}\right\}\wedge {G}\in \mathrm{USGraph}\right)\right)\wedge \left\{{A},{B}\right\}\in {E}\right)\to {w}={y}\right)\right)\right)$
78 77 com3l ${⊢}\left({w}={A}\vee {w}={B}\right)\to \left(\left\{{A},{w}\right\}\in {E}\to \left(\left({y}\in \left\{{A},{B}\right\}\wedge \left\{{A},{y}\right\}\in {E}\right)\to \left(\left(\left(\left({A}\in {X}\wedge {B}\in {Y}\wedge {A}\ne {B}\right)\wedge \left({V}=\left\{{A},{B},{C}\right\}\wedge {G}\in \mathrm{USGraph}\right)\right)\wedge \left\{{A},{B}\right\}\in {E}\right)\to {w}={y}\right)\right)\right)$
79 15 78 sylbi ${⊢}{w}\in \left\{{A},{B}\right\}\to \left(\left\{{A},{w}\right\}\in {E}\to \left(\left({y}\in \left\{{A},{B}\right\}\wedge \left\{{A},{y}\right\}\in {E}\right)\to \left(\left(\left(\left({A}\in {X}\wedge {B}\in {Y}\wedge {A}\ne {B}\right)\wedge \left({V}=\left\{{A},{B},{C}\right\}\wedge {G}\in \mathrm{USGraph}\right)\right)\wedge \left\{{A},{B}\right\}\in {E}\right)\to {w}={y}\right)\right)\right)$
80 79 imp31 ${⊢}\left(\left({w}\in \left\{{A},{B}\right\}\wedge \left\{{A},{w}\right\}\in {E}\right)\wedge \left({y}\in \left\{{A},{B}\right\}\wedge \left\{{A},{y}\right\}\in {E}\right)\right)\to \left(\left(\left(\left({A}\in {X}\wedge {B}\in {Y}\wedge {A}\ne {B}\right)\wedge \left({V}=\left\{{A},{B},{C}\right\}\wedge {G}\in \mathrm{USGraph}\right)\right)\wedge \left\{{A},{B}\right\}\in {E}\right)\to {w}={y}\right)$
81 80 com12 ${⊢}\left(\left(\left({A}\in {X}\wedge {B}\in {Y}\wedge {A}\ne {B}\right)\wedge \left({V}=\left\{{A},{B},{C}\right\}\wedge {G}\in \mathrm{USGraph}\right)\right)\wedge \left\{{A},{B}\right\}\in {E}\right)\to \left(\left(\left({w}\in \left\{{A},{B}\right\}\wedge \left\{{A},{w}\right\}\in {E}\right)\wedge \left({y}\in \left\{{A},{B}\right\}\wedge \left\{{A},{y}\right\}\in {E}\right)\right)\to {w}={y}\right)$
82 81 alrimivv ${⊢}\left(\left(\left({A}\in {X}\wedge {B}\in {Y}\wedge {A}\ne {B}\right)\wedge \left({V}=\left\{{A},{B},{C}\right\}\wedge {G}\in \mathrm{USGraph}\right)\right)\wedge \left\{{A},{B}\right\}\in {E}\right)\to \forall {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left(\left({w}\in \left\{{A},{B}\right\}\wedge \left\{{A},{w}\right\}\in {E}\right)\wedge \left({y}\in \left\{{A},{B}\right\}\wedge \left\{{A},{y}\right\}\in {E}\right)\right)\to {w}={y}\right)$
83 eleq1w ${⊢}{w}={y}\to \left({w}\in \left\{{A},{B}\right\}↔{y}\in \left\{{A},{B}\right\}\right)$
84 preq2 ${⊢}{w}={y}\to \left\{{A},{w}\right\}=\left\{{A},{y}\right\}$
85 84 eleq1d ${⊢}{w}={y}\to \left(\left\{{A},{w}\right\}\in {E}↔\left\{{A},{y}\right\}\in {E}\right)$
86 83 85 anbi12d ${⊢}{w}={y}\to \left(\left({w}\in \left\{{A},{B}\right\}\wedge \left\{{A},{w}\right\}\in {E}\right)↔\left({y}\in \left\{{A},{B}\right\}\wedge \left\{{A},{y}\right\}\in {E}\right)\right)$
87 86 eu4 ${⊢}\exists !{w}\phantom{\rule{.4em}{0ex}}\left({w}\in \left\{{A},{B}\right\}\wedge \left\{{A},{w}\right\}\in {E}\right)↔\left(\exists {w}\phantom{\rule{.4em}{0ex}}\left({w}\in \left\{{A},{B}\right\}\wedge \left\{{A},{w}\right\}\in {E}\right)\wedge \forall {w}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left(\left({w}\in \left\{{A},{B}\right\}\wedge \left\{{A},{w}\right\}\in {E}\right)\wedge \left({y}\in \left\{{A},{B}\right\}\wedge \left\{{A},{y}\right\}\in {E}\right)\right)\to {w}={y}\right)\right)$
88 13 82 87 sylanbrc ${⊢}\left(\left(\left({A}\in {X}\wedge {B}\in {Y}\wedge {A}\ne {B}\right)\wedge \left({V}=\left\{{A},{B},{C}\right\}\wedge {G}\in \mathrm{USGraph}\right)\right)\wedge \left\{{A},{B}\right\}\in {E}\right)\to \exists !{w}\phantom{\rule{.4em}{0ex}}\left({w}\in \left\{{A},{B}\right\}\wedge \left\{{A},{w}\right\}\in {E}\right)$
89 df-reu ${⊢}\exists !{w}\in \left\{{A},{B}\right\}\phantom{\rule{.4em}{0ex}}\left\{{A},{w}\right\}\in {E}↔\exists !{w}\phantom{\rule{.4em}{0ex}}\left({w}\in \left\{{A},{B}\right\}\wedge \left\{{A},{w}\right\}\in {E}\right)$
90 88 89 sylibr ${⊢}\left(\left(\left({A}\in {X}\wedge {B}\in {Y}\wedge {A}\ne {B}\right)\wedge \left({V}=\left\{{A},{B},{C}\right\}\wedge {G}\in \mathrm{USGraph}\right)\right)\wedge \left\{{A},{B}\right\}\in {E}\right)\to \exists !{w}\in \left\{{A},{B}\right\}\phantom{\rule{.4em}{0ex}}\left\{{A},{w}\right\}\in {E}$
91 90 ex ${⊢}\left(\left({A}\in {X}\wedge {B}\in {Y}\wedge {A}\ne {B}\right)\wedge \left({V}=\left\{{A},{B},{C}\right\}\wedge {G}\in \mathrm{USGraph}\right)\right)\to \left(\left\{{A},{B}\right\}\in {E}\to \exists !{w}\in \left\{{A},{B}\right\}\phantom{\rule{.4em}{0ex}}\left\{{A},{w}\right\}\in {E}\right)$