metakunt19

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

	Ref	Expression
Hypotheses	metakunt19.1	$⊢ φ \to M \in ℕ$
	metakunt19.2	$⊢ φ \to I \in ℕ$
	metakunt19.3	$⊢ φ \to I \leq M$
	metakunt19.4	$⊢ B = (x \in (1 \dots M) ⟼ if (x = M, M, if (x < I, x + M - I, x + 1 - I)))$
	metakunt19.5	$⊢ C = (x \in (1 \dots I - 1) ⟼ x + M - I)$
	metakunt19.6	$⊢ D = (x \in (I \dots M - 1) ⟼ x + 1 - I)$
Assertion	metakunt19	$⊢ φ \to ((C Fn (1 \dots I - 1) \land D Fn (I \dots M - 1) \land (C \cup D) Fn ((1 \dots I - 1) \cup (I \dots M - 1))) \land \{⟨M, M⟩\} Fn \{M\})$

Proof

Step	Hyp	Ref	Expression
1		metakunt19.1	$⊢ φ \to M \in ℕ$
2		metakunt19.2	$⊢ φ \to I \in ℕ$
3		metakunt19.3	$⊢ φ \to I \leq M$
4		metakunt19.4	$⊢ B = (x \in (1 \dots M) ⟼ if (x = M, M, if (x < I, x + M - I, x + 1 - I)))$
5		metakunt19.5	$⊢ C = (x \in (1 \dots I - 1) ⟼ x + M - I)$
6		metakunt19.6	$⊢ D = (x \in (I \dots M - 1) ⟼ x + 1 - I)$
7		elfzelz	$⊢ x \in (1 \dots I - 1) \to x \in ℤ$
8	7	adantl	$⊢ (φ \land x \in (1 \dots I - 1)) \to x \in ℤ$
9	1	nnzd	$⊢ φ \to M \in ℤ$
10	9	adantr	$⊢ (φ \land x \in (1 \dots I - 1)) \to M \in ℤ$
11	2	nnzd	$⊢ φ \to I \in ℤ$
12	11	adantr	$⊢ (φ \land x \in (1 \dots I - 1)) \to I \in ℤ$
13	10 12	zsubcld	$⊢ (φ \land x \in (1 \dots I - 1)) \to M - I \in ℤ$
14	8 13	zaddcld	$⊢ (φ \land x \in (1 \dots I - 1)) \to x + M - I \in ℤ$
15	14 5	fmptd	$⊢ φ \to C : (1 \dots I - 1) ⟶ ℤ$
16	15	ffnd	$⊢ φ \to C Fn (1 \dots I - 1)$
17		elfzelz	$⊢ x \in (I \dots M - 1) \to x \in ℤ$
18	17	adantl	$⊢ (φ \land x \in (I \dots M - 1)) \to x \in ℤ$
19		1zzd	$⊢ (φ \land x \in (I \dots M - 1)) \to 1 \in ℤ$
20	11	adantr	$⊢ (φ \land x \in (I \dots M - 1)) \to I \in ℤ$
21	19 20	zsubcld	$⊢ (φ \land x \in (I \dots M - 1)) \to 1 - I \in ℤ$
22	18 21	zaddcld	$⊢ (φ \land x \in (I \dots M - 1)) \to x + 1 - I \in ℤ$
23	22 6	fmptd	$⊢ φ \to D : (I \dots M - 1) ⟶ ℤ$
24	23	ffnd	$⊢ φ \to D Fn (I \dots M - 1)$
25	1 2 3	metakunt18	$⊢ φ \to (((1 \dots I - 1) \cap (I \dots M - 1) = \emptyset \land (1 \dots I - 1) \cap \{M\} = \emptyset \land (I \dots M - 1) \cap \{M\} = \emptyset) \land ((M - I + 1 \dots M - 1) \cap (1 \dots M - I) = \emptyset \land (M - I + 1 \dots M - 1) \cap \{M\} = \emptyset \land (1 \dots M - I) \cap \{M\} = \emptyset))$
26	25	simpld	$⊢ φ \to ((1 \dots I - 1) \cap (I \dots M - 1) = \emptyset \land (1 \dots I - 1) \cap \{M\} = \emptyset \land (I \dots M - 1) \cap \{M\} = \emptyset)$
27	26	simp1d	$⊢ φ \to (1 \dots I - 1) \cap (I \dots M - 1) = \emptyset$
28	16 24 27	fnund	$⊢ φ \to (C \cup D) Fn ((1 \dots I - 1) \cup (I \dots M - 1))$
29	16 24 28	3jca	$⊢ φ \to (C Fn (1 \dots I - 1) \land D Fn (I \dots M - 1) \land (C \cup D) Fn ((1 \dots I - 1) \cup (I \dots M - 1)))$
30		fnsng	$⊢ (M \in ℕ \land M \in ℕ) \to \{⟨M, M⟩\} Fn \{M\}$
31	1 1 30	syl2anc	$⊢ φ \to \{⟨M, M⟩\} Fn \{M\}$
32	29 31	jca	$⊢ φ \to ((C Fn (1 \dots I - 1) \land D Fn (I \dots M - 1) \land (C \cup D) Fn ((1 \dots I - 1) \cup (I \dots M - 1))) \land \{⟨M, M⟩\} Fn \{M\})$

Metamath Proof Explorer

Theorem metakunt19

Proof