metakunt20

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

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

Proof

Step	Hyp	Ref	Expression
1		metakunt20.1	$⊢ φ \to M \in ℕ$
2		metakunt20.2	$⊢ φ \to I \in ℕ$
3		metakunt20.3	$⊢ φ \to I \leq M$
4		metakunt20.4	$⊢ B = (x \in (1 \dots M) ⟼ if (x = M, M, if (x < I, x + M - I, x + 1 - I)))$
5		metakunt20.5	$⊢ C = (x \in (1 \dots I - 1) ⟼ x + M - I)$
6		metakunt20.6	$⊢ D = (x \in (I \dots M - 1) ⟼ x + 1 - I)$
7		metakunt20.7	$⊢ φ \to X \in (1 \dots M)$
8		metakunt20.8	$⊢ φ \to X = M$
9	4	a1i	$⊢ φ \to B = (x \in (1 \dots M) ⟼ if (x = M, M, if (x < I, x + M - I, x + 1 - I)))$
10		eqeq1	$⊢ x = X \to (x = M \leftrightarrow X = M)$
11		breq1	$⊢ x = X \to (x < I \leftrightarrow X < I)$
12		oveq1	$⊢ x = X \to x + M - I = X + M - I$
13		oveq1	$⊢ x = X \to x + 1 - I = X + 1 - I$
14	11 12 13	ifbieq12d	$⊢ x = X \to if (x < I, x + M - I, x + 1 - I) = if (X < I, X + M - I, X + 1 - I)$
15	10 14	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))$
16	15	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))$
17		iftrue	$⊢ X = M \to if (X = M, M, if (X < I, X + M - I, X + 1 - I)) = M$
18	8 17	syl	$⊢ φ \to if (X = M, M, if (X < I, X + M - I, X + 1 - I)) = M$
19	18	adantr	$⊢ (φ \land x = X) \to if (X = M, M, if (X < I, X + M - I, X + 1 - I)) = M$
20	8	eqcomd	$⊢ φ \to M = X$
21	20	adantr	$⊢ (φ \land x = X) \to M = X$
22	19 21	eqtrd	$⊢ (φ \land x = X) \to if (X = M, M, if (X < I, X + M - I, X + 1 - I)) = X$
23	16 22	eqtrd	$⊢ (φ \land x = X) \to if (x = M, M, if (x < I, x + M - I, x + 1 - I)) = X$
24	9 23 7 7	fvmptd	$⊢ φ \to B (X) = X$
25	8	fveq2d	$⊢ φ \to \{⟨M, M⟩\} (X) = \{⟨M, M⟩\} (M)$
26		fvsng	$⊢ (M \in ℕ \land M \in ℕ) \to \{⟨M, M⟩\} (M) = M$
27	1 1 26	syl2anc	$⊢ φ \to \{⟨M, M⟩\} (M) = M$
28	25 27	eqtrd	$⊢ φ \to \{⟨M, M⟩\} (X) = M$
29	28	eqcomd	$⊢ φ \to M = \{⟨M, M⟩\} (X)$
30	24 8 29	3eqtrd	$⊢ φ \to B (X) = \{⟨M, M⟩\} (X)$
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	1	nnzd	$⊢ φ \to M \in ℤ$
36		fzsn	$⊢ M \in ℤ \to (M \dots M) = \{M\}$
37	35 36	syl	$⊢ φ \to (M \dots M) = \{M\}$
38	37	ineq2d	$⊢ φ \to ((1 \dots I - 1) \cup (I \dots M - 1)) \cap (M \dots M) = ((1 \dots I - 1) \cup (I \dots M - 1)) \cap \{M\}$
39	38	eqcomd	$⊢ φ \to ((1 \dots I - 1) \cup (I \dots M - 1)) \cap \{M\} = ((1 \dots I - 1) \cup (I \dots M - 1)) \cap (M \dots M)$
40	2	nncnd	$⊢ φ \to I \in ℂ$
41	1	nncnd	$⊢ φ \to M \in ℂ$
42	40 41	pncan3d	$⊢ φ \to I + M - I = M$
43	42	oveq2d	$⊢ φ \to (1 ..^I + M - I) = (1 ..^M)$
44		fzoval	$⊢ M \in ℤ \to (1 ..^M) = (1 \dots M - 1)$
45	35 44	syl	$⊢ φ \to (1 ..^M) = (1 \dots M - 1)$
46	43 45	eqtrd	$⊢ φ \to (1 ..^I + M - I) = (1 \dots M - 1)$
47	46	eqcomd	$⊢ φ \to (1 \dots M - 1) = (1 ..^I + M - I)$
48		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
49	2 48	eleqtrdi	$⊢ φ \to I \in ℤ_{\geq 1}$
50	2	nnzd	$⊢ φ \to I \in ℤ$
51	50 35	jca	$⊢ φ \to (I \in ℤ \land M \in ℤ)$
52		znn0sub	$⊢ (I \in ℤ \land M \in ℤ) \to (I \leq M \leftrightarrow M - I \in ℕ_{0})$
53	51 52	syl	$⊢ φ \to (I \leq M \leftrightarrow M - I \in ℕ_{0})$
54	3 53	mpbid	$⊢ φ \to M - I \in ℕ_{0}$
55		fzoun	$⊢ (I \in ℤ_{\geq 1} \land M - I \in ℕ_{0}) \to (1 ..^I + M - I) = (1 ..^I) \cup (I ..^I + M - I)$
56	49 54 55	syl2anc	$⊢ φ \to (1 ..^I + M - I) = (1 ..^I) \cup (I ..^I + M - I)$
57	47 56	eqtrd	$⊢ φ \to (1 \dots M - 1) = (1 ..^I) \cup (I ..^I + M - I)$
58		fzoval	$⊢ I \in ℤ \to (1 ..^I) = (1 \dots I - 1)$
59	50 58	syl	$⊢ φ \to (1 ..^I) = (1 \dots I - 1)$
60	42	oveq2d	$⊢ φ \to (I ..^I + M - I) = (I ..^M)$
61		fzoval	$⊢ M \in ℤ \to (I ..^M) = (I \dots M - 1)$
62	35 61	syl	$⊢ φ \to (I ..^M) = (I \dots M - 1)$
63	60 62	eqtrd	$⊢ φ \to (I ..^I + M - I) = (I \dots M - 1)$
64	59 63	uneq12d	$⊢ φ \to (1 ..^I) \cup (I ..^I + M - I) = (1 \dots I - 1) \cup (I \dots M - 1)$
65	57 64	eqtrd	$⊢ φ \to (1 \dots M - 1) = (1 \dots I - 1) \cup (I \dots M - 1)$
66	65	ineq1d	$⊢ φ \to (1 \dots M - 1) \cap (M \dots M) = ((1 \dots I - 1) \cup (I \dots M - 1)) \cap (M \dots M)$
67	66	eqcomd	$⊢ φ \to ((1 \dots I - 1) \cup (I \dots M - 1)) \cap (M \dots M) = (1 \dots M - 1) \cap (M \dots M)$
68	1	nnred	$⊢ φ \to M \in ℝ$
69	68	ltm1d	$⊢ φ \to M - 1 < M$
70		fzdisj	$⊢ M - 1 < M \to (1 \dots M - 1) \cap (M \dots M) = \emptyset$
71	69 70	syl	$⊢ φ \to (1 \dots M - 1) \cap (M \dots M) = \emptyset$
72	67 71	eqtrd	$⊢ φ \to ((1 \dots I - 1) \cup (I \dots M - 1)) \cap (M \dots M) = \emptyset$
73	39 72	eqtrd	$⊢ φ \to ((1 \dots I - 1) \cup (I \dots M - 1)) \cap \{M\} = \emptyset$
74		elsng	$⊢ X \in (1 \dots M) \to (X \in \{M\} \leftrightarrow X = M)$
75	7 74	syl	$⊢ φ \to (X \in \{M\} \leftrightarrow X = M)$
76	8 75	mpbird	$⊢ φ \to X \in \{M\}$
77	33 34 73 76	fvun2d	$⊢ φ \to ((C \cup D) \cup \{⟨M, M⟩\}) (X) = \{⟨M, M⟩\} (X)$
78	77	eqcomd	$⊢ φ \to \{⟨M, M⟩\} (X) = ((C \cup D) \cup \{⟨M, M⟩\}) (X)$
79	30 78	eqtrd	$⊢ φ \to B (X) = ((C \cup D) \cup \{⟨M, M⟩\}) (X)$

Metamath Proof Explorer

Theorem metakunt20

Proof