Theorem usgredgprvALT

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

	Ref	Expression
Hypotheses	usgredg2.e	|- E = ( iEdg ` G )
	usgredgprv.v	|- V = ( Vtx ` G )
Assertion	usgredgprvALT	|- ( ( G e. USGraph /\ X e. dom E ) -> ( ( E ` X ) = { M , N } -> ( M e. V /\ N e. V ) ) )

Proof

Step	Hyp	Ref	Expression
1		usgredg2.e	|- E = ( iEdg ` G )
2		usgredgprv.v	|- V = ( Vtx ` G )
3	1 2	usgrss	|- ( ( G e. USGraph /\ X e. dom E ) -> ( E ` X ) C_ V )
4	1	usgredg2	|- ( ( G e. USGraph /\ X e. dom E ) -> ( # ` ( E ` X ) ) = 2 )
5		sseq1	|- ( ( E ` X ) = { M , N } -> ( ( E ` X ) C_ V <-> { M , N } C_ V ) )
6		fveq2	|- ( ( E ` X ) = { M , N } -> ( # ` ( E ` X ) ) = ( # ` { M , N } ) )
7	6	eqeq1d	|- ( ( E ` X ) = { M , N } -> ( ( # ` ( E ` X ) ) = 2 <-> ( # ` { M , N } ) = 2 ) )
8	5 7	anbi12d	|- ( ( E ` X ) = { M , N } -> ( ( ( E ` X ) C_ V /\ ( # ` ( E ` X ) ) = 2 ) <-> ( { M , N } C_ V /\ ( # ` { M , N } ) = 2 ) ) )
9		eqid	|- { M , N } = { M , N }
10	9	hashprdifel	|- ( ( # ` { M , N } ) = 2 -> ( M e. { M , N } /\ N e. { M , N } /\ M =/= N ) )
11		prssg	|- ( ( M e. { M , N } /\ N e. { M , N } ) -> ( ( M e. V /\ N e. V ) <-> { M , N } C_ V ) )
12	11	3adant3	|- ( ( M e. { M , N } /\ N e. { M , N } /\ M =/= N ) -> ( ( M e. V /\ N e. V ) <-> { M , N } C_ V ) )
13	12	biimprd	|- ( ( M e. { M , N } /\ N e. { M , N } /\ M =/= N ) -> ( { M , N } C_ V -> ( M e. V /\ N e. V ) ) )
14	10 13	syl	|- ( ( # ` { M , N } ) = 2 -> ( { M , N } C_ V -> ( M e. V /\ N e. V ) ) )
15	14	impcom	|- ( ( { M , N } C_ V /\ ( # ` { M , N } ) = 2 ) -> ( M e. V /\ N e. V ) )
16	8 15	syl6bi	|- ( ( E ` X ) = { M , N } -> ( ( ( E ` X ) C_ V /\ ( # ` ( E ` X ) ) = 2 ) -> ( M e. V /\ N e. V ) ) )
17	16	com12	|- ( ( ( E ` X ) C_ V /\ ( # ` ( E ` X ) ) = 2 ) -> ( ( E ` X ) = { M , N } -> ( M e. V /\ N e. V ) ) )
18	3 4 17	syl2anc	|- ( ( G e. USGraph /\ X e. dom E ) -> ( ( E ` X ) = { M , N } -> ( M e. V /\ N e. V ) ) )