Theorem isat

Description: The predicate "is an atom". ( ela analog.) (Contributed by NM, 18-Sep-2011)

	Ref	Expression
Hypotheses	isatom.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	isatom.z	⊢ 0 = ( 0. ‘ 𝐾 )
	isatom.c	⊢ 𝐶 = ( ⋖ ‘ 𝐾 )
	isatom.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
Assertion	isat	⊢ ( 𝐾 ∈ 𝐷 → ( 𝑃 ∈ 𝐴 ↔ ( 𝑃 ∈ 𝐵 ∧ 0 𝐶 𝑃 ) ) )

Proof

Step	Hyp	Ref	Expression
1		isatom.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		isatom.z	⊢ 0 = ( 0. ‘ 𝐾 )
3		isatom.c	⊢ 𝐶 = ( ⋖ ‘ 𝐾 )
4		isatom.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
5	1 2 3 4	pats	⊢ ( 𝐾 ∈ 𝐷 → 𝐴 = { 𝑥 ∈ 𝐵 ∣ 0 𝐶 𝑥 } )
6	5	eleq2d	⊢ ( 𝐾 ∈ 𝐷 → ( 𝑃 ∈ 𝐴 ↔ 𝑃 ∈ { 𝑥 ∈ 𝐵 ∣ 0 𝐶 𝑥 } ) )
7		breq2	⊢ ( 𝑥 = 𝑃 → ( 0 𝐶 𝑥 ↔ 0 𝐶 𝑃 ) )
8	7	elrab	⊢ ( 𝑃 ∈ { 𝑥 ∈ 𝐵 ∣ 0 𝐶 𝑥 } ↔ ( 𝑃 ∈ 𝐵 ∧ 0 𝐶 𝑃 ) )
9	6 8	bitrdi	⊢ ( 𝐾 ∈ 𝐷 → ( 𝑃 ∈ 𝐴 ↔ ( 𝑃 ∈ 𝐵 ∧ 0 𝐶 𝑃 ) ) )