Metamath Proof Explorer

Theorem elpcliN

Description: Implication of membership in the projective subspace closure function. (Contributed by NM, 13-Sep-2013) (New usage is discouraged.)

Ref Expression
Hypotheses elpcli.s ⊢ S = PSubSp ⁡ K
elpcli.c ⊢ U = PCl ⁡ K
Assertion elpcliN ⊢ K ∈ V ∧ X ⊆ Y ∧ Y ∈ S ∧ Q ∈ U ⁡ X → Q ∈ Y

Proof

Step Hyp Ref Expression
1 elpcli.s ⊢ S = PSubSp ⁡ K
2 elpcli.c ⊢ U = PCl ⁡ K
3 simp1 ⊢ K ∈ V ∧ X ⊆ Y ∧ Y ∈ S → K ∈ V
4 simp2 ⊢ K ∈ V ∧ X ⊆ Y ∧ Y ∈ S → X ⊆ Y
5 eqid ⊢ Atoms ⁡ K = Atoms ⁡ K
6 5 1 psubssat ⊢ K ∈ V ∧ Y ∈ S → Y ⊆ Atoms ⁡ K
7 6 3adant2 ⊢ K ∈ V ∧ X ⊆ Y ∧ Y ∈ S → Y ⊆ Atoms ⁡ K
8 4 7 sstrd ⊢ K ∈ V ∧ X ⊆ Y ∧ Y ∈ S → X ⊆ Atoms ⁡ K
9 5 1 2 pclvalN ⊢ K ∈ V ∧ X ⊆ Atoms ⁡ K → U ⁡ X = ⋂ z ∈ S | X ⊆ z
10 3 8 9 syl2anc ⊢ K ∈ V ∧ X ⊆ Y ∧ Y ∈ S → U ⁡ X = ⋂ z ∈ S | X ⊆ z
11 10 eleq2d ⊢ K ∈ V ∧ X ⊆ Y ∧ Y ∈ S → Q ∈ U ⁡ X ↔ Q ∈ ⋂ z ∈ S | X ⊆ z
12 elintrabg ⊢ Q ∈ ⋂ z ∈ S | X ⊆ z → Q ∈ ⋂ z ∈ S | X ⊆ z ↔ ∀ z ∈ S X ⊆ z → Q ∈ z
13 12 ibi ⊢ Q ∈ ⋂ z ∈ S | X ⊆ z → ∀ z ∈ S X ⊆ z → Q ∈ z
14 11 13 syl6bi ⊢ K ∈ V ∧ X ⊆ Y ∧ Y ∈ S → Q ∈ U ⁡ X → ∀ z ∈ S X ⊆ z → Q ∈ z
15 sseq2 ⊢ z = Y → X ⊆ z ↔ X ⊆ Y
16 eleq2 ⊢ z = Y → Q ∈ z ↔ Q ∈ Y
17 15 16 imbi12d ⊢ z = Y → X ⊆ z → Q ∈ z ↔ X ⊆ Y → Q ∈ Y
18 17 rspccv ⊢ ∀ z ∈ S X ⊆ z → Q ∈ z → Y ∈ S → X ⊆ Y → Q ∈ Y
19 18 com13 ⊢ X ⊆ Y → Y ∈ S → ∀ z ∈ S X ⊆ z → Q ∈ z → Q ∈ Y
20 19 imp ⊢ X ⊆ Y ∧ Y ∈ S → ∀ z ∈ S X ⊆ z → Q ∈ z → Q ∈ Y
21 20 3adant1 ⊢ K ∈ V ∧ X ⊆ Y ∧ Y ∈ S → ∀ z ∈ S X ⊆ z → Q ∈ z → Q ∈ Y
22 14 21 syld ⊢ K ∈ V ∧ X ⊆ Y ∧ Y ∈ S → Q ∈ U ⁡ X → Q ∈ Y
23 22 imp ⊢ K ∈ V ∧ X ⊆ Y ∧ Y ∈ S ∧ Q ∈ U ⁡ X → Q ∈ Y