Theorem toplatmeet

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

	Ref	Expression
Hypotheses	toplatmeet.i	$$⊢I=\mathrm{toInc}\left(J\right)$$
	toplatmeet.j	$$⊢\phi \to J\in \mathrm{Top}$$
	toplatmeet.a	$$⊢\phi \to A\in J$$
	toplatmeet.b	$$⊢\phi \to B\in J$$
	toplatmeet.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(I\right)$$
Assertion	toplatmeet	$$⊢\phi \to A\underset{\dot{}}{\wedge }B=A\cap B$$

Proof

Step	Hyp	Ref	Expression
1		toplatmeet.i	$$⊢I=\mathrm{toInc}\left(J\right)$$
2		toplatmeet.j	$$⊢\phi \to J\in \mathrm{Top}$$
3		toplatmeet.a	$$⊢\phi \to A\in J$$
4		toplatmeet.b	$$⊢\phi \to B\in J$$
5		toplatmeet.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(I\right)$$
6		eqid	$$⊢\mathrm{glb}\left(I\right)=\mathrm{glb}\left(I\right)$$
7	1	ipopos	$$⊢I\in \mathrm{Poset}$$
8	7	a1i	$$⊢\phi \to I\in \mathrm{Poset}$$
9	6 5 8 3 4	meetval	$$⊢\phi \to A\underset{\dot{}}{\wedge }B=\mathrm{glb}\left(I\right)\left(\left\{A,B\right\}\right)$$
10	3 4	prssd	$$⊢\phi \to \left\{A,B\right\}\subseteq J$$
11	6	a1i	$$⊢\phi \to \mathrm{glb}\left(I\right)=\mathrm{glb}\left(I\right)$$
12		intprg	$$⊢\left(A\in J\wedge B\in J\right)\to \bigcap \left\{A,B\right\}=A\cap B$$
13	3 4 12	syl2anc	$$⊢\phi \to \bigcap \left\{A,B\right\}=A\cap B$$
14		inopn	$$⊢\left(J\in \mathrm{Top}\wedge A\in J\wedge B\in J\right)\to A\cap B\in J$$
15	2 3 4 14	syl3anc	$$⊢\phi \to A\cap B\in J$$
16	13 15	eqeltrd	$$⊢\phi \to \bigcap \left\{A,B\right\}\in J$$
17		unimax	$$⊢\bigcap \left\{A,B\right\}\in J\to \bigcup \left\{x\in J|x\subseteq \bigcap \left\{A,B\right\}\right\}=\bigcap \left\{A,B\right\}$$
18	16 17	syl	$$⊢\phi \to \bigcup \left\{x\in J|x\subseteq \bigcap \left\{A,B\right\}\right\}=\bigcap \left\{A,B\right\}$$
19	18 13	eqtr2d	$$⊢\phi \to A\cap B=\bigcup \left\{x\in J|x\subseteq \bigcap \left\{A,B\right\}\right\}$$
20	1 2 10 11 19 15	ipoglb	$$⊢\phi \to \mathrm{glb}\left(I\right)\left(\left\{A,B\right\}\right)=A\cap B$$
21	9 20	eqtrd	$$⊢\phi \to A\underset{\dot{}}{\wedge }B=A\cap B$$