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	|- ( ph -> X e. A )
	iunlub.2	|- ( ( ph /\ x = X ) -> B = C )
	iunlub.3	|- ( ( ph /\ x e. A ) -> B C_ C )
Assertion	iunlub	|- ( ph -> U_ x e. A B = C )

Proof

Step	Hyp	Ref	Expression
1		iunlub.1	|- ( ph -> X e. A )
2		iunlub.2	|- ( ( ph /\ x = X ) -> B = C )
3		iunlub.3	|- ( ( ph /\ x e. A ) -> B C_ C )
4	3	iunssd	|- ( ph -> U_ x e. A B C_ C )
5	2	sseq2d	|- ( ( ph /\ x = X ) -> ( C C_ B <-> C C_ C ) )
6		ssidd	|- ( ph -> C C_ C )
7	1 5 6	rspcedvd	|- ( ph -> E. x e. A C C_ B )
8		ssiun	|- ( E. x e. A C C_ B -> C C_ U_ x e. A B )
9	7 8	syl	|- ( ph -> C C_ U_ x e. A B )
10	4 9	eqssd	|- ( ph -> U_ x e. A B = C )