This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 e. USGraph -> { x e. dom E | ( E ` x ) = { U } } = (/) )

Proof

Step Hyp Ref Expression
1 usgrnloopv.e 
 |-  E = ( iEdg ` G )
2 neirr 
 |-  -. U =/= U
3 1 usgrnloop 
 |-  ( G e. USGraph -> ( E. x e. dom E ( E ` x ) = { U , U } -> U =/= U ) )
4 2 3 mtoi 
 |-  ( G e. USGraph -> -. E. x e. dom E ( E ` x ) = { U , U } )
5 simpr 
 |-  ( ( G e. USGraph /\ ( E ` x ) = { U } ) -> ( E ` x ) = { U } )
6 dfsn2 
 |-  { U } = { U , U }
7 5 6 eqtrdi 
 |-  ( ( G e. USGraph /\ ( E ` x ) = { U } ) -> ( E ` x ) = { U , U } )
8 7 ex 
 |-  ( G e. USGraph -> ( ( E ` x ) = { U } -> ( E ` x ) = { U , U } ) )
9 8 reximdv 
 |-  ( G e. USGraph -> ( E. x e. dom E ( E ` x ) = { U } -> E. x e. dom E ( E ` x ) = { U , U } ) )
10 4 9 mtod 
 |-  ( G e. USGraph -> -. E. x e. dom E ( E ` x ) = { U } )
11 ralnex 
 |-  ( A. x e. dom E -. ( E ` x ) = { U } <-> -. E. x e. dom E ( E ` x ) = { U } )
12 10 11 sylibr 
 |-  ( G e. USGraph -> A. x e. dom E -. ( E ` x ) = { U } )
13 rabeq0 
 |-  ( { x e. dom E | ( E ` x ) = { U } } = (/) <-> A. x e. dom E -. ( E ` x ) = { U } )
14 12 13 sylibr 
 |-  ( G e. USGraph -> { x e. dom E | ( E ` x ) = { U } } = (/) )