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

Theorem f1omptsnlem 31782
Description: This is the core of the proof of f1omptsn 31783, but to avoid the distinct variables on the definitions, we split this proof into two. (Contributed by ML, 15-Jul-2020.)
Hypotheses
Ref Expression
f1omptsn.f  |-  F  =  ( x  e.  A  |->  { x } )
f1omptsn.r  |-  R  =  { u  |  E. x  e.  A  u  =  { x } }
Assertion
Ref Expression
f1omptsnlem  |-  F : A
-1-1-onto-> R
Distinct variable groups:    x, A, u    x, F    u, R, x
Allowed substitution hint:    F( u)

Proof of Theorem f1omptsnlem
Dummy variable  y is distinct from all other variables.
StepHypRef Expression
1 f1omptsn.f . . . . 5  |-  F  =  ( x  e.  A  |->  { x } )
2 eqid 2461 . . . . . . 7  |-  { x }  =  { x }
3 snex 4654 . . . . . . . 8  |-  { x }  e.  _V
4 eqsbc3 3318 . . . . . . . 8  |-  ( { x }  e.  _V  ->  ( [. { x }  /  u ]. u  =  { x }  <->  { x }  =  { x } ) )
53, 4ax-mp 5 . . . . . . 7  |-  ( [. { x }  /  u ]. u  =  {
x }  <->  { x }  =  { x } )
62, 5mpbir 214 . . . . . 6  |-  [. {
x }  /  u ]. u  =  {
x }
7 sbcel2 3789 . . . . . . . 8  |-  ( [. { x }  /  u ]. x  e.  A  <->  x  e.  [_ { x }  /  u ]_ A
)
8 csbconstg 3387 . . . . . . . . . 10  |-  ( { x }  e.  _V  ->  [_ { x }  /  u ]_ A  =  A )
93, 8ax-mp 5 . . . . . . . . 9  |-  [_ {
x }  /  u ]_ A  =  A
109eleq2i 2531 . . . . . . . 8  |-  ( x  e.  [_ { x }  /  u ]_ A  <->  x  e.  A )
117, 10bitri 257 . . . . . . 7  |-  ( [. { x }  /  u ]. x  e.  A  <->  x  e.  A )
12 df-rex 2754 . . . . . . . . . . . . 13  |-  ( E. x  e.  A  u  =  { x }  <->  E. x ( x  e.  A  /\  u  =  { x } ) )
13 f1omptsn.r . . . . . . . . . . . . . . 15  |-  R  =  { u  |  E. x  e.  A  u  =  { x } }
1413abeq2i 2573 . . . . . . . . . . . . . 14  |-  ( u  e.  R  <->  E. x  e.  A  u  =  { x } )
1514biimpri 211 . . . . . . . . . . . . 13  |-  ( E. x  e.  A  u  =  { x }  ->  u  e.  R )
1612, 15sylbir 218 . . . . . . . . . . . 12  |-  ( E. x ( x  e.  A  /\  u  =  { x } )  ->  u  e.  R
)
171619.23bi 1959 . . . . . . . . . . 11  |-  ( ( x  e.  A  /\  u  =  { x } )  ->  u  e.  R )
1817sbcth 3293 . . . . . . . . . 10  |-  ( { x }  e.  _V  ->  [. { x }  /  u ]. ( ( x  e.  A  /\  u  =  { x } )  ->  u  e.  R ) )
193, 18ax-mp 5 . . . . . . . . 9  |-  [. {
x }  /  u ]. ( ( x  e.  A  /\  u  =  { x } )  ->  u  e.  R
)
20 sbcimg 3320 . . . . . . . . . 10  |-  ( { x }  e.  _V  ->  ( [. { x }  /  u ]. (
( x  e.  A  /\  u  =  {
x } )  ->  u  e.  R )  <->  (
[. { x }  /  u ]. ( x  e.  A  /\  u  =  { x } )  ->  [. { x }  /  u ]. u  e.  R ) ) )
213, 20ax-mp 5 . . . . . . . . 9  |-  ( [. { x }  /  u ]. ( ( x  e.  A  /\  u  =  { x } )  ->  u  e.  R
)  <->  ( [. {
x }  /  u ]. ( x  e.  A  /\  u  =  {
x } )  ->  [. { x }  /  u ]. u  e.  R
) )
2219, 21mpbi 213 . . . . . . . 8  |-  ( [. { x }  /  u ]. ( x  e.  A  /\  u  =  { x } )  ->  [. { x }  /  u ]. u  e.  R )
23 sbcan 3321 . . . . . . . 8  |-  ( [. { x }  /  u ]. ( x  e.  A  /\  u  =  { x } )  <-> 
( [. { x }  /  u ]. x  e.  A  /\  [. {
x }  /  u ]. u  =  {
x } ) )
24 sbcel1v 3337 . . . . . . . 8  |-  ( [. { x }  /  u ]. u  e.  R  <->  { x }  e.  R
)
2522, 23, 243imtr3i 273 . . . . . . 7  |-  ( (
[. { x }  /  u ]. x  e.  A  /\  [. {
x }  /  u ]. u  =  {
x } )  ->  { x }  e.  R )
2611, 25sylanbr 480 . . . . . 6  |-  ( ( x  e.  A  /\  [. { x }  /  u ]. u  =  {
x } )  ->  { x }  e.  R )
276, 26mpan2 682 . . . . 5  |-  ( x  e.  A  ->  { x }  e.  R )
281, 27fmpti 6067 . . . 4  |-  F : A
--> R
291fvmpt2 5979 . . . . . . . . 9  |-  ( ( x  e.  A  /\  { x }  e.  R
)  ->  ( F `  x )  =  {
x } )
3027, 29mpdan 679 . . . . . . . 8  |-  ( x  e.  A  ->  ( F `  x )  =  { x } )
31 sneq 3989 . . . . . . . . 9  |-  ( x  =  y  ->  { x }  =  { y } )
3231, 1, 3fvmpt3i 5975 . . . . . . . 8  |-  ( y  e.  A  ->  ( F `  y )  =  { y } )
3330, 32eqeqan12d 2477 . . . . . . 7  |-  ( ( x  e.  A  /\  y  e.  A )  ->  ( ( F `  x )  =  ( F `  y )  <->  { x }  =  { y } ) )
34 vex 3059 . . . . . . . 8  |-  x  e. 
_V
35 sneqbg 4154 . . . . . . . 8  |-  ( x  e.  _V  ->  ( { x }  =  { y }  <->  x  =  y ) )
3634, 35ax-mp 5 . . . . . . 7  |-  ( { x }  =  {
y }  <->  x  =  y )
3733, 36syl6bb 269 . . . . . 6  |-  ( ( x  e.  A  /\  y  e.  A )  ->  ( ( F `  x )  =  ( F `  y )  <-> 
x  =  y ) )
3837biimpd 212 . . . . 5  |-  ( ( x  e.  A  /\  y  e.  A )  ->  ( ( F `  x )  =  ( F `  y )  ->  x  =  y ) )
3938rgen2a 2826 . . . 4  |-  A. x  e.  A  A. y  e.  A  ( ( F `  x )  =  ( F `  y )  ->  x  =  y )
40 dff13 6183 . . . 4  |-  ( F : A -1-1-> R  <->  ( F : A --> R  /\  A. x  e.  A  A. y  e.  A  (
( F `  x
)  =  ( F `
 y )  ->  x  =  y )
) )
4128, 39, 40mpbir2an 936 . . 3  |-  F : A -1-1-> R
42 f1f1orn 5847 . . 3  |-  ( F : A -1-1-> R  ->  F : A -1-1-onto-> ran  F )
4341, 42ax-mp 5 . 2  |-  F : A
-1-1-onto-> ran  F
44 rnmptsn 31781 . . . 4  |-  ran  (
x  e.  A  |->  { x } )  =  { u  |  E. x  e.  A  u  =  { x } }
451rneqi 5079 . . . 4  |-  ran  F  =  ran  ( x  e.  A  |->  { x }
)
4644, 45, 133eqtr4i 2493 . . 3  |-  ran  F  =  R
47 f1oeq3 5829 . . 3  |-  ( ran 
F  =  R  -> 
( F : A -1-1-onto-> ran  F  <-> 
F : A -1-1-onto-> R ) )
4846, 47ax-mp 5 . 2  |-  ( F : A -1-1-onto-> ran  F  <->  F : A
-1-1-onto-> R )
4943, 48mpbi 213 1  |-  F : A
-1-1-onto-> R
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189    /\ wa 375    = wceq 1454   E.wex 1673    e. wcel 1897   {cab 2447   A.wral 2748   E.wrex 2749   _Vcvv 3056   [.wsbc 3278   [_csb 3374   {csn 3979    |-> cmpt 4474   ran crn 4853   -->wf 5596   -1-1->wf1 5597   -1-1-onto->wf1o 5599   ` cfv 5600
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-8 1899  ax-9 1906  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441  ax-sep 4538  ax-nul 4547  ax-pow 4594  ax-pr 4652
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1457  df-fal 1460  df-ex 1674  df-nf 1678  df-sb 1808  df-eu 2313  df-mo 2314  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-ne 2634  df-ral 2753  df-rex 2754  df-rab 2757  df-v 3058  df-sbc 3279  df-csb 3375  df-dif 3418  df-un 3420  df-in 3422  df-ss 3429  df-nul 3743  df-if 3893  df-sn 3980  df-pr 3982  df-op 3986  df-uni 4212  df-br 4416  df-opab 4475  df-mpt 4476  df-id 4767  df-xp 4858  df-rel 4859  df-cnv 4860  df-co 4861  df-dm 4862  df-rn 4863  df-res 4864  df-ima 4865  df-iota 5564  df-fun 5602  df-fn 5603  df-f 5604  df-f1 5605  df-fo 5606  df-f1o 5607  df-fv 5608
This theorem is referenced by:  f1omptsn  31783
  Copyright terms: Public domain W3C validator