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

Theorem pwfseqlem5 9074
Description: Lemma for pwfseq 9075. Although in some ways pwfseqlem4 9073 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 8444. 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 8431. 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 8197), which can be used to construct a pairing function explicitly using properties of the ordinal exponential (infxpenc 8435). (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 3015 . . . . . . . . . . 11  |-  t  e. 
_V
6 simprl3 1056 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( (
t  C_  A  /\  r  C_  ( t  X.  t )  /\  r  We  t )  /\  om  ~<_  t ) )  -> 
r  We  t )
74, 6sylan2b 482 . . . . . . . . . . 11  |-  ( (
ph  /\  ps )  ->  r  We  t )
8 pwfseqlem5.o . . . . . . . . . . . 12  |-  O  = OrdIso
( r ,  t )
98oiiso 8038 . . . . . . . . . . 11  |-  ( ( t  e.  _V  /\  r  We  t )  ->  O  Isom  _E  ,  r  ( dom  O , 
t ) )
105, 7, 9sylancr 674 . . . . . . . . . 10  |-  ( (
ph  /\  ps )  ->  O  Isom  _E  ,  r  ( dom  O , 
t ) )
11 isof1o 6201 . . . . . . . . . 10  |-  ( O 
Isom  _E  ,  r 
( dom  O , 
t )  ->  O : dom  O -1-1-onto-> t )
1210, 11syl 17 . . . . . . . . 9  |-  ( (
ph  /\  ps )  ->  O : dom  O -1-1-onto-> t
)
138oion 8037 . . . . . . . . . . . . 13  |-  ( t  e.  _V  ->  dom  O  e.  On )
145, 13ax-mp 5 . . . . . . . . . . . 12  |-  dom  O  e.  On
1514a1i 11 . . . . . . . . . . 11  |-  ( (
ph  /\  ps )  ->  dom  O  e.  On )
168oien 8039 . . . . . . . . . . . . 13  |-  ( ( t  e.  _V  /\  r  We  t )  ->  dom  O  ~~  t
)
175, 7, 16sylancr 674 . . . . . . . . . . . 12  |-  ( (
ph  /\  ps )  ->  dom  O  ~~  t
)
181adantr 471 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ps )  ->  G : ~P A -1-1-> U_ n  e.  om  ( A  ^m  n ) )
19 omex 8134 . . . . . . . . . . . . . . . . 17  |-  om  e.  _V
20 ovex 6303 . . . . . . . . . . . . . . . . 17  |-  ( A  ^m  n )  e. 
_V
2119, 20iunex 6760 . . . . . . . . . . . . . . . 16  |-  U_ n  e.  om  ( A  ^m  n )  e.  _V
22 f1dmex 6750 . . . . . . . . . . . . . . . 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 673 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ps )  ->  ~P A  e.  _V )
24 pwexb 6589 . . . . . . . . . . . . . . 15  |-  ( A  e.  _V  <->  ~P A  e.  _V )
2523, 24sylibr 217 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ps )  ->  A  e.  _V )
26 simprl1 1054 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( (
t  C_  A  /\  r  C_  ( t  X.  t )  /\  r  We  t )  /\  om  ~<_  t ) )  -> 
t  C_  A )
274, 26sylan2b 482 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ps )  ->  t  C_  A )
28 ssdomg 7601 . . . . . . . . . . . . . 14  |-  ( A  e.  _V  ->  (
t  C_  A  ->  t  ~<_  A ) )
2925, 27, 28sylc 62 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ps )  ->  t  ~<_  A )
30 canth2g 7712 . . . . . . . . . . . . . 14  |-  ( A  e.  _V  ->  A  ~<  ~P A )
31 sdomdom 7583 . . . . . . . . . . . . . 14  |-  ( A 
~<  ~P A  ->  A  ~<_  ~P A )
3225, 30, 313syl 18 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ps )  ->  A  ~<_  ~P A )
33 domtr 7608 . . . . . . . . . . . . 13  |-  ( ( t  ~<_  A  /\  A  ~<_  ~P A )  ->  t  ~<_  ~P A )
3429, 32, 33syl2anc 671 . . . . . . . . . . . 12  |-  ( (
ph  /\  ps )  ->  t  ~<_  ~P A )
35 endomtr 7613 . . . . . . . . . . . 12  |-  ( ( dom  O  ~~  t  /\  t  ~<_  ~P A
)  ->  dom  O  ~<_  ~P A )
3617, 34, 35syl2anc 671 . . . . . . . . . . 11  |-  ( (
ph  /\  ps )  ->  dom  O  ~<_  ~P A
)
37 elharval 8064 . . . . . . . . . . 11  |-  ( dom 
O  e.  (har `  ~P A )  <->  ( dom  O  e.  On  /\  dom  O  ~<_  ~P A ) )
3815, 36, 37sylanbrc 675 . . . . . . . . . 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 471 . . . . . . . . . 10  |-  ( (
ph  /\  ps )  ->  A. b  e.  (har
`  ~P A ) ( om  C_  b  ->  ( N `  b
) : ( b  X.  b ) -1-1-onto-> b ) )
41 cardom 8406 . . . . . . . . . . . 12  |-  ( card `  om )  =  om
42 simprr 771 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( (
t  C_  A  /\  r  C_  ( t  X.  t )  /\  r  We  t )  /\  om  ~<_  t ) )  ->  om 
~<_  t )
434, 42sylan2b 482 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ps )  ->  om  ~<_  t )
4417ensymd 7606 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ps )  ->  t  ~~  dom  O
)
45 domentr 7614 . . . . . . . . . . . . . 14  |-  ( ( om  ~<_  t  /\  t  ~~  dom  O )  ->  om 
~<_  dom  O )
4643, 44, 45syl2anc 671 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ps )  ->  om  ~<_  dom  O )
47 omelon 8137 . . . . . . . . . . . . . . 15  |-  om  e.  On
48 onenon 8369 . . . . . . . . . . . . . . 15  |-  ( om  e.  On  ->  om  e.  dom  card )
4947, 48ax-mp 5 . . . . . . . . . . . . . 14  |-  om  e.  dom  card
50 onenon 8369 . . . . . . . . . . . . . . 15  |-  ( dom 
O  e.  On  ->  dom 
O  e.  dom  card )
5114, 50mp1i 13 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ps )  ->  dom  O  e.  dom  card )
52 carddom2 8397 . . . . . . . . . . . . . 14  |-  ( ( om  e.  dom  card  /\ 
dom  O  e.  dom  card )  ->  ( ( card `  om )  C_  ( card `  dom  O )  <->  om 
~<_  dom  O ) )
5349, 51, 52sylancr 674 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ps )  ->  ( ( card `  om )  C_  ( card `  dom  O )  <->  om  ~<_  dom  O )
)
5446, 53mpbird 240 . . . . . . . . . . . 12  |-  ( (
ph  /\  ps )  ->  ( card `  om )  C_  ( card `  dom  O ) )
5541, 54syl5eqssr 3444 . . . . . . . . . . 11  |-  ( (
ph  /\  ps )  ->  om  C_  ( card ` 
dom  O ) )
56 cardonle 8377 . . . . . . . . . . . 12  |-  ( dom 
O  e.  On  ->  (
card `  dom  O ) 
C_  dom  O )
5715, 56syl 17 . . . . . . . . . . 11  |-  ( (
ph  /\  ps )  ->  ( card `  dom  O )  C_  dom  O )
5855, 57sstrd 3409 . . . . . . . . . 10  |-  ( (
ph  /\  ps )  ->  om  C_  dom  O )
59 sseq2 3421 . . . . . . . . . . . 12  |-  ( b  =  dom  O  -> 
( om  C_  b  <->  om  C_  dom  O ) )
60 fveq2 5847 . . . . . . . . . . . . . 14  |-  ( b  =  dom  O  -> 
( N `  b
)  =  ( N `
 dom  O )
)
61 f1oeq1 5787 . . . . . . . . . . . . . 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 17 . . . . . . . . . . . . 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 4830 . . . . . . . . . . . . . . 15  |-  ( ( b  =  dom  O  /\  b  =  dom  O )  ->  ( b  X.  b )  =  ( dom  O  X.  dom  O ) )
6463anidms 655 . . . . . . . . . . . . . 14  |-  ( b  =  dom  O  -> 
( b  X.  b
)  =  ( dom 
O  X.  dom  O
) )
65 f1oeq2 5788 . . . . . . . . . . . . . 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 17 . . . . . . . . . . . . 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 5789 . . . . . . . . . . . . 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 287 . . . . . . . . . . . 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 326 . . . . . . . . . . 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 3113 . . . . . . . . . 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 63 . . . . . . . . 9  |-  ( (
ph  /\  ps )  ->  ( N `  dom  O ) : ( dom 
O  X.  dom  O
)
-1-1-onto-> dom  O )
72 f1oco 5818 . . . . . . . . 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 671 . . . . . . . 8  |-  ( (
ph  /\  ps )  ->  ( O  o.  ( N `  dom  O ) ) : ( dom 
O  X.  dom  O
)
-1-1-onto-> t )
74 f1of 5796 . . . . . . . . . . . . . . 15  |-  ( O : dom  O -1-1-onto-> t  ->  O : dom  O --> t )
7512, 74syl 17 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ps )  ->  O : dom  O --> t )
7675feqmptd 5900 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ps )  ->  O  =  ( u  e.  dom  O  |->  ( O `  u ) ) )
77 f1oeq1 5787 . . . . . . . . . . . . 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 17 . . . . . . . . . . . 12  |-  ( (
ph  /\  ps )  ->  ( O : dom  O -1-1-onto-> t  <-> 
( u  e.  dom  O 
|->  ( O `  u
) ) : dom  O -1-1-onto-> t ) )
7912, 78mpbid 215 . . . . . . . . . . 11  |-  ( (
ph  /\  ps )  ->  ( u  e.  dom  O 
|->  ( O `  u
) ) : dom  O -1-1-onto-> t )
8075feqmptd 5900 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ps )  ->  O  =  ( v  e.  dom  O  |->  ( O `  v ) ) )
81 f1oeq1 5787 . . . . . . . . . . . . 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 17 . . . . . . . . . . . 12  |-  ( (
ph  /\  ps )  ->  ( O : dom  O -1-1-onto-> t  <-> 
( v  e.  dom  O 
|->  ( O `  v
) ) : dom  O -1-1-onto-> t ) )
8312, 82mpbid 215 . . . . . . . . . . 11  |-  ( (
ph  /\  ps )  ->  ( v  e.  dom  O 
|->  ( O `  v
) ) : dom  O -1-1-onto-> t )
8479, 83xpf1o 7720 . . . . . . . . . 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 5787 . . . . . . . . . . 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 5 . . . . . . . . . 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 217 . . . . . . . . 9  |-  ( (
ph  /\  ps )  ->  T : ( dom 
O  X.  dom  O
)
-1-1-onto-> ( t  X.  t
) )
89 f1ocnv 5808 . . . . . . . . 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 17 . . . . . . . 8  |-  ( (
ph  /\  ps )  ->  `' T : ( t  X.  t ) -1-1-onto-> ( dom 
O  X.  dom  O
) )
91 f1oco 5818 . . . . . . . 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 671 . . . . . . 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 5787 . . . . . . . 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 5 . . . . . . 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 217 . . . . . 6  |-  ( (
ph  /\  ps )  ->  P : ( t  X.  t ) -1-1-onto-> t )
97 f1of1 5795 . . . . . 6  |-  ( P : ( t  X.  t ) -1-1-onto-> t  ->  P :
( t  X.  t
) -1-1-> t )
9896, 97syl 17 . . . . 5  |-  ( (
ph  /\  ps )  ->  P : ( t  X.  t ) -1-1-> t )
99 f1of1 5795 . . . . . . . . . . . . 13  |-  ( O : dom  O -1-1-onto-> t  ->  O : dom  O -1-1-> t )
10012, 99syl 17 . . . . . . . . . . . 12  |-  ( (
ph  /\  ps )  ->  O : dom  O -1-1-> t )
101 f1ssres 5768 . . . . . . . . . . . 12  |-  ( ( O : dom  O -1-1-> t  /\  om  C_  dom  O )  ->  ( O  |` 
om ) : om -1-1-> t )
102100, 58, 101syl2anc 671 . . . . . . . . . . 11  |-  ( (
ph  /\  ps )  ->  ( O  |`  om ) : om -1-1-> t )
103 f1f1orn 5807 . . . . . . . . . . 11  |-  ( ( O  |`  om ) : om -1-1-> t  ->  ( O  |`  om ) : om -1-1-onto-> ran  ( O  |`  om ) )
104102, 103syl 17 . . . . . . . . . 10  |-  ( (
ph  /\  ps )  ->  ( O  |`  om ) : om -1-1-onto-> ran  ( O  |`  om ) )
10575, 58feqresmpt 5901 . . . . . . . . . . 11  |-  ( (
ph  /\  ps )  ->  ( O  |`  om )  =  ( x  e. 
om  |->  ( O `  x ) ) )
106 f1oeq1 5787 . . . . . . . . . . 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 17 . . . . . . . . . 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 215 . . . . . . . . 9  |-  ( (
ph  /\  ps )  ->  ( x  e.  om  |->  ( O `  x ) ) : om -1-1-onto-> ran  ( O  |`  om ) )
109 mptresid 5136 . . . . . . . . . 10  |-  ( y  e.  t  |->  y )  =  (  _I  |`  t
)
110 f1oi 5832 . . . . . . . . . . 11  |-  (  _I  |`  t ) : t -1-1-onto-> t
111 f1oeq1 5787 . . . . . . . . . . 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 241 . . . . . . . . . 10  |-  ( ( y  e.  t  |->  y )  =  (  _I  |`  t )  ->  (
y  e.  t  |->  y ) : t -1-1-onto-> t )
113109, 112mp1i 13 . . . . . . . . 9  |-  ( (
ph  /\  ps )  ->  ( y  e.  t 
|->  y ) : t -1-1-onto-> t )
114108, 113xpf1o 7720 . . . . . . . 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 5787 . . . . . . . . 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 5 . . . . . . . 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 217 . . . . . . 7  |-  ( (
ph  /\  ps )  ->  I : ( om 
X.  t ) -1-1-onto-> ( ran  ( O  |`  om )  X.  t ) )
119 f1of1 5795 . . . . . . 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 17 . . . . . 6  |-  ( (
ph  /\  ps )  ->  I : ( om 
X.  t ) -1-1-> ( ran  ( O  |`  om )  X.  t
) )
121 f1f 5761 . . . . . . 7  |-  ( ( O  |`  om ) : om -1-1-> t  ->  ( O  |`  om ) : om --> t )
122 frn 5717 . . . . . . 7  |-  ( ( O  |`  om ) : om --> t  ->  ran  ( O  |`  om )  C_  t )
123 xpss1 4920 . . . . . . 7  |-  ( ran  ( O  |`  om )  C_  t  ->  ( ran  ( O  |`  om )  X.  t )  C_  (
t  X.  t ) )
124102, 121, 122, 1234syl 19 . . . . . 6  |-  ( (
ph  /\  ps )  ->  ( ran  ( O  |`  om )  X.  t
)  C_  ( t  X.  t ) )
125 f1ss 5766 . . . . . 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 ) )
126120, 124, 125syl2anc 671 . . . . 5  |-  ( (
ph  /\  ps )  ->  I : ( om 
X.  t ) -1-1-> ( t  X.  t ) )
127 f1co 5770 . . . . 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 )
12898, 126, 127syl2anc 671 . . . 4  |-  ( (
ph  /\  ps )  ->  ( P  o.  I
) : ( om 
X.  t ) -1-1-> t )
1295a1i 11 . . . . 5  |-  ( (
ph  /\  ps )  ->  t  e.  _V )
130 peano1 6699 . . . . . . . 8  |-  (/)  e.  om
131130a1i 11 . . . . . . 7  |-  ( (
ph  /\  ps )  -> 
(/)  e.  om )
13258, 131sseldd 3400 . . . . . 6  |-  ( (
ph  /\  ps )  -> 
(/)  e.  dom  O )
13375, 132ffvelrnd 6006 . . . . 5  |-  ( (
ph  /\  ps )  ->  ( O `  (/) )  e.  t )
134 pwfseqlem5.s . . . . 5  |-  S  = seq𝜔 ( ( k  e.  _V ,  f  e.  _V  |->  ( x  e.  (
t  ^m  suc  k ) 
|->  ( ( f `  ( x  |`  k ) ) P ( x `
 k ) ) ) ) ,  { <.
(/) ,  ( O `  (/) ) >. } )
135 pwfseqlem5.q . . . . 5  |-  Q  =  ( y  e.  U_ n  e.  om  (
t  ^m  n )  |-> 
<. dom  y ,  ( ( S `  dom  y ) `  y
) >. )
136129, 133, 96, 134, 135fseqenlem2 8442 . . . 4  |-  ( (
ph  /\  ps )  ->  Q : U_ n  e.  om  ( t  ^m  n ) -1-1-> ( om 
X.  t ) )
137 f1co 5770 . . . 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 )
138128, 136, 137syl2anc 671 . . 3  |-  ( (
ph  /\  ps )  ->  ( ( P  o.  I )  o.  Q
) : U_ n  e.  om  ( t  ^m  n ) -1-1-> t )
139 pwfseqlem5.k . . . 4  |-  K  =  ( ( P  o.  I )  o.  Q
)
140 f1eq1 5756 . . . 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 ) )
141139, 140ax-mp 5 . . 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 )
142138, 141sylibr 217 . 2  |-  ( (
ph  /\  ps )  ->  K : U_ n  e.  om  ( t  ^m  n ) -1-1-> t )
143 eqid 2451 . 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 ) ) ) } )
144 eqid 2451 . 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 } ) ) )
145 eqid 2451 . . 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 ) ) }
146145fpwwe2cbv 9041 . 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 ) ) }
147 eqid 2451 . 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 ) ) }
1481, 2, 3, 4, 142, 143, 144, 146, 147pwfseqlem4 9073 1  |-  -.  ph
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 189    /\ wa 375    /\ w3a 986    = wceq 1447    e. wcel 1890   A.wral 2736   {crab 2740   _Vcvv 3012   [.wsbc 3234    i^i cin 3370    C_ wss 3371   (/)c0 3698   ifcif 3848   ~Pcpw 3918   {csn 3935   <.cop 3941   U.cuni 4167   |^|cint 4203   U_ciun 4247   class class class wbr 4373   {copab 4431    |-> cmpt 4432    _E cep 4720    _I cid 4721    We wwe 4769    X. cxp 4809   `'ccnv 4810   dom cdm 4811   ran crn 4812    |` cres 4813   "cima 4814    o. ccom 4815   Oncon0 5401   suc csuc 5403   -->wf 5556   -1-1->wf1 5557   -1-1-onto->wf1o 5559   ` cfv 5560    Isom wiso 5561  (class class class)co 6275    |-> cmpt2 6277   omcom 6679  seq𝜔cseqom 7150    ^m cmap 7458    ~~ cen 7552    ~<_ cdom 7553    ~< csdm 7554   Fincfn 7555  OrdIsocoi 8010  harchar 8057   cardccrd 8355
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1672  ax-4 1685  ax-5 1761  ax-6 1808  ax-7 1854  ax-8 1892  ax-9 1899  ax-10 1918  ax-11 1923  ax-12 1936  ax-13 2091  ax-ext 2431  ax-rep 4486  ax-sep 4496  ax-nul 4505  ax-pow 4553  ax-pr 4611  ax-un 6570  ax-inf2 8132
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 987  df-3an 988  df-tru 1450  df-ex 1667  df-nf 1671  df-sb 1801  df-eu 2303  df-mo 2304  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2623  df-ral 2741  df-rex 2742  df-reu 2743  df-rmo 2744  df-rab 2745  df-v 3014  df-sbc 3235  df-csb 3331  df-dif 3374  df-un 3376  df-in 3378  df-ss 3385  df-pss 3387  df-nul 3699  df-if 3849  df-pw 3920  df-sn 3936  df-pr 3938  df-tp 3940  df-op 3942  df-uni 4168  df-int 4204  df-iun 4249  df-br 4374  df-opab 4433  df-mpt 4434  df-tr 4469  df-eprel 4722  df-id 4726  df-po 4732  df-so 4733  df-fr 4770  df-se 4771  df-we 4772  df-xp 4817  df-rel 4818  df-cnv 4819  df-co 4820  df-dm 4821  df-rn 4822  df-res 4823  df-ima 4824  df-pred 5358  df-ord 5404  df-on 5405  df-lim 5406  df-suc 5407  df-iota 5524  df-fun 5562  df-fn 5563  df-f 5564  df-f1 5565  df-fo 5566  df-f1o 5567  df-fv 5568  df-isom 5569  df-riota 6237  df-ov 6278  df-oprab 6279  df-mpt2 6280  df-om 6680  df-1st 6780  df-2nd 6781  df-wrecs 7014  df-recs 7076  df-rdg 7114  df-seqom 7151  df-1o 7168  df-er 7349  df-map 7460  df-en 7556  df-dom 7557  df-sdom 7558  df-fin 7559  df-oi 8011  df-har 8059  df-card 8359
This theorem is referenced by:  pwfseq  9075
  Copyright terms: Public domain W3C validator