Metamath Proof Explorer


Theorem fiunicl

Description: If a set is closed under the union of two sets, then it is closed under finite union. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses fiunicl.1 φ x A y A x y A
fiunicl.2 φ A Fin
fiunicl.3 φ A
Assertion fiunicl φ A A

Proof

Step Hyp Ref Expression
1 fiunicl.1 φ x A y A x y A
2 fiunicl.2 φ A Fin
3 fiunicl.3 φ A
4 uniiun A = z A z
5 nfv z φ
6 simpr φ z A z A
7 5 6 1 2 3 fiiuncl φ z A z A
8 4 7 eqeltrid φ A A