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

Theorem pwfseqlem5 8285
Description: Lemma for pwfseq 8286. Although in some ways pwfseqlem4 8284 is the "main" part of the proof, one last aspect which makes up a remark in the original text is by far the hardest part to formalize. The main proof relies on the existence of an injection  K from the set of finite sequences on an infinite set 
x to  x. Now this alone would not be difficult to prove; this is mostly the claim of fseqen 7654. However, what is needed for the proof is a canonical injection on these sets, so we have to start from scratch pulling together explicit bijections from the lemmas.

If one attempts such a program, it will mostly go through, but there is one key step which is inherently nonconstructive, namely the proof of infxpen 7642. The resolution is not obvious, but it turns out that reversing an infinite ordinal's Cantor normal form absorbs all the non-leading terms (cnfcom3c 7409), which can be used to construct a pairing function explicitly using properties of the ordinal exponential (infxpenc 7645). (Contributed by Mario Carneiro, 31-May-2015.)

Hypotheses
Ref Expression
pwfseqlem5.g  |-  ( ph  ->  G : ~P A -1-1-> U_ n  e.  om  ( A  ^m  n ) )
pwfseqlem5.x  |-  ( ph  ->  X  C_  A )
pwfseqlem5.h  |-  ( ph  ->  H : om -1-1-onto-> X )
pwfseqlem5.ps  |-  ( ps  <->  ( ( t  C_  A  /\  r  C_  ( t  X.  t )  /\  r  We  t )  /\  om  ~<_  t ) )
pwfseqlem5.n  |-  ( ph  ->  A. b  e.  (har
`  ~P A ) ( om  C_  b  ->  ( N `  b
) : ( b  X.  b ) -1-1-onto-> b ) )
pwfseqlem5.o  |-  O  = OrdIso
( r ,  t )
pwfseqlem5.t  |-  T  =  ( u  e.  dom  O ,  v  e.  dom  O 
|->  <. ( O `  u ) ,  ( O `  v )
>. )
pwfseqlem5.p  |-  P  =  ( ( O  o.  ( N `  dom  O
) )  o.  `' T )
pwfseqlem5.s  |-  S  = seq𝜔 ( ( k  e.  _V ,  f  e.  _V  |->  ( x  e.  (
t  ^m  suc  k ) 
|->  ( ( f `  ( x  |`  k ) ) P ( x `
 k ) ) ) ) ,  { <.
(/) ,  ( O `  (/) ) >. } )
pwfseqlem5.q  |-  Q  =  ( y  e.  U_ n  e.  om  (
t  ^m  n )  |-> 
<. dom  y ,  ( ( S `  dom  y ) `  y
) >. )
pwfseqlem5.i  |-  I  =  ( x  e.  om ,  y  e.  t  |-> 
<. ( O `  x
) ,  y >.
)
pwfseqlem5.k  |-  K  =  ( ( P  o.  I )  o.  Q
)
Assertion
Ref Expression
pwfseqlem5  |-  -.  ph
Distinct variable groups:    n, b, G    r, b, t, H   
f, k, x, P   
f, b, k, u, v, x, y, n, r, t    ph, b,
k, n, r, t, x, y    K, b, n    N, b    ps, k, n, x, y    S, n, y    A, b, n, r, t    O, b, u, v, x, y
Allowed substitution hints:    ph( v, u, f)    ps( v, u, t, f, r, b)    A( x, y, v, u, f, k)    P( y, v, u, t, n, r, b)    Q( x, y, v, u, t, f, k, n, r, b)    S( x, v, u, t, f, k, r, b)    T( x, y, v, u, t, f, k, n, r, b)    G( x, y, v, u, t, f, k, r)    H( x, y, v, u, f, k, n)    I( x, y, v, u, t, f, k, n, r, b)    K( x, y, v, u, t, f, k, r)    N( x, y, v, u, t, f, k, n, r)    O( t, f, k, n, r)    X( x, y, v, u, t, f, k, n, r, b)

Proof of Theorem pwfseqlem5
Dummy variables  a 
c  d  i  j  m  s  w  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 pwfseqlem5.g . 2  |-  ( ph  ->  G : ~P A -1-1-> U_ n  e.  om  ( A  ^m  n ) )
2 pwfseqlem5.x . 2  |-  ( ph  ->  X  C_  A )
3 pwfseqlem5.h . 2  |-  ( ph  ->  H : om -1-1-onto-> X )
4 pwfseqlem5.ps . 2  |-  ( ps  <->  ( ( t  C_  A  /\  r  C_  ( t  X.  t )  /\  r  We  t )  /\  om  ~<_  t ) )
5 vex 2791 . . . . . . . . . . 11  |-  t  e. 
_V
6 simprl3 1002 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( (
t  C_  A  /\  r  C_  ( t  X.  t )  /\  r  We  t )  /\  om  ~<_  t ) )  -> 
r  We  t )
74, 6sylan2b 461 . . . . . . . . . . 11  |-  ( (
ph  /\  ps )  ->  r  We  t )
8 pwfseqlem5.o . . . . . . . . . . . 12  |-  O  = OrdIso
( r ,  t )
98oiiso 7252 . . . . . . . . . . 11  |-  ( ( t  e.  _V  /\  r  We  t )  ->  O  Isom  _E  ,  r  ( dom  O , 
t ) )
105, 7, 9sylancr 644 . . . . . . . . . 10  |-  ( (
ph  /\  ps )  ->  O  Isom  _E  ,  r  ( dom  O , 
t ) )
11 isof1o 5822 . . . . . . . . . 10  |-  ( O 
Isom  _E  ,  r 
( dom  O , 
t )  ->  O : dom  O -1-1-onto-> t )
1210, 11syl 15 . . . . . . . . 9  |-  ( (
ph  /\  ps )  ->  O : dom  O -1-1-onto-> t
)
138oion 7251 . . . . . . . . . . . . 13  |-  ( t  e.  _V  ->  dom  O  e.  On )
145, 13ax-mp 8 . . . . . . . . . . . 12  |-  dom  O  e.  On
1514a1i 10 . . . . . . . . . . 11  |-  ( (
ph  /\  ps )  ->  dom  O  e.  On )
168oien 7253 . . . . . . . . . . . . 13  |-  ( ( t  e.  _V  /\  r  We  t )  ->  dom  O  ~~  t
)
175, 7, 16sylancr 644 . . . . . . . . . . . 12  |-  ( (
ph  /\  ps )  ->  dom  O  ~~  t
)
181adantr 451 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ps )  ->  G : ~P A -1-1-> U_ n  e.  om  ( A  ^m  n ) )
19 omex 7344 . . . . . . . . . . . . . . . . 17  |-  om  e.  _V
20 ovex 5883 . . . . . . . . . . . . . . . . 17  |-  ( A  ^m  n )  e. 
_V
2119, 20iunex 5770 . . . . . . . . . . . . . . . 16  |-  U_ n  e.  om  ( A  ^m  n )  e.  _V
22 f1dmex 5751 . . . . . . . . . . . . . . . 16  |-  ( ( G : ~P A -1-1-> U_ n  e.  om  ( A  ^m  n )  /\  U_ n  e.  om  ( A  ^m  n )  e. 
_V )  ->  ~P A  e.  _V )
2318, 21, 22sylancl 643 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ps )  ->  ~P A  e.  _V )
24 pwexb 4564 . . . . . . . . . . . . . . 15  |-  ( A  e.  _V  <->  ~P A  e.  _V )
2523, 24sylibr 203 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ps )  ->  A  e.  _V )
26 simprl1 1000 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( (
t  C_  A  /\  r  C_  ( t  X.  t )  /\  r  We  t )  /\  om  ~<_  t ) )  -> 
t  C_  A )
274, 26sylan2b 461 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ps )  ->  t  C_  A )
28 ssdomg 6907 . . . . . . . . . . . . . 14  |-  ( A  e.  _V  ->  (
t  C_  A  ->  t  ~<_  A ) )
2925, 27, 28sylc 56 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ps )  ->  t  ~<_  A )
30 canth2g 7015 . . . . . . . . . . . . . 14  |-  ( A  e.  _V  ->  A  ~<  ~P A )
31 sdomdom 6889 . . . . . . . . . . . . . 14  |-  ( A 
~<  ~P A  ->  A  ~<_  ~P A )
3225, 30, 313syl 18 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ps )  ->  A  ~<_  ~P A )
33 domtr 6914 . . . . . . . . . . . . 13  |-  ( ( t  ~<_  A  /\  A  ~<_  ~P A )  ->  t  ~<_  ~P A )
3429, 32, 33syl2anc 642 . . . . . . . . . . . 12  |-  ( (
ph  /\  ps )  ->  t  ~<_  ~P A )
35 endomtr 6919 . . . . . . . . . . . 12  |-  ( ( dom  O  ~~  t  /\  t  ~<_  ~P A
)  ->  dom  O  ~<_  ~P A )
3617, 34, 35syl2anc 642 . . . . . . . . . . 11  |-  ( (
ph  /\  ps )  ->  dom  O  ~<_  ~P A
)
37 elharval 7277 . . . . . . . . . . 11  |-  ( dom 
O  e.  (har `  ~P A )  <->  ( dom  O  e.  On  /\  dom  O  ~<_  ~P A ) )
3815, 36, 37sylanbrc 645 . . . . . . . . . 10  |-  ( (
ph  /\  ps )  ->  dom  O  e.  (har
`  ~P A ) )
39 pwfseqlem5.n . . . . . . . . . . 11  |-  ( ph  ->  A. b  e.  (har
`  ~P A ) ( om  C_  b  ->  ( N `  b
) : ( b  X.  b ) -1-1-onto-> b ) )
4039adantr 451 . . . . . . . . . 10  |-  ( (
ph  /\  ps )  ->  A. b  e.  (har
`  ~P A ) ( om  C_  b  ->  ( N `  b
) : ( b  X.  b ) -1-1-onto-> b ) )
41 cardom 7619 . . . . . . . . . . . 12  |-  ( card `  om )  =  om
42 simprr 733 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( (
t  C_  A  /\  r  C_  ( t  X.  t )  /\  r  We  t )  /\  om  ~<_  t ) )  ->  om 
~<_  t )
434, 42sylan2b 461 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ps )  ->  om  ~<_  t )
44 ensym 6910 . . . . . . . . . . . . . . 15  |-  ( dom 
O  ~~  t  ->  t 
~~  dom  O )
4517, 44syl 15 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ps )  ->  t  ~~  dom  O
)
46 domentr 6920 . . . . . . . . . . . . . 14  |-  ( ( om  ~<_  t  /\  t  ~~  dom  O )  ->  om 
~<_  dom  O )
4743, 45, 46syl2anc 642 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ps )  ->  om  ~<_  dom  O )
48 omelon 7347 . . . . . . . . . . . . . . 15  |-  om  e.  On
49 onenon 7582 . . . . . . . . . . . . . . 15  |-  ( om  e.  On  ->  om  e.  dom  card )
5048, 49ax-mp 8 . . . . . . . . . . . . . 14  |-  om  e.  dom  card
51 onenon 7582 . . . . . . . . . . . . . . 15  |-  ( dom 
O  e.  On  ->  dom 
O  e.  dom  card )
5214, 51mp1i 11 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ps )  ->  dom  O  e.  dom  card )
53 carddom2 7610 . . . . . . . . . . . . . 14  |-  ( ( om  e.  dom  card  /\ 
dom  O  e.  dom  card )  ->  ( ( card `  om )  C_  ( card `  dom  O )  <->  om 
~<_  dom  O ) )
5450, 52, 53sylancr 644 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ps )  ->  ( ( card `  om )  C_  ( card `  dom  O )  <->  om  ~<_  dom  O )
)
5547, 54mpbird 223 . . . . . . . . . . . 12  |-  ( (
ph  /\  ps )  ->  ( card `  om )  C_  ( card `  dom  O ) )
5641, 55syl5eqssr 3223 . . . . . . . . . . 11  |-  ( (
ph  /\  ps )  ->  om  C_  ( card ` 
dom  O ) )
57 cardonle 7590 . . . . . . . . . . . 12  |-  ( dom 
O  e.  On  ->  (
card `  dom  O ) 
C_  dom  O )
5815, 57syl 15 . . . . . . . . . . 11  |-  ( (
ph  /\  ps )  ->  ( card `  dom  O )  C_  dom  O )
5956, 58sstrd 3189 . . . . . . . . . 10  |-  ( (
ph  /\  ps )  ->  om  C_  dom  O )
60 sseq2 3200 . . . . . . . . . . . 12  |-  ( b  =  dom  O  -> 
( om  C_  b  <->  om  C_  dom  O ) )
61 fveq2 5525 . . . . . . . . . . . . . 14  |-  ( b  =  dom  O  -> 
( N `  b
)  =  ( N `
 dom  O )
)
62 f1oeq1 5463 . . . . . . . . . . . . . 14  |-  ( ( N `  b )  =  ( N `  dom  O )  ->  (
( N `  b
) : ( b  X.  b ) -1-1-onto-> b  <->  ( N `  dom  O ) : ( b  X.  b
)
-1-1-onto-> b ) )
6361, 62syl 15 . . . . . . . . . . . . 13  |-  ( b  =  dom  O  -> 
( ( N `  b ) : ( b  X.  b ) -1-1-onto-> b  <-> 
( N `  dom  O ) : ( b  X.  b ) -1-1-onto-> b ) )
64 xpeq12 4708 . . . . . . . . . . . . . . 15  |-  ( ( b  =  dom  O  /\  b  =  dom  O )  ->  ( b  X.  b )  =  ( dom  O  X.  dom  O ) )
6564anidms 626 . . . . . . . . . . . . . 14  |-  ( b  =  dom  O  -> 
( b  X.  b
)  =  ( dom 
O  X.  dom  O
) )
66 f1oeq2 5464 . . . . . . . . . . . . . 14  |-  ( ( b  X.  b )  =  ( dom  O  X.  dom  O )  -> 
( ( N `  dom  O ) : ( b  X.  b ) -1-1-onto-> b  <-> 
( N `  dom  O ) : ( dom 
O  X.  dom  O
)
-1-1-onto-> b ) )
6765, 66syl 15 . . . . . . . . . . . . 13  |-  ( b  =  dom  O  -> 
( ( N `  dom  O ) : ( b  X.  b ) -1-1-onto-> b  <-> 
( N `  dom  O ) : ( dom 
O  X.  dom  O
)
-1-1-onto-> b ) )
68 f1oeq3 5465 . . . . . . . . . . . . 13  |-  ( b  =  dom  O  -> 
( ( N `  dom  O ) : ( dom  O  X.  dom  O ) -1-1-onto-> b  <->  ( N `  dom  O ) : ( dom  O  X.  dom  O ) -1-1-onto-> dom  O ) )
6963, 67, 683bitrd 270 . . . . . . . . . . . 12  |-  ( b  =  dom  O  -> 
( ( N `  b ) : ( b  X.  b ) -1-1-onto-> b  <-> 
( N `  dom  O ) : ( dom 
O  X.  dom  O
)
-1-1-onto-> dom  O ) )
7060, 69imbi12d 311 . . . . . . . . . . 11  |-  ( b  =  dom  O  -> 
( ( om  C_  b  ->  ( N `  b
) : ( b  X.  b ) -1-1-onto-> b )  <-> 
( om  C_  dom  O  ->  ( N `  dom  O ) : ( dom  O  X.  dom  O ) -1-1-onto-> dom  O ) ) )
7170rspcv 2880 . . . . . . . . . 10  |-  ( dom 
O  e.  (har `  ~P A )  ->  ( A. b  e.  (har `  ~P A ) ( om  C_  b  ->  ( N `  b ) : ( b  X.  b ) -1-1-onto-> b )  ->  ( om  C_  dom  O  -> 
( N `  dom  O ) : ( dom 
O  X.  dom  O
)
-1-1-onto-> dom  O ) ) )
7238, 40, 59, 71syl3c 57 . . . . . . . . 9  |-  ( (
ph  /\  ps )  ->  ( N `  dom  O ) : ( dom 
O  X.  dom  O
)
-1-1-onto-> dom  O )
73 f1oco 5496 . . . . . . . . 9  |-  ( ( O : dom  O -1-1-onto-> t  /\  ( N `  dom  O ) : ( dom 
O  X.  dom  O
)
-1-1-onto-> dom  O )  ->  ( O  o.  ( N `  dom  O ) ) : ( dom  O  X.  dom  O ) -1-1-onto-> t )
7412, 72, 73syl2anc 642 . . . . . . . 8  |-  ( (
ph  /\  ps )  ->  ( O  o.  ( N `  dom  O ) ) : ( dom 
O  X.  dom  O
)
-1-1-onto-> t )
75 f1of 5472 . . . . . . . . . . . . . . 15  |-  ( O : dom  O -1-1-onto-> t  ->  O : dom  O --> t )
7612, 75syl 15 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ps )  ->  O : dom  O --> t )
7776feqmptd 5575 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ps )  ->  O  =  ( u  e.  dom  O  |->  ( O `  u ) ) )
78 f1oeq1 5463 . . . . . . . . . . . . 13  |-  ( O  =  ( u  e. 
dom  O  |->  ( O `
 u ) )  ->  ( O : dom  O -1-1-onto-> t  <->  ( u  e. 
dom  O  |->  ( O `
 u ) ) : dom  O -1-1-onto-> t ) )
