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 ⊢ F = w ∈ 𝑷 , v ∈ 𝑷 ⟼ x | ∃ y ∈ w ∃ z ∈ v x = y G z
genp.2 ⊢ y ∈ 𝑸 ∧ z ∈ 𝑸 → y G z ∈ 𝑸
Assertion genpss ⊢ A ∈ 𝑷 ∧ B ∈ 𝑷 → A F B ⊆ 𝑸

Proof

Step Hyp Ref Expression
1 genp.1 ⊢ F = w ∈ 𝑷 , v ∈ 𝑷 ⟼ x | ∃ y ∈ w ∃ z ∈ v x = y G z
2 genp.2 ⊢ y ∈ 𝑸 ∧ z ∈ 𝑸 → y G z ∈ 𝑸
3 1 2 genpelv ⊢ A ∈ 𝑷 ∧ B ∈ 𝑷 → f ∈ A F B ↔ ∃ g ∈ A ∃ h ∈ B f = g G h
4 elprnq ⊢ A ∈ 𝑷 ∧ g ∈ A → g ∈ 𝑸
5 4 ex ⊢ A ∈ 𝑷 → g ∈ A → g ∈ 𝑸
6 elprnq ⊢ B ∈ 𝑷 ∧ h ∈ B → h ∈ 𝑸
7 6 ex ⊢ B ∈ 𝑷 → h ∈ B → h ∈ 𝑸
8 5 7 im2anan9 ⊢ A ∈ 𝑷 ∧ B ∈ 𝑷 → g ∈ A ∧ h ∈ B → g ∈ 𝑸 ∧ h ∈ 𝑸
9 2 caovcl ⊢ g ∈ 𝑸 ∧ h ∈ 𝑸 → g G h ∈ 𝑸
10 8 9 syl6 ⊢ A ∈ 𝑷 ∧ B ∈ 𝑷 → g ∈ A ∧ h ∈ B → g G h ∈ 𝑸
11 eleq1a ⊢ g G h ∈ 𝑸 → f = g G h → f ∈ 𝑸
12 10 11 syl6 ⊢ A ∈ 𝑷 ∧ B ∈ 𝑷 → g ∈ A ∧ h ∈ B → f = g G h → f ∈ 𝑸
13 12 rexlimdvv ⊢ A ∈ 𝑷 ∧ B ∈ 𝑷 → ∃ g ∈ A ∃ h ∈ B f = g G h → f ∈ 𝑸
14 3 13 sylbid ⊢ A ∈ 𝑷 ∧ B ∈ 𝑷 → f ∈ A F B → f ∈ 𝑸
15 14 ssrdv ⊢ A ∈ 𝑷 ∧ B ∈ 𝑷 → A F B ⊆ 𝑸