Theorem finlam ≪ | index | src | ≫ 

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