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=Vtx⁡G
3vfriswmgr.e ⊢E=Edg⁡G
Assertion 3vfriswmgrlem ⊢A∈X∧B∈Y∧A≠B∧V=ABC∧G∈USGraph→AB∈E→∃!w∈ABAw∈E

Proof

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