Metamath Proof Explorer

Theorem metakunt20

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

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

Proof

Step Hyp Ref Expression
1 metakunt20.1 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
2 metakunt20.2 ⊢ ( 𝜑 → 𝐼 ∈ ℕ )
3 metakunt20.3 ⊢ ( 𝜑 → 𝐼 ≤ 𝑀 )
4 metakunt20.4 ⊢ 𝐵 = ( 𝑥 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑥 = 𝑀 , 𝑀 , if ( 𝑥 < 𝐼 , ( 𝑥 + ( 𝑀 − 𝐼 ) ) , ( 𝑥 + ( 1 − 𝐼 ) ) ) ) )
5 metakunt20.5 ⊢ 𝐶 = ( 𝑥 ∈ ( 1 ... ( 𝐼 − 1 ) ) ↦ ( 𝑥 + ( 𝑀 − 𝐼 ) ) )
6 metakunt20.6 ⊢ 𝐷 = ( 𝑥 ∈ ( 𝐼 ... ( 𝑀 − 1 ) ) ↦ ( 𝑥 + ( 1 − 𝐼 ) ) )
7 metakunt20.7 ⊢ ( 𝜑 → 𝑋 ∈ ( 1 ... 𝑀 ) )
8 metakunt20.8 ⊢ ( 𝜑 → 𝑋 = 𝑀 )
9 4 a1i ⊢ ( 𝜑 → 𝐵 = ( 𝑥 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑥 = 𝑀 , 𝑀 , if ( 𝑥 < 𝐼 , ( 𝑥 + ( 𝑀 − 𝐼 ) ) , ( 𝑥 + ( 1 − 𝐼 ) ) ) ) ) )
10 eqeq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 = 𝑀 ↔ 𝑋 = 𝑀 ) )
11 breq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 < 𝐼 ↔ 𝑋 < 𝐼 ) )
12 oveq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 + ( 𝑀 − 𝐼 ) ) = ( 𝑋 + ( 𝑀 − 𝐼 ) ) )
13 oveq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 + ( 1 − 𝐼 ) ) = ( 𝑋 + ( 1 − 𝐼 ) ) )
14 11 12 13 ifbieq12d ⊢ ( 𝑥 = 𝑋 → if ( 𝑥 < 𝐼 , ( 𝑥 + ( 𝑀 − 𝐼 ) ) , ( 𝑥 + ( 1 − 𝐼 ) ) ) = if ( 𝑋 < 𝐼 , ( 𝑋 + ( 𝑀 − 𝐼 ) ) , ( 𝑋 + ( 1 − 𝐼 ) ) ) )
15 10 14 ifbieq2d ⊢ ( 𝑥 = 𝑋 → if ( 𝑥 = 𝑀 , 𝑀 , if ( 𝑥 < 𝐼 , ( 𝑥 + ( 𝑀 − 𝐼 ) ) , ( 𝑥 + ( 1 − 𝐼 ) ) ) ) = if ( 𝑋 = 𝑀 , 𝑀 , if ( 𝑋 < 𝐼 , ( 𝑋 + ( 𝑀 − 𝐼 ) ) , ( 𝑋 + ( 1 − 𝐼 ) ) ) ) )
16 15 adantl ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → if ( 𝑥 = 𝑀 , 𝑀 , if ( 𝑥 < 𝐼 , ( 𝑥 + ( 𝑀 − 𝐼 ) ) , ( 𝑥 + ( 1 − 𝐼 ) ) ) ) = if ( 𝑋 = 𝑀 , 𝑀 , if ( 𝑋 < 𝐼 , ( 𝑋 + ( 𝑀 − 𝐼 ) ) , ( 𝑋 + ( 1 − 𝐼 ) ) ) ) )
17 iftrue ⊢ ( 𝑋 = 𝑀 → if ( 𝑋 = 𝑀 , 𝑀 , if ( 𝑋 < 𝐼 , ( 𝑋 + ( 𝑀 − 𝐼 ) ) , ( 𝑋 + ( 1 − 𝐼 ) ) ) ) = 𝑀 )
18 8 17 syl ⊢ ( 𝜑 → if ( 𝑋 = 𝑀 , 𝑀 , if ( 𝑋 < 𝐼 , ( 𝑋 + ( 𝑀 − 𝐼 ) ) , ( 𝑋 + ( 1 − 𝐼 ) ) ) ) = 𝑀 )
19 18 adantr ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → if ( 𝑋 = 𝑀 , 𝑀 , if ( 𝑋 < 𝐼 , ( 𝑋 + ( 𝑀 − 𝐼 ) ) , ( 𝑋 + ( 1 − 𝐼 ) ) ) ) = 𝑀 )
20 8 eqcomd ⊢ ( 𝜑 → 𝑀 = 𝑋 )
21 20 adantr ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → 𝑀 = 𝑋 )
22 19 21 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → if ( 𝑋 = 𝑀 , 𝑀 , if ( 𝑋 < 𝐼 , ( 𝑋 + ( 𝑀 − 𝐼 ) ) , ( 𝑋 + ( 1 − 𝐼 ) ) ) ) = 𝑋 )
23 16 22 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → if ( 𝑥 = 𝑀 , 𝑀 , if ( 𝑥 < 𝐼 , ( 𝑥 + ( 𝑀 − 𝐼 ) ) , ( 𝑥 + ( 1 − 𝐼 ) ) ) ) = 𝑋 )
24 9 23 7 7 fvmptd ⊢ ( 𝜑 → ( 𝐵 ‘ 𝑋 ) = 𝑋 )
25 8 fveq2d ⊢ ( 𝜑 → ( { ⟨ 𝑀 , 𝑀 ⟩ } ‘ 𝑋 ) = ( { ⟨ 𝑀 , 𝑀 ⟩ } ‘ 𝑀 ) )
26 fvsng ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑀 ∈ ℕ ) → ( { ⟨ 𝑀 , 𝑀 ⟩ } ‘ 𝑀 ) = 𝑀 )
27 1 1 26 syl2anc ⊢ ( 𝜑 → ( { ⟨ 𝑀 , 𝑀 ⟩ } ‘ 𝑀 ) = 𝑀 )
28 25 27 eqtrd ⊢ ( 𝜑 → ( { ⟨ 𝑀 , 𝑀 ⟩ } ‘ 𝑋 ) = 𝑀 )
29 28 eqcomd ⊢ ( 𝜑 → 𝑀 = ( { ⟨ 𝑀 , 𝑀 ⟩ } ‘ 𝑋 ) )
30 24 8 29 3eqtrd ⊢ ( 𝜑 → ( 𝐵 ‘ 𝑋 ) = ( { ⟨ 𝑀 , 𝑀 ⟩ } ‘ 𝑋 ) )
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 1 nnzd ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
36 fzsn ⊢ ( 𝑀 ∈ ℤ → ( 𝑀 ... 𝑀 ) = { 𝑀 } )
37 35 36 syl ⊢ ( 𝜑 → ( 𝑀 ... 𝑀 ) = { 𝑀 } )
38 37 ineq2d ⊢ ( 𝜑 → ( ( ( 1 ... ( 𝐼 − 1 ) ) ∪ ( 𝐼 ... ( 𝑀 − 1 ) ) ) ∩ ( 𝑀 ... 𝑀 ) ) = ( ( ( 1 ... ( 𝐼 − 1 ) ) ∪ ( 𝐼 ... ( 𝑀 − 1 ) ) ) ∩ { 𝑀 } ) )
39 38 eqcomd ⊢ ( 𝜑 → ( ( ( 1 ... ( 𝐼 − 1 ) ) ∪ ( 𝐼 ... ( 𝑀 − 1 ) ) ) ∩ { 𝑀 } ) = ( ( ( 1 ... ( 𝐼 − 1 ) ) ∪ ( 𝐼 ... ( 𝑀 − 1 ) ) ) ∩ ( 𝑀 ... 𝑀 ) ) )
40 2 nncnd ⊢ ( 𝜑 → 𝐼 ∈ ℂ )
41 1 nncnd ⊢ ( 𝜑 → 𝑀 ∈ ℂ )
42 40 41 pncan3d ⊢ ( 𝜑 → ( 𝐼 + ( 𝑀 − 𝐼 ) ) = 𝑀 )
43 42 oveq2d ⊢ ( 𝜑 → ( 1 ..^ ( 𝐼 + ( 𝑀 − 𝐼 ) ) ) = ( 1 ..^ 𝑀 ) )
44 fzoval ⊢ ( 𝑀 ∈ ℤ → ( 1 ..^ 𝑀 ) = ( 1 ... ( 𝑀 − 1 ) ) )
45 35 44 syl ⊢ ( 𝜑 → ( 1 ..^ 𝑀 ) = ( 1 ... ( 𝑀 − 1 ) ) )
46 43 45 eqtrd ⊢ ( 𝜑 → ( 1 ..^ ( 𝐼 + ( 𝑀 − 𝐼 ) ) ) = ( 1 ... ( 𝑀 − 1 ) ) )
47 46 eqcomd ⊢ ( 𝜑 → ( 1 ... ( 𝑀 − 1 ) ) = ( 1 ..^ ( 𝐼 + ( 𝑀 − 𝐼 ) ) ) )
48 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
49 2 48 eleqtrdi ⊢ ( 𝜑 → 𝐼 ∈ ( ℤ≥ ‘ 1 ) )
50 2 nnzd ⊢ ( 𝜑 → 𝐼 ∈ ℤ )
51 50 35 jca ⊢ ( 𝜑 → ( 𝐼 ∈ ℤ ∧ 𝑀 ∈ ℤ ) )
52 znn0sub ⊢ ( ( 𝐼 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝐼 ≤ 𝑀 ↔ ( 𝑀 − 𝐼 ) ∈ ℕ0 ) )
53 51 52 syl ⊢ ( 𝜑 → ( 𝐼 ≤ 𝑀 ↔ ( 𝑀 − 𝐼 ) ∈ ℕ0 ) )
54 3 53 mpbid ⊢ ( 𝜑 → ( 𝑀 − 𝐼 ) ∈ ℕ0 )
55 fzoun ⊢ ( ( 𝐼 ∈ ( ℤ≥ ‘ 1 ) ∧ ( 𝑀 − 𝐼 ) ∈ ℕ0 ) → ( 1 ..^ ( 𝐼 + ( 𝑀 − 𝐼 ) ) ) = ( ( 1 ..^ 𝐼 ) ∪ ( 𝐼 ..^ ( 𝐼 + ( 𝑀 − 𝐼 ) ) ) ) )
56 49 54 55 syl2anc ⊢ ( 𝜑 → ( 1 ..^ ( 𝐼 + ( 𝑀 − 𝐼 ) ) ) = ( ( 1 ..^ 𝐼 ) ∪ ( 𝐼 ..^ ( 𝐼 + ( 𝑀 − 𝐼 ) ) ) ) )
57 47 56 eqtrd ⊢ ( 𝜑 → ( 1 ... ( 𝑀 − 1 ) ) = ( ( 1 ..^ 𝐼 ) ∪ ( 𝐼 ..^ ( 𝐼 + ( 𝑀 − 𝐼 ) ) ) ) )
58 fzoval ⊢ ( 𝐼 ∈ ℤ → ( 1 ..^ 𝐼 ) = ( 1 ... ( 𝐼 − 1 ) ) )
59 50 58 syl ⊢ ( 𝜑 → ( 1 ..^ 𝐼 ) = ( 1 ... ( 𝐼 − 1 ) ) )
60 42 oveq2d ⊢ ( 𝜑 → ( 𝐼 ..^ ( 𝐼 + ( 𝑀 − 𝐼 ) ) ) = ( 𝐼 ..^ 𝑀 ) )
61 fzoval ⊢ ( 𝑀 ∈ ℤ → ( 𝐼 ..^ 𝑀 ) = ( 𝐼 ... ( 𝑀 − 1 ) ) )
62 35 61 syl ⊢ ( 𝜑 → ( 𝐼 ..^ 𝑀 ) = ( 𝐼 ... ( 𝑀 − 1 ) ) )
63 60 62 eqtrd ⊢ ( 𝜑 → ( 𝐼 ..^ ( 𝐼 + ( 𝑀 − 𝐼 ) ) ) = ( 𝐼 ... ( 𝑀 − 1 ) ) )
64 59 63 uneq12d ⊢ ( 𝜑 → ( ( 1 ..^ 𝐼 ) ∪ ( 𝐼 ..^ ( 𝐼 + ( 𝑀 − 𝐼 ) ) ) ) = ( ( 1 ... ( 𝐼 − 1 ) ) ∪ ( 𝐼 ... ( 𝑀 − 1 ) ) ) )
65 57 64 eqtrd ⊢ ( 𝜑 → ( 1 ... ( 𝑀 − 1 ) ) = ( ( 1 ... ( 𝐼 − 1 ) ) ∪ ( 𝐼 ... ( 𝑀 − 1 ) ) ) )
66 65 ineq1d ⊢ ( 𝜑 → ( ( 1 ... ( 𝑀 − 1 ) ) ∩ ( 𝑀 ... 𝑀 ) ) = ( ( ( 1 ... ( 𝐼 − 1 ) ) ∪ ( 𝐼 ... ( 𝑀 − 1 ) ) ) ∩ ( 𝑀 ... 𝑀 ) ) )
67 66 eqcomd ⊢ ( 𝜑 → ( ( ( 1 ... ( 𝐼 − 1 ) ) ∪ ( 𝐼 ... ( 𝑀 − 1 ) ) ) ∩ ( 𝑀 ... 𝑀 ) ) = ( ( 1 ... ( 𝑀 − 1 ) ) ∩ ( 𝑀 ... 𝑀 ) ) )
68 1 nnred ⊢ ( 𝜑 → 𝑀 ∈ ℝ )
69 68 ltm1d ⊢ ( 𝜑 → ( 𝑀 − 1 ) < 𝑀 )
70 fzdisj ⊢ ( ( 𝑀 − 1 ) < 𝑀 → ( ( 1 ... ( 𝑀 − 1 ) ) ∩ ( 𝑀 ... 𝑀 ) ) = ∅ )
71 69 70 syl ⊢ ( 𝜑 → ( ( 1 ... ( 𝑀 − 1 ) ) ∩ ( 𝑀 ... 𝑀 ) ) = ∅ )
72 67 71 eqtrd ⊢ ( 𝜑 → ( ( ( 1 ... ( 𝐼 − 1 ) ) ∪ ( 𝐼 ... ( 𝑀 − 1 ) ) ) ∩ ( 𝑀 ... 𝑀 ) ) = ∅ )
73 39 72 eqtrd ⊢ ( 𝜑 → ( ( ( 1 ... ( 𝐼 − 1 ) ) ∪ ( 𝐼 ... ( 𝑀 − 1 ) ) ) ∩ { 𝑀 } ) = ∅ )
74 elsng ⊢ ( 𝑋 ∈ ( 1 ... 𝑀 ) → ( 𝑋 ∈ { 𝑀 } ↔ 𝑋 = 𝑀 ) )
75 7 74 syl ⊢ ( 𝜑 → ( 𝑋 ∈ { 𝑀 } ↔ 𝑋 = 𝑀 ) )
76 8 75 mpbird ⊢ ( 𝜑 → 𝑋 ∈ { 𝑀 } )
77 33 34 73 76 fvun2d ⊢ ( 𝜑 → ( ( ( 𝐶 ∪ 𝐷 ) ∪ { ⟨ 𝑀 , 𝑀 ⟩ } ) ‘ 𝑋 ) = ( { ⟨ 𝑀 , 𝑀 ⟩ } ‘ 𝑋 ) )
78 77 eqcomd ⊢ ( 𝜑 → ( { ⟨ 𝑀 , 𝑀 ⟩ } ‘ 𝑋 ) = ( ( ( 𝐶 ∪ 𝐷 ) ∪ { ⟨ 𝑀 , 𝑀 ⟩ } ) ‘ 𝑋 ) )
79 30 78 eqtrd ⊢ ( 𝜑 → ( 𝐵 ‘ 𝑋 ) = ( ( ( 𝐶 ∪ 𝐷 ) ∪ { ⟨ 𝑀 , 𝑀 ⟩ } ) ‘ 𝑋 ) )