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 ⊢ E = iEdg ⁡ G
Assertion usgrnloopvALT ⊢ G ∈ USGraph ∧ M ∈ W → E ⁡ X = M N → M ≠ N

Proof

Step Hyp Ref Expression
1 usgrnloopv.e ⊢ E = iEdg ⁡ G
2 prnzg ⊢ M ∈ W → M N ≠ ∅
3 2 adantl ⊢ E ⁡ X = M N ∧ M ∈ W → M N ≠ ∅
4 neeq1 ⊢ E ⁡ X = M N → E ⁡ X ≠ ∅ ↔ M N ≠ ∅
5 4 adantr ⊢ E ⁡ X = M N ∧ M ∈ W → E ⁡ X ≠ ∅ ↔ M N ≠ ∅
6 3 5 mpbird ⊢ E ⁡ X = M N ∧ M ∈ W → E ⁡ X ≠ ∅
7 fvfundmfvn0 ⊢ E ⁡ X ≠ ∅ → X ∈ dom ⁡ E ∧ Fun ⁡ E ↾ X
8 6 7 syl ⊢ E ⁡ X = M N ∧ M ∈ W → X ∈ dom ⁡ E ∧ Fun ⁡ E ↾ X
9 1 usgredg2 ⊢ G ∈ USGraph ∧ X ∈ dom ⁡ E → E ⁡ X = 2
10 fveq2 ⊢ E ⁡ X = M N → E ⁡ X = M N
11 10 eqeq1d ⊢ E ⁡ X = M N → E ⁡ X = 2 ↔ M N = 2
12 eqid ⊢ M N = M N
13 12 hashprdifel ⊢ M N = 2 → M ∈ M N ∧ N ∈ M N ∧ M ≠ N
14 13 simp3d ⊢ M N = 2 → M ≠ N
15 11 14 syl6bi ⊢ E ⁡ X = M N → E ⁡ X = 2 → M ≠ N
16 15 adantr ⊢ E ⁡ X = M N ∧ M ∈ W → E ⁡ X = 2 → M ≠ N
17 9 16 syl5com ⊢ G ∈ USGraph ∧ X ∈ dom ⁡ E → E ⁡ X = M N ∧ M ∈ W → M ≠ N
18 17 expcom ⊢ X ∈ dom ⁡ E → G ∈ USGraph → E ⁡ X = M N ∧ M ∈ W → M ≠ N
19 18 com23 ⊢ X ∈ dom ⁡ E → E ⁡ X = M N ∧ M ∈ W → G ∈ USGraph → M ≠ N
20 19 adantr ⊢ X ∈ dom ⁡ E ∧ Fun ⁡ E ↾ X → E ⁡ X = M N ∧ M ∈ W → G ∈ USGraph → M ≠ N
21 8 20 mpcom ⊢ E ⁡ X = M N ∧ M ∈ W → G ∈ USGraph → M ≠ N
22 21 ex ⊢ E ⁡ X = M N → M ∈ W → G ∈ USGraph → M ≠ N
23 22 com13 ⊢ G ∈ USGraph → M ∈ W → E ⁡ X = M N → M ≠ N
24 23 imp ⊢ G ∈ USGraph ∧ M ∈ W → E ⁡ X = M N → M ≠ N