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

Theorem cantnfp1lem3OLD 7906
Description: Lemma for cantnfp1OLD 7907. (Contributed by Mario Carneiro, 28-May-2015.) Obsolete version of cantnfp1lem3 7880 as of 1-Jul-2019. (New usage is discouraged.)
Hypotheses
Ref Expression
cantnfsOLD.1  |-  S  =  dom  ( A CNF  B
)
cantnfsOLD.2  |-  ( ph  ->  A  e.  On )
cantnfsOLD.3  |-  ( ph  ->  B  e.  On )
cantnfp1OLD.4  |-  ( ph  ->  G  e.  S )
cantnfp1OLD.5  |-  ( ph  ->  X  e.  B )
cantnfp1OLD.6  |-  ( ph  ->  Y  e.  A )
cantnfp1OLD.7  |-  ( ph  ->  ( `' G "
( _V  \  1o ) )  C_  X
)
cantnfp1OLD.f  |-  F  =  ( t  e.  B  |->  if ( t  =  X ,  Y , 
( G `  t
) ) )
cantnfp1OLD.8  |-  ( ph  -> 
(/)  e.  Y )
cantnfp1OLD.o  |-  O  = OrdIso
(  _E  ,  ( `' F " ( _V 
\  1o ) ) )
cantnfp1OLD.h  |-  H  = seq𝜔 ( ( k  e.  _V ,  z  e.  _V  |->  ( ( ( A  ^o  ( O `  k ) )  .o  ( F `  ( O `  k )
) )  +o  z
) ) ,  (/) )
cantnfp1OLD.k  |-  K  = OrdIso
(  _E  ,  ( `' G " ( _V 
\  1o ) ) )
cantnfp1OLD.m  |-  M  = seq𝜔 ( ( k  e.  _V ,  z  e.  _V  |->  ( ( ( A  ^o  ( K `  k ) )  .o  ( G `  ( K `  k )
) )  +o  z
) ) ,  (/) )
Assertion
Ref Expression
cantnfp1lem3OLD  |-  ( 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 cantnfp1lem3OLD
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 cantnfsOLD.1 . . 3  |-  S  =  dom  ( A CNF  B
)
2 cantnfsOLD.2 . . 3  |-  ( ph  ->  A  e.  On )
3 cantnfsOLD.3 . . 3  |-  ( ph  ->  B  e.  On )
4 cantnfp1OLD.o . . 3  |-  O  = OrdIso
(  _E  ,  ( `' F " ( _V 
\  1o ) ) )
5 cantnfp1OLD.4 . . . 4  |-  ( ph  ->  G  e.  S )
6 cantnfp1OLD.5 . . . 4  |-  ( ph  ->  X  e.  B )
7 cantnfp1OLD.6 . . . 4  |-  ( ph  ->  Y  e.  A )
8 cantnfp1OLD.7 . . . 4  |-  ( ph  ->  ( `' G "
( _V  \  1o ) )  C_  X
)
9 cantnfp1OLD.f . . . 4  |-  F  =  ( t  e.  B  |->  if ( t  =  X ,  Y , 
( G `  t
) ) )
101, 2, 3, 5, 6, 7, 8, 9cantnfp1lem1OLD 7904 . . 3  |-  ( ph  ->  F  e.  S )
11 cantnfp1OLD.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, 11cantnfvalOLD 7898 . 2  |-  ( ph  ->  ( ( A CNF  B
) `  F )  =  ( H `  dom  O ) )
13 cantnfp1OLD.8 . . . 4  |-  ( ph  -> 
(/)  e.  Y )
141, 2, 3, 5, 6, 7, 8, 9, 13, 4cantnfp1lem2OLD 7905 . . 3  |-  ( ph  ->  dom  O  =  suc  U.
dom  O )
1514fveq2d 5690 . 2  |-  ( ph  ->  ( H `  dom  O )  =  ( H `
 suc  U. dom  O
) )
161, 2, 3, 4, 10cantnfclOLD 7897 . . . . . . 7  |-  ( ph  ->  (  _E  We  ( `' F " ( _V 
\  1o ) )  /\  dom  O  e. 
om ) )
1716simprd 463 . . . . . 6  |-  ( ph  ->  dom  O  e.  om )
1814, 17eqeltrrd 2513 . . . . 5  |-  ( ph  ->  suc  U. dom  O  e.  om )
19 peano2b 6487 . . . . 5  |-  ( U. dom  O  e.  om  <->  suc  U. dom  O  e.  om )
2018, 19sylibr 212 . . . 4  |-  ( ph  ->  U. dom  O  e. 
om )
211, 2, 3, 4, 10, 11cantnfsucOLD 7900 . . . 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 668 . . 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 5184 . . . . . . . . . . . . . . . . 17  |-  ( `' F " ( _V 
\  1o ) ) 
C_  dom  F
247adantr 465 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  t  e.  B )  ->  Y  e.  A )
251, 2, 3cantnfsOLD 7896 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( G  e.  S  <->  ( G : B --> A  /\  ( `' G " ( _V 
\  1o ) )  e.  Fin ) ) )
265, 25mpbid 210 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( G : B --> A  /\  ( `' G " ( _V  \  1o ) )  e.  Fin ) )
2726simpld 459 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  G : B --> A )
2827ffvelrnda 5838 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  t  e.  B )  ->  ( G `  t )  e.  A )
29 ifcl 3826 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( Y  e.  A  /\  ( G `  t )  e.  A )  ->  if ( t  =  X ,  Y ,  ( G `  t ) )  e.  A )
3024, 28, 29syl2anc 661 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  t  e.  B )  ->  if ( t  =  X ,  Y ,  ( G `  t ) )  e.  A )
3130, 9fmptd 5862 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  F : B --> A )
32 fdm 5558 . . . . . . . . . . . . . . . . . 18  |-  ( F : B --> A  ->  dom  F  =  B )
3331, 32syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  dom  F  =  B )
3423, 33syl5sseq 3399 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( `' F "
( _V  \  1o ) )  C_  B
)
353, 34ssexd 4434 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( `' F "
( _V  \  1o ) )  e.  _V )
3616simpld 459 . . . . . . . . . . . . . . 15  |-  ( ph  ->  _E  We  ( `' F " ( _V 
\  1o ) ) )
374oiiso 7743 . . . . . . . . . . . . . . 15  |-  ( ( ( `' F "
( _V  \  1o ) )  e.  _V  /\  _E  We  ( `' F " ( _V 
\  1o ) ) )  ->  O  Isom  _E  ,  _E  ( dom 
O ,  ( `' F " ( _V 
\  1o ) ) ) )
3835, 36, 37syl2anc 661 . . . . . . . . . . . . . 14  |-  ( ph  ->  O  Isom  _E  ,  _E  ( dom  O ,  ( `' F " ( _V 
\  1o ) ) ) )
39 isof1o 6011 . . . . . . . . . . . . . 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 5648 . . . . . . . . . . . . 13  |-  ( O : dom  O -1-1-onto-> ( `' F " ( _V 
\  1o ) )  ->  `' O :
( `' F "
( _V  \  1o ) ) -1-1-onto-> dom  O )
42 f1of 5636 . . . . . . . . . . . . 13  |-  ( `' O : ( `' F " ( _V 
\  1o ) ) -1-1-onto-> dom 
O  ->  `' O : ( `' F " ( _V  \  1o ) ) --> dom  O
)
4340, 41, 423syl 20 . . . . . . . . . . . 12  |-  ( ph  ->  `' O : ( `' F " ( _V 
\  1o ) ) --> dom  O )
44 iftrue 3792 . . . . . . . . . . . . . . . . 17  |-  ( t  =  X  ->  if ( t  =  X ,  Y ,  ( G `  t ) )  =  Y )
4544, 9fvmptg 5767 . . . . . . . . . . . . . . . 16  |-  ( ( X  e.  B  /\  Y  e.  A )  ->  ( F `  X
)  =  Y )
466, 7, 45syl2anc 661 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( F `  X
)  =  Y )
47 onelon 4739 . . . . . . . . . . . . . . . . . 18  |-  ( ( A  e.  On  /\  Y  e.  A )  ->  Y  e.  On )
482, 7, 47syl2anc 661 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  Y  e.  On )
49 on0eln0 4769 . . . . . . . . . . . . . . . . 17  |-  ( Y  e.  On  ->  ( (/) 
e.  Y  <->  Y  =/=  (/) ) )
5048, 49syl 16 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( (/)  e.  Y  <->  Y  =/=  (/) ) )
5113, 50mpbid 210 . . . . . . . . . . . . . . 15  |-  ( ph  ->  Y  =/=  (/) )
5246, 51eqnetrd 2621 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( F `  X
)  =/=  (/) )
53 fvex 5696 . . . . . . . . . . . . . . 15  |-  ( F `
 X )  e. 
_V
54 dif1o 6932 . . . . . . . . . . . . . . 15  |-  ( ( F `  X )  e.  ( _V  \  1o )  <->  ( ( F `
 X )  e. 
_V  /\  ( F `  X )  =/=  (/) ) )
5553, 54mpbiran 909 . . . . . . . . . . . . . 14  |-  ( ( F `  X )  e.  ( _V  \  1o )  <->  ( F `  X )  =/=  (/) )
5652, 55sylibr 212 . . . . . . . . . . . . 13  |-  ( ph  ->  ( F `  X
)  e.  ( _V 
\  1o ) )
57 ffn 5554 . . . . . . . . . . . . . 14  |-  ( F : B --> A  ->  F  Fn  B )
58 elpreima 5818 . . . . . . . . . . . . . 14  |-  ( F  Fn  B  ->  ( X  e.  ( `' F " ( _V  \  1o ) )  <->  ( X  e.  B  /\  ( F `  X )  e.  ( _V  \  1o ) ) ) )
5931, 57, 583syl 20 . . . . . . . . . . . . 13  |-  ( ph  ->  ( X  e.  ( `' F " ( _V 
\  1o ) )  <-> 
( X  e.  B  /\  ( F `  X
)  e.  ( _V 
\  1o ) ) ) )
606, 56, 59mpbir2and 913 . . . . . . . . . . . 12  |-  ( ph  ->  X  e.  ( `' F " ( _V 
\  1o ) ) )
6143, 60ffvelrnd 5839 . . . . . . . . . . 11  |-  ( ph  ->  ( `' O `  X )  e.  dom  O )
62 elssuni 4116 . . . . . . . . . . 11  |-  ( ( `' O `  X )  e.  dom  O  -> 
( `' O `  X )  C_  U. dom  O )
6361, 62syl 16 . . . . . . . . . 10  |-  ( ph  ->  ( `' O `  X )  C_  U. dom  O )
644oicl 7735 . . . . . . . . . . . 12  |-  Ord  dom  O
65 ordelon 4738 . . . . . . . . . . . 12  |-  ( ( Ord  dom  O  /\  ( `' O `  X )  e.  dom  O )  ->  ( `' O `  X )  e.  On )
6664, 61, 65sylancr 663 . . . . . . . . . . 11  |-  ( ph  ->  ( `' O `  X )  e.  On )
67 nnon 6477 . . . . . . . . . . . 12  |-  ( U. dom  O  e.  om  ->  U.
dom  O  e.  On )
6820, 67syl 16 . . . . . . . . . . 11  |-  ( ph  ->  U. dom  O  e.  On )
69 ontri1 4748 . . . . . . . . . . 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 661 . . . . . . . . . 10  |-  ( ph  ->  ( ( `' O `  X )  C_  U. dom  O  <->  -.  U. dom  O  e.  ( `' O `  X ) ) )
7163, 70mpbid 210 . . . . . . . . 9  |-  ( ph  ->  -.  U. dom  O  e.  ( `' O `  X ) )
72 sucidg 4792 . . . . . . . . . . . . . 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 2515 . . . . . . . . . . . 12  |-  ( ph  ->  U. dom  O  e. 
dom  O )
75 isorel 6012 . . . . . . . . . . . 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 1216 . . . . . . . . . . 11  |-  ( ph  ->  ( U. dom  O  _E  ( `' O `  X )  <->  ( O `  U. dom  O )  _E  ( O `  ( `' O `  X ) ) ) )
77 fvex 5696 . . . . . . . . . . . 12  |-  ( `' O `  X )  e.  _V
7877epelc 4629 . . . . . . . . . . 11  |-  ( U. dom  O  _E  ( `' O `  X )  <->  U. dom  O  e.  ( `' O `  X ) )
79 fvex 5696 . . . . . . . . . . . 12  |-  ( O `
 ( `' O `  X ) )  e. 
_V
8079epelc 4629 . . . . . . . . . . 11  |-  ( ( O `  U. dom  O )  _E  ( O `
 ( `' O `  X ) )  <->  ( O `  U. dom  O )  e.  ( O `  ( `' O `  X ) ) )
8176, 78, 803bitr3g 287 . . . . . . . . . 10  |-  ( ph  ->  ( U. dom  O  e.  ( `' O `  X )  <->  ( O `  U. dom  O )  e.  ( O `  ( `' O `  X ) ) ) )
82 f1ocnvfv2 5979 . . . . . . . . . . . 12  |-  ( ( O : dom  O -1-1-onto-> ( `' F " ( _V 
\  1o ) )  /\  X  e.  ( `' F " ( _V 
\  1o ) ) )  ->  ( O `  ( `' O `  X ) )  =  X )
8340, 60, 82syl2anc 661 . . . . . . . . . . 11  |-  ( ph  ->  ( O `  ( `' O `  X ) )  =  X )
8483eleq2d 2505 . . . . . . . . . 10  |-  ( ph  ->  ( ( O `  U. dom  O )  e.  ( O `  ( `' O `  X ) )  <->  ( O `  U. dom  O )  e.  X ) )
8581, 84bitrd 253 . . . . . . . . 9  |-  ( ph  ->  ( U. dom  O  e.  ( `' O `  X )  <->  ( O `  U. dom  O )  e.  X ) )
8671, 85mtbid 300 . . . . . . . 8  |-  ( ph  ->  -.  ( O `  U. dom  O )  e.  X )
878sseld 3350 . . . . . . . . . 10  |-  ( ph  ->  ( ( O `  U. dom  O )  e.  ( `' G "
( _V  \  1o ) )  ->  ( O `  U. dom  O
)  e.  X ) )
88 onss 6397 . . . . . . . . . . . . . . . 16  |-  ( B  e.  On  ->  B  C_  On )
893, 88syl 16 . . . . . . . . . . . . . . 15  |-  ( ph  ->  B  C_  On )
9034, 89sstrd 3361 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( `' F "
( _V  \  1o ) )  C_  On )
914oif 7736 . . . . . . . . . . . . . . . 16  |-  O : dom  O --> ( `' F " ( _V  \  1o ) )
9291ffvelrni 5837 . . . . . . . . . . . . . . 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 3352 . . . . . . . . . . . . 13  |-  ( ph  ->  ( O `  U. dom  O )  e.  On )
95 eloni 4724 . . . . . . . . . . . . 13  |-  ( ( O `  U. dom  O )  e.  On  ->  Ord  ( O `  U. dom  O ) )
9694, 95syl 16 . . . . . . . . . . . 12  |-  ( ph  ->  Ord  ( O `  U. dom  O ) )
97 ordn2lp 4734 . . . . . . . . . . . 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 422 . . . . . . . . . . 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 212 . . . . . . . . . 10  |-  ( ph  ->  ( ( O `  U. dom  O )  e.  X  ->  -.  X  e.  ( O `  U. dom  O ) ) )
10187, 100syld 44 . . . . . . . . 9  |-  ( ph  ->  ( ( O `  U. dom  O )  e.  ( `' G "
( _V  \  1o ) )  ->  -.  X  e.  ( O `  U. dom  O ) ) )
102 onelon 4739 . . . . . . . . . . . . 13  |-  ( ( B  e.  On  /\  X  e.  B )  ->  X  e.  On )
1033, 6, 102syl2anc 661 . . . . . . . . . . . 12  |-  ( ph  ->  X  e.  On )
104 eloni 4724 . . . . . . . . . . . 12  |-  ( X  e.  On  ->  Ord  X )
105103, 104syl 16 . . . . . . . . . . 11  |-  ( ph  ->  Ord  X )
106 ordirr 4732 . . . . . . . . . . 11  |-  ( Ord 
X  ->  -.  X  e.  X )
107105, 106syl 16 . . . . . . . . . 10  |-  ( ph  ->  -.  X  e.  X
)
108 elsni 3897 . . . . . . . . . . . 12  |-  ( ( O `  U. dom  O )  e.  { X }  ->  ( O `  U. dom  O )  =  X )
109108eleq2d 2505 . . . . . . . . . . 11  |-  ( ( O `  U. dom  O )  e.  { X }  ->  ( X  e.  ( O `  U. dom  O )  <->  X  e.  X ) )
110109notbid 294 . . . . . . . . . 10  |-  ( ( O `  U. dom  O )  e.  { X }  ->  ( -.  X  e.  ( O `  U. dom  O )  <->  -.  X  e.  X ) )
111107, 110syl5ibrcom 222 . . . . . . . . 9  |-  ( ph  ->  ( ( O `  U. dom  O )  e. 
{ X }  ->  -.  X  e.  ( O `
 U. dom  O
) ) )
112 df1o2 6924 . . . . . . . . . . . . . 14  |-  1o  =  { (/) }
113112difeq2i 3466 . . . . . . . . . . . . 13  |-  ( _V 
\  1o )  =  ( _V  \  { (/)
} )
114113imaeq2i 5162 . . . . . . . . . . . 12  |-  ( `' F " ( _V 
\  1o ) )  =  ( `' F " ( _V  \  { (/)
} ) )
115 eldifi 3473 . . . . . . . . . . . . . . . 16  |-  ( k  e.  ( B  \ 
( ( `' G " ( _V  \  1o ) )  u.  { X } ) )  -> 
k  e.  B )
116115adantl 466 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  k  e.  ( B  \  (
( `' G "
( _V  \  1o ) )  u.  { X } ) ) )  ->  k  e.  B
)
1177adantr 465 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  k  e.  ( B  \  (
( `' G "
( _V  \  1o ) )  u.  { X } ) ) )  ->  Y  e.  A
)
118 fvex 5696 . . . . . . . . . . . . . . . 16  |-  ( G `
 k )  e. 
_V
119 ifexg 3854 . . . . . . . . . . . . . . . 16  |-  ( ( Y  e.  A  /\  ( G `  k )  e.  _V )  ->  if ( k  =  X ,  Y ,  ( G `  k ) )  e.  _V )
120117, 118, 119sylancl 662 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  k  e.  ( B  \  (
( `' G "
( _V  \  1o ) )  u.  { X } ) ) )  ->  if ( k  =  X ,  Y ,  ( G `  k ) )  e. 
_V )
121 eqeq1 2444 . . . . . . . . . . . . . . . . 17  |-  ( t  =  k  ->  (
t  =  X  <->  k  =  X ) )
122 fveq2 5686 . . . . . . . . . . . . . . . . 17  |-  ( t  =  k  ->  ( G `  t )  =  ( G `  k ) )
123121, 122ifbieq2d 3809 . . . . . . . . . . . . . . . 16  |-  ( t  =  k  ->  if ( t  =  X ,  Y ,  ( G `  t ) )  =  if ( k  =  X ,  Y ,  ( G `  k ) ) )
124123, 9fvmptg 5767 . . . . . . . . . . . . . . 15  |-  ( ( k  e.  B  /\  if ( k  =  X ,  Y ,  ( G `  k ) )  e.  _V )  ->  ( F `  k
)  =  if ( k  =  X ,  Y ,  ( G `  k ) ) )
125116, 120, 124syl2anc 661 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  k  e.  ( B  \  (
( `' G "
( _V  \  1o ) )  u.  { X } ) ) )  ->  ( F `  k )  =  if ( k  =  X ,  Y ,  ( G `  k ) ) )
126 eldifn 3474 . . . . . . . . . . . . . . . . 17  |-  ( k  e.  ( B  \ 
( ( `' G " ( _V  \  1o ) )  u.  { X } ) )  ->  -.  k  e.  (
( `' G "
( _V  \  1o ) )  u.  { X } ) )
127126adantl 466 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  k  e.  ( B  \  (
( `' G "
( _V  \  1o ) )  u.  { X } ) ) )  ->  -.  k  e.  ( ( `' G " ( _V  \  1o ) )  u.  { X } ) )
128 elsn 3886 . . . . . . . . . . . . . . . . 17  |-  ( k  e.  { X }  <->  k  =  X )
129 elun2 3519 . . . . . . . . . . . . . . . . 17  |-  ( k  e.  { X }  ->  k  e.  ( ( `' G " ( _V 
\  1o ) )  u.  { X }
) )
130128, 129sylbir 213 . . . . . . . . . . . . . . . 16  |-  ( k  =  X  ->  k  e.  ( ( `' G " ( _V  \  1o ) )  u.  { X } ) )
131127, 130nsyl 121 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  k  e.  ( B  \  (
( `' G "
( _V  \  1o ) )  u.  { X } ) ) )  ->  -.  k  =  X )
132 iffalse 3794 . . . . . . . . . . . . . . 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 3514 . . . . . . . . . . . . . . . . 17  |-  ( `' G " ( _V 
\  1o ) ) 
C_  ( ( `' G " ( _V 
\  1o ) )  u.  { X }
)
135 sscon 3485 . . . . . . . . . . . . . . . . 17  |-  ( ( `' G " ( _V 
\  1o ) ) 
C_  ( ( `' G " ( _V 
\  1o ) )  u.  { X }
)  ->  ( B  \  ( ( `' G " ( _V  \  1o ) )  u.  { X } ) )  C_  ( B  \  ( `' G " ( _V 
\  1o ) ) ) )
136134, 135ax-mp 5 . . . . . . . . . . . . . . . 16  |-  ( B 
\  ( ( `' G " ( _V 
\  1o ) )  u.  { X }
) )  C_  ( B  \  ( `' G " ( _V  \  1o ) ) )
137136sseli 3347 . . . . . . . . . . . . . . 15  |-  ( k  e.  ( B  \ 
( ( `' G " ( _V  \  1o ) )  u.  { X } ) )  -> 
k  e.  ( B 
\  ( `' G " ( _V  \  1o ) ) ) )
138113imaeq2i 5162 . . . . . . . . . . . . . . . . 17  |-  ( `' G " ( _V 
\  1o ) )  =  ( `' G " ( _V  \  { (/)
} ) )
139 eqimss2 3404 . . . . . . . . . . . . . . . . 17  |-  ( ( `' G " ( _V 
\  1o ) )  =  ( `' G " ( _V  \  { (/)
} ) )  -> 
( `' G "
( _V  \  { (/)
} ) )  C_  ( `' G " ( _V 
\  1o ) ) )
140138, 139mp1i 12 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( `' G "
( _V  \  { (/)
} ) )  C_  ( `' G " ( _V 
\  1o ) ) )
14127, 140suppssrOLD 5832 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  k  e.  ( B  \  ( `' G " ( _V 
\  1o ) ) ) )  ->  ( G `  k )  =  (/) )
142137, 141sylan2 474 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  k  e.  ( B  \  (
( `' G "
( _V  \  1o ) )  u.  { X } ) ) )  ->  ( G `  k )  =  (/) )
143125, 133, 1423eqtrd 2474 . . . . . . . . . . . . 13  |-  ( (
ph  /\  k  e.  ( B  \  (
( `' G "
( _V  \  1o ) )  u.  { X } ) ) )  ->  ( F `  k )  =  (/) )
14431, 143suppssOLD 5831 . . . . . . . . . . . 12  |-  ( ph  ->  ( `' F "
( _V  \  { (/)
} ) )  C_  ( ( `' G " ( _V  \  1o ) )  u.  { X } ) )
145114, 144syl5eqss 3395 . . . . . . . . . . 11  |-  ( ph  ->  ( `' F "
( _V  \  1o ) )  C_  (
( `' G "
( _V  \  1o ) )  u.  { X } ) )
146145, 93sseldd 3352 . . . . . . . . . 10  |-  ( ph  ->  ( O `  U. dom  O )  e.  ( ( `' G "
( _V  \  1o ) )  u.  { X } ) )
147 elun 3492 . . . . . . . . . 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 196 . . . . . . . . 9  |-  ( ph  ->  ( ( O `  U. dom  O )  e.  ( `' G "
( _V  \  1o ) )  \/  ( O `  U. dom  O
)  e.  { X } ) )
149101, 111, 148mpjaod 381 . . . . . . . 8  |-  ( ph  ->  -.  X  e.  ( O `  U. dom  O ) )
150 ioran 490 . . . . . . . 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 664 . . . . . . 7  |-  ( ph  ->  -.  ( ( O `
 U. dom  O
)  e.  X  \/  X  e.  ( O `  U. dom  O ) ) )
152 ordtri3 4750 . . . . . . . 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 661 . . . . . . 7  |-  ( ph  ->  ( ( O `  U. dom  O )  =  X  <->  -.  ( ( O `  U. dom  O
)  e.  X  \/  X  e.  ( O `  U. dom  O ) ) ) )
154151, 153mpbird 232 . . . . . 6  |-  ( ph  ->  ( O `  U. dom  O )  =  X )
155154oveq2d 6102 . . . . 5  |-  ( ph  ->  ( A  ^o  ( O `  U. dom  O
) )  =  ( A  ^o  X ) )
156154fveq2d 5690 . . . . . 6  |-  ( ph  ->  ( F `  ( O `  U. dom  O
) )  =  ( F `  X ) )
157156, 46eqtrd 2470 . . . . 5  |-  ( ph  ->  ( F `  ( O `  U. dom  O
) )  =  Y )
158155, 157oveq12d 6104 . . . 4  |-  ( ph  ->  ( ( A  ^o  ( O `  U. dom  O ) )  .o  ( F `  ( O `  U. dom  O ) ) )  =  ( ( A  ^o  X
)  .o  Y ) )
159 nnord 6479 . . . . . . . . 9  |-  ( U. dom  O  e.  om  ->  Ord  U. dom  O )
16020, 159syl 16 . . . . . . . 8  |-  ( ph  ->  Ord  U. dom  O
)
161 sssucid 4791 . . . . . . . . . 10  |-  U. dom  O 
C_  suc  U. dom  O
162161, 14syl5sseqr 3400 . . . . . . . . 9  |-  ( ph  ->  U. dom  O  C_  dom  O )
163 f1ofo 5643 . . . . . . . . . . . . 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 5620 . . . . . . . . . . . 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 5554 . . . . . . . . . . . . . 14  |-  ( O : dom  O --> ( `' F " ( _V 
\  1o ) )  ->  O  Fn  dom  O )
16891, 167ax-mp 5 . . . . . . . . . . . . 13  |-  O  Fn  dom  O
169 fnsnfv 5746 . . . . . . . . . . . . 13  |-  ( ( O  Fn  dom  O  /\  U. dom  O  e. 
dom  O )  ->  { ( O `  U. dom  O ) }  =  ( O " { U. dom  O }
) )
170168, 74, 169sylancr 663 . . . . . . . . . . . 12  |-  ( ph  ->  { ( O `  U. dom  O ) }  =  ( O " { U. dom  O }
) )
171154sneqd 3884 . . . . . . . . . . . 12  |-  ( ph  ->  { ( O `  U. dom  O ) }  =  { X }
)
172170, 171eqtr3d 2472 . . . . . . . . . . 11  |-  ( ph  ->  ( O " { U. dom  O } )  =  { X }
)
173166, 172difeq12d 3470 . . . . . . . . . 10  |-  ( ph  ->  ( ( O " dom  O )  \  ( O " { U. dom  O } ) )  =  ( ( `' F " ( _V  \  1o ) )  \  { X } ) )
174 ordirr 4732 . . . . . . . . . . . . . . . . 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 3931 . . . . . . . . . . . . . . . 16  |-  ( ( U. dom  O  i^i  { U. dom  O }
)  =  (/)  <->  -.  U. dom  O  e.  U. dom  O
)
177175, 176sylibr 212 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( U. dom  O  i^i  { U. dom  O } )  =  (/) )
178 disj3 3718 . . . . . . . . . . . . . . 15  |-  ( ( U. dom  O  i^i  { U. dom  O }
)  =  (/)  <->  U. dom  O  =  ( U. dom  O 
\  { U. dom  O } ) )
179177, 178sylib 196 . . . . . . . . . . . . . 14  |-  ( ph  ->  U. dom  O  =  ( U. dom  O  \  { U. dom  O } ) )
180 difun2 3753 . . . . . . . . . . . . . 14  |-  ( ( U. dom  O  u.  { U. dom  O }
)  \  { U. dom  O } )  =  ( U. dom  O  \  { U. dom  O }
)
181179, 180syl6eqr 2488 . . . . . . . . . . . . 13  |-  ( ph  ->  U. dom  O  =  ( ( U. dom  O  u.  { U. dom  O } )  \  { U. dom  O } ) )
182 df-suc 4720 . . . . . . . . . . . . . . 15  |-  suc  U. dom  O  =  ( U. dom  O  u.  { U. dom  O } )
18314, 182syl6eq 2486 . . . . . . . . . . . . . 14  |-  ( ph  ->  dom  O  =  ( U. dom  O  u.  { U. dom  O }
) )
184183difeq1d 3468 . . . . . . . . . . . . 13  |-  ( ph  ->  ( dom  O  \  { U. dom  O }
)  =  ( ( U. dom  O  u.  { U. dom  O }
)  \  { U. dom  O } ) )
185181, 184eqtr4d 2473 . . . . . . . . . . . 12  |-  ( ph  ->  U. dom  O  =  ( dom  O  \  { U. dom  O }
) )
186185imaeq2d 5164 . . . . . . . . . . 11  |-  ( ph  ->  ( O " U. dom  O )  =  ( O " ( dom 
O  \  { U. dom  O } ) ) )
187 dff1o3 5642 . . . . . . . . . . . . 13  |-  ( O : dom  O -1-1-onto-> ( `' F " ( _V 
\  1o ) )  <-> 
( O : dom  O
-onto-> ( `' F "
( _V  \  1o ) )  /\  Fun  `' O ) )
188187simprbi 464 . . . . . . . . . . . 12  |-  ( O : dom  O -1-1-onto-> ( `' F " ( _V 
\  1o ) )  ->  Fun  `' O
)
189 imadif 5488 . . . . . . . . . . . 12  |-  ( Fun  `' O  ->  ( O
" ( dom  O  \  { U. dom  O } ) )  =  ( ( O " dom  O )  \  ( O " { U. dom  O } ) ) )
19040, 188, 1893syl 20 . . . . . . . . . . 11  |-  ( ph  ->  ( O " ( dom  O  \  { U. dom  O } ) )  =  ( ( O
" dom  O )  \  ( O " { U. dom  O }
) ) )
191186, 190eqtrd 2470 . . . . . . . . . 10  |-  ( ph  ->  ( O " U. dom  O )  =  ( ( O " dom  O )  \  ( O
" { U. dom  O } ) ) )
1928, 107ssneldd 3354 . . . . . . . . . . . . 13  |-  ( ph  ->  -.  X  e.  ( `' G " ( _V 
\  1o ) ) )
193 disjsn 3931 . . . . . . . . . . . . 13  |-  ( ( ( `' G "
( _V  \  1o ) )  i^i  { X } )  =  (/)  <->  -.  X  e.  ( `' G " ( _V  \  1o ) ) )
194192, 193sylibr 212 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( `' G " ( _V  \  1o ) )  i^i  { X } )  =  (/) )
195 fvex 5696 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( G `
 X )  e. 
_V
196 dif1o 6932 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( G `  X )  e.  ( _V  \  1o )  <->  ( ( G `
 X )  e. 
_V  /\  ( G `  X )  =/=  (/) ) )
197195, 196mpbiran 909 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( G `  X )  e.  ( _V  \  1o )  <->  ( G `  X )  =/=  (/) )
198 ffn 5554 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( G : B --> A  ->  G  Fn  B )
19927, 198syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  G  Fn  B )
200 elpreima 5818 . . . . . . . . . . . . . . . . . . . . . . . 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 3350 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( X  e.  ( `' G " ( _V 
\  1o ) )  ->  X  e.  X
) )
203201, 202sylbird 235 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( ( X  e.  B  /\  ( G `
 X )  e.  ( _V  \  1o ) )  ->  X  e.  X ) )
2046, 203mpand 675 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( ( G `  X )  e.  ( _V  \  1o )  ->  X  e.  X
) )
205197, 204syl5bir 218 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( ( G `  X )  =/=  (/)  ->  X  e.  X ) )
206205necon1bd 2674 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( -.  X  e.  X  ->  ( G `  X )  =  (/) ) )
207107, 206mpd 15 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( G `  X
)  =  (/) )
208207adantr 465 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  k  e.  ( B  \  ( `' F " ( _V 
\  { (/) } ) ) ) )  -> 
( G `  X
)  =  (/) )
209 fveq2 5686 . . . . . . . . . . . . . . . . . 18  |-  ( k  =  X  ->  ( G `  k )  =  ( G `  X ) )
210209eqeq1d 2446 . . . . . . . . . . . . . . . . 17  |-  ( k  =  X  ->  (
( G `  k
)  =  (/)  <->  ( G `  X )  =  (/) ) )
211208, 210syl5ibrcom 222 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  k  e.  ( B  \  ( `' F " ( _V 
\  { (/) } ) ) ) )  -> 
( k  =  X  ->  ( G `  k )  =  (/) ) )
212 eldifi 3473 . . . . . . . . . . . . . . . . . . . 20  |-  ( k  e.  ( B  \ 
( `' F "
( _V  \  { (/)
} ) ) )  ->  k  e.  B
)
213212adantl 466 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  k  e.  ( B  \  ( `' F " ( _V 
\  { (/) } ) ) ) )  -> 
k  e.  B )
2147adantr 465 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  k  e.  ( B  \  ( `' F " ( _V 
\  { (/) } ) ) ) )  ->  Y  e.  A )
215214, 118, 119sylancl 662 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  k  e.  ( B  \  ( `' F " ( _V 
\  { (/) } ) ) ) )  ->  if ( k  =  X ,  Y ,  ( G `  k ) )  e.  _V )
216213, 215, 124syl2anc 661 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  k  e.  ( B  \  ( `' F " ( _V 
\  { (/) } ) ) ) )  -> 
( F `  k
)  =  if ( k  =  X ,  Y ,  ( G `  k ) ) )
217 ssid 3370 . . . . . . . . . . . . . . . . . . . 20  |-  ( `' F " ( _V 
\  { (/) } ) )  C_  ( `' F " ( _V  \  { (/) } ) )
218217a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( `' F "
( _V  \  { (/)
} ) )  C_  ( `' F " ( _V 
\  { (/) } ) ) )
21931, 218suppssrOLD 5832 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  k  e.  ( B  \  ( `' F " ( _V 
\  { (/) } ) ) ) )  -> 
( F `  k
)  =  (/) )
220216, 219eqtr3d 2472 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  k  e.  ( B  \  ( `' F " ( _V 
\  { (/) } ) ) ) )  ->  if ( k  =  X ,  Y ,  ( G `  k ) )  =  (/) )
221132eqeq1d 2446 . . . . . . . . . . . . . . . . 17  |-  ( -.  k  =  X  -> 
( if ( k  =  X ,  Y ,  ( G `  k ) )  =  (/) 
<->  ( G `  k
)  =  (/) ) )
222220, 221syl5ibcom 220 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  k  e.  ( B  \  ( `' F " ( _V 
\  { (/) } ) ) ) )  -> 
( -.  k  =  X  ->  ( G `  k )  =  (/) ) )
223211, 222pm2.61d 158 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  k  e.  ( B  \  ( `' F " ( _V 
\  { (/) } ) ) ) )  -> 
( G `  k
)  =  (/) )
22427, 223suppssOLD 5831 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( `' G "
( _V  \  { (/)
} ) )  C_  ( `' F " ( _V 
\  { (/) } ) ) )
225224, 138, 1143sstr4g 3392 . . . . . . . . . . . . 13  |-  ( ph  ->  ( `' G "
( _V  \  1o ) )  C_  ( `' F " ( _V 
\  1o ) ) )
226 reldisj 3717 . . . . . . . . . . . . 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 210 . . . . . . . . . . 11  |-  ( ph  ->  ( `' G "
( _V  \  1o ) )  C_  (
( `' F "
( _V  \  1o ) )  \  { X } ) )
229 uncom 3495 . . . . . . . . . . . . 13  |-  ( ( `' G " ( _V 
\  1o ) )  u.  { X }
)  =  ( { X }  u.  ( `' G " ( _V 
\  1o ) ) )
230145, 229syl6sseq 3397 . . . . . . . . . . . 12  |-  ( ph  ->  ( `' F "
( _V  \  1o ) )  C_  ( { X }  u.  ( `' G " ( _V 
\  1o ) ) ) )
231 ssundif 3757 . . . . . . . . . . . 12  |-  ( ( `' F " ( _V 
\  1o ) ) 
C_  ( { X }  u.  ( `' G " ( _V  \  1o ) ) )  <->  ( ( `' F " ( _V 
\  1o ) ) 
\  { X }
)  C_  ( `' G " ( _V  \  1o ) ) )
232230, 231sylib 196 . . . . . . . . . . 11  |-  ( ph  ->  ( ( `' F " ( _V  \  1o ) )  \  { X } )  C_  ( `' G " ( _V 
\  1o ) ) )
233228, 232eqssd 3368 . . . . . . . . . 10  |-  ( ph  ->  ( `' G "
( _V  \  1o ) )  =  ( ( `' F "
( _V  \  1o ) )  \  { X } ) )
234173, 191, 2333eqtr4rd 2481 . . . . . . . . 9  |-  ( ph  ->  ( `' G "
( _V  \  1o ) )  =  ( O " U. dom  O ) )
235 isores3 6021 . . . . . . . . 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 1218 . . . . . . . 8  |-  ( ph  ->  ( O  |`  U. dom  O )  Isom  _E  ,  _E  ( U. dom  O , 
( `' G "
( _V  \  1o ) ) ) )
237 cantnfp1OLD.k . . . . . . . . . . 11  |-  K  = OrdIso
(  _E  ,  ( `' G " ( _V 
\  1o ) ) )
2381, 2, 3, 237, 5cantnfclOLD 7897 . . . . . . . . . 10  |-  ( ph  ->  (  _E  We  ( `' G " ( _V 
\  1o ) )  /\  dom  K  e. 
om ) )
239238simpld 459 . . . . . . . . 9  |-  ( ph  ->  _E  We  ( `' G " ( _V 
\  1o ) ) )
240 epse 4698 . . . . . . . . 9  |-  _E Se  ( `' G " ( _V 
\  1o ) )
241237oieu 7745 . . . . . . . . 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 662 . . . . . . . 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 912 . . . . . . 7  |-  ( ph  ->  ( U. dom  O  =  dom  K  /\  ( O  |`  U. dom  O
)  =  K ) )
244243simpld 459 . . . . . 6  |-  ( ph  ->  U. dom  O  =  dom  K )
245244fveq2d 5690 . . . . 5  |-  ( ph  ->  ( M `  U. dom  O )  =  ( M `  dom  K
) )
246 eleq1 2498 . . . . . . . . . 10  |-  ( x  =  (/)  ->  ( x  e.  dom  O  <->  (/)  e.  dom  O ) )
247 fveq2 5686 . . . . . . . . . . 11  |-  ( x  =  (/)  ->  ( H `
 x )  =  ( H `  (/) ) )
