Metamath Proof Explorer

Theorem metakunt21

Description: Show that B coincides on the union of bijections of functions. (Contributed by metakunt, 28-May-2024)

Ref Expression
Hypotheses metakunt21.1 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
metakunt21.2 ⊢ ( 𝜑 → 𝐼 ∈ ℕ )
metakunt21.3 ⊢ ( 𝜑 → 𝐼 ≤ 𝑀 )
metakunt21.4 ⊢ 𝐵 = ( 𝑥 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑥 = 𝑀 , 𝑀 , if ( 𝑥 < 𝐼 , ( 𝑥 + ( 𝑀 − 𝐼 ) ) , ( 𝑥 + ( 1 − 𝐼 ) ) ) ) )
metakunt21.5 ⊢ 𝐶 = ( 𝑥 ∈ ( 1 ... ( 𝐼 − 1 ) ) ↦ ( 𝑥 + ( 𝑀 − 𝐼 ) ) )
metakunt21.6 ⊢ 𝐷 = ( 𝑥 ∈ ( 𝐼 ... ( 𝑀 − 1 ) ) ↦ ( 𝑥 + ( 1 − 𝐼 ) ) )
metakunt21.7 ⊢ ( 𝜑 → 𝑋 ∈ ( 1 ... 𝑀 ) )
metakunt21.8 ⊢ ( 𝜑 → ¬ 𝑋 = 𝑀 )
metakunt21.9 ⊢ ( 𝜑 → 𝑋 < 𝐼 )
Assertion metakunt21 ( 𝜑 → ( 𝐵 ‘ 𝑋 ) = ( ( ( 𝐶 ∪ 𝐷 ) ∪ { ⟨ 𝑀 , 𝑀 ⟩ } ) ‘ 𝑋 ) )

Proof

