Metamath Proof Explorer

Theorem nfrgr2v

Description: Any graph with two (different) vertices is not a friendship graph. (Contributed by Alexander van der Vekens, 30-Sep-2017) (Proof shortened by Alexander van der Vekens, 13-Sep-2018) (Revised by AV, 29-Mar-2021)

Ref Expression
Assertion nfrgr2v 
|- ( ( ( A e. X /\ B e. Y /\ A =/= B ) /\ ( Vtx ` G ) = { A , B } ) -> G e/ FriendGraph )

Proof

Step Hyp Ref Expression
1 neirr 
 |-  -. A =/= A
2 eqid 
 |-  ( Edg ` G ) = ( Edg ` G )
3 2 usgredgne 
 |-  ( ( G e. USGraph /\ { A , A } e. ( Edg ` G ) ) -> A =/= A )
4 3 ex 
 |-  ( G e. USGraph -> ( { A , A } e. ( Edg ` G ) -> A =/= A ) )
5 1 4 mtoi 
 |-  ( G e. USGraph -> -. { A , A } e. ( Edg ` G ) )
6 5 adantl 
 |-  ( ( ( A e. X /\ B e. Y /\ A =/= B ) /\ G e. USGraph ) -> -. { A , A } e. ( Edg ` G ) )
7 6 intnanrd 
 |-  ( ( ( A e. X /\ B e. Y /\ A =/= B ) /\ G e. USGraph ) -> -. ( { A , A } e. ( Edg ` G ) /\ { A , B } e. ( Edg ` G ) ) )
8 prex 
 |-  { A , A } e. _V
9 prex 
 |-  { A , B } e. _V
10 8 9 prss 
 |-  ( ( { A , A } e. ( Edg ` G ) /\ { A , B } e. ( Edg ` G ) ) <-> { { A , A } , { A , B } } C_ ( Edg ` G ) )
11 7 10 sylnib 
 |-  ( ( ( A e. X /\ B e. Y /\ A =/= B ) /\ G e. USGraph ) -> -. { { A , A } , { A , B } } C_ ( Edg ` G ) )
12 neirr 
 |-  -. B =/= B
13 2 usgredgne 
 |-  ( ( G e. USGraph /\ { B , B } e. ( Edg ` G ) ) -> B =/= B )
14 13 ex 
 |-  ( G e. USGraph -> ( { B , B } e. ( Edg ` G ) -> B =/= B ) )
15 12 14 mtoi 
 |-  ( G e. USGraph -> -. { B , B } e. ( Edg ` G ) )
16 15 adantl 
 |-  ( ( ( A e. X /\ B e. Y /\ A =/= B ) /\ G e. USGraph ) -> -. { B , B } e. ( Edg ` G ) )
17 16 intnand 
 |-  ( ( ( A e. X /\ B e. Y /\ A =/= B ) /\ G e. USGraph ) -> -. ( { B , A } e. ( Edg ` G ) /\ { B , B } e. ( Edg ` G ) ) )
18 prex 
 |-  { B , A } e. _V
19 prex 
 |-  { B , B } e. _V
20 18 19 prss 
 |-  ( ( { B , A } e. ( Edg ` G ) /\ { B , B } e. ( Edg ` G ) ) <-> { { B , A } , { B , B } } C_ ( Edg ` G ) )
21 17 20 sylnib 
 |-  ( ( ( A e. X /\ B e. Y /\ A =/= B ) /\ G e. USGraph ) -> -. { { B , A } , { B , B } } C_ ( Edg ` G ) )
22 ioran 
 |-  ( -. ( { { A , A } , { A , B } } C_ ( Edg ` G ) \/ { { B , A } , { B , B } } C_ ( Edg ` G ) ) <-> ( -. { { A , A } , { A , B } } C_ ( Edg ` G ) /\ -. { { B , A } , { B , B } } C_ ( Edg ` G ) ) )
23 11 21 22 sylanbrc 
 |-  ( ( ( A e. X /\ B e. Y /\ A =/= B ) /\ G e. USGraph ) -> -. ( { { A , A } , { A , B } } C_ ( Edg ` G ) \/ { { B , A } , { B , B } } C_ ( Edg ` G ) ) )
24 preq1 
 |-  ( x = A -> { x , A } = { A , A } )
25 preq1 
 |-  ( x = A -> { x , B } = { A , B } )
26 24 25 preq12d 
 |-  ( x = A -> { { x , A } , { x , B } } = { { A , A } , { A , B } } )
27 26 sseq1d 
 |-  ( x = A -> ( { { x , A } , { x , B } } C_ ( Edg ` G ) <-> { { A , A } , { A , B } } C_ ( Edg ` G ) ) )
28 preq1 
 |-  ( x = B -> { x , A } = { B , A } )
29 preq1 
 |-  ( x = B -> { x , B } = { B , B } )
30 28 29 preq12d 
 |-  ( x = B -> { { x , A } , { x , B } } = { { B , A } , { B , B } } )
31 30 sseq1d 
 |-  ( x = B -> ( { { x , A } , { x , B } } C_ ( Edg ` G ) <-> { { B , A } , { B , B } } C_ ( Edg ` G ) ) )
32 27 31 rexprg 
 |-  ( ( A e. X /\ B e. Y ) -> ( E. x e. { A , B } { { x , A } , { x , B } } C_ ( Edg ` G ) <-> ( { { A , A } , { A , B } } C_ ( Edg ` G ) \/ { { B , A } , { B , B } } C_ ( Edg ` G ) ) ) )
