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∈Vxkxl⊆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∈vxkxl⊆e↔∃!x∈Vxkxl⊆e
20 19 adantr ⊢v=V∧e=E→∃!x∈vxkxl⊆e↔∃!x∈Vxkxl⊆e
21 sseq2 ⊢e=E→xkxl⊆e↔xkxl⊆E
22 21 adantl ⊢v=V∧e=E→xkxl⊆e↔xkxl⊆E
23 22 reubidv ⊢v=V∧e=E→∃!x∈Vxkxl⊆e↔∃!x∈Vxkxl⊆E
24 20 23 bitrd ⊢v=V∧e=E→∃!x∈vxkxl⊆e↔∃!x∈Vxkxl⊆E
25 18 24 raleqbidv ⊢v=V∧e=E→∀l∈v∖k∃!x∈vxkxl⊆e↔∀l∈V∖k∃!x∈Vxkxl⊆E
26 16 25 raleqbidv ⊢v=V∧e=E→∀k∈v∀l∈v∖k∃!x∈vxkxl⊆e↔∀k∈V∀l∈V∖k∃!x∈Vxkxl⊆E
27 15 26 syl6bi ⊢g=G→v=Vtx⁡g∧e=Edg⁡g→∀k∈v∀l∈v∖k∃!x∈vxkxl⊆e↔∀k∈V∀l∈V∖k∃!x∈Vxkxl⊆E
28 3 4 27 sbc2iedv ⊢g=G→[˙Vtx⁡g/v]˙[˙Edg⁡g/e]˙∀k∈v∀l∈v∖k∃!x∈vxkxl⊆e↔∀k∈V∀l∈V∖k∃!x∈Vxkxl⊆E
29 df-frgr ⊢FriendGraph=g∈USGraph|[˙Vtx⁡g/v]˙[˙Edg⁡g/e]˙∀k∈v∀l∈v∖k∃!x∈vxkxl⊆e
30 28 29 elrab2 ⊢G∈FriendGraph↔G∈USGraph∧∀k∈V∀l∈V∖k∃!x∈Vxkxl⊆E