Metamath Proof Explorer

Theorem isfrgr

Description: The property of being a friendship graph. (Contributed by Alexander van der Vekens, 4-Oct-2017) (Revised by AV, 29-Mar-2021) (Revised by AV, 3-Jan-2024)

Ref Expression
Hypotheses isfrgr.v ⊢ V = Vtx ⁡ G
isfrgr.e ⊢ E = Edg ⁡ G
Assertion isfrgr ⊢ G ∈ FriendGraph ↔ G ∈ USGraph ∧ ∀ k ∈ V ∀ l ∈ V ∖ k ∃! x ∈ V x k x l ⊆ E

Proof

Step Hyp Ref Expression
1 isfrgr.v ⊢ V = Vtx ⁡ G
2 isfrgr.e ⊢ E = Edg ⁡ G
3 fvex ⊢ Vtx ⁡ g ∈ V
4 fvex ⊢ Edg ⁡ g ∈ V
5 fveq2 ⊢ g = G → Vtx ⁡ g = Vtx ⁡ G
6 5 eqeq2d ⊢ g = G → v = Vtx ⁡ g ↔ v = Vtx ⁡ G
7 1 eqcomi ⊢ Vtx ⁡ G = V
8 7 eqeq2i ⊢ v = Vtx ⁡ G ↔ v = V
9 6 8 bitrdi ⊢ g = G → v = Vtx ⁡ g ↔ v = V
10 fveq2 ⊢ g = G → Edg ⁡ g = Edg ⁡ G
11 10 eqeq2d ⊢ g = G → e = Edg ⁡ g ↔ e = Edg ⁡ G
12 2 eqcomi ⊢ Edg ⁡ G = E
13 12 eqeq2i ⊢ e = Edg ⁡ G ↔ e = E
14 11 13 bitrdi ⊢ g = G → e = Edg ⁡ g ↔ e = E
15 9 14 anbi12d ⊢ g = G → v = Vtx ⁡ g ∧ e = Edg ⁡ g ↔ v = V ∧ e = E
16 simpl ⊢ v = V ∧ e = E → v = V
17 difeq1 ⊢ v = V → v ∖ k = V ∖ k
18 17 adantr ⊢ v = V ∧ e = E → v ∖ k = V ∖ k
19 reueq1 ⊢ v = V → ∃! x ∈ v x k x l ⊆ e ↔ ∃! x ∈ V x k x l ⊆ e
20 19 adantr ⊢ v = V ∧ e = E → ∃! x ∈ v x k x l ⊆ e ↔ ∃! x ∈ V x k x l ⊆ e
21 sseq2 ⊢ e = E → x k x l ⊆ e ↔ x k x l ⊆ E
22 21 adantl ⊢ v = V ∧ e = E → x k x l ⊆ e ↔ x k x l ⊆ E
23 22 reubidv ⊢ v = V ∧ e = E → ∃! x ∈ V x k x l ⊆ e ↔ ∃! x ∈ V x k x l ⊆ E
24 20 23 bitrd ⊢ v = V ∧ e = E → ∃! x ∈ v x k x l ⊆ e ↔ ∃! x ∈ V x k x l ⊆ E
25 18 24 raleqbidv ⊢ v = V ∧ e = E → ∀ l ∈ v ∖ k ∃! x ∈ v x k x l ⊆ e ↔ ∀ l ∈ V ∖ k ∃! x ∈ V x k x l ⊆ E
26 16 25 raleqbidv ⊢ v = V ∧ e = E → ∀ k ∈ v ∀ l ∈ v ∖ k ∃! x ∈ v x k x l ⊆ e ↔ ∀ k ∈ V ∀ l ∈ V ∖ k ∃! x ∈ V x k x l ⊆ E
27 15 26 biimtrdi ⊢ g = G → v = Vtx ⁡ g ∧ e = Edg ⁡ g → ∀ k ∈ v ∀ l ∈ v ∖ k ∃! x ∈ v x k x l ⊆ e ↔ ∀ k ∈ V ∀ l ∈ V ∖ k ∃! x ∈ V x k x l ⊆ E
28 3 4 27 sbc2iedv ⊢ g = G → [˙ Vtx ⁡ g / v]˙ [˙ Edg ⁡ g / e]˙ ∀ k ∈ v ∀ l ∈ v ∖ k ∃! x ∈ v x k x l ⊆ e ↔ ∀ k ∈ V ∀ l ∈ V ∖ k ∃! x ∈ V x k x l ⊆ E
29 df-frgr ⊢ FriendGraph = g ∈ USGraph | [˙ Vtx ⁡ g / v]˙ [˙ Edg ⁡ g / e]˙ ∀ k ∈ v ∀ l ∈ v ∖ k ∃! x ∈ v x k x l ⊆ e
30 28 29 elrab2 ⊢ G ∈ FriendGraph ↔ G ∈ USGraph ∧ ∀ k ∈ V ∀ l ∈ V ∖ k ∃! x ∈ V x k x l ⊆ E