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

Theorem cantnfp1lem3 7384
Description: Lemma for cantnfp1 7385. (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 7382 . . 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 7371 . 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 7383 . . 3  |-  ( ph  ->  dom  O  =  suc  U.
dom  O )
1514fveq2d 5531 . 2  |-  ( ph  ->  ( H `  dom  O )  =  ( H `
 suc  U. dom  O
) )
161, 2, 3, 4, 10cantnfcl 7370 . . . . . . 7  |-  ( ph  ->  (  _E  We  ( `' F " ( _V 
\  1o ) )  /\  dom  O  e. 
om ) )
1716simprd 449 . . . . . 6  |-  ( ph  ->  dom  O  e.  om )
1814, 17eqeltrrd 2360 . . . . 5  |-  ( ph  ->  suc  U. dom  O  e.  om )
19 peano2b 4674 . . . . 5  |-  ( U. dom  O  e.  om  <->  suc  U. dom  O  e.  om )
2018, 19sylibr 203 . . . 4  |-  ( ph  ->  U. dom  O  e. 
om )
211, 2, 3, 4, 10, 11cantnfsuc 7373 . . . 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 649 . . 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 5035 . . . . . . . . . . . . . . . . 17  |-  ( `' F " ( _V 
\  1o ) ) 
C_  dom  F
247adantr 451 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  t  e.  B )  ->  Y  e.  A )
251, 2, 3cantnfs 7369 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( G  e.  S  <->  ( G : B --> A  /\  ( `' G " ( _V 
\  1o ) )  e.  Fin ) ) )
265, 25mpbid 201 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( G : B --> A  /\  ( `' G " ( _V  \  1o ) )  e.  Fin ) )
2726simpld 445 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  G : B --> A )
28 ffvelrn 5665 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( G : B --> A  /\  t  e.  B )  ->  ( G `  t
)  e.  A )
2927, 28sylan 457 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  t  e.  B )  ->  ( G `  t )  e.  A )
30 ifcl 3603 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( Y  e.  A  /\  ( G `  t )  e.  A )  ->  if ( t  =  X ,  Y ,  ( G `  t ) )  e.  A )
3124, 29, 30syl2anc 642 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  t  e.  B )  ->  if ( t  =  X ,  Y ,  ( G `  t ) )  e.  A )
3231, 9fmptd 5686 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  F : B --> A )
33 fdm 5395 . . . . . . . . . . . . . . . . . 18  |-  ( F : B --> A  ->  dom  F  =  B )
3432, 33syl 15 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  dom  F  =  B )
3523, 34syl5sseq 3228 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( `' F "
( _V  \  1o ) )  C_  B
)
36 ssexg 4162 . . . . . . . . . . . . . . . 16  |-  ( ( ( `' F "
( _V  \  1o ) )  C_  B  /\  B  e.  On )  ->  ( `' F " ( _V  \  1o ) )  e.  _V )
3735, 3, 36syl2anc 642 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( `' F "
( _V  \  1o ) )  e.  _V )
3816simpld 445 . . . . . . . . . . . . . . 15  |-  ( ph  ->  _E  We  ( `' F " ( _V 
\  1o ) ) )
394oiiso 7254 . . . . . . . . . . . . . . 15  |-  ( ( ( `' F "
( _V  \  1o ) )  e.  _V  /\  _E  We  ( `' F " ( _V 
\  1o ) ) )  ->  O  Isom  _E  ,  _E  ( dom 
O ,  ( `' F " ( _V 
\  1o ) ) ) )
4037, 38, 39syl2anc 642 . . . . . . . . . . . . . 14  |-  ( ph  ->  O  Isom  _E  ,  _E  ( dom  O ,  ( `' F " ( _V 
\  1o ) ) ) )
41 isof1o 5824 . . . . . . . . . . . . . 14  |-  ( O 
Isom  _E  ,  _E  ( dom  O ,  ( `' F " ( _V 
\  1o ) ) )  ->  O : dom  O -1-1-onto-> ( `' F "
( _V  \  1o ) ) )
4240, 41syl 15 . . . . . . . . . . . . 13  |-  ( ph  ->  O : dom  O -1-1-onto-> ( `' F " ( _V 
\  1o ) ) )
43 f1ocnv 5487 . . . . . . . . . . . . 13  |-  ( O : dom  O -1-1-onto-> ( `' F " ( _V 
\  1o ) )  ->  `' O :
( `' F "
( _V  \  1o ) ) -1-1-onto-> dom  O )
44 f1of 5474 . . . . . . . . . . . . 13  |-  ( `' O : ( `' F " ( _V 
\  1o ) ) -1-1-onto-> dom 
O  ->  `' O : ( `' F " ( _V  \  1o ) ) --> dom  O
)
4542, 43, 443syl 18 . . . . . . . . . . . 12  |-  ( ph  ->  `' O : ( `' F " ( _V 
\  1o ) ) --> dom  O )
46 iftrue 3573 . . . . . . . . . . . . . . . . 17  |-  ( t  =  X  ->  if ( t  =  X ,  Y ,  ( G `  t ) )  =  Y )
4746, 9fvmptg 5602 . . . . . . . . . . . . . . . 16  |-  ( ( X  e.  B  /\  Y  e.  A )  ->  ( F `  X
)  =  Y )
486, 7, 47syl2anc 642 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( F `  X
)  =  Y )
49 onelon 4419 . . . . . . . . . . . . . . . . . 18  |-  ( ( A  e.  On  /\  Y  e.  A )  ->  Y  e.  On )
502, 7, 49syl2anc 642 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  Y  e.  On )
51 on0eln0 4449 . . . . . . . . . . . . . . . . 17  |-  ( Y  e.  On  ->  ( (/) 
e.  Y  <->  Y  =/=  (/) ) )
5250, 51syl 15 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( (/)  e.  Y  <->  Y  =/=  (/) ) )
5313, 52mpbid 201 . . . . . . . . . . . . . . 15  |-  ( ph  ->  Y  =/=  (/) )
5448, 53eqnetrd 2466 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( F `  X
)  =/=  (/) )
55 fvex 5541 . . . . . . . . . . . . . . 15  |-  ( F `
 X )  e. 
_V
56 dif1o 6501 . . . . . . . . . . . . . . 15  |-  ( ( F `  X )  e.  ( _V  \  1o )  <->  ( ( F `
 X )  e. 
_V  /\  ( F `  X )  =/=  (/) ) )
5755, 56mpbiran 884 . . . . . . . . . . . . . 14  |-  ( ( F `  X )  e.  ( _V  \  1o )  <->  ( F `  X )  =/=  (/) )
5854, 57sylibr 203 . . . . . . . . . . . . 13  |-  ( ph  ->  ( F `  X
)  e.  ( _V 
\  1o ) )
59 ffn 5391 . . . . . . . . . . . . . 14  |-  ( F : B --> A  ->  F  Fn  B )
60 elpreima 5647 . . . . . . . . . . . . . 14  |-  ( F  Fn  B  ->  ( X  e.  ( `' F " ( _V  \  1o ) )  <->  ( X  e.  B  /\  ( F `  X )  e.  ( _V  \  1o ) ) ) )
6132, 59, 603syl 18 . . . . . . . . . . . . 13  |-  ( ph  ->  ( X  e.  ( `' F " ( _V 
\  1o ) )  <-> 
( X  e.  B  /\  ( F `  X
)  e.  ( _V 
\  1o ) ) ) )
626, 58, 61mpbir2and 888 . . . . . . . . . . . 12  |-  ( ph  ->  X  e.  ( `' F " ( _V 
\  1o ) ) )
63 ffvelrn 5665 . . . . . . . . . . . 12  |-  ( ( `' O : ( `' F " ( _V 
\  1o ) ) --> dom  O  /\  X  e.  ( `' F "
( _V  \  1o ) ) )  -> 
( `' O `  X )  e.  dom  O )
6445, 62, 63syl2anc 642 . . . . . . . . . . 11  |-  ( ph  ->  ( `' O `  X )  e.  dom  O )
65 elssuni 3857 . . . . . . . . . . 11  |-  ( ( `' O `  X )  e.  dom  O  -> 
( `' O `  X )  C_  U. dom  O )
6664, 65syl 15 . . . . . . . . . 10  |-  ( ph  ->  ( `' O `  X )  C_  U. dom  O )
674oicl 7246 . . . . . . . . . . . 12  |-  Ord  dom  O
68 ordelon 4418 . . . . . . . . . . . 12  |-  ( ( Ord  dom  O  /\  ( `' O `  X )  e.  dom  O )  ->  ( `' O `  X )  e.  On )
6967, 64, 68sylancr 644 . . . . . . . . . . 11  |-  ( ph  ->  ( `' O `  X )  e.  On )
70 nnon 4664 . . . . . . . . . . . 12  |-  ( U. dom  O  e.  om  ->  U.
dom  O  e.  On )
7120, 70syl 15 . . . . . . . . . . 11  |-  ( ph  ->  U. dom  O  e.  On )
72 ontri1 4428 . . . . . . . . . . 11  |-  ( ( ( `' O `  X )  e.  On  /\ 
U. dom  O  e.  On )  ->  ( ( `' O `  X ) 
C_  U. dom  O  <->  -.  U. dom  O  e.  ( `' O `  X ) ) )
7369, 71, 72syl2anc 642 . . . . . . . . . 10  |-  ( ph  ->  ( ( `' O `  X )  C_  U. dom  O  <->  -.  U. dom  O  e.  ( `' O `  X ) ) )
7466, 73mpbid 201 . . . . . . . . 9  |-  ( ph  ->  -.  U. dom  O  e.  ( `' O `  X ) )
75 sucidg 4472 . . . . . . . . . . . . . 14  |-  ( U. dom  O  e.  om  ->  U.
dom  O  e.  suc  U.
dom  O )
7620, 75syl 15 . . . . . . . . . . . . 13  |-  ( ph  ->  U. dom  O  e. 
suc  U. dom  O )
7776, 14eleqtrrd 2362 . . . . . . . . . . . 12  |-  ( ph  ->  U. dom  O  e. 
dom  O )
78 isorel 5825 . . . . . . . . . . . 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 )
) ) )
7940, 77, 64, 78syl12anc 1180 . . . . . . . . . . 11  |-  ( ph  ->  ( U. dom  O  _E  ( `' O `  X )  <->  ( O `  U. dom  O )  _E  ( O `  ( `' O `  X ) ) ) )
80 fvex 5541 . . . . . . . . . . . 12  |-  ( `' O `  X )  e.  _V
8180epelc 4309 . . . . . . . . . . 11  |-  ( U. dom  O  _E  ( `' O `  X )  <->  U. dom  O  e.  ( `' O `  X ) )
82 fvex 5541 . . . . . . . . . . . 12  |-  ( O `
 ( `' O `  X ) )  e. 
_V
8382epelc 4309 . . . . . . . . . . 11  |-  ( ( O `  U. dom  O )  _E  ( O `
 ( `' O `  X ) )  <->  ( O `  U. dom  O )  e.  ( O `  ( `' O `  X ) ) )
8479, 81, 833bitr3g 278 . . . . . . . . . 10  |-  ( ph  ->  ( U. dom  O  e.  ( `' O `  X )  <->  ( O `  U. dom  O )  e.  ( O `  ( `' O `  X ) ) ) )
85 f1ocnvfv2 5795 . . . . . . . . . . . 12  |-  ( ( O : dom  O -1-1-onto-> ( `' F " ( _V 
\  1o ) )  /\  X  e.  ( `' F " ( _V 
\  1o ) ) )  ->  ( O `  ( `' O `  X ) )  =  X )
8642, 62, 85syl2anc 642 . . . . . . . . . . 11  |-  ( ph  ->  ( O `  ( `' O `  X ) )  =  X )
8786eleq2d 2352 . . . . . . . . . 10  |-  ( ph  ->  ( ( O `  U. dom  O )  e.  ( O `  ( `' O `  X ) )  <->  ( O `  U. dom  O )  e.  X ) )
8884, 87bitrd 244 . . . . . . . . 9  |-  ( ph  ->  ( U. dom  O  e.  ( `' O `  X )  <->  ( O `  U. dom  O )  e.  X ) )
8974, 88mtbid 291 . . . . . . . 8  |-  ( ph  ->  -.  ( O `  U. dom  O )  e.  X )
908sseld 3181 . . . . . . . . . 10  |-  ( ph  ->  ( ( O `  U. dom  O )  e.  ( `' G "
( _V  \  1o ) )  ->  ( O `  U. dom  O
)  e.  X ) )
91 onss 4584 . . . . . . . . . . . . . . . 16  |-  ( B  e.  On  ->  B  C_  On )
923, 91syl 15 . . . . . . . . . . . . . . 15  |-  ( ph  ->  B  C_  On )
9335, 92sstrd 3191 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( `' F "
( _V  \  1o ) )  C_  On )
944oif 7247 . . . . . . . . . . . . . . . 16  |-  O : dom  O --> ( `' F " ( _V  \  1o ) )
9594ffvelrni 5666 . . . . . . . . . . . . . . 15  |-  ( U. dom  O  e.  dom  O  ->  ( O `  U. dom  O )  e.  ( `' F " ( _V 
\  1o ) ) )
9677, 95syl 15 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( O `  U. dom  O )  e.  ( `' F " ( _V 
\  1o ) ) )
9793, 96sseldd 3183 . . . . . . . . . . . . 13  |-  ( ph  ->  ( O `  U. dom  O )  e.  On )
98 eloni 4404 . . . . . . . . . . . . 13  |-  ( ( O `  U. dom  O )  e.  On  ->  Ord  ( O `  U. dom  O ) )
9997, 98syl 15 . . . . . . . . . . . 12  |-  ( ph  ->  Ord  ( O `  U. dom  O ) )
100 ordn2lp 4414 . . . . . . . . . . . 12  |-  ( Ord  ( O `  U. dom  O )  ->  -.  ( ( O `  U. dom  O )  e.  X  /\  X  e.  ( O `  U. dom  O ) ) )
10199, 100syl 15 . . . . . . . . . . 11  |-  ( ph  ->  -.  ( ( O `
 U. dom  O
)  e.  X  /\  X  e.  ( O `  U. dom  O ) ) )
102 imnan 411 . . . . . . . . . . 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
) ) )
103101, 102sylibr 203 . . . . . . . . . 10  |-  ( ph  ->  ( ( O `  U. dom  O )  e.  X  ->  -.  X  e.  ( O `  U. dom  O ) ) )
10490, 103syld 40 . . . . . . . . 9  |-  ( ph  ->  ( ( O `  U. dom  O )  e.  ( `' G "
( _V  \  1o ) )  ->  -.  X  e.  ( O `  U. dom  O ) ) )
105 onelon 4419 . . . . . . . . . . . . 13  |-  ( ( B  e.  On  /\  X  e.  B )  ->  X  e.  On )
1063, 6, 105syl2anc 642 . . . . . . . . . . . 12  |-  ( ph  ->  X  e.  On )
107 eloni 4404 . . . . . . . . . . . 12  |-  ( X  e.  On  ->  Ord  X )
108106, 107syl 15 . . . . . . . . . . 11  |-  ( ph  ->  Ord  X )
109 ordirr 4412 . . . . . . . . . . 11  |-  ( Ord 
X  ->  -.  X  e.  X )
110108, 109syl 15 . . . . . . . . . 10  |-  ( ph  ->  -.  X  e.  X
)
111 elsni 3666 . . . . . . . . . . . 12  |-  ( ( O `  U. dom  O )  e.  { X }  ->  ( O `  U. dom  O )  =  X )
112111eleq2d 2352 . . . . . . . . . . 11  |-  ( ( O `  U. dom  O )  e.  { X }  ->  ( X  e.  ( O `  U. dom  O )  <->  X  e.  X ) )
113112notbid 285 . . . . . . . . . 10  |-  ( ( O `  U. dom  O )  e.  { X }  ->  ( -.  X  e.  ( O `  U. dom  O )  <->  -.  X  e.  X ) )
114110, 113syl5ibrcom 213 . . . . . . . . 9  |-  ( ph  ->  ( ( O `  U. dom  O )  e. 
{ X }  ->  -.  X  e.  ( O `
 U. dom  O
) ) )
115 df1o2 6493 . . . . . . . . . . . . . 14  |-  1o  =  { (/) }
116115difeq2i 3293 . . . . . . . . . . . . 13  |-  ( _V 
\  1o )  =  ( _V  \  { (/)
} )
117116imaeq2i 5012 . . . . . . . . . . . 12  |-  ( `' F " ( _V 
\  1o ) )  =  ( `' F " ( _V  \  { (/)
} ) )
118 eldifi 3300 . . . . . . . . . . . . . . . 16  |-  ( k  e.  ( B  \ 
( ( `' G " ( _V  \  1o ) )  u.  { X } ) )  -> 
k  e.  B )
119118adantl 452 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  k  e.  ( B  \  (
( `' G "
( _V  \  1o ) )  u.  { X } ) ) )  ->  k  e.  B
)
1207adantr 451 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  k  e.  ( B  \  (
( `' G "
( _V  \  1o ) )  u.  { X } ) ) )  ->  Y  e.  A
)
121 fvex 5541 . . . . . . . . . . . . . . . 16  |-  ( G `
 k )  e. 
_V
122 ifexg 3626 . . . . . . . . . . . . . . . 16  |-  ( ( Y  e.  A  /\  ( G `  k )  e.  _V )  ->  if ( k  =  X ,  Y ,  ( G `  k ) )  e.  _V )
123120, 121, 122sylancl 643 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  k  e.  ( B  \  (
( `' G "
( _V  \  1o ) )  u.  { X } ) ) )  ->  if ( k  =  X ,  Y ,  ( G `  k ) )  e. 
_V )
124 eqeq1 2291 . . . . . . . . . . . . . . . . 17  |-  ( t  =  k  ->  (
t  =  X  <->  k  =  X ) )
125 fveq2 5527 . . . . . . . . . . . . . . . . 17  |-  ( t  =  k  ->  ( G `  t )  =  ( G `  k ) )
126124, 125ifbieq2d 3587 . . . . . . . . . . . . . . . 16  |-  ( t  =  k  ->  if ( t  =  X ,  Y ,  ( G `  t ) )  =  if ( k  =  X ,  Y ,  ( G `  k ) ) )
127126, 9fvmptg 5602 . . . . . . . . . . . . . . 15  |-  ( ( k  e.  B  /\  if ( k  =  X ,  Y ,  ( G `  k ) )  e.  _V )  ->  ( F `  k
)  =  if ( k  =  X ,  Y ,  ( G `  k ) ) )
128119, 123, 127syl2anc 642 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  k  e.  ( B  \  (
( `' G "
( _V  \  1o ) )  u.  { X } ) ) )  ->  ( F `  k )  =  if ( k  =  X ,  Y ,  ( G `  k ) ) )
129 eldifn 3301 . . . . . . . . . . . . . . . . 17  |-  ( k  e.  ( B  \ 
( ( `' G " ( _V  \  1o ) )  u.  { X } ) )  ->  -.  k  e.  (
( `' G "
( _V  \  1o ) )  u.  { X } ) )
130129adantl 452 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  k  e.  ( B  \  (
( `' G "
( _V  \  1o ) )  u.  { X } ) ) )  ->  -.  k  e.  ( ( `' G " ( _V  \  1o ) )  u.  { X } ) )
131 elsn 3657 . . . . . . . . . . . . . . . . 17  |-  ( k  e.  { X }  <->  k  =  X )
132 elun2 3345 . . . . . . . . . . . . . . . . 17  |-  ( k  e.  { X }  ->  k  e.  ( ( `' G " ( _V 
\  1o ) )  u.  { X }
) )
133131, 132sylbir 204 . . . . . . . . . . . . . . . 16  |-  ( k  =  X  ->  k  e.  ( ( `' G " ( _V  \  1o ) )  u.  { X } ) )
134130, 133nsyl 113 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  k  e.  ( B  \  (
( `' G "
( _V  \  1o ) )  u.  { X } ) ) )  ->  -.  k  =  X )
135 iffalse 3574 . . . . . . . . . . . . . . 15  |-  ( -.  k  =  X  ->  if ( k  =  X ,  Y ,  ( G `  k ) )  =  ( G `
 k ) )
136134, 135syl 15 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  k  e.  ( B  \  (
( `' G "
( _V  \  1o ) )  u.  { X } ) ) )  ->  if ( k  =  X ,  Y ,  ( G `  k ) )  =  ( G `  k
) )
137 ssun1 3340 . . . . . . . . . . . . . . . . 17  |-  ( `' G " ( _V 
\  1o ) ) 
C_  ( ( `' G " ( _V 
\  1o ) )  u.  { X }
)
138 sscon 3312 . . . . . . . . . . . . . . . . 17  |-  ( ( `' G " ( _V 
\  1o ) ) 
C_  ( ( `' G " ( _V 
\  1o ) )  u.  { X }
)  ->  ( B  \  ( ( `' G " ( _V  \  1o ) )  u.  { X } ) )  C_  ( B  \  ( `' G " ( _V 
\  1o ) ) ) )
139137, 138ax-mp 8 . . . . . . . . . . . . . . . 16  |-  ( B 
\  ( ( `' G " ( _V 
\  1o ) )  u.  { X }
) )  C_  ( B  \  ( `' G " ( _V  \  1o ) ) )
140139sseli 3178 . . . . . . . . . . . . . . 15  |-  ( k  e.  ( B  \ 
( ( `' G " ( _V  \  1o ) )  u.  { X } ) )  -> 
k  e.  ( B 
\  ( `' G " ( _V  \  1o ) ) ) )
141116imaeq2i 5012 . . . . . . . . . . . . . . . . 17  |-  ( `' G " ( _V 
\  1o ) )  =  ( `' G " ( _V  \  { (/)
} ) )
142 eqimss2 3233 . . . . . . . . . . . . . . . . 17  |-  ( ( `' G " ( _V 
\  1o ) )  =  ( `' G " ( _V  \  { (/)
} ) )  -> 
( `' G "
( _V  \  { (/)
} ) )  C_  ( `' G " ( _V 
\  1o ) ) )
143141, 142mp1i 11 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( `' G "
( _V  \  { (/)
} ) )  C_  ( `' G " ( _V 
\  1o ) ) )
14427, 143suppssr 5661 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  k  e.  ( B  \  ( `' G " ( _V 
\  1o ) ) ) )  ->  ( G `  k )  =  (/) )
145140, 144sylan2 460 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  k  e.  ( B  \  (
( `' G "
( _V  \  1o ) )  u.  { X } ) ) )  ->  ( G `  k )  =  (/) )
146128, 136, 1453eqtrd 2321 . . . . . . . . . . . . 13  |-  ( (
ph  /\  k  e.  ( B  \  (
( `' G "
( _V  \  1o ) )  u.  { X } ) ) )  ->  ( F `  k )  =  (/) )
14732, 146suppss 5660 . . . . . . . . . . . 12  |-  ( ph  ->  ( `' F "
( _V  \  { (/)
} ) )  C_  ( ( `' G " ( _V  \  1o ) )  u.  { X } ) )
148117, 147syl5eqss 3224 . . . . . . . . . . 11  |-  ( ph  ->  ( `' F "
( _V  \  1o ) )  C_  (
( `' G "
( _V  \  1o ) )  u.  { X } ) )
149148, 96sseldd 3183 . . . . . . . . . 10  |-  ( ph  ->  ( O `  U. dom  O )  e.  ( ( `' G "
( _V  \  1o ) )  u.  { X } ) )
150 elun 3318 . . . . . . . . . 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 } ) )
151149, 150sylib 188 . . . . . . . . 9  |-  ( ph  ->  ( ( O `  U. dom  O )  e.  ( `' G "
( _V  \  1o ) )  \/  ( O `  U. dom  O
)  e.  { X } ) )
152104, 114, 151mpjaod 370 . . . . . . . 8  |-  ( ph  ->  -.  X  e.  ( O `  U. dom  O ) )
153 ioran 476 . . . . . . . 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
) ) )
15489, 152, 153sylanbrc 645 . . . . . . 7  |-  ( ph  ->  -.  ( ( O `
 U. dom  O
)  e.  X  \/  X  e.  ( O `  U. dom  O ) ) )
155 ordtri3 4430 . . . . . . . 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 ) ) ) )
15699, 108, 155syl2anc 642 . . . . . . 7  |-  ( ph  ->  ( ( O `  U. dom  O )  =  X  <->  -.  ( ( O `  U. dom  O
)  e.  X  \/  X  e.  ( O `  U. dom  O ) ) ) )
157154, 156mpbird 223 . . . . . 6  |-  ( ph  ->  ( O `  U. dom  O )  =  X )
158157oveq2d 5876 . . . . 5  |-  ( ph  ->  ( A  ^o  ( O `  U. dom  O
) )  =  ( A  ^o  X ) )
159157fveq2d 5531 . . . . . 6  |-  ( ph  ->  ( F `  ( O `  U. dom  O
) )  =  ( F `  X ) )
160159, 48eqtrd 2317 . . . . 5  |-  ( ph  ->  ( F `  ( O `  U. dom  O
) )  =  Y )
161158, 160oveq12d 5878 . . . 4  |-  ( ph  ->  ( ( A  ^o  ( O `  U. dom  O ) )  .o  ( F `  ( O `  U. dom  O ) ) )  =  ( ( A  ^o  X
)  .o  Y ) )
162 nnord 4666 . . . . . . . . 9  |-  ( U. dom  O  e.  om  ->  Ord  U. dom  O )
16320, 162syl 15 . . . . . . . 8  |-  ( ph  ->  Ord  U. dom  O
)
164 sssucid 4471 . . . . . . . . . 10  |-  U. dom  O 
C_  suc  U. dom  O
165164, 14syl5sseqr 3229 . . . . . . . . 9  |-  ( ph  ->  U. dom  O  C_  dom  O )
166 f1ofo 5481 . . . . . . . . . . . . 13  |-  ( O : dom  O -1-1-onto-> ( `' F " ( _V 
\  1o ) )  ->  O : dom  O
-onto-> ( `' F "
( _V  \  1o ) ) )
16742, 166syl 15 . . . . . . . . . . . 12  |-  ( ph  ->  O : dom  O -onto->
( `' F "
( _V  \  1o ) ) )
168 foima 5458 . . . . . . . . . . . 12  |-  ( O : dom  O -onto-> ( `' F " ( _V 
\  1o ) )  ->  ( O " dom  O )  =  ( `' F " ( _V 
\  1o ) ) )
169167, 168syl 15 . . . . . . . . . . 11  |-  ( ph  ->  ( O " dom  O )  =  ( `' F " ( _V 
\  1o ) ) )
170 ffn 5391 . . . . . . . . . . . . . 14  |-  ( O : dom  O --> ( `' F " ( _V 
\  1o ) )  ->  O  Fn  dom  O )
17194, 170ax-mp 8 . . . . . . . . . . . . 13  |-  O  Fn  dom  O
172 fnsnfv 5584 . . . . . . . . . . . . 13  |-  ( ( O  Fn  dom  O  /\  U. dom  O  e. 
dom  O )  ->  { ( O `  U. dom  O ) }  =  ( O " { U. dom  O }
) )
173171, 77, 172sylancr 644 . . . . . . . . . . . 12  |-  ( ph  ->  { ( O `  U. dom  O ) }  =  ( O " { U. dom  O }
) )
174157sneqd 3655 . . . . . . . . . . . 12  |-  ( ph  ->  { ( O `  U. dom  O ) }  =  { X }
)
175173, 174eqtr3d 2319 . . . . . . . . . . 11  |-  ( ph  ->  ( O " { U. dom  O } )  =  { X }
)
176169, 175difeq12d 3297 . . . . . . . . . 10  |-  ( ph  ->  ( ( O " dom  O )  \  ( O " { U. dom  O } ) )  =  ( ( `' F " ( _V  \  1o ) )  \  { X } ) )
177 ordirr 4412 . . . . . . . . . . . . . . . . 17  |-  ( Ord  U. dom  O  ->  -.  U.
dom  O  e.  U. dom  O )
178163, 177syl 15 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  -.  U. dom  O  e.  U. dom  O )
179 disjsn 3695 . . . . . . . . . . . . . . . 16  |-  ( ( U. dom  O  i^i  { U. dom  O }
)  =  (/)  <->  -.  U. dom  O  e.  U. dom  O
)
180178, 179sylibr 203 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( U. dom  O  i^i  { U. dom  O } )  =  (/) )
181 disj3 3501 . . . . . . . . . . . . . . 15  |-  ( ( U. dom  O  i^i  { U. dom  O }
)  =  (/)  <->  U. dom  O  =  ( U. dom  O 
\  { U. dom  O } ) )
182180, 181sylib 188 . . . . . . . . . . . . . 14  |-  ( ph  ->  U. dom  O  =  ( U. dom  O  \  { U. dom  O } ) )
183 difun2 3535 . . . . . . . . . . . . . 14  |-  ( ( U. dom  O  u.  { U. dom  O }
)  \  { U. dom  O } )  =  ( U. dom  O  \  { U. dom  O }
)
184182, 183syl6eqr 2335 . . . . . . . . . . . . 13  |-  ( ph  ->  U. dom  O  =  ( ( U. dom  O  u.  { U. dom  O } )  \  { U. dom  O } ) )
185 df-suc 4400 . . . . . . . . . . . . . . 15  |-  suc  U. dom  O  =  ( U. dom  O  u.  { U. dom  O } )
18614, 185syl6eq 2333 . . . . . . . . . . . . . 14  |-  ( ph  ->  dom  O  =  ( U. dom  O  u.  { U. dom  O }
) )
187186difeq1d 3295 . . . . . . . . . . . . 13  |-  ( ph  ->  ( dom  O  \  { U. dom  O }
)  =  ( ( U. dom  O  u.  { U. dom  O }
)  \  { U. dom  O } ) )
188184, 187eqtr4d 2320 . . . . . . . . . . . 12  |-  ( ph  ->  U. dom  O  =  ( dom  O  \  { U. dom  O }
) )
189188imaeq2d 5014 . . . . . . . . . . 11  |-  ( ph  ->  ( O " U. dom  O )  =  ( O " ( dom 
O  \  { U. dom  O } ) ) )
190 dff1o3 5480 . . . . . . . . . . . . 13  |-  ( O : dom  O -1-1-onto-> ( `' F " ( _V 
\  1o ) )  <-> 
( O : dom  O
-onto-> ( `' F "
( _V  \  1o ) )  /\  Fun  `' O ) )
191190simprbi 450 . . . . . . . . . . . 12  |-  ( O : dom  O -1-1-onto-> ( `' F " ( _V 
\  1o ) )  ->  Fun  `' O
)
192 imadif 5329 . . . . . . . . . . . 12  |-  ( Fun  `' O  ->  ( O
" ( dom  O  \  { U. dom  O } ) )  =  ( ( O " dom  O )  \  ( O " { U. dom  O } ) ) )
19342, 191, 1923syl 18 . . . . . . . . . . 11  |-  ( ph  ->  ( O " ( dom  O  \  { U. dom  O } ) )  =  ( ( O
" dom  O )  \  ( O " { U. dom  O }
) ) )
194189, 193eqtrd 2317 . . . . . . . . . 10  |-  ( ph  ->  ( O " U. dom  O )  =  ( ( O " dom  O )  \  ( O
" { U. dom  O } ) ) )
1958sseld 3181 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( X  e.  ( `' G " ( _V 
\  1o ) )  ->  X  e.  X
) )
196110, 195mtod 168 . . . . . . . . . . . . 13  |-  ( ph  ->  -.  X  e.  ( `' G " ( _V 
\  1o ) ) )
197 disjsn 3695 . . . . . . . . . . . . 13  |-  ( ( ( `' G "
( _V  \  1o ) )  i^i  { X } )  =  (/)  <->  -.  X  e.  ( `' G " ( _V  \  1o ) ) )
198196, 197sylibr 203 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( `' G " ( _V  \  1o ) )  i^i  { X } )  =  (/) )
199 fvex 5541 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( G `
 X )  e. 
_V
200 dif1o 6501 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( G `  X )  e.  ( _V  \  1o )  <->  ( ( G `
 X )  e. 
_V  /\  ( G `  X )  =/=  (/) ) )
201199, 200mpbiran 884 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( G `  X )  e.  ( _V  \  1o )  <->  ( G `  X )  =/=  (/) )
202 ffn 5391 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( G : B --> A  ->  G  Fn  B )
20327, 202syl 15 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  G  Fn  B )
204 elpreima 5647 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( G  Fn  B  ->  ( X  e.  ( `' G " ( _V  \  1o ) )  <->  ( X  e.  B  /\  ( G `  X )  e.  ( _V  \  1o ) ) ) )
205203, 204syl 15 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( X  e.  ( `' G " ( _V 
\  1o ) )  <-> 
( X  e.  B  /\  ( G `  X
)  e.  ( _V 
\  1o ) ) ) )
206205, 195sylbird 226 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( ( X  e.  B  /\  ( G `
 X )  e.  ( _V  \  1o ) )  ->  X  e.  X ) )
2076, 206mpand 656 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( ( G `  X )  e.  ( _V  \  1o )  ->  X  e.  X
) )
208201, 207syl5bir 209 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( ( G `  X )  =/=  (/)  ->  X  e.  X ) )
209208necon1bd 2516 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( -.  X  e.  X  ->  ( G `  X )  =  (/) ) )
210110, 209mpd 14 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( G `  X
)  =  (/) )
211210adantr 451 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  k  e.  ( B  \  ( `' F " ( _V 
\  { (/) } ) ) ) )  -> 
( G `  X
)  =  (/) )
212 fveq2 5527 . . . . . . . . . . . . . . . . . 18  |-  ( k  =  X  ->  ( G `  k )  =  ( G `  X ) )
213212eqeq1d 2293 . . . . . . . . . . . . . . . . 17  |-  ( k  =  X  ->  (
( G `  k
)  =  (/)  <->  ( G `  X )  =  (/) ) )
214211, 213syl5ibrcom 213 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  k  e.  ( B  \  ( `' F " ( _V 
\  { (/) } ) ) ) )  -> 
( k  =  X  ->  ( G `  k )  =  (/) ) )
215 eldifi 3300 . . . . . . . . . . . . . . . . . . . 20  |-  ( k  e.  ( B  \ 
( `' F "
( _V  \  { (/)
} ) ) )  ->  k  e.  B
)
216215adantl 452 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  k  e.  ( B  \  ( `' F " ( _V 
\  { (/) } ) ) ) )  -> 
k  e.  B )
2177adantr 451 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  k  e.  ( B  \  ( `' F " ( _V 
\  { (/) } ) ) ) )  ->  Y  e.  A )
218217, 121, 122sylancl 643 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  k  e.  ( B  \  ( `' F " ( _V 
\  { (/) } ) ) ) )  ->  if ( k  =  X ,  Y ,  ( G `  k ) )  e.  _V )
219216, 218, 127syl2anc 642 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  k  e.  ( B  \  ( `' F " ( _V 
\  { (/) } ) ) ) )  -> 
( F `  k
)  =  if ( k  =  X ,  Y ,  ( G `  k ) ) )
220 ssid 3199 . . . . . . . . . . . . . . . . . . . 20  |-  ( `' F " ( _V 
\  { (/) } ) )  C_  ( `' F " ( _V  \  { (/) } ) )
221220a1i 10 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( `' F "
( _V  \  { (/)
} ) )  C_  ( `' F " ( _V 
\  { (/) } ) ) )
22232, 221suppssr 5661 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  k  e.  ( B  \  ( `' F " ( _V 
\  { (/) } ) ) ) )  -> 
( F `  k
)  =  (/) )
223219, 222eqtr3d 2319 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  k  e.  ( B  \  ( `' F " ( _V 
\  { (/) } ) ) ) )  ->  if ( k  =  X ,  Y ,  ( G `  k ) )  =  (/) )
224135eqeq1d 2293 . . . . . . . . . . . . . . . . 17  |-  ( -.  k  =  X  -> 
( if ( k  =  X ,  Y ,  ( G `  k ) )  =  (/) 
<->  ( G `  k
)  =  (/) ) )
225223, 224syl5ibcom 211 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  k  e.  ( B  \  ( `' F " ( _V 
\  { (/) } ) ) ) )  -> 
( -.  k  =  X  ->  ( G `  k )  =  (/) ) )
226214, 225pm2.61d 150 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  k  e.  ( B  \  ( `' F " ( _V 
\  { (/) } ) ) ) )  -> 
( G `  k
)  =  (/) )
22727, 226suppss 5660 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( `' G "
( _V  \  { (/)
} ) )  C_  ( `' F " ( _V 
\  { (/) } ) ) )
228227, 141, 1173sstr4g 3221 . . . . . . . . . . . . 13  |-  ( ph  ->  ( `' G "
( _V  \  1o ) )  C_  ( `' F " ( _V 
\  1o ) ) )
229 reldisj 3500 . . . . . . . . . . . . 13  |-  ( ( `' G " ( _V 
\  1o ) ) 
C_  ( `' F " ( _V  \  1o ) )  ->  (
( ( `' G " ( _V  \  1o ) )  i^i  { X } )  =  (/)  <->  ( `' G " ( _V 
\  1o ) ) 
C_  ( ( `' F " ( _V 
\  1o ) ) 
\  { X }
) ) )
230228, 229syl 15 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( ( `' G " ( _V 
\  1o ) )  i^i  { X }
)  =  (/)  <->  ( `' G " ( _V  \  1o ) )  C_  (
( `' F "
( _V  \  1o ) )  \  { X } ) ) )
231198, 230mpbid 201 . . . . . . . . . . 11  |-  ( ph  ->  ( `' G "
( _V  \  1o ) )  C_  (
( `' F "
( _V  \  1o ) )  \  { X } ) )
232 uncom 3321 . . . . . . . . . . . . 13  |-  ( ( `' G " ( _V 
\  1o ) )  u.  { X }
)  =  ( { X }  u.  ( `' G " ( _V 
\  1o ) ) )
233148, 232syl6sseq 3226 . . . . . . . . . . . 12  |-  ( ph  ->  ( `' F "
( _V  \  1o ) )  C_  ( { X }  u.  ( `' G " ( _V 
\  1o ) ) ) )
234 ssundif 3539 . . . . . . . . . . . 12  |-  ( ( `' F " ( _V 
\  1o ) ) 
C_  ( { X }  u.  ( `' G " ( _V  \  1o ) ) )  <->  ( ( `' F " ( _V 
\  1o ) ) 
\  { X }
)  C_  ( `' G " ( _V  \  1o ) ) )
235233, 234sylib 188 . . . . . . . . . . 11  |-  ( ph  ->  ( ( `' F " ( _V  \  1o ) )  \  { X } )  C_  ( `' G " ( _V 
\  1o ) ) )
236231, 235eqssd 3198 . . . . . . . . . 10  |-  ( ph  ->  ( `' G "
( _V  \  1o ) )  =  ( ( `' F "
( _V  \  1o ) )  \  { X } ) )
237176, 194, 2363eqtr4rd 2328 . . . . . . . . 9  |-  ( ph  ->  ( `' G "
( _V  \  1o ) )  =  ( O " U. dom  O ) )
238 isores3 5834 . . . . . . . . 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 ) ) ) )
23940, 165, 237, 238syl3anc 1182 . . . . . . . 8  |-  ( ph  ->  ( O  |`  U. dom  O )  Isom  _E  ,  _E  ( U. dom  O , 
( `' G "
( _V  \  1o ) ) ) )
240 cantnfp1.k . . . . . . . . . . 11  |-  K  = OrdIso
(  _E  ,  ( `' G " ( _V 
\  1o ) ) )
2411, 2, 3, 240, 5cantnfcl 7370 . . . . . . . . . 10  |-  ( ph  ->  (  _E  We  ( `' G " ( _V 
\  1o ) )  /\  dom  K  e. 
om ) )
242241simpld 445 . . . . . . . . 9  |-  ( ph  ->  _E  We  ( `' G " ( _V 
\  1o ) ) )
243 epse 4378 . . . . . . . . 9  |-  _E Se  ( `' G " ( _V 
\  1o ) )
244240oieu 7256 . . . . . . . . 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 ) ) )
245242, 243, 244sylancl 643 . . . . . . . 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 ) ) )
246163, 239, 245mpbi2and 887 . . . . . . 7  |-  ( ph  ->  ( U. dom  O  =  dom  K  /\  ( O  |`  U. dom  O
)  =  K ) )
247246simpld 445 . . . . . 6  |-  ( ph  ->  U. dom  O  =  dom  K )
248247fveq2d 5531 . . . . 5  |-  ( ph  ->  ( M `  U. dom  O )  =  ( M `  dom  K
) )
249 eleq1 2345 . . . . . . . . . 10  |-  ( x  =  (/)  ->  ( x  e.  dom  O  <->  (/)  e.  dom  O ) )
250 fveq2 5527 . . . . . . . . . . 11  |-  ( x  =  (/)  ->  ( H `
 x )  =  ( H `  (/) ) )
