Metamath Proof Explorer


Theorem 1to2vfriswmgr

Description: Every friendship graph with one or two 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 1to2vfriswmgr ( ( 𝐴𝑋 ∧ ( 𝑉 = { 𝐴 } ∨ 𝑉 = { 𝐴 , 𝐵 } ) ) → ( 𝐺 ∈ FriendGraph → ∃ 𝑉𝑣 ∈ ( 𝑉 ∖ { } ) ( { 𝑣 , } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( 𝑉 ∖ { } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) )

Proof

Step Hyp Ref Expression
1 3vfriswmgr.v 𝑉 = ( Vtx ‘ 𝐺 )
2 3vfriswmgr.e 𝐸 = ( Edg ‘ 𝐺 )
3 1vwmgr ( ( 𝐴𝑋𝑉 = { 𝐴 } ) → ∃ 𝑉𝑣 ∈ ( 𝑉 ∖ { } ) ( { 𝑣 , } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( 𝑉 ∖ { } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) )
4 3 a1d ( ( 𝐴𝑋𝑉 = { 𝐴 } ) → ( 𝐺 ∈ FriendGraph → ∃ 𝑉𝑣 ∈ ( 𝑉 ∖ { } ) ( { 𝑣 , } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( 𝑉 ∖ { } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) )
5 4 expcom ( 𝑉 = { 𝐴 } → ( 𝐴𝑋 → ( 𝐺 ∈ FriendGraph → ∃ 𝑉𝑣 ∈ ( 𝑉 ∖ { } ) ( { 𝑣 , } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( 𝑉 ∖ { } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) ) )
6 simpr ( ( ( 𝐵 ∈ V ∧ 𝐴𝐵 ) ∧ 𝐴𝑋 ) → 𝐴𝑋 )
7 simpll ( ( ( 𝐵 ∈ V ∧ 𝐴𝐵 ) ∧ 𝐴𝑋 ) → 𝐵 ∈ V )
8 simplr ( ( ( 𝐵 ∈ V ∧ 𝐴𝐵 ) ∧ 𝐴𝑋 ) → 𝐴𝐵 )
9 6 7 8 3jca ( ( ( 𝐵 ∈ V ∧ 𝐴𝐵 ) ∧ 𝐴𝑋 ) → ( 𝐴𝑋𝐵 ∈ V ∧ 𝐴𝐵 ) )
10 1 eqeq1i ( 𝑉 = { 𝐴 , 𝐵 } ↔ ( Vtx ‘ 𝐺 ) = { 𝐴 , 𝐵 } )
11 10 biimpi ( 𝑉 = { 𝐴 , 𝐵 } → ( Vtx ‘ 𝐺 ) = { 𝐴 , 𝐵 } )
12 nfrgr2v ( ( ( 𝐴𝑋𝐵 ∈ V ∧ 𝐴𝐵 ) ∧ ( Vtx ‘ 𝐺 ) = { 𝐴 , 𝐵 } ) → 𝐺 ∉ FriendGraph )
13 9 11 12 syl2anr ( ( 𝑉 = { 𝐴 , 𝐵 } ∧ ( ( 𝐵 ∈ V ∧ 𝐴𝐵 ) ∧ 𝐴𝑋 ) ) → 𝐺 ∉ FriendGraph )
14 df-nel ( 𝐺 ∉ FriendGraph ↔ ¬ 𝐺 ∈ FriendGraph )
15 13 14 sylib ( ( 𝑉 = { 𝐴 , 𝐵 } ∧ ( ( 𝐵 ∈ V ∧ 𝐴𝐵 ) ∧ 𝐴𝑋 ) ) → ¬ 𝐺 ∈ FriendGraph )
16 15 pm2.21d ( ( 𝑉 = { 𝐴 , 𝐵 } ∧ ( ( 𝐵 ∈ V ∧ 𝐴𝐵 ) ∧ 𝐴𝑋 ) ) → ( 𝐺 ∈ FriendGraph → ∃ 𝑉𝑣 ∈ ( 𝑉 ∖ { } ) ( { 𝑣 , } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( 𝑉 ∖ { } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) )
17 16 expcom ( ( ( 𝐵 ∈ V ∧ 𝐴𝐵 ) ∧ 𝐴𝑋 ) → ( 𝑉 = { 𝐴 , 𝐵 } → ( 𝐺 ∈ FriendGraph → ∃ 𝑉𝑣 ∈ ( 𝑉 ∖ { } ) ( { 𝑣 , } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( 𝑉 ∖ { } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) ) )
18 17 ex ( ( 𝐵 ∈ V ∧ 𝐴𝐵 ) → ( 𝐴𝑋 → ( 𝑉 = { 𝐴 , 𝐵 } → ( 𝐺 ∈ FriendGraph → ∃ 𝑉𝑣 ∈ ( 𝑉 ∖ { } ) ( { 𝑣 , } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( 𝑉 ∖ { } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) ) ) )
19 18 com23 ( ( 𝐵 ∈ V ∧ 𝐴𝐵 ) → ( 𝑉 = { 𝐴 , 𝐵 } → ( 𝐴𝑋 → ( 𝐺 ∈ FriendGraph → ∃ 𝑉𝑣 ∈ ( 𝑉 ∖ { } ) ( { 𝑣 , } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( 𝑉 ∖ { } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) ) ) )
20 ianor ( ¬ ( 𝐵 ∈ V ∧ 𝐴𝐵 ) ↔ ( ¬ 𝐵 ∈ V ∨ ¬ 𝐴𝐵 ) )
21 prprc2 ( ¬ 𝐵 ∈ V → { 𝐴 , 𝐵 } = { 𝐴 } )
22 nne ( ¬ 𝐴𝐵𝐴 = 𝐵 )
23 preq2 ( 𝐵 = 𝐴 → { 𝐴 , 𝐵 } = { 𝐴 , 𝐴 } )
24 23 eqcoms ( 𝐴 = 𝐵 → { 𝐴 , 𝐵 } = { 𝐴 , 𝐴 } )
25 dfsn2 { 𝐴 } = { 𝐴 , 𝐴 }
26 24 25 eqtr4di ( 𝐴 = 𝐵 → { 𝐴 , 𝐵 } = { 𝐴 } )
27 22 26 sylbi ( ¬ 𝐴𝐵 → { 𝐴 , 𝐵 } = { 𝐴 } )
28 21 27 jaoi ( ( ¬ 𝐵 ∈ V ∨ ¬ 𝐴𝐵 ) → { 𝐴 , 𝐵 } = { 𝐴 } )
29 20 28 sylbi ( ¬ ( 𝐵 ∈ V ∧ 𝐴𝐵 ) → { 𝐴 , 𝐵 } = { 𝐴 } )
30 29 eqeq2d ( ¬ ( 𝐵 ∈ V ∧ 𝐴𝐵 ) → ( 𝑉 = { 𝐴 , 𝐵 } ↔ 𝑉 = { 𝐴 } ) )
31 30 5 syl6bi ( ¬ ( 𝐵 ∈ V ∧ 𝐴𝐵 ) → ( 𝑉 = { 𝐴 , 𝐵 } → ( 𝐴𝑋 → ( 𝐺 ∈ FriendGraph → ∃ 𝑉𝑣 ∈ ( 𝑉 ∖ { } ) ( { 𝑣 , } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( 𝑉 ∖ { } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) ) ) )
32 19 31 pm2.61i ( 𝑉 = { 𝐴 , 𝐵 } → ( 𝐴𝑋 → ( 𝐺 ∈ FriendGraph → ∃ 𝑉𝑣 ∈ ( 𝑉 ∖ { } ) ( { 𝑣 , } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( 𝑉 ∖ { } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) ) )
33 5 32 jaoi ( ( 𝑉 = { 𝐴 } ∨ 𝑉 = { 𝐴 , 𝐵 } ) → ( 𝐴𝑋 → ( 𝐺 ∈ FriendGraph → ∃ 𝑉𝑣 ∈ ( 𝑉 ∖ { } ) ( { 𝑣 , } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( 𝑉 ∖ { } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) ) )
34 33 impcom ( ( 𝐴𝑋 ∧ ( 𝑉 = { 𝐴 } ∨ 𝑉 = { 𝐴 , 𝐵 } ) ) → ( 𝐺 ∈ FriendGraph → ∃ 𝑉𝑣 ∈ ( 𝑉 ∖ { } ) ( { 𝑣 , } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( 𝑉 ∖ { } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) )