33 32 3adant3 
 |-  ( ( A e. X /\ B e. Y /\ A =/= B ) -> ( E. x e. { A , B } { { x , A } , { x , B } } C_ ( Edg ` G ) <-> ( { { A , A } , { A , B } } C_ ( Edg ` G ) \/ { { B , A } , { B , B } } C_ ( Edg ` G ) ) ) )
34 33 adantr 
 |-  ( ( ( A e. X /\ B e. Y /\ A =/= B ) /\ G e. USGraph ) -> ( E. x e. { A , B } { { x , A } , { x , B } } C_ ( Edg ` G ) <-> ( { { A , A } , { A , B } } C_ ( Edg ` G ) \/ { { B , A } , { B , B } } C_ ( Edg ` G ) ) ) )
35 23 34 mtbird 
 |-  ( ( ( A e. X /\ B e. Y /\ A =/= B ) /\ G e. USGraph ) -> -. E. x e. { A , B } { { x , A } , { x , B } } C_ ( Edg ` G ) )
36 reurex 
 |-  ( E! x e. { A , B } { { x , A } , { x , B } } C_ ( Edg ` G ) -> E. x e. { A , B } { { x , A } , { x , B } } C_ ( Edg ` G ) )
37 35 36 nsyl 
 |-  ( ( ( A e. X /\ B e. Y /\ A =/= B ) /\ G e. USGraph ) -> -. E! x e. { A , B } { { x , A } , { x , B } } C_ ( Edg ` G ) )
38 37 orcd 
 |-  ( ( ( A e. X /\ B e. Y /\ A =/= B ) /\ G e. USGraph ) -> ( -. E! x e. { A , B } { { x , A } , { x , B } } C_ ( Edg ` G ) \/ -. E! x e. { A , B } { { x , B } , { x , A } } C_ ( Edg ` G ) ) )
39 rexnal 
 |-  ( E. l e. ( { A , B } \ { A } ) -. E! x e. { A , B } { { x , A } , { x , l } } C_ ( Edg ` G ) <-> -. A. l e. ( { A , B } \ { A } ) E! x e. { A , B } { { x , A } , { x , l } } C_ ( Edg ` G ) )
40 39 bicomi 
 |-  ( -. A. l e. ( { A , B } \ { A } ) E! x e. { A , B } { { x , A } , { x , l } } C_ ( Edg ` G ) <-> E. l e. ( { A , B } \ { A } ) -. E! x e. { A , B } { { x , A } , { x , l } } C_ ( Edg ` G ) )
41 40 a1i 
 |-  ( ( ( A e. X /\ B e. Y /\ A =/= B ) /\ G e. USGraph ) -> ( -. A. l e. ( { A , B } \ { A } ) E! x e. { A , B } { { x , A } , { x , l } } C_ ( Edg ` G ) <-> E. l e. ( { A , B } \ { A } ) -. E! x e. { A , B } { { x , A } , { x , l } } C_ ( Edg ` G ) ) )
42 difprsn1 
 |-  ( A =/= B -> ( { A , B } \ { A } ) = { B } )
43 42 3ad2ant3 
 |-  ( ( A e. X /\ B e. Y /\ A =/= B ) -> ( { A , B } \ { A } ) = { B } )
