Theorem unfin ≪ | index | src | ≫ 

theorem unfin (A B: set): $ finite A -> finite B -> finite (A u. B) $;
StepHypRefExpression
1 lteq2 
z = max m n -> (x < z <-> x < max m n)
2 1 imeq2d 
z = max m n -> (x e. A u. B -> x < z <-> x e. A u. B -> x < max m n)
3 2 aleqd 
z = max m n -> (A. x (x e. A u. B -> x < z) <-> A. x (x e. A u. B -> x < max m n))
4 3 iexe 
A. x (x e. A u. B -> x < max m n) -> E. z A. x (x e. A u. B -> x < z)
5 4 conv finite 
A. x (x e. A u. B -> x < max m n) -> finite (A u. B)
6 lemax1 
m <= max m n
7 ltletr 
x < m -> m <= max m n -> x < max m n
8 6, 7 mpi 
x < m -> x < max m n
9 8 imim2i 
(x e. A -> x < m) -> x e. A -> x < max m n
10 lemax2 
n <= max m n
11 ltletr 
x < n -> n <= max m n -> x < max m n
12 10, 11 mpi 
x < n -> x < max m n
13 12 imim2i 
(x e. B -> x < n) -> x e. B -> x < max m n
14 elun 
x e. A u. B <-> x e. A \/ x e. B
15 14 imeq1i 
x e. A u. B -> x < max m n <-> x e. A \/ x e. B -> x < max m n
16 eor 
(x e. A -> x < max m n) -> (x e. B -> x < max m n) -> x e. A \/ x e. B -> x < max m n
17 15, 16 syl6ibr 
(x e. A -> x < max m n) -> (x e. B -> x < max m n) -> x e. A u. B -> x < max m n
18 13, 17 syl5 
(x e. A -> x < max m n) -> (x e. B -> x < n) -> x e. A u. B -> x < max m n
19 9, 18 rsyl 
(x e. A -> x < m) -> (x e. B -> x < n) -> x e. A u. B -> x < max m n
20 19 al2imi 
A. x (x e. A -> x < m) -> A. x (x e. B -> x < n) -> A. x (x e. A u. B -> x < max m n)
21 5, 20 syl6 
A. x (x e. A -> x < m) -> A. x (x e. B -> x < n) -> finite (A u. B)
22 21 eexd 
A. x (x e. A -> x < m) -> E. n A. x (x e. B -> x < n) -> finite (A u. B)
23 22 conv finite 
A. x (x e. A -> x < m) -> finite B -> finite (A u. B)
24 23 eex 
E. m A. x (x e. A -> x < m) -> finite B -> finite (A u. B)
25 24 conv finite 
finite A -> finite B -> finite (A u. B)

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)