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	ffvelrnda	⊢ ( ( 𝐺 ∈ 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 )