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