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 ⊢ < 𝑷 = x y | 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