Metamath Proof Explorer

Theorem frgrnbnb

Description: If two neighbors U and W of a vertex X have a common neighbor A in a friendship graph, then this common neighbor A must be the vertex X . (Contributed by Alexander van der Vekens, 19-Dec-2017) (Revised by AV, 2-Apr-2021) (Proof shortened by AV, 13-Feb-2022)

Ref Expression
Hypotheses frgrnbnb.e 
|- E = ( Edg ` G )
frgrnbnb.n 
|- D = ( G NeighbVtx X )
Assertion frgrnbnb 
|- ( ( G e. FriendGraph /\ ( U e. D /\ W e. D ) /\ U =/= W ) -> ( ( { U , A } e. E /\ { W , A } e. E ) -> A = X ) )

Proof

Step Hyp Ref Expression
1 frgrnbnb.e 
 |-  E = ( Edg ` G )
2 frgrnbnb.n 
 |-  D = ( G NeighbVtx X )
3 frgrusgr 
 |-  ( G e. FriendGraph -> G e. USGraph )
4 2 eleq2i 
 |-  ( U e. D <-> U e. ( G NeighbVtx X ) )
5 1 nbusgreledg 
 |-  ( G e. USGraph -> ( U e. ( G NeighbVtx X ) <-> { U , X } e. E ) )
6 5 biimpd 
 |-  ( G e. USGraph -> ( U e. ( G NeighbVtx X ) -> { U , X } e. E ) )
7 4 6 syl5bi 
 |-  ( G e. USGraph -> ( U e. D -> { U , X } e. E ) )
8 2 eleq2i 
 |-  ( W e. D <-> W e. ( G NeighbVtx X ) )
9 1 nbusgreledg 
 |-  ( G e. USGraph -> ( W e. ( G NeighbVtx X ) <-> { W , X } e. E ) )
10 9 biimpd 
 |-  ( G e. USGraph -> ( W e. ( G NeighbVtx X ) -> { W , X } e. E ) )
11 8 10 syl5bi 
 |-  ( G e. USGraph -> ( W e. D -> { W , X } e. E ) )
12 7 11 anim12d 
 |-  ( G e. USGraph -> ( ( U e. D /\ W e. D ) -> ( { U , X } e. E /\ { W , X } e. E ) ) )
13 12 imp 
 |-  ( ( G e. USGraph /\ ( U e. D /\ W e. D ) ) -> ( { U , X } e. E /\ { W , X } e. E ) )
14 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
15 14 nbgrisvtx 
 |-  ( U e. ( G NeighbVtx X ) -> U e. ( Vtx ` G ) )
16 15 2 eleq2s 
 |-  ( U e. D -> U e. ( Vtx ` G ) )
17 14 nbgrisvtx 
 |-  ( W e. ( G NeighbVtx X ) -> W e. ( Vtx ` G ) )
18 17 2 eleq2s 
 |-  ( W e. D -> W e. ( Vtx ` G ) )
19 16 18 anim12i 
 |-  ( ( U e. D /\ W e. D ) -> ( U e. ( Vtx ` G ) /\ W e. ( Vtx ` G ) ) )
20 19 adantl 
 |-  ( ( G e. USGraph /\ ( U e. D /\ W e. D ) ) -> ( U e. ( Vtx ` G ) /\ W e. ( Vtx ` G ) ) )
21 1 14 usgrpredgv 
 |-  ( ( G e. USGraph /\ { U , A } e. E ) -> ( U e. ( Vtx ` G ) /\ A e. ( Vtx ` G ) ) )
22 21 ad2ant2r 
 |-  ( ( ( G e. USGraph /\ ( U e. D /\ W e. D ) ) /\ ( { U , A } e. E /\ { W , A } e. E ) ) -> ( U e. ( Vtx ` G ) /\ A e. ( Vtx ` G ) ) )
23 ax-1 
 |-  ( A = X -> ( G e. FriendGraph -> A = X ) )
