metakunt23

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

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

Proof

Step	Hyp	Ref	Expression
1		metakunt23.1	$⊢ φ \to M \in ℕ$
2		metakunt23.2	$⊢ φ \to I \in ℕ$
3		metakunt23.3	$⊢ φ \to I \leq M$
4		metakunt23.4	$⊢ B = (x \in (1 \dots M) ⟼ if (x = M, M, if (x < I, x + M - I, x + 1 - I)))$
5		metakunt23.5	$⊢ C = (x \in (1 \dots I - 1) ⟼ x + M - I)$
6		metakunt23.6	$⊢ D = (x \in (I \dots M - 1) ⟼ x + 1 - I)$
7		metakunt23.7	$⊢ φ \to X \in (1 \dots M)$
8	1	adantr	$⊢ (φ \land X = M) \to M \in ℕ$
9	2	adantr	$⊢ (φ \land X = M) \to I \in ℕ$
10	3	adantr	$⊢ (φ \land X = M) \to I \leq M$
11	7	adantr	$⊢ (φ \land X = M) \to X \in (1 \dots M)$
12		simpr	$⊢ (φ \land X = M) \to X = M$
13	8 9 10 4 5 6 11 12	metakunt20	$⊢ (φ \land X = M) \to B (X) = ((C \cup D) \cup \{⟨M, M⟩\}) (X)$
14	1	ad2antrr	$⊢ ((φ \land \neg X = M) \land X < I) \to M \in ℕ$
15	2	ad2antrr	$⊢ ((φ \land \neg X = M) \land X < I) \to I \in ℕ$
16	3	ad2antrr	$⊢ ((φ \land \neg X = M) \land X < I) \to I \leq M$
17	7	ad2antrr	$⊢ ((φ \land \neg X = M) \land X < I) \to X \in (1 \dots M)$
18		simplr	$⊢ ((φ \land \neg X = M) \land X < I) \to \neg X = M$
19		simpr	$⊢ ((φ \land \neg X = M) \land X < I) \to X < I$
20	14 15 16 4 5 6 17 18 19	metakunt21	$⊢ ((φ \land \neg X = M) \land X < I) \to B (X) = ((C \cup D) \cup \{⟨M, M⟩\}) (X)$
21	1	ad2antrr	$⊢ ((φ \land \neg X = M) \land \neg X < I) \to M \in ℕ$
22	2	ad2antrr	$⊢ ((φ \land \neg X = M) \land \neg X < I) \to I \in ℕ$
23	3	ad2antrr	$⊢ ((φ \land \neg X = M) \land \neg X < I) \to I \leq M$
24	7	ad2antrr	$⊢ ((φ \land \neg X = M) \land \neg X < I) \to X \in (1 \dots M)$
25		simplr	$⊢ ((φ \land \neg X = M) \land \neg X < I) \to \neg X = M$
26		simpr	$⊢ ((φ \land \neg X = M) \land \neg X < I) \to \neg X < I$
27	21 22 23 4 5 6 24 25 26	metakunt22	$⊢ ((φ \land \neg X = M) \land \neg X < I) \to B (X) = ((C \cup D) \cup \{⟨M, M⟩\}) (X)$
28	20 27	pm2.61dan	$⊢ (φ \land \neg X = M) \to B (X) = ((C \cup D) \cup \{⟨M, M⟩\}) (X)$
29	13 28	pm2.61dan	$⊢ φ \to B (X) = ((C \cup D) \cup \{⟨M, M⟩\}) (X)$

Metamath Proof Explorer

Theorem metakunt23

Proof