Metamath Proof Explorer

Theorem frgr1v

Description: Any graph with (at most) one vertex is a friendship graph. (Contributed by Alexander van der Vekens, 4-Oct-2017) (Revised by AV, 29-Mar-2021)

Ref Expression
Assertion frgr1v ( ( 𝐺 ∈ USGraph ∧ ( Vtx ‘ 𝐺 ) = { 𝑁 } ) → 𝐺 ∈ FriendGraph )

Proof

Step Hyp Ref Expression
1 simpl ⊢ ( ( 𝐺 ∈ USGraph ∧ ( Vtx ‘ 𝐺 ) = { 𝑁 } ) → 𝐺 ∈ USGraph )
2 ral0 ⊢ ∀ 𝑙 ∈ ∅ ∃! 𝑥 ∈ { 𝑁 } { { 𝑥 , 𝑁 } , { 𝑥 , 𝑙 } } ⊆ ( Edg ‘ 𝐺 )
3 sneq ⊢ ( 𝑘 = 𝑁 → { 𝑘 } = { 𝑁 } )
4 3 difeq2d ⊢ ( 𝑘 = 𝑁 → ( { 𝑁 } ∖ { 𝑘 } ) = ( { 𝑁 } ∖ { 𝑁 } ) )
5 difid ⊢ ( { 𝑁 } ∖ { 𝑁 } ) = ∅
6 4 5 eqtrdi ⊢ ( 𝑘 = 𝑁 → ( { 𝑁 } ∖ { 𝑘 } ) = ∅ )
7 preq2 ⊢ ( 𝑘 = 𝑁 → { 𝑥 , 𝑘 } = { 𝑥 , 𝑁 } )
8 7 preq1d ⊢ ( 𝑘 = 𝑁 → { { 𝑥 , 𝑘 } , { 𝑥 , 𝑙 } } = { { 𝑥 , 𝑁 } , { 𝑥 , 𝑙 } } )
9 8 sseq1d ⊢ ( 𝑘 = 𝑁 → ( { { 𝑥 , 𝑘 } , { 𝑥 , 𝑙 } } ⊆ ( Edg ‘ 𝐺 ) ↔ { { 𝑥 , 𝑁 } , { 𝑥 , 𝑙 } } ⊆ ( Edg ‘ 𝐺 ) ) )
10 9 reubidv ⊢ ( 𝑘 = 𝑁 → ( ∃! 𝑥 ∈ { 𝑁 } { { 𝑥 , 𝑘 } , { 𝑥 , 𝑙 } } ⊆ ( Edg ‘ 𝐺 ) ↔ ∃! 𝑥 ∈ { 𝑁 } { { 𝑥 , 𝑁 } , { 𝑥 , 𝑙 } } ⊆ ( Edg ‘ 𝐺 ) ) )
11 6 10 raleqbidv ⊢ ( 𝑘 = 𝑁 → ( ∀ 𝑙 ∈ ( { 𝑁 } ∖ { 𝑘 } ) ∃! 𝑥 ∈ { 𝑁 } { { 𝑥 , 𝑘 } , { 𝑥 , 𝑙 } } ⊆ ( Edg ‘ 𝐺 ) ↔ ∀ 𝑙 ∈ ∅ ∃! 𝑥 ∈ { 𝑁 } { { 𝑥 , 𝑁 } , { 𝑥 , 𝑙 } } ⊆ ( Edg ‘ 𝐺 ) ) )
12 11 ralsng ⊢ ( 𝑁 ∈ V → ( ∀ 𝑘 ∈ { 𝑁 } ∀ 𝑙 ∈ ( { 𝑁 } ∖ { 𝑘 } ) ∃! 𝑥 ∈ { 𝑁 } { { 𝑥 , 𝑘 } , { 𝑥 , 𝑙 } } ⊆ ( Edg ‘ 𝐺 ) ↔ ∀ 𝑙 ∈ ∅ ∃! 𝑥 ∈ { 𝑁 } { { 𝑥 , 𝑁 } , { 𝑥 , 𝑙 } } ⊆ ( Edg ‘ 𝐺 ) ) )
13 2 12 mpbiri ⊢ ( 𝑁 ∈ V → ∀ 𝑘 ∈ { 𝑁 } ∀ 𝑙 ∈ ( { 𝑁 } ∖ { 𝑘 } ) ∃! 𝑥 ∈ { 𝑁 } { { 𝑥 , 𝑘 } , { 𝑥 , 𝑙 } } ⊆ ( Edg ‘ 𝐺 ) )
14 snprc ⊢ ( ¬ 𝑁 ∈ V ↔ { 𝑁 } = ∅ )
15 rzal ⊢ ( { 𝑁 } = ∅ → ∀ 𝑘 ∈ { 𝑁 } ∀ 𝑙 ∈ ( { 𝑁 } ∖ { 𝑘 } ) ∃! 𝑥 ∈ { 𝑁 } { { 𝑥 , 𝑘 } , { 𝑥 , 𝑙 } } ⊆ ( Edg ‘ 𝐺 ) )
16 14 15 sylbi ⊢ ( ¬ 𝑁 ∈ V → ∀ 𝑘 ∈ { 𝑁 } ∀ 𝑙 ∈ ( { 𝑁 } ∖ { 𝑘 } ) ∃! 𝑥 ∈ { 𝑁 } { { 𝑥 , 𝑘 } , { 𝑥 , 𝑙 } } ⊆ ( Edg ‘ 𝐺 ) )
17 13 16 pm2.61i ⊢ ∀ 𝑘 ∈ { 𝑁 } ∀ 𝑙 ∈ ( { 𝑁 } ∖ { 𝑘 } ) ∃! 𝑥 ∈ { 𝑁 } { { 𝑥 , 𝑘 } , { 𝑥 , 𝑙 } } ⊆ ( Edg ‘ 𝐺 )
18 id ⊢ ( ( Vtx ‘ 𝐺 ) = { 𝑁 } → ( Vtx ‘ 𝐺 ) = { 𝑁 } )
19 difeq1 ⊢ ( ( Vtx ‘ 𝐺 ) = { 𝑁 } → ( ( Vtx ‘ 𝐺 ) ∖ { 𝑘 } ) = ( { 𝑁 } ∖ { 𝑘 } ) )
20 reueq1 ⊢ ( ( Vtx ‘ 𝐺 ) = { 𝑁 } → ( ∃! 𝑥 ∈ ( Vtx ‘ 𝐺 ) { { 𝑥 , 𝑘 } , { 𝑥 , 𝑙 } } ⊆ ( Edg ‘ 𝐺 ) ↔ ∃! 𝑥 ∈ { 𝑁 } { { 𝑥 , 𝑘 } , { 𝑥 , 𝑙 } } ⊆ ( Edg ‘ 𝐺 ) ) )
21 19 20 raleqbidv ⊢ ( ( Vtx ‘ 𝐺 ) = { 𝑁 } → ( ∀ 𝑙 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝑘 } ) ∃! 𝑥 ∈ ( Vtx ‘ 𝐺 ) { { 𝑥 , 𝑘 } , { 𝑥 , 𝑙 } } ⊆ ( Edg ‘ 𝐺 ) ↔ ∀ 𝑙 ∈ ( { 𝑁 } ∖ { 𝑘 } ) ∃! 𝑥 ∈ { 𝑁 } { { 𝑥 , 𝑘 } , { 𝑥 , 𝑙 } } ⊆ ( Edg ‘ 𝐺 ) ) )
22 18 21 raleqbidv ⊢ ( ( Vtx ‘ 𝐺 ) = { 𝑁 } → ( ∀ 𝑘 ∈ ( Vtx ‘ 𝐺 ) ∀ 𝑙 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝑘 } ) ∃! 𝑥 ∈ ( Vtx ‘ 𝐺 ) { { 𝑥 , 𝑘 } , { 𝑥 , 𝑙 } } ⊆ ( Edg ‘ 𝐺 ) ↔ ∀ 𝑘 ∈ { 𝑁 } ∀ 𝑙 ∈ ( { 𝑁 } ∖ { 𝑘 } ) ∃! 𝑥 ∈ { 𝑁 } { { 𝑥 , 𝑘 } , { 𝑥 , 𝑙 } } ⊆ ( Edg ‘ 𝐺 ) ) )
23 22 adantl ⊢ ( ( 𝐺 ∈ USGraph ∧ ( Vtx ‘ 𝐺 ) = { 𝑁 } ) → ( ∀ 𝑘 ∈ ( Vtx ‘ 𝐺 ) ∀ 𝑙 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝑘 } ) ∃! 𝑥 ∈ ( Vtx ‘ 𝐺 ) { { 𝑥 , 𝑘 } , { 𝑥 , 𝑙 } } ⊆ ( Edg ‘ 𝐺 ) ↔ ∀ 𝑘 ∈ { 𝑁 } ∀ 𝑙 ∈ ( { 𝑁 } ∖ { 𝑘 } ) ∃! 𝑥 ∈ { 𝑁 } { { 𝑥 , 𝑘 } , { 𝑥 , 𝑙 } } ⊆ ( Edg ‘ 𝐺 ) ) )
24 17 23 mpbiri ⊢ ( ( 𝐺 ∈ USGraph ∧ ( Vtx ‘ 𝐺 ) = { 𝑁 } ) → ∀ 𝑘 ∈ ( Vtx ‘ 𝐺 ) ∀ 𝑙 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝑘 } ) ∃! 𝑥 ∈ ( Vtx ‘ 𝐺 ) { { 𝑥 , 𝑘 } , { 𝑥 , 𝑙 } } ⊆ ( Edg ‘ 𝐺 ) )
25 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
26 eqid ⊢ ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 )
27 25 26 isfrgr ⊢ ( 𝐺 ∈ FriendGraph ↔ ( 𝐺 ∈ USGraph ∧ ∀ 𝑘 ∈ ( Vtx ‘ 𝐺 ) ∀ 𝑙 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝑘 } ) ∃! 𝑥 ∈ ( Vtx ‘ 𝐺 ) { { 𝑥 , 𝑘 } , { 𝑥 , 𝑙 } } ⊆ ( Edg ‘ 𝐺 ) ) )
28 1 24 27 sylanbrc ⊢ ( ( 𝐺 ∈ USGraph ∧ ( Vtx ‘ 𝐺 ) = { 𝑁 } ) → 𝐺 ∈ FriendGraph )