251 fveq2 5527 . . . . . . . . . . . 12  |-  ( x  =  (/)  ->  ( M `
 x )  =  ( M `  (/) ) )
252 0ex 4152 . . . . . . . . . . . . 13  |-  (/)  e.  _V
253 cantnfp1.m . . . . . . . . . . . . . 14  |-  M  = seq𝜔 ( ( k  e.  _V ,  z  e.  _V  |->  ( ( ( A  ^o  ( K `  k ) )  .o  ( G `  ( K `  k )
) )  +o  z
) ) ,  (/) )
254253seqom0g 6470 . . . . . . . . . . . . 13  |-  ( (/)  e.  _V  ->  ( M `  (/) )  =  (/) )
255252, 254ax-mp 8 . . . . . . . . . . . 12  |-  ( M `
 (/) )  =  (/)
256251, 255syl6eq 2333 . . . . . . . . . . 11  |-  ( x  =  (/)  ->  ( M `
 x )  =  (/) )
257250, 256eqeq12d 2299 . . . . . . . . . 10  |-  ( x  =  (/)  ->  ( ( H `  x )  =  ( M `  x )  <->  ( H `  (/) )  =  (/) ) )
258249, 257imbi12d 311 . . . . . . . . 9  |-  ( x  =  (/)  ->  ( ( x  e.  dom  O  ->  ( H `  x
)  =  ( M `
 x ) )  <-> 
( (/)  e.  dom  O  ->  ( H `  (/) )  =  (/) ) ) )
259258imbi2d 307 . . . . . . . 8  |-  ( x  =  (/)  ->  ( (
ph  ->  ( x  e. 
dom  O  ->  ( H `
 x )  =  ( M `  x
) ) )  <->  ( ph  ->  ( (/)  e.  dom  O  ->  ( H `  (/) )  =  (/) ) ) ) )
260 eleq1 2345 . . . . . . . . . 10  |-  ( x  =  y  ->  (
x  e.  dom  O  <->  y  e.  dom  O ) )
261 fveq2 5527 . . . . . . . . . . 11  |-  ( x  =  y  ->  ( H `  x )  =  ( H `  y ) )
262 fveq2 5527 . . . . . . . . . . 11  |-  ( x  =  y  ->  ( M `  x )  =  ( M `  y ) )
263261, 262eqeq12d 2299 . . . . . . . . . 10  |-  ( x  =  y  ->  (
( H `  x
)  =  ( M `
 x )  <->  ( H `  y )  =  ( M `  y ) ) )
264260, 263imbi12d 311 . . . . . . . . 9  |-  ( x  =  y  ->  (
( x  e.  dom  O  ->  ( H `  x )  =  ( M `  x ) )  <->  ( y  e. 
dom  O  ->  ( H `
 y )  =  ( M `  y
) ) ) )
265264imbi2d 307 . . . . . . . 8  |-  ( x  =  y  ->  (
( ph  ->  ( x  e.  dom  O  -> 
( H `  x
)  =  ( M `
 x ) ) )  <->  ( ph  ->  ( y  e.  dom  O  ->  ( H `  y
)  =  ( M `
 y ) ) ) ) )
266 eleq1 2345 . . . . . . . . . 10  |-  ( x  =  suc  y  -> 
( x  e.  dom  O  <->  suc  y  e.  dom  O ) )
267 fveq2 5527 . . . . . . . . . . 11  |-  ( x  =  suc  y  -> 
( H `  x
)  =  ( H `
 suc  y )
)
268 fveq2 5527 . . . . . . . . . . 11  |-  ( x  =  suc  y  -> 
( M `  x
)  =  ( M `
 suc  y )
)
269267, 268eqeq12d 2299 . . . . . . . . . 10  |-  ( x  =  suc  y  -> 
( ( H `  x )  =  ( M `  x )  <-> 
( H `  suc  y )  =  ( M `  suc  y
) ) )
270266, 269imbi12d 311 . . . . . . . . 9  |-  ( x  =  suc  y  -> 
( ( x  e. 
dom  O  ->  ( H `
 x )  =  ( M `  x
) )  <->  ( suc  y  e.  dom  O  -> 
( H `  suc  y )  =  ( M `  suc  y
) ) ) )
271270imbi2d 307 . . . . . . . 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
) ) ) ) )
272 eleq1 2345 . . . . . . . . . 10  |-  ( x  =  U. dom  O  ->  ( x  e.  dom  O  <->  U. dom  O  e.  dom  O ) )
273 fveq2 5527 . . . . . . . . . . 11  |-  ( x  =  U. dom  O  ->  ( H `  x
)  =  ( H `
 U. dom  O
) )
274 fveq2 5527 . . . . . . . . . . 11  |-  ( x  =  U. dom  O  ->  ( M `  x
)  =  ( M `
 U. dom  O
) )
275273, 274eqeq12d 2299 . . . . . . . . . 10  |-  ( x  =  U. dom  O  ->  ( ( H `  x )  =  ( M `  x )  <-> 
( H `  U. dom  O )  =  ( M `  U. dom  O ) ) )
276272, 275imbi12d 311 . . . . . . . . 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 ) ) ) )
277276imbi2d 307 . . . . . . . 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
) ) ) ) )
27811seqom0g 6470 . . . . . . . . . 10  |-  ( (/)  e.  _V  ->  ( H `  (/) )  =  (/) )
279252, 278mp1i 11 . . . . . . . . 9  |-  ( (/)  e.  dom  O  ->  ( H `  (/) )  =  (/) )
280279a1i 10 . . . . . . . 8  |-  ( ph  ->  ( (/)  e.  dom  O  ->  ( H `  (/) )  =  (/) ) )
281 nnord 4666 . . . . . . . . . . . . . . . 16  |-  ( dom 
O  e.  om  ->  Ord 
dom  O )
28217, 281syl 15 . . . . . . . . . . . . . . 15  |-  ( ph  ->  Ord  dom  O )
283 ordtr 4408 . . . . . . . . . . . . . . 15  |-  ( Ord 
dom  O  ->  Tr  dom  O )
284282, 283syl 15 . . . . . . . . . . . . . 14  |-  ( ph  ->  Tr  dom  O )
285 trsuc 4478 . . . . . . . . . . . . . 14  |-  ( ( Tr  dom  O  /\  suc  y  e.  dom  O )  ->  y  e.  dom  O )
286284, 285sylan 457 . . . . . . . . . . . . 13  |-  ( (
ph  /\  suc  y  e. 
dom  O )  -> 
y  e.  dom  O
)
287286ex 423 . . . . . . . . . . . 12  |-  ( ph  ->  ( suc  y  e. 
dom  O  ->  y  e. 
dom  O ) )
288287imim1d 69 . . . . . . . . . . 11  |-  ( ph  ->  ( ( y  e. 
dom  O  ->  ( H `
 y )  =  ( M `  y
) )  ->  ( suc  y  e.  dom  O  ->  ( H `  y )  =  ( M `  y ) ) ) )
289 oveq2 5868 . . . . . . . . . . . . . 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 )
) )
290 elnn 4668 . . . . . . . . . . . . . . . . . . 19  |-  ( ( y  e.  dom  O  /\  dom  O  e.  om )  ->  y  e.  om )
291290ancoms 439 . . . . . . . . . . . . . . . . . 18  |-  ( ( dom  O  e.  om  /\  y  e.  dom  O
)  ->  y  e.  om )
29217, 291sylan 457 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  y  e.  dom  O )  ->  y  e.  om )
293286, 292syldan 456 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  suc  y  e. 
dom  O )  -> 
y  e.  om )
2941, 2, 3, 4, 10, 11cantnfsuc 7373 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  y  e.  om )  ->  ( H `  suc  y )  =  ( ( ( A  ^o  ( O `  y ) )  .o  ( F `  ( O `  y )
) )  +o  ( H `  y )
) )
295293, 294syldan 456 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  suc  y  e. 
dom  O )  -> 
( H `  suc  y )  =  ( ( ( A  ^o  ( O `  y ) )  .o  ( F `
 ( O `  y ) ) )  +o  ( H `  y ) ) )
2961, 2, 3, 240, 5, 253cantnfsuc 7373 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  y  e.  om )  ->  ( M `  suc  y )  =  ( ( ( A  ^o  ( K `  y ) )  .o  ( G `  ( K `  y )
) )  +o  ( M `  y )
) )
297293, 296syldan 456 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  suc  y  e. 
dom  O )  -> 
( M `  suc  y )  =  ( ( ( A  ^o  ( K `  y ) )  .o  ( G `
 ( K `  y ) ) )  +o  ( M `  y ) ) )
298246simprd 449 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( O  |`  U. dom  O )  =  K )
299298fveq1d 5529 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( ( O  |`  U.
dom  O ) `  y )  =  ( K `  y ) )
300299adantr 451 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  suc  y  e. 
dom  O )  -> 
( ( O  |`  U.
dom  O ) `  y )  =  ( K `  y ) )
30114eleq2d 2352 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( suc  y  e. 
dom  O  <->  suc  y  e.  suc  U.
dom  O ) )
302301biimpa 470 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  suc  y  e. 
dom  O )  ->  suc  y  e.  suc  U.
dom  O )
303163adantr 451 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  suc  y  e. 
dom  O )  ->  Ord  U. dom  O )
304 ordsucelsuc 4615 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( Ord  U. dom  O  ->  (
y  e.  U. dom  O  <->  suc  y  e.  suc  U.
dom  O ) )
305303, 304syl 15 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  suc  y  e. 
dom  O )  -> 
( y  e.  U. dom  O  <->  suc  y  e.  suc  U.
dom  O ) )
306302, 305mpbird 223 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  suc  y  e. 
dom  O )  -> 
y  e.  U. dom  O )
307 fvres 5544 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  e.  U. dom  O  ->  ( ( O  |`  U.
dom  O ) `  y )  =  ( O `  y ) )
308306, 307syl 15 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  suc  y  e. 
dom  O )  -> 
( ( O  |`  U.
dom  O ) `  y )  =  ( O `  y ) )
309300, 308eqtr3d 2319 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  suc  y  e. 
dom  O )  -> 
( K `  y
)  =  ( O `
 y ) )
310309oveq2d 5876 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  suc  y  e. 
dom  O )  -> 
( A  ^o  ( K `  y )
)  =  ( A  ^o  ( O `  y ) ) )
311 cnvimass 5035 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( `' G " ( _V 
\  1o ) ) 
C_  dom  G
312 fdm 5395 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( G : B --> A  ->  dom  G  =  B )
31327, 312syl 15 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  dom  G  =  B )
314311, 313syl5sseq 3228 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( `' G "
( _V  \  1o ) )  C_  B
)
315314adantr 451 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  suc  y  e. 
dom  O )  -> 
( `' G "
( _V  \  1o ) )  C_  B
)
316247adantr 451 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  suc  y  e. 
dom  O )  ->  U. dom  O  =  dom  K )
317306, 316eleqtrd 2361 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  suc  y  e. 
dom  O )  -> 
y  e.  dom  K
)
318240oif 7247 . . . . . . . . . . . . . . . . . . . . . . 23  |-  K : dom  K --> ( `' G " ( _V  \  1o ) )
319318ffvelrni 5666 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  e.  dom  K  -> 
( K `  y
)  e.  ( `' G " ( _V 
\  1o ) ) )
320317, 319syl 15 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  suc  y  e. 
dom  O )  -> 
( K `  y
)  e.  ( `' G " ( _V 
\  1o ) ) )
321315, 320sseldd 3183 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  suc  y  e. 
dom  O )  -> 
( K `  y
)  e.  B )
3227adantr 451 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  suc  y  e. 
dom  O )  ->  Y  e.  A )
323 fvex 5541 . . . . . . . . . . . . . . . . . . . . 21  |-  ( G `
 ( K `  y ) )  e. 
