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 ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
3vfriswmgr.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion 1to3vfriswmgr ( ( 𝐴 ∈ 𝑋 ∧ ( 𝑉 = { 𝐴 } ∨ 𝑉 = { 𝐴 , 𝐵 } ∨ 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ) ) → ( 𝐺 ∈ FriendGraph → ∃ ℎ ∈ 𝑉 ∀ 𝑣 ∈ ( 𝑉 ∖ { ℎ } ) ( { 𝑣 , ℎ } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( 𝑉 ∖ { ℎ } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) )

Proof

Step Hyp Ref Expression
1 3vfriswmgr.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 3vfriswmgr.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
3 df-3or ⊢ ( ( 𝑉 = { 𝐴 } ∨ 𝑉 = { 𝐴 , 𝐵 } ∨ 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ) ↔ ( ( 𝑉 = { 𝐴 } ∨ 𝑉 = { 𝐴 , 𝐵 } ) ∨ 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ) )
4 1 2 1to2vfriswmgr ⊢ ( ( 𝐴 ∈ 𝑋 ∧ ( 𝑉 = { 𝐴 } ∨ 𝑉 = { 𝐴 , 𝐵 } ) ) → ( 𝐺 ∈ FriendGraph → ∃ ℎ ∈ 𝑉 ∀ 𝑣 ∈ ( 𝑉 ∖ { ℎ } ) ( { 𝑣 , ℎ } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( 𝑉 ∖ { ℎ } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) )
5 4 expcom ⊢ ( ( 𝑉 = { 𝐴 } ∨ 𝑉 = { 𝐴 , 𝐵 } ) → ( 𝐴 ∈ 𝑋 → ( 𝐺 ∈ FriendGraph → ∃ ℎ ∈ 𝑉 ∀ 𝑣 ∈ ( 𝑉 ∖ { ℎ } ) ( { 𝑣 , ℎ } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( 𝑉 ∖ { ℎ } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) ) )
6 tppreq3 ⊢ ( 𝐵 = 𝐶 → { 𝐴 , 𝐵 , 𝐶 } = { 𝐴 , 𝐵 } )
7 6 eqeq2d ⊢ ( 𝐵 = 𝐶 → ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ↔ 𝑉 = { 𝐴 , 𝐵 } ) )
8 olc ⊢ ( 𝑉 = { 𝐴 , 𝐵 } → ( 𝑉 = { 𝐴 } ∨ 𝑉 = { 𝐴 , 𝐵 } ) )
9 8 anim1ci ⊢ ( ( 𝑉 = { 𝐴 , 𝐵 } ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 ∈ 𝑋 ∧ ( 𝑉 = { 𝐴 } ∨ 𝑉 = { 𝐴 , 𝐵 } ) ) )
10 9 4 syl ⊢ ( ( 𝑉 = { 𝐴 , 𝐵 } ∧ 𝐴 ∈ 𝑋 ) → ( 𝐺 ∈ FriendGraph → ∃ ℎ ∈ 𝑉 ∀ 𝑣 ∈ ( 𝑉 ∖ { ℎ } ) ( { 𝑣 , ℎ } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( 𝑉 ∖ { ℎ } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) )
11 10 ex ⊢ ( 𝑉 = { 𝐴 , 𝐵 } → ( 𝐴 ∈ 𝑋 → ( 𝐺 ∈ FriendGraph → ∃ ℎ ∈ 𝑉 ∀ 𝑣 ∈ ( 𝑉 ∖ { ℎ } ) ( { 𝑣 , ℎ } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( 𝑉 ∖ { ℎ } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) ) )
12 7 11 biimtrdi ⊢ ( 𝐵 = 𝐶 → ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } → ( 𝐴 ∈ 𝑋 → ( 𝐺 ∈ FriendGraph → ∃ ℎ ∈ 𝑉 ∀ 𝑣 ∈ ( 𝑉 ∖ { ℎ } ) ( { 𝑣 , ℎ } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( 𝑉 ∖ { ℎ } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) ) ) )
13 tpprceq3 ⊢ ( ¬ ( 𝐵 ∈ V ∧ 𝐵 ≠ 𝐴 ) → { 𝐶 , 𝐴 , 𝐵 } = { 𝐶 , 𝐴 } )
14 tprot ⊢ { 𝐶 , 𝐴 , 𝐵 } = { 𝐴 , 𝐵 , 𝐶 }
15 14 eqeq1i ⊢ ( { 𝐶 , 𝐴 , 𝐵 } = { 𝐶 , 𝐴 } ↔ { 𝐴 , 𝐵 , 𝐶 } = { 𝐶 , 𝐴 } )
16 15 biimpi ⊢ ( { 𝐶 , 𝐴 , 𝐵 } = { 𝐶 , 𝐴 } → { 𝐴 , 𝐵 , 𝐶 } = { 𝐶 , 𝐴 } )
17 prcom ⊢ { 𝐶 , 𝐴 } = { 𝐴 , 𝐶 }
18 16 17 eqtrdi ⊢ ( { 𝐶 , 𝐴 , 𝐵 } = { 𝐶 , 𝐴 } → { 𝐴 , 𝐵 , 𝐶 } = { 𝐴 , 𝐶 } )
19 18 eqeq2d ⊢ ( { 𝐶 , 𝐴 , 𝐵 } = { 𝐶 , 𝐴 } → ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ↔ 𝑉 = { 𝐴 , 𝐶 } ) )
20 olc ⊢ ( 𝑉 = { 𝐴 , 𝐶 } → ( 𝑉 = { 𝐴 } ∨ 𝑉 = { 𝐴 , 𝐶 } ) )
21 1 2 1to2vfriswmgr ⊢ ( ( 𝐴 ∈ 𝑋 ∧ ( 𝑉 = { 𝐴 } ∨ 𝑉 = { 𝐴 , 𝐶 } ) ) → ( 𝐺 ∈ FriendGraph → ∃ ℎ ∈ 𝑉 ∀ 𝑣 ∈ ( 𝑉 ∖ { ℎ } ) ( { 𝑣 , ℎ } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( 𝑉 ∖ { ℎ } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) )
22 20 21 sylan2 ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝑉 = { 𝐴 , 𝐶 } ) → ( 𝐺 ∈ FriendGraph → ∃ ℎ ∈ 𝑉 ∀ 𝑣 ∈ ( 𝑉 ∖ { ℎ } ) ( { 𝑣 , ℎ } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( 𝑉 ∖ { ℎ } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) )
23 22 expcom ⊢ ( 𝑉 = { 𝐴 , 𝐶 } → ( 𝐴 ∈ 𝑋 → ( 𝐺 ∈ FriendGraph → ∃ ℎ ∈ 𝑉 ∀ 𝑣 ∈ ( 𝑉 ∖ { ℎ } ) ( { 𝑣 , ℎ } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( 𝑉 ∖ { ℎ } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) ) )
24 19 23 biimtrdi ⊢ ( { 𝐶 , 𝐴 , 𝐵 } = { 𝐶 , 𝐴 } → ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } → ( 𝐴 ∈ 𝑋 → ( 𝐺 ∈ FriendGraph → ∃ ℎ ∈ 𝑉 ∀ 𝑣 ∈ ( 𝑉 ∖ { ℎ } ) ( { 𝑣 , ℎ } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( 𝑉 ∖ { ℎ } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) ) ) )
25 13 24 syl ⊢ ( ¬ ( 𝐵 ∈ V ∧ 𝐵 ≠ 𝐴 ) → ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } → ( 𝐴 ∈ 𝑋 → ( 𝐺 ∈ FriendGraph → ∃ ℎ ∈ 𝑉 ∀ 𝑣 ∈ ( 𝑉 ∖ { ℎ } ) ( { 𝑣 , ℎ } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( 𝑉 ∖ { ℎ } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) ) ) )
26 25 a1d ⊢ ( ¬ ( 𝐵 ∈ V ∧ 𝐵 ≠ 𝐴 ) → ( 𝐵 ≠ 𝐶 → ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } → ( 𝐴 ∈ 𝑋 → ( 𝐺 ∈ FriendGraph → ∃ ℎ ∈ 𝑉 ∀ 𝑣 ∈ ( 𝑉 ∖ { ℎ } ) ( { 𝑣 , ℎ } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( 𝑉 ∖ { ℎ } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) ) ) ) )
27 tpprceq3 ⊢ ( ¬ ( 𝐶 ∈ V ∧ 𝐶 ≠ 𝐴 ) → { 𝐵 , 𝐴 , 𝐶 } = { 𝐵 , 𝐴 } )
28 tpcoma ⊢ { 𝐵 , 𝐴 , 𝐶 } = { 𝐴 , 𝐵 , 𝐶 }
29 28 eqeq1i ⊢ ( { 𝐵 , 𝐴 , 𝐶 } = { 𝐵 , 𝐴 } ↔ { 𝐴 , 𝐵 , 𝐶 } = { 𝐵 , 𝐴 } )
30 29 biimpi ⊢ ( { 𝐵 , 𝐴 , 𝐶 } = { 𝐵 , 𝐴 } → { 𝐴 , 𝐵 , 𝐶 } = { 𝐵 , 𝐴 } )
31 prcom ⊢ { 𝐵 , 𝐴 } = { 𝐴 , 𝐵 }
32 30 31 eqtrdi ⊢ ( { 𝐵 , 𝐴 , 𝐶 } = { 𝐵 , 𝐴 } → { 𝐴 , 𝐵 , 𝐶 } = { 𝐴 , 𝐵 } )
33 32 eqeq2d ⊢ ( { 𝐵 , 𝐴 , 𝐶 } = { 𝐵 , 𝐴 } → ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ↔ 𝑉 = { 𝐴 , 𝐵 } ) )
34 8 4 sylan2 ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝑉 = { 𝐴 , 𝐵 } ) → ( 𝐺 ∈ FriendGraph → ∃ ℎ ∈ 𝑉 ∀ 𝑣 ∈ ( 𝑉 ∖ { ℎ } ) ( { 𝑣 , ℎ } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( 𝑉 ∖ { ℎ } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) )
35 34 expcom ⊢ ( 𝑉 = { 𝐴 , 𝐵 } → ( 𝐴 ∈ 𝑋 → ( 𝐺 ∈ FriendGraph → ∃ ℎ ∈ 𝑉 ∀ 𝑣 ∈ ( 𝑉 ∖ { ℎ } ) ( { 𝑣 , ℎ } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( 𝑉 ∖ { ℎ } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) ) )
36 35 a1d ⊢ ( 𝑉 = { 𝐴 , 𝐵 } → ( 𝐵 ≠ 𝐶 → ( 𝐴 ∈ 𝑋 → ( 𝐺 ∈ FriendGraph → ∃ ℎ ∈ 𝑉 ∀ 𝑣 ∈ ( 𝑉 ∖ { ℎ } ) ( { 𝑣 , ℎ } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( 𝑉 ∖ { ℎ } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) ) ) )
37 33 36 biimtrdi ⊢ ( { 𝐵 , 𝐴 , 𝐶 } = { 𝐵 , 𝐴 } → ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } → ( 𝐵 ≠ 𝐶 → ( 𝐴 ∈ 𝑋 → ( 𝐺 ∈ FriendGraph → ∃ ℎ ∈ 𝑉 ∀ 𝑣 ∈ ( 𝑉 ∖ { ℎ } ) ( { 𝑣 , ℎ } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( 𝑉 ∖ { ℎ } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) ) ) ) )
38 27 37 syl ⊢ ( ¬ ( 𝐶 ∈ V ∧ 𝐶 ≠ 𝐴 ) → ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } → ( 𝐵 ≠ 𝐶 → ( 𝐴 ∈ 𝑋 → ( 𝐺 ∈ FriendGraph → ∃ ℎ ∈ 𝑉 ∀ 𝑣 ∈ ( 𝑉 ∖ { ℎ } ) ( { 𝑣 , ℎ } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( 𝑉 ∖ { ℎ } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) ) ) ) )
39 38 com23 ⊢ ( ¬ ( 𝐶 ∈ V ∧ 𝐶 ≠ 𝐴 ) → ( 𝐵 ≠ 𝐶 → ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } → ( 𝐴 ∈ 𝑋 → ( 𝐺 ∈ FriendGraph → ∃ ℎ ∈ 𝑉 ∀ 𝑣 ∈ ( 𝑉 ∖ { ℎ } ) ( { 𝑣 , ℎ } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( 𝑉 ∖ { ℎ } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) ) ) ) )
40 simpl ⊢ ( ( 𝐵 ∈ V ∧ 𝐵 ≠ 𝐴 ) → 𝐵 ∈ V )
41 simpl ⊢ ( ( 𝐶 ∈ V ∧ 𝐶 ≠ 𝐴 ) → 𝐶 ∈ V )
42 40 41 anim12i ⊢ ( ( ( 𝐵 ∈ V ∧ 𝐵 ≠ 𝐴 ) ∧ ( 𝐶 ∈ V ∧ 𝐶 ≠ 𝐴 ) ) → ( 𝐵 ∈ V ∧ 𝐶 ∈ V ) )
43 42 ad2antrr ⊢ ( ( ( ( ( 𝐵 ∈ V ∧ 𝐵 ≠ 𝐴 ) ∧ ( 𝐶 ∈ V ∧ 𝐶 ≠ 𝐴 ) ) ∧ 𝐵 ≠ 𝐶 ) ∧ 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ) → ( 𝐵 ∈ V ∧ 𝐶 ∈ V ) )
44 43 anim1ci ⊢ ( ( ( ( ( ( 𝐵 ∈ V ∧ 𝐵 ≠ 𝐴 ) ∧ ( 𝐶 ∈ V ∧ 𝐶 ≠ 𝐴 ) ) ∧ 𝐵 ≠ 𝐶 ) ∧ 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ) ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 ∈ 𝑋 ∧ ( 𝐵 ∈ V ∧ 𝐶 ∈ V ) ) )
45 3anass ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V ) ↔ ( 𝐴 ∈ 𝑋 ∧ ( 𝐵 ∈ V ∧ 𝐶 ∈ V ) ) )
46 44 45 sylibr ⊢ ( ( ( ( ( ( 𝐵 ∈ V ∧ 𝐵 ≠ 𝐴 ) ∧ ( 𝐶 ∈ V ∧ 𝐶 ≠ 𝐴 ) ) ∧ 𝐵 ≠ 𝐶 ) ∧ 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ) ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V ) )
47 simpr ⊢ ( ( 𝐵 ∈ V ∧ 𝐵 ≠ 𝐴 ) → 𝐵 ≠ 𝐴 )
48 47 necomd ⊢ ( ( 𝐵 ∈ V ∧ 𝐵 ≠ 𝐴 ) → 𝐴 ≠ 𝐵 )
49 simpr ⊢ ( ( 𝐶 ∈ V ∧ 𝐶 ≠ 𝐴 ) → 𝐶 ≠ 𝐴 )
50 49 necomd ⊢ ( ( 𝐶 ∈ V ∧ 𝐶 ≠ 𝐴 ) → 𝐴 ≠ 𝐶 )
51 48 50 anim12i ⊢ ( ( ( 𝐵 ∈ V ∧ 𝐵 ≠ 𝐴 ) ∧ ( 𝐶 ∈ V ∧ 𝐶 ≠ 𝐴 ) ) → ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ) )
52 51 anim1i ⊢ ( ( ( ( 𝐵 ∈ V ∧ 𝐵 ≠ 𝐴 ) ∧ ( 𝐶 ∈ V ∧ 𝐶 ≠ 𝐴 ) ) ∧ 𝐵 ≠ 𝐶 ) → ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ) ∧ 𝐵 ≠ 𝐶 ) )
53 df-3an ⊢ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ↔ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ) ∧ 𝐵 ≠ 𝐶 ) )
54 52 53 sylibr ⊢ ( ( ( ( 𝐵 ∈ V ∧ 𝐵 ≠ 𝐴 ) ∧ ( 𝐶 ∈ V ∧ 𝐶 ≠ 𝐴 ) ) ∧ 𝐵 ≠ 𝐶 ) → ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) )
55 54 ad2antrr ⊢ ( ( ( ( ( ( 𝐵 ∈ V ∧ 𝐵 ≠ 𝐴 ) ∧ ( 𝐶 ∈ V ∧ 𝐶 ≠ 𝐴 ) ) ∧ 𝐵 ≠ 𝐶 ) ∧ 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ) ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) )
56 simplr ⊢ ( ( ( ( ( ( 𝐵 ∈ V ∧ 𝐵 ≠ 𝐴 ) ∧ ( 𝐶 ∈ V ∧ 𝐶 ≠ 𝐴 ) ) ∧ 𝐵 ≠ 𝐶 ) ∧ 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ) ∧ 𝐴 ∈ 𝑋 ) → 𝑉 = { 𝐴 , 𝐵 , 𝐶 } )
57 1 2 3vfriswmgr ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ) → ( 𝐺 ∈ FriendGraph → ∃ ℎ ∈ 𝑉 ∀ 𝑣 ∈ ( 𝑉 ∖ { ℎ } ) ( { 𝑣 , ℎ } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( 𝑉 ∖ { ℎ } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) )
58 46 55 56 57 syl3anc ⊢ ( ( ( ( ( ( 𝐵 ∈ V ∧ 𝐵 ≠ 𝐴 ) ∧ ( 𝐶 ∈ V ∧ 𝐶 ≠ 𝐴 ) ) ∧ 𝐵 ≠ 𝐶 ) ∧ 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ) ∧ 𝐴 ∈ 𝑋 ) → ( 𝐺 ∈ FriendGraph → ∃ ℎ ∈ 𝑉 ∀ 𝑣 ∈ ( 𝑉 ∖ { ℎ } ) ( { 𝑣 , ℎ } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( 𝑉 ∖ { ℎ } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) )
59 58 exp41 ⊢ ( ( ( 𝐵 ∈ V ∧ 𝐵 ≠ 𝐴 ) ∧ ( 𝐶 ∈ V ∧ 𝐶 ≠ 𝐴 ) ) → ( 𝐵 ≠ 𝐶 → ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } → ( 𝐴 ∈ 𝑋 → ( 𝐺 ∈ FriendGraph → ∃ ℎ ∈ 𝑉 ∀ 𝑣 ∈ ( 𝑉 ∖ { ℎ } ) ( { 𝑣 , ℎ } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( 𝑉 ∖ { ℎ } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) ) ) ) )
60 26 39 59 ecase ⊢ ( 𝐵 ≠ 𝐶 → ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } → ( 𝐴 ∈ 𝑋 → ( 𝐺 ∈ FriendGraph → ∃ ℎ ∈ 𝑉 ∀ 𝑣 ∈ ( 𝑉 ∖ { ℎ } ) ( { 𝑣 , ℎ } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( 𝑉 ∖ { ℎ } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) ) ) )
61 12 60 pm2.61ine ⊢ ( 𝑉 = { 𝐴 , 𝐵 , 𝐶 } → ( 𝐴 ∈ 𝑋 → ( 𝐺 ∈ FriendGraph → ∃ ℎ ∈ 𝑉 ∀ 𝑣 ∈ ( 𝑉 ∖ { ℎ } ) ( { 𝑣 , ℎ } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( 𝑉 ∖ { ℎ } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) ) )
62 5 61 jaoi ⊢ ( ( ( 𝑉 = { 𝐴 } ∨ 𝑉 = { 𝐴 , 𝐵 } ) ∨ 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ) → ( 𝐴 ∈ 𝑋 → ( 𝐺 ∈ FriendGraph → ∃ ℎ ∈ 𝑉 ∀ 𝑣 ∈ ( 𝑉 ∖ { ℎ } ) ( { 𝑣 , ℎ } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( 𝑉 ∖ { ℎ } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) ) )
63 3 62 sylbi ⊢ ( ( 𝑉 = { 𝐴 } ∨ 𝑉 = { 𝐴 , 𝐵 } ∨ 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ) → ( 𝐴 ∈ 𝑋 → ( 𝐺 ∈ FriendGraph → ∃ ℎ ∈ 𝑉 ∀ 𝑣 ∈ ( 𝑉 ∖ { ℎ } ) ( { 𝑣 , ℎ } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( 𝑉 ∖ { ℎ } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) ) )
64 63 impcom ⊢ ( ( 𝐴 ∈ 𝑋 ∧ ( 𝑉 = { 𝐴 } ∨ 𝑉 = { 𝐴 , 𝐵 } ∨ 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ) ) → ( 𝐺 ∈ FriendGraph → ∃ ℎ ∈ 𝑉 ∀ 𝑣 ∈ ( 𝑉 ∖ { ℎ } ) ( { 𝑣 , ℎ } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( 𝑉 ∖ { ℎ } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) )