Metamath Proof Explorer

Theorem metakunt23

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

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

Proof

Step Hyp Ref Expression
1 metakunt23.1 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
2 metakunt23.2 ⊢ ( 𝜑 → 𝐼 ∈ ℕ )
3 metakunt23.3 ⊢ ( 𝜑 → 𝐼 ≤ 𝑀 )
4 metakunt23.4 ⊢ 𝐵 = ( 𝑥 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑥 = 𝑀 , 𝑀 , if ( 𝑥 < 𝐼 , ( 𝑥 + ( 𝑀 − 𝐼 ) ) , ( 𝑥 + ( 1 − 𝐼 ) ) ) ) )
5 metakunt23.5 ⊢ 𝐶 = ( 𝑥 ∈ ( 1 ... ( 𝐼 − 1 ) ) ↦ ( 𝑥 + ( 𝑀 − 𝐼 ) ) )
6 metakunt23.6 ⊢ 𝐷 = ( 𝑥 ∈ ( 𝐼 ... ( 𝑀 − 1 ) ) ↦ ( 𝑥 + ( 1 − 𝐼 ) ) )
7 metakunt23.7 ⊢ ( 𝜑 → 𝑋 ∈ ( 1 ... 𝑀 ) )
8 1 adantr ⊢ ( ( 𝜑 ∧ 𝑋 = 𝑀 ) → 𝑀 ∈ ℕ )
9 2 adantr ⊢ ( ( 𝜑 ∧ 𝑋 = 𝑀 ) → 𝐼 ∈ ℕ )
10 3 adantr ⊢ ( ( 𝜑 ∧ 𝑋 = 𝑀 ) → 𝐼 ≤ 𝑀 )
11 7 adantr ⊢ ( ( 𝜑 ∧ 𝑋 = 𝑀 ) → 𝑋 ∈ ( 1 ... 𝑀 ) )
12 simpr ⊢ ( ( 𝜑 ∧ 𝑋 = 𝑀 ) → 𝑋 = 𝑀 )
13 8 9 10 4 5 6 11 12 metakunt20 ⊢ ( ( 𝜑 ∧ 𝑋 = 𝑀 ) → ( 𝐵 ‘ 𝑋 ) = ( ( ( 𝐶 ∪ 𝐷 ) ∪ { ⟨ 𝑀 , 𝑀 ⟩ } ) ‘ 𝑋 ) )
14 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 = 𝑀 ) ∧ 𝑋 < 𝐼 ) → 𝑀 ∈ ℕ )
15 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 = 𝑀 ) ∧ 𝑋 < 𝐼 ) → 𝐼 ∈ ℕ )
16 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 = 𝑀 ) ∧ 𝑋 < 𝐼 ) → 𝐼 ≤ 𝑀 )
17 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 = 𝑀 ) ∧ 𝑋 < 𝐼 ) → 𝑋 ∈ ( 1 ... 𝑀 ) )
18 simplr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 = 𝑀 ) ∧ 𝑋 < 𝐼 ) → ¬ 𝑋 = 𝑀 )
19 simpr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 = 𝑀 ) ∧ 𝑋 < 𝐼 ) → 𝑋 < 𝐼 )
20 14 15 16 4 5 6 17 18 19 metakunt21 ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 = 𝑀 ) ∧ 𝑋 < 𝐼 ) → ( 𝐵 ‘ 𝑋 ) = ( ( ( 𝐶 ∪ 𝐷 ) ∪ { ⟨ 𝑀 , 𝑀 ⟩ } ) ‘ 𝑋 ) )
21 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 = 𝑀 ) ∧ ¬ 𝑋 < 𝐼 ) → 𝑀 ∈ ℕ )
22 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 = 𝑀 ) ∧ ¬ 𝑋 < 𝐼 ) → 𝐼 ∈ ℕ )
23 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 = 𝑀 ) ∧ ¬ 𝑋 < 𝐼 ) → 𝐼 ≤ 𝑀 )
24 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 = 𝑀 ) ∧ ¬ 𝑋 < 𝐼 ) → 𝑋 ∈ ( 1 ... 𝑀 ) )
25 simplr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 = 𝑀 ) ∧ ¬ 𝑋 < 𝐼 ) → ¬ 𝑋 = 𝑀 )
26 simpr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 = 𝑀 ) ∧ ¬ 𝑋 < 𝐼 ) → ¬ 𝑋 < 𝐼 )
27 21 22 23 4 5 6 24 25 26 metakunt22 ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 = 𝑀 ) ∧ ¬ 𝑋 < 𝐼 ) → ( 𝐵 ‘ 𝑋 ) = ( ( ( 𝐶 ∪ 𝐷 ) ∪ { ⟨ 𝑀 , 𝑀 ⟩ } ) ‘ 𝑋 ) )
28 20 27 pm2.61dan ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = 𝑀 ) → ( 𝐵 ‘ 𝑋 ) = ( ( ( 𝐶 ∪ 𝐷 ) ∪ { ⟨ 𝑀 , 𝑀 ⟩ } ) ‘ 𝑋 ) )
29 13 28 pm2.61dan ⊢ ( 𝜑 → ( 𝐵 ‘ 𝑋 ) = ( ( ( 𝐶 ∪ 𝐷 ) ∪ { ⟨ 𝑀 , 𝑀 ⟩ } ) ‘ 𝑋 ) )