44 43 adantr 
 |-  ( ( ( A e. X /\ B e. Y /\ A =/= B ) /\ G e. USGraph ) -> ( { A , B } \ { A } ) = { B } )
45 44 rexeqdv 
 |-  ( ( ( A e. X /\ B e. Y /\ A =/= B ) /\ G e. USGraph ) -> ( E. l e. ( { A , B } \ { A } ) -. E! x e. { A , B } { { x , A } , { x , l } } C_ ( Edg ` G ) <-> E. l e. { B } -. E! x e. { A , B } { { x , A } , { x , l } } C_ ( Edg ` G ) ) )
46 preq2 
 |-  ( l = B -> { x , l } = { x , B } )
47 46 preq2d 
 |-  ( l = B -> { { x , A } , { x , l } } = { { x , A } , { x , B } } )
48 47 sseq1d 
 |-  ( l = B -> ( { { x , A } , { x , l } } C_ ( Edg ` G ) <-> { { x , A } , { x , B } } C_ ( Edg ` G ) ) )
49 48 reubidv 
 |-  ( l = B -> ( E! x e. { A , B } { { x , A } , { x , l } } C_ ( Edg ` G ) <-> E! x e. { A , B } { { x , A } , { x , B } } C_ ( Edg ` G ) ) )
50 49 notbid 
 |-  ( l = B -> ( -. E! x e. { A , B } { { x , A } , { x , l } } C_ ( Edg ` G ) <-> -. E! x e. { A , B } { { x , A } , { x , B } } C_ ( Edg ` G ) ) )
51 50 rexsng 
 |-  ( B e. Y -> ( E. l e. { B } -. E! x e. { A , B } { { x , A } , { x , l } } C_ ( Edg ` G ) <-> -. E! x e. { A , B } { { x , A } , { x , B } } C_ ( Edg ` G ) ) )
52 51 3ad2ant2 
 |-  ( ( A e. X /\ B e. Y /\ A =/= B ) -> ( E. l e. { B } -. E! x e. { A , B } { { x , A } , { x , l } } C_ ( Edg ` G ) <-> -. E! x e. { A , B } { { x , A } , { x , B } } C_ ( Edg ` G ) ) )
53 52 adantr 
 |-  ( ( ( A e. X /\ B e. Y /\ A =/= B ) /\ G e. USGraph ) -> ( E. l e. { B } -. E! x e. { A , B } { { x , A } , { x , l } } C_ ( Edg ` G ) <-> -. E! x e. { A , B } { { x , A } , { x , B } } C_ ( Edg ` G ) ) )
54 41 45 53 3bitrd 
 |-  ( ( ( A e. X /\ B e. Y /\ A =/= B ) /\ G e. USGraph ) -> ( -. A. l e. ( { A , B } \ { A } ) E! x e. { A , B } { { x , A } , { x , l } } C_ ( Edg ` G ) <-> -. E! x e. { A , B } { { x , A } , { x , B } } C_ ( Edg ` G ) ) )
55 rexnal 
 |-  ( E. l e. ( { A , B } \ { B } ) -. E! x e. { A , B } { { x , B } , { x , l } } C_ ( Edg ` G ) <-> -. A. l e. ( { A , B } \ { B } ) E! x e. { A , B } { { x , B } , { x , l } } C_ ( Edg ` G ) )
56 55 bicomi 
 |-  ( -. A. l e. ( { A , B } \ { B } ) E! x e. { A , B } { { x , B } , { x , l } } C_ ( Edg ` G ) <-> E. l e. ( { A , B } \ { B } ) -. E! x e. { A , B } { { x , B } , { x , l } } C_ ( Edg ` G ) )
57 56 a1i 
 |-  ( ( ( A e. X /\ B e. Y /\ A =/= B ) /\ G e. USGraph ) -> ( -. A. l e. ( { A , B } \ { B } ) E! x e. { A , B } { { x , B } , { x , l } } C_ ( Edg ` G ) <-> E. l e. ( { A , B } \ { B } ) -. E! x e. { A , B } { { x , B } , { x , l } } C_ ( Edg ` G ) ) )
58 difprsn2 
 |-  ( A =/= B -> ( { A , B } \ { B } ) = { A } )