24 23 2a1d 
 |-  ( A = X -> ( ( { U , A } e. E /\ { W , A } e. E ) -> ( ( ( X e. ( Vtx ` G ) /\ A e. ( Vtx ` G ) ) /\ ( U e. ( Vtx ` G ) /\ W e. ( Vtx ` G ) ) ) -> ( G e. FriendGraph -> A = X ) ) ) )
25 24 2a1d 
 |-  ( A = X -> ( U =/= W -> ( ( { U , X } e. E /\ { W , X } e. E ) -> ( ( { U , A } e. E /\ { W , A } e. E ) -> ( ( ( X e. ( Vtx ` G ) /\ A e. ( Vtx ` G ) ) /\ ( U e. ( Vtx ` G ) /\ W e. ( Vtx ` G ) ) ) -> ( G e. FriendGraph -> A = X ) ) ) ) ) )
26 simpll 
 |-  ( ( ( G e. USGraph /\ ( ( X e. ( Vtx ` G ) /\ A e. ( Vtx ` G ) ) /\ ( U e. ( Vtx ` G ) /\ W e. ( Vtx ` G ) ) ) ) /\ ( A =/= X /\ U =/= W ) ) -> G e. USGraph )
27 simprrr 
 |-  ( ( G e. USGraph /\ ( ( X e. ( Vtx ` G ) /\ A e. ( Vtx ` G ) ) /\ ( U e. ( Vtx ` G ) /\ W e. ( Vtx ` G ) ) ) ) -> W e. ( Vtx ` G ) )
28 27 adantr 
 |-  ( ( ( G e. USGraph /\ ( ( X e. ( Vtx ` G ) /\ A e. ( Vtx ` G ) ) /\ ( U e. ( Vtx ` G ) /\ W e. ( Vtx ` G ) ) ) ) /\ ( A =/= X /\ U =/= W ) ) -> W e. ( Vtx ` G ) )
29 simprrl 
 |-  ( ( G e. USGraph /\ ( ( X e. ( Vtx ` G ) /\ A e. ( Vtx ` G ) ) /\ ( U e. ( Vtx ` G ) /\ W e. ( Vtx ` G ) ) ) ) -> U e. ( Vtx ` G ) )
30 29 adantr 
 |-  ( ( ( G e. USGraph /\ ( ( X e. ( Vtx ` G ) /\ A e. ( Vtx ` G ) ) /\ ( U e. ( Vtx ` G ) /\ W e. ( Vtx ` G ) ) ) ) /\ ( A =/= X /\ U =/= W ) ) -> U e. ( Vtx ` G ) )
31 necom 
 |-  ( U =/= W <-> W =/= U )
32 31 biimpi 
 |-  ( U =/= W -> W =/= U )
33 32 adantl 
 |-  ( ( A =/= X /\ U =/= W ) -> W =/= U )
34 33 adantl 
 |-  ( ( ( G e. USGraph /\ ( ( X e. ( Vtx ` G ) /\ A e. ( Vtx ` G ) ) /\ ( U e. ( Vtx ` G ) /\ W e. ( Vtx ` G ) ) ) ) /\ ( A =/= X /\ U =/= W ) ) -> W =/= U )
35 28 30 34 3jca 
 |-  ( ( ( G e. USGraph /\ ( ( X e. ( Vtx ` G ) /\ A e. ( Vtx ` G ) ) /\ ( U e. ( Vtx ` G ) /\ W e. ( Vtx ` G ) ) ) ) /\ ( A =/= X /\ U =/= W ) ) -> ( W e. ( Vtx ` G ) /\ U e. ( Vtx ` G ) /\ W =/= U ) )
36 simprll 
 |-  ( ( G e. USGraph /\ ( ( X e. ( Vtx ` G ) /\ A e. ( Vtx ` G ) ) /\ ( U e. ( Vtx ` G ) /\ W e. ( Vtx ` G ) ) ) ) -> X e. ( Vtx ` G ) )
37 36 adantr 
 |-  ( ( ( G e. USGraph /\ ( ( X e. ( Vtx ` G ) /\ A e. ( Vtx ` G ) ) /\ ( U e. ( Vtx ` G ) /\ W e. ( Vtx ` G ) ) ) ) /\ ( A =/= X /\ U =/= W ) ) -> X e. ( Vtx ` G ) )
