This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-lat

Description: Define the class of all lattices. A lattice is a poset in which the join and meet of any two elements always exists. (Contributed by NM, 18-Oct-2012) (Revised by NM, 12-Sep-2018)

Ref Expression
Assertion df-lat Lat = { 𝑝 ∈ Poset ∣ ( dom ( join ‘ 𝑝 ) = ( ( Base ‘ 𝑝 ) × ( Base ‘ 𝑝 ) ) ∧ dom ( meet ‘ 𝑝 ) = ( ( Base ‘ 𝑝 ) × ( Base ‘ 𝑝 ) ) ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 clat ⊢ Lat
1 vp ⊢ 𝑝
2 cpo ⊢ Poset
3 cjn ⊢ join
4 1 cv ⊢ 𝑝
5 4 3 cfv ⊢ ( join ‘ 𝑝 )
6 5 cdm ⊢ dom ( join ‘ 𝑝 )
7 cbs ⊢ Base
8 4 7 cfv ⊢ ( Base ‘ 𝑝 )
9 8 8 cxp ⊢ ( ( Base ‘ 𝑝 ) × ( Base ‘ 𝑝 ) )
10 6 9 wceq ⊢ dom ( join ‘ 𝑝 ) = ( ( Base ‘ 𝑝 ) × ( Base ‘ 𝑝 ) )
11 cmee ⊢ meet
12 4 11 cfv ⊢ ( meet ‘ 𝑝 )
13 12 cdm ⊢ dom ( meet ‘ 𝑝 )
14 13 9 wceq ⊢ dom ( meet ‘ 𝑝 ) = ( ( Base ‘ 𝑝 ) × ( Base ‘ 𝑝 ) )
15 10 14 wa ⊢ ( dom ( join ‘ 𝑝 ) = ( ( Base ‘ 𝑝 ) × ( Base ‘ 𝑝 ) ) ∧ dom ( meet ‘ 𝑝 ) = ( ( Base ‘ 𝑝 ) × ( Base ‘ 𝑝 ) ) )
16 15 1 2 crab ⊢ { 𝑝 ∈ Poset ∣ ( dom ( join ‘ 𝑝 ) = ( ( Base ‘ 𝑝 ) × ( Base ‘ 𝑝 ) ) ∧ dom ( meet ‘ 𝑝 ) = ( ( Base ‘ 𝑝 ) × ( Base ‘ 𝑝 ) ) ) }
17 0 16 wceq ⊢ Lat = { 𝑝 ∈ Poset ∣ ( dom ( join ‘ 𝑝 ) = ( ( Base ‘ 𝑝 ) × ( Base ‘ 𝑝 ) ) ∧ dom ( meet ‘ 𝑝 ) = ( ( Base ‘ 𝑝 ) × ( Base ‘ 𝑝 ) ) ) }