59 58 3ad2ant3 
 |-  ( ( A e. X /\ B e. Y /\ A =/= B ) -> ( { A , B } \ { B } ) = { A } )
60 59 adantr 
 |-  ( ( ( A e. X /\ B e. Y /\ A =/= B ) /\ G e. USGraph ) -> ( { A , B } \ { B } ) = { A } )
61 60 rexeqdv 
 |-  ( ( ( A e. X /\ B e. Y /\ A =/= B ) /\ G e. USGraph ) -> ( E. l e. ( { A , B } \ { B } ) -. E! x e. { A , B } { { x , B } , { x , l } } C_ ( Edg ` G ) <-> E. l e. { A } -. E! x e. { A , B } { { x , B } , { x , l } } C_ ( Edg ` G ) ) )
62 preq2 
 |-  ( l = A -> { x , l } = { x , A } )
63 62 preq2d 
 |-  ( l = A -> { { x , B } , { x , l } } = { { x , B } , { x , A } } )
64 63 sseq1d 
 |-  ( l = A -> ( { { x , B } , { x , l } } C_ ( Edg ` G ) <-> { { x , B } , { x , A } } C_ ( Edg ` G ) ) )
65 64 reubidv 
 |-  ( l = A -> ( E! x e. { A , B } { { x , B } , { x , l } } C_ ( Edg ` G ) <-> E! x e. { A , B } { { x , B } , { x , A } } C_ ( Edg ` G ) ) )
66 65 notbid 
 |-  ( l = A -> ( -. E! x e. { A , B } { { x , B } , { x , l } } C_ ( Edg ` G ) <-> -. E! x e. { A , B } { { x , B } , { x , A } } C_ ( Edg ` G ) ) )
67 66 rexsng 
 |-  ( A e. X -> ( E. l e. { A } -. E! x e. { A , B } { { x , B } , { x , l } } C_ ( Edg ` G ) <-> -. E! x e. { A , B } { { x , B } , { x , A } } C_ ( Edg ` G ) ) )
68 67 3ad2ant1 
 |-  ( ( A e. X /\ B e. Y /\ A =/= B ) -> ( E. l e. { A } -. E! x e. { A , B } { { x , B } , { x , l } } C_ ( Edg ` G ) <-> -. E! x e. { A , B } { { x , B } , { x , A } } C_ ( Edg ` G ) ) )
69 68 adantr 
 |-  ( ( ( A e. X /\ B e. Y /\ A =/= B ) /\ G e. USGraph ) -> ( E. l e. { A } -. E! x e. { A , B } { { x , B } , { x , l } } C_ ( Edg ` G ) <-> -. E! x e. { A , B } { { x , B } , { x , A } } C_ ( Edg ` G ) ) )
70 57 61 69 3bitrd 
 |-  ( ( ( A e. X /\ B e. Y /\ A =/= B ) /\ G e. USGraph ) -> ( -. A. l e. ( { A , B } \ { B } ) E! x e. { A , B } { { x , B } , { x , l } } C_ ( Edg ` G ) <-> -. E! x e. { A , B } { { x , B } , { x , A } } C_ ( Edg ` G ) ) )
71 54 70 orbi12d 
 |-  ( ( ( A e. X /\ B e. Y /\ A =/= B ) /\ G e. USGraph ) -> ( ( -. A. l e. ( { A , B } \ { A } ) E! x e. { A , B } { { x , A } , { x , l } } C_ ( Edg ` G ) \/ -. A. l e. ( { A , B } \ { B } ) E! x e. { A , B } { { x , B } , { x , l } } C_ ( Edg ` G ) ) <-> ( -. E! x e. { A , B } { { x , A } , { x , B } } C_ ( Edg ` G ) \/ -. E! x e. { A , B } { { x , B } , { x , A } } C_ ( Edg ` G ) ) ) )
72 38 71 mpbird 
 |-  ( ( ( A e. X /\ B e. Y /\ A =/= B ) /\ G e. USGraph ) -> ( -. A. l e. ( { A , B } \ { A } ) E! x e. { A , B } { { x , A } , { x , l } } C_ ( Edg ` G ) \/ -. A. l e. ( { A , B } \ { B } ) E! x e. { A , B } { { x , B } , { x , l } } C_ ( Edg ` G ) ) )
73 sneq 
 |-  ( k = A -> { k } = { A } )
