Metamath Proof Explorer


Theorem metakunt13

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

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

Proof

Step Hyp Ref Expression
1 metakunt13.1 φ M
2 metakunt13.2 φ I
3 metakunt13.3 φ I M
4 metakunt13.4 A = x 1 M if x = I M if x < I x x 1
5 metakunt13.5 C = y 1 M if y = M I if y < I y y + 1
6 metakunt13.6 φ X 1 M
7 1 2 3 4 5 6 metakunt10 φ X = M A C X = X
8 7 ex φ X = M A C X = X
9 1 2 3 4 5 6 metakunt11 φ X < I A C X = X
10 9 ex φ X < I A C X = X
11 1 2 3 4 5 6 metakunt12 φ ¬ X = M X < I A C X = X
12 11 ex φ ¬ X = M X < I A C X = X
13 8 10 12 ecase3d φ A C X = X