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

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 ⊢ 𝐹 = ( 𝑤 ∈ P , 𝑣 ∈ P ↦ { 𝑥 ∣ ∃ 𝑦 ∈ 𝑤 ∃ 𝑧 ∈ 𝑣 𝑥 = ( 𝑦 𝐺 𝑧 ) } )
genp.2 ⊢ ( ( 𝑦 ∈ Q ∧ 𝑧 ∈ Q ) → ( 𝑦 𝐺 𝑧 ) ∈ Q )
Assertion genpelv ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ( 𝐶 ∈ ( 𝐴 𝐹 𝐵 ) ↔ ∃ 𝑔 ∈ 𝐴 ∃ ℎ ∈ 𝐵 𝐶 = ( 𝑔 𝐺 ℎ ) ) )

Proof

Step Hyp Ref Expression
1 genp.1 ⊢ 𝐹 = ( 𝑤 ∈ P , 𝑣 ∈ P ↦ { 𝑥 ∣ ∃ 𝑦 ∈ 𝑤 ∃ 𝑧 ∈ 𝑣 𝑥 = ( 𝑦 𝐺 𝑧 ) } )
2 genp.2 ⊢ ( ( 𝑦 ∈ Q ∧ 𝑧 ∈ Q ) → ( 𝑦 𝐺 𝑧 ) ∈ Q )
3 1 2 genpv ⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ( 𝐴 𝐹 𝐵 ) = { 𝑓 ∣ ∃ 𝑔 ∈ 𝐴 ∃ ℎ ∈ 𝐵 𝑓 = ( 𝑔 𝐺 ℎ ) } )
4 3 eleq2d ⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ( 𝐶 ∈ ( 𝐴 𝐹 𝐵 ) ↔ 𝐶 ∈ { 𝑓 ∣ ∃ 𝑔 ∈ 𝐴 ∃ ℎ ∈ 𝐵 𝑓 = ( 𝑔 𝐺 ℎ ) } ) )
5 id ⊢ ( 𝐶 = ( 𝑔 𝐺 ℎ ) → 𝐶 = ( 𝑔 𝐺 ℎ ) )
6 ovex ⊢ ( 𝑔 𝐺 ℎ ) ∈ V
7 5 6 eqeltrdi ⊢ ( 𝐶 = ( 𝑔 𝐺 ℎ ) → 𝐶 ∈ V )
8 7 rexlimivw ⊢ ( ∃ ℎ ∈ 𝐵 𝐶 = ( 𝑔 𝐺 ℎ ) → 𝐶 ∈ V )
9 8 rexlimivw ⊢ ( ∃ 𝑔 ∈ 𝐴 ∃ ℎ ∈ 𝐵 𝐶 = ( 𝑔 𝐺 ℎ ) → 𝐶 ∈ V )
10 eqeq1 ⊢ ( 𝑓 = 𝐶 → ( 𝑓 = ( 𝑔 𝐺 ℎ ) ↔ 𝐶 = ( 𝑔 𝐺 ℎ ) ) )
11 10 2rexbidv ⊢ ( 𝑓 = 𝐶 → ( ∃ 𝑔 ∈ 𝐴 ∃ ℎ ∈ 𝐵 𝑓 = ( 𝑔 𝐺 ℎ ) ↔ ∃ 𝑔 ∈ 𝐴 ∃ ℎ ∈ 𝐵 𝐶 = ( 𝑔 𝐺 ℎ ) ) )
12 9 11 elab3 ⊢ ( 𝐶 ∈ { 𝑓 ∣ ∃ 𝑔 ∈ 𝐴 ∃ ℎ ∈ 𝐵 𝑓 = ( 𝑔 𝐺 ℎ ) } ↔ ∃ 𝑔 ∈ 𝐴 ∃ ℎ ∈ 𝐵 𝐶 = ( 𝑔 𝐺 ℎ ) )
13 4 12 bitrdi ⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ( 𝐶 ∈ ( 𝐴 𝐹 𝐵 ) ↔ ∃ 𝑔 ∈ 𝐴 ∃ ℎ ∈ 𝐵 𝐶 = ( 𝑔 𝐺 ℎ ) ) )