74 73 difeq2d 
 |-  ( k = A -> ( { A , B } \ { k } ) = ( { A , B } \ { A } ) )
75 preq2 
 |-  ( k = A -> { x , k } = { x , A } )
76 75 preq1d 
 |-  ( k = A -> { { x , k } , { x , l } } = { { x , A } , { x , l } } )
77 76 sseq1d 
 |-  ( k = A -> ( { { x , k } , { x , l } } C_ ( Edg ` G ) <-> { { x , A } , { x , l } } C_ ( Edg ` G ) ) )
78 77 reubidv 
 |-  ( k = A -> ( E! x e. { A , B } { { x , k } , { x , l } } C_ ( Edg ` G ) <-> E! x e. { A , B } { { x , A } , { x , l } } C_ ( Edg ` G ) ) )
79 74 78 raleqbidv 
 |-  ( k = A -> ( A. l e. ( { A , B } \ { k } ) E! x e. { A , B } { { x , k } , { x , l } } C_ ( Edg ` G ) <-> A. l e. ( { A , B } \ { A } ) E! x e. { A , B } { { x , A } , { x , l } } C_ ( Edg ` G ) ) )
80 79 notbid 
 |-  ( k = A -> ( -. A. l e. ( { A , B } \ { k } ) E! x e. { A , B } { { x , k } , { x , l } } C_ ( Edg ` G ) <-> -. A. l e. ( { A , B } \ { A } ) E! x e. { A , B } { { x , A } , { x , l } } C_ ( Edg ` G ) ) )
81 sneq 
 |-  ( k = B -> { k } = { B } )
82 81 difeq2d 
 |-  ( k = B -> ( { A , B } \ { k } ) = ( { A , B } \ { B } ) )
83 preq2 
 |-  ( k = B -> { x , k } = { x , B } )
84 83 preq1d 
 |-  ( k = B -> { { x , k } , { x , l } } = { { x , B } , { x , l } } )
85 84 sseq1d 
 |-  ( k = B -> ( { { x , k } , { x , l } } C_ ( Edg ` G ) <-> { { x , B } , { x , l } } C_ ( Edg ` G ) ) )
86 85 reubidv 
 |-  ( k = B -> ( E! x e. { A , B } { { x , k } , { x , l } } C_ ( Edg ` G ) <-> E! x e. { A , B } { { x , B } , { x , l } } C_ ( Edg ` G ) ) )
87 82 86 raleqbidv 
 |-  ( k = B -> ( A. l e. ( { A , B } \ { k } ) E! x e. { A , B } { { x , k } , { x , l } } C_ ( Edg ` G ) <-> A. l e. ( { A , B } \ { B } ) E! x e. { A , B } { { x , B } , { x , l } } C_ ( Edg ` G ) ) )
88 87 notbid 
 |-  ( k = B -> ( -. A. l e. ( { A , B } \ { k } ) E! x e. { A , B } { { x , k } , { x , l } } C_ ( Edg ` G ) <-> -. A. l e. ( { A , B } \ { B } ) E! x e. { A , B } { { x , B } , { x , l } } C_ ( Edg ` G ) ) )
89 80 88 rexprg 
 |-  ( ( A e. X /\ B e. Y ) -> ( E. k e. { A , B } -. A. l e. ( { A , B } \ { k } ) E! x e. { A , B } { { x , k } , { x , l } } C_ ( Edg ` G ) <-> ( -. A. l e. ( { A , B } \ { A } ) E! x e. { A , B } { { x , A } , { x , l } } C_ ( Edg ` G ) \/ -. A. l e. ( { A , B } \ { B } ) E! x e. { A , B } { { x , B } , { x , l } } C_ ( Edg ` G ) ) ) )
90 89 3adant3 
 |-  ( ( A e. X /\ B e. Y /\ A =/= B ) -> ( E. k e. { A , B } -. A. l e. ( { A , B } \ { k } ) E! x e. { A , B } { { x , k } , { x , l } } C_ ( Edg ` G ) <-> ( -. A. l e. ( { A , B } \ { A } ) E! x e. { A , B } { { x , A } , { x , l } } C_ ( Edg ` G ) \/ -. A. l e. ( { A , B } \ { B } ) E! x e. { A , B } { { x , B } , { x , l } } C_ ( Edg ` G ) ) ) )
