# Metamath Proof Explorer

## Theorem cvlatexch2

Description: Atom exchange property. (Contributed by NM, 5-Nov-2012)

Ref Expression
Hypotheses cvlatexch.l
cvlatexch.j
cvlatexch.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
Assertion cvlatexch2

### Proof

Step Hyp Ref Expression
1 cvlatexch.l
2 cvlatexch.j
3 cvlatexch.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
4 1 2 3 cvlatexch1
5 cvllat ${⊢}{K}\in \mathrm{CvLat}\to {K}\in \mathrm{Lat}$
6 5 3ad2ant1 ${⊢}\left({K}\in \mathrm{CvLat}\wedge \left({P}\in {A}\wedge {Q}\in {A}\wedge {R}\in {A}\right)\wedge {P}\ne {R}\right)\to {K}\in \mathrm{Lat}$
7 simp22 ${⊢}\left({K}\in \mathrm{CvLat}\wedge \left({P}\in {A}\wedge {Q}\in {A}\wedge {R}\in {A}\right)\wedge {P}\ne {R}\right)\to {Q}\in {A}$
8 eqid ${⊢}{\mathrm{Base}}_{{K}}={\mathrm{Base}}_{{K}}$
9 8 3 atbase ${⊢}{Q}\in {A}\to {Q}\in {\mathrm{Base}}_{{K}}$
10 7 9 syl ${⊢}\left({K}\in \mathrm{CvLat}\wedge \left({P}\in {A}\wedge {Q}\in {A}\wedge {R}\in {A}\right)\wedge {P}\ne {R}\right)\to {Q}\in {\mathrm{Base}}_{{K}}$
11 simp23 ${⊢}\left({K}\in \mathrm{CvLat}\wedge \left({P}\in {A}\wedge {Q}\in {A}\wedge {R}\in {A}\right)\wedge {P}\ne {R}\right)\to {R}\in {A}$
12 8 3 atbase ${⊢}{R}\in {A}\to {R}\in {\mathrm{Base}}_{{K}}$
13 11 12 syl ${⊢}\left({K}\in \mathrm{CvLat}\wedge \left({P}\in {A}\wedge {Q}\in {A}\wedge {R}\in {A}\right)\wedge {P}\ne {R}\right)\to {R}\in {\mathrm{Base}}_{{K}}$
14 8 2 latjcom
15 6 10 13 14 syl3anc
16 15 breq2d
17 simp21 ${⊢}\left({K}\in \mathrm{CvLat}\wedge \left({P}\in {A}\wedge {Q}\in {A}\wedge {R}\in {A}\right)\wedge {P}\ne {R}\right)\to {P}\in {A}$
18 8 3 atbase ${⊢}{P}\in {A}\to {P}\in {\mathrm{Base}}_{{K}}$
19 17 18 syl ${⊢}\left({K}\in \mathrm{CvLat}\wedge \left({P}\in {A}\wedge {Q}\in {A}\wedge {R}\in {A}\right)\wedge {P}\ne {R}\right)\to {P}\in {\mathrm{Base}}_{{K}}$
20 8 2 latjcom
21 6 19 13 20 syl3anc
22 21 breq2d
23 4 16 22 3imtr4d