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	$$⊢\phi \to X\in A$$
	iunlub.2	$$⊢\left(\phi \wedge x=X\right)\to B=C$$
	iunlub.3	$$⊢\left(\phi \wedge x\in A\right)\to B\subseteq C$$
Assertion	iunlub	$$⊢\phi \to \bigcup _{x\in A}B=C$$

Proof

Step	Hyp	Ref	Expression
1		iunlub.1	$$⊢\phi \to X\in A$$
2		iunlub.2	$$⊢\left(\phi \wedge x=X\right)\to B=C$$
3		iunlub.3	$$⊢\left(\phi \wedge x\in A\right)\to B\subseteq C$$
4	3	iunssd	$$⊢\phi \to \bigcup _{x\in A}B\subseteq C$$
5	2	sseq2d	$$⊢\left(\phi \wedge x=X\right)\to \left(C\subseteq B\leftrightarrow C\subseteq C\right)$$
6		ssidd	$$⊢\phi \to C\subseteq C$$
7	1 5 6	rspcedvd	$$⊢\phi \to \exists x\in AC\subseteq B$$
8		ssiun	$$⊢\exists x\in AC\subseteq B\to C\subseteq \bigcup _{x\in A}B$$
9	7 8	syl	$$⊢\phi \to C\subseteq \bigcup _{x\in A}B$$
10	4 9	eqssd	$$⊢\phi \to \bigcup _{x\in A}B=C$$