_V
324 ifexg 3626 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( Y  e.  A  /\  ( G `  ( K `
 y ) )  e.  _V )  ->  if ( ( K `  y )  =  X ,  Y ,  ( G `  ( K `
 y ) ) )  e.  _V )
325322, 323, 324sylancl 643 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  suc  y  e. 
dom  O )  ->  if ( ( K `  y )  =  X ,  Y ,  ( G `  ( K `
 y ) ) )  e.  _V )
326 eqeq1 2291 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( t  =  ( K `  y )  ->  (
t  =  X  <->  ( K `  y )  =  X ) )
327 fveq2 5527 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( t  =  ( K `  y )  ->  ( G `  t )  =  ( G `  ( K `  y ) ) )
328326, 327ifbieq2d 3587 . . . . . . . . . . . . . . . . . . . . 21  |-  ( t  =  ( K `  y )  ->  if ( t  =  X ,  Y ,  ( G `  t ) )  =  if ( ( K `  y
)  =  X ,  Y ,  ( G `  ( K `  y
) ) ) )
329328, 9fvmptg 5602 . . . . . . . . . . . . . . . . . . . 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
) ) ) )
330321, 325, 329syl2anc 642 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  suc  y  e. 
dom  O )  -> 
( F `  ( K `  y )
)  =  if ( ( K `  y
)  =  X ,  Y ,  ( G `  ( K `  y
) ) ) )
331309fveq2d 5531 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  suc  y  e. 
dom  O )  -> 
( F `  ( K `  y )
)  =  ( F `
 ( O `  y ) ) )
