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

Theorem cantnfp1lem3 7571
Description: Lemma for cantnfp1 7572. (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 7569 . . 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 7558 . 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 7570 . . 3  |-  ( ph  ->  dom  O  =  suc  U.
dom  O )
1514fveq2d 5674 . 2  |-  ( ph  ->  ( H `  dom  O )  =  ( H `
 suc  U. dom  O
) )
161, 2, 3, 4, 10cantnfcl 7557 . . . . . . 7  |-  ( ph  ->  (  _E  We  ( `' F " ( _V 
\  1o ) )  /\  dom  O  e. 
om ) )
1716simprd 450 . . . . . 6  |-  ( ph  ->  dom  O  e.  om )
1814, 17eqeltrrd 2464 . . . . 5  |-  ( ph  ->  suc  U. dom  O  e.  om )
19 peano2b 4803 . . . . 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 7560 . . . 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 5166 . . . . . . . . . . . . . . . . 17  |-  ( `' F " ( _V 
\  1o ) ) 
C_  dom  F
247adantr 452 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  t  e.  B )  ->  Y  e.  A )
251, 2, 3cantnfs 7556 . . . . . . . . . . . . . . . . . . . . . . 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 5811 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  t  e.  B )  ->  ( G `  t )  e.  A )
29 ifcl 3720 . . . . . . . . . . . . . . . . . . . 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 5834 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  F : B --> A )
32 fdm 5537 . . . . . . . . . . . . . . . . . 18  |-  ( F : B --> A  ->  dom  F  =  B )
3331, 32syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  dom  F  =  B )
3423, 33syl5sseq 3341 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( `' F "
( _V  \  1o ) )  C_  B
)
353, 34ssexd 4293 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( `' F "
( _V  \  1o ) )  e.  _V )
3616simpld 446 . . . . . . . . . . . . . . 15  |-  ( ph  ->  _E  We  ( `' F " ( _V 
\  1o ) ) )
374oiiso 7441 . . . . . . . . . . . . . . 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 5986 . . . . . . . . . . . . . 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 5629 . . . . . . . . . . . . 13  |-  ( O : dom  O -1-1-onto-> ( `' F " ( _V 
\  1o ) )  ->  `' O :
( `' F "
( _V  \  1o ) ) -1-1-onto-> dom  O )
42 f1of 5616 . . . . . . . . . . . . 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 3690 . . . . . . . . . . . . . . . . 17  |-  ( t  =  X  ->  if ( t  =  X ,  Y ,  ( G `  t ) )  =  Y )
4544, 9fvmptg 5745 . . . . . . . . . . . . . . . 16  |-  ( ( X  e.  B  /\  Y  e.  A )  ->  ( F `  X
)  =  Y )
466, 7, 45syl2anc 643 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( F `  X
)  =  Y )
47 onelon 4549 . . . . . . . . . . . . . . . . . 18  |-  ( ( A  e.  On  /\  Y  e.  A )  ->  Y  e.  On )
482, 7, 47syl2anc 643 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  Y  e.  On )
49 on0eln0 4579 . . . . . . . . . . . . . . . . 17  |-  ( Y  e.  On  ->  ( (/) 
e.  Y  <->  Y  =/=  (/) ) )
5048, 49syl 16 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( (/)  e.  Y  <->  Y  =/=  (/) ) )
5113, 50mpbid 202 . . . . . . . . . . . . . . 15  |-  ( ph  ->  Y  =/=  (/) )
5246, 51eqnetrd 2570 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( F `  X
)  =/=  (/) )
53 fvex 5684 . . . . . . . . . . . . . . 15  |-  ( F `
 X )  e. 
