Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  ltprord Structured version   Visualization version   GIF version

Theorem ltprord 9731
 Description: Positive real 'less than' in terms of proper subset. (Contributed by NM, 20-Feb-1996.) (New usage is discouraged.)
Assertion
Ref Expression
ltprord ((𝐴P𝐵P) → (𝐴<P 𝐵𝐴𝐵))

Proof of Theorem ltprord
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eleq1 2676 . . . . 5 (𝑥 = 𝐴 → (𝑥P𝐴P))
21anbi1d 737 . . . 4 (𝑥 = 𝐴 → ((𝑥P𝑦P) ↔ (𝐴P𝑦P)))
3 psseq1 3656 . . . 4 (𝑥 = 𝐴 → (𝑥𝑦𝐴𝑦))
42, 3anbi12d 743 . . 3 (𝑥 = 𝐴 → (((𝑥P𝑦P) ∧ 𝑥𝑦) ↔ ((𝐴P𝑦P) ∧ 𝐴𝑦)))
5 eleq1 2676 . . . . 5 (𝑦 = 𝐵 → (𝑦P𝐵P))
65anbi2d 736 . . . 4 (𝑦 = 𝐵 → ((𝐴P𝑦P) ↔ (𝐴P𝐵P)))
7 psseq2 3657 . . . 4 (𝑦 = 𝐵 → (𝐴𝑦𝐴𝐵))
86, 7anbi12d 743 . . 3 (𝑦 = 𝐵 → (((𝐴P𝑦P) ∧ 𝐴𝑦) ↔ ((𝐴P𝐵P) ∧ 𝐴𝐵)))
9 df-ltp 9686 . . 3 <P = {⟨𝑥, 𝑦⟩ ∣ ((𝑥P𝑦P) ∧ 𝑥𝑦)}
104, 8, 9brabg 4919 . 2 ((𝐴P𝐵P) → (𝐴<P 𝐵 ↔ ((𝐴P𝐵P) ∧ 𝐴𝐵)))
1110bianabs 920 1 ((𝐴P𝐵P) → (𝐴<P 𝐵𝐴𝐵))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   = wceq 1475   ∈ wcel 1977   ⊊ wpss 3541   class class class wbr 4583  Pcnp 9560
 Copyright terms: Public domain W3C validator