91 90 adantr 
 |-  ( ( ( A e. X /\ B e. Y /\ A =/= B ) /\ G e. USGraph ) -> ( E. k e. { A , B } -. A. l e. ( { A , B } \ { k } ) E! x e. { A , B } { { x , k } , { x , l } } C_ ( Edg ` G ) <-> ( -. A. l e. ( { A , B } \ { A } ) E! x e. { A , B } { { x , A } , { x , l } } C_ ( Edg ` G ) \/ -. A. l e. ( { A , B } \ { B } ) E! x e. { A , B } { { x , B } , { x , l } } C_ ( Edg ` G ) ) ) )
92 72 91 mpbird 
 |-  ( ( ( A e. X /\ B e. Y /\ A =/= B ) /\ G e. USGraph ) -> E. k e. { A , B } -. A. l e. ( { A , B } \ { k } ) E! x e. { A , B } { { x , k } , { x , l } } C_ ( Edg ` G ) )
93 rexnal 
 |-  ( E. k e. { A , B } -. A. l e. ( { A , B } \ { k } ) E! x e. { A , B } { { x , k } , { x , l } } C_ ( Edg ` G ) <-> -. A. k e. { A , B } A. l e. ( { A , B } \ { k } ) E! x e. { A , B } { { x , k } , { x , l } } C_ ( Edg ` G ) )
94 92 93 sylib 
 |-  ( ( ( A e. X /\ B e. Y /\ A =/= B ) /\ G e. USGraph ) -> -. A. k e. { A , B } A. l e. ( { A , B } \ { k } ) E! x e. { A , B } { { x , k } , { x , l } } C_ ( Edg ` G ) )
95 94 intnand 
 |-  ( ( ( A e. X /\ B e. Y /\ A =/= B ) /\ G e. USGraph ) -> -. ( G e. USGraph /\ A. k e. { A , B } A. l e. ( { A , B } \ { k } ) E! x e. { A , B } { { x , k } , { x , l } } C_ ( Edg ` G ) ) )
96 95 adantlr 
 |-  ( ( ( ( A e. X /\ B e. Y /\ A =/= B ) /\ ( Vtx ` G ) = { A , B } ) /\ G e. USGraph ) -> -. ( G e. USGraph /\ A. k e. { A , B } A. l e. ( { A , B } \ { k } ) E! x e. { A , B } { { x , k } , { x , l } } C_ ( Edg ` G ) ) )
97 id 
 |-  ( ( Vtx ` G ) = { A , B } -> ( Vtx ` G ) = { A , B } )
98 difeq1 
 |-  ( ( Vtx ` G ) = { A , B } -> ( ( Vtx ` G ) \ { k } ) = ( { A , B } \ { k } ) )
99 reueq1 
 |-  ( ( Vtx ` G ) = { A , B } -> ( E! x e. ( Vtx ` G ) { { x , k } , { x , l } } C_ ( Edg ` G ) <-> E! x e. { A , B } { { x , k } , { x , l } } C_ ( Edg ` G ) ) )
