MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ovmpt3rab1 Structured version   Unicode version

Theorem ovmpt3rab1 6515
Description: The value of an operation defined by the maps-to notation with a function into a class abstraction as a result. The domain of the function and the base set of the class abstraction may depend on the operands, using implicit substitution. (Contributed by AV, 16-Jul-2018.) (Revised by AV, 16-May-2019.)
Hypotheses
Ref Expression
ovmpt3rab1.o  |-  O  =  ( x  e.  _V ,  y  e.  _V  |->  ( z  e.  M  |->  { a  e.  N  |  ph } ) )
ovmpt3rab1.m  |-  ( ( x  =  X  /\  y  =  Y )  ->  M  =  K )
ovmpt3rab1.n  |-  ( ( x  =  X  /\  y  =  Y )  ->  N  =  L )
ovmpt3rab1.p  |-  ( ( x  =  X  /\  y  =  Y )  ->  ( ph  <->  ps )
)
ovmpt3rab1.x  |-  F/ x ps
ovmpt3rab1.y  |-  F/ y ps
Assertion
Ref Expression
ovmpt3rab1  |-  ( ( X  e.  V  /\  Y  e.  W  /\  K  e.  U )  ->  ( X O Y )  =  ( z  e.  K  |->  { a  e.  L  |  ps } ) )
Distinct variable groups:    x, K, y, z    L, a, x, y    N, a    x, V, y    x, W, y   
x, U, y    X, a, x, y, z    Y, a, x, y, z
Allowed substitution hints:    ph( x, y, z, a)    ps( x, y, z, a)    U( z, a)    K( a)    L( z)    M( x, y, z, a)    N( x, y, z)    O( x, y, z, a)    V( z, a)    W( z, a)

Proof of Theorem ovmpt3rab1
StepHypRef Expression
1 ovmpt3rab1.o . . 3  |-  O  =  ( x  e.  _V ,  y  e.  _V  |->  ( z  e.  M  |->  { a  e.  N  |  ph } ) )
21a1i 11 . 2  |-  ( ( X  e.  V  /\  Y  e.  W  /\  K  e.  U )  ->  O  =  ( x  e.  _V ,  y  e.  _V  |->  ( z  e.  M  |->  { a  e.  N  |  ph } ) ) )
3 ovmpt3rab1.m . . . 4  |-  ( ( x  =  X  /\  y  =  Y )  ->  M  =  K )
4 ovmpt3rab1.n . . . . 5  |-  ( ( x  =  X  /\  y  =  Y )  ->  N  =  L )
5 ovmpt3rab1.p . . . . 5  |-  ( ( x  =  X  /\  y  =  Y )  ->  ( ph  <->  ps )
)
64, 5rabeqbidv 3088 . . . 4  |-  ( ( x  =  X  /\  y  =  Y )  ->  { a  e.  N  |  ph }  =  {
a  e.  L  |  ps } )
73, 6mpteq12dv 4511 . . 3  |-  ( ( x  =  X  /\  y  =  Y )  ->  ( z  e.  M  |->  { a  e.  N  |  ph } )  =  ( z  e.  K  |->  { a  e.  L  |  ps } ) )
87adantl 466 . 2  |-  ( ( ( X  e.  V  /\  Y  e.  W  /\  K  e.  U
)  /\  ( x  =  X  /\  y  =  Y ) )  -> 
( z  e.  M  |->  { a  e.  N  |  ph } )  =  ( z  e.  K  |->  { a  e.  L  |  ps } ) )
9 eqidd 2442 . 2  |-  ( ( ( X  e.  V  /\  Y  e.  W  /\  K  e.  U
)  /\  x  =  X )  ->  _V  =  _V )
10 elex 3102 . . 3  |-  ( X  e.  V  ->  X  e.  _V )
11103ad2ant1 1016 . 2  |-  ( ( X  e.  V  /\  Y  e.  W  /\  K  e.  U )  ->  X  e.  _V )
12 elex 3102 . . 3  |-  ( Y  e.  W  ->  Y  e.  _V )
13123ad2ant2 1017 . 2  |-  ( ( X  e.  V  /\  Y  e.  W  /\  K  e.  U )  ->  Y  e.  _V )
14 mptexg 6123 . . 3  |-  ( K  e.  U  ->  (
z  e.  K  |->  { a  e.  L  |  ps } )  e.  _V )
15143ad2ant3 1018 . 2  |-  ( ( X  e.  V  /\  Y  e.  W  /\  K  e.  U )  ->  ( z  e.  K  |->  { a  e.  L  |  ps } )  e. 
_V )
16 nfv 1692 . 2  |-  F/ x
( X  e.  V  /\  Y  e.  W  /\  K  e.  U
)
17 nfv 1692 . 2  |-  F/ y ( X  e.  V  /\  Y  e.  W  /\  K  e.  U
)
18 nfcv 2603 . 2  |-  F/_ y X
19 nfcv 2603 . 2  |-  F/_ x Y
20 nfcv 2603 . . 3  |-  F/_ x K
21 ovmpt3rab1.x . . . 4  |-  F/ x ps
22 nfcv 2603 . . . 4  |-  F/_ x L
2321, 22nfrab 3023 . . 3  |-  F/_ x { a  e.  L  |  ps }
2420, 23nfmpt 4521 . 2  |-  F/_ x
( z  e.  K  |->  { a  e.  L  |  ps } )
25 nfcv 2603 . . 3  |-  F/_ y K
26 ovmpt3rab1.y . . . 4  |-  F/ y ps
27 nfcv 2603 . . . 4  |-  F/_ y L
2826, 27nfrab 3023 . . 3  |-  F/_ y { a  e.  L  |  ps }
2925, 28nfmpt 4521 . 2  |-  F/_ y
( z  e.  K  |->  { a  e.  L  |  ps } )
302, 8, 9, 11, 13, 15, 16, 17, 18, 19, 24, 29ovmpt2dxf 6409 1  |-  ( ( X  e.  V  /\  Y  e.  W  /\  K  e.  U )  ->  ( X O Y )  =  ( z  e.  K  |->  { a  e.  L  |  ps } ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    /\ w3a 972    = wceq 1381   F/wnf 1601    e. wcel 1802   {crab 2795   _Vcvv 3093    |-> cmpt 4491  (class class class)co 6277    |-> cmpt2 6279
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-9 1806  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419  ax-rep 4544  ax-sep 4554  ax-nul 4562  ax-pr 4672
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 974  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-eu 2270  df-mo 2271  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-ne 2638  df-ral 2796  df-rex 2797  df-reu 2798  df-rab 2800  df-v 3095  df-sbc 3312  df-csb 3418  df-dif 3461  df-un 3463  df-in 3465  df-ss 3472  df-nul 3768  df-if 3923  df-sn 4011  df-pr 4013  df-op 4017  df-uni 4231  df-iun 4313  df-br 4434  df-opab 4492  df-mpt 4493  df-id 4781  df-xp 4991  df-rel 4992  df-cnv 4993  df-co 4994  df-dm 4995  df-rn 4996  df-res 4997  df-ima 4998  df-iota 5537  df-fun 5576  df-fn 5577  df-f 5578  df-f1 5579  df-fo 5580  df-f1o 5581  df-fv 5582  df-ov 6280  df-oprab 6281  df-mpt2 6282
This theorem is referenced by:  ovmpt3rabdm  6516  elovmpt3rab1  6517
  Copyright terms: Public domain W3C validator