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 } } = (/) )