Theorem leastlem ≪ | index | src | ≫ 

theorem leastlem (A: set) (a: nat) {z: nat}:
  $ a e. A -> least A e. A /\ A. z (z e. A -> least A <= z) $;
StepHypRefExpression
1 id 
x = a -> x = a
2 1 lteq1d 
x = a -> (x < z <-> a < z)
3 2 imeq2d 
x = a -> (z e. A -> x < z <-> z e. A -> a < z)
4 3 aleqd 
x = a -> (A. z (z e. A -> x < z) <-> A. z (z e. A -> a < z))
5 4 oreq1d 
x = a -> (A. z (z e. A -> x < z) \/ E. u (u e. A /\ A. z (z e. A -> u <= z)) <-> A. z (z e. A -> a < z) \/ E. u (u e. A /\ A. z (z e. A -> u <= z)))
6 id 
x = 0 -> x = 0
7 6 lteq1d 
x = 0 -> (x < z <-> 0 < z)
8 7 imeq2d 
x = 0 -> (z e. A -> x < z <-> z e. A -> 0 < z)
9 8 aleqd 
x = 0 -> (A. z (z e. A -> x < z) <-> A. z (z e. A -> 0 < z))
10 9 oreq1d 
x = 0 -> (A. z (z e. A -> x < z) \/ E. u (u e. A /\ A. z (z e. A -> u <= z)) <-> A. z (z e. A -> 0 < z) \/ E. u (u e. A /\ A. z (z e. A -> u <= z)))
11 id 
x = y -> x = y
12 11 lteq1d 
x = y -> (x < z <-> y < z)
13 12 imeq2d 
x = y -> (z e. A -> x < z <-> z e. A -> y < z)
14 13 aleqd 
x = y -> (A. z (z e. A -> x < z) <-> A. z (z e. A -> y < z))
15 14 oreq1d 
x = y -> (A. z (z e. A -> x < z) \/ E. u (u e. A /\ A. z (z e. A -> u <= z)) <-> A. z (z e. A -> y < z) \/ E. u (u e. A /\ A. z (z e. A -> u <= z)))
16 id 
x = suc y -> x = suc y
17 16 lteq1d 
x = suc y -> (x < z <-> suc y < z)
18 17 imeq2d 
x = suc y -> (z e. A -> x < z <-> z e. A -> suc y < z)
19 18 aleqd 
x = suc y -> (A. z (z e. A -> x < z) <-> A. z (z e. A -> suc y < z))
20 19 oreq1d 
x = suc y -> (A. z (z e. A -> x < z) \/ E. u (u e. A /\ A. z (z e. A -> u <= z)) <-> A. z (z e. A -> suc y < z) \/ E. u (u e. A /\ A. z (z e. A -> u <= z)))
21 eleq1 
u = 0 -> (u e. A <-> 0 e. A)
22 leeq1 
u = 0 -> (u <= z <-> 0 <= z)
23 22 imeq2d 
u = 0 -> (z e. A -> u <= z <-> z e. A -> 0 <= z)
24 23 aleqd 
u = 0 -> (A. z (z e. A -> u <= z) <-> A. z (z e. A -> 0 <= z))
25 21, 24 aneqd 
u = 0 -> (u e. A /\ A. z (z e. A -> u <= z) <-> 0 e. A /\ A. z (z e. A -> 0 <= z))
26 25 iexe 
0 e. A /\ A. z (z e. A -> 0 <= z) -> E. u (u e. A /\ A. z (z e. A -> u <= z))
27 id 
0 e. A -> 0 e. A
28 le01 
0 <= z
29 28 a1i 
z e. A -> 0 <= z
30 29 ax_gen 
A. z (z e. A -> 0 <= z)
31 30 a1i 
0 e. A -> A. z (z e. A -> 0 <= z)
32 26, 27, 31 sylan 
0 e. A -> E. u (u e. A /\ A. z (z e. A -> u <= z))
33 32 orrd 
0 e. A -> A. z (z e. A -> 0 < z) \/ E. u (u e. A /\ A. z (z e. A -> u <= z))
34 lt01 
0 < z <-> z != 0
35 anl 
~0 e. A /\ z e. A -> ~0 e. A
36 anr 
~0 e. A /\ z e. A -> z e. A
37 eleq1 
z = 0 -> (z e. A <-> 0 e. A)
38 37 bi1d 
z = 0 -> z e. A -> 0 e. A
39 36, 38 syl5 
z = 0 -> ~0 e. A /\ z e. A -> 0 e. A
40 39 com12 
~0 e. A /\ z e. A -> z = 0 -> 0 e. A
41 35, 40 mtd 
~0 e. A /\ z e. A -> ~z = 0
42 41 conv ne 
~0 e. A /\ z e. A -> z != 0
43 34, 42 sylibr 
~0 e. A /\ z e. A -> 0 < z
44 43 ialda 
~0 e. A -> A. z (z e. A -> 0 < z)
45 44 orld 
~0 e. A -> A. z (z e. A -> 0 < z) \/ E. u (u e. A /\ A. z (z e. A -> u <= z))
46 33, 45 cases 
A. z (z e. A -> 0 < z) \/ E. u (u e. A /\ A. z (z e. A -> u <= z))
47 eor 
(A. z (z e. A -> y < z) -> A. z (z e. A -> suc y < z) \/ E. u (u e. A /\ A. z (z e. A -> u <= z))) ->
  (E. u (u e. A /\ A. z (z e. A -> u <= z)) -> A. z (z e. A -> suc y < z) \/ E. u (u e. A /\ A. z (z e. A -> u <= z))) ->
  A. z (z e. A -> y < z) \/ E. u (u e. A /\ A. z (z e. A -> u <= z)) ->
  A. z (z e. A -> suc y < z) \/ E. u (u e. A /\ A. z (z e. A -> u <= z))
