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=AtomsK
pclfin.c U=PClK
Assertion pclcmpatN KAtLatXAPUXyFinyXPUy

Proof

Step Hyp Ref Expression
1 pclfin.a A=AtomsK
2 pclfin.c U=PClK
3 1 2 pclfinN KAtLatXAUX=yFin𝒫XUy
4 3 eleq2d KAtLatXAPUXPyFin𝒫XUy
5 eliun PyFin𝒫XUyyFin𝒫XPUy
6 4 5 bitrdi KAtLatXAPUXyFin𝒫XPUy
7 elin yFin𝒫XyFiny𝒫X
8 elpwi y𝒫XyX
9 8 anim2i yFiny𝒫XyFinyX
10 7 9 sylbi yFin𝒫XyFinyX
11 10 anim1i yFin𝒫XPUyyFinyXPUy
12 anass yFinyXPUyyFinyXPUy
13 11 12 sylib yFin𝒫XPUyyFinyXPUy
14 13 reximi2 yFin𝒫XPUyyFinyXPUy
15 6 14 syl6bi KAtLatXAPUXyFinyXPUy
16 15 3impia KAtLatXAPUXyFinyXPUy