100 98 99 raleqbidv 
 |-  ( ( Vtx ` G ) = { A , B } -> ( A. l e. ( ( Vtx ` G ) \ { k } ) E! x e. ( Vtx ` G ) { { x , k } , { x , l } } C_ ( Edg ` G ) <-> A. l e. ( { A , B } \ { k } ) E! x e. { A , B } { { x , k } , { x , l } } C_ ( Edg ` G ) ) )
101 97 100 raleqbidv 
 |-  ( ( Vtx ` G ) = { A , B } -> ( A. k e. ( Vtx ` G ) A. l e. ( ( Vtx ` G ) \ { k } ) E! x e. ( Vtx ` G ) { { x , k } , { x , l } } C_ ( Edg ` G ) <-> A. k e. { A , B } A. l e. ( { A , B } \ { k } ) E! x e. { A , B } { { x , k } , { x , l } } C_ ( Edg ` G ) ) )
102 101 anbi2d 
 |-  ( ( Vtx ` G ) = { A , B } -> ( ( G e. USGraph /\ A. k e. ( Vtx ` G ) A. l e. ( ( Vtx ` G ) \ { k } ) E! x e. ( Vtx ` G ) { { x , k } , { x , l } } C_ ( Edg ` G ) ) <-> ( G e. USGraph /\ A. k e. { A , B } A. l e. ( { A , B } \ { k } ) E! x e. { A , B } { { x , k } , { x , l } } C_ ( Edg ` G ) ) ) )
103 102 notbid 
 |-  ( ( Vtx ` G ) = { A , B } -> ( -. ( G e. USGraph /\ A. k e. ( Vtx ` G ) A. l e. ( ( Vtx ` G ) \ { k } ) E! x e. ( Vtx ` G ) { { x , k } , { x , l } } C_ ( Edg ` G ) ) <-> -. ( G e. USGraph /\ A. k e. { A , B } A. l e. ( { A , B } \ { k } ) E! x e. { A , B } { { x , k } , { x , l } } C_ ( Edg ` G ) ) ) )
104 103 adantl 
 |-  ( ( ( A e. X /\ B e. Y /\ A =/= B ) /\ ( Vtx ` G ) = { A , B } ) -> ( -. ( G e. USGraph /\ A. k e. ( Vtx ` G ) A. l e. ( ( Vtx ` G ) \ { k } ) E! x e. ( Vtx ` G ) { { x , k } , { x , l } } C_ ( Edg ` G ) ) <-> -. ( G e. USGraph /\ A. k e. { A , B } A. l e. ( { A , B } \ { k } ) E! x e. { A , B } { { x , k } , { x , l } } C_ ( Edg ` G ) ) ) )
105 104 adantr 
 |-  ( ( ( ( A e. X /\ B e. Y /\ A =/= B ) /\ ( Vtx ` G ) = { A , B } ) /\ G e. USGraph ) -> ( -. ( G e. USGraph /\ A. k e. ( Vtx ` G ) A. l e. ( ( Vtx ` G ) \ { k } ) E! x e. ( Vtx ` G ) { { x , k } , { x , l } } C_ ( Edg ` G ) ) <-> -. ( G e. USGraph /\ A. k e. { A , B } A. l e. ( { A , B } \ { k } ) E! x e. { A , B } { { x , k } , { x , l } } C_ ( Edg ` G ) ) ) )
106 96 105 mpbird 
 |-  ( ( ( ( A e. X /\ B e. Y /\ A =/= B ) /\ ( Vtx ` G ) = { A , B } ) /\ G e. USGraph ) -> -. ( G e. USGraph /\ A. k e. ( Vtx ` G ) A. l e. ( ( Vtx ` G ) \ { k } ) E! x e. ( Vtx ` G ) { { x , k } , { x , l } } C_ ( Edg ` G ) ) )
107 df-nel 
 |-  ( G e/ FriendGraph <-> -. G e. FriendGraph )
108 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
109 108 2 isfrgr 
 |-  ( G e. FriendGraph <-> ( G e. USGraph /\ A. k e. ( Vtx ` G ) A. l e. ( ( Vtx ` G ) \ { k } ) E! x e. ( Vtx ` G ) { { x , k } , { x , l } } C_ ( Edg ` G ) ) )
110 107 109 xchbinx 
 |-  ( G e/ FriendGraph <-> -. ( G e. USGraph /\ A. k e. ( Vtx ` G ) A. l e. ( ( Vtx ` G ) \ { k } ) E! x e. ( Vtx ` G ) { { x , k } , { x , l } } C_ ( Edg ` G ) ) )
111 106 110 sylibr 
 |-  ( ( ( ( A e. X /\ B e. Y /\ A =/= B ) /\ ( Vtx ` G ) = { A , B } ) /\ G e. USGraph ) -> G e/ FriendGraph )
112 111 expcom 
 |-  ( G e. USGraph -> ( ( ( A e. X /\ B e. Y /\ A =/= B ) /\ ( Vtx ` G ) = { A , B } ) -> G e/ FriendGraph ) )
113 frgrusgr 
 |-  ( G e. FriendGraph -> G e. USGraph )
114 113 con3i 
 |-  ( -. G e. USGraph -> -. G e. FriendGraph )
115 114 107 sylibr 
 |-  ( -. G e. USGraph -> G e/ FriendGraph )
116 115 a1d 
 |-  ( -. G e. USGraph -> ( ( ( A e. X /\ B e. Y /\ A =/= B ) /\ ( Vtx ` G ) = { A , B } ) -> G e/ FriendGraph ) )
117 112 116 pm2.61i 
 |-  ( ( ( A e. X /\ B e. Y /\ A =/= B ) /\ ( Vtx ` G ) = { A , B } ) -> G e/ FriendGraph )