HomeHome Metamath Proof Explorer
Theorem List (p. 332 of 370)
< Previous  Next >
Browser slow? Try the
Unicode version.

Mirrors  >  Metamath Home Page  >  MPE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Color key:    Metamath Proof Explorer  Metamath Proof Explorer
(1-25511)
  Hilbert Space Explorer  Hilbert Space Explorer
(25512-27036)
  Users' Mathboxes  Users' Mathboxes
(27037-36923)
 

Theorem List for Metamath Proof Explorer - 33101-33200   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theorembnj1021 33101* Technical lemma for bnj69 33145. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
 |-  ( ph 
 <->  ( f `  (/) )  = 
 pred ( X ,  A ,  R )
 )   &    |-  ( ps  <->  A. i  e.  om  ( suc  i  e.  n  ->  ( f `  suc  i )  =  U_ y  e.  ( f `  i
 )  pred ( y ,  A ,  R ) ) )   &    |-  ( ch  <->  ( n  e.  D  /\  f  Fn  n  /\  ph  /\  ps ) )   &    |-  ( th  <->  ( R  FrSe  A 
 /\  X  e.  A  /\  y  e.  trCl ( X ,  A ,  R )  /\  z  e. 
 pred ( y ,  A ,  R ) ) )   &    |-  ( ta  <->  ( m  e. 
 om  /\  n  =  suc  m  /\  p  = 
 suc  n ) )   &    |-  ( et  <->  ( i  e.  n  /\  y  e.  ( f `  i
 ) ) )   &    |-  D  =  ( om  \  { (/)
 } )   &    |-  B  =  {
 f  |  E. n  e.  D  ( f  Fn  n  /\  ph  /\  ps ) }   =>    |- 
 E. f E. n E. i E. m ( th  ->  ( th  /\ 
 ch  /\  et  /\  E. p ta ) )
 
Theorembnj907 33102* Technical lemma for bnj69 33145. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
 |-  ( ph 
 <->  ( f `  (/) )  = 
 pred ( X ,  A ,  R )
 )   &    |-  ( ps  <->  A. i  e.  om  ( suc  i  e.  n  ->  ( f `  suc  i )  =  U_ y  e.  ( f `  i
 )  pred ( y ,  A ,  R ) ) )   &    |-  ( ch  <->  ( n  e.  D  /\  f  Fn  n  /\  ph  /\  ps ) )   &    |-  ( th  <->  ( R  FrSe  A 
 /\  X  e.  A  /\  y  e.  trCl ( X ,  A ,  R )  /\  z  e. 
 pred ( y ,  A ,  R ) ) )   &    |-  ( ta  <->  ( m  e. 
 om  /\  n  =  suc  m  /\  p  = 
 suc  n ) )   &    |-  ( et  <->  ( i  e.  n  /\  y  e.  ( f `  i
 ) ) )   &    |-  ( ph'  <->  [. p  /  n ]. ph )   &    |-  ( ps'  <->  [. p  /  n ].
 ps )   &    |-  ( ch'  <->  [. p  /  n ].
 ch )   &    |-  ( ph"  <->  [. G  /  f ]. ph' )   &    |-  ( ps"  <->  [. G  /  f ]. ps' )   &    |-  ( ch"  <->  [. G  /  f ]. ch' )   &    |-  D  =  ( om  \  { (/) } )   &    |-  B  =  { f  |  E. n  e.  D  (
 f  Fn  n  /\  ph 
 /\  ps ) }   &    |-  C  =  U_ y  e.  (
 f `  m )  pred ( y ,  A ,  R )   &    |-  G  =  ( f  u.  { <. n ,  C >. } )   =>    |-  (
 ( R  FrSe  A  /\  X  e.  A )  -> 
 TrFo (  trCl ( X ,  A ,  R ) ,  A ,  R ) )
 
Theorembnj1029 33103 Property of  trCl. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
 |-  (
 ( R  FrSe  A  /\  X  e.  A )  -> 
 TrFo (  trCl ( X ,  A ,  R ) ,  A ,  R ) )
 
Theorembnj1033 33104* Technical lemma for bnj69 33145. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
 |-  ( ph 
 <->  ( f `  (/) )  = 
 pred ( X ,  A ,  R )
 )   &    |-  ( ps  <->  A. i  e.  om  ( suc  i  e.  n  ->  ( f `  suc  i )  =  U_ y  e.  ( f `  i
 )  pred ( y ,  A ,  R ) ) )   &    |-  ( ch  <->  ( n  e.  D  /\  f  Fn  n  /\  ph  /\  ps ) )   &    |-  ( th  <->  ( R  FrSe  A 
 /\  X  e.  A ) )   &    |-  ( ta  <->  ( B  e.  _V 
 /\  TrFo ( B ,  A ,  R )  /\  pred ( X ,  A ,  R )  C_  B ) )   &    |-  ( et 
 <->  z  e.  trCl ( X ,  A ,  R ) )   &    |-  ( ze 
 <->  ( i  e.  n  /\  z  e.  (
 f `  i )
 ) )   &    |-  D  =  ( om  \  { (/) } )   &    |-  K  =  { f  |  E. n  e.  D  (
 f  Fn  n  /\  ph 
 /\  ps ) }   &    |-  ( E. f E. n E. i ( th  /\  ta 
 /\  ch  /\  ze )  ->  z  e.  B )   =>    |-  ( ( th  /\  ta )  ->  trCl ( X ,  A ,  R )  C_  B )
 
Theorembnj1034 33105* Technical lemma for bnj69 33145. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
 |-  ( ph 
 <->  ( f `  (/) )  = 
 pred ( X ,  A ,  R )
 )   &    |-  ( ps  <->  A. i  e.  om  ( suc  i  e.  n  ->  ( f `  suc  i )  =  U_ y  e.  ( f `  i
 )  pred ( y ,  A ,  R ) ) )   &    |-  ( ch  <->  ( n  e.  D  /\  f  Fn  n  /\  ph  /\  ps ) )   &    |-  ( th  <->  ( R  FrSe  A 
 /\  X  e.  A ) )   &    |-  ( ta  <->  ( B  e.  _V 
 /\  TrFo ( B ,  A ,  R )  /\  pred ( X ,  A ,  R )  C_  B ) )   &    |-  ( ze 
 <->  ( i  e.  n  /\  z  e.  (
 f `  i )
 ) )   &    |-  D  =  ( om  \  { (/) } )   &    |-  K  =  { f  |  E. n  e.  D  (
 f  Fn  n  /\  ph 
 /\  ps ) }   &    |-  ( E. f E. n E. i ( th  /\  ta 
 /\  ch  /\  ze )  ->  z  e.  B )   =>    |-  ( ( th  /\  ta )  ->  trCl ( X ,  A ,  R )  C_  B )
 
Theorembnj1039 33106 Technical lemma for bnj69 33145. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
 |-  ( ps 
 <-> 
 A. i  e.  om  ( suc  i  e.  n  ->  ( f `  suc  i )  =  U_ y  e.  ( f `  i
 )  pred ( y ,  A ,  R ) ) )   &    |-  ( ps'  <->  [. j  /  i ]. ps )   =>    |-  ( ps'  <->  A. i  e.  om  ( suc  i  e.  n  ->  ( f `  suc  i )  =  U_ y  e.  ( f `  i
 )  pred ( y ,  A ,  R ) ) )
 
Theorembnj1040 33107* Technical lemma for bnj69 33145. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
 |-  ( ph'  <->  [. j  /  i ]. ph )   &    |-  ( ps'  <->  [. j  /  i ]. ps )   &    |-  ( ch  <->  ( n  e.  D  /\  f  Fn  n  /\  ph  /\  ps ) )   &    |-  ( ch'  <->  [. j  /  i ]. ch )   =>    |-  ( ch'  <->  ( n  e.  D  /\  f  Fn  n  /\  ph'  /\  ps' ) )
 
Theorembnj1047 33108 Technical lemma for bnj69 33145. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
 |-  ( rh 
 <-> 
 A. j  e.  n  ( j  _E  i  -> 
 [. j  /  i ]. et ) )   &    |-  ( et'  <->  [. j  /  i ]. et )   =>    |-  ( rh  <->  A. j  e.  n  ( j  _E  i  ->  et' ) )
 
Theorembnj1049 33109 Technical lemma for bnj69 33145. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
 |-  ( ze 
 <->  ( i  e.  n  /\  z  e.  (
 f `  i )
 ) )   &    |-  ( et  <->  ( ( th  /\ 
 ta  /\  ch  /\  ze )  ->  z  e.  B ) )   =>    |-  ( A. i  e.  n  et  <->  A. i et )
 
Theorembnj1052 33110* Technical lemma for bnj69 33145. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
 |-  ( ph 
 <->  ( f `  (/) )  = 
 pred ( X ,  A ,  R )
 )   &    |-  ( ps  <->  A. i  e.  om  ( suc  i  e.  n  ->  ( f `  suc  i )  =  U_ y  e.  ( f `  i
 )  pred ( y ,  A ,  R ) ) )   &    |-  ( ch  <->  ( n  e.  D  /\  f  Fn  n  /\  ph  /\  ps ) )   &    |-  ( th  <->  ( R  FrSe  A 
 /\  X  e.  A ) )   &    |-  ( ta  <->  ( B  e.  _V 
 /\  TrFo ( B ,  A ,  R )  /\  pred ( X ,  A ,  R )  C_  B ) )   &    |-  ( ze 
 <->  ( i  e.  n  /\  z  e.  (
 f `  i )
 ) )   &    |-  D  =  ( om  \  { (/) } )   &    |-  K  =  { f  |  E. n  e.  D  (
 f  Fn  n  /\  ph 
 /\  ps ) }   &    |-  ( et 
 <->  ( ( th  /\  ta 
 /\  ch  /\  ze )  ->  z  e.  B ) )   &    |-  ( rh  <->  A. j  e.  n  ( j  _E  i  -> 
 [. j  /  i ]. et ) )   &    |-  (
 ( th  /\  ta  /\  ch 
 /\  ze )  ->  (  _E  Fr  n  /\  A. i  e.  n  ( rh  ->  et ) ) )   =>    |-  ( ( th  /\  ta )  ->  trCl ( X ,  A ,  R )  C_  B )
 
Theorembnj1053 33111* Technical lemma for bnj69 33145. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
 |-  ( ph 
 <->  ( f `  (/) )  = 
 pred ( X ,  A ,  R )
 )   &    |-  ( ps  <->  A. i  e.  om  ( suc  i  e.  n  ->  ( f `  suc  i )  =  U_ y  e.  ( f `  i
 )  pred ( y ,  A ,  R ) ) )   &    |-  ( ch  <->  ( n  e.  D  /\  f  Fn  n  /\  ph  /\  ps ) )   &    |-  ( th  <->  ( R  FrSe  A 
 /\  X  e.  A ) )   &    |-  ( ta  <->  ( B  e.  _V 
 /\  TrFo ( B ,  A ,  R )  /\  pred ( X ,  A ,  R )  C_  B ) )   &    |-  ( ze 
 <->  ( i  e.  n  /\  z  e.  (
 f `  i )
 ) )   &    |-  D  =  ( om  \  { (/) } )   &    |-  K  =  { f  |  E. n  e.  D  (
 f  Fn  n  /\  ph 
 /\  ps ) }   &    |-  ( et 
 <->  ( ( th  /\  ta 
 /\  ch  /\  ze )  ->  z  e.  B ) )   &    |-  ( rh  <->  A. j  e.  n  ( j  _E  i  -> 
 [. j  /  i ]. et ) )   &    |-  (
 ( th  /\  ta  /\  ch 
 /\  ze )  ->  A. i  e.  n  ( rh  ->  et ) )   =>    |-  ( ( th  /\ 
 ta )  ->  trCl ( X ,  A ,  R )  C_  B )
 
Theorembnj1071 33112 Technical lemma for bnj69 33145. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
 |-  D  =  ( om  \  { (/)
 } )   =>    |-  ( n  e.  D  ->  _E  Fr  n )
 
Theorembnj1083 33113 Technical lemma for bnj69 33145. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
 |-  ( ch 
 <->  ( n  e.  D  /\  f  Fn  n  /\  ph  /\  ps )
 )   &    |-  K  =  { f  |  E. n  e.  D  ( f  Fn  n  /\  ph  /\  ps ) }   =>    |-  ( f  e.  K  <->  E. n ch )
 
