Theorem ltprord

Description: Positive real 'less than' in terms of proper subset. (Contributed by NM, 20-Feb-1996) (New usage is discouraged.)

	Ref	Expression
Assertion	ltprord	|- ( ( A e. P. /\ B e. P. ) -> ( A A C. B ) )

Proof

Step	Hyp	Ref	Expression
1		eleq1	|- ( x = A -> ( x e. P. <-> A e. P. ) )
2	1	anbi1d	|- ( x = A -> ( ( x e. P. /\ y e. P. ) <-> ( A e. P. /\ y e. P. ) ) )
3		psseq1	|- ( x = A -> ( x C. y <-> A C. y ) )
4	2 3	anbi12d	|- ( x = A -> ( ( ( x e. P. /\ y e. P. ) /\ x C. y ) <-> ( ( A e. P. /\ y e. P. ) /\ A C. y ) ) )
5		eleq1	|- ( y = B -> ( y e. P. <-> B e. P. ) )
6	5	anbi2d	|- ( y = B -> ( ( A e. P. /\ y e. P. ) <-> ( A e. P. /\ B e. P. ) ) )
7		psseq2	|- ( y = B -> ( A C. y <-> A C. B ) )
8	6 7	anbi12d	|- ( y = B -> ( ( ( A e. P. /\ y e. P. ) /\ A C. y ) <-> ( ( A e. P. /\ B e. P. ) /\ A C. B ) ) )
9		df-ltp	|- . | ( ( x e. P. /\ y e. P. ) /\ x C. y ) }
10	4 8 9	brabg	|- ( ( A e. P. /\ B e. P. ) -> ( A ( ( A e. P. /\ B e. P. ) /\ A C. B ) ) )
11	10	bianabs	|- ( ( A e. P. /\ B e. P. ) -> ( A A C. B ) )