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 ‘ 𝑝 ) ) ) }