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

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 ( ( 𝑉 ∈ 𝑊 ∧ ( ♯ ‘ 𝑉 ) = 3 ) → ∃ 𝑎 ∃ 𝑏 ∃ 𝑐 𝑉 = { 𝑎 , 𝑏 , 𝑐 } )

Proof

Step Hyp Ref Expression
1 3nn0 ⊢ 3 ∈ ℕ0
2 hashvnfin ⊢ ( ( 𝑉 ∈ 𝑊 ∧ 3 ∈ ℕ0 ) → ( ( ♯ ‘ 𝑉 ) = 3 → 𝑉 ∈ Fin ) )
3 1 2 mpan2 ⊢ ( 𝑉 ∈ 𝑊 → ( ( ♯ ‘ 𝑉 ) = 3 → 𝑉 ∈ Fin ) )
4 3 imp ⊢ ( ( 𝑉 ∈ 𝑊 ∧ ( ♯ ‘ 𝑉 ) = 3 ) → 𝑉 ∈ Fin )
5 hash3 ⊢ ( ♯ ‘ 3o ) = 3
6 5 eqcomi ⊢ 3 = ( ♯ ‘ 3o )
7 6 a1i ⊢ ( 𝑉 ∈ Fin → 3 = ( ♯ ‘ 3o ) )
8 7 eqeq2d ⊢ ( 𝑉 ∈ Fin → ( ( ♯ ‘ 𝑉 ) = 3 ↔ ( ♯ ‘ 𝑉 ) = ( ♯ ‘ 3o ) ) )
9 3onn ⊢ 3o ∈ ω
10 nnfi ⊢ ( 3o ∈ ω → 3o ∈ Fin )
11 9 10 ax-mp ⊢ 3o ∈ Fin
12 hashen ⊢ ( ( 𝑉 ∈ Fin ∧ 3o ∈ Fin ) → ( ( ♯ ‘ 𝑉 ) = ( ♯ ‘ 3o ) ↔ 𝑉 ≈ 3o ) )
13 11 12 mpan2 ⊢ ( 𝑉 ∈ Fin → ( ( ♯ ‘ 𝑉 ) = ( ♯ ‘ 3o ) ↔ 𝑉 ≈ 3o ) )
14 13 biimpd ⊢ ( 𝑉 ∈ Fin → ( ( ♯ ‘ 𝑉 ) = ( ♯ ‘ 3o ) → 𝑉 ≈ 3o ) )
15 8 14 sylbid ⊢ ( 𝑉 ∈ Fin → ( ( ♯ ‘ 𝑉 ) = 3 → 𝑉 ≈ 3o ) )
16 15 adantld ⊢ ( 𝑉 ∈ Fin → ( ( 𝑉 ∈ 𝑊 ∧ ( ♯ ‘ 𝑉 ) = 3 ) → 𝑉 ≈ 3o ) )
17 4 16 mpcom ⊢ ( ( 𝑉 ∈ 𝑊 ∧ ( ♯ ‘ 𝑉 ) = 3 ) → 𝑉 ≈ 3o )
18 en3 ⊢ ( 𝑉 ≈ 3o → ∃ 𝑎 ∃ 𝑏 ∃ 𝑐 𝑉 = { 𝑎 , 𝑏 , 𝑐 } )
19 17 18 syl ⊢ ( ( 𝑉 ∈ 𝑊 ∧ ( ♯ ‘ 𝑉 ) = 3 ) → ∃ 𝑎 ∃ 𝑏 ∃ 𝑐 𝑉 = { 𝑎 , 𝑏 , 𝑐 } )