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 ∈ v x = y G z
genp.2 ⊢ y ∈ 𝑸 ∧ z ∈ 𝑸 → y G z ∈ 𝑸
Assertion genpelv ⊢ A ∈ 𝑷 ∧ B ∈ 𝑷 → C ∈ A F B ↔ ∃ g ∈ A ∃ h ∈ B C = g G h

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 genpv ⊢ A ∈ 𝑷 ∧ B ∈ 𝑷 → A F B = f | ∃ g ∈ A ∃ h ∈ B f = g G h
4 3 eleq2d ⊢ A ∈ 𝑷 ∧ B ∈ 𝑷 → C ∈ A F B ↔ C ∈ f | ∃ g ∈ A ∃ h ∈ B f = g G h
5 id ⊢ C = g G h → C = g G h
6 ovex ⊢ g G h ∈ V
7 5 6 eqeltrdi ⊢ C = g G h → C ∈ V
8 7 rexlimivw ⊢ ∃ h ∈ B C = g G h → C ∈ V
9 8 rexlimivw ⊢ ∃ g ∈ A ∃ h ∈ B C = g G h → C ∈ V
10 eqeq1 ⊢ f = C → f = g G h ↔ C = g G h
11 10 2rexbidv ⊢ f = C → ∃ g ∈ A ∃ h ∈ B f = g G h ↔ ∃ g ∈ A ∃ h ∈ B C = g G h
12 9 11 elab3 ⊢ C ∈ f | ∃ g ∈ A ∃ h ∈ B f = g G h ↔ ∃ g ∈ A ∃ h ∈ B C = g G h
13 4 12 bitrdi ⊢ A ∈ 𝑷 ∧ B ∈ 𝑷 → C ∈ A F B ↔ ∃ g ∈ A ∃ h ∈ B C = g G h