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	⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ( 𝐴 <P 𝐵 ↔ 𝐴 ⊊ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		eleq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 ∈ P ↔ 𝐴 ∈ P ) )
2	1	anbi1d	⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 ∈ P ∧ 𝑦 ∈ P ) ↔ ( 𝐴 ∈ P ∧ 𝑦 ∈ P ) ) )
3		psseq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 ⊊ 𝑦 ↔ 𝐴 ⊊ 𝑦 ) )
4	2 3	anbi12d	⊢ ( 𝑥 = 𝐴 → ( ( ( 𝑥 ∈ P ∧ 𝑦 ∈ P ) ∧ 𝑥 ⊊ 𝑦 ) ↔ ( ( 𝐴 ∈ P ∧ 𝑦 ∈ P ) ∧ 𝐴 ⊊ 𝑦 ) ) )
5		eleq1	⊢ ( 𝑦 = 𝐵 → ( 𝑦 ∈ P ↔ 𝐵 ∈ P ) )
6	5	anbi2d	⊢ ( 𝑦 = 𝐵 → ( ( 𝐴 ∈ P ∧ 𝑦 ∈ P ) ↔ ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) ) )
7		psseq2	⊢ ( 𝑦 = 𝐵 → ( 𝐴 ⊊ 𝑦 ↔ 𝐴 ⊊ 𝐵 ) )
8	6 7	anbi12d	⊢ ( 𝑦 = 𝐵 → ( ( ( 𝐴 ∈ P ∧ 𝑦 ∈ P ) ∧ 𝐴 ⊊ 𝑦 ) ↔ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) ∧ 𝐴 ⊊ 𝐵 ) ) )
9		df-ltp	⊢ <P = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ P ∧ 𝑦 ∈ P ) ∧ 𝑥 ⊊ 𝑦 ) }
10	4 8 9	brabg	⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ( 𝐴 <P 𝐵 ↔ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) ∧ 𝐴 ⊊ 𝐵 ) ) )
11	10	bianabs	⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ( 𝐴 <P 𝐵 ↔ 𝐴 ⊊ 𝐵 ) )