Users' Mathboxes Mathbox for ML < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  mptsnunlem Structured version   Unicode version

Theorem mptsnunlem 31474
Description: This is the core of the proof of mptsnun 31475, but to avoid the distinct variables on the definitions, we split this proof into two. (Contributed by ML, 16-Jul-2020.)
Hypotheses
Ref Expression
mptsnun.f  |-  F  =  ( x  e.  A  |->  { x } )
mptsnun.r  |-  R  =  { u  |  E. x  e.  A  u  =  { x } }
Assertion
Ref Expression
mptsnunlem  |-  ( B 
C_  A  ->  B  =  U. ( F " B ) )
Distinct variable groups:    u, A, x    u, B, x    x, F
Allowed substitution hints:    R( x, u)    F( u)

Proof of Theorem mptsnunlem
Dummy variable  z is distinct from all other variables.
StepHypRef Expression
1 df-ima 4867 . . . . . . 7  |-  ( F
" B )  =  ran  ( F  |`  B )
2 mptsnun.f . . . . . . . . . . 11  |-  F  =  ( x  e.  A  |->  { x } )
32reseq1i 5121 . . . . . . . . . 10  |-  ( F  |`  B )  =  ( ( x  e.  A  |->  { x } )  |`  B )
4 resmpt 5174 . . . . . . . . . 10  |-  ( B 
C_  A  ->  (
( x  e.  A  |->  { x } )  |`  B )  =  ( x  e.  B  |->  { x } ) )
53, 4syl5eq 2482 . . . . . . . . 9  |-  ( B 
C_  A  ->  ( F  |`  B )  =  ( x  e.  B  |->  { x } ) )
65rneqd 5082 . . . . . . . 8  |-  ( B 
C_  A  ->  ran  ( F  |`  B )  =  ran  ( x  e.  B  |->  { x } ) )
7 rnmptsn 31471 . . . . . . . 8  |-  ran  (
x  e.  B  |->  { x } )  =  { u  |  E. x  e.  B  u  =  { x } }
86, 7syl6eq 2486 . . . . . . 7  |-  ( B 
C_  A  ->  ran  ( F  |`  B )  =  { u  |  E. x  e.  B  u  =  { x } } )
91, 8syl5eq 2482 . . . . . 6  |-  ( B 
C_  A  ->  ( F " B )  =  { u  |  E. x  e.  B  u  =  { x } }
)
109unieqd 4232 . . . . 5  |-  ( B 
C_  A  ->  U. ( F " B )  = 
U. { u  |  E. x  e.  B  u  =  { x } } )
1110eleq2d 2499 . . . 4  |-  ( B 
C_  A  ->  (
x  e.  U. ( F " B )  <->  x  e.  U. { u  |  E. x  e.  B  u  =  { x } }
) )
12 eleq1 2501 . . . . . 6  |-  ( z  =  x  ->  (
z  e.  B  <->  x  e.  B ) )
13 eluniab 4233 . . . . . . . . 9  |-  ( z  e.  U. { u  |  E. x  e.  B  u  =  { x } }  <->  E. u ( z  e.  u  /\  E. x  e.  B  u  =  { x } ) )
14 ancom 451 . . . . . . . . . . . . 13  |-  ( ( z  e.  u  /\  E. x  e.  B  u  =  { x }
)  <->  ( E. x  e.  B  u  =  { x }  /\  z  e.  u )
)
15 r19.41v 2987 . . . . . . . . . . . . 13  |-  ( E. x  e.  B  ( u  =  { x }  /\  z  e.  u
)  <->  ( E. x  e.  B  u  =  { x }  /\  z  e.  u )
)
16 df-rex 2788 . . . . . . . . . . . . 13  |-  ( E. x  e.  B  ( u  =  { x }  /\  z  e.  u
)  <->  E. x ( x  e.  B  /\  (
u  =  { x }  /\  z  e.  u
) ) )
1714, 15, 163bitr2i 276 . . . . . . . . . . . 12  |-  ( ( z  e.  u  /\  E. x  e.  B  u  =  { x }
)  <->  E. x ( x  e.  B  /\  (
u  =  { x }  /\  z  e.  u
) ) )
18 eleq2 2502 . . . . . . . . . . . . . . . . 17  |-  ( u  =  { x }  ->  ( z  e.  u  <->  z  e.  { x }
) )
1918anbi2d 708 . . . . . . . . . . . . . . . 16  |-  ( u  =  { x }  ->  ( ( u  =  { x }  /\  z  e.  u )  <->  ( u  =  { x }  /\  z  e.  {
x } ) ) )
2019adantr 466 . . . . . . . . . . . . . . 15  |-  ( ( u  =  { x }  /\  z  e.  u
)  ->  ( (
u  =  { x }  /\  z  e.  u
)  <->  ( u  =  { x }  /\  z  e.  { x } ) ) )
2120ibi 244 . . . . . . . . . . . . . 14  |-  ( ( u  =  { x }  /\  z  e.  u
)  ->  ( u  =  { x }  /\  z  e.  { x } ) )
2221anim2i 571 . . . . . . . . . . . . 13  |-  ( ( x  e.  B  /\  ( u  =  {
x }  /\  z  e.  u ) )  -> 
( x  e.  B  /\  ( u  =  {
x }  /\  z  e.  { x } ) ) )
2322eximi 1703 . . . . . . . . . . . 12  |-  ( E. x ( x  e.  B  /\  ( u  =  { x }  /\  z  e.  u
) )  ->  E. x
( x  e.  B  /\  ( u  =  {
x }  /\  z  e.  { x } ) ) )
2417, 23sylbi 198 . . . . . . . . . . 11  |-  ( ( z  e.  u  /\  E. x  e.  B  u  =  { x }
)  ->  E. x
( x  e.  B  /\  ( u  =  {
x }  /\  z  e.  { x } ) ) )
25 an12 804 . . . . . . . . . . . . 13  |-  ( ( x  e.  B  /\  ( u  =  {
x }  /\  z  e.  { x } ) )  <->  ( u  =  { x }  /\  ( x  e.  B  /\  z  e.  { x } ) ) )
2625exbii 1714 . . . . . . . . . . . 12  |-  ( E. x ( x  e.  B  /\  ( u  =  { x }  /\  z  e.  { x } ) )  <->  E. x
( u  =  {
x }  /\  (
x  e.  B  /\  z  e.  { x } ) ) )
27 exsimpr 1725 . . . . . . . . . . . 12  |-  ( E. x ( u  =  { x }  /\  ( x  e.  B  /\  z  e.  { x } ) )  ->  E. x ( x  e.  B  /\  z  e. 
{ x } ) )
2826, 27sylbi 198 . . . . . . . . . . 11  |-  ( E. x ( x  e.  B  /\  ( u  =  { x }  /\  z  e.  { x } ) )  ->  E. x ( x  e.  B  /\  z  e. 
{ x } ) )
2924, 28syl 17 . . . . . . . . . 10  |-  ( ( z  e.  u  /\  E. x  e.  B  u  =  { x }
)  ->  E. x
( x  e.  B  /\  z  e.  { x } ) )
3029exlimiv 1769 . . . . . . . . 9  |-  ( E. u ( z  e.  u  /\  E. x  e.  B  u  =  { x } )  ->  E. x ( x  e.  B  /\  z  e.  { x } ) )
3113, 30sylbi 198 . . . . . . . 8  |-  ( z  e.  U. { u  |  E. x  e.  B  u  =  { x } }  ->  E. x
( x  e.  B  /\  z  e.  { x } ) )
32 elsn 4016 . . . . . . . . . 10  |-  ( z  e.  { x }  <->  z  =  x )
3332anbi2i 698 . . . . . . . . 9  |-  ( ( x  e.  B  /\  z  e.  { x } )  <->  ( x  e.  B  /\  z  =  x ) )
3433exbii 1714 . . . . . . . 8  |-  ( E. x ( x  e.  B  /\  z  e. 
{ x } )  <->  E. x ( x  e.  B  /\  z  =  x ) )
3531, 34sylib 199 . . . . . . 7  |-  ( z  e.  U. { u  |  E. x  e.  B  u  =  { x } }  ->  E. x
( x  e.  B  /\  z  =  x
) )
3612biimparc 489 . . . . . . . 8  |-  ( ( x  e.  B  /\  z  =  x )  ->  z  e.  B )
3736exlimiv 1769 . . . . . . 7  |-  ( E. x ( x  e.  B  /\  z  =  x )  ->  z  e.  B )
3835, 37syl 17 . . . . . 6  |-  ( z  e.  U. { u  |  E. x  e.  B  u  =  { x } }  ->  z  e.  B )
3912, 38vtoclga 3151 . . . . 5  |-  ( x  e.  U. { u  |  E. x  e.  B  u  =  { x } }  ->  x  e.  B )
40 equid 1842 . . . . . 6  |-  x  =  x
41 eqid 2429 . . . . . . . . . . . 12  |-  { x }  =  { x }
42 snex 4663 . . . . . . . . . . . . . 14  |-  { x }  e.  _V
43 sbcg 3371 . . . . . . . . . . . . . 14  |-  ( { x }  e.  _V  ->  ( [. { x }  /  u ]. x  e.  B  <->  x  e.  B
) )
4442, 43ax-mp 5 . . . . . . . . . . . . 13  |-  ( [. { x }  /  u ]. x  e.  B  <->  x  e.  B )
45 eqsbc3 3345 . . . . . . . . . . . . . 14  |-  ( { x }  e.  _V  ->  ( [. { x }  /  u ]. u  =  { x }  <->  { x }  =  { x } ) )
4642, 45ax-mp 5 . . . . . . . . . . . . 13  |-  ( [. { x }  /  u ]. u  =  {
x }  <->  { x }  =  { x } )
4718adantl 467 . . . . . . . . . . . . . . . . . 18  |-  ( ( x  e.  B  /\  u  =  { x } )  ->  (
z  e.  u  <->  z  e.  { x } ) )
48 df-rex 2788 . . . . . . . . . . . . . . . . . . . 20  |-  ( E. x  e.  B  u  =  { x }  <->  E. x ( x  e.  B  /\  u  =  { x } ) )
4913biimpri 209 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( E. u ( z  e.  u  /\  E. x  e.  B  u  =  { x } )  ->  z  e.  U. { u  |  E. x  e.  B  u  =  { x } }
)
504919.23bi 1924 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( z  e.  u  /\  E. x  e.  B  u  =  { x }
)  ->  z  e.  U. { u  |  E. x  e.  B  u  =  { x } }
)
5150expcom 436 . . . . . . . . . . . . . . . . . . . 20  |-  ( E. x  e.  B  u  =  { x }  ->  ( z  e.  u  ->  z  e.  U. {
u  |  E. x  e.  B  u  =  { x } }
) )
5248, 51sylbir 216 . . . . . . . . . . . . . . . . . . 19  |-  ( E. x ( x  e.  B  /\  u  =  { x } )  ->  ( z  e.  u  ->  z  e.  U. { u  |  E. x  e.  B  u  =  { x } }
) )
535219.23bi 1924 . . . . . . . . . . . . . . . . . 18  |-  ( ( x  e.  B  /\  u  =  { x } )  ->  (
z  e.  u  -> 
z  e.  U. {
u  |  E. x  e.  B  u  =  { x } }
) )
5447, 53sylbird 238 . . . . . . . . . . . . . . . . 17  |-  ( ( x  e.  B  /\  u  =  { x } )  ->  (
z  e.  { x }  ->  z  e.  U. { u  |  E. x  e.  B  u  =  { x } }
) )
5554sbcth 3320 . . . . . . . . . . . . . . . 16  |-  ( { x }  e.  _V  ->  [. { x }  /  u ]. ( ( x  e.  B  /\  u  =  { x } )  ->  (
z  e.  { x }  ->  z  e.  U. { u  |  E. x  e.  B  u  =  { x } }
) ) )
5642, 55ax-mp 5 . . . . . . . . . . . . . . 15  |-  [. {
x }  /  u ]. ( ( x  e.  B  /\  u  =  { x } )  ->  ( z  e. 
{ x }  ->  z  e.  U. { u  |  E. x  e.  B  u  =  { x } } ) )
57 sbcimg 3347 . . . . . . . . . . . . . . . 16  |-  ( { x }  e.  _V  ->  ( [. { x }  /  u ]. (
( x  e.  B  /\  u  =  {
x } )  -> 
( z  e.  {
x }  ->  z  e.  U. { u  |  E. x  e.  B  u  =  { x } } ) )  <->  ( [. { x }  /  u ]. ( x  e.  B  /\  u  =  { x } )  ->  [. { x }  /  u ]. ( z  e.  { x }  ->  z  e.  U. {
u  |  E. x  e.  B  u  =  { x } }
) ) ) )
5842, 57ax-mp 5 . . . . . . . . . . . . . . 15  |-  ( [. { x }  /  u ]. ( ( x  e.  B  /\  u  =  { x } )  ->  ( z  e. 
{ x }  ->  z  e.  U. { u  |  E. x  e.  B  u  =  { x } } ) )  <->  ( [. { x }  /  u ]. ( x  e.  B  /\  u  =  { x } )  ->  [. { x }  /  u ]. ( z  e.  { x }  ->  z  e.  U. {
u  |  E. x  e.  B  u  =  { x } }
) ) )
5956, 58mpbi 211 . . . . . . . . . . . . . 14  |-  ( [. { x }  /  u ]. ( x  e.  B  /\  u  =  { x } )  ->  [. { x }  /  u ]. ( z  e.  { x }  ->  z  e.  U. {
u  |  E. x  e.  B  u  =  { x } }
) )
60 sbcan 3348 . . . . . . . . . . . . . 14  |-  ( [. { x }  /  u ]. ( x  e.  B  /\  u  =  { x } )  <-> 
( [. { x }  /  u ]. x  e.  B  /\  [. {
x }  /  u ]. u  =  {
x } ) )
61 nfv 1754 . . . . . . . . . . . . . . . 16  |-  F/ u  z  e.  { x }
62 nfab1 2593 . . . . . . . . . . . . . . . . . 18  |-  F/_ u { u  |  E. x  e.  B  u  =  { x } }
6362nfuni 4228 . . . . . . . . . . . . . . . . 17  |-  F/_ u U. { u  |  E. x  e.  B  u  =  { x } }
6463nfcri 2584 . . . . . . . . . . . . . . . 16  |-  F/ u  z  e.  U. { u  |  E. x  e.  B  u  =  { x } }
6561, 64nfim 1978 . . . . . . . . . . . . . . 15  |-  F/ u
( z  e.  {
x }  ->  z  e.  U. { u  |  E. x  e.  B  u  =  { x } } )
66 sbctt 3368 . . . . . . . . . . . . . . 15  |-  ( ( { x }  e.  _V  /\  F/ u ( z  e.  { x }  ->  z  e.  U. { u  |  E. x  e.  B  u  =  { x } }
) )  ->  ( [. { x }  /  u ]. ( z  e. 
{ x }  ->  z  e.  U. { u  |  E. x  e.  B  u  =  { x } } )  <->  ( z  e.  { x }  ->  z  e.  U. { u  |  E. x  e.  B  u  =  { x } } ) ) )
6742, 65, 66mp2an 676 . . . . . . . . . . . . . 14  |-  ( [. { x }  /  u ]. ( z  e. 
{ x }  ->  z  e.  U. { u  |  E. x  e.  B  u  =  { x } } )  <->  ( z  e.  { x }  ->  z  e.  U. { u  |  E. x  e.  B  u  =  { x } } ) )
6859, 60, 673imtr3i 268 . . . . . . . . . . . . 13  |-  ( (
[. { x }  /  u ]. x  e.  B  /\  [. {
x }  /  u ]. u  =  {
x } )  -> 
( z  e.  {
x }  ->  z  e.  U. { u  |  E. x  e.  B  u  =  { x } } ) )
6944, 46, 68syl2anbr 482 . . . . . . . . . . . 12  |-  ( ( x  e.  B  /\  { x }  =  {
x } )  -> 
( z  e.  {
x }  ->  z  e.  U. { u  |  E. x  e.  B  u  =  { x } } ) )
7041, 69mpan2 675 . . . . . . . . . . 11  |-  ( x  e.  B  ->  (
z  e.  { x }  ->  z  e.  U. { u  |  E. x  e.  B  u  =  { x } }
) )
7132, 70syl5bir 221 . . . . . . . . . 10  |-  ( x  e.  B  ->  (
z  =  x  -> 
z  e.  U. {
u  |  E. x  e.  B  u  =  { x } }
) )
72 eleq1 2501 . . . . . . . . . 10  |-  ( z  =  x  ->  (
z  e.  U. {
u  |  E. x  e.  B  u  =  { x } }  <->  x  e.  U. { u  |  E. x  e.  B  u  =  { x } } ) )
7371, 72mpbidi 219 . . . . . . . . 9  |-  ( x  e.  B  ->  (
z  =  x  ->  x  e.  U. { u  |  E. x  e.  B  u  =  { x } } ) )
7473com12 32 . . . . . . . 8  |-  ( z  =  x  ->  (
x  e.  B  ->  x  e.  U. { u  |  E. x  e.  B  u  =  { x } } ) )
7574sbimi 1795 . . . . . . 7  |-  ( [ x  /  z ] z  =  x  ->  [ x  /  z ] ( x  e.  B  ->  x  e.  U. { u  |  E. x  e.  B  u  =  { x } }
) )
76 equsb3 2228 . . . . . . 7  |-  ( [ x  /  z ] z  =  x  <->  x  =  x )
77 nfv 1754 . . . . . . . 8  |-  F/ z ( x  e.  B  ->  x  e.  U. {
u  |  E. x  e.  B  u  =  { x } }
)
7877sbf 2175 . . . . . . 7  |-  ( [ x  /  z ] ( x  e.  B  ->  x  e.  U. {
u  |  E. x  e.  B  u  =  { x } }
)  <->  ( x  e.  B  ->  x  e.  U. { u  |  E. x  e.  B  u  =  { x } }
) )
7975, 76, 783imtr3i 268 . . . . . 6  |-  ( x  =  x  ->  (
x  e.  B  ->  x  e.  U. { u  |  E. x  e.  B  u  =  { x } } ) )
8040, 79ax-mp 5 . . . . 5  |-  ( x  e.  B  ->  x  e.  U. { u  |  E. x  e.  B  u  =  { x } } )
8139, 80impbii 190 . . . 4  |-  ( x  e.  U. { u  |  E. x  e.  B  u  =  { x } }  <->  x  e.  B
)
8211, 81syl6bb 264 . . 3  |-  ( B 
C_  A  ->  (
x  e.  U. ( F " B )  <->  x  e.  B ) )
8382eqrdv 2426 . 2  |-  ( B 
C_  A  ->  U. ( F " B )  =  B )
8483eqcomd 2437 1  |-  ( B 
C_  A  ->  B  =  U. ( F " B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    /\ wa 370    = wceq 1437   E.wex 1659   F/wnf 1663   [wsb 1789    e. wcel 1870   {cab 2414   E.wrex 2783   _Vcvv 3087   [.wsbc 3305    C_ wss 3442   {csn 4002   U.cuni 4222    |-> cmpt 4484   ran crn 4855    |` cres 4856   "cima 4857
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-9 1874  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407  ax-sep 4548  ax-nul 4556  ax-pr 4661
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-eu 2270  df-mo 2271  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-ne 2627  df-ral 2787  df-rex 2788  df-rab 2791  df-v 3089  df-sbc 3306  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-nul 3768  df-if 3916  df-sn 4003  df-pr 4005  df-op 4009  df-uni 4223  df-br 4427  df-opab 4485  df-mpt 4486  df-xp 4860  df-rel 4861  df-cnv 4862  df-dm 4864  df-rn 4865  df-res 4866  df-ima 4867
This theorem is referenced by:  mptsnun  31475
  Copyright terms: Public domain W3C validator