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		elfznn	$$⊢X\in \left(1\dots M\right)\to X\in \mathbb{N}$$
49	7 48	syl	$$⊢\phi \to X\in \mathbb{N}$$
50	49	nnzd	$$⊢\phi \to X\in \mathbb{Z}$$
51	2	nnred	$$⊢\phi \to I\in ℝ$$
52	49	nnred	$$⊢\phi \to X\in ℝ$$
53	51 52	lenltd	$$⊢\phi \to \left(I\le X\leftrightarrow \neg X<I\right)$$
54	9 53	mpbird	$$⊢\phi \to I\le X$$
55		elfzle2	$$⊢X\in \left(1\dots M\right)\to X\le M$$
56	7 55	syl	$$⊢\phi \to X\le M$$
57		df-ne	$$⊢X\ne M\leftrightarrow \neg X=M$$
58	8 57	sylibr	$$⊢\phi \to X\ne M$$
59	58	necomd	$$⊢\phi \to M\ne X$$
60	56 59	jca	$$⊢\phi \to \left(X\le M\wedge M\ne X\right)$$
61	1	nnred	$$⊢\phi \to M\in ℝ$$
62	52 61	ltlend	$$⊢\phi \to \left(X<M\leftrightarrow \left(X\le M\wedge M\ne X\right)\right)$$
63	60 62	mpbird	$$⊢\phi \to X<M$$
64		zltlem1	$$⊢\left(X\in \mathbb{Z}\wedge M\in \mathbb{Z}\right)\to \left(X<M\leftrightarrow X\le M-1\right)$$
65	50 46 64	syl2anc	$$⊢\phi \to \left(X<M\leftrightarrow X\le M-1\right)$$
66	63 65	mpbid	$$⊢\phi \to X\le M-1$$
67	27 47 50 54 66	elfzd	$$⊢\phi \to X\in \left(I\dots M-1\right)$$
68		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)$$
69	67 68	syl	$$⊢\phi \to X\in \left(\left(1\dots I-1\right)\cup \left(I\dots M-1\right)\right)$$
70	33 34 45 69	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)$$
71	32	simp1d	$$⊢\phi \to CFn\left(1\dots I-1\right)$$
72	32	simp2d	$$⊢\phi \to DFn\left(I\dots M-1\right)$$
73	38	simp1d	$$⊢\phi \to \left(1\dots I-1\right)\cap \left(I\dots M-1\right)=\varnothing$$
74	71 72 73 67	fvun2d	$$⊢\phi \to \left(C\cup D\right)\left(X\right)=D\left(X\right)$$
75	6	a1i	$$⊢\phi \to D=\left(x\in \left(I\dots M-1\right)⟼x+1-I\right)$$
76		simpr	$$⊢\left(\phi \wedge x=X\right)\to x=X$$
77	76	oveq1d	$$⊢\left(\phi \wedge x=X\right)\to x+1-I=X+1-I$$
78	25	zred	$$⊢\phi \to X\in ℝ$$
79		lenlt	$$⊢\left(I\in ℝ\wedge X\in ℝ\right)\to \left(I\le X\leftrightarrow \neg X<I\right)$$
80	51 78 79	syl2anc	$$⊢\phi \to \left(I\le X\leftrightarrow \neg X<I\right)$$
81	9 80	mpbird	$$⊢\phi \to I\le X$$
82	78 61	ltlend	$$⊢\phi \to \left(X<M\leftrightarrow \left(X\le M\wedge M\ne X\right)\right)$$
83	60 82	mpbird	$$⊢\phi \to X<M$$
84	25 46 64	syl2anc	$$⊢\phi \to \left(X<M\leftrightarrow X\le M-1\right)$$
85	83 84	mpbid	$$⊢\phi \to X\le M-1$$
86	27 47 25 81 85	elfzd	$$⊢\phi \to X\in \left(I\dots M-1\right)$$
87	75 77 86 29	fvmptd	$$⊢\phi \to D\left(X\right)=X+1-I$$
88	74 87	eqtrd	$$⊢\phi \to \left(C\cup D\right)\left(X\right)=X+1-I$$
89	70 88	eqtrd	$$⊢\phi \to \left(\left(C\cup D\right)\cup \left\{⟨M,M⟩\right\}\right)\left(X\right)=X+1-I$$
90	89	eqcomd	$$⊢\phi \to X+1-I=\left(\left(C\cup D\right)\cup \left\{⟨M,M⟩\right\}\right)\left(X\right)$$
91	30 90	eqtrd	$$⊢\phi \to B\left(X\right)=\left(\left(C\cup D\right)\cup \left\{⟨M,M⟩\right\}\right)\left(X\right)$$