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

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

Proof

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