Theorem frgr0v

Description: Any null graph (set with no vertices) is a friendship graph iff its edge function is empty. (Contributed by Alexander van der Vekens, 4-Oct-2017) (Revised by AV, 29-Mar-2021)

	Ref	Expression
Assertion	frgr0v	⊢ ( ( 𝐺 ∈ 𝑊 ∧ ( Vtx ‘ 𝐺 ) = ∅ ) → ( 𝐺 ∈ FriendGraph ↔ ( iEdg ‘ 𝐺 ) = ∅ ) )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
2		eqid	⊢ ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 )
3	1 2	isfrgr	⊢ ( 𝐺 ∈ FriendGraph ↔ ( 𝐺 ∈ USGraph ∧ ∀ 𝑘 ∈ ( Vtx ‘ 𝐺 ) ∀ 𝑙 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝑘 } ) ∃! 𝑥 ∈ ( Vtx ‘ 𝐺 ) { { 𝑥 , 𝑘 } , { 𝑥 , 𝑙 } } ⊆ ( Edg ‘ 𝐺 ) ) )
4		usgruhgr	⊢ ( 𝐺 ∈ USGraph → 𝐺 ∈ UHGraph )
5	4	adantr	⊢ ( ( 𝐺 ∈ USGraph ∧ ∀ 𝑘 ∈ ( Vtx ‘ 𝐺 ) ∀ 𝑙 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝑘 } ) ∃! 𝑥 ∈ ( Vtx ‘ 𝐺 ) { { 𝑥 , 𝑘 } , { 𝑥 , 𝑙 } } ⊆ ( Edg ‘ 𝐺 ) ) → 𝐺 ∈ UHGraph )
6		uhgr0vb	⊢ ( ( 𝐺 ∈ 𝑊 ∧ ( Vtx ‘ 𝐺 ) = ∅ ) → ( 𝐺 ∈ UHGraph ↔ ( iEdg ‘ 𝐺 ) = ∅ ) )
7	5 6	imbitrid	⊢ ( ( 𝐺 ∈ 𝑊 ∧ ( Vtx ‘ 𝐺 ) = ∅ ) → ( ( 𝐺 ∈ USGraph ∧ ∀ 𝑘 ∈ ( Vtx ‘ 𝐺 ) ∀ 𝑙 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝑘 } ) ∃! 𝑥 ∈ ( Vtx ‘ 𝐺 ) { { 𝑥 , 𝑘 } , { 𝑥 , 𝑙 } } ⊆ ( Edg ‘ 𝐺 ) ) → ( iEdg ‘ 𝐺 ) = ∅ ) )
8		simpll	⊢ ( ( ( 𝐺 ∈ 𝑊 ∧ ( Vtx ‘ 𝐺 ) = ∅ ) ∧ ( iEdg ‘ 𝐺 ) = ∅ ) → 𝐺 ∈ 𝑊 )
9		simpr	⊢ ( ( ( 𝐺 ∈ 𝑊 ∧ ( Vtx ‘ 𝐺 ) = ∅ ) ∧ ( iEdg ‘ 𝐺 ) = ∅ ) → ( iEdg ‘ 𝐺 ) = ∅ )
10	8 9	usgr0e	⊢ ( ( ( 𝐺 ∈ 𝑊 ∧ ( Vtx ‘ 𝐺 ) = ∅ ) ∧ ( iEdg ‘ 𝐺 ) = ∅ ) → 𝐺 ∈ USGraph )
11		ral0	⊢ ∀ 𝑘 ∈ ∅ ∀ 𝑙 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝑘 } ) ∃! 𝑥 ∈ ( Vtx ‘ 𝐺 ) { { 𝑥 , 𝑘 } , { 𝑥 , 𝑙 } } ⊆ ( Edg ‘ 𝐺 )
12		raleq	⊢ ( ( Vtx ‘ 𝐺 ) = ∅ → ( ∀ 𝑘 ∈ ( Vtx ‘ 𝐺 ) ∀ 𝑙 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝑘 } ) ∃! 𝑥 ∈ ( Vtx ‘ 𝐺 ) { { 𝑥 , 𝑘 } , { 𝑥 , 𝑙 } } ⊆ ( Edg ‘ 𝐺 ) ↔ ∀ 𝑘 ∈ ∅ ∀ 𝑙 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝑘 } ) ∃! 𝑥 ∈ ( Vtx ‘ 𝐺 ) { { 𝑥 , 𝑘 } , { 𝑥 , 𝑙 } } ⊆ ( Edg ‘ 𝐺 ) ) )
13	12	adantl	⊢ ( ( 𝐺 ∈ 𝑊 ∧ ( Vtx ‘ 𝐺 ) = ∅ ) → ( ∀ 𝑘 ∈ ( Vtx ‘ 𝐺 ) ∀ 𝑙 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝑘 } ) ∃! 𝑥 ∈ ( Vtx ‘ 𝐺 ) { { 𝑥 , 𝑘 } , { 𝑥 , 𝑙 } } ⊆ ( Edg ‘ 𝐺 ) ↔ ∀ 𝑘 ∈ ∅ ∀ 𝑙 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝑘 } ) ∃! 𝑥 ∈ ( Vtx ‘ 𝐺 ) { { 𝑥 , 𝑘 } , { 𝑥 , 𝑙 } } ⊆ ( Edg ‘ 𝐺 ) ) )
14	11 13	mpbiri	⊢ ( ( 𝐺 ∈ 𝑊 ∧ ( Vtx ‘ 𝐺 ) = ∅ ) → ∀ 𝑘 ∈ ( Vtx ‘ 𝐺 ) ∀ 𝑙 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝑘 } ) ∃! 𝑥 ∈ ( Vtx ‘ 𝐺 ) { { 𝑥 , 𝑘 } , { 𝑥 , 𝑙 } } ⊆ ( Edg ‘ 𝐺 ) )
15	14	adantr	⊢ ( ( ( 𝐺 ∈ 𝑊 ∧ ( Vtx ‘ 𝐺 ) = ∅ ) ∧ ( iEdg ‘ 𝐺 ) = ∅ ) → ∀ 𝑘 ∈ ( Vtx ‘ 𝐺 ) ∀ 𝑙 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝑘 } ) ∃! 𝑥 ∈ ( Vtx ‘ 𝐺 ) { { 𝑥 , 𝑘 } , { 𝑥 , 𝑙 } } ⊆ ( Edg ‘ 𝐺 ) )
16	10 15	jca	⊢ ( ( ( 𝐺 ∈ 𝑊 ∧ ( Vtx ‘ 𝐺 ) = ∅ ) ∧ ( iEdg ‘ 𝐺 ) = ∅ ) → ( 𝐺 ∈ USGraph ∧ ∀ 𝑘 ∈ ( Vtx ‘ 𝐺 ) ∀ 𝑙 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝑘 } ) ∃! 𝑥 ∈ ( Vtx ‘ 𝐺 ) { { 𝑥 , 𝑘 } , { 𝑥 , 𝑙 } } ⊆ ( Edg ‘ 𝐺 ) ) )
17	16	ex	⊢ ( ( 𝐺 ∈ 𝑊 ∧ ( Vtx ‘ 𝐺 ) = ∅ ) → ( ( iEdg ‘ 𝐺 ) = ∅ → ( 𝐺 ∈ USGraph ∧ ∀ 𝑘 ∈ ( Vtx ‘ 𝐺 ) ∀ 𝑙 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝑘 } ) ∃! 𝑥 ∈ ( Vtx ‘ 𝐺 ) { { 𝑥 , 𝑘 } , { 𝑥 , 𝑙 } } ⊆ ( Edg ‘ 𝐺 ) ) ) )
18	7 17	impbid	⊢ ( ( 𝐺 ∈ 𝑊 ∧ ( Vtx ‘ 𝐺 ) = ∅ ) → ( ( 𝐺 ∈ USGraph ∧ ∀ 𝑘 ∈ ( Vtx ‘ 𝐺 ) ∀ 𝑙 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝑘 } ) ∃! 𝑥 ∈ ( Vtx ‘ 𝐺 ) { { 𝑥 , 𝑘 } , { 𝑥 , 𝑙 } } ⊆ ( Edg ‘ 𝐺 ) ) ↔ ( iEdg ‘ 𝐺 ) = ∅ ) )
19	3 18	bitrid	⊢ ( ( 𝐺 ∈ 𝑊 ∧ ( Vtx ‘ 𝐺 ) = ∅ ) → ( 𝐺 ∈ FriendGraph ↔ ( iEdg ‘ 𝐺 ) = ∅ ) )