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