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

Metamath Proof Explorer

Theorem prnmax

Description: A positive real has no largest member. Definition 9-3.1(iii) of Gleason p. 121. (Contributed by NM, 9-Mar-1996) (Revised by Mario Carneiro, 11-May-2013) (New usage is discouraged.)

Ref Expression
Assertion prnmax ⊢ A ∈ 𝑷 ∧ B ∈ A → ∃ x ∈ A B < 𝑸 x

Proof

Step Hyp Ref Expression
1 eleq1 ⊢ y = B → y ∈ A ↔ B ∈ A
2 1 anbi2d ⊢ y = B → A ∈ 𝑷 ∧ y ∈ A ↔ A ∈ 𝑷 ∧ B ∈ A
3 breq1 ⊢ y = B → y < 𝑸 x ↔ B < 𝑸 x
4 3 rexbidv ⊢ y = B → ∃ x ∈ A y < 𝑸 x ↔ ∃ x ∈ A B < 𝑸 x
5 2 4 imbi12d ⊢ y = B → A ∈ 𝑷 ∧ y ∈ A → ∃ x ∈ A y < 𝑸 x ↔ A ∈ 𝑷 ∧ B ∈ A → ∃ x ∈ A B < 𝑸 x
6 elnpi ⊢ A ∈ 𝑷 ↔ A ∈ V ∧ ∅ ⊂ A ∧ A ⊂ 𝑸 ∧ ∀ y ∈ A ∀ x x < 𝑸 y → x ∈ A ∧ ∃ x ∈ A y < 𝑸 x
7 6 simprbi ⊢ A ∈ 𝑷 → ∀ y ∈ A ∀ x x < 𝑸 y → x ∈ A ∧ ∃ x ∈ A y < 𝑸 x
8 7 r19.21bi ⊢ A ∈ 𝑷 ∧ y ∈ A → ∀ x x < 𝑸 y → x ∈ A ∧ ∃ x ∈ A y < 𝑸 x
9 8 simprd ⊢ A ∈ 𝑷 ∧ y ∈ A → ∃ x ∈ A y < 𝑸 x
10 5 9 vtoclg ⊢ B ∈ A → A ∈ 𝑷 ∧ B ∈ A → ∃ x ∈ A B < 𝑸 x
11 10 anabsi7 ⊢ A ∈ 𝑷 ∧ B ∈ A → ∃ x ∈ A B < 𝑸 x