Metamath Proof Explorer


Theorem usgrnloop0ALT

Description: Alternate proof of usgrnloop0 , not using umgrnloop0 . (Contributed by Alexander van der Vekens, 6-Dec-2017) (Revised by AV, 17-Oct-2020) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypothesis usgrnloopv.e E = iEdg G
Assertion usgrnloop0ALT G USGraph x dom E | E x = U =

Proof

Step Hyp Ref Expression
1 usgrnloopv.e E = iEdg G
2 neirr ¬ U U
3 1 usgrnloop G USGraph x dom E E x = U U U U
4 2 3 mtoi G USGraph ¬ x dom E E x = U U
5 simpr G USGraph E x = U E x = U
6 dfsn2 U = U U
7 5 6 eqtrdi G USGraph E x = U E x = U U
8 7 ex G USGraph E x = U E x = U U
9 8 reximdv G USGraph x dom E E x = U x dom E E x = U U
10 4 9 mtod G USGraph ¬ x dom E E x = U
11 ralnex x dom E ¬ E x = U ¬ x dom E E x = U
12 10 11 sylibr G USGraph x dom E ¬ E x = U
13 rabeq0 x dom E | E x = U = x dom E ¬ E x = U
14 12 13 sylibr G USGraph x dom E | E x = U =