pclcmpatN

Description: The set of projective subspaces is compactly atomistic: if an atom is in the projective subspace closure of a set of atoms, it also belongs to the projective subspace closure of a finite subset of that set. Analogous to Lemma 3.3.10 of PtakPulmannova p. 74. (Contributed by NM, 10-Sep-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	pclfin.a	$⊢ A = Atoms (K)$
	pclfin.c	$⊢ U = PCl (K)$
Assertion	pclcmpatN	$⊢ (K \in AtLat \land X \subseteq A \land P \in U (X)) \to \exists y \in Fin (y \subseteq X \land P \in U (y))$

Proof

Step	Hyp	Ref	Expression
1		pclfin.a	$⊢ A = Atoms (K)$
2		pclfin.c	$⊢ U = PCl (K)$
3	1 2	pclfinN	$⊢ (K \in AtLat \land X \subseteq A) \to U (X) = ⋃_{y \in Fin \cap 𝒫 X} U (y)$
4	3	eleq2d	$⊢ (K \in AtLat \land X \subseteq A) \to (P \in U (X) \leftrightarrow P \in ⋃_{y \in Fin \cap 𝒫 X} U (y))$
5		eliun	$⊢ P \in ⋃_{y \in Fin \cap 𝒫 X} U (y) \leftrightarrow \exists y \in (Fin \cap 𝒫 X) P \in U (y)$
6	4 5	bitrdi	$⊢ (K \in AtLat \land X \subseteq A) \to (P \in U (X) \leftrightarrow \exists y \in (Fin \cap 𝒫 X) P \in U (y))$
7		elin	$⊢ y \in (Fin \cap 𝒫 X) \leftrightarrow (y \in Fin \land y \in 𝒫 X)$
8		elpwi	$⊢ y \in 𝒫 X \to y \subseteq X$
9	8	anim2i	$⊢ (y \in Fin \land y \in 𝒫 X) \to (y \in Fin \land y \subseteq X)$
10	7 9	sylbi	$⊢ y \in (Fin \cap 𝒫 X) \to (y \in Fin \land y \subseteq X)$
11	10	anim1i	$⊢ (y \in (Fin \cap 𝒫 X) \land P \in U (y)) \to ((y \in Fin \land y \subseteq X) \land P \in U (y))$
12		anass	$⊢ ((y \in Fin \land y \subseteq X) \land P \in U (y)) \leftrightarrow (y \in Fin \land (y \subseteq X \land P \in U (y)))$
13	11 12	sylib	$⊢ (y \in (Fin \cap 𝒫 X) \land P \in U (y)) \to (y \in Fin \land (y \subseteq X \land P \in U (y)))$
14	13	reximi2	$⊢ \exists y \in (Fin \cap 𝒫 X) P \in U (y) \to \exists y \in Fin (y \subseteq X \land P \in U (y))$
15	6 14	biimtrdi	$⊢ (K \in AtLat \land X \subseteq A) \to (P \in U (X) \to \exists y \in Fin (y \subseteq X \land P \in U (y)))$
16	15	3impia	$⊢ (K \in AtLat \land X \subseteq A \land P \in U (X)) \to \exists y \in Fin (y \subseteq X \land P \in U (y))$

Metamath Proof Explorer

Theorem pclcmpatN

Proof