meetat2 - Mathbox for Norm Megill

	Mathbox for Norm Megill		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > meetat2		Structured version Visualization version GIF version

Theorem meetat2 35079

Description: The meet of any element with an atom is either the atom or zero. (Contributed by NM, 30-Aug-2012.)

**Hypotheses**
Ref	Expression
m.b	⊢ 𝐵 = (Base‘𝐾)
m.m	⊢ ∧ = (meet‘𝐾)
m.z	⊢ 0 = (0.‘𝐾)
m.a	⊢ 𝐴 = (Atoms‘𝐾)

**Assertion**
Ref	Expression
meetat2	⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴) → ((𝑋 ∧ 𝑃) ∈ 𝐴 ∨ (𝑋 ∧ 𝑃) = 0 ))

**Proof of Theorem meetat2**
Step	Hyp	Ref	Expression
1		m.b	. . 3 ⊢ 𝐵 = (Base‘𝐾)
2		m.m	. . 3 ⊢ ∧ = (meet‘𝐾)
3		m.z	. . 3 ⊢ 0 = (0.‘𝐾)
4		m.a	. . 3 ⊢ 𝐴 = (Atoms‘𝐾)
5	1, 2, 3, 4	meetat 35078	. 2 ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴) → ((𝑋 ∧ 𝑃) = 𝑃 ∨ (𝑋 ∧ 𝑃) = 0 ))
6		eleq1a 2826	. . . 4 ⊢ (𝑃 ∈ 𝐴 → ((𝑋 ∧ 𝑃) = 𝑃 → (𝑋 ∧ 𝑃) ∈ 𝐴))
7	6	3ad2ant3 1129	. . 3 ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴) → ((𝑋 ∧ 𝑃) = 𝑃 → (𝑋 ∧ 𝑃) ∈ 𝐴))
8	7	orim1d 920	. 2 ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴) → (((𝑋 ∧ 𝑃) = 𝑃 ∨ (𝑋 ∧ 𝑃) = 0 ) → ((𝑋 ∧ 𝑃) ∈ 𝐴 ∨ (𝑋 ∧ 𝑃) = 0 )))
9	5, 8	mpd 15	1 ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴) → ((𝑋 ∧ 𝑃) ∈ 𝐴 ∨ (𝑋 ∧ 𝑃) = 0 ))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∨ wo 382 ∧ w3a 1072 = wceq 1624 ∈ wcel 2131 ‘cfv 6041 (class class class)co 6805 Basecbs 16051 meetcmee 17138 0.cp0 17230 OLcol 34956 Atomscatm 35045

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1863 ax-4 1878 ax-5 1980 ax-6 2046 ax-7 2082 ax-8 2133 ax-9 2140 ax-10 2160 ax-11 2175 ax-12 2188 ax-13 2383 ax-ext 2732 ax-rep 4915 ax-sep 4925 ax-nul 4933 ax-pow 4984 ax-pr 5047 ax-un 7106

This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3an 1074 df-tru 1627 df-ex 1846 df-nf 1851 df-sb 2039 df-eu 2603 df-mo 2604 df-clab 2739 df-cleq 2745 df-clel 2748 df-nfc 2883 df-ne 2925 df-ral 3047 df-rex 3048 df-reu 3049 df-rab 3051 df-v 3334 df-sbc 3569 df-csb 3667 df-dif 3710 df-un 3712 df-in 3714 df-ss 3721 df-nul 4051 df-if 4223 df-pw 4296 df-sn 4314 df-pr 4316 df-op 4320 df-uni 4581 df-iun 4666 df-br 4797 df-opab 4857 df-mpt 4874 df-id 5166 df-xp 5264 df-rel 5265 df-cnv 5266 df-co 5267 df-dm 5268 df-rn 5269 df-res 5270 df-ima 5271 df-iota 6004 df-fun 6043 df-fn 6044 df-f 6045 df-f1 6046 df-fo 6047 df-f1o 6048 df-fv 6049 df-riota 6766 df-ov 6808 df-oprab 6809 df-preset 17121 df-poset 17139 df-plt 17151 df-lub 17167 df-glb 17168 df-join 17169 df-meet 17170 df-p0 17232 df-lat 17239 df-oposet 34958 df-ol 34960 df-covers 35048 df-ats 35049

This theorem is referenced by: 2at0mat0 35306 atmod1i1m 35639

W3C validator