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

Metamath Proof Explorer

Theorem usgredg2ALT

Description: Alternate proof of usgredg2 , not using umgredg2 . (Contributed by Alexander van der Vekens, 11-Aug-2017) (Revised by AV, 16-Oct-2020) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypothesis usgredg2.e ⊢ 𝐸 = ( iEdg ‘ 𝐺 )
Assertion usgredg2ALT ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ dom 𝐸 ) → ( ♯ ‘ ( 𝐸 ‘ 𝑋 ) ) = 2 )

Proof

Step Hyp Ref Expression
1 usgredg2.e ⊢ 𝐸 = ( iEdg ‘ 𝐺 )
2 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
3 2 1 usgrf ⊢ ( 𝐺 ∈ USGraph → 𝐸 : dom 𝐸 –1-1→ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } )
4 f1f ⊢ ( 𝐸 : dom 𝐸 –1-1→ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } → 𝐸 : dom 𝐸 ⟶ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } )
5 3 4 syl ⊢ ( 𝐺 ∈ USGraph → 𝐸 : dom 𝐸 ⟶ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } )
6 5 ffvelcdmda ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ dom 𝐸 ) → ( 𝐸 ‘ 𝑋 ) ∈ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } )
7 fveq2 ⊢ ( 𝑥 = ( 𝐸 ‘ 𝑋 ) → ( ♯ ‘ 𝑥 ) = ( ♯ ‘ ( 𝐸 ‘ 𝑋 ) ) )
8 7 eqeq1d ⊢ ( 𝑥 = ( 𝐸 ‘ 𝑋 ) → ( ( ♯ ‘ 𝑥 ) = 2 ↔ ( ♯ ‘ ( 𝐸 ‘ 𝑋 ) ) = 2 ) )
9 8 elrab ⊢ ( ( 𝐸 ‘ 𝑋 ) ∈ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ↔ ( ( 𝐸 ‘ 𝑋 ) ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∧ ( ♯ ‘ ( 𝐸 ‘ 𝑋 ) ) = 2 ) )
10 9 simprbi ⊢ ( ( 𝐸 ‘ 𝑋 ) ∈ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } → ( ♯ ‘ ( 𝐸 ‘ 𝑋 ) ) = 2 )
11 6 10 syl ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ dom 𝐸 ) → ( ♯ ‘ ( 𝐸 ‘ 𝑋 ) ) = 2 )