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 ⊢ 𝐸 = ( 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 𝐸 ∣ ( 𝐸 ‘ 𝑥 ) = { 𝑈 } } = ∅ )