Theorem metakunt22

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

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

Proof

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