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 ∈ X ∧ B ∈ Y ∧ A ≠ B ∧ Vtx ⁡ G = A B → G ∉ FriendGraph

Proof

Step Hyp Ref Expression
1 neirr ⊢ ¬ A ≠ A
2 eqid ⊢ Edg ⁡ G = Edg ⁡ G
3 2 usgredgne ⊢ G ∈ USGraph ∧ A A ∈ Edg ⁡ G → A ≠ A
4 3 ex ⊢ G ∈ USGraph → A A ∈ Edg ⁡ G → A ≠ A
5 1 4 mtoi ⊢ G ∈ USGraph → ¬ A A ∈ Edg ⁡ G
6 5 adantl ⊢ A ∈ X ∧ B ∈ Y ∧ A ≠ B ∧ G ∈ USGraph → ¬ A A ∈ Edg ⁡ G
7 6 intnanrd ⊢ A ∈ X ∧ B ∈ Y ∧ A ≠ B ∧ G ∈ USGraph → ¬ A A ∈ Edg ⁡ G ∧ A B ∈ Edg ⁡ G
8 prex ⊢ A A ∈ V
9 prex ⊢ A B ∈ V
10 8 9 prss ⊢ A A ∈ Edg ⁡ G ∧ A B ∈ Edg ⁡ G ↔ A A A B ⊆ Edg ⁡ G
11 7 10 sylnib ⊢ A ∈ X ∧ B ∈ Y ∧ A ≠ B ∧ G ∈ USGraph → ¬ A A A B ⊆ Edg ⁡ G
12 neirr ⊢ ¬ B ≠ B
13 2 usgredgne ⊢ G ∈ USGraph ∧ B B ∈ Edg ⁡ G → B ≠ B
14 13 ex ⊢ G ∈ USGraph → B B ∈ Edg ⁡ G → B ≠ B
15 12 14 mtoi ⊢ G ∈ USGraph → ¬ B B ∈ Edg ⁡ G
16 15 adantl ⊢ A ∈ X ∧ B ∈ Y ∧ A ≠ B ∧ G ∈ USGraph → ¬ B B ∈ Edg ⁡ G
17 16 intnand ⊢ A ∈ X ∧ B ∈ Y ∧ A ≠ B ∧ G ∈ USGraph → ¬ B A ∈ Edg ⁡ G ∧ B B ∈ Edg ⁡ G
18 prex ⊢ B A ∈ V
19 prex ⊢ B B ∈ V
20 18 19 prss ⊢ B A ∈ Edg ⁡ G ∧ B B ∈ Edg ⁡ G ↔ B A B B ⊆ Edg ⁡ G
21 17 20 sylnib ⊢ A ∈ X ∧ B ∈ Y ∧ A ≠ B ∧ G ∈ USGraph → ¬ B A B B ⊆ Edg ⁡ G
22 ioran ⊢ ¬ A A A B ⊆ Edg ⁡ G ∨ B A B B ⊆ Edg ⁡ G ↔ ¬ A A A B ⊆ Edg ⁡ G ∧ ¬ B A B B ⊆ Edg ⁡ G
23 11 21 22 sylanbrc ⊢ A ∈ X ∧ B ∈ Y ∧ A ≠ B ∧ G ∈ USGraph → ¬ A A A B ⊆ Edg ⁡ G ∨ B A B B ⊆ 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 ⊆ Edg ⁡ G ↔ A A A B ⊆ 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 ⊆ Edg ⁡ G ↔ B A B B ⊆ Edg ⁡ G
32 27 31 rexprg ⊢ A ∈ X ∧ B ∈ Y → ∃ x ∈ A B x A x B ⊆ Edg ⁡ G ↔ A A A B ⊆ Edg ⁡ G ∨ B A B B ⊆ Edg ⁡ G
33 32 3adant3 ⊢ A ∈ X ∧ B ∈ Y ∧ A ≠ B → ∃ x ∈ A B x A x B ⊆ Edg ⁡ G ↔ A A A B ⊆ Edg ⁡ G ∨ B A B B ⊆ Edg ⁡ G
34 33 adantr ⊢ A ∈ X ∧ B ∈ Y ∧ A ≠ B ∧ G ∈ USGraph → ∃ x ∈ A B x A x B ⊆ Edg ⁡ G ↔ A A A B ⊆ Edg ⁡ G ∨ B A B B ⊆ Edg ⁡ G
35 23 34 mtbird ⊢ A ∈ X ∧ B ∈ Y ∧ A ≠ B ∧ G ∈ USGraph → ¬ ∃ x ∈ A B x A x B ⊆ Edg ⁡ G
36 reurex ⊢ ∃! x ∈ A B x A x B ⊆ Edg ⁡ G → ∃ x ∈ A B x A x B ⊆ Edg ⁡ G
37 35 36 nsyl ⊢ A ∈ X ∧ B ∈ Y ∧ A ≠ B ∧ G ∈ USGraph → ¬ ∃! x ∈ A B x A x B ⊆ Edg ⁡ G
38 37 orcd ⊢ A ∈ X ∧ B ∈ Y ∧ A ≠ B ∧ G ∈ USGraph → ¬ ∃! x ∈ A B x A x B ⊆ Edg ⁡ G ∨ ¬ ∃! x ∈ A B x B x A ⊆ Edg ⁡ G
39 rexnal ⊢ ∃ l ∈ A B ∖ A ¬ ∃! x ∈ A B x A x l ⊆ Edg ⁡ G ↔ ¬ ∀ l ∈ A B ∖ A ∃! x ∈ A B x A x l ⊆ Edg ⁡ G
40 39 bicomi ⊢ ¬ ∀ l ∈ A B ∖ A ∃! x ∈ A B x A x l ⊆ Edg ⁡ G ↔ ∃ l ∈ A B ∖ A ¬ ∃! x ∈ A B x A x l ⊆ Edg ⁡ G
41 40 a1i ⊢ A ∈ X ∧ B ∈ Y ∧ A ≠ B ∧ G ∈ USGraph → ¬ ∀ l ∈ A B ∖ A ∃! x ∈ A B x A x l ⊆ Edg ⁡ G ↔ ∃ l ∈ A B ∖ A ¬ ∃! x ∈ A B x A x l ⊆ Edg ⁡ G
42 difprsn1 ⊢ A ≠ B → A B ∖ A = B
43 42 3ad2ant3 ⊢ A ∈ X ∧ B ∈ Y ∧ A ≠ B → A B ∖ A = B
44 43 adantr ⊢ A ∈ X ∧ B ∈ Y ∧ A ≠ B ∧ G ∈ USGraph → A B ∖ A = B
45 44 rexeqdv ⊢ A ∈ X ∧ B ∈ Y ∧ A ≠ B ∧ G ∈ USGraph → ∃ l ∈ A B ∖ A ¬ ∃! x ∈ A B x A x l ⊆ Edg ⁡ G ↔ ∃ l ∈ B ¬ ∃! x ∈ A B x A x l ⊆ 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 ⊆ Edg ⁡ G ↔ x A x B ⊆ Edg ⁡ G
49 48 reubidv ⊢ l = B → ∃! x ∈ A B x A x l ⊆ Edg ⁡ G ↔ ∃! x ∈ A B x A x B ⊆ Edg ⁡ G
50 49 notbid ⊢ l = B → ¬ ∃! x ∈ A B x A x l ⊆ Edg ⁡ G ↔ ¬ ∃! x ∈ A B x A x B ⊆ Edg ⁡ G
51 50 rexsng ⊢ B ∈ Y → ∃ l ∈ B ¬ ∃! x ∈ A B x A x l ⊆ Edg ⁡ G ↔ ¬ ∃! x ∈ A B x A x B ⊆ Edg ⁡ G
52 51 3ad2ant2 ⊢ A ∈ X ∧ B ∈ Y ∧ A ≠ B → ∃ l ∈ B ¬ ∃! x ∈ A B x A x l ⊆ Edg ⁡ G ↔ ¬ ∃! x ∈ A B x A x B ⊆ Edg ⁡ G
53 52 adantr ⊢ A ∈ X ∧ B ∈ Y ∧ A ≠ B ∧ G ∈ USGraph → ∃ l ∈ B ¬ ∃! x ∈ A B x A x l ⊆ Edg ⁡ G ↔ ¬ ∃! x ∈ A B x A x B ⊆ Edg ⁡ G
54 41 45 53 3bitrd ⊢ A ∈ X ∧ B ∈ Y ∧ A ≠ B ∧ G ∈ USGraph → ¬ ∀ l ∈ A B ∖ A ∃! x ∈ A B x A x l ⊆ Edg ⁡ G ↔ ¬ ∃! x ∈ A B x A x B ⊆ Edg ⁡ G
55 rexnal ⊢ ∃ l ∈ A B ∖ B ¬ ∃! x ∈ A B x B x l ⊆ Edg ⁡ G ↔ ¬ ∀ l ∈ A B ∖ B ∃! x ∈ A B x B x l ⊆ Edg ⁡ G
56 55 bicomi ⊢ ¬ ∀ l ∈ A B ∖ B ∃! x ∈ A B x B x l ⊆ Edg ⁡ G ↔ ∃ l ∈ A B ∖ B ¬ ∃! x ∈ A B x B x l ⊆ Edg ⁡ G
57 56 a1i ⊢ A ∈ X ∧ B ∈ Y ∧ A ≠ B ∧ G ∈ USGraph → ¬ ∀ l ∈ A B ∖ B ∃! x ∈ A B x B x l ⊆ Edg ⁡ G ↔ ∃ l ∈ A B ∖ B ¬ ∃! x ∈ A B x B x l ⊆ Edg ⁡ G
58 difprsn2 ⊢ A ≠ B → A B ∖ B = A
59 58 3ad2ant3 ⊢ A ∈ X ∧ B ∈ Y ∧ A ≠ B → A B ∖ B = A
60 59 adantr ⊢ A ∈ X ∧ B ∈ Y ∧ A ≠ B ∧ G ∈ USGraph → A B ∖ B = A
61 60 rexeqdv ⊢ A ∈ X ∧ B ∈ Y ∧ A ≠ B ∧ G ∈ USGraph → ∃ l ∈ A B ∖ B ¬ ∃! x ∈ A B x B x l ⊆ Edg ⁡ G ↔ ∃ l ∈ A ¬ ∃! x ∈ A B x B x l ⊆ 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 ⊆ Edg ⁡ G ↔ x B x A ⊆ Edg ⁡ G
65 64 reubidv ⊢ l = A → ∃! x ∈ A B x B x l ⊆ Edg ⁡ G ↔ ∃! x ∈ A B x B x A ⊆ Edg ⁡ G
66 65 notbid ⊢ l = A → ¬ ∃! x ∈ A B x B x l ⊆ Edg ⁡ G ↔ ¬ ∃! x ∈ A B x B x A ⊆ Edg ⁡ G
67 66 rexsng ⊢ A ∈ X → ∃ l ∈ A ¬ ∃! x ∈ A B x B x l ⊆ Edg ⁡ G ↔ ¬ ∃! x ∈ A B x B x A ⊆ Edg ⁡ G
68 67 3ad2ant1 ⊢ A ∈ X ∧ B ∈ Y ∧ A ≠ B → ∃ l ∈ A ¬ ∃! x ∈ A B x B x l ⊆ Edg ⁡ G ↔ ¬ ∃! x ∈ A B x B x A ⊆ Edg ⁡ G
69 68 adantr ⊢ A ∈ X ∧ B ∈ Y ∧ A ≠ B ∧ G ∈ USGraph → ∃ l ∈ A ¬ ∃! x ∈ A B x B x l ⊆ Edg ⁡ G ↔ ¬ ∃! x ∈ A B x B x A ⊆ Edg ⁡ G
70 57 61 69 3bitrd ⊢ A ∈ X ∧ B ∈ Y ∧ A ≠ B ∧ G ∈ USGraph → ¬ ∀ l ∈ A B ∖ B ∃! x ∈ A B x B x l ⊆ Edg ⁡ G ↔ ¬ ∃! x ∈ A B x B x A ⊆ Edg ⁡ G
71 54 70 orbi12d ⊢ A ∈ X ∧ B ∈ Y ∧ A ≠ B ∧ G ∈ USGraph → ¬ ∀ l ∈ A B ∖ A ∃! x ∈ A B x A x l ⊆ Edg ⁡ G ∨ ¬ ∀ l ∈ A B ∖ B ∃! x ∈ A B x B x l ⊆ Edg ⁡ G ↔ ¬ ∃! x ∈ A B x A x B ⊆ Edg ⁡ G ∨ ¬ ∃! x ∈ A B x B x A ⊆ Edg ⁡ G
72 38 71 mpbird ⊢ A ∈ X ∧ B ∈ Y ∧ A ≠ B ∧ G ∈ USGraph → ¬ ∀ l ∈ A B ∖ A ∃! x ∈ A B x A x l ⊆ Edg ⁡ G ∨ ¬ ∀ l ∈ A B ∖ B ∃! x ∈ A B x B x l ⊆ 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 ⊆ Edg ⁡ G ↔ x A x l ⊆ Edg ⁡ G
78 77 reubidv ⊢ k = A → ∃! x ∈ A B x k x l ⊆ Edg ⁡ G ↔ ∃! x ∈ A B x A x l ⊆ Edg ⁡ G
79 74 78 raleqbidv ⊢ k = A → ∀ l ∈ A B ∖ k ∃! x ∈ A B x k x l ⊆ Edg ⁡ G ↔ ∀ l ∈ A B ∖ A ∃! x ∈ A B x A x l ⊆ Edg ⁡ G
80 79 notbid ⊢ k = A → ¬ ∀ l ∈ A B ∖ k ∃! x ∈ A B x k x l ⊆ Edg ⁡ G ↔ ¬ ∀ l ∈ A B ∖ A ∃! x ∈ A B x A x l ⊆ 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 ⊆ Edg ⁡ G ↔ x B x l ⊆ Edg ⁡ G
86 85 reubidv ⊢ k = B → ∃! x ∈ A B x k x l ⊆ Edg ⁡ G ↔ ∃! x ∈ A B x B x l ⊆ Edg ⁡ G
87 82 86 raleqbidv ⊢ k = B → ∀ l ∈ A B ∖ k ∃! x ∈ A B x k x l ⊆ Edg ⁡ G ↔ ∀ l ∈ A B ∖ B ∃! x ∈ A B x B x l ⊆ Edg ⁡ G
88 87 notbid ⊢ k = B → ¬ ∀ l ∈ A B ∖ k ∃! x ∈ A B x k x l ⊆ Edg ⁡ G ↔ ¬ ∀ l ∈ A B ∖ B ∃! x ∈ A B x B x l ⊆ Edg ⁡ G
89 80 88 rexprg ⊢ A ∈ X ∧ B ∈ Y → ∃ k ∈ A B ¬ ∀ l ∈ A B ∖ k ∃! x ∈ A B x k x l ⊆ Edg ⁡ G ↔ ¬ ∀ l ∈ A B ∖ A ∃! x ∈ A B x A x l ⊆ Edg ⁡ G ∨ ¬ ∀ l ∈ A B ∖ B ∃! x ∈ A B x B x l ⊆ Edg ⁡ G
90 89 3adant3 ⊢ A ∈ X ∧ B ∈ Y ∧ A ≠ B → ∃ k ∈ A B ¬ ∀ l ∈ A B ∖ k ∃! x ∈ A B x k x l ⊆ Edg ⁡ G ↔ ¬ ∀ l ∈ A B ∖ A ∃! x ∈ A B x A x l ⊆ Edg ⁡ G ∨ ¬ ∀ l ∈ A B ∖ B ∃! x ∈ A B x B x l ⊆ Edg ⁡ G
91 90 adantr ⊢ A ∈ X ∧ B ∈ Y ∧ A ≠ B ∧ G ∈ USGraph → ∃ k ∈ A B ¬ ∀ l ∈ A B ∖ k ∃! x ∈ A B x k x l ⊆ Edg ⁡ G ↔ ¬ ∀ l ∈ A B ∖ A ∃! x ∈ A B x A x l ⊆ Edg ⁡ G ∨ ¬ ∀ l ∈ A B ∖ B ∃! x ∈ A B x B x l ⊆ Edg ⁡ G
92 72 91 mpbird ⊢ A ∈ X ∧ B ∈ Y ∧ A ≠ B ∧ G ∈ USGraph → ∃ k ∈ A B ¬ ∀ l ∈ A B ∖ k ∃! x ∈ A B x k x l ⊆ Edg ⁡ G
93 rexnal ⊢ ∃ k ∈ A B ¬ ∀ l ∈ A B ∖ k ∃! x ∈ A B x k x l ⊆ Edg ⁡ G ↔ ¬ ∀ k ∈ A B ∀ l ∈ A B ∖ k ∃! x ∈ A B x k x l ⊆ Edg ⁡ G
94 92 93 sylib ⊢ A ∈ X ∧ B ∈ Y ∧ A ≠ B ∧ G ∈ USGraph → ¬ ∀ k ∈ A B ∀ l ∈ A B ∖ k ∃! x ∈ A B x k x l ⊆ Edg ⁡ G
95 94 intnand ⊢ A ∈ X ∧ B ∈ Y ∧ A ≠ B ∧ G ∈ USGraph → ¬ G ∈ USGraph ∧ ∀ k ∈ A B ∀ l ∈ A B ∖ k ∃! x ∈ A B x k x l ⊆ Edg ⁡ G
96 95 adantlr ⊢ A ∈ X ∧ B ∈ Y ∧ A ≠ B ∧ Vtx ⁡ G = A B ∧ G ∈ USGraph → ¬ G ∈ USGraph ∧ ∀ k ∈ A B ∀ l ∈ A B ∖ k ∃! x ∈ A B x k x l ⊆ 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 → ∃! x ∈ Vtx ⁡ G x k x l ⊆ Edg ⁡ G ↔ ∃! x ∈ A B x k x l ⊆ Edg ⁡ G
100 98 99 raleqbidv ⊢ Vtx ⁡ G = A B → ∀ l ∈ Vtx ⁡ G ∖ k ∃! x ∈ Vtx ⁡ G x k x l ⊆ Edg ⁡ G ↔ ∀ l ∈ A B ∖ k ∃! x ∈ A B x k x l ⊆ Edg ⁡ G
101 97 100 raleqbidv ⊢ Vtx ⁡ G = A B → ∀ k ∈ Vtx ⁡ G ∀ l ∈ Vtx ⁡ G ∖ k ∃! x ∈ Vtx ⁡ G x k x l ⊆ Edg ⁡ G ↔ ∀ k ∈ A B ∀ l ∈ A B ∖ k ∃! x ∈ A B x k x l ⊆ Edg ⁡ G
102 101 anbi2d ⊢ Vtx ⁡ G = A B → G ∈ USGraph ∧ ∀ k ∈ Vtx ⁡ G ∀ l ∈ Vtx ⁡ G ∖ k ∃! x ∈ Vtx ⁡ G x k x l ⊆ Edg ⁡ G ↔ G ∈ USGraph ∧ ∀ k ∈ A B ∀ l ∈ A B ∖ k ∃! x ∈ A B x k x l ⊆ Edg ⁡ G
103 102 notbid ⊢ Vtx ⁡ G = A B → ¬ G ∈ USGraph ∧ ∀ k ∈ Vtx ⁡ G ∀ l ∈ Vtx ⁡ G ∖ k ∃! x ∈ Vtx ⁡ G x k x l ⊆ Edg ⁡ G ↔ ¬ G ∈ USGraph ∧ ∀ k ∈ A B ∀ l ∈ A B ∖ k ∃! x ∈ A B x k x l ⊆ Edg ⁡ G
104 103 adantl ⊢ A ∈ X ∧ B ∈ Y ∧ A ≠ B ∧ Vtx ⁡ G = A B → ¬ G ∈ USGraph ∧ ∀ k ∈ Vtx ⁡ G ∀ l ∈ Vtx ⁡ G ∖ k ∃! x ∈ Vtx ⁡ G x k x l ⊆ Edg ⁡ G ↔ ¬ G ∈ USGraph ∧ ∀ k ∈ A B ∀ l ∈ A B ∖ k ∃! x ∈ A B x k x l ⊆ Edg ⁡ G
105 104 adantr ⊢ A ∈ X ∧ B ∈ Y ∧ A ≠ B ∧ Vtx ⁡ G = A B ∧ G ∈ USGraph → ¬ G ∈ USGraph ∧ ∀ k ∈ Vtx ⁡ G ∀ l ∈ Vtx ⁡ G ∖ k ∃! x ∈ Vtx ⁡ G x k x l ⊆ Edg ⁡ G ↔ ¬ G ∈ USGraph ∧ ∀ k ∈ A B ∀ l ∈ A B ∖ k ∃! x ∈ A B x k x l ⊆ Edg ⁡ G
106 96 105 mpbird ⊢ A ∈ X ∧ B ∈ Y ∧ A ≠ B ∧ Vtx ⁡ G = A B ∧ G ∈ USGraph → ¬ G ∈ USGraph ∧ ∀ k ∈ Vtx ⁡ G ∀ l ∈ Vtx ⁡ G ∖ k ∃! x ∈ Vtx ⁡ G x k x l ⊆ Edg ⁡ G
107 df-nel ⊢ G ∉ FriendGraph ↔ ¬ G ∈ FriendGraph
108 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
109 108 2 isfrgr ⊢ G ∈ FriendGraph ↔ G ∈ USGraph ∧ ∀ k ∈ Vtx ⁡ G ∀ l ∈ Vtx ⁡ G ∖ k ∃! x ∈ Vtx ⁡ G x k x l ⊆ Edg ⁡ G
110 107 109 xchbinx ⊢ G ∉ FriendGraph ↔ ¬ G ∈ USGraph ∧ ∀ k ∈ Vtx ⁡ G ∀ l ∈ Vtx ⁡ G ∖ k ∃! x ∈ Vtx ⁡ G x k x l ⊆ Edg ⁡ G
111 106 110 sylibr ⊢ A ∈ X ∧ B ∈ Y ∧ A ≠ B ∧ Vtx ⁡ G = A B ∧ G ∈ USGraph → G ∉ FriendGraph
112 111 expcom ⊢ G ∈ USGraph → A ∈ X ∧ B ∈ Y ∧ A ≠ B ∧ Vtx ⁡ G = A B → G ∉ FriendGraph
113 frgrusgr ⊢ G ∈ FriendGraph → G ∈ USGraph
114 113 con3i ⊢ ¬ G ∈ USGraph → ¬ G ∈ FriendGraph
115 114 107 sylibr ⊢ ¬ G ∈ USGraph → G ∉ FriendGraph
116 115 a1d ⊢ ¬ G ∈ USGraph → A ∈ X ∧ B ∈ Y ∧ A ≠ B ∧ Vtx ⁡ G = A B → G ∉ FriendGraph
117 112 116 pm2.61i ⊢ A ∈ X ∧ B ∈ Y ∧ A ≠ B ∧ Vtx ⁡ G = A B → G ∉ FriendGraph