Metamath Proof Explorer

Theorem metakunt22

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

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

Proof

Step Hyp Ref Expression
1 metakunt22.1 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
2 metakunt22.2 ⊢ ( 𝜑 → 𝐼 ∈ ℕ )
3 metakunt22.3 ⊢ ( 𝜑 → 𝐼 ≤ 𝑀 )
4 metakunt22.4 ⊢ 𝐵 = ( 𝑥 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑥 = 𝑀 , 𝑀 , if ( 𝑥 < 𝐼 , ( 𝑥 + ( 𝑀 − 𝐼 ) ) , ( 𝑥 + ( 1 − 𝐼 ) ) ) ) )
5 metakunt22.5 ⊢ 𝐶 = ( 𝑥 ∈ ( 1 ... ( 𝐼 − 1 ) ) ↦ ( 𝑥 + ( 𝑀 − 𝐼 ) ) )
6 metakunt22.6 ⊢ 𝐷 = ( 𝑥 ∈ ( 𝐼 ... ( 𝑀 − 1 ) ) ↦ ( 𝑥 + ( 1 − 𝐼 ) ) )
7 metakunt22.7 ⊢ ( 𝜑 → 𝑋 ∈ ( 1 ... 𝑀 ) )
8 metakunt22.8 ⊢ ( 𝜑 → ¬ 𝑋 = 𝑀 )
9 metakunt22.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 iffalse ⊢ ( ¬ 𝑋 = 𝑀 → if ( 𝑋 = 𝑀 , 𝑀 , if ( 𝑋 < 𝐼 , ( 𝑋 + ( 𝑀 − 𝐼 ) ) , ( 𝑋 + ( 1 − 𝐼 ) ) ) ) = if ( 𝑋 < 𝐼 , ( 𝑋 + ( 𝑀 − 𝐼 ) ) , ( 𝑋 + ( 1 − 𝐼 ) ) ) )
19 8 18 syl ⊢ ( 𝜑 → if ( 𝑋 = 𝑀 , 𝑀 , if ( 𝑋 < 𝐼 , ( 𝑋 + ( 𝑀 − 𝐼 ) ) , ( 𝑋 + ( 1 − 𝐼 ) ) ) ) = if ( 𝑋 < 𝐼 , ( 𝑋 + ( 𝑀 − 𝐼 ) ) , ( 𝑋 + ( 1 − 𝐼 ) ) ) )
20 iffalse ⊢ ( ¬ 𝑋 < 𝐼 → if ( 𝑋 < 𝐼 , ( 𝑋 + ( 𝑀 − 𝐼 ) ) , ( 𝑋 + ( 1 − 𝐼 ) ) ) = ( 𝑋 + ( 1 − 𝐼 ) ) )
21 9 20 syl ⊢ ( 𝜑 → if ( 𝑋 < 𝐼 , ( 𝑋 + ( 𝑀 − 𝐼 ) ) , ( 𝑋 + ( 1 − 𝐼 ) ) ) = ( 𝑋 + ( 1 − 𝐼 ) ) )
22 19 21 eqtrd ⊢ ( 𝜑 → if ( 𝑋 = 𝑀 , 𝑀 , if ( 𝑋 < 𝐼 , ( 𝑋 + ( 𝑀 − 𝐼 ) ) , ( 𝑋 + ( 1 − 𝐼 ) ) ) ) = ( 𝑋 + ( 1 − 𝐼 ) ) )
23 22 adantr ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → if ( 𝑋 = 𝑀 , 𝑀 , if ( 𝑋 < 𝐼 , ( 𝑋 + ( 𝑀 − 𝐼 ) ) , ( 𝑋 + ( 1 − 𝐼 ) ) ) ) = ( 𝑋 + ( 1 − 𝐼 ) ) )
24 17 23 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → if ( 𝑥 = 𝑀 , 𝑀 , if ( 𝑥 < 𝐼 , ( 𝑥 + ( 𝑀 − 𝐼 ) ) , ( 𝑥 + ( 1 − 𝐼 ) ) ) ) = ( 𝑋 + ( 1 − 𝐼 ) ) )
25 7 elfzelzd ⊢ ( 𝜑 → 𝑋 ∈ ℤ )
26 1zzd ⊢ ( 𝜑 → 1 ∈ ℤ )
27 2 nnzd ⊢ ( 𝜑 → 𝐼 ∈ ℤ )
28 26 27 zsubcld ⊢ ( 𝜑 → ( 1 − 𝐼 ) ∈ ℤ )
29 25 28 zaddcld ⊢ ( 𝜑 → ( 𝑋 + ( 1 − 𝐼 ) ) ∈ ℤ )
30 10 24 7 29 fvmptd ⊢ ( 𝜑 → ( 𝐵 ‘ 𝑋 ) = ( 𝑋 + ( 1 − 𝐼 ) ) )
31 1 2 3 4 5 6 metakunt19 ⊢ ( 𝜑 → ( ( 𝐶 Fn ( 1 ... ( 𝐼 − 1 ) ) ∧ 𝐷 Fn ( 𝐼 ... ( 𝑀 − 1 ) ) ∧ ( 𝐶 ∪ 𝐷 ) Fn ( ( 1 ... ( 𝐼 − 1 ) ) ∪ ( 𝐼 ... ( 𝑀 − 1 ) ) ) ) ∧ { ⟨ 𝑀 , 𝑀 ⟩ } Fn { 𝑀 } ) )
32 31 simpld ⊢ ( 𝜑 → ( 𝐶 Fn ( 1 ... ( 𝐼 − 1 ) ) ∧ 𝐷 Fn ( 𝐼 ... ( 𝑀 − 1 ) ) ∧ ( 𝐶 ∪ 𝐷 ) Fn ( ( 1 ... ( 𝐼 − 1 ) ) ∪ ( 𝐼 ... ( 𝑀 − 1 ) ) ) ) )
33 32 simp3d ⊢ ( 𝜑 → ( 𝐶 ∪ 𝐷 ) Fn ( ( 1 ... ( 𝐼 − 1 ) ) ∪ ( 𝐼 ... ( 𝑀 − 1 ) ) ) )
34 31 simprd ⊢ ( 𝜑 → { ⟨ 𝑀 , 𝑀 ⟩ } Fn { 𝑀 } )
35 indir ⊢ ( ( ( 1 ... ( 𝐼 − 1 ) ) ∪ ( 𝐼 ... ( 𝑀 − 1 ) ) ) ∩ { 𝑀 } ) = ( ( ( 1 ... ( 𝐼 − 1 ) ) ∩ { 𝑀 } ) ∪ ( ( 𝐼 ... ( 𝑀 − 1 ) ) ∩ { 𝑀 } ) )
36 35 a1i ⊢ ( 𝜑 → ( ( ( 1 ... ( 𝐼 − 1 ) ) ∪ ( 𝐼 ... ( 𝑀 − 1 ) ) ) ∩ { 𝑀 } ) = ( ( ( 1 ... ( 𝐼 − 1 ) ) ∩ { 𝑀 } ) ∪ ( ( 𝐼 ... ( 𝑀 − 1 ) ) ∩ { 𝑀 } ) ) )
37 1 2 3 metakunt18 ⊢ ( 𝜑 → ( ( ( ( 1 ... ( 𝐼 − 1 ) ) ∩ ( 𝐼 ... ( 𝑀 − 1 ) ) ) = ∅ ∧ ( ( 1 ... ( 𝐼 − 1 ) ) ∩ { 𝑀 } ) = ∅ ∧ ( ( 𝐼 ... ( 𝑀 − 1 ) ) ∩ { 𝑀 } ) = ∅ ) ∧ ( ( ( ( ( 𝑀 − 𝐼 ) + 1 ) ... ( 𝑀 − 1 ) ) ∩ ( 1 ... ( 𝑀 − 𝐼 ) ) ) = ∅ ∧ ( ( ( ( 𝑀 − 𝐼 ) + 1 ) ... ( 𝑀 − 1 ) ) ∩ { 𝑀 } ) = ∅ ∧ ( ( 1 ... ( 𝑀 − 𝐼 ) ) ∩ { 𝑀 } ) = ∅ ) ) )
38 37 simpld ⊢ ( 𝜑 → ( ( ( 1 ... ( 𝐼 − 1 ) ) ∩ ( 𝐼 ... ( 𝑀 − 1 ) ) ) = ∅ ∧ ( ( 1 ... ( 𝐼 − 1 ) ) ∩ { 𝑀 } ) = ∅ ∧ ( ( 𝐼 ... ( 𝑀 − 1 ) ) ∩ { 𝑀 } ) = ∅ ) )
39 38 simp2d ⊢ ( 𝜑 → ( ( 1 ... ( 𝐼 − 1 ) ) ∩ { 𝑀 } ) = ∅ )
40 38 simp3d ⊢ ( 𝜑 → ( ( 𝐼 ... ( 𝑀 − 1 ) ) ∩ { 𝑀 } ) = ∅ )
41 39 40 uneq12d ⊢ ( 𝜑 → ( ( ( 1 ... ( 𝐼 − 1 ) ) ∩ { 𝑀 } ) ∪ ( ( 𝐼 ... ( 𝑀 − 1 ) ) ∩ { 𝑀 } ) ) = ( ∅ ∪ ∅ ) )
42 unidm ⊢ ( ∅ ∪ ∅ ) = ∅
43 42 a1i ⊢ ( 𝜑 → ( ∅ ∪ ∅ ) = ∅ )
44 41 43 eqtrd ⊢ ( 𝜑 → ( ( ( 1 ... ( 𝐼 − 1 ) ) ∩ { 𝑀 } ) ∪ ( ( 𝐼 ... ( 𝑀 − 1 ) ) ∩ { 𝑀 } ) ) = ∅ )
45 36 44 eqtrd ⊢ ( 𝜑 → ( ( ( 1 ... ( 𝐼 − 1 ) ) ∪ ( 𝐼 ... ( 𝑀 − 1 ) ) ) ∩ { 𝑀 } ) = ∅ )
46 1 nnzd ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
47 46 26 zsubcld ⊢ ( 𝜑 → ( 𝑀 − 1 ) ∈ ℤ )
48 elfznn ⊢ ( 𝑋 ∈ ( 1 ... 𝑀 ) → 𝑋 ∈ ℕ )
49 7 48 syl ⊢ ( 𝜑 → 𝑋 ∈ ℕ )
50 49 nnzd ⊢ ( 𝜑 → 𝑋 ∈ ℤ )
51 2 nnred ⊢ ( 𝜑 → 𝐼 ∈ ℝ )
52 49 nnred ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
53 51 52 lenltd ⊢ ( 𝜑 → ( 𝐼 ≤ 𝑋 ↔ ¬ 𝑋 < 𝐼 ) )
54 9 53 mpbird ⊢ ( 𝜑 → 𝐼 ≤ 𝑋 )
55 elfzle2 ⊢ ( 𝑋 ∈ ( 1 ... 𝑀 ) → 𝑋 ≤ 𝑀 )
56 7 55 syl ⊢ ( 𝜑 → 𝑋 ≤ 𝑀 )
57 df-ne ⊢ ( 𝑋 ≠ 𝑀 ↔ ¬ 𝑋 = 𝑀 )
58 8 57 sylibr ⊢ ( 𝜑 → 𝑋 ≠ 𝑀 )
59 58 necomd ⊢ ( 𝜑 → 𝑀 ≠ 𝑋 )
60 56 59 jca ⊢ ( 𝜑 → ( 𝑋 ≤ 𝑀 ∧ 𝑀 ≠ 𝑋 ) )
61 1 nnred ⊢ ( 𝜑 → 𝑀 ∈ ℝ )
62 52 61 ltlend ⊢ ( 𝜑 → ( 𝑋 < 𝑀 ↔ ( 𝑋 ≤ 𝑀 ∧ 𝑀 ≠ 𝑋 ) ) )
63 60 62 mpbird ⊢ ( 𝜑 → 𝑋 < 𝑀 )
64 zltlem1 ⊢ ( ( 𝑋 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝑋 < 𝑀 ↔ 𝑋 ≤ ( 𝑀 − 1 ) ) )
65 50 46 64 syl2anc ⊢ ( 𝜑 → ( 𝑋 < 𝑀 ↔ 𝑋 ≤ ( 𝑀 − 1 ) ) )
66 63 65 mpbid ⊢ ( 𝜑 → 𝑋 ≤ ( 𝑀 − 1 ) )
67 27 47 50 54 66 elfzd ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐼 ... ( 𝑀 − 1 ) ) )
68 elun2 ⊢ ( 𝑋 ∈ ( 𝐼 ... ( 𝑀 − 1 ) ) → 𝑋 ∈ ( ( 1 ... ( 𝐼 − 1 ) ) ∪ ( 𝐼 ... ( 𝑀 − 1 ) ) ) )
69 67 68 syl ⊢ ( 𝜑 → 𝑋 ∈ ( ( 1 ... ( 𝐼 − 1 ) ) ∪ ( 𝐼 ... ( 𝑀 − 1 ) ) ) )
70 33 34 45 69 fvun1d ⊢ ( 𝜑 → ( ( ( 𝐶 ∪ 𝐷 ) ∪ { ⟨ 𝑀 , 𝑀 ⟩ } ) ‘ 𝑋 ) = ( ( 𝐶 ∪ 𝐷 ) ‘ 𝑋 ) )
71 32 simp1d ⊢ ( 𝜑 → 𝐶 Fn ( 1 ... ( 𝐼 − 1 ) ) )
72 32 simp2d ⊢ ( 𝜑 → 𝐷 Fn ( 𝐼 ... ( 𝑀 − 1 ) ) )
73 38 simp1d ⊢ ( 𝜑 → ( ( 1 ... ( 𝐼 − 1 ) ) ∩ ( 𝐼 ... ( 𝑀 − 1 ) ) ) = ∅ )
74 71 72 73 67 fvun2d ⊢ ( 𝜑 → ( ( 𝐶 ∪ 𝐷 ) ‘ 𝑋 ) = ( 𝐷 ‘ 𝑋 ) )
75 6 a1i ⊢ ( 𝜑 → 𝐷 = ( 𝑥 ∈ ( 𝐼 ... ( 𝑀 − 1 ) ) ↦ ( 𝑥 + ( 1 − 𝐼 ) ) ) )
76 simpr ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → 𝑥 = 𝑋 )
77 76 oveq1d ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ( 𝑥 + ( 1 − 𝐼 ) ) = ( 𝑋 + ( 1 − 𝐼 ) ) )
78 25 zred ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
79 lenlt ⊢ ( ( 𝐼 ∈ ℝ ∧ 𝑋 ∈ ℝ ) → ( 𝐼 ≤ 𝑋 ↔ ¬ 𝑋 < 𝐼 ) )
80 51 78 79 syl2anc ⊢ ( 𝜑 → ( 𝐼 ≤ 𝑋 ↔ ¬ 𝑋 < 𝐼 ) )
81 9 80 mpbird ⊢ ( 𝜑 → 𝐼 ≤ 𝑋 )
82 78 61 ltlend ⊢ ( 𝜑 → ( 𝑋 < 𝑀 ↔ ( 𝑋 ≤ 𝑀 ∧ 𝑀 ≠ 𝑋 ) ) )
83 60 82 mpbird ⊢ ( 𝜑 → 𝑋 < 𝑀 )
84 25 46 64 syl2anc ⊢ ( 𝜑 → ( 𝑋 < 𝑀 ↔ 𝑋 ≤ ( 𝑀 − 1 ) ) )
85 83 84 mpbid ⊢ ( 𝜑 → 𝑋 ≤ ( 𝑀 − 1 ) )
86 27 47 25 81 85 elfzd ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐼 ... ( 𝑀 − 1 ) ) )
87 75 77 86 29 fvmptd ⊢ ( 𝜑 → ( 𝐷 ‘ 𝑋 ) = ( 𝑋 + ( 1 − 𝐼 ) ) )
88 74 87 eqtrd ⊢ ( 𝜑 → ( ( 𝐶 ∪ 𝐷 ) ‘ 𝑋 ) = ( 𝑋 + ( 1 − 𝐼 ) ) )
89 70 88 eqtrd ⊢ ( 𝜑 → ( ( ( 𝐶 ∪ 𝐷 ) ∪ { ⟨ 𝑀 , 𝑀 ⟩ } ) ‘ 𝑋 ) = ( 𝑋 + ( 1 − 𝐼 ) ) )
90 89 eqcomd ⊢ ( 𝜑 → ( 𝑋 + ( 1 − 𝐼 ) ) = ( ( ( 𝐶 ∪ 𝐷 ) ∪ { ⟨ 𝑀 , 𝑀 ⟩ } ) ‘ 𝑋 ) )
91 30 90 eqtrd ⊢ ( 𝜑 → ( 𝐵 ‘ 𝑋 ) = ( ( ( 𝐶 ∪ 𝐷 ) ∪ { ⟨ 𝑀 , 𝑀 ⟩ } ) ‘ 𝑋 ) )