Theorem iunlub

Description: The indexed union is the the lowest upper bound if it exists. (Contributed by Zhi Wang, 1-Nov-2025)

	Ref	Expression
Hypotheses	iunlub.1	⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
	iunlub.2	⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → 𝐵 = 𝐶 )
	iunlub.3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ⊆ 𝐶 )
Assertion	iunlub	⊢ ( 𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 = 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		iunlub.1	⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
2		iunlub.2	⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → 𝐵 = 𝐶 )
3		iunlub.3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ⊆ 𝐶 )
4	3	iunssd	⊢ ( 𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 )
5	2	sseq2d	⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ( 𝐶 ⊆ 𝐵 ↔ 𝐶 ⊆ 𝐶 ) )
6		ssidd	⊢ ( 𝜑 → 𝐶 ⊆ 𝐶 )
7	1 5 6	rspcedvd	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐴 𝐶 ⊆ 𝐵 )
8		ssiun	⊢ ( ∃ 𝑥 ∈ 𝐴 𝐶 ⊆ 𝐵 → 𝐶 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 )
9	7 8	syl	⊢ ( 𝜑 → 𝐶 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 )
10	4 9	eqssd	⊢ ( 𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 = 𝐶 )