Theorem toplatmeet

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

	Ref	Expression
Hypotheses	toplatmeet.i	⊢ 𝐼 = ( toInc ‘ 𝐽 )
	toplatmeet.j	⊢ ( 𝜑 → 𝐽 ∈ Top )
	toplatmeet.a	⊢ ( 𝜑 → 𝐴 ∈ 𝐽 )
	toplatmeet.b	⊢ ( 𝜑 → 𝐵 ∈ 𝐽 )
	toplatmeet.m	⊢ ∧ = ( meet ‘ 𝐼 )
Assertion	toplatmeet	⊢ ( 𝜑 → ( 𝐴 ∧ 𝐵 ) = ( 𝐴 ∩ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		toplatmeet.i	⊢ 𝐼 = ( toInc ‘ 𝐽 )
2		toplatmeet.j	⊢ ( 𝜑 → 𝐽 ∈ Top )
3		toplatmeet.a	⊢ ( 𝜑 → 𝐴 ∈ 𝐽 )
4		toplatmeet.b	⊢ ( 𝜑 → 𝐵 ∈ 𝐽 )
5		toplatmeet.m	⊢ ∧ = ( meet ‘ 𝐼 )
6		eqid	⊢ ( glb ‘ 𝐼 ) = ( glb ‘ 𝐼 )
7	1	ipopos	⊢ 𝐼 ∈ Poset
8	7	a1i	⊢ ( 𝜑 → 𝐼 ∈ Poset )
9	6 5 8 3 4	meetval	⊢ ( 𝜑 → ( 𝐴 ∧ 𝐵 ) = ( ( glb ‘ 𝐼 ) ‘ { 𝐴 , 𝐵 } ) )
10	3 4	prssd	⊢ ( 𝜑 → { 𝐴 , 𝐵 } ⊆ 𝐽 )
11	6	a1i	⊢ ( 𝜑 → ( glb ‘ 𝐼 ) = ( glb ‘ 𝐼 ) )
12		intprg	⊢ ( ( 𝐴 ∈ 𝐽 ∧ 𝐵 ∈ 𝐽 ) → ∩ { 𝐴 , 𝐵 } = ( 𝐴 ∩ 𝐵 ) )
13	3 4 12	syl2anc	⊢ ( 𝜑 → ∩ { 𝐴 , 𝐵 } = ( 𝐴 ∩ 𝐵 ) )
14		inopn	⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝐽 ∧ 𝐵 ∈ 𝐽 ) → ( 𝐴 ∩ 𝐵 ) ∈ 𝐽 )
15	2 3 4 14	syl3anc	⊢ ( 𝜑 → ( 𝐴 ∩ 𝐵 ) ∈ 𝐽 )
16	13 15	eqeltrd	⊢ ( 𝜑 → ∩ { 𝐴 , 𝐵 } ∈ 𝐽 )
17		unimax	⊢ ( ∩ { 𝐴 , 𝐵 } ∈ 𝐽 → ∪ { 𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ ∩ { 𝐴 , 𝐵 } } = ∩ { 𝐴 , 𝐵 } )
18	16 17	syl	⊢ ( 𝜑 → ∪ { 𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ ∩ { 𝐴 , 𝐵 } } = ∩ { 𝐴 , 𝐵 } )
19	18 13	eqtr2d	⊢ ( 𝜑 → ( 𝐴 ∩ 𝐵 ) = ∪ { 𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ ∩ { 𝐴 , 𝐵 } } )
20	1 2 10 11 19 15	ipoglb	⊢ ( 𝜑 → ( ( glb ‘ 𝐼 ) ‘ { 𝐴 , 𝐵 } ) = ( 𝐴 ∩ 𝐵 ) )
21	9 20	eqtrd	⊢ ( 𝜑 → ( 𝐴 ∧ 𝐵 ) = ( 𝐴 ∩ 𝐵 ) )