Metamath Proof Explorer

Theorem nb3grprlem2

Description: Lemma 2 for nb3grpr . (Contributed by Alexander van der Vekens, 17-Oct-2017) (Revised by AV, 28-Oct-2020) (Proof shortened by AV, 13-Feb-2022)

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
nb3grpr.n ⊢ φ → A ≠ B ∧ A ≠ C ∧ B ≠ C
Assertion nb3grprlem2 ⊢ φ → G NeighbVtx A = B C ↔ ∃ v ∈ V ∃ w ∈ V ∖ v G NeighbVtx A = v w

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 nb3grpr.n ⊢ φ → A ≠ B ∧ A ≠ C ∧ B ≠ C
7 sneq ⊢ v = A → v = A
8 7 difeq2d ⊢ v = A → A B C ∖ v = A B C ∖ A
9 preq1 ⊢ v = A → v w = A w
10 9 eqeq2d ⊢ v = A → G NeighbVtx A = v w ↔ G NeighbVtx A = A w
11 8 10 rexeqbidv ⊢ v = A → ∃ w ∈ A B C ∖ v G NeighbVtx A = v w ↔ ∃ w ∈ A B C ∖ A G NeighbVtx A = A w
12 sneq ⊢ v = B → v = B
13 12 difeq2d ⊢ v = B → A B C ∖ v = A B C ∖ B
14 preq1 ⊢ v = B → v w = B w
15 14 eqeq2d ⊢ v = B → G NeighbVtx A = v w ↔ G NeighbVtx A = B w
16 13 15 rexeqbidv ⊢ v = B → ∃ w ∈ A B C ∖ v G NeighbVtx A = v w ↔ ∃ w ∈ A B C ∖ B G NeighbVtx A = B w
17 sneq ⊢ v = C → v = C
18 17 difeq2d ⊢ v = C → A B C ∖ v = A B C ∖ C
19 preq1 ⊢ v = C → v w = C w
20 19 eqeq2d ⊢ v = C → G NeighbVtx A = v w ↔ G NeighbVtx A = C w
21 18 20 rexeqbidv ⊢ v = C → ∃ w ∈ A B C ∖ v G NeighbVtx A = v w ↔ ∃ w ∈ A B C ∖ C G NeighbVtx A = C w
22 11 16 21 rextpg ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z → ∃ v ∈ A B C ∃ w ∈ A B C ∖ v G NeighbVtx A = v w ↔ ∃ w ∈ A B C ∖ A G NeighbVtx A = A w ∨ ∃ w ∈ A B C ∖ B G NeighbVtx A = B w ∨ ∃ w ∈ A B C ∖ C G NeighbVtx A = C w
23 5 22 syl ⊢ φ → ∃ v ∈ A B C ∃ w ∈ A B C ∖ v G NeighbVtx A = v w ↔ ∃ w ∈ A B C ∖ A G NeighbVtx A = A w ∨ ∃ w ∈ A B C ∖ B G NeighbVtx A = B w ∨ ∃ w ∈ A B C ∖ C G NeighbVtx A = C w
24 4 3 jca ⊢ φ → V = A B C ∧ G ∈ USGraph
25 simpl ⊢ V = A B C ∧ G ∈ USGraph → V = A B C
26 difeq1 ⊢ V = A B C → V ∖ v = A B C ∖ v
27 26 adantr ⊢ V = A B C ∧ G ∈ USGraph → V ∖ v = A B C ∖ v
28 27 rexeqdv ⊢ V = A B C ∧ G ∈ USGraph → ∃ w ∈ V ∖ v G NeighbVtx A = v w ↔ ∃ w ∈ A B C ∖ v G NeighbVtx A = v w
29 25 28 rexeqbidv ⊢ V = A B C ∧ G ∈ USGraph → ∃ v ∈ V ∃ w ∈ V ∖ v G NeighbVtx A = v w ↔ ∃ v ∈ A B C ∃ w ∈ A B C ∖ v G NeighbVtx A = v w
30 24 29 syl ⊢ φ → ∃ v ∈ V ∃ w ∈ V ∖ v G NeighbVtx A = v w ↔ ∃ v ∈ A B C ∃ w ∈ A B C ∖ v G NeighbVtx A = v w
31 preq2 ⊢ w = B → A w = A B
32 31 eqeq2d ⊢ w = B → G NeighbVtx A = A w ↔ G NeighbVtx A = A B
33 preq2 ⊢ w = C → A w = A C
34 33 eqeq2d ⊢ w = C → G NeighbVtx A = A w ↔ G NeighbVtx A = A C
35 32 34 rexprg ⊢ B ∈ Y ∧ C ∈ Z → ∃ w ∈ B C G NeighbVtx A = A w ↔ G NeighbVtx A = A B ∨ G NeighbVtx A = A C
36 35 3adant1 ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z → ∃ w ∈ B C G NeighbVtx A = A w ↔ G NeighbVtx A = A B ∨ G NeighbVtx A = A C
37 preq2 ⊢ w = C → B w = B C
38 37 eqeq2d ⊢ w = C → G NeighbVtx A = B w ↔ G NeighbVtx A = B C
39 preq2 ⊢ w = A → B w = B A
40 39 eqeq2d ⊢ w = A → G NeighbVtx A = B w ↔ G NeighbVtx A = B A
41 38 40 rexprg ⊢ C ∈ Z ∧ A ∈ X → ∃ w ∈ C A G NeighbVtx A = B w ↔ G NeighbVtx A = B C ∨ G NeighbVtx A = B A
42 41 ancoms ⊢ A ∈ X ∧ C ∈ Z → ∃ w ∈ C A G NeighbVtx A = B w ↔ G NeighbVtx A = B C ∨ G NeighbVtx A = B A
43 42 3adant2 ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z → ∃ w ∈ C A G NeighbVtx A = B w ↔ G NeighbVtx A = B C ∨ G NeighbVtx A = B A
44 preq2 ⊢ w = A → C w = C A
45 44 eqeq2d ⊢ w = A → G NeighbVtx A = C w ↔ G NeighbVtx A = C A
46 preq2 ⊢ w = B → C w = C B
47 46 eqeq2d ⊢ w = B → G NeighbVtx A = C w ↔ G NeighbVtx A = C B
48 45 47 rexprg ⊢ A ∈ X ∧ B ∈ Y → ∃ w ∈ A B G NeighbVtx A = C w ↔ G NeighbVtx A = C A ∨ G NeighbVtx A = C B
49 48 3adant3 ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z → ∃ w ∈ A B G NeighbVtx A = C w ↔ G NeighbVtx A = C A ∨ G NeighbVtx A = C B
50 36 43 49 3orbi123d ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z → ∃ w ∈ B C G NeighbVtx A = A w ∨ ∃ w ∈ C A G NeighbVtx A = B w ∨ ∃ w ∈ A B G NeighbVtx A = C w ↔ G NeighbVtx A = A B ∨ G NeighbVtx A = A C ∨ G NeighbVtx A = B C ∨ G NeighbVtx A = B A ∨ G NeighbVtx A = C A ∨ G NeighbVtx A = C B
51 5 50 syl ⊢ φ → ∃ w ∈ B C G NeighbVtx A = A w ∨ ∃ w ∈ C A G NeighbVtx A = B w ∨ ∃ w ∈ A B G NeighbVtx A = C w ↔ G NeighbVtx A = A B ∨ G NeighbVtx A = A C ∨ G NeighbVtx A = B C ∨ G NeighbVtx A = B A ∨ G NeighbVtx A = C A ∨ G NeighbVtx A = C B
52 tprot ⊢ A B C = B C A
53 52 a1i ⊢ A ≠ B ∧ A ≠ C ∧ B ≠ C → A B C = B C A
54 53 difeq1d ⊢ A ≠ B ∧ A ≠ C ∧ B ≠ C → A B C ∖ A = B C A ∖ A
55 necom ⊢ A ≠ B ↔ B ≠ A
56 necom ⊢ A ≠ C ↔ C ≠ A
57 diftpsn3 ⊢ B ≠ A ∧ C ≠ A → B C A ∖ A = B C
58 55 56 57 syl2anb ⊢ A ≠ B ∧ A ≠ C → B C A ∖ A = B C
59 58 3adant3 ⊢ A ≠ B ∧ A ≠ C ∧ B ≠ C → B C A ∖ A = B C
60 54 59 eqtrd ⊢ A ≠ B ∧ A ≠ C ∧ B ≠ C → A B C ∖ A = B C
61 60 rexeqdv ⊢ A ≠ B ∧ A ≠ C ∧ B ≠ C → ∃ w ∈ A B C ∖ A G NeighbVtx A = A w ↔ ∃ w ∈ B C G NeighbVtx A = A w
62 tprot ⊢ C A B = A B C
63 62 eqcomi ⊢ A B C = C A B
64 63 a1i ⊢ A ≠ B ∧ A ≠ C ∧ B ≠ C → A B C = C A B
65 64 difeq1d ⊢ A ≠ B ∧ A ≠ C ∧ B ≠ C → A B C ∖ B = C A B ∖ B
66 necom ⊢ B ≠ C ↔ C ≠ B
67 66 anbi1i ⊢ B ≠ C ∧ A ≠ B ↔ C ≠ B ∧ A ≠ B
68 67 biimpi ⊢ B ≠ C ∧ A ≠ B → C ≠ B ∧ A ≠ B
69 68 ancoms ⊢ A ≠ B ∧ B ≠ C → C ≠ B ∧ A ≠ B
70 diftpsn3 ⊢ C ≠ B ∧ A ≠ B → C A B ∖ B = C A
71 69 70 syl ⊢ A ≠ B ∧ B ≠ C → C A B ∖ B = C A
72 71 3adant2 ⊢ A ≠ B ∧ A ≠ C ∧ B ≠ C → C A B ∖ B = C A
73 65 72 eqtrd ⊢ A ≠ B ∧ A ≠ C ∧ B ≠ C → A B C ∖ B = C A
74 73 rexeqdv ⊢ A ≠ B ∧ A ≠ C ∧ B ≠ C → ∃ w ∈ A B C ∖ B G NeighbVtx A = B w ↔ ∃ w ∈ C A G NeighbVtx A = B w
75 diftpsn3 ⊢ A ≠ C ∧ B ≠ C → A B C ∖ C = A B
76 75 3adant1 ⊢ A ≠ B ∧ A ≠ C ∧ B ≠ C → A B C ∖ C = A B
77 76 rexeqdv ⊢ A ≠ B ∧ A ≠ C ∧ B ≠ C → ∃ w ∈ A B C ∖ C G NeighbVtx A = C w ↔ ∃ w ∈ A B G NeighbVtx A = C w
78 61 74 77 3orbi123d ⊢ A ≠ B ∧ A ≠ C ∧ B ≠ C → ∃ w ∈ A B C ∖ A G NeighbVtx A = A w ∨ ∃ w ∈ A B C ∖ B G NeighbVtx A = B w ∨ ∃ w ∈ A B C ∖ C G NeighbVtx A = C w ↔ ∃ w ∈ B C G NeighbVtx A = A w ∨ ∃ w ∈ C A G NeighbVtx A = B w ∨ ∃ w ∈ A B G NeighbVtx A = C w
79 6 78 syl ⊢ φ → ∃ w ∈ A B C ∖ A G NeighbVtx A = A w ∨ ∃ w ∈ A B C ∖ B G NeighbVtx A = B w ∨ ∃ w ∈ A B C ∖ C G NeighbVtx A = C w ↔ ∃ w ∈ B C G NeighbVtx A = A w ∨ ∃ w ∈ C A G NeighbVtx A = B w ∨ ∃ w ∈ A B G NeighbVtx A = C w
80 prcom ⊢ C B = B C
81 80 eqeq2i ⊢ G NeighbVtx A = C B ↔ G NeighbVtx A = B C
82 81 orbi2i ⊢ G NeighbVtx A = B C ∨ G NeighbVtx A = C B ↔ G NeighbVtx A = B C ∨ G NeighbVtx A = B C
83 oridm ⊢ G NeighbVtx A = B C ∨ G NeighbVtx A = B C ↔ G NeighbVtx A = B C
84 82 83 bitr2i ⊢ G NeighbVtx A = B C ↔ G NeighbVtx A = B C ∨ G NeighbVtx A = C B
85 84 a1i ⊢ φ → G NeighbVtx A = B C ↔ G NeighbVtx A = B C ∨ G NeighbVtx A = C B
86 nbgrnself2 ⊢ A ∉ G NeighbVtx A
87 df-nel ⊢ A ∉ G NeighbVtx A ↔ ¬ A ∈ G NeighbVtx A
88 prid2g ⊢ A ∈ X → A ∈ B A
89 88 3ad2ant1 ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z → A ∈ B A
90 eleq2 ⊢ G NeighbVtx A = B A → A ∈ G NeighbVtx A ↔ A ∈ B A
91 89 90 syl5ibrcom ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z → G NeighbVtx A = B A → A ∈ G NeighbVtx A
92 91 con3rr3 ⊢ ¬ A ∈ G NeighbVtx A → A ∈ X ∧ B ∈ Y ∧ C ∈ Z → ¬ G NeighbVtx A = B A
93 87 92 sylbi ⊢ A ∉ G NeighbVtx A → A ∈ X ∧ B ∈ Y ∧ C ∈ Z → ¬ G NeighbVtx A = B A
94 86 5 93 mpsyl ⊢ φ → ¬ G NeighbVtx A = B A
95 biorf ⊢ ¬ G NeighbVtx A = B A → G NeighbVtx A = B C ↔ G NeighbVtx A = B A ∨ G NeighbVtx A = B C
96 orcom ⊢ G NeighbVtx A = B A ∨ G NeighbVtx A = B C ↔ G NeighbVtx A = B C ∨ G NeighbVtx A = B A
97 95 96 bitrdi ⊢ ¬ G NeighbVtx A = B A → G NeighbVtx A = B C ↔ G NeighbVtx A = B C ∨ G NeighbVtx A = B A
98 94 97 syl ⊢ φ → G NeighbVtx A = B C ↔ G NeighbVtx A = B C ∨ G NeighbVtx A = B A
99 prid2g ⊢ A ∈ X → A ∈ C A
100 99 3ad2ant1 ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z → A ∈ C A
101 eleq2 ⊢ G NeighbVtx A = C A → A ∈ G NeighbVtx A ↔ A ∈ C A
102 100 101 syl5ibrcom ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z → G NeighbVtx A = C A → A ∈ G NeighbVtx A
103 102 con3rr3 ⊢ ¬ A ∈ G NeighbVtx A → A ∈ X ∧ B ∈ Y ∧ C ∈ Z → ¬ G NeighbVtx A = C A
104 87 103 sylbi ⊢ A ∉ G NeighbVtx A → A ∈ X ∧ B ∈ Y ∧ C ∈ Z → ¬ G NeighbVtx A = C A
105 86 5 104 mpsyl ⊢ φ → ¬ G NeighbVtx A = C A
106 biorf ⊢ ¬ G NeighbVtx A = C A → G NeighbVtx A = C B ↔ G NeighbVtx A = C A ∨ G NeighbVtx A = C B
107 105 106 syl ⊢ φ → G NeighbVtx A = C B ↔ G NeighbVtx A = C A ∨ G NeighbVtx A = C B
108 98 107 orbi12d ⊢ φ → G NeighbVtx A = B C ∨ G NeighbVtx A = C B ↔ G NeighbVtx A = B C ∨ G NeighbVtx A = B A ∨ G NeighbVtx A = C A ∨ G NeighbVtx A = C B
109 prid1g ⊢ A ∈ X → A ∈ A B
110 109 3ad2ant1 ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z → A ∈ A B
111 eleq2 ⊢ G NeighbVtx A = A B → A ∈ G NeighbVtx A ↔ A ∈ A B
112 110 111 syl5ibrcom ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z → G NeighbVtx A = A B → A ∈ G NeighbVtx A
113 112 con3dimp ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ ¬ A ∈ G NeighbVtx A → ¬ G NeighbVtx A = A B
114 prid1g ⊢ A ∈ X → A ∈ A C
115 114 3ad2ant1 ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z → A ∈ A C
116 eleq2 ⊢ G NeighbVtx A = A C → A ∈ G NeighbVtx A ↔ A ∈ A C
117 115 116 syl5ibrcom ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z → G NeighbVtx A = A C → A ∈ G NeighbVtx A
118 117 con3dimp ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ ¬ A ∈ G NeighbVtx A → ¬ G NeighbVtx A = A C
119 113 118 jca ⊢ A ∈ X ∧ B ∈ Y ∧ C ∈ Z ∧ ¬ A ∈ G NeighbVtx A → ¬ G NeighbVtx A = A B ∧ ¬ G NeighbVtx A = A C
120 119 expcom ⊢ ¬ A ∈ G NeighbVtx A → A ∈ X ∧ B ∈ Y ∧ C ∈ Z → ¬ G NeighbVtx A = A B ∧ ¬ G NeighbVtx A = A C
121 87 120 sylbi ⊢ A ∉ G NeighbVtx A → A ∈ X ∧ B ∈ Y ∧ C ∈ Z → ¬ G NeighbVtx A = A B ∧ ¬ G NeighbVtx A = A C
122 86 5 121 mpsyl ⊢ φ → ¬ G NeighbVtx A = A B ∧ ¬ G NeighbVtx A = A C
123 ioran ⊢ ¬ G NeighbVtx A = A B ∨ G NeighbVtx A = A C ↔ ¬ G NeighbVtx A = A B ∧ ¬ G NeighbVtx A = A C
124 122 123 sylibr ⊢ φ → ¬ G NeighbVtx A = A B ∨ G NeighbVtx A = A C
125 124 3bior1fd ⊢ φ → G NeighbVtx A = B C ∨ G NeighbVtx A = B A ∨ G NeighbVtx A = C A ∨ G NeighbVtx A = C B ↔ G NeighbVtx A = A B ∨ G NeighbVtx A = A C ∨ G NeighbVtx A = B C ∨ G NeighbVtx A = B A ∨ G NeighbVtx A = C A ∨ G NeighbVtx A = C B
126 85 108 125 3bitrd ⊢ φ → G NeighbVtx A = B C ↔ G NeighbVtx A = A B ∨ G NeighbVtx A = A C ∨ G NeighbVtx A = B C ∨ G NeighbVtx A = B A ∨ G NeighbVtx A = C A ∨ G NeighbVtx A = C B
127 51 79 126 3bitr4rd ⊢ φ → G NeighbVtx A = B C ↔ ∃ w ∈ A B C ∖ A G NeighbVtx A = A w ∨ ∃ w ∈ A B C ∖ B G NeighbVtx A = B w ∨ ∃ w ∈ A B C ∖ C G NeighbVtx A = C w
128 23 30 127 3bitr4rd ⊢ φ → G NeighbVtx A = B C ↔ ∃ v ∈ V ∃ w ∈ V ∖ v G NeighbVtx A = v w