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 ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
psubclset.p ⊢ ⊥ = ( ⊥𝑃 ‘ 𝐾 )
psubclset.c ⊢ 𝐶 = ( PSubCl ‘ 𝐾 )
Assertion ispsubclN ( 𝐾 ∈ 𝐷 → ( 𝑋 ∈ 𝐶 ↔ ( 𝑋 ⊆ 𝐴 ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑋 ) ) )

Proof

Step Hyp Ref Expression
1 psubclset.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
2 psubclset.p ⊢ ⊥ = ( ⊥𝑃 ‘ 𝐾 )
3 psubclset.c ⊢ 𝐶 = ( PSubCl ‘ 𝐾 )
4 1 2 3 psubclsetN ⊢ ( 𝐾 ∈ 𝐷 → 𝐶 = { 𝑥 ∣ ( 𝑥 ⊆ 𝐴 ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑥 ) ) = 𝑥 ) } )
5 4 eleq2d ⊢ ( 𝐾 ∈ 𝐷 → ( 𝑋 ∈ 𝐶 ↔ 𝑋 ∈ { 𝑥 ∣ ( 𝑥 ⊆ 𝐴 ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑥 ) ) = 𝑥 ) } ) )
6 1 fvexi ⊢ 𝐴 ∈ V
7 6 ssex ⊢ ( 𝑋 ⊆ 𝐴 → 𝑋 ∈ V )
8 7 adantr ⊢ ( ( 𝑋 ⊆ 𝐴 ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑋 ) → 𝑋 ∈ V )
9 sseq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 ⊆ 𝐴 ↔ 𝑋 ⊆ 𝐴 ) )
10 2fveq3 ⊢ ( 𝑥 = 𝑋 → ( ⊥ ‘ ( ⊥ ‘ 𝑥 ) ) = ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) )
11 id ⊢ ( 𝑥 = 𝑋 → 𝑥 = 𝑋 )
12 10 11 eqeq12d ⊢ ( 𝑥 = 𝑋 → ( ( ⊥ ‘ ( ⊥ ‘ 𝑥 ) ) = 𝑥 ↔ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑋 ) )
13 9 12 anbi12d ⊢ ( 𝑥 = 𝑋 → ( ( 𝑥 ⊆ 𝐴 ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑥 ) ) = 𝑥 ) ↔ ( 𝑋 ⊆ 𝐴 ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑋 ) ) )
14 8 13 elab3 ⊢ ( 𝑋 ∈ { 𝑥 ∣ ( 𝑥 ⊆ 𝐴 ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑥 ) ) = 𝑥 ) } ↔ ( 𝑋 ⊆ 𝐴 ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑋 ) )
15 5 14 bitrdi ⊢ ( 𝐾 ∈ 𝐷 → ( 𝑋 ∈ 𝐶 ↔ ( 𝑋 ⊆ 𝐴 ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑋 ) ) )