Theorem 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 e. AtLat /\ X C_ A /\ P e. ( U ` X ) ) -> E. y e. Fin ( y C_ X /\ P e. ( U ` y ) ) )

Proof

Step	Hyp	Ref	Expression
1		pclfin.a	|- A = ( Atoms ` K )
2		pclfin.c	|- U = ( PCl ` K )
3	1 2	pclfinN	|- ( ( K e. AtLat /\ X C_ A ) -> ( U ` X ) = U_ y e. ( Fin i^i ~P X ) ( U ` y ) )
4	3	eleq2d	|- ( ( K e. AtLat /\ X C_ A ) -> ( P e. ( U ` X ) <-> P e. U_ y e. ( Fin i^i ~P X ) ( U ` y ) ) )
5		eliun	|- ( P e. U_ y e. ( Fin i^i ~P X ) ( U ` y ) <-> E. y e. ( Fin i^i ~P X ) P e. ( U ` y ) )
6	4 5	bitrdi	|- ( ( K e. AtLat /\ X C_ A ) -> ( P e. ( U ` X ) <-> E. y e. ( Fin i^i ~P X ) P e. ( U ` y ) ) )
7		elin	|- ( y e. ( Fin i^i ~P X ) <-> ( y e. Fin /\ y e. ~P X ) )
8		elpwi	|- ( y e. ~P X -> y C_ X )
9	8	anim2i	|- ( ( y e. Fin /\ y e. ~P X ) -> ( y e. Fin /\ y C_ X ) )
10	7 9	sylbi	|- ( y e. ( Fin i^i ~P X ) -> ( y e. Fin /\ y C_ X ) )
11	10	anim1i	|- ( ( y e. ( Fin i^i ~P X ) /\ P e. ( U ` y ) ) -> ( ( y e. Fin /\ y C_ X ) /\ P e. ( U ` y ) ) )
12		anass	|- ( ( ( y e. Fin /\ y C_ X ) /\ P e. ( U ` y ) ) <-> ( y e. Fin /\ ( y C_ X /\ P e. ( U ` y ) ) ) )
13	11 12	sylib	|- ( ( y e. ( Fin i^i ~P X ) /\ P e. ( U ` y ) ) -> ( y e. Fin /\ ( y C_ X /\ P e. ( U ` y ) ) ) )
14	13	reximi2	|- ( E. y e. ( Fin i^i ~P X ) P e. ( U ` y ) -> E. y e. Fin ( y C_ X /\ P e. ( U ` y ) ) )
15	6 14	syl6bi	|- ( ( K e. AtLat /\ X C_ A ) -> ( P e. ( U ` X ) -> E. y e. Fin ( y C_ X /\ P e. ( U ` y ) ) ) )
16	15	3impia	|- ( ( K e. AtLat /\ X C_ A /\ P e. ( U ` X ) ) -> E. y e. Fin ( y C_ X /\ P e. ( U ` y ) ) )