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 ⊢ 𝐸 = ( Edg ‘ 𝐺 )
frgrnbnb.n ⊢ 𝐷 = ( 𝐺 NeighbVtx 𝑋 )
Assertion frgrnbnb ( ( 𝐺 ∈ FriendGraph ∧ ( 𝑈 ∈ 𝐷 ∧ 𝑊 ∈ 𝐷 ) ∧ 𝑈 ≠ 𝑊 ) → ( ( { 𝑈 , 𝐴 } ∈ 𝐸 ∧ { 𝑊 , 𝐴 } ∈ 𝐸 ) → 𝐴 = 𝑋 ) )

Proof

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