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

Theorem cantnfp1lem3 7592
Description: Lemma for cantnfp1 7593. (Contributed by Mario Carneiro, 28-May-2015.)
Hypotheses
Ref Expression
cantnfs.1  |-  S  =  dom  ( A CNF  B
)
cantnfs.2  |-  ( ph  ->  A  e.  On )
cantnfs.3  |-  ( ph  ->  B  e.  On )
cantnfp1.4  |-  ( ph  ->  G  e.  S )
cantnfp1.5  |-  ( ph  ->  X  e.  B )
cantnfp1.6  |-  ( ph  ->  Y  e.  A )
cantnfp1.7  |-  ( ph  ->  ( `' G "
( _V  \  1o ) )  C_  X
)
cantnfp1.f  |-  F  =  ( t  e.  B  |->  if ( t  =  X ,  Y , 
( G `  t
) ) )
cantnfp1.8  |-  ( ph  -> 
(/)  e.  Y )
cantnfp1.o  |-  O  = OrdIso
(  _E  ,  ( `' F " ( _V 
\  1o ) ) )
cantnfp1.h  |-  H  = seq𝜔 ( ( k  e.  _V ,  z  e.  _V  |->  ( ( ( A  ^o  ( O `  k ) )  .o  ( F `  ( O `  k )
) )  +o  z
) ) ,  (/) )
cantnfp1.k  |-  K  = OrdIso
(  _E  ,  ( `' G " ( _V 
\  1o ) ) )
cantnfp1.m  |-  M  = seq𝜔 ( ( k  e.  _V ,  z  e.  _V  |->  ( ( ( A  ^o  ( K `  k ) )  .o  ( G `  ( K `  k )
) )  +o  z
) ) ,  (/) )
Assertion
Ref Expression
cantnfp1lem3  |-  ( ph  ->  ( ( A CNF  B
) `  F )  =  ( ( ( A  ^o  X )  .o  Y )  +o  ( ( A CNF  B
) `  G )
) )
Distinct variable groups:    t, k,
z, B    A, k,
t, z    k, F, z    S, k, t, z   
k, G, t, z   
k, K, t, z   
k, O, z    ph, k,
t, z    k, Y, t, z    k, X, t, z
Allowed substitution hints:    F( t)    H( z, t, k)    M( z, t, k)    O( t)

