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