Metamath Proof Explorer

Theorem hash2prde

Description: A set of size two is an unordered pair of two different elements. (Contributed by Alexander van der Vekens, 8-Dec-2017)

Ref Expression
Assertion hash2prde ⊢ V ∈ W ∧ V = 2 → ∃ a ∃ b a ≠ b ∧ V = a b

Proof

Step Hyp Ref Expression
1 hash2pr ⊢ V ∈ W ∧ V = 2 → ∃ a ∃ b V = a b
2 equid ⊢ b = b
3 vex ⊢ a ∈ V
4 vex ⊢ b ∈ V
5 3 4 preqsn ⊢ a b = b ↔ a = b ∧ b = b
6 eqeq2 ⊢ a b = b → V = a b ↔ V = b
7 fveq2 ⊢ V = b → V = b
8 hashsng ⊢ b ∈ V → b = 1
9 8 elv ⊢ b = 1
10 7 9 eqtrdi ⊢ V = b → V = 1
11 eqeq1 ⊢ V = 2 → V = 1 ↔ 2 = 1
12 1ne2 ⊢ 1 ≠ 2
13 df-ne ⊢ 1 ≠ 2 ↔ ¬ 1 = 2
14 pm2.21 ⊢ ¬ 1 = 2 → 1 = 2 → a ≠ b
15 13 14 sylbi ⊢ 1 ≠ 2 → 1 = 2 → a ≠ b
16 12 15 ax-mp ⊢ 1 = 2 → a ≠ b
17 16 eqcoms ⊢ 2 = 1 → a ≠ b
18 11 17 biimtrdi ⊢ V = 2 → V = 1 → a ≠ b
19 18 adantl ⊢ V ∈ W ∧ V = 2 → V = 1 → a ≠ b
20 10 19 syl5com ⊢ V = b → V ∈ W ∧ V = 2 → a ≠ b
21 6 20 biimtrdi ⊢ a b = b → V = a b → V ∈ W ∧ V = 2 → a ≠ b
22 21 impcomd ⊢ a b = b → V ∈ W ∧ V = 2 ∧ V = a b → a ≠ b
23 5 22 sylbir ⊢ a = b ∧ b = b → V ∈ W ∧ V = 2 ∧ V = a b → a ≠ b
24 2 23 mpan2 ⊢ a = b → V ∈ W ∧ V = 2 ∧ V = a b → a ≠ b
25 ax-1 ⊢ a ≠ b → V ∈ W ∧ V = 2 ∧ V = a b → a ≠ b
26 24 25 pm2.61ine ⊢ V ∈ W ∧ V = 2 ∧ V = a b → a ≠ b
27 simpr ⊢ V ∈ W ∧ V = 2 ∧ V = a b → V = a b
28 26 27 jca ⊢ V ∈ W ∧ V = 2 ∧ V = a b → a ≠ b ∧ V = a b
29 28 ex ⊢ V ∈ W ∧ V = 2 → V = a b → a ≠ b ∧ V = a b
30 29 2eximdv ⊢ V ∈ W ∧ V = 2 → ∃ a ∃ b V = a b → ∃ a ∃ b a ≠ b ∧ V = a b
31 1 30 mpd ⊢ V ∈ W ∧ V = 2 → ∃ a ∃ b a ≠ b ∧ V = a b