Proof of Theorem cantnfp1lem3
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 cantnfs.1 . . 3  |-  S  =  dom  ( A CNF  B
)
2 cantnfs.2 . . 3  |-  ( ph  ->  A  e.  On )
3 cantnfs.3 . . 3  |-  ( ph  ->  B  e.  On )
4 cantnfp1.o . . 3  |-  O  = OrdIso
(  _E  ,  ( `' F " ( _V 
\  1o ) ) )
5 cantnfp1.4 . . . 4  |-  ( ph  ->  G  e.  S )
6 cantnfp1.5 . . . 4  |-  ( ph  ->  X  e.  B )
7 cantnfp1.6 . . . 4  |-  ( ph  ->  Y  e.  A )
8 cantnfp1.7 . . . 4  |-  ( ph  ->  ( `' G "
( _V  \  1o ) )  C_  X
)
9 cantnfp1.f . . . 4  |-  F  =  ( t  e.  B  |->  if ( t  =  X ,  Y , 
( G `  t
) ) )
101, 2, 3, 5, 6, 7, 8, 9cantnfp1lem1 7590 . . 3  |-  ( ph  ->  F  e.  S )
11 cantnfp1.h . . 3  |-  H  = seq𝜔 ( ( k  e.  _V ,  z  e.  _V  |->  ( ( ( A  ^o  ( O `  k ) )  .o  ( F `  ( O `  k )
) )  +o  z
) ) ,  (/) )
121, 2, 3, 4, 10, 11cantnfval 7579 . 2  |-  ( ph  ->  ( ( A CNF  B
) `  F )  =  ( H `  dom  O ) )
13 cantnfp1.8 . . . 4  |-  ( ph  -> 
(/)  e.  Y )
141, 2, 3, 5, 6, 7, 8, 9, 13, 4cantnfp1lem2 7591 . . 3  |-  ( ph  ->  dom  O  =  suc  U.
dom  O )
1514fveq2d 5691 . 2  |-  ( ph  ->  ( H `  dom  O )  =  ( H `
 suc  U. dom  O
) )
161, 2, 3, 4, 10cantnfcl 7578 . . . . . . 7  |-  ( ph  ->  (  _E  We  ( `' F " ( _V 
\  1o ) )  /\  dom  O  e. 
om ) )
1716simprd 450 . . . . . 6  |-  ( ph  ->  dom  O  e.  om )
1814, 17eqeltrrd 2479 . . . . 5  |-  ( ph  ->  suc  U. dom  O  e.  om )
19 peano2b 4820 . . . . 5  |-  ( U. dom  O  e.  om  <->  suc  U. dom  O  e.  om )
2018, 19sylibr 204 . . . 4  |-  ( ph  ->  U. dom  O  e. 
om )
211, 2, 3, 4, 10, 11cantnfsuc 7581 . . . 4  |-  ( (
ph  /\  U. dom  O  e.  om )  ->  ( H `  suc  U. dom  O )  =  ( ( ( A  ^o  ( O `  U. dom  O
) )  .o  ( F `  ( O `  U. dom  O ) ) )  +o  ( H `  U. dom  O
) ) )
2220, 21mpdan 650 . . 3  |-  ( ph  ->  ( H `  suc  U.
dom  O )  =  ( ( ( A  ^o  ( O `  U. dom  O ) )  .o  ( F `  ( O `  U. dom  O ) ) )  +o  ( H `  U. dom  O ) ) )
23 cnvimass 5183 . . . . . . . . . . . . . . . . 17  |-  ( `' F " ( _V 
\  1o ) ) 
C_  dom  F
247adantr 452 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  t  e.  B )  ->  Y  e.  A )
251, 2, 3cantnfs 7577 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( G  e.  S  <->  ( G : B --> A  /\  ( `' G " ( _V 
\  1o ) )  e.  Fin ) ) )
265, 25mpbid 202 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( G : B --> A  /\  ( `' G " ( _V  \  1o ) )  e.  Fin ) )
2726simpld 446 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  G : B --> A )
2827ffvelrnda 5829 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  t  e.  B )  ->  ( G `  t )  e.  A )
29 ifcl 3735 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( Y  e.  A  /\  ( G `  t )  e.  A )  ->  if ( t  =  X ,  Y ,  ( G `  t ) )  e.  A )
3024, 28, 29syl2anc 643 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  t  e.  B )  ->  if ( t  =  X ,  Y ,  ( G `  t ) )  e.  A )
3130, 9fmptd 5852 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  F : B --> A )
32 fdm 5554 . . . . . . . . . . . . . . . . . 18  |-  ( F : B --> A  ->  dom  F  =  B )
3331, 32syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  dom  F  =  B )
3423, 33syl5sseq 3356 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( `' F "
( _V  \  1o ) )  C_  B
)
353, 34ssexd 4310 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( `' F "
( _V  \  1o ) )  e.  _V )
3616simpld 446 . . . . . . . . . . . . . . 15  |-  ( ph  ->  _E  We  ( `' F " ( _V 
\  1o ) ) )
374oiiso 7462 . . . . . . . . . . . . . . 15  |-  ( ( ( `' F "
( _V  \  1o ) )  e.  _V  /\  _E  We  ( `' F " ( _V 
\  1o ) ) )  ->  O  Isom  _E  ,  _E  ( dom 
O ,  ( `' F " ( _V 
\  1o ) ) ) )
3835, 36, 37syl2anc 643 . . . . . . . . . . . . . 14  |-  ( ph  ->  O  Isom  _E  ,  _E  ( dom  O ,  ( `' F " ( _V 
\  1o ) ) ) )
39 isof1o 6004 . . . . . . . . . . . . . 14  |-  ( O 
Isom  _E  ,  _E  ( dom  O ,  ( `' F " ( _V 
\  1o ) ) )  ->  O : dom  O -1-1-onto-> ( `' F "
( _V  \  1o ) ) )
4038, 39syl 16 . . . . . . . . . . . . 13  |-  ( ph  ->  O : dom  O -1-1-onto-> ( `' F " ( _V 
\  1o ) ) )
41 f1ocnv 5646 . . . . . . . . . . . . 13  |-  ( O : dom  O -1-1-onto-> ( `' F " ( _V 
\  1o ) )  ->  `' O :
( `' F "
( _V  \  1o ) ) -1-1-onto-> dom  O )
42 f1of 5633 . . . . . . . . . . . . 13  |-  ( `' O : ( `' F " ( _V 
\  1o ) ) -1-1-onto-> dom 
O  ->  `' O : ( `' F " ( _V  \  1o ) ) --> dom  O
)
4340, 41, 423syl 19 . . . . . . . . . . . 12  |-  ( ph  ->  `' O : ( `' F " ( _V 
\  1o ) ) --> dom  O )
44 iftrue 3705 . . . . . . . . . . . . . . . . 17  |-  ( t  =  X  ->  if ( t  =  X ,  Y ,  ( G `  t ) )  =  Y )
4544, 9fvmptg 5763 . . . . . . . . . . . . . . . 16  |-  ( ( X  e.  B  /\  Y  e.  A )  ->  ( F `  X
)  =  Y )
466, 7, 45syl2anc 643 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( F `  X
)  =  Y )
47 onelon 4566 . . . . . . . . . . . . . . . . . 18  |-  ( ( A  e.  On  /\  Y  e.  A )  ->  Y  e.  On )
482, 7, 47syl2anc 643 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  Y  e.  On )
49 on0eln0 4596 . . . . . . . . . . . . . . . . 17  |-  ( Y  e.  On  ->  ( (/) 
e.  Y  <->  Y  =/=  (/) ) )
5048, 49syl 16 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( (/)  e.  Y  <->  Y  =/=  (/) ) )
5113, 50mpbid 202 . . . . . . . . . . . . . . 15  |-  ( ph  ->  Y  =/=  (/) )
5246, 51eqnetrd 2585 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( F `  X
)  =/=  (/) )
53 fvex 5701 . . . . . . . . . . . . . . 15  |-  ( F `
 X )  e. 
_V
54 dif1o 6703 . . . . . . . . . . . . . . 15  |-  ( ( F `  X )  e.  ( _V  \  1o )  <->  ( ( F `
 X )  e. 
_V  /\  ( F `  X )  =/=  (/) ) )
5553, 54mpbiran 885 . . . . . . . . . . . . . 14  |-  ( ( F `  X )  e.  ( _V  \  1o )  <->  ( F `  X )  =/=  (/) )
5652, 55sylibr 204 . . . . . . . . . . . . 13  |-  ( ph  ->  ( F `  X
)  e.  ( _V 
\  1o ) )
57 ffn 5550 . . . . . . . . . . . . . 14  |-  ( F : B --> A  ->  F  Fn  B )
58 elpreima 5809 . . . . . . . . . . . . . 14  |-  ( F  Fn  B  ->  ( X  e.  ( `' F " ( _V  \  1o ) )  <->  ( X  e.  B  /\  ( F `  X )  e.  ( _V  \  1o ) ) ) )
5931, 57, 583syl 19 . . . . . . . . . . . . 13  |-  ( ph  ->  ( X  e.  ( `' F " ( _V 
\  1o ) )  <-> 
( X  e.  B  /\  ( F `  X
)  e.  ( _V 
\  1o ) ) ) )
606, 56, 59mpbir2and 889 . . . . . . . . . . . 12  |-  ( ph  ->  X  e.  ( `' F " ( _V 
\  1o ) ) )
6143, 60ffvelrnd 5830 . . . . . . . . . . 11  |-  ( ph  ->  ( `' O `  X )  e.  dom  O )
62 elssuni 4003 . . . . . . . . . . 11  |-  ( ( `' O `  X )  e.  dom  O  -> 
( `' O `  X )  C_  U. dom  O )
6361, 62syl 16 . . . . . . . . . 10  |-  ( ph  ->  ( `' O `  X )  C_  U. dom  O )
644oicl 7454 . . . . . . . . . . . 12  |-  Ord  dom  O
65 ordelon 4565 . . . . . . . . . . . 12  |-  ( ( Ord  dom  O  /\  ( `' O `  X )  e.  dom  O )  ->  ( `' O `  X )  e.  On )
6664, 61, 65sylancr 645 . . . . . . . . . . 11  |-  ( ph  ->  ( `' O `  X )  e.  On )
67 nnon 4810 . . . . . . . . . . . 12  |-  ( U. dom  O  e.  om  ->  U.
dom  O  e.  On )
6820, 67syl 16 . . . . . . . . . . 11  |-  ( ph  ->  U. dom  O  e.  On )
69 ontri1 4575 . . . . . . . . . . 11  |-  ( ( ( `' O `  X )  e.  On  /\ 
U. dom  O  e.  On )  ->  ( ( `' O `  X ) 
C_  U. dom  O  <->  -.  U. dom  O  e.  ( `' O `  X ) ) )
7066, 68, 69syl2anc 643 . . . . . . . . . 10  |-  ( ph  ->  ( ( `' O `  X )  C_  U. dom  O  <->  -.  U. dom  O  e.  ( `' O `  X ) ) )
7163, 70mpbid 202 . . . . . . . . 9  |-  ( ph  ->  -.  U. dom  O  e.  ( `' O `  X ) )
72 sucidg 4619 . . . . . . . . . . . . . 14  |-  ( U. dom  O  e.  om  ->  U.
dom  O  e.  suc  U.
dom  O )
7320, 72syl 16 . . . . . . . . . . . . 13  |-  ( ph  ->  U. dom  O  e. 
suc  U. dom  O )
7473, 14eleqtrrd 2481 . . . . . . . . . . . 12  |-  ( ph  ->  U. dom  O  e. 
dom  O )
75 isorel 6005 . . . . . . . . . . . 12  |-  ( ( O  Isom  _E  ,  _E  ( dom  O ,  ( `' F " ( _V 
\  1o ) ) )  /\  ( U. dom  O  e.  dom  O  /\  ( `' O `  X )  e.  dom  O ) )  ->  ( U. dom  O  _E  ( `' O `  X )  <-> 
( O `  U. dom  O )  _E  ( O `  ( `' O `  X )
) ) )
7638, 74, 61, 75syl12anc 1182 . . . . . . . . . . 11  |-  ( ph  ->  ( U. dom  O  _E  ( `' O `  X )  <->  ( O `  U. dom  O )  _E  ( O `  ( `' O `  X ) ) ) )
77 fvex 5701 . . . . . . . . . . . 12  |-  ( `' O `  X )  e.  _V
7877epelc 4456 . . . . . . . . . . 11  |-  ( U. dom  O  _E  ( `' O `  X )  <->  U. dom  O  e.  ( `' O `  X ) )
79 fvex 5701 . . . . . . . . . . . 12  |-  ( O `
 ( `' O `  X ) )  e. 
_V
8079epelc 4456 . . . . . . . . . . 11  |-  ( ( O `  U. dom  O )  _E  ( O `
 ( `' O `  X ) )  <->  ( O `  U. dom  O )  e.  ( O `  ( `' O `  X ) ) )
8176, 78, 803bitr3g 279 . . . . . . . . . 10  |-  ( ph  ->  ( U. dom  O  e.  ( `' O `  X )  <->  ( O `  U. dom  O )  e.  ( O `  ( `' O `  X ) ) ) )
82 f1ocnvfv2 5974 . . . . . . . . . . . 12  |-  ( ( O : dom  O -1-1-onto-> ( `' F " ( _V 
\  1o ) )  /\  X  e.  ( `' F " ( _V 
\  1o ) ) )  ->  ( O `  ( `' O `  X ) )  =  X )
8340, 60, 82syl2anc 643 . . . . . . . . . . 11  |-  ( ph  ->  ( O `  ( `' O `  X ) )  =  X )
8483eleq2d 2471 . . . . . . . . . 10  |-  ( ph  ->  ( ( O `  U. dom  O )  e.  ( O `  ( `' O `  X ) )  <->  ( O `  U. dom  O )  e.  X ) )
8581, 84bitrd 245 . . . . . . . . 9  |-  ( ph  ->  ( U. dom  O  e.  ( `' O `  X )  <->  ( O `  U. dom  O )  e.  X ) )
8671, 85mtbid 292 . . . . . . . 8  |-  ( ph  ->  -.  ( O `  U. dom  O )  e.  X )
878sseld 3307 . . . . . . . . . 10  |-  ( ph  ->  ( ( O `  U. dom  O )  e.  ( `' G "
( _V  \  1o ) )  ->  ( O `  U. dom  O
)  e.  X ) )
88 onss 4730 . . . . . . . . . . . . . . . 16  |-  ( B  e.  On  ->  B  C_  On )
893, 88syl 16 . . . . . . . . . . . . . . 15  |-  ( ph  ->  B  C_  On )
9034, 89sstrd 3318 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( `' F "
( _V  \  1o ) )  C_  On )
914oif 7455 . . . . . . . . . . . . . . . 16  |-  O : dom  O --> ( `' F " ( _V  \  1o ) )
9291ffvelrni 5828 . . . . . . . . . . . . . . 15  |-  ( U. dom  O  e.  dom  O  ->  ( O `  U. dom  O )  e.  ( `' F " ( _V 
\  1o ) ) )
9374, 92syl 16 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( O `  U. dom  O )  e.  ( `' F " ( _V 
\  1o ) ) )
9490, 93sseldd 3309 . . . . . . . . . . . . 13  |-  ( ph  ->  ( O `  U. dom  O )  e.  On )
95 eloni 4551 . . . . . . . . . . . . 13  |-  ( ( O `  U. dom  O )  e.  On  ->  Ord  ( O `  U. dom  O ) )
9694, 95syl 16 . . . . . . . . . . . 12  |-  ( ph  ->  Ord  ( O `  U. dom  O ) )
97 ordn2lp 4561 . . . . . . . . . . . 12  |-  ( Ord  ( O `  U. dom  O )  ->  -.  ( ( O `  U. dom  O )  e.  X  /\  X  e.  ( O `  U. dom  O ) ) )
9896, 97syl 16 . . . . . . . . . . 11  |-  ( ph  ->  -.  ( ( O `
 U. dom  O
)  e.  X  /\  X  e.  ( O `  U. dom  O ) ) )
99 imnan 412 . . . . . . . . . . 11  |-  ( ( ( O `  U. dom  O )  e.  X  ->  -.  X  e.  ( O `  U. dom  O ) )  <->  -.  (
( O `  U. dom  O )  e.  X  /\  X  e.  ( O `  U. dom  O
) ) )
10098, 99sylibr 204 . . . . . . . . . 10  |-  ( ph  ->  ( ( O `  U. dom  O )  e.  X  ->  -.  X  e.  ( O `  U. dom  O ) ) )
10187, 100syld 42 . . . . . . . . 9  |-  ( ph  ->  ( ( O `  U. dom  O )  e.  ( `' G "
( _V  \  1o ) )  ->  -.  X  e.  ( O `  U. dom  O ) ) )
102 onelon 4566 . . . . . . . . . . . . 13  |-  ( ( B  e.  On  /\  X  e.  B )  ->  X  e.  On )
1033, 6, 102syl2anc 643 . . . . . . . . . . . 12  |-  ( ph  ->  X  e.  On )
104 eloni 4551 . . . . . . . . . . . 12  |-  ( X  e.  On  ->  Ord  X )
105103, 104syl 16 . . . . . . . . . . 11  |-  ( ph  ->  Ord  X )
106 ordirr 4559 . . . . . . . . . . 11  |-  ( Ord 
X  ->  -.  X  e.  X )
107105, 106syl 16 . . . . . . . . . 10  |-  ( ph  ->  -.  X  e.  X
)
108 elsni 3798 . . . . . . . . . . . 12  |-  ( ( O `  U. dom  O )  e.  { X }  ->  ( O `  U. dom  O )  =  X )
109108eleq2d 2471 . . . . . . . . . . 11  |-  ( ( O `  U. dom  O )  e.  { X }  ->  ( X  e.  ( O `  U. dom  O )  <->  X  e.  X ) )
110109notbid 286 . . . . . . . . . 10  |-  ( ( O `  U. dom  O )  e.  { X }  ->  ( -.  X  e.  ( O `  U. dom  O )  <->  -.  X  e.  X ) )
111107, 110syl5ibrcom 214 . . . . . . . . 9  |-  ( ph  ->  ( ( O `  U. dom  O )  e. 
{ X }  ->  -.  X  e.  ( O `
 U. dom  O
) ) )
112 df1o2 6695 . . . . . . . . . . . . . 14  |-  1o  =  { (/) }
113112difeq2i 3422 . . . . . . . . . . . . 13  |-  ( _V 
\  1o )  =  ( _V  \  { (/)
} )
114113imaeq2i 5160 . . . . . . . . . . . 12  |-  ( `' F " ( _V 
\  1o ) )  =  ( `' F " ( _V  \  { (/)
} ) )
115 eldifi 3429 . . . . . . . . . . . . . . . 16  |-  ( k  e.  ( B  \ 
( ( `' G " ( _V  \  1o ) )  u.  { X } ) )  -> 
k  e.  B )
116115adantl 453 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  k  e.  ( B  \  (
( `' G "
( _V  \  1o ) )  u.  { X } ) ) )  ->  k  e.  B
)
1177adantr 452 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  k  e.  ( B  \  (
( `' G "
( _V  \  1o ) )  u.  { X } ) ) )  ->  Y  e.  A
)
118 fvex 5701 . . . . . . . . . . . . . . . 16  |-  ( G `
 k )  e. 
_V
119 ifexg 3758 . . . . . . . . . . . . . . . 16  |-  ( ( Y  e.  A  /\  ( G `  k )  e.  _V )  ->  if ( k  =  X ,  Y ,  ( G `  k ) )  e.  _V )
120117, 118, 119sylancl 644 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  k  e.  ( B  \  (
( `' G "
( _V  \  1o ) )  u.  { X } ) ) )  ->  if ( k  =  X ,  Y ,  ( G `  k ) )  e. 
_V )
121 eqeq1 2410 . . . . . . . . . . . . . . . . 17  |-  ( t  =  k  ->  (
t  =  X  <->  k  =  X ) )
122 fveq2 5687 . . . . . . . . . . . . . . . . 17  |-  ( t  =  k  ->  ( G `  t )  =  ( G `  k ) )
123121, 122ifbieq2d 3719 . . . . . . . . . . . . . . . 16  |-  ( t  =  k  ->  if ( t  =  X ,  Y ,  ( G `  t ) )  =  if ( k  =  X ,  Y ,  ( G `  k ) ) )
124123, 9fvmptg 5763 . . . . . . . . . . . . . . 15  |-  ( ( k  e.  B  /\  if ( k  =  X ,  Y ,  ( G `  k ) )  e.  _V )  ->  ( F `  k
)  =  if ( k  =  X ,  Y ,  ( G `  k ) ) )
125116, 120, 124syl2anc 643 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  k  e.  ( B  \  (
( `' G "
( _V  \  1o ) )  u.  { X } ) ) )  ->  ( F `  k )  =  if ( k  =  X ,  Y ,  ( G `  k ) ) )
126 eldifn 3430 . . . . . . . . . . . . . . . . 17  |-  ( k  e.  ( B  \ 
( ( `' G " ( _V  \  1o ) )  u.  { X } ) )  ->  -.  k  e.  (
( `' G "
( _V  \  1o ) )  u.  { X } ) )
127126adantl 453 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  k  e.  ( B  \  (
( `' G "
( _V  \  1o ) )  u.  { X } ) ) )  ->  -.  k  e.  ( ( `' G " ( _V  \  1o ) )  u.  { X } ) )
128 elsn 3789 . . . . . . . . . . . . . . . . 17  |-  ( k  e.  { X }  <->  k  =  X )
129 elun2 3475 . . . . . . . . . . . . . . . . 17  |-  ( k  e.  { X }  ->  k  e.  ( ( `' G " ( _V 
\  1o ) )  u.  { X }
) )
130128, 129sylbir 205 . . . . . . . . . . . . . . . 16  |-  ( k  =  X  ->  k  e.  ( ( `' G " ( _V  \  1o ) )  u.  { X } ) )
131127, 130nsyl 115 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  k  e.  ( B  \  (
( `' G "
( _V  \  1o ) )  u.  { X } ) ) )  ->  -.  k  =  X )
132 iffalse 3706 . . . . . . . . . . . . . . 15  |-  ( -.  k  =  X  ->  if ( k  =  X ,  Y ,  ( G `  k ) )  =  ( G `
 k ) )
133131, 132syl 16 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  k  e.  ( B  \  (
( `' G "
( _V  \  1o ) )  u.  { X } ) ) )  ->  if ( k  =  X ,  Y ,  ( G `  k ) )  =  ( G `  k
) )
134 ssun1 3470 . . . . . . . . . . . . . . . . 17  |-  ( `' G " ( _V 
\  1o ) ) 
C_  ( ( `' G " ( _V 
\  1o ) )  u.  { X }
)
135 sscon 3441 . . . . . . . . . . . . . . . . 17  |-  ( ( `' G " ( _V 
\  1o ) ) 
C_  ( ( `' G " ( _V 
\  1o ) )  u.  { X }
)  ->  ( B  \  ( ( `' G " ( _V  \  1o ) )  u.  { X } ) )  C_  ( B  \  ( `' G " ( _V 
\  1o ) ) ) )
136134, 135ax-mp 8 . . . . . . . . . . . . . . . 16  |-  ( B 
\  ( ( `' G " ( _V 
\  1o ) )  u.  { X }
) )  C_  ( B  \  ( `' G " ( _V  \  1o ) ) )
137136sseli 3304 . . . . . . . . . . . . . . 15  |-  ( k  e.  ( B  \ 
( ( `' G " ( _V  \  1o ) )  u.  { X } ) )  -> 
k  e.  ( B 
\  ( `' G " ( _V  \  1o ) ) ) )
138113imaeq2i 5160 . . . . . . . . . . . . . . . . 17  |-  ( `' G " ( _V 
\  1o ) )  =  ( `' G " ( _V  \  { (/)
} ) )
139 eqimss2 3361 . . . . . . . . . . . . . . . . 17  |-  ( ( `' G " ( _V 
\  1o ) )  =  ( `' G " ( _V  \  { (/)
} ) )  -> 
( `' G "
( _V  \  { (/)
} ) )  C_  ( `' G " ( _V 
\  1o ) ) )
140138, 139mp1i 12 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( `' G "
( _V  \  { (/)
} ) )  C_  ( `' G " ( _V 
\  1o ) ) )
14127, 140suppssr 5823 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  k  e.  ( B  \  ( `' G " ( _V 
\  1o ) ) ) )  ->  ( G `  k )  =  (/) )
142137, 141sylan2 461 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  k  e.  ( B  \  (
( `' G "
( _V  \  1o ) )  u.  { X } ) ) )  ->  ( G `  k )  =  (/) )
143125, 133, 1423eqtrd 2440 . . . . . . . . . . . . 13  |-  ( (
ph  /\  k  e.  ( B  \  (
( `' G "
( _V  \  1o ) )  u.  { X } ) ) )  ->  ( F `  k )  =  (/) )
14431, 143suppss 5822 . . . . . . . . . . . 12  |-  ( ph  ->  ( `' F "
( _V  \  { (/)
} ) )  C_  ( ( `' G " ( _V  \  1o ) )  u.  { X } ) )
145114, 144syl5eqss 3352 . . . . . . . . . . 11  |-  ( ph  ->  ( `' F "
( _V  \  1o ) )  C_  (
( `' G "
( _V  \  1o ) )  u.  { X } ) )
146145, 93sseldd 3309 . . . . . . . . . 10  |-  ( ph  ->  ( O `  U. dom  O )  e.  ( ( `' G "
( _V  \  1o ) )  u.  { X } ) )
147 elun 3448 . . . . . . . . . 10  |-  ( ( O `  U. dom  O )  e.  ( ( `' G " ( _V 
\  1o ) )  u.  { X }
)  <->  ( ( O `
 U. dom  O
)  e.  ( `' G " ( _V 
\  1o ) )  \/  ( O `  U. dom  O )  e. 
{ X } ) )
148146, 147sylib 189 . . . . . . . . 9  |-  ( ph  ->  ( ( O `  U. dom  O )  e.  ( `' G "
( _V  \  1o ) )  \/  ( O `  U. dom  O
)  e.  { X } ) )
149101, 111, 148mpjaod 371 . . . . . . . 8  |-  ( ph  ->  -.  X  e.  ( O `  U. dom  O ) )
150 ioran 477 . . . . . . . 8  |-  ( -.  ( ( O `  U. dom  O )  e.  X  \/  X  e.  ( O `  U. dom  O ) )  <->  ( -.  ( O `  U. dom  O )  e.  X  /\  -.  X  e.  ( O `  U. dom  O
) ) )
15186, 149, 150sylanbrc 646 . . . . . . 7  |-  ( ph  ->  -.  ( ( O `
 U. dom  O
)  e.  X  \/  X  e.  ( O `  U. dom  O ) ) )
152 ordtri3 4577 . . . . . . . 8  |-  ( ( Ord  ( O `  U. dom  O )  /\  Ord  X )  ->  (
( O `  U. dom  O )  =  X  <->  -.  ( ( O `  U. dom  O )  e.  X  \/  X  e.  ( O `  U. dom  O ) ) ) )
15396, 105, 152syl2anc 643 . . . . . . 7  |-  ( ph  ->  ( ( O `  U. dom  O )  =  X  <->  -.  ( ( O `  U. dom  O
)  e.  X  \/  X  e.  ( O `  U. dom  O ) ) ) )
154151, 153mpbird 224 . . . . . 6  |-  ( ph  ->  ( O `  U. dom  O )  =  X )
155154oveq2d 6056 . . . . 5  |-  ( ph  ->  ( A  ^o  ( O `  U. dom  O
) )  =  ( A  ^o  X ) )
156154fveq2d 5691 . . . . . 6  |-  ( ph  ->  ( F `  ( O `  U. dom  O
) )  =  ( F `  X ) )
157156, 46eqtrd 2436 . . . . 5  |-  ( ph  ->  ( F `  ( O `  U. dom  O
) )  =  Y )
158155, 157oveq12d 6058 . . . 4  |-  ( ph  ->  ( ( A  ^o  ( O `  U. dom  O ) )  .o  ( F `  ( O `  U. dom  O ) ) )  =  ( ( A  ^o  X
)  .o  Y ) )
159 nnord 4812 . . . . . . . . 9  |-  ( U. dom  O  e.  om  ->  Ord  U. dom  O )
16020, 159syl 16 . . . . . . . 8  |-  ( ph  ->  Ord  U. dom  O
)
161 sssucid 4618 . . . . . . . . . 10  |-  U. dom  O 
C_  suc  U. dom  O
162161, 14syl5sseqr 3357 . . . . . . . . 9  |-  ( ph  ->  U. dom  O  C_  dom  O )
163 f1ofo 5640 . . . . . . . . . . . . 13  |-  ( O : dom  O -1-1-onto-> ( `' F " ( _V 
\  1o ) )  ->  O : dom  O
-onto-> ( `' F "
( _V  \  1o ) ) )
16440, 163syl 16 . . . . . . . . . . . 12  |-  ( ph  ->  O : dom  O -onto->
( `' F "
( _V  \  1o ) ) )
165 foima 5617 . . . . . . . . . . . 12  |-  ( O : dom  O -onto-> ( `' F " ( _V 
\  1o ) )  ->  ( O " dom  O )  =  ( `' F " ( _V 
\  1o ) ) )
166164, 165syl 16 . . . . . . . . . . 11  |-  ( ph  ->  ( O " dom  O )  =  ( `' F " ( _V 
\  1o ) ) )
167 ffn 5550 . . . . . . . . . . . . . 14  |-  ( O : dom  O --> ( `' F " ( _V 
\  1o ) )  ->  O  Fn  dom  O )
16891, 167ax-mp 8 . . . . . . . . . . . . 13  |-  O  Fn  dom  O
169 fnsnfv 5745 . . . . . . . . . . . . 13  |-  ( ( O  Fn  dom  O  /\  U. dom  O  e. 
dom  O )  ->  { ( O `  U. dom  O ) }  =  ( O " { U. dom  O }
) )
170168, 74, 169sylancr 645 . . . . . . . . . . . 12  |-  ( ph  ->  { ( O `  U. dom  O ) }  =  ( O " { U. dom  O }
) )
171154sneqd 3787 . . . . . . . . . . . 12  |-  ( ph  ->  { ( O `  U. dom  O ) }  =  { X }
)
172170, 171eqtr3d 2438 . . . . . . . . . . 11  |-  ( ph  ->  ( O " { U. dom  O } )  =  { X }
)
173166, 172difeq12d 3426 . . . . . . . . . 10  |-  ( ph  ->  ( ( O " dom  O )  \  ( O " { U. dom  O } ) )  =  ( ( `' F " ( _V  \  1o ) )  \  { X } ) )
174 ordirr 4559 . . . . . . . . . . . . . . . . 17  |-  ( Ord  U. dom  O  ->  -.  U.
dom  O  e.  U. dom  O )
175160, 174syl 16 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  -.  U. dom  O  e.  U. dom  O )
176 disjsn 3828 . . . . . . . . . . . . . . . 16  |-  ( ( U. dom  O  i^i  { U. dom  O }
)  =  (/)  <->  -.  U. dom  O  e.  U. dom  O
)
177175, 176sylibr 204 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( U. dom  O  i^i  { U. dom  O } )  =  (/) )
178 disj3 3632 . . . . . . . . . . . . . . 15  |-  ( ( U. dom  O  i^i  { U. dom  O }
)  =  (/)  <->  U. dom  O  =  ( U. dom  O 
\  { U. dom  O } ) )
179177, 178sylib 189 . . . . . . . . . . . . . 14  |-  ( ph  ->  U. dom  O  =  ( U. dom  O  \  { U. dom  O } ) )
180 difun2 3667 . . . . . . . . . . . . . 14  |-  ( ( U. dom  O  u.  { U. dom  O }
)  \  { U. dom  O } )  =  ( U. dom  O  \  { U. dom  O }
)
181179, 180syl6eqr 2454 . . . . . . . . . . . . 13  |-  ( ph  ->  U. dom  O  =  ( ( U. dom  O  u.  { U. dom  O } )  \  { U. dom  O } ) )
182 df-suc 4547 . . . . . . . . . . . . . . 15  |-  suc  U. dom  O  =  ( U. dom  O  u.  { U. dom  O } )
18314, 182syl6eq 2452 . . . . . . . . . . . . . 14  |-  ( ph  ->  dom  O  =  ( U. dom  O  u.  { U. dom  O }
) )
184183difeq1d 3424 . . . . . . . . . . . . 13  |-  ( ph  ->  ( dom  O  \  { U. dom  O }
)  =  ( ( U. dom  O  u.  { U. dom  O }
)  \  { U. dom  O } ) )
185181, 184eqtr4d 2439 . . . . . . . . . . . 12  |-  ( ph  ->  U. dom  O  =  ( dom  O  \  { U. dom  O }
) )
186185imaeq2d 5162 . . . . . . . . . . 11  |-  ( ph  ->  ( O " U. dom  O )  =  ( O " ( dom 
O  \  { U. dom  O } ) ) )
187 dff1o3 5639 . . . . . . . . . . . . 13  |-  ( O : dom  O -1-1-onto-> ( `' F " ( _V 
\  1o ) )  <-> 
( O : dom  O
-onto-> ( `' F "
( _V  \  1o ) )  /\  Fun  `' O ) )
188187simprbi 451 . . . . . . . . . . . 12  |-  ( O : dom  O -1-1-onto-> ( `' F " ( _V 
\  1o ) )  ->  Fun  `' O
)
189 imadif 5487 . . . . . . . . . . . 12  |-  ( Fun  `' O  ->  ( O
" ( dom  O  \  { U. dom  O } ) )  =  ( ( O " dom  O )  \  ( O " { U. dom  O } ) ) )
19040, 188, 1893syl 19 . . . . . . . . . . 11  |-  ( ph  ->  ( O " ( dom  O  \  { U. dom  O } ) )  =  ( ( O
" dom  O )  \  ( O " { U. dom  O }
) ) )
191186, 190eqtrd 2436 . . . . . . . . . 10  |-  ( ph  ->  ( O " U. dom  O )  =  ( ( O " dom  O )  \  ( O
" { U. dom  O } ) ) )
1928, 107ssneldd 3311 . . . . . . . . . . . . 13  |-  ( ph  ->  -.  X  e.  ( `' G " ( _V 
\  1o ) ) )
193 disjsn 3828 . . . . . . . . . . . . 13  |-  ( ( ( `' G "
( _V  \  1o ) )  i^i  { X } )  =  (/)  <->  -.  X  e.  ( `' G " ( _V  \  1o ) ) )
194192, 193sylibr 204 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( `' G " ( _V  \  1o ) )  i^i  { X } )  =  (/) )
195 fvex 5701 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( G `
 X )  e. 
_V
196 dif1o 6703 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( G `  X )  e.  ( _V  \  1o )  <->  ( ( G `
 X )  e. 
_V  /\  ( G `  X )  =/=  (/) ) )
197195, 196mpbiran 885 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( G `  X )  e.  ( _V  \  1o )  <->  ( G `  X )  =/=  (/) )
198 ffn 5550 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( G : B --> A  ->  G  Fn  B )
19927, 198syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  G  Fn  B )
200 elpreima 5809 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( G  Fn  B  ->  ( X  e.  ( `' G " ( _V  \  1o ) )  <->  ( X  e.  B  /\  ( G `  X )  e.  ( _V  \  1o ) ) ) )
201199, 200syl 16 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( X  e.  ( `' G " ( _V 
\  1o ) )  <-> 
( X  e.  B  /\  ( G `  X
)  e.  ( _V 
\  1o ) ) ) )
2028sseld 3307 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( X  e.  ( `' G " ( _V 
\  1o ) )  ->  X  e.  X
) )
203201, 202sylbird 227 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( ( X  e.  B  /\  ( G `
 X )  e.  ( _V  \  1o ) )  ->  X  e.  X ) )
2046, 203mpand 657 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( ( G `  X )  e.  ( _V  \  1o )  ->  X  e.  X
) )
205197, 204syl5bir 210 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( ( G `  X )  =/=  (/)  ->  X  e.  X ) )
206205necon1bd 2635 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( -.  X  e.  X  ->  ( G `  X )  =  (/) ) )
207107, 206mpd 15 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( G `  X
)  =  (/) )
208207adantr 452 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  k  e.  ( B  \  ( `' F " ( _V 
\  { (/) } ) ) ) )  -> 
( G `  X
)  =  (/) )
209 fveq2 5687 . . . . . . . . . . . . . . . . . 18  |-  ( k  =  X  ->  ( G `  k )  =  ( G `  X ) )
210209eqeq1d 2412 . . . . . . . . . . . . . . . . 17  |-  ( k  =  X  ->  (
( G `  k
)  =  (/)  <->  ( G `  X )  =  (/) ) )
211208, 210syl5ibrcom 214 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  k  e.  ( B  \  ( `' F " ( _V 
\  { (/) } ) ) ) )  -> 
( k  =  X  ->  ( G `  k )  =  (/) ) )
212 eldifi 3429 . . . . . . . . . . . . . . . . . . . 20  |-  ( k  e.  ( B  \ 
( `' F "
( _V  \  { (/)
} ) ) )  ->  k  e.  B
)
213212adantl 453 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  k  e.  ( B  \  ( `' F " ( _V 
\  { (/) } ) ) ) )  -> 
k  e.  B )
2147adantr 452 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  k  e.  ( B  \  ( `' F " ( _V 
\  { (/) } ) ) ) )  ->  Y  e.  A )
215214, 118, 119sylancl 644 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  k  e.  ( B  \  ( `' F " ( _V 
\  { (/) } ) ) ) )  ->  if ( k  =  X ,  Y ,  ( G `  k ) )  e.  _V )
216213, 215, 124syl2anc 643 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  k  e.  ( B  \  ( `' F " ( _V 
\  { (/) } ) ) ) )  -> 
( F `  k
)  =  if ( k  =  X ,  Y ,  ( G `  k ) ) )
217 ssid 3327 . . . . . . . . . . . . . . . . . . . 20  |-  ( `' F " ( _V 
\  { (/) } ) )  C_  ( `' F " ( _V  \  { (/) } ) )
218217a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( `' F "
( _V  \  { (/)
} ) )  C_  ( `' F " ( _V 
\  { (/) } ) ) )
21931, 218suppssr 5823 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  k  e.  ( B  \  ( `' F " ( _V 
\  { (/) } ) ) ) )  -> 
( F `  k
)  =  (/) )
220216, 219eqtr3d 2438 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  k  e.  ( B  \  ( `' F " ( _V 
\  { (/) } ) ) ) )  ->  if ( k  =  X ,  Y ,  ( G `  k ) )  =  (/) )
221132eqeq1d 2412 . . . . . . . . . . . . . . . . 17  |-  ( -.  k  =  X  -> 
( if ( k  =  X ,  Y ,  ( G `  k ) )  =  (/) 
<->  ( G `  k
)  =  (/) ) )
222220, 221syl5ibcom 212 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  k  e.  ( B  \  ( `' F " ( _V 
\  { (/) } ) ) ) )  -> 
( -.  k  =  X  ->  ( G `  k )  =  (/) ) )
223211, 222pm2.61d 152 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  k  e.  ( B  \  ( `' F " ( _V 
\  { (/) } ) ) ) )  -> 
( G `  k
)  =  (/) )
22427, 223suppss 5822 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( `' G "
( _V  \  { (/)
} ) )  C_  ( `' F " ( _V 
\  { (/) } ) ) )
225224, 138, 1143sstr4g 3349 . . . . . . . . . . . . 13  |-  ( ph  ->  ( `' G "
( _V  \  1o ) )  C_  ( `' F " ( _V 
\  1o ) ) )
226 reldisj 3631 . . . . . . . . . . . . 13  |-  ( ( `' G " ( _V 
\  1o ) ) 
C_  ( `' F " ( _V  \  1o ) )  ->  (
( ( `' G " ( _V  \  1o ) )  i^i  { X } )  =  (/)  <->  ( `' G " ( _V 
\  1o ) ) 
C_  ( ( `' F " ( _V 
\  1o ) ) 
\  { X }
) ) )
227225, 226syl 16 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( ( `' G " ( _V 
\  1o ) )  i^i  { X }
)  =  (/)  <->  ( `' G " ( _V  \  1o ) )  C_  (
( `' F "
( _V  \  1o ) )  \  { X } ) ) )
228194, 227mpbid 202 . . . . . . . . . . 11  |-  ( ph  ->  ( `' G "
( _V  \  1o ) )  C_  (
( `' F "
( _V  \  1o ) )  \  { X } ) )
229 uncom 3451 . . . . . . . . . . . . 13  |-  ( ( `' G " ( _V 
\  1o ) )  u.  { X }
)  =  ( { X }  u.  ( `' G " ( _V 
\  1o ) ) )
230145, 229syl6sseq 3354 . . . . . . . . . . . 12  |-  ( ph  ->  ( `' F "
( _V  \  1o ) )  C_  ( { X }  u.  ( `' G " ( _V 
\  1o ) ) ) )
231 ssundif 3671 . . . . . . . . . . . 12  |-  ( ( `' F " ( _V 
\  1o ) ) 
C_  ( { X }  u.  ( `' G " ( _V  \  1o ) ) )  <->  ( ( `' F " ( _V 
\  1o ) ) 
\  { X }
)  C_  ( `' G " ( _V  \  1o ) ) )
232230, 231sylib 189 . . . . . . . . . . 11  |-  ( ph  ->  ( ( `' F " ( _V  \  1o ) )  \  { X } )  C_  ( `' G " ( _V 
\  1o ) ) )
233228, 232eqssd 3325 . . . . . . . . . 10  |-  ( ph  ->  ( `' G "
( _V  \  1o ) )  =  ( ( `' F "
( _V  \  1o ) )  \  { X } ) )
234173, 191, 2333eqtr4rd 2447 . . . . . . . . 9  |-  ( ph  ->  ( `' G "
( _V  \  1o ) )  =  ( O " U. dom  O ) )
235 isores3 6014 . . . . . . . . 9  |-  ( ( O  Isom  _E  ,  _E  ( dom  O ,  ( `' F " ( _V 
\  1o ) ) )  /\  U. dom  O 
C_  dom  O  /\  ( `' G " ( _V 
\  1o ) )  =  ( O " U. dom  O ) )  ->  ( O  |`  U.
dom  O )  Isom  _E  ,  _E  ( U. dom  O ,  ( `' G " ( _V 
\  1o ) ) ) )
23638, 162, 234, 235syl3anc 1184 . . . . . . . 8  |-  ( ph  ->  ( O  |`  U. dom  O )  Isom  _E  ,  _E  ( U. dom  O , 
( `' G "
( _V  \  1o ) ) ) )
237 cantnfp1.k . . . . . . . . . . 11  |-  K  = OrdIso
(  _E  ,  ( `' G " ( _V 
\  1o ) ) )
2381, 2, 3, 237, 5cantnfcl 7578 . . . . . . . . . 10  |-  ( ph  ->  (  _E  We  ( `' G " ( _V 
\  1o ) )  /\  dom  K  e. 
om ) )
239238simpld 446 . . . . . . . . 9  |-  ( ph  ->  _E  We  ( `' G " ( _V 
\  1o ) ) )
240 epse 4525 . . . . . . . . 9  |-  _E Se  ( `' G " ( _V 
\  1o ) )
241237oieu 7464 . . . . . . . . 9  |-  ( (  _E  We  ( `' G " ( _V 
\  1o ) )  /\  _E Se  ( `' G " ( _V 
\  1o ) ) )  ->  ( ( Ord  U. dom  O  /\  ( O  |`  U. dom  O )  Isom  _E  ,  _E  ( U. dom  O , 
( `' G "
( _V  \  1o ) ) ) )  <-> 
( U. dom  O  =  dom  K  /\  ( O  |`  U. dom  O
)  =  K ) ) )
242239, 240, 241sylancl 644 . . . . . . . 8  |-  ( ph  ->  ( ( Ord  U. dom  O  /\  ( O  |`  U. dom  O ) 
Isom  _E  ,  _E  ( U. dom  O , 
( `' G "
( _V  \  1o ) ) ) )  <-> 
( U. dom  O  =  dom  K  /\  ( O  |`  U. dom  O
)  =  K ) ) )
243160, 236, 242mpbi2and 888 . . . . . . 7  |-  ( ph  ->  ( U. dom  O  =  dom  K  /\  ( O  |`  U. dom  O
)  =  K ) )
244243simpld 446 . . . . . 6  |-  ( ph  ->  U. dom  O  =  dom  K )
245244fveq2d 5691 . . . . 5  |-  ( ph  ->  ( M `  U. dom  O )  =  ( M `  dom  K
) )
246 eleq1 2464 . . . . . . . . . 10  |-  ( x  =  (/)  ->  ( x  e.  dom  O  <->  (/)  e.  dom  O ) )
247 fveq2 5687 . . . . . . . . . . 11  |-  ( x  =  (/)  ->  ( H `
 x )  =  ( H `  (/) ) )
