Theorem isclat

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

	Ref	Expression
Hypotheses	isclat.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	isclat.u	⊢ 𝑈 = ( lub ‘ 𝐾 )
	isclat.g	⊢ 𝐺 = ( glb ‘ 𝐾 )
Assertion	isclat	⊢ ( 𝐾 ∈ CLat ↔ ( 𝐾 ∈ Poset ∧ ( dom 𝑈 = 𝒫 𝐵 ∧ dom 𝐺 = 𝒫 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		isclat.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		isclat.u	⊢ 𝑈 = ( lub ‘ 𝐾 )
3		isclat.g	⊢ 𝐺 = ( glb ‘ 𝐾 )
4		fveq2	⊢ ( 𝑙 = 𝐾 → ( lub ‘ 𝑙 ) = ( lub ‘ 𝐾 ) )
5	4 2	eqtr4di	⊢ ( 𝑙 = 𝐾 → ( lub ‘ 𝑙 ) = 𝑈 )
6	5	dmeqd	⊢ ( 𝑙 = 𝐾 → dom ( lub ‘ 𝑙 ) = dom 𝑈 )
7		fveq2	⊢ ( 𝑙 = 𝐾 → ( Base ‘ 𝑙 ) = ( Base ‘ 𝐾 ) )
8	7 1	eqtr4di	⊢ ( 𝑙 = 𝐾 → ( Base ‘ 𝑙 ) = 𝐵 )
9	8	pweqd	⊢ ( 𝑙 = 𝐾 → 𝒫 ( Base ‘ 𝑙 ) = 𝒫 𝐵 )
10	6 9	eqeq12d	⊢ ( 𝑙 = 𝐾 → ( dom ( lub ‘ 𝑙 ) = 𝒫 ( Base ‘ 𝑙 ) ↔ dom 𝑈 = 𝒫 𝐵 ) )
11		fveq2	⊢ ( 𝑙 = 𝐾 → ( glb ‘ 𝑙 ) = ( glb ‘ 𝐾 ) )
12	11 3	eqtr4di	⊢ ( 𝑙 = 𝐾 → ( glb ‘ 𝑙 ) = 𝐺 )
13	12	dmeqd	⊢ ( 𝑙 = 𝐾 → dom ( glb ‘ 𝑙 ) = dom 𝐺 )
14	13 9	eqeq12d	⊢ ( 𝑙 = 𝐾 → ( dom ( glb ‘ 𝑙 ) = 𝒫 ( Base ‘ 𝑙 ) ↔ dom 𝐺 = 𝒫 𝐵 ) )
15	10 14	anbi12d	⊢ ( 𝑙 = 𝐾 → ( ( dom ( lub ‘ 𝑙 ) = 𝒫 ( Base ‘ 𝑙 ) ∧ dom ( glb ‘ 𝑙 ) = 𝒫 ( Base ‘ 𝑙 ) ) ↔ ( dom 𝑈 = 𝒫 𝐵 ∧ dom 𝐺 = 𝒫 𝐵 ) ) )
16		df-clat	⊢ CLat = { 𝑙 ∈ Poset ∣ ( dom ( lub ‘ 𝑙 ) = 𝒫 ( Base ‘ 𝑙 ) ∧ dom ( glb ‘ 𝑙 ) = 𝒫 ( Base ‘ 𝑙 ) ) }
17	15 16	elrab2	⊢ ( 𝐾 ∈ CLat ↔ ( 𝐾 ∈ Poset ∧ ( dom 𝑈 = 𝒫 𝐵 ∧ dom 𝐺 = 𝒫 𝐵 ) ) )