Metamath Proof Explorer


Theorem pclssidN

Description: A set of atoms is included in its projective subspace closure. (Contributed by NM, 12-Sep-2013) (New usage is discouraged.)

Ref Expression
Hypotheses pclss.a A = Atoms K
pclss.c U = PCl K
Assertion pclssidN K V X A X U X

Proof

Step Hyp Ref Expression
1 pclss.a A = Atoms K
2 pclss.c U = PCl K
3 ssintub X y PSubSp K | X y
4 eqid PSubSp K = PSubSp K
5 1 4 2 pclvalN K V X A U X = y PSubSp K | X y
6 3 5 sseqtrrid K V X A X U X