Theorembnj1090 33114* Technical lemma for bnj69 33145. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
 |-  ( et 
 <->  ( ( f  e.  K  /\  i  e. 
 dom  f )  ->  ( f `  i
 )  C_  B )
 )   &    |-  ( rh  <->  A. j  e.  n  ( j  _E  i  -> 
 [. j  /  i ]. et ) )   &    |-  ( et'  <->  [. j  /  i ]. et )   &    |-  ( si  <->  ( ( j  e.  n  /\  j  _E  i )  ->  et' ) )   &    |-  ( ph0  <->  ( i  e.  n  /\  si  /\  f  e.  K  /\  i  e.  dom  f ) )   &    |-  ( ( th  /\ 
 ta  /\  ch  /\  ze )  ->  A. i E. j
 ( ph0  ->  ( f `  i )  C_  B ) )   =>    |-  ( ( th  /\  ta 
 /\  ch  /\  ze )  ->  A. i  e.  n  ( rh  ->  et )
 )
 
Theorembnj1093 33115* Technical lemma for bnj69 33145. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
 |-  E. j
 ( ( ( th  /\ 
 ta  /\  ch )  /\  ph0 )  ->  (
 f `  i )  C_  B )   &    |-  ( ps  <->  A. i  e.  om  ( suc  i  e.  n  ->  ( f `  suc  i )  =  U_ y  e.  ( f `  i
 )  pred ( y ,  A ,  R ) ) )   &    |-  ( ch  <->  ( n  e.  D  /\  f  Fn  n  /\  ph  /\  ps ) )   =>    |-  ( ( th  /\  ta 
 /\  ch  /\  ze )  ->  A. i E. j
 ( ph0  ->  ( f `  i )  C_  B ) )
 
Theorembnj1097 33116 Technical lemma for bnj69 33145. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
 |-  ( ph 
 <->  ( f `  (/) )  = 
 pred ( X ,  A ,  R )
 )   &    |-  ( ch  <->  ( n  e.  D  /\  f  Fn  n  /\  ph  /\  ps ) )   &    |-  ( ta  <->  ( B  e.  _V 
 /\  TrFo ( B ,  A ,  R )  /\  pred ( X ,  A ,  R )  C_  B ) )   =>    |-  ( ( i  =  (/)  /\  ( ( th  /\  ta  /\  ch )  /\  ph0 ) )  ->  ( f `  i
 )  C_  B )
 
