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	⊢ ( 𝐾 ∈ 𝐷 → ( 𝑋 ∈ 𝐶 ↔ ( 𝑋 ⊆ 𝐴 ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑋 ) ) )