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

Theorem pwfseqlem5 8502
Description: Lemma for pwfseq 8503. Although in some ways pwfseqlem4 8501 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 7872. 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 7860. 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 7627), which can be used to construct a pairing function explicitly using properties of the ordinal exponential (infxpenc 7863). (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 2927 . . . . . . . . . . 11  |-  t  e. 
_V
6 simprl3 1004 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( (
t  C_  A  /\  r  C_  ( t  X.  t )  /\  r  We  t )  /\  om  ~<_  t ) )  -> 
r  We  t )
74, 6sylan2b 462 . . . . . . . . . . 11  |-  ( (
ph  /\  ps )  ->  r  We  t )
8 pwfseqlem5.o . . . . . . . . . . . 12  |-  O  = OrdIso
( r ,  t )
98oiiso 7470 . . . . . . . . . . 11  |-  ( ( t  e.  _V  /\  r  We  t )  ->  O  Isom  _E  ,  r  ( dom  O , 
t ) )
105, 7, 9sylancr 645 . . . . . . . . . 10  |-  ( (
ph  /\  ps )  ->  O  Isom  _E  ,  r  ( dom  O , 
t ) )
11 isof1o 6012 . . . . . . . . . 10  |-  ( O 
Isom  _E  ,  r 
( dom  O , 
t )  ->  O : dom  O -1-1-onto-> t )
1210, 11syl 16 . . . . . . . . 9  |-  ( (
ph  /\  ps )  ->  O : dom  O -1-1-onto-> t
)
138oion 7469 . . . . . . . . . . . . 13  |-  ( t  e.  _V  ->  dom  O  e.  On )
145, 13ax-mp 8 . . . . . . . . . . . 12  |-  dom  O  e.  On
1514a1i 11 . . . . . . . . . . 11  |-  ( (
ph  /\  ps )  ->  dom  O  e.  On )
168oien 7471 . . . . . . . . . . . . 13  |-  ( ( t  e.  _V  /\  r  We  t )  ->  dom  O  ~~  t
)
175, 7, 16sylancr 645 . . . . . . . . . . . 12  |-  ( (
ph  /\  ps )  ->  dom  O  ~~  t
)
181adantr 452 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ps )  ->  G : ~P A -1-1-> U_ n  e.  om  ( A  ^m  n ) )
19 omex 7562 . . . . . . . . . . . . . . . . 17  |-  om  e.  _V
20 ovex 6073 . . . . . . . . . . . . . . . . 17  |-  ( A  ^m  n )  e. 
_V
2119, 20iunex 5958 . . . . . . . . . . . . . . . 16  |-  U_ n  e.  om  ( A  ^m  n )  e.  _V
22 f1dmex 5938 . . . . . . . . . . . . . . . 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 644 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ps )  ->  ~P A  e.  _V )
24 pwexb 4720 . . . . . . . . . . . . . . 15  |-  ( A  e.  _V  <->  ~P A  e.  _V )
2523, 24sylibr 204 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ps )  ->  A  e.  _V )
26 simprl1 1002 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( (
t  C_  A  /\  r  C_  ( t  X.  t )  /\  r  We  t )  /\  om  ~<_  t ) )  -> 
t  C_  A )
274, 26sylan2b 462 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ps )  ->  t  C_  A )
28 ssdomg 7120 . . . . . . . . . . . . . 14  |-  ( A  e.  _V  ->  (
t  C_  A  ->  t  ~<_  A ) )
2925, 27, 28sylc 58 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ps )  ->  t  ~<_  A )
30 canth2g 7228 . . . . . . . . . . . . . 14  |-  ( A  e.  _V  ->  A  ~<  ~P A )
31 sdomdom 7102 . . . . . . . . . . . . . 14  |-  ( A 
~<  ~P A  ->  A  ~<_  ~P A )
3225, 30, 313syl 19 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ps )  ->  A  ~<_  ~P A )
33 domtr 7127 . . . . . . . . . . . . 13  |-  ( ( t  ~<_  A  /\  A  ~<_  ~P A )  ->  t  ~<_  ~P A )
3429, 32, 33syl2anc 643 . . . . . . . . . . . 12  |-  ( (
ph  /\  ps )  ->  t  ~<_  ~P A )
35 endomtr 7132 . . . . . . . . . . . 12  |-  ( ( dom  O  ~~  t  /\  t  ~<_  ~P A
)  ->  dom  O  ~<_  ~P A )
3617, 34, 35syl2anc 643 . . . . . . . . . . 11  |-  ( (
ph  /\  ps )  ->  dom  O  ~<_  ~P A
)
37 elharval 7495 . . . . . . . . . . 11  |-  ( dom 
O  e.  (har `  ~P A )  <->  ( dom  O  e.  On  /\  dom  O  ~<_  ~P A ) )
3815, 36, 37sylanbrc 646 . . . . . . . . . 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 452 . . . . . . . . . 10  |-  ( (
ph  /\  ps )  ->  A. b  e.  (har
`  ~P A ) ( om  C_  b  ->  ( N `  b
) : ( b  X.  b ) -1-1-onto-> b ) )
41 cardom 7837 . . . . . . . . . . . 12  |-  ( card `  om )  =  om
42 simprr 734 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( (
t  C_  A  /\  r  C_  ( t  X.  t )  /\  r  We  t )  /\  om  ~<_  t ) )  ->  om 
~<_  t )
434, 42sylan2b 462 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ps )  ->  om  ~<_  t )
4417ensymd 7125 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ps )  ->  t  ~~  dom  O
)
45 domentr 7133 . . . . . . . . . . . . . 14  |-  ( ( om  ~<_  t  /\  t  ~~  dom  O )  ->  om 
~<_  dom  O )
4643, 44, 45syl2anc 643 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ps )  ->  om  ~<_  dom  O )
47 omelon 7565 . . . . . . . . . . . . . . 15  |-  om  e.  On
48 onenon 7800 . . . . . . . . . . . . . . 15  |-  ( om  e.  On  ->  om  e.  dom  card )
4947, 48ax-mp 8 . . . . . . . . . . . . . 14  |-  om  e.  dom  card
50 onenon 7800 . . . . . . . . . . . . . . 15  |-  ( dom 
O  e.  On  ->  dom 
O  e.  dom  card )
5114, 50mp1i 12 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ps )  ->  dom  O  e.  dom  card )
52 carddom2 7828 . . . . . . . . . . . . . 14  |-  ( ( om  e.  dom  card  /\ 
dom  O  e.  dom  card )  ->  ( ( card `  om )  C_  ( card `  dom  O )  <->  om 
~<_  dom  O ) )
5349, 51, 52sylancr 645 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ps )  ->  ( ( card `  om )  C_  ( card `  dom  O )  <->  om  ~<_  dom  O )
)
5446, 53mpbird 224 . . . . . . . . . . . 12  |-  ( (
ph  /\  ps )  ->  ( card `  om )  C_  ( card `  dom  O ) )
5541, 54syl5eqssr 3361 . . . . . . . . . . 11  |-  ( (
ph  /\  ps )  ->  om  C_  ( card ` 
dom  O ) )
56 cardonle 7808 . . . . . . . . . . . 12  |-  ( dom 
O  e.  On  ->  (
card `  dom  O ) 
C_  dom  O )
5715, 56syl 16 . . . . . . . . . . 11  |-  ( (
ph  /\  ps )  ->  ( card `  dom  O )  C_  dom  O )
5855, 57sstrd 3326 . . . . . . . . . 10  |-  ( (
ph  /\  ps )  ->  om  C_  dom  O )
59 sseq2 3338 . . . . . . . . . . . 12  |-  ( b  =  dom  O  -> 
( om  C_  b  <->  om  C_  dom  O ) )
60 fveq2 5695 . . . . . . . . . . . . . 14  |-  ( b  =  dom  O  -> 
( N `  b
)  =  ( N `
 dom  O )
)
61 f1oeq1 5632 . . . . . . . . . . . . . 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 ) )
6260, 61syl 16 . . . . . . . . . . . . 13  |-  ( b  =  dom  O  -> 
( ( N `  b ) : ( b  X.  b ) -1-1-onto-> b  <-> 
( N `  dom  O ) : ( b  X.  b ) -1-1-onto-> b ) )
63 xpeq12 4864 . . . . . . . . . . . . . . 15  |-  ( ( b  =  dom  O  /\  b  =  dom  O )  ->  ( b  X.  b )  =  ( dom  O  X.  dom  O ) )
6463anidms 627 . . . . . . . . . . . . . 14  |-  ( b  =  dom  O  -> 
( b  X.  b
)  =  ( dom 
O  X.  dom  O
) )
65 f1oeq2 5633 . . . . . . . . . . . . . 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 ) )
6664, 65syl 16 . . . . . . . . . . . . 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 ) )
67 f1oeq3 5634 . . . . . . . . . . . . 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 ) )
6862, 66, 673bitrd 271 . . . . . . . . . . . 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 ) )
6959, 68imbi12d 312 . . . . . . . . . . 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 ) ) )
7069rspcv 3016 . . . . . . . . . 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 ) ) )
7138, 40, 58, 70syl3c 59 . . . . . . . . 9  |-  ( (
ph  /\  ps )  ->  ( N `  dom  O ) : ( dom 
O  X.  dom  O
)
-1-1-onto-> dom  O )
72 f1oco 5665 . . . . . . . . 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 )
7312, 71, 72syl2anc 643 . . . . . . . 8  |-  ( (
ph  /\  ps )  ->  ( O  o.  ( N `  dom  O ) ) : ( dom 
O  X.  dom  O
)
-1-1-onto-> t )
74 f1of 5641 . . . . . . . . . . . . . . 15  |-  ( O : dom  O -1-1-onto-> t  ->  O : dom  O --> t )
7512, 74syl 16 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ps )  ->  O : dom  O --> t )
7675feqmptd 5746 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ps )  ->  O  =  ( u  e.  dom  O  |->  ( O `  u ) ) )
77 f1oeq1 5632 . . . . . . . . . . . . 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 ) )
7876, 77syl 16 . . . . . . . . . . . 12  |-  ( (
ph  /\  ps )  ->  ( O : dom  O -1-1-onto-> t  <-> 
( u  e.  dom  O 
|->  ( O `  u
) ) : dom  O -1-1-onto-> t ) )
7912, 78mpbid 202 . . . . . . . . . . 11  |-  ( (
ph  /\  ps )  ->  ( u  e.  dom  O 
|->  ( O `  u
) ) : dom  O -1-1-onto-> t )
8075feqmptd 5746 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ps )  ->  O  =  ( v  e.  dom  O  |->  ( O `  v ) ) )
81 f1oeq1 5632 . . . . . . . . . . . . 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 ) )
8280, 81syl 16 . . . . . . . . . . . 12  |-  ( (
ph  /\  ps )  ->  ( O : dom  O -1-1-onto-> t  <-> 
( v  e.  dom  O 
|->  ( O `  v
) ) : dom  O -1-1-onto-> t ) )
8312, 82mpbid 202 . . . . . . . . . . 11  |-  ( (
ph  /\  ps )  ->  ( v  e.  dom  O 
|->  ( O `  v
) ) : dom  O -1-1-onto-> t )
8479, 83xpf1o 7236 . . . . . . . . . 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
) )
85 pwfseqlem5.t . . . . . . . . . . 11  |-  T  =  ( u  e.  dom  O ,  v  e.  dom  O 
|->  <. ( O `  u ) ,  ( O `  v )
>. )
86 f1oeq1 5632 . . . . . . . . . . 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
) ) )
8785, 86ax-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
) )
8884, 87sylibr 204 . . . . . . . . 9  |-  ( (
ph  /\  ps )  ->  T : ( dom 
O  X.  dom  O
)
-1-1-onto-> ( t  X.  t
) )
89 f1ocnv 5654 . . . . . . . . 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
) )
9088, 89syl 16 . . . . . . . 8  |-  ( (
ph  /\  ps )  ->  `' T : ( t  X.  t ) -1-1-onto-> ( dom 
O  X.  dom  O
) )
91 f1oco 5665 . . . . . . . 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 )
9273, 90, 91syl2anc 643 . . . . . . 7  |-  ( (
ph  /\  ps )  ->  ( ( O  o.  ( N `  dom  O
) )  o.  `' T ) : ( t  X.  t ) -1-1-onto-> t )
93 pwfseqlem5.p . . . . . . . 8  |-  P  =  ( ( O  o.  ( N `  dom  O
) )  o.  `' T )
94 f1oeq1 5632 . . . . . . . 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 ) )
9593, 94ax-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 )
9692, 95sylibr 204 . . . . . 6  |-  ( (
ph  /\  ps )  ->  P : ( t  X.  t ) -1-1-onto-> t )
97 f1of1 5640 . . . . . 6  |-  ( P : ( t  X.  t ) -1-1-onto-> t  ->  P :
( t  X.  t
) -1-1-> t )
9896, 97syl 16 . . . . 5  |-  ( (
ph  /\  ps )  ->  P : ( t  X.  t ) -1-1-> t )
99 f1of1 5640 . . . . . . . . . . . . 13  |-  ( O : dom  O -1-1-onto-> t  ->  O : dom  O -1-1-> t )
10012, 99syl 16 . . . . . . . . . . . 12  |-  ( (
ph  /\  ps )  ->  O : dom  O -1-1-> t )
101 f1ssres 5613 . . . . . . . . . . . 12  |-  ( ( O : dom  O -1-1-> t  /\  om  C_  dom  O )  ->  ( O  |` 
om ) : om -1-1-> t )
102100, 58, 101syl2anc 643 . . . . . . . . . . 11  |-  ( (
ph  /\  ps )  ->  ( O  |`  om ) : om -1-1-> t )
103 f1f1orn 5652 . . . . . . . . . . 11  |-  ( ( O  |`  om ) : om -1-1-> t  ->  ( O  |`  om ) : om -1-1-onto-> ran  ( O  |`  om ) )
104102, 103syl 16 . . . . . . . . . 10  |-  ( (
ph  /\  ps )  ->  ( O  |`  om ) : om -1-1-onto-> ran  ( O  |`  om ) )
10575, 58feqresmpt 5747 . . . . . . . . . . 11  |-  ( (
ph  /\  ps )  ->  ( O  |`  om )  =  ( x  e. 
om  |->  ( O `  x ) ) )
106 f1oeq1 5632 . . . . . . . . . . 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 ) ) )
107105, 106syl 16 . . . . . . . . . 10  |-  ( (
ph  /\  ps )  ->  ( ( O  |`  om ) : om -1-1-onto-> ran  ( O  |`  om )  <->  ( x  e. 
om  |->  ( O `  x ) ) : om -1-1-onto-> ran  ( O  |`  om ) ) )
108104, 107mpbid 202 . . . . . . . . 9  |-  ( (
ph  /\  ps )  ->  ( x  e.  om  |->  ( O `  x ) ) : om -1-1-onto-> ran  ( O  |`  om ) )
109 mptresid 5162 . . . . . . . . . 10  |-  ( y  e.  t  |->  y )  =  (  _I  |`  t
)
110 f1oi 5680 . . . . . . . . . . 11  |-  (  _I  |`  t ) : t -1-1-onto-> t
111 f1oeq1 5632 . . . . . . . . . . 11  |-  ( ( y  e.  t  |->  y )  =  (  _I  |`  t )  ->  (
( y  e.  t 
|->  y ) : t -1-1-onto-> t  <-> 
(  _I  |`  t
) : t -1-1-onto-> t ) )
112110, 111mpbiri 225 . . . . . . . . . 10  |-  ( ( y  e.  t  |->  y )  =  (  _I  |`  t )  ->  (
y  e.  t  |->  y ) : t -1-1-onto-> t )
113109, 112mp1i 12 . . . . . . . . 9  |-  ( (
ph  /\  ps )  ->  ( y  e.  t 
|->  y ) : t -1-1-onto-> t )
114108, 113xpf1o 7236 . . . . . . . 8  |-  ( (
ph  /\  ps )  ->  ( x  e.  om ,  y  e.  t  |-> 
<. ( O `  x
) ,  y >.
) : ( om 
X.  t ) -1-1-onto-> ( ran  ( O  |`  om )  X.  t ) )
115 pwfseqlem5.i . . . . . . . . 9  |-  I  =  ( x  e.  om ,  y  e.  t  |-> 
<. ( O `  x
) ,  y >.
)
116 f1oeq1 5632 . . . . . . . . 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 ) ) )
117115, 116ax-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 ) )
118114, 117sylibr 204 . . . . . . 7  |-  ( (
ph  /\  ps )  ->  I : ( om 
X.  t ) -1-1-onto-> ( ran  ( O  |`  om )  X.  t ) )
119 f1of1 5640 . . . . . . 7  |-  ( I : ( om  X.  t ) -1-1-onto-> ( ran  ( O  |`  om )  X.  t
)  ->  I :
( om  X.  t
) -1-1-> ( ran  ( O  |`  om )  X.  t ) )
120118, 119syl 16 . . . . . 6  |-  ( (
ph  /\  ps )  ->  I : ( om 
X.  t ) -1-1-> ( ran  ( O  |`  om )  X.  t
) )
121 f1f 5606 . . . . . . . 8  |-  ( ( O  |`  om ) : om -1-1-> t  ->  ( O  |`  om ) : om --> t )
122 frn 5564 . . . . . . . 8  |-  ( ( O  |`  om ) : om --> t  ->  ran  ( O  |`  om )  C_  t )
123102, 121, 1223syl 19 . . . . . . 7  |-  ( (
ph  /\  ps )  ->  ran  ( O  |`  om )  C_  t )
124 xpss1 4951 . . . . . . 7  |-  ( ran  ( O  |`  om )  C_  t  ->  ( ran  ( O  |`  om )  X.  t )  C_  (
t  X.  t ) )
125123, 124syl 16 . . . . . 6  |-  ( (
ph  /\  ps )  ->  ( ran  ( O  |`  om )  X.  t
)  C_  ( t  X.  t ) )
126 f1ss 5611 . . . . . 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 ) )
127120, 125, 126syl2anc 643 . . . . 5  |-  ( (
ph  /\  ps )  ->  I : ( om 
X.  t ) -1-1-> ( t  X.  t ) )
128 f1co 5615 . . . . 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 )
12998, 127, 128syl2anc 643 . . . 4  |-  ( (
ph  /\  ps )  ->  ( P  o.  I
) : ( om 
X.  t ) -1-1-> t )
1305a1i 11 . . . . 5  |-  ( (
ph  /\  ps )  ->  t  e.  _V )
131 peano1 4831 . . . . . . . 8  |-  (/)  e.  om
132131a1i 11 . . . . . . 7  |-  ( (
ph  /\  ps )  -> 
(/)  e.  om )
13358, 132sseldd 3317 . . . . . 6  |-  ( (
ph  /\  ps )  -> 
(/)  e.  dom  O )
13475, 133ffvelrnd 5838 . . . . 5  |-  ( (
ph  /\  ps )  ->  ( O `  (/) )  e.  t )
135 pwfseqlem5.s . . . . 5  |-  S  = seq𝜔 ( ( k  e.  _V ,  f  e.  _V  |->  ( x  e.  (
t  ^m  suc  k ) 
|->  ( ( f `  ( x  |`  k ) ) P ( x `
 k ) ) ) ) ,  { <.
(/) ,  ( O `  (/) ) >. } )
136 pwfseqlem5.q . . . . 5  |-  Q  =  ( y  e.  U_ n  e.  om  (
t  ^m  n )  |-> 
<. dom  y ,  ( ( S `  dom  y ) `  y
) >. )
137130, 134, 96, 135, 136fseqenlem2 7870 . . . 4  |-  ( (
ph  /\  ps )  ->  Q : U_ n  e.  om  ( t  ^m  n ) -1-1-> ( om 
X.  t ) )
138 f1co 5615 . . . 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 )
139129, 137, 138syl2anc 643 . . 3  |-  ( (
ph  /\  ps )  ->  ( ( P  o.  I )  o.  Q
) : U_ n  e.  om  ( t  ^m  n ) -1-1-> t )
140 pwfseqlem5.k . . . 4  |-  K  =  ( ( P  o.  I )  o.  Q
)
141 f1eq1 5601 . . . 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 ) )
142140, 141ax-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 )
143139, 142sylibr 204 . 2  |-  ( (
ph  /\  ps )  ->  K : U_ n  e.  om  ( t  ^m  n ) -1-1-> t )
144 eqid 2412 . 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 ) ) ) } )
145 eqid 2412 . 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 } ) ) )
146 eqid 2412 . . 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 ) ) }
147146fpwwe2cbv 8469 . 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 ) ) }
148 eqid 2412 . 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 ) ) }
1491, 2, 3, 4, 143, 144, 145, 147, 148pwfseqlem4 8501 1  |-  -.  ph
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 177    /\ wa 359    /\ w3a 936    = wceq 1649    e. wcel 1721   A.wral 2674   {crab 2678   _Vcvv 2924   [.wsbc 3129    i^i cin 3287    C_ wss 3288   (/)c0 3596   ifcif 3707   ~Pcpw 3767   {csn 3782   <.cop 3785   U.cuni 3983   |^|cint 4018   U_ciun 4061   class class class wbr 4180   {copab 4233    e. cmpt 4234    _E cep 4460    _I cid 4461    We wwe 4508   Oncon0 4549   suc csuc 4551   omcom 4812    X. cxp 4843   `'ccnv 4844   dom cdm 4845   ran crn 4846    |` cres 4847   "cima 4848    o. ccom 4849   -->wf 5417   -1-1->wf1 5418   -1-1-onto->wf1o 5420   ` cfv 5421    Isom wiso 5422  (class class class)co 6048    e. cmpt2 6050  seq𝜔cseqom 6671    ^m cmap 6985    ~~ cen 7073    ~<_ cdom 7074    ~< csdm 7075   Fincfn 7076  OrdIsocoi 7442  harchar 7488   cardccrd 7786
This theorem is referenced by:  pwfseq  8503
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 2393  ax-rep 4288  ax-sep 4298  ax-nul 4306  ax-pow 4345  ax-pr 4371  ax-un 4668  ax-inf2 7560
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 2266  df-mo 2267  df-clab 2399  df-cleq 2405  df-clel 2408  df-nfc 2537  df-ne 2577  df-ral 2679  df-rex 2680  df-reu 2681  df-rmo 2682  df-rab 2683  df-v 2926  df-sbc 3130  df-csb 3220  df-dif 3291  df-un 3293  df-in 3295  df-ss 3302  df-pss 3304  df-nul 3597  df-if 3708  df-pw 3769  df-sn 3788  df-pr 3789  df-tp 3790  df-op 3791  df-uni 3984  df-int 4019  df-iun 4063  df-br 4181  df-opab 4235  df-mpt 4236  df-tr 4271  df-eprel 4462  df-id 4466  df-po 4471  df-so 4472  df-fr 4509  df-se 4510  df-we 4511  df-ord 4552  df-on 4553  df-lim 4554  df-suc 4555  df-om 4813  df-xp 4851  df-rel 4852  df-cnv 4853  df-co 4854  df-dm 4855  df-rn 4856  df-res 4857  df-ima 4858  df-iota 5385  df-fun 5423  df-fn 5424  df-f 5425  df-f1 5426  df-fo 5427  df-f1o 5428  df-fv 5429  df-isom 5430  df-ov 6051  df-oprab 6052  df-mpt2 6053  df-1st 6316  df-2nd 6317  df-riota 6516  df-recs 6600  df-rdg 6635  df-seqom 6672  df-1o 6691  df-er 6872  df-map 6987  df-en 7077  df-dom 7078  df-sdom 7079  df-fin 7080  df-oi 7443  df-har 7490  df-card 7790
  Copyright terms: Public domain W3C validator