Metamath Proof Explorer


Theorem unfid

Description: The union of two finite sets is finite. (Contributed by Glauco Siliprandi, 5-Feb-2022)

Ref Expression
Hypotheses unfid.1
|- ( ph -> A e. Fin )
unfid.2
|- ( ph -> B e. Fin )
Assertion unfid
|- ( ph -> ( A u. B ) e. Fin )

Proof

Step Hyp Ref Expression
1 unfid.1
 |-  ( ph -> A e. Fin )
2 unfid.2
 |-  ( ph -> B e. Fin )
3 unfi
 |-  ( ( A e. Fin /\ B e. Fin ) -> ( A u. B ) e. Fin )
4 1 2 3 syl2anc
 |-  ( ph -> ( A u. B ) e. Fin )