This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem atcvr0

Description: An atom covers zero. ( atcv0 analog.) (Contributed by NM, 4-Nov-2011)

Ref Expression
Hypotheses atomcvr0.z ⊢ 0 ˙ = 0. ⁡ K
atomcvr0.c ⊢ C = ⋖ K
atomcvr0.a ⊢ A = Atoms ⁡ K
Assertion atcvr0 ⊢ K ∈ D ∧ P ∈ A → 0 ˙ C P

Proof

Step Hyp Ref Expression
1 atomcvr0.z ⊢ 0 ˙ = 0. ⁡ K
2 atomcvr0.c ⊢ C = ⋖ K
3 atomcvr0.a ⊢ A = Atoms ⁡ K
4 eqid ⊢ Base K = Base K
5 4 1 2 3 isat ⊢ K ∈ D → P ∈ A ↔ P ∈ Base K ∧ 0 ˙ C P
6 5 simplbda ⊢ K ∈ D ∧ P ∈ A → 0 ˙ C P