HomeHome Metamath Proof Explorer
Theorem List (p. 294 of 328)
< 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-21514)
  Hilbert Space Explorer  Hilbert Space Explorer
(21515-23037)
  Users' Mathboxes  Users' Mathboxes
(23038-32776)
 

Theorem List for Metamath Proof Explorer - 29301-29400   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theorembnj986 29301* Technical lemma for bnj69 29355. 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  \  { (/) } )   &    |-  ( ta 
 <->  ( m  e.  om  /\  n  =  suc  m  /\  p  =  suc  n ) )   =>    |-  ( ch  ->  E. m E. p ta )
 
Theorembnj996 29302* Technical lemma for bnj69 29355. 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 E. p ( th  ->  ( ch  /\  ta  /\  et ) )
 
Theorembnj998 29303* Technical lemma for bnj69 29355. 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 ) )   &    |-  ( 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 >. } )   =>    |-  (
 ( th  /\  ch  /\  ta 
 /\  et )  ->  ch" )
 
Theorembnj999 29304* Technical lemma for bnj69 29355. 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 ) )   &    |-  ( ph'  <->  [. p  /  n ].
 ph )   &    |-  ( ps'  <->  [. p  /  n ].
 ps )   &    |-  ( ch'  <->  [. p  /  n ].
 ch )   &    |-  ( ph"  <->  [. G  /  f ]. ph' )   &    |-  ( ps"  <->  [. G  /  f ]. ps' )   &    |-  ( ch"  <->  [. G  /  f ]. ch' )   &    |-  C  =  U_ y  e.  ( f `  m )  pred (
 y ,  A ,  R )   &    |-  G  =  ( f  u.  { <. n ,  C >. } )   =>    |-  (
 ( ch"  /\  i  e.  om 
 /\  suc  i  e.  p  /\  y  e.  ( G `  i ) ) 
 ->  pred ( y ,  A ,  R ) 
 C_  ( G `  suc  i ) )
 
Theorembnj1001 29305 Technical lemma for bnj69 29355. 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 )
 )   &    |-  ( ta  <->  ( m  e. 
 om  /\  n  =  suc  m  /\  p  = 
 suc  n ) )   &    |-  ( et  <->  ( i  e.  n  /\  y  e.  ( f `  i
 ) ) )   &    |-  D  =  ( om  \  { (/)
 } )   &    |-  ( ( th  /\ 
 ch  /\  ta  /\  et )  ->  ch" )   =>    |-  ( ( th  /\  ch 
 /\  ta  /\  et )  ->  ( ch"  /\  i  e.  om 
 /\  suc  i  e.  p ) )
 
Theorembnj1006 29306* Technical lemma for bnj69 29355. 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  \  { (/) } )   &    |-  C  =  U_ y  e.  (
 f `  m )  pred ( y ,  A ,  R )   &    |-  G  =  ( f  u.  { <. n ,  C >. } )   &    |-  (
 ( th  /\  ch  /\  ta 
 /\  et )  ->  ( ch"  /\  i  e.  om  /\  suc  i  e.  p ) )   =>    |-  ( ( th  /\  ch 
 /\  ta  /\  et )  -> 
 pred ( y ,  A ,  R ) 
 C_  ( G `  suc  i ) )
 
Theorembnj1014 29307* Technical lemma for bnj69 29355. 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 ) }   =>    |-  ( ( g  e.  B  /\  j  e.  dom  g )  ->  ( g `  j
 )  C_  trCl ( X ,  A ,  R ) )
 
Theorembnj1015 29308* Technical lemma for bnj69 29355. 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 ) }   &    |-  G  e.  V   &    |-  J  e.  V   =>    |-  (
 ( G  e.  B  /\  J  e.  dom  G )  ->  ( G `  J )  C_  trCl ( X ,  A ,  R ) )
 
