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

Metamath Proof Explorer

Theorem isumgr

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

Ref Expression
Hypotheses isumgr.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
isumgr.e ⊢ 𝐸 = ( iEdg ‘ 𝐺 )
Assertion isumgr ( 𝐺 ∈ 𝑈 → ( 𝐺 ∈ UMGraph ↔ 𝐸 : dom 𝐸 ⟶ { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ) )

Proof

Step Hyp Ref Expression
1 isumgr.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 isumgr.e ⊢ 𝐸 = ( iEdg ‘ 𝐺 )
3 df-umgr ⊢ UMGraph = { 𝑔 ∣ [ ( Vtx ‘ 𝑔 ) / 𝑣 ] [ ( iEdg ‘ 𝑔 ) / 𝑒 ] 𝑒 : dom 𝑒 ⟶ { 𝑥 ∈ ( 𝒫 𝑣 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } }
4 3 eleq2i ⊢ ( 𝐺 ∈ UMGraph ↔ 𝐺 ∈ { 𝑔 ∣ [ ( Vtx ‘ 𝑔 ) / 𝑣 ] [ ( iEdg ‘ 𝑔 ) / 𝑒 ] 𝑒 : dom 𝑒 ⟶ { 𝑥 ∈ ( 𝒫 𝑣 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } } )
5 fveq2 ⊢ ( ℎ = 𝐺 → ( iEdg ‘ ℎ ) = ( iEdg ‘ 𝐺 ) )
6 5 2 eqtr4di ⊢ ( ℎ = 𝐺 → ( iEdg ‘ ℎ ) = 𝐸 )
7 5 dmeqd ⊢ ( ℎ = 𝐺 → dom ( iEdg ‘ ℎ ) = dom ( iEdg ‘ 𝐺 ) )
8 2 eqcomi ⊢ ( iEdg ‘ 𝐺 ) = 𝐸
9 8 dmeqi ⊢ dom ( iEdg ‘ 𝐺 ) = dom 𝐸
10 7 9 eqtrdi ⊢ ( ℎ = 𝐺 → dom ( iEdg ‘ ℎ ) = dom 𝐸 )
11 fveq2 ⊢ ( ℎ = 𝐺 → ( Vtx ‘ ℎ ) = ( Vtx ‘ 𝐺 ) )
12 11 1 eqtr4di ⊢ ( ℎ = 𝐺 → ( Vtx ‘ ℎ ) = 𝑉 )
13 12 pweqd ⊢ ( ℎ = 𝐺 → 𝒫 ( Vtx ‘ ℎ ) = 𝒫 𝑉 )
14 13 difeq1d ⊢ ( ℎ = 𝐺 → ( 𝒫 ( Vtx ‘ ℎ ) ∖ { ∅ } ) = ( 𝒫 𝑉 ∖ { ∅ } ) )
15 14 rabeqdv ⊢ ( ℎ = 𝐺 → { 𝑥 ∈ ( 𝒫 ( Vtx ‘ ℎ ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } = { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } )
16 6 10 15 feq123d ⊢ ( ℎ = 𝐺 → ( ( iEdg ‘ ℎ ) : dom ( iEdg ‘ ℎ ) ⟶ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ ℎ ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ↔ 𝐸 : dom 𝐸 ⟶ { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ) )
17 fvexd ⊢ ( 𝑔 = ℎ → ( Vtx ‘ 𝑔 ) ∈ V )
18 fveq2 ⊢ ( 𝑔 = ℎ → ( Vtx ‘ 𝑔 ) = ( Vtx ‘ ℎ ) )
19 fvexd ⊢ ( ( 𝑔 = ℎ ∧ 𝑣 = ( Vtx ‘ ℎ ) ) → ( iEdg ‘ 𝑔 ) ∈ V )
20 fveq2 ⊢ ( 𝑔 = ℎ → ( iEdg ‘ 𝑔 ) = ( iEdg ‘ ℎ ) )
21 20 adantr ⊢ ( ( 𝑔 = ℎ ∧ 𝑣 = ( Vtx ‘ ℎ ) ) → ( iEdg ‘ 𝑔 ) = ( iEdg ‘ ℎ ) )
22 simpr ⊢ ( ( ( 𝑔 = ℎ ∧ 𝑣 = ( Vtx ‘ ℎ ) ) ∧ 𝑒 = ( iEdg ‘ ℎ ) ) → 𝑒 = ( iEdg ‘ ℎ ) )
23 22 dmeqd ⊢ ( ( ( 𝑔 = ℎ ∧ 𝑣 = ( Vtx ‘ ℎ ) ) ∧ 𝑒 = ( iEdg ‘ ℎ ) ) → dom 𝑒 = dom ( iEdg ‘ ℎ ) )
24 pweq ⊢ ( 𝑣 = ( Vtx ‘ ℎ ) → 𝒫 𝑣 = 𝒫 ( Vtx ‘ ℎ ) )
25 24 ad2antlr ⊢ ( ( ( 𝑔 = ℎ ∧ 𝑣 = ( Vtx ‘ ℎ ) ) ∧ 𝑒 = ( iEdg ‘ ℎ ) ) → 𝒫 𝑣 = 𝒫 ( Vtx ‘ ℎ ) )
26 25 difeq1d ⊢ ( ( ( 𝑔 = ℎ ∧ 𝑣 = ( Vtx ‘ ℎ ) ) ∧ 𝑒 = ( iEdg ‘ ℎ ) ) → ( 𝒫 𝑣 ∖ { ∅ } ) = ( 𝒫 ( Vtx ‘ ℎ ) ∖ { ∅ } ) )
27 26 rabeqdv ⊢ ( ( ( 𝑔 = ℎ ∧ 𝑣 = ( Vtx ‘ ℎ ) ) ∧ 𝑒 = ( iEdg ‘ ℎ ) ) → { 𝑥 ∈ ( 𝒫 𝑣 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } = { 𝑥 ∈ ( 𝒫 ( Vtx ‘ ℎ ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } )
28 22 23 27 feq123d ⊢ ( ( ( 𝑔 = ℎ ∧ 𝑣 = ( Vtx ‘ ℎ ) ) ∧ 𝑒 = ( iEdg ‘ ℎ ) ) → ( 𝑒 : dom 𝑒 ⟶ { 𝑥 ∈ ( 𝒫 𝑣 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ↔ ( iEdg ‘ ℎ ) : dom ( iEdg ‘ ℎ ) ⟶ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ ℎ ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ) )
29 19 21 28 sbcied2 ⊢ ( ( 𝑔 = ℎ ∧ 𝑣 = ( Vtx ‘ ℎ ) ) → ( [ ( iEdg ‘ 𝑔 ) / 𝑒 ] 𝑒 : dom 𝑒 ⟶ { 𝑥 ∈ ( 𝒫 𝑣 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ↔ ( iEdg ‘ ℎ ) : dom ( iEdg ‘ ℎ ) ⟶ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ ℎ ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ) )
30 17 18 29 sbcied2 ⊢ ( 𝑔 = ℎ → ( [ ( Vtx ‘ 𝑔 ) / 𝑣 ] [ ( iEdg ‘ 𝑔 ) / 𝑒 ] 𝑒 : dom 𝑒 ⟶ { 𝑥 ∈ ( 𝒫 𝑣 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ↔ ( iEdg ‘ ℎ ) : dom ( iEdg ‘ ℎ ) ⟶ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ ℎ ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ) )
31 30 cbvabv ⊢ { 𝑔 ∣ [ ( Vtx ‘ 𝑔 ) / 𝑣 ] [ ( iEdg ‘ 𝑔 ) / 𝑒 ] 𝑒 : dom 𝑒 ⟶ { 𝑥 ∈ ( 𝒫 𝑣 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } } = { ℎ ∣ ( iEdg ‘ ℎ ) : dom ( iEdg ‘ ℎ ) ⟶ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ ℎ ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } }
32 16 31 elab2g ⊢ ( 𝐺 ∈ 𝑈 → ( 𝐺 ∈ { 𝑔 ∣ [ ( Vtx ‘ 𝑔 ) / 𝑣 ] [ ( iEdg ‘ 𝑔 ) / 𝑒 ] 𝑒 : dom 𝑒 ⟶ { 𝑥 ∈ ( 𝒫 𝑣 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } } ↔ 𝐸 : dom 𝐸 ⟶ { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ) )
33 4 32 bitrid ⊢ ( 𝐺 ∈ 𝑈 → ( 𝐺 ∈ UMGraph ↔ 𝐸 : dom 𝐸 ⟶ { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ) )