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 ( ( 𝐴 ∈ P ∧ 𝐵 ∈ 𝐴 ) → ∃ 𝑥 ∈ 𝐴 𝐵 <Q 𝑥 )

Proof

Step Hyp Ref Expression
1 eleq1 ⊢ ( 𝑦 = 𝐵 → ( 𝑦 ∈ 𝐴 ↔ 𝐵 ∈ 𝐴 ) )
2 1 anbi2d ⊢ ( 𝑦 = 𝐵 → ( ( 𝐴 ∈ P ∧ 𝑦 ∈ 𝐴 ) ↔ ( 𝐴 ∈ P ∧ 𝐵 ∈ 𝐴 ) ) )
3 breq1 ⊢ ( 𝑦 = 𝐵 → ( 𝑦 <Q 𝑥 ↔ 𝐵 <Q 𝑥 ) )
4 3 rexbidv ⊢ ( 𝑦 = 𝐵 → ( ∃ 𝑥 ∈ 𝐴 𝑦 <Q 𝑥 ↔ ∃ 𝑥 ∈ 𝐴 𝐵 <Q 𝑥 ) )
5 2 4 imbi12d ⊢ ( 𝑦 = 𝐵 → ( ( ( 𝐴 ∈ P ∧ 𝑦 ∈ 𝐴 ) → ∃ 𝑥 ∈ 𝐴 𝑦 <Q 𝑥 ) ↔ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ 𝐴 ) → ∃ 𝑥 ∈ 𝐴 𝐵 <Q 𝑥 ) ) )
6 elnpi ⊢ ( 𝐴 ∈ P ↔ ( ( 𝐴 ∈ V ∧ ∅ ⊊ 𝐴 ∧ 𝐴 ⊊ Q ) ∧ ∀ 𝑦 ∈ 𝐴 ( ∀ 𝑥 ( 𝑥 <Q 𝑦 → 𝑥 ∈ 𝐴 ) ∧ ∃ 𝑥 ∈ 𝐴 𝑦 <Q 𝑥 ) ) )
7 6 simprbi ⊢ ( 𝐴 ∈ P → ∀ 𝑦 ∈ 𝐴 ( ∀ 𝑥 ( 𝑥 <Q 𝑦 → 𝑥 ∈ 𝐴 ) ∧ ∃ 𝑥 ∈ 𝐴 𝑦 <Q 𝑥 ) )
8 7 r19.21bi ⊢ ( ( 𝐴 ∈ P ∧ 𝑦 ∈ 𝐴 ) → ( ∀ 𝑥 ( 𝑥 <Q 𝑦 → 𝑥 ∈ 𝐴 ) ∧ ∃ 𝑥 ∈ 𝐴 𝑦 <Q 𝑥 ) )
9 8 simprd ⊢ ( ( 𝐴 ∈ P ∧ 𝑦 ∈ 𝐴 ) → ∃ 𝑥 ∈ 𝐴 𝑦 <Q 𝑥 )
10 5 9 vtoclg ⊢ ( 𝐵 ∈ 𝐴 → ( ( 𝐴 ∈ P ∧ 𝐵 ∈ 𝐴 ) → ∃ 𝑥 ∈ 𝐴 𝐵 <Q 𝑥 ) )
11 10 anabsi7 ⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ 𝐴 ) → ∃ 𝑥 ∈ 𝐴 𝐵 <Q 𝑥 )