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

Metamath Proof Explorer

Theorem isat2

Description: The predicate "is an atom". ( elatcv0 analog.) (Contributed by NM, 18-Jun-2012)

	Ref	Expression
Hypotheses	isatom.b	$⊢ B = {Base}_{K}$
	isatom.z	$⊢ \underset{˙}{0} = 0. (K)$
	isatom.c	$⊢ C = ⋖_{K}$
	isatom.a	$⊢ A = Atoms (K)$
Assertion	isat2	$⊢ (K \in D \land P \in B) \to (P \in A \leftrightarrow \underset{˙}{0} C P)$

Step	Hyp	Ref	Expression
1		isatom.b	$⊢ B = {Base}_{K}$
2		isatom.z	$⊢ \underset{˙}{0} = 0. (K)$
3		isatom.c	$⊢ C = ⋖_{K}$
4		isatom.a	$⊢ A = Atoms (K)$
5	1 2 3 4	isat	$⊢ K \in D \to (P \in A \leftrightarrow (P \in B \land \underset{˙}{0} C P))$
6	5	baibd	$⊢ (K \in D \land P \in B) \to (P \in A \leftrightarrow \underset{˙}{0} C P)$