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	⊢ 𝐸 = ( iEdg ‘ 𝐺 )
Assertion	usgrnloop0ALT	⊢ ( 𝐺 ∈ USGraph → { 𝑥 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑥 ) = { 𝑈 } } = ∅ )

Proof

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