metakunt25

	Ref	Expression
Hypotheses	metakunt25.1	$⊢ φ \to M \in ℕ$
	metakunt25.2	$⊢ φ \to I \in ℕ$
	metakunt25.3	$⊢ φ \to I \leq M$
	metakunt25.4	$⊢ B = (x \in (1 \dots M) ⟼ if (x = M, M, if (x < I, x + M - I, x + 1 - I)))$
Assertion	metakunt25	$⊢ φ \to B : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)$

Proof

Step	Hyp	Ref	Expression
1		metakunt25.1	$⊢ φ \to M \in ℕ$
2		metakunt25.2	$⊢ φ \to I \in ℕ$
3		metakunt25.3	$⊢ φ \to I \leq M$
4		metakunt25.4	$⊢ B = (x \in (1 \dots M) ⟼ if (x = M, M, if (x < I, x + M - I, x + 1 - I)))$
5		eqid	$⊢ (x \in (1 \dots I - 1) ⟼ x + M - I) = (x \in (1 \dots I - 1) ⟼ x + M - I)$
6	1 2 3 5	metakunt15	$⊢ φ \to (x \in (1 \dots I - 1) ⟼ x + M - I) : (1 \dots I - 1) \underset{1-1 onto}{⟶} (M - I + 1 \dots M - 1)$
7		eqid	$⊢ (x \in (I \dots M - 1) ⟼ x + 1 - I) = (x \in (I \dots M - 1) ⟼ x + 1 - I)$
8	1 2 3 7	metakunt16	$⊢ φ \to (x \in (I \dots M - 1) ⟼ x + 1 - I) : (I \dots M - 1) \underset{1-1 onto}{⟶} (1 \dots M - I)$
9		f1osng	$⊢ (M \in ℕ \land M \in ℕ) \to \{⟨M, M⟩\} : \{M\} \underset{1-1 onto}{⟶} \{M\}$
10	1 1 9	syl2anc	$⊢ φ \to \{⟨M, M⟩\} : \{M\} \underset{1-1 onto}{⟶} \{M\}$
11	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))$
12	11	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)$
13	12	simp1d	$⊢ φ \to (1 \dots I - 1) \cap (I \dots M - 1) = \emptyset$
14	12	simp2d	$⊢ φ \to (1 \dots I - 1) \cap \{M\} = \emptyset$
15	12	simp3d	$⊢ φ \to (I \dots M - 1) \cap \{M\} = \emptyset$
16	11	simprd	$⊢ φ \to ((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)$
17	16	simp1d	$⊢ φ \to (M - I + 1 \dots M - 1) \cap (1 \dots M - I) = \emptyset$
18	16	simp2d	$⊢ φ \to (M - I + 1 \dots M - 1) \cap \{M\} = \emptyset$
19	16	simp3d	$⊢ φ \to (1 \dots M - I) \cap \{M\} = \emptyset$
20		eleq1	$⊢ M = if (x = M, M, if (x < I, x + M - I, x + 1 - I)) \to (M \in ℤ \leftrightarrow if (x = M, M, if (x < I, x + M - I, x + 1 - I)) \in ℤ)$
21		eleq1	$⊢ if (x < I, x + M - I, x + 1 - I) = if (x = M, M, if (x < I, x + M - I, x + 1 - I)) \to (if (x < I, x + M - I, x + 1 - I) \in ℤ \leftrightarrow if (x = M, M, if (x < I, x + M - I, x + 1 - I)) \in ℤ)$
22	1	nnzd	$⊢ φ \to M \in ℤ$
23	22	adantr	$⊢ (φ \land x \in (1 \dots M)) \to M \in ℤ$
24	23	adantr	$⊢ ((φ \land x \in (1 \dots M)) \land x = M) \to M \in ℤ$
25		eleq1	$⊢ x + M - I = if (x < I, x + M - I, x + 1 - I) \to (x + M - I \in ℤ \leftrightarrow if (x < I, x + M - I, x + 1 - I) \in ℤ)$
26		eleq1	$⊢ x + 1 - I = if (x < I, x + M - I, x + 1 - I) \to (x + 1 - I \in ℤ \leftrightarrow if (x < I, x + M - I, x + 1 - I) \in ℤ)$
27		elfzelz	$⊢ x \in (1 \dots M) \to x \in ℤ$
28	27	adantl	$⊢ (φ \land x \in (1 \dots M)) \to x \in ℤ$
29	28	adantr	$⊢ ((φ \land x \in (1 \dots M)) \land \neg x = M) \to x \in ℤ$
30	29	adantr	$⊢ (((φ \land x \in (1 \dots M)) \land \neg x = M) \land x < I) \to x \in ℤ$
31	23	ad2antrr	$⊢ (((φ \land x \in (1 \dots M)) \land \neg x = M) \land x < I) \to M \in ℤ$
32	2	nnzd	$⊢ φ \to I \in ℤ$
33	32	adantr	$⊢ (φ \land x \in (1 \dots M)) \to I \in ℤ$
34	33	adantr	$⊢ ((φ \land x \in (1 \dots M)) \land \neg x = M) \to I \in ℤ$
35	34	adantr	$⊢ (((φ \land x \in (1 \dots M)) \land \neg x = M) \land x < I) \to I \in ℤ$
36	31 35	zsubcld	$⊢ (((φ \land x \in (1 \dots M)) \land \neg x = M) \land x < I) \to M - I \in ℤ$
37	30 36	zaddcld	$⊢ (((φ \land x \in (1 \dots M)) \land \neg x = M) \land x < I) \to x + M - I \in ℤ$
38	29	adantr	$⊢ (((φ \land x \in (1 \dots M)) \land \neg x = M) \land \neg x < I) \to x \in ℤ$
39		1zzd	$⊢ (((φ \land x \in (1 \dots M)) \land \neg x = M) \land \neg x < I) \to 1 \in ℤ$
40	34	adantr	$⊢ (((φ \land x \in (1 \dots M)) \land \neg x = M) \land \neg x < I) \to I \in ℤ$
41	39 40	zsubcld	$⊢ (((φ \land x \in (1 \dots M)) \land \neg x = M) \land \neg x < I) \to 1 - I \in ℤ$
42	38 41	zaddcld	$⊢ (((φ \land x \in (1 \dots M)) \land \neg x = M) \land \neg x < I) \to x + 1 - I \in ℤ$
43	25 26 37 42	ifbothda	$⊢ ((φ \land x \in (1 \dots M)) \land \neg x = M) \to if (x < I, x + M - I, x + 1 - I) \in ℤ$
44	20 21 24 43	ifbothda	$⊢ (φ \land x \in (1 \dots M)) \to if (x = M, M, if (x < I, x + M - I, x + 1 - I)) \in ℤ$
45	44 4	fmptd	$⊢ φ \to B : (1 \dots M) ⟶ ℤ$
46	45	ffnd	$⊢ φ \to B Fn (1 \dots M)$
47	1 2 3 4 5 7	metakunt19	$⊢ φ \to (((x \in (1 \dots I - 1) ⟼ x + M - I) Fn (1 \dots I - 1) \land (x \in (I \dots M - 1) ⟼ x + 1 - I) Fn (I \dots M - 1) \land ((x \in (1 \dots I - 1) ⟼ x + M - I) \cup (x \in (I \dots M - 1) ⟼ x + 1 - I)) Fn ((1 \dots I - 1) \cup (I \dots M - 1))) \land \{⟨M, M⟩\} Fn \{M\})$
48	47	simpld	$⊢ φ \to ((x \in (1 \dots I - 1) ⟼ x + M - I) Fn (1 \dots I - 1) \land (x \in (I \dots M - 1) ⟼ x + 1 - I) Fn (I \dots M - 1) \land ((x \in (1 \dots I - 1) ⟼ x + M - I) \cup (x \in (I \dots M - 1) ⟼ x + 1 - I)) Fn ((1 \dots I - 1) \cup (I \dots M - 1)))$
49	48	simp3d	$⊢ φ \to ((x \in (1 \dots I - 1) ⟼ x + M - I) \cup (x \in (I \dots M - 1) ⟼ x + 1 - I)) Fn ((1 \dots I - 1) \cup (I \dots M - 1))$
50	47	simprd	$⊢ φ \to \{⟨M, M⟩\} Fn \{M\}$
51	1 2 3	metakunt24	$⊢ φ \to (((1 \dots I - 1) \cup (I \dots M - 1)) \cap \{M\} = \emptyset \land (1 \dots M) = ((1 \dots I - 1) \cup (I \dots M - 1)) \cup \{M\} \land (1 \dots M) = ((M - I + 1 \dots M - 1) \cup (1 \dots M - I)) \cup \{M\})$
52	51	simp1d	$⊢ φ \to ((1 \dots I - 1) \cup (I \dots M - 1)) \cap \{M\} = \emptyset$
53	49 50 52	fnund	$⊢ φ \to (((x \in (1 \dots I - 1) ⟼ x + M - I) \cup (x \in (I \dots M - 1) ⟼ x + 1 - I)) \cup \{⟨M, M⟩\}) Fn (((1 \dots I - 1) \cup (I \dots M - 1)) \cup \{M\})$
54	51	simp2d	$⊢ φ \to (1 \dots M) = ((1 \dots I - 1) \cup (I \dots M - 1)) \cup \{M\}$
55	1	adantr	$⊢ (φ \land y \in (1 \dots M)) \to M \in ℕ$
56	2	adantr	$⊢ (φ \land y \in (1 \dots M)) \to I \in ℕ$
57	3	adantr	$⊢ (φ \land y \in (1 \dots M)) \to I \leq M$
58		simpr	$⊢ (φ \land y \in (1 \dots M)) \to y \in (1 \dots M)$
59	55 56 57 4 5 7 58	metakunt23	$⊢ (φ \land y \in (1 \dots M)) \to B (y) = (((x \in (1 \dots I - 1) ⟼ x + M - I) \cup (x \in (I \dots M - 1) ⟼ x + 1 - I)) \cup \{⟨M, M⟩\}) (y)$
60	46 53 54 59	eqfnfv2d2	$⊢ φ \to B = ((x \in (1 \dots I - 1) ⟼ x + M - I) \cup (x \in (I \dots M - 1) ⟼ x + 1 - I)) \cup \{⟨M, M⟩\}$
61	51	simp3d	$⊢ φ \to (1 \dots M) = ((M - I + 1 \dots M - 1) \cup (1 \dots M - I)) \cup \{M\}$
62	6 8 10 13 14 15 17 18 19 60 54 61	metakunt17	$⊢ φ \to B : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)$

Metamath Proof Explorer

Theorem metakunt25

Proof