Metamath Proof Explorer


Theorem genpprecl

Description: Pre-closure law for general operation on positive reals. (Contributed by NM, 10-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 genpprecl ( ( 𝐴P𝐵P ) → ( ( 𝐶𝐴𝐷𝐵 ) → ( 𝐶 𝐺 𝐷 ) ∈ ( 𝐴 𝐹 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 genp.1 𝐹 = ( 𝑤P , 𝑣P ↦ { 𝑥 ∣ ∃ 𝑦𝑤𝑧𝑣 𝑥 = ( 𝑦 𝐺 𝑧 ) } )
2 genp.2 ( ( 𝑦Q𝑧Q ) → ( 𝑦 𝐺 𝑧 ) ∈ Q )
3 eqid ( 𝐶 𝐺 𝐷 ) = ( 𝐶 𝐺 𝐷 )
4 rspceov ( ( 𝐶𝐴𝐷𝐵 ∧ ( 𝐶 𝐺 𝐷 ) = ( 𝐶 𝐺 𝐷 ) ) → ∃ 𝑔𝐴𝐵 ( 𝐶 𝐺 𝐷 ) = ( 𝑔 𝐺 ) )
5 3 4 mp3an3 ( ( 𝐶𝐴𝐷𝐵 ) → ∃ 𝑔𝐴𝐵 ( 𝐶 𝐺 𝐷 ) = ( 𝑔 𝐺 ) )
6 1 2 genpelv ( ( 𝐴P𝐵P ) → ( ( 𝐶 𝐺 𝐷 ) ∈ ( 𝐴 𝐹 𝐵 ) ↔ ∃ 𝑔𝐴𝐵 ( 𝐶 𝐺 𝐷 ) = ( 𝑔 𝐺 ) ) )
7 5 6 syl5ibr ( ( 𝐴P𝐵P ) → ( ( 𝐶𝐴𝐷𝐵 ) → ( 𝐶 𝐺 𝐷 ) ∈ ( 𝐴 𝐹 𝐵 ) ) )