# Metamath Proof Explorer

## Theorem 1to3vfriswmgr

Description: Every friendship graph with one, two or three vertices is a windmill graph. (Contributed by Alexander van der Vekens, 6-Oct-2017) (Revised by AV, 31-Mar-2021)

Ref Expression
Hypotheses 3vfriswmgr.v ${⊢}{V}=\mathrm{Vtx}\left({G}\right)$
3vfriswmgr.e ${⊢}{E}=\mathrm{Edg}\left({G}\right)$
Assertion 1to3vfriswmgr ${⊢}\left({A}\in {X}\wedge \left({V}=\left\{{A}\right\}\vee {V}=\left\{{A},{B}\right\}\vee {V}=\left\{{A},{B},{C}\right\}\right)\right)\to \left({G}\in \mathrm{FriendGraph}\to \exists {h}\in {V}\phantom{\rule{.4em}{0ex}}\forall {v}\in \left({V}\setminus \left\{{h}\right\}\right)\phantom{\rule{.4em}{0ex}}\left(\left\{{v},{h}\right\}\in {E}\wedge \exists !{w}\in \left({V}\setminus \left\{{h}\right\}\right)\phantom{\rule{.4em}{0ex}}\left\{{v},{w}\right\}\in {E}\right)\right)$

### Proof

