![]() |
Metamath
Proof Explorer Theorem List (p. 186 of 491) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30946) |
![]() (30947-32469) |
![]() (32470-49035) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | lattr 18501 | A lattice ordering is transitive. (sstr 4003 analog.) (Contributed by NM, 17-Nov-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍) → 𝑋 ≤ 𝑍)) | ||
Theorem | latasymd 18502 | Deduce equality from lattice ordering. (eqssd 4012 analog.) (Contributed by NM, 18-Nov-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ (𝜑 → 𝐾 ∈ Lat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑋 ≤ 𝑌) & ⊢ (𝜑 → 𝑌 ≤ 𝑋) ⇒ ⊢ (𝜑 → 𝑋 = 𝑌) | ||
Theorem | lattrd 18503 | A lattice ordering is transitive. Deduction version of lattr 18501. (Contributed by NM, 3-Sep-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ (𝜑 → 𝐾 ∈ Lat) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → 𝑋 ≤ 𝑌) & ⊢ (𝜑 → 𝑌 ≤ 𝑍) ⇒ ⊢ (𝜑 → 𝑋 ≤ 𝑍) | ||
Theorem | latjcom 18504 | The join of a lattice commutes. (chjcom 31534 analog.) (Contributed by NM, 16-Sep-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∨ 𝑌) = (𝑌 ∨ 𝑋)) | ||
Theorem | latlej1 18505 | A join's first argument is less than or equal to the join. (chub1 31535 analog.) (Contributed by NM, 17-Sep-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝑋 ≤ (𝑋 ∨ 𝑌)) | ||
Theorem | latlej2 18506 | A join's second argument is less than or equal to the join. (chub2 31536 analog.) (Contributed by NM, 17-Sep-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝑌 ≤ (𝑋 ∨ 𝑌)) | ||
Theorem | latjle12 18507 | A join is less than or equal to a third value iff each argument is less than or equal to the third value. (chlub 31537 analog.) (Contributed by NM, 17-Sep-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ≤ 𝑍 ∧ 𝑌 ≤ 𝑍) ↔ (𝑋 ∨ 𝑌) ≤ 𝑍)) | ||
Theorem | latleeqj1 18508 | "Less than or equal to" in terms of join. (chlejb1 31540 analog.) (Contributed by NM, 21-Oct-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 ↔ (𝑋 ∨ 𝑌) = 𝑌)) | ||
Theorem | latleeqj2 18509 | "Less than or equal to" in terms of join. (chlejb2 31541 analog.) (Contributed by NM, 14-Nov-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 ↔ (𝑌 ∨ 𝑋) = 𝑌)) | ||
Theorem | latjlej1 18510 | Add join to both sides of a lattice ordering. (chlej1i 31501 analog.) (Contributed by NM, 8-Nov-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 ≤ 𝑌 → (𝑋 ∨ 𝑍) ≤ (𝑌 ∨ 𝑍))) | ||
Theorem | latjlej2 18511 | Add join to both sides of a lattice ordering. (chlej2i 31502 analog.) (Contributed by NM, 8-Nov-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 ≤ 𝑌 → (𝑍 ∨ 𝑋) ≤ (𝑍 ∨ 𝑌))) | ||
Theorem | latjlej12 18512 | Add join to both sides of a lattice ordering. (chlej12i 31503 analog.) (Contributed by NM, 8-Nov-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵)) → ((𝑋 ≤ 𝑌 ∧ 𝑍 ≤ 𝑊) → (𝑋 ∨ 𝑍) ≤ (𝑌 ∨ 𝑊))) | ||
Theorem | latnlej 18513 | An idiom to express that a lattice element differs from two others. (Contributed by NM, 28-May-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ ¬ 𝑋 ≤ (𝑌 ∨ 𝑍)) → (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍)) | ||
Theorem | latnlej1l 18514 | An idiom to express that a lattice element differs from two others. (Contributed by NM, 19-Jul-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ ¬ 𝑋 ≤ (𝑌 ∨ 𝑍)) → 𝑋 ≠ 𝑌) | ||
Theorem | latnlej1r 18515 | An idiom to express that a lattice element differs from two others. (Contributed by NM, 19-Jul-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ ¬ 𝑋 ≤ (𝑌 ∨ 𝑍)) → 𝑋 ≠ 𝑍) | ||
Theorem | latnlej2 18516 | An idiom to express that a lattice element differs from two others. (Contributed by NM, 10-Jul-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ ¬ 𝑋 ≤ (𝑌 ∨ 𝑍)) → (¬ 𝑋 ≤ 𝑌 ∧ ¬ 𝑋 ≤ 𝑍)) | ||
Theorem | latnlej2l 18517 | An idiom to express that a lattice element differs from two others. (Contributed by NM, 19-Jul-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ ¬ 𝑋 ≤ (𝑌 ∨ 𝑍)) → ¬ 𝑋 ≤ 𝑌) | ||
Theorem | latnlej2r 18518 | An idiom to express that a lattice element differs from two others. (Contributed by NM, 19-Jul-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ ¬ 𝑋 ≤ (𝑌 ∨ 𝑍)) → ¬ 𝑋 ≤ 𝑍) | ||
Theorem | latjidm 18519 | Lattice join is idempotent. Analogue of unidm 4166. (Contributed by NM, 8-Oct-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵) → (𝑋 ∨ 𝑋) = 𝑋) | ||
Theorem | latmcom 18520 | The join of a lattice commutes. (Contributed by NM, 6-Nov-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∧ = (meet‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∧ 𝑌) = (𝑌 ∧ 𝑋)) | ||
Theorem | latmle1 18521 | A meet is less than or equal to its first argument. (Contributed by NM, 21-Oct-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∧ = (meet‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∧ 𝑌) ≤ 𝑋) | ||
Theorem | latmle2 18522 | A meet is less than or equal to its second argument. (Contributed by NM, 21-Oct-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∧ = (meet‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∧ 𝑌) ≤ 𝑌) | ||
Theorem | latlem12 18523 | 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 18524 | "Less than or equal to" in terms of meet. (Contributed by NM, 7-Nov-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∧ = (meet‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 ↔ (𝑋 ∧ 𝑌) = 𝑋)) | ||
Theorem | latleeqm2 18525 | "Less than or equal to" in terms of meet. (Contributed by NM, 7-Nov-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∧ = (meet‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 ↔ (𝑌 ∧ 𝑋) = 𝑋)) | ||
Theorem | latmlem1 18526 | Add meet to both sides of a lattice ordering. (Contributed by NM, 10-Nov-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∧ = (meet‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 ≤ 𝑌 → (𝑋 ∧ 𝑍) ≤ (𝑌 ∧ 𝑍))) | ||
Theorem | latmlem2 18527 | Add meet to both sides of a lattice ordering. (sslin 4250 analog.) (Contributed by NM, 10-Nov-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∧ = (meet‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 ≤ 𝑌 → (𝑍 ∧ 𝑋) ≤ (𝑍 ∧ 𝑌))) | ||
Theorem | latmlem12 18528 | Add join to both sides of a lattice ordering. (ss2in 4252 analog.) (Contributed by NM, 10-Nov-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∧ = (meet‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵)) → ((𝑋 ≤ 𝑌 ∧ 𝑍 ≤ 𝑊) → (𝑋 ∧ 𝑍) ≤ (𝑌 ∧ 𝑊))) | ||
Theorem | latnlemlt 18529 | Negation of "less than or equal to" expressed in terms of meet and less-than. (nssinpss 4272 analog.) (Contributed by NM, 5-Feb-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ < = (lt‘𝐾) & ⊢ ∧ = (meet‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (¬ 𝑋 ≤ 𝑌 ↔ (𝑋 ∧ 𝑌) < 𝑋)) | ||
Theorem | latnle 18530 | Equivalent expressions for "not less than" in a lattice. (chnle 31542 analog.) (Contributed by NM, 16-Nov-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ < = (lt‘𝐾) & ⊢ ∨ = (join‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (¬ 𝑌 ≤ 𝑋 ↔ 𝑋 < (𝑋 ∨ 𝑌))) | ||
Theorem | latmidm 18531 | Lattice meet is idempotent. Analogue of inidm 4234. (Contributed by NM, 8-Nov-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∧ = (meet‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵) → (𝑋 ∧ 𝑋) = 𝑋) | ||
Theorem | latabs1 18532 | Lattice absorption law. From definition of lattice in [Kalmbach] p. 14. (chabs1 31544 analog.) (Contributed by NM, 8-Nov-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∨ (𝑋 ∧ 𝑌)) = 𝑋) | ||
Theorem | latabs2 18533 | Lattice absorption law. From definition of lattice in [Kalmbach] p. 14. (chabs2 31545 analog.) (Contributed by NM, 8-Nov-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∧ (𝑋 ∨ 𝑌)) = 𝑋) | ||
Theorem | latledi 18534 | An ortholattice is distributive in one ordering direction. (ledi 31568 analog.) (Contributed by NM, 7-Nov-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ∧ 𝑌) ∨ (𝑋 ∧ 𝑍)) ≤ (𝑋 ∧ (𝑌 ∨ 𝑍))) | ||
Theorem | latmlej11 18535 | Ordering of a meet and join with a common variable. (Contributed by NM, 4-Oct-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 ∧ 𝑌) ≤ (𝑋 ∨ 𝑍)) | ||
Theorem | latmlej12 18536 | Ordering of a meet and join with a common variable. (Contributed by NM, 4-Oct-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 ∧ 𝑌) ≤ (𝑍 ∨ 𝑋)) | ||
Theorem | latmlej21 18537 | Ordering of a meet and join with a common variable. (Contributed by NM, 4-Oct-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑌 ∧ 𝑋) ≤ (𝑋 ∨ 𝑍)) | ||
Theorem | latmlej22 18538 | Ordering of a meet and join with a common variable. (Contributed by NM, 4-Oct-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑌 ∧ 𝑋) ≤ (𝑍 ∨ 𝑋)) | ||
Theorem | lubsn 18539 | The least upper bound of a singleton. (chsupsn 31441 analog.) (Contributed by NM, 20-Oct-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝑈 = (lub‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵) → (𝑈‘{𝑋}) = 𝑋) | ||
Theorem | latjass 18540 | Lattice join is associative. Lemma 2.2 in [MegPav2002] p. 362. (chjass 31561 analog.) (Contributed by NM, 17-Sep-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ∨ 𝑌) ∨ 𝑍) = (𝑋 ∨ (𝑌 ∨ 𝑍))) | ||
Theorem | latj12 18541 | Swap 1st and 2nd members of lattice join. (chj12 31562 analog.) (Contributed by NM, 4-Jun-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 ∨ (𝑌 ∨ 𝑍)) = (𝑌 ∨ (𝑋 ∨ 𝑍))) | ||
Theorem | latj32 18542 | 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 18543 | Swap 1st and 3rd members of lattice join. (Contributed by NM, 4-Jun-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 ∨ (𝑌 ∨ 𝑍)) = (𝑍 ∨ (𝑌 ∨ 𝑋))) | ||
Theorem | latj31 18544 | 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 18545 | Rotate lattice join of 3 classes. (Contributed by NM, 23-Jul-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ∨ 𝑌) ∨ 𝑍) = ((𝑍 ∨ 𝑋) ∨ 𝑌)) | ||
Theorem | latj4 18546 | Rearrangement of lattice join of 4 classes. (chj4 31563 analog.) (Contributed by NM, 14-Jun-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵)) → ((𝑋 ∨ 𝑌) ∨ (𝑍 ∨ 𝑊)) = ((𝑋 ∨ 𝑍) ∨ (𝑌 ∨ 𝑊))) | ||
Theorem | latj4rot 18547 | Rotate lattice join of 4 classes. (Contributed by NM, 11-Jul-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵)) → ((𝑋 ∨ 𝑌) ∨ (𝑍 ∨ 𝑊)) = ((𝑊 ∨ 𝑋) ∨ (𝑌 ∨ 𝑍))) | ||
Theorem | latjjdi 18548 | Lattice join distributes over itself. (Contributed by NM, 30-Jul-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 ∨ (𝑌 ∨ 𝑍)) = ((𝑋 ∨ 𝑌) ∨ (𝑋 ∨ 𝑍))) | ||
Theorem | latjjdir 18549 | Lattice join distributes over itself. (Contributed by NM, 2-Aug-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ∨ 𝑌) ∨ 𝑍) = ((𝑋 ∨ 𝑍) ∨ (𝑌 ∨ 𝑍))) | ||
Theorem | mod1ile 18550 | The weak direction of the modular law (e.g., pmod1i 39830, atmod1i1 39839) that holds in any lattice. (Contributed by NM, 11-May-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 ≤ 𝑍 → (𝑋 ∨ (𝑌 ∧ 𝑍)) ≤ ((𝑋 ∨ 𝑌) ∧ 𝑍))) | ||
Theorem | mod2ile 18551 | The weak direction of the modular law (e.g., pmod2iN 39831) that holds in any lattice. (Contributed by NM, 11-May-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑍 ≤ 𝑋 → ((𝑋 ∧ 𝑌) ∨ 𝑍) ≤ (𝑋 ∧ (𝑌 ∨ 𝑍)))) | ||
Theorem | latmass 18552 | Lattice meet is associative. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∧ = (meet‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ∧ 𝑌) ∧ 𝑍) = (𝑋 ∧ (𝑌 ∧ 𝑍))) | ||
Theorem | latdisdlem 18553* | Lemma for latdisd 18554. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) ⇒ ⊢ (𝐾 ∈ Lat → (∀𝑢 ∈ 𝐵 ∀𝑣 ∈ 𝐵 ∀𝑤 ∈ 𝐵 (𝑢 ∨ (𝑣 ∧ 𝑤)) = ((𝑢 ∨ 𝑣) ∧ (𝑢 ∨ 𝑤)) → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 (𝑥 ∧ (𝑦 ∨ 𝑧)) = ((𝑥 ∧ 𝑦) ∨ (𝑥 ∧ 𝑧)))) | ||
Theorem | latdisd 18554* | 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 → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 (𝑥 ∨ (𝑦 ∧ 𝑧)) = ((𝑥 ∨ 𝑦) ∧ (𝑥 ∨ 𝑧)) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 (𝑥 ∧ (𝑦 ∨ 𝑧)) = ((𝑥 ∧ 𝑦) ∨ (𝑥 ∧ 𝑧)))) | ||
Syntax | ccla 18555 | Extend class notation with complete lattices. |
class CLat | ||
Definition | df-clat 18556 | 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 18557 | 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 18558 | A complete lattice is a poset. (Contributed by NM, 8-Sep-2018.) |
⊢ (𝐾 ∈ CLat → 𝐾 ∈ Poset) | ||
Theorem | clatlem 18559 | Lemma for properties of a complete lattice. (Contributed by NM, 14-Sep-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝑈 = (lub‘𝐾) & ⊢ 𝐺 = (glb‘𝐾) ⇒ ⊢ ((𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵) → ((𝑈‘𝑆) ∈ 𝐵 ∧ (𝐺‘𝑆) ∈ 𝐵)) | ||
Theorem | clatlubcl 18560 | Any subset of the base set has an LUB in a complete lattice. (Contributed by NM, 14-Sep-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝑈 = (lub‘𝐾) ⇒ ⊢ ((𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵) → (𝑈‘𝑆) ∈ 𝐵) | ||
Theorem | clatlubcl2 18561 | 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 18562 | Any subset of the base set has a GLB in a complete lattice. (Contributed by NM, 14-Sep-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝐺 = (glb‘𝐾) ⇒ ⊢ ((𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵) → (𝐺‘𝑆) ∈ 𝐵) | ||
Theorem | clatglbcl2 18563 | 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 18564 | Being a complete lattice is self-dual. (Contributed by Stefan O'Rear, 29-Jan-2015.) |
⊢ 𝐷 = (ODual‘𝑂) ⇒ ⊢ (𝑂 ∈ CLat ↔ 𝐷 ∈ CLat) | ||
Theorem | clatl 18565 | A complete lattice is a lattice. (Contributed by NM, 18-Sep-2011.) TODO: use eqrelrdv2 5807 to shorten proof and eliminate joindmss 18436 and meetdmss 18450? |
⊢ (𝐾 ∈ CLat → 𝐾 ∈ Lat) | ||
Theorem | isglbd 18566* | Properties that determine the greatest lower bound of a complete lattice. (Contributed by Mario Carneiro, 19-Mar-2014.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝐺 = (glb‘𝐾) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → 𝐻 ≤ 𝑦) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝑆 𝑥 ≤ 𝑦) → 𝑥 ≤ 𝐻) & ⊢ (𝜑 → 𝐾 ∈ CLat) & ⊢ (𝜑 → 𝑆 ⊆ 𝐵) & ⊢ (𝜑 → 𝐻 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐺‘𝑆) = 𝐻) | ||
Theorem | lublem 18567* | Lemma for the least upper bound properties in a complete lattice. (Contributed by NM, 19-Oct-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝑈 = (lub‘𝐾) ⇒ ⊢ ((𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵) → (∀𝑦 ∈ 𝑆 𝑦 ≤ (𝑈‘𝑆) ∧ ∀𝑧 ∈ 𝐵 (∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 → (𝑈‘𝑆) ≤ 𝑧))) | ||
Theorem | lubub 18568 | The LUB of a complete lattice subset is an upper bound. (Contributed by NM, 19-Oct-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝑈 = (lub‘𝐾) ⇒ ⊢ ((𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑋 ∈ 𝑆) → 𝑋 ≤ (𝑈‘𝑆)) | ||
Theorem | lubl 18569* | The LUB of a complete lattice subset is the least bound. (Contributed by NM, 19-Oct-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝑈 = (lub‘𝐾) ⇒ ⊢ ((𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑋 ∈ 𝐵) → (∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑋 → (𝑈‘𝑆) ≤ 𝑋)) | ||
Theorem | lubss 18570 | Subset law for least upper bounds. (chsupss 31370 analog.) (Contributed by NM, 20-Oct-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝑈 = (lub‘𝐾) ⇒ ⊢ ((𝐾 ∈ CLat ∧ 𝑇 ⊆ 𝐵 ∧ 𝑆 ⊆ 𝑇) → (𝑈‘𝑆) ≤ (𝑈‘𝑇)) | ||
Theorem | lubel 18571 | 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 18572 | The LUB of a union. (Contributed by NM, 5-Mar-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝑈 = (lub‘𝐾) ⇒ ⊢ ((𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝐵) → (𝑈‘(𝑆 ∪ 𝑇)) = ((𝑈‘𝑆) ∨ (𝑈‘𝑇))) | ||
Theorem | clatglb 18573* | Properties of greatest lower bound of a complete lattice. (Contributed by NM, 5-Dec-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝐺 = (glb‘𝐾) ⇒ ⊢ ((𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵) → (∀𝑦 ∈ 𝑆 (𝐺‘𝑆) ≤ 𝑦 ∧ ∀𝑧 ∈ 𝐵 (∀𝑦 ∈ 𝑆 𝑧 ≤ 𝑦 → 𝑧 ≤ (𝐺‘𝑆)))) | ||
Theorem | clatglble 18574 | The greatest lower bound is the least element. (Contributed by NM, 5-Dec-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝐺 = (glb‘𝐾) ⇒ ⊢ ((𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑋 ∈ 𝑆) → (𝐺‘𝑆) ≤ 𝑋) | ||
Theorem | clatleglb 18575* | 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 18576 | Subset law for greatest lower bound. (Contributed by Mario Carneiro, 16-Apr-2014.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝐺 = (glb‘𝐾) ⇒ ⊢ ((𝐾 ∈ CLat ∧ 𝑇 ⊆ 𝐵 ∧ 𝑆 ⊆ 𝑇) → (𝐺‘𝑇) ≤ (𝐺‘𝑆)) | ||
Syntax | cdlat 18577 | The class of distributive lattices. |
class DLat | ||
Definition | df-dlat 18578* | A distributive lattice is a lattice in which meets distribute over joins, or equivalently (latdisd 18554) joins distribute over meets. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
⊢ DLat = {𝑘 ∈ Lat ∣ [(Base‘𝑘) / 𝑏][(join‘𝑘) / 𝑗][(meet‘𝑘) / 𝑚]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 (𝑥𝑚(𝑦𝑗𝑧)) = ((𝑥𝑚𝑦)𝑗(𝑥𝑚𝑧))} | ||
Theorem | isdlat 18579* | Property of being a distributive lattice. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) ⇒ ⊢ (𝐾 ∈ DLat ↔ (𝐾 ∈ Lat ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 (𝑥 ∧ (𝑦 ∨ 𝑧)) = ((𝑥 ∧ 𝑦) ∨ (𝑥 ∧ 𝑧)))) | ||
Theorem | dlatmjdi 18580 | In a distributive lattice, meets distribute over joins. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) ⇒ ⊢ ((𝐾 ∈ DLat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 ∧ (𝑌 ∨ 𝑍)) = ((𝑋 ∧ 𝑌) ∨ (𝑋 ∧ 𝑍))) | ||
Theorem | dlatl 18581 | A distributive lattice is a lattice. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
⊢ (𝐾 ∈ DLat → 𝐾 ∈ Lat) | ||
Theorem | odudlatb 18582 | 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 18583 | In a distributive lattice, joins distribute over meets. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) ⇒ ⊢ ((𝐾 ∈ DLat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 ∨ (𝑌 ∧ 𝑍)) = ((𝑋 ∨ 𝑌) ∧ (𝑋 ∨ 𝑍))) | ||
Syntax | cipo 18584 | Class function defining inclusion posets. |
class toInc | ||
Definition | df-ipo 18585* |
For any family of sets, define the poset of that family ordered by
inclusion. See ipobas 18588, ipolerval 18589, and ipole 18591 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 18586 | The structure of df-ipo 18585 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 18587* | 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 18588 | 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 18589* | Relation of the inclusion poset. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
⊢ 𝐼 = (toInc‘𝐹) ⇒ ⊢ (𝐹 ∈ 𝑉 → {〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ 𝐹 ∧ 𝑥 ⊆ 𝑦)} = (le‘𝐼)) | ||
Theorem | ipotset 18590 | Topology of the inclusion poset. (Contributed by Mario Carneiro, 24-Oct-2015.) |
⊢ 𝐼 = (toInc‘𝐹) & ⊢ ≤ = (le‘𝐼) ⇒ ⊢ (𝐹 ∈ 𝑉 → (ordTop‘ ≤ ) = (TopSet‘𝐼)) | ||
Theorem | ipole 18591 | Weak order condition of the inclusion poset. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
⊢ 𝐼 = (toInc‘𝐹) & ⊢ ≤ = (le‘𝐼) ⇒ ⊢ ((𝐹 ∈ 𝑉 ∧ 𝑋 ∈ 𝐹 ∧ 𝑌 ∈ 𝐹) → (𝑋 ≤ 𝑌 ↔ 𝑋 ⊆ 𝑌)) | ||
Theorem | ipolt 18592 | Strict order condition of the inclusion poset. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
⊢ 𝐼 = (toInc‘𝐹) & ⊢ < = (lt‘𝐼) ⇒ ⊢ ((𝐹 ∈ 𝑉 ∧ 𝑋 ∈ 𝐹 ∧ 𝑌 ∈ 𝐹) → (𝑋 < 𝑌 ↔ 𝑋 ⊊ 𝑌)) | ||
Theorem | ipopos 18593 | The inclusion poset on a family of sets is actually a poset. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
⊢ 𝐼 = (toInc‘𝐹) ⇒ ⊢ 𝐼 ∈ Poset | ||
Theorem | isipodrs 18594* | Condition for a family of sets to be directed by inclusion. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
⊢ ((toInc‘𝐴) ∈ Dirset ↔ (𝐴 ∈ V ∧ 𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∃𝑧 ∈ 𝐴 (𝑥 ∪ 𝑦) ⊆ 𝑧)) | ||
Theorem | ipodrscl 18595 | Direction by inclusion as used here implies sethood. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
⊢ ((toInc‘𝐴) ∈ Dirset → 𝐴 ∈ V) | ||
Theorem | ipodrsfi 18596* | Finite upper bound property for directed collections of sets. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
⊢ (((toInc‘𝐴) ∈ Dirset ∧ 𝑋 ⊆ 𝐴 ∧ 𝑋 ∈ Fin) → ∃𝑧 ∈ 𝐴 ∪ 𝑋 ⊆ 𝑧) | ||
Theorem | fpwipodrs 18597 | The finite subsets of any set are directed by inclusion. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
⊢ (𝐴 ∈ 𝑉 → (toInc‘(𝒫 𝐴 ∩ Fin)) ∈ Dirset) | ||
Theorem | ipodrsima 18598* | The monotone image of a directed set. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
⊢ (𝜑 → 𝐹 Fn 𝒫 𝐴) & ⊢ ((𝜑 ∧ (𝑢 ⊆ 𝑣 ∧ 𝑣 ⊆ 𝐴)) → (𝐹‘𝑢) ⊆ (𝐹‘𝑣)) & ⊢ (𝜑 → (toInc‘𝐵) ∈ Dirset) & ⊢ (𝜑 → 𝐵 ⊆ 𝒫 𝐴) & ⊢ (𝜑 → (𝐹 “ 𝐵) ∈ 𝑉) ⇒ ⊢ (𝜑 → (toInc‘(𝐹 “ 𝐵)) ∈ Dirset) | ||
Theorem | isacs3lem 18599* | An algebraic closure system satisfies isacs3 18607. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
⊢ (𝐶 ∈ (ACS‘𝑋) → (𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠 ∈ 𝐶))) | ||
Theorem | acsdrsel 18600 | An algebraic closure system contains all directed unions of closed sets. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
⊢ ((𝐶 ∈ (ACS‘𝑋) ∧ 𝑌 ⊆ 𝐶 ∧ (toInc‘𝑌) ∈ Dirset) → ∪ 𝑌 ∈ 𝐶) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |