Theorem metakunt19

Description: Domains on restrictions of functions. (Contributed by metakunt, 28-May-2024)

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

Proof

Step	Hyp	Ref	Expression
1		metakunt19.1	⊢ ( 𝜑 → 𝑀 ∈ ℕ )
2		metakunt19.2	⊢ ( 𝜑 → 𝐼 ∈ ℕ )
3		metakunt19.3	⊢ ( 𝜑 → 𝐼 ≤ 𝑀 )
4		metakunt19.4	⊢ 𝐵 = ( 𝑥 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑥 = 𝑀 , 𝑀 , if ( 𝑥 < 𝐼 , ( 𝑥 + ( 𝑀 − 𝐼 ) ) , ( 𝑥 + ( 1 − 𝐼 ) ) ) ) )
5		metakunt19.5	⊢ 𝐶 = ( 𝑥 ∈ ( 1 ... ( 𝐼 − 1 ) ) ↦ ( 𝑥 + ( 𝑀 − 𝐼 ) ) )
6		metakunt19.6	⊢ 𝐷 = ( 𝑥 ∈ ( 𝐼 ... ( 𝑀 − 1 ) ) ↦ ( 𝑥 + ( 1 − 𝐼 ) ) )
7		elfzelz	⊢ ( 𝑥 ∈ ( 1 ... ( 𝐼 − 1 ) ) → 𝑥 ∈ ℤ )
8	7	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( 𝐼 − 1 ) ) ) → 𝑥 ∈ ℤ )
9	1	nnzd	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
10	9	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( 𝐼 − 1 ) ) ) → 𝑀 ∈ ℤ )
11	2	nnzd	⊢ ( 𝜑 → 𝐼 ∈ ℤ )
12	11	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( 𝐼 − 1 ) ) ) → 𝐼 ∈ ℤ )
13	10 12	zsubcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( 𝐼 − 1 ) ) ) → ( 𝑀 − 𝐼 ) ∈ ℤ )
14	8 13	zaddcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( 𝐼 − 1 ) ) ) → ( 𝑥 + ( 𝑀 − 𝐼 ) ) ∈ ℤ )
15	14 5	fmptd	⊢ ( 𝜑 → 𝐶 : ( 1 ... ( 𝐼 − 1 ) ) ⟶ ℤ )
16	15	ffnd	⊢ ( 𝜑 → 𝐶 Fn ( 1 ... ( 𝐼 − 1 ) ) )
17		elfzelz	⊢ ( 𝑥 ∈ ( 𝐼 ... ( 𝑀 − 1 ) ) → 𝑥 ∈ ℤ )
18	17	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ... ( 𝑀 − 1 ) ) ) → 𝑥 ∈ ℤ )
19		1zzd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ... ( 𝑀 − 1 ) ) ) → 1 ∈ ℤ )
20	11	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ... ( 𝑀 − 1 ) ) ) → 𝐼 ∈ ℤ )
21	19 20	zsubcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ... ( 𝑀 − 1 ) ) ) → ( 1 − 𝐼 ) ∈ ℤ )
22	18 21	zaddcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ... ( 𝑀 − 1 ) ) ) → ( 𝑥 + ( 1 − 𝐼 ) ) ∈ ℤ )
23	22 6	fmptd	⊢ ( 𝜑 → 𝐷 : ( 𝐼 ... ( 𝑀 − 1 ) ) ⟶ ℤ )
24	23	ffnd	⊢ ( 𝜑 → 𝐷 Fn ( 𝐼 ... ( 𝑀 − 1 ) ) )
25	1 2 3	metakunt18	⊢ ( 𝜑 → ( ( ( ( 1 ... ( 𝐼 − 1 ) ) ∩ ( 𝐼 ... ( 𝑀 − 1 ) ) ) = ∅ ∧ ( ( 1 ... ( 𝐼 − 1 ) ) ∩ { 𝑀 } ) = ∅ ∧ ( ( 𝐼 ... ( 𝑀 − 1 ) ) ∩ { 𝑀 } ) = ∅ ) ∧ ( ( ( ( ( 𝑀 − 𝐼 ) + 1 ) ... ( 𝑀 − 1 ) ) ∩ ( 1 ... ( 𝑀 − 𝐼 ) ) ) = ∅ ∧ ( ( ( ( 𝑀 − 𝐼 ) + 1 ) ... ( 𝑀 − 1 ) ) ∩ { 𝑀 } ) = ∅ ∧ ( ( 1 ... ( 𝑀 − 𝐼 ) ) ∩ { 𝑀 } ) = ∅ ) ) )
26	25	simpld	⊢ ( 𝜑 → ( ( ( 1 ... ( 𝐼 − 1 ) ) ∩ ( 𝐼 ... ( 𝑀 − 1 ) ) ) = ∅ ∧ ( ( 1 ... ( 𝐼 − 1 ) ) ∩ { 𝑀 } ) = ∅ ∧ ( ( 𝐼 ... ( 𝑀 − 1 ) ) ∩ { 𝑀 } ) = ∅ ) )
27	26	simp1d	⊢ ( 𝜑 → ( ( 1 ... ( 𝐼 − 1 ) ) ∩ ( 𝐼 ... ( 𝑀 − 1 ) ) ) = ∅ )
28	16 24 27	fnund	⊢ ( 𝜑 → ( 𝐶 ∪ 𝐷 ) Fn ( ( 1 ... ( 𝐼 − 1 ) ) ∪ ( 𝐼 ... ( 𝑀 − 1 ) ) ) )
29	16 24 28	3jca	⊢ ( 𝜑 → ( 𝐶 Fn ( 1 ... ( 𝐼 − 1 ) ) ∧ 𝐷 Fn ( 𝐼 ... ( 𝑀 − 1 ) ) ∧ ( 𝐶 ∪ 𝐷 ) Fn ( ( 1 ... ( 𝐼 − 1 ) ) ∪ ( 𝐼 ... ( 𝑀 − 1 ) ) ) ) )
30		fnsng	⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑀 ∈ ℕ ) → { ⟨ 𝑀 , 𝑀 ⟩ } Fn { 𝑀 } )
31	1 1 30	syl2anc	⊢ ( 𝜑 → { ⟨ 𝑀 , 𝑀 ⟩ } Fn { 𝑀 } )
32	29 31	jca	⊢ ( 𝜑 → ( ( 𝐶 Fn ( 1 ... ( 𝐼 − 1 ) ) ∧ 𝐷 Fn ( 𝐼 ... ( 𝑀 − 1 ) ) ∧ ( 𝐶 ∪ 𝐷 ) Fn ( ( 1 ... ( 𝐼 − 1 ) ) ∪ ( 𝐼 ... ( 𝑀 − 1 ) ) ) ) ∧ { ⟨ 𝑀 , 𝑀 ⟩ } Fn { 𝑀 } ) )