ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ovmpos Unicode version

Theorem ovmpos 5946
Description: Value of a function given by the maps-to notation, expressed using explicit substitution. (Contributed by Mario Carneiro, 30-Apr-2015.)
Hypothesis
Ref Expression
ovmpos.3  |-  F  =  ( x  e.  C ,  y  e.  D  |->  R )
Assertion
Ref Expression
ovmpos  |-  ( ( A  e.  C  /\  B  e.  D  /\  [_ A  /  x ]_ [_ B  /  y ]_ R  e.  V )  ->  ( A F B )  =  [_ A  /  x ]_ [_ B  /  y ]_ R
)
Distinct variable groups:    x, y, A   
x, B, y    x, C, y    x, D, y
Allowed substitution hints:    R( x, y)    F( x, y)    V( x, y)

Proof of Theorem ovmpos
StepHypRef Expression
1 elex 2723 . . 3  |-  ( [_ A  /  x ]_ [_ B  /  y ]_ R  e.  V  ->  [_ A  /  x ]_ [_ B  /  y ]_ R  e.  _V )
2 nfcv 2299 . . . . 5  |-  F/_ x A
3 nfcv 2299 . . . . 5  |-  F/_ y A
4 nfcv 2299 . . . . 5  |-  F/_ y B
5 nfcsb1v 3064 . . . . . . 7  |-  F/_ x [_ A  /  x ]_ R
65nfel1 2310 . . . . . 6  |-  F/ x [_ A  /  x ]_ R  e.  _V
7 ovmpos.3 . . . . . . . . 9  |-  F  =  ( x  e.  C ,  y  e.  D  |->  R )
8 nfmpo1 5890 . . . . . . . . 9  |-  F/_ x
( x  e.  C ,  y  e.  D  |->  R )
97, 8nfcxfr 2296 . . . . . . . 8  |-  F/_ x F
10 nfcv 2299 . . . . . . . 8  |-  F/_ x
y
112, 9, 10nfov 5853 . . . . . . 7  |-  F/_ x
( A F y )
1211, 5nfeq 2307 . . . . . 6  |-  F/ x
( A F y )  =  [_ A  /  x ]_ R
136, 12nfim 1552 . . . . 5  |-  F/ x
( [_ A  /  x ]_ R  e.  _V  ->  ( A F y )  =  [_ A  /  x ]_ R )
14 nfcsb1v 3064 . . . . . . 7  |-  F/_ y [_ B  /  y ]_ [_ A  /  x ]_ R
1514nfel1 2310 . . . . . 6  |-  F/ y
[_ B  /  y ]_ [_ A  /  x ]_ R  e.  _V
16 nfmpo2 5891 . . . . . . . . 9  |-  F/_ y
( x  e.  C ,  y  e.  D  |->  R )
177, 16nfcxfr 2296 . . . . . . . 8  |-  F/_ y F
183, 17, 4nfov 5853 . . . . . . 7  |-  F/_ y
( A F B )
1918, 14nfeq 2307 . . . . . 6  |-  F/ y ( A F B )  =  [_ B  /  y ]_ [_ A  /  x ]_ R
2015, 19nfim 1552 . . . . 5  |-  F/ y ( [_ B  / 
y ]_ [_ A  /  x ]_ R  e.  _V  ->  ( A F B )  =  [_ B  /  y ]_ [_ A  /  x ]_ R )
21 csbeq1a 3040 . . . . . . 7  |-  ( x  =  A  ->  R  =  [_ A  /  x ]_ R )
2221eleq1d 2226 . . . . . 6  |-  ( x  =  A  ->  ( R  e.  _V  <->  [_ A  /  x ]_ R  e.  _V ) )
23 oveq1 5833 . . . . . . 7  |-  ( x  =  A  ->  (
x F y )  =  ( A F y ) )
2423, 21eqeq12d 2172 . . . . . 6  |-  ( x  =  A  ->  (
( x F y )  =  R  <->  ( A F y )  = 
[_ A  /  x ]_ R ) )
2522, 24imbi12d 233 . . . . 5  |-  ( x  =  A  ->  (
( R  e.  _V  ->  ( x F y )  =  R )  <-> 
( [_ A  /  x ]_ R  e.  _V  ->  ( A F y )  =  [_ A  /  x ]_ R ) ) )
26 csbeq1a 3040 . . . . . . 7  |-  ( y  =  B  ->  [_ A  /  x ]_ R  = 
[_ B  /  y ]_ [_ A  /  x ]_ R )
2726eleq1d 2226 . . . . . 6  |-  ( y  =  B  ->  ( [_ A  /  x ]_ R  e.  _V  <->  [_ B  /  y ]_ [_ A  /  x ]_ R  e.  _V )
)
28 oveq2 5834 . . . . . . 7  |-  ( y  =  B  ->  ( A F y )  =  ( A F B ) )
2928, 26eqeq12d 2172 . . . . . 6  |-  ( y  =  B  ->  (
( A F y )  =  [_ A  /  x ]_ R  <->  ( A F B )  =  [_ B  /  y ]_ [_ A  /  x ]_ R ) )
3027, 29imbi12d 233 . . . . 5  |-  ( y  =  B  ->  (
( [_ A  /  x ]_ R  e.  _V  ->  ( A F y )  =  [_ A  /  x ]_ R )  <-> 
( [_ B  /  y ]_ [_ A  /  x ]_ R  e.  _V  ->  ( A F B )  =  [_ B  /  y ]_ [_ A  /  x ]_ R ) ) )
317ovmpt4g 5945 . . . . . 6  |-  ( ( x  e.  C  /\  y  e.  D  /\  R  e.  _V )  ->  ( x F y )  =  R )
32313expia 1187 . . . . 5  |-  ( ( x  e.  C  /\  y  e.  D )  ->  ( R  e.  _V  ->  ( x F y )  =  R ) )
332, 3, 4, 13, 20, 25, 30, 32vtocl2gaf 2779 . . . 4  |-  ( ( A  e.  C  /\  B  e.  D )  ->  ( [_ B  / 
y ]_ [_ A  /  x ]_ R  e.  _V  ->  ( A F B )  =  [_ B  /  y ]_ [_ A  /  x ]_ R ) )
34 csbcomg 3054 . . . . 5  |-  ( ( A  e.  C  /\  B  e.  D )  ->  [_ A  /  x ]_ [_ B  /  y ]_ R  =  [_ B  /  y ]_ [_ A  /  x ]_ R )
3534eleq1d 2226 . . . 4  |-  ( ( A  e.  C  /\  B  e.  D )  ->  ( [_ A  /  x ]_ [_ B  / 
y ]_ R  e.  _V  <->  [_ B  /  y ]_ [_ A  /  x ]_ R  e.  _V )
)
3634eqeq2d 2169 . . . 4  |-  ( ( A  e.  C  /\  B  e.  D )  ->  ( ( A F B )  =  [_ A  /  x ]_ [_ B  /  y ]_ R  <->  ( A F B )  =  [_ B  / 
y ]_ [_ A  /  x ]_ R ) )
3733, 35, 363imtr4d 202 . . 3  |-  ( ( A  e.  C  /\  B  e.  D )  ->  ( [_ A  /  x ]_ [_ B  / 
y ]_ R  e.  _V  ->  ( A F B )  =  [_ A  /  x ]_ [_ B  /  y ]_ R
) )
381, 37syl5 32 . 2  |-  ( ( A  e.  C  /\  B  e.  D )  ->  ( [_ A  /  x ]_ [_ B  / 
y ]_ R  e.  V  ->  ( A F B )  =  [_ A  /  x ]_ [_ B  /  y ]_ R
) )
39383impia 1182 1  |-  ( ( A  e.  C  /\  B  e.  D  /\  [_ A  /  x ]_ [_ B  /  y ]_ R  e.  V )  ->  ( A F B )  =  [_ A  /  x ]_ [_ B  /  y ]_ R
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    /\ w3a 963    = wceq 1335    e. wcel 2128   _Vcvv 2712   [_csb 3031  (class class class)co 5826    e. cmpo 5828
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-14 2131  ax-ext 2139  ax-sep 4084  ax-pow 4137  ax-pr 4171  ax-setind 4498
This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1338  df-fal 1341  df-nf 1441  df-sb 1743  df-eu 2009  df-mo 2010  df-clab 2144  df-cleq 2150  df-clel 2153  df-nfc 2288  df-ne 2328  df-ral 2440  df-rex 2441  df-v 2714  df-sbc 2938  df-csb 3032  df-dif 3104  df-un 3106  df-in 3108  df-ss 3115  df-pw 3546  df-sn 3567  df-pr 3568  df-op 3570  df-uni 3775  df-br 3968  df-opab 4028  df-id 4255  df-xp 4594  df-rel 4595  df-cnv 4596  df-co 4597  df-dm 4598  df-iota 5137  df-fun 5174  df-fv 5180  df-ov 5829  df-oprab 5830  df-mpo 5831
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator