This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem usgrnloopALT

Description: Alternate proof of usgrnloop , not using umgrnloop . (Contributed by Alexander van der Vekens, 19-Aug-2017) (Proof shortened by Alexander van der Vekens, 20-Mar-2018) (Revised by AV, 17-Oct-2020) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypothesis usgrnloopv.e ⊢ 𝐸 = ( iEdg ‘ 𝐺 )
Assertion usgrnloopALT ( 𝐺 ∈ USGraph → ( ∃ 𝑥 ∈ dom 𝐸 ( 𝐸 ‘ 𝑥 ) = { 𝑀 , 𝑁 } → 𝑀 ≠ 𝑁 ) )

Proof

Step Hyp Ref Expression
1 usgrnloopv.e ⊢ 𝐸 = ( iEdg ‘ 𝐺 )
2 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
3 1 2 usgredgprv ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑥 ∈ dom 𝐸 ) → ( ( 𝐸 ‘ 𝑥 ) = { 𝑀 , 𝑁 } → ( 𝑀 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑁 ∈ ( Vtx ‘ 𝐺 ) ) ) )
4 3 imp ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑥 ∈ dom 𝐸 ) ∧ ( 𝐸 ‘ 𝑥 ) = { 𝑀 , 𝑁 } ) → ( 𝑀 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑁 ∈ ( Vtx ‘ 𝐺 ) ) )
5 1 usgrnloopv ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑀 ∈ ( Vtx ‘ 𝐺 ) ) → ( ( 𝐸 ‘ 𝑥 ) = { 𝑀 , 𝑁 } → 𝑀 ≠ 𝑁 ) )
6 5 ex ⊢ ( 𝐺 ∈ USGraph → ( 𝑀 ∈ ( Vtx ‘ 𝐺 ) → ( ( 𝐸 ‘ 𝑥 ) = { 𝑀 , 𝑁 } → 𝑀 ≠ 𝑁 ) ) )
7 6 com23 ⊢ ( 𝐺 ∈ USGraph → ( ( 𝐸 ‘ 𝑥 ) = { 𝑀 , 𝑁 } → ( 𝑀 ∈ ( Vtx ‘ 𝐺 ) → 𝑀 ≠ 𝑁 ) ) )
8 7 adantr ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑥 ∈ dom 𝐸 ) → ( ( 𝐸 ‘ 𝑥 ) = { 𝑀 , 𝑁 } → ( 𝑀 ∈ ( Vtx ‘ 𝐺 ) → 𝑀 ≠ 𝑁 ) ) )
9 8 imp ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑥 ∈ dom 𝐸 ) ∧ ( 𝐸 ‘ 𝑥 ) = { 𝑀 , 𝑁 } ) → ( 𝑀 ∈ ( Vtx ‘ 𝐺 ) → 𝑀 ≠ 𝑁 ) )
10 9 com12 ⊢ ( 𝑀 ∈ ( Vtx ‘ 𝐺 ) → ( ( ( 𝐺 ∈ USGraph ∧ 𝑥 ∈ dom 𝐸 ) ∧ ( 𝐸 ‘ 𝑥 ) = { 𝑀 , 𝑁 } ) → 𝑀 ≠ 𝑁 ) )
11 10 adantr ⊢ ( ( 𝑀 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑁 ∈ ( Vtx ‘ 𝐺 ) ) → ( ( ( 𝐺 ∈ USGraph ∧ 𝑥 ∈ dom 𝐸 ) ∧ ( 𝐸 ‘ 𝑥 ) = { 𝑀 , 𝑁 } ) → 𝑀 ≠ 𝑁 ) )
12 4 11 mpcom ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑥 ∈ dom 𝐸 ) ∧ ( 𝐸 ‘ 𝑥 ) = { 𝑀 , 𝑁 } ) → 𝑀 ≠ 𝑁 )
13 12 ex ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑥 ∈ dom 𝐸 ) → ( ( 𝐸 ‘ 𝑥 ) = { 𝑀 , 𝑁 } → 𝑀 ≠ 𝑁 ) )
14 13 rexlimdva ⊢ ( 𝐺 ∈ USGraph → ( ∃ 𝑥 ∈ dom 𝐸 ( 𝐸 ‘ 𝑥 ) = { 𝑀 , 𝑁 } → 𝑀 ≠ 𝑁 ) )