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 biimpi ⊢ T = 3 → 3 = T
10 9 adantl ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ T = 3 → 3 = T
11 7 10 eqtrid ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ T = 3 → 0 ..^ 3 = T
12 fzofi ⊢ 0 ..^ 3 ∈ Fin
13 12 a1i ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V → 0 ..^ 3 ∈ Fin
14 tpfi ⊢ A B C ∈ Fin
15 2 14 eqeltri ⊢ T ∈ Fin
16 15 a1i ⊢ T = 3 → T ∈ Fin
17 hashen ⊢ 0 ..^ 3 ∈ Fin ∧ T ∈ Fin → 0 ..^ 3 = T ↔ 0 ..^ 3 ≈ T
18 13 16 17 syl2an ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ T = 3 → 0 ..^ 3 = T ↔ 0 ..^ 3 ≈ T
19 11 18 mpbid ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ T = 3 → 0 ..^ 3 ≈ T
20 15 a1i ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ T = 3 → T ∈ Fin
21 fofinf1o ⊢ F : 0 ..^ 3 ⟶ onto T ∧ 0 ..^ 3 ≈ T ∧ T ∈ Fin → F : 0 ..^ 3 ⟶ 1-1 onto T
22 4 19 20 21 syl3anc ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ T = 3 → F : 0 ..^ 3 ⟶ 1-1 onto T