Theorem atbase

Description: An atom is a member of the lattice base set (i.e. a lattice element). ( atelch analog.) (Contributed by NM, 10-Oct-2011)

	Ref	Expression
Hypotheses	atombase.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	atombase.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
Assertion	atbase	⊢ ( 𝑃 ∈ 𝐴 → 𝑃 ∈ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		atombase.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		atombase.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
3		n0i	⊢ ( 𝑃 ∈ 𝐴 → ¬ 𝐴 = ∅ )
4	2	eqeq1i	⊢ ( 𝐴 = ∅ ↔ ( Atoms ‘ 𝐾 ) = ∅ )
5	3 4	sylnib	⊢ ( 𝑃 ∈ 𝐴 → ¬ ( Atoms ‘ 𝐾 ) = ∅ )
6		fvprc	⊢ ( ¬ 𝐾 ∈ V → ( Atoms ‘ 𝐾 ) = ∅ )
7	5 6	nsyl2	⊢ ( 𝑃 ∈ 𝐴 → 𝐾 ∈ V )
8		eqid	⊢ ( 0. ‘ 𝐾 ) = ( 0. ‘ 𝐾 )
9		eqid	⊢ ( ⋖ ‘ 𝐾 ) = ( ⋖ ‘ 𝐾 )
10	1 8 9 2	isat	⊢ ( 𝐾 ∈ V → ( 𝑃 ∈ 𝐴 ↔ ( 𝑃 ∈ 𝐵 ∧ ( 0. ‘ 𝐾 ) ( ⋖ ‘ 𝐾 ) 𝑃 ) ) )
11	10	simprbda	⊢ ( ( 𝐾 ∈ V ∧ 𝑃 ∈ 𝐴 ) → 𝑃 ∈ 𝐵 )
12	7 11	mpancom	⊢ ( 𝑃 ∈ 𝐴 → 𝑃 ∈ 𝐵 )