Metamath Proof Explorer

Theorem unfi2

Description: The union of two finite sets is finite. Part of Corollary 6K of Enderton p. 144. This version of unfi is useful only if we assume the Axiom of Infinity (see comments in fin2inf ). (Contributed by NM, 22-Oct-2004) (Revised by Mario Carneiro, 27-Apr-2015)

Ref Expression
Assertion unfi2 ⊢ A ≺ ω ∧ B ≺ ω → A ∪ B ≺ ω

Proof

Step Hyp Ref Expression
1 isfinite2 ⊢ A ≺ ω → A ∈ Fin
2 isfinite2 ⊢ B ≺ ω → B ∈ Fin
3 unfi ⊢ A ∈ Fin ∧ B ∈ Fin → A ∪ B ∈ Fin
4 1 2 3 syl2an ⊢ A ≺ ω ∧ B ≺ ω → A ∪ B ∈ Fin
5 fin2inf ⊢ A ≺ ω → ω ∈ V
6 5 adantr ⊢ A ≺ ω ∧ B ≺ ω → ω ∈ V
7 isfiniteg ⊢ ω ∈ V → A ∪ B ∈ Fin ↔ A ∪ B ≺ ω
8 6 7 syl ⊢ A ≺ ω ∧ B ≺ ω → A ∪ B ∈ Fin ↔ A ∪ B ≺ ω
9 4 8 mpbid ⊢ A ≺ ω ∧ B ≺ ω → A ∪ B ≺ ω