# Metamath Proof Explorer

Description: Lemma for paddass . The case when p = z . (Contributed by NM, 11-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)$
5 simplll ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {p}={z}\right)\wedge \left({X}\subseteq {A}\wedge {Y}\subseteq {A}\wedge {Z}\subseteq {A}\right)\right)\wedge {z}\in {Z}\right)\to {K}\in \mathrm{HL}$
6 simplr3 ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {p}={z}\right)\wedge \left({X}\subseteq {A}\wedge {Y}\subseteq {A}\wedge {Z}\subseteq {A}\right)\right)\wedge {z}\in {Z}\right)\to {Z}\subseteq {A}$
7 simplr1 ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {p}={z}\right)\wedge \left({X}\subseteq {A}\wedge {Y}\subseteq {A}\wedge {Z}\subseteq {A}\right)\right)\wedge {z}\in {Z}\right)\to {X}\subseteq {A}$
8 simplr2 ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {p}={z}\right)\wedge \left({X}\subseteq {A}\wedge {Y}\subseteq {A}\wedge {Z}\subseteq {A}\right)\right)\wedge {z}\in {Z}\right)\to {Y}\subseteq {A}$
13 simpllr ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {p}={z}\right)\wedge \left({X}\subseteq {A}\wedge {Y}\subseteq {A}\wedge {Z}\subseteq {A}\right)\right)\wedge {z}\in {Z}\right)\to {p}={z}$
14 simpr ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {p}={z}\right)\wedge \left({X}\subseteq {A}\wedge {Y}\subseteq {A}\wedge {Z}\subseteq {A}\right)\right)\wedge {z}\in {Z}\right)\to {z}\in {Z}$
15 13 14 eqeltrd ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {p}={z}\right)\wedge \left({X}\subseteq {A}\wedge {Y}\subseteq {A}\wedge {Z}\subseteq {A}\right)\right)\wedge {z}\in {Z}\right)\to {p}\in {Z}$