Metamath Proof Explorer


Theorem metakunt12

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

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

Proof

Step Hyp Ref Expression
1 metakunt12.1 φ M
2 metakunt12.2 φ I
3 metakunt12.3 φ I M
4 metakunt12.4 A = x 1 M if x = I M if x < I x x 1
5 metakunt12.5 C = y 1 M if y = M I if y < I y y + 1
6 metakunt12.6 φ X 1 M
7 ioran ¬ X = M X < I ¬ X = M ¬ X < I
8 4 a1i φ ¬ X = M ¬ X < I A = x 1 M if x = I M if x < I x x 1
9 eqeq1 x = C X x = I C X = I
10 breq1 x = C X x < I C X < I
11 id x = C X x = C X
12 oveq1 x = C X x 1 = C X 1
13 10 11 12 ifbieq12d x = C X if x < I x x 1 = if C X < I C X C X 1
14 9 13 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
15 14 adantl φ ¬ X = M ¬ X < I 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
16 5 a1i φ ¬ X = M ¬ X < I C = y 1 M if y = M I if y < I y y + 1
17 eqeq1 y = X y = M X = M
18 breq1 y = X y < I X < I
19 id y = X y = X
20 oveq1 y = X y + 1 = X + 1
21 18 19 20 ifbieq12d y = X if y < I y y + 1 = if X < I X X + 1
22 17 21 ifbieq2d y = X if y = M I if y < I y y + 1 = if X = M I if X < I X X + 1
23 22 adantl φ ¬ X = M ¬ X < I y = X if y = M I if y < I y y + 1 = if X = M I if X < I X X + 1
24 simp2 φ ¬ X = M ¬ X < I ¬ X = M
25 iffalse ¬ X = M if X = M I if X < I X X + 1 = if X < I X X + 1
26 24 25 syl φ ¬ X = M ¬ X < I if X = M I if X < I X X + 1 = if X < I X X + 1
27 simp3 φ ¬ X = M ¬ X < I ¬ X < I
28 iffalse ¬ X < I if X < I X X + 1 = X + 1
29 27 28 syl φ ¬ X = M ¬ X < I if X < I X X + 1 = X + 1
30 26 29 eqtrd φ ¬ X = M ¬ X < I if X = M I if X < I X X + 1 = X + 1
31 30 adantr φ ¬ X = M ¬ X < I y = X if X = M I if X < I X X + 1 = X + 1
32 23 31 eqtrd φ ¬ X = M ¬ X < I y = X if y = M I if y < I y y + 1 = X + 1
33 6 3ad2ant1 φ ¬ X = M ¬ X < I X 1 M
34 6 elfzelzd φ X
35 34 3ad2ant1 φ ¬ X = M ¬ X < I X
36 35 peano2zd φ ¬ X = M ¬ X < I X + 1
37 16 32 33 36 fvmptd φ ¬ X = M ¬ X < I C X = X + 1
38 eqeq1 C X = X + 1 C X = I X + 1 = I
39 breq1 C X = X + 1 C X < I X + 1 < I
40 id C X = X + 1 C X = X + 1
41 oveq1 C X = X + 1 C X 1 = X + 1 - 1
42 39 40 41 ifbieq12d C X = X + 1 if C X < I C X C X 1 = if X + 1 < I X + 1 X + 1 - 1
43 38 42 ifbieq2d C X = X + 1 if C X = I M if C X < I C X C X 1 = if X + 1 = I M if X + 1 < I X + 1 X + 1 - 1
44 37 43 syl φ ¬ X = M ¬ X < I if C X = I M if C X < I C X C X 1 = if X + 1 = I M if X + 1 < I X + 1 X + 1 - 1
45 2 nnred φ I
46 45 3ad2ant1 φ ¬ X = M ¬ X < I I
47 35 zred φ ¬ X = M ¬ X < I X
48 36 zred φ ¬ X = M ¬ X < I X + 1
49 46 47 lenltd φ ¬ X = M ¬ X < I I X ¬ X < I
50 27 49 mpbird φ ¬ X = M ¬ X < I I X
51 47 ltp1d φ ¬ X = M ¬ X < I X < X + 1
52 46 47 48 50 51 lelttrd φ ¬ X = M ¬ X < I I < X + 1
53 46 52 ltned φ ¬ X = M ¬ X < I I X + 1
54 53 necomd φ ¬ X = M ¬ X < I X + 1 I
55 54 neneqd φ ¬ X = M ¬ X < I ¬ X + 1 = I
56 iffalse ¬ X + 1 = I if X + 1 = I M if X + 1 < I X + 1 X + 1 - 1 = if X + 1 < I X + 1 X + 1 - 1
57 55 56 syl φ ¬ X = M ¬ X < I if X + 1 = I M if X + 1 < I X + 1 X + 1 - 1 = if X + 1 < I X + 1 X + 1 - 1
58 47 lep1d φ ¬ X = M ¬ X < I X X + 1
59 46 47 48 50 58 letrd φ ¬ X = M ¬ X < I I X + 1
60 46 48 lenltd φ ¬ X = M ¬ X < I I X + 1 ¬ X + 1 < I
61 59 60 mpbid φ ¬ X = M ¬ X < I ¬ X + 1 < I
62 iffalse ¬ X + 1 < I if X + 1 < I X + 1 X + 1 - 1 = X + 1 - 1
63 61 62 syl φ ¬ X = M ¬ X < I if X + 1 < I X + 1 X + 1 - 1 = X + 1 - 1
64 35 zcnd φ ¬ X = M ¬ X < I X
65 1cnd φ ¬ X = M ¬ X < I 1
66 64 65 pncand φ ¬ X = M ¬ X < I X + 1 - 1 = X
67 57 63 66 3eqtrd φ ¬ X = M ¬ X < I if X + 1 = I M if X + 1 < I X + 1 X + 1 - 1 = X
68 44 67 eqtrd φ ¬ X = M ¬ X < I if C X = I M if C X < I C X C X 1 = X
69 68 adantr φ ¬ X = M ¬ X < I x = C X if C X = I M if C X < I C X C X 1 = X
70 15 69 eqtrd φ ¬ X = M ¬ X < I x = C X if x = I M if x < I x x 1 = X
71 1 2 3 5 metakunt2 φ C : 1 M 1 M
72 71 3ad2ant1 φ ¬ X = M ¬ X < I C : 1 M 1 M
73 72 33 ffvelrnd φ ¬ X = M ¬ X < I C X 1 M
74 8 70 73 33 fvmptd φ ¬ X = M ¬ X < I A C X = X
75 74 3expb φ ¬ X = M ¬ X < I A C X = X
76 7 75 sylan2b φ ¬ X = M X < I A C X = X