Theorembnj1018 29309* Technical lemma for bnj69 29355. 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 ) )   &    |-  ( 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 >. } )   &    |-  ( ch"  <->  ( p  e.  D  /\  G  Fn  p  /\  ph"  /\  ps" ) )   &    |-  ( ( th  /\  ch 
 /\  ta  /\  et )  ->  ch" )   &    |-  ( ( th  /\ 
 ch  /\  ta  /\  et )  ->  ( ch"  /\  i  e.  om  /\  suc  i  e.  p ) )   =>    |-  ( ( th  /\ 
 ch  /\  et  /\  E. p ta )  ->  ( G `  suc  i ) 
 C_  trCl ( X ,  A ,  R )
 )
 
Theorembnj1020 29310* Technical lemma for bnj69 29355. 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 >. } )   &    |-  ( ch"  <->  ( p  e.  D  /\  G  Fn  p  /\  ph"  /\  ps" ) )   =>    |-  ( ( th  /\  ch 
 /\  et  /\  E. p ta )  ->  pred (
 y ,  A ,  R )  C_  trCl ( X ,  A ,  R ) )
 
Theorembnj1021 29311* Technical lemma for bnj69 29355. 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 29312* Technical lemma for bnj69 29355. 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 29313 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 29314* Technical lemma for bnj69 29355. 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 29315* Technical lemma for bnj69 29355. 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 29316 Technical lemma for bnj69 29355. 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 29317* Technical lemma for bnj69 29355. 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 29318 Technical lemma for bnj69 29355. 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 29319 Technical lemma for bnj69 29355. 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 29320* Technical lemma for bnj69 29355. 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 29321* Technical lemma for bnj69 29355. 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 29322 Technical lemma for bnj69 29355. 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 29323 Technical lemma for bnj69 29355. 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 29324* Technical lemma for bnj69 29355. 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 29325* Technical lemma for bnj69 29355. 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 29326 Technical lemma for bnj69 29355. 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 29327* Technical lemma for bnj69 29355. 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 29328* Technical lemma for bnj69 29355. 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 29329* Technical lemma for bnj69 29355. 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 29330 Technical lemma for bnj69 29355. 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 29331* Technical lemma for bnj69 29355. 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 29332* Technical lemma for bnj69 29355. 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 29333 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 29334* Technical lemma for bnj69 29355. 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 29335* Technical lemma for bnj69 29355. 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 29336 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 29337 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 29338* Technical lemma for bnj69 29355. 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 29339 Property of  trCl. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
 |-  trCl ( X ,  A ,  R )  C_  A
 
Theorembnj1137 29340* 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 29341 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 29342* Technical lemma for bnj69 29355. 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 29343 Technical lemma for bnj69 29355. 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 29344* 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 29345 Technical lemma for bnj69 29355. 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 29346 Technical lemma for bnj69 29355. 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 29347 Technical lemma for bnj69 29355. 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 29348 Technical lemma for bnj69 29355. 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 29349 Technical lemma for bnj69 29355. 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 29350* Technical lemma for bnj69 29355. 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 29351 Technical lemma for bnj69 29355. 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 29352* Technical lemma for bnj69 29355. 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 29353* Technical lemma for bnj69 29355. 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 29354* Technical lemma for bnj69 29355. 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 )
 
18.26.3  The existence of a minimal element in certain classes
 
Theorembnj69 29355* Existence of a minimal element in certain classes: if  R is well-founded and set-like on 
A, then every non-empty 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 29356* Existence of a minimal element in certain classes: if  R is well-founded and set-like on 
A, then every non-empty 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 )
 
18.26.4  Well-founded induction
 
Theorembnj1204 29357* 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 29358* Technical lemma for bnj60 29407. 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 29359* Technical lemma for bnj60 29407. 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 29360* Technical lemma for bnj60 29407. 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 29361* Technical lemma for bnj60 29407. 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 29362* Technical lemma for bnj60 29407. 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 29363* Technical lemma for bnj60 29407. 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 29364* Technical lemma for bnj60 29407. 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 29365* Technical lemma for bnj60 29407. 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 29366* Technical lemma for bnj60 29407. 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 29367* Technical lemma for bnj60 29407. 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 29368* Technical lemma for bnj60 29407. 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 29369* Technical lemma for bnj60 29407. 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 29370 Technical lemma for bnj60 29407. 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 29371* Technical lemma for bnj60 29407. 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 29372* Technical lemma for bnj60 29407. 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 29373 Property of  FrSe. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
 |-  ( R  FrSe  A  ->  R  Se  A )
 
Theorembnj1371 29374* Technical lemma for bnj60 29407. 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 29375* Technical lemma for bnj60 29407. 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 29376* Technical lemma for bnj60 29407. 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 29377* Technical lemma for bnj60 29407. 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 29378* Technical lemma for bnj60 29407. 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 29379* Technical lemma for bnj60 29407. 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 29380* 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 29381* Technical lemma for bnj1414 29382. 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 29382* 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 29383* Technical lemma for bnj60 29407. 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 29384 Technical lemma for bnj60 29407. 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 29385 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 29386* Technical lemma for bnj60 29407. 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 29387* Technical lemma for bnj60 29407. 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 29388* Technical lemma for bnj60 29407. 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 29389* Technical lemma for bnj60 29407. 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 29390* Technical lemma for bnj60 29407. 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 29391* Technical lemma for bnj60 29407. 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 29392* Technical lemma for bnj60 29407. 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 29393* Technical lemma for bnj60 29407. 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 29394* Technical lemma for bnj60 29407. 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 29395* Technical lemma for bnj60 29407. 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 29396* Technical lemma for bnj60 29407. 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 29397* Technical lemma for bnj60 29407. 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 29398* Technical lemma for bnj60 29407. 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  |  -.