38 simprlr 
 |-  ( ( G e. USGraph /\ ( ( X e. ( Vtx ` G ) /\ A e. ( Vtx ` G ) ) /\ ( U e. ( Vtx ` G ) /\ W e. ( Vtx ` G ) ) ) ) -> A e. ( Vtx ` G ) )
39 38 adantr 
 |-  ( ( ( G e. USGraph /\ ( ( X e. ( Vtx ` G ) /\ A e. ( Vtx ` G ) ) /\ ( U e. ( Vtx ` G ) /\ W e. ( Vtx ` G ) ) ) ) /\ ( A =/= X /\ U =/= W ) ) -> A e. ( Vtx ` G ) )
40 necom 
 |-  ( A =/= X <-> X =/= A )
41 40 biimpi 
 |-  ( A =/= X -> X =/= A )
42 41 adantr 
 |-  ( ( A =/= X /\ U =/= W ) -> X =/= A )
43 42 adantl 
 |-  ( ( ( G e. USGraph /\ ( ( X e. ( Vtx ` G ) /\ A e. ( Vtx ` G ) ) /\ ( U e. ( Vtx ` G ) /\ W e. ( Vtx ` G ) ) ) ) /\ ( A =/= X /\ U =/= W ) ) -> X =/= A )
44 37 39 43 3jca 
 |-  ( ( ( G e. USGraph /\ ( ( X e. ( Vtx ` G ) /\ A e. ( Vtx ` G ) ) /\ ( U e. ( Vtx ` G ) /\ W e. ( Vtx ` G ) ) ) ) /\ ( A =/= X /\ U =/= W ) ) -> ( X e. ( Vtx ` G ) /\ A e. ( Vtx ` G ) /\ X =/= A ) )
45 26 35 44 3jca 
 |-  ( ( ( G e. USGraph /\ ( ( X e. ( Vtx ` G ) /\ A e. ( Vtx ` G ) ) /\ ( U e. ( Vtx ` G ) /\ W e. ( Vtx ` G ) ) ) ) /\ ( A =/= X /\ U =/= W ) ) -> ( G e. USGraph /\ ( W e. ( Vtx ` G ) /\ U e. ( Vtx ` G ) /\ W =/= U ) /\ ( X e. ( Vtx ` G ) /\ A e. ( Vtx ` G ) /\ X =/= A ) ) )
46 45 ad4ant14 
 |-  ( ( ( ( ( G e. USGraph /\ ( ( X e. ( Vtx ` G ) /\ A e. ( Vtx ` G ) ) /\ ( U e. ( Vtx ` G ) /\ W e. ( Vtx ` G ) ) ) ) /\ ( { U , X } e. E /\ { W , X } e. E ) ) /\ ( { U , A } e. E /\ { W , A } e. E ) ) /\ ( A =/= X /\ U =/= W ) ) -> ( G e. USGraph /\ ( W e. ( Vtx ` G ) /\ U e. ( Vtx ` G ) /\ W =/= U ) /\ ( X e. ( Vtx ` G ) /\ A e. ( Vtx ` G ) /\ X =/= A ) ) )
47 prcom 
 |-  { U , X } = { X , U }
48 47 eleq1i 
 |-  ( { U , X } e. E <-> { X , U } e. E )
49 48 biimpi 
 |-  ( { U , X } e. E -> { X , U } e. E )
50 49 anim1ci 
 |-  ( ( { U , X } e. E /\ { W , X } e. E ) -> ( { W , X } e. E /\ { X , U } e. E ) )
51 50 adantl 
 |-  ( ( ( G e. USGraph /\ ( ( X e. ( Vtx ` G ) /\ A e. ( Vtx ` G ) ) /\ ( U e. ( Vtx ` G ) /\ W e. ( Vtx ` G ) ) ) ) /\ ( { U , X } e. E /\ { W , X } e. E ) ) -> ( { W , X } e. E /\ { X , U } e. E ) )
52 prcom 
 |-  { W , A } = { A , W }
53 52 eleq1i 
 |-  ( { W , A } e. E <-> { A , W } e. E )