48 eleq1 
u = suc y -> (u e. A <-> suc y e. A)
49 leeq1 
u = suc y -> (u <= z <-> suc y <= z)
50 49 imeq2d 
u = suc y -> (z e. A -> u <= z <-> z e. A -> suc y <= z)
51 50 aleqd 
u = suc y -> (A. z (z e. A -> u <= z) <-> A. z (z e. A -> suc y <= z))
52 48, 51 aneqd 
u = suc y -> (u e. A /\ A. z (z e. A -> u <= z) <-> suc y e. A /\ A. z (z e. A -> suc y <= z))
53 52 iexe 
suc y e. A /\ A. z (z e. A -> suc y <= z) -> E. u (u e. A /\ A. z (z e. A -> u <= z))
54 anr 
A. z (z e. A -> y < z) /\ suc y e. A -> suc y e. A
55 anl 
A. z (z e. A -> y < z) /\ suc y e. A -> A. z (z e. A -> y < z)
56 55 conv lt 
A. z (z e. A -> y < z) /\ suc y e. A -> A. z (z e. A -> suc y <= z)
57 53, 54, 56 sylan 
A. z (z e. A -> y < z) /\ suc y e. A -> E. u (u e. A /\ A. z (z e. A -> u <= z))
58 57 orrd 
A. z (z e. A -> y < z) /\ suc y e. A -> A. z (z e. A -> suc y < z) \/ E. u (u e. A /\ A. z (z e. A -> u <= z))
59 nfal1 
F/ z A. z (z e. A -> y < z)
60 nfv 
F/ z ~suc y e. A
61 59, 60 nfan 
F/ z A. z (z e. A -> y < z) /\ ~suc y e. A
62 ltlene 
suc y < z <-> suc y <= z /\ suc y != z
63 eal 
A. z (z e. A -> y < z) -> z e. A -> y < z
64 63 conv lt 
A. z (z e. A -> y < z) -> z e. A -> suc y <= z
65 64 anwl 
A. z (z e. A -> y < z) /\ ~suc y e. A -> z e. A -> suc y <= z
66 65 imp 
A. z (z e. A -> y < z) /\ ~suc y e. A /\ z e. A -> suc y <= z
67 anlr 
A. z (z e. A -> y < z) /\ ~suc y e. A /\ z e. A -> ~suc y e. A
68 eleq1 
suc y = z -> (suc y e. A <-> z e. A)
69 68 anwr 
A. z (z e. A -> y < z) /\ ~suc y e. A /\ z e. A /\ suc y = z -> (suc y e. A <-> z e. A)
70 anlr 
A. z (z e. A -> y < z) /\ ~suc y e. A /\ z e. A /\ suc y = z -> z e. A
71 69, 70 mpbird 
A. z (z e. A -> y < z) /\ ~suc y e. A /\ z e. A /\ suc y = z -> suc y e. A
72 67, 71 mtand 
A. z (z e. A -> y < z) /\ ~suc y e. A /\ z e. A -> ~suc y = z
73 72 conv ne 
A. z (z e. A -> y < z) /\ ~suc y e. A /\ z e. A -> suc y != z
74 66, 73 iand 
A. z (z e. A -> y < z) /\ ~suc y e. A /\ z e. A -> suc y <= z /\ suc y != z
75 62, 74 sylibr 
A. z (z e. A -> y < z) /\ ~suc y e. A /\ z e. A -> suc y < z
76 75 exp 
A. z (z e. A -> y < z) /\ ~suc y e. A -> z e. A -> suc y < z
77 61, 76 ialdh 
A. z (z e. A -> y < z) /\ ~suc y e. A -> A. z (z e. A -> suc y < z)
78 77 orld 
A. z (z e. A -> y < z) /\ ~suc y e. A -> A. z (z e. A -> suc y < z) \/ E. u (u e. A /\ A. z (z e. A -> u <= z))
79 58, 78 casesda 
A. z (z e. A -> y < z) -> A. z (z e. A -> suc y < z) \/ E. u (u e. A /\ A. z (z e. A -> u <= z))
80 47, 79 ax_mp 
(E. u (u e. A /\ A. z (z e. A -> u <= z)) -> A. z (z e. A -> suc y < z) \/ E. u (u e. A /\ A. z (z e. A -> u <= z))) ->
  A. z (z e. A -> y < z) \/ E. u (u e. A /\ A. z (z e. A -> u <= z)) ->
  A. z (z e. A -> suc y < z) \/ E. u (u e. A /\ A. z (z e. A -> u <= z))
