Metamath Proof Explorer

Theorem unifi2

Description: The finite union of finite sets is finite. Exercise 13 of Enderton p. 144. This version of unifi is useful only if we assume the Axiom of Infinity (see comments in fin2inf ). (Contributed by NM, 11-Mar-2006)

Ref Expression
Assertion unifi2 ⊢ A ≺ ω ∧ ∀ x ∈ A x ≺ ω → ⋃ A ≺ ω

Proof

Step Hyp Ref Expression
1 isfinite2 ⊢ A ≺ ω → A ∈ Fin
2 isfinite2 ⊢ x ≺ ω → x ∈ Fin
3 2 ralimi ⊢ ∀ x ∈ A x ≺ ω → ∀ x ∈ A x ∈ Fin
4 dfss3 ⊢ A ⊆ Fin ↔ ∀ x ∈ A x ∈ Fin
5 3 4 sylibr ⊢ ∀ x ∈ A x ≺ ω → A ⊆ Fin
6 unifi ⊢ A ∈ Fin ∧ A ⊆ Fin → ⋃ A ∈ Fin
7 1 5 6 syl2an ⊢ A ≺ ω ∧ ∀ x ∈ A x ≺ ω → ⋃ A ∈ Fin
8 fin2inf ⊢ A ≺ ω → ω ∈ V
9 8 adantr ⊢ A ≺ ω ∧ ∀ x ∈ A x ≺ ω → ω ∈ V
10 isfiniteg ⊢ ω ∈ V → ⋃ A ∈ Fin ↔ ⋃ A ≺ ω
11 9 10 syl ⊢ A ≺ ω ∧ ∀ x ∈ A x ≺ ω → ⋃ A ∈ Fin ↔ ⋃ A ≺ ω
12 7 11 mpbid ⊢ A ≺ ω ∧ ∀ x ∈ A x ≺ ω → ⋃ A ≺ ω