P. 186 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 18501-18600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	latjcl 18501	Closure of join operation in a lattice. (chjcom 31869 analog.) (Contributed by NM, 14-Sep-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∨ 𝑌) ∈ 𝐵)
Theorem	latmcl 18502	Closure of meet operation in a lattice. (incom 4161 analog.) (Contributed by NM, 14-Sep-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∧ 𝑌) ∈ 𝐵)
Theorem	latref 18503	A lattice ordering is reflexive. (ssid 3958 analog.) (Contributed by NM, 8-Oct-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵) → 𝑋 ≤ 𝑋)
Theorem	latasymb 18504	A lattice ordering is asymmetric. (eqss 3951 analog.) (Contributed by NM, 22-Oct-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑋) ↔ 𝑋 = 𝑌))
Theorem	latasym 18505	A lattice ordering is asymmetric. (eqss 3951 analog.) (Contributed by NM, 8-Oct-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑋) → 𝑋 = 𝑌))
Theorem	lattr 18506	A lattice ordering is transitive. (sstr 3944 analog.) (Contributed by NM, 17-Nov-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍) → 𝑋 ≤ 𝑍))
Theorem	latasymd 18507	Deduce equality from lattice ordering. (eqssd 3953 analog.) (Contributed by NM, 18-Nov-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ (𝜑 → 𝐾 ∈ Lat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑋 ≤ 𝑌)    &   ⊢ (𝜑 → 𝑌 ≤ 𝑋)    ⇒   ⊢ (𝜑 → 𝑋 = 𝑌)
Theorem	lattrd 18508	A lattice ordering is transitive. Deduction version of lattr 18506. (Contributed by NM, 3-Sep-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ (𝜑 → 𝐾 ∈ Lat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑋 ≤ 𝑌)    &   ⊢ (𝜑 → 𝑌 ≤ 𝑍)    ⇒   ⊢ (𝜑 → 𝑋 ≤ 𝑍)
Theorem	latjcom 18509	The join of a lattice commutes. (chjcom 31869 analog.) (Contributed by NM, 16-Sep-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∨ 𝑌) = (𝑌 ∨ 𝑋))
Theorem	latlej1 18510	A join's first argument is less than or equal to the join. (chub1 31870 analog.) (Contributed by NM, 17-Sep-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝑋 ≤ (𝑋 ∨ 𝑌))
Theorem	latlej2 18511	A join's second argument is less than or equal to the join. (chub2 31871 analog.) (Contributed by NM, 17-Sep-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝑌 ≤ (𝑋 ∨ 𝑌))
Theorem	latjle12 18512	A join is less than or equal to a third value iff each argument is less than or equal to the third value. (chlub 31872 analog.) (Contributed by NM, 17-Sep-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ≤ 𝑍 ∧ 𝑌 ≤ 𝑍) ↔ (𝑋 ∨ 𝑌) ≤ 𝑍))
Theorem	latleeqj1 18513	"Less than or equal to" in terms of join. (chlejb1 31875 analog.) (Contributed by NM, 21-Oct-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 ↔ (𝑋 ∨ 𝑌) = 𝑌))
Theorem	latleeqj2 18514	"Less than or equal to" in terms of join. (chlejb2 31876 analog.) (Contributed by NM, 14-Nov-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 ↔ (𝑌 ∨ 𝑋) = 𝑌))
Theorem	latjlej1 18515	Add join to both sides of a lattice ordering. (chlej1i 31836 analog.) (Contributed by NM, 8-Nov-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 ≤ 𝑌 → (𝑋 ∨ 𝑍) ≤ (𝑌 ∨ 𝑍)))
Theorem	latjlej2 18516	Add join to both sides of a lattice ordering. (chlej2i 31837 analog.) (Contributed by NM, 8-Nov-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 ≤ 𝑌 → (𝑍 ∨ 𝑋) ≤ (𝑍 ∨ 𝑌)))
Theorem	latjlej12 18517	Add join to both sides of a lattice ordering. (chlej12i 31838 analog.) (Contributed by NM, 8-Nov-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵)) → ((𝑋 ≤ 𝑌 ∧ 𝑍 ≤ 𝑊) → (𝑋 ∨ 𝑍) ≤ (𝑌 ∨ 𝑊)))
Theorem	latnlej 18518	An idiom to express that a lattice element differs from two others. (Contributed by NM, 28-May-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ ¬ 𝑋 ≤ (𝑌 ∨ 𝑍)) → (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍))
Theorem	latnlej1l 18519	An idiom to express that a lattice element differs from two others. (Contributed by NM, 19-Jul-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ ¬ 𝑋 ≤ (𝑌 ∨ 𝑍)) → 𝑋 ≠ 𝑌)
Theorem	latnlej1r 18520	An idiom to express that a lattice element differs from two others. (Contributed by NM, 19-Jul-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ ¬ 𝑋 ≤ (𝑌 ∨ 𝑍)) → 𝑋 ≠ 𝑍)
Theorem	latnlej2 18521	An idiom to express that a lattice element differs from two others. (Contributed by NM, 10-Jul-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ ¬ 𝑋 ≤ (𝑌 ∨ 𝑍)) → (¬ 𝑋 ≤ 𝑌 ∧ ¬ 𝑋 ≤ 𝑍))
Theorem	latnlej2l 18522	An idiom to express that a lattice element differs from two others. (Contributed by NM, 19-Jul-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ ¬ 𝑋 ≤ (𝑌 ∨ 𝑍)) → ¬ 𝑋 ≤ 𝑌)
Theorem	latnlej2r 18523	An idiom to express that a lattice element differs from two others. (Contributed by NM, 19-Jul-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ ¬ 𝑋 ≤ (𝑌 ∨ 𝑍)) → ¬ 𝑋 ≤ 𝑍)
Theorem	latjidm 18524	Lattice join is idempotent. Analogue of unidm 4110. (Contributed by NM, 8-Oct-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵) → (𝑋 ∨ 𝑋) = 𝑋)
Theorem	latmcom 18525	The join of a lattice commutes. (Contributed by NM, 6-Nov-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∧ 𝑌) = (𝑌 ∧ 𝑋))
Theorem	latmle1 18526	A meet is less than or equal to its first argument. (Contributed by NM, 21-Oct-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∧ 𝑌) ≤ 𝑋)
Theorem	latmle2 18527	A meet is less than or equal to its second argument. (Contributed by NM, 21-Oct-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∧ 𝑌) ≤ 𝑌)
Theorem	latlem12 18528	An element is less than or equal to a meet iff the element is less than or equal to each argument of the meet. (Contributed by NM, 21-Oct-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ≤ 𝑌 ∧ 𝑋 ≤ 𝑍) ↔ 𝑋 ≤ (𝑌 ∧ 𝑍)))
Theorem	latleeqm1 18529	"Less than or equal to" in terms of meet. (Contributed by NM, 7-Nov-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 ↔ (𝑋 ∧ 𝑌) = 𝑋))
Theorem	latleeqm2 18530	"Less than or equal to" in terms of meet. (Contributed by NM, 7-Nov-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 ↔ (𝑌 ∧ 𝑋) = 𝑋))
Theorem	latmlem1 18531	Add meet to both sides of a lattice ordering. (Contributed by NM, 10-Nov-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 ≤ 𝑌 → (𝑋 ∧ 𝑍) ≤ (𝑌 ∧ 𝑍)))
Theorem	latmlem2 18532	Add meet to both sides of a lattice ordering. (sslin 4194 analog.) (Contributed by NM, 10-Nov-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 ≤ 𝑌 → (𝑍 ∧ 𝑋) ≤ (𝑍 ∧ 𝑌)))
Theorem	latmlem12 18533	Add join to both sides of a lattice ordering. (ss2in 4196 analog.) (Contributed by NM, 10-Nov-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵)) → ((𝑋 ≤ 𝑌 ∧ 𝑍 ≤ 𝑊) → (𝑋 ∧ 𝑍) ≤ (𝑌 ∧ 𝑊)))
Theorem	latnlemlt 18534	Negation of "less than or equal to" expressed in terms of meet and less-than. (nssinpss 4219 analog.) (Contributed by NM, 5-Feb-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ < = (lt‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (¬ 𝑋 ≤ 𝑌 ↔ (𝑋 ∧ 𝑌) < 𝑋))
Theorem	latnle 18535	Equivalent expressions for "not less than" in a lattice. (chnle 31877 analog.) (Contributed by NM, 16-Nov-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ < = (lt‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (¬ 𝑌 ≤ 𝑋 ↔ 𝑋 < (𝑋 ∨ 𝑌)))
Theorem	latmidm 18536	Lattice meet is idempotent. Analogue of inidm 4178. (Contributed by NM, 8-Nov-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵) → (𝑋 ∧ 𝑋) = 𝑋)
Theorem	latabs1 18537	Lattice absorption law. From definition of lattice in [Kalmbach] p. 14. (chabs1 31879 analog.) (Contributed by NM, 8-Nov-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∨ (𝑋 ∧ 𝑌)) = 𝑋)
Theorem	latabs2 18538	Lattice absorption law. From definition of lattice in [Kalmbach] p. 14. (chabs2 31880 analog.) (Contributed by NM, 8-Nov-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∧ (𝑋 ∨ 𝑌)) = 𝑋)
Theorem	latledi 18539	An ortholattice is distributive in one ordering direction. (ledi 31903 analog.) (Contributed by NM, 7-Nov-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ∧ 𝑌) ∨ (𝑋 ∧ 𝑍)) ≤ (𝑋 ∧ (𝑌 ∨ 𝑍)))
Theorem	latmlej11 18540	Ordering of a meet and join with a common variable. (Contributed by NM, 4-Oct-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 ∧ 𝑌) ≤ (𝑋 ∨ 𝑍))
Theorem	latmlej12 18541	Ordering of a meet and join with a common variable. (Contributed by NM, 4-Oct-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 ∧ 𝑌) ≤ (𝑍 ∨ 𝑋))
Theorem	latmlej21 18542	Ordering of a meet and join with a common variable. (Contributed by NM, 4-Oct-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑌 ∧ 𝑋) ≤ (𝑋 ∨ 𝑍))
Theorem	latmlej22 18543	Ordering of a meet and join with a common variable. (Contributed by NM, 4-Oct-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑌 ∧ 𝑋) ≤ (𝑍 ∨ 𝑋))
Theorem	lubsn 18544	The least upper bound of a singleton. (chsupsn 31776 analog.) (Contributed by NM, 20-Oct-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝑈 = (lub‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵) → (𝑈‘{𝑋}) = 𝑋)
Theorem	latjass 18545	Lattice join is associative. Lemma 2.2 in [MegPav2002] p. 362. (chjass 31896 analog.) (Contributed by NM, 17-Sep-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ∨ 𝑌) ∨ 𝑍) = (𝑋 ∨ (𝑌 ∨ 𝑍)))
Theorem	latj12 18546	Swap 1st and 2nd members of lattice join. (chj12 31897 analog.) (Contributed by NM, 4-Jun-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 ∨ (𝑌 ∨ 𝑍)) = (𝑌 ∨ (𝑋 ∨ 𝑍)))
Theorem	latj32 18547	Swap 2nd and 3rd members of lattice join. Lemma 2.2 in [MegPav2002] p. 362. (Contributed by NM, 2-Dec-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ∨ 𝑌) ∨ 𝑍) = ((𝑋 ∨ 𝑍) ∨ 𝑌))
Theorem	latj13 18548	Swap 1st and 3rd members of lattice join. (Contributed by NM, 4-Jun-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 ∨ (𝑌 ∨ 𝑍)) = (𝑍 ∨ (𝑌 ∨ 𝑋)))
Theorem	latj31 18549	Swap 2nd and 3rd members of lattice join. Lemma 2.2 in [MegPav2002] p. 362. (Contributed by NM, 23-Jun-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ∨ 𝑌) ∨ 𝑍) = ((𝑍 ∨ 𝑌) ∨ 𝑋))
Theorem	latjrot 18550	Rotate lattice join of 3 classes. (Contributed by NM, 23-Jul-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ∨ 𝑌) ∨ 𝑍) = ((𝑍 ∨ 𝑋) ∨ 𝑌))
Theorem	latj4 18551	Rearrangement of lattice join of 4 classes. (chj4 31898 analog.) (Contributed by NM, 14-Jun-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵)) → ((𝑋 ∨ 𝑌) ∨ (𝑍 ∨ 𝑊)) = ((𝑋 ∨ 𝑍) ∨ (𝑌 ∨ 𝑊)))
Theorem	latj4rot 18552	Rotate lattice join of 4 classes. (Contributed by NM, 11-Jul-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵)) → ((𝑋 ∨ 𝑌) ∨ (𝑍 ∨ 𝑊)) = ((𝑊 ∨ 𝑋) ∨ (𝑌 ∨ 𝑍)))
Theorem	latjjdi 18553	Lattice join distributes over itself. (Contributed by NM, 30-Jul-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 ∨ (𝑌 ∨ 𝑍)) = ((𝑋 ∨ 𝑌) ∨ (𝑋 ∨ 𝑍)))
Theorem	latjjdir 18554	Lattice join distributes over itself. (Contributed by NM, 2-Aug-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ∨ 𝑌) ∨ 𝑍) = ((𝑋 ∨ 𝑍) ∨ (𝑌 ∨ 𝑍)))
Theorem	mod1ile 18555	The weak direction of the modular law (e.g., pmod1i 40650, atmod1i1 40659) that holds in any lattice. (Contributed by NM, 11-May-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 ≤ 𝑍 → (𝑋 ∨ (𝑌 ∧ 𝑍)) ≤ ((𝑋 ∨ 𝑌) ∧ 𝑍)))
Theorem	mod2ile 18556	The weak direction of the modular law (e.g., pmod2iN 40651) that holds in any lattice. (Contributed by NM, 11-May-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑍 ≤ 𝑋 → ((𝑋 ∧ 𝑌) ∨ 𝑍) ≤ (𝑋 ∧ (𝑌 ∨ 𝑍))))
Theorem	latmass 18557	Lattice meet is associative. (Contributed by Stefan O'Rear, 30-Jan-2015.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ∧ 𝑌) ∧ 𝑍) = (𝑋 ∧ (𝑌 ∧ 𝑍)))
Theorem	latdisdlem 18558*	Lemma for latdisd 18559. (Contributed by Stefan O'Rear, 30-Jan-2015.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    ⇒   ⊢ (𝐾 ∈ Lat → (∀𝑢 ∈ 𝐵 ∀𝑣 ∈ 𝐵 ∀𝑤 ∈ 𝐵 (𝑢 ∨ (𝑣 ∧ 𝑤)) = ((𝑢 ∨ 𝑣) ∧ (𝑢 ∨ 𝑤)) → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 (𝑥 ∧ (𝑦 ∨ 𝑧)) = ((𝑥 ∧ 𝑦) ∨ (𝑥 ∧ 𝑧))))
Theorem	latdisd 18559*	In a lattice, joins distribute over meets if and only if meets distribute over joins; the distributive property is self-dual. (Contributed by Stefan O'Rear, 29-Jan-2015.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    ⇒   ⊢ (𝐾 ∈ Lat → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 (𝑥 ∨ (𝑦 ∧ 𝑧)) = ((𝑥 ∨ 𝑦) ∧ (𝑥 ∨ 𝑧)) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 (𝑥 ∧ (𝑦 ∨ 𝑧)) = ((𝑥 ∧ 𝑦) ∨ (𝑥 ∧ 𝑧))))
9.5.2  Complete lattices
Syntax	ccla 18560	Extend class notation with complete lattices.
class CLat
Definition	df-clat 18561	Define the class of all complete lattices, where every subset of the base set has an LUB and a GLB. (Contributed by NM, 18-Oct-2012.) (Revised by NM, 12-Sep-2018.)
⊢ CLat = {𝑝 ∈ Poset ∣ (dom (lub‘𝑝) = 𝒫 (Base‘𝑝) ∧ dom (glb‘𝑝) = 𝒫 (Base‘𝑝))}
Theorem	isclat 18562	The predicate "is a complete lattice". (Contributed by NM, 18-Oct-2012.) (Revised by NM, 12-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝑈 = (lub‘𝐾)    &   ⊢ 𝐺 = (glb‘𝐾)    ⇒   ⊢ (𝐾 ∈ CLat ↔ (𝐾 ∈ Poset ∧ (dom 𝑈 = 𝒫 𝐵 ∧ dom 𝐺 = 𝒫 𝐵)))
Theorem	clatpos 18563	A complete lattice is a poset. (Contributed by NM, 8-Sep-2018.)
⊢ (𝐾 ∈ CLat → 𝐾 ∈ Poset)
Theorem	clatlem 18564	Lemma for properties of a complete lattice. (Contributed by NM, 14-Sep-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝑈 = (lub‘𝐾)    &   ⊢ 𝐺 = (glb‘𝐾)    ⇒   ⊢ ((𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵) → ((𝑈‘𝑆) ∈ 𝐵 ∧ (𝐺‘𝑆) ∈ 𝐵))
Theorem	clatlubcl 18565	Any subset of the base set has an LUB in a complete lattice. (Contributed by NM, 14-Sep-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝑈 = (lub‘𝐾)    ⇒   ⊢ ((𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵) → (𝑈‘𝑆) ∈ 𝐵)
Theorem	clatlubcl2 18566	Any subset of the base set has an LUB in a complete lattice. (Contributed by NM, 13-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝑈 = (lub‘𝐾)    ⇒   ⊢ ((𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵) → 𝑆 ∈ dom 𝑈)
Theorem	clatglbcl 18567	Any subset of the base set has a GLB in a complete lattice. (Contributed by NM, 14-Sep-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐺 = (glb‘𝐾)    ⇒   ⊢ ((𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵) → (𝐺‘𝑆) ∈ 𝐵)
Theorem	clatglbcl2 18568	Any subset of the base set has a GLB in a complete lattice. (Contributed by NM, 13-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐺 = (glb‘𝐾)    ⇒   ⊢ ((𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵) → 𝑆 ∈ dom 𝐺)
Theorem	oduclatb 18569	Being a complete lattice is self-dual. (Contributed by Stefan O'Rear, 29-Jan-2015.)
⊢ 𝐷 = (ODual‘𝑂)    ⇒   ⊢ (𝑂 ∈ CLat ↔ 𝐷 ∈ CLat)
Theorem	clatl 18570	A complete lattice is a lattice. (Contributed by NM, 18-Sep-2011.) TODO: use eqrelrdv2 5780 to shorten proof and eliminate joindmss 18439 and meetdmss 18453?
⊢ (𝐾 ∈ CLat → 𝐾 ∈ Lat)
Theorem	isglbd 18571*	Properties that determine the greatest lower bound of a complete lattice. (Contributed by Mario Carneiro, 19-Mar-2014.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐺 = (glb‘𝐾)    &   ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → 𝐻 ≤ 𝑦)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝑆 𝑥 ≤ 𝑦) → 𝑥 ≤ 𝐻)    &   ⊢ (𝜑 → 𝐾 ∈ CLat)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝐵)    &   ⊢ (𝜑 → 𝐻 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐺‘𝑆) = 𝐻)
Theorem	lublem 18572*	Lemma for the least upper bound properties in a complete lattice. (Contributed by NM, 19-Oct-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝑈 = (lub‘𝐾)    ⇒   ⊢ ((𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵) → (∀𝑦 ∈ 𝑆 𝑦 ≤ (𝑈‘𝑆) ∧ ∀𝑧 ∈ 𝐵 (∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 → (𝑈‘𝑆) ≤ 𝑧)))
Theorem	lubub 18573	The LUB of a complete lattice subset is an upper bound. (Contributed by NM, 19-Oct-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝑈 = (lub‘𝐾)    ⇒   ⊢ ((𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑋 ∈ 𝑆) → 𝑋 ≤ (𝑈‘𝑆))
Theorem	lubl 18574*	The LUB of a complete lattice subset is the least bound. (Contributed by NM, 19-Oct-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝑈 = (lub‘𝐾)    ⇒   ⊢ ((𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑋 ∈ 𝐵) → (∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑋 → (𝑈‘𝑆) ≤ 𝑋))
Theorem	lubss 18575	Subset law for least upper bounds. (chsupss 31705 analog.) (Contributed by NM, 20-Oct-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝑈 = (lub‘𝐾)    ⇒   ⊢ ((𝐾 ∈ CLat ∧ 𝑇 ⊆ 𝐵 ∧ 𝑆 ⊆ 𝑇) → (𝑈‘𝑆) ≤ (𝑈‘𝑇))
Theorem	lubel 18576	An element of a set is less than or equal to the least upper bound of the set. (Contributed by NM, 21-Oct-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝑈 = (lub‘𝐾)    ⇒   ⊢ ((𝐾 ∈ CLat ∧ 𝑋 ∈ 𝑆 ∧ 𝑆 ⊆ 𝐵) → 𝑋 ≤ (𝑈‘𝑆))
Theorem	lubun 18577	The LUB of a union. (Contributed by NM, 5-Mar-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝑈 = (lub‘𝐾)    ⇒   ⊢ ((𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝐵) → (𝑈‘(𝑆 ∪ 𝑇)) = ((𝑈‘𝑆) ∨ (𝑈‘𝑇)))
Theorem	clatglb 18578*	Properties of greatest lower bound of a complete lattice. (Contributed by NM, 5-Dec-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐺 = (glb‘𝐾)    ⇒   ⊢ ((𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵) → (∀𝑦 ∈ 𝑆 (𝐺‘𝑆) ≤ 𝑦 ∧ ∀𝑧 ∈ 𝐵 (∀𝑦 ∈ 𝑆 𝑧 ≤ 𝑦 → 𝑧 ≤ (𝐺‘𝑆))))
Theorem	clatglble 18579	The greatest lower bound is the least element. (Contributed by NM, 5-Dec-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐺 = (glb‘𝐾)    ⇒   ⊢ ((𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑋 ∈ 𝑆) → (𝐺‘𝑆) ≤ 𝑋)
Theorem	clatleglb 18580*	Two ways of expressing "less than or equal to the greatest lower bound." (Contributed by NM, 5-Dec-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐺 = (glb‘𝐾)    ⇒   ⊢ ((𝐾 ∈ CLat ∧ 𝑋 ∈ 𝐵 ∧ 𝑆 ⊆ 𝐵) → (𝑋 ≤ (𝐺‘𝑆) ↔ ∀𝑦 ∈ 𝑆 𝑋 ≤ 𝑦))
Theorem	clatglbss 18581	Subset law for greatest lower bound. (Contributed by Mario Carneiro, 16-Apr-2014.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐺 = (glb‘𝐾)    ⇒   ⊢ ((𝐾 ∈ CLat ∧ 𝑇 ⊆ 𝐵 ∧ 𝑆 ⊆ 𝑇) → (𝐺‘𝑇) ≤ (𝐺‘𝑆))
9.5.3  Distributive lattices
Syntax	cdlat 18582	The class of distributive lattices.
class DLat
Definition	df-dlat 18583*	A distributive lattice is a lattice in which meets distribute over joins, or equivalently (latdisd 18559) joins distribute over meets. (Contributed by Stefan O'Rear, 30-Jan-2015.)
⊢ DLat = {𝑘 ∈ Lat ∣ [(Base‘𝑘) / 𝑏][(join‘𝑘) / 𝑗][(meet‘𝑘) / 𝑚]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 (𝑥𝑚(𝑦𝑗𝑧)) = ((𝑥𝑚𝑦)𝑗(𝑥𝑚𝑧))}
Theorem	isdlat 18584*	Property of being a distributive lattice. (Contributed by Stefan O'Rear, 30-Jan-2015.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    ⇒   ⊢ (𝐾 ∈ DLat ↔ (𝐾 ∈ Lat ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 (𝑥 ∧ (𝑦 ∨ 𝑧)) = ((𝑥 ∧ 𝑦) ∨ (𝑥 ∧ 𝑧))))
Theorem	dlatmjdi 18585	In a distributive lattice, meets distribute over joins. (Contributed by Stefan O'Rear, 30-Jan-2015.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    ⇒   ⊢ ((𝐾 ∈ DLat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 ∧ (𝑌 ∨ 𝑍)) = ((𝑋 ∧ 𝑌) ∨ (𝑋 ∧ 𝑍)))
Theorem	dlatl 18586	A distributive lattice is a lattice. (Contributed by Stefan O'Rear, 30-Jan-2015.)
⊢ (𝐾 ∈ DLat → 𝐾 ∈ Lat)
Theorem	odudlatb 18587	The dual of a distributive lattice is a distributive lattice and conversely. (Contributed by Stefan O'Rear, 30-Jan-2015.)
⊢ 𝐷 = (ODual‘𝐾)    ⇒   ⊢ (𝐾 ∈ 𝑉 → (𝐾 ∈ DLat ↔ 𝐷 ∈ DLat))
Theorem	dlatjmdi 18588	In a distributive lattice, joins distribute over meets. (Contributed by Stefan O'Rear, 30-Jan-2015.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    ⇒   ⊢ ((𝐾 ∈ DLat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 ∨ (𝑌 ∧ 𝑍)) = ((𝑋 ∨ 𝑌) ∧ (𝑋 ∨ 𝑍)))
9.5.4  Subset order structures
Syntax	cipo 18589	Class function defining inclusion posets.
class toInc
Definition	df-ipo 18590*	For any family of sets, define the poset of that family ordered by inclusion. See ipobas 18593, ipolerval 18594, and ipole 18596 for its contract. EDITORIAL: I'm not thrilled with the name. Any suggestions? (Contributed by Stefan O'Rear, 30-Jan-2015.) (New usage is discouraged.)
⊢ toInc = (𝑓 ∈ V ↦ ⦋{⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝑓 ∧ 𝑥 ⊆ 𝑦)} / 𝑜⦌({⟨(Base‘ndx), 𝑓⟩, ⟨(TopSet‘ndx), (ordTop‘𝑜)⟩} ∪ {⟨(le‘ndx), 𝑜⟩, ⟨(oc‘ndx), (𝑥 ∈ 𝑓 ↦ ∪ {𝑦 ∈ 𝑓 ∣ (𝑦 ∩ 𝑥) = ∅})⟩}))
Theorem	ipostr 18591	The structure of df-ipo 18590 is a structure defining indices up to 11. (Contributed by Mario Carneiro, 25-Oct-2015.)
⊢ ({⟨(Base‘ndx), 𝐵⟩, ⟨(TopSet‘ndx), 𝐽⟩} ∪ {⟨(le‘ndx), ≤ ⟩, ⟨(oc‘ndx), ⊥ ⟩}) Struct ⟨1, ;11⟩
Theorem	ipoval 18592*	Value of the inclusion poset. (Contributed by Stefan O'Rear, 30-Jan-2015.)
⊢ 𝐼 = (toInc‘𝐹)    &   ⊢ ≤ = {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝐹 ∧ 𝑥 ⊆ 𝑦)}    ⇒   ⊢ (𝐹 ∈ 𝑉 → 𝐼 = ({⟨(Base‘ndx), 𝐹⟩, ⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩} ∪ {⟨(le‘ndx), ≤ ⟩, ⟨(oc‘ndx), (𝑥 ∈ 𝐹 ↦ ∪ {𝑦 ∈ 𝐹 ∣ (𝑦 ∩ 𝑥) = ∅})⟩}))
Theorem	ipobas 18593	Base set of the inclusion poset. (Contributed by Stefan O'Rear, 30-Jan-2015.) (Revised by Mario Carneiro, 25-Oct-2015.)
⊢ 𝐼 = (toInc‘𝐹)    ⇒   ⊢ (𝐹 ∈ 𝑉 → 𝐹 = (Base‘𝐼))
Theorem	ipolerval 18594*	Relation of the inclusion poset. (Contributed by Stefan O'Rear, 30-Jan-2015.)
⊢ 𝐼 = (toInc‘𝐹)    ⇒   ⊢ (𝐹 ∈ 𝑉 → {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝐹 ∧ 𝑥 ⊆ 𝑦)} = (le‘𝐼))
Theorem	ipotset 18595	Topology of the inclusion poset. (Contributed by Mario Carneiro, 24-Oct-2015.)
⊢ 𝐼 = (toInc‘𝐹)    &   ⊢ ≤ = (le‘𝐼)    ⇒   ⊢ (𝐹 ∈ 𝑉 → (ordTop‘ ≤ ) = (TopSet‘𝐼))
Theorem	ipole 18596	Weak order condition of the inclusion poset. (Contributed by Stefan O'Rear, 30-Jan-2015.)
⊢ 𝐼 = (toInc‘𝐹)    &   ⊢ ≤ = (le‘𝐼)    ⇒   ⊢ ((𝐹 ∈ 𝑉 ∧ 𝑋 ∈ 𝐹 ∧ 𝑌 ∈ 𝐹) → (𝑋 ≤ 𝑌 ↔ 𝑋 ⊆ 𝑌))
Theorem	ipolt 18597	Strict order condition of the inclusion poset. (Contributed by Stefan O'Rear, 30-Jan-2015.)
⊢ 𝐼 = (toInc‘𝐹)    &   ⊢ < = (lt‘𝐼)    ⇒   ⊢ ((𝐹 ∈ 𝑉 ∧ 𝑋 ∈ 𝐹 ∧ 𝑌 ∈ 𝐹) → (𝑋 < 𝑌 ↔ 𝑋 ⊊ 𝑌))
Theorem	ipopos 18598	The inclusion poset on a family of sets is actually a poset. (Contributed by Stefan O'Rear, 30-Jan-2015.)
⊢ 𝐼 = (toInc‘𝐹)    ⇒   ⊢ 𝐼 ∈ Poset
Theorem	isipodrs 18599*	Condition for a family of sets to be directed by inclusion. (Contributed by Stefan O'Rear, 2-Apr-2015.)
⊢ ((toInc‘𝐴) ∈ Dirset ↔ (𝐴 ∈ V ∧ 𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∃𝑧 ∈ 𝐴 (𝑥 ∪ 𝑦) ⊆ 𝑧))
Theorem	ipodrscl 18600	Direction by inclusion as used here implies sethood. (Contributed by Stefan O'Rear, 2-Apr-2015.)
⊢ ((toInc‘𝐴) ∈ Dirset → 𝐴 ∈ V)