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 \in USGraph \to \{x \in dom E \| E (x) = \{U\}\} = \emptyset$

Proof

Step	Hyp	Ref	Expression
1		usgrnloopv.e	$⊢ E = iEdg (G)$
2		neirr	$⊢ \neg U \neq U$
3	1	usgrnloop	$⊢ G \in USGraph \to (\exists x \in dom E E (x) = \{U, U\} \to U \neq U)$
4	2 3	mtoi	$⊢ G \in USGraph \to \neg \exists x \in dom E E (x) = \{U, U\}$
5		simpr	$⊢ (G \in USGraph \land E (x) = \{U\}) \to E (x) = \{U\}$
6		dfsn2	$⊢ \{U\} = \{U, U\}$
7	5 6	syl6eq	$⊢ (G \in USGraph \land E (x) = \{U\}) \to E (x) = \{U, U\}$
8	7	ex	$⊢ G \in USGraph \to (E (x) = \{U\} \to E (x) = \{U, U\})$
9	8	reximdv	$⊢ G \in USGraph \to (\exists x \in dom E E (x) = \{U\} \to \exists x \in dom E E (x) = \{U, U\})$
10	4 9	mtod	$⊢ G \in USGraph \to \neg \exists x \in dom E E (x) = \{U\}$
11		ralnex	$⊢ \forall x \in dom E \neg E (x) = \{U\} \leftrightarrow \neg \exists x \in dom E E (x) = \{U\}$
12	10 11	sylibr	$⊢ G \in USGraph \to \forall x \in dom E \neg E (x) = \{U\}$
13		rabeq0	$⊢ \{x \in dom E \| E (x) = \{U\}\} = \emptyset \leftrightarrow \forall x \in dom E \neg E (x) = \{U\}$
14	12 13	sylibr	$⊢ G \in USGraph \to \{x \in dom E \| E (x) = \{U\}\} = \emptyset$