Metamath Proof Explorer


Theorem wrdumgr

Description: The property of being an undirected multigraph, expressing the edges as "words". (Contributed by AV, 24-Nov-2020)

Ref Expression
Hypotheses isumgr.v 𝑉 = ( Vtx ‘ 𝐺 )
isumgr.e 𝐸 = ( iEdg ‘ 𝐺 )
Assertion wrdumgr ( ( 𝐺𝑈𝐸 ∈ Word 𝑋 ) → ( 𝐺 ∈ UMGraph ↔ 𝐸 ∈ Word { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } ) )

Proof

Step Hyp Ref Expression
1 isumgr.v 𝑉 = ( Vtx ‘ 𝐺 )
2 isumgr.e 𝐸 = ( iEdg ‘ 𝐺 )
3 1 2 isumgrs ( 𝐺𝑈 → ( 𝐺 ∈ UMGraph ↔ 𝐸 : dom 𝐸 ⟶ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } ) )
4 3 adantr ( ( 𝐺𝑈𝐸 ∈ Word 𝑋 ) → ( 𝐺 ∈ UMGraph ↔ 𝐸 : dom 𝐸 ⟶ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } ) )
5 wrdf ( 𝐸 ∈ Word 𝑋𝐸 : ( 0 ..^ ( ♯ ‘ 𝐸 ) ) ⟶ 𝑋 )
6 5 adantl ( ( 𝐺𝑈𝐸 ∈ Word 𝑋 ) → 𝐸 : ( 0 ..^ ( ♯ ‘ 𝐸 ) ) ⟶ 𝑋 )
7 6 fdmd ( ( 𝐺𝑈𝐸 ∈ Word 𝑋 ) → dom 𝐸 = ( 0 ..^ ( ♯ ‘ 𝐸 ) ) )
8 7 feq2d ( ( 𝐺𝑈𝐸 ∈ Word 𝑋 ) → ( 𝐸 : dom 𝐸 ⟶ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } ↔ 𝐸 : ( 0 ..^ ( ♯ ‘ 𝐸 ) ) ⟶ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } ) )
9 iswrdi ( 𝐸 : ( 0 ..^ ( ♯ ‘ 𝐸 ) ) ⟶ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } → 𝐸 ∈ Word { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } )
10 wrdf ( 𝐸 ∈ Word { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } → 𝐸 : ( 0 ..^ ( ♯ ‘ 𝐸 ) ) ⟶ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } )
11 9 10 impbii ( 𝐸 : ( 0 ..^ ( ♯ ‘ 𝐸 ) ) ⟶ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } ↔ 𝐸 ∈ Word { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } )
12 8 11 bitrdi ( ( 𝐺𝑈𝐸 ∈ Word 𝑋 ) → ( 𝐸 : dom 𝐸 ⟶ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } ↔ 𝐸 ∈ Word { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } ) )
13 4 12 bitrd ( ( 𝐺𝑈𝐸 ∈ Word 𝑋 ) → ( 𝐺 ∈ UMGraph ↔ 𝐸 ∈ Word { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } ) )