Metamath Proof Explorer


Theorem genpv

Description: Value of general operation (addition or multiplication) on positive reals. (Contributed by NM, 10-Mar-1996) (Revised by Mario Carneiro, 17-Nov-2014) (New usage is discouraged.)

Ref Expression
Hypotheses genp.1 𝐹 = ( 𝑤P , 𝑣P ↦ { 𝑥 ∣ ∃ 𝑦𝑤𝑧𝑣 𝑥 = ( 𝑦 𝐺 𝑧 ) } )
genp.2 ( ( 𝑦Q𝑧Q ) → ( 𝑦 𝐺 𝑧 ) ∈ Q )
Assertion genpv ( ( 𝐴P𝐵P ) → ( 𝐴 𝐹 𝐵 ) = { 𝑓 ∣ ∃ 𝑔𝐴𝐵 𝑓 = ( 𝑔 𝐺 ) } )

Proof

Step Hyp Ref Expression
1 genp.1 𝐹 = ( 𝑤P , 𝑣P ↦ { 𝑥 ∣ ∃ 𝑦𝑤𝑧𝑣 𝑥 = ( 𝑦 𝐺 𝑧 ) } )
2 genp.2 ( ( 𝑦Q𝑧Q ) → ( 𝑦 𝐺 𝑧 ) ∈ Q )
3 oveq1 ( 𝑓 = 𝐴 → ( 𝑓 𝐹 𝑔 ) = ( 𝐴 𝐹 𝑔 ) )
4 rexeq ( 𝑓 = 𝐴 → ( ∃ 𝑦𝑓𝑧𝑔 𝑥 = ( 𝑦 𝐺 𝑧 ) ↔ ∃ 𝑦𝐴𝑧𝑔 𝑥 = ( 𝑦 𝐺 𝑧 ) ) )
5 4 abbidv ( 𝑓 = 𝐴 → { 𝑥 ∣ ∃ 𝑦𝑓𝑧𝑔 𝑥 = ( 𝑦 𝐺 𝑧 ) } = { 𝑥 ∣ ∃ 𝑦𝐴𝑧𝑔 𝑥 = ( 𝑦 𝐺 𝑧 ) } )
6 3 5 eqeq12d ( 𝑓 = 𝐴 → ( ( 𝑓 𝐹 𝑔 ) = { 𝑥 ∣ ∃ 𝑦𝑓𝑧𝑔 𝑥 = ( 𝑦 𝐺 𝑧 ) } ↔ ( 𝐴 𝐹 𝑔 ) = { 𝑥 ∣ ∃ 𝑦𝐴𝑧𝑔 𝑥 = ( 𝑦 𝐺 𝑧 ) } ) )
7 oveq2 ( 𝑔 = 𝐵 → ( 𝐴 𝐹 𝑔 ) = ( 𝐴 𝐹 𝐵 ) )
8 rexeq ( 𝑔 = 𝐵 → ( ∃ 𝑧𝑔 𝑥 = ( 𝑦 𝐺 𝑧 ) ↔ ∃ 𝑧𝐵 𝑥 = ( 𝑦 𝐺 𝑧 ) ) )
9 8 rexbidv ( 𝑔 = 𝐵 → ( ∃ 𝑦𝐴𝑧𝑔 𝑥 = ( 𝑦 𝐺 𝑧 ) ↔ ∃ 𝑦𝐴𝑧𝐵 𝑥 = ( 𝑦 𝐺 𝑧 ) ) )
10 9 abbidv ( 𝑔 = 𝐵 → { 𝑥 ∣ ∃ 𝑦𝐴𝑧𝑔 𝑥 = ( 𝑦 𝐺 𝑧 ) } = { 𝑥 ∣ ∃ 𝑦𝐴𝑧𝐵 𝑥 = ( 𝑦 𝐺 𝑧 ) } )
11 7 10 eqeq12d ( 𝑔 = 𝐵 → ( ( 𝐴 𝐹 𝑔 ) = { 𝑥 ∣ ∃ 𝑦𝐴𝑧𝑔 𝑥 = ( 𝑦 𝐺 𝑧 ) } ↔ ( 𝐴 𝐹 𝐵 ) = { 𝑥 ∣ ∃ 𝑦𝐴𝑧𝐵 𝑥 = ( 𝑦 𝐺 𝑧 ) } ) )
12 elprnq ( ( 𝑓P𝑦𝑓 ) → 𝑦Q )
13 elprnq ( ( 𝑔P𝑧𝑔 ) → 𝑧Q )
14 eleq1 ( 𝑥 = ( 𝑦 𝐺 𝑧 ) → ( 𝑥Q ↔ ( 𝑦 𝐺 𝑧 ) ∈ Q ) )
15 2 14 syl5ibrcom ( ( 𝑦Q𝑧Q ) → ( 𝑥 = ( 𝑦 𝐺 𝑧 ) → 𝑥Q ) )
16 12 13 15 syl2an ( ( ( 𝑓P𝑦𝑓 ) ∧ ( 𝑔P𝑧𝑔 ) ) → ( 𝑥 = ( 𝑦 𝐺 𝑧 ) → 𝑥Q ) )
17 16 an4s ( ( ( 𝑓P𝑔P ) ∧ ( 𝑦𝑓𝑧𝑔 ) ) → ( 𝑥 = ( 𝑦 𝐺 𝑧 ) → 𝑥Q ) )
18 17 rexlimdvva ( ( 𝑓P𝑔P ) → ( ∃ 𝑦𝑓𝑧𝑔 𝑥 = ( 𝑦 𝐺 𝑧 ) → 𝑥Q ) )
19 18 abssdv ( ( 𝑓P𝑔P ) → { 𝑥 ∣ ∃ 𝑦𝑓𝑧𝑔 𝑥 = ( 𝑦 𝐺 𝑧 ) } ⊆ Q )
20 nqex Q ∈ V
21 ssexg ( ( { 𝑥 ∣ ∃ 𝑦𝑓𝑧𝑔 𝑥 = ( 𝑦 𝐺 𝑧 ) } ⊆ QQ ∈ V ) → { 𝑥 ∣ ∃ 𝑦𝑓𝑧𝑔 𝑥 = ( 𝑦 𝐺 𝑧 ) } ∈ V )
22 19 20 21 sylancl ( ( 𝑓P𝑔P ) → { 𝑥 ∣ ∃ 𝑦𝑓𝑧𝑔 𝑥 = ( 𝑦 𝐺 𝑧 ) } ∈ V )
23 rexeq ( 𝑤 = 𝑓 → ( ∃ 𝑦𝑤𝑧𝑣 𝑥 = ( 𝑦 𝐺 𝑧 ) ↔ ∃ 𝑦𝑓𝑧𝑣 𝑥 = ( 𝑦 𝐺 𝑧 ) ) )
24 23 abbidv ( 𝑤 = 𝑓 → { 𝑥 ∣ ∃ 𝑦𝑤𝑧𝑣 𝑥 = ( 𝑦 𝐺 𝑧 ) } = { 𝑥 ∣ ∃ 𝑦𝑓𝑧𝑣 𝑥 = ( 𝑦 𝐺 𝑧 ) } )
25 rexeq ( 𝑣 = 𝑔 → ( ∃ 𝑧𝑣 𝑥 = ( 𝑦 𝐺 𝑧 ) ↔ ∃ 𝑧𝑔 𝑥 = ( 𝑦 𝐺 𝑧 ) ) )
26 25 rexbidv ( 𝑣 = 𝑔 → ( ∃ 𝑦𝑓𝑧𝑣 𝑥 = ( 𝑦 𝐺 𝑧 ) ↔ ∃ 𝑦𝑓𝑧𝑔 𝑥 = ( 𝑦 𝐺 𝑧 ) ) )
27 26 abbidv ( 𝑣 = 𝑔 → { 𝑥 ∣ ∃ 𝑦𝑓𝑧𝑣 𝑥 = ( 𝑦 𝐺 𝑧 ) } = { 𝑥 ∣ ∃ 𝑦𝑓𝑧𝑔 𝑥 = ( 𝑦 𝐺 𝑧 ) } )
28 24 27 1 ovmpog ( ( 𝑓P𝑔P ∧ { 𝑥 ∣ ∃ 𝑦𝑓𝑧𝑔 𝑥 = ( 𝑦 𝐺 𝑧 ) } ∈ V ) → ( 𝑓 𝐹 𝑔 ) = { 𝑥 ∣ ∃ 𝑦𝑓𝑧𝑔 𝑥 = ( 𝑦 𝐺 𝑧 ) } )
29 22 28 mpd3an3 ( ( 𝑓P𝑔P ) → ( 𝑓 𝐹 𝑔 ) = { 𝑥 ∣ ∃ 𝑦𝑓𝑧𝑔 𝑥 = ( 𝑦 𝐺 𝑧 ) } )
30 6 11 29 vtocl2ga ( ( 𝐴P𝐵P ) → ( 𝐴 𝐹 𝐵 ) = { 𝑥 ∣ ∃ 𝑦𝐴𝑧𝐵 𝑥 = ( 𝑦 𝐺 𝑧 ) } )
31 eqeq1 ( 𝑥 = 𝑓 → ( 𝑥 = ( 𝑦 𝐺 𝑧 ) ↔ 𝑓 = ( 𝑦 𝐺 𝑧 ) ) )
32 31 2rexbidv ( 𝑥 = 𝑓 → ( ∃ 𝑦𝐴𝑧𝐵 𝑥 = ( 𝑦 𝐺 𝑧 ) ↔ ∃ 𝑦𝐴𝑧𝐵 𝑓 = ( 𝑦 𝐺 𝑧 ) ) )
33 oveq1 ( 𝑦 = 𝑔 → ( 𝑦 𝐺 𝑧 ) = ( 𝑔 𝐺 𝑧 ) )
34 33 eqeq2d ( 𝑦 = 𝑔 → ( 𝑓 = ( 𝑦 𝐺 𝑧 ) ↔ 𝑓 = ( 𝑔 𝐺 𝑧 ) ) )
35 oveq2 ( 𝑧 = → ( 𝑔 𝐺 𝑧 ) = ( 𝑔 𝐺 ) )
36 35 eqeq2d ( 𝑧 = → ( 𝑓 = ( 𝑔 𝐺 𝑧 ) ↔ 𝑓 = ( 𝑔 𝐺 ) ) )
37 34 36 cbvrex2vw ( ∃ 𝑦𝐴𝑧𝐵 𝑓 = ( 𝑦 𝐺 𝑧 ) ↔ ∃ 𝑔𝐴𝐵 𝑓 = ( 𝑔 𝐺 ) )
38 32 37 bitrdi ( 𝑥 = 𝑓 → ( ∃ 𝑦𝐴𝑧𝐵 𝑥 = ( 𝑦 𝐺 𝑧 ) ↔ ∃ 𝑔𝐴𝐵 𝑓 = ( 𝑔 𝐺 ) ) )
39 38 cbvabv { 𝑥 ∣ ∃ 𝑦𝐴𝑧𝐵 𝑥 = ( 𝑦 𝐺 𝑧 ) } = { 𝑓 ∣ ∃ 𝑔𝐴𝐵 𝑓 = ( 𝑔 𝐺 ) }
40 30 39 eqtrdi ( ( 𝐴P𝐵P ) → ( 𝐴 𝐹 𝐵 ) = { 𝑓 ∣ ∃ 𝑔𝐴𝐵 𝑓 = ( 𝑔 𝐺 ) } )