Theorem unisalgen2

Description: The union of a set belongs is equal to the union of the sigma-algebra generated by the set. (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Hypotheses	unisalgen2.x	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	unisalgen2.s	⊢ 𝑆 = ( SalGen ‘ 𝐴 )
Assertion	unisalgen2	⊢ ( 𝜑 → ∪ 𝑆 = ∪ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		unisalgen2.x	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2		unisalgen2.s	⊢ 𝑆 = ( SalGen ‘ 𝐴 )
3	2	eqcomi	⊢ ( SalGen ‘ 𝐴 ) = 𝑆
4	3	a1i	⊢ ( 𝜑 → ( SalGen ‘ 𝐴 ) = 𝑆 )
5	1	dfsalgen2	⊢ ( 𝜑 → ( ( SalGen ‘ 𝐴 ) = 𝑆 ↔ ( ( 𝑆 ∈ SAlg ∧ ∪ 𝑆 = ∪ 𝐴 ∧ 𝐴 ⊆ 𝑆 ) ∧ ∀ 𝑥 ∈ SAlg ( ( ∪ 𝑥 = ∪ 𝐴 ∧ 𝐴 ⊆ 𝑥 ) → 𝑆 ⊆ 𝑥 ) ) ) )
6	4 5	mpbid	⊢ ( 𝜑 → ( ( 𝑆 ∈ SAlg ∧ ∪ 𝑆 = ∪ 𝐴 ∧ 𝐴 ⊆ 𝑆 ) ∧ ∀ 𝑥 ∈ SAlg ( ( ∪ 𝑥 = ∪ 𝐴 ∧ 𝐴 ⊆ 𝑥 ) → 𝑆 ⊆ 𝑥 ) ) )
7	6	simpld	⊢ ( 𝜑 → ( 𝑆 ∈ SAlg ∧ ∪ 𝑆 = ∪ 𝐴 ∧ 𝐴 ⊆ 𝑆 ) )
8	7	simp2d	⊢ ( 𝜑 → ∪ 𝑆 = ∪ 𝐴 )