Metamath Proof Explorer

Theorem isumgr

Description: The property of being an undirected multigraph. (Contributed by AV, 24-Nov-2020)

Ref Expression
Hypotheses isumgr.v ⊢ V = Vtx ⁡ G
isumgr.e ⊢ E = iEdg ⁡ G
Assertion isumgr ⊢ G ∈ U → G ∈ UMGraph ↔ E : dom ⁡ E ⟶ x ∈ 𝒫 V ∖ ∅ | x = 2

Proof

Step Hyp Ref Expression
1 isumgr.v ⊢ V = Vtx ⁡ G
2 isumgr.e ⊢ E = iEdg ⁡ G
3 df-umgr ⊢ UMGraph = g | [˙ Vtx ⁡ g / v]˙ [˙ iEdg ⁡ g / e]˙ e : dom ⁡ e ⟶ x ∈ 𝒫 v ∖ ∅ | x = 2
4 3 eleq2i ⊢ G ∈ UMGraph ↔ G ∈ g | [˙ Vtx ⁡ g / v]˙ [˙ iEdg ⁡ g / e]˙ e : dom ⁡ e ⟶ x ∈ 𝒫 v ∖ ∅ | x = 2
5 fveq2 ⊢ h = G → iEdg ⁡ h = iEdg ⁡ G
6 5 2 eqtr4di ⊢ h = G → iEdg ⁡ h = E
7 5 dmeqd ⊢ h = G → dom ⁡ iEdg ⁡ h = dom ⁡ iEdg ⁡ G
8 2 eqcomi ⊢ iEdg ⁡ G = E
9 8 dmeqi ⊢ dom ⁡ iEdg ⁡ G = dom ⁡ E
10 7 9 eqtrdi ⊢ h = G → dom ⁡ iEdg ⁡ h = dom ⁡ E
11 fveq2 ⊢ h = G → Vtx ⁡ h = Vtx ⁡ G
12 11 1 eqtr4di ⊢ h = G → Vtx ⁡ h = V
13 12 pweqd ⊢ h = G → 𝒫 Vtx ⁡ h = 𝒫 V
14 13 difeq1d ⊢ h = G → 𝒫 Vtx ⁡ h ∖ ∅ = 𝒫 V ∖ ∅
15 14 rabeqdv ⊢ h = G → x ∈ 𝒫 Vtx ⁡ h ∖ ∅ | x = 2 = x ∈ 𝒫 V ∖ ∅ | x = 2
16 6 10 15 feq123d ⊢ h = G → iEdg ⁡ h : dom ⁡ iEdg ⁡ h ⟶ x ∈ 𝒫 Vtx ⁡ h ∖ ∅ | x = 2 ↔ E : dom ⁡ E ⟶ x ∈ 𝒫 V ∖ ∅ | x = 2
17 fvexd ⊢ g = h → Vtx ⁡ g ∈ V
18 fveq2 ⊢ g = h → Vtx ⁡ g = Vtx ⁡ h
19 fvexd ⊢ g = h ∧ v = Vtx ⁡ h → iEdg ⁡ g ∈ V
20 fveq2 ⊢ g = h → iEdg ⁡ g = iEdg ⁡ h
21 20 adantr ⊢ g = h ∧ v = Vtx ⁡ h → iEdg ⁡ g = iEdg ⁡ h
22 simpr ⊢ g = h ∧ v = Vtx ⁡ h ∧ e = iEdg ⁡ h → e = iEdg ⁡ h
23 22 dmeqd ⊢ g = h ∧ v = Vtx ⁡ h ∧ e = iEdg ⁡ h → dom ⁡ e = dom ⁡ iEdg ⁡ h
24 pweq ⊢ v = Vtx ⁡ h → 𝒫 v = 𝒫 Vtx ⁡ h
25 24 ad2antlr ⊢ g = h ∧ v = Vtx ⁡ h ∧ e = iEdg ⁡ h → 𝒫 v = 𝒫 Vtx ⁡ h
26 25 difeq1d ⊢ g = h ∧ v = Vtx ⁡ h ∧ e = iEdg ⁡ h → 𝒫 v ∖ ∅ = 𝒫 Vtx ⁡ h ∖ ∅
27 26 rabeqdv ⊢ g = h ∧ v = Vtx ⁡ h ∧ e = iEdg ⁡ h → x ∈ 𝒫 v ∖ ∅ | x = 2 = x ∈ 𝒫 Vtx ⁡ h ∖ ∅ | x = 2
28 22 23 27 feq123d ⊢ g = h ∧ v = Vtx ⁡ h ∧ e = iEdg ⁡ h → e : dom ⁡ e ⟶ x ∈ 𝒫 v ∖ ∅ | x = 2 ↔ iEdg ⁡ h : dom ⁡ iEdg ⁡ h ⟶ x ∈ 𝒫 Vtx ⁡ h ∖ ∅ | x = 2
29 19 21 28 sbcied2 ⊢ g = h ∧ v = Vtx ⁡ h → [˙ iEdg ⁡ g / e]˙ e : dom ⁡ e ⟶ x ∈ 𝒫 v ∖ ∅ | x = 2 ↔ iEdg ⁡ h : dom ⁡ iEdg ⁡ h ⟶ x ∈ 𝒫 Vtx ⁡ h ∖ ∅ | x = 2
30 17 18 29 sbcied2 ⊢ g = h → [˙ Vtx ⁡ g / v]˙ [˙ iEdg ⁡ g / e]˙ e : dom ⁡ e ⟶ x ∈ 𝒫 v ∖ ∅ | x = 2 ↔ iEdg ⁡ h : dom ⁡ iEdg ⁡ h ⟶ x ∈ 𝒫 Vtx ⁡ h ∖ ∅ | x = 2
31 30 cbvabv ⊢ g | [˙ Vtx ⁡ g / v]˙ [˙ iEdg ⁡ g / e]˙ e : dom ⁡ e ⟶ x ∈ 𝒫 v ∖ ∅ | x = 2 = h | iEdg ⁡ h : dom ⁡ iEdg ⁡ h ⟶ x ∈ 𝒫 Vtx ⁡ h ∖ ∅ | x = 2
32 16 31 elab2g ⊢ G ∈ U → G ∈ g | [˙ Vtx ⁡ g / v]˙ [˙ iEdg ⁡ g / e]˙ e : dom ⁡ e ⟶ x ∈ 𝒫 v ∖ ∅ | x = 2 ↔ E : dom ⁡ E ⟶ x ∈ 𝒫 V ∖ ∅ | x = 2
33 4 32 syl5bb ⊢ G ∈ U → G ∈ UMGraph ↔ E : dom ⁡ E ⟶ x ∈ 𝒫 V ∖ ∅ | x = 2