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

Metamath Proof Explorer

Theorem pclssN

Description: Ordering is preserved by subspace closure. (Contributed by NM, 8-Sep-2013) (New usage is discouraged.)

		Ref	Expression
	Hypotheses	pclss.a	$⊢ A = Atoms (K)$
		pclss.c	$⊢ U = PCl (K)$
	Assertion	pclssN	$⊢ (K \in V \land X \subseteq Y \land Y \subseteq A) \to U (X) \subseteq U (Y)$

Proof

Step	Hyp	Ref	Expression
1		pclss.a	$⊢ A = Atoms (K)$
2		pclss.c	$⊢ U = PCl (K)$
3		sstr2	$⊢ X \subseteq Y \to (Y \subseteq y \to X \subseteq y)$
4	3	3ad2ant2	$⊢ (K \in V \land X \subseteq Y \land Y \subseteq A) \to (Y \subseteq y \to X \subseteq y)$
5	4	adantr	$⊢ ((K \in V \land X \subseteq Y \land Y \subseteq A) \land y \in PSubSp (K)) \to (Y \subseteq y \to X \subseteq y)$
6	5	ss2rabdv	$⊢ (K \in V \land X \subseteq Y \land Y \subseteq A) \to \{y \in PSubSp (K) \| Y \subseteq y\} \subseteq \{y \in PSubSp (K) \| X \subseteq y\}$
7		intss	$⊢ \{y \in PSubSp (K) \| Y \subseteq y\} \subseteq \{y \in PSubSp (K) \| X \subseteq y\} \to ⋂ \{y \in PSubSp (K) \| X \subseteq y\} \subseteq ⋂ \{y \in PSubSp (K) \| Y \subseteq y\}$
8	6 7	syl	$⊢ (K \in V \land X \subseteq Y \land Y \subseteq A) \to ⋂ \{y \in PSubSp (K) \| X \subseteq y\} \subseteq ⋂ \{y \in PSubSp (K) \| Y \subseteq y\}$
9		simp1	$⊢ (K \in V \land X \subseteq Y \land Y \subseteq A) \to K \in V$
10		sstr	$⊢ (X \subseteq Y \land Y \subseteq A) \to X \subseteq A$
11	10	3adant1	$⊢ (K \in V \land X \subseteq Y \land Y \subseteq A) \to X \subseteq A$
12		eqid	$⊢ PSubSp (K) = PSubSp (K)$
13	1 12 2	pclvalN	$⊢ (K \in V \land X \subseteq A) \to U (X) = ⋂ \{y \in PSubSp (K) \| X \subseteq y\}$
14	9 11 13	syl2anc	$⊢ (K \in V \land X \subseteq Y \land Y \subseteq A) \to U (X) = ⋂ \{y \in PSubSp (K) \| X \subseteq y\}$
15	1 12 2	pclvalN	$⊢ (K \in V \land Y \subseteq A) \to U (Y) = ⋂ \{y \in PSubSp (K) \| Y \subseteq y\}$
16	15	3adant2	$⊢ (K \in V \land X \subseteq Y \land Y \subseteq A) \to U (Y) = ⋂ \{y \in PSubSp (K) \| Y \subseteq y\}$
17	8 14 16	3sstr4d	$⊢ (K \in V \land X \subseteq Y \land Y \subseteq A) \to U (X) \subseteq U (Y)$