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=AB→G∉FriendGraph

Proof

Step Hyp Ref Expression
1 neirr ⊢¬A≠A
2 eqid ⊢Edg⁡G=Edg⁡G
3 2 usgredgne ⊢G∈USGraph∧AA∈Edg⁡G→A≠A
4 3 ex ⊢G∈USGraph→AA∈Edg⁡G→A≠A
5 1 4 mtoi ⊢G∈USGraph→¬AA∈Edg⁡G
6 5 adantl ⊢A∈X∧B∈Y∧A≠B∧G∈USGraph→¬AA∈Edg⁡G
7 6 intnanrd ⊢A∈X∧B∈Y∧A≠B∧G∈USGraph→¬AA∈Edg⁡G∧AB∈Edg⁡G
8 prex ⊢AA∈V
9 prex ⊢AB∈V
10 8 9 prss ⊢AA∈Edg⁡G∧AB∈Edg⁡G↔AAAB⊆Edg⁡G
11 7 10 sylnib ⊢A∈X∧B∈Y∧A≠B∧G∈USGraph→¬AAAB⊆Edg⁡G
12 neirr ⊢¬B≠B
13 2 usgredgne ⊢G∈USGraph∧BB∈Edg⁡G→B≠B
14 13 ex ⊢G∈USGraph→BB∈Edg⁡G→B≠B
15 12 14 mtoi ⊢G∈USGraph→¬BB∈Edg⁡G
16 15 adantl ⊢A∈X∧B∈Y∧A≠B∧G∈USGraph→¬BB∈Edg⁡G
17 16 intnand ⊢A∈X∧B∈Y∧A≠B∧G∈USGraph→¬BA∈Edg⁡G∧BB∈Edg⁡G
18 prex ⊢BA∈V
19 prex ⊢BB∈V
20 18 19 prss ⊢BA∈Edg⁡G∧BB∈Edg⁡G↔BABB⊆Edg⁡G
21 17 20 sylnib ⊢A∈X∧B∈Y∧A≠B∧G∈USGraph→¬BABB⊆Edg⁡G
22 ioran ⊢¬AAAB⊆Edg⁡G∨BABB⊆Edg⁡G↔¬AAAB⊆Edg⁡G∧¬BABB⊆Edg⁡G
23 11 21 22 sylanbrc ⊢A∈X∧B∈Y∧A≠B∧G∈USGraph→¬AAAB⊆Edg⁡G∨BABB⊆Edg⁡G
24 preq1 ⊢x=A→xA=AA
25 preq1 ⊢x=A→xB=AB
26 24 25 preq12d ⊢x=A→xAxB=AAAB
27 26 sseq1d ⊢x=A→xAxB⊆Edg⁡G↔AAAB⊆Edg⁡G
28 preq1 ⊢x=B→xA=BA
29 preq1 ⊢x=B→xB=BB
30 28 29 preq12d ⊢x=B→xAxB=BABB
31 30 sseq1d ⊢x=B→xAxB⊆Edg⁡G↔BABB⊆Edg⁡G
32 27 31 rexprg ⊢A∈X∧B∈Y→∃x∈ABxAxB⊆Edg⁡G↔AAAB⊆Edg⁡G∨BABB⊆Edg⁡G
33 32 3adant3 ⊢A∈X∧B∈Y∧A≠B→∃x∈ABxAxB⊆Edg⁡G↔AAAB⊆Edg⁡G∨BABB⊆Edg⁡G
34 33 adantr ⊢A∈X∧B∈Y∧A≠B∧G∈USGraph→∃x∈ABxAxB⊆Edg⁡G↔AAAB⊆Edg⁡G∨BABB⊆Edg⁡G
35 23 34 mtbird ⊢A∈X∧B∈Y∧A≠B∧G∈USGraph→¬∃x∈ABxAxB⊆Edg⁡G
36 reurex ⊢∃!x∈ABxAxB⊆Edg⁡G→∃x∈ABxAxB⊆Edg⁡G
37 35 36 nsyl ⊢A∈X∧B∈Y∧A≠B∧G∈USGraph→¬∃!x∈ABxAxB⊆Edg⁡G
38 37 orcd ⊢A∈X∧B∈Y∧A≠B∧G∈USGraph→¬∃!x∈ABxAxB⊆Edg⁡G∨¬∃!x∈ABxBxA⊆Edg⁡G
39 rexnal ⊢∃l∈AB∖A¬∃!x∈ABxAxl⊆Edg⁡G↔¬∀l∈AB∖A∃!x∈ABxAxl⊆Edg⁡G
40 39 bicomi ⊢¬∀l∈AB∖A∃!x∈ABxAxl⊆Edg⁡G↔∃l∈AB∖A¬∃!x∈ABxAxl⊆Edg⁡G
41 40 a1i ⊢A∈X∧B∈Y∧A≠B∧G∈USGraph→¬∀l∈AB∖A∃!x∈ABxAxl⊆Edg⁡G↔∃l∈AB∖A¬∃!x∈ABxAxl⊆Edg⁡G
42 difprsn1 ⊢A≠B→AB∖A=B
43 42 3ad2ant3 ⊢A∈X∧B∈Y∧A≠B→AB∖A=B
44 43 adantr ⊢A∈X∧B∈Y∧A≠B∧G∈USGraph→AB∖A=B
45 44 rexeqdv ⊢A∈X∧B∈Y∧A≠B∧G∈USGraph→∃l∈AB∖A¬∃!x∈ABxAxl⊆Edg⁡G↔∃l∈B¬∃!x∈ABxAxl⊆Edg⁡G
46 preq2 ⊢l=B→xl=xB
47 46 preq2d ⊢l=B→xAxl=xAxB
48 47 sseq1d ⊢l=B→xAxl⊆Edg⁡G↔xAxB⊆Edg⁡G
49 48 reubidv ⊢l=B→∃!x∈ABxAxl⊆Edg⁡G↔∃!x∈ABxAxB⊆Edg⁡G
50 49 notbid ⊢l=B→¬∃!x∈ABxAxl⊆Edg⁡G↔¬∃!x∈ABxAxB⊆Edg⁡G
51 50 rexsng ⊢B∈Y→∃l∈B¬∃!x∈ABxAxl⊆Edg⁡G↔¬∃!x∈ABxAxB⊆Edg⁡G
52 51 3ad2ant2 ⊢A∈X∧B∈Y∧A≠B→∃l∈B¬∃!x∈ABxAxl⊆Edg⁡G↔¬∃!x∈ABxAxB⊆Edg⁡G
53 52 adantr ⊢A∈X∧B∈Y∧A≠B∧G∈USGraph→∃l∈B¬∃!x∈ABxAxl⊆Edg⁡G↔¬∃!x∈ABxAxB⊆Edg⁡G
54 41 45 53 3bitrd ⊢A∈X∧B∈Y∧A≠B∧G∈USGraph→¬∀l∈AB∖A∃!x∈ABxAxl⊆Edg⁡G↔¬∃!x∈ABxAxB⊆Edg⁡G
55 rexnal ⊢∃l∈AB∖B¬∃!x∈ABxBxl⊆Edg⁡G↔¬∀l∈AB∖B∃!x∈ABxBxl⊆Edg⁡G
56 55 bicomi ⊢¬∀l∈AB∖B∃!x∈ABxBxl⊆Edg⁡G↔∃l∈AB∖B¬∃!x∈ABxBxl⊆Edg⁡G
57 56 a1i ⊢A∈X∧B∈Y∧A≠B∧G∈USGraph→¬∀l∈AB∖B∃!x∈ABxBxl⊆Edg⁡G↔∃l∈AB∖B¬∃!x∈ABxBxl⊆Edg⁡G
58 difprsn2 ⊢A≠B→AB∖B=A
59 58 3ad2ant3 ⊢A∈X∧B∈Y∧A≠B→AB∖B=A
60 59 adantr ⊢A∈X∧B∈Y∧A≠B∧G∈USGraph→AB∖B=A
61 60 rexeqdv ⊢A∈X∧B∈Y∧A≠B∧G∈USGraph→∃l∈AB∖B¬∃!x∈ABxBxl⊆Edg⁡G↔∃l∈A¬∃!x∈ABxBxl⊆Edg⁡G
62 preq2 ⊢l=A→xl=xA
63 62 preq2d ⊢l=A→xBxl=xBxA
64 63 sseq1d ⊢l=A→xBxl⊆Edg⁡G↔xBxA⊆Edg⁡G
65 64 reubidv ⊢l=A→∃!x∈ABxBxl⊆Edg⁡G↔∃!x∈ABxBxA⊆Edg⁡G
66 65 notbid ⊢l=A→¬∃!x∈ABxBxl⊆Edg⁡G↔¬∃!x∈ABxBxA⊆Edg⁡G
67 66 rexsng ⊢A∈X→∃l∈A¬∃!x∈ABxBxl⊆Edg⁡G↔¬∃!x∈ABxBxA⊆Edg⁡G
68 67 3ad2ant1 ⊢A∈X∧B∈Y∧A≠B→∃l∈A¬∃!x∈ABxBxl⊆Edg⁡G↔¬∃!x∈ABxBxA⊆Edg⁡G
69 68 adantr ⊢A∈X∧B∈Y∧A≠B∧G∈USGraph→∃l∈A¬∃!x∈ABxBxl⊆Edg⁡G↔¬∃!x∈ABxBxA⊆Edg⁡G
70 57 61 69 3bitrd ⊢A∈X∧B∈Y∧A≠B∧G∈USGraph→¬∀l∈AB∖B∃!x∈ABxBxl⊆Edg⁡G↔¬∃!x∈ABxBxA⊆Edg⁡G
71 54 70 orbi12d ⊢A∈X∧B∈Y∧A≠B∧G∈USGraph→¬∀l∈AB∖A∃!x∈ABxAxl⊆Edg⁡G∨¬∀l∈AB∖B∃!x∈ABxBxl⊆Edg⁡G↔¬∃!x∈ABxAxB⊆Edg⁡G∨¬∃!x∈ABxBxA⊆Edg⁡G
72 38 71 mpbird ⊢A∈X∧B∈Y∧A≠B∧G∈USGraph→¬∀l∈AB∖A∃!x∈ABxAxl⊆Edg⁡G∨¬∀l∈AB∖B∃!x∈ABxBxl⊆Edg⁡G
73 sneq ⊢k=A→k=A
74 73 difeq2d ⊢k=A→AB∖k=AB∖A
75 preq2 ⊢k=A→xk=xA
76 75 preq1d ⊢k=A→xkxl=xAxl
77 76 sseq1d ⊢k=A→xkxl⊆Edg⁡G↔xAxl⊆Edg⁡G
78 77 reubidv ⊢k=A→∃!x∈ABxkxl⊆Edg⁡G↔∃!x∈ABxAxl⊆Edg⁡G
79 74 78 raleqbidv ⊢k=A→∀l∈AB∖k∃!x∈ABxkxl⊆Edg⁡G↔∀l∈AB∖A∃!x∈ABxAxl⊆Edg⁡G
80 79 notbid ⊢k=A→¬∀l∈AB∖k∃!x∈ABxkxl⊆Edg⁡G↔¬∀l∈AB∖A∃!x∈ABxAxl⊆Edg⁡G
81 sneq ⊢k=B→k=B
82 81 difeq2d ⊢k=B→AB∖k=AB∖B
83 preq2 ⊢k=B→xk=xB
84 83 preq1d ⊢k=B→xkxl=xBxl
85 84 sseq1d ⊢k=B→xkxl⊆Edg⁡G↔xBxl⊆Edg⁡G
86 85 reubidv ⊢k=B→∃!x∈ABxkxl⊆Edg⁡G↔∃!x∈ABxBxl⊆Edg⁡G
87 82 86 raleqbidv ⊢k=B→∀l∈AB∖k∃!x∈ABxkxl⊆Edg⁡G↔∀l∈AB∖B∃!x∈ABxBxl⊆Edg⁡G
88 87 notbid ⊢k=B→¬∀l∈AB∖k∃!x∈ABxkxl⊆Edg⁡G↔¬∀l∈AB∖B∃!x∈ABxBxl⊆Edg⁡G
89 80 88 rexprg ⊢A∈X∧B∈Y→∃k∈AB¬∀l∈AB∖k∃!x∈ABxkxl⊆Edg⁡G↔¬∀l∈AB∖A∃!x∈ABxAxl⊆Edg⁡G∨¬∀l∈AB∖B∃!x∈ABxBxl⊆Edg⁡G
90 89 3adant3 ⊢A∈X∧B∈Y∧A≠B→∃k∈AB¬∀l∈AB∖k∃!x∈ABxkxl⊆Edg⁡G↔¬∀l∈AB∖A∃!x∈ABxAxl⊆Edg⁡G∨¬∀l∈AB∖B∃!x∈ABxBxl⊆Edg⁡G
91 90 adantr ⊢A∈X∧B∈Y∧A≠B∧G∈USGraph→∃k∈AB¬∀l∈AB∖k∃!x∈ABxkxl⊆Edg⁡G↔¬∀l∈AB∖A∃!x∈ABxAxl⊆Edg⁡G∨¬∀l∈AB∖B∃!x∈ABxBxl⊆Edg⁡G
92 72 91 mpbird ⊢A∈X∧B∈Y∧A≠B∧G∈USGraph→∃k∈AB¬∀l∈AB∖k∃!x∈ABxkxl⊆Edg⁡G
93 rexnal ⊢∃k∈AB¬∀l∈AB∖k∃!x∈ABxkxl⊆Edg⁡G↔¬∀k∈AB∀l∈AB∖k∃!x∈ABxkxl⊆Edg⁡G
94 92 93 sylib ⊢A∈X∧B∈Y∧A≠B∧G∈USGraph→¬∀k∈AB∀l∈AB∖k∃!x∈ABxkxl⊆Edg⁡G
95 94 intnand ⊢A∈X∧B∈Y∧A≠B∧G∈USGraph→¬G∈USGraph∧∀k∈AB∀l∈AB∖k∃!x∈ABxkxl⊆Edg⁡G
96 95 adantlr ⊢A∈X∧B∈Y∧A≠B∧Vtx⁡G=AB∧G∈USGraph→¬G∈USGraph∧∀k∈AB∀l∈AB∖k∃!x∈ABxkxl⊆Edg⁡G
97 id ⊢Vtx⁡G=AB→Vtx⁡G=AB
98 difeq1 ⊢Vtx⁡G=AB→Vtx⁡G∖k=AB∖k
99 reueq1 ⊢Vtx⁡G=AB→∃!x∈Vtx⁡Gxkxl⊆Edg⁡G↔∃!x∈ABxkxl⊆Edg⁡G
100 98 99 raleqbidv ⊢Vtx⁡G=AB→∀l∈Vtx⁡G∖k∃!x∈Vtx⁡Gxkxl⊆Edg⁡G↔∀l∈AB∖k∃!x∈ABxkxl⊆Edg⁡G
101 97 100 raleqbidv ⊢Vtx⁡G=AB→∀k∈Vtx⁡G∀l∈Vtx⁡G∖k∃!x∈Vtx⁡Gxkxl⊆Edg⁡G↔∀k∈AB∀l∈AB∖k∃!x∈ABxkxl⊆Edg⁡G
102 101 anbi2d ⊢Vtx⁡G=AB→G∈USGraph∧∀k∈Vtx⁡G∀l∈Vtx⁡G∖k∃!x∈Vtx⁡Gxkxl⊆Edg⁡G↔G∈USGraph∧∀k∈AB∀l∈AB∖k∃!x∈ABxkxl⊆Edg⁡G
103 102 notbid ⊢Vtx⁡G=AB→¬G∈USGraph∧∀k∈Vtx⁡G∀l∈Vtx⁡G∖k∃!x∈Vtx⁡Gxkxl⊆Edg⁡G↔¬G∈USGraph∧∀k∈AB∀l∈AB∖k∃!x∈ABxkxl⊆Edg⁡G
104 103 adantl ⊢A∈X∧B∈Y∧A≠B∧Vtx⁡G=AB→¬G∈USGraph∧∀k∈Vtx⁡G∀l∈Vtx⁡G∖k∃!x∈Vtx⁡Gxkxl⊆Edg⁡G↔¬G∈USGraph∧∀k∈AB∀l∈AB∖k∃!x∈ABxkxl⊆Edg⁡G
105 104 adantr ⊢A∈X∧B∈Y∧A≠B∧Vtx⁡G=AB∧G∈USGraph→¬G∈USGraph∧∀k∈Vtx⁡G∀l∈Vtx⁡G∖k∃!x∈Vtx⁡Gxkxl⊆Edg⁡G↔¬G∈USGraph∧∀k∈AB∀l∈AB∖k∃!x∈ABxkxl⊆Edg⁡G
106 96 105 mpbird ⊢A∈X∧B∈Y∧A≠B∧Vtx⁡G=AB∧G∈USGraph→¬G∈USGraph∧∀k∈Vtx⁡G∀l∈Vtx⁡G∖k∃!x∈Vtx⁡Gxkxl⊆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⁡Gxkxl⊆Edg⁡G
110 107 109 xchbinx ⊢G∉FriendGraph↔¬G∈USGraph∧∀k∈Vtx⁡G∀l∈Vtx⁡G∖k∃!x∈Vtx⁡Gxkxl⊆Edg⁡G
111 106 110 sylibr ⊢A∈X∧B∈Y∧A≠B∧Vtx⁡G=AB∧G∈USGraph→G∉FriendGraph
112 111 expcom ⊢G∈USGraph→A∈X∧B∈Y∧A≠B∧Vtx⁡G=AB→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=AB→G∉FriendGraph
117 112 116 pm2.61i ⊢A∈X∧B∈Y∧A≠B∧Vtx⁡G=AB→G∉FriendGraph