Metamath Proof Explorer

Theorem hash3tr

Description: A set of size three is an unordered triple. (Contributed by Alexander van der Vekens, 13-Sep-2018)

Ref Expression
Assertion hash3tr ⊢ V ∈ W ∧ V = 3 → ∃ a ∃ b ∃ c V = a b c

Proof

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