Theorem islat

Description: The predicate "is a lattice." (Contributed by NM, 18-Oct-2012) (Revised by NM, 12-Sep-2018)

	Ref	Expression
Hypotheses	islat.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	islat.j	⊢ ∨ = ( join ‘ 𝐾 )
	islat.m	⊢ ∧ = ( meet ‘ 𝐾 )
Assertion	islat	⊢ ( 𝐾 ∈ Lat ↔ ( 𝐾 ∈ Poset ∧ ( dom ∨ = ( 𝐵 × 𝐵 ) ∧ dom ∧ = ( 𝐵 × 𝐵 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		islat.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		islat.j	⊢ ∨ = ( join ‘ 𝐾 )
3		islat.m	⊢ ∧ = ( meet ‘ 𝐾 )
4		fveq2	⊢ ( 𝑙 = 𝐾 → ( join ‘ 𝑙 ) = ( join ‘ 𝐾 ) )
5	4 2	eqtr4di	⊢ ( 𝑙 = 𝐾 → ( join ‘ 𝑙 ) = ∨ )
6	5	dmeqd	⊢ ( 𝑙 = 𝐾 → dom ( join ‘ 𝑙 ) = dom ∨ )
7		fveq2	⊢ ( 𝑙 = 𝐾 → ( Base ‘ 𝑙 ) = ( Base ‘ 𝐾 ) )
8	7 1	eqtr4di	⊢ ( 𝑙 = 𝐾 → ( Base ‘ 𝑙 ) = 𝐵 )
9	8	sqxpeqd	⊢ ( 𝑙 = 𝐾 → ( ( Base ‘ 𝑙 ) × ( Base ‘ 𝑙 ) ) = ( 𝐵 × 𝐵 ) )
10	6 9	eqeq12d	⊢ ( 𝑙 = 𝐾 → ( dom ( join ‘ 𝑙 ) = ( ( Base ‘ 𝑙 ) × ( Base ‘ 𝑙 ) ) ↔ dom ∨ = ( 𝐵 × 𝐵 ) ) )
11		fveq2	⊢ ( 𝑙 = 𝐾 → ( meet ‘ 𝑙 ) = ( meet ‘ 𝐾 ) )
12	11 3	eqtr4di	⊢ ( 𝑙 = 𝐾 → ( meet ‘ 𝑙 ) = ∧ )
13	12	dmeqd	⊢ ( 𝑙 = 𝐾 → dom ( meet ‘ 𝑙 ) = dom ∧ )
14	13 9	eqeq12d	⊢ ( 𝑙 = 𝐾 → ( dom ( meet ‘ 𝑙 ) = ( ( Base ‘ 𝑙 ) × ( Base ‘ 𝑙 ) ) ↔ dom ∧ = ( 𝐵 × 𝐵 ) ) )
15	10 14	anbi12d	⊢ ( 𝑙 = 𝐾 → ( ( dom ( join ‘ 𝑙 ) = ( ( Base ‘ 𝑙 ) × ( Base ‘ 𝑙 ) ) ∧ dom ( meet ‘ 𝑙 ) = ( ( Base ‘ 𝑙 ) × ( Base ‘ 𝑙 ) ) ) ↔ ( dom ∨ = ( 𝐵 × 𝐵 ) ∧ dom ∧ = ( 𝐵 × 𝐵 ) ) ) )
16		df-lat	⊢ Lat = { 𝑙 ∈ Poset ∣ ( dom ( join ‘ 𝑙 ) = ( ( Base ‘ 𝑙 ) × ( Base ‘ 𝑙 ) ) ∧ dom ( meet ‘ 𝑙 ) = ( ( Base ‘ 𝑙 ) × ( Base ‘ 𝑙 ) ) ) }
17	15 16	elrab2	⊢ ( 𝐾 ∈ Lat ↔ ( 𝐾 ∈ Poset ∧ ( dom ∨ = ( 𝐵 × 𝐵 ) ∧ dom ∧ = ( 𝐵 × 𝐵 ) ) ) )