54 53 biimpi 
 |-  ( { W , A } e. E -> { A , W } e. E )
55 54 anim2i 
 |-  ( ( { U , A } e. E /\ { W , A } e. E ) -> ( { U , A } e. E /\ { A , W } e. E ) )
56 51 55 anim12i 
 |-  ( ( ( ( G e. USGraph /\ ( ( X e. ( Vtx ` G ) /\ A e. ( Vtx ` G ) ) /\ ( U e. ( Vtx ` G ) /\ W e. ( Vtx ` G ) ) ) ) /\ ( { U , X } e. E /\ { W , X } e. E ) ) /\ ( { U , A } e. E /\ { W , A } e. E ) ) -> ( ( { W , X } e. E /\ { X , U } e. E ) /\ ( { U , A } e. E /\ { A , W } e. E ) ) )
57 56 adantr 
 |-  ( ( ( ( ( G e. USGraph /\ ( ( X e. ( Vtx ` G ) /\ A e. ( Vtx ` G ) ) /\ ( U e. ( Vtx ` G ) /\ W e. ( Vtx ` G ) ) ) ) /\ ( { U , X } e. E /\ { W , X } e. E ) ) /\ ( { U , A } e. E /\ { W , A } e. E ) ) /\ ( A =/= X /\ U =/= W ) ) -> ( ( { W , X } e. E /\ { X , U } e. E ) /\ ( { U , A } e. E /\ { A , W } e. E ) ) )
58 14 1 4cyclusnfrgr 
 |-  ( ( G e. USGraph /\ ( W e. ( Vtx ` G ) /\ U e. ( Vtx ` G ) /\ W =/= U ) /\ ( X e. ( Vtx ` G ) /\ A e. ( Vtx ` G ) /\ X =/= A ) ) -> ( ( ( { W , X } e. E /\ { X , U } e. E ) /\ ( { U , A } e. E /\ { A , W } e. E ) ) -> G e/ FriendGraph ) )
59 46 57 58 sylc 
 |-  ( ( ( ( ( G e. USGraph /\ ( ( X e. ( Vtx ` G ) /\ A e. ( Vtx ` G ) ) /\ ( U e. ( Vtx ` G ) /\ W e. ( Vtx ` G ) ) ) ) /\ ( { U , X } e. E /\ { W , X } e. E ) ) /\ ( { U , A } e. E /\ { W , A } e. E ) ) /\ ( A =/= X /\ U =/= W ) ) -> G e/ FriendGraph )
60 df-nel 
 |-  ( G e/ FriendGraph <-> -. G e. FriendGraph )
61 59 60 sylib 
 |-  ( ( ( ( ( G e. USGraph /\ ( ( X e. ( Vtx ` G ) /\ A e. ( Vtx ` G ) ) /\ ( U e. ( Vtx ` G ) /\ W e. ( Vtx ` G ) ) ) ) /\ ( { U , X } e. E /\ { W , X } e. E ) ) /\ ( { U , A } e. E /\ { W , A } e. E ) ) /\ ( A =/= X /\ U =/= W ) ) -> -. G e. FriendGraph )
62 61 pm2.21d 
 |-  ( ( ( ( ( G e. USGraph /\ ( ( X e. ( Vtx ` G ) /\ A e. ( Vtx ` G ) ) /\ ( U e. ( Vtx ` G ) /\ W e. ( Vtx ` G ) ) ) ) /\ ( { U , X } e. E /\ { W , X } e. E ) ) /\ ( { U , A } e. E /\ { W , A } e. E ) ) /\ ( A =/= X /\ U =/= W ) ) -> ( G e. FriendGraph -> A = X ) )
63 62 ex 
 |-  ( ( ( ( G e. USGraph /\ ( ( X e. ( Vtx ` G ) /\ A e. ( Vtx ` G ) ) /\ ( U e. ( Vtx ` G ) /\ W e. ( Vtx ` G ) ) ) ) /\ ( { U , X } e. E /\ { W , X } e. E ) ) /\ ( { U , A } e. E /\ { W , A } e. E ) ) -> ( ( A =/= X /\ U =/= W ) -> ( G e. FriendGraph -> A = X ) ) )
