Metamath Proof Explorer

Theorem genpnmax

Description: An operation on positive reals has no largest member. (Contributed by NM, 10-Mar-1996) (Revised by Mario Carneiro, 12-Jun-2013) (New usage is discouraged.)

Ref Expression
Hypotheses genp.1 ⊢ 𝐹 = ( 𝑤 ∈ P , 𝑣 ∈ P ↦ { 𝑥 ∣ ∃ 𝑦 ∈ 𝑤 ∃ 𝑧 ∈ 𝑣 𝑥 = ( 𝑦 𝐺 𝑧 ) } )
genp.2 ⊢ ( ( 𝑦 ∈ Q ∧ 𝑧 ∈ Q ) → ( 𝑦 𝐺 𝑧 ) ∈ Q )
genpnmax.2 ⊢ ( 𝑣 ∈ Q → ( 𝑧 <Q 𝑤 ↔ ( 𝑣 𝐺 𝑧 ) <Q ( 𝑣 𝐺 𝑤 ) ) )
genpnmax.3 ⊢ ( 𝑧 𝐺 𝑤 ) = ( 𝑤 𝐺 𝑧 )
Assertion genpnmax ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ( 𝑓 ∈ ( 𝐴 𝐹 𝐵 ) → ∃ 𝑥 ∈ ( 𝐴 𝐹 𝐵 ) 𝑓 <Q 𝑥 ) )

Proof

