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 
|- ( ph -> G e. USGraph )
nb3grpr.t 
|- ( ph -> V = { A , B , C } )
nb3grpr.s 
|- ( ph -> ( A e. X /\ B e. Y /\ C e. Z ) )
Assertion nb3grprlem1 
|- ( ph -> ( ( G NeighbVtx A ) = { B , C } <-> ( { A , B } e. E /\ { A , C } e. E ) ) )

Proof

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