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 ( ( ( 𝐴𝑋𝐵𝑌𝐴𝐵 ) ∧ ( Vtx ‘ 𝐺 ) = { 𝐴 , 𝐵 } ) → 𝐺 ∉ FriendGraph )

Proof

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