Theorem finuni | index | src |

theorem finuni (A: set): $ finite A -> finite (sUnion A) $;
StepHypRefExpression
1 eluni
a2 e. sUnion A <-> E. a3 (a2 e. a3 /\ a3 e. A)
2 eexb
E. a3 (a2 e. a3 /\ a3 e. A) -> a2 < a1 <-> A. a3 (a2 e. a3 /\ a3 e. A -> a2 < a1)
3 ancom
a2 e. a3 /\ a3 e. A -> a3 e. A /\ a2 e. a3
4 impexp
a3 e. A /\ a2 e. a3 -> a2 < a1 <-> a3 e. A -> a2 e. a3 -> a2 < a1
5 lttr
a2 < a3 -> a3 < a1 -> a2 < a1
6 ellt
a2 e. a3 -> a2 < a3
7 5, 6 syl
a2 e. a3 -> a3 < a1 -> a2 < a1
8 7 com12
a3 < a1 -> a2 e. a3 -> a2 < a1
9 8 imim2i
(a3 e. A -> a3 < a1) -> a3 e. A -> a2 e. a3 -> a2 < a1
10 4, 9 sylibr
(a3 e. A -> a3 < a1) -> a3 e. A /\ a2 e. a3 -> a2 < a1
11 3, 10 syl5
(a3 e. A -> a3 < a1) -> a2 e. a3 /\ a3 e. A -> a2 < a1
12 11 alimi
A. a3 (a3 e. A -> a3 < a1) -> A. a3 (a2 e. a3 /\ a3 e. A -> a2 < a1)
13 2, 12 sylibr
A. a3 (a3 e. A -> a3 < a1) -> E. a3 (a2 e. a3 /\ a3 e. A) -> a2 < a1
14 1, 13 syl5bi
A. a3 (a3 e. A -> a3 < a1) -> a2 e. sUnion A -> a2 < a1
15 14 iald
A. a3 (a3 e. A -> a3 < a1) -> A. a2 (a2 e. sUnion A -> a2 < a1)
16 15 eximi
E. a1 A. a3 (a3 e. A -> a3 < a1) -> E. a1 A. a2 (a2 e. sUnion A -> a2 < a1)
17 16 conv finite
finite A -> finite (sUnion 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)