_V
54 dif1o 6682 . . . . . . . . . . . . . . 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 5533 . . . . . . . . . . . . . 14  |-  ( F : B --> A  ->  F  Fn  B )
58 elpreima 5791 . . . . . . . . . . . . . 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 5812 . . . . . . . . . . 11  |-  ( ph  ->  ( `' O `  X )  e.  dom  O )
62 elssuni 3987 . . . . . . . . . . 11  |-  ( ( `' O `  X )  e.  dom  O  -> 
( `' O `  X )  C_  U. dom  O )
6361, 62syl 16 . . . . . . . . . 10  |-  ( ph  ->  ( `' O `  X )  C_  U. dom  O )
644oicl 7433 . . . . . . . . . . . 12  |-  Ord  dom  O
65 ordelon 4548 . . . . . . . . . . . 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 4793 . . . . . . . . . . . 12  |-  ( U. dom  O  e.  om  ->  U.
dom  O  e.  On )
6820, 67syl 16 . . . . . . . . . . 11  |-  ( ph  ->  U. dom  O  e.  On )
69 ontri1 4558 . . . . . . . . . . 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 4602 . . . . . . . . . . . . . 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 2466 . . . . . . . . . . . 12  |-  ( ph  ->  U. dom  O  e. 
dom  O )
75 isorel 5987 . . . . . . . . . . . 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 5684 . . . . . . . . . . . 12  |-  ( `' O `  X )  e.  _V
7877epelc 4439 . . . . . . . . . . 11  |-  ( U. dom  O  _E  ( `' O `  X )  <->  U. dom  O  e.  ( `' O `  X ) )
79 fvex 5684 . . . . . . . . . . . 12  |-  ( O `
 ( `' O `  X ) )  e. 
_V
8079epelc 4439 . . . . . . . . . . 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 5956 . . . . . . . . . . . 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 2456 . . . . . . . . . 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 3292 . . . . . . . . . 10  |-  ( ph  ->  ( ( O `  U. dom  O )  e.  ( `' G "
( _V  \  1o ) )  ->  ( O `  U. dom  O
)  e.  X ) )
88 onss 4713 . . . . . . . . . . . . . . . 16  |-  ( B  e.  On  ->  B  C_  On )
893, 88syl 16 . . . . . . . . . . . . . . 15  |-  ( ph  ->  B  C_  On )
9034, 89sstrd 3303 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( `' F "
( _V  \  1o ) )  C_  On )
914oif 7434 . . . . . . . . . . . . . . . 16  |-  O : dom  O --> ( `' F " ( _V  \  1o ) )
9291ffvelrni 5810 . . . . . . . . . . . . . . 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 3294 . . . . . . . . . . . . 13  |-  ( ph  ->  ( O `  U. dom  O )  e.  On )
95 eloni 4534 . . . . . . . . . . . . 13  |-  ( ( O `  U. dom  O )  e.  On  ->  Ord  ( O `  U. dom  O ) )
9694, 95syl 16 . . . . . . . . . . . 12  |-  ( ph  ->  Ord  ( O `  U. dom  O ) )
97 ordn2lp 4544 . . . . . . . . . . . 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 4549 . . . . . . . . . . . . 13  |-  ( ( B  e.  On  /\  X  e.  B )  ->  X  e.  On )
1033, 6, 102syl2anc 643 . . . . . . . . . . . 12  |-  ( ph  ->  X  e.  On )
104 eloni 4534 . . . . . . . . . . . 12  |-  ( X  e.  On  ->  Ord  X )
105103, 104syl 16 . . . . . . . . . . 11  |-  ( ph  ->  Ord  X )
106 ordirr 4542 . . . . . . . . . . 11  |-  ( Ord 
X  ->  -.  X  e.  X )
107105, 106syl 16 . . . . . . . . . 10  |-  ( ph  ->  -.  X  e.  X
)
108 elsni 3783 . . . . . . . . . . . 12  |-  ( ( O `  U. dom  O )  e.  { X }  ->  ( O `  U. dom  O )  =  X )
109108eleq2d 2456 . . . . . . . . . . 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 6674 . . . . . . . . . . . . . 14  |-  1o  =  { (/) }
113112difeq2i 3407 . . . . . . . . . . . . 13  |-  ( _V 
\  1o )  =  ( _V  \  { (/)
} )
114113imaeq2i 5143 . . . . . . . . . . . 12  |-  ( `' F " ( _V 
\  1o ) )  =  ( `' F " ( _V  \  { (/)
} ) )
115 eldifi 3414 . . . . . . . . . . . . . . . 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 5684 . . . . . . . . . . . . . . . 16  |-  ( G `
 k )  e. 
_V
119 ifexg 3743 . . . . . . . . . . . . . . . 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 2395 . . . . . . . . . . . . . . . . 17  |-  ( t  =  k  ->  (
t  =  X  <->  k  =  X ) )
122 fveq2 5670 . . . . . . . . . . . . . . . . 17  |-  ( t  =  k  ->  ( G `  t )  =  ( G `  k ) )
123121, 122ifbieq2d 3704 . . . . . . . . . . . . . . . 16  |-  ( t  =  k  ->  if ( t  =  X ,  Y ,  ( G `  t ) )  =  if ( k  =  X ,  Y ,  ( G `  k ) ) )
124123, 9fvmptg 5745 . . . . . . . . . . . . . . 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 3415 . . . . . . . . . . . . . . . . 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 3774 . . . . . . . . . . . . . . . . 17  |-  ( k  e.  { X }  <->  k  =  X )
129 elun2 3460 . . . . . . . . . . . . . . . . 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 3691 . . . . . . . . . . . . . . 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 3455 . . . . . . . . . . . . . . . . 17  |-  ( `' G " ( _V 
\  1o ) ) 
C_  ( ( `' G " ( _V 
\  1o ) )  u.  { X }
)
135 sscon 3426 . . . . . . . . . . . . . . . . 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 3289 . . . . . . . . . . . . . . 15  |-  ( k  e.  ( B  \ 
( ( `' G " ( _V  \  1o ) )  u.  { X } ) )  -> 
k  e.  ( B 
\  ( `' G " ( _V  \  1o ) ) ) )
138113imaeq2i 5143 . . . . . . . . . . . . . . . . 17  |-  ( `' G " ( _V 
\  1o ) )  =  ( `' G " ( _V  \  { (/)
} ) )
139 eqimss2 3346 . . . . . . . . . . . . . . . . 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 5805 . . . . . . . . . . . . . . 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 2425 . . . . . . . . . . . . 13  |-  ( (
ph  /\  k  e.  ( B  \  (
( `' G "
( _V  \  1o ) )  u.  { X } ) ) )  ->  ( F `  k )  =  (/) )
14431, 143suppss 5804 . . . . . . . . . . . 12  |-  ( ph  ->  ( `' F "
( _V  \  { (/)
} ) )  C_  ( ( `' G " ( _V  \  1o ) )  u.  { X } ) )
145114, 144syl5eqss 3337 . . . . . . . . . . 11  |-  ( ph  ->  ( `' F "
( _V  \  1o ) )  C_  (
( `' G "
( _V  \  1o ) )  u.  { X } ) )
146145, 93sseldd 3294 . . . . . . . . . 10  |-  ( ph  ->  ( O `  U. dom  O )  e.  ( ( `' G "
( _V  \  1o ) )  u.  { X } ) )
147 elun 3433 . . . . . . . . . 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 4560 . . . . . . . 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 6038 . . . . 5  |-  ( ph  ->  ( A  ^o  ( O `  U. dom  O
) )  =  ( A  ^o  X ) )
156154fveq2d 5674 . . . . . 6  |-  ( ph  ->  ( F `  ( O `  U. dom  O
) )  =  ( F `  X ) )
157156, 46eqtrd 2421 . . . . 5  |-  ( ph  ->  ( F `  ( O `  U. dom  O
) )  =  Y )
158155, 157oveq12d 6040 . . . 4  |-  ( ph  ->  ( ( A  ^o  ( O `  U. dom  O ) )  .o  ( F `  ( O `  U. dom  O ) ) )  =  ( ( A  ^o  X
)  .o  Y ) )
159 nnord 4795 . . . . . . . . 9  |-  ( U. dom  O  e.  om  ->  Ord  U. dom  O )
16020, 159syl 16 . . . . . . . 8  |-  ( ph  ->  Ord  U. dom  O
)
161 sssucid 4601 . . . . . . . . . 10  |-  U. dom  O 
C_  suc  U. dom  O
162161, 14syl5sseqr 3342 . . . . . . . . 9  |-  ( ph  ->  U. dom  O  C_  dom  O )
163 f1ofo 5623 . . . . . . . . . . . . 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 5600 . . . . . . . . . . . 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 5533 . . . . . . . . . . . . . 14  |-  ( O : dom  O --> ( `' F " ( _V 
\  1o ) )  ->  O  Fn  dom  O )
16891, 167ax-mp 8 . . . . . . . . . . . . 13  |-  O  Fn  dom  O
169 fnsnfv 5727 . . . . . . . . . . . . 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 3772 . . . . . . . . . . . 12  |-  ( ph  ->  { ( O `  U. dom  O ) }  =  { X }
)
172170, 171eqtr3d 2423 . . . . . . . . . . 11  |-  ( ph  ->  ( O " { U. dom  O } )  =  { X }
)
173166, 172difeq12d 3411 . . . . . . . . . 10  |-  ( ph  ->  ( ( O " dom  O )  \  ( O " { U. dom  O } ) )  =  ( ( `' F " ( _V  \  1o ) )  \  { X } ) )
174 ordirr 4542 . . . . . . . . . . . . . . . . 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 3813 . . . . . . . . . . . . . . . 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 3617 . . . . . . . . . . . . . . 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 3652 . . . . . . . . . . . . . 14  |-  ( ( U. dom  O  u.  { U. dom  O }
)  \  { U. dom  O } )  =  ( U. dom  O  \  { U. dom  O }
)
181179, 180syl6eqr 2439 . . . . . . . . . . . . 13  |-  ( ph  ->  U. dom  O  =  ( ( U. dom  O  u.  { U. dom  O } )  \  { U. dom  O } ) )
182 df-suc 4530 . . . . . . . . . . . . . . 15  |-  suc  U. dom  O  =  ( U. dom  O  u.  { U. dom  O } )
18314, 182syl6eq 2437 . . . . . . . . . . . . . 14  |-  ( ph  ->  dom  O  =  ( U. dom  O  u.  { U. dom  O }
) )
184183difeq1d 3409 . . . . . . . . . . . . 13  |-  ( ph  ->  ( dom  O  \  { U. dom  O }
)  =  ( ( U. dom  O  u.  { U. dom  O }
)  \  { U. dom  O } ) )
185181, 184eqtr4d 2424 . . . . . . . . . . . 12  |-  ( ph  ->  U. dom  O  =  ( dom  O  \  { U. dom  O }
) )
186185imaeq2d 5145 . . . . . . . . . . 11  |-  ( ph  ->  ( O " U. dom  O )  =  ( O " ( dom 
O  \  { U. dom  O } ) ) )
187 dff1o3 5622 . . . . . . . . . . . . 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 5470 . . . . . . . . . . . 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 2421 . . . . . . . . . 10  |-  ( ph  ->  ( O " U. dom  O )  =  ( ( O " dom  O )  \  ( O
" { U. dom  O } ) ) )
1928, 107ssneldd 3296 . . . . . . . . . . . . 13  |-  ( ph  ->  -.  X  e.  ( `' G " ( _V 
\  1o ) ) )
193 disjsn 3813 . . . . . . . . . . . . 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 5684 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( G `
 X )  e. 
_V
196 dif1o 6682 . . . . . . . . . . . . . . . . . . . . . 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 5533 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( G : B --> A  ->  G  Fn  B )
19927, 198syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  G  Fn  B )
200 elpreima 5791 . . . . . . . . . . . . . . . . . . . . . . . 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 3292 . . . . . . . . . . . . . . . . . . . . . . 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 2620 . . . . . . . . . . . . . . . . . . 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 5670 . . . . . . . . . . . . . . . . . 18  |-  ( k  =  X  ->  ( G `  k )  =  ( G `  X ) )
210209eqeq1d 2397 . . . . . . . . . . . . . . . . 17  |-  ( k  =  X  ->  (
( G `  k
)  =  (/)  <->  ( G `  X )  =  (/) ) )
211208, 210syl5ibrcom 214 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  k  e.  ( B  \  ( `' F " ( _V 
\  { (/) } ) ) ) )  -> 
( k  =  X  ->  ( G `  k )  =  (/) ) )
212 eldifi 3414 . . . . . . . . . . . . . . . . . . . 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 3312 . . . . . . . . . . . . . . . . . . . 20  |-  ( `' F " ( _V 
\  { (/) } ) )  C_  ( `' F " ( _V  \  { (/) } ) )
218217a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( `' F "
( _V  \  { (/)
} ) )  C_  ( `' F " ( _V 
\  { (/) } ) ) )
21931, 218suppssr 5805 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  k  e.  ( B  \  ( `' F " ( _V 
\  { (/) } ) ) ) )  -> 
( F `  k
)  =  (/) )
220216, 219eqtr3d 2423 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  k  e.  ( B  \  ( `' F " ( _V 
\  { (/) } ) ) ) )  ->  if ( k  =  X ,  Y ,  ( G `  k ) )  =  (/) )
221132eqeq1d 2397 . . . . . . . . . . . . . . . . 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 5804 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( `' G "
( _V  \  { (/)
} ) )  C_  ( `' F " ( _V 
\  { (/) } ) ) )
225224, 138, 1143sstr4g 3334 . . . . . . . . . . . . 13  |-  ( ph  ->  ( `' G "
( _V  \  1o ) )  C_  ( `' F " ( _V 
\  1o ) ) )
226 reldisj 3616 . . . . . . . . . . . . 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 3436 . . . . . . . . . . . . 13  |-  ( ( `' G " ( _V 
\  1o ) )  u.  { X }
)  =  ( { X }  u.  ( `' G " ( _V 
\  1o ) ) )
230145, 229syl6sseq 3339 . . . . . . . . . . . 12  |-  ( ph  ->  ( `' F "
( _V  \  1o ) )  C_  ( { X }  u.  ( `' G " ( _V 
\  1o ) ) ) )
231 ssundif 3656 . . . . . . . . . . . 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 3310 . . . . . . . . . 10  |-  ( ph  ->  ( `' G "
( _V  \  1o ) )  =  ( ( `' F "
( _V  \  1o ) )  \  { X } ) )
234173, 191, 2333eqtr4rd 2432 . . . . . . . . 9  |-  ( ph  ->  ( `' G "
( _V  \  1o ) )  =  ( O " U. dom  O ) )
235 isores3 5996 . . . . . . . . 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 7557 . . . . . . . . . 10  |-  ( ph  ->  (  _E  We  ( `' G " ( _V 
\  1o ) )  /\  dom  K  e. 
om ) )
239238simpld 446 . . . . . . . . 9  |-  ( ph  ->  _E  We  ( `' G " ( _V 
\  1o ) ) )
240 epse 4508 . . . . . . . . 9  |-  _E Se  ( `' G " ( _V 
\  1o ) )
241237oieu 7443 . . . . . . . . 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 5674 . . . . 5  |-  ( ph  ->  ( M `  U. dom  O )  =  ( M `  dom  K
) )
246 eleq1 2449 . . . . . . . . . 10  |-  ( x  =  (/)  ->  ( x  e.  dom  O  <->  (/)  e.  dom  O ) )
247 fveq2 5670 . . . . . . . . . . 11  |-  ( x  =  (/)  ->  ( H `
 x )  =  ( H `  (/) ) )
248 fveq2 5670 . . . . . . . . . . . 12  |-  ( x  =  (/)  ->  ( M `
 x )  =  ( M `  (/) ) )
249 0ex 4282 . . . . . . . . . . . . 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 6651 . . . . . . . . . . . . 13  |-  ( (/)  e.  _V  ->  ( M `  (/) )  =  (/) )
252249, 251ax-mp 8 . . . . . . . . . . . 12  |-  ( M `
 (/) )  =  (/)
253248, 252syl6eq 2437 . . . . . . . . . . 11  |-  ( x  =  (/)  ->  ( M `
 x )  =  (/) )
254247, 253eqeq12d 2403 . . . . . . . . . 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 2449 . . . . . . . . . 10  |-  ( x  =  y  ->  (
x  e.  dom  O  <->  y  e.  dom  O ) )
258 fveq2 5670 . . . . . . . . . . 11  |-  ( x  =  y  ->  ( H `  x )  =  ( H `  y ) )
259 fveq2 5670 . . . . . . . . . . 11  |-  ( x  =  y  ->  ( M `  x )  =  ( M `  y ) )
260258, 259eqeq12d 2403 . . . . . . . . . 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 2449 . . . . . . . . . 10  |-  ( x  =  suc  y  -> 
( x  e.  dom  O  <->  suc  y  e.  dom  O ) )
264 fveq2 5670 . . . . . . . . . . 11  |-  ( x  =  suc  y  -> 
( H `  x
)  =  ( H `
 suc  y )
)
265 fveq2 5670 . . . . . . . . . . 11  |-  ( x  =  suc  y  -> 
( M `  x
)  =  ( M `
 suc  y )
)
266264, 265eqeq12d 2403 . . . . . . . . . 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 2449 . . . . . . . . . 10  |-  ( x  =  U. dom  O  ->  ( x  e.  dom  O  <->  U. dom  O  e.  dom  O ) )
270 fveq2 5670 . . . . . . . . . . 11  |-  ( x  =  U. dom  O  ->  ( H `  x
)  =  ( H `
 U. dom  O
) )
271 fveq2 5670 . . . . . . . . . . 11  |-  ( x  =  U. dom  O  ->  ( M `  x
)  =  ( M `
 U. dom  O
) )
272270, 271eqeq12d 2403 . . . . . . . . . 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 6651 . . . . . . . . . 10  |-  ( (/)  e.  _V  ->  ( H `  (/) )  =  (/) )
276249, 275mp1i 12 . . . . . . . . 9  |-  ( (/)  e.  dom  O  ->  ( H `  (/) )  =  (/) )
277276a1i 11 . . . . . . . 8  |-  ( ph  ->  ( (/)  e.  dom  O  ->  ( H `  (/) )  =  (/) ) )
278 nnord 4795 . . . . . . . . . . . . . . . 16  |-  ( dom 
O  e.  om  ->  Ord 
dom  O )
27917, 278syl 16 . . . . . . . . . . . . . . 15  |-  ( ph  ->  Ord  dom  O )
280 ordtr 4538 . . . . . . . . . . . . . . 15  |-  ( Ord 
dom  O  ->  Tr  dom  O )
281279, 280syl 16 . . . . . . . . . . . . . 14  |-  ( ph  ->  Tr  dom  O )
282 trsuc 4608 . . . . . . . . . . . . . 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 6030 . . . . . . . . . . . . . 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 4797 . . . . . . . . . . . . . . . . . . 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 7560 . . . . . . . . . . . . . . . 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 7560 . . . . . . . . . . . . . . . . 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 5672 . . . . . . . . . . . . . . . . . . . . 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 2456 . . . . . . . . . . . . . . . . . . . . . . 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 4744 . . . . . . . . . . . . . . . . . . . . . . 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 5687 . . . . . . . . . . . . . . . . . . . . 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 2423 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  suc  y  e. 
dom  O )  -> 
( K `  y
)  =  ( O `
 y ) )
