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

Metamath Proof Explorer

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 ⊢ ( 𝑃 ∈ 𝐴 → 𝑃 ∈ 𝐵 )