248 fveq2 5686 . . . . . . . . . . . 12  |-  ( x  =  (/)  ->  ( M `
 x )  =  ( M `  (/) ) )
249 0ex 4417 . . . . . . . . . . . . 13  |-  (/)  e.  _V
250 cantnfp1OLD.m . . . . . . . . . . . . . 14  |-  M  = seq𝜔 ( ( k  e.  _V ,  z  e.  _V  |->  ( ( ( A  ^o  ( K `  k ) )  .o  ( G `  ( K `  k )
) )  +o  z
) ) ,  (/) )
251250seqom0g 6903 . . . . . . . . . . . . 13  |-  ( (/)  e.  _V  ->  ( M `  (/) )  =  (/) )
252249, 251ax-mp 5 . . . . . . . . . . . 12  |-  ( M `
 (/) )  =  (/)
253248, 252syl6eq 2486 . . . . . . . . . . 11  |-  ( x  =  (/)  ->  ( M `
 x )  =  (/) )
254247, 253eqeq12d 2452 . . . . . . . . . 10  |-  ( x  =  (/)  ->  ( ( H `  x )  =  ( M `  x )  <->  ( H `  (/) )  =  (/) ) )
255246, 254imbi12d 320 . . . . . . . . 9  |-  ( x  =  (/)  ->  ( ( x  e.  dom  O  ->  ( H `  x
)  =  ( M `
 x ) )  <-> 
( (/)  e.  dom  O  ->  ( H `  (/) )  =  (/) ) ) )
256255imbi2d 316 . . . . . . . 8  |-  ( x  =  (/)  ->  ( (
ph  ->  ( x  e. 
dom  O  ->  ( H `
 x )  =  ( M `  x
) ) )  <->  ( ph  ->  ( (/)  e.  dom  O  ->  ( H `  (/) )  =  (/) ) ) ) )
257 eleq1 2498 . . . . . . . . . 10  |-  ( x  =  y  ->  (
x  e.  dom  O  <->  y  e.  dom  O ) )
258 fveq2 5686 . . . . . . . . . . 11  |-  ( x  =  y  ->  ( H `  x )  =  ( H `  y ) )
259 fveq2 5686 . . . . . . . . . . 11  |-  ( x  =  y  ->  ( M `  x )  =  ( M `  y ) )
260258, 259eqeq12d 2452 . . . . . . . . . 10  |-  ( x  =  y  ->  (
( H `  x
)  =  ( M `
 x )  <->  ( H `  y )  =  ( M `  y ) ) )
261257, 260imbi12d 320 . . . . . . . . 9  |-  ( x  =  y  ->  (
( x  e.  dom  O  ->  ( H `  x )  =  ( M `  x ) )  <->  ( y  e. 
dom  O  ->  ( H `
 y )  =  ( M `  y
) ) ) )
262261imbi2d 316 . . . . . . . 8  |-  ( x  =  y  ->  (
( ph  ->  ( x  e.  dom  O  -> 
( H `  x
)  =  ( M `
 x ) ) )  <->  ( ph  ->  ( y  e.  dom  O  ->  ( H `  y
)  =  ( M `
 y ) ) ) ) )
263 eleq1 2498 . . . . . . . . . 10  |-  ( x  =  suc  y  -> 
( x  e.  dom  O  <->  suc  y  e.  dom  O ) )
264 fveq2 5686 . . . . . . . . . . 11  |-  ( x  =  suc  y  -> 
( H `  x
)  =  ( H `
 suc  y )
)
265 fveq2 5686 . . . . . . . . . . 11  |-  ( x  =  suc  y  -> 
( M `  x
)  =  ( M `
 suc  y )
)
266264, 265eqeq12d 2452 . . . . . . . . . 10  |-  ( x  =  suc  y  -> 
( ( H `  x )  =  ( M `  x )  <-> 
( H `  suc  y )  =  ( M `  suc  y
) ) )
267263, 266imbi12d 320 . . . . . . . . 9  |-  ( x  =  suc  y  -> 
( ( x  e. 
dom  O  ->  ( H `
 x )  =  ( M `  x
) )  <->  ( suc  y  e.  dom  O  -> 
( H `  suc  y )  =  ( M `  suc  y
) ) ) )
268267imbi2d 316 . . . . . . . 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 2498 . . . . . . . . . 10  |-  ( x  =  U. dom  O  ->  ( x  e.  dom  O  <->  U. dom  O  e.  dom  O ) )
270 fveq2 5686 . . . . . . . . . . 11  |-  ( x  =  U. dom  O  ->  ( H `  x
)  =  ( H `
 U. dom  O
) )
271 fveq2 5686 . . . . . . . . . . 11  |-  ( x  =  U. dom  O  ->  ( M `  x
)  =  ( M `
 U. dom  O
) )
272270, 271eqeq12d 2452 . . . . . . . . . 10  |-  ( x  =  U. dom  O  ->  ( ( H `  x )  =  ( M `  x )  <-> 
( H `  U. dom  O )  =  ( M `  U. dom  O ) ) )
273269, 272imbi12d 320 . . . . . . . . 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 316 . . . . . . . 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 6903 . . . . . . . . . 10  |-  ( (/)  e.  _V  ->  ( H `  (/) )  =  (/) )
276249, 275mp1i 12 . . . . . . . . 9  |-  ( (/)  e.  dom  O  ->  ( H `  (/) )  =  (/) )
277276a1i 11 . . . . . . . 8  |-  ( ph  ->  ( (/)  e.  dom  O  ->  ( H `  (/) )  =  (/) ) )
278 nnord 6479 . . . . . . . . . . . . . . . 16  |-  ( dom 
O  e.  om  ->  Ord 
dom  O )
27917, 278syl 16 . . . . . . . . . . . . . . 15  |-  ( ph  ->  Ord  dom  O )
280 ordtr 4728 . . . . . . . . . . . . . . 15  |-  ( Ord 
dom  O  ->  Tr  dom  O )
281279, 280syl 16 . . . . . . . . . . . . . 14  |-  ( ph  ->  Tr  dom  O )
282 trsuc 4798 . . . . . . . . . . . . . 14  |-  ( ( Tr  dom  O  /\  suc  y  e.  dom  O )  ->  y  e.  dom  O )
283281, 282sylan 471 . . . . . . . . . . . . 13  |-  ( (
ph  /\  suc  y  e. 
dom  O )  -> 
y  e.  dom  O
)
284283ex 434 . . . . . . . . . . . 12  |-  ( ph  ->  ( suc  y  e. 
dom  O  ->  y  e. 
dom  O ) )
285284imim1d 75 . . . . . . . . . . 11  |-  ( ph  ->  ( ( y  e. 
dom  O  ->  ( H `
 y )  =  ( M `  y
) )  ->  ( suc  y  e.  dom  O  ->  ( H `  y )  =  ( M `  y ) ) ) )
286 oveq2 6094 . . . . . . . . . . . . . 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 6481 . . . . . . . . . . . . . . . . . . 19  |-  ( ( y  e.  dom  O  /\  dom  O  e.  om )  ->  y  e.  om )
288287ancoms 453 . . . . . . . . . . . . . . . . . 18  |-  ( ( dom  O  e.  om  /\  y  e.  dom  O
)  ->  y  e.  om )
28917, 288sylan 471 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  y  e.  dom  O )  ->  y  e.  om )
290283, 289syldan 470 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  suc  y  e. 
dom  O )  -> 
y  e.  om )
2911, 2, 3, 4, 10, 11cantnfsucOLD 7900 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  y  e.  om )  ->  ( H `  suc  y )  =  ( ( ( A  ^o  ( O `  y ) )  .o  ( F `  ( O `  y )
) )  +o  ( H `  y )
) )
292290, 291syldan 470 . . . . . . . . . . . . . . 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, 250cantnfsucOLD 7900 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  y  e.  om )  ->  ( M `  suc  y )  =  ( ( ( A  ^o  ( K `  y ) )  .o  ( G `  ( K `  y )
) )  +o  ( M `  y )
) )
294290, 293syldan 470 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  suc  y  e. 
dom  O )  -> 
( M `  suc  y )  =  ( ( ( A  ^o  ( K `  y ) )  .o  ( G `
 ( K `  y ) ) )  +o  ( M `  y ) ) )
295243simprd 463 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( O  |`  U. dom  O )  =  K )
296295fveq1d 5688 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( ( O  |`  U.
dom  O ) `  y )  =  ( K `  y ) )
297296adantr 465 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  suc  y  e. 
dom  O )  -> 
( ( O  |`  U.
dom  O ) `  y )  =  ( K `  y ) )
29814eleq2d 2505 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( suc  y  e. 
dom  O  <->  suc  y  e.  suc  U.
dom  O ) )
299298biimpa 484 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  suc  y  e. 
dom  O )  ->  suc  y  e.  suc  U.
dom  O )
300160adantr 465 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  suc  y  e. 
dom  O )  ->  Ord  U. dom  O )
301 ordsucelsuc 6428 . . . . . . . . . . . . . . . . . . . . . . 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 232 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  suc  y  e. 
dom  O )  -> 
y  e.  U. dom  O )
304 fvres 5699 . . . . . . . . . . . . . . . . . . . . 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 2472 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  suc  y  e. 
dom  O )  -> 
( K `  y
)  =  ( O `
 y ) )