64 63 com23 
 |-  ( ( ( ( G e. USGraph /\ ( ( X e. ( Vtx ` G ) /\ A e. ( Vtx ` G ) ) /\ ( U e. ( Vtx ` G ) /\ W e. ( Vtx ` G ) ) ) ) /\ ( { U , X } e. E /\ { W , X } e. E ) ) /\ ( { U , A } e. E /\ { W , A } e. E ) ) -> ( G e. FriendGraph -> ( ( A =/= X /\ U =/= W ) -> A = X ) ) )
65 64 exp41 
 |-  ( G e. USGraph -> ( ( ( X e. ( Vtx ` G ) /\ A e. ( Vtx ` G ) ) /\ ( U e. ( Vtx ` G ) /\ W e. ( Vtx ` G ) ) ) -> ( ( { U , X } e. E /\ { W , X } e. E ) -> ( ( { U , A } e. E /\ { W , A } e. E ) -> ( G e. FriendGraph -> ( ( A =/= X /\ U =/= W ) -> A = X ) ) ) ) ) )
66 65 com25 
 |-  ( G e. USGraph -> ( G e. FriendGraph -> ( ( { U , X } e. E /\ { W , X } e. E ) -> ( ( { U , A } e. E /\ { W , A } e. E ) -> ( ( ( X e. ( Vtx ` G ) /\ A e. ( Vtx ` G ) ) /\ ( U e. ( Vtx ` G ) /\ W e. ( Vtx ` G ) ) ) -> ( ( A =/= X /\ U =/= W ) -> A = X ) ) ) ) ) )
67 3 66 mpcom 
 |-  ( G e. FriendGraph -> ( ( { U , X } e. E /\ { W , X } e. E ) -> ( ( { U , A } e. E /\ { W , A } e. E ) -> ( ( ( X e. ( Vtx ` G ) /\ A e. ( Vtx ` G ) ) /\ ( U e. ( Vtx ` G ) /\ W e. ( Vtx ` G ) ) ) -> ( ( A =/= X /\ U =/= W ) -> A = X ) ) ) ) )
68 67 com15 
 |-  ( ( A =/= X /\ U =/= W ) -> ( ( { U , X } e. E /\ { W , X } e. E ) -> ( ( { U , A } e. E /\ { W , A } e. E ) -> ( ( ( X e. ( Vtx ` G ) /\ A e. ( Vtx ` G ) ) /\ ( U e. ( Vtx ` G ) /\ W e. ( Vtx ` G ) ) ) -> ( G e. FriendGraph -> A = X ) ) ) ) )
69 68 ex 
 |-  ( A =/= X -> ( U =/= W -> ( ( { U , X } e. E /\ { W , X } e. E ) -> ( ( { U , A } e. E /\ { W , A } e. E ) -> ( ( ( X e. ( Vtx ` G ) /\ A e. ( Vtx ` G ) ) /\ ( U e. ( Vtx ` G ) /\ W e. ( Vtx ` G ) ) ) -> ( G e. FriendGraph -> A = X ) ) ) ) ) )
70 25 69 pm2.61ine 
 |-  ( U =/= W -> ( ( { U , X } e. E /\ { W , X } e. E ) -> ( ( { U , A } e. E /\ { W , A } e. E ) -> ( ( ( X e. ( Vtx ` G ) /\ A e. ( Vtx ` G ) ) /\ ( U e. ( Vtx ` G ) /\ W e. ( Vtx ` G ) ) ) -> ( G e. FriendGraph -> A = X ) ) ) ) )
71 70 imp 
 |-  ( ( U =/= W /\ ( { U , X } e. E /\ { W , X } e. E ) ) -> ( ( { U , A } e. E /\ { W , A } e. E ) -> ( ( ( X e. ( Vtx ` G ) /\ A e. ( Vtx ` G ) ) /\ ( U e. ( Vtx ` G ) /\ W e. ( Vtx ` G ) ) ) -> ( G e. FriendGraph -> A = X ) ) ) )
