Metamath Proof Explorer


Theorem usgrnloopALT

Description: Alternate proof of usgrnloop , not using umgrnloop . (Contributed by Alexander van der Vekens, 19-Aug-2017) (Proof shortened by Alexander van der Vekens, 20-Mar-2018) (Revised by AV, 17-Oct-2020) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypothesis usgrnloopv.e E = iEdg G
Assertion usgrnloopALT G USGraph x dom E E x = M N M N

Proof

Step Hyp Ref Expression
1 usgrnloopv.e E = iEdg G
2 eqid Vtx G = Vtx G
3 1 2 usgredgprv G USGraph x dom E E x = M N M Vtx G N Vtx G
4 3 imp G USGraph x dom E E x = M N M Vtx G N Vtx G
5 1 usgrnloopv G USGraph M Vtx G E x = M N M N
6 5 ex G USGraph M Vtx G E x = M N M N
7 6 com23 G USGraph E x = M N M Vtx G M N
8 7 adantr G USGraph x dom E E x = M N M Vtx G M N
9 8 imp G USGraph x dom E E x = M N M Vtx G M N
10 9 com12 M Vtx G G USGraph x dom E E x = M N M N
11 10 adantr M Vtx G N Vtx G G USGraph x dom E E x = M N M N
12 4 11 mpcom G USGraph x dom E E x = M N M N
13 12 ex G USGraph x dom E E x = M N M N
14 13 rexlimdva G USGraph x dom E E x = M N M N