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 )