Theorem iinglb

Description: The indexed intersection is the the greatest lower 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 )
	iinglb.3	|- ( ( ph /\ x e. A ) -> C C_ B )
Assertion	iinglb	|- ( ph -> |^|_ 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		iinglb.3	|- ( ( ph /\ x e. A ) -> C C_ B )
4	2	sseq1d	|- ( ( ph /\ x = X ) -> ( B C_ C <-> C C_ C ) )
5		ssidd	|- ( ph -> C C_ C )
6	1 4 5	rspcedvd	|- ( ph -> E. x e. A B C_ C )
7		iinss	|- ( E. x e. A B C_ C -> |^|_ x e. A B C_ C )
8	6 7	syl	|- ( ph -> |^|_ x e. A B C_ C )
9	3	ralrimiva	|- ( ph -> A. x e. A C C_ B )
10		ssiin	|- ( C C_ |^|_ x e. A B <-> A. x e. A C C_ B )
11	9 10	sylibr	|- ( ph -> C C_ |^|_ x e. A B )
12	8 11	eqssd	|- ( ph -> |^|_ x e. A B = C )