Theorem lhpbase

Description: A co-atom is a member of the lattice base set (i.e., a lattice element). (Contributed by NM, 18-May-2012)

	Ref	Expression
Hypotheses	lhpbase.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	lhpbase.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
Assertion	lhpbase	⊢ ( 𝑊 ∈ 𝐻 → 𝑊 ∈ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		lhpbase.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		lhpbase.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
3		n0i	⊢ ( 𝑊 ∈ 𝐻 → ¬ 𝐻 = ∅ )
4	2	eqeq1i	⊢ ( 𝐻 = ∅ ↔ ( LHyp ‘ 𝐾 ) = ∅ )
5	3 4	sylnib	⊢ ( 𝑊 ∈ 𝐻 → ¬ ( LHyp ‘ 𝐾 ) = ∅ )
6		fvprc	⊢ ( ¬ 𝐾 ∈ V → ( LHyp ‘ 𝐾 ) = ∅ )
7	5 6	nsyl2	⊢ ( 𝑊 ∈ 𝐻 → 𝐾 ∈ V )
8		eqid	⊢ ( 1. ‘ 𝐾 ) = ( 1. ‘ 𝐾 )
9		eqid	⊢ ( ⋖ ‘ 𝐾 ) = ( ⋖ ‘ 𝐾 )
10	1 8 9 2	islhp	⊢ ( 𝐾 ∈ V → ( 𝑊 ∈ 𝐻 ↔ ( 𝑊 ∈ 𝐵 ∧ 𝑊 ( ⋖ ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ) ) )
11	10	simprbda	⊢ ( ( 𝐾 ∈ V ∧ 𝑊 ∈ 𝐻 ) → 𝑊 ∈ 𝐵 )
12	7 11	mpancom	⊢ ( 𝑊 ∈ 𝐻 → 𝑊 ∈ 𝐵 )