81 orr 
E. u (u e. A /\ A. z (z e. A -> u <= z)) -> A. z (z e. A -> suc y < z) \/ E. u (u e. A /\ A. z (z e. A -> u <= z))
82 80, 81 ax_mp 
A. z (z e. A -> y < z) \/ E. u (u e. A /\ A. z (z e. A -> u <= z)) -> A. z (z e. A -> suc y < z) \/ E. u (u e. A /\ A. z (z e. A -> u <= z))
83 5, 10, 15, 20, 46, 82 ind 
A. z (z e. A -> a < z) \/ E. u (u e. A /\ A. z (z e. A -> u <= z))
84 83 conv or 
~A. z (z e. A -> a < z) -> E. u (u e. A /\ A. z (z e. A -> u <= z))
85 ltirr 
~a < a
86 85 a1i 
a e. A -> ~a < a
87 eleq1 
z = a -> (z e. A <-> a e. A)
88 lteq2 
z = a -> (a < z <-> a < a)
89 87, 88 imeqd 
z = a -> (z e. A -> a < z <-> a e. A -> a < a)
90 89 eale 
A. z (z e. A -> a < z) -> a e. A -> a < a
91 90 com12 
a e. A -> A. z (z e. A -> a < z) -> a < a
92 86, 91 mtd 
a e. A -> ~A. z (z e. A -> a < z)
93 84, 92 syl 
a e. A -> E. u (u e. A /\ A. z (z e. A -> u <= z))
94 anll 
u e. A /\ A. z (z e. A -> u <= z) /\ (v e. A /\ A. z (z e. A -> v <= z)) -> u e. A
95 eleq1 
z = u -> (z e. A <-> u e. A)
96 leeq2 
z = u -> (v <= z <-> v <= u)
97 95, 96 imeqd 
z = u -> (z e. A -> v <= z <-> u e. A -> v <= u)
98 97 eale 
A. z (z e. A -> v <= z) -> u e. A -> v <= u
99 98 anwr 
v e. A /\ A. z (z e. A -> v <= z) -> u e. A -> v <= u
100 99 anwr 
u e. A /\ A. z (z e. A -> u <= z) /\ (v e. A /\ A. z (z e. A -> v <= z)) -> u e. A -> v <= u
101 94, 100 mpd 
u e. A /\ A. z (z e. A -> u <= z) /\ (v e. A /\ A. z (z e. A -> v <= z)) -> v <= u
102 anrl 
u e. A /\ A. z (z e. A -> u <= z) /\ (v e. A /\ A. z (z e. A -> v <= z)) -> v e. A
103 eleq1 
z = v -> (z e. A <-> v e. A)
104 leeq2 
z = v -> (u <= z <-> u <= v)
105 103, 104 imeqd 
z = v -> (z e. A -> u <= z <-> v e. A -> u <= v)
106 105 eale 
A. z (z e. A -> u <= z) -> v e. A -> u <= v
107 106 anwr 
u e. A /\ A. z (z e. A -> u <= z) -> v e. A -> u <= v
108 107 anwl 
u e. A /\ A. z (z e. A -> u <= z) /\ (v e. A /\ A. z (z e. A -> v <= z)) -> v e. A -> u <= v
109 102, 108 mpd 
u e. A /\ A. z (z e. A -> u <= z) /\ (v e. A /\ A. z (z e. A -> v <= z)) -> u <= v
110 101, 109 leasymd 
u e. A /\ A. z (z e. A -> u <= z) /\ (v e. A /\ A. z (z e. A -> v <= z)) -> v = u
111 110 exp 
u e. A /\ A. z (z e. A -> u <= z) -> v e. A /\ A. z (z e. A -> v <= z) -> v = u
112 eleq1 
v = u -> (v e. A <-> u e. A)
113 leeq1 
v = u -> (v <= z <-> u <= z)
114 113 imeq2d 
v = u -> (z e. A -> v <= z <-> z e. A -> u <= z)
115 114 aleqd 
v = u -> (A. z (z e. A -> v <= z) <-> A. z (z e. A -> u <= z))
116 112, 115 aneqd 
v = u -> (v e. A /\ A. z (z e. A -> v <= z) <-> u e. A /\ A. z (z e. A -> u <= z))
117 116 bi2d 
v = u -> u e. A /\ A. z (z e. A -> u <= z) -> v e. A /\ A. z (z e. A -> v <= z)
118 117 com12 
u e. A /\ A. z (z e. A -> u <= z) -> v = u -> v e. A /\ A. z (z e. A -> v <= z)
119 111, 118 ibid 
u e. A /\ A. z (z e. A -> u <= z) -> (v e. A /\ A. z (z e. A -> v <= z) <-> v = u)
120 119 eqtheabd 
u e. A /\ A. z (z e. A -> u <= z) -> the {v | v e. A /\ A. z (z e. A -> v <= z)} = u
121 120 conv least 
u e. A /\ A. z (z e. A -> u <= z) -> least A = u
122 eleq1 
least A = u -> (least A e. A <-> u e. A)
123 leeq1 
least A = u -> (least A <= z <-> u <= z)
124 123 imeq2d 
least A = u -> (z e. A -> least A <= z <-> z e. A -> u <= z)
125 124 aleqd 
least A = u -> (A. z (z e. A -> least A <= z) <-> A. z (z e. A -> u <= z))
126 122, 125 aneqd 
least A = u -> (least A e. A /\ A. z (z e. A -> least A <= z) <-> u e. A /\ A. z (z e. A -> u <= z))
127 121, 126 rsyl 
u e. A /\ A. z (z e. A -> u <= z) -> (least A e. A /\ A. z (z e. A -> least A <= z) <-> u e. A /\ A. z (z e. A -> u <= z))
128 id 
u e. A /\ A. z (z e. A -> u <= z) -> u e. A /\ A. z (z e. A -> u <= z)
129 127, 128 mpbird 
u e. A /\ A. z (z e. A -> u <= z) -> least A e. A /\ A. z (z e. A -> least A <= z)
130 129 eex 
E. u (u e. A /\ A. z (z e. A -> u <= z)) -> least A e. A /\ A. z (z e. A -> least A <= z)
131 93, 130 rsyl 
a e. A -> least A e. A /\ A. z (z e. A -> least A <= z)

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), axs_peano (peano1, peano2, peano5, addeq, add0, addS)