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

Theorem ac6sfi 7310
Description: A version of ac6s 8320 for finite sets. (Contributed by Jeffrey Hankins, 26-Jun-2009.) (Proof shortened by Mario Carneiro, 29-Jan-2014.)
Hypothesis
Ref Expression
ac6sfi.1  |-  ( y  =  ( f `  x )  ->  ( ph 
<->  ps ) )
Assertion
Ref Expression
ac6sfi  |-  ( ( A  e.  Fin  /\  A. x  e.  A  E. y  e.  B  ph )  ->  E. f ( f : A --> B  /\  A. x  e.  A  ps ) )
Distinct variable groups:    x, f, A    y, f, B, x    ph, f    ps, y
Allowed substitution hints:    ph( x, y)    ps( x, f)    A( y)

Proof of Theorem ac6sfi
Dummy variables  u  w  z  g are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 raleq 2864 . . . 4  |-  ( u  =  (/)  ->  ( A. x  e.  u  E. y  e.  B  ph  <->  A. x  e.  (/)  E. y  e.  B  ph ) )
2 feq2 5536 . . . . . 6  |-  ( u  =  (/)  ->  ( f : u --> B  <->  f : (/) --> B ) )
3 raleq 2864 . . . . . 6  |-  ( u  =  (/)  ->  ( A. x  e.  u  ps  <->  A. x  e.  (/)  ps )
)
42, 3anbi12d 692 . . . . 5  |-  ( u  =  (/)  ->  ( ( f : u --> B  /\  A. x  e.  u  ps ) 
<->  ( f : (/) --> B  /\  A. x  e.  (/)  ps ) ) )
54exbidv 1633 . . . 4  |-  ( u  =  (/)  ->  ( E. f ( f : u --> B  /\  A. x  e.  u  ps ) 
<->  E. f ( f : (/) --> B  /\  A. x  e.  (/)  ps )
) )
61, 5imbi12d 312 . . 3  |-  ( u  =  (/)  ->  ( ( A. x  e.  u  E. y  e.  B  ph 
->  E. f ( f : u --> B  /\  A. x  e.  u  ps ) )  <->  ( A. x  e.  (/)  E. y  e.  B  ph  ->  E. f
( f : (/) --> B  /\  A. x  e.  (/)  ps ) ) ) )
7 raleq 2864 . . . 4  |-  ( u  =  w  ->  ( A. x  e.  u  E. y  e.  B  ph  <->  A. x  e.  w  E. y  e.  B  ph )
)
8 feq2 5536 . . . . . 6  |-  ( u  =  w  ->  (
f : u --> B  <->  f :
w --> B ) )
9 raleq 2864 . . . . . 6  |-  ( u  =  w  ->  ( A. x  e.  u  ps 
<-> 
A. x  e.  w  ps ) )
108, 9anbi12d 692 . . . . 5  |-  ( u  =  w  ->  (
( f : u --> B  /\  A. x  e.  u  ps )  <->  ( f : w --> B  /\  A. x  e.  w  ps ) ) )
1110exbidv 1633 . . . 4  |-  ( u  =  w  ->  ( E. f ( f : u --> B  /\  A. x  e.  u  ps ) 
<->  E. f ( f : w --> B  /\  A. x  e.  w  ps ) ) )
127, 11imbi12d 312 . . 3  |-  ( u  =  w  ->  (
( A. x  e.  u  E. y  e.  B  ph  ->  E. f
( f : u --> B  /\  A. x  e.  u  ps )
)  <->  ( A. x  e.  w  E. y  e.  B  ph  ->  E. f
( f : w --> B  /\  A. x  e.  w  ps )
) ) )
13 raleq 2864 . . . 4  |-  ( u  =  ( w  u. 
{ z } )  ->  ( A. x  e.  u  E. y  e.  B  ph  <->  A. x  e.  ( w  u.  {
z } ) E. y  e.  B  ph ) )
14 feq2 5536 . . . . . . 7  |-  ( u  =  ( w  u. 
{ z } )  ->  ( f : u --> B  <->  f :
( w  u.  {
z } ) --> B ) )
15 raleq 2864 . . . . . . 7  |-  ( u  =  ( w  u. 
{ z } )  ->  ( A. x  e.  u  ps  <->  A. x  e.  ( w  u.  {
z } ) ps ) )
1614, 15anbi12d 692 . . . . . 6  |-  ( u  =  ( w  u. 
{ z } )  ->  ( ( f : u --> B  /\  A. x  e.  u  ps ) 
<->  ( f : ( w  u.  { z } ) --> B  /\  A. x  e.  ( w  u.  { z } ) ps ) ) )
1716exbidv 1633 . . . . 5  |-  ( u  =  ( w  u. 
{ z } )  ->  ( E. f
( f : u --> B  /\  A. x  e.  u  ps )  <->  E. f ( f : ( w  u.  {
z } ) --> B  /\  A. x  e.  ( w  u.  {
z } ) ps ) ) )
18 feq1 5535 . . . . . . 7  |-  ( f  =  g  ->  (
f : ( w  u.  { z } ) --> B  <->  g :
( w  u.  {
z } ) --> B ) )
19 fvex 5701 . . . . . . . . . 10  |-  ( f `
 x )  e. 
_V
20 ac6sfi.1 . . . . . . . . . 10  |-  ( y  =  ( f `  x )  ->  ( ph 
<->  ps ) )
2119, 20sbcie 3155 . . . . . . . . 9  |-  ( [. ( f `  x
)  /  y ]. ph  <->  ps )
22 fveq1 5686 . . . . . . . . . 10  |-  ( f  =  g  ->  (
f `  x )  =  ( g `  x ) )
23 dfsbcq 3123 . . . . . . . . . 10  |-  ( ( f `  x )  =  ( g `  x )  ->  ( [. ( f `  x
)  /  y ]. ph  <->  [. ( g `  x
)  /  y ]. ph ) )
2422, 23syl 16 . . . . . . . . 9  |-  ( f  =  g  ->  ( [. ( f `  x
)  /  y ]. ph  <->  [. ( g `  x
)  /  y ]. ph ) )
2521, 24syl5bbr 251 . . . . . . . 8  |-  ( f  =  g  ->  ( ps 
<-> 
[. ( g `  x )  /  y ]. ph ) )
2625ralbidv 2686 . . . . . . 7  |-  ( f  =  g  ->  ( A. x  e.  (
w  u.  { z } ) ps  <->  A. x  e.  ( w  u.  {
z } ) [. ( g `  x
)  /  y ]. ph ) )
2718, 26anbi12d 692 . . . . . 6  |-  ( f  =  g  ->  (
( f : ( w  u.  { z } ) --> B  /\  A. x  e.  ( w  u.  { z } ) ps )  <->  ( g : ( w  u. 
{ z } ) --> B  /\  A. x  e.  ( w  u.  {
z } ) [. ( g `  x
)  /  y ]. ph ) ) )
2827cbvexv 2053 . . . . 5  |-  ( E. f ( f : ( w  u.  {
z } ) --> B  /\  A. x  e.  ( w  u.  {
z } ) ps )  <->  E. g ( g : ( w  u. 
{ z } ) --> B  /\  A. x  e.  ( w  u.  {
z } ) [. ( g `  x
)  /  y ]. ph ) )
2917, 28syl6bb 253 . . . 4  |-  ( u  =  ( w  u. 
{ z } )  ->  ( E. f
( f : u --> B  /\  A. x  e.  u  ps )  <->  E. g ( g : ( w  u.  {
z } ) --> B  /\  A. x  e.  ( w  u.  {
z } ) [. ( g `  x
)  /  y ]. ph ) ) )
3013, 29imbi12d 312 . . 3  |-  ( u  =  ( w  u. 
{ z } )  ->  ( ( A. x  e.  u  E. y  e.  B  ph  ->  E. f ( f : u --> B  /\  A. x  e.  u  ps ) )  <->  ( A. x  e.  ( w  u.  { z } ) E. y  e.  B  ph 
->  E. g ( g : ( w  u. 
{ z } ) --> B  /\  A. x  e.  ( w  u.  {
z } ) [. ( g `  x
)  /  y ]. ph ) ) ) )
31 raleq 2864 . . . 4  |-  ( u  =  A  ->  ( A. x  e.  u  E. y  e.  B  ph  <->  A. x  e.  A  E. y  e.  B  ph )
)
32 feq2 5536 . . . . . 6  |-  ( u  =  A  ->  (
f : u --> B  <->  f : A
--> B ) )
33 raleq 2864 . . . . . 6  |-  ( u  =  A  ->  ( A. x  e.  u  ps 
<-> 
A. x  e.  A  ps ) )
3432, 33anbi12d 692 . . . . 5  |-  ( u  =  A  ->  (
( f : u --> B  /\  A. x  e.  u  ps )  <->  ( f : A --> B  /\  A. x  e.  A  ps ) ) )
3534exbidv 1633 . . . 4  |-  ( u  =  A  ->  ( E. f ( f : u --> B  /\  A. x  e.  u  ps ) 
<->  E. f ( f : A --> B  /\  A. x  e.  A  ps ) ) )
3631, 35imbi12d 312 . . 3  |-  ( u  =  A  ->  (
( A. x  e.  u  E. y  e.  B  ph  ->  E. f
( f : u --> B  /\  A. x  e.  u  ps )
)  <->  ( A. x  e.  A  E. y  e.  B  ph  ->  E. f
( f : A --> B  /\  A. x  e.  A  ps ) ) ) )
37 f0 5586 . . . 4  |-  (/) : (/) --> B
38 0ex 4299 . . . . 5  |-  (/)  e.  _V
39 ral0 3692 . . . . . . 7  |-  A. x  e.  (/)  ps
4039biantru 492 . . . . . 6  |-  ( f : (/) --> B  <->  ( f : (/) --> B  /\  A. x  e.  (/)  ps )
)
41 feq1 5535 . . . . . 6  |-  ( f  =  (/)  ->  ( f : (/) --> B  <->  (/) : (/) --> B ) )
4240, 41syl5bbr 251 . . . . 5  |-  ( f  =  (/)  ->  ( ( f : (/) --> B  /\  A. x  e.  (/)  ps )  <->  (/) :
(/) --> B ) )
4338, 42spcev 3003 . . . 4  |-  ( (/) :
(/) --> B  ->  E. f
( f : (/) --> B  /\  A. x  e.  (/)  ps ) )
4437, 43mp1i 12 . . 3  |-  ( A. x  e.  (/)  E. y  e.  B  ph  ->  E. f
( f : (/) --> B  /\  A. x  e.  (/)  ps ) )
45 ssun1 3470 . . . . . . 7  |-  w  C_  ( w  u.  { z } )
46 ssralv 3367 . . . . . . 7  |-  ( w 
C_  ( w  u. 
{ z } )  ->  ( A. x  e.  ( w  u.  {
z } ) E. y  e.  B  ph  ->  A. x  e.  w  E. y  e.  B  ph ) )
4745, 46ax-mp 8 . . . . . 6  |-  ( A. x  e.  ( w  u.  { z } ) E. y  e.  B  ph 
->  A. x  e.  w  E. y  e.  B  ph )
4847imim1i 56 . . . . 5  |-  ( ( A. x  e.  w  E. y  e.  B  ph 
->  E. f ( f : w --> B  /\  A. x  e.  w  ps ) )  ->  ( A. x  e.  (
w  u.  { z } ) E. y  e.  B  ph  ->  E. f
( f : w --> B  /\  A. x  e.  w  ps )
) )
49 ssun2 3471 . . . . . . . . 9  |-  { z }  C_  ( w  u.  { z } )
50 ssralv 3367 . . . . . . . . 9  |-  ( { z }  C_  (
w  u.  { z } )  ->  ( A. x  e.  (
w  u.  { z } ) E. y  e.  B  ph  ->  A. x  e.  { z } E. y  e.  B  ph )
)
5149, 50ax-mp 8 . . . . . . . 8  |-  ( A. x  e.  ( w  u.  { z } ) E. y  e.  B  ph 
->  A. x  e.  {
z } E. y  e.  B  ph )
52 vex 2919 . . . . . . . . . 10  |-  z  e. 
_V
53 ralsns 3804 . . . . . . . . . 10  |-  ( z  e.  _V  ->  ( A. x  e.  { z } E. y  e.  B  ph  <->  [. z  /  x ]. E. y  e.  B  ph ) )
5452, 53ax-mp 8 . . . . . . . . 9  |-  ( A. x  e.  { z } E. y  e.  B  ph  <->  [. z  /  x ]. E. y  e.  B  ph )
55 sbcrexg 3196 . . . . . . . . . 10  |-  ( z  e.  _V  ->  ( [. z  /  x ]. E. y  e.  B  ph  <->  E. y  e.  B  [. z  /  x ]. ph )
)
5652, 55ax-mp 8 . . . . . . . . 9  |-  ( [. z  /  x ]. E. y  e.  B  ph  <->  E. y  e.  B  [. z  /  x ]. ph )
5754, 56bitri 241 . . . . . . . 8  |-  ( A. x  e.  { z } E. y  e.  B  ph  <->  E. y  e.  B  [. z  /  x ]. ph )
5851, 57sylib 189 . . . . . . 7  |-  ( A. x  e.  ( w  u.  { z } ) E. y  e.  B  ph 
->  E. y  e.  B  [. z  /  x ]. ph )
59 nfv 1626 . . . . . . . 8  |-  F/ y  -.  z  e.  w
60 nfv 1626 . . . . . . . . 9  |-  F/ y E. f ( f : w --> B  /\  A. x  e.  w  ps )
61 nfv 1626 . . . . . . . . . . 11  |-  F/ y  g : ( w  u.  { z } ) --> B
62 nfcv 2540 . . . . . . . . . . . 12  |-  F/_ y
( w  u.  {
z } )
63 nfsbc1v 3140 . . . . . . . . . . . 12  |-  F/ y
[. ( g `  x )  /  y ]. ph
6462, 63nfral 2719 . . . . . . . . . . 11  |-  F/ y A. x  e.  ( w  u.  { z } ) [. (
g `  x )  /  y ]. ph
6561, 64nfan 1842 . . . . . . . . . 10  |-  F/ y ( g : ( w  u.  { z } ) --> B  /\  A. x  e.  ( w  u.  { z } ) [. ( g `
 x )  / 
y ]. ph )
6665nfex 1861 . . . . . . . . 9  |-  F/ y E. g ( g : ( w  u. 
{ z } ) --> B  /\  A. x  e.  ( w  u.  {
z } ) [. ( g `  x
)  /  y ]. ph )
6760, 66nfim 1828 . . . . . . . 8  |-  F/ y ( E. f ( f : w --> B  /\  A. x  e.  w  ps )  ->  E. g ( g : ( w  u. 
{ z } ) --> B  /\  A. x  e.  ( w  u.  {
z } ) [. ( g `  x
)  /  y ]. ph ) )
68 simprl 733 . . . . . . . . . . . . 13  |-  ( ( ( -.  z  e.  w  /\  y  e.  B  /\  [. z  /  x ]. ph )  /\  ( f : w --> B  /\  A. x  e.  w  ps )
)  ->  f :
w --> B )
69 vex 2919 . . . . . . . . . . . . . . . 16  |-  y  e. 
_V
7052, 69f1osn 5674 . . . . . . . . . . . . . . 15  |-  { <. z ,  y >. } : { z } -1-1-onto-> { y }
71 f1of 5633 . . . . . . . . . . . . . . 15  |-  ( {
<. z ,  y >. } : { z } -1-1-onto-> { y }  ->  { <. z ,  y >. } : { z } --> { y } )
7270, 71mp1i 12 . . . . . . . . . . . . . 14  |-  ( ( ( -.  z  e.  w  /\  y  e.  B  /\  [. z  /  x ]. ph )  /\  ( f : w --> B  /\  A. x  e.  w  ps )
)  ->  { <. z ,  y >. } : { z } --> { y } )
73 simpl2 961 . . . . . . . . . . . . . . 15  |-  ( ( ( -.  z  e.  w  /\  y  e.  B  /\  [. z  /  x ]. ph )  /\  ( f : w --> B  /\  A. x  e.  w  ps )
)  ->  y  e.  B )
7473snssd 3903 . . . . . . . . . . . . . 14  |-  ( ( ( -.  z  e.  w  /\  y  e.  B  /\  [. z  /  x ]. ph )  /\  ( f : w --> B  /\  A. x  e.  w  ps )
)  ->  { y }  C_  B )
75 fss 5558 . . . . . . . . . . . . . 14  |-  ( ( { <. z ,  y
>. } : { z } --> { y }  /\  { y } 
C_  B )  ->  { <. z ,  y
>. } : { z } --> B )
7672, 74, 75syl2anc 643 . . . . . . . . . . . . 13  |-  ( ( ( -.  z  e.  w  /\  y  e.  B  /\  [. z  /  x ]. ph )  /\  ( f : w --> B  /\  A. x  e.  w  ps )
)  ->  { <. z ,  y >. } : { z } --> B )
77 simpl1 960 . . . . . . . . . . . . . 14  |-  ( ( ( -.  z  e.  w  /\  y  e.  B  /\  [. z  /  x ]. ph )  /\  ( f : w --> B  /\  A. x  e.  w  ps )
)  ->  -.  z  e.  w )
78 disjsn 3828 . . . . . . . . . . . . . 14  |-  ( ( w  i^i  { z } )  =  (/)  <->  -.  z  e.  w )
7977, 78sylibr 204 . . . . . . . . . . . . 13  |-  ( ( ( -.  z  e.  w  /\  y  e.  B  /\  [. z  /  x ]. ph )  /\  ( f : w --> B  /\  A. x  e.  w  ps )
)  ->  ( w  i^i  { z } )  =  (/) )
80 fun2 5567 . . . . . . . . . . . . 13  |-  ( ( ( f : w --> B  /\  { <. z ,  y >. } : { z } --> B )  /\  ( w  i^i 
{ z } )  =  (/) )  ->  (
f  u.  { <. z ,  y >. } ) : ( w  u. 
{ z } ) --> B )
8168, 76, 79, 80syl21anc 1183 . . . . . . . . . . . 12  |-  ( ( ( -.  z  e.  w  /\  y  e.  B  /\  [. z  /  x ]. ph )  /\  ( f : w --> B  /\  A. x  e.  w  ps )
)  ->  ( f  u.  { <. z ,  y
>. } ) : ( w  u.  { z } ) --> B )
82 simprr 734 . . . . . . . . . . . . . 14  |-  ( ( ( -.  z  e.  w  /\  y  e.  B  /\  [. z  /  x ]. ph )  /\  ( f : w --> B  /\  A. x  e.  w  ps )
)  ->  A. x  e.  w  ps )
83 eleq1a 2473 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  w  ->  (
z  =  x  -> 
z  e.  w ) )
8483necon3bd 2604 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  w  ->  ( -.  z  e.  w  ->  z  =/=  x ) )
8584impcom 420 . . . . . . . . . . . . . . . . 17  |-  ( ( -.  z  e.  w  /\  x  e.  w
)  ->  z  =/=  x )
86 fvunsn 5884 . . . . . . . . . . . . . . . . 17  |-  ( z  =/=  x  ->  (
( f  u.  { <. z ,  y >. } ) `  x
)  =  ( f `
 x ) )
87 dfsbcq 3123 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( f  u.  { <. z ,  y >. } ) `  x
)  =  ( f `
 x )  -> 
( [. ( ( f  u.  { <. z ,  y >. } ) `
 x )  / 
y ]. ph  <->  [. ( f `
 x )  / 
y ]. ph ) )
8887, 21syl6rbb 254 . . . . . . . . . . . . . . . . 17  |-  ( ( ( f  u.  { <. z ,  y >. } ) `  x
)  =  ( f `
 x )  -> 
( ps  <->  [. ( ( f  u.  { <. z ,  y >. } ) `
 x )  / 
y ]. ph ) )
8985, 86, 883syl 19 . . . . . . . . . . . . . . . 16  |-  ( ( -.  z  e.  w  /\  x  e.  w
)  ->  ( ps  <->  [. ( ( f  u. 
{ <. z ,  y
>. } ) `  x
)  /  y ]. ph ) )
9089ralbidva 2682 . . . . . . . . . . . . . . 15  |-  ( -.  z  e.  w  -> 
( A. x  e.  w  ps  <->  A. x  e.  w  [. ( ( f  u.  { <. z ,  y >. } ) `
 x )  / 
y ]. ph ) )
9177, 90syl 16 . . . . . . . . . . . . . 14  |-  ( ( ( -.  z  e.  w  /\  y  e.  B  /\  [. z  /  x ]. ph )  /\  ( f : w --> B  /\  A. x  e.  w  ps )
)  ->  ( A. x  e.  w  ps  <->  A. x  e.  w  [. ( ( f  u. 
{ <. z ,  y
>. } ) `  x
)  /  y ]. ph ) )
9282, 91mpbid 202 . . . . . . . . . . . . 13  |-  ( ( ( -.  z  e.  w  /\  y  e.  B  /\  [. z  /  x ]. ph )  /\  ( f : w --> B  /\  A. x  e.  w  ps )
)  ->  A. x  e.  w  [. ( ( f  u.  { <. z ,  y >. } ) `
 x )  / 
y ]. ph )
93 simpl3 962 . . . . . . . . . . . . . 14  |-  ( ( ( -.  z  e.  w  /\  y  e.  B  /\  [. z  /  x ]. ph )  /\  ( f : w --> B  /\  A. x  e.  w  ps )
)  ->  [. z  /  x ]. ph )
94 ffun 5552 . . . . . . . . . . . . . . . . 17  |-  ( ( f  u.  { <. z ,  y >. } ) : ( w  u. 
{ z } ) --> B  ->  Fun  ( f  u.  { <. z ,  y >. } ) )
95 ssun2 3471 . . . . . . . . . . . . . . . . . 18  |-  { <. z ,  y >. }  C_  ( f  u.  { <. z ,  y >. } )
9652snid 3801 . . . . . . . . . . . . . . . . . . 19  |-  z  e. 
{ z }
9769dmsnop 5303 . . . . . . . . . . . . . . . . . . 19  |-  dom  { <. z ,  y >. }  =  { z }
9896, 97eleqtrri 2477 . . . . . . . . . . . . . . . . . 18  |-  z  e. 
dom  { <. z ,  y
>. }
99 funssfv 5705 . . . . . . . . . . . . . . . . . 18  |-  ( ( Fun  ( f  u. 
{ <. z ,  y
>. } )  /\  { <. z ,  y >. }  C_  ( f  u. 
{ <. z ,  y
>. } )  /\  z  e.  dom  { <. z ,  y >. } )  ->  ( ( f  u.  { <. z ,  y >. } ) `
 z )  =  ( { <. z ,  y >. } `  z ) )
10095, 98, 99mp3an23 1271 . . . . . . . . . . . . . . . . 17  |-  ( Fun  ( f  u.  { <. z ,  y >. } )  ->  (
( f  u.  { <. z ,  y >. } ) `  z
)  =  ( {
<. z ,  y >. } `  z )
)
10181, 94, 1003syl 19 . . . . . . . . . . . . . . . 16  |-  ( ( ( -.  z  e.  w  /\  y  e.  B  /\  [. z  /  x ]. ph )  /\  ( f : w --> B  /\  A. x  e.  w  ps )
)  ->  ( (
f  u.  { <. z ,  y >. } ) `
 z )  =  ( { <. z ,  y >. } `  z ) )
10252, 69fvsn 5885 . . . . . . . . . . . . . . . 16  |-  ( {
<. z ,  y >. } `  z )  =  y
103101, 102syl6req 2453 . . . . . . . . . . . . . . 15  |-  ( ( ( -.  z  e.  w  /\  y  e.  B  /\  [. z  /  x ]. ph )  /\  ( f : w --> B  /\  A. x  e.  w  ps )
)  ->  y  =  ( ( f  u. 
{ <. z ,  y
>. } ) `  z
) )
104 ralsns 3804 . . . . . . . . . . . . . . . . 17  |-  ( z  e.  _V  ->  ( A. x  e.  { z } ph  <->  [. z  /  x ]. ph ) )
10552, 104ax-mp 8 . . . . . . . . . . . . . . . 16  |-  ( A. x  e.  { z } ph  <->  [. z  /  x ]. ph )
106 elsni 3798 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  e.  { z }  ->  x  =  z )
107106fveq2d 5691 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  e.  { z }  ->  ( ( f  u.  { <. z ,  y >. } ) `
 x )  =  ( ( f  u. 
{ <. z ,  y
>. } ) `  z
) )
108107eqeq2d 2415 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  { z }  ->  ( y  =  ( ( f  u. 
{ <. z ,  y
>. } ) `  x
)  <->  y  =  ( ( f  u.  { <. z ,  y >. } ) `  z
) ) )
109108biimparc 474 . . . . . . . . . . . . . . . . . 18  |-  ( ( y  =  ( ( f  u.  { <. z ,  y >. } ) `
 z )  /\  x  e.  { z } )  ->  y  =  ( ( f  u.  { <. z ,  y >. } ) `
 x ) )
110 sbceq1a 3131 . . . . . . . . . . . . . . . . . 18  |-  ( y  =  ( ( f  u.  { <. z ,  y >. } ) `
 x )  -> 
( ph  <->  [. ( ( f  u.  { <. z ,  y >. } ) `
 x )  / 
y ]. ph ) )
111109, 110syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ( y  =  ( ( f  u.  { <. z ,  y >. } ) `
 z )  /\  x  e.  { z } )  ->  ( ph 
<-> 
[. ( ( f  u.  { <. z ,  y >. } ) `
 x )  / 
y ]. ph ) )
112111ralbidva 2682 . . . . . . . . . . . . . . . 16  |-  ( y  =  ( ( f  u.  { <. z ,  y >. } ) `
 z )  -> 
( A. x  e. 
{ z } ph  <->  A. x  e.  { z } [. ( ( f  u.  { <. z ,  y >. } ) `
 x )  / 
y ]. ph ) )
113105, 112syl5bbr 251 . . . . . . . . . . . . . . 15  |-  ( y  =  ( ( f  u.  { <. z ,  y >. } ) `
 z )  -> 
( [. z  /  x ]. ph  <->  A. x  e.  {
z } [. (
( f  u.  { <. z ,  y >. } ) `  x
)  /  y ]. ph ) )
114103, 113syl 16 . . . . . . . . . . . . . 14  |-  ( ( ( -.  z  e.  w  /\  y  e.  B  /\  [. z  /  x ]. ph )  /\  ( f : w --> B  /\  A. x  e.  w  ps )
)  ->  ( [. z  /  x ]. ph  <->  A. x  e.  { z } [. ( ( f  u. 
{ <. z ,  y
>. } ) `  x
)  /  y ]. ph ) )
11593, 114mpbid 202 . . . . . . . . . . . . 13  |-  ( ( ( -.  z  e.  w  /\  y  e.  B  /\  [. z  /  x ]. ph )  /\  ( f : w --> B  /\  A. x  e.  w  ps )
)  ->  A. x  e.  { z } [. ( ( f  u. 
{ <. z ,  y
>. } ) `  x
)  /  y ]. ph )
116 ralun 3489 . . . . . . . . . . . . 13  |-  ( ( A. x  e.  w  [. ( ( f  u. 
{ <. z ,  y
>. } ) `  x
)  /  y ]. ph 
/\  A. x  e.  {
z } [. (
( f  u.  { <. z ,  y >. } ) `  x
)  /  y ]. ph )  ->  A. x  e.  ( w  u.  {
z } ) [. ( ( f  u. 
{ <. z ,  y
>. } ) `  x
)  /  y ]. ph )
11792, 115, 116syl2anc 643 . . . . . . . . . . . 12  |-  ( ( ( -.  z  e.  w  /\  y  e.  B  /\  [. z  /  x ]. ph )  /\  ( f : w --> B  /\  A. x  e.  w  ps )
)  ->  A. x  e.  ( w  u.  {
z } ) [. ( ( f  u. 
{ <. z ,  y
>. } ) `  x
)  /  y ]. ph )
118 vex 2919 . . . . . . . . . . . . . 14  |-  f  e. 
_V
119 snex 4365 . . . . . . . . . . . . . 14  |-  { <. z ,  y >. }  e.  _V
120118, 119unex 4666 . . . . . . . . . . . . 13  |-  ( f  u.  { <. z ,  y >. } )  e.  _V
121 feq1 5535 . . . . . . . . . . . . . 14  |-  ( g  =  ( f  u. 
{ <. z ,  y
>. } )  ->  (
g : ( w  u.  { z } ) --> B  <->  ( f  u.  { <. z ,  y
>. } ) : ( w  u.  { z } ) --> B ) )
122 fveq1 5686 . . . . . . . . . . . . . . . 16  |-  ( g  =  ( f  u. 
{ <. z ,  y
>. } )  ->  (
g `  x )  =  ( ( f  u.  { <. z ,  y >. } ) `
 x ) )
123 dfsbcq 3123 . . . . . . . . . . . . . . . 16  |-  ( ( g `  x )  =  ( ( f  u.  { <. z ,  y >. } ) `
 x )  -> 
( [. ( g `  x )  /  y ]. ph  <->  [. ( ( f  u.  { <. z ,  y >. } ) `
 x )  / 
y ]. ph ) )
124122, 123syl 16 . . . . . . . . . . . . . . 15  |-  ( g  =  ( f  u. 
{ <. z ,  y
>. } )  ->  ( [. ( g `  x
)  /  y ]. ph  <->  [. ( ( f  u. 
{ <. z ,  y
>. } ) `  x
)  /  y ]. ph ) )
125124ralbidv 2686 . . . . . . . . . . . . . 14  |-  ( g  =  ( f  u. 
{ <. z ,  y
>. } )  ->  ( A. x  e.  (
w  u.  { z } ) [. (
g `  x )  /  y ]. ph  <->  A. x  e.  ( w  u.  {
z } ) [. ( ( f  u. 
{ <. z ,  y
>. } ) `  x
)  /  y ]. ph ) )
126121, 125anbi12d 692 . . . . . . . . . . . . 13  |-  ( g  =  ( f  u. 
{ <. z ,  y
>. } )  ->  (
( g : ( w  u.  { z } ) --> B  /\  A. x  e.  ( w  u.  { z } ) [. ( g `
 x )  / 
y ]. ph )  <->  ( (
f  u.  { <. z ,  y >. } ) : ( w  u. 
{ z } ) --> B  /\  A. x  e.  ( w  u.  {
z } ) [. ( ( f  u. 
{ <. z ,  y
>. } ) `  x
)  /  y ]. ph ) ) )
127120, 126spcev 3003 . . . . . . . . . . . 12  |-  ( ( ( f  u.  { <. z ,  y >. } ) : ( w  u.  { z } ) --> B  /\  A. x  e.  ( w  u.  { z } ) [. ( ( f  u.  { <. z ,  y >. } ) `
 x )  / 
y ]. ph )  ->  E. g ( g : ( w  u.  {
z } ) --> B  /\  A. x  e.  ( w  u.  {
z } ) [. ( g `  x
)  /  y ]. ph ) )
12881, 117, 127syl2anc 643 . . . . . . . . . . 11  |-  ( ( ( -.  z  e.  w  /\  y  e.  B  /\  [. z  /  x ]. ph )  /\  ( f : w --> B  /\  A. x  e.  w  ps )
)  ->  E. g
( g : ( w  u.  { z } ) --> B  /\  A. x  e.  ( w  u.  { z } ) [. ( g `
 x )  / 
y ]. ph ) )
129128ex 424 . . . . . . . . . 10  |-  ( ( -.  z  e.  w  /\  y  e.  B  /\  [. z  /  x ]. ph )  ->  (
( f : w --> B  /\  A. x  e.  w  ps )  ->  E. g ( g : ( w  u. 
{ z } ) --> B  /\  A. x  e.  ( w  u.  {
z } ) [. ( g `  x
)  /  y ]. ph ) ) )
130129exlimdv 1643 . . . . . . . . 9  |-  ( ( -.  z  e.  w  /\  y  e.  B  /\  [. z  /  x ]. ph )  ->  ( E. f ( f : w --> B  /\  A. x  e.  w  ps )  ->  E. g ( g : ( w  u. 
{ z } ) --> B  /\  A. x  e.  ( w  u.  {
z } ) [. ( g `  x
)  /  y ]. ph ) ) )
1311303exp 1152 . . . . . . . 8  |-  ( -.  z  e.  w  -> 
( y  e.  B  ->  ( [. z  /  x ]. ph  ->  ( E. f ( f : w --> B  /\  A. x  e.  w  ps )  ->  E. g ( g : ( w  u. 
{ z } ) --> B  /\  A. x  e.  ( w  u.  {
z } ) [. ( g `  x
)  /  y ]. ph ) ) ) ) )
13259, 67, 131rexlimd 2787 . . . . . . 7  |-  ( -.  z  e.  w  -> 
( E. y  e.  B  [. z  /  x ]. ph  ->  ( E. f ( f : w --> B  /\  A. x  e.  w  ps )  ->  E. g ( g : ( w  u. 
{ z } ) --> B  /\  A. x  e.  ( w  u.  {
z } ) [. ( g `  x
)  /  y ]. ph ) ) ) )
13358, 132syl5 30 . . . . . 6  |-  ( -.  z  e.  w  -> 
( A. x  e.  ( w  u.  {
z } ) E. y  e.  B  ph  ->  ( E. f ( f : w --> B  /\  A. x  e.  w  ps )  ->  E. g ( g : ( w  u. 
{ z } ) --> B  /\  A. x  e.  ( w  u.  {
z } ) [. ( g `  x
)  /  y ]. ph ) ) ) )
134133a2d 24 . . . . 5  |-  ( -.  z  e.  w  -> 
( ( A. x  e.  ( w  u.  {
z } ) E. y  e.  B  ph  ->  E. f ( f : w --> B  /\  A. x  e.  w  ps ) )  ->  ( A. x  e.  (
w  u.  { z } ) E. y  e.  B  ph  ->  E. g
( g : ( w  u.  { z } ) --> B  /\  A. x  e.  ( w  u.  { z } ) [. ( g `
 x )  / 
y ]. ph ) ) ) )
13548, 134syl5 30 . . . 4  |-  ( -.  z  e.  w  -> 
( ( A. x  e.  w  E. y  e.  B  ph  ->  E. f
( f : w --> B  /\  A. x  e.  w  ps )
)  ->  ( A. x  e.  ( w  u.  { z } ) E. y  e.  B  ph 
->  E. g ( g : ( w  u. 
{ z } ) --> B  /\  A. x  e.  ( w  u.  {
z } ) [. ( g `  x
)  /  y ]. ph ) ) ) )
136135adantl 453 . . 3  |-  ( ( w  e.  Fin  /\  -.  z  e.  w
)  ->  ( ( A. x  e.  w  E. y  e.  B  ph 
->  E. f ( f : w --> B  /\  A. x  e.  w  ps ) )  ->  ( A. x  e.  (
w  u.  { z } ) E. y  e.  B  ph  ->  E. g
( g : ( w  u.  { z } ) --> B  /\  A. x  e.  ( w  u.  { z } ) [. ( g `
 x )  / 
y ]. ph ) ) ) )
1376, 12, 30, 36, 44, 136findcard2s 7308 . 2  |-  ( A  e.  Fin  ->  ( A. x  e.  A  E. y  e.  B  ph 
->  E. f ( f : A --> B  /\  A. x  e.  A  ps ) ) )
138137imp 419 1  |-  ( ( A  e.  Fin  /\  A. x  e.  A  E. y  e.  B  ph )  ->  E. f ( f : A --> B  /\  A. x  e.  A  ps ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 177    /\ wa 359    /\ w3a 936   E.wex 1547    = wceq 1649    e. wcel 1721    =/= wne 2567   A.wral 2666   E.wrex 2667   _Vcvv 2916   [.wsbc 3121    u. cun 3278    i^i cin 3279    C_ wss 3280   (/)c0 3588   {csn 3774   <.cop 3777   dom cdm 4837   Fun wfun 5407   -->wf 5409   -1-1-onto->wf1o 5412   ` cfv 5413   Fincfn 7068
This theorem is referenced by:  fissuni  7369  fipreima  7370  indexfi  7372  finacn  7887  axcc4dom  8277  ttukeylem6  8350  firest  13615  ablfaclem3  15600  ablfac2  15602  cmpcovf  17408  cmpsub  17417  tgcmp  17418  hauscmplem  17423  ptcnplem  17606  alexsubALTlem3  18033  alexsubALT  18035  tsmsxplem1  18135  ovolicc2lem5  19370  ovolicc2  19371  limciun  19734  cvmliftlem15  24938  comppfsc  26277  istotbnd3  26370  sstotbnd2  26373  sstotbnd  26374  prdsbnd  26392  prdstotbnd  26393  heiborlem1  26410  heibor  26420  kelac1  27029  hbt  27202
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 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-sep 4290  ax-nul 4298  ax-pow 4337  ax-pr 4363  ax-un 4660
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-ral 2671  df-rex 2672  df-rab 2675  df-v 2918  df-sbc 3122  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-pss 3296  df-nul 3589  df-if 3700  df-pw 3761  df-sn 3780  df-pr 3781  df-tp 3782  df-op 3783  df-uni 3976  df-br 4173  df-opab 4227  df-tr 4263  df-eprel 4454  df-id 4458  df-po 4463  df-so 4464  df-fr 4501  df-we 4503  df-ord 4544  df-on 4545  df-lim 4546  df-suc 4547  df-om 4805  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-iota 5377  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-1o 6683  df-er 6864  df-en 7069  df-fin 7072
  Copyright terms: Public domain W3C validator