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 AtLat X A P U X y Fin y X P U y

Proof

Step Hyp Ref Expression
1 pclfin.a A = Atoms K
2 pclfin.c U = PCl K
3 1 2 pclfinN K AtLat X A U X = y Fin 𝒫 X U y
4 3 eleq2d K AtLat X A P U X P y Fin 𝒫 X U y
5 eliun P y Fin 𝒫 X U y y Fin 𝒫 X P U y
6 4 5 bitrdi K AtLat X A P U X y Fin 𝒫 X P U y
7 elin y Fin 𝒫 X y Fin y 𝒫 X
8 elpwi y 𝒫 X y X
9 8 anim2i y Fin y 𝒫 X y Fin y X
10 7 9 sylbi y Fin 𝒫 X y Fin y X
11 10 anim1i y Fin 𝒫 X P U y y Fin y X P U y
12 anass y Fin y X P U y y Fin y X P U y
13 11 12 sylib y Fin 𝒫 X P U y y Fin y X P U y
14 13 reximi2 y Fin 𝒫 X P U y y Fin y X P U y
15 6 14 syl6bi K AtLat X A P U X y Fin y X P U y
16 15 3impia K AtLat X A P U X y Fin y X P U y