72 71 com13 
 |-  ( ( ( X e. ( Vtx ` G ) /\ A e. ( Vtx ` G ) ) /\ ( U e. ( Vtx ` G ) /\ W e. ( Vtx ` G ) ) ) -> ( ( { U , A } e. E /\ { W , A } e. E ) -> ( ( U =/= W /\ ( { U , X } e. E /\ { W , X } e. E ) ) -> ( G e. FriendGraph -> A = X ) ) ) )
73 72 ex 
 |-  ( ( X e. ( Vtx ` G ) /\ A e. ( Vtx ` G ) ) -> ( ( U e. ( Vtx ` G ) /\ W e. ( Vtx ` G ) ) -> ( ( { U , A } e. E /\ { W , A } e. E ) -> ( ( U =/= W /\ ( { U , X } e. E /\ { W , X } e. E ) ) -> ( G e. FriendGraph -> A = X ) ) ) ) )
74 73 com25 
 |-  ( ( X e. ( Vtx ` G ) /\ A e. ( Vtx ` G ) ) -> ( G e. FriendGraph -> ( ( { U , A } e. E /\ { W , A } e. E ) -> ( ( U =/= W /\ ( { U , X } e. E /\ { W , X } e. E ) ) -> ( ( U e. ( Vtx ` G ) /\ W e. ( Vtx ` G ) ) -> A = X ) ) ) ) )
75 74 ex 
 |-  ( X e. ( Vtx ` G ) -> ( A e. ( Vtx ` G ) -> ( G e. FriendGraph -> ( ( { U , A } e. E /\ { W , A } e. E ) -> ( ( U =/= W /\ ( { U , X } e. E /\ { W , X } e. E ) ) -> ( ( U e. ( Vtx ` G ) /\ W e. ( Vtx ` G ) ) -> A = X ) ) ) ) ) )
76 14 nbgrcl 
 |-  ( U e. ( G NeighbVtx X ) -> X e. ( Vtx ` G ) )
77 76 2 eleq2s 
 |-  ( U e. D -> X e. ( Vtx ` G ) )
78 77 adantr 
 |-  ( ( U e. D /\ W e. D ) -> X e. ( Vtx ` G ) )
79 78 adantl 
 |-  ( ( G e. USGraph /\ ( U e. D /\ W e. D ) ) -> X e. ( Vtx ` G ) )
80 75 79 syl11 
 |-  ( A e. ( Vtx ` G ) -> ( ( G e. USGraph /\ ( U e. D /\ W e. D ) ) -> ( G e. FriendGraph -> ( ( { U , A } e. E /\ { W , A } e. E ) -> ( ( U =/= W /\ ( { U , X } e. E /\ { W , X } e. E ) ) -> ( ( U e. ( Vtx ` G ) /\ W e. ( Vtx ` G ) ) -> A = X ) ) ) ) ) )
81 80 com34 
 |-  ( A e. ( Vtx ` G ) -> ( ( G e. USGraph /\ ( U e. D /\ W e. D ) ) -> ( ( { U , A } e. E /\ { W , A } e. E ) -> ( G e. FriendGraph -> ( ( U =/= W /\ ( { U , X } e. E /\ { W , X } e. E ) ) -> ( ( U e. ( Vtx ` G ) /\ W e. ( Vtx ` G ) ) -> A = X ) ) ) ) ) )
