Metamath Proof Explorer

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∈𝑷∧B∈𝑷→A<𝑷B↔A⊂B

Proof

Step Hyp Ref Expression
1 eleq1 ⊢x=A→x∈𝑷↔A∈𝑷
2 1 anbi1d ⊢x=A→x∈𝑷∧y∈𝑷↔A∈𝑷∧y∈𝑷
3 psseq1 ⊢x=A→x⊂y↔A⊂y
4 2 3 anbi12d ⊢x=A→x∈𝑷∧y∈𝑷∧x⊂y↔A∈𝑷∧y∈𝑷∧A⊂y
5 eleq1 ⊢y=B→y∈𝑷↔B∈𝑷
6 5 anbi2d ⊢y=B→A∈𝑷∧y∈𝑷↔A∈𝑷∧B∈𝑷
7 psseq2 ⊢y=B→A⊂y↔A⊂B
8 6 7 anbi12d ⊢y=B→A∈𝑷∧y∈𝑷∧A⊂y↔A∈𝑷∧B∈𝑷∧A⊂B
9 df-ltp ⊢<𝑷=xy|x∈𝑷∧y∈𝑷∧x⊂y
10 4 8 9 brabg ⊢A∈𝑷∧B∈𝑷→A<𝑷B↔A∈𝑷∧B∈𝑷∧A⊂B
11 10 bianabs ⊢A∈𝑷∧B∈𝑷→A<𝑷B↔A⊂B