This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝐴 ∈ 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 𝐵 ↔ 𝐴 ⊊ 𝐵 ) )