metakunt22

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

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

Proof

Step	Hyp	Ref	Expression
1		metakunt22.1	$⊢ φ \to M \in ℕ$
2		metakunt22.2	$⊢ φ \to I \in ℕ$
3		metakunt22.3	$⊢ φ \to I \leq M$
4		metakunt22.4	$⊢ B = (x \in (1 \dots M) ⟼ if (x = M, M, if (x < I, x + M - I, x + 1 - I)))$
5		metakunt22.5	$⊢ C = (x \in (1 \dots I - 1) ⟼ x + M - I)$
6		metakunt22.6	$⊢ D = (x \in (I \dots M - 1) ⟼ x + 1 - I)$
7		metakunt22.7	$⊢ φ \to X \in (1 \dots M)$
8		metakunt22.8	$⊢ φ \to \neg X = M$
9		metakunt22.9	$⊢ φ \to \neg 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		iffalse	$⊢ \neg X = M \to if (X = M, M, if (X < I, X + M - I, X + 1 - I)) = if (X < I, X + M - I, X + 1 - I)$
19	8 18	syl	$⊢ φ \to if (X = M, M, if (X < I, X + M - I, X + 1 - I)) = if (X < I, X + M - I, X + 1 - I)$
20		iffalse	$⊢ \neg X < I \to if (X < I, X + M - I, X + 1 - I) = X + 1 - I$
21	9 20	syl	$⊢ φ \to if (X < I, X + M - I, X + 1 - I) = X + 1 - I$
22	19 21	eqtrd	$⊢ φ \to if (X = M, M, if (X < I, X + M - I, X + 1 - I)) = X + 1 - I$
23	22	adantr	$⊢ (φ \land x = X) \to if (X = M, M, if (X < I, X + M - I, X + 1 - I)) = X + 1 - I$
24	17 23	eqtrd	$⊢ (φ \land x = X) \to if (x = M, M, if (x < I, x + M - I, x + 1 - I)) = X + 1 - I$
25	7	elfzelzd	$⊢ φ \to X \in ℤ$
26		1zzd	$⊢ φ \to 1 \in ℤ$
27	2	nnzd	$⊢ φ \to I \in ℤ$
28	26 27	zsubcld	$⊢ φ \to 1 - I \in ℤ$
29	25 28	zaddcld	$⊢ φ \to X + 1 - I \in ℤ$
30	10 24 7 29	fvmptd	$⊢ φ \to B (X) = X + 1 - I$
31	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\})$
32	31	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)))$
33	32	simp3d	$⊢ φ \to (C \cup D) Fn ((1 \dots I - 1) \cup (I \dots M - 1))$
34	31	simprd	$⊢ φ \to \{⟨M, M⟩\} Fn \{M\}$
35		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\})$
36	35	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\})$
37	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))$
38	37	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)$
39	38	simp2d	$⊢ φ \to (1 \dots I - 1) \cap \{M\} = \emptyset$
40	38	simp3d	$⊢ φ \to (I \dots M - 1) \cap \{M\} = \emptyset$
41	39 40	uneq12d	$⊢ φ \to ((1 \dots I - 1) \cap \{M\}) \cup ((I \dots M - 1) \cap \{M\}) = \emptyset \cup \emptyset$
42		unidm	$⊢ \emptyset \cup \emptyset = \emptyset$
43	42	a1i	$⊢ φ \to \emptyset \cup \emptyset = \emptyset$
44	41 43	eqtrd	$⊢ φ \to ((1 \dots I - 1) \cap \{M\}) \cup ((I \dots M - 1) \cap \{M\}) = \emptyset$
45	36 44	eqtrd	$⊢ φ \to ((1 \dots I - 1) \cup (I \dots M - 1)) \cap \{M\} = \emptyset$
46	1	nnzd	$⊢ φ \to M \in ℤ$
47	46 26	zsubcld	$⊢ φ \to M - 1 \in ℤ$
48	2	nnred	$⊢ φ \to I \in ℝ$
49		elfznn	$⊢ X \in (1 \dots M) \to X \in ℕ$
50	7 49	syl	$⊢ φ \to X \in ℕ$
51	50	nnred	$⊢ φ \to X \in ℝ$
52	48 51	lenltd	$⊢ φ \to (I \leq X \leftrightarrow \neg X < I)$
53	9 52	mpbird	$⊢ φ \to I \leq X$
54		elfzle2	$⊢ X \in (1 \dots M) \to X \leq M$
55	7 54	syl	$⊢ φ \to X \leq M$
56		df-ne	$⊢ X \neq M \leftrightarrow \neg X = M$
57	8 56	sylibr	$⊢ φ \to X \neq M$
58	57	necomd	$⊢ φ \to M \neq X$
59	55 58	jca	$⊢ φ \to (X \leq M \land M \neq X)$
60	1	nnred	$⊢ φ \to M \in ℝ$
61	51 60	ltlend	$⊢ φ \to (X < M \leftrightarrow (X \leq M \land M \neq X))$
62	59 61	mpbird	$⊢ φ \to X < M$
63		zltlem1	$⊢ (X \in ℤ \land M \in ℤ) \to (X < M \leftrightarrow X \leq M - 1)$
64	25 46 63	syl2anc	$⊢ φ \to (X < M \leftrightarrow X \leq M - 1)$
65	62 64	mpbid	$⊢ φ \to X \leq M - 1$
66	27 47 25 53 65	elfzd	$⊢ φ \to X \in (I \dots M - 1)$
67		elun2	$⊢ X \in (I \dots M - 1) \to X \in ((1 \dots I - 1) \cup (I \dots M - 1))$
68	66 67	syl	$⊢ φ \to X \in ((1 \dots I - 1) \cup (I \dots M - 1))$
69	33 34 45 68	fvun1d	$⊢ φ \to ((C \cup D) \cup \{⟨M, M⟩\}) (X) = (C \cup D) (X)$
70	32	simp1d	$⊢ φ \to C Fn (1 \dots I - 1)$
71	32	simp2d	$⊢ φ \to D Fn (I \dots M - 1)$
72	38	simp1d	$⊢ φ \to (1 \dots I - 1) \cap (I \dots M - 1) = \emptyset$
73	70 71 72 66	fvun2d	$⊢ φ \to (C \cup D) (X) = D (X)$
74	6	a1i	$⊢ φ \to D = (x \in (I \dots M - 1) ⟼ x + 1 - I)$
75		simpr	$⊢ (φ \land x = X) \to x = X$
76	75	oveq1d	$⊢ (φ \land x = X) \to x + 1 - I = X + 1 - I$
77	25	zred	$⊢ φ \to X \in ℝ$
78		lenlt	$⊢ (I \in ℝ \land X \in ℝ) \to (I \leq X \leftrightarrow \neg X < I)$
79	48 77 78	syl2anc	$⊢ φ \to (I \leq X \leftrightarrow \neg X < I)$
80	9 79	mpbird	$⊢ φ \to I \leq X$
81	77 60	ltlend	$⊢ φ \to (X < M \leftrightarrow (X \leq M \land M \neq X))$
82	59 81	mpbird	$⊢ φ \to X < M$
83	82 64	mpbid	$⊢ φ \to X \leq M - 1$
84	27 47 25 80 83	elfzd	$⊢ φ \to X \in (I \dots M - 1)$
85	74 76 84 29	fvmptd	$⊢ φ \to D (X) = X + 1 - I$
86	73 85	eqtrd	$⊢ φ \to (C \cup D) (X) = X + 1 - I$
87	69 86	eqtrd	$⊢ φ \to ((C \cup D) \cup \{⟨M, M⟩\}) (X) = X + 1 - I$
88	87	eqcomd	$⊢ φ \to X + 1 - I = ((C \cup D) \cup \{⟨M, M⟩\}) (X)$
89	30 88	eqtrd	$⊢ φ \to B (X) = ((C \cup D) \cup \{⟨M, M⟩\}) (X)$

Metamath Proof Explorer

Theorem metakunt22

Proof