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

Metamath Proof Explorer

Theorem genpss

Description: The result of an operation on positive reals is a subset of the positive fractions. (Contributed by NM, 18-Nov-1995) (Revised by Mario Carneiro, 12-Jun-2013) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 genp.1 ⊢ 𝐹 = ( 𝑤 ∈ P , 𝑣 ∈ P ↦ { 𝑥 ∣ ∃ 𝑦 ∈ 𝑤 ∃ 𝑧 ∈ 𝑣 𝑥 = ( 𝑦 𝐺 𝑧 ) } )
2 genp.2 ⊢ ( ( 𝑦 ∈ Q ∧ 𝑧 ∈ Q ) → ( 𝑦 𝐺 𝑧 ) ∈ Q )
3 1 2 genpelv ⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ( 𝑓 ∈ ( 𝐴 𝐹 𝐵 ) ↔ ∃ 𝑔 ∈ 𝐴 ∃ ℎ ∈ 𝐵 𝑓 = ( 𝑔 𝐺 ℎ ) ) )
4 elprnq ⊢ ( ( 𝐴 ∈ P ∧ 𝑔 ∈ 𝐴 ) → 𝑔 ∈ Q )
5 4 ex ⊢ ( 𝐴 ∈ P → ( 𝑔 ∈ 𝐴 → 𝑔 ∈ Q ) )
6 elprnq ⊢ ( ( 𝐵 ∈ P ∧ ℎ ∈ 𝐵 ) → ℎ ∈ Q )
7 6 ex ⊢ ( 𝐵 ∈ P → ( ℎ ∈ 𝐵 → ℎ ∈ Q ) )
8 5 7 im2anan9 ⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ( ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ) → ( 𝑔 ∈ Q ∧ ℎ ∈ Q ) ) )
9 2 caovcl ⊢ ( ( 𝑔 ∈ Q ∧ ℎ ∈ Q ) → ( 𝑔 𝐺 ℎ ) ∈ Q )
10 8 9 syl6 ⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ( ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ) → ( 𝑔 𝐺 ℎ ) ∈ Q ) )
11 eleq1a ⊢ ( ( 𝑔 𝐺 ℎ ) ∈ Q → ( 𝑓 = ( 𝑔 𝐺 ℎ ) → 𝑓 ∈ Q ) )
12 10 11 syl6 ⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ( ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ) → ( 𝑓 = ( 𝑔 𝐺 ℎ ) → 𝑓 ∈ Q ) ) )
13 12 rexlimdvv ⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ( ∃ 𝑔 ∈ 𝐴 ∃ ℎ ∈ 𝐵 𝑓 = ( 𝑔 𝐺 ℎ ) → 𝑓 ∈ Q ) )
14 3 13 sylbid ⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ( 𝑓 ∈ ( 𝐴 𝐹 𝐵 ) → 𝑓 ∈ Q ) )
15 14 ssrdv ⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ( 𝐴 𝐹 𝐵 ) ⊆ Q )