Metamath Proof Explorer

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 ⊢ G ∈ W ∧ Vtx ⁡ G = ∅ → G ∈ FriendGraph ↔ iEdg ⁡ G = ∅

Proof

Step Hyp Ref Expression
1 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
2 eqid ⊢ Edg ⁡ G = Edg ⁡ G
3 1 2 isfrgr ⊢ G ∈ FriendGraph ↔ G ∈ USGraph ∧ ∀ k ∈ Vtx ⁡ G ∀ l ∈ Vtx ⁡ G ∖ k ∃! x ∈ Vtx ⁡ G x k x l ⊆ Edg ⁡ G
4 usgruhgr ⊢ G ∈ USGraph → G ∈ UHGraph
5 4 adantr ⊢ G ∈ USGraph ∧ ∀ k ∈ Vtx ⁡ G ∀ l ∈ Vtx ⁡ G ∖ k ∃! x ∈ Vtx ⁡ G x k x l ⊆ Edg ⁡ G → G ∈ UHGraph
6 uhgr0vb ⊢ G ∈ W ∧ Vtx ⁡ G = ∅ → G ∈ UHGraph ↔ iEdg ⁡ G = ∅
7 5 6 imbitrid ⊢ G ∈ W ∧ Vtx ⁡ G = ∅ → G ∈ USGraph ∧ ∀ k ∈ Vtx ⁡ G ∀ l ∈ Vtx ⁡ G ∖ k ∃! x ∈ Vtx ⁡ G x k x l ⊆ Edg ⁡ G → iEdg ⁡ G = ∅
8 simpll ⊢ G ∈ W ∧ Vtx ⁡ G = ∅ ∧ iEdg ⁡ G = ∅ → G ∈ W
9 simpr ⊢ G ∈ W ∧ Vtx ⁡ G = ∅ ∧ iEdg ⁡ G = ∅ → iEdg ⁡ G = ∅
10 8 9 usgr0e ⊢ G ∈ W ∧ Vtx ⁡ G = ∅ ∧ iEdg ⁡ G = ∅ → G ∈ USGraph
11 ral0 ⊢ ∀ k ∈ ∅ ∀ l ∈ Vtx ⁡ G ∖ k ∃! x ∈ Vtx ⁡ G x k x l ⊆ Edg ⁡ G
12 raleq ⊢ Vtx ⁡ G = ∅ → ∀ k ∈ Vtx ⁡ G ∀ l ∈ Vtx ⁡ G ∖ k ∃! x ∈ Vtx ⁡ G x k x l ⊆ Edg ⁡ G ↔ ∀ k ∈ ∅ ∀ l ∈ Vtx ⁡ G ∖ k ∃! x ∈ Vtx ⁡ G x k x l ⊆ Edg ⁡ G
13 12 adantl ⊢ G ∈ W ∧ Vtx ⁡ G = ∅ → ∀ k ∈ Vtx ⁡ G ∀ l ∈ Vtx ⁡ G ∖ k ∃! x ∈ Vtx ⁡ G x k x l ⊆ Edg ⁡ G ↔ ∀ k ∈ ∅ ∀ l ∈ Vtx ⁡ G ∖ k ∃! x ∈ Vtx ⁡ G x k x l ⊆ Edg ⁡ G
14 11 13 mpbiri ⊢ G ∈ W ∧ Vtx ⁡ G = ∅ → ∀ k ∈ Vtx ⁡ G ∀ l ∈ Vtx ⁡ G ∖ k ∃! x ∈ Vtx ⁡ G x k x l ⊆ Edg ⁡ G
15 14 adantr ⊢ G ∈ W ∧ Vtx ⁡ G = ∅ ∧ iEdg ⁡ G = ∅ → ∀ k ∈ Vtx ⁡ G ∀ l ∈ Vtx ⁡ G ∖ k ∃! x ∈ Vtx ⁡ G x k x l ⊆ Edg ⁡ G
16 10 15 jca ⊢ G ∈ W ∧ Vtx ⁡ G = ∅ ∧ iEdg ⁡ G = ∅ → G ∈ USGraph ∧ ∀ k ∈ Vtx ⁡ G ∀ l ∈ Vtx ⁡ G ∖ k ∃! x ∈ Vtx ⁡ G x k x l ⊆ Edg ⁡ G
17 16 ex ⊢ G ∈ W ∧ Vtx ⁡ G = ∅ → iEdg ⁡ G = ∅ → G ∈ USGraph ∧ ∀ k ∈ Vtx ⁡ G ∀ l ∈ Vtx ⁡ G ∖ k ∃! x ∈ Vtx ⁡ G x k x l ⊆ Edg ⁡ G
18 7 17 impbid ⊢ G ∈ W ∧ Vtx ⁡ G = ∅ → G ∈ USGraph ∧ ∀ k ∈ Vtx ⁡ G ∀ l ∈ Vtx ⁡ G ∖ k ∃! x ∈ Vtx ⁡ G x k x l ⊆ Edg ⁡ G ↔ iEdg ⁡ G = ∅
19 3 18 bitrid ⊢ G ∈ W ∧ Vtx ⁡ G = ∅ → G ∈ FriendGraph ↔ iEdg ⁡ G = ∅