This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑥 ∪ 𝑦 ) ∈ 𝐴 )
	fiunicl.2	⊢ ( 𝜑 → 𝐴 ∈ Fin )
	fiunicl.3	⊢ ( 𝜑 → 𝐴 ≠ ∅ )
Assertion	fiunicl	⊢ ( 𝜑 → ∪ 𝐴 ∈ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		fiunicl.1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑥 ∪ 𝑦 ) ∈ 𝐴 )
2		fiunicl.2	⊢ ( 𝜑 → 𝐴 ∈ Fin )
3		fiunicl.3	⊢ ( 𝜑 → 𝐴 ≠ ∅ )
4		uniiun	⊢ ∪ 𝐴 = ∪ 𝑧 ∈ 𝐴 𝑧
5		nfv	⊢ Ⅎ 𝑧 𝜑
6		simpr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → 𝑧 ∈ 𝐴 )
7	5 6 1 2 3	fiiuncl	⊢ ( 𝜑 → ∪ 𝑧 ∈ 𝐴 𝑧 ∈ 𝐴 )
8	4 7	eqeltrid	⊢ ( 𝜑 → ∪ 𝐴 ∈ 𝐴 )