Metamath Proof Explorer

Theorem genpelv

Description: Membership in value of general operation (addition or multiplication) on positive reals. (Contributed by NM, 13-Mar-1996) (Revised by Mario Carneiro, 12-Jun-2013) (New usage is discouraged.)

Ref Expression
Hypotheses genp.1 ⊢F=w∈𝑷,v∈𝑷⟼x|∃y∈w∃z∈vx=yGz
genp.2 ⊢y∈𝑸∧z∈𝑸→yGz∈𝑸
Assertion genpelv ⊢A∈𝑷∧B∈𝑷→C∈AFB↔∃g∈A∃h∈BC=gGh

Proof

Step Hyp Ref Expression
1 genp.1 ⊢F=w∈𝑷,v∈𝑷⟼x|∃y∈w∃z∈vx=yGz
2 genp.2 ⊢y∈𝑸∧z∈𝑸→yGz∈𝑸
3 1 2 genpv ⊢A∈𝑷∧B∈𝑷→AFB=f|∃g∈A∃h∈Bf=gGh
4 3 eleq2d ⊢A∈𝑷∧B∈𝑷→C∈AFB↔C∈f|∃g∈A∃h∈Bf=gGh
5 id ⊢C=gGh→C=gGh
6 ovex ⊢gGh∈V
7 5 6 eqeltrdi ⊢C=gGh→C∈V
8 7 rexlimivw ⊢∃h∈BC=gGh→C∈V
9 8 rexlimivw ⊢∃g∈A∃h∈BC=gGh→C∈V
10 eqeq1 ⊢f=C→f=gGh↔C=gGh
11 10 2rexbidv ⊢f=C→∃g∈A∃h∈Bf=gGh↔∃g∈A∃h∈BC=gGh
12 9 11 elab3 ⊢C∈f|∃g∈A∃h∈Bf=gGh↔∃g∈A∃h∈BC=gGh
13 4 12 bitrdi ⊢A∈𝑷∧B∈𝑷→C∈AFB↔∃g∈A∃h∈BC=gGh