332196adantr 451 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  suc  y  e. 
dom  O )  ->  -.  X  e.  ( `' G " ( _V 
\  1o ) ) )
333 nelneq 2383 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( K `  y
)  e.  ( `' G " ( _V 
\  1o ) )  /\  -.  X  e.  ( `' G "
( _V  \  1o ) ) )  ->  -.  ( K `  y
)  =  X )
334320, 332, 333syl2anc 642 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  suc  y  e. 
dom  O )  ->  -.  ( K `  y
)  =  X )
335 iffalse 3574 . . . . . . . . . . . . . . . . . . . 20  |-  ( -.  ( K `  y
)  =  X  ->  if ( ( K `  y )  =  X ,  Y ,  ( G `  ( K `
 y ) ) )  =  ( G `
 ( K `  y ) ) )
336334, 335syl 15 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  suc  y  e. 
dom  O )  ->  if ( ( K `  y )  =  X ,  Y ,  ( G `  ( K `
 y ) ) )  =  ( G `
 ( K `  y ) ) )
337330, 331, 3363eqtr3rd 2326 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  suc  y  e. 
dom  O )  -> 
( G `  ( K `  y )
)  =  ( F `
 ( O `  y ) ) )
338310, 337oveq12d 5878 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  suc  y  e. 
dom  O )  -> 
( ( A  ^o  ( K `  y ) )  .o  ( G `
 ( K `  y ) ) )  =  ( ( A  ^o  ( O `  y ) )  .o  ( F `  ( O `  y )
) ) )
339338oveq1d 5875 . . . . . . . . . . . . . . . 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 ) ) )
340297, 339eqtrd 2317 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  suc  y  e. 
dom  O )  -> 
( M `  suc  y )  =  ( ( ( A  ^o  ( O `  y ) )  .o  ( F `
 ( O `  y ) ) )  +o  ( M `  y ) ) )
341295, 340eqeq12d 2299 . . . . . . . . . . . . . 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 ) ) ) )
342289, 341syl5ibr 212 . . . . . . . . . . . . 13  |-  ( (
ph  /\  suc  y  e. 
dom  O )  -> 
( ( H `  y )  =  ( M `  y )  ->  ( H `  suc  y )  =  ( M `  suc  y
) ) )
343342ex 423 . . . . . . . . . . . 12  |-  ( ph  ->  ( suc  y  e. 
dom  O  ->  ( ( H `  y )  =  ( M `  y )  ->  ( H `  suc  y )  =  ( M `  suc  y ) ) ) )
344343a2d 23 . . . . . . . . . . 11  |-  ( ph  ->  ( ( suc  y  e.  dom  O  ->  ( H `  y )  =  ( M `  y ) )  -> 
( suc  y  e.  dom  O  ->  ( H `  suc  y )  =  ( M `  suc  y ) ) ) )
345288, 344syld 40 . . . . . . . . . 10  |-  ( ph  ->  ( ( y  e. 
dom  O  ->  ( H `
 y )  =  ( M `  y
) )  ->  ( suc  y  e.  dom  O  ->  ( H `  suc  y )  =  ( M `  suc  y
) ) ) )
346345a2i 12 . . . . . . . . 9  |-  ( (
ph  ->  ( y  e. 
dom  O  ->  ( H `
 y )  =  ( M `  y
) ) )  -> 
( ph  ->  ( suc  y  e.  dom  O  ->  ( H `  suc  y )  =  ( M `  suc  y
) ) ) )
347346a1i 10 . . . . . . . 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 ) ) ) ) )
348259, 265, 271, 277, 280, 347finds 4684 . . . . . . 7  |-  ( U. dom  O  e.  om  ->  (
ph  ->  ( U. dom  O  e.  dom  O  -> 
( H `  U. dom  O )  =  ( M `  U. dom  O ) ) ) )
34920, 348mpcom 32 . . . . . 6  |-  ( ph  ->  ( U. dom  O  e.  dom  O  ->  ( H `  U. dom  O
)  =  ( M `
 U. dom  O
) ) )
35077, 349mpd 14 . . . . 5  |-  ( ph  ->  ( H `  U. dom  O )  =  ( M `  U. dom  O ) )
3511, 2, 3, 240, 5, 253cantnfval 7371 . . . . 5  |-  ( ph  ->  ( ( A CNF  B
) `  G )  =  ( M `  dom  K ) )
352248, 350, 3513eqtr4d 2327 . . . 4  |-  ( ph  ->  ( H `  U. dom  O )  =  ( ( A CNF  B ) `
 G ) )