248 fveq2 5687 . . . . . . . . . . . 12  |-  ( x  =  (/)  ->  ( M `
 x )  =  ( M `  (/) ) )
249 0ex 4299 . . . . . . . . . . . . 13  |-  (/)  e.  _V
250 cantnfp1.m . . . . . . . . . . . . . 14  |-  M  = seq𝜔 ( ( k  e.  _V ,  z  e.  _V  |->  ( ( ( A  ^o  ( K `  k ) )  .o  ( G `  ( K `  k )
) )  +o  z
) ) ,  (/) )
251250seqom0g 6672 . . . . . . . . . . . . 13  |-  ( (/)  e.  _V  ->  ( M `  (/) )  =  (/) )
252249, 251ax-mp 8 . . . . . . . . . . . 12  |-  ( M `
 (/) )  =  (/)
253248, 252syl6eq 2452 . . . . . . . . . . 11  |-  ( x  =  (/)  ->  ( M `
 x )  =  (/) )
254247, 253eqeq12d 2418 . . . . . . . . . 10  |-  ( x  =  (/)  ->  ( ( H `  x )  =  ( M `  x )  <->  ( H `  (/) )  =  (/) ) )
255246, 254imbi12d 312 . . . . . . . . 9  |-  ( x  =  (/)  ->  ( ( x  e.  dom  O  ->  ( H `  x
)  =  ( M `
 x ) )  <-> 
( (/)  e.  dom  O  ->  ( H `  (/) )  =  (/) ) ) )
256255imbi2d 308 . . . . . . . 8  |-  ( x  =  (/)  ->  ( (
ph  ->  ( x  e. 
dom  O  ->  ( H `
 x )  =  ( M `  x
) ) )  <->  ( ph  ->  ( (/)  e.  dom  O  ->  ( H `  (/) )  =  (/) ) ) ) )
257 eleq1 2464 . . . . . . . . . 10  |-  ( x  =  y  ->  (
x  e.  dom  O  <->  y  e.  dom  O ) )
258 fveq2 5687 . . . . . . . . . . 11  |-  ( x  =  y  ->  ( H `  x )  =  ( H `  y ) )
259 fveq2 5687 . . . . . . . . . . 11  |-  ( x  =  y  ->  ( M `  x )  =  ( M `  y ) )
260258, 259eqeq12d 2418 . . . . . . . . . 10  |-  ( x  =  y  ->  (
( H `  x
)  =  ( M `
 x )  <->  ( H `  y )  =  ( M `  y ) ) )
261257, 260imbi12d 312 . . . . . . . . 9  |-  ( x  =  y  ->  (
( x  e.  dom  O  ->  ( H `  x )  =  ( M `  x ) )  <->  ( y  e. 
dom  O  ->  ( H `
 y )  =  ( M `  y
) ) ) )
262261imbi2d 308 . . . . . . . 8  |-  ( x  =  y  ->  (
( ph  ->  ( x  e.  dom  O  -> 
( H `  x
)  =  ( M `
 x ) ) )  <->  ( ph  ->  ( y  e.  dom  O  ->  ( H `  y
)  =  ( M `
 y ) ) ) ) )
263 eleq1 2464 . . . . . . . . . 10  |-  ( x  =  suc  y  -> 
( x  e.  dom  O  <->  suc  y  e.  dom  O ) )
264 fveq2 5687 . . . . . . . . . . 11  |-  ( x  =  suc  y  -> 
( H `  x
)  =  ( H `
 suc  y )
)
265 fveq2 5687 . . . . . . . . . . 11  |-  ( x  =  suc  y  -> 
( M `  x
)  =  ( M `
 suc  y )
)
266264, 265eqeq12d 2418 . . . . . . . . . 10  |-  ( x  =  suc  y  -> 
( ( H `  x )  =  ( M `  x )  <-> 
( H `  suc  y )  =  ( M `  suc  y
) ) )
267263, 266imbi12d 312 . . . . . . . . 9  |-  ( x  =  suc  y  -> 
( ( x  e. 
dom  O  ->  ( H `
 x )  =  ( M `  x
) )  <->  ( suc  y  e.  dom  O  -> 
( H `  suc  y )  =  ( M `  suc  y
) ) ) )
268267imbi2d 308 . . . . . . . 8  |-  ( x  =  suc  y  -> 
( ( ph  ->  ( x  e.  dom  O  ->  ( H `  x
)  =  ( M `
 x ) ) )  <->  ( ph  ->  ( suc  y  e.  dom  O  ->  ( H `  suc  y )  =  ( M `  suc  y
) ) ) ) )
269 eleq1 2464 . . . . . . . . . 10  |-  ( x  =  U. dom  O  ->  ( x  e.  dom  O  <->  U. dom  O  e.  dom  O ) )
270 fveq2 5687 . . . . . . . . . . 11  |-  ( x  =  U. dom  O  ->  ( H `  x
)  =  ( H `
 U. dom  O
) )
271 fveq2 5687 . . . . . . . . . . 11  |-  ( x  =  U. dom  O  ->  ( M `  x
)  =  ( M `
 U. dom  O
) )
272270, 271eqeq12d 2418 . . . . . . . . . 10  |-  ( x  =  U. dom  O  ->  ( ( H `  x )  =  ( M `  x )  <-> 
( H `  U. dom  O )  =  ( M `  U. dom  O ) ) )
273269, 272imbi12d 312 . . . . . . . . 9  |-  ( x  =  U. dom  O  ->  ( ( x  e. 
dom  O  ->  ( H `
 x )  =  ( M `  x
) )  <->  ( U. dom  O  e.  dom  O  ->  ( H `  U. dom  O )  =  ( M `  U. dom  O ) ) ) )
274273imbi2d 308 . . . . . . . 8  |-  ( x  =  U. dom  O  ->  ( ( ph  ->  ( x  e.  dom  O  ->  ( H `  x
)  =  ( M `
 x ) ) )  <->  ( ph  ->  ( U. dom  O  e. 
dom  O  ->  ( H `
 U. dom  O
)  =  ( M `
 U. dom  O
) ) ) ) )
27511seqom0g 6672 . . . . . . . . . 10  |-  ( (/)  e.  _V  ->  ( H `  (/) )  =  (/) )
276249, 275mp1i 12 . . . . . . . . 9  |-  ( (/)  e.  dom  O  ->  ( H `  (/) )  =  (/) )
277276a1i 11 . . . . . . . 8  |-  ( ph  ->  ( (/)  e.  dom  O  ->  ( H `  (/) )  =  (/) ) )
278 nnord 4812 . . . . . . . . . . . . . . . 16  |-  ( dom 
O  e.  om  ->  Ord 
dom  O )
27917, 278syl 16 . . . . . . . . . . . . . . 15  |-  ( ph  ->  Ord  dom  O )
280 ordtr 4555 . . . . . . . . . . . . . . 15  |-  ( Ord 
dom  O  ->  Tr  dom  O )
281279, 280syl 16 . . . . . . . . . . . . . 14  |-  ( ph  ->  Tr  dom  O )
282 trsuc 4625 . . . . . . . . . . . . . 14  |-  ( ( Tr  dom  O  /\  suc  y  e.  dom  O )  ->  y  e.  dom  O )
283281, 282sylan 458 . . . . . . . . . . . . 13  |-  ( (
ph  /\  suc  y  e. 
dom  O )  -> 
y  e.  dom  O
)
284283ex 424 . . . . . . . . . . . 12  |-  ( ph  ->  ( suc  y  e. 
dom  O  ->  y  e. 
dom  O ) )
285284imim1d 71 . . . . . . . . . . 11  |-  ( ph  ->  ( ( y  e. 
dom  O  ->  ( H `
 y )  =  ( M `  y
) )  ->  ( suc  y  e.  dom  O  ->  ( H `  y )  =  ( M `  y ) ) ) )
286 oveq2 6048 . . . . . . . . . . . . . 14  |-  ( ( H `  y )  =  ( M `  y )  ->  (
( ( A  ^o  ( O `  y ) )  .o  ( F `
 ( O `  y ) ) )  +o  ( H `  y ) )  =  ( ( ( A  ^o  ( O `  y ) )  .o  ( F `  ( O `  y )
) )  +o  ( M `  y )
) )
287 elnn 4814 . . . . . . . . . . . . . . . . . . 19  |-  ( ( y  e.  dom  O  /\  dom  O  e.  om )  ->  y  e.  om )
288287ancoms 440 . . . . . . . . . . . . . . . . . 18  |-  ( ( dom  O  e.  om  /\  y  e.  dom  O
)  ->  y  e.  om )
28917, 288sylan 458 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  y  e.  dom  O )  ->  y  e.  om )
290283, 289syldan 457 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  suc  y  e. 
dom  O )  -> 
y  e.  om )
2911, 2, 3, 4, 10, 11cantnfsuc 7581 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  y  e.  om )  ->  ( H `  suc  y )  =  ( ( ( A  ^o  ( O `  y ) )  .o  ( F `  ( O `  y )
) )  +o  ( H `  y )
) )
292290, 291syldan 457 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  suc  y  e. 
dom  O )  -> 
( H `  suc  y )  =  ( ( ( A  ^o  ( O `  y ) )  .o  ( F `
 ( O `  y ) ) )  +o  ( H `  y ) ) )
2931, 2, 3, 237, 5, 250cantnfsuc 7581 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  y  e.  om )  ->  ( M `  suc  y )  =  ( ( ( A  ^o  ( K `  y ) )  .o  ( G `  ( K `  y )
) )  +o  ( M `  y )
) )
294290, 293syldan 457 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  suc  y  e. 
dom  O )  -> 
( M `  suc  y )  =  ( ( ( A  ^o  ( K `  y ) )  .o  ( G `
 ( K `  y ) ) )  +o  ( M `  y ) ) )
295243simprd 450 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( O  |`  U. dom  O )  =  K )
296295fveq1d 5689 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( ( O  |`  U.
dom  O ) `  y )  =  ( K `  y ) )
297296adantr 452 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  suc  y  e. 
dom  O )  -> 
( ( O  |`  U.
dom  O ) `  y )  =  ( K `  y ) )
29814eleq2d 2471 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( suc  y  e. 
dom  O  <->  suc  y  e.  suc  U.
dom  O ) )
299298biimpa 471 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  suc  y  e. 
dom  O )  ->  suc  y  e.  suc  U.
dom  O )
300160adantr 452 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  suc  y  e. 
dom  O )  ->  Ord  U. dom  O )
301 ordsucelsuc 4761 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( Ord  U. dom  O  ->  (
y  e.  U. dom  O  <->  suc  y  e.  suc  U.
dom  O ) )
302300, 301syl 16 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  suc  y  e. 
dom  O )  -> 
( y  e.  U. dom  O  <->  suc  y  e.  suc  U.
dom  O ) )
303299, 302mpbird 224 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  suc  y  e. 
dom  O )  -> 
y  e.  U. dom  O )
304 fvres 5704 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  e.  U. dom  O  ->  ( ( O  |`  U.
dom  O ) `  y )  =  ( O `  y ) )
305303, 304syl 16 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  suc  y  e. 
dom  O )  -> 
( ( O  |`  U.
dom  O ) `  y )  =  ( O `  y ) )
306297, 305eqtr3d 2438 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  suc  y  e. 
dom  O )  -> 
( K `  y
)  =  ( O `
 y ) )
307306oveq2d 6056 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  suc  y  e. 
dom  O )  -> 
( A  ^o  ( K `  y )
)  =  ( A  ^o  ( O `  y ) ) )
308 cnvimass 5183 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( `' G " ( _V 
\  1o ) ) 
C_  dom  G
309 fdm 5554 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( G : B --> A  ->  dom  G  =  B )
31027, 309syl 16 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  dom  G  =  B )
311308, 310syl5sseq 3356 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( `' G "
( _V  \  1o ) )  C_  B
)
312311adantr 452 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  suc  y  e. 
dom  O )  -> 
( `' G "
( _V  \  1o ) )  C_  B
)
313244adantr 452 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  suc  y  e. 
dom  O )  ->  U. dom  O  =  dom  K )
314303, 313eleqtrd 2480 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  suc  y  e. 
dom  O )  -> 
y  e.  dom  K
)
315237oif 7455 . . . . . . . . . . . . . . . . . . . . . . 23  |-  K : dom  K --> ( `' G " ( _V  \  1o ) )
316315ffvelrni 5828 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  e.  dom  K  -> 
( K `  y
)  e.  ( `' G " ( _V 
\  1o ) ) )
317314, 316syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  suc  y  e. 
dom  O )  -> 
( K `  y
)  e.  ( `' G " ( _V 
\  1o ) ) )
318312, 317sseldd 3309 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  suc  y  e. 
dom  O )  -> 
( K `  y
)  e.  B )
3197adantr 452 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  suc  y  e. 
dom  O )  ->  Y  e.  A )
320 fvex 5701 . . . . . . . . . . . . . . . . . . . . 21  |-  ( G `
 ( K `  y ) )  e. 
