Theorem eqlower ≪ | index | src | ≫ 

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