MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  latcl2 Structured version   Visualization version   GIF version

Theorem latcl2 18399
Description: The join and meet of any two elements exist. (Contributed by NM, 14-Sep-2018.)
Hypotheses
Ref Expression
latcl2.b 𝐡 = (Baseβ€˜πΎ)
latcl2.j ∨ = (joinβ€˜πΎ)
latcl2.m ∧ = (meetβ€˜πΎ)
latcl2.k (πœ‘ β†’ 𝐾 ∈ Lat)
latcl2.x (πœ‘ β†’ 𝑋 ∈ 𝐡)
latcl2.y (πœ‘ β†’ π‘Œ ∈ 𝐡)
Assertion
Ref Expression
latcl2 (πœ‘ β†’ (βŸ¨π‘‹, π‘ŒβŸ© ∈ dom ∨ ∧ βŸ¨π‘‹, π‘ŒβŸ© ∈ dom ∧ ))

Proof of Theorem latcl2
StepHypRef Expression
1 latcl2.x . . . 4 (πœ‘ β†’ 𝑋 ∈ 𝐡)
2 latcl2.y . . . 4 (πœ‘ β†’ π‘Œ ∈ 𝐡)
31, 2opelxpd 5708 . . 3 (πœ‘ β†’ βŸ¨π‘‹, π‘ŒβŸ© ∈ (𝐡 Γ— 𝐡))
4 latcl2.k . . . . 5 (πœ‘ β†’ 𝐾 ∈ Lat)
5 latcl2.b . . . . . 6 𝐡 = (Baseβ€˜πΎ)
6 latcl2.j . . . . . 6 ∨ = (joinβ€˜πΎ)
7 latcl2.m . . . . . 6 ∧ = (meetβ€˜πΎ)
85, 6, 7islat 18396 . . . . 5 (𝐾 ∈ Lat ↔ (𝐾 ∈ Poset ∧ (dom ∨ = (𝐡 Γ— 𝐡) ∧ dom ∧ = (𝐡 Γ— 𝐡))))
94, 8sylib 217 . . . 4 (πœ‘ β†’ (𝐾 ∈ Poset ∧ (dom ∨ = (𝐡 Γ— 𝐡) ∧ dom ∧ = (𝐡 Γ— 𝐡))))
109simprld 769 . . 3 (πœ‘ β†’ dom ∨ = (𝐡 Γ— 𝐡))
113, 10eleqtrrd 2830 . 2 (πœ‘ β†’ βŸ¨π‘‹, π‘ŒβŸ© ∈ dom ∨ )
129simprrd 771 . . 3 (πœ‘ β†’ dom ∧ = (𝐡 Γ— 𝐡))
133, 12eleqtrrd 2830 . 2 (πœ‘ β†’ βŸ¨π‘‹, π‘ŒβŸ© ∈ dom ∧ )
1411, 13jca 511 1 (πœ‘ β†’ (βŸ¨π‘‹, π‘ŒβŸ© ∈ dom ∨ ∧ βŸ¨π‘‹, π‘ŒβŸ© ∈ dom ∧ ))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ∧ wa 395   = wceq 1533   ∈ wcel 2098  βŸ¨cop 4629   Γ— cxp 5667  dom cdm 5669  β€˜cfv 6536  Basecbs 17151  Posetcpo 18270  joincjn 18274  meetcmee 18275  Latclat 18394
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2697  ax-sep 5292  ax-nul 5299  ax-pr 5420
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2704  df-cleq 2718  df-clel 2804  df-ral 3056  df-rex 3065  df-rab 3427  df-v 3470  df-dif 3946  df-un 3948  df-in 3950  df-ss 3960  df-nul 4318  df-if 4524  df-sn 4624  df-pr 4626  df-op 4630  df-uni 4903  df-br 5142  df-opab 5204  df-xp 5675  df-dm 5679  df-iota 6488  df-fv 6544  df-lat 18395
This theorem is referenced by:  latlej1  18411  latlej2  18412  latjle12  18413  latmle1  18427  latmle2  18428  latlem12  18429
  Copyright terms: Public domain W3C validator