_V
321 ifexg 3758 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( Y  e.  A  /\  ( G `  ( K `
 y ) )  e.  _V )  ->  if ( ( K `  y )  =  X ,  Y ,  ( G `  ( K `
 y ) ) )  e.  _V )
322319, 320, 321sylancl 644 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  suc  y  e. 
dom  O )  ->  if ( ( K `  y )  =  X ,  Y ,  ( G `  ( K `
 y ) ) )  e.  _V )
323 eqeq1 2410 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( t  =  ( K `  y )  ->  (
t  =  X  <->  ( K `  y )  =  X ) )
324 fveq2 5687 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( t  =  ( K `  y )  ->  ( G `  t )  =  ( G `  ( K `  y ) ) )
325323, 324ifbieq2d 3719 . . . . . . . . . . . . . . . . . . . . 21  |-  ( t  =  ( K `  y )  ->  if ( t  =  X ,  Y ,  ( G `  t ) )  =  if ( ( K `  y
)  =  X ,  Y ,  ( G `  ( K `  y
) ) ) )
326325, 9fvmptg 5763 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( K `  y
)  e.  B  /\  if ( ( K `  y )  =  X ,  Y ,  ( G `  ( K `
 y ) ) )  e.  _V )  ->  ( F `  ( K `  y )
)  =  if ( ( K `  y
)  =  X ,  Y ,  ( G `  ( K `  y
) ) ) )
327318, 322, 326syl2anc 643 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  suc  y  e. 
dom  O )  -> 
( F `  ( K `  y )
)  =  if ( ( K `  y
)  =  X ,  Y ,  ( G `  ( K `  y
) ) ) )
328306fveq2d 5691 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  suc  y  e. 
dom  O )  -> 
( F `  ( K `  y )
)  =  ( F `
 ( O `  y ) ) )
329192adantr 452 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  suc  y  e. 
dom  O )  ->  -.  X  e.  ( `' G " ( _V 
\  1o ) ) )
330 nelneq 2502 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( K `  y
)  e.  ( `' G " ( _V 
\  1o ) )  /\  -.  X  e.  ( `' G "
( _V  \  1o ) ) )  ->  -.  ( K `  y
)  =  X )
331317, 329, 330syl2anc 643 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  suc  y  e. 
dom  O )  ->  -.  ( K `  y
)  =  X )
332 iffalse 3706 . . . . . . . . . . . . . . . . . . . 20  |-  ( -.  ( K `  y
)  =  X  ->  if ( ( K `  y )  =  X ,  Y ,  ( G `  ( K `
 y ) ) )  =  ( G `
 ( K `  y ) ) )
333331, 332syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  suc  y  e. 
dom  O )  ->  if ( ( K `  y )  =  X ,  Y ,  ( G `  ( K `
 y ) ) )  =  ( G `
 ( K `  y ) ) )
