Theorem toplatmeet

Description: Meets in a topology are realized by intersections. (Contributed by Zhi Wang, 30-Sep-2024)

	Ref	Expression
Hypotheses	toplatmeet.i	|- I = ( toInc ` J )
	toplatmeet.j	|- ( ph -> J e. Top )
	toplatmeet.a	|- ( ph -> A e. J )
	toplatmeet.b	|- ( ph -> B e. J )
	toplatmeet.m	|- ./\ = ( meet ` I )
Assertion	toplatmeet	|- ( ph -> ( A ./\ B ) = ( A i^i B ) )

Proof

Step	Hyp	Ref	Expression
1		toplatmeet.i	|- I = ( toInc ` J )
2		toplatmeet.j	|- ( ph -> J e. Top )
3		toplatmeet.a	|- ( ph -> A e. J )
4		toplatmeet.b	|- ( ph -> B e. J )
5		toplatmeet.m	|- ./\ = ( meet ` I )
6		eqid	|- ( glb ` I ) = ( glb ` I )
7	1	ipopos	|- I e. Poset
8	7	a1i	|- ( ph -> I e. Poset )
9	6 5 8 3 4	meetval	|- ( ph -> ( A ./\ B ) = ( ( glb ` I ) ` { A , B } ) )
10	3 4	prssd	|- ( ph -> { A , B } C_ J )
11	6	a1i	|- ( ph -> ( glb ` I ) = ( glb ` I ) )
12		intprg	|- ( ( A e. J /\ B e. J ) -> |^| { A , B } = ( A i^i B ) )
13	3 4 12	syl2anc	|- ( ph -> |^| { A , B } = ( A i^i B ) )
14		inopn	|- ( ( J e. Top /\ A e. J /\ B e. J ) -> ( A i^i B ) e. J )
15	2 3 4 14	syl3anc	|- ( ph -> ( A i^i B ) e. J )
16	13 15	eqeltrd	|- ( ph -> |^| { A , B } e. J )
17		unimax	|- ( |^| { A , B } e. J -> U. { x e. J | x C_ |^| { A , B } } = |^| { A , B } )
18	16 17	syl	|- ( ph -> U. { x e. J | x C_ |^| { A , B } } = |^| { A , B } )
19	18 13	eqtr2d	|- ( ph -> ( A i^i B ) = U. { x e. J | x C_ |^| { A , B } } )
20	1 2 10 11 19 15	ipoglb	|- ( ph -> ( ( glb ` I ) ` { A , B } ) = ( A i^i B ) )
21	9 20	eqtrd	|- ( ph -> ( A ./\ B ) = ( A i^i B ) )