Step Hyp Ref Expression
1 3vfriswmgr.v ${⊢}{V}=\mathrm{Vtx}\left({G}\right)$
2 3vfriswmgr.e ${⊢}{E}=\mathrm{Edg}\left({G}\right)$
3 df-3or ${⊢}\left({V}=\left\{{A}\right\}\vee {V}=\left\{{A},{B}\right\}\vee {V}=\left\{{A},{B},{C}\right\}\right)↔\left(\left({V}=\left\{{A}\right\}\vee {V}=\left\{{A},{B}\right\}\right)\vee {V}=\left\{{A},{B},{C}\right\}\right)$
4 1 2 1to2vfriswmgr ${⊢}\left({A}\in {X}\wedge \left({V}=\left\{{A}\right\}\vee {V}=\left\{{A},{B}\right\}\right)\right)\to \left({G}\in \mathrm{FriendGraph}\to \exists {h}\in {V}\phantom{\rule{.4em}{0ex}}\forall {v}\in \left({V}\setminus \left\{{h}\right\}\right)\phantom{\rule{.4em}{0ex}}\left(\left\{{v},{h}\right\}\in {E}\wedge \exists !{w}\in \left({V}\setminus \left\{{h}\right\}\right)\phantom{\rule{.4em}{0ex}}\left\{{v},{w}\right\}\in {E}\right)\right)$
5 4 expcom ${⊢}\left({V}=\left\{{A}\right\}\vee {V}=\left\{{A},{B}\right\}\right)\to \left({A}\in {X}\to \left({G}\in \mathrm{FriendGraph}\to \exists {h}\in {V}\phantom{\rule{.4em}{0ex}}\forall {v}\in \left({V}\setminus \left\{{h}\right\}\right)\phantom{\rule{.4em}{0ex}}\left(\left\{{v},{h}\right\}\in {E}\wedge \exists !{w}\in \left({V}\setminus \left\{{h}\right\}\right)\phantom{\rule{.4em}{0ex}}\left\{{v},{w}\right\}\in {E}\right)\right)\right)$
6 tppreq3 ${⊢}{B}={C}\to \left\{{A},{B},{C}\right\}=\left\{{A},{B}\right\}$
7 6 eqeq2d ${⊢}{B}={C}\to \left({V}=\left\{{A},{B},{C}\right\}↔{V}=\left\{{A},{B}\right\}\right)$
8 olc ${⊢}{V}=\left\{{A},{B}\right\}\to \left({V}=\left\{{A}\right\}\vee {V}=\left\{{A},{B}\right\}\right)$
9 8 anim1ci ${⊢}\left({V}=\left\{{A},{B}\right\}\wedge {A}\in {X}\right)\to \left({A}\in {X}\wedge \left({V}=\left\{{A}\right\}\vee {V}=\left\{{A},{B}\right\}\right)\right)$
10 9 4 syl ${⊢}\left({V}=\left\{{A},{B}\right\}\wedge {A}\in {X}\right)\to \left({G}\in \mathrm{FriendGraph}\to \exists {h}\in {V}\phantom{\rule{.4em}{0ex}}\forall {v}\in \left({V}\setminus \left\{{h}\right\}\right)\phantom{\rule{.4em}{0ex}}\left(\left\{{v},{h}\right\}\in {E}\wedge \exists !{w}\in \left({V}\setminus \left\{{h}\right\}\right)\phantom{\rule{.4em}{0ex}}\left\{{v},{w}\right\}\in {E}\right)\right)$
11 10 ex ${⊢}{V}=\left\{{A},{B}\right\}\to \left({A}\in {X}\to \left({G}\in \mathrm{FriendGraph}\to \exists {h}\in {V}\phantom{\rule{.4em}{0ex}}\forall {v}\in \left({V}\setminus \left\{{h}\right\}\right)\phantom{\rule{.4em}{0ex}}\left(\left\{{v},{h}\right\}\in {E}\wedge \exists !{w}\in \left({V}\setminus \left\{{h}\right\}\right)\phantom{\rule{.4em}{0ex}}\left\{{v},{w}\right\}\in {E}\right)\right)\right)$
12 7 11 syl6bi ${⊢}{B}={C}\to \left({V}=\left\{{A},{B},{C}\right\}\to \left({A}\in {X}\to \left({G}\in \mathrm{FriendGraph}\to \exists {h}\in {V}\phantom{\rule{.4em}{0ex}}\forall {v}\in \left({V}\setminus \left\{{h}\right\}\right)\phantom{\rule{.4em}{0ex}}\left(\left\{{v},{h}\right\}\in {E}\wedge \exists !{w}\in \left({V}\setminus \left\{{h}\right\}\right)\phantom{\rule{.4em}{0ex}}\left\{{v},{w}\right\}\in {E}\right)\right)\right)\right)$
13 tpprceq3 ${⊢}¬\left({B}\in \mathrm{V}\wedge {B}\ne {A}\right)\to \left\{{C},{A},{B}\right\}=\left\{{C},{A}\right\}$
14 tprot ${⊢}\left\{{C},{A},{B}\right\}=\left\{{A},{B},{C}\right\}$
15 14 eqeq1i ${⊢}\left\{{C},{A},{B}\right\}=\left\{{C},{A}\right\}↔\left\{{A},{B},{C}\right\}=\left\{{C},{A}\right\}$
16 15 biimpi ${⊢}\left\{{C},{A},{B}\right\}=\left\{{C},{A}\right\}\to \left\{{A},{B},{C}\right\}=\left\{{C},{A}\right\}$
17 prcom ${⊢}\left\{{C},{A}\right\}=\left\{{A},{C}\right\}$
18 16 17 syl6eq ${⊢}\left\{{C},{A},{B}\right\}=\left\{{C},{A}\right\}\to \left\{{A},{B},{C}\right\}=\left\{{A},{C}\right\}$
19 18 eqeq2d ${⊢}\left\{{C},{A},{B}\right\}=\left\{{C},{A}\right\}\to \left({V}=\left\{{A},{B},{C}\right\}↔{V}=\left\{{A},{C}\right\}\right)$
20 olc ${⊢}{V}=\left\{{A},{C}\right\}\to \left({V}=\left\{{A}\right\}\vee {V}=\left\{{A},{C}\right\}\right)$
21 1 2 1to2vfriswmgr ${⊢}\left({A}\in {X}\wedge \left({V}=\left\{{A}\right\}\vee {V}=\left\{{A},{C}\right\}\right)\right)\to \left({G}\in \mathrm{FriendGraph}\to \exists {h}\in {V}\phantom{\rule{.4em}{0ex}}\forall {v}\in \left({V}\setminus \left\{{h}\right\}\right)\phantom{\rule{.4em}{0ex}}\left(\left\{{v},{h}\right\}\in {E}\wedge \exists !{w}\in \left({V}\setminus \left\{{h}\right\}\right)\phantom{\rule{.4em}{0ex}}\left\{{v},{w}\right\}\in {E}\right)\right)$
22 20 21 sylan2 ${⊢}\left({A}\in {X}\wedge {V}=\left\{{A},{C}\right\}\right)\to \left({G}\in \mathrm{FriendGraph}\to \exists {h}\in {V}\phantom{\rule{.4em}{0ex}}\forall {v}\in \left({V}\setminus \left\{{h}\right\}\right)\phantom{\rule{.4em}{0ex}}\left(\left\{{v},{h}\right\}\in {E}\wedge \exists !{w}\in \left({V}\setminus \left\{{h}\right\}\right)\phantom{\rule{.4em}{0ex}}\left\{{v},{w}\right\}\in {E}\right)\right)$
23 22 expcom ${⊢}{V}=\left\{{A},{C}\right\}\to \left({A}\in {X}\to \left({G}\in \mathrm{FriendGraph}\to \exists {h}\in {V}\phantom{\rule{.4em}{0ex}}\forall {v}\in \left({V}\setminus \left\{{h}\right\}\right)\phantom{\rule{.4em}{0ex}}\left(\left\{{v},{h}\right\}\in {E}\wedge \exists !{w}\in \left({V}\setminus \left\{{h}\right\}\right)\phantom{\rule{.4em}{0ex}}\left\{{v},{w}\right\}\in {E}\right)\right)\right)$
24 19 23 syl6bi ${⊢}\left\{{C},{A},{B}\right\}=\left\{{C},{A}\right\}\to \left({V}=\left\{{A},{B},{C}\right\}\to \left({A}\in {X}\to \left({G}\in \mathrm{FriendGraph}\to \exists {h}\in {V}\phantom{\rule{.4em}{0ex}}\forall {v}\in \left({V}\setminus \left\{{h}\right\}\right)\phantom{\rule{.4em}{0ex}}\left(\left\{{v},{h}\right\}\in {E}\wedge \exists !{w}\in \left({V}\setminus \left\{{h}\right\}\right)\phantom{\rule{.4em}{0ex}}\left\{{v},{w}\right\}\in {E}\right)\right)\right)\right)$
25 13 24 syl ${⊢}¬\left({B}\in \mathrm{V}\wedge {B}\ne {A}\right)\to \left({V}=\left\{{A},{B},{C}\right\}\to \left({A}\in {X}\to \left({G}\in \mathrm{FriendGraph}\to \exists {h}\in {V}\phantom{\rule{.4em}{0ex}}\forall {v}\in \left({V}\setminus \left\{{h}\right\}\right)\phantom{\rule{.4em}{0ex}}\left(\left\{{v},{h}\right\}\in {E}\wedge \exists !{w}\in \left({V}\setminus \left\{{h}\right\}\right)\phantom{\rule{.4em}{0ex}}\left\{{v},{w}\right\}\in {E}\right)\right)\right)\right)$
26 25 a1d ${⊢}¬\left({B}\in \mathrm{V}\wedge {B}\ne {A}\right)\to \left({B}\ne {C}\to \left({V}=\left\{{A},{B},{C}\right\}\to \left({A}\in {X}\to \left({G}\in \mathrm{FriendGraph}\to \exists {h}\in {V}\phantom{\rule{.4em}{0ex}}\forall {v}\in \left({V}\setminus \left\{{h}\right\}\right)\phantom{\rule{.4em}{0ex}}\left(\left\{{v},{h}\right\}\in {E}\wedge \exists !{w}\in \left({V}\setminus \left\{{h}\right\}\right)\phantom{\rule{.4em}{0ex}}\left\{{v},{w}\right\}\in {E}\right)\right)\right)\right)\right)$
27 tpprceq3 ${⊢}¬\left({C}\in \mathrm{V}\wedge {C}\ne {A}\right)\to \left\{{B},{A},{C}\right\}=\left\{{B},{A}\right\}$
28 tpcoma ${⊢}\left\{{B},{A},{C}\right\}=\left\{{A},{B},{C}\right\}$
29 28 eqeq1i ${⊢}\left\{{B},{A},{C}\right\}=\left\{{B},{A}\right\}↔\left\{{A},{B},{C}\right\}=\left\{{B},{A}\right\}$
30 29 biimpi ${⊢}\left\{{B},{A},{C}\right\}=\left\{{B},{A}\right\}\to \left\{{A},{B},{C}\right\}=\left\{{B},{A}\right\}$
31 prcom ${⊢}\left\{{B},{A}\right\}=\left\{{A},{B}\right\}$
32 30 31 syl6eq ${⊢}\left\{{B},{A},{C}\right\}=\left\{{B},{A}\right\}\to \left\{{A},{B},{C}\right\}=\left\{{A},{B}\right\}$
33 32 eqeq2d ${⊢}\left\{{B},{A},{C}\right\}=\left\{{B},{A}\right\}\to \left({V}=\left\{{A},{B},{C}\right\}↔{V}=\left\{{A},{B}\right\}\right)$
34 8 4 sylan2 ${⊢}\left({A}\in {X}\wedge {V}=\left\{{A},{B}\right\}\right)\to \left({G}\in \mathrm{FriendGraph}\to \exists {h}\in {V}\phantom{\rule{.4em}{0ex}}\forall {v}\in \left({V}\setminus \left\{{h}\right\}\right)\phantom{\rule{.4em}{0ex}}\left(\left\{{v},{h}\right\}\in {E}\wedge \exists !{w}\in \left({V}\setminus \left\{{h}\right\}\right)\phantom{\rule{.4em}{0ex}}\left\{{v},{w}\right\}\in {E}\right)\right)$
35 34 expcom ${⊢}{V}=\left\{{A},{B}\right\}\to \left({A}\in {X}\to \left({G}\in \mathrm{FriendGraph}\to \exists {h}\in {V}\phantom{\rule{.4em}{0ex}}\forall {v}\in \left({V}\setminus \left\{{h}\right\}\right)\phantom{\rule{.4em}{0ex}}\left(\left\{{v},{h}\right\}\in {E}\wedge \exists !{w}\in \left({V}\setminus \left\{{h}\right\}\right)\phantom{\rule{.4em}{0ex}}\left\{{v},{w}\right\}\in {E}\right)\right)\right)$
36 35 a1d ${⊢}{V}=\left\{{A},{B}\right\}\to \left({B}\ne {C}\to \left({A}\in {X}\to \left({G}\in \mathrm{FriendGraph}\to \exists {h}\in {V}\phantom{\rule{.4em}{0ex}}\forall {v}\in \left({V}\setminus \left\{{h}\right\}\right)\phantom{\rule{.4em}{0ex}}\left(\left\{{v},{h}\right\}\in {E}\wedge \exists !{w}\in \left({V}\setminus \left\{{h}\right\}\right)\phantom{\rule{.4em}{0ex}}\left\{{v},{w}\right\}\in {E}\right)\right)\right)\right)$
37 33 36 syl6bi ${⊢}\left\{{B},{A},{C}\right\}=\left\{{B},{A}\right\}\to \left({V}=\left\{{A},{B},{C}\right\}\to \left({B}\ne {C}\to \left({A}\in {X}\to \left({G}\in \mathrm{FriendGraph}\to \exists {h}\in {V}\phantom{\rule{.4em}{0ex}}\forall {v}\in \left({V}\setminus \left\{{h}\right\}\right)\phantom{\rule{.4em}{0ex}}\left(\left\{{v},{h}\right\}\in {E}\wedge \exists !{w}\in \left({V}\setminus \left\{{h}\right\}\right)\phantom{\rule{.4em}{0ex}}\left\{{v},{w}\right\}\in {E}\right)\right)\right)\right)\right)$
38 27 37 syl ${⊢}¬\left({C}\in \mathrm{V}\wedge {C}\ne {A}\right)\to \left({V}=\left\{{A},{B},{C}\right\}\to \left({B}\ne {C}\to \left({A}\in {X}\to \left({G}\in \mathrm{FriendGraph}\to \exists {h}\in {V}\phantom{\rule{.4em}{0ex}}\forall {v}\in \left({V}\setminus \left\{{h}\right\}\right)\phantom{\rule{.4em}{0ex}}\left(\left\{{v},{h}\right\}\in {E}\wedge \exists !{w}\in \left({V}\setminus \left\{{h}\right\}\right)\phantom{\rule{.4em}{0ex}}\left\{{v},{w}\right\}\in {E}\right)\right)\right)\right)\right)$
39 38 com23 ${⊢}¬\left({C}\in \mathrm{V}\wedge {C}\ne {A}\right)\to \left({B}\ne {C}\to \left({V}=\left\{{A},{B},{C}\right\}\to \left({A}\in {X}\to \left({G}\in \mathrm{FriendGraph}\to \exists {h}\in {V}\phantom{\rule{.4em}{0ex}}\forall {v}\in \left({V}\setminus \left\{{h}\right\}\right)\phantom{\rule{.4em}{0ex}}\left(\left\{{v},{h}\right\}\in {E}\wedge \exists !{w}\in \left({V}\setminus \left\{{h}\right\}\right)\phantom{\rule{.4em}{0ex}}\left\{{v},{w}\right\}\in {E}\right)\right)\right)\right)\right)$
40 simpl ${⊢}\left({B}\in \mathrm{V}\wedge {B}\ne {A}\right)\to {B}\in \mathrm{V}$
41 simpl ${⊢}\left({C}\in \mathrm{V}\wedge {C}\ne {A}\right)\to {C}\in \mathrm{V}$
42 40 41 anim12i ${⊢}\left(\left({B}\in \mathrm{V}\wedge {B}\ne {A}\right)\wedge \left({C}\in \mathrm{V}\wedge {C}\ne {A}\right)\right)\to \left({B}\in \mathrm{V}\wedge {C}\in \mathrm{V}\right)$
43 42 ad2antrr ${⊢}\left(\left(\left(\left({B}\in \mathrm{V}\wedge {B}\ne {A}\right)\wedge \left({C}\in \mathrm{V}\wedge {C}\ne {A}\right)\right)\wedge {B}\ne {C}\right)\wedge {V}=\left\{{A},{B},{C}\right\}\right)\to \left({B}\in \mathrm{V}\wedge {C}\in \mathrm{V}\right)$
44 43 anim1ci ${⊢}\left(\left(\left(\left(\left({B}\in \mathrm{V}\wedge {B}\ne {A}\right)\wedge \left({C}\in \mathrm{V}\wedge {C}\ne {A}\right)\right)\wedge {B}\ne {C}\right)\wedge {V}=\left\{{A},{B},{C}\right\}\right)\wedge {A}\in {X}\right)\to \left({A}\in {X}\wedge \left({B}\in \mathrm{V}\wedge {C}\in \mathrm{V}\right)\right)$
45 3anass ${⊢}\left({A}\in {X}\wedge {B}\in \mathrm{V}\wedge {C}\in \mathrm{V}\right)↔\left({A}\in {X}\wedge \left({B}\in \mathrm{V}\wedge {C}\in \mathrm{V}\right)\right)$
46 44 45 sylibr ${⊢}\left(\left(\left(\left(\left({B}\in \mathrm{V}\wedge {B}\ne {A}\right)\wedge \left({C}\in \mathrm{V}\wedge {C}\ne {A}\right)\right)\wedge {B}\ne {C}\right)\wedge {V}=\left\{{A},{B},{C}\right\}\right)\wedge {A}\in {X}\right)\to \left({A}\in {X}\wedge {B}\in \mathrm{V}\wedge {C}\in \mathrm{V}\right)$
47 simpr ${⊢}\left({B}\in \mathrm{V}\wedge {B}\ne {A}\right)\to {B}\ne {A}$
48 47 necomd ${⊢}\left({B}\in \mathrm{V}\wedge {B}\ne {A}\right)\to {A}\ne {B}$
49 simpr ${⊢}\left({C}\in \mathrm{V}\wedge {C}\ne {A}\right)\to {C}\ne {A}$
50 49 necomd ${⊢}\left({C}\in \mathrm{V}\wedge {C}\ne {A}\right)\to {A}\ne {C}$
51 48 50 anim12i ${⊢}\left(\left({B}\in \mathrm{V}\wedge {B}\ne {A}\right)\wedge \left({C}\in \mathrm{V}\wedge {C}\ne {A}\right)\right)\to \left({A}\ne {B}\wedge {A}\ne {C}\right)$
52 51 anim1i ${⊢}\left(\left(\left({B}\in \mathrm{V}\wedge {B}\ne {A}\right)\wedge \left({C}\in \mathrm{V}\wedge {C}\ne {A}\right)\right)\wedge {B}\ne {C}\right)\to \left(\left({A}\ne {B}\wedge {A}\ne {C}\right)\wedge {B}\ne {C}\right)$
53 df-3an ${⊢}\left({A}\ne {B}\wedge {A}\ne {C}\wedge {B}\ne {C}\right)↔\left(\left({A}\ne {B}\wedge {A}\ne {C}\right)\wedge {B}\ne {C}\right)$
54 52 53 sylibr ${⊢}\left(\left(\left({B}\in \mathrm{V}\wedge {B}\ne {A}\right)\wedge \left({C}\in \mathrm{V}\wedge {C}\ne {A}\right)\right)\wedge {B}\ne {C}\right)\to \left({A}\ne {B}\wedge {A}\ne {C}\wedge {B}\ne {C}\right)$
55 54 ad2antrr ${⊢}\left(\left(\left(\left(\left({B}\in \mathrm{V}\wedge {B}\ne {A}\right)\wedge \left({C}\in \mathrm{V}\wedge {C}\ne {A}\right)\right)\wedge {B}\ne {C}\right)\wedge {V}=\left\{{A},{B},{C}\right\}\right)\wedge {A}\in {X}\right)\to \left({A}\ne {B}\wedge {A}\ne {C}\wedge {B}\ne {C}\right)$
56 simplr ${⊢}\left(\left(\left(\left(\left({B}\in \mathrm{V}\wedge {B}\ne {A}\right)\wedge \left({C}\in \mathrm{V}\wedge {C}\ne {A}\right)\right)\wedge {B}\ne {C}\right)\wedge {V}=\left\{{A},{B},{C}\right\}\right)\wedge {A}\in {X}\right)\to {V}=\left\{{A},{B},{C}\right\}$
57 1 2 3vfriswmgr ${⊢}\left(\left({A}\in {X}\wedge {B}\in \mathrm{V}\wedge {C}\in \mathrm{V}\right)\wedge \left({A}\ne {B}\wedge {A}\ne {C}\wedge {B}\ne {C}\right)\wedge {V}=\left\{{A},{B},{C}\right\}\right)\to \left({G}\in \mathrm{FriendGraph}\to \exists {h}\in {V}\phantom{\rule{.4em}{0ex}}\forall {v}\in \left({V}\setminus \left\{{h}\right\}\right)\phantom{\rule{.4em}{0ex}}\left(\left\{{v},{h}\right\}\in {E}\wedge \exists !{w}\in \left({V}\setminus \left\{{h}\right\}\right)\phantom{\rule{.4em}{0ex}}\left\{{v},{w}\right\}\in {E}\right)\right)$
58 46 55 56 57 syl3anc ${⊢}\left(\left(\left(\left(\left({B}\in \mathrm{V}\wedge {B}\ne {A}\right)\wedge \left({C}\in \mathrm{V}\wedge {C}\ne {A}\right)\right)\wedge {B}\ne {C}\right)\wedge {V}=\left\{{A},{B},{C}\right\}\right)\wedge {A}\in {X}\right)\to \left({G}\in \mathrm{FriendGraph}\to \exists {h}\in {V}\phantom{\rule{.4em}{0ex}}\forall {v}\in \left({V}\setminus \left\{{h}\right\}\right)\phantom{\rule{.4em}{0ex}}\left(\left\{{v},{h}\right\}\in {E}\wedge \exists !{w}\in \left({V}\setminus \left\{{h}\right\}\right)\phantom{\rule{.4em}{0ex}}\left\{{v},{w}\right\}\in {E}\right)\right)$
59 58 exp41 ${⊢}\left(\left({B}\in \mathrm{V}\wedge {B}\ne {A}\right)\wedge \left({C}\in \mathrm{V}\wedge {C}\ne {A}\right)\right)\to \left({B}\ne {C}\to \left({V}=\left\{{A},{B},{C}\right\}\to \left({A}\in {X}\to \left({G}\in \mathrm{FriendGraph}\to \exists {h}\in {V}\phantom{\rule{.4em}{0ex}}\forall {v}\in \left({V}\setminus \left\{{h}\right\}\right)\phantom{\rule{.4em}{0ex}}\left(\left\{{v},{h}\right\}\in {E}\wedge \exists !{w}\in \left({V}\setminus \left\{{h}\right\}\right)\phantom{\rule{.4em}{0ex}}\left\{{v},{w}\right\}\in {E}\right)\right)\right)\right)\right)$
60 26 39 59 ecase ${⊢}{B}\ne {C}\to \left({V}=\left\{{A},{B},{C}\right\}\to \left({A}\in {X}\to \left({G}\in \mathrm{FriendGraph}\to \exists {h}\in {V}\phantom{\rule{.4em}{0ex}}\forall {v}\in \left({V}\setminus \left\{{h}\right\}\right)\phantom{\rule{.4em}{0ex}}\left(\left\{{v},{h}\right\}\in {E}\wedge \exists !{w}\in \left({V}\setminus \left\{{h}\right\}\right)\phantom{\rule{.4em}{0ex}}\left\{{v},{w}\right\}\in {E}\right)\right)\right)\right)$
61 12 60 pm2.61ine ${⊢}{V}=\left\{{A},{B},{C}\right\}\to \left({A}\in {X}\to \left({G}\in \mathrm{FriendGraph}\to \exists {h}\in {V}\phantom{\rule{.4em}{0ex}}\forall {v}\in \left({V}\setminus \left\{{h}\right\}\right)\phantom{\rule{.4em}{0ex}}\left(\left\{{v},{h}\right\}\in {E}\wedge \exists !{w}\in \left({V}\setminus \left\{{h}\right\}\right)\phantom{\rule{.4em}{0ex}}\left\{{v},{w}\right\}\in {E}\right)\right)\right)$
62 5 61 jaoi ${⊢}\left(\left({V}=\left\{{A}\right\}\vee {V}=\left\{{A},{B}\right\}\right)\vee {V}=\left\{{A},{B},{C}\right\}\right)\to \left({A}\in {X}\to \left({G}\in \mathrm{FriendGraph}\to \exists {h}\in {V}\phantom{\rule{.4em}{0ex}}\forall {v}\in \left({V}\setminus \left\{{h}\right\}\right)\phantom{\rule{.4em}{0ex}}\left(\left\{{v},{h}\right\}\in {E}\wedge \exists !{w}\in \left({V}\setminus \left\{{h}\right\}\right)\phantom{\rule{.4em}{0ex}}\left\{{v},{w}\right\}\in {E}\right)\right)\right)$
63 3 62 sylbi ${⊢}\left({V}=\left\{{A}\right\}\vee {V}=\left\{{A},{B}\right\}\vee {V}=\left\{{A},{B},{C}\right\}\right)\to \left({A}\in {X}\to \left({G}\in \mathrm{FriendGraph}\to \exists {h}\in {V}\phantom{\rule{.4em}{0ex}}\forall {v}\in \left({V}\setminus \left\{{h}\right\}\right)\phantom{\rule{.4em}{0ex}}\left(\left\{{v},{h}\right\}\in {E}\wedge \exists !{w}\in \left({V}\setminus \left\{{h}\right\}\right)\phantom{\rule{.4em}{0ex}}\left\{{v},{w}\right\}\in {E}\right)\right)\right)$
64 63 impcom ${⊢}\left({A}\in {X}\wedge \left({V}=\left\{{A}\right\}\vee {V}=\left\{{A},{B}\right\}\vee {V}=\left\{{A},{B},{C}\right\}\right)\right)\to \left({G}\in \mathrm{FriendGraph}\to \exists {h}\in {V}\phantom{\rule{.4em}{0ex}}\forall {v}\in \left({V}\setminus \left\{{h}\right\}\right)\phantom{\rule{.4em}{0ex}}\left(\left\{{v},{h}\right\}\in {E}\wedge \exists !{w}\in \left({V}\setminus \left\{{h}\right\}\right)\phantom{\rule{.4em}{0ex}}\left\{{v},{w}\right\}\in {E}\right)\right)$