Step Hyp Ref Expression
1 genp.1 ⊢ 𝐹 = ( 𝑤 ∈ P , 𝑣 ∈ P ↦ { 𝑥 ∣ ∃ 𝑦 ∈ 𝑤 ∃ 𝑧 ∈ 𝑣 𝑥 = ( 𝑦 𝐺 𝑧 ) } )
2 genp.2 ⊢ ( ( 𝑦 ∈ Q ∧ 𝑧 ∈ Q ) → ( 𝑦 𝐺 𝑧 ) ∈ Q )
3 genpnmax.2 ⊢ ( 𝑣 ∈ Q → ( 𝑧 <Q 𝑤 ↔ ( 𝑣 𝐺 𝑧 ) <Q ( 𝑣 𝐺 𝑤 ) ) )
4 genpnmax.3 ⊢ ( 𝑧 𝐺 𝑤 ) = ( 𝑤 𝐺 𝑧 )
5 1 2 genpelv ⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ( 𝑓 ∈ ( 𝐴 𝐹 𝐵 ) ↔ ∃ 𝑔 ∈ 𝐴 ∃ ℎ ∈ 𝐵 𝑓 = ( 𝑔 𝐺 ℎ ) ) )
6 prnmax ⊢ ( ( 𝐴 ∈ P ∧ 𝑔 ∈ 𝐴 ) → ∃ 𝑦 ∈ 𝐴 𝑔 <Q 𝑦 )
7 6 adantr ⊢ ( ( ( 𝐴 ∈ P ∧ 𝑔 ∈ 𝐴 ) ∧ ( 𝐵 ∈ P ∧ ℎ ∈ 𝐵 ) ) → ∃ 𝑦 ∈ 𝐴 𝑔 <Q 𝑦 )
8 1 2 genpprecl ⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ( ( 𝑦 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ) → ( 𝑦 𝐺 ℎ ) ∈ ( 𝐴 𝐹 𝐵 ) ) )
9 8 exp4b ⊢ ( 𝐴 ∈ P → ( 𝐵 ∈ P → ( 𝑦 ∈ 𝐴 → ( ℎ ∈ 𝐵 → ( 𝑦 𝐺 ℎ ) ∈ ( 𝐴 𝐹 𝐵 ) ) ) ) )
10 9 com34 ⊢ ( 𝐴 ∈ P → ( 𝐵 ∈ P → ( ℎ ∈ 𝐵 → ( 𝑦 ∈ 𝐴 → ( 𝑦 𝐺 ℎ ) ∈ ( 𝐴 𝐹 𝐵 ) ) ) ) )
11 10 imp32 ⊢ ( ( 𝐴 ∈ P ∧ ( 𝐵 ∈ P ∧ ℎ ∈ 𝐵 ) ) → ( 𝑦 ∈ 𝐴 → ( 𝑦 𝐺 ℎ ) ∈ ( 𝐴 𝐹 𝐵 ) ) )
12 elprnq ⊢ ( ( 𝐵 ∈ P ∧ ℎ ∈ 𝐵 ) → ℎ ∈ Q )
13 vex ⊢ 𝑔 ∈ V
14 vex ⊢ 𝑦 ∈ V
15 vex ⊢ ℎ ∈ V
16 13 14 3 15 4 caovord2 ⊢ ( ℎ ∈ Q → ( 𝑔 <Q 𝑦 ↔ ( 𝑔 𝐺 ℎ ) <Q ( 𝑦 𝐺 ℎ ) ) )
17 16 biimpd ⊢ ( ℎ ∈ Q → ( 𝑔 <Q 𝑦 → ( 𝑔 𝐺 ℎ ) <Q ( 𝑦 𝐺 ℎ ) ) )
18 12 17 syl ⊢ ( ( 𝐵 ∈ P ∧ ℎ ∈ 𝐵 ) → ( 𝑔 <Q 𝑦 → ( 𝑔 𝐺 ℎ ) <Q ( 𝑦 𝐺 ℎ ) ) )
19 18 adantl ⊢ ( ( 𝐴 ∈ P ∧ ( 𝐵 ∈ P ∧ ℎ ∈ 𝐵 ) ) → ( 𝑔 <Q 𝑦 → ( 𝑔 𝐺 ℎ ) <Q ( 𝑦 𝐺 ℎ ) ) )
20 11 19 anim12d ⊢ ( ( 𝐴 ∈ P ∧ ( 𝐵 ∈ P ∧ ℎ ∈ 𝐵 ) ) → ( ( 𝑦 ∈ 𝐴 ∧ 𝑔 <Q 𝑦 ) → ( ( 𝑦 𝐺 ℎ ) ∈ ( 𝐴 𝐹 𝐵 ) ∧ ( 𝑔 𝐺 ℎ ) <Q ( 𝑦 𝐺 ℎ ) ) ) )
21 breq2 ⊢ ( 𝑥 = ( 𝑦 𝐺 ℎ ) → ( ( 𝑔 𝐺 ℎ ) <Q 𝑥 ↔ ( 𝑔 𝐺 ℎ ) <Q ( 𝑦 𝐺 ℎ ) ) )
22 21 rspcev ⊢ ( ( ( 𝑦 𝐺 ℎ ) ∈ ( 𝐴 𝐹 𝐵 ) ∧ ( 𝑔 𝐺 ℎ ) <Q ( 𝑦 𝐺 ℎ ) ) → ∃ 𝑥 ∈ ( 𝐴 𝐹 𝐵 ) ( 𝑔 𝐺 ℎ ) <Q 𝑥 )
23 20 22 syl6 ⊢ ( ( 𝐴 ∈ P ∧ ( 𝐵 ∈ P ∧ ℎ ∈ 𝐵 ) ) → ( ( 𝑦 ∈ 𝐴 ∧ 𝑔 <Q 𝑦 ) → ∃ 𝑥 ∈ ( 𝐴 𝐹 𝐵 ) ( 𝑔 𝐺 ℎ ) <Q 𝑥 ) )
24 23 adantlr ⊢ ( ( ( 𝐴 ∈ P ∧ 𝑔 ∈ 𝐴 ) ∧ ( 𝐵 ∈ P ∧ ℎ ∈ 𝐵 ) ) → ( ( 𝑦 ∈ 𝐴 ∧ 𝑔 <Q 𝑦 ) → ∃ 𝑥 ∈ ( 𝐴 𝐹 𝐵 ) ( 𝑔 𝐺 ℎ ) <Q 𝑥 ) )
25 24 expd ⊢ ( ( ( 𝐴 ∈ P ∧ 𝑔 ∈ 𝐴 ) ∧ ( 𝐵 ∈ P ∧ ℎ ∈ 𝐵 ) ) → ( 𝑦 ∈ 𝐴 → ( 𝑔 <Q 𝑦 → ∃ 𝑥 ∈ ( 𝐴 𝐹 𝐵 ) ( 𝑔 𝐺 ℎ ) <Q 𝑥 ) ) )
26 25 rexlimdv ⊢ ( ( ( 𝐴 ∈ P ∧ 𝑔 ∈ 𝐴 ) ∧ ( 𝐵 ∈ P ∧ ℎ ∈ 𝐵 ) ) → ( ∃ 𝑦 ∈ 𝐴 𝑔 <Q 𝑦 → ∃ 𝑥 ∈ ( 𝐴 𝐹 𝐵 ) ( 𝑔 𝐺 ℎ ) <Q 𝑥 ) )
27 7 26 mpd ⊢ ( ( ( 𝐴 ∈ P ∧ 𝑔 ∈ 𝐴 ) ∧ ( 𝐵 ∈ P ∧ ℎ ∈ 𝐵 ) ) → ∃ 𝑥 ∈ ( 𝐴 𝐹 𝐵 ) ( 𝑔 𝐺 ℎ ) <Q 𝑥 )
28 27 an4s ⊢ ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ) ) → ∃ 𝑥 ∈ ( 𝐴 𝐹 𝐵 ) ( 𝑔 𝐺 ℎ ) <Q 𝑥 )
29 breq1 ⊢ ( 𝑓 = ( 𝑔 𝐺 ℎ ) → ( 𝑓 <Q 𝑥 ↔ ( 𝑔 𝐺 ℎ ) <Q 𝑥 ) )
30 29 rexbidv ⊢ ( 𝑓 = ( 𝑔 𝐺 ℎ ) → ( ∃ 𝑥 ∈ ( 𝐴 𝐹 𝐵 ) 𝑓 <Q 𝑥 ↔ ∃ 𝑥 ∈ ( 𝐴 𝐹 𝐵 ) ( 𝑔 𝐺 ℎ ) <Q 𝑥 ) )
31 28 30 imbitrrid ⊢ ( 𝑓 = ( 𝑔 𝐺 ℎ ) → ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ) ) → ∃ 𝑥 ∈ ( 𝐴 𝐹 𝐵 ) 𝑓 <Q 𝑥 ) )
32 31 expdcom ⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ( ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ) → ( 𝑓 = ( 𝑔 𝐺 ℎ ) → ∃ 𝑥 ∈ ( 𝐴 𝐹 𝐵 ) 𝑓 <Q 𝑥 ) ) )
33 32 rexlimdvv ⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ( ∃ 𝑔 ∈ 𝐴 ∃ ℎ ∈ 𝐵 𝑓 = ( 𝑔 𝐺 ℎ ) → ∃ 𝑥 ∈ ( 𝐴 𝐹 𝐵 ) 𝑓 <Q 𝑥 ) )
34 5 33 sylbid ⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ( 𝑓 ∈ ( 𝐴 𝐹 𝐵 ) → ∃ 𝑥 ∈ ( 𝐴 𝐹 𝐵 ) 𝑓 <Q 𝑥 ) )