82 81 impd 
 |-  ( A e. ( Vtx ` G ) -> ( ( ( G e. USGraph /\ ( U e. D /\ W e. D ) ) /\ ( { U , A } e. E /\ { W , A } e. E ) ) -> ( G e. FriendGraph -> ( ( U =/= W /\ ( { U , X } e. E /\ { W , X } e. E ) ) -> ( ( U e. ( Vtx ` G ) /\ W e. ( Vtx ` G ) ) -> A = X ) ) ) ) )
83 82 adantl 
 |-  ( ( U e. ( Vtx ` G ) /\ A e. ( Vtx ` G ) ) -> ( ( ( G e. USGraph /\ ( U e. D /\ W e. D ) ) /\ ( { U , A } e. E /\ { W , A } e. E ) ) -> ( G e. FriendGraph -> ( ( U =/= W /\ ( { U , X } e. E /\ { W , X } e. E ) ) -> ( ( U e. ( Vtx ` G ) /\ W e. ( Vtx ` G ) ) -> A = X ) ) ) ) )
84 22 83 mpcom 
 |-  ( ( ( G e. USGraph /\ ( U e. D /\ W e. D ) ) /\ ( { U , A } e. E /\ { W , A } e. E ) ) -> ( G e. FriendGraph -> ( ( U =/= W /\ ( { U , X } e. E /\ { W , X } e. E ) ) -> ( ( U e. ( Vtx ` G ) /\ W e. ( Vtx ` G ) ) -> A = X ) ) ) )
85 84 ex 
 |-  ( ( G e. USGraph /\ ( U e. D /\ W e. D ) ) -> ( ( { U , A } e. E /\ { W , A } e. E ) -> ( G e. FriendGraph -> ( ( U =/= W /\ ( { U , X } e. E /\ { W , X } e. E ) ) -> ( ( U e. ( Vtx ` G ) /\ W e. ( Vtx ` G ) ) -> A = X ) ) ) ) )
86 85 com25 
 |-  ( ( G e. USGraph /\ ( U e. D /\ W e. D ) ) -> ( ( U e. ( Vtx ` G ) /\ W e. ( Vtx ` G ) ) -> ( G e. FriendGraph -> ( ( U =/= W /\ ( { U , X } e. E /\ { W , X } e. E ) ) -> ( ( { U , A } e. E /\ { W , A } e. E ) -> A = X ) ) ) ) )
87 86 com14 
 |-  ( ( U =/= W /\ ( { U , X } e. E /\ { W , X } e. E ) ) -> ( ( U e. ( Vtx ` G ) /\ W e. ( Vtx ` G ) ) -> ( G e. FriendGraph -> ( ( G e. USGraph /\ ( U e. D /\ W e. D ) ) -> ( ( { U , A } e. E /\ { W , A } e. E ) -> A = X ) ) ) ) )
88 87 ex 
 |-  ( U =/= W -> ( ( { U , X } e. E /\ { W , X } e. E ) -> ( ( U e. ( Vtx ` G ) /\ W e. ( Vtx ` G ) ) -> ( G e. FriendGraph -> ( ( G e. USGraph /\ ( U e. D /\ W e. D ) ) -> ( ( { U , A } e. E /\ { W , A } e. E ) -> A = X ) ) ) ) ) )
89 88 com15 
 |-  ( ( G e. USGraph /\ ( U e. D /\ W e. D ) ) -> ( ( { U , X } e. E /\ { W , X } e. E ) -> ( ( U e. ( Vtx ` G ) /\ W e. ( Vtx ` G ) ) -> ( G e. FriendGraph -> ( U =/= W -> ( ( { U , A } e. E /\ { W , A } e. E ) -> A = X ) ) ) ) ) )
90 13 20 89 mp2d 
 |-  ( ( G e. USGraph /\ ( U e. D /\ W e. D ) ) -> ( G e. FriendGraph -> ( U =/= W -> ( ( { U , A } e. E /\ { W , A } e. E ) -> A = X ) ) ) )
91 90 ex 
 |-  ( G e. USGraph -> ( ( U e. D /\ W e. D ) -> ( G e. FriendGraph -> ( U =/= W -> ( ( { U , A } e. E /\ { W , A } e. E ) -> A = X ) ) ) ) )
92 91 com23 
 |-  ( G e. USGraph -> ( G e. FriendGraph -> ( ( U e. D /\ W e. D ) -> ( U =/= W -> ( ( { U , A } e. E /\ { W , A } e. E ) -> A = X ) ) ) ) )
93 3 92 mpcom 
 |-  ( G e. FriendGraph -> ( ( U e. D /\ W e. D ) -> ( U =/= W -> ( ( { U , A } e. E /\ { W , A } e. E ) -> A = X ) ) ) )
94 93 3imp 
 |-  ( ( G e. FriendGraph /\ ( U e. D /\ W e. D ) /\ U =/= W ) -> ( ( { U , A } e. E /\ { W , A } e. E ) -> A = X ) )