Metamath Proof Explorer

Theorem ispsubsp

Description: The predicate "is a projective subspace". (Contributed by NM, 2-Oct-2011)

		Ref	Expression
	Hypotheses	psubspset.l	\|- .<_ = ( le ` K )
		psubspset.j	\|- .\/ = ( join ` K )
		psubspset.a	\|- A = ( Atoms ` K )
		psubspset.s	\|- S = ( PSubSp ` K )
	Assertion	ispsubsp	\|- ( K e. D -> ( X e. S <-> ( X C_ A /\ A. p e. X A. q e. X A. r e. A ( r .<_ ( p .\/ q ) -> r e. X ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		psubspset.l	\|- .<_ = ( le ` K )
2		psubspset.j	\|- .\/ = ( join ` K )
3		psubspset.a	\|- A = ( Atoms ` K )
4		psubspset.s	\|- S = ( PSubSp ` K )
5	1 2 3 4	psubspset	\|- ( K e. D -> S = { x \| ( x C_ A /\ A. p e. x A. q e. x A. r e. A ( r .<_ ( p .\/ q ) -> r e. x ) ) } )
6	5	eleq2d	\|- ( K e. D -> ( X e. S <-> X e. { x \| ( x C_ A /\ A. p e. x A. q e. x A. r e. A ( r .<_ ( p .\/ q ) -> r e. x ) ) } ) )
7	3	fvexi	\|- A e. _V
8	7	ssex	\|- ( X C_ A -> X e. _V )
9	8	adantr	\|- ( ( X C_ A /\ A. p e. X A. q e. X A. r e. A ( r .<_ ( p .\/ q ) -> r e. X ) ) -> X e. _V )
10		sseq1	\|- ( x = X -> ( x C_ A <-> X C_ A ) )
11		eleq2	\|- ( x = X -> ( r e. x <-> r e. X ) )
12	11	imbi2d	\|- ( x = X -> ( ( r .<_ ( p .\/ q ) -> r e. x ) <-> ( r .<_ ( p .\/ q ) -> r e. X ) ) )
13	12	ralbidv	\|- ( x = X -> ( A. r e. A ( r .<_ ( p .\/ q ) -> r e. x ) <-> A. r e. A ( r .<_ ( p .\/ q ) -> r e. X ) ) )
14	13	raleqbi1dv	\|- ( x = X -> ( A. q e. x A. r e. A ( r .<_ ( p .\/ q ) -> r e. x ) <-> A. q e. X A. r e. A ( r .<_ ( p .\/ q ) -> r e. X ) ) )
15	14	raleqbi1dv	\|- ( x = X -> ( A. p e. x A. q e. x A. r e. A ( r .<_ ( p .\/ q ) -> r e. x ) <-> A. p e. X A. q e. X A. r e. A ( r .<_ ( p .\/ q ) -> r e. X ) ) )
16	10 15	anbi12d	\|- ( x = X -> ( ( x C_ A /\ A. p e. x A. q e. x A. r e. A ( r .<_ ( p .\/ q ) -> r e. x ) ) <-> ( X C_ A /\ A. p e. X A. q e. X A. r e. A ( r .<_ ( p .\/ q ) -> r e. X ) ) ) )
17	9 16	elab3	\|- ( X e. { x \| ( x C_ A /\ A. p e. x A. q e. x A. r e. A ( r .<_ ( p .\/ q ) -> r e. x ) ) } <-> ( X C_ A /\ A. p e. X A. q e. X A. r e. A ( r .<_ ( p .\/ q ) -> r e. X ) ) )
18	6 17	bitrdi	\|- ( K e. D -> ( X e. S <-> ( X C_ A /\ A. p e. X A. q e. X A. r e. A ( r .<_ ( p .\/ q ) -> r e. X ) ) ) )