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 ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
nb3grpr.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
nb3grpr.g ⊢ ( 𝜑 → 𝐺 ∈ USGraph )
nb3grpr.t ⊢ ( 𝜑 → 𝑉 = { 𝐴 , 𝐵 , 𝐶 } )
nb3grpr.s ⊢ ( 𝜑 → ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) )
Assertion nb3grprlem1 ( 𝜑 → ( ( 𝐺 NeighbVtx 𝐴 ) = { 𝐵 , 𝐶 } ↔ ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐴 , 𝐶 } ∈ 𝐸 ) ) )

Proof

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