307306oveq2d 6038 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  suc  y  e. 
dom  O )  -> 
( A  ^o  ( K `  y )
)  =  ( A  ^o  ( O `  y ) ) )
308 cnvimass 5166 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( `' G " ( _V 
\  1o ) ) 
C_  dom  G
309 fdm 5537 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( G : B --> A  ->  dom  G  =  B )
31027, 309syl 16 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  dom  G  =  B )
311308, 310syl5sseq 3341 . . . . . . . . . . . . . . . . . . . . . 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 2465 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  suc  y  e. 
dom  O )  -> 
y  e.  dom  K
)
315237oif 7434 . . . . . . . . . . . . . . . . . . . . . . 23  |-  K : dom  K --> ( `' G " ( _V  \  1o ) )
316315ffvelrni 5810 . . . . . . . . . . . . . . . . . . . . . 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 3294 . . . . . . . . . . . . . . . . . . . 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 5684 . . . . . . . . . . . . . . . . . . . . 21  |-  ( G `
 ( K `  y ) )  e. 
_V
321 ifexg 3743 . . . . . . . . . . . . . . . . . . . . 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 2395 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( t  =  ( K `  y )  ->  (
t  =  X  <->  ( K `  y )  =  X ) )
324 fveq2 5670 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( t  =  ( K `  y )  ->  ( G `  t )  =  ( G `  ( K `  y ) ) )
325323, 324ifbieq2d 3704 . . . . . . . . . . . . . . . . . . . . 21  |-  ( t  =  ( K `  y )  ->  if ( t  =  X ,  Y ,  ( G `  t ) )  =  if ( ( K `  y
)  =  X ,  Y ,  ( G `  ( K `  y
) ) ) )
326325, 9fvmptg 5745 . . . . . . . . . . . . . . . . . . . 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 5674 . . . . . . . . . . . . . . . . . . 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 2487 . . . . . . . . . . . . . . . . . . . . 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 3691 . . . . . . . . . . . . . . . . . . . 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 2430 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  suc  y  e. 
dom  O )  -> 
( G `  ( K `  y )
)  =  ( F `
 ( O `  y ) ) )
335307, 334oveq12d 6040 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  suc  y  e. 
dom  O )  -> 
( ( A  ^o  ( K `  y ) )  .o  ( G `
 ( K `  y ) ) )  =  ( ( A  ^o  ( O `  y ) )  .o  ( F `  ( O `  y )
) ) )
336335oveq1d 6037 . . . . . . . . . . . . . . . 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 2421 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  suc  y  e. 
dom  O )  -> 
( M `  suc  y )  =  ( ( ( A  ^o  ( O `  y ) )  .o  ( F `
 ( O `  y ) ) )  +o  ( M `  y ) ) )
338292, 337eqeq12d 2403 . . . . . . . . . . . . . 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 4813 . . . . . . 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 7558 . . . . 5  |-  ( ph  ->  ( ( A CNF  B
) `  G )  =  ( M `  dom  K ) )
349245, 347, 3483eqtr4d 2431 . . . 4  |-  ( ph  ->  ( H `  U. dom  O )  =  ( ( A CNF  B ) `
 G ) )
350158, 349oveq12d 6040 . . 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 2421 . 2  |-  ( ph  ->  ( H `  suc  U.
dom  O )  =  ( ( ( A  ^o  X )  .o  Y )  +o  (
( A CNF  B ) `
 G ) ) )
35212, 15, 3513eqtrd 2425 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 1717    =/= wne 2552   _Vcvv 2901    \ cdif 3262    u. cun 3263    i^i cin 3264    C_ wss 3265   (/)c0 3573   ifcif 3684   {csn 3759   U.cuni 3959   class class class wbr 4155    e. cmpt 4209   Tr wtr 4245    _E cep 4435   Se wse 4482    We wwe 4483   Ord word 4523   Oncon0 4524   suc csuc 4526   omcom 4787   `'ccnv 4819   dom cdm 4820    |` cres 4822   "cima 4823   Fun wfun 5390    Fn wfn 5391   -->wf 5392   -onto->wfo 5394   -1-1-onto->wf1o 5395   ` cfv 5396    Isom wiso 5397  (class class class)co 6022    e. cmpt2 6024  seq𝜔cseqom 6642   1oc1o 6655    +o coa 6659    .o comu 6660    ^o coe 6661   Fincfn 7047  OrdIsocoi 7413   CNF ccnf 7551
This theorem is referenced by:  cantnfp1  7572
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 1661  ax-8 1682  ax-13 1719  ax-14 1721  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2370  ax-rep 4263  ax-sep 4273  ax-nul 4281  ax-pow 4320  ax-pr 4346  ax-un 4643
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 2244  df-mo 2245  df-clab 2376  df-cleq 2382  df-clel 2385  df-nfc 2514  df-ne 2554  df-ral 2656  df-rex 2657  df-reu 2658  df-rmo 2659  df-rab 2660  df-v 2903  df-sbc 3107  df-csb 3197  df-dif 3268  df-un 3270  df-in 3272  df-ss 3279  df-pss 3281  df-nul 3574  df-if 3685  df-pw 3746  df-sn 3765  df-pr 3766  df-tp 3767  df-op 3768  df-uni 3960  df-int 3995  df-iun 4039  df-br 4156  df-opab 4210  df-mpt 4211  df-tr 4246  df-eprel 4437  df-id 4441  df-po 4446  df-so 4447  df-fr 4484  df-se 4485  df-we 4486  df-ord 4527  df-on 4528  df-lim 4529  df-suc 4530  df-om 4788  df-xp 4826  df-rel 4827  df-cnv 4828  df-co 4829  df-dm 4830  df-rn 4831  df-res 4832  df-ima 4833  df-iota 5360  df-fun 5398  df-fn 5399  df-f 5400  df-f1 5401  df-fo 5402  df-f1o 5403  df-fv 5404  df-isom 5405  df-ov 6025  df-oprab 6026  df-mpt2 6027  df-2nd 6291  df-riota 6487  df-recs 6571  df-rdg 6606  df-seqom 6643  df-1o 6662  df-oadd 6666  df-er 6843  df-map 6958  df-en 7048  df-dom 7049  df-sdom 7050  df-fin 7051  df-oi 7414  df-cnf 7552
  Copyright terms: Public domain W3C validator