MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ixpsnf1o Unicode version

Theorem ixpsnf1o 7040
Description: A bijection between a class and single-point functions to it. (Contributed by Stefan O'Rear, 24-Jan-2015.)
Hypothesis
Ref Expression
ixpsnf1o.f  |-  F  =  ( x  e.  A  |->  ( { I }  X.  { x } ) )
Assertion
Ref Expression
ixpsnf1o  |-  ( I  e.  V  ->  F : A -1-1-onto-> X_ y  e.  {
I } A )
Distinct variable groups:    x, I,
y    x, A, y    x, V, y    y, F
Allowed substitution hint:    F( x)

Proof of Theorem ixpsnf1o
Dummy variables  a 
b  c are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ixpsnf1o.f . 2  |-  F  =  ( x  e.  A  |->  ( { I }  X.  { x } ) )
2 snex 4348 . . . 4  |-  { I }  e.  _V
3 snex 4348 . . . 4  |-  { x }  e.  _V
42, 3xpex 4932 . . 3  |-  ( { I }  X.  {
x } )  e. 
_V
54a1i 11 . 2  |-  ( ( I  e.  V  /\  x  e.  A )  ->  ( { I }  X.  { x } )  e.  _V )
6 vex 2904 . . . . 5  |-  a  e. 
_V
76rnex 5075 . . . 4  |-  ran  a  e.  _V
87uniex 4647 . . 3  |-  U. ran  a  e.  _V
98a1i 11 . 2  |-  ( ( I  e.  V  /\  a  e.  X_ y  e. 
{ I } A
)  ->  U. ran  a  e.  _V )
10 sneq 3770 . . . . . 6  |-  ( b  =  I  ->  { b }  =  { I } )
1110xpeq1d 4843 . . . . 5  |-  ( b  =  I  ->  ( { b }  X.  { x } )  =  ( { I }  X.  { x }
) )
1211eqeq2d 2400 . . . 4  |-  ( b  =  I  ->  (
a  =  ( { b }  X.  {
x } )  <->  a  =  ( { I }  X.  { x } ) ) )
1312anbi2d 685 . . 3  |-  ( b  =  I  ->  (
( x  e.  A  /\  a  =  ( { b }  X.  { x } ) )  <->  ( x  e.  A  /\  a  =  ( { I }  X.  { x } ) ) ) )
14 vex 2904 . . . . . 6  |-  b  e. 
_V
15 elixpsn 7039 . . . . . 6  |-  ( b  e.  _V  ->  (
a  e.  X_ y  e.  { b } A  <->  E. c  e.  A  a  =  { <. b ,  c >. } ) )
1614, 15ax-mp 8 . . . . 5  |-  ( a  e.  X_ y  e.  {
b } A  <->  E. c  e.  A  a  =  { <. b ,  c
>. } )
1710ixpeq1d 7012 . . . . . 6  |-  ( b  =  I  ->  X_ y  e.  { b } A  =  X_ y  e.  {
I } A )
1817eleq2d 2456 . . . . 5  |-  ( b  =  I  ->  (
a  e.  X_ y  e.  { b } A  <->  a  e.  X_ y  e.  {
I } A ) )
1916, 18syl5bbr 251 . . . 4  |-  ( b  =  I  ->  ( E. c  e.  A  a  =  { <. b ,  c >. }  <->  a  e.  X_ y  e.  { I } A ) )
2019anbi1d 686 . . 3  |-  ( b  =  I  ->  (
( E. c  e.  A  a  =  { <. b ,  c >. }  /\  x  =  U. ran  a )  <->  ( a  e.  X_ y  e.  {
I } A  /\  x  =  U. ran  a
) ) )
21 vex 2904 . . . . . . 7  |-  x  e. 
_V
2214, 21xpsn 5851 . . . . . 6  |-  ( { b }  X.  {
x } )  =  { <. b ,  x >. }
2322eqeq2i 2399 . . . . 5  |-  ( a  =  ( { b }  X.  { x } )  <->  a  =  { <. b ,  x >. } )
2423anbi2i 676 . . . 4  |-  ( ( x  e.  A  /\  a  =  ( {
b }  X.  {
x } ) )  <-> 
( x  e.  A  /\  a  =  { <. b ,  x >. } ) )
25 eqid 2389 . . . . . . . . 9  |-  { <. b ,  x >. }  =  { <. b ,  x >. }
26 opeq2 3929 . . . . . . . . . . . 12  |-  ( c  =  x  ->  <. b ,  c >.  =  <. b ,  x >. )
2726sneqd 3772 . . . . . . . . . . 11  |-  ( c  =  x  ->  { <. b ,  c >. }  =  { <. b ,  x >. } )
2827eqeq2d 2400 . . . . . . . . . 10  |-  ( c  =  x  ->  ( { <. b ,  x >. }  =  { <. b ,  c >. }  <->  { <. b ,  x >. }  =  { <. b ,  x >. } ) )
2928rspcev 2997 . . . . . . . . 9  |-  ( ( x  e.  A  /\  {
<. b ,  x >. }  =  { <. b ,  x >. } )  ->  E. c  e.  A  { <. b ,  x >. }  =  { <. b ,  c >. } )
3025, 29mpan2 653 . . . . . . . 8  |-  ( x  e.  A  ->  E. c  e.  A  { <. b ,  x >. }  =  { <. b ,  c >. } )
3114, 21op2nda 5296 . . . . . . . . 9  |-  U. ran  {
<. b ,  x >. }  =  x
3231eqcomi 2393 . . . . . . . 8  |-  x  = 
U. ran  { <. b ,  x >. }
3330, 32jctir 525 . . . . . . 7  |-  ( x  e.  A  ->  ( E. c  e.  A  { <. b ,  x >. }  =  { <. b ,  c >. }  /\  x  =  U. ran  { <. b ,  x >. } ) )
34 eqeq1 2395 . . . . . . . . 9  |-  ( a  =  { <. b ,  x >. }  ->  (
a  =  { <. b ,  c >. }  <->  { <. b ,  x >. }  =  { <. b ,  c >. } ) )
3534rexbidv 2672 . . . . . . . 8  |-  ( a  =  { <. b ,  x >. }  ->  ( E. c  e.  A  a  =  { <. b ,  c >. }  <->  E. c  e.  A  { <. b ,  x >. }  =  { <. b ,  c >. } ) )
36 rneq 5037 . . . . . . . . . 10  |-  ( a  =  { <. b ,  x >. }  ->  ran  a  =  ran  { <. b ,  x >. } )
3736unieqd 3970 . . . . . . . . 9  |-  ( a  =  { <. b ,  x >. }  ->  U. ran  a  =  U. ran  { <. b ,  x >. } )
3837eqeq2d 2400 . . . . . . . 8  |-  ( a  =  { <. b ,  x >. }  ->  (
x  =  U. ran  a 
<->  x  =  U. ran  {
<. b ,  x >. } ) )
3935, 38anbi12d 692 . . . . . . 7  |-  ( a  =  { <. b ,  x >. }  ->  (
( E. c  e.  A  a  =  { <. b ,  c >. }  /\  x  =  U. ran  a )  <->  ( E. c  e.  A  { <. b ,  x >. }  =  { <. b ,  c >. }  /\  x  =  U. ran  { <. b ,  x >. } ) ) )
4033, 39syl5ibrcom 214 . . . . . 6  |-  ( x  e.  A  ->  (
a  =  { <. b ,  x >. }  ->  ( E. c  e.  A  a  =  { <. b ,  c >. }  /\  x  =  U. ran  a
) ) )
4140imp 419 . . . . 5  |-  ( ( x  e.  A  /\  a  =  { <. b ,  x >. } )  -> 
( E. c  e.  A  a  =  { <. b ,  c >. }  /\  x  =  U. ran  a ) )
42 vex 2904 . . . . . . . . . . 11  |-  c  e. 
_V
4314, 42op2nda 5296 . . . . . . . . . 10  |-  U. ran  {
<. b ,  c >. }  =  c
4443eqeq2i 2399 . . . . . . . . 9  |-  ( x  =  U. ran  { <. b ,  c >. } 
<->  x  =  c )
45 eqidd 2390 . . . . . . . . . . 11  |-  ( c  e.  A  ->  { <. b ,  c >. }  =  { <. b ,  c
>. } )
4645ancli 535 . . . . . . . . . 10  |-  ( c  e.  A  ->  (
c  e.  A  /\  {
<. b ,  c >. }  =  { <. b ,  c >. } ) )
47 eleq1 2449 . . . . . . . . . . 11  |-  ( x  =  c  ->  (
x  e.  A  <->  c  e.  A ) )
48 opeq2 3929 . . . . . . . . . . . . 13  |-  ( x  =  c  ->  <. b ,  x >.  =  <. b ,  c >. )
4948sneqd 3772 . . . . . . . . . . . 12  |-  ( x  =  c  ->  { <. b ,  x >. }  =  { <. b ,  c
>. } )
5049eqeq2d 2400 . . . . . . . . . . 11  |-  ( x  =  c  ->  ( { <. b ,  c
>. }  =  { <. b ,  x >. }  <->  { <. b ,  c >. }  =  { <. b ,  c
>. } ) )
5147, 50anbi12d 692 . . . . . . . . . 10  |-  ( x  =  c  ->  (
( x  e.  A  /\  { <. b ,  c
>. }  =  { <. b ,  x >. } )  <-> 
( c  e.  A  /\  { <. b ,  c
>. }  =  { <. b ,  c >. } ) ) )
5246, 51syl5ibrcom 214 . . . . . . . . 9  |-  ( c  e.  A  ->  (
x  =  c  -> 
( x  e.  A  /\  { <. b ,  c
>. }  =  { <. b ,  x >. } ) ) )
5344, 52syl5bi 209 . . . . . . . 8  |-  ( c  e.  A  ->  (
x  =  U. ran  {
<. b ,  c >. }  ->  ( x  e.  A  /\  { <. b ,  c >. }  =  { <. b ,  x >. } ) ) )
54 rneq 5037 . . . . . . . . . . 11  |-  ( a  =  { <. b ,  c >. }  ->  ran  a  =  ran  { <. b ,  c >. } )
5554unieqd 3970 . . . . . . . . . 10  |-  ( a  =  { <. b ,  c >. }  ->  U.
ran  a  =  U. ran  { <. b ,  c
>. } )
5655eqeq2d 2400 . . . . . . . . 9  |-  ( a  =  { <. b ,  c >. }  ->  ( x  =  U. ran  a 
<->  x  =  U. ran  {
<. b ,  c >. } ) )
57 eqeq1 2395 . . . . . . . . . 10  |-  ( a  =  { <. b ,  c >. }  ->  ( a  =  { <. b ,  x >. }  <->  { <. b ,  c >. }  =  { <. b ,  x >. } ) )
5857anbi2d 685 . . . . . . . . 9  |-  ( a  =  { <. b ,  c >. }  ->  ( ( x  e.  A  /\  a  =  { <. b ,  x >. } )  <->  ( x  e.  A  /\  { <. b ,  c >. }  =  { <. b ,  x >. } ) ) )
5956, 58imbi12d 312 . . . . . . . 8  |-  ( a  =  { <. b ,  c >. }  ->  ( ( x  =  U. ran  a  ->  ( x  e.  A  /\  a  =  { <. b ,  x >. } ) )  <->  ( x  =  U. ran  { <. b ,  c >. }  ->  ( x  e.  A  /\  {
<. b ,  c >. }  =  { <. b ,  x >. } ) ) ) )
6053, 59syl5ibrcom 214 . . . . . . 7  |-  ( c  e.  A  ->  (
a  =  { <. b ,  c >. }  ->  ( x  =  U. ran  a  ->  ( x  e.  A  /\  a  =  { <. b ,  x >. } ) ) ) )
6160rexlimiv 2769 . . . . . 6  |-  ( E. c  e.  A  a  =  { <. b ,  c >. }  ->  ( x  =  U. ran  a  ->  ( x  e.  A  /\  a  =  { <. b ,  x >. } ) ) )
6261imp 419 . . . . 5  |-  ( ( E. c  e.  A  a  =  { <. b ,  c >. }  /\  x  =  U. ran  a
)  ->  ( x  e.  A  /\  a  =  { <. b ,  x >. } ) )
6341, 62impbii 181 . . . 4  |-  ( ( x  e.  A  /\  a  =  { <. b ,  x >. } )  <->  ( E. c  e.  A  a  =  { <. b ,  c
>. }  /\  x  = 
U. ran  a )
)
6424, 63bitri 241 . . 3  |-  ( ( x  e.  A  /\  a  =  ( {
b }  X.  {
x } ) )  <-> 
( E. c  e.  A  a  =  { <. b ,  c >. }  /\  x  =  U. ran  a ) )
6513, 20, 64vtoclbg 2957 . 2  |-  ( I  e.  V  ->  (
( x  e.  A  /\  a  =  ( { I }  X.  { x } ) )  <->  ( a  e.  X_ y  e.  { I } A  /\  x  =  U. ran  a ) ) )
661, 5, 9, 65f1od 6235 1  |-  ( I  e.  V  ->  F : A -1-1-onto-> X_ y  e.  {
I } A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359    = wceq 1649    e. wcel 1717   E.wrex 2652   _Vcvv 2901   {csn 3759   <.cop 3762   U.cuni 3959    e. cmpt 4209    X. cxp 4818   ran crn 4821   -1-1-onto->wf1o 5395   X_cixp 7001
This theorem is referenced by:  mapsnf1o  7041
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-13 1719  ax-14 1721  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2370  ax-sep 4273  ax-nul 4281  ax-pow 4320  ax-pr 4346  ax-un 4643
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2244  df-mo 2245  df-clab 2376  df-cleq 2382  df-clel 2385  df-nfc 2514  df-ne 2554  df-ral 2656  df-rex 2657  df-reu 2658  df-rab 2660  df-v 2903  df-sbc 3107  df-dif 3268  df-un 3270  df-in 3272  df-ss 3279  df-nul 3574  df-if 3685  df-pw 3746  df-sn 3765  df-pr 3766  df-op 3768  df-uni 3960  df-br 4156  df-opab 4210  df-mpt 4211  df-id 4441  df-xp 4826  df-rel 4827  df-cnv 4828  df-co 4829  df-dm 4830  df-rn 4831  df-res 4832  df-ima 4833  df-iota 5360  df-fun 5398  df-fn 5399  df-f 5400  df-f1 5401  df-fo 5402  df-f1o 5403  df-fv 5404  df-ixp 7002
  Copyright terms: Public domain W3C validator