Theorem atcmp 40063

Description: If two atoms are comparable, they are equal. (atsseq 32677 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

Step	Hyp	Ref	Expression
1		atlpos 40053	. . 3 ⊢ (𝐾 ∈ AtLat → 𝐾 ∈ Poset)
2	1	3ad2ant1 1151	. 2 ⊢ ((𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → 𝐾 ∈ Poset)
3		eqid 2763	. . . 4 ⊢ (Base‘𝐾) = (Base‘𝐾)
4		atcmp.a	. . . 4 ⊢ 𝐴 = (Atoms‘𝐾)
5	3, 4	atbase 40041	. . 3 ⊢ (𝑃 ∈ 𝐴 → 𝑃 ∈ (Base‘𝐾))
6	5	3ad2ant2 1152	. 2 ⊢ ((𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → 𝑃 ∈ (Base‘𝐾))
7	3, 4	atbase 40041	. . 3 ⊢ (𝑄 ∈ 𝐴 → 𝑄 ∈ (Base‘𝐾))
8	7	3ad2ant3 1153	. 2 ⊢ ((𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → 𝑄 ∈ (Base‘𝐾))
9		eqid 2763	. . . 4 ⊢ (0.‘𝐾) = (0.‘𝐾)
10	3, 9	atl0cl 40055	. . 3 ⊢ (𝐾 ∈ AtLat → (0.‘𝐾) ∈ (Base‘𝐾))
11	10	3ad2ant1 1151	. 2 ⊢ ((𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → (0.‘𝐾) ∈ (Base‘𝐾))
12		eqid 2763	. . . 4 ⊢ ( ⋖ ‘𝐾) = ( ⋖ ‘𝐾)
13	9, 12, 4	atcvr0 40040	. . 3 ⊢ ((𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴) → (0.‘𝐾)( ⋖ ‘𝐾)𝑃)
14	13	3adant3 1150	. 2 ⊢ ((𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → (0.‘𝐾)( ⋖ ‘𝐾)𝑃)
15	9, 12, 4	atcvr0 40040	. . 3 ⊢ ((𝐾 ∈ AtLat ∧ 𝑄 ∈ 𝐴) → (0.‘𝐾)( ⋖ ‘𝐾)𝑄)
16	15	3adant2 1149	. 2 ⊢ ((𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → (0.‘𝐾)( ⋖ ‘𝐾)𝑄)
17		atcmp.l	. . 3 ⊢ ≤ = (le‘𝐾)
18	3, 17, 12	cvrcmp 40035	. 2 ⊢ ((𝐾 ∈ Poset ∧ (𝑃 ∈ (Base‘𝐾) ∧ 𝑄 ∈ (Base‘𝐾) ∧ (0.‘𝐾) ∈ (Base‘𝐾)) ∧ ((0.‘𝐾)( ⋖ ‘𝐾)𝑃 ∧ (0.‘𝐾)( ⋖ ‘𝐾)𝑄)) → (𝑃 ≤ 𝑄 ↔ 𝑃 = 𝑄))
19	2, 6, 8, 11, 14, 16, 18	syl132anc 1415	1 ⊢ ((𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → (𝑃 ≤ 𝑄 ↔ 𝑃 = 𝑄))

Syntax hints:   → wi 4   ↔ wb 209   ∧ w3a 1103   = wceq 1570   ∈ wcel 2143   class class class wbr 5110  ‘cfv 6538  Basecbs 17270  lecple 17318  Posetcpo 18364  0.cp0 18478   ⋖ ccvr 40014  Atomscatm 40015  AtLatcal 40016

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-rep 5239  ax-sep 5258  ax-nul 5270  ax-pow 5338  ax-pr 5406  ax-un 7734

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3080  df-rex 3090  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3457  df-sbc 3746  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-pw 4565  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-iun 4959  df-br 5111  df-opab 5175  df-mpt 5194  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-riota 7369  df-proset 18351  df-poset 18370  df-plt 18385  df-glb 18402  df-p0 18480  df-lat 18489  df-covers 40018  df-ats 40019  df-atl 40050

This theorem is referenced by:  atncmp  40064  atnlt  40065  atnle  40069  cvlsupr2  40095  cvratlem  40173  2atjm  40197  atbtwn  40198  2atm  40279  2llnmeqat  40323  dalem25  40450  dalem55  40479  dalem57  40481  snatpsubN  40502  pmapat  40515  2llnma1b  40538  cdlemblem  40545  lhp2at0nle  40787  lhpat3  40798  4atexlemcnd  40824  trlval3  40939  cdlemc5  40947  cdleme3  40989  cdleme7  41001  cdleme11k  41020  cdleme16b  41031  cdleme16e  41034  cdleme16f  41035  cdlemednpq  41051  cdleme20j  41070  cdleme22aa  41091  cdleme22cN  41094  cdleme22d  41095  cdlemf2  41314  cdlemb3  41358  cdlemg12e  41399  cdlemg17dALTN  41416  cdlemg19a  41435  cdlemg27b  41448  cdlemg31d  41452  trlcone  41480  cdlemi  41572  tendotr  41582  cdlemk17  41610  cdlemk52  41706  cdleml1N  41728  dia2dimlem1  41816  dia2dimlem2  41817  dia2dimlem3  41818