Theorem umgredgprv

Description: In a multigraph, an edge is an unordered pair of vertices. This theorem would not hold for arbitrary hyper-/pseudographs since either M or N could be proper classes ( ( EX ) would be a loop in this case), which are no vertices of course. (Contributed by Alexander van der Vekens, 19-Aug-2017) (Revised by AV, 11-Dec-2020)

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

Proof

Step	Hyp	Ref	Expression
1		umgrnloopv.e	|- E = ( iEdg ` G )
2		umgredgprv.v	|- V = ( Vtx ` G )
3		umgruhgr	|- ( G e. UMGraph -> G e. UHGraph )
4	2 1	uhgrss	|- ( ( G e. UHGraph /\ X e. dom E ) -> ( E ` X ) C_ V )
5	3 4	sylan	|- ( ( G e. UMGraph /\ X e. dom E ) -> ( E ` X ) C_ V )
6	2 1	umgredg2	|- ( ( G e. UMGraph /\ X e. dom E ) -> ( # ` ( E ` X ) ) = 2 )
7		sseq1	|- ( ( E ` X ) = { M , N } -> ( ( E ` X ) C_ V <-> { M , N } C_ V ) )
8		fveqeq2	|- ( ( E ` X ) = { M , N } -> ( ( # ` ( E ` X ) ) = 2 <-> ( # ` { M , N } ) = 2 ) )
9	7 8	anbi12d	|- ( ( E ` X ) = { M , N } -> ( ( ( E ` X ) C_ V /\ ( # ` ( E ` X ) ) = 2 ) <-> ( { M , N } C_ V /\ ( # ` { M , N } ) = 2 ) ) )
10		eqid	|- { M , N } = { M , N }
11	10	hashprdifel	|- ( ( # ` { M , N } ) = 2 -> ( M e. { M , N } /\ N e. { M , N } /\ M =/= N ) )
12		prssg	|- ( ( M e. { M , N } /\ N e. { M , N } ) -> ( ( M e. V /\ N e. V ) <-> { M , N } C_ V ) )
13	12	3adant3	|- ( ( M e. { M , N } /\ N e. { M , N } /\ M =/= N ) -> ( ( M e. V /\ N e. V ) <-> { M , N } C_ V ) )
14	13	biimprd	|- ( ( M e. { M , N } /\ N e. { M , N } /\ M =/= N ) -> ( { M , N } C_ V -> ( M e. V /\ N e. V ) ) )
15	11 14	syl	|- ( ( # ` { M , N } ) = 2 -> ( { M , N } C_ V -> ( M e. V /\ N e. V ) ) )
16	15	impcom	|- ( ( { M , N } C_ V /\ ( # ` { M , N } ) = 2 ) -> ( M e. V /\ N e. V ) )
17	9 16	syl6bi	|- ( ( E ` X ) = { M , N } -> ( ( ( E ` X ) C_ V /\ ( # ` ( E ` X ) ) = 2 ) -> ( M e. V /\ N e. V ) ) )
18	17	com12	|- ( ( ( E ` X ) C_ V /\ ( # ` ( E ` X ) ) = 2 ) -> ( ( E ` X ) = { M , N } -> ( M e. V /\ N e. V ) ) )
19	5 6 18	syl2anc	|- ( ( G e. UMGraph /\ X e. dom E ) -> ( ( E ` X ) = { M , N } -> ( M e. V /\ N e. V ) ) )