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

Metamath Proof Explorer

Theorem wrdupgr

Description: The property of being an undirected pseudograph, expressing the edges as "words". (Contributed by Mario Carneiro, 11-Mar-2015) (Revised by AV, 10-Oct-2020)

Ref Expression
Hypotheses isupgr.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
isupgr.e ⊢ 𝐸 = ( iEdg ‘ 𝐺 )
Assertion wrdupgr ( ( 𝐺 ∈ 𝑈 ∧ 𝐸 ∈ Word 𝑋 ) → ( 𝐺 ∈ UPGraph ↔ 𝐸 ∈ Word { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } ) )

Proof

Step Hyp Ref Expression
1 isupgr.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 isupgr.e ⊢ 𝐸 = ( iEdg ‘ 𝐺 )
3 1 2 isupgr ⊢ ( 𝐺 ∈ 𝑈 → ( 𝐺 ∈ UPGraph ↔ 𝐸 : dom 𝐸 ⟶ { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } ) )
4 3 adantr ⊢ ( ( 𝐺 ∈ 𝑈 ∧ 𝐸 ∈ Word 𝑋 ) → ( 𝐺 ∈ UPGraph ↔ 𝐸 : 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 𝑋 ) → ( 𝐺 ∈ UPGraph ↔ 𝐸 ∈ Word { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } ) )