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	|- E = ( iEdg ` G )
Assertion	usgredg2ALT	|- ( ( G e. USGraph /\ X e. dom E ) -> ( # ` ( E ` X ) ) = 2 )

Proof

Step	Hyp	Ref	Expression
1		usgredg2.e	|- E = ( iEdg ` G )
2		eqid	|- ( Vtx ` G ) = ( Vtx ` G )
3	2 1	usgrf	|- ( G e. USGraph -> E : dom E -1-1-> { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) = 2 } )
4		f1f	|- ( E : dom E -1-1-> { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) = 2 } -> E : dom E --> { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) = 2 } )
5	3 4	syl	|- ( G e. USGraph -> E : dom E --> { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) = 2 } )
6	5	ffvelrnda	|- ( ( G e. USGraph /\ X e. dom E ) -> ( E ` X ) e. { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) = 2 } )
7		fveq2	|- ( x = ( E ` X ) -> ( # ` x ) = ( # ` ( E ` X ) ) )
8	7	eqeq1d	|- ( x = ( E ` X ) -> ( ( # ` x ) = 2 <-> ( # ` ( E ` X ) ) = 2 ) )
9	8	elrab	|- ( ( E ` X ) e. { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) = 2 } <-> ( ( E ` X ) e. ( ~P ( Vtx ` G ) \ { (/) } ) /\ ( # ` ( E ` X ) ) = 2 ) )
10	9	simprbi	|- ( ( E ` X ) e. { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) = 2 } -> ( # ` ( E ` X ) ) = 2 )
11	6 10	syl	|- ( ( G e. USGraph /\ X e. dom E ) -> ( # ` ( E ` X ) ) = 2 )