Metamath Proof Explorer

Theorem tpfo

Description: A function onto a (proper) triple. (Contributed by AV, 20-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 tpfo ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V → F : 0 ..^ 3 ⟶ 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 tpf ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V → F : 0 ..^ 3 ⟶ T
4 eltpi ⊢ t ∈ A B C → t = A ∨ t = B ∨ t = C
5 3nn ⊢ 3 ∈ ℕ
6 lbfzo0 ⊢ 0 ∈ 0 ..^ 3 ↔ 3 ∈ ℕ
7 5 6 mpbir ⊢ 0 ∈ 0 ..^ 3
8 7 a1i ⊢ A ∈ V → 0 ∈ 0 ..^ 3
9 fveq2 ⊢ i = 0 → F ⁡ i = F ⁡ 0
10 9 eqeq2d ⊢ i = 0 → A = F ⁡ i ↔ A = F ⁡ 0
11 10 adantl ⊢ A ∈ V ∧ i = 0 → A = F ⁡ i ↔ A = F ⁡ 0
12 1 tpf1ofv0 ⊢ A ∈ V → F ⁡ 0 = A
13 12 eqcomd ⊢ A ∈ V → A = F ⁡ 0
14 8 11 13 rspcedvd ⊢ A ∈ V → ∃ i ∈ 0 ..^ 3 A = F ⁡ i
15 eqeq1 ⊢ t = A → t = F ⁡ i ↔ A = F ⁡ i
16 15 rexbidv ⊢ t = A → ∃ i ∈ 0 ..^ 3 t = F ⁡ i ↔ ∃ i ∈ 0 ..^ 3 A = F ⁡ i
17 14 16 syl5ibrcom ⊢ A ∈ V → t = A → ∃ i ∈ 0 ..^ 3 t = F ⁡ i
18 1nn0 ⊢ 1 ∈ ℕ 0
19 1lt3 ⊢ 1 < 3
20 elfzo0 ⊢ 1 ∈ 0 ..^ 3 ↔ 1 ∈ ℕ 0 ∧ 3 ∈ ℕ ∧ 1 < 3
21 18 5 19 20 mpbir3an ⊢ 1 ∈ 0 ..^ 3
22 21 a1i ⊢ B ∈ V → 1 ∈ 0 ..^ 3
23 fveq2 ⊢ i = 1 → F ⁡ i = F ⁡ 1
24 23 eqeq2d ⊢ i = 1 → B = F ⁡ i ↔ B = F ⁡ 1
25 24 adantl ⊢ B ∈ V ∧ i = 1 → B = F ⁡ i ↔ B = F ⁡ 1
26 1 tpf1ofv1 ⊢ B ∈ V → F ⁡ 1 = B
27 26 eqcomd ⊢ B ∈ V → B = F ⁡ 1
28 22 25 27 rspcedvd ⊢ B ∈ V → ∃ i ∈ 0 ..^ 3 B = F ⁡ i
29 eqeq1 ⊢ t = B → t = F ⁡ i ↔ B = F ⁡ i
30 29 rexbidv ⊢ t = B → ∃ i ∈ 0 ..^ 3 t = F ⁡ i ↔ ∃ i ∈ 0 ..^ 3 B = F ⁡ i
31 28 30 syl5ibrcom ⊢ B ∈ V → t = B → ∃ i ∈ 0 ..^ 3 t = F ⁡ i
32 2nn0 ⊢ 2 ∈ ℕ 0
33 2lt3 ⊢ 2 < 3
34 elfzo0 ⊢ 2 ∈ 0 ..^ 3 ↔ 2 ∈ ℕ 0 ∧ 3 ∈ ℕ ∧ 2 < 3
35 32 5 33 34 mpbir3an ⊢ 2 ∈ 0 ..^ 3
36 35 a1i ⊢ C ∈ V → 2 ∈ 0 ..^ 3
37 fveq2 ⊢ i = 2 → F ⁡ i = F ⁡ 2
38 37 eqeq2d ⊢ i = 2 → C = F ⁡ i ↔ C = F ⁡ 2
39 38 adantl ⊢ C ∈ V ∧ i = 2 → C = F ⁡ i ↔ C = F ⁡ 2
40 1 tpf1ofv2 ⊢ C ∈ V → F ⁡ 2 = C
41 40 eqcomd ⊢ C ∈ V → C = F ⁡ 2
42 36 39 41 rspcedvd ⊢ C ∈ V → ∃ i ∈ 0 ..^ 3 C = F ⁡ i
43 eqeq1 ⊢ t = C → t = F ⁡ i ↔ C = F ⁡ i
44 43 rexbidv ⊢ t = C → ∃ i ∈ 0 ..^ 3 t = F ⁡ i ↔ ∃ i ∈ 0 ..^ 3 C = F ⁡ i
45 42 44 syl5ibrcom ⊢ C ∈ V → t = C → ∃ i ∈ 0 ..^ 3 t = F ⁡ i
46 17 31 45 3jaao ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V → t = A ∨ t = B ∨ t = C → ∃ i ∈ 0 ..^ 3 t = F ⁡ i
47 4 46 syl5com ⊢ t ∈ A B C → A ∈ V ∧ B ∈ V ∧ C ∈ V → ∃ i ∈ 0 ..^ 3 t = F ⁡ i
48 47 2 eleq2s ⊢ t ∈ T → A ∈ V ∧ B ∈ V ∧ C ∈ V → ∃ i ∈ 0 ..^ 3 t = F ⁡ i
49 48 com12 ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V → t ∈ T → ∃ i ∈ 0 ..^ 3 t = F ⁡ i
50 49 ralrimiv ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V → ∀ t ∈ T ∃ i ∈ 0 ..^ 3 t = F ⁡ i
51 dffo3 ⊢ F : 0 ..^ 3 ⟶ onto T ↔ F : 0 ..^ 3 ⟶ T ∧ ∀ t ∈ T ∃ i ∈ 0 ..^ 3 t = F ⁡ i
52 3 50 51 sylanbrc ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V → F : 0 ..^ 3 ⟶ onto T