Metamath Proof Explorer


Theorem metakunt10

Description: C is the right inverse for A. (Contributed by metakunt, 24-May-2024)

Ref Expression
Hypotheses metakunt10.1 φ M
metakunt10.2 φ I
metakunt10.3 φ I M
metakunt10.4 A = x 1 M if x = I M if x < I x x 1
metakunt10.5 C = y 1 M if y = M I if y < I y y + 1
metakunt10.6 φ X 1 M
Assertion metakunt10 φ X = M A C X = X

Proof

Step Hyp Ref Expression
1 metakunt10.1 φ M
2 metakunt10.2 φ I
3 metakunt10.3 φ I M
4 metakunt10.4 A = x 1 M if x = I M if x < I x x 1
5 metakunt10.5 C = y 1 M if y = M I if y < I y y + 1
6 metakunt10.6 φ X 1 M
7 4 a1i φ X = M A = x 1 M if x = I M if x < I x x 1
8 eqeq1 x = C X x = I C X = I
9 breq1 x = C X x < I C X < I
10 id x = C X x = C X
11 oveq1 x = C X x 1 = C X 1
12 9 10 11 ifbieq12d x = C X if x < I x x 1 = if C X < I C X C X 1
13 8 12 ifbieq2d x = C X if x = I M if x < I x x 1 = if C X = I M if C X < I C X C X 1
14 13 adantl φ X = M x = C X if x = I M if x < I x x 1 = if C X = I M if C X < I C X C X 1
15 fveq2 X = M C X = C M
16 15 adantl φ X = M C X = C M
17 5 a1i φ C = y 1 M if y = M I if y < I y y + 1
18 iftrue y = M if y = M I if y < I y y + 1 = I
19 18 adantl φ y = M if y = M I if y < I y y + 1 = I
20 1zzd φ 1
21 1 nnzd φ M
22 1 nnge1d φ 1 M
23 1 nnred φ M
24 23 leidd φ M M
25 20 21 21 22 24 elfzd φ M 1 M
26 17 19 25 2 fvmptd φ C M = I
27 26 adantr φ X = M C M = I
28 16 27 eqtrd φ X = M C X = I
29 iftrue C X = I if C X = I M if C X < I C X C X 1 = M
30 28 29 syl φ X = M if C X = I M if C X < I C X C X 1 = M
31 simpr φ X = M X = M
32 31 eqcomd φ X = M M = X
33 30 32 eqtrd φ X = M if C X = I M if C X < I C X C X 1 = X
34 33 adantr φ X = M x = C X if C X = I M if C X < I C X C X 1 = X
35 14 34 eqtrd φ X = M x = C X if x = I M if x < I x x 1 = X
36 1 2 3 5 metakunt2 φ C : 1 M 1 M
37 36 adantr φ X = M C : 1 M 1 M
38 6 adantr φ X = M X 1 M
39 37 38 ffvelrnd φ X = M C X 1 M
40 7 35 39 38 fvmptd φ X = M A C X = X