This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem upgrop

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

Ref Expression
Assertion upgrop ( 𝐺 ∈ UPGraph → ⟨ ( Vtx ‘ 𝐺 ) , ( iEdg ‘ 𝐺 ) ⟩ ∈ UPGraph )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
2 eqid ⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 )
3 1 2 upgrf ⊢ ( 𝐺 ∈ UPGraph → ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ { 𝑝 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑝 ) ≤ 2 } )
4 fvex ⊢ ( Vtx ‘ 𝐺 ) ∈ V
5 fvex ⊢ ( iEdg ‘ 𝐺 ) ∈ V
6 4 5 pm3.2i ⊢ ( ( Vtx ‘ 𝐺 ) ∈ V ∧ ( iEdg ‘ 𝐺 ) ∈ V )
7 opex ⊢ ⟨ ( Vtx ‘ 𝐺 ) , ( iEdg ‘ 𝐺 ) ⟩ ∈ V
8 eqid ⊢ ( Vtx ‘ ⟨ ( Vtx ‘ 𝐺 ) , ( iEdg ‘ 𝐺 ) ⟩ ) = ( Vtx ‘ ⟨ ( Vtx ‘ 𝐺 ) , ( iEdg ‘ 𝐺 ) ⟩ )
9 eqid ⊢ ( iEdg ‘ ⟨ ( Vtx ‘ 𝐺 ) , ( iEdg ‘ 𝐺 ) ⟩ ) = ( iEdg ‘ ⟨ ( Vtx ‘ 𝐺 ) , ( iEdg ‘ 𝐺 ) ⟩ )
10 8 9 isupgr ⊢ ( ⟨ ( Vtx ‘ 𝐺 ) , ( iEdg ‘ 𝐺 ) ⟩ ∈ V → ( ⟨ ( Vtx ‘ 𝐺 ) , ( iEdg ‘ 𝐺 ) ⟩ ∈ UPGraph ↔ ( iEdg ‘ ⟨ ( Vtx ‘ 𝐺 ) , ( iEdg ‘ 𝐺 ) ⟩ ) : dom ( iEdg ‘ ⟨ ( Vtx ‘ 𝐺 ) , ( iEdg ‘ 𝐺 ) ⟩ ) ⟶ { 𝑝 ∈ ( 𝒫 ( Vtx ‘ ⟨ ( Vtx ‘ 𝐺 ) , ( iEdg ‘ 𝐺 ) ⟩ ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑝 ) ≤ 2 } ) )
11 7 10 mp1i ⊢ ( ( ( Vtx ‘ 𝐺 ) ∈ V ∧ ( iEdg ‘ 𝐺 ) ∈ V ) → ( ⟨ ( Vtx ‘ 𝐺 ) , ( iEdg ‘ 𝐺 ) ⟩ ∈ UPGraph ↔ ( iEdg ‘ ⟨ ( Vtx ‘ 𝐺 ) , ( iEdg ‘ 𝐺 ) ⟩ ) : dom ( iEdg ‘ ⟨ ( Vtx ‘ 𝐺 ) , ( iEdg ‘ 𝐺 ) ⟩ ) ⟶ { 𝑝 ∈ ( 𝒫 ( Vtx ‘ ⟨ ( Vtx ‘ 𝐺 ) , ( iEdg ‘ 𝐺 ) ⟩ ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑝 ) ≤ 2 } ) )
12 opiedgfv ⊢ ( ( ( Vtx ‘ 𝐺 ) ∈ V ∧ ( iEdg ‘ 𝐺 ) ∈ V ) → ( iEdg ‘ ⟨ ( Vtx ‘ 𝐺 ) , ( iEdg ‘ 𝐺 ) ⟩ ) = ( iEdg ‘ 𝐺 ) )
13 12 dmeqd ⊢ ( ( ( Vtx ‘ 𝐺 ) ∈ V ∧ ( iEdg ‘ 𝐺 ) ∈ V ) → dom ( iEdg ‘ ⟨ ( Vtx ‘ 𝐺 ) , ( iEdg ‘ 𝐺 ) ⟩ ) = dom ( iEdg ‘ 𝐺 ) )
14 opvtxfv ⊢ ( ( ( Vtx ‘ 𝐺 ) ∈ V ∧ ( iEdg ‘ 𝐺 ) ∈ V ) → ( Vtx ‘ ⟨ ( Vtx ‘ 𝐺 ) , ( iEdg ‘ 𝐺 ) ⟩ ) = ( Vtx ‘ 𝐺 ) )
15 14 pweqd ⊢ ( ( ( Vtx ‘ 𝐺 ) ∈ V ∧ ( iEdg ‘ 𝐺 ) ∈ V ) → 𝒫 ( Vtx ‘ ⟨ ( Vtx ‘ 𝐺 ) , ( iEdg ‘ 𝐺 ) ⟩ ) = 𝒫 ( Vtx ‘ 𝐺 ) )
16 15 difeq1d ⊢ ( ( ( Vtx ‘ 𝐺 ) ∈ V ∧ ( iEdg ‘ 𝐺 ) ∈ V ) → ( 𝒫 ( Vtx ‘ ⟨ ( Vtx ‘ 𝐺 ) , ( iEdg ‘ 𝐺 ) ⟩ ) ∖ { ∅ } ) = ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) )
17 16 rabeqdv ⊢ ( ( ( Vtx ‘ 𝐺 ) ∈ V ∧ ( iEdg ‘ 𝐺 ) ∈ V ) → { 𝑝 ∈ ( 𝒫 ( Vtx ‘ ⟨ ( Vtx ‘ 𝐺 ) , ( iEdg ‘ 𝐺 ) ⟩ ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑝 ) ≤ 2 } = { 𝑝 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑝 ) ≤ 2 } )
18 12 13 17 feq123d ⊢ ( ( ( Vtx ‘ 𝐺 ) ∈ V ∧ ( iEdg ‘ 𝐺 ) ∈ V ) → ( ( iEdg ‘ ⟨ ( Vtx ‘ 𝐺 ) , ( iEdg ‘ 𝐺 ) ⟩ ) : dom ( iEdg ‘ ⟨ ( Vtx ‘ 𝐺 ) , ( iEdg ‘ 𝐺 ) ⟩ ) ⟶ { 𝑝 ∈ ( 𝒫 ( Vtx ‘ ⟨ ( Vtx ‘ 𝐺 ) , ( iEdg ‘ 𝐺 ) ⟩ ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑝 ) ≤ 2 } ↔ ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ { 𝑝 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑝 ) ≤ 2 } ) )
19 11 18 bitrd ⊢ ( ( ( Vtx ‘ 𝐺 ) ∈ V ∧ ( iEdg ‘ 𝐺 ) ∈ V ) → ( ⟨ ( Vtx ‘ 𝐺 ) , ( iEdg ‘ 𝐺 ) ⟩ ∈ UPGraph ↔ ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ { 𝑝 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑝 ) ≤ 2 } ) )
20 6 19 mp1i ⊢ ( 𝐺 ∈ UPGraph → ( ⟨ ( Vtx ‘ 𝐺 ) , ( iEdg ‘ 𝐺 ) ⟩ ∈ UPGraph ↔ ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ { 𝑝 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑝 ) ≤ 2 } ) )
21 3 20 mpbird ⊢ ( 𝐺 ∈ UPGraph → ⟨ ( Vtx ‘ 𝐺 ) , ( iEdg ‘ 𝐺 ) ⟩ ∈ UPGraph )