This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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