Theorem eqlower ≪ | index | src | ≫ 

pub theorem eqlower (A: set): $ finite A <-> A == lower A $;
StepHypRefExpression
1 biidd 
y = z -> (x e. n <-> x e. n)
2 eqidd 
y = z -> x = x
3 id 
y = z -> y = z
4 2, 3 addeqd 
y = z -> x + y = x + z
5 eqsidd 
y = z -> A == A
6 4, 5 eleqd 
y = z -> (x + y e. A <-> x + z e. A)
7 1, 6 bieqd 
y = z -> (x e. n <-> x + y e. A <-> (x e. n <-> x + z e. A))
8 7 aleqd 
y = z -> (A. x (x e. n <-> x + y e. A) <-> A. x (x e. n <-> x + z e. A))
9 8 exeqd 
y = z -> (E. n A. x (x e. n <-> x + y e. A) <-> E. n A. x (x e. n <-> x + z e. A))
10 biidd 
y = z -> (E. n A == n <-> E. n A == n)
11 9, 10 imeqd 
y = z -> (E. n A. x (x e. n <-> x + y e. A) -> E. n A == n <-> E. n A. x (x e. n <-> x + z e. A) -> E. n A == n)
12 biidd 
y = 0 -> (x e. n <-> x e. n)
13 eqidd 
y = 0 -> x = x
14 id 
y = 0 -> y = 0
15 13, 14 addeqd 
y = 0 -> x + y = x + 0
16 eqsidd 
y = 0 -> A == A
17 15, 16 eleqd 
y = 0 -> (x + y e. A <-> x + 0 e. A)
18 12, 17 bieqd 
y = 0 -> (x e. n <-> x + y e. A <-> (x e. n <-> x + 0 e. A))
19 18 aleqd 
y = 0 -> (A. x (x e. n <-> x + y e. A) <-> A. x (x e. n <-> x + 0 e. A))
20 19 exeqd 
y = 0 -> (E. n A. x (x e. n <-> x + y e. A) <-> E. n A. x (x e. n <-> x + 0 e. A))
21 biidd 
y = 0 -> (E. n A == n <-> E. n A == n)
22 20, 21 imeqd 
y = 0 -> (E. n A. x (x e. n <-> x + y e. A) -> E. n A == n <-> E. n A. x (x e. n <-> x + 0 e. A) -> E. n A == n)
23 biidd 
y = suc z -> (x e. n <-> x e. n)
24 eqidd 
y = suc z -> x = x
25 id 
y = suc z -> y = suc z
26 24, 25 addeqd 
y = suc z -> x + y = x + suc z
27 eqsidd 
y = suc z -> A == A
28 26, 27 eleqd 
y = suc z -> (x + y e. A <-> x + suc z e. A)
29 23, 28 bieqd 
y = suc z -> (x e. n <-> x + y e. A <-> (x e. n <-> x + suc z e. A))
30 29 aleqd 
y = suc z -> (A. x (x e. n <-> x + y e. A) <-> A. x (x e. n <-> x + suc z e. A))
31 30 exeqd 
y = suc z -> (E. n A. x (x e. n <-> x + y e. A) <-> E. n A. x (x e. n <-> x + suc z e. A))
32 biidd 
y = suc z -> (E. n A == n <-> E. n A == n)
33 31, 32 imeqd 
y = suc z -> (E. n A. x (x e. n <-> x + y e. A) -> E. n A == n <-> E. n A. x (x e. n <-> x + suc z e. A) -> E. n A == n)
34 eleq1 
x + 0 = x -> (x + 0 e. A <-> x e. A)
35 add0 
x + 0 = x
36 34, 35 ax_mp 
x + 0 e. A <-> x e. A
37 id 
(x e. n <-> x + 0 e. A) -> (x e. n <-> x + 0 e. A)
38 36, 37 syl6bb 
(x e. n <-> x + 0 e. A) -> (x e. n <-> x e. A)
39 38 bicomd 
(x e. n <-> x + 0 e. A) -> (x e. A <-> x e. n)
40 39 alimi 
A. x (x e. n <-> x + 0 e. A) -> A. x (x e. A <-> x e. n)
41 40 conv eqs 
A. x (x e. n <-> x + 0 e. A) -> A == n
42 41 eximi 
E. n A. x (x e. n <-> x + 0 e. A) -> E. n A == n
43 anr 
m = n /\ y = x -> y = x
44 anl 
m = n /\ y = x -> m = n
45 43, 44 elneqd 
m = n /\ y = x -> (y e. m <-> x e. n)
46 addeq1 
y = x -> y + z = x + z
47 46 anwr 
m = n /\ y = x -> y + z = x + z
48 47 eleq1d 
m = n /\ y = x -> (y + z e. A <-> x + z e. A)
49 45, 48 bieqd 
m = n /\ y = x -> (y e. m <-> y + z e. A <-> (x e. n <-> x + z e. A))
50 49 cbvald 
m = n -> (A. y (y e. m <-> y + z e. A) <-> A. x (x e. n <-> x + z e. A))
51 50 cbvex 
E. m A. y (y e. m <-> y + z e. A) <-> E. n A. x (x e. n <-> x + z e. A)
52 bitr 
(0 e. if (z e. A) (b1 n) (b0 n) <-> odd (if (z e. A) (b1 n) (b0 n))) ->
  (odd (if (z e. A) (b1 n) (b0 n)) <-> z e. A) ->
  (0 e. if (z e. A) (b1 n) (b0 n) <-> z e. A)
