Theorem optfin ≪ | index | src | ≫ 

theorem optfin (A: set): $ finite A -> finite (Option A) $;
StepHypRefExpression
1 lteq1 
x = 0 -> (x < m <-> 0 < m)
2 lt01S 
0 < suc n
3 lteq2 
m = suc n -> (0 < m <-> 0 < suc n)
4 2, 3 mpbiri 
m = suc n -> 0 < m
5 4 anwr 
A. y (y e. A -> y < n) /\ m = suc n -> 0 < m
6 1, 5 syl5ibrcom 
A. y (y e. A -> y < n) /\ m = suc n -> x = 0 -> x < m
7 6 imp 
A. y (y e. A -> y < n) /\ m = suc n /\ x = 0 -> x < m
8 7 a1d 
A. y (y e. A -> y < n) /\ m = suc n /\ x = 0 -> x e. Option A -> x < m
9 sub1can 
x != 0 -> suc (x - 1) = x
10 9 conv ne 
~x = 0 -> suc (x - 1) = x
11 10 anwr 
A. y (y e. A -> y < n) /\ m = suc n /\ ~x = 0 -> suc (x - 1) = x
12 11 eqcomd 
A. y (y e. A -> y < n) /\ m = suc n /\ ~x = 0 -> x = suc (x - 1)
13 12 eleq1d 
A. y (y e. A -> y < n) /\ m = suc n /\ ~x = 0 -> (x e. Option A <-> suc (x - 1) e. Option A)
14 anlr 
A. y (y e. A -> y < n) /\ m = suc n /\ ~x = 0 -> m = suc n
15 12, 14 lteqd 
A. y (y e. A -> y < n) /\ m = suc n /\ ~x = 0 -> (x < m <-> suc (x - 1) < suc n)
16 13, 15 imeqd 
A. y (y e. A -> y < n) /\ m = suc n /\ ~x = 0 -> (x e. Option A -> x < m <-> suc (x - 1) e. Option A -> suc (x - 1) < suc n)
17 bicom 
(suc (x - 1) e. Option A <-> x - 1 e. A) -> (x - 1 e. A <-> suc (x - 1) e. Option A)
18 optS 
suc (x - 1) e. Option A <-> x - 1 e. A
19 17, 18 ax_mp 
x - 1 e. A <-> suc (x - 1) e. Option A
20 ltsuc 
x - 1 < n <-> suc (x - 1) < suc n
21 19, 20 imeqi 
x - 1 e. A -> x - 1 < n <-> suc (x - 1) e. Option A -> suc (x - 1) < suc n
22 eleq1 
y = x - 1 -> (y e. A <-> x - 1 e. A)
23 lteq1 
y = x - 1 -> (y < n <-> x - 1 < n)
24 22, 23 imeqd 
y = x - 1 -> (y e. A -> y < n <-> x - 1 e. A -> x - 1 < n)
25 24 eale 
A. y (y e. A -> y < n) -> x - 1 e. A -> x - 1 < n
26 25 anwll 
A. y (y e. A -> y < n) /\ m = suc n /\ ~x = 0 -> x - 1 e. A -> x - 1 < n
27 21, 26 sylib 
A. y (y e. A -> y < n) /\ m = suc n /\ ~x = 0 -> suc (x - 1) e. Option A -> suc (x - 1) < suc n
28 16, 27 mpbird 
A. y (y e. A -> y < n) /\ m = suc n /\ ~x = 0 -> x e. Option A -> x < m
29 8, 28 casesda 
A. y (y e. A -> y < n) /\ m = suc n -> x e. Option A -> x < m
30 29 iald 
A. y (y e. A -> y < n) /\ m = suc n -> A. x (x e. Option A -> x < m)
31 30 iexde 
A. y (y e. A -> y < n) -> E. m A. x (x e. Option A -> x < m)
32 31 conv finite 
A. y (y e. A -> y < n) -> finite (Option A)
33 32 eex 
E. n A. y (y e. A -> y < n) -> finite (Option A)
34 33 conv finite 
finite A -> finite (Option 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, add0, addS)