| Step | Hyp | Ref
| Expression |
| 1 | | tpf1o.f |
. . 3
⊢ 𝐹 = (𝑥 ∈ (0..^3) ↦ if(𝑥 = 0, 𝐴, if(𝑥 = 1, 𝐵, 𝐶))) |
| 2 | | tpf.t |
. . 3
⊢ 𝑇 = {𝐴, 𝐵, 𝐶} |
| 3 | 1, 2 | tpf 14538 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → 𝐹:(0..^3)⟶𝑇) |
| 4 | | eltpi 4688 |
. . . . . 6
⊢ (𝑡 ∈ {𝐴, 𝐵, 𝐶} → (𝑡 = 𝐴 ∨ 𝑡 = 𝐵 ∨ 𝑡 = 𝐶)) |
| 5 | | 3nn 12345 |
. . . . . . . . . . 11
⊢ 3 ∈
ℕ |
| 6 | | lbfzo0 13739 |
. . . . . . . . . . 11
⊢ (0 ∈
(0..^3) ↔ 3 ∈ ℕ) |
| 7 | 5, 6 | mpbir 231 |
. . . . . . . . . 10
⊢ 0 ∈
(0..^3) |
| 8 | 7 | a1i 11 |
. . . . . . . . 9
⊢ (𝐴 ∈ 𝑉 → 0 ∈ (0..^3)) |
| 9 | | fveq2 6906 |
. . . . . . . . . . 11
⊢ (𝑖 = 0 → (𝐹‘𝑖) = (𝐹‘0)) |
| 10 | 9 | eqeq2d 2748 |
. . . . . . . . . 10
⊢ (𝑖 = 0 → (𝐴 = (𝐹‘𝑖) ↔ 𝐴 = (𝐹‘0))) |
| 11 | 10 | adantl 481 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑖 = 0) → (𝐴 = (𝐹‘𝑖) ↔ 𝐴 = (𝐹‘0))) |
| 12 | 1 | tpf1ofv0 14535 |
. . . . . . . . . 10
⊢ (𝐴 ∈ 𝑉 → (𝐹‘0) = 𝐴) |
| 13 | 12 | eqcomd 2743 |
. . . . . . . . 9
⊢ (𝐴 ∈ 𝑉 → 𝐴 = (𝐹‘0)) |
| 14 | 8, 11, 13 | rspcedvd 3624 |
. . . . . . . 8
⊢ (𝐴 ∈ 𝑉 → ∃𝑖 ∈ (0..^3)𝐴 = (𝐹‘𝑖)) |
| 15 | | eqeq1 2741 |
. . . . . . . . 9
⊢ (𝑡 = 𝐴 → (𝑡 = (𝐹‘𝑖) ↔ 𝐴 = (𝐹‘𝑖))) |
| 16 | 15 | rexbidv 3179 |
. . . . . . . 8
⊢ (𝑡 = 𝐴 → (∃𝑖 ∈ (0..^3)𝑡 = (𝐹‘𝑖) ↔ ∃𝑖 ∈ (0..^3)𝐴 = (𝐹‘𝑖))) |
| 17 | 14, 16 | syl5ibrcom 247 |
. . . . . . 7
⊢ (𝐴 ∈ 𝑉 → (𝑡 = 𝐴 → ∃𝑖 ∈ (0..^3)𝑡 = (𝐹‘𝑖))) |
| 18 | | 1nn0 12542 |
. . . . . . . . . . 11
⊢ 1 ∈
ℕ0 |
| 19 | | 1lt3 12439 |
. . . . . . . . . . 11
⊢ 1 <
3 |
| 20 | | elfzo0 13740 |
. . . . . . . . . . 11
⊢ (1 ∈
(0..^3) ↔ (1 ∈ ℕ0 ∧ 3 ∈ ℕ ∧ 1
< 3)) |
| 21 | 18, 5, 19, 20 | mpbir3an 1342 |
. . . . . . . . . 10
⊢ 1 ∈
(0..^3) |
| 22 | 21 | a1i 11 |
. . . . . . . . 9
⊢ (𝐵 ∈ 𝑉 → 1 ∈ (0..^3)) |
| 23 | | fveq2 6906 |
. . . . . . . . . . 11
⊢ (𝑖 = 1 → (𝐹‘𝑖) = (𝐹‘1)) |
| 24 | 23 | eqeq2d 2748 |
. . . . . . . . . 10
⊢ (𝑖 = 1 → (𝐵 = (𝐹‘𝑖) ↔ 𝐵 = (𝐹‘1))) |
| 25 | 24 | adantl 481 |
. . . . . . . . 9
⊢ ((𝐵 ∈ 𝑉 ∧ 𝑖 = 1) → (𝐵 = (𝐹‘𝑖) ↔ 𝐵 = (𝐹‘1))) |
| 26 | 1 | tpf1ofv1 14536 |
. . . . . . . . . 10
⊢ (𝐵 ∈ 𝑉 → (𝐹‘1) = 𝐵) |
| 27 | 26 | eqcomd 2743 |
. . . . . . . . 9
⊢ (𝐵 ∈ 𝑉 → 𝐵 = (𝐹‘1)) |
| 28 | 22, 25, 27 | rspcedvd 3624 |
. . . . . . . 8
⊢ (𝐵 ∈ 𝑉 → ∃𝑖 ∈ (0..^3)𝐵 = (𝐹‘𝑖)) |
| 29 | | eqeq1 2741 |
. . . . . . . . 9
⊢ (𝑡 = 𝐵 → (𝑡 = (𝐹‘𝑖) ↔ 𝐵 = (𝐹‘𝑖))) |
| 30 | 29 | rexbidv 3179 |
. . . . . . . 8
⊢ (𝑡 = 𝐵 → (∃𝑖 ∈ (0..^3)𝑡 = (𝐹‘𝑖) ↔ ∃𝑖 ∈ (0..^3)𝐵 = (𝐹‘𝑖))) |
| 31 | 28, 30 | syl5ibrcom 247 |
. . . . . . 7
⊢ (𝐵 ∈ 𝑉 → (𝑡 = 𝐵 → ∃𝑖 ∈ (0..^3)𝑡 = (𝐹‘𝑖))) |
| 32 | | 2nn0 12543 |
. . . . . . . . . . 11
⊢ 2 ∈
ℕ0 |
| 33 | | 2lt3 12438 |
. . . . . . . . . . 11
⊢ 2 <
3 |
| 34 | | elfzo0 13740 |
. . . . . . . . . . 11
⊢ (2 ∈
(0..^3) ↔ (2 ∈ ℕ0 ∧ 3 ∈ ℕ ∧ 2
< 3)) |
| 35 | 32, 5, 33, 34 | mpbir3an 1342 |
. . . . . . . . . 10
⊢ 2 ∈
(0..^3) |
| 36 | 35 | a1i 11 |
. . . . . . . . 9
⊢ (𝐶 ∈ 𝑉 → 2 ∈ (0..^3)) |
| 37 | | fveq2 6906 |
. . . . . . . . . . 11
⊢ (𝑖 = 2 → (𝐹‘𝑖) = (𝐹‘2)) |
| 38 | 37 | eqeq2d 2748 |
. . . . . . . . . 10
⊢ (𝑖 = 2 → (𝐶 = (𝐹‘𝑖) ↔ 𝐶 = (𝐹‘2))) |
| 39 | 38 | adantl 481 |
. . . . . . . . 9
⊢ ((𝐶 ∈ 𝑉 ∧ 𝑖 = 2) → (𝐶 = (𝐹‘𝑖) ↔ 𝐶 = (𝐹‘2))) |
| 40 | 1 | tpf1ofv2 14537 |
. . . . . . . . . 10
⊢ (𝐶 ∈ 𝑉 → (𝐹‘2) = 𝐶) |
| 41 | 40 | eqcomd 2743 |
. . . . . . . . 9
⊢ (𝐶 ∈ 𝑉 → 𝐶 = (𝐹‘2)) |
| 42 | 36, 39, 41 | rspcedvd 3624 |
. . . . . . . 8
⊢ (𝐶 ∈ 𝑉 → ∃𝑖 ∈ (0..^3)𝐶 = (𝐹‘𝑖)) |
| 43 | | eqeq1 2741 |
. . . . . . . . 9
⊢ (𝑡 = 𝐶 → (𝑡 = (𝐹‘𝑖) ↔ 𝐶 = (𝐹‘𝑖))) |
| 44 | 43 | rexbidv 3179 |
. . . . . . . 8
⊢ (𝑡 = 𝐶 → (∃𝑖 ∈ (0..^3)𝑡 = (𝐹‘𝑖) ↔ ∃𝑖 ∈ (0..^3)𝐶 = (𝐹‘𝑖))) |
| 45 | 42, 44 | syl5ibrcom 247 |
. . . . . . 7
⊢ (𝐶 ∈ 𝑉 → (𝑡 = 𝐶 → ∃𝑖 ∈ (0..^3)𝑡 = (𝐹‘𝑖))) |
| 46 | 17, 31, 45 | 3jaao 1435 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → ((𝑡 = 𝐴 ∨ 𝑡 = 𝐵 ∨ 𝑡 = 𝐶) → ∃𝑖 ∈ (0..^3)𝑡 = (𝐹‘𝑖))) |
| 47 | 4, 46 | syl5com 31 |
. . . . 5
⊢ (𝑡 ∈ {𝐴, 𝐵, 𝐶} → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → ∃𝑖 ∈ (0..^3)𝑡 = (𝐹‘𝑖))) |
| 48 | 47, 2 | eleq2s 2859 |
. . . 4
⊢ (𝑡 ∈ 𝑇 → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → ∃𝑖 ∈ (0..^3)𝑡 = (𝐹‘𝑖))) |
| 49 | 48 | com12 32 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (𝑡 ∈ 𝑇 → ∃𝑖 ∈ (0..^3)𝑡 = (𝐹‘𝑖))) |
| 50 | 49 | ralrimiv 3145 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → ∀𝑡 ∈ 𝑇 ∃𝑖 ∈ (0..^3)𝑡 = (𝐹‘𝑖)) |
| 51 | | dffo3 7122 |
. 2
⊢ (𝐹:(0..^3)–onto→𝑇 ↔ (𝐹:(0..^3)⟶𝑇 ∧ ∀𝑡 ∈ 𝑇 ∃𝑖 ∈ (0..^3)𝑡 = (𝐹‘𝑖))) |
| 52 | 3, 50, 51 | sylanbrc 583 |
1
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → 𝐹:(0..^3)–onto→𝑇) |