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 ∈ 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 biimtrdi ⊢ 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