Metamath Proof Explorer

Theorem elovmporab

Description: Implications for the value of an operation, defined by the maps-to notation with a class abstraction as a result, having an element. (Contributed by Alexander van der Vekens, 15-Jul-2018)

Ref Expression
Hypotheses elovmporab.o ⊢O=x∈V,y∈V⟼z∈M|φ
elovmporab.v ⊢X∈V∧Y∈V→M∈V
Assertion elovmporab ⊢Z∈XOY→X∈V∧Y∈V∧Z∈M

Proof

Step Hyp Ref Expression
1 elovmporab.o ⊢O=x∈V,y∈V⟼z∈M|φ
2 elovmporab.v ⊢X∈V∧Y∈V→M∈V
3 1 elmpocl ⊢Z∈XOY→X∈V∧Y∈V
4 1 a1i ⊢X∈V∧Y∈V→O=x∈V,y∈V⟼z∈M|φ
5 sbceq1a ⊢y=Y→φ↔[˙Y/y]˙φ
6 sbceq1a ⊢x=X→[˙Y/y]˙φ↔[˙X/x]˙[˙Y/y]˙φ
7 5 6 sylan9bbr ⊢x=X∧y=Y→φ↔[˙X/x]˙[˙Y/y]˙φ
8 7 adantl ⊢X∈V∧Y∈V∧x=X∧y=Y→φ↔[˙X/x]˙[˙Y/y]˙φ
9 8 rabbidv ⊢X∈V∧Y∈V∧x=X∧y=Y→z∈M|φ=z∈M|[˙X/x]˙[˙Y/y]˙φ
10 eqidd ⊢X∈V∧Y∈V∧x=X→V=V
11 simpl ⊢X∈V∧Y∈V→X∈V
12 simpr ⊢X∈V∧Y∈V→Y∈V
13 rabexg ⊢M∈V→z∈M|[˙X/x]˙[˙Y/y]˙φ∈V
14 2 13 syl ⊢X∈V∧Y∈V→z∈M|[˙X/x]˙[˙Y/y]˙φ∈V
15 nfcv ⊢Ⅎ_xX
16 15 nfel1 ⊢ℲxX∈V
17 nfcv ⊢Ⅎ_xY
18 17 nfel1 ⊢ℲxY∈V
19 16 18 nfan ⊢ℲxX∈V∧Y∈V
20 nfcv ⊢Ⅎ_yX
21 20 nfel1 ⊢ℲyX∈V
22 nfcv ⊢Ⅎ_yY
23 22 nfel1 ⊢ℲyY∈V
24 21 23 nfan ⊢ℲyX∈V∧Y∈V
25 nfsbc1v ⊢Ⅎx[˙X/x]˙[˙Y/y]˙φ
26 nfcv ⊢Ⅎ_xM
27 25 26 nfrabw ⊢Ⅎ_xz∈M|[˙X/x]˙[˙Y/y]˙φ
28 nfsbc1v ⊢Ⅎy[˙Y/y]˙φ
29 20 28 nfsbcw ⊢Ⅎy[˙X/x]˙[˙Y/y]˙φ
30 nfcv ⊢Ⅎ_yM
31 29 30 nfrabw ⊢Ⅎ_yz∈M|[˙X/x]˙[˙Y/y]˙φ
32 4 9 10 11 12 14 19 24 20 17 27 31 ovmpodxf ⊢X∈V∧Y∈V→XOY=z∈M|[˙X/x]˙[˙Y/y]˙φ
33 32 eleq2d ⊢X∈V∧Y∈V→Z∈XOY↔Z∈z∈M|[˙X/x]˙[˙Y/y]˙φ
34 df-3an ⊢X∈V∧Y∈V∧Z∈M↔X∈V∧Y∈V∧Z∈M
35 34 simplbi2com ⊢Z∈M→X∈V∧Y∈V→X∈V∧Y∈V∧Z∈M
36 elrabi ⊢Z∈z∈M|[˙X/x]˙[˙Y/y]˙φ→Z∈M
37 35 36 syl11 ⊢X∈V∧Y∈V→Z∈z∈M|[˙X/x]˙[˙Y/y]˙φ→X∈V∧Y∈V∧Z∈M
38 33 37 sylbid ⊢X∈V∧Y∈V→Z∈XOY→X∈V∧Y∈V∧Z∈M
39 3 38 mpcom ⊢Z∈XOY→X∈V∧Y∈V∧Z∈M