Theorembnj1110 33117* Technical lemma for bnj69 33145. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
 |-  ( ch 
 <->  ( n  e.  D  /\  f  Fn  n  /\  ph  /\  ps )
 )   &    |-  D  =  ( om  \  { (/) } )   &    |-  ( si 
 <->  ( ( j  e.  n  /\  j  _E  i )  ->  et' ) )   &    |-  ( ph0  <->  ( i  e.  n  /\  si  /\  f  e.  K  /\  i  e.  dom  f ) )   &    |-  ( et'  <->  ( ( f  e.  K  /\  j  e.  dom  f )  ->  ( f `  j
 )  C_  B )
 )   =>    |- 
 E. j ( ( i  =/=  (/)  /\  (
 ( th  /\  ta  /\  ch )  /\  ph0 ) ) 
 ->  ( j  e.  n  /\  i  =  suc  j  /\  ( f `  j )  C_  B ) )
 
Theorembnj1112 33118* Technical lemma for bnj69 33145. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
 |-  ( ps 
 <-> 
 A. i  e.  om  ( suc  i  e.  n  ->  ( f `  suc  i )  =  U_ y  e.  ( f `  i
 )  pred ( y ,  A ,  R ) ) )   =>    |-  ( ps  <->  A. j ( ( j  e.  om  /\  suc  j  e.  n ) 
 ->  ( f `  suc  j )  =  U_ y  e.  ( f `  j
 )  pred ( y ,  A ,  R ) ) )
 
Theorembnj1118 33119* Technical lemma for bnj69 33145. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
 |-  ( ps 
 <-> 
 A. i  e.  om  ( suc  i  e.  n  ->  ( f `  suc  i )  =  U_ y  e.  ( f `  i
 )  pred ( y ,  A ,  R ) ) )   &    |-  ( ch  <->  ( n  e.  D  /\  f  Fn  n  /\  ph  /\  ps ) )   &    |-  ( ta  <->  ( B  e.  _V 
 /\  TrFo ( B ,  A ,  R )  /\  pred ( X ,  A ,  R )  C_  B ) )   &    |-  D  =  ( om  \  { (/)
 } )   &    |-  ( si  <->  ( ( j  e.  n  /\  j  _E  i )  ->  et' ) )   &    |-  ( ph0  <->  ( i  e.  n  /\  si  /\  f  e.  K  /\  i  e.  dom  f ) )   &    |-  ( et'  <->  ( ( f  e.  K  /\  j  e.  dom  f )  ->  ( f `  j
 )  C_  B )
 )   =>    |- 
 E. j ( ( i  =/=  (/)  /\  (
 ( th  /\  ta  /\  ch )  /\  ph0 ) ) 
 ->  ( f `  i
 )  C_  B )
 
Theorembnj1121 33120 Technical lemma for bnj69 33145. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
 |-  ( th 
 <->  ( R  FrSe  A  /\  X  e.  A )
 )   &    |-  ( ta  <->  ( B  e.  _V 
 /\  TrFo ( B ,  A ,  R )  /\  pred ( X ,  A ,  R )  C_  B ) )   &    |-  ( ch 
 <->  ( n  e.  D  /\  f  Fn  n  /\  ph  /\  ps )
 )   &    |-  ( ze  <->  ( i  e.  n  /\  z  e.  ( f `  i
 ) ) )   &    |-  ( et 
 <->  ( ( f  e.  K  /\  i  e. 
 dom  f )  ->  ( f `  i
 )  C_  B )
 )   &    |-  ( ( th  /\  ta 
 /\  ch  /\  ze )  ->  A. i  e.  n  et )   &    |-  K  =  {
 f  |  E. n  e.  D  ( f  Fn  n  /\  ph  /\  ps ) }   =>    |-  ( ( th  /\  ta 
 /\  ch  /\  ze )  ->  z  e.  B )
 
Theorembnj1123 33121* Technical lemma for bnj69 33145. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
 |-  ( ps 
 <-> 
 A. i  e.  om  ( suc  i  e.  n  ->  ( f `  suc  i )  =  U_ y  e.  ( f `  i
 )  pred ( y ,  A ,  R ) ) )   &    |-  K  =  {
 f  |  E. n  e.  D  ( f  Fn  n  /\  ph  /\  ps ) }   &    |-  ( et  <->  ( ( f  e.  K  /\  i  e.  dom  f )  ->  ( f `  i
 )  C_  B )
 )   &    |-  ( et'  <->  [. j  /  i ]. et )   =>    |-  ( et'  <->  ( ( f  e.  K  /\  j  e.  dom  f )  ->  ( f `  j
 )  C_  B )
 )
 
Theorembnj1030 33122* Technical lemma for bnj69 33145. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
 |-  ( ph 
 <->  ( f `  (/) )  = 
 pred ( X ,  A ,  R )
 )   &    |-  ( ps  <->  A. i  e.  om  ( suc  i  e.  n  ->  ( f `  suc  i )  =  U_ y  e.  ( f `  i
 )  pred ( y ,  A ,  R ) ) )   &    |-  ( ch  <->  ( n  e.  D  /\  f  Fn  n  /\  ph  /\  ps ) )   &    |-  ( th  <->  ( R  FrSe  A 
 /\  X  e.  A ) )   &    |-  ( ta  <->  ( B  e.  _V 
 /\  TrFo ( B ,  A ,  R )  /\  pred ( X ,  A ,  R )  C_  B ) )   &    |-  ( ze 
 <->  ( i  e.  n  /\  z  e.  (
 f `  i )
 ) )   &    |-  D  =  ( om  \  { (/) } )   &    |-  K  =  { f  |  E. n  e.  D  (
 f  Fn  n  /\  ph 
 /\  ps ) }   &    |-  ( et 
 <->  ( ( f  e.  K  /\  i  e. 
 dom  f )  ->  ( f `  i
 )  C_  B )
 )   &    |-  ( rh  <->  A. j  e.  n  ( j  _E  i  -> 
 [. j  /  i ]. et ) )   &    |-  ( ph'  <->  [. j  /  i ]. ph )   &    |-  ( ps'  <->  [. j  /  i ]. ps )   &    |-  ( ch'  <->  [. j  /  i ]. ch )   &    |-  ( th'  <->  [. j  /  i ]. th )   &    |-  ( ta'  <->  [. j  /  i ]. ta )   &    |-  ( ze'  <->  [. j  /  i ]. ze )   &    |-  ( et'  <->  [. j  /  i ]. et )   &    |-  ( si  <->  ( ( j  e.  n  /\  j  _E  i )  ->  et' ) )   &    |-  ( ph0  <->  ( i  e.  n  /\  si  /\  f  e.  K  /\  i  e.  dom  f ) )   =>    |-  ( ( th  /\  ta )  ->  trCl ( X ,  A ,  R )  C_  B )
 
Theorembnj1124 33123 Property of  trCl. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
 |-  ( th 
 <->  ( R  FrSe  A  /\  X  e.  A )
 )   &    |-  ( ta  <->  ( B  e.  _V 
 /\  TrFo ( B ,  A ,  R )  /\  pred ( X ,  A ,  R )  C_  B ) )   =>    |-  ( ( th  /\ 
 ta )  ->  trCl ( X ,  A ,  R )  C_  B )
 
Theorembnj1133 33124* Technical lemma for bnj69 33145. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
 |-  D  =  ( om  \  { (/)
 } )   &    |-  ( ch  <->  ( n  e.  D  /\  f  Fn  n  /\  ph  /\  ps ) )   &    |-  ( ta  <->  A. j  e.  n  ( j  _E  i  -> 
 [. j  /  i ]. th ) )   &    |-  (
 ( i  e.  n  /\  ta )  ->  th )   =>    |-  ( ch  ->  A. i  e.  n  th )
 
Theorembnj1128 33125* Technical lemma for bnj69 33145. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
 |-  ( ph 
 <->  ( f `  (/) )  = 
 pred ( X ,  A ,  R )
 )   &    |-  ( ps  <->  A. i  e.  om  ( suc  i  e.  n  ->  ( f `  suc  i )  =  U_ y  e.  ( f `  i
 )  pred ( y ,  A ,  R ) ) )   &    |-  D  =  ( om  \  { (/) } )   &    |-  B  =  { f  |  E. n  e.  D  (
 f  Fn  n  /\  ph 
 /\  ps ) }   &    |-  ( ch 
 <->  ( n  e.  D  /\  f  Fn  n  /\  ph  /\  ps )
 )   &    |-  ( th  <->  ( ch  ->  ( f `  i ) 
 C_  A ) )   &    |-  ( ta  <->  A. j  e.  n  ( j  _E  i  -> 
 [. j  /  i ]. th ) )   &    |-  ( ph'  <->  [. j  /  i ]. ph )   &    |-  ( ps'  <->  [. j  /  i ]. ps )   &    |-  ( ch'  <->  [. j  /  i ]. ch )   &    |-  ( th'  <->  [. j  /  i ]. th )   =>    |-  ( Y  e.  trCl ( X ,  A ,  R )  ->  Y  e.  A )
 
Theorembnj1127 33126 Property of  trCl. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
 |-  ( Y  e.  trCl ( X ,  A ,  R )  ->  Y  e.  A )
 
Theorembnj1125 33127 Property of  trCl. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
 |-  (
 ( R  FrSe  A  /\  X  e.  A  /\  Y  e.  trCl ( X ,  A ,  R ) )  ->  trCl ( Y ,  A ,  R )  C_  trCl ( X ,  A ,  R ) )
 
Theorembnj1145 33128* Technical lemma for bnj69 33145. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
 |-  ( ph 
 <->  ( f `  (/) )  = 
 pred ( X ,  A ,  R )
 )   &    |-  ( ps  <->  A. i  e.  om  ( suc  i  e.  n  ->  ( f `  suc  i )  =  U_ y  e.  ( f `  i
 )  pred ( y ,  A ,  R ) ) )   &    |-  D  =  ( om  \  { (/) } )   &    |-  B  =  { f  |  E. n  e.  D  (
 f  Fn  n  /\  ph 
 /\  ps ) }   &    |-  ( ch 
 <->  ( n  e.  D  /\  f  Fn  n  /\  ph  /\  ps )
 )   &    |-  ( th  <->  ( ( i  =/=  (/)  /\  i  e.  n  /\  ch )  /\  ( j  e.  n  /\  i  =  suc  j ) ) )   =>    |-  trCl
 ( X ,  A ,  R )  C_  A
 
Theorembnj1147 33129 Property of  trCl. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
 |-  trCl ( X ,  A ,  R )  C_  A
 
Theorembnj1137 33130* Property of  trCl. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Proof shortened by Mario Carneiro, 22-Dec-2016.) (New usage is discouraged.)
 |-  B  =  (  pred ( X ,  A ,  R )  u.  U_ y  e.  trCl  ( X ,  A ,  R )  trCl ( y ,  A ,  R ) )   =>    |-  ( ( R  FrSe  A 
 /\  X  e.  A )  ->  TrFo ( B ,  A ,  R )
 )
 
Theorembnj1148 33131 Property of  pred. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
 |-  (
 ( R  FrSe  A  /\  X  e.  A )  -> 
 pred ( X ,  A ,  R )  e.  _V )
 
Theorembnj1136 33132* Technical lemma for bnj69 33145. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
 |-  B  =  (  pred ( X ,  A ,  R )  u.  U_ y  e.  trCl  ( X ,  A ,  R )  trCl ( y ,  A ,  R ) )   &    |-  ( th  <->  ( R  FrSe  A 
 /\  X  e.  A ) )   &    |-  ( ta  <->  ( B  e.  _V 
 /\  TrFo ( B ,  A ,  R )  /\  pred ( X ,  A ,  R )  C_  B ) )   =>    |-  ( ( R 
 FrSe  A  /\  X  e.  A )  ->  trCl ( X ,  A ,  R )  =  B )
 
Theorembnj1152 33133 Technical lemma for bnj69 33145. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
 |-  ( Y  e.  pred ( X ,  A ,  R ) 
 <->  ( Y  e.  A  /\  Y R X ) )
 
Theorembnj1154 33134* Property of  Fr. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
 |-  (
 ( R  Fr  A  /\  B  C_  A  /\  B  =/=  (/)  /\  B  e.  _V )  ->  E. x  e.  B  A. y  e.  B  -.  y R x )
 
Theorembnj1171 33135 Technical lemma for bnj69 33145. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
 |-  (
 ( ph  /\  ps )  ->  B  C_  A )   &    |-  E. z A. w ( ( ph  /\ 
 ps )  ->  (
 z  e.  B  /\  ( w  e.  A  ->  ( w R z 
 ->  -.  w  e.  B ) ) ) )   =>    |-  E. z A. w ( ( ph  /\  ps )  ->  ( z  e.  B  /\  ( w  e.  B  ->  -.  w R z ) ) )
 
Theorembnj1172 33136 Technical lemma for bnj69 33145. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
 |-  C  =  (  trCl ( X ,  A ,  R )  i^i  B )   &    |-  E. z A. w ( ( ph  /\ 
 ps )  ->  (
 ( ph  /\  ps  /\  z  e.  C )  /\  ( th  ->  ( w R z  ->  -.  w  e.  B ) ) ) )   &    |-  ( ( ph  /\ 
 ps  /\  z  e.  C )  ->  ( th  <->  w  e.  A ) )   =>    |-  E. z A. w ( ( ph  /\  ps )  ->  ( z  e.  B  /\  ( w  e.  A  ->  ( w R z  ->  -.  w  e.  B ) ) ) )
 
Theorembnj1173 33137 Technical lemma for bnj69 33145. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
 |-  C  =  (  trCl ( X ,  A ,  R )  i^i  B )   &    |-  ( th 
 <->  ( ( R  FrSe  A 
 /\  X  e.  A  /\  z  e.  trCl ( X ,  A ,  R ) )  /\  ( R  FrSe  A  /\  z  e.  A )  /\  w  e.  A ) )   &    |-  ( ( ph  /\ 
 ps )  ->  R  FrSe  A )   &    |-  ( ( ph  /\ 
 ps )  ->  X  e.  A )   =>    |-  ( ( ph  /\  ps  /\  z  e.  C ) 
 ->  ( th  <->  w  e.  A ) )
 
Theorembnj1174 33138 Technical lemma for bnj69 33145. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
 |-  C  =  (  trCl ( X ,  A ,  R )  i^i  B )   &    |-  E. z A. w ( ( ph  /\ 
 ps )  ->  (
 z  e.  C  /\  ( th  ->  ( w R z  ->  -.  w  e.  C ) ) ) )   &    |-  ( th  ->  ( w R z  ->  w  e.  trCl ( X ,  A ,  R ) ) )   =>    |-  E. z A. w ( ( ph  /\ 
 ps )  ->  (
 ( ph  /\  ps  /\  z  e.  C )  /\  ( th  ->  ( w R z  ->  -.  w  e.  B ) ) ) )
 
Theorembnj1175 33139 Technical lemma for bnj69 33145. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
 |-  C  =  (  trCl ( X ,  A ,  R )  i^i  B )   &    |-  ( ch 
 <->  ( ( R  FrSe  A 
 /\  X  e.  A  /\  z  e.  trCl ( X ,  A ,  R ) )  /\  ( R  FrSe  A  /\  z  e.  A )  /\  ( w  e.  A  /\  w R z ) ) )   &    |-  ( th  <->  ( ( R 
 FrSe  A  /\  X  e.  A  /\  z  e.  trCl ( X ,  A ,  R ) )  /\  ( R  FrSe  A  /\  z  e.  A )  /\  w  e.  A ) )   =>    |-  ( th  ->  ( w R z  ->  w  e.  trCl ( X ,  A ,  R )
 ) )
 
Theorembnj1176 33140* Technical lemma for bnj69 33145. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
 |-  (
 ( ph  /\  ps )  ->  ( R  Fr  A  /\  C  C_  A  /\  C  =/=  (/)  /\  C  e.  _V ) )   &    |-  ( ( R  Fr  A  /\  C  C_  A  /\  C  =/=  (/)  /\  C  e.  _V )  ->  E. z  e.  C  A. w  e.  C  -.  w R z )   =>    |-  E. z A. w ( ( ph  /\ 
 ps )  ->  (
 z  e.  C  /\  ( th  ->  ( w R z  ->  -.  w  e.  C ) ) ) )
 
Theorembnj1177 33141 Technical lemma for bnj69 33145. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
 |-  ( ps 
 <->  ( X  e.  B  /\  y  e.  B  /\  y R X ) )   &    |-  C  =  ( 
 trCl ( X ,  A ,  R )  i^i  B )   &    |-  ( ( ph  /\ 
 ps )  ->  R  FrSe  A )   &    |-  ( ( ph  /\ 
 ps )  ->  B  C_  A )   &    |-  ( ( ph  /\ 
 ps )  ->  X  e.  A )   =>    |-  ( ( ph  /\  ps )  ->  ( R  Fr  A  /\  C  C_  A  /\  C  =/=  (/)  /\  C  e.  _V ) )
 
Theorembnj1186 33142* Technical lemma for bnj69 33145. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
 |-  E. z A. w ( ( ph  /\ 
 ps )  ->  (
 z  e.  B  /\  ( w  e.  B  ->  -.  w R z ) ) )   =>    |-  ( ( ph  /\ 
 ps )  ->  E. z  e.  B  A. w  e.  B  -.  w R z )
 
Theorembnj1190 33143* Technical lemma for bnj69 33145. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
 |-  ( ph 
 <->  ( R  FrSe  A  /\  B  C_  A  /\  B  =/= 
 (/) ) )   &    |-  ( ps 
 <->  ( x  e.  B  /\  y  e.  B  /\  y R x ) )   =>    |-  ( ( ph  /\  ps )  ->  E. w  e.  B  A. z  e.  B  -.  z R w )
 
Theorembnj1189 33144* Technical lemma for bnj69 33145. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
 |-  ( ph 
 <->  ( R  FrSe  A  /\  B  C_  A  /\  B  =/= 
 (/) ) )   &    |-  ( ps 
 <->  ( x  e.  B  /\  y  e.  B  /\  y R x ) )   &    |-  ( ch  <->  A. y  e.  B  -.  y R x )   =>    |-  ( ph  ->  E. x  e.  B  A. y  e.  B  -.  y R x )
 
21.28.3  The existence of a minimal element in certain classes
 
Theorembnj69 33145* Existence of a minimal element in certain classes: if  R is well-founded and set-like on 
A, then every nonempty subclass of  A has a minimal element. The proof has been taken from Chapter 4 of Don Monk's notes on Set Theory. See http://euclid.colorado.edu/~monkd/setth.pdf. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
 |-  (
 ( R  FrSe  A  /\  B  C_  A  /\  B  =/= 
 (/) )  ->  E. x  e.  B  A. y  e.  B  -.  y R x )
 
Theorembnj1228 33146* Existence of a minimal element in certain classes: if  R is well-founded and set-like on 
A, then every nonempty subclass of  A has a minimal element. The proof has been taken from Chapter 4 of Don Monk's notes on Set Theory. See http://euclid.colorado.edu/~monkd/setth.pdf. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
 |-  ( w  e.  B  ->  A. x  w  e.  B )   =>    |-  ( ( R  FrSe  A 
 /\  B  C_  A  /\  B  =/=  (/) )  ->  E. x  e.  B  A. y  e.  B  -.  y R x )
 
21.28.4  Well-founded induction
 
Theorembnj1204 33147* Well-founded induction. The proof has been taken from Chapter 4 of Don Monk's notes on Set Theory. See http://euclid.colorado.edu/~monkd/setth.pdf. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
 |-  ( ps 
 <-> 
 A. y  e.  A  ( y R x 
 ->  [. y  /  x ].
 ph ) )   =>    |-  ( ( R 
 FrSe  A  /\  A. x  e.  A  ( ps  ->  ph ) )  ->  A. x  e.  A  ph )
 
Theorembnj1234 33148* Technical lemma for bnj60 33197. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
 |-  Y  =  <. x ,  (
 f  |`  pred ( x ,  A ,  R )
 ) >.   &    |-  C  =  { f  |  E. d  e.  B  ( f  Fn  d  /\  A. x  e.  d  ( f `  x )  =  ( G `  Y ) ) }   &    |-  Z  =  <. x ,  (
 g  |`  pred ( x ,  A ,  R )
 ) >.   &    |-  D  =  { g  |  E. d  e.  B  ( g  Fn  d  /\  A. x  e.  d  ( g `  x )  =  ( G `  Z ) ) }   =>    |-  C  =  D
 
Theorembnj1245 33149* Technical lemma for bnj60 33197. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
 |-  B  =  { d  |  ( d  C_  A  /\  A. x  e.  d  pred ( x ,  A ,  R )  C_  d ) }   &    |-  Y  =  <. x ,  ( f  |`  pred
 ( x ,  A ,  R ) ) >.   &    |-  C  =  { f  |  E. d  e.  B  (
 f  Fn  d  /\  A. x  e.  d  ( f `  x )  =  ( G `  Y ) ) }   &    |-  D  =  ( dom  g  i^i 
 dom  h )   &    |-  E  =  { x  e.  D  |  ( g `  x )  =/=  ( h `  x ) }   &    |-  ( ph 
 <->  ( R  FrSe  A  /\  g  e.  C  /\  h  e.  C  /\  ( g  |`  D )  =/=  ( h  |`  D ) ) )   &    |-  ( ps  <->  ( ph  /\  x  e.  E  /\  A. y  e.  E  -.  y R x ) )   &    |-  Z  =  <. x ,  ( h  |`  pred ( x ,  A ,  R )
 ) >.   &    |-  K  =  { h  |  E. d  e.  B  ( h  Fn  d  /\  A. x  e.  d  ( h `  x )  =  ( G `  Z ) ) }   =>    |-  ( ph  ->  dom  h  C_  A )
 
Theorembnj1256 33150* Technical lemma for bnj60 33197. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
 |-  B  =  { d  |  ( d  C_  A  /\  A. x  e.  d  pred ( x ,  A ,  R )  C_  d ) }   &    |-  Y  =  <. x ,  ( f  |`  pred
 ( x ,  A ,  R ) ) >.   &    |-  C  =  { f  |  E. d  e.  B  (
 f  Fn  d  /\  A. x  e.  d  ( f `  x )  =  ( G `  Y ) ) }   &    |-  D  =  ( dom  g  i^i 
 dom  h )   &    |-  E  =  { x  e.  D  |  ( g `  x )  =/=  ( h `  x ) }   &    |-  ( ph 
 <->  ( R  FrSe  A  /\  g  e.  C  /\  h  e.  C  /\  ( g  |`  D )  =/=  ( h  |`  D ) ) )   &    |-  ( ps  <->  ( ph  /\  x  e.  E  /\  A. y  e.  E  -.  y R x ) )   =>    |-  ( ph  ->  E. d  e.  B  g  Fn  d )
 
Theorembnj1259 33151* Technical lemma for bnj60 33197. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
 |-  B  =  { d  |  ( d  C_  A  /\  A. x  e.  d  pred ( x ,  A ,  R )  C_  d ) }   &    |-  Y  =  <. x ,  ( f  |`  pred
 ( x ,  A ,  R ) ) >.   &    |-  C  =  { f  |  E. d  e.  B  (
 f  Fn  d  /\  A. x  e.  d  ( f `  x )  =  ( G `  Y ) ) }   &    |-  D  =  ( dom  g  i^i 
 dom  h )   &    |-  E  =  { x  e.  D  |  ( g `  x )  =/=  ( h `  x ) }   &    |-  ( ph 
 <->  ( R  FrSe  A  /\  g  e.  C  /\  h  e.  C  /\  ( g  |`  D )  =/=  ( h  |`  D ) ) )   &    |-  ( ps  <->  ( ph  /\  x  e.  E  /\  A. y  e.  E  -.  y R x ) )   =>    |-  ( ph  ->  E. d  e.  B  h  Fn  d )
 
Theorembnj1253 33152* Technical lemma for bnj60 33197. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
 |-  B  =  { d  |  ( d  C_  A  /\  A. x  e.  d  pred ( x ,  A ,  R )  C_  d ) }   &    |-  Y  =  <. x ,  ( f  |`  pred
 ( x ,  A ,  R ) ) >.   &    |-  C  =  { f  |  E. d  e.  B  (
 f  Fn  d  /\  A. x  e.  d  ( f `  x )  =  ( G `  Y ) ) }   &    |-  D  =  ( dom  g  i^i 
 dom  h )   &    |-  E  =  { x  e.  D  |  ( g `  x )  =/=  ( h `  x ) }   &    |-  ( ph 
 <->  ( R  FrSe  A  /\  g  e.  C  /\  h  e.  C  /\  ( g  |`  D )  =/=  ( h  |`  D ) ) )   &    |-  ( ps  <->  ( ph  /\  x  e.  E  /\  A. y  e.  E  -.  y R x ) )   =>    |-  ( ph  ->  E  =/=  (/) )
 
Theorembnj1279 33153* Technical lemma for bnj60 33197. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
 |-  B  =  { d  |  ( d  C_  A  /\  A. x  e.  d  pred ( x ,  A ,  R )  C_  d ) }   &    |-  Y  =  <. x ,  ( f  |`  pred
 ( x ,  A ,  R ) ) >.   &    |-  C  =  { f  |  E. d  e.  B  (
 f  Fn  d  /\  A. x  e.  d  ( f `  x )  =  ( G `  Y ) ) }   &    |-  D  =  ( dom  g  i^i 
 dom  h )   &    |-  E  =  { x  e.  D  |  ( g `  x )  =/=  ( h `  x ) }   &    |-  ( ph 
 <->  ( R  FrSe  A  /\  g  e.  C  /\  h  e.  C  /\  ( g  |`  D )  =/=  ( h  |`  D ) ) )   &    |-  ( ps  <->  ( ph  /\  x  e.  E  /\  A. y  e.  E  -.  y R x ) )   =>    |-  ( ( x  e.  E  /\  A. y  e.  E  -.  y R x )  ->  (  pred ( x ,  A ,  R )  i^i  E )  =  (/) )
 
Theorembnj1286 33154* Technical lemma for bnj60 33197. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
 |-  B  =  { d  |  ( d  C_  A  /\  A. x  e.  d  pred ( x ,  A ,  R )  C_  d ) }   &    |-  Y  =  <. x ,  ( f  |`  pred
 ( x ,  A ,  R ) ) >.   &    |-  C  =  { f  |  E. d  e.  B  (
 f  Fn  d  /\  A. x  e.  d  ( f `  x )  =  ( G `  Y ) ) }   &    |-  D  =  ( dom  g  i^i 
 dom  h )   &    |-  E  =  { x  e.  D  |  ( g `  x )  =/=  ( h `  x ) }   &    |-  ( ph 
 <->  ( R  FrSe  A  /\  g  e.  C  /\  h  e.  C  /\  ( g  |`  D )  =/=  ( h  |`  D ) ) )   &    |-  ( ps  <->  ( ph  /\  x  e.  E  /\  A. y  e.  E  -.  y R x ) )   =>    |-  ( ps  ->  pred
 ( x ,  A ,  R )  C_  D )
 
Theorembnj1280 33155* Technical lemma for bnj60 33197. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
 |-  B  =  { d  |  ( d  C_  A  /\  A. x  e.  d  pred ( x ,  A ,  R )  C_  d ) }   &    |-  Y  =  <. x ,  ( f  |`  pred
 ( x ,  A ,  R ) ) >.   &    |-  C  =  { f  |  E. d  e.  B  (
 f  Fn  d  /\  A. x  e.  d  ( f `  x )  =  ( G `  Y ) ) }   &    |-  D  =  ( dom  g  i^i 
 dom  h )   &    |-  E  =  { x  e.  D  |  ( g `  x )  =/=  ( h `  x ) }   &    |-  ( ph 
 <->  ( R  FrSe  A  /\  g  e.  C  /\  h  e.  C  /\  ( g  |`  D )  =/=  ( h  |`  D ) ) )   &    |-  ( ps  <->  ( ph  /\  x  e.  E  /\  A. y  e.  E  -.  y R x ) )   &    |-  ( ps  ->  (  pred ( x ,  A ,  R )  i^i  E )  =  (/) )   =>    |-  ( ps  ->  (
 g  |`  pred ( x ,  A ,  R )
 )  =  ( h  |`  pred ( x ,  A ,  R )
 ) )
 
Theorembnj1296 33156* Technical lemma for bnj60 33197. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
 |-  B  =  { d  |  ( d  C_  A  /\  A. x  e.  d  pred ( x ,  A ,  R )  C_  d ) }   &    |-  Y  =  <. x ,  ( f  |`  pred
 ( x ,  A ,  R ) ) >.   &    |-  C  =  { f  |  E. d  e.  B  (
 f  Fn  d  /\  A. x  e.  d  ( f `  x )  =  ( G `  Y ) ) }   &    |-  D  =  ( dom  g  i^i 
 dom  h )   &    |-  E  =  { x  e.  D  |  ( g `  x )  =/=  ( h `  x ) }   &    |-  ( ph 
 <->  ( R  FrSe  A  /\  g  e.  C  /\  h  e.  C  /\  ( g  |`  D )  =/=  ( h  |`  D ) ) )   &    |-  ( ps  <->  ( ph  /\  x  e.  E  /\  A. y  e.  E  -.  y R x ) )   &    |-  ( ps  ->  ( g  |`  pred
 ( x ,  A ,  R ) )  =  ( h  |`  pred ( x ,  A ,  R ) ) )   &    |-  Z  =  <. x ,  ( g  |`  pred ( x ,  A ,  R ) ) >.   &    |-  K  =  { g  |  E. d  e.  B  (
 g  Fn  d  /\  A. x  e.  d  ( g `  x )  =  ( G `  Z ) ) }   &    |-  W  =  <. x ,  ( h  |`  pred ( x ,  A ,  R )
 ) >.   &    |-  L  =  { h  |  E. d  e.  B  ( h  Fn  d  /\  A. x  e.  d  ( h `  x )  =  ( G `  W ) ) }   =>    |-  ( ps  ->  ( g `  x )  =  ( h `  x ) )
 
Theorembnj1309 33157* Technical lemma for bnj60 33197. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
 |-  B  =  { d  |  ( d  C_  A  /\  A. x  e.  d  pred ( x ,  A ,  R )  C_  d ) }   =>    |-  ( w  e.  B  ->  A. x  w  e.  B )
 
Theorembnj1307 33158* Technical lemma for bnj60 33197. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
 |-  C  =  { f  |  E. d  e.  B  (
 f  Fn  d  /\  A. x  e.  d  ( f `  x )  =  ( G `  Y ) ) }   &    |-  ( w  e.  B  ->  A. x  w  e.  B )   =>    |-  ( w  e.  C  ->  A. x  w  e.  C )
 
Theorembnj1311 33159* Technical lemma for bnj60 33197. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
 |-  B  =  { d  |  ( d  C_  A  /\  A. x  e.  d  pred ( x ,  A ,  R )  C_  d ) }   &    |-  Y  =  <. x ,  ( f  |`  pred
 ( x ,  A ,  R ) ) >.   &    |-  C  =  { f  |  E. d  e.  B  (
 f  Fn  d  /\  A. x  e.  d  ( f `  x )  =  ( G `  Y ) ) }   &    |-  D  =  ( dom  g  i^i 
 dom  h )   =>    |-  ( ( R 
 FrSe  A  /\  g  e.  C  /\  h  e.  C )  ->  (
 g  |`  D )  =  ( h  |`  D ) )
 
Theorembnj1318 33160 Technical lemma for bnj60 33197. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
 |-  ( X  =  Y  ->  trCl
 ( X ,  A ,  R )  =  trCl ( Y ,  A ,  R ) )
 
Theorembnj1326 33161* Technical lemma for bnj60 33197. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
 |-  B  =  { d  |  ( d  C_  A  /\  A. x  e.  d  pred ( x ,  A ,  R )  C_  d ) }   &    |-  Y  =  <. x ,  ( f  |`  pred
 ( x ,  A ,  R ) ) >.   &    |-  C  =  { f  |  E. d  e.  B  (
 f  Fn  d  /\  A. x  e.  d  ( f `  x )  =  ( G `  Y ) ) }   &    |-  D  =  ( dom  g  i^i 
 dom  h )   =>    |-  ( ( R 
 FrSe  A  /\  g  e.  C  /\  h  e.  C )  ->  (
 g  |`  D )  =  ( h  |`  D ) )
 
Theorembnj1321 33162* Technical lemma for bnj60 33197. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
 |-  B  =  { d  |  ( d  C_  A  /\  A. x  e.  d  pred ( x ,  A ,  R )  C_  d ) }   &    |-  Y  =  <. x ,  ( f  |`  pred
 ( x ,  A ,  R ) ) >.   &    |-  C  =  { f  |  E. d  e.  B  (
 f  Fn  d  /\  A. x  e.  d  ( f `  x )  =  ( G `  Y ) ) }   &    |-  ( ta 
 <->  ( f  e.  C  /\  dom  f  =  ( { x }  u.  trCl
 ( x ,  A ,  R ) ) ) )   =>    |-  ( ( R  FrSe  A 
 /\  E. f ta )  ->  E! f ta )
 
Theorembnj1364 33163 Property of  FrSe. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
 |-  ( R  FrSe  A  ->  R  Se  A )
 
Theorembnj1371 33164* Technical lemma for bnj60 33197. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
 |-  B  =  { d  |  ( d  C_  A  /\  A. x  e.  d  pred ( x ,  A ,  R )  C_  d ) }   &    |-  Y  =  <. x ,  ( f  |`  pred
 ( x ,  A ,  R ) ) >.   &    |-  C  =  { f  |  E. d  e.  B  (
 f  Fn  d  /\  A. x  e.  d  ( f `  x )  =  ( G `  Y ) ) }   &    |-  ( ta 
 <->  ( f  e.  C  /\  dom  f  =  ( { x }  u.  trCl
 ( x ,  A ,  R ) ) ) )   &    |-  D  =  { x  e.  A  |  -.  E. f ta }   &    |-  ( ps 
 <->  ( R  FrSe  A  /\  D  =/=  (/) ) )   &    |-  ( ch 
 <->  ( ps  /\  x  e.  D  /\  A. y  e.  D  -.  y R x ) )   &    |-  ( ta'  <->  [. y  /  x ]. ta )   &    |-  H  =  {
 f  |  E. y  e.  pred  ( x ,  A ,  R ) ta'
 }   &    |-  P  =  U. H   &    |-  ( ta'  <->  ( f  e.  C  /\  dom  f  =  ( {
 y }  u.  trCl ( y ,  A ,  R ) ) ) )   =>    |-  ( f  e.  H  ->  Fun  f )
 
Theorembnj1373 33165* Technical lemma for bnj60 33197. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
 |-  B  =  { d  |  ( d  C_  A  /\  A. x  e.  d  pred ( x ,  A ,  R )  C_  d ) }   &    |-  Y  =  <. x ,  ( f  |`  pred
 ( x ,  A ,  R ) ) >.   &    |-  C  =  { f  |  E. d  e.  B  (
 f  Fn  d  /\  A. x  e.  d  ( f `  x )  =  ( G `  Y ) ) }   &    |-  ( ta 
 <->  ( f  e.  C  /\  dom  f  =  ( { x }  u.  trCl
 ( x ,  A ,  R ) ) ) )   &    |-  ( ta'  <->  [. y  /  x ].
 ta )   =>    |-  ( ta'  <->  ( f  e.  C  /\  dom  f  =  ( { y }  u.  trCl ( y ,  A ,  R ) ) ) )
 
Theorembnj1374 33166* Technical lemma for bnj60 33197. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
 |-  B  =  { d  |  ( d  C_  A  /\  A. x  e.  d  pred ( x ,  A ,  R )  C_  d ) }   &    |-  Y  =  <. x ,  ( f  |`  pred
 ( x ,  A ,  R ) ) >.   &    |-  C  =  { f  |  E. d  e.  B  (
 f  Fn  d  /\  A. x  e.  d  ( f `  x )  =  ( G `  Y ) ) }   &    |-  ( ta 
 <->  ( f  e.  C  /\  dom  f  =  ( { x }  u.  trCl
 ( x ,  A ,  R ) ) ) )   &    |-  D  =  { x  e.  A  |  -.  E. f ta }   &    |-  ( ps 
 <->  ( R  FrSe  A  /\  D  =/=  (/) ) )   &    |-  ( ch 
 <->  ( ps  /\  x  e.  D  /\  A. y  e.  D  -.  y R x ) )   &    |-  ( ta'  <->  [. y  /  x ]. ta )   &    |-  H  =  {
 f  |  E. y  e.  pred  ( x ,  A ,  R ) ta'
 }   =>    |-  ( f  e.  H  ->  f  e.  C )
 
Theorembnj1384 33167* Technical lemma for bnj60 33197. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
 |-  B  =  { d  |  ( d  C_  A  /\  A. x  e.  d  pred ( x ,  A ,  R )  C_  d ) }   &    |-  Y  =  <. x ,  ( f  |`  pred
 ( x ,  A ,  R ) ) >.   &    |-  C  =  { f  |  E. d  e.  B  (
 f  Fn  d  /\  A. x  e.  d  ( f `  x )  =  ( G `  Y ) ) }   &    |-  ( ta 
 <->  ( f  e.  C  /\  dom  f  =  ( { x }  u.  trCl
 ( x ,  A ,  R ) ) ) )   &    |-  D  =  { x  e.  A  |  -.  E. f ta }   &    |-  ( ps 
 <->  ( R  FrSe  A  /\  D  =/=  (/) ) )   &    |-  ( ch 
 <->  ( ps  /\  x  e.  D  /\  A. y  e.  D  -.  y R x ) )   &    |-  ( ta'  <->  [. y  /  x ]. ta )   &    |-  H  =  {
 f  |  E. y  e.  pred  ( x ,  A ,  R ) ta'
 }   &    |-  P  =  U. H   =>    |-  ( R  FrSe  A  ->  Fun  P )
 
Theorembnj1388 33168* Technical lemma for bnj60 33197. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
 |-  B  =  { d  |  ( d  C_  A  /\  A. x  e.  d  pred ( x ,  A ,  R )  C_  d ) }   &    |-  Y  =  <. x ,  ( f  |`  pred
 ( x ,  A ,  R ) ) >.   &    |-  C  =  { f  |  E. d  e.  B  (
 f  Fn  d  /\  A. x  e.  d  ( f `  x )  =  ( G `  Y ) ) }   &    |-  ( ta 
 <->  ( f  e.  C  /\  dom  f  =  ( { x }  u.  trCl
 ( x ,  A ,  R ) ) ) )   &    |-  D  =  { x  e.  A  |  -.  E. f ta }   &    |-  ( ps 
 <->  ( R  FrSe  A  /\  D  =/=  (/) ) )   &    |-  ( ch 
 <->  ( ps  /\  x  e.  D  /\  A. y  e.  D  -.  y R x ) )   &    |-  ( ta'  <->  [. y  /  x ]. ta )   =>    |-  ( ch  ->  A. y  e.  pred  ( x ,  A ,  R ) E. f ta' )
 
Theorembnj1398 33169* Technical lemma for bnj60 33197. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
 |-  B  =  { d  |  ( d  C_  A  /\  A. x  e.  d  pred ( x ,  A ,  R )  C_  d ) }   &    |-  Y  =  <. x ,  ( f  |`  pred
 ( x ,  A ,  R ) ) >.   &    |-  C  =  { f  |  E. d  e.  B  (
 f  Fn  d  /\  A. x  e.  d  ( f `  x )  =  ( G `  Y ) ) }   &    |-  ( ta 
 <->  ( f  e.  C  /\  dom  f  =  ( { x }  u.  trCl
 ( x ,  A ,  R ) ) ) )   &    |-  D  =  { x  e.  A  |  -.  E. f ta }   &    |-  ( ps 
 <->  ( R  FrSe  A  /\  D  =/=  (/) ) )   &    |-  ( ch 
 <->  ( ps  /\  x  e.  D  /\  A. y  e.  D  -.  y R x ) )   &    |-  ( ta'  <->  [. y  /  x ]. ta )   &    |-  H  =  {
 f  |  E. y  e.  pred  ( x ,  A ,  R ) ta'
 }   &    |-  P  =  U. H   &    |-  ( th 
 <->  ( ch  /\  z  e.  U_ y  e.  pred  ( x ,  A ,  R ) ( {
 y }  u.  trCl ( y ,  A ,  R ) ) ) )   &    |-  ( et  <->  ( th  /\  y  e.  pred ( x ,  A ,  R )  /\  z  e.  ( { y }  u.  trCl
 ( y ,  A ,  R ) ) ) )   =>    |-  ( ch  ->  U_ y  e.  pred  ( x ,  A ,  R )
 ( { y }  u.  trCl ( y ,  A ,  R ) )  =  dom  P )
 
Theorembnj1413 33170* Property of  trCl. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
 |-  B  =  (  pred ( X ,  A ,  R )  u.  U_ y  e.  pred  ( X ,  A ,  R )  trCl ( y ,  A ,  R ) )   =>    |-  ( ( R  FrSe  A 
 /\  X  e.  A )  ->  B  e.  _V )
 
Theorembnj1408 33171* Technical lemma for bnj1414 33172. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
 |-  B  =  (  pred ( X ,  A ,  R )  u.  U_ y  e.  pred  ( X ,  A ,  R )  trCl ( y ,  A ,  R ) )   &    |-  C  =  ( 
 pred ( X ,  A ,  R )  u.  U_ y  e.  trCl  ( X ,  A ,  R )  trCl ( y ,  A ,  R ) )   &    |-  ( th  <->  ( R  FrSe  A 
 /\  X  e.  A ) )   &    |-  ( ta  <->  ( B  e.  _V 
 /\  TrFo ( B ,  A ,  R )  /\  pred ( X ,  A ,  R )  C_  B ) )   =>    |-  ( ( R 
 FrSe  A  /\  X  e.  A )  ->  trCl ( X ,  A ,  R )  =  B )
 
Theorembnj1414 33172* Property of  trCl. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
 |-  B  =  (  pred ( X ,  A ,  R )  u.  U_ y  e.  pred  ( X ,  A ,  R )  trCl ( y ,  A ,  R ) )   =>    |-  ( ( R  FrSe  A 
 /\  X  e.  A )  ->  trCl ( X ,  A ,  R )  =  B )
 
Theorembnj1415 33173* Technical lemma for bnj60 33197. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
 |-  B  =  { d  |  ( d  C_  A  /\  A. x  e.  d  pred ( x ,  A ,  R )  C_  d ) }   &    |-  Y  =  <. x ,  ( f  |`  pred
 ( x ,  A ,  R ) ) >.   &    |-  C  =  { f  |  E. d  e.  B  (
 f  Fn  d  /\  A. x  e.  d  ( f `  x )  =  ( G `  Y ) ) }   &    |-  ( ta 
 <->  ( f  e.  C  /\  dom  f  =  ( { x }  u.  trCl
 ( x ,  A ,  R ) ) ) )   &    |-  D  =  { x  e.  A  |  -.  E. f ta }   &    |-  ( ps 
 <->  ( R  FrSe  A  /\  D  =/=  (/) ) )   &    |-  ( ch 
 <->  ( ps  /\  x  e.  D  /\  A. y  e.  D  -.  y R x ) )   &    |-  ( ta'  <->  [. y  /  x ]. ta )   &    |-  H  =  {
 f  |  E. y  e.  pred  ( x ,  A ,  R ) ta'
 }   &    |-  P  =  U. H   =>    |-  ( ch  ->  dom  P  =  trCl ( x ,  A ,  R ) )
 
Theorembnj1416 33174 Technical lemma for bnj60 33197. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
 |-  B  =  { d  |  ( d  C_  A  /\  A. x  e.  d  pred ( x ,  A ,  R )  C_  d ) }   &    |-  Y  =  <. x ,  ( f  |`  pred
 ( x ,  A ,  R ) ) >.   &    |-  C  =  { f  |  E. d  e.  B  (
 f  Fn  d  /\  A. x  e.  d  ( f `  x )  =  ( G `  Y ) ) }   &    |-  ( ta 
 <->  ( f  e.  C  /\  dom  f  =  ( { x }  u.  trCl
 ( x ,  A ,  R ) ) ) )   &    |-  D  =  { x  e.  A  |  -.  E. f ta }   &    |-  ( ps 
 <->  ( R  FrSe  A  /\  D  =/=  (/) ) )   &    |-  ( ch 
 <->  ( ps  /\  x  e.  D  /\  A. y  e.  D  -.  y R x ) )   &    |-  ( ta'  <->  [. y  /  x ]. ta )   &    |-  H  =  {
 f  |  E. y  e.  pred  ( x ,  A ,  R ) ta'
 }   &    |-  P  =  U. H   &    |-  Z  =  <. x ,  ( P  |`  pred ( x ,  A ,  R )
 ) >.   &    |-  Q  =  ( P  u.  { <. x ,  ( G `  Z )
 >. } )   &    |-  ( ch  ->  dom 
 P  =  trCl ( x ,  A ,  R ) )   =>    |-  ( ch  ->  dom 
 Q  =  ( { x }  u.  trCl ( x ,  A ,  R ) ) )
 
Theorembnj1418 33175 Property of  pred. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
 |-  (
 y  e.  pred ( x ,  A ,  R )  ->  y R x )
 
Theorembnj1417 33176* Technical lemma for bnj60 33197. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Proof shortened by Mario Carneiro, 22-Dec-2016.) (New usage is discouraged.)
 |-  ( ph 
 <->  R  FrSe  A )   &    |-  ( ps 
 <->  -.  x  e.  trCl ( x ,  A ,  R ) )   &    |-  ( ch 
 <-> 
 A. y  e.  A  ( y R x 
 ->  [. y  /  x ].
 ps ) )   &    |-  ( th 
 <->  ( ph  /\  x  e.  A  /\  ch )
 )   &    |-  B  =  (  pred ( x ,  A ,  R )  u.  U_ y  e.  pred  ( x ,  A ,  R )  trCl ( y ,  A ,  R ) )   =>    |-  ( ph  ->  A. x  e.  A  -.  x  e.  trCl ( x ,  A ,  R ) )
 
Theorembnj1421 33177* Technical lemma for bnj60 33197. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
 |-  B  =  { d  |  ( d  C_  A  /\  A. x  e.  d  pred ( x ,  A ,  R )  C_  d ) }   &    |-  Y  =  <. x ,  ( f  |`  pred
 ( x ,  A ,  R ) ) >.   &    |-  C  =  { f  |  E. d  e.  B  (
 f  Fn  d  /\  A. x  e.  d  ( f `  x )  =  ( G `  Y ) ) }   &    |-  ( ta 
 <->  ( f  e.  C  /\  dom  f  =  ( { x }  u.  trCl
 ( x ,  A ,  R ) ) ) )   &    |-  D  =  { x  e.  A  |  -.  E. f ta }   &    |-  ( ps 
 <->  ( R  FrSe  A  /\  D  =/=  (/) ) )   &    |-  ( ch 
 <->  ( ps  /\  x  e.  D  /\  A. y  e.  D  -.  y R x ) )   &    |-  ( ta'  <->  [. y  /  x ]. ta )   &    |-  H  =  {
 f  |  E. y  e.  pred  ( x ,  A ,  R ) ta'
 }   &    |-  P  =  U. H   &    |-  Z  =  <. x ,  ( P  |`  pred ( x ,  A ,  R )
 ) >.   &    |-  Q  =  ( P  u.  { <. x ,  ( G `  Z )
 >. } )   &    |-  ( ch  ->  Fun 
 P )   &    |-  ( ch  ->  dom 
 Q  =  ( { x }  u.  trCl ( x ,  A ,  R ) ) )   &    |-  ( ch  ->  dom  P  =  trCl ( x ,  A ,  R ) )   =>    |-  ( ch  ->  Fun 
 Q )
 
Theorembnj1444 33178* Technical lemma for bnj60 33197. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
 |-  B  =  { d  |  ( d  C_  A  /\  A. x  e.  d  pred ( x ,  A ,  R )  C_  d ) }   &    |-  Y  =  <. x ,  ( f  |`  pred
 ( x ,  A ,  R ) ) >.   &    |-  C  =  { f  |  E. d  e.  B  (
 f  Fn  d  /\  A. x  e.  d  ( f `  x )  =  ( G `  Y ) ) }   &    |-  ( ta 
 <->  ( f  e.  C  /\  dom  f  =  ( { x }  u.  trCl
 ( x ,  A ,  R ) ) ) )   &    |-  D  =  { x  e.  A  |  -.  E. f ta }   &    |-  ( ps 
 <->  ( R  FrSe  A  /\  D  =/=  (/) ) )   &    |-  ( ch 
 <->  ( ps  /\  x  e.  D  /\  A. y  e.  D  -.  y R x ) )   &    |-  ( ta'  <->  [. y  /  x ]. ta )   &    |-  H  =  {
 f  |  E. y  e.  pred  ( x ,  A ,  R ) ta'
 }   &    |-  P  =  U. H   &    |-  Z  =  <. x ,  ( P  |`  pred ( x ,  A ,  R )
 ) >.   &    |-  Q  =  ( P  u.  { <. x ,  ( G `  Z )
 >. } )   &    |-  W  =  <. z ,  ( Q  |`  pred (
 z ,  A ,  R ) ) >.   &    |-  E  =  ( { x }  u.  trCl ( x ,  A ,  R )
 )   &    |-  ( ch  ->  P  Fn  trCl ( x ,  A ,  R )
 )   &    |-  ( ch  ->  Q  Fn  ( { x }  u.  trCl ( x ,  A ,  R )
 ) )   &    |-  ( th  <->  ( ch  /\  z  e.  E )
 )   &    |-  ( et  <->  ( th  /\  z  e.  { x } ) )   &    |-  ( ze 
 <->  ( th  /\  z  e.  trCl ( x ,  A ,  R )
 ) )   &    |-  ( rh  <->  ( ze  /\  f  e.  H  /\  z  e.  dom  f ) )   =>    |-  ( rh  ->  A. y rh )
 
Theorembnj1445 33179* Technical lemma for bnj60 33197. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
 |-  B  =  { d  |  ( d  C_  A  /\  A. x  e.  d  pred ( x ,  A ,  R )  C_  d ) }   &    |-  Y  =  <. x ,  ( f  |`  pred
 ( x ,  A ,  R ) ) >.   &    |-  C  =  { f  |  E. d  e.  B  (
 f  Fn  d  /\  A. x  e.  d  ( f `  x )  =  ( G `  Y ) ) }   &    |-  ( ta 
 <->  ( f  e.  C  /\  dom  f  =  ( { x }  u.  trCl
 ( x ,  A ,  R ) ) ) )   &    |-  D  =  { x  e.  A  |  -.  E. f ta }   &    |-  ( ps 
 <->  ( R  FrSe  A  /\  D  =/=  (/) ) )   &    |-  ( ch 
 <->  ( ps  /\  x  e.  D  /\  A. y  e.  D  -.  y R x ) )   &    |-  ( ta'  <->  [. y  /  x ]. ta )   &    |-  H  =  {
 f  |  E. y  e.  pred  ( x ,  A ,  R ) ta'
 }   &    |-  P  =  U. H   &    |-  Z  =  <. x ,  ( P  |`  pred ( x ,  A ,  R )
 ) >.   &    |-  Q  =  ( P  u.  { <. x ,  ( G `  Z )
 >. } )   &    |-  W  =  <. z ,  ( Q  |`  pred (
 z ,  A ,  R ) ) >.   &    |-  E  =  ( { x }  u.  trCl ( x ,  A ,  R )
 )   &    |-  ( ch  ->  P  Fn  trCl ( x ,  A ,  R )
 )   &    |-  ( ch  ->  Q  Fn  ( { x }  u.  trCl ( x ,  A ,  R )
 ) )   &    |-  ( th  <->  ( ch  /\  z  e.  E )
 )   &    |-  ( et  <->  ( th  /\  z  e.  { x } ) )   &    |-  ( ze 
 <->  ( th  /\  z  e.  trCl ( x ,  A ,  R )
 ) )   &    |-  ( rh  <->  ( ze  /\  f  e.  H  /\  z  e.  dom  f ) )   &    |-  ( si  <->  ( rh  /\  y  e.  pred ( x ,  A ,  R )  /\  f  e.  C  /\  dom  f  =  ( { y }  u.  trCl
 ( y ,  A ,  R ) ) ) )   &    |-  ( ph  <->  ( si  /\  d  e.  B  /\  f  Fn  d  /\  A. x  e.  d  (
 f `  x )  =  ( G `  Y ) ) )   &    |-  X  =  <. z ,  (
 f  |`  pred ( z ,  A ,  R ) ) >.   =>    |-  ( si  ->  A. d si )
 
