Metamath Proof Explorer


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 ) ) )