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

Theorem mptsnunlem 31785
Description: This is the core of the proof of mptsnun 31786, 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 4866 . . . . . . 7  |-  ( F
" B )  =  ran  ( F  |`  B )
2 mptsnun.f . . . . . . . . . . 11  |-  F  =  ( x  e.  A  |->  { x } )
32reseq1i 5120 . . . . . . . . . 10  |-  ( F  |`  B )  =  ( ( x  e.  A  |->  { x } )  |`  B )
4 resmpt 5173 . . . . . . . . . 10  |-  ( B 
C_  A  ->  (
( x  e.  A  |->  { x } )  |`  B )  =  ( x  e.  B  |->  { x } ) )
53, 4syl5eq 2508 . . . . . . . . 9  |-  ( B 
C_  A  ->  ( F  |`  B )  =  ( x  e.  B  |->  { x } ) )
65rneqd 5081 . . . . . . . 8  |-  ( B 
C_  A  ->  ran  ( F  |`  B )  =  ran  ( x  e.  B  |->  { x } ) )
7 rnmptsn 31782 . . . . . . . 8  |-  ran  (
x  e.  B  |->  { x } )  =  { u  |  E. x  e.  B  u  =  { x } }
86, 7syl6eq 2512 . . . . . . 7  |-  ( B 
C_  A  ->  ran  ( F  |`  B )  =  { u  |  E. x  e.  B  u  =  { x } } )
91, 8syl5eq 2508 . . . . . 6  |-  ( B 
C_  A  ->  ( F " B )  =  { u  |  E. x  e.  B  u  =  { x } }
)
109unieqd 4222 . . . . 5  |-  ( B 
C_  A  ->  U. ( F " B )  = 
U. { u  |  E. x  e.  B  u  =  { x } } )
1110eleq2d 2525 . . . 4  |-  ( B 
C_  A  ->  (
x  e.  U. ( F " B )  <->  x  e.  U. { u  |  E. x  e.  B  u  =  { x } }
) )
12 eleq1 2528 . . . . . 6  |-  ( z  =  x  ->  (
z  e.  B  <->  x  e.  B ) )
13 eluniab 4223 . . . . . . . . 9  |-  ( z  e.  U. { u  |  E. x  e.  B  u  =  { x } }  <->  E. u ( z  e.  u  /\  E. x  e.  B  u  =  { x } ) )
14 ancom 456 . . . . . . . . . . . . 13  |-  ( ( z  e.  u  /\  E. x  e.  B  u  =  { x }
)  <->  ( E. x  e.  B  u  =  { x }  /\  z  e.  u )
)
15 r19.41v 2954 . . . . . . . . . . . . 13  |-  ( E. x  e.  B  ( u  =  { x }  /\  z  e.  u
)  <->  ( E. x  e.  B  u  =  { x }  /\  z  e.  u )
)
16 df-rex 2755 . . . . . . . . . . . . 13  |-  ( E. x  e.  B  ( u  =  { x }  /\  z  e.  u
)  <->  E. x ( x  e.  B  /\  (
u  =  { x }  /\  z  e.  u
) ) )
1714, 15, 163bitr2i 281 . . . . . . . . . . . 12  |-  ( ( z  e.  u  /\  E. x  e.  B  u  =  { x }
)  <->  E. x ( x  e.  B  /\  (
u  =  { x }  /\  z  e.  u
) ) )
18 eleq2 2529 . . . . . . . . . . . . . . . . 17  |-  ( u  =  { x }  ->  ( z  e.  u  <->  z  e.  { x }
) )
1918anbi2d 715 . . . . . . . . . . . . . . . 16  |-  ( u  =  { x }  ->  ( ( u  =  { x }  /\  z  e.  u )  <->  ( u  =  { x }  /\  z  e.  {
x } ) ) )
2019adantr 471 . . . . . . . . . . . . . . 15  |-  ( ( u  =  { x }  /\  z  e.  u
)  ->  ( (
u  =  { x }  /\  z  e.  u
)  <->  ( u  =  { x }  /\  z  e.  { x } ) ) )
2120ibi 249 . . . . . . . . . . . . . 14  |-  ( ( u  =  { x }  /\  z  e.  u
)  ->  ( u  =  { x }  /\  z  e.  { x } ) )
2221anim2i 577 . . . . . . . . . . . . 13  |-  ( ( x  e.  B  /\  ( u  =  {
x }  /\  z  e.  u ) )  -> 
( x  e.  B  /\  ( u  =  {
x }  /\  z  e.  { x } ) ) )
2322eximi 1718 . . . . . . . . . . . 12  |-  ( E. x ( x  e.  B  /\  ( u  =  { x }  /\  z  e.  u
) )  ->  E. x
( x  e.  B  /\  ( u  =  {
x }  /\  z  e.  { x } ) ) )
2417, 23sylbi 200 . . . . . . . . . . 11  |-  ( ( z  e.  u  /\  E. x  e.  B  u  =  { x }
)  ->  E. x
( x  e.  B  /\  ( u  =  {
x }  /\  z  e.  { x } ) ) )
25 an12 811 . . . . . . . . . . . . 13  |-  ( ( x  e.  B  /\  ( u  =  {
x }  /\  z  e.  { x } ) )  <->  ( u  =  { x }  /\  ( x  e.  B  /\  z  e.  { x } ) ) )
2625exbii 1729 . . . . . . . . . . . 12  |-  ( E. x ( x  e.  B  /\  ( u  =  { x }  /\  z  e.  { x } ) )  <->  E. x
( u  =  {
x }  /\  (
x  e.  B  /\  z  e.  { x } ) ) )
27 exsimpr 1741 . . . . . . . . . . . 12  |-  ( E. x ( u  =  { x }  /\  ( x  e.  B  /\  z  e.  { x } ) )  ->  E. x ( x  e.  B  /\  z  e. 
{ x } ) )
2826, 27sylbi 200 . . . . . . . . . . 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 1787 . . . . . . . . 9  |-  ( E. u ( z  e.  u  /\  E. x  e.  B  u  =  { x } )  ->  E. x ( x  e.  B  /\  z  e.  { x } ) )
3113, 30sylbi 200 . . . . . . . 8  |-  ( z  e.  U. { u  |  E. x  e.  B  u  =  { x } }  ->  E. x
( x  e.  B  /\  z  e.  { x } ) )
32 elsn 3994 . . . . . . . . . 10  |-  ( z  e.  { x }  <->  z  =  x )
3332anbi2i 705 . . . . . . . . 9  |-  ( ( x  e.  B  /\  z  e.  { x } )  <->  ( x  e.  B  /\  z  =  x ) )
3433exbii 1729 . . . . . . . 8  |-  ( E. x ( x  e.  B  /\  z  e. 
{ x } )  <->  E. x ( x  e.  B  /\  z  =  x ) )
3531, 34sylib 201 . . . . . . 7  |-  ( z  e.  U. { u  |  E. x  e.  B  u  =  { x } }  ->  E. x
( x  e.  B  /\  z  =  x
) )
3612biimparc 494 . . . . . . . 8  |-  ( ( x  e.  B  /\  z  =  x )  ->  z  e.  B )
3736exlimiv 1787 . . . . . . 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 3125 . . . . 5  |-  ( x  e.  U. { u  |  E. x  e.  B  u  =  { x } }  ->  x  e.  B )
40 equid 1866 . . . . . 6  |-  x  =  x
41 eqid 2462 . . . . . . . . . . . 12  |-  { x }  =  { x }
42 snex 4655 . . . . . . . . . . . . . 14  |-  { x }  e.  _V
43 sbcg 3345 . . . . . . . . . . . . . 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 3319 . . . . . . . . . . . . . 14  |-  ( { x }  e.  _V  ->  ( [. { x }  /  u ]. u  =  { x }  <->  { x }  =  { x } ) )
4642, 45ax-mp 5 . . . . . . . . . . . . 13  |-  ( [. { x }  /  u ]. u  =  {
x }  <->  { x }  =  { x } )
4718adantl 472 . . . . . . . . . . . . . . . . . 18  |-  ( ( x  e.  B  /\  u  =  { x } )  ->  (
z  e.  u  <->  z  e.  { x } ) )
48 df-rex 2755 . . . . . . . . . . . . . . . . . . . 20  |-  ( E. x  e.  B  u  =  { x }  <->  E. x ( x  e.  B  /\  u  =  { x } ) )
4913biimpri 211 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( E. u ( z  e.  u  /\  E. x  e.  B  u  =  { x } )  ->  z  e.  U. { u  |  E. x  e.  B  u  =  { x } }
)
504919.23bi 1960 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( z  e.  u  /\  E. x  e.  B  u  =  { x }
)  ->  z  e.  U. { u  |  E. x  e.  B  u  =  { x } }
)
5150expcom 441 . . . . . . . . . . . . . . . . . . . 20  |-  ( E. x  e.  B  u  =  { x }  ->  ( z  e.  u  ->  z  e.  U. {
u  |  E. x  e.  B  u  =  { x } }
) )
5248, 51sylbir 218 . . . . . . . . . . . . . . . . . . 19  |-  ( E. x ( x  e.  B  /\  u  =  { x } )  ->  ( z  e.  u  ->  z  e.  U. { u  |  E. x  e.  B  u  =  { x } }
) )
535219.23bi 1960 . . . . . . . . . . . . . . . . . 18  |-  ( ( x  e.  B  /\  u  =  { x } )  ->  (
z  e.  u  -> 
z  e.  U. {
u  |  E. x  e.  B  u  =  { x } }
) )
5447, 53sylbird 243 . . . . . . . . . . . . . . . . 17  |-  ( ( x  e.  B  /\  u  =  { x } )  ->  (
z  e.  { x }  ->  z  e.  U. { u  |  E. x  e.  B  u  =  { x } }
) )
5554sbcth 3294 . . . . . . . . . . . . . . . 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 3321 . . . . . . . . . . . . . . . 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 213 . . . . . . . . . . . . . 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 3322 . . . . . . . . . . . . . 14  |-  ( [. { x }  /  u ]. ( x  e.  B  /\  u  =  { x } )  <-> 
( [. { x }  /  u ]. x  e.  B  /\  [. {
x }  /  u ]. u  =  {
x } ) )
61 nfv 1772 . . . . . . . . . . . . . . . 16  |-  F/ u  z  e.  { x }
62 nfab1 2605 . . . . . . . . . . . . . . . . . 18  |-  F/_ u { u  |  E. x  e.  B  u  =  { x } }
6362nfuni 4218 . . . . . . . . . . . . . . . . 17  |-  F/_ u U. { u  |  E. x  e.  B  u  =  { x } }
6463nfcri 2597 . . . . . . . . . . . . . . . 16  |-  F/ u  z  e.  U. { u  |  E. x  e.  B  u  =  { x } }
6561, 64nfim 2014 . . . . . . . . . . . . . . 15  |-  F/ u
( z  e.  {
x }  ->  z  e.  U. { u  |  E. x  e.  B  u  =  { x } } )
66 sbctt 3342 . . . . . . . . . . . . . . 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 683 . . . . . . . . . . . . . 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 273 . . . . . . . . . . . . 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 487 . . . . . . . . . . . 12  |-  ( ( x  e.  B  /\  { x }  =  {
x } )  -> 
( z  e.  {
x }  ->  z  e.  U. { u  |  E. x  e.  B  u  =  { x } } ) )
7041, 69mpan2 682 . . . . . . . . . . 11  |-  ( x  e.  B  ->  (
z  e.  { x }  ->  z  e.  U. { u  |  E. x  e.  B  u  =  { x } }
) )
7132, 70syl5bir 226 . . . . . . . . . 10  |-  ( x  e.  B  ->  (
z  =  x  -> 
z  e.  U. {
u  |  E. x  e.  B  u  =  { x } }
) )
72 eleq1 2528 . . . . . . . . . 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 224 . . . . . . . . 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 1814 . . . . . . 7  |-  ( [ x  /  z ] z  =  x  ->  [ x  /  z ] ( x  e.  B  ->  x  e.  U. { u  |  E. x  e.  B  u  =  { x } }
) )
76 equsb3 2272 . . . . . . 7  |-  ( [ x  /  z ] z  =  x  <->  x  =  x )
77 nfv 1772 . . . . . . . 8  |-  F/ z ( x  e.  B  ->  x  e.  U. {
u  |  E. x  e.  B  u  =  { x } }
)
7877sbf 2220 . . . . . . 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 273 . . . . . 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 192 . . . 4  |-  ( x  e.  U. { u  |  E. x  e.  B  u  =  { x } }  <->  x  e.  B
)
8211, 81syl6bb 269 . . 3  |-  ( B 
C_  A  ->  (
x  e.  U. ( F " B )  <->  x  e.  B ) )
8382eqrdv 2460 . 2  |-  ( B 
C_  A  ->  U. ( F " B )  =  B )
8483eqcomd 2468 1  |-  ( B 
C_  A  ->  B  =  U. ( F " B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189    /\ wa 375    = wceq 1455   E.wex 1674   F/wnf 1678   [wsb 1808    e. wcel 1898   {cab 2448   E.wrex 2750   _Vcvv 3057   [.wsbc 3279    C_ wss 3416   {csn 3980   U.cuni 4212    |-> cmpt 4475   ran crn 4854    |` cres 4855   "cima 4856
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-sep 4539  ax-nul 4548  ax-pr 4653
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-ral 2754  df-rex 2755  df-rab 2758  df-v 3059  df-sbc 3280  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3744  df-if 3894  df-sn 3981  df-pr 3983  df-op 3987  df-uni 4213  df-br 4417  df-opab 4476  df-mpt 4477  df-xp 4859  df-rel 4860  df-cnv 4861  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866
This theorem is referenced by:  mptsnun  31786
  Copyright terms: Public domain W3C validator