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

Metamath Proof Explorer

Theorem elprchashprn2

Description: If one element of an unordered pair is not a set, the size of the unordered pair is not 2. (Contributed by Alexander van der Vekens, 7-Oct-2017)

Ref Expression
Assertion elprchashprn2 ⊢ ¬ M ∈ V → ¬ M N = 2

Proof

Step Hyp Ref Expression
1 prprc1 ⊢ ¬ M ∈ V → M N = N
2 hashsng ⊢ N ∈ V → N = 1
3 fveq2 ⊢ M N = N → M N = N
4 3 eqcomd ⊢ M N = N → N = M N
5 4 eqeq1d ⊢ M N = N → N = 1 ↔ M N = 1
6 5 biimpa ⊢ M N = N ∧ N = 1 → M N = 1
7 id ⊢ M N = 1 → M N = 1
8 1ne2 ⊢ 1 ≠ 2
9 8 a1i ⊢ M N = 1 → 1 ≠ 2
10 7 9 eqnetrd ⊢ M N = 1 → M N ≠ 2
11 10 neneqd ⊢ M N = 1 → ¬ M N = 2
12 6 11 syl ⊢ M N = N ∧ N = 1 → ¬ M N = 2
13 12 expcom ⊢ N = 1 → M N = N → ¬ M N = 2
14 2 13 syl ⊢ N ∈ V → M N = N → ¬ M N = 2
15 snprc ⊢ ¬ N ∈ V ↔ N = ∅
16 eqeq2 ⊢ N = ∅ → M N = N ↔ M N = ∅
17 16 biimpa ⊢ N = ∅ ∧ M N = N → M N = ∅
18 hash0 ⊢ ∅ = 0
19 fveq2 ⊢ M N = ∅ → M N = ∅
20 19 eqcomd ⊢ M N = ∅ → ∅ = M N
21 20 eqeq1d ⊢ M N = ∅ → ∅ = 0 ↔ M N = 0
22 21 biimpa ⊢ M N = ∅ ∧ ∅ = 0 → M N = 0
23 id ⊢ M N = 0 → M N = 0
24 0ne2 ⊢ 0 ≠ 2
25 24 a1i ⊢ M N = 0 → 0 ≠ 2
26 23 25 eqnetrd ⊢ M N = 0 → M N ≠ 2
27 26 neneqd ⊢ M N = 0 → ¬ M N = 2
28 22 27 syl ⊢ M N = ∅ ∧ ∅ = 0 → ¬ M N = 2
29 17 18 28 sylancl ⊢ N = ∅ ∧ M N = N → ¬ M N = 2
30 29 ex ⊢ N = ∅ → M N = N → ¬ M N = 2
31 15 30 sylbi ⊢ ¬ N ∈ V → M N = N → ¬ M N = 2
32 14 31 pm2.61i ⊢ M N = N → ¬ M N = 2
33 1 32 syl ⊢ ¬ M ∈ V → ¬ M N = 2