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

Theorem ralrnmpt 5612
Description: A restricted quantifier over an image set. (Contributed by Mario Carneiro, 20-Aug-2015.)
Hypotheses
Ref Expression
ralrnmpt.1  |-  F  =  ( x  e.  A  |->  B )
ralrnmpt.2  |-  ( y  =  B  ->  ( ps 
<->  ch ) )
Assertion
Ref Expression
ralrnmpt  |-  ( A. x  e.  A  B  e.  V  ->  ( A. y  e.  ran  F ps  <->  A. x  e.  A  ch ) )
Distinct variable groups:    x, A    y, B    ch, y    y, F    ps, x
Allowed substitution hints:    ps( y)    ch( x)    A( y)    B( x)    F( x)    V( x, y)

Proof of Theorem ralrnmpt
Dummy variables  w  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ralrnmpt.1 . . . . 5  |-  F  =  ( x  e.  A  |->  B )
21fnmpt 5299 . . . 4  |-  ( A. x  e.  A  B  e.  V  ->  F  Fn  A )
3 dfsbcq 2939 . . . . 5  |-  ( w  =  ( F `  z )  ->  ( [. w  /  y ]. ps  <->  [. ( F `  z )  /  y ]. ps ) )
43ralrn 5608 . . . 4  |-  ( F  Fn  A  ->  ( A. w  e.  ran  F
[. w  /  y ]. ps  <->  A. z  e.  A  [. ( F `  z
)  /  y ]. ps ) )
52, 4syl 14 . . 3  |-  ( A. x  e.  A  B  e.  V  ->  ( A. w  e.  ran  F [. w  /  y ]. ps  <->  A. z  e.  A  [. ( F `  z )  /  y ]. ps ) )
6 nfv 1508 . . . . 5  |-  F/ w ps
7 nfsbc1v 2955 . . . . 5  |-  F/ y
[. w  /  y ]. ps
8 sbceq1a 2946 . . . . 5  |-  ( y  =  w  ->  ( ps 
<-> 
[. w  /  y ]. ps ) )
96, 7, 8cbvral 2676 . . . 4  |-  ( A. y  e.  ran  F ps  <->  A. w  e.  ran  F [. w  /  y ]. ps )
109bicomi 131 . . 3  |-  ( A. w  e.  ran  F [. w  /  y ]. ps  <->  A. y  e.  ran  F ps )
11 nfmpt1 4060 . . . . . . 7  |-  F/_ x
( x  e.  A  |->  B )
121, 11nfcxfr 2296 . . . . . 6  |-  F/_ x F
13 nfcv 2299 . . . . . 6  |-  F/_ x
z
1412, 13nffv 5481 . . . . 5  |-  F/_ x
( F `  z
)
15 nfv 1508 . . . . 5  |-  F/ x ps
1614, 15nfsbc 2957 . . . 4  |-  F/ x [. ( F `  z
)  /  y ]. ps
17 nfv 1508 . . . 4  |-  F/ z
[. ( F `  x )  /  y ]. ps
18 fveq2 5471 . . . . 5  |-  ( z  =  x  ->  ( F `  z )  =  ( F `  x ) )
19 dfsbcq 2939 . . . . 5  |-  ( ( F `  z )  =  ( F `  x )  ->  ( [. ( F `  z
)  /  y ]. ps 
<-> 
[. ( F `  x )  /  y ]. ps ) )
2018, 19syl 14 . . . 4  |-  ( z  =  x  ->  ( [. ( F `  z
)  /  y ]. ps 
<-> 
[. ( F `  x )  /  y ]. ps ) )
2116, 17, 20cbvral 2676 . . 3  |-  ( A. z  e.  A  [. ( F `  z )  /  y ]. ps  <->  A. x  e.  A  [. ( F `  x )  /  y ]. ps )
225, 10, 213bitr3g 221 . 2  |-  ( A. x  e.  A  B  e.  V  ->  ( A. y  e.  ran  F ps  <->  A. x  e.  A  [. ( F `  x )  /  y ]. ps ) )
231fvmpt2 5554 . . . . . 6  |-  ( ( x  e.  A  /\  B  e.  V )  ->  ( F `  x
)  =  B )
24 dfsbcq 2939 . . . . . 6  |-  ( ( F `  x )  =  B  ->  ( [. ( F `  x
)  /  y ]. ps 
<-> 
[. B  /  y ]. ps ) )
2523, 24syl 14 . . . . 5  |-  ( ( x  e.  A  /\  B  e.  V )  ->  ( [. ( F `
 x )  / 
y ]. ps  <->  [. B  / 
y ]. ps ) )
26 ralrnmpt.2 . . . . . . 7  |-  ( y  =  B  ->  ( ps 
<->  ch ) )
2726sbcieg 2969 . . . . . 6  |-  ( B  e.  V  ->  ( [. B  /  y ]. ps  <->  ch ) )
2827adantl 275 . . . . 5  |-  ( ( x  e.  A  /\  B  e.  V )  ->  ( [. B  / 
y ]. ps  <->  ch )
)
2925, 28bitrd 187 . . . 4  |-  ( ( x  e.  A  /\  B  e.  V )  ->  ( [. ( F `
 x )  / 
y ]. ps  <->  ch )
)
3029ralimiaa 2519 . . 3  |-  ( A. x  e.  A  B  e.  V  ->  A. x  e.  A  ( [. ( F `  x )  /  y ]. ps  <->  ch ) )
31 ralbi 2589 . . 3  |-  ( A. x  e.  A  ( [. ( F `  x
)  /  y ]. ps 
<->  ch )  ->  ( A. x  e.  A  [. ( F `  x
)  /  y ]. ps 
<-> 
A. x  e.  A  ch ) )
3230, 31syl 14 . 2  |-  ( A. x  e.  A  B  e.  V  ->  ( A. x  e.  A  [. ( F `  x )  /  y ]. ps  <->  A. x  e.  A  ch ) )
3322, 32bitrd 187 1  |-  ( A. x  e.  A  B  e.  V  ->  ( A. y  e.  ran  F ps  <->  A. x  e.  A  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    <-> wb 104    = wceq 1335    e. wcel 2128   A.wral 2435   [.wsbc 2937    |-> cmpt 4028   ran crn 4590    Fn wfn 5168   ` cfv 5173
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-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 4085  ax-pow 4138  ax-pr 4172
This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1338  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-ral 2440  df-rex 2441  df-v 2714  df-sbc 2938  df-csb 3032  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 4029  df-mpt 4030  df-id 4256  df-xp 4595  df-rel 4596  df-cnv 4597  df-co 4598  df-dm 4599  df-rn 4600  df-iota 5138  df-fun 5175  df-fn 5176  df-fv 5181
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator