toplatmeet

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

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

Metamath Proof Explorer