Theorem Arrayfin ≪ | index | src | ≫ 

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