![]() |
Mathbox for Norm Megill |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > atcmp | Structured version Visualization version GIF version |
Description: If two atoms are comparable, they are equal. (atsseq 29820 analog.) (Contributed by NM, 13-Oct-2011.) |
Ref | Expression |
---|---|
atcmp.l | ⊢ ≤ = (le‘𝐾) |
atcmp.a | ⊢ 𝐴 = (Atoms‘𝐾) |
Ref | Expression |
---|---|
atcmp | ⊢ ((𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → (𝑃 ≤ 𝑄 ↔ 𝑃 = 𝑄)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | atlpos 35993 | . . 3 ⊢ (𝐾 ∈ AtLat → 𝐾 ∈ Poset) | |
2 | 1 | 3ad2ant1 1126 | . 2 ⊢ ((𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → 𝐾 ∈ Poset) |
3 | eqid 2795 | . . . 4 ⊢ (Base‘𝐾) = (Base‘𝐾) | |
4 | atcmp.a | . . . 4 ⊢ 𝐴 = (Atoms‘𝐾) | |
5 | 3, 4 | atbase 35981 | . . 3 ⊢ (𝑃 ∈ 𝐴 → 𝑃 ∈ (Base‘𝐾)) |
6 | 5 | 3ad2ant2 1127 | . 2 ⊢ ((𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → 𝑃 ∈ (Base‘𝐾)) |
7 | 3, 4 | atbase 35981 | . . 3 ⊢ (𝑄 ∈ 𝐴 → 𝑄 ∈ (Base‘𝐾)) |
8 | 7 | 3ad2ant3 1128 | . 2 ⊢ ((𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → 𝑄 ∈ (Base‘𝐾)) |
9 | eqid 2795 | . . . 4 ⊢ (0.‘𝐾) = (0.‘𝐾) | |
10 | 3, 9 | atl0cl 35995 | . . 3 ⊢ (𝐾 ∈ AtLat → (0.‘𝐾) ∈ (Base‘𝐾)) |
11 | 10 | 3ad2ant1 1126 | . 2 ⊢ ((𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → (0.‘𝐾) ∈ (Base‘𝐾)) |
12 | eqid 2795 | . . . 4 ⊢ ( ⋖ ‘𝐾) = ( ⋖ ‘𝐾) | |
13 | 9, 12, 4 | atcvr0 35980 | . . 3 ⊢ ((𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴) → (0.‘𝐾)( ⋖ ‘𝐾)𝑃) |
14 | 13 | 3adant3 1125 | . 2 ⊢ ((𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → (0.‘𝐾)( ⋖ ‘𝐾)𝑃) |
15 | 9, 12, 4 | atcvr0 35980 | . . 3 ⊢ ((𝐾 ∈ AtLat ∧ 𝑄 ∈ 𝐴) → (0.‘𝐾)( ⋖ ‘𝐾)𝑄) |
16 | 15 | 3adant2 1124 | . 2 ⊢ ((𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → (0.‘𝐾)( ⋖ ‘𝐾)𝑄) |
17 | atcmp.l | . . 3 ⊢ ≤ = (le‘𝐾) | |
18 | 3, 17, 12 | cvrcmp 35975 | . 2 ⊢ ((𝐾 ∈ Poset ∧ (𝑃 ∈ (Base‘𝐾) ∧ 𝑄 ∈ (Base‘𝐾) ∧ (0.‘𝐾) ∈ (Base‘𝐾)) ∧ ((0.‘𝐾)( ⋖ ‘𝐾)𝑃 ∧ (0.‘𝐾)( ⋖ ‘𝐾)𝑄)) → (𝑃 ≤ 𝑄 ↔ 𝑃 = 𝑄)) |
19 | 2, 6, 8, 11, 14, 16, 18 | syl132anc 1381 | 1 ⊢ ((𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → (𝑃 ≤ 𝑄 ↔ 𝑃 = 𝑄)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 ∧ w3a 1080 = wceq 1522 ∈ wcel 2081 class class class wbr 4966 ‘cfv 6230 Basecbs 16317 lecple 16406 Posetcpo 17384 0.cp0 17481 ⋖ ccvr 35954 Atomscatm 35955 AtLatcal 35956 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1777 ax-4 1791 ax-5 1888 ax-6 1947 ax-7 1992 ax-8 2083 ax-9 2091 ax-10 2112 ax-11 2126 ax-12 2141 ax-13 2344 ax-ext 2769 ax-rep 5086 ax-sep 5099 ax-nul 5106 ax-pow 5162 ax-pr 5226 ax-un 7324 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3an 1082 df-tru 1525 df-ex 1762 df-nf 1766 df-sb 2043 df-mo 2576 df-eu 2612 df-clab 2776 df-cleq 2788 df-clel 2863 df-nfc 2935 df-ne 2985 df-ral 3110 df-rex 3111 df-reu 3112 df-rab 3114 df-v 3439 df-sbc 3710 df-csb 3816 df-dif 3866 df-un 3868 df-in 3870 df-ss 3878 df-nul 4216 df-if 4386 df-pw 4459 df-sn 4477 df-pr 4479 df-op 4483 df-uni 4750 df-iun 4831 df-br 4967 df-opab 5029 df-mpt 5046 df-id 5353 df-xp 5454 df-rel 5455 df-cnv 5456 df-co 5457 df-dm 5458 df-rn 5459 df-res 5460 df-ima 5461 df-iota 6194 df-fun 6232 df-fn 6233 df-f 6234 df-f1 6235 df-fo 6236 df-f1o 6237 df-fv 6238 df-riota 6982 df-proset 17372 df-poset 17390 df-plt 17402 df-glb 17419 df-p0 17483 df-lat 17490 df-covers 35958 df-ats 35959 df-atl 35990 |
This theorem is referenced by: atncmp 36004 atnlt 36005 atnle 36009 cvlsupr2 36035 cvratlem 36113 2atjm 36137 atbtwn 36138 2atm 36219 2llnmeqat 36263 dalem25 36390 dalem55 36419 dalem57 36421 snatpsubN 36442 pmapat 36455 2llnma1b 36478 cdlemblem 36485 lhp2at0nle 36727 lhpat3 36738 4atexlemcnd 36764 trlval3 36879 cdlemc5 36887 cdleme3 36929 cdleme7 36941 cdleme11k 36960 cdleme16b 36971 cdleme16e 36974 cdleme16f 36975 cdlemednpq 36991 cdleme20j 37010 cdleme22aa 37031 cdleme22cN 37034 cdleme22d 37035 cdlemf2 37254 cdlemb3 37298 cdlemg12e 37339 cdlemg17dALTN 37356 cdlemg19a 37375 cdlemg27b 37388 cdlemg31d 37392 trlcone 37420 cdlemi 37512 tendotr 37522 cdlemk17 37550 cdlemk52 37646 cdleml1N 37668 dia2dimlem1 37756 dia2dimlem2 37757 dia2dimlem3 37758 |
Copyright terms: Public domain | W3C validator |