334327, 328, 3333eqtr3rd 2445 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  suc  y  e. 
dom  O )  -> 
( G `  ( K `  y )
)  =  ( F `
 ( O `  y ) ) )
335307, 334oveq12d 6058 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  suc  y  e. 
dom  O )  -> 
( ( A  ^o  ( K `  y ) )  .o  ( G `
 ( K `  y ) ) )  =  ( ( A  ^o  ( O `  y ) )  .o  ( F `  ( O `  y )
) ) )
336335oveq1d 6055 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  suc  y  e. 
dom  O )  -> 
( ( ( A  ^o  ( K `  y ) )  .o  ( G `  ( K `  y )
) )  +o  ( M `  y )
)  =  ( ( ( A  ^o  ( O `  y )
)  .o  ( F `
 ( O `  y ) ) )  +o  ( M `  y ) ) )
337294, 336eqtrd 2436 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  suc  y  e. 
dom  O )  -> 
( M `  suc  y )  =  ( ( ( A  ^o  ( O `  y ) )  .o  ( F `
 ( O `  y ) ) )  +o  ( M `  y ) ) )
338292, 337eqeq12d 2418 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  suc  y  e. 
dom  O )  -> 
( ( H `  suc  y )  =  ( M `  suc  y
)  <->  ( ( ( A  ^o  ( O `
 y ) )  .o  ( F `  ( O `  y ) ) )  +o  ( H `  y )
)  =  ( ( ( A  ^o  ( O `  y )
)  .o  ( F `
 ( O `  y ) ) )  +o  ( M `  y ) ) ) )
339286, 338syl5ibr 213 . . . . . . . . . . . . 13  |-  ( (
ph  /\  suc  y  e. 
dom  O )  -> 
( ( H `  y )  =  ( M `  y )  ->  ( H `  suc  y )  =  ( M `  suc  y
) ) )
340339ex 424 . . . . . . . . . . . 12  |-  ( ph  ->  ( suc  y  e. 
dom  O  ->  ( ( H `  y )  =  ( M `  y )  ->  ( H `  suc  y )  =  ( M `  suc  y ) ) ) )
341340a2d 24 . . . . . . . . . . 11  |-  ( ph  ->  ( ( suc  y  e.  dom  O  ->  ( H `  y )  =  ( M `  y ) )  -> 
( suc  y  e.  dom  O  ->  ( H `  suc  y )  =  ( M `  suc  y ) ) ) )
342285, 341syld 42 . . . . . . . . . 10  |-  ( ph  ->  ( ( y  e. 
dom  O  ->  ( H `
 y )  =  ( M `  y
) )  ->  ( suc  y  e.  dom  O  ->  ( H `  suc  y )  =  ( M `  suc  y
) ) ) )
343342a2i 13 . . . . . . . . 9  |-  ( (
ph  ->  ( y  e. 
dom  O  ->  ( H `
 y )  =  ( M `  y
) ) )  -> 
( ph  ->  ( suc  y  e.  dom  O  ->  ( H `  suc  y )  =  ( M `  suc  y
) ) ) )
344343a1i 11 . . . . . . . 8  |-  ( y  e.  om  ->  (
( ph  ->  ( y  e.  dom  O  -> 
( H `  y
)  =  ( M `
 y ) ) )  ->  ( ph  ->  ( suc  y  e. 
dom  O  ->  ( H `
 suc  y )  =  ( M `  suc  y ) ) ) ) )
345256, 262, 268, 274, 277, 344finds 4830 . . . . . . 7  |-  ( U. dom  O  e.  om  ->  (
ph  ->  ( U. dom  O  e.  dom  O  -> 
( H `  U. dom  O )  =  ( M `  U. dom  O ) ) ) )
34620, 345mpcom 34 . . . . . 6  |-  ( ph  ->  ( U. dom  O  e.  dom  O  ->  ( H `  U. dom  O
)  =  ( M `
 U. dom  O
) ) )
34774, 346mpd 15 . . . . 5  |-  ( ph  ->  ( H `  U. dom  O )  =  ( M `  U. dom  O ) )
3481, 2, 3, 237, 5, 250cantnfval 7579 . . . . 5  |-  ( ph  ->  ( ( A CNF  B
) `  G )  =  ( M `  dom  K ) )
349245, 347, 3483eqtr4d 2446 . . . 4  |-  ( ph  ->  ( H `  U. dom  O )  =  ( ( A CNF  B ) `
 G ) )
350158, 349oveq12d 6058 . . 3  |-  ( ph  ->  ( ( ( A  ^o  ( O `  U. dom  O ) )  .o  ( F `  ( O `  U. dom  O ) ) )  +o  ( H `  U. dom  O ) )  =  ( ( ( A  ^o  X )  .o  Y )  +o  (
( A CNF  B ) `
 G ) ) )
