Metamath Proof Explorer


Theorem metakunt4

Description: Value of A. (Contributed by metakunt, 23-May-2024)

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

Proof

Step Hyp Ref Expression
1 metakunt4.1 φ M
2 metakunt4.2 φ I
3 metakunt4.3 φ I M
4 metakunt4.4 A = x 1 M if x = M I if x < I x x + 1
5 metakunt4.5 φ X 1 M
6 4 a1i φ A = x 1 M if x = M I if x < I x x + 1
7 eqeq1 x = X x = M X = M
8 breq1 x = X x < I X < I
9 id x = X x = X
10 oveq1 x = X x + 1 = X + 1
11 8 9 10 ifbieq12d x = X if x < I x x + 1 = if X < I X X + 1
12 7 11 ifbieq2d x = X if x = M I if x < I x x + 1 = if X = M I if X < I X X + 1
13 12 adantl φ x = X if x = M I if x < I x x + 1 = if X = M I if X < I X X + 1
14 2 nnzd φ I
15 5 elfzelzd φ X
16 15 peano2zd φ X + 1
17 15 16 ifcld φ if X < I X X + 1
18 14 17 ifcld φ if X = M I if X < I X X + 1
19 6 13 5 18 fvmptd φ A X = if X = M I if X < I X X + 1