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 𝑥 )