Theorem finlam ≪ | index | src | ≫ 

theorem finlam (A: set) {x: nat} (v: nat x):
  $ finite A -> finite ((\ x, v) |` A) $;
StepHypRefExpression
1 id 
_1 = m -> _1 = m
2 1 lteq2d 
_1 = m -> (x < _1 <-> x < m)
3 2 imeq1d 
_1 = m -> (x < _1 -> x, v < n <-> x < m -> x, v < n)
4 3 aleqd 
_1 = m -> (A. x (x < _1 -> x, v < n) <-> A. x (x < m -> x, v < n))
5 4 exeqd 
_1 = m -> (E. n A. x (x < _1 -> x, v < n) <-> E. n A. x (x < m -> x, v < n))
6 id 
_1 = 0 -> _1 = 0
7 6 lteq2d 
_1 = 0 -> (x < _1 <-> x < 0)
8 7 imeq1d 
_1 = 0 -> (x < _1 -> x, v < n <-> x < 0 -> x, v < n)
9 8 aleqd 
_1 = 0 -> (A. x (x < _1 -> x, v < n) <-> A. x (x < 0 -> x, v < n))
10 9 exeqd 
_1 = 0 -> (E. n A. x (x < _1 -> x, v < n) <-> E. n A. x (x < 0 -> x, v < n))
11 id 
_1 = a1 -> _1 = a1
12 11 lteq2d 
_1 = a1 -> (x < _1 <-> x < a1)
13 12 imeq1d 
_1 = a1 -> (x < _1 -> x, v < n <-> x < a1 -> x, v < n)
14 13 aleqd 
_1 = a1 -> (A. x (x < _1 -> x, v < n) <-> A. x (x < a1 -> x, v < n))
15 14 exeqd 
_1 = a1 -> (E. n A. x (x < _1 -> x, v < n) <-> E. n A. x (x < a1 -> x, v < n))
16 id 
_1 = suc a1 -> _1 = suc a1
17 16 lteq2d 
_1 = suc a1 -> (x < _1 <-> x < suc a1)
18 17 imeq1d 
_1 = suc a1 -> (x < _1 -> x, v < n <-> x < suc a1 -> x, v < n)
19 18 aleqd 
_1 = suc a1 -> (A. x (x < _1 -> x, v < n) <-> A. x (x < suc a1 -> x, v < n))
20 19 exeqd 
_1 = suc a1 -> (E. n A. x (x < _1 -> x, v < n) <-> E. n A. x (x < suc a1 -> x, v < n))
21 absurd 
~x < 0 -> x < 0 -> x, v < n
22 lt02 
~x < 0
23 21, 22 ax_mp 
x < 0 -> x, v < n
24 23 a1i 
n = a2 -> x < 0 -> x, v < n
25 24 iald 
n = a2 -> A. x (x < 0 -> x, v < n)
26 25 iexie 
E. n A. x (x < 0 -> x, v < n)
27 lteq2 
n = a3 -> (x, v < n <-> x, v < a3)
28 27 imeq2d 
n = a3 -> (x < suc a1 -> x, v < n <-> x < suc a1 -> x, v < a3)
29 28 aleqd 
n = a3 -> (A. x (x < suc a1 -> x, v < n) <-> A. x (x < suc a1 -> x, v < a3))
30 29 cbvex 
E. n A. x (x < suc a1 -> x, v < n) <-> E. a3 A. x (x < suc a1 -> x, v < a3)
31 nfnv 
FN/ x n
32 nfnv 
FN/ x a1
33 nfsbn1 
FN/ x N[a1 / x] v
34 32, 33 nfpr 
FN/ x a1, N[a1 / x] v
35 34 nfsuc 
FN/ x suc (a1, N[a1 / x] v)
36 31, 35 nfmax 
FN/ x max n (suc (a1, N[a1 / x] v))
37 36 nfeq2 
F/ x a3 = max n (suc (a1, N[a1 / x] v))
38 lteq2 
a3 = max n (suc (a1, N[a1 / x] v)) -> (x, v < a3 <-> x, v < max n (suc (a1, N[a1 / x] v)))
39 38 imeq2d 
a3 = max n (suc (a1, N[a1 / x] v)) -> (x < suc a1 -> x, v < a3 <-> x < suc a1 -> x, v < max n (suc (a1, N[a1 / x] v)))
40 37, 39 aleqdh 
a3 = max n (suc (a1, N[a1 / x] v)) -> (A. x (x < suc a1 -> x, v < a3) <-> A. x (x < suc a1 -> x, v < max n (suc (a1, N[a1 / x] v))))
41 40 iexe 
A. x (x < suc a1 -> x, v < max n (suc (a1, N[a1 / x] v))) -> E. a3 A. x (x < suc a1 -> x, v < a3)
42 leltsuc 
x <= a1 <-> x < suc a1
43 leloe 
x <= a1 <-> x < a1 \/ x = a1
44 lemax1 
n <= max n (suc (a1, N[a1 / x] v))
45 ltletr 
x, v < n -> n <= max n (suc (a1, N[a1 / x] v)) -> x, v < max n (suc (a1, N[a1 / x] v))
46 44, 45 mpi 
x, v < n -> x, v < max n (suc (a1, N[a1 / x] v))
47 46 imim2i 
(x < a1 -> x, v < n) -> x < a1 -> x, v < max n (suc (a1, N[a1 / x] v))
48 lemax2 
suc (x, v) <= max n (suc (x, v))
49 eqidd 
x = a1 -> n = n
50 id 
x = a1 -> x = a1
51 sbnq 
x = a1 -> v = N[a1 / x] v
52 50, 51 preqd 
x = a1 -> x, v = a1, N[a1 / x] v
53 52 suceqd 
x = a1 -> suc (x, v) = suc (a1, N[a1 / x] v)
54 49, 53 maxeqd 
x = a1 -> max n (suc (x, v)) = max n (suc (a1, N[a1 / x] v))
55 54 lteq2d 
x = a1 -> (x, v < max n (suc (x, v)) <-> x, v < max n (suc (a1, N[a1 / x] v)))
56 55 conv lt 
x = a1 -> (suc (x, v) <= max n (suc (x, v)) <-> x, v < max n (suc (a1, N[a1 / x] v)))
57 48, 56 mpbii 
x = a1 -> x, v < max n (suc (a1, N[a1 / x] v))
58 57 a1i 
(x < a1 -> x, v < n) -> x = a1 -> x, v < max n (suc (a1, N[a1 / x] v))
59 47, 58 eord 
(x < a1 -> x, v < n) -> x < a1 \/ x = a1 -> x, v < max n (suc (a1, N[a1 / x] v))
60 43, 59 syl5bi 
(x < a1 -> x, v < n) -> x <= a1 -> x, v < max n (suc (a1, N[a1 / x] v))
61 42, 60 syl5bir 
(x < a1 -> x, v < n) -> x < suc a1 -> x, v < max n (suc (a1, N[a1 / x] v))
62 61 alimi 
A. x (x < a1 -> x, v < n) -> A. x (x < suc a1 -> x, v < max n (suc (a1, N[a1 / x] v)))
63 41, 62 syl 
A. x (x < a1 -> x, v < n) -> E. a3 A. x (x < suc a1 -> x, v < a3)
64 63 eex 
E. n A. x (x < a1 -> x, v < n) -> E. a3 A. x (x < suc a1 -> x, v < a3)
65 30, 64 sylibr 
E. n A. x (x < a1 -> x, v < n) -> E. n A. x (x < suc a1 -> x, v < n)
66 5, 10, 15, 20, 26, 65 ind 
E. n A. x (x < m -> x, v < n)
67 elres 
p e. (\ x, v) |` A <-> p e. \ x, v /\ fst p e. A
68 impexp 
p e. \ x, v /\ fst p e. A -> p < n <-> p e. \ x, v -> fst p e. A -> p < n
69 eqeq1 
q = p -> (q = x, v <-> p = x, v)
70 69 exeqd 
q = p -> (E. x q = x, v <-> E. x p = x, v)
71 70 elabe 
p e. {q | E. x q = x, v} <-> E. x p = x, v
72 71 conv lam 
p e. \ x, v <-> E. x p = x, v
73 eexb 
E. x p = x, v -> fst p e. A -> p < n <-> A. x (p = x, v -> fst p e. A -> p < n)
74 fstpr 
fst (x, v) = x
75 fsteq 
p = x, v -> fst p = fst (x, v)
76 74, 75 syl6eq 
p = x, v -> fst p = x
77 76 eleq1d 
p = x, v -> (fst p e. A <-> x e. A)
78 lteq1 
p = x, v -> (p < n <-> x, v < n)
79 77, 78 imeqd 
p = x, v -> (fst p e. A -> p < n <-> x e. A -> x, v < n)
80 id 
(x e. A -> x, v < n) -> x e. A -> x, v < n
81 79, 80 syl5ibrcom 
(x e. A -> x, v < n) -> p = x, v -> fst p e. A -> p < n
82 81 alimi 
A. x (x e. A -> x, v < n) -> A. x (p = x, v -> fst p e. A -> p < n)
83 73, 82 sylibr 
A. x (x e. A -> x, v < n) -> E. x p = x, v -> fst p e. A -> p < n
84 72, 83 syl5bi 
A. x (x e. A -> x, v < n) -> p e. \ x, v -> fst p e. A -> p < n
85 68, 84 sylibr 
A. x (x e. A -> x, v < n) -> p e. \ x, v /\ fst p e. A -> p < n
86 67, 85 syl5bi 
A. x (x e. A -> x, v < n) -> p e. (\ x, v) |` A -> p < n
87 86 iald 
A. x (x e. A -> x, v < n) -> A. p (p e. (\ x, v) |` A -> p < n)
88 anl 
(x e. A -> x < m) /\ (x < m -> x, v < n) -> x e. A -> x < m
89 anr 
(x e. A -> x < m) /\ (x < m -> x, v < n) -> x < m -> x, v < n
90 88, 89 syld 
(x e. A -> x < m) /\ (x < m -> x, v < n) -> x e. A -> x, v < n
91 90 exp 
(x e. A -> x < m) -> (x < m -> x, v < n) -> x e. A -> x, v < n
92 91 al2imi 
A. x (x e. A -> x < m) -> A. x (x < m -> x, v < n) -> A. x (x e. A -> x, v < n)
93 87, 92 syl6 
A. x (x e. A -> x < m) -> A. x (x < m -> x, v < n) -> A. p (p e. (\ x, v) |` A -> p < n)
94 93 eximd 
A. x (x e. A -> x < m) -> E. n A. x (x < m -> x, v < n) -> E. n A. p (p e. (\ x, v) |` A -> p < n)
95 94 conv finite 
A. x (x e. A -> x < m) -> E. n A. x (x < m -> x, v < n) -> finite ((\ x, v) |` A)
96 66, 95 mpi 
A. x (x e. A -> x < m) -> finite ((\ x, v) |` A)
97 96 eex 
E. m A. x (x e. A -> x < m) -> finite ((\ x, v) |` A)
98 97 conv finite 
finite A -> finite ((\ x, v) |` 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)