Metamath Proof Explorer

Theorem nb3grprlem1

Description: Lemma 1 for nb3grpr . (Contributed by Alexander van der Vekens, 15-Oct-2017) (Revised by AV, 28-Oct-2020)

Ref Expression
Hypotheses nb3grpr.v ⊢V=Vtx⁡G
nb3grpr.e ⊢E=Edg⁡G
nb3grpr.g ⊢φ→G∈USGraph
nb3grpr.t ⊢φ→V=ABC
nb3grpr.s ⊢φ→A∈X∧B∈Y∧C∈Z
Assertion nb3grprlem1 ⊢φ→GNeighbVtxA=BC↔AB∈E∧AC∈E

Proof

Step Hyp Ref Expression
1 nb3grpr.v ⊢V=Vtx⁡G
2 nb3grpr.e ⊢E=Edg⁡G
3 nb3grpr.g ⊢φ→G∈USGraph
4 nb3grpr.t ⊢φ→V=ABC
5 nb3grpr.s ⊢φ→A∈X∧B∈Y∧C∈Z
6 prid1g ⊢B∈Y→B∈BC
7 6 3ad2ant2 ⊢A∈X∧B∈Y∧C∈Z→B∈BC
8 5 7 syl ⊢φ→B∈BC
9 8 adantr ⊢φ∧GNeighbVtxA=BC→B∈BC
10 eleq2 ⊢BC=GNeighbVtxA→B∈BC↔B∈GNeighbVtxA
11 10 eqcoms ⊢GNeighbVtxA=BC→B∈BC↔B∈GNeighbVtxA
12 11 adantl ⊢φ∧GNeighbVtxA=BC→B∈BC↔B∈GNeighbVtxA
13 9 12 mpbid ⊢φ∧GNeighbVtxA=BC→B∈GNeighbVtxA
14 2 nbusgreledg ⊢G∈USGraph→B∈GNeighbVtxA↔BA∈E
15 prcom ⊢BA=AB
16 15 a1i ⊢G∈USGraph→BA=AB
17 16 eleq1d ⊢G∈USGraph→BA∈E↔AB∈E
18 14 17 bitrd ⊢G∈USGraph→B∈GNeighbVtxA↔AB∈E
19 3 18 syl ⊢φ→B∈GNeighbVtxA↔AB∈E
20 19 adantr ⊢φ∧GNeighbVtxA=BC→B∈GNeighbVtxA↔AB∈E
21 13 20 mpbid ⊢φ∧GNeighbVtxA=BC→AB∈E
22 prid2g ⊢C∈Z→C∈BC
23 22 3ad2ant3 ⊢A∈X∧B∈Y∧C∈Z→C∈BC
24 5 23 syl ⊢φ→C∈BC
25 24 adantr ⊢φ∧GNeighbVtxA=BC→C∈BC
26 eleq2 ⊢BC=GNeighbVtxA→C∈BC↔C∈GNeighbVtxA
27 26 eqcoms ⊢GNeighbVtxA=BC→C∈BC↔C∈GNeighbVtxA
28 27 adantl ⊢φ∧GNeighbVtxA=BC→C∈BC↔C∈GNeighbVtxA
29 25 28 mpbid ⊢φ∧GNeighbVtxA=BC→C∈GNeighbVtxA
30 2 nbusgreledg ⊢G∈USGraph→C∈GNeighbVtxA↔CA∈E
31 prcom ⊢CA=AC
32 31 a1i ⊢G∈USGraph→CA=AC
33 32 eleq1d ⊢G∈USGraph→CA∈E↔AC∈E
34 30 33 bitrd ⊢G∈USGraph→C∈GNeighbVtxA↔AC∈E
35 3 34 syl ⊢φ→C∈GNeighbVtxA↔AC∈E
36 35 adantr ⊢φ∧GNeighbVtxA=BC→C∈GNeighbVtxA↔AC∈E
37 29 36 mpbid ⊢φ∧GNeighbVtxA=BC→AC∈E
38 21 37 jca ⊢φ∧GNeighbVtxA=BC→AB∈E∧AC∈E
39 1 2 nbusgr ⊢G∈USGraph→GNeighbVtxA=v∈V|Av∈E
40 3 39 syl ⊢φ→GNeighbVtxA=v∈V|Av∈E
41 40 adantr ⊢φ∧AB∈E∧AC∈E→GNeighbVtxA=v∈V|Av∈E
42 eleq2 ⊢V=ABC→v∈V↔v∈ABC
43 4 42 syl ⊢φ→v∈V↔v∈ABC
44 43 adantr ⊢φ∧AB∈E∧AC∈E→v∈V↔v∈ABC
45 vex ⊢v∈V
46 45 eltp ⊢v∈ABC↔v=A∨v=B∨v=C
47 2 usgredgne ⊢G∈USGraph∧Av∈E→A≠v
48 df-ne ⊢A≠v↔¬A=v
49 pm2.24 ⊢A=v→¬A=v→v=B∨v=C
50 49 eqcoms ⊢v=A→¬A=v→v=B∨v=C
51 50 com12 ⊢¬A=v→v=A→v=B∨v=C
52 48 51 sylbi ⊢A≠v→v=A→v=B∨v=C
53 47 52 syl ⊢G∈USGraph∧Av∈E→v=A→v=B∨v=C
54 53 ex ⊢G∈USGraph→Av∈E→v=A→v=B∨v=C
55 3 54 syl ⊢φ→Av∈E→v=A→v=B∨v=C
56 55 adantr ⊢φ∧AB∈E∧AC∈E→Av∈E→v=A→v=B∨v=C
57 56 com3r ⊢v=A→φ∧AB∈E∧AC∈E→Av∈E→v=B∨v=C
58 orc ⊢v=B→v=B∨v=C
59 58 2a1d ⊢v=B→φ∧AB∈E∧AC∈E→Av∈E→v=B∨v=C
60 olc ⊢v=C→v=B∨v=C
61 60 2a1d ⊢v=C→φ∧AB∈E∧AC∈E→Av∈E→v=B∨v=C
62 57 59 61 3jaoi ⊢v=A∨v=B∨v=C→φ∧AB∈E∧AC∈E→Av∈E→v=B∨v=C
63 46 62 sylbi ⊢v∈ABC→φ∧AB∈E∧AC∈E→Av∈E→v=B∨v=C
64 63 com12 ⊢φ∧AB∈E∧AC∈E→v∈ABC→Av∈E→v=B∨v=C
65 44 64 sylbid ⊢φ∧AB∈E∧AC∈E→v∈V→Av∈E→v=B∨v=C
66 65 impd ⊢φ∧AB∈E∧AC∈E→v∈V∧Av∈E→v=B∨v=C
67 eqid ⊢B=B
68 67 3mix2i ⊢B=A∨B=B∨B=C
69 5 simp2d ⊢φ→B∈Y
70 eltpg ⊢B∈Y→B∈ABC↔B=A∨B=B∨B=C
71 69 70 syl ⊢φ→B∈ABC↔B=A∨B=B∨B=C
72 68 71 mpbiri ⊢φ→B∈ABC
73 72 adantr ⊢φ∧v=B→B∈ABC
74 eleq1 ⊢v=B→v∈ABC↔B∈ABC
75 74 bicomd ⊢v=B→B∈ABC↔v∈ABC
76 75 adantl ⊢φ∧v=B→B∈ABC↔v∈ABC
77 73 76 mpbid ⊢φ∧v=B→v∈ABC
78 42 bicomd ⊢V=ABC→v∈ABC↔v∈V
79 4 78 syl ⊢φ→v∈ABC↔v∈V
80 79 adantr ⊢φ∧v=B→v∈ABC↔v∈V
81 77 80 mpbid ⊢φ∧v=B→v∈V
82 81 ex ⊢φ→v=B→v∈V
83 82 adantr ⊢φ∧AB∈E∧AC∈E→v=B→v∈V
84 83 impcom ⊢v=B∧φ∧AB∈E∧AC∈E→v∈V
85 preq2 ⊢B=v→AB=Av
86 85 eleq1d ⊢B=v→AB∈E↔Av∈E
87 86 eqcoms ⊢v=B→AB∈E↔Av∈E
88 87 biimpcd ⊢AB∈E→v=B→Av∈E
89 88 ad2antrl ⊢φ∧AB∈E∧AC∈E→v=B→Av∈E
90 89 impcom ⊢v=B∧φ∧AB∈E∧AC∈E→Av∈E
91 84 90 jca ⊢v=B∧φ∧AB∈E∧AC∈E→v∈V∧Av∈E
92 91 ex ⊢v=B→φ∧AB∈E∧AC∈E→v∈V∧Av∈E
93 tpid3g ⊢C∈Z→C∈ABC
94 93 3ad2ant3 ⊢A∈X∧B∈Y∧C∈Z→C∈ABC
95 5 94 syl ⊢φ→C∈ABC
96 95 adantr ⊢φ∧v=C→C∈ABC
97 eleq1 ⊢v=C→v∈ABC↔C∈ABC
98 97 bicomd ⊢v=C→C∈ABC↔v∈ABC
99 98 adantl ⊢φ∧v=C→C∈ABC↔v∈ABC
100 96 99 mpbid ⊢φ∧v=C→v∈ABC
101 79 adantr ⊢φ∧v=C→v∈ABC↔v∈V
102 100 101 mpbid ⊢φ∧v=C→v∈V
103 102 ex ⊢φ→v=C→v∈V
104 103 adantr ⊢φ∧AB∈E∧AC∈E→v=C→v∈V
105 104 impcom ⊢v=C∧φ∧AB∈E∧AC∈E→v∈V
106 preq2 ⊢C=v→AC=Av
107 106 eleq1d ⊢C=v→AC∈E↔Av∈E
108 107 eqcoms ⊢v=C→AC∈E↔Av∈E
109 108 biimpcd ⊢AC∈E→v=C→Av∈E
110 109 ad2antll ⊢φ∧AB∈E∧AC∈E→v=C→Av∈E
111 110 impcom ⊢v=C∧φ∧AB∈E∧AC∈E→Av∈E
112 105 111 jca ⊢v=C∧φ∧AB∈E∧AC∈E→v∈V∧Av∈E
113 112 ex ⊢v=C→φ∧AB∈E∧AC∈E→v∈V∧Av∈E
114 92 113 jaoi ⊢v=B∨v=C→φ∧AB∈E∧AC∈E→v∈V∧Av∈E
115 114 com12 ⊢φ∧AB∈E∧AC∈E→v=B∨v=C→v∈V∧Av∈E
116 66 115 impbid ⊢φ∧AB∈E∧AC∈E→v∈V∧Av∈E↔v=B∨v=C
117 116 abbidv ⊢φ∧AB∈E∧AC∈E→v|v∈V∧Av∈E=v|v=B∨v=C
118 df-rab ⊢v∈V|Av∈E=v|v∈V∧Av∈E
119 dfpr2 ⊢BC=v|v=B∨v=C
120 117 118 119 3eqtr4g ⊢φ∧AB∈E∧AC∈E→v∈V|Av∈E=BC
121 41 120 eqtrd ⊢φ∧AB∈E∧AC∈E→GNeighbVtxA=BC
122 38 121 impbida ⊢φ→GNeighbVtxA=BC↔AB∈E∧AC∈E