35122, 350eqtrd 2436 . 2  |-  ( ph  ->  ( H `  suc  U.
dom  O )  =  ( ( ( A  ^o  X )  .o  Y )  +o  (
( A CNF  B ) `
 G ) ) )
35212, 15, 3513eqtrd 2440 1  |-  ( ph  ->  ( ( A CNF  B
) `  F )  =  ( ( ( A  ^o  X )  .o  Y )  +o  ( ( A CNF  B
) `  G )
) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 177    \/ wo 358    /\ wa 359    = wceq 1649    e. wcel 1721    =/= wne 2567   _Vcvv 2916    \ cdif 3277    u. cun 3278    i^i cin 3279    C_ wss 3280   (/)c0 3588   ifcif 3699   {csn 3774   U.cuni 3975   class class class wbr 4172    e. cmpt 4226   Tr wtr 4262    _E cep 4452   Se wse 4499    We wwe 4500   Ord word 4540   Oncon0 4541   suc csuc 4543   omcom 4804   `'ccnv 4836   dom cdm 4837    |` cres 4839   "cima 4840   Fun wfun 5407    Fn wfn 5408   -->wf 5409   -onto->wfo 5411   -1-1-onto->wf1o 5412   ` cfv 5413    Isom wiso 5414  (class class class)co 6040    e. cmpt2 6042  seq𝜔cseqom 6663   1oc1o 6676    +o coa 6680    .o comu 6681    ^o coe 6682   Fincfn 7068  OrdIsocoi 7434   CNF ccnf 7572
This theorem is referenced by:  cantnfp1  7593
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-rep 4280  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-reu 2673  df-rmo 2674  df-rab 2675  df-v 2918  df-sbc 3122  df-csb 3212  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-int 4011  df-iun 4055  df-br 4173  df-opab 4227  df-mpt 4228  df-tr 4263  df-eprel 4454  df-id 4458  df-po 4463  df-so 4464  df-fr 4501  df-se 4502  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-isom 5422  df-ov 6043  df-oprab 6044  df-mpt2 6045  df-2nd 6309  df-riota 6508  df-recs 6592  df-rdg 6627  df-seqom 6664  df-1o 6683  df-oadd 6687  df-er 6864  df-map 6979  df-en 7069  df-dom 7070  df-sdom 7071  df-fin 7072  df-oi 7435  df-cnf 7573
  Copyright terms: Public domain W3C validator