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

Metamath Proof Explorer

Theorem ispsubclN

Description: The predicate "is a closed projective subspace". (Contributed by NM, 23-Jan-2012) (New usage is discouraged.)

Ref Expression
Hypotheses psubclset.a ⊢ A = Atoms ⁡ K
psubclset.p ⊢ ⊥ ˙ = ⊥ 𝑃 ⁡ K
psubclset.c ⊢ C = PSubCl ⁡ K
Assertion ispsubclN ⊢ K ∈ D → X ∈ C ↔ X ⊆ A ∧ ⊥ ˙ ⁡ ⊥ ˙ ⁡ X = X

Proof

Step Hyp Ref Expression
1 psubclset.a ⊢ A = Atoms ⁡ K
2 psubclset.p ⊢ ⊥ ˙ = ⊥ 𝑃 ⁡ K
3 psubclset.c ⊢ C = PSubCl ⁡ K
4 1 2 3 psubclsetN ⊢ K ∈ D → C = x | x ⊆ A ∧ ⊥ ˙ ⁡ ⊥ ˙ ⁡ x = x
5 4 eleq2d ⊢ K ∈ D → X ∈ C ↔ X ∈ x | x ⊆ A ∧ ⊥ ˙ ⁡ ⊥ ˙ ⁡ x = x
6 1 fvexi ⊢ A ∈ V
7 6 ssex ⊢ X ⊆ A → X ∈ V
8 7 adantr ⊢ X ⊆ A ∧ ⊥ ˙ ⁡ ⊥ ˙ ⁡ X = X → X ∈ V
9 sseq1 ⊢ x = X → x ⊆ A ↔ X ⊆ A
10 2fveq3 ⊢ x = X → ⊥ ˙ ⁡ ⊥ ˙ ⁡ x = ⊥ ˙ ⁡ ⊥ ˙ ⁡ X
11 id ⊢ x = X → x = X
12 10 11 eqeq12d ⊢ x = X → ⊥ ˙ ⁡ ⊥ ˙ ⁡ x = x ↔ ⊥ ˙ ⁡ ⊥ ˙ ⁡ X = X
13 9 12 anbi12d ⊢ x = X → x ⊆ A ∧ ⊥ ˙ ⁡ ⊥ ˙ ⁡ x = x ↔ X ⊆ A ∧ ⊥ ˙ ⁡ ⊥ ˙ ⁡ X = X
14 8 13 elab3 ⊢ X ∈ x | x ⊆ A ∧ ⊥ ˙ ⁡ ⊥ ˙ ⁡ x = x ↔ X ⊆ A ∧ ⊥ ˙ ⁡ ⊥ ˙ ⁡ X = X
15 5 14 bitrdi ⊢ K ∈ D → X ∈ C ↔ X ⊆ A ∧ ⊥ ˙ ⁡ ⊥ ˙ ⁡ X = X