Metamath Proof Explorer

Theorem hash2pr

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

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

Proof

Step Hyp Ref Expression
1 2nn0 ⊢ 2 ∈ ℕ 0
2 hashvnfin ⊢ V ∈ W ∧ 2 ∈ ℕ 0 → V = 2 → V ∈ Fin
3 1 2 mpan2 ⊢ V ∈ W → V = 2 → V ∈ Fin
4 3 imp ⊢ V ∈ W ∧ V = 2 → V ∈ Fin
5 hash2 ⊢ 2 𝑜 = 2
6 5 eqcomi ⊢ 2 = 2 𝑜
7 6 a1i ⊢ V ∈ Fin → 2 = 2 𝑜
8 7 eqeq2d ⊢ V ∈ Fin → V = 2 ↔ V = 2 𝑜
9 2onn ⊢ 2 𝑜 ∈ ω
10 nnfi ⊢ 2 𝑜 ∈ ω → 2 𝑜 ∈ Fin
11 9 10 ax-mp ⊢ 2 𝑜 ∈ Fin
12 hashen ⊢ V ∈ Fin ∧ 2 𝑜 ∈ Fin → V = 2 𝑜 ↔ V ≈ 2 𝑜
13 11 12 mpan2 ⊢ V ∈ Fin → V = 2 𝑜 ↔ V ≈ 2 𝑜
14 13 biimpd ⊢ V ∈ Fin → V = 2 𝑜 → V ≈ 2 𝑜
15 8 14 sylbid ⊢ V ∈ Fin → V = 2 → V ≈ 2 𝑜
16 15 adantld ⊢ V ∈ Fin → V ∈ W ∧ V = 2 → V ≈ 2 𝑜
17 4 16 mpcom ⊢ V ∈ W ∧ V = 2 → V ≈ 2 𝑜
18 en2 ⊢ V ≈ 2 𝑜 → ∃ a ∃ b V = a b
19 17 18 syl ⊢ V ∈ W ∧ V = 2 → ∃ a ∃ b V = a b