# Metamath Proof Explorer

Description: Lemma for paddass . Show s =/= z by contradiction. (Contributed by NM, 8-Jan-2012)

Ref Expression
paddasslem.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$

### Proof

Step Hyp Ref Expression
3 paddasslem.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
4 breq1
5 4 biimpac
6 eqid ${⊢}{\mathrm{Base}}_{{K}}={\mathrm{Base}}_{{K}}$
7 simpll1
8 7 hllatd
9 simpll2
10 6 3 atbase ${⊢}{r}\in {A}\to {r}\in {\mathrm{Base}}_{{K}}$
11 9 10 syl
12 simp32 ${⊢}\left({K}\in \mathrm{HL}\wedge {r}\in {A}\wedge \left({x}\in {A}\wedge {y}\in {A}\wedge {z}\in {A}\right)\right)\to {y}\in {A}$
14 6 3 atbase ${⊢}{y}\in {A}\to {y}\in {\mathrm{Base}}_{{K}}$
15 13 14 syl
16 simp33 ${⊢}\left({K}\in \mathrm{HL}\wedge {r}\in {A}\wedge \left({x}\in {A}\wedge {y}\in {A}\wedge {z}\in {A}\right)\right)\to {z}\in {A}$
18 6 3 atbase ${⊢}{z}\in {A}\to {z}\in {\mathrm{Base}}_{{K}}$
19 17 18 syl
20 6 2 latjcl
21 8 15 19 20 syl3anc
22 simp31 ${⊢}\left({K}\in \mathrm{HL}\wedge {r}\in {A}\wedge \left({x}\in {A}\wedge {y}\in {A}\wedge {z}\in {A}\right)\right)\to {x}\in {A}$
24 6 3 atbase ${⊢}{x}\in {A}\to {x}\in {\mathrm{Base}}_{{K}}$
25 23 24 syl
26 6 2 latjcl
27 8 25 15 26 syl3anc
28 simplr
29 1 2 3 hlatlej2
30 7 23 13 29 syl3anc
31 simpr
32 6 1 2 latjle12
33 32 biimpd
34 8 15 19 27 33 syl13anc
35 30 31 34 mp2and
36 6 1 8 11 21 27 28 35 lattrd
37 36 ex
38 5 37 syl5
39 38 expdimp
40 39 necon3bd
41 40 exp31
42 41 com23
43 42 com24
44 43 3imp2