Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  atcmp Structured version   Visualization version   GIF version

Theorem atcmp 37819
Description: If two atoms are comparable, they are equal. (atsseq 31331 analog.) (Contributed by NM, 13-Oct-2011.)
Hypotheses
Ref Expression
atcmp.l ≀ = (leβ€˜πΎ)
atcmp.a 𝐴 = (Atomsβ€˜πΎ)
Assertion
Ref Expression
atcmp ((𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) β†’ (𝑃 ≀ 𝑄 ↔ 𝑃 = 𝑄))

Proof of Theorem atcmp
StepHypRef Expression
1 atlpos 37809 . . 3 (𝐾 ∈ AtLat β†’ 𝐾 ∈ Poset)
213ad2ant1 1134 . 2 ((𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) β†’ 𝐾 ∈ Poset)
3 eqid 2733 . . . 4 (Baseβ€˜πΎ) = (Baseβ€˜πΎ)
4 atcmp.a . . . 4 𝐴 = (Atomsβ€˜πΎ)
53, 4atbase 37797 . . 3 (𝑃 ∈ 𝐴 β†’ 𝑃 ∈ (Baseβ€˜πΎ))
653ad2ant2 1135 . 2 ((𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) β†’ 𝑃 ∈ (Baseβ€˜πΎ))
73, 4atbase 37797 . . 3 (𝑄 ∈ 𝐴 β†’ 𝑄 ∈ (Baseβ€˜πΎ))
873ad2ant3 1136 . 2 ((𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) β†’ 𝑄 ∈ (Baseβ€˜πΎ))
9 eqid 2733 . . . 4 (0.β€˜πΎ) = (0.β€˜πΎ)
103, 9atl0cl 37811 . . 3 (𝐾 ∈ AtLat β†’ (0.β€˜πΎ) ∈ (Baseβ€˜πΎ))
11103ad2ant1 1134 . 2 ((𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) β†’ (0.β€˜πΎ) ∈ (Baseβ€˜πΎ))
12 eqid 2733 . . . 4 ( β‹– β€˜πΎ) = ( β‹– β€˜πΎ)
139, 12, 4atcvr0 37796 . . 3 ((𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴) β†’ (0.β€˜πΎ)( β‹– β€˜πΎ)𝑃)
14133adant3 1133 . 2 ((𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) β†’ (0.β€˜πΎ)( β‹– β€˜πΎ)𝑃)
159, 12, 4atcvr0 37796 . . 3 ((𝐾 ∈ AtLat ∧ 𝑄 ∈ 𝐴) β†’ (0.β€˜πΎ)( β‹– β€˜πΎ)𝑄)
16153adant2 1132 . 2 ((𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) β†’ (0.β€˜πΎ)( β‹– β€˜πΎ)𝑄)
17 atcmp.l . . 3 ≀ = (leβ€˜πΎ)
183, 17, 12cvrcmp 37791 . 2 ((𝐾 ∈ Poset ∧ (𝑃 ∈ (Baseβ€˜πΎ) ∧ 𝑄 ∈ (Baseβ€˜πΎ) ∧ (0.β€˜πΎ) ∈ (Baseβ€˜πΎ)) ∧ ((0.β€˜πΎ)( β‹– β€˜πΎ)𝑃 ∧ (0.β€˜πΎ)( β‹– β€˜πΎ)𝑄)) β†’ (𝑃 ≀ 𝑄 ↔ 𝑃 = 𝑄))
192, 6, 8, 11, 14, 16, 18syl132anc 1389 1 ((𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) β†’ (𝑃 ≀ 𝑄 ↔ 𝑃 = 𝑄))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107   class class class wbr 5106  β€˜cfv 6497  Basecbs 17088  lecple 17145  Posetcpo 18201  0.cp0 18317   β‹– ccvr 37770  Atomscatm 37771  AtLatcal 37772
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5243  ax-sep 5257  ax-nul 5264  ax-pow 5321  ax-pr 5385  ax-un 7673
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3353  df-rab 3407  df-v 3446  df-sbc 3741  df-csb 3857  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-pw 4563  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-iun 4957  df-br 5107  df-opab 5169  df-mpt 5190  df-id 5532  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-iota 6449  df-fun 6499  df-fn 6500  df-f 6501  df-f1 6502  df-fo 6503  df-f1o 6504  df-fv 6505  df-riota 7314  df-proset 18189  df-poset 18207  df-plt 18224  df-glb 18241  df-p0 18319  df-lat 18326  df-covers 37774  df-ats 37775  df-atl 37806
This theorem is referenced by:  atncmp  37820  atnlt  37821  atnle  37825  cvlsupr2  37851  cvratlem  37930  2atjm  37954  atbtwn  37955  2atm  38036  2llnmeqat  38080  dalem25  38207  dalem55  38236  dalem57  38238  snatpsubN  38259  pmapat  38272  2llnma1b  38295  cdlemblem  38302  lhp2at0nle  38544  lhpat3  38555  4atexlemcnd  38581  trlval3  38696  cdlemc5  38704  cdleme3  38746  cdleme7  38758  cdleme11k  38777  cdleme16b  38788  cdleme16e  38791  cdleme16f  38792  cdlemednpq  38808  cdleme20j  38827  cdleme22aa  38848  cdleme22cN  38851  cdleme22d  38852  cdlemf2  39071  cdlemb3  39115  cdlemg12e  39156  cdlemg17dALTN  39173  cdlemg19a  39192  cdlemg27b  39205  cdlemg31d  39209  trlcone  39237  cdlemi  39329  tendotr  39339  cdlemk17  39367  cdlemk52  39463  cdleml1N  39485  dia2dimlem1  39573  dia2dimlem2  39574  dia2dimlem3  39575
  Copyright terms: Public domain W3C validator