Theorem appleid1 ≪ | index | src | ≫ 

theorem appleid1 (f x: nat): $ f @ x <= f $;
StepHypRefExpression
1 theid 
{a3 | x, a3 e. f} == {a1 | a1 = a2} -> the {a3 | x, a3 e. f} = a2
2 1 conv app 
{a3 | x, a3 e. f} == {a1 | a1 = a2} -> f @ x = a2
3 2 leeq1d 
{a3 | x, a3 e. f} == {a1 | a1 = a2} -> (f @ x <= f <-> a2 <= f)
4 eqeq1 
a1 = a2 -> (a1 = a2 <-> a2 = a2)
5 4 elabe 
a2 e. {a1 | a1 = a2} <-> a2 = a2
6 eqid 
a2 = a2
7 5, 6 mpbir 
a2 e. {a1 | a1 = a2}
8 eleq2 
{a3 | x, a3 e. f} == {a1 | a1 = a2} -> (a2 e. {a3 | x, a3 e. f} <-> a2 e. {a1 | a1 = a2})
9 7, 8 mpbiri 
{a3 | x, a3 e. f} == {a1 | a1 = a2} -> a2 e. {a3 | x, a3 e. f}
10 preq2 
a3 = a2 -> x, a3 = x, a2
11 10 eleq1d 
a3 = a2 -> (x, a3 e. f <-> x, a2 e. f)
12 11 elabe 
a2 e. {a3 | x, a3 e. f} <-> x, a2 e. f
13 ellt 
x, a2 e. f -> x, a2 < f
14 ltle 
x, a2 < f -> x, a2 <= f
15 letr 
a2 <= x, a2 -> x, a2 <= f -> a2 <= f
16 leprid2 
a2 <= x, a2
17 15, 16 ax_mp 
x, a2 <= f -> a2 <= f
18 14, 17 rsyl 
x, a2 < f -> a2 <= f
19 13, 18 rsyl 
x, a2 e. f -> a2 <= f
20 12, 19 sylbi 
a2 e. {a3 | x, a3 e. f} -> a2 <= f
21 9, 20 rsyl 
{a3 | x, a3 e. f} == {a1 | a1 = a2} -> a2 <= f
22 3, 21 mpbird 
{a3 | x, a3 e. f} == {a1 | a1 = a2} -> f @ x <= f
23 22 eex 
E. a2 {a3 | x, a3 e. f} == {a1 | a1 = a2} -> f @ x <= f
24 le01 
0 <= f
25 the0 
~E. a2 {a3 | x, a3 e. f} == {a1 | a1 = a2} -> the {a3 | x, a3 e. f} = 0
26 25 conv app 
~E. a2 {a3 | x, a3 e. f} == {a1 | a1 = a2} -> f @ x = 0
27 26 leeq1d 
~E. a2 {a3 | x, a3 e. f} == {a1 | a1 = a2} -> (f @ x <= f <-> 0 <= f)
28 24, 27 mpbiri 
~E. a2 {a3 | x, a3 e. f} == {a1 | a1 = a2} -> f @ x <= f
29 23, 28 cases 
f @ x <= f

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp, itru), axs_pred_calc (ax_gen, ax_4, ax_5, ax_6, ax_7, ax_10, ax_11, ax_12), axs_set (elab, ax_8), axs_the (theid, the0), axs_peano (peano1, peano2, peano5, addeq, muleq, add0, addS, mul0, mulS)