Metamath Proof Explorer

Theorem tpfo

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

Ref Expression
Hypotheses tpf1o.f ⊢ 𝐹 = ( 𝑥 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑥 = 0 , 𝐴 , if ( 𝑥 = 1 , 𝐵 , 𝐶 ) ) )
tpf.t ⊢ 𝑇 = { 𝐴 , 𝐵 , 𝐶 }
Assertion tpfo ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → 𝐹 : ( 0 ..^ 3 ) –onto→ 𝑇 )

Proof

Step Hyp Ref Expression
1 tpf1o.f ⊢ 𝐹 = ( 𝑥 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑥 = 0 , 𝐴 , if ( 𝑥 = 1 , 𝐵 , 𝐶 ) ) )
2 tpf.t ⊢ 𝑇 = { 𝐴 , 𝐵 , 𝐶 }
3 1 2 tpf ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → 𝐹 : ( 0 ..^ 3 ) ⟶ 𝑇 )
4 eltpi ⊢ ( 𝑡 ∈ { 𝐴 , 𝐵 , 𝐶 } → ( 𝑡 = 𝐴 ∨ 𝑡 = 𝐵 ∨ 𝑡 = 𝐶 ) )
5 3nn ⊢ 3 ∈ ℕ
6 lbfzo0 ⊢ ( 0 ∈ ( 0 ..^ 3 ) ↔ 3 ∈ ℕ )
7 5 6 mpbir ⊢ 0 ∈ ( 0 ..^ 3 )
8 7 a1i ⊢ ( 𝐴 ∈ 𝑉 → 0 ∈ ( 0 ..^ 3 ) )
9 fveq2 ⊢ ( 𝑖 = 0 → ( 𝐹 ‘ 𝑖 ) = ( 𝐹 ‘ 0 ) )
10 9 eqeq2d ⊢ ( 𝑖 = 0 → ( 𝐴 = ( 𝐹 ‘ 𝑖 ) ↔ 𝐴 = ( 𝐹 ‘ 0 ) ) )
11 10 adantl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑖 = 0 ) → ( 𝐴 = ( 𝐹 ‘ 𝑖 ) ↔ 𝐴 = ( 𝐹 ‘ 0 ) ) )
12 1 tpf1ofv0 ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐹 ‘ 0 ) = 𝐴 )
13 12 eqcomd ⊢ ( 𝐴 ∈ 𝑉 → 𝐴 = ( 𝐹 ‘ 0 ) )
14 8 11 13 rspcedvd ⊢ ( 𝐴 ∈ 𝑉 → ∃ 𝑖 ∈ ( 0 ..^ 3 ) 𝐴 = ( 𝐹 ‘ 𝑖 ) )
15 eqeq1 ⊢ ( 𝑡 = 𝐴 → ( 𝑡 = ( 𝐹 ‘ 𝑖 ) ↔ 𝐴 = ( 𝐹 ‘ 𝑖 ) ) )
16 15 rexbidv ⊢ ( 𝑡 = 𝐴 → ( ∃ 𝑖 ∈ ( 0 ..^ 3 ) 𝑡 = ( 𝐹 ‘ 𝑖 ) ↔ ∃ 𝑖 ∈ ( 0 ..^ 3 ) 𝐴 = ( 𝐹 ‘ 𝑖 ) ) )
17 14 16 syl5ibrcom ⊢ ( 𝐴 ∈ 𝑉 → ( 𝑡 = 𝐴 → ∃ 𝑖 ∈ ( 0 ..^ 3 ) 𝑡 = ( 𝐹 ‘ 𝑖 ) ) )
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 ⊢ ( 𝐵 ∈ 𝑉 → 1 ∈ ( 0 ..^ 3 ) )
23 fveq2 ⊢ ( 𝑖 = 1 → ( 𝐹 ‘ 𝑖 ) = ( 𝐹 ‘ 1 ) )
24 23 eqeq2d ⊢ ( 𝑖 = 1 → ( 𝐵 = ( 𝐹 ‘ 𝑖 ) ↔ 𝐵 = ( 𝐹 ‘ 1 ) ) )
25 24 adantl ⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝑖 = 1 ) → ( 𝐵 = ( 𝐹 ‘ 𝑖 ) ↔ 𝐵 = ( 𝐹 ‘ 1 ) ) )
26 1 tpf1ofv1 ⊢ ( 𝐵 ∈ 𝑉 → ( 𝐹 ‘ 1 ) = 𝐵 )
27 26 eqcomd ⊢ ( 𝐵 ∈ 𝑉 → 𝐵 = ( 𝐹 ‘ 1 ) )
28 22 25 27 rspcedvd ⊢ ( 𝐵 ∈ 𝑉 → ∃ 𝑖 ∈ ( 0 ..^ 3 ) 𝐵 = ( 𝐹 ‘ 𝑖 ) )
29 eqeq1 ⊢ ( 𝑡 = 𝐵 → ( 𝑡 = ( 𝐹 ‘ 𝑖 ) ↔ 𝐵 = ( 𝐹 ‘ 𝑖 ) ) )
30 29 rexbidv ⊢ ( 𝑡 = 𝐵 → ( ∃ 𝑖 ∈ ( 0 ..^ 3 ) 𝑡 = ( 𝐹 ‘ 𝑖 ) ↔ ∃ 𝑖 ∈ ( 0 ..^ 3 ) 𝐵 = ( 𝐹 ‘ 𝑖 ) ) )
31 28 30 syl5ibrcom ⊢ ( 𝐵 ∈ 𝑉 → ( 𝑡 = 𝐵 → ∃ 𝑖 ∈ ( 0 ..^ 3 ) 𝑡 = ( 𝐹 ‘ 𝑖 ) ) )
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 ⊢ ( 𝐶 ∈ 𝑉 → 2 ∈ ( 0 ..^ 3 ) )
37 fveq2 ⊢ ( 𝑖 = 2 → ( 𝐹 ‘ 𝑖 ) = ( 𝐹 ‘ 2 ) )
38 37 eqeq2d ⊢ ( 𝑖 = 2 → ( 𝐶 = ( 𝐹 ‘ 𝑖 ) ↔ 𝐶 = ( 𝐹 ‘ 2 ) ) )
39 38 adantl ⊢ ( ( 𝐶 ∈ 𝑉 ∧ 𝑖 = 2 ) → ( 𝐶 = ( 𝐹 ‘ 𝑖 ) ↔ 𝐶 = ( 𝐹 ‘ 2 ) ) )
40 1 tpf1ofv2 ⊢ ( 𝐶 ∈ 𝑉 → ( 𝐹 ‘ 2 ) = 𝐶 )
41 40 eqcomd ⊢ ( 𝐶 ∈ 𝑉 → 𝐶 = ( 𝐹 ‘ 2 ) )
42 36 39 41 rspcedvd ⊢ ( 𝐶 ∈ 𝑉 → ∃ 𝑖 ∈ ( 0 ..^ 3 ) 𝐶 = ( 𝐹 ‘ 𝑖 ) )
43 eqeq1 ⊢ ( 𝑡 = 𝐶 → ( 𝑡 = ( 𝐹 ‘ 𝑖 ) ↔ 𝐶 = ( 𝐹 ‘ 𝑖 ) ) )
44 43 rexbidv ⊢ ( 𝑡 = 𝐶 → ( ∃ 𝑖 ∈ ( 0 ..^ 3 ) 𝑡 = ( 𝐹 ‘ 𝑖 ) ↔ ∃ 𝑖 ∈ ( 0 ..^ 3 ) 𝐶 = ( 𝐹 ‘ 𝑖 ) ) )
45 42 44 syl5ibrcom ⊢ ( 𝐶 ∈ 𝑉 → ( 𝑡 = 𝐶 → ∃ 𝑖 ∈ ( 0 ..^ 3 ) 𝑡 = ( 𝐹 ‘ 𝑖 ) ) )
46 17 31 45 3jaao ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → ( ( 𝑡 = 𝐴 ∨ 𝑡 = 𝐵 ∨ 𝑡 = 𝐶 ) → ∃ 𝑖 ∈ ( 0 ..^ 3 ) 𝑡 = ( 𝐹 ‘ 𝑖 ) ) )
47 4 46 syl5com ⊢ ( 𝑡 ∈ { 𝐴 , 𝐵 , 𝐶 } → ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → ∃ 𝑖 ∈ ( 0 ..^ 3 ) 𝑡 = ( 𝐹 ‘ 𝑖 ) ) )
48 47 2 eleq2s ⊢ ( 𝑡 ∈ 𝑇 → ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → ∃ 𝑖 ∈ ( 0 ..^ 3 ) 𝑡 = ( 𝐹 ‘ 𝑖 ) ) )
49 48 com12 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → ( 𝑡 ∈ 𝑇 → ∃ 𝑖 ∈ ( 0 ..^ 3 ) 𝑡 = ( 𝐹 ‘ 𝑖 ) ) )
50 49 ralrimiv ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → ∀ 𝑡 ∈ 𝑇 ∃ 𝑖 ∈ ( 0 ..^ 3 ) 𝑡 = ( 𝐹 ‘ 𝑖 ) )
51 dffo3 ⊢ ( 𝐹 : ( 0 ..^ 3 ) –onto→ 𝑇 ↔ ( 𝐹 : ( 0 ..^ 3 ) ⟶ 𝑇 ∧ ∀ 𝑡 ∈ 𝑇 ∃ 𝑖 ∈ ( 0 ..^ 3 ) 𝑡 = ( 𝐹 ‘ 𝑖 ) ) )
52 3 50 51 sylanbrc ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → 𝐹 : ( 0 ..^ 3 ) –onto→ 𝑇 )