umgrpredgv

Description: An edge of a multigraph always connects two vertices. Analogue of umgredgprv . This theorem does not hold for arbitrary pseudographs: if either M or N is a proper class, then { M , N } e. E could still hold ( { M , N } would be either { M } or { N } , see prprc1 or prprc2 , i.e. a loop), but M e. V or N e. V would not be true. (Contributed by AV, 27-Nov-2020)

	Ref	Expression
Hypotheses	upgredg.v	\|- V = ( Vtx ` G )
	upgredg.e	\|- E = ( Edg ` G )
Assertion	umgrpredgv	\|- ( ( G e. UMGraph /\ { M , N } e. E ) -> ( M e. V /\ N e. V ) )

Proof

Step	Hyp	Ref	Expression
1		upgredg.v	\|- V = ( Vtx ` G )
2		upgredg.e	\|- E = ( Edg ` G )
3	2	eleq2i	\|- ( { M , N } e. E <-> { M , N } e. ( Edg ` G ) )
4		edgumgr	\|- ( ( G e. UMGraph /\ { M , N } e. ( Edg ` G ) ) -> ( { M , N } e. ~P ( Vtx ` G ) /\ ( # ` { M , N } ) = 2 ) )
5	3 4	sylan2b	\|- ( ( G e. UMGraph /\ { M , N } e. E ) -> ( { M , N } e. ~P ( Vtx ` G ) /\ ( # ` { M , N } ) = 2 ) )
6		eqid	\|- { M , N } = { M , N }
7	6	hashprdifel	\|- ( ( # ` { M , N } ) = 2 -> ( M e. { M , N } /\ N e. { M , N } /\ M =/= N ) )
8	1	eqcomi	\|- ( Vtx ` G ) = V
9	8	pweqi	\|- ~P ( Vtx ` G ) = ~P V
10	9	eleq2i	\|- ( { M , N } e. ~P ( Vtx ` G ) <-> { M , N } e. ~P V )
11		prelpw	\|- ( ( M e. { M , N } /\ N e. { M , N } ) -> ( ( M e. V /\ N e. V ) <-> { M , N } e. ~P V ) )
12	11	biimprd	\|- ( ( M e. { M , N } /\ N e. { M , N } ) -> ( { M , N } e. ~P V -> ( M e. V /\ N e. V ) ) )
13	10 12	biimtrid	\|- ( ( M e. { M , N } /\ N e. { M , N } ) -> ( { M , N } e. ~P ( Vtx ` G ) -> ( M e. V /\ N e. V ) ) )
14	13	3adant3	\|- ( ( M e. { M , N } /\ N e. { M , N } /\ M =/= N ) -> ( { M , N } e. ~P ( Vtx ` G ) -> ( M e. V /\ N e. V ) ) )
15	7 14	syl	\|- ( ( # ` { M , N } ) = 2 -> ( { M , N } e. ~P ( Vtx ` G ) -> ( M e. V /\ N e. V ) ) )
16	15	impcom	\|- ( ( { M , N } e. ~P ( Vtx ` G ) /\ ( # ` { M , N } ) = 2 ) -> ( M e. V /\ N e. V ) )
17	5 16	syl	\|- ( ( G e. UMGraph /\ { M , N } e. E ) -> ( M e. V /\ N e. V ) )

Metamath Proof Explorer

Theorem umgrpredgv

Proof