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	biimtrdi	⊢ ( ¬ ( 𝐵 ∈ V ∧ 𝐴 ≠ 𝐵 ) → ( 𝑉 = { 𝐴 , 𝐵 } → ( 𝐴 ∈ 𝑋 → ( 𝐺 ∈ FriendGraph → ∃ ℎ ∈ 𝑉 ∀ 𝑣 ∈ ( 𝑉 ∖ { ℎ } ) ( { 𝑣 , ℎ } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( 𝑉 ∖ { ℎ } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) ) ) )
32	19 31	pm2.61i	⊢ ( 𝑉 = { 𝐴 , 𝐵 } → ( 𝐴 ∈ 𝑋 → ( 𝐺 ∈ FriendGraph → ∃ ℎ ∈ 𝑉 ∀ 𝑣 ∈ ( 𝑉 ∖ { ℎ } ) ( { 𝑣 , ℎ } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( 𝑉 ∖ { ℎ } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) ) )
33	5 32	jaoi	⊢ ( ( 𝑉 = { 𝐴 } ∨ 𝑉 = { 𝐴 , 𝐵 } ) → ( 𝐴 ∈ 𝑋 → ( 𝐺 ∈ FriendGraph → ∃ ℎ ∈ 𝑉 ∀ 𝑣 ∈ ( 𝑉 ∖ { ℎ } ) ( { 𝑣 , ℎ } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( 𝑉 ∖ { ℎ } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) ) )
34	33	impcom	⊢ ( ( 𝐴 ∈ 𝑋 ∧ ( 𝑉 = { 𝐴 } ∨ 𝑉 = { 𝐴 , 𝐵 } ) ) → ( 𝐺 ∈ FriendGraph → ∃ ℎ ∈ 𝑉 ∀ 𝑣 ∈ ( 𝑉 ∖ { ℎ } ) ( { 𝑣 , ℎ } ∈ 𝐸 ∧ ∃! 𝑤 ∈ ( 𝑉 ∖ { ℎ } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) )

Metamath Proof Explorer

Theorem 1to2vfriswmgr

Proof