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 ( 𝐴 ∈ Fin → 𝐴 ⊆ Fin )

Proof

Step Hyp Ref Expression
1 elssuni ( 𝑥𝐴𝑥 𝐴 )
2 ssfi ( ( 𝐴 ∈ Fin ∧ 𝑥 𝐴 ) → 𝑥 ∈ Fin )
3 2 ex ( 𝐴 ∈ Fin → ( 𝑥 𝐴𝑥 ∈ Fin ) )
4 1 3 syl5 ( 𝐴 ∈ Fin → ( 𝑥𝐴𝑥 ∈ Fin ) )
5 4 ssrdv ( 𝐴 ∈ Fin → 𝐴 ⊆ Fin )