353161, 352oveq12d 5878 . . 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 ) ) )
35422, 353eqtrd 2317 . 2  |-  ( ph  ->  ( H `  suc  U.
dom  O )  =  ( ( ( A  ^o  X )  .o  Y )  +o  (
( A CNF  B ) `
 G ) ) )
35512, 15, 3543eqtrd 2321 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 176    \/ wo 357    /\ wa 358    = wceq 1625    e. wcel 1686    =/= wne 2448   _Vcvv 2790    \ cdif 3151    u. cun 3152    i^i cin 3153    C_ wss 3154   (/)c0 3457   ifcif 3567   {csn 3642   U.cuni 3829   class class class wbr 4025    e. cmpt 4079   Tr wtr 4115    _E cep 4305   Se wse 4352    We wwe 4353   Ord word 4393   Oncon0 4394   suc csuc 4396   omcom 4658   `'ccnv 4690   dom cdm 4691    |` cres 4693   "cima 4694   Fun wfun 5251    Fn wfn 5252   -->wf 5253   -onto->wfo 5255   -1-1-onto->wf1o 5256   ` cfv 5257    Isom wiso 5258  (class class class)co 5860    e. cmpt2 5862  seq𝜔cseqom 6461   1oc1o 6474    +o coa 6478    .o comu 6479    ^o coe 6480   Fincfn 6865  OrdIsocoi 7226   CNF ccnf 7364
This theorem is referenced by:  cantnfp1  7385
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-13 1688  ax-14 1690  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266  ax-rep 4133  ax-sep 4143  ax-nul 4151  ax-pow 4190  ax-pr 4216  ax-un 4514
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-eu 2149  df-mo 2150  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-ne 2450  df-ral 2550  df-rex 2551  df-reu 2552  df-rmo 2553  df-rab 2554  df-v 2792  df-sbc 2994  df-csb 3084  df-dif 3157  df-un 3159  df-in 3161  df-ss 3168  df-pss 3170  df-nul 3458  df-if 3568  df-pw 3629  df-sn 3648  df-pr 3649  df-tp 3650  df-op 3651  df-uni 3830  df-int 3865  df-iun 3909  df-br 4026  df-opab 4080  df-mpt 4081  df-tr 4116  df-eprel 4307  df-id 4311  df-po 4316  df-so 4317  df-fr 4354  df-se 4355  df-we 4356  df-ord 4397  df-on 4398  df-lim 4399  df-suc 4400  df-om 4659  df-xp 4697  df-rel 4698  df-cnv 4699  df-co 4700  df-dm 4701  df-rn 4702  df-res 4703  df-ima 4704  df-iota 5221  df-fun 5259  df-fn 5260  df-f 5261  df-f1 5262  df-fo 5263  df-f1o 5264  df-fv 5265  df-isom 5266  df-ov 5863  df-oprab 5864  df-mpt2 5865  df-2nd 6125  df-riota 6306  df-recs 6390  df-rdg 6425  df-seqom 6462  df-1o 6481  df-oadd 6485  df-er 6662  df-map 6776  df-en 6866  df-dom 6867  df-sdom 6868  df-fin 6869  df-oi 7227  df-cnf 7365
  Copyright terms: Public domain W3C validator