Step Hyp Ref Expression
1 metakunt21.1 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
2 metakunt21.2 ⊢ ( 𝜑 → 𝐼 ∈ ℕ )
3 metakunt21.3 ⊢ ( 𝜑 → 𝐼 ≤ 𝑀 )
4 metakunt21.4 ⊢ 𝐵 = ( 𝑥 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑥 = 𝑀 , 𝑀 , if ( 𝑥 < 𝐼 , ( 𝑥 + ( 𝑀 − 𝐼 ) ) , ( 𝑥 + ( 1 − 𝐼 ) ) ) ) )
5 metakunt21.5 ⊢ 𝐶 = ( 𝑥 ∈ ( 1 ... ( 𝐼 − 1 ) ) ↦ ( 𝑥 + ( 𝑀 − 𝐼 ) ) )
6 metakunt21.6 ⊢ 𝐷 = ( 𝑥 ∈ ( 𝐼 ... ( 𝑀 − 1 ) ) ↦ ( 𝑥 + ( 1 − 𝐼 ) ) )
7 metakunt21.7 ⊢ ( 𝜑 → 𝑋 ∈ ( 1 ... 𝑀 ) )
8 metakunt21.8 ⊢ ( 𝜑 → ¬ 𝑋 = 𝑀 )
9 metakunt21.9 ⊢ ( 𝜑 → 𝑋 < 𝐼 )
10 4 a1i ⊢ ( 𝜑 → 𝐵 = ( 𝑥 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑥 = 𝑀 , 𝑀 , if ( 𝑥 < 𝐼 , ( 𝑥 + ( 𝑀 − 𝐼 ) ) , ( 𝑥 + ( 1 − 𝐼 ) ) ) ) ) )
11 eqeq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 = 𝑀 ↔ 𝑋 = 𝑀 ) )
12 breq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 < 𝐼 ↔ 𝑋 < 𝐼 ) )
13 oveq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 + ( 𝑀 − 𝐼 ) ) = ( 𝑋 + ( 𝑀 − 𝐼 ) ) )
14 oveq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 + ( 1 − 𝐼 ) ) = ( 𝑋 + ( 1 − 𝐼 ) ) )
15 12 13 14 ifbieq12d ⊢ ( 𝑥 = 𝑋 → if ( 𝑥 < 𝐼 , ( 𝑥 + ( 𝑀 − 𝐼 ) ) , ( 𝑥 + ( 1 − 𝐼 ) ) ) = if ( 𝑋 < 𝐼 , ( 𝑋 + ( 𝑀 − 𝐼 ) ) , ( 𝑋 + ( 1 − 𝐼 ) ) ) )
16 11 15 ifbieq2d ⊢ ( 𝑥 = 𝑋 → if ( 𝑥 = 𝑀 , 𝑀 , if ( 𝑥 < 𝐼 , ( 𝑥 + ( 𝑀 − 𝐼 ) ) , ( 𝑥 + ( 1 − 𝐼 ) ) ) ) = if ( 𝑋 = 𝑀 , 𝑀 , if ( 𝑋 < 𝐼 , ( 𝑋 + ( 𝑀 − 𝐼 ) ) , ( 𝑋 + ( 1 − 𝐼 ) ) ) ) )
17 16 adantl ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → if ( 𝑥 = 𝑀 , 𝑀 , if ( 𝑥 < 𝐼 , ( 𝑥 + ( 𝑀 − 𝐼 ) ) , ( 𝑥 + ( 1 − 𝐼 ) ) ) ) = if ( 𝑋 = 𝑀 , 𝑀 , if ( 𝑋 < 𝐼 , ( 𝑋 + ( 𝑀 − 𝐼 ) ) , ( 𝑋 + ( 1 − 𝐼 ) ) ) ) )
18 8 iffalsed ⊢ ( 𝜑 → if ( 𝑋 = 𝑀 , 𝑀 , if ( 𝑋 < 𝐼 , ( 𝑋 + ( 𝑀 − 𝐼 ) ) , ( 𝑋 + ( 1 − 𝐼 ) ) ) ) = if ( 𝑋 < 𝐼 , ( 𝑋 + ( 𝑀 − 𝐼 ) ) , ( 𝑋 + ( 1 − 𝐼 ) ) ) )
19 9 iftrued ⊢ ( 𝜑 → if ( 𝑋 < 𝐼 , ( 𝑋 + ( 𝑀 − 𝐼 ) ) , ( 𝑋 + ( 1 − 𝐼 ) ) ) = ( 𝑋 + ( 𝑀 − 𝐼 ) ) )
20 18 19 eqtrd ⊢ ( 𝜑 → if ( 𝑋 = 𝑀 , 𝑀 , if ( 𝑋 < 𝐼 , ( 𝑋 + ( 𝑀 − 𝐼 ) ) , ( 𝑋 + ( 1 − 𝐼 ) ) ) ) = ( 𝑋 + ( 𝑀 − 𝐼 ) ) )
21 20 adantr ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → if ( 𝑋 = 𝑀 , 𝑀 , if ( 𝑋 < 𝐼 , ( 𝑋 + ( 𝑀 − 𝐼 ) ) , ( 𝑋 + ( 1 − 𝐼 ) ) ) ) = ( 𝑋 + ( 𝑀 − 𝐼 ) ) )
22 17 21 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → if ( 𝑥 = 𝑀 , 𝑀 , if ( 𝑥 < 𝐼 , ( 𝑥 + ( 𝑀 − 𝐼 ) ) , ( 𝑥 + ( 1 − 𝐼 ) ) ) ) = ( 𝑋 + ( 𝑀 − 𝐼 ) ) )
23 7 elfzelzd ⊢ ( 𝜑 → 𝑋 ∈ ℤ )
24 1 nnzd ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
25 2 nnzd ⊢ ( 𝜑 → 𝐼 ∈ ℤ )
26 24 25 zsubcld ⊢ ( 𝜑 → ( 𝑀 − 𝐼 ) ∈ ℤ )
27 23 26 zaddcld ⊢ ( 𝜑 → ( 𝑋 + ( 𝑀 − 𝐼 ) ) ∈ ℤ )
28 10 22 7 27 fvmptd ⊢ ( 𝜑 → ( 𝐵 ‘ 𝑋 ) = ( 𝑋 + ( 𝑀 − 𝐼 ) ) )
29 1 2 3 4 5 6 metakunt19 ⊢ ( 𝜑 → ( ( 𝐶 Fn ( 1 ... ( 𝐼 − 1 ) ) ∧ 𝐷 Fn ( 𝐼 ... ( 𝑀 − 1 ) ) ∧ ( 𝐶 ∪ 𝐷 ) Fn ( ( 1 ... ( 𝐼 − 1 ) ) ∪ ( 𝐼 ... ( 𝑀 − 1 ) ) ) ) ∧ { ⟨ 𝑀 , 𝑀 ⟩ } Fn { 𝑀 } ) )
30 29 simpld ⊢ ( 𝜑 → ( 𝐶 Fn ( 1 ... ( 𝐼 − 1 ) ) ∧ 𝐷 Fn ( 𝐼 ... ( 𝑀 − 1 ) ) ∧ ( 𝐶 ∪ 𝐷 ) Fn ( ( 1 ... ( 𝐼 − 1 ) ) ∪ ( 𝐼 ... ( 𝑀 − 1 ) ) ) ) )
31 30 simp3d ⊢ ( 𝜑 → ( 𝐶 ∪ 𝐷 ) Fn ( ( 1 ... ( 𝐼 − 1 ) ) ∪ ( 𝐼 ... ( 𝑀 − 1 ) ) ) )
32 29 simprd ⊢ ( 𝜑 → { ⟨ 𝑀 , 𝑀 ⟩ } Fn { 𝑀 } )
33 indir ⊢ ( ( ( 1 ... ( 𝐼 − 1 ) ) ∪ ( 𝐼 ... ( 𝑀 − 1 ) ) ) ∩ { 𝑀 } ) = ( ( ( 1 ... ( 𝐼 − 1 ) ) ∩ { 𝑀 } ) ∪ ( ( 𝐼 ... ( 𝑀 − 1 ) ) ∩ { 𝑀 } ) )
34 33 a1i ⊢ ( 𝜑 → ( ( ( 1 ... ( 𝐼 − 1 ) ) ∪ ( 𝐼 ... ( 𝑀 − 1 ) ) ) ∩ { 𝑀 } ) = ( ( ( 1 ... ( 𝐼 − 1 ) ) ∩ { 𝑀 } ) ∪ ( ( 𝐼 ... ( 𝑀 − 1 ) ) ∩ { 𝑀 } ) ) )
35 1 2 3 metakunt18 ⊢ ( 𝜑 → ( ( ( ( 1 ... ( 𝐼 − 1 ) ) ∩ ( 𝐼 ... ( 𝑀 − 1 ) ) ) = ∅ ∧ ( ( 1 ... ( 𝐼 − 1 ) ) ∩ { 𝑀 } ) = ∅ ∧ ( ( 𝐼 ... ( 𝑀 − 1 ) ) ∩ { 𝑀 } ) = ∅ ) ∧ ( ( ( ( ( 𝑀 − 𝐼 ) + 1 ) ... ( 𝑀 − 1 ) ) ∩ ( 1 ... ( 𝑀 − 𝐼 ) ) ) = ∅ ∧ ( ( ( ( 𝑀 − 𝐼 ) + 1 ) ... ( 𝑀 − 1 ) ) ∩ { 𝑀 } ) = ∅ ∧ ( ( 1 ... ( 𝑀 − 𝐼 ) ) ∩ { 𝑀 } ) = ∅ ) ) )
36 35 simpld ⊢ ( 𝜑 → ( ( ( 1 ... ( 𝐼 − 1 ) ) ∩ ( 𝐼 ... ( 𝑀 − 1 ) ) ) = ∅ ∧ ( ( 1 ... ( 𝐼 − 1 ) ) ∩ { 𝑀 } ) = ∅ ∧ ( ( 𝐼 ... ( 𝑀 − 1 ) ) ∩ { 𝑀 } ) = ∅ ) )
37 36 simp2d ⊢ ( 𝜑 → ( ( 1 ... ( 𝐼 − 1 ) ) ∩ { 𝑀 } ) = ∅ )
38 36 simp3d ⊢ ( 𝜑 → ( ( 𝐼 ... ( 𝑀 − 1 ) ) ∩ { 𝑀 } ) = ∅ )
39 37 38 uneq12d ⊢ ( 𝜑 → ( ( ( 1 ... ( 𝐼 − 1 ) ) ∩ { 𝑀 } ) ∪ ( ( 𝐼 ... ( 𝑀 − 1 ) ) ∩ { 𝑀 } ) ) = ( ∅ ∪ ∅ ) )
40 unidm ⊢ ( ∅ ∪ ∅ ) = ∅
41 40 a1i ⊢ ( 𝜑 → ( ∅ ∪ ∅ ) = ∅ )
42 39 41 eqtrd ⊢ ( 𝜑 → ( ( ( 1 ... ( 𝐼 − 1 ) ) ∩ { 𝑀 } ) ∪ ( ( 𝐼 ... ( 𝑀 − 1 ) ) ∩ { 𝑀 } ) ) = ∅ )
43 34 42 eqtrd ⊢ ( 𝜑 → ( ( ( 1 ... ( 𝐼 − 1 ) ) ∪ ( 𝐼 ... ( 𝑀 − 1 ) ) ) ∩ { 𝑀 } ) = ∅ )
44 1zzd ⊢ ( 𝜑 → 1 ∈ ℤ )
45 25 44 zsubcld ⊢ ( 𝜑 → ( 𝐼 − 1 ) ∈ ℤ )
46 elfznn ⊢ ( 𝑋 ∈ ( 1 ... 𝑀 ) → 𝑋 ∈ ℕ )
47 7 46 syl ⊢ ( 𝜑 → 𝑋 ∈ ℕ )
48 47 nnge1d ⊢ ( 𝜑 → 1 ≤ 𝑋 )
49 zltlem1 ⊢ ( ( 𝑋 ∈ ℤ ∧ 𝐼 ∈ ℤ ) → ( 𝑋 < 𝐼 ↔ 𝑋 ≤ ( 𝐼 − 1 ) ) )
50 23 25 49 syl2anc ⊢ ( 𝜑 → ( 𝑋 < 𝐼 ↔ 𝑋 ≤ ( 𝐼 − 1 ) ) )
51 9 50 mpbid ⊢ ( 𝜑 → 𝑋 ≤ ( 𝐼 − 1 ) )
52 44 45 23 48 51 elfzd ⊢ ( 𝜑 → 𝑋 ∈ ( 1 ... ( 𝐼 − 1 ) ) )
53 elun1 ⊢ ( 𝑋 ∈ ( 1 ... ( 𝐼 − 1 ) ) → 𝑋 ∈ ( ( 1 ... ( 𝐼 − 1 ) ) ∪ ( 𝐼 ... ( 𝑀 − 1 ) ) ) )
54 52 53 syl ⊢ ( 𝜑 → 𝑋 ∈ ( ( 1 ... ( 𝐼 − 1 ) ) ∪ ( 𝐼 ... ( 𝑀 − 1 ) ) ) )
55 31 32 43 54 fvun1d ⊢ ( 𝜑 → ( ( ( 𝐶 ∪ 𝐷 ) ∪ { ⟨ 𝑀 , 𝑀 ⟩ } ) ‘ 𝑋 ) = ( ( 𝐶 ∪ 𝐷 ) ‘ 𝑋 ) )
56 30 simp1d ⊢ ( 𝜑 → 𝐶 Fn ( 1 ... ( 𝐼 − 1 ) ) )
57 30 simp2d ⊢ ( 𝜑 → 𝐷 Fn ( 𝐼 ... ( 𝑀 − 1 ) ) )
58 36 simp1d ⊢ ( 𝜑 → ( ( 1 ... ( 𝐼 − 1 ) ) ∩ ( 𝐼 ... ( 𝑀 − 1 ) ) ) = ∅ )
59 56 57 58 52 fvun1d ⊢ ( 𝜑 → ( ( 𝐶 ∪ 𝐷 ) ‘ 𝑋 ) = ( 𝐶 ‘ 𝑋 ) )
60 5 a1i ⊢ ( 𝜑 → 𝐶 = ( 𝑥 ∈ ( 1 ... ( 𝐼 − 1 ) ) ↦ ( 𝑥 + ( 𝑀 − 𝐼 ) ) ) )
61 13 adantl ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ( 𝑥 + ( 𝑀 − 𝐼 ) ) = ( 𝑋 + ( 𝑀 − 𝐼 ) ) )
62 60 61 52 27 fvmptd ⊢ ( 𝜑 → ( 𝐶 ‘ 𝑋 ) = ( 𝑋 + ( 𝑀 − 𝐼 ) ) )
63 59 62 eqtrd ⊢ ( 𝜑 → ( ( 𝐶 ∪ 𝐷 ) ‘ 𝑋 ) = ( 𝑋 + ( 𝑀 − 𝐼 ) ) )
64 55 63 eqtrd ⊢ ( 𝜑 → ( ( ( 𝐶 ∪ 𝐷 ) ∪ { ⟨ 𝑀 , 𝑀 ⟩ } ) ‘ 𝑋 ) = ( 𝑋 + ( 𝑀 − 𝐼 ) ) )
65 64 eqcomd ⊢ ( 𝜑 → ( 𝑋 + ( 𝑀 − 𝐼 ) ) = ( ( ( 𝐶 ∪ 𝐷 ) ∪ { ⟨ 𝑀 , 𝑀 ⟩ } ) ‘ 𝑋 ) )
66 28 65 eqtrd ⊢ ( 𝜑 → ( 𝐵 ‘ 𝑋 ) = ( ( ( 𝐶 ∪ 𝐷 ) ∪ { ⟨ 𝑀 , 𝑀 ⟩ } ) ‘ 𝑋 ) )