Metamath Proof Explorer

Theorem tpf1o

Description: A bijection onto a (proper) triple. (Contributed by AV, 21-Jul-2025)

Ref Expression
Hypotheses tpf1o.f ⊢ F = x ∈ 0 ..^ 3 ⟼ if x = 0 A if x = 1 B C
tpf.t ⊢ T = A B C
Assertion tpf1o ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ T = 3 → F : 0 ..^ 3 ⟶ 1-1 onto T

Proof

Step Hyp Ref Expression
1 tpf1o.f ⊢ F = x ∈ 0 ..^ 3 ⟼ if x = 0 A if x = 1 B C
2 tpf.t ⊢ T = A B C
3 1 2 tpfo ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V → F : 0 ..^ 3 ⟶ onto T
4 3 adantr ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ T = 3 → F : 0 ..^ 3 ⟶ onto T
5 3nn0 ⊢ 3 ∈ ℕ 0
6 hashfzo0 ⊢ 3 ∈ ℕ 0 → 0 ..^ 3 = 3
7 5 6 ax-mp ⊢ 0 ..^ 3 = 3
8 eqcom ⊢ T = 3 ↔ 3 = T
9 8 bilani ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ T = 3 → 3 = T
10 7 9 eqtrid ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ T = 3 → 0 ..^ 3 = T
11 fzofi ⊢ 0 ..^ 3 ∈ Fin
12 11 a1i ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V → 0 ..^ 3 ∈ Fin
13 tpfi ⊢ A B C ∈ Fin
14 2 13 eqeltri ⊢ T ∈ Fin
15 14 a1i ⊢ T = 3 → T ∈ Fin
16 hashen ⊢ 0 ..^ 3 ∈ Fin ∧ T ∈ Fin → 0 ..^ 3 = T ↔ 0 ..^ 3 ≈ T
17 12 15 16 syl2an ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ T = 3 → 0 ..^ 3 = T ↔ 0 ..^ 3 ≈ T
18 10 17 mpbid ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ T = 3 → 0 ..^ 3 ≈ T
19 14 a1i ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ T = 3 → T ∈ Fin
20 fofinf1o ⊢ F : 0 ..^ 3 ⟶ onto T ∧ 0 ..^ 3 ≈ T ∧ T ∈ Fin → F : 0 ..^ 3 ⟶ 1-1 onto T
21 4 18 19 20 syl3anc ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ T = 3 → F : 0 ..^ 3 ⟶ 1-1 onto T