Theorem Arrayfin ≪ | index | src | ≫ 

theorem Arrayfin (A: set) (n: nat): $ finite A -> finite (Array A n) $;
StepHypRefExpression
1 id 
_1 = n -> _1 = n
2 1 Arrayeq2d 
_1 = n -> Array A _1 == Array A n
3 2 fineqd 
_1 = n -> (finite (Array A _1) <-> finite (Array A n))
4 id 
_1 = 0 -> _1 = 0
5 4 Arrayeq2d 
_1 = 0 -> Array A _1 == Array A 0
6 5 fineqd 
_1 = 0 -> (finite (Array A _1) <-> finite (Array A 0))
7 id 
_1 = a1 -> _1 = a1
8 7 Arrayeq2d 
_1 = a1 -> Array A _1 == Array A a1
9 8 fineqd 
_1 = a1 -> (finite (Array A _1) <-> finite (Array A a1))
10 id 
_1 = suc a1 -> _1 = suc a1
11 10 Arrayeq2d 
_1 = suc a1 -> Array A _1 == Array A (suc a1)
12 11 fineqd 
_1 = suc a1 -> (finite (Array A _1) <-> finite (Array A (suc a1)))
13 fineq 
Array A 0 == sn 0 -> (finite (Array A 0) <-> finite (sn 0))
14 bitr4 
(a2 e. Array A 0 <-> a2 = 0) -> (a2 e. sn 0 <-> a2 = 0) -> (a2 e. Array A 0 <-> a2 e. sn 0)
15 elArray02 
a2 e. Array A 0 <-> a2 = 0
16 14, 15 ax_mp 
(a2 e. sn 0 <-> a2 = 0) -> (a2 e. Array A 0 <-> a2 e. sn 0)
17 elsn 
a2 e. sn 0 <-> a2 = 0
18 16, 17 ax_mp 
a2 e. Array A 0 <-> a2 e. sn 0
19 18 eqri 
Array A 0 == sn 0
20 13, 19 ax_mp 
finite (Array A 0) <-> finite (sn 0)
21 finns 
finite (sn 0)
22 20, 21 mpbir 
finite (Array A 0)
23 22 a1i 
finite A -> finite (Array A 0)
24 xpfin 
finite A -> finite (Array A a1) -> finite (Xp A (Array A a1))
25 24 imp 
finite A /\ finite (Array A a1) -> finite (Xp A (Array A a1))
26 lefin 
finite {a3 | a3 <= lower (Xp A (Array A a1))}
27 finss 
Array A (suc a1) C_ {a3 | a3 <= lower (Xp A (Array A a1))} -> finite {a3 | a3 <= lower (Xp A (Array A a1))} -> finite (Array A (suc a1))
28 26, 27 mpi 
Array A (suc a1) C_ {a3 | a3 <= lower (Xp A (Array A a1))} -> finite (Array A (suc a1))
29 ssab2 
A. a3 (a3 e. Array A (suc a1) -> a3 <= lower (Xp A (Array A a1))) <-> Array A (suc a1) C_ {a3 | a3 <= lower (Xp A (Array A a1))}
30 elArrayS2 
a3 e. Array A (suc a1) <-> E. a4 E. a5 (a4 e. A /\ a5 e. Array A a1 /\ a3 = a4 : a5)
31 anrr 
finite (Xp A (Array A a1)) /\ (a4 e. A /\ a5 e. Array A a1 /\ a3 = a4 : a5) -> a3 = a4 : a5
32 31 leeq1d 
finite (Xp A (Array A a1)) /\ (a4 e. A /\ a5 e. Array A a1 /\ a3 = a4 : a5) -> (a3 <= lower (Xp A (Array A a1)) <-> a4 : a5 <= lower (Xp A (Array A a1)))
33 ellt 
a4, a5 e. lower (Xp A (Array A a1)) -> a4, a5 < lower (Xp A (Array A a1))
34 33 conv cons, lt 
a4, a5 e. lower (Xp A (Array A a1)) -> a4 : a5 <= lower (Xp A (Array A a1))
35 ellower 
finite (Xp A (Array A a1)) -> (a4, a5 e. lower (Xp A (Array A a1)) <-> a4, a5 e. Xp A (Array A a1))
36 35 anwl 
finite (Xp A (Array A a1)) /\ (a4 e. A /\ a5 e. Array A a1 /\ a3 = a4 : a5) -> (a4, a5 e. lower (Xp A (Array A a1)) <-> a4, a5 e. Xp A (Array A a1))
37 prelxp 
a4, a5 e. Xp A (Array A a1) <-> a4 e. A /\ a5 e. Array A a1
38 anrl 
finite (Xp A (Array A a1)) /\ (a4 e. A /\ a5 e. Array A a1 /\ a3 = a4 : a5) -> a4 e. A /\ a5 e. Array A a1
39 37, 38 sylibr 
finite (Xp A (Array A a1)) /\ (a4 e. A /\ a5 e. Array A a1 /\ a3 = a4 : a5) -> a4, a5 e. Xp A (Array A a1)
40 36, 39 mpbird 
finite (Xp A (Array A a1)) /\ (a4 e. A /\ a5 e. Array A a1 /\ a3 = a4 : a5) -> a4, a5 e. lower (Xp A (Array A a1))
41 34, 40 syl 
finite (Xp A (Array A a1)) /\ (a4 e. A /\ a5 e. Array A a1 /\ a3 = a4 : a5) -> a4 : a5 <= lower (Xp A (Array A a1))
42 32, 41 mpbird 
finite (Xp A (Array A a1)) /\ (a4 e. A /\ a5 e. Array A a1 /\ a3 = a4 : a5) -> a3 <= lower (Xp A (Array A a1))
43 42 eexda 
finite (Xp A (Array A a1)) -> E. a5 (a4 e. A /\ a5 e. Array A a1 /\ a3 = a4 : a5) -> a3 <= lower (Xp A (Array A a1))
44 43 eexd 
finite (Xp A (Array A a1)) -> E. a4 E. a5 (a4 e. A /\ a5 e. Array A a1 /\ a3 = a4 : a5) -> a3 <= lower (Xp A (Array A a1))
45 30, 44 syl5bi 
finite (Xp A (Array A a1)) -> a3 e. Array A (suc a1) -> a3 <= lower (Xp A (Array A a1))
46 45 iald 
finite (Xp A (Array A a1)) -> A. a3 (a3 e. Array A (suc a1) -> a3 <= lower (Xp A (Array A a1)))
47 29, 46 sylib 
finite (Xp A (Array A a1)) -> Array A (suc a1) C_ {a3 | a3 <= lower (Xp A (Array A a1))}
48 28, 47 syl 
finite (Xp A (Array A a1)) -> finite (Array A (suc a1))
49 25, 48 rsyl 
finite A /\ finite (Array A a1) -> finite (Array A (suc a1))
50 3, 6, 9, 12, 23, 49 indd 
finite A -> finite (Array A n)

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)