307306oveq2d 6102 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  suc  y  e. 
dom  O )  -> 
( A  ^o  ( K `  y )
)  =  ( A  ^o  ( O `  y ) ) )
308 cnvimass 5184 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( `' G " ( _V 
\  1o ) ) 
C_  dom  G
309 fdm 5558 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( G : B --> A  ->  dom  G  =  B )
31027, 309syl 16 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  dom  G  =  B )
311308, 310syl5sseq 3399 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( `' G "
( _V  \  1o ) )  C_  B
)
312311adantr 465 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  suc  y  e. 
dom  O )  -> 
( `' G "
( _V  \  1o ) )  C_  B
)
313244adantr 465 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  suc  y  e. 
dom  O )  ->  U. dom  O  =  dom  K )
314303, 313eleqtrd 2514 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  suc  y  e. 
dom  O )  -> 
y  e.  dom  K
)
315237oif 7736 . . . . . . . . . . . . . . . . . . . . . . 23  |-  K : dom  K --> ( `' G " ( _V  \  1o ) )
316315ffvelrni 5837 . . . . . . . . . . . . . . . . . . . . . 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 3352 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  suc  y  e. 
dom  O )  -> 
( K `  y
)  e.  B )
3197adantr 465 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  suc  y  e. 
dom  O )  ->  Y  e.  A )
320 fvex 5696 . . . . . . . . . . . . . . . . . . . . 21  |-  ( G `
 ( K `  y ) )  e. 
_V
321 ifexg 3854 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( Y  e.  A  /\  ( G `  ( K `
 y ) )  e.  _V )  ->  if ( ( K `  y )  =  X ,  Y ,  ( G `  ( K `
 y ) ) )  e.  _V )