53 el01 
0 e. if (z e. A) (b1 n) (b0 n) <-> odd (if (z e. A) (b1 n) (b0 n))
54 52, 53 ax_mp 
(odd (if (z e. A) (b1 n) (b0 n)) <-> z e. A) -> (0 e. if (z e. A) (b1 n) (b0 n) <-> z e. A)
55 ax_3 
(~z e. A -> ~odd (if (z e. A) (b1 n) (b0 n))) -> odd (if (z e. A) (b1 n) (b0 n)) -> z e. A
56 ifneg 
~z e. A -> if (z e. A) (b1 n) (b0 n) = b0 n
57 56 oddeqd 
~z e. A -> (odd (if (z e. A) (b1 n) (b0 n)) <-> odd (b0 n))
58 b0odd 
~odd (b0 n)
59 58 a1i 
~z e. A -> ~odd (b0 n)
60 57, 59 mtbird 
~z e. A -> ~odd (if (z e. A) (b1 n) (b0 n))
61 55, 60 ax_mp 
odd (if (z e. A) (b1 n) (b0 n)) -> z e. A
62 b1odd 
odd (b1 n)
63 ifpos 
z e. A -> if (z e. A) (b1 n) (b0 n) = b1 n
64 63 oddeqd 
z e. A -> (odd (if (z e. A) (b1 n) (b0 n)) <-> odd (b1 n))
65 62, 64 mpbiri 
z e. A -> odd (if (z e. A) (b1 n) (b0 n))
66 61, 65 ibii 
odd (if (z e. A) (b1 n) (b0 n)) <-> z e. A
67 54, 66 ax_mp 
0 e. if (z e. A) (b1 n) (b0 n) <-> z e. A
68 anr 
m = if (z e. A) (b1 n) (b0 n) /\ y = 0 -> y = 0
69 anl 
m = if (z e. A) (b1 n) (b0 n) /\ y = 0 -> m = if (z e. A) (b1 n) (b0 n)
70 68, 69 elneqd 
m = if (z e. A) (b1 n) (b0 n) /\ y = 0 -> (y e. m <-> 0 e. if (z e. A) (b1 n) (b0 n))
71 add01 
0 + z = z
72 addeq1 
y = 0 -> y + z = 0 + z
73 72 anwr 
m = if (z e. A) (b1 n) (b0 n) /\ y = 0 -> y + z = 0 + z
74 71, 73 syl6eq 
m = if (z e. A) (b1 n) (b0 n) /\ y = 0 -> y + z = z
75 74 eleq1d 
m = if (z e. A) (b1 n) (b0 n) /\ y = 0 -> (y + z e. A <-> z e. A)
76 70, 75 bieqd 
m = if (z e. A) (b1 n) (b0 n) /\ y = 0 -> (y e. m <-> y + z e. A <-> (0 e. if (z e. A) (b1 n) (b0 n) <-> z e. A))
77 67, 76 mpbiri 
m = if (z e. A) (b1 n) (b0 n) /\ y = 0 -> (y e. m <-> y + z e. A)
78 77 a1d 
m = if (z e. A) (b1 n) (b0 n) /\ y = 0 -> A. x (x e. n <-> x + suc z e. A) -> (y e. m <-> y + z e. A)
79 bitr3 
(y - 1 e. if (z e. A) (b1 n) (b0 n) // 2 <-> y - 1 e. n) ->
  (y - 1 e. if (z e. A) (b1 n) (b0 n) // 2 <-> suc (y - 1) e. if (z e. A) (b1 n) (b0 n)) ->
  (y - 1 e. n <-> suc (y - 1) e. if (z e. A) (b1 n) (b0 n))
80 elneq2 
if (z e. A) (b1 n) (b0 n) // 2 = n -> (y - 1 e. if (z e. A) (b1 n) (b0 n) // 2 <-> y - 1 e. n)
81 b1div2 
b1 n // 2 = n
82 63 diveq1d 
z e. A -> if (z e. A) (b1 n) (b0 n) // 2 = b1 n // 2
83 81, 82 syl6eq 
z e. A -> if (z e. A) (b1 n) (b0 n) // 2 = n
84 b0div2 
b0 n // 2 = n
85 56 diveq1d 
~z e. A -> if (z e. A) (b1 n) (b0 n) // 2 = b0 n // 2
86 84, 85 syl6eq 
~z e. A -> if (z e. A) (b1 n) (b0 n) // 2 = n
87 83, 86 cases 
if (z e. A) (b1 n) (b0 n) // 2 = n
88 80, 87 ax_mp 
y - 1 e. if (z e. A) (b1 n) (b0 n) // 2 <-> y - 1 e. n
89 79, 88 ax_mp 
(y - 1 e. if (z e. A) (b1 n) (b0 n) // 2 <-> suc (y - 1) e. if (z e. A) (b1 n) (b0 n)) -> (y - 1 e. n <-> suc (y - 1) e. if (z e. A) (b1 n) (b0 n))
90 eldiv2 
y - 1 e. if (z e. A) (b1 n) (b0 n) // 2 <-> suc (y - 1) e. if (z e. A) (b1 n) (b0 n)
91 89, 90 ax_mp 
y - 1 e. n <-> suc (y - 1) e. if (z e. A) (b1 n) (b0 n)
92 anr 
m = if (z e. A) (b1 n) (b0 n) /\ ~y = 0 /\ x = y - 1 -> x = y - 1
93 92 eleq1d 
m = if (z e. A) (b1 n) (b0 n) /\ ~y = 0 /\ x = y - 1 -> (x e. n <-> y - 1 e. n)
94 sub1can 
y != 0 -> suc (y - 1) = y
95 anlr 
m = if (z e. A) (b1 n) (b0 n) /\ ~y = 0 /\ x = y - 1 -> ~y = 0
96 95 conv ne 
m = if (z e. A) (b1 n) (b0 n) /\ ~y = 0 /\ x = y - 1 -> y != 0
97 94, 96 syl 
m = if (z e. A) (b1 n) (b0 n) /\ ~y = 0 /\ x = y - 1 -> suc (y - 1) = y
98 97 eqcomd 
m = if (z e. A) (b1 n) (b0 n) /\ ~y = 0 /\ x = y - 1 -> y = suc (y - 1)
99 anll 
m = if (z e. A) (b1 n) (b0 n) /\ ~y = 0 /\ x = y - 1 -> m = if (z e. A) (b1 n) (b0 n)
100 98, 99 elneqd 
m = if (z e. A) (b1 n) (b0 n) /\ ~y = 0 /\ x = y - 1 -> (y e. m <-> suc (y - 1) e. if (z e. A) (b1 n) (b0 n))
101 93, 100 bieqd 
m = if (z e. A) (b1 n) (b0 n) /\ ~y = 0 /\ x = y - 1 -> (x e. n <-> y e. m <-> (y - 1 e. n <-> suc (y - 1) e. if (z e. A) (b1 n) (b0 n)))
102 91, 101 mpbiri 
m = if (z e. A) (b1 n) (b0 n) /\ ~y = 0 /\ x = y - 1 -> (x e. n <-> y e. m)
103 addSass 
suc x + z = x + suc z
104 92 suceqd 
m = if (z e. A) (b1 n) (b0 n) /\ ~y = 0 /\ x = y - 1 -> suc x = suc (y - 1)
105 104, 97 eqtrd 
m = if (z e. A) (b1 n) (b0 n) /\ ~y = 0 /\ x = y - 1 -> suc x = y
106 105 addeq1d 
m = if (z e. A) (b1 n) (b0 n) /\ ~y = 0 /\ x = y - 1 -> suc x + z = y + z
107 103, 106 syl5eqr 
m = if (z e. A) (b1 n) (b0 n) /\ ~y = 0 /\ x = y - 1 -> x + suc z = y + z
108 107 eleq1d 
m = if (z e. A) (b1 n) (b0 n) /\ ~y = 0 /\ x = y - 1 -> (x + suc z e. A <-> y + z e. A)
109 102, 108 bieqd 
m = if (z e. A) (b1 n) (b0 n) /\ ~y = 0 /\ x = y - 1 -> (x e. n <-> x + suc z e. A <-> (y e. m <-> y + z e. A))
110 109 bi1d 
m = if (z e. A) (b1 n) (b0 n) /\ ~y = 0 /\ x = y - 1 -> (x e. n <-> x + suc z e. A) -> (y e. m <-> y + z e. A)
111 110 ealde 
m = if (z e. A) (b1 n) (b0 n) /\ ~y = 0 -> A. x (x e. n <-> x + suc z e. A) -> (y e. m <-> y + z e. A)
112 78, 111 casesda 
m = if (z e. A) (b1 n) (b0 n) -> A. x (x e. n <-> x + suc z e. A) -> (y e. m <-> y + z e. A)
113 112 impcom 
A. x (x e. n <-> x + suc z e. A) /\ m = if (z e. A) (b1 n) (b0 n) -> (y e. m <-> y + z e. A)
114 113 iald 
A. x (x e. n <-> x + suc z e. A) /\ m = if (z e. A) (b1 n) (b0 n) -> A. y (y e. m <-> y + z e. A)
115 114 iexde 
A. x (x e. n <-> x + suc z e. A) -> E. m A. y (y e. m <-> y + z e. A)
116 115 eex 
E. n A. x (x e. n <-> x + suc z e. A) -> E. m A. y (y e. m <-> y + z e. A)
117 51, 116 sylib 
E. n A. x (x e. n <-> x + suc z e. A) -> E. n A. x (x e. n <-> x + z e. A)
118 117 imim1i 
(E. n A. x (x e. n <-> x + z e. A) -> E. n A == n) -> E. n A. x (x e. n <-> x + suc z e. A) -> E. n A == n
119 11, 22, 11, 33, 42, 118 ind 
E. n A. x (x e. n <-> x + z e. A) -> E. n A == n
120 anr 
A. y (y e. A -> y < z) /\ n = 0 -> n = 0
121 120 elneq2d 
A. y (y e. A -> y < z) /\ n = 0 -> (x e. n <-> x e. 0)
122 el02 
~x e. 0
123 122 a1i 
A. y (y e. A -> y < z) /\ n = 0 -> ~x e. 0
124 lenlt 
z <= x + z <-> ~x + z < z
125 leaddid2 
z <= x + z
126 124, 125 mpbi 
~x + z < z
127 126 a1i 
A. y (y e. A -> y < z) /\ n = 0 -> ~x + z < z
128 eleq1 
y = x + z -> (y e. A <-> x + z e. A)
129 lteq1 
y = x + z -> (y < z <-> x + z < z)
130 128, 129 imeqd 
y = x + z -> (y e. A -> y < z <-> x + z e. A -> x + z < z)
131 130 eale 
A. y (y e. A -> y < z) -> x + z e. A -> x + z < z
132 131 anwl 
A. y (y e. A -> y < z) /\ n = 0 -> x + z e. A -> x + z < z
133 127, 132 mtd 
A. y (y e. A -> y < z) /\ n = 0 -> ~x + z e. A
134 123, 133 binthd 
A. y (y e. A -> y < z) /\ n = 0 -> (x e. 0 <-> x + z e. A)
135 121, 134 bitrd 
A. y (y e. A -> y < z) /\ n = 0 -> (x e. n <-> x + z e. A)
136 135 iald 
A. y (y e. A -> y < z) /\ n = 0 -> A. x (x e. n <-> x + z e. A)
137 136 iexde 
A. y (y e. A -> y < z) -> E. n A. x (x e. n <-> x + z e. A)
138 119, 137 syl 
A. y (y e. A -> y < z) -> E. n A == n
139 138 eex 
E. z A. y (y e. A -> y < z) -> E. n A == n
140 139 conv finite 
finite A -> E. n A == n
141 id 
A == n -> A == n
142 nsinj 
x == n <-> x = n
143 eqseq2 
A == n -> (x == A <-> x == n)
144 142, 143 syl6bb 
A == n -> (x == A <-> x = n)
145 144 eqtheabd 
A == n -> the {x | x == A} = n
146 145 conv lower 
A == n -> lower A = n
147 146 eqcomd 
A == n -> n = lower A
148 147 nseqd 
A == n -> n == lower A
149 141, 148 eqstrd 
A == n -> A == lower A
150 149 eex 
E. n A == n -> A == lower A
151 140, 150 rsyl 
finite A -> A == lower A
152 finns 
finite (lower A)
153 fineq 
A == lower A -> (finite A <-> finite (lower A))
154 152, 153 mpbiri 
A == lower A -> finite A
155 151, 154 ibii 
finite A <-> A == lower A

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)