Metamath Proof Explorer

Theorem usgrnloopvALT

Description: Alternate proof of usgrnloopv , not using umgrnloopv . (Contributed by Alexander van der Vekens, 26-Jan-2018) (Revised by AV, 17-Oct-2020) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypothesis usgrnloopv.e ⊢ 𝐸 = ( iEdg ‘ 𝐺 )
Assertion usgrnloopvALT ( ( 𝐺 ∈ USGraph ∧ 𝑀 ∈ 𝑊 ) → ( ( 𝐸 ‘ 𝑋 ) = { 𝑀 , 𝑁 } → 𝑀 ≠ 𝑁 ) )

Proof

Step Hyp Ref Expression
1 usgrnloopv.e ⊢ 𝐸 = ( iEdg ‘ 𝐺 )
2 prnzg ⊢ ( 𝑀 ∈ 𝑊 → { 𝑀 , 𝑁 } ≠ ∅ )
3 2 adantl ⊢ ( ( ( 𝐸 ‘ 𝑋 ) = { 𝑀 , 𝑁 } ∧ 𝑀 ∈ 𝑊 ) → { 𝑀 , 𝑁 } ≠ ∅ )
4 neeq1 ⊢ ( ( 𝐸 ‘ 𝑋 ) = { 𝑀 , 𝑁 } → ( ( 𝐸 ‘ 𝑋 ) ≠ ∅ ↔ { 𝑀 , 𝑁 } ≠ ∅ ) )
5 4 adantr ⊢ ( ( ( 𝐸 ‘ 𝑋 ) = { 𝑀 , 𝑁 } ∧ 𝑀 ∈ 𝑊 ) → ( ( 𝐸 ‘ 𝑋 ) ≠ ∅ ↔ { 𝑀 , 𝑁 } ≠ ∅ ) )
6 3 5 mpbird ⊢ ( ( ( 𝐸 ‘ 𝑋 ) = { 𝑀 , 𝑁 } ∧ 𝑀 ∈ 𝑊 ) → ( 𝐸 ‘ 𝑋 ) ≠ ∅ )
7 fvfundmfvn0 ⊢ ( ( 𝐸 ‘ 𝑋 ) ≠ ∅ → ( 𝑋 ∈ dom 𝐸 ∧ Fun ( 𝐸 ↾ { 𝑋 } ) ) )
8 6 7 syl ⊢ ( ( ( 𝐸 ‘ 𝑋 ) = { 𝑀 , 𝑁 } ∧ 𝑀 ∈ 𝑊 ) → ( 𝑋 ∈ dom 𝐸 ∧ Fun ( 𝐸 ↾ { 𝑋 } ) ) )
9 1 usgredg2 ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ dom 𝐸 ) → ( ♯ ‘ ( 𝐸 ‘ 𝑋 ) ) = 2 )
10 fveq2 ⊢ ( ( 𝐸 ‘ 𝑋 ) = { 𝑀 , 𝑁 } → ( ♯ ‘ ( 𝐸 ‘ 𝑋 ) ) = ( ♯ ‘ { 𝑀 , 𝑁 } ) )
11 10 eqeq1d ⊢ ( ( 𝐸 ‘ 𝑋 ) = { 𝑀 , 𝑁 } → ( ( ♯ ‘ ( 𝐸 ‘ 𝑋 ) ) = 2 ↔ ( ♯ ‘ { 𝑀 , 𝑁 } ) = 2 ) )
12 eqid ⊢ { 𝑀 , 𝑁 } = { 𝑀 , 𝑁 }
13 12 hashprdifel ⊢ ( ( ♯ ‘ { 𝑀 , 𝑁 } ) = 2 → ( 𝑀 ∈ { 𝑀 , 𝑁 } ∧ 𝑁 ∈ { 𝑀 , 𝑁 } ∧ 𝑀 ≠ 𝑁 ) )
14 13 simp3d ⊢ ( ( ♯ ‘ { 𝑀 , 𝑁 } ) = 2 → 𝑀 ≠ 𝑁 )
15 11 14 biimtrdi ⊢ ( ( 𝐸 ‘ 𝑋 ) = { 𝑀 , 𝑁 } → ( ( ♯ ‘ ( 𝐸 ‘ 𝑋 ) ) = 2 → 𝑀 ≠ 𝑁 ) )
16 15 adantr ⊢ ( ( ( 𝐸 ‘ 𝑋 ) = { 𝑀 , 𝑁 } ∧ 𝑀 ∈ 𝑊 ) → ( ( ♯ ‘ ( 𝐸 ‘ 𝑋 ) ) = 2 → 𝑀 ≠ 𝑁 ) )
17 9 16 syl5com ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ dom 𝐸 ) → ( ( ( 𝐸 ‘ 𝑋 ) = { 𝑀 , 𝑁 } ∧ 𝑀 ∈ 𝑊 ) → 𝑀 ≠ 𝑁 ) )
18 17 expcom ⊢ ( 𝑋 ∈ dom 𝐸 → ( 𝐺 ∈ USGraph → ( ( ( 𝐸 ‘ 𝑋 ) = { 𝑀 , 𝑁 } ∧ 𝑀 ∈ 𝑊 ) → 𝑀 ≠ 𝑁 ) ) )
19 18 com23 ⊢ ( 𝑋 ∈ dom 𝐸 → ( ( ( 𝐸 ‘ 𝑋 ) = { 𝑀 , 𝑁 } ∧ 𝑀 ∈ 𝑊 ) → ( 𝐺 ∈ USGraph → 𝑀 ≠ 𝑁 ) ) )
20 19 adantr ⊢ ( ( 𝑋 ∈ dom 𝐸 ∧ Fun ( 𝐸 ↾ { 𝑋 } ) ) → ( ( ( 𝐸 ‘ 𝑋 ) = { 𝑀 , 𝑁 } ∧ 𝑀 ∈ 𝑊 ) → ( 𝐺 ∈ USGraph → 𝑀 ≠ 𝑁 ) ) )
21 8 20 mpcom ⊢ ( ( ( 𝐸 ‘ 𝑋 ) = { 𝑀 , 𝑁 } ∧ 𝑀 ∈ 𝑊 ) → ( 𝐺 ∈ USGraph → 𝑀 ≠ 𝑁 ) )
22 21 ex ⊢ ( ( 𝐸 ‘ 𝑋 ) = { 𝑀 , 𝑁 } → ( 𝑀 ∈ 𝑊 → ( 𝐺 ∈ USGraph → 𝑀 ≠ 𝑁 ) ) )
23 22 com13 ⊢ ( 𝐺 ∈ USGraph → ( 𝑀 ∈ 𝑊 → ( ( 𝐸 ‘ 𝑋 ) = { 𝑀 , 𝑁 } → 𝑀 ≠ 𝑁 ) ) )
24 23 imp ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑀 ∈ 𝑊 ) → ( ( 𝐸 ‘ 𝑋 ) = { 𝑀 , 𝑁 } → 𝑀 ≠ 𝑁 ) )