322319, 320, 321sylancl 662 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  suc  y  e. 
dom  O )  ->  if ( ( K `  y )  =  X ,  Y ,  ( G `  ( K `
 y ) ) )  e.  _V )
323 eqeq1 2444 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( t  =  ( K `  y )  ->  (
t  =  X  <->  ( K `  y )  =  X ) )
324 fveq2 5686 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( t  =  ( K `  y )  ->  ( G `  t )  =  ( G `  ( K `  y ) ) )
325323, 324ifbieq2d 3809 . . . . . . . . . . . . . . . . . . . . 21  |-  ( t  =  ( K `  y )  ->  if ( t  =  X ,  Y ,  ( G `  t ) )  =  if ( ( K `  y
)  =  X ,  Y ,  ( G `  ( K `  y
) ) ) )
326325, 9fvmptg 5767 . . . . . . . . . . . . . . . . . . . 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 661 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  suc  y  e. 
dom  O )  -> 
( F `  ( K `  y )
)  =  if ( ( K `  y
)  =  X ,  Y ,  ( G `  ( K `  y
) ) ) )
328306fveq2d 5690 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  suc  y  e. 
dom  O )  -> 
( F `  ( K `  y )
)  =  ( F `
 ( O `  y ) ) )
329192adantr 465 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  suc  y  e. 
dom  O )  ->  -.  X  e.  ( `' G " ( _V 
\  1o ) ) )
330 nelneq 2536 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( K `  y
)  e.  ( `' G " ( _V 
\  1o ) )  /\  -.  X  e.  ( `' G "
( _V  \  1o ) ) )  ->  -.  ( K `  y
)  =  X )
331317, 329, 330syl2anc 661 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  suc  y  e. 
dom  O )  ->  -.  ( K `  y
)  =  X )
332 iffalse 3794 . . . . . . . . . . . . . . . . . . . 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 2479 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  suc  y  e. 
dom  O )  -> 
( G `  ( K `  y )
)  =  ( F `
 ( O `  y ) ) )
335307, 334oveq12d 6104 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  suc  y  e. 
dom  O )  -> 
( ( A  ^o  ( K `  y ) )  .o  ( G `
 ( K `  y ) ) )  =  ( ( A  ^o  ( O `  y ) )  .o  ( F `  ( O `  y )
) ) )
336335oveq1d 6101 . . . . . . . . . . . . . . . 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 2470 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  suc  y  e. 
dom  O )  -> 
( M `  suc  y )  =  ( ( ( A  ^o  ( O `  y ) )  .o  ( F `
 ( O `  y ) ) )  +o  ( M `  y ) ) )
338292, 337eqeq12d 2452 . . . . . . . . . . . . . 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 221 . . . . . . . . . . . . 13  |-  ( (
ph  /\  suc  y  e. 
dom  O )  -> 
( ( H `  y )  =  ( M `  y )  ->  ( H `  suc  y )  =  ( M `  suc  y
) ) )
340339ex 434 . . . . . . . . . . . 12  |-  ( ph  ->  ( suc  y  e. 
dom  O  ->  ( ( H `  y )  =  ( M `  y )  ->  ( H `  suc  y )  =  ( M `  suc  y ) ) ) )
341340a2d 26 . . . . . . . . . . 11  |-  ( ph  ->  ( ( suc  y  e.  dom  O  ->  ( H `  y )  =  ( M `  y ) )  -> 
( suc  y  e.  dom  O  ->  ( H `  suc  y )  =  ( M `  suc  y ) ) ) )
342285, 341syld 44 . . . . . . . . . 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 6497 . . . . . . 7  |-  ( U. dom  O  e.  om  ->  (
ph  ->  ( U. dom  O  e.  dom  O  -> 
( H `  U. dom  O )  =  ( M `  U. dom  O ) ) ) )
34620, 345mpcom 36 . . . . . 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, 250cantnfvalOLD 7898 . . . . 5  |-  ( ph  ->  ( ( A CNF  B
) `  G )  =  ( M `  dom  K ) )
349245, 347, 3483eqtr4d 2480 . . . 4  |-  ( ph  ->  ( H `  U. dom  O )  =  ( ( A CNF  B ) `
 G ) )
350158, 349oveq12d 6104 . . 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 2470 . 2  |-  ( ph  ->  ( H `  suc  U.
dom  O )  =  ( ( ( A  ^o  X )  .o  Y )  +o  (
( A CNF  B ) `
 G ) ) )
35212, 15, 3513eqtrd 2474 1  |-  ( ph  ->  ( ( A CNF  B
) `  F )  =  ( ( ( A  ^o  X )  .o  Y )  +o  ( ( A CNF  B
) `  G )
) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    \/ wo 368    /\ wa 369    = wceq 1369    e. wcel 1756    =/= wne 2601   _Vcvv 2967    \ cdif 3320    u. cun 3321    i^i cin 3322    C_ wss 3323   (/)c0 3632   ifcif 3786   {csn 3872   U.cuni 4086   class class class wbr 4287    e. cmpt 4345   Tr wtr 4380    _E cep 4625   Se wse 4672    We wwe 4673   Ord word 4713   Oncon0 4714   suc csuc 4716   `'ccnv 4834   dom cdm 4835    |` cres 4837   "cima 4838   Fun wfun 5407    Fn wfn 5408   -->wf 5409   -onto->wfo 5411   -1-1-onto->wf1o 5412   ` cfv 5413    Isom wiso 5414  (class class class)co 6086    e. cmpt2 6088   omcom 6471  seq𝜔cseqom 6894   1oc1o 6905    +o coa 6909    .o comu 6910    ^o coe 6911   Fincfn 7302  OrdIsocoi 7715   CNF ccnf 7859
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-rep 4398  ax-sep 4408  ax-nul 4416  ax-pow 4465  ax-pr 4526  ax-un 6367
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-fal 1375  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2256  df-mo 2257  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2715  df-rex 2716  df-reu 2717  df-rmo 2718  df-rab 2719  df-v 2969  df-sbc 3182  df-csb 3284  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-pss 3339  df-nul 3633  df-if 3787  df-pw 3857  df-sn 3873  df-pr 3875  df-tp 3877  df-op 3879  df-uni 4087  df-int 4124  df-iun 4168  df-br 4288  df-opab 4346  df-mpt 4347  df-tr 4381  df-eprel 4627  df-id 4631  df-po 4636  df-so 4637  df-fr 4674  df-se 4675  df-we 4676  df-ord 4717  df-on 4718  df-lim 4719  df-suc 4720  df-xp 4841  df-rel 4842  df-cnv 4843  df-co 4844  df-dm 4845  df-rn 4846  df-res 4847  df-ima 4848  df-iota 5376  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-isom 5422  df-riota 6047  df-ov 6089  df-oprab 6090  df-mpt2 6091  df-om 6472  df-1st 6572  df-2nd 6573  df-supp 6686  df-recs 6824  df-rdg 6858  df-seqom 6895  df-1o 6912  df-oadd 6916  df-er 7093  df-map 7208  df-en 7303  df-dom 7304  df-sdom 7305  df-fin 7306  df-fsupp 7613  df-oi 7716  df-cnf 7860
This theorem is referenced by:  cantnfp1OLD  7907
  Copyright terms: Public domain W3C validator