Theorembnj1446 33180* Technical lemma for bnj60 33197. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
 |-  B  =  { d  |  ( d  C_  A  /\  A. x  e.  d  pred ( x ,  A ,  R )  C_  d ) }   &    |-  Y  =  <. x ,  ( f  |`  pred
 ( x ,  A ,  R ) ) >.   &    |-  C  =  { f  |  E. d  e.  B  (
 f  Fn  d  /\  A. x  e.  d  ( f `  x )  =  ( G `  Y ) ) }   &    |-  ( ta 
 <->  ( f  e.  C  /\  dom  f  =  ( { x }  u.  trCl
 ( x ,  A ,  R ) ) ) )   &    |-  D  =  { x  e.  A  |  -.  E. f ta }   &    |-  ( ps 
 <->  ( R  FrSe  A  /\  D  =/=  (/) ) )   &    |-  ( ch 
 <->  ( ps  /\  x  e.  D  /\  A. y  e.  D  -.  y R x ) )   &    |-  ( ta'  <->  [. y  /  x ]. ta )   &    |-  H  =  {
 f  |  E. y  e.  pred  ( x ,  A ,  R ) ta'
 }   &    |-  P  =  U. H   &    |-  Z  =  <. x ,  ( P  |`  pred ( x ,  A ,  R )
 ) >.   &    |-  Q  =  ( P  u.  { <. x ,  ( G `  Z )
 >. } )   &    |-  W  =  <. z ,  ( Q  |`  pred (
 z ,  A ,  R ) ) >.   =>    |-  ( ( Q `
  z )  =  ( G `  W )  ->  A. d ( Q `
  z )  =  ( G `  W ) )
 
Theorembnj1447 33181* Technical lemma for bnj60 33197. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
 |-  B  =  { d  |  ( d  C_  A  /\  A. x  e.  d  pred ( x ,  A ,  R )  C_  d ) }   &    |-  Y  =  <. x ,  ( f  |`  pred
 ( x ,  A ,  R ) ) >.   &    |-  C  =  { f  |  E. d  e.  B  (
 f  Fn  d  /\  A. x  e.  d  ( f `  x )  =  ( G `  Y ) ) }   &    |-  ( ta 
 <->  ( f  e.  C  /\  dom  f  =  ( { x }  u.  trCl
 ( x ,  A ,  R ) ) ) )   &    |-  D  =  { x  e.  A  |  -.  E. f ta }   &    |-  ( ps 
 <->  ( R  FrSe  A  /\  D  =/=  (/) ) )   &    |-  ( ch 
 <->  ( ps  /\  x  e.  D  /\  A. y  e.  D  -.  y R x ) )   &    |-  ( ta'  <->  [. y  /  x ]. ta )   &    |-  H  =  {
 f  |  E. y  e.  pred  ( x ,  A ,  R ) ta'
 }   &    |-  P  =  U. H   &    |-  Z  =  <. x ,  ( P  |`  pred ( x ,  A ,  R )
 ) >.   &    |-  Q  =  ( P  u.  { <. x ,  ( G `  Z )
 >. } )   &    |-  W  =  <. z ,  ( Q  |`  pred (
 z ,  A ,  R ) ) >.   =>    |-  ( ( Q `
  z )  =  ( G `  W )  ->  A. y ( Q `
  z )  =  ( G `  W ) )
 
Theorembnj1448 33182* Technical lemma for bnj60 33197. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
 |-  B  =  { d  |  ( d  C_  A  /\  A. x  e.  d  pred ( x ,  A ,  R )  C_  d ) }   &    |-  Y  =  <. x ,  ( f  |`  pred
 ( x ,  A ,  R ) ) >.   &    |-  C  =  { f  |  E. d  e.  B  (
 f  Fn  d  /\  A. x  e.  d  ( f `  x )  =  ( G `  Y ) ) }   &    |-  ( ta 
 <->  ( f  e.  C  /\  dom  f  =  ( { x }  u.  trCl
 ( x ,  A ,  R ) ) ) )   &    |-  D  =  { x  e.  A  |  -.  E. f ta }   &    |-  ( ps 
 <->  ( R  FrSe  A  /\  D  =/=  (/) ) )   &    |-  ( ch 
 <->  ( ps  /\  x  e.  D  /\  A. y  e.  D  -.  y R x ) )   &    |-  ( ta'  <->  [. y  /  x ]. ta )   &    |-  H  =  {
 f  |  E. y  e.  pred  ( x ,  A ,  R ) ta'
 }   &    |-  P  =  U. H   &    |-  Z  =  <. x ,  ( P  |`  pred ( x ,  A ,  R )
 ) >.   &    |-  Q  =  ( P  u.  { <. x ,  ( G `  Z )
 >. } )   &    |-  W  =  <. z ,  ( Q  |`  pred (
 z ,  A ,  R ) ) >.   =>    |-  ( ( Q `
  z )  =  ( G `  W )  ->  A. f ( Q `
  z )  =  ( G `  W ) )
 
Theorembnj1449 33183* Technical lemma for bnj60 33197. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
 |-  B  =  { d  |  ( d  C_  A  /\  A. x  e.  d  pred ( x ,  A ,  R )  C_  d ) }   &    |-  Y  =  <. x ,  ( f  |`  pred
 ( x ,  A ,  R ) ) >.   &    |-  C  =  { f  |  E. d  e.  B  (
 f  Fn  d  /\  A. x  e.  d  ( f `  x )  =  ( G `  Y ) ) }   &    |-  ( ta 
 <->  ( f  e.  C  /\  dom  f  =  ( { x }  u.  trCl
 ( x ,  A ,  R ) ) ) )   &    |-  D  =  { x  e.  A  |  -.  E. f ta }   &    |-  ( ps 
 <->  ( R  FrSe  A  /\  D  =/=  (/) ) )   &    |-  ( ch 
 <->  ( ps  /\  x  e.  D  /\  A. y  e.  D  -.  y R x ) )   &    |-  ( ta'  <->  [. y  /  x ]. ta )   &    |-  H  =  {
 f  |  E. y  e.  pred  ( x ,  A ,  R ) ta'
 }   &    |-  P  =  U. H   &    |-  Z  =  <. x ,  ( P  |`  pred ( x ,  A ,  R )
 ) >.   &    |-  Q  =  ( P  u.  { <. x ,  ( G `  Z )
 >. } )   &    |-  W  =  <. z ,  ( Q  |`  pred (
 z ,  A ,  R ) ) >.   &    |-  E  =  ( { x }  u.  trCl ( x ,  A ,  R )
 )   &    |-  ( ch  ->  P  Fn  trCl ( x ,  A ,  R )
 )   &    |-  ( ch  ->  Q  Fn  ( { x }  u.  trCl ( x ,  A ,  R )
 ) )   &    |-  ( th  <->  ( ch  /\  z  e.  E )
 )   &    |-  ( et  <->  ( th  /\  z  e.  { x } ) )   &    |-  ( ze 
 <->  ( th  /\  z  e.  trCl ( x ,  A ,  R )
 ) )   =>    |-  ( ze  ->  A. f ze )
 
Theorembnj1442 33184* Technical lemma for bnj60 33197. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
 |-  B  =  { d  |  ( d  C_  A  /\  A. x  e.  d  pred ( x ,  A ,  R )  C_  d ) }   &    |-  Y  =  <. x ,  ( f  |`  pred
 ( x ,  A ,  R ) ) >.   &    |-  C  =  { f  |  E. d  e.  B  (
 f  Fn  d  /\  A. x  e.  d  ( f `  x )  =  ( G `  Y ) ) }   &    |-  ( ta 
 <->  ( f  e.  C  /\  dom  f  =  ( { x }  u.  trCl
 ( x ,  A ,  R ) ) ) )   &    |-  D  =  { x  e.  A  |  -.  E. f ta }   &    |-  ( ps 
 <->  ( R  FrSe  A  /\  D  =/=  (/) ) )   &    |-  ( ch 
 <->  ( ps  /\  x  e.  D  /\  A. y  e.  D  -.  y R x ) )   &    |-  ( ta'  <->  [. y  /  x ]. ta )   &    |-  H  =  {
 f  |  E. y  e.  pred  ( x ,  A ,  R ) ta'
 }   &    |-  P  =  U. H   &    |-  Z  =  <. x ,  ( P  |`  pred ( x ,  A ,  R )
 ) >.   &    |-  Q  =  ( P  u.  { <. x ,  ( G `  Z )
 >. } )   &    |-  W  =  <. z ,  ( Q  |`  pred (
 z ,  A ,  R ) ) >.   &    |-  E  =  ( { x }  u.  trCl ( x ,  A ,  R )
 )   &    |-  ( ch  ->  P  Fn  trCl ( x ,  A ,  R )
 )   &    |-  ( ch  ->  Q  Fn  ( { x }  u.  trCl ( x ,  A ,  R )
 ) )   &    |-  ( th  <->  ( ch  /\  z  e.  E )
 )   &    |-  ( et  <->  ( th  /\  z  e.  { x } ) )   =>    |-  ( et  ->  ( Q `  z )  =  ( G `  W ) )
 
Theorembnj1450 33185* Technical lemma for bnj60 33197. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
 |-  B  =  { d  |  ( d  C_  A  /\  A. x  e.  d  pred ( x ,  A ,  R )  C_  d ) }   &    |-  Y  =  <. x ,  ( f  |`  pred
 ( x ,  A ,  R ) ) >.   &    |-  C  =  { f  |  E. d  e.  B  (
 f  Fn  d  /\  A. x  e.  d  ( f `  x )  =  ( G `  Y ) ) }   &    |-  ( ta 
 <->  ( f  e.  C  /\  dom  f  =  ( { x }  u.  trCl
 ( x ,  A ,  R ) ) ) )   &    |-  D  =  { x  e.  A  |  -.  E. f ta }   &    |-  ( ps 
 <->  ( R  FrSe  A  /\  D  =/=  (/) ) )   &    |-  ( ch 
 <->  ( ps  /\  x  e.  D  /\  A. y  e.  D  -.  y R x ) )   &    |-  ( ta'  <->  [. y  /  x ]. ta )   &    |-  H  =  {
 f  |  E. y  e.  pred  ( x ,  A ,  R ) ta'
 }   &    |-  P  =  U. H   &    |-  Z  =  <. x ,  ( P  |`  pred ( x ,  A ,  R )
 ) >.   &    |-  Q  =  ( P  u.  { <. x ,  ( G `  Z )
 >. } )   &    |-  W  =  <. z ,  ( Q  |`  pred (
 z ,  A ,  R ) ) >.   &    |-  E  =  ( { x }  u.  trCl ( x ,  A ,  R )
 )   &    |-  ( ch  ->  P  Fn  trCl ( x ,  A ,  R )
 )   &    |-  ( ch  ->  Q  Fn  ( { x }  u.  trCl ( x ,  A ,  R )
 ) )   &    |-  ( th  <->  ( ch  /\  z  e.  E )
 )   &    |-  ( et  <->  ( th  /\  z  e.  { x } ) )   &    |-  ( ze 
 <->  ( th  /\  z  e.  trCl ( x ,  A ,  R )
 ) )   &    |-  ( rh  <->  ( ze  /\  f  e.  H  /\  z  e.  dom  f ) )   &    |-  ( si  <->  ( rh  /\  y  e.  pred ( x ,  A ,  R )  /\  f  e.  C  /\  dom  f  =  ( { y }  u.  trCl
 ( y ,  A ,  R ) ) ) )   &    |-  ( ph  <->  ( si  /\  d  e.  B  /\  f  Fn  d  /\  A. x  e.  d  (
 f `  x )  =  ( G `  Y ) ) )   &    |-  X  =  <. z ,  (
 f  |`  pred ( z ,  A ,  R ) ) >.   =>    |-  ( ze  ->  ( Q `  z )  =  ( G `  W ) )
 
Theorembnj1423 33186* Technical lemma for bnj60 33197. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
 |-  B  =  { d  |  ( d  C_  A  /\  A. x  e.  d  pred ( x ,  A ,  R )  C_  d ) }   &    |-  Y  =  <. x ,  ( f  |`  pred
 ( x ,  A ,  R ) ) >.   &    |-  C  =  { f  |  E. d  e.  B  (
 f  Fn  d  /\  A. x  e.  d  ( f `  x )  =  ( G `  Y ) ) }   &    |-  ( ta 
 <->  ( f  e.  C  /\  dom  f  =  ( { x }  u.  trCl
 ( x ,  A ,  R ) ) ) )   &    |-  D  =  { x  e.  A  |  -.  E. f ta }   &    |-  ( ps 
 <->  ( R  FrSe  A  /\  D  =/=  (/) ) )   &    |-  ( ch 
 <->  ( ps  /\  x  e.  D  /\  A. y  e.  D  -.  y R x ) )   &    |-  ( ta'  <->  [. y  /  x ]. ta )   &    |-  H  =  {
 f  |  E. y  e.  pred  ( x ,  A ,  R ) ta'
 }   &    |-  P  =  U. H   &    |-  Z  =  <. x ,  ( P  |`  pred ( x ,  A ,  R )
 ) >.   &    |-  Q  =  ( P  u.  { <. x ,  ( G `  Z )
 >. } )   &    |-  W  =  <. z ,  ( Q  |`  pred (
 z ,  A ,  R ) ) >.   &    |-  E  =  ( { x }  u.  trCl ( x ,  A ,  R )
 )   &    |-  ( ch  ->  P  Fn  trCl ( x ,  A ,  R )
 )   &    |-  ( ch  ->  Q  Fn  ( { x }  u.  trCl ( x ,  A ,  R )
 ) )   =>    |-  ( ch  ->  A. z  e.  E  ( Q `  z )  =  ( G `  W ) )
 
Theorembnj1452 33187* Technical lemma for bnj60 33197. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
 |-  B  =  { d  |  ( d  C_  A  /\  A. x  e.  d  pred ( x ,  A ,  R )  C_  d ) }   &    |-  Y  =  <. x ,  ( f  |`  pred
 ( x ,  A ,  R ) ) >.   &    |-  C  =  { f  |  E. d  e.  B  (
 f  Fn  d  /\  A. x  e.  d  ( f `  x )  =  ( G `  Y ) ) }   &    |-  ( ta 
 <->  ( f  e.  C  /\  dom  f  =  ( { x }  u.  trCl
 ( x ,  A ,  R ) ) ) )   &    |-  D  =  { x  e.  A  |  -.  E. f ta }   &    |-  ( ps 
 <->  ( R  FrSe  A  /\  D  =/=  (/) ) )   &    |-  ( ch 
 <->  ( ps  /\  x  e.  D  /\  A. y  e.  D  -.  y R x ) )   &    |-  ( ta'  <->  [. y  /  x ]. ta )   &    |-  H  =  {
 f  |  E. y  e.  pred  ( x ,  A ,  R ) ta'
 }   &    |-  P  =  U. H   &    |-  Z  =  <. x ,  ( P  |`  pred ( x ,  A ,  R )
 ) >.   &    |-  Q  =  ( P  u.  { <. x ,  ( G `  Z )
 >. } )   &    |-  W  =  <. z ,  ( Q  |`  pred (
 z ,  A ,  R ) ) >.   &    |-  E  =  ( { x }  u.  trCl ( x ,  A ,  R )
 )   =>    |-  ( ch  ->  E  e.  B )
 
Theorembnj1466 33188* Technical lemma for bnj60 33197. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
 |-  B  =  { d  |  ( d  C_  A  /\  A. x  e.  d  pred ( x ,  A ,  R )  C_  d ) }   &    |-  Y  =  <. x ,  ( f  |`  pred
 ( x ,  A ,  R ) ) >.   &    |-  C  =  { f  |  E. d  e.  B  (
 f  Fn  d  /\  A. x  e.  d  ( f `  x )  =  ( G `  Y ) ) }   &    |-  ( ta 
 <->  ( f  e.  C  /\  dom  f  =  ( { x }  u.  trCl
 ( x ,  A ,  R ) ) ) )   &    |-  D  =  { x  e.  A  |  -.  E. f ta }   &    |-  ( ps 
 <->  ( R  FrSe  A  /\  D  =/=  (/) ) )   &    |-  ( ch 
 <->  ( ps  /\  x  e.  D  /\  A. y  e.  D  -.  y R x ) )   &    |-  ( ta'  <->  [. y  /  x ]. ta )   &    |-  H  =  {
 f  |  E. y  e.  pred  ( x ,  A ,  R ) ta'
 }   &    |-  P  =  U. H   &    |-  Z  =  <. x ,  ( P  |`  pred ( x ,  A ,  R )
 ) >.   &    |-  Q  =  ( P  u.  { <. x ,  ( G `  Z )
 >. } )   =>    |-  ( w  e.  Q  ->  A. f  w  e.  Q )
 
Theorembnj1467 33189* Technical lemma for bnj60 33197. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
 |-  B  =  { d  |  ( d  C_  A  /\  A. x  e.  d  pred ( x ,  A ,  R )  C_  d ) }   &    |-  Y  =  <. x ,  ( f  |`  pred
 ( x ,  A ,  R ) ) >.   &    |-  C  =  { f  |  E. d  e.  B  (
 f  Fn  d  /\  A. x  e.  d  ( f `  x )  =  ( G `  Y ) ) }   &    |-  ( ta 
 <->  ( f  e.  C  /\  dom  f  =  ( { x }  u.  trCl
 ( x ,  A ,  R ) ) ) )   &    |-  D  =  { x  e.  A  |  -.  E. f ta }   &    |-  ( ps 
 <->  ( R  FrSe  A  /\  D  =/=  (/) ) )   &    |-  ( ch 
 <->  ( ps  /\  x  e.  D  /\  A. y  e.  D  -.  y R x ) )   &    |-  ( ta'  <->  [. y  /  x ]. ta )   &    |-  H  =  {
 f  |  E. y  e.  pred  ( x ,  A ,  R ) ta'
 }   &    |-  P  =  U. H   &    |-  Z  =  <. x ,  ( P  |`  pred ( x ,  A ,  R )
 ) >.   &    |-  Q  =  ( P  u.  { <. x ,  ( G `  Z )
 >. } )   =>    |-  ( w  e.  Q  ->  A. d  w  e.  Q )
 
Theorembnj1463 33190* Technical lemma for bnj60 33197. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
 |-  B  =  { d  |  ( d  C_  A  /\  A. x  e.  d  pred ( x ,  A ,  R )  C_  d ) }   &    |-  Y  =  <. x ,  ( f  |`  pred
 ( x ,  A ,  R ) ) >.   &    |-  C  =  { f  |  E. d  e.  B  (
 f  Fn  d  /\  A. x  e.  d  ( f `  x )  =  ( G `  Y ) ) }   &    |-  ( ta 
 <->  ( f  e.  C  /\  dom  f  =  ( { x }  u.  trCl
 ( x ,  A ,  R ) ) ) )   &    |-  D  =  { x  e.  A  |  -.  E. f ta }   &    |-  ( ps 
 <->  ( R  FrSe  A  /\  D  =/=  (/) ) )   &    |-  ( ch 
 <->  ( ps  /\  x  e.  D  /\  A. y  e.  D  -.  y R x ) )   &    |-  ( ta'  <->  [. y  /  x ]. ta )   &    |-  H  =  {
 f  |  E. y  e.  pred  ( x ,  A ,  R ) ta'
 }   &    |-  P  =  U. H   &    |-  Z  =  <. x ,  ( P  |`  pred ( x ,  A ,  R )
 ) >.   &    |-  Q  =  ( P  u.  { <. x ,  ( G `  Z )
 >. } )   &    |-  W  =  <. z ,  ( Q  |`  pred (
 z ,  A ,  R ) ) >.   &    |-  E  =  ( { x }  u.  trCl ( x ,  A ,  R )
 )   &    |-  ( ch  ->  Q  e.  _V )   &    |-  ( ch  ->  A. z  e.  E  ( Q `  z )  =  ( G `  W ) )   &    |-  ( ch  ->  Q  Fn  E )   &    |-  ( ch  ->  E  e.  B )   =>    |-  ( ch  ->  Q  e.  C )
 
Theorembnj1489 33191* Technical lemma for bnj60 33197. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
 |-  B  =  { d  |  ( d  C_  A  /\  A. x  e.  d  pred ( x ,  A ,  R )  C_  d ) }   &    |-  Y  =  <. x ,  ( f  |`  pred
 ( x ,  A ,  R ) ) >.   &    |-  C  =  { f  |  E. d  e.  B  (
 f  Fn  d  /\  A. x  e.  d  ( f `  x )  =  ( G `  Y ) ) }   &    |-  ( ta 
 <->  ( f  e.  C  /\  dom  f  =  ( { x }  u.  trCl
 ( x ,  A ,  R ) ) ) )   &    |-  D  =  { x  e.  A  |  -.  E. f ta }   &    |-  ( ps 
 <->  ( R  FrSe  A  /\  D  =/=  (/) ) )   &    |-  ( ch 
 <->  ( ps  /\  x  e.  D  /\  A. y  e.  D  -.  y R x ) )   &    |-  ( ta'  <->  [. y  /  x ]. ta )   &    |-  H  =  {
 f  |  E. y  e.  pred  ( x ,  A ,  R ) ta'
 }   &    |-  P  =  U. H   &    |-  Z  =  <. x ,  ( P  |`  pred ( x ,  A ,  R )
 ) >.   &    |-  Q  =  ( P  u.  { <. x ,  ( G `  Z )
 >. } )   =>    |-  ( ch  ->  Q  e.  _V )
 
Theorembnj1491 33192* Technical lemma for bnj60 33197. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
 |-  B  =  { d  |  ( d  C_  A  /\  A. x  e.  d  pred ( x ,  A ,  R )  C_  d ) }   &    |-  Y  =  <. x ,  ( f  |`  pred
 ( x ,  A ,  R ) ) >.   &    |-  C  =  { f  |  E. d  e.  B  (
 f  Fn  d  /\  A. x  e.  d  ( f `  x )  =  ( G `  Y ) ) }   &    |-  ( ta 
 <->  ( f  e.  C  /\  dom  f  =  ( { x }  u.  trCl
 ( x ,  A ,  R ) ) ) )   &    |-  D  =  { x  e.  A  |  -.  E. f ta }   &    |-  ( ps 
 <->  ( R  FrSe  A  /\  D  =/=  (/) ) )   &    |-  ( ch 
 <->  ( ps  /\  x  e.  D  /\  A. y  e.  D  -.  y R x ) )   &    |-  ( ta'  <->  [. y  /  x ]. ta )   &    |-  H  =  {
 f  |  E. y  e.  pred  ( x ,  A ,  R ) ta'
 }   &    |-  P  =  U. H   &    |-  Z  =  <. x ,  ( P  |`  pred ( x ,  A ,  R )
 ) >.   &    |-  Q  =  ( P  u.  { <. x ,  ( G `  Z )
 >. } )   &    |-  ( ch  ->  ( Q  e.  C  /\  dom 
 Q  =  ( { x }  u.  trCl ( x ,  A ,  R ) ) ) )   =>    |-  ( ( ch  /\  Q  e.  _V )  ->  E. f ( f  e.  C  /\  dom  f  =  ( { x }  u.  trCl ( x ,  A ,  R ) ) ) )
 
Theorembnj1312 33193* Technical lemma for bnj60 33197. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
 |-  B  =  { d  |  ( d  C_  A  /\  A. x  e.  d  pred ( x ,  A ,  R )  C_  d ) }   &    |-  Y  =  <. x ,  ( f  |`  pred
 ( x ,  A ,  R ) ) >.   &    |-  C  =  { f  |  E. d  e.  B  (
 f  Fn  d  /\  A. x  e.  d  ( f `  x )  =  ( G `  Y ) ) }   &    |-  ( ta 
 <->  ( f  e.  C  /\  dom  f  =  ( { x }  u.  trCl
 ( x ,  A ,  R ) ) ) )   &    |-  D  =  { x  e.  A  |  -.  E. f ta }   &    |-  ( ps 
 <->  ( R  FrSe  A  /\  D  =/=  (/) ) )   &    |-  ( ch 
 <->  ( ps  /\  x  e.  D  /\  A. y  e.  D  -.  y R x ) )   &    |-  ( ta'  <->  [. y  /  x ]. ta )   &    |-  H  =  {
 f  |  E. y  e.  pred  ( x ,  A ,  R ) ta'
 }   &    |-  P  =  U. H   &    |-  Z  =  <. x ,  ( P  |`  pred ( x ,  A ,  R )
 ) >.   &    |-  Q  =  ( P  u.  { <. x ,  ( G `  Z )
 >. } )   &    |-  W  =  <. z ,  ( Q  |`  pred (
 z ,  A ,  R ) ) >.   &    |-  E  =  ( { x }  u.  trCl ( x ,  A ,  R )
 )   =>    |-  ( R  FrSe  A  ->  A. x  e.  A  E. f  e.  C  dom  f  =  ( { x }  u.  trCl ( x ,  A ,  R ) ) )
 
Theorembnj1493 33194* Technical lemma for bnj60 33197. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
 |-  B  =  { d  |  ( d  C_  A  /\  A. x  e.  d  pred ( x ,  A ,  R )  C_  d ) }   &    |-  Y  =  <. x ,  ( f  |`  pred
 ( x ,  A ,  R ) ) >.   &    |-  C  =  { f  |  E. d  e.  B  (
 f  Fn  d  /\  A. x  e.  d  ( f `  x )  =  ( G `  Y ) ) }   =>    |-  ( R  FrSe  A  ->  A. x  e.  A  E. f  e.  C  dom  f  =  ( { x }  u.  trCl ( x ,  A ,  R )
 ) )
 
Theorembnj1497 33195* Technical lemma for bnj60 33197. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
 |-  B  =  { d  |  ( d  C_  A  /\  A. x  e.  d  pred ( x ,  A ,  R )  C_  d ) }   &    |-  Y  =  <. x ,  ( f  |`  pred
 ( x ,  A ,  R ) ) >.   &    |-  C  =  { f  |  E. d  e.  B  (
 f  Fn  d  /\  A. x  e.  d  ( f `  x )  =  ( G `  Y ) ) }   =>    |-  A. g  e.  C  Fun  g
 
Theorembnj1498 33196* Technical lemma for bnj60 33197. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
 |-  B  =  { d  |  ( d  C_  A  /\  A. x  e.  d  pred ( x ,  A ,  R )  C_  d ) }   &    |-  Y  =  <. x ,  ( f  |`  pred
 ( x ,  A ,  R ) ) >.   &    |-  C  =  { f  |  E. d  e.  B  (
 f  Fn  d  /\  A. x  e.  d  ( f `  x )  =  ( G `  Y ) ) }   &    |-  F  =  U. C   =>    |-  ( R  FrSe  A  ->  dom 
 F  =  A )
 
21.28.5  Well-founded recursion, part 1 of 3
 
Theorembnj60 33197* Well-founded recursion, part 1 of 3. The proof has been taken from Chapter 4 of Don Monk's notes on Set Theory. See http://euclid.colorado.edu/~monkd/setth.pdf. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
 |-  B  =  { d  |  ( d  C_  A  /\  A. x  e.  d  pred ( x ,  A ,  R )  C_  d ) }   &    |-  Y  =  <. x ,  ( f  |`  pred
 ( x ,  A ,  R ) ) >.   &    |-  C  =  { f  |  E. d  e.  B  (
 f  Fn  d  /\  A. x  e.  d  ( f `  x )  =  ( G `  Y ) ) }   &    |-  F  =  U. C   =>    |-  ( R  FrSe  A  ->  F  Fn  A )
 
Theorembnj1514 33198* Technical lemma for bnj1500 33203. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
 |-  B  =  { d  |  ( d  C_  A  /\  A. x  e.  d  pred ( x ,  A ,  R )  C_  d ) }   &    |-  Y  =  <. x ,  ( f  |`  pred
 ( x ,  A ,  R ) ) >.   &    |-  C  =  { f  |  E. d  e.  B  (
 f  Fn  d  /\  A. x  e.  d  ( f `  x )  =  ( G `  Y ) ) }   =>    |-  (
 f  e.  C  ->  A. x  e.  dom  f
 ( f `  x )  =  ( G `  Y ) )
 
Theorembnj1518 33199* Technical lemma for bnj1500 33203. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
 |-  B  =  { d  |  ( d  C_  A  /\  A. x  e.  d  pred ( x ,  A ,  R )  C_  d ) }   &    |-  Y  =  <. x ,  ( f  |`  pred
 ( x ,  A ,  R ) ) >.   &    |-  C  =  { f  |  E. d  e.  B  (
 f  Fn  d  /\  A. x  e.  d  ( f `  x )  =  ( G `  Y ) ) }   &    |-  F  =  U. C   &    |-  ( ph  <->  ( R  FrSe  A 
 /\  x  e.  A ) )   &    |-  ( ps  <->  ( ph  /\  f  e.  C  /\  x  e. 
 dom  f ) )   =>    |-  ( ps  ->  A. d ps )
 
Theorembnj1519 33200* Technical lemma for bnj1500 33203. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
 |-  B  =  { d  |  ( d  C_  A  /\  A. x  e.  d  pred ( x ,  A ,  R )  C_  d ) }   &    |-  Y  =  <. x ,  ( f  |`  pred
 ( x ,  A ,  R ) ) >.   &    |-  C  =  { f  |  E. d  e.  B  (
 f  Fn  d  /\  A. x  e.  d  ( f `  x )  =  ( G `  Y ) ) }   &    |-  F  =  U. C   =>    |-  ( ( F `  x )  =  ( G `  <. x ,  ( F  |`  pred ( x ,  A ,  R )
 ) >. )  ->  A. d
 ( F