Metamath Proof Explorer

Theorem unifi3

Description: If a union is finite, then all its elements are finite. See unifi . (Contributed by Thierry Arnoux, 27-Aug-2017)

Ref Expression
Assertion unifi3 
|- ( U. A e. Fin -> A C_ Fin )

Proof

Step Hyp Ref Expression
1 elssuni 
 |-  ( x e. A -> x C_ U. A )
2 ssfi 
 |-  ( ( U. A e. Fin /\ x C_ U. A ) -> x e. Fin )
3 2 ex 
 |-  ( U. A e. Fin -> ( x C_ U. A -> x e. Fin ) )
4 1 3 syl5 
 |-  ( U. A e. Fin -> ( x e. A -> x e. Fin ) )
5 4 ssrdv 
 |-  ( U. A e. Fin -> A C_ Fin )