Theorem umgrnloop0

Description: A multigraph has no loops. (Contributed by Alexander van der Vekens, 6-Dec-2017) (Revised by AV, 11-Dec-2020)

	Ref	Expression
Hypothesis	umgrnloopv.e	⊢ 𝐸 = ( iEdg ‘ 𝐺 )
Assertion	umgrnloop0	⊢ ( 𝐺 ∈ UMGraph → { 𝑥 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑥 ) = { 𝑈 } } = ∅ )

Proof

Step	Hyp	Ref	Expression
1		umgrnloopv.e	⊢ 𝐸 = ( iEdg ‘ 𝐺 )
2		neirr	⊢ ¬ 𝑈 ≠ 𝑈
3	1	umgrnloop	⊢ ( 𝐺 ∈ UMGraph → ( ∃ 𝑥 ∈ dom 𝐸 ( 𝐸 ‘ 𝑥 ) = { 𝑈 , 𝑈 } → 𝑈 ≠ 𝑈 ) )
4	2 3	mtoi	⊢ ( 𝐺 ∈ UMGraph → ¬ ∃ 𝑥 ∈ dom 𝐸 ( 𝐸 ‘ 𝑥 ) = { 𝑈 , 𝑈 } )
5		simpr	⊢ ( ( 𝐺 ∈ UMGraph ∧ ( 𝐸 ‘ 𝑥 ) = { 𝑈 } ) → ( 𝐸 ‘ 𝑥 ) = { 𝑈 } )
6		dfsn2	⊢ { 𝑈 } = { 𝑈 , 𝑈 }
7	5 6	eqtrdi	⊢ ( ( 𝐺 ∈ UMGraph ∧ ( 𝐸 ‘ 𝑥 ) = { 𝑈 } ) → ( 𝐸 ‘ 𝑥 ) = { 𝑈 , 𝑈 } )
8	7	ex	⊢ ( 𝐺 ∈ UMGraph → ( ( 𝐸 ‘ 𝑥 ) = { 𝑈 } → ( 𝐸 ‘ 𝑥 ) = { 𝑈 , 𝑈 } ) )
9	8	reximdv	⊢ ( 𝐺 ∈ UMGraph → ( ∃ 𝑥 ∈ dom 𝐸 ( 𝐸 ‘ 𝑥 ) = { 𝑈 } → ∃ 𝑥 ∈ dom 𝐸 ( 𝐸 ‘ 𝑥 ) = { 𝑈 , 𝑈 } ) )
10	4 9	mtod	⊢ ( 𝐺 ∈ UMGraph → ¬ ∃ 𝑥 ∈ dom 𝐸 ( 𝐸 ‘ 𝑥 ) = { 𝑈 } )
11		ralnex	⊢ ( ∀ 𝑥 ∈ dom 𝐸 ¬ ( 𝐸 ‘ 𝑥 ) = { 𝑈 } ↔ ¬ ∃ 𝑥 ∈ dom 𝐸 ( 𝐸 ‘ 𝑥 ) = { 𝑈 } )
12	10 11	sylibr	⊢ ( 𝐺 ∈ UMGraph → ∀ 𝑥 ∈ dom 𝐸 ¬ ( 𝐸 ‘ 𝑥 ) = { 𝑈 } )
13		rabeq0	⊢ ( { 𝑥 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑥 ) = { 𝑈 } } = ∅ ↔ ∀ 𝑥 ∈ dom 𝐸 ¬ ( 𝐸 ‘ 𝑥 ) = { 𝑈 } )
14	12 13	sylibr	⊢ ( 𝐺 ∈ UMGraph → { 𝑥 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑥 ) = { 𝑈 } } = ∅ )