Metamath Proof Explorer


Theorem elovmporab1

Description: Implications for the value of an operation, defined by the maps-to notation with a class abstraction as a result, having an element. Here, the base set of the class abstraction depends on the first operand. Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker elovmporab1w when possible. (Contributed by Alexander van der Vekens, 15-Jul-2018) (New usage is discouraged.)

Ref Expression
Hypotheses elovmporab1.o O = x V , y V z x / m M | φ
elovmporab1.v X V Y V X / m M V
Assertion elovmporab1 Z X O Y X V Y V Z X / m M

Proof

Step Hyp Ref Expression
1 elovmporab1.o O = x V , y V z x / m M | φ
2 elovmporab1.v X V Y V X / m M V
3 1 elmpocl Z X O Y X V Y V
4 1 a1i X V Y V O = x V , y V z x / m M | φ
5 csbeq1 x = X x / m M = X / m M
6 5 ad2antrl X V Y V x = X y = Y x / m M = X / m M
7 sbceq1a y = Y φ [˙Y / y]˙ φ
8 sbceq1a x = X [˙Y / y]˙ φ [˙X / x]˙ [˙Y / y]˙ φ
9 7 8 sylan9bbr x = X y = Y φ [˙X / x]˙ [˙Y / y]˙ φ
10 9 adantl X V Y V x = X y = Y φ [˙X / x]˙ [˙Y / y]˙ φ
11 6 10 rabeqbidv X V Y V x = X y = Y z x / m M | φ = z X / m M | [˙X / x]˙ [˙Y / y]˙ φ
12 eqidd X V Y V x = X V = V
13 simpl X V Y V X V
14 simpr X V Y V Y V
15 rabexg X / m M V z X / m M | [˙X / x]˙ [˙Y / y]˙ φ V
16 2 15 syl X V Y V z X / m M | [˙X / x]˙ [˙Y / y]˙ φ V
17 nfcv _ x X
18 17 nfel1 x X V
19 nfcv _ x Y
20 19 nfel1 x Y V
21 18 20 nfan x X V Y V
22 nfcv _ y X
23 22 nfel1 y X V
24 nfcv _ y Y
25 24 nfel1 y Y V
26 23 25 nfan y X V Y V
27 nfsbc1v x [˙X / x]˙ [˙Y / y]˙ φ
28 nfcv _ x M
29 17 28 nfcsb _ x X / m M
30 27 29 nfrab _ x z X / m M | [˙X / x]˙ [˙Y / y]˙ φ
31 nfsbc1v y [˙Y / y]˙ φ
32 22 31 nfsbc y [˙X / x]˙ [˙Y / y]˙ φ
33 nfcv _ y M
34 22 33 nfcsb _ y X / m M
35 32 34 nfrab _ y z X / m M | [˙X / x]˙ [˙Y / y]˙ φ
36 4 11 12 13 14 16 21 26 22 19 30 35 ovmpodxf X V Y V X O Y = z X / m M | [˙X / x]˙ [˙Y / y]˙ φ
37 36 eleq2d X V Y V Z X O Y Z z X / m M | [˙X / x]˙ [˙Y / y]˙ φ
38 df-3an X V Y V Z X / m M X V Y V Z X / m M
39 38 simplbi2com Z X / m M X V Y V X V Y V Z X / m M
40 elrabi Z z X / m M | [˙X / x]˙ [˙Y / y]˙ φ Z X / m M
41 39 40 syl11 X V Y V Z z X / m M | [˙X / x]˙ [˙Y / y]˙ φ X V Y V Z X / m M
42 37 41 sylbid X V Y V Z X O Y X V Y V Z X / m M
43 3 42 mpcom Z X O Y X V Y V Z X / m M