pclclN

Description: Closure of the projective subspace closure function. (Contributed by NM, 8-Sep-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	pclfval.a	$⊢ A = Atoms (K)$
	pclfval.s	$⊢ S = PSubSp (K)$
	pclfval.c	$⊢ U = PCl (K)$
Assertion	pclclN	$⊢ (K \in V \land X \subseteq A) \to U (X) \in S$

Proof

Step	Hyp	Ref	Expression
1		pclfval.a	$⊢ A = Atoms (K)$
2		pclfval.s	$⊢ S = PSubSp (K)$
3		pclfval.c	$⊢ U = PCl (K)$
4	1 2 3	pclvalN	$⊢ (K \in V \land X \subseteq A) \to U (X) = ⋂ \{y \in S \| X \subseteq y\}$
5	1 2	atpsubN	$⊢ K \in V \to A \in S$
6		sseq2	$⊢ y = A \to (X \subseteq y \leftrightarrow X \subseteq A)$
7	6	intminss	$⊢ (A \in S \land X \subseteq A) \to ⋂ \{y \in S \| X \subseteq y\} \subseteq A$
8	5 7	sylan	$⊢ (K \in V \land X \subseteq A) \to ⋂ \{y \in S \| X \subseteq y\} \subseteq A$
9		r19.26	$⊢ \forall y \in S ((X \subseteq y \to p \in y) \land (X \subseteq y \to q \in y)) \leftrightarrow (\forall y \in S (X \subseteq y \to p \in y) \land \forall y \in S (X \subseteq y \to q \in y))$
10		jcab	$⊢ (X \subseteq y \to (p \in y \land q \in y)) \leftrightarrow ((X \subseteq y \to p \in y) \land (X \subseteq y \to q \in y))$
11	10	ralbii	$⊢ \forall y \in S (X \subseteq y \to (p \in y \land q \in y)) \leftrightarrow \forall y \in S ((X \subseteq y \to p \in y) \land (X \subseteq y \to q \in y))$
12		vex	$⊢ p \in V$
13	12	elintrab	$⊢ p \in ⋂ \{y \in S \| X \subseteq y\} \leftrightarrow \forall y \in S (X \subseteq y \to p \in y)$
14		vex	$⊢ q \in V$
15	14	elintrab	$⊢ q \in ⋂ \{y \in S \| X \subseteq y\} \leftrightarrow \forall y \in S (X \subseteq y \to q \in y)$
16	13 15	anbi12i	$⊢ (p \in ⋂ \{y \in S \| X \subseteq y\} \land q \in ⋂ \{y \in S \| X \subseteq y\}) \leftrightarrow (\forall y \in S (X \subseteq y \to p \in y) \land \forall y \in S (X \subseteq y \to q \in y))$
17	9 11 16	3bitr4ri	$⊢ (p \in ⋂ \{y \in S \| X \subseteq y\} \land q \in ⋂ \{y \in S \| X \subseteq y\}) \leftrightarrow \forall y \in S (X \subseteq y \to (p \in y \land q \in y))$
18		simpll1	$⊢ (((K \in V \land r \leq_{K} (p join (K) q) \land r \in A) \land y \in S) \land (p \in y \land q \in y)) \to K \in V$
19		simplr	$⊢ (((K \in V \land r \leq_{K} (p join (K) q) \land r \in A) \land y \in S) \land (p \in y \land q \in y)) \to y \in S$
20		simpll3	$⊢ (((K \in V \land r \leq_{K} (p join (K) q) \land r \in A) \land y \in S) \land (p \in y \land q \in y)) \to r \in A$
21		simprl	$⊢ (((K \in V \land r \leq_{K} (p join (K) q) \land r \in A) \land y \in S) \land (p \in y \land q \in y)) \to p \in y$
22		simprr	$⊢ (((K \in V \land r \leq_{K} (p join (K) q) \land r \in A) \land y \in S) \land (p \in y \land q \in y)) \to q \in y$
23		simpll2	$⊢ (((K \in V \land r \leq_{K} (p join (K) q) \land r \in A) \land y \in S) \land (p \in y \land q \in y)) \to r \leq_{K} (p join (K) q)$
24		eqid	$⊢ \leq_{K} = \leq_{K}$
25		eqid	$⊢ join (K) = join (K)$
26	24 25 1 2	psubspi2N	$⊢ ((K \in V \land y \in S \land r \in A) \land (p \in y \land q \in y \land r \leq_{K} (p join (K) q))) \to r \in y$
27	18 19 20 21 22 23 26	syl33anc	$⊢ (((K \in V \land r \leq_{K} (p join (K) q) \land r \in A) \land y \in S) \land (p \in y \land q \in y)) \to r \in y$
28	27	ex	$⊢ ((K \in V \land r \leq_{K} (p join (K) q) \land r \in A) \land y \in S) \to ((p \in y \land q \in y) \to r \in y)$
29	28	imim2d	$⊢ ((K \in V \land r \leq_{K} (p join (K) q) \land r \in A) \land y \in S) \to ((X \subseteq y \to (p \in y \land q \in y)) \to (X \subseteq y \to r \in y))$
30	29	ralimdva	$⊢ (K \in V \land r \leq_{K} (p join (K) q) \land r \in A) \to (\forall y \in S (X \subseteq y \to (p \in y \land q \in y)) \to \forall y \in S (X \subseteq y \to r \in y))$
31		vex	$⊢ r \in V$
32	31	elintrab	$⊢ r \in ⋂ \{y \in S \| X \subseteq y\} \leftrightarrow \forall y \in S (X \subseteq y \to r \in y)$
33	30 32	imbitrrdi	$⊢ (K \in V \land r \leq_{K} (p join (K) q) \land r \in A) \to (\forall y \in S (X \subseteq y \to (p \in y \land q \in y)) \to r \in ⋂ \{y \in S \| X \subseteq y\})$
34	33	3exp	$⊢ K \in V \to (r \leq_{K} (p join (K) q) \to (r \in A \to (\forall y \in S (X \subseteq y \to (p \in y \land q \in y)) \to r \in ⋂ \{y \in S \| X \subseteq y\})))$
35	34	com24	$⊢ K \in V \to (\forall y \in S (X \subseteq y \to (p \in y \land q \in y)) \to (r \in A \to (r \leq_{K} (p join (K) q) \to r \in ⋂ \{y \in S \| X \subseteq y\})))$
36	17 35	biimtrid	$⊢ K \in V \to ((p \in ⋂ \{y \in S \| X \subseteq y\} \land q \in ⋂ \{y \in S \| X \subseteq y\}) \to (r \in A \to (r \leq_{K} (p join (K) q) \to r \in ⋂ \{y \in S \| X \subseteq y\})))$
37	36	ralrimdv	$⊢ K \in V \to ((p \in ⋂ \{y \in S \| X \subseteq y\} \land q \in ⋂ \{y \in S \| X \subseteq y\}) \to \forall r \in A (r \leq_{K} (p join (K) q) \to r \in ⋂ \{y \in S \| X \subseteq y\}))$
38	37	ralrimivv	$⊢ K \in V \to \forall p \in ⋂ \{y \in S \| X \subseteq y\} \forall q \in ⋂ \{y \in S \| X \subseteq y\} \forall r \in A (r \leq_{K} (p join (K) q) \to r \in ⋂ \{y \in S \| X \subseteq y\})$
39	38	adantr	$⊢ (K \in V \land X \subseteq A) \to \forall p \in ⋂ \{y \in S \| X \subseteq y\} \forall q \in ⋂ \{y \in S \| X \subseteq y\} \forall r \in A (r \leq_{K} (p join (K) q) \to r \in ⋂ \{y \in S \| X \subseteq y\})$
40	24 25 1 2	ispsubsp	$⊢ K \in V \to (⋂ \{y \in S \| X \subseteq y\} \in S \leftrightarrow (⋂ \{y \in S \| X \subseteq y\} \subseteq A \land \forall p \in ⋂ \{y \in S \| X \subseteq y\} \forall q \in ⋂ \{y \in S \| X \subseteq y\} \forall r \in A (r \leq_{K} (p join (K) q) \to r \in ⋂ \{y \in S \| X \subseteq y\})))$
41	40	adantr	$⊢ (K \in V \land X \subseteq A) \to (⋂ \{y \in S \| X \subseteq y\} \in S \leftrightarrow (⋂ \{y \in S \| X \subseteq y\} \subseteq A \land \forall p \in ⋂ \{y \in S \| X \subseteq y\} \forall q \in ⋂ \{y \in S \| X \subseteq y\} \forall r \in A (r \leq_{K} (p join (K) q) \to r \in ⋂ \{y \in S \| X \subseteq y\})))$
42	8 39 41	mpbir2and	$⊢ (K \in V \land X \subseteq A) \to ⋂ \{y \in S \| X \subseteq y\} \in S$
43	4 42	eqeltrd	$⊢ (K \in V \land X \subseteq A) \to U (X) \in S$

Metamath Proof Explorer

Theorem pclclN

Proof