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 ) → ∃ 𝑎 ∃ 𝑏 𝑉 = { 𝑎 , 𝑏 } )