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

Metamath Proof Explorer

Theorem sspmaplubN

Description: A set of atoms is a subset of the projective map of its LUB. (Contributed by NM, 6-Mar-2012) (New usage is discouraged.)

	Ref	Expression
Hypotheses	sspmaplub.u	$⊢ U = lub (K)$
	sspmaplub.a	$⊢ A = Atoms (K)$
	sspmaplub.m	$⊢ M = pmap (K)$
Assertion	sspmaplubN	$⊢ (K \in HL \land S \subseteq A) \to S \subseteq M (U (S))$

Step	Hyp	Ref	Expression
1		sspmaplub.u	$⊢ U = lub (K)$
2		sspmaplub.a	$⊢ A = Atoms (K)$
3		sspmaplub.m	$⊢ M = pmap (K)$
4		eqid	$⊢ ⊥_{𝑃} (K) = ⊥_{𝑃} (K)$
5	2 4	2polssN	$⊢ (K \in HL \land S \subseteq A) \to S \subseteq ⊥_{𝑃} (K) (⊥_{𝑃} (K) (S))$
6	1 2 3 4	2polvalN	$⊢ (K \in HL \land S \subseteq A) \to ⊥_{𝑃} (K) (⊥_{𝑃} (K) (S)) = M (U (S))$
7	5 6	sseqtrd	$⊢ (K \in HL \land S \subseteq A) \to S \subseteq M (U (S))$