metakunt21

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

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

Proof

Step	Hyp	Ref	Expression
1		metakunt21.1	$⊢ φ \to M \in ℕ$
2		metakunt21.2	$⊢ φ \to I \in ℕ$
3		metakunt21.3	$⊢ φ \to I \leq M$
4		metakunt21.4	$⊢ B = (x \in (1 \dots M) ⟼ if (x = M, M, if (x < I, x + M - I, x + 1 - I)))$
5		metakunt21.5	$⊢ C = (x \in (1 \dots I - 1) ⟼ x + M - I)$
6		metakunt21.6	$⊢ D = (x \in (I \dots M - 1) ⟼ x + 1 - I)$
7		metakunt21.7	$⊢ φ \to X \in (1 \dots M)$
8		metakunt21.8	$⊢ φ \to \neg X = M$
9		metakunt21.9	$⊢ φ \to X < I$
10	4	a1i	$⊢ φ \to B = (x \in (1 \dots M) ⟼ if (x = M, M, if (x < I, x + M - I, x + 1 - I)))$
11		eqeq1	$⊢ x = X \to (x = M \leftrightarrow X = M)$
12		breq1	$⊢ x = X \to (x < I \leftrightarrow X < I)$
13		oveq1	$⊢ x = X \to x + M - I = X + M - I$
14		oveq1	$⊢ x = X \to x + 1 - I = X + 1 - I$
15	12 13 14	ifbieq12d	$⊢ x = X \to if (x < I, x + M - I, x + 1 - I) = if (X < I, X + M - I, X + 1 - I)$
16	11 15	ifbieq2d	$⊢ x = X \to if (x = M, M, if (x < I, x + M - I, x + 1 - I)) = if (X = M, M, if (X < I, X + M - I, X + 1 - I))$
17	16	adantl	$⊢ (φ \land x = X) \to if (x = M, M, if (x < I, x + M - I, x + 1 - I)) = if (X = M, M, if (X < I, X + M - I, X + 1 - I))$
18	8	iffalsed	$⊢ φ \to if (X = M, M, if (X < I, X + M - I, X + 1 - I)) = if (X < I, X + M - I, X + 1 - I)$
19	9	iftrued	$⊢ φ \to if (X < I, X + M - I, X + 1 - I) = X + M - I$
20	18 19	eqtrd	$⊢ φ \to if (X = M, M, if (X < I, X + M - I, X + 1 - I)) = X + M - I$
21	20	adantr	$⊢ (φ \land x = X) \to if (X = M, M, if (X < I, X + M - I, X + 1 - I)) = X + M - I$
22	17 21	eqtrd	$⊢ (φ \land x = X) \to if (x = M, M, if (x < I, x + M - I, x + 1 - I)) = X + M - I$
23	7	elfzelzd	$⊢ φ \to X \in ℤ$
24	1	nnzd	$⊢ φ \to M \in ℤ$
25	2	nnzd	$⊢ φ \to I \in ℤ$
26	24 25	zsubcld	$⊢ φ \to M - I \in ℤ$
27	23 26	zaddcld	$⊢ φ \to X + M - I \in ℤ$
28	10 22 7 27	fvmptd	$⊢ φ \to B (X) = X + M - I$
29	1 2 3 4 5 6	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\})$
30	29	simpld	$⊢ φ \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)))$
31	30	simp3d	$⊢ φ \to (C \cup D) Fn ((1 \dots I - 1) \cup (I \dots M - 1))$
32	29	simprd	$⊢ φ \to \{⟨M, M⟩\} Fn \{M\}$
33		indir	$⊢ ((1 \dots I - 1) \cup (I \dots M - 1)) \cap \{M\} = ((1 \dots I - 1) \cap \{M\}) \cup ((I \dots M - 1) \cap \{M\})$
34	33	a1i	$⊢ φ \to ((1 \dots I - 1) \cup (I \dots M - 1)) \cap \{M\} = ((1 \dots I - 1) \cap \{M\}) \cup ((I \dots M - 1) \cap \{M\})$
35	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))$
36	35	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)$
37	36	simp2d	$⊢ φ \to (1 \dots I - 1) \cap \{M\} = \emptyset$
38	36	simp3d	$⊢ φ \to (I \dots M - 1) \cap \{M\} = \emptyset$
39	37 38	uneq12d	$⊢ φ \to ((1 \dots I - 1) \cap \{M\}) \cup ((I \dots M - 1) \cap \{M\}) = \emptyset \cup \emptyset$
40		unidm	$⊢ \emptyset \cup \emptyset = \emptyset$
41	40	a1i	$⊢ φ \to \emptyset \cup \emptyset = \emptyset$
42	39 41	eqtrd	$⊢ φ \to ((1 \dots I - 1) \cap \{M\}) \cup ((I \dots M - 1) \cap \{M\}) = \emptyset$
43	34 42	eqtrd	$⊢ φ \to ((1 \dots I - 1) \cup (I \dots M - 1)) \cap \{M\} = \emptyset$
44		1zzd	$⊢ φ \to 1 \in ℤ$
45	25 44	zsubcld	$⊢ φ \to I - 1 \in ℤ$
46		elfznn	$⊢ X \in (1 \dots M) \to X \in ℕ$
47	7 46	syl	$⊢ φ \to X \in ℕ$
48	47	nnge1d	$⊢ φ \to 1 \leq X$
49		zltlem1	$⊢ (X \in ℤ \land I \in ℤ) \to (X < I \leftrightarrow X \leq I - 1)$
50	23 25 49	syl2anc	$⊢ φ \to (X < I \leftrightarrow X \leq I - 1)$
51	9 50	mpbid	$⊢ φ \to X \leq I - 1$
52	44 45 23 48 51	elfzd	$⊢ φ \to X \in (1 \dots I - 1)$
53		elun1	$⊢ X \in (1 \dots I - 1) \to X \in ((1 \dots I - 1) \cup (I \dots M - 1))$
54	52 53	syl	$⊢ φ \to X \in ((1 \dots I - 1) \cup (I \dots M - 1))$
55	31 32 43 54	fvun1d	$⊢ φ \to ((C \cup D) \cup \{⟨M, M⟩\}) (X) = (C \cup D) (X)$
56	30	simp1d	$⊢ φ \to C Fn (1 \dots I - 1)$
57	30	simp2d	$⊢ φ \to D Fn (I \dots M - 1)$
58	36	simp1d	$⊢ φ \to (1 \dots I - 1) \cap (I \dots M - 1) = \emptyset$
59	56 57 58 52	fvun1d	$⊢ φ \to (C \cup D) (X) = C (X)$
60	5	a1i	$⊢ φ \to C = (x \in (1 \dots I - 1) ⟼ x + M - I)$
61	13	adantl	$⊢ (φ \land x = X) \to x + M - I = X + M - I$
62	60 61 52 27	fvmptd	$⊢ φ \to C (X) = X + M - I$
63	59 62	eqtrd	$⊢ φ \to (C \cup D) (X) = X + M - I$
64	55 63	eqtrd	$⊢ φ \to ((C \cup D) \cup \{⟨M, M⟩\}) (X) = X + M - I$
65	64	eqcomd	$⊢ φ \to X + M - I = ((C \cup D) \cup \{⟨M, M⟩\}) (X)$
66	28 65	eqtrd	$⊢ φ \to B (X) = ((C \cup D) \cup \{⟨M, M⟩\}) (X)$

Metamath Proof Explorer

Theorem metakunt21

Proof