7977, 78syl 15 . . . . . . . . . . . 12  |-  ( (
ph  /\  ps )  ->  ( O : dom  O -1-1-onto-> t  <-> 
( u  e.  dom  O 
|->  ( O `  u
) ) : dom  O -1-1-onto-> t ) )
8012, 79mpbid 201 . . . . . . . . . . 11  |-  ( (
ph  /\  ps )  ->  ( u  e.  dom  O 
|->  ( O `  u
) ) : dom  O -1-1-onto-> t )
8176feqmptd 5575 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ps )  ->  O  =  ( v  e.  dom  O  |->  ( O `  v ) ) )
82 f1oeq1 5463 . . . . . . . . . . . . 13  |-  ( O  =  ( v  e. 
dom  O  |->  ( O `
 v ) )  ->  ( O : dom  O -1-1-onto-> t  <->  ( v  e. 
dom  O  |->  ( O `
 v ) ) : dom  O -1-1-onto-> t ) )
8381, 82syl 15 . . . . . . . . . . . 12  |-  ( (
ph  /\  ps )  ->  ( O : dom  O -1-1-onto-> t  <-> 
( v  e.  dom  O 
|->  ( O `  v
) ) : dom  O -1-1-onto-> t ) )
8412, 83mpbid 201 . . . . . . . . . . 11  |-  ( (
ph  /\  ps )  ->  ( v  e.  dom  O 
|->  ( O `  v
) ) : dom  O -1-1-onto-> t )
8580, 84xpf1o 7023 . . . . . . . . . 10  |-  ( (
ph  /\  ps )  ->  ( u  e.  dom  O ,  v  e.  dom  O 
|->  <. ( O `  u ) ,  ( O `  v )
>. ) : ( dom 
O  X.  dom  O
)
-1-1-onto-> ( t  X.  t
) )
86 pwfseqlem5.t . . . . . . . . . . 11  |-  T  =  ( u  e.  dom  O ,  v  e.  dom  O 
|->  <. ( O `  u ) ,  ( O `  v )
>. )
87 f1oeq1 5463 . . . . . . . . . . 11  |-  ( T  =  ( u  e. 
dom  O ,  v  e.  dom  O  |->  <.
( O `  u
) ,  ( O `
 v ) >.
)  ->  ( T : ( dom  O  X.  dom  O ) -1-1-onto-> ( t  X.  t )  <->  ( u  e.  dom  O ,  v  e.  dom  O  |->  <.
( O `  u
) ,  ( O `
 v ) >.
) : ( dom 
O  X.  dom  O
)
-1-1-onto-> ( t  X.  t
) ) )
8886, 87ax-mp 8 . . . . . . . . . 10  |-  ( T : ( dom  O  X.  dom  O ) -1-1-onto-> ( t  X.  t )  <->  ( u  e.  dom  O ,  v  e.  dom  O  |->  <.
( O `  u
) ,  ( O `
 v ) >.
) : ( dom 
O  X.  dom  O
)
-1-1-onto-> ( t  X.  t
) )
8985, 88sylibr 203 . . . . . . . . 9  |-  ( (
ph  /\  ps )  ->  T : ( dom 
O  X.  dom  O
)
-1-1-onto-> ( t  X.  t
) )
90 f1ocnv 5485 . . . . . . . . 9  |-  ( T : ( dom  O  X.  dom  O ) -1-1-onto-> ( t  X.  t )  ->  `' T : ( t  X.  t ) -1-1-onto-> ( dom 
O  X.  dom  O
) )
9189, 90syl 15 . . . . . . . 8  |-  ( (
ph  /\  ps )  ->  `' T : ( t  X.  t ) -1-1-onto-> ( dom 
O  X.  dom  O
) )
92 f1oco 5496 . . . . . . . 8  |-  ( ( ( O  o.  ( N `  dom  O ) ) : ( dom 
O  X.  dom  O
)
-1-1-onto-> t  /\  `' T :
( t  X.  t
)
-1-1-onto-> ( dom  O  X.  dom  O ) )  ->  (
( O  o.  ( N `  dom  O ) )  o.  `' T
) : ( t  X.  t ) -1-1-onto-> t )
9374, 91, 92syl2anc 642 . . . . . . 7  |-  ( (
ph  /\  ps )  ->  ( ( O  o.  ( N `  dom  O
) )  o.  `' T ) : ( t  X.  t ) -1-1-onto-> t )
94 pwfseqlem5.p . . . . . . . 8  |-  P  =  ( ( O  o.  ( N `  dom  O
) )  o.  `' T )
95 f1oeq1 5463 . . . . . . . 8  |-  ( P  =  ( ( O  o.  ( N `  dom  O ) )  o.  `' T )  ->  ( P : ( t  X.  t ) -1-1-onto-> t  <->  ( ( O  o.  ( N `  dom  O ) )  o.  `' T ) : ( t  X.  t ) -1-1-onto-> t ) )
9694, 95ax-mp 8 . . . . . . 7  |-  ( P : ( t  X.  t ) -1-1-onto-> t  <->  ( ( O  o.  ( N `  dom  O ) )  o.  `' T ) : ( t  X.  t ) -1-1-onto-> t )
9793, 96sylibr 203 . . . . . 6  |-  ( (
ph  /\  ps )  ->  P : ( t  X.  t ) -1-1-onto-> t )
98 f1of1 5471 . . . . . 6  |-  ( P : ( t  X.  t ) -1-1-onto-> t  ->  P :
( t  X.  t
) -1-1-> t )
9997, 98syl 15 . . . . 5  |-  ( (
ph  /\  ps )  ->  P : ( t  X.  t ) -1-1-> t )
100 f1of1 5471 . . . . . . . . . . . . 13  |-  ( O : dom  O -1-1-onto-> t  ->  O : dom  O -1-1-> t )
10112, 100syl 15 . . . . . . . . . . . 12  |-  ( (
ph  /\  ps )  ->  O : dom  O -1-1-> t )
102 f1ssres 5444 . . . . . . . . . . . 12  |-  ( ( O : dom  O -1-1-> t  /\  om  C_  dom  O )  ->  ( O  |` 
om ) : om -1-1-> t )
103101, 59, 102syl2anc 642 . . . . . . . . . . 11  |-  ( (
ph  /\  ps )  ->  ( O  |`  om ) : om -1-1-> t )
104 f1f1orn 5483 . . . . . . . . . . 11  |-  ( ( O  |`  om ) : om -1-1-> t  ->  ( O  |`  om ) : om -1-1-onto-> ran  ( O  |`  om ) )
105103, 104syl 15 . . . . . . . . . 10  |-  ( (
ph  /\  ps )  ->  ( O  |`  om ) : om -1-1-onto-> ran  ( O  |`  om ) )
10676, 59feqresmpt 5576 . . . . . . . . . . 11  |-  ( (
ph  /\  ps )  ->  ( O  |`  om )  =  ( x  e. 
om  |->  ( O `  x ) ) )
107 f1oeq1 5463 . . . . . . . . . . 11  |-  ( ( O  |`  om )  =  ( x  e. 
om  |->  ( O `  x ) )  -> 
( ( O  |`  om ) : om -1-1-onto-> ran  ( O  |`  om )  <->  ( x  e. 
om  |->  ( O `  x ) ) : om -1-1-onto-> ran  ( O  |`  om ) ) )
108106, 107syl 15 . . . . . . . . . 10  |-  ( (
ph  /\  ps )  ->  ( ( O  |`  om ) : om -1-1-onto-> ran  ( O  |`  om )  <->  ( x  e. 
om  |->  ( O `  x ) ) : om -1-1-onto-> ran  ( O  |`  om ) ) )
109105, 108mpbid 201 . . . . . . . . 9  |-  ( (
ph  /\  ps )  ->  ( x  e.  om  |->  ( O `  x ) ) : om -1-1-onto-> ran  ( O  |`  om ) )
110 mptresid 5004 . . . . . . . . . 10  |-  ( y  e.  t  |->  y )  =  (  _I  |`  t
)
111 f1oi 5511 . . . . . . . . . . 11  |-  (  _I  |`  t ) : t -1-1-onto-> t
112 f1oeq1 5463 . . . . . . . . . . 11  |-  ( ( y  e.  t  |->  y )  =  (  _I  |`  t )  ->  (
( y  e.  t 
|->  y ) : t -1-1-onto-> t  <-> 
(  _I  |`  t
) : t -1-1-onto-> t ) )
113111, 112mpbiri 224 . . . . . . . . . 10  |-  ( ( y  e.  t  |->  y )  =  (  _I  |`  t )  ->  (
y  e.  t  |->  y ) : t -1-1-onto-> t )
114110, 113mp1i 11 . . . . . . . . 9  |-  ( (
ph  /\  ps )  ->  ( y  e.  t 
|->  y ) : t -1-1-onto-> t )
115109, 114xpf1o 7023 . . . . . . . 8  |-  ( (
ph  /\  ps )  ->  ( x  e.  om ,  y  e.  t  |-> 
<. ( O `  x
) ,  y >.
) : ( om 
X.  t ) -1-1-onto-> ( ran  ( O  |`  om )  X.  t ) )
116 pwfseqlem5.i . . . . . . . . 9  |-  I  =  ( x  e.  om ,  y  e.  t  |-> 
<. ( O `  x
) ,  y >.
)
117 f1oeq1 5463 . . . . . . . . 9  |-  ( I  =  ( x  e. 
om ,  y  e.  t  |->  <. ( O `  x ) ,  y
>. )  ->  ( I : ( om  X.  t ) -1-1-onto-> ( ran  ( O  |`  om )  X.  t
)  <->  ( x  e. 
om ,  y  e.  t  |->  <. ( O `  x ) ,  y
>. ) : ( om 
X.  t ) -1-1-onto-> ( ran  ( O  |`  om )  X.  t ) ) )
118116, 117ax-mp 8 . . . . . . . 8  |-  ( I : ( om  X.  t ) -1-1-onto-> ( ran  ( O  |`  om )  X.  t
)  <->  ( x  e. 
om ,  y  e.  t  |->  <. ( O `  x ) ,  y
>. ) : ( om 
X.  t ) -1-1-onto-> ( ran  ( O  |`  om )  X.  t ) )
119115, 118sylibr 203 . . . . . . 7  |-  ( (
ph  /\  ps )  ->  I : ( om 
X.  t ) -1-1-onto-> ( ran  ( O  |`  om )  X.  t ) )
120 f1of1 5471 . . . . . . 7  |-  ( I : ( om  X.  t ) -1-1-onto-> ( ran  ( O  |`  om )  X.  t
)  ->  I :
( om  X.  t
) -1-1-> ( ran  ( O  |`  om )  X.  t ) )
121119, 120syl 15 . . . . . 6  |-  ( (
ph  /\  ps )  ->  I : ( om 
X.  t ) -1-1-> ( ran  ( O  |`  om )  X.  t
) )
122 f1f 5437 . . . . . . . 8  |-  ( ( O  |`  om ) : om -1-1-> t  ->  ( O  |`  om ) : om --> t )
123 frn 5395 . . . . . . . 8  |-  ( ( O  |`  om ) : om --> t  ->  ran  ( O  |`  om )  C_  t )
124103, 122, 1233syl 18 . . . . . . 7  |-  ( (
ph  /\  ps )  ->  ran  ( O  |`  om )  C_  t )
125 xpss1 4795 . . . . . . 7  |-  ( ran  ( O  |`  om )  C_  t  ->  ( ran  ( O  |`  om )  X.  t )  C_  (
t  X.  t ) )
126124, 125syl 15 . . . . . 6  |-  ( (
ph  /\  ps )  ->  ( ran  ( O  |`  om )  X.  t
)  C_  ( t  X.  t ) )
127 f1ss 5442 . . . . . 6  |-  ( ( I : ( om 
X.  t ) -1-1-> ( ran  ( O  |`  om )  X.  t
)  /\  ( ran  ( O  |`  om )  X.  t )  C_  (
t  X.  t ) )  ->  I :
( om  X.  t
) -1-1-> ( t  X.  t ) )
128121, 126, 127syl2anc 642 . . . . 5  |-  ( (
ph  /\  ps )  ->  I : ( om 
X.  t ) -1-1-> ( t  X.  t ) )
129 f1co 5446 . . . . 5  |-  ( ( P : ( t  X.  t ) -1-1-> t  /\  I : ( om  X.  t )
-1-1-> ( t  X.  t
) )  ->  ( P  o.  I ) : ( om  X.  t ) -1-1-> t )
13099, 128, 129syl2anc 642 . . . 4  |-  ( (
ph  /\  ps )  ->  ( P  o.  I
) : ( om 
X.  t ) -1-1-> t )
1315a1i 10 . . . . 5  |-  ( (
ph  /\  ps )  ->  t  e.  _V )
132 peano1 4675 . . . . . . . 8  |-  (/)  e.  om
133132a1i 10 . . . . . . 7  |-  ( (
ph  /\  ps )  -> 
(/)  e.  om )
13459, 133sseldd 3181 . . . . . 6  |-  ( (
ph  /\  ps )  -> 
(/)  e.  dom  O )
135 ffvelrn 5663 . . . . . 6  |-  ( ( O : dom  O --> t  /\  (/)  e.  dom  O
)  ->  ( O `  (/) )  e.  t )
13676, 134, 135syl2anc 642 . . . . 5  |-  ( (
ph  /\  ps )  ->  ( O `  (/) )  e.  t )
137 pwfseqlem5.s . . . . 5  |-  S  = seq𝜔 ( ( k  e.  _V ,  f  e.  _V  |->  ( x  e.  (
t  ^m  suc  k ) 
|->  ( ( f `  ( x  |`  k ) ) P ( x `
 k ) ) ) ) ,  { <.
(/) ,  ( O `  (/) ) >. } )
138 pwfseqlem5.q . . . . 5  |-  Q  =  ( y  e.  U_ n  e.  om  (
t  ^m  n )  |-> 
<. dom  y ,  ( ( S `  dom  y ) `  y
) >. )
139131, 136, 97, 137, 138fseqenlem2 7652 . . . 4  |-  ( (
ph  /\  ps )  ->  Q : U_ n  e.  om  ( t  ^m  n ) -1-1-> ( om 
X.  t ) )
140 f1co 5446 . . . 4  |-  ( ( ( P  o.  I
) : ( om 
X.  t ) -1-1-> t  /\  Q : U_ n  e.  om  (
t  ^m  n ) -1-1-> ( om  X.  t
) )  ->  (
( P  o.  I
)  o.  Q ) : U_ n  e. 
om  ( t  ^m  n ) -1-1-> t )
141130, 139, 140syl2anc 642 . . 3  |-  ( (
ph  /\  ps )  ->  ( ( P  o.  I )  o.  Q
) : U_ n  e.  om  ( t  ^m  n ) -1-1-> t )
142 pwfseqlem5.k . . . 4  |-  K  =  ( ( P  o.  I )  o.  Q
)
143 f1eq1 5432 . . . 4  |-  ( K  =  ( ( P  o.  I )  o.  Q )  ->  ( K : U_ n  e. 
om  ( t  ^m  n ) -1-1-> t  <->  ( ( P  o.  I )  o.  Q ) : U_ n  e.  om  (
t  ^m  n ) -1-1-> t ) )
144142, 143ax-mp 8 . . 3  |-  ( K : U_ n  e. 
om  ( t  ^m  n ) -1-1-> t  <->  ( ( P  o.  I )  o.  Q ) : U_ n  e.  om  (
t  ^m  n ) -1-1-> t )
145141, 144sylibr 203 . 2  |-  ( (
ph  /\  ps )  ->  K : U_ n  e.  om  ( t  ^m  n ) -1-1-> t )
146 eqid 2283 . 2  |-  ( G `
 { i  e.  t  |  ( ( `' K `  i )  e.  ran  G  /\  -.  i  e.  ( `' G `  ( `' K `  i ) ) ) } )  =  ( G `  { i  e.  t  |  ( ( `' K `  i )  e.  ran  G  /\  -.  i  e.  ( `' G `  ( `' K `  i ) ) ) } )
147 eqid 2283 . 2  |-  ( t  e.  _V ,  r  e.  _V  |->  if ( t  e.  Fin , 
( H `  ( card `  t ) ) ,  ( ( G `
 { i  e.  t  |  ( ( `' K `  i )  e.  ran  G  /\  -.  i  e.  ( `' G `  ( `' K `  i ) ) ) } ) `
 |^| { z  e. 
om  |  -.  (
( G `  {
i  e.  t  |  ( ( `' K `  i )  e.  ran  G  /\  -.  i  e.  ( `' G `  ( `' K `  i ) ) ) } ) `
 z )  e.  t } ) ) )  =  ( t  e.  _V ,  r  e.  _V  |->  if ( t  e.  Fin , 
( H `  ( card `  t ) ) ,  ( ( G `
 { i  e.  t  |  ( ( `' K `  i )  e.  ran  G  /\  -.  i  e.  ( `' G `  ( `' K `  i ) ) ) } ) `
 |^| { z  e. 
om  |  -.  (
( G `  {
i  e.  t  |  ( ( `' K `  i )  e.  ran  G  /\  -.  i  e.  ( `' G `  ( `' K `  i ) ) ) } ) `
 z )  e.  t } ) ) )
148 eqid 2283 . . 3  |-  { <. c ,  d >.  |  ( ( c  C_  A  /\  d  C_  ( c  X.  c ) )  /\  ( d  We  c  /\  A. m  e.  c  [. ( `' d " { m } )  /  j ]. ( j ( t  e.  _V ,  r  e.  _V  |->  if ( t  e.  Fin , 
( H `  ( card `  t ) ) ,  ( ( G `
 { i  e.  t  |  ( ( `' K `  i )  e.  ran  G  /\  -.  i  e.  ( `' G `  ( `' K `  i ) ) ) } ) `
 |^| { z  e. 
om  |  -.  (
( G `  {
i  e.  t  |  ( ( `' K `  i )  e.  ran  G  /\  -.  i  e.  ( `' G `  ( `' K `  i ) ) ) } ) `
 z )  e.  t } ) ) ) ( d  i^i  ( j  X.  j
) ) )  =  m ) ) }  =  { <. c ,  d >.  |  ( ( c  C_  A  /\  d  C_  ( c  X.  c ) )  /\  ( d  We  c  /\  A. m  e.  c  [. ( `' d " { m } )  /  j ]. ( j ( t  e.  _V ,  r  e.  _V  |->  if ( t  e.  Fin , 
( H `  ( card `  t ) ) ,  ( ( G `
 { i  e.  t  |  ( ( `' K `  i )  e.  ran  G  /\  -.  i  e.  ( `' G `  ( `' K `  i ) ) ) } ) `
 |^| { z  e. 
om  |  -.  (
( G `  {
i  e.  t  |  ( ( `' K `  i )  e.  ran  G  /\  -.  i  e.  ( `' G `  ( `' K `  i ) ) ) } ) `
 z )  e.  t } ) ) ) ( d  i^i  ( j  X.  j
) ) )  =  m ) ) }
149148fpwwe2cbv 8252 . 2  |-  { <. c ,  d >.  |  ( ( c  C_  A  /\  d  C_  ( c  X.  c ) )  /\  ( d  We  c  /\  A. m  e.  c  [. ( `' d " { m } )  /  j ]. ( j ( t  e.  _V ,  r  e.  _V  |->  if ( t  e.  Fin , 
( H `  ( card `  t ) ) ,  ( ( G `
 { i  e.  t  |  ( ( `' K `  i )  e.  ran  G  /\  -.  i  e.  ( `' G `  ( `' K `  i ) ) ) } ) `
 |^| { z  e. 
om  |  -.  (
( G `  {
i  e.  t  |  ( ( `' K `  i )  e.  ran  G  /\  -.  i  e.  ( `' G `  ( `' K `  i ) ) ) } ) `
 z )  e.  t } ) ) ) ( d  i^i  ( j  X.  j
) ) )  =  m ) ) }  =  { <. a ,  s >.  |  ( ( a  C_  A  /\  s  C_  ( a  X.  a ) )  /\  ( s  We  a  /\  A. b  e.  a  [. ( `' s " { b } )  /  w ]. ( w ( t  e.  _V ,  r  e.  _V  |->  if ( t  e.  Fin , 
( H `  ( card `  t ) ) ,  ( ( G `
 { i  e.  t  |  ( ( `' K `  i )  e.  ran  G  /\  -.  i  e.  ( `' G `  ( `' K `  i ) ) ) } ) `
 |^| { z  e. 
om  |  -.  (
( G `  {
i  e.  t  |  ( ( `' K `  i )  e.  ran  G  /\  -.  i  e.  ( `' G `  ( `' K `  i ) ) ) } ) `
 z )  e.  t } ) ) ) ( s  i^i  ( w  X.  w
) ) )  =  b ) ) }
150 eqid 2283 . 2  |-  U. dom  {
<. c ,  d >.  |  ( ( c 
C_  A  /\  d  C_  ( c  X.  c
) )  /\  (
d  We  c  /\  A. m  e.  c  [. ( `' d " {
m } )  / 
j ]. ( j ( t  e.  _V , 
r  e.  _V  |->  if ( t  e.  Fin ,  ( H `  ( card `  t ) ) ,  ( ( G `
 { i  e.  t  |  ( ( `' K `  i )  e.  ran  G  /\  -.  i  e.  ( `' G `  ( `' K `  i ) ) ) } ) `
 |^| { z  e. 
om  |  -.  (
( G `  {
i  e.  t  |  ( ( `' K `  i )  e.  ran  G  /\  -.  i  e.  ( `' G `  ( `' K `  i ) ) ) } ) `
 z )  e.  t } ) ) ) ( d  i^i  ( j  X.  j
) ) )  =  m ) ) }  =  U. dom  { <. c ,  d >.  |  ( ( c 
C_  A  /\  d  C_  ( c  X.  c
) )  /\  (
d  We  c  /\  A. m  e.  c  [. ( `' d " {
m } )  / 
j ]. ( j ( t  e.  _V , 
r  e.  _V  |->  if ( t  e.  Fin ,  ( H `  ( card `  t ) ) ,  ( ( G `
 { i  e.  t  |  ( ( `' K `  i )  e.  ran  G  /\  -.  i  e.  ( `' G `  ( `' K `  i ) ) ) } ) `
 |^| { z  e. 
om  |  -.  (
( G `  {
i  e.  t  |  ( ( `' K `  i )  e.  ran  G  /\  -.  i  e.  ( `' G `  ( `' K `  i ) ) ) } ) `
 z )  e.  t } ) ) ) ( d  i^i  ( j  X.  j
) ) )  =  m ) ) }
1511, 2, 3, 4, 145, 146, 147, 149, 150pwfseqlem4 8284 1  |-  -.  ph
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 176    /\ wa 358    /\ w3a 934    = wceq 1623    e. wcel 1684   A.wral 2543   {crab 2547   _Vcvv 2788   [.wsbc 2991    i^i cin 3151    C_ wss 3152   (/)c0 3455   ifcif 3565   ~Pcpw 3625   {csn 3640   <.cop 3643   U.cuni 3827   |^|cint 3862   U_ciun 3905   class class class wbr 4023   {copab 4076    e. cmpt 4077    _E cep 4303    _I cid 4304    We wwe 4351   Oncon0 4392   suc csuc 4394   omcom 4656    X. cxp 4687   `'ccnv 4688   dom cdm 4689   ran crn 4690    |` cres 4691   "cima 4692    o. ccom 4693   -->wf 5251   -1-1->wf1 5252   -1-1-onto->wf1o 5254   ` cfv 5255    Isom wiso 5256  (class class class)co 5858    e. cmpt2 5860  seq𝜔cseqom 6459    ^m cmap 6772    ~~ cen 6860    ~<_ cdom 6861    ~< csdm 6862   Fincfn 6863  OrdIsocoi 7224  harchar 7270   cardccrd 7568
This theorem is referenced by:  pwfseq  8286
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-13 1686  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-rep 4131  ax-sep 4141  ax-nul 4149  ax-pow 4188  ax-pr 4214  ax-un 4512  ax-inf2 7342
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rex 2549  df-reu 2550  df-rmo 2551  df-rab 2552  df-v 2790  df-sbc 2992  df-csb 3082  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-pss 3168  df-nul 3456  df-if 3566  df-pw 3627  df-sn 3646  df-pr 3647  df-tp 3648  df-op 3649  df-uni 3828  df-int 3863  df-iun 3907  df-br 4024  df-opab 4078  df-mpt 4079  df-tr 4114  df-eprel 4305  df-id 4309  df-po 4314  df-so 4315  df-fr 4352  df-se 4353  df-we 4354  df-ord 4395  df-on 4396  df-lim 4397  df-suc 4398  df-om 4657  df-xp 4695  df-rel 4696  df-cnv 4697  df-co 4698  df-dm 4699  df-rn 4700  df-res 4701  df-ima 4702  df-iota 5219  df-fun 5257  df-fn 5258  df-f 5259  df-f1 5260  df-fo 5261  df-f1o 5262  df-fv 5263  df-isom 5264  df-ov 5861  df-oprab 5862  df-mpt2 5863  df-1st 6122  df-2nd 6123  df-riota 6304  df-recs 6388  df-rdg 6423  df-seqom 6460  df-1o 6479  df-er 6660  df-map 6774  df-en 6864  df-dom 6865  df-sdom 6866  df-fin 6867  df-oi 7225  df-har 7272  df-card 7572
  Copyright terms: Public domain W3C validator