Metamath Proof Explorer

Theorem upgrop

Description: A pseudograph represented by an ordered pair. (Contributed by AV, 12-Dec-2021)

Ref Expression
Assertion upgrop ⊢ G ∈ UPGraph → Vtx ⁡ G iEdg ⁡ G ∈ UPGraph

Proof

Step Hyp Ref Expression
1 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
2 eqid ⊢ iEdg ⁡ G = iEdg ⁡ G
3 1 2 upgrf ⊢ G ∈ UPGraph → iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ p ∈ 𝒫 Vtx ⁡ G ∖ ∅ | p ≤ 2
4 fvex ⊢ Vtx ⁡ G ∈ V
5 fvex ⊢ iEdg ⁡ G ∈ V
6 4 5 pm3.2i ⊢ Vtx ⁡ G ∈ V ∧ iEdg ⁡ G ∈ V
7 opex ⊢ Vtx ⁡ G iEdg ⁡ G ∈ V
8 eqid ⊢ Vtx ⁡ Vtx ⁡ G iEdg ⁡ G = Vtx ⁡ Vtx ⁡ G iEdg ⁡ G
9 eqid ⊢ iEdg ⁡ Vtx ⁡ G iEdg ⁡ G = iEdg ⁡ Vtx ⁡ G iEdg ⁡ G
10 8 9 isupgr ⊢ Vtx ⁡ G iEdg ⁡ G ∈ V → Vtx ⁡ G iEdg ⁡ G ∈ UPGraph ↔ iEdg ⁡ Vtx ⁡ G iEdg ⁡ G : dom ⁡ iEdg ⁡ Vtx ⁡ G iEdg ⁡ G ⟶ p ∈ 𝒫 Vtx ⁡ Vtx ⁡ G iEdg ⁡ G ∖ ∅ | p ≤ 2
11 7 10 mp1i ⊢ Vtx ⁡ G ∈ V ∧ iEdg ⁡ G ∈ V → Vtx ⁡ G iEdg ⁡ G ∈ UPGraph ↔ iEdg ⁡ Vtx ⁡ G iEdg ⁡ G : dom ⁡ iEdg ⁡ Vtx ⁡ G iEdg ⁡ G ⟶ p ∈ 𝒫 Vtx ⁡ Vtx ⁡ G iEdg ⁡ G ∖ ∅ | p ≤ 2
12 opiedgfv ⊢ Vtx ⁡ G ∈ V ∧ iEdg ⁡ G ∈ V → iEdg ⁡ Vtx ⁡ G iEdg ⁡ G = iEdg ⁡ G
13 12 dmeqd ⊢ Vtx ⁡ G ∈ V ∧ iEdg ⁡ G ∈ V → dom ⁡ iEdg ⁡ Vtx ⁡ G iEdg ⁡ G = dom ⁡ iEdg ⁡ G
14 opvtxfv ⊢ Vtx ⁡ G ∈ V ∧ iEdg ⁡ G ∈ V → Vtx ⁡ Vtx ⁡ G iEdg ⁡ G = Vtx ⁡ G
15 14 pweqd ⊢ Vtx ⁡ G ∈ V ∧ iEdg ⁡ G ∈ V → 𝒫 Vtx ⁡ Vtx ⁡ G iEdg ⁡ G = 𝒫 Vtx ⁡ G
16 15 difeq1d ⊢ Vtx ⁡ G ∈ V ∧ iEdg ⁡ G ∈ V → 𝒫 Vtx ⁡ Vtx ⁡ G iEdg ⁡ G ∖ ∅ = 𝒫 Vtx ⁡ G ∖ ∅
17 16 rabeqdv ⊢ Vtx ⁡ G ∈ V ∧ iEdg ⁡ G ∈ V → p ∈ 𝒫 Vtx ⁡ Vtx ⁡ G iEdg ⁡ G ∖ ∅ | p ≤ 2 = p ∈ 𝒫 Vtx ⁡ G ∖ ∅ | p ≤ 2
18 12 13 17 feq123d ⊢ Vtx ⁡ G ∈ V ∧ iEdg ⁡ G ∈ V → iEdg ⁡ Vtx ⁡ G iEdg ⁡ G : dom ⁡ iEdg ⁡ Vtx ⁡ G iEdg ⁡ G ⟶ p ∈ 𝒫 Vtx ⁡ Vtx ⁡ G iEdg ⁡ G ∖ ∅ | p ≤ 2 ↔ iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ p ∈ 𝒫 Vtx ⁡ G ∖ ∅ | p ≤ 2
19 11 18 bitrd ⊢ Vtx ⁡ G ∈ V ∧ iEdg ⁡ G ∈ V → Vtx ⁡ G iEdg ⁡ G ∈ UPGraph ↔ iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ p ∈ 𝒫 Vtx ⁡ G ∖ ∅ | p ≤ 2
20 6 19 mp1i ⊢ G ∈ UPGraph → Vtx ⁡ G iEdg ⁡ G ∈ UPGraph ↔ iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ p ∈ 𝒫 Vtx ⁡ G ∖ ∅ | p ≤ 2
21 3 20 mpbird ⊢ G ∈ UPGraph → Vtx ⁡ G iEdg ⁡ G ∈ UPGraph