P. 310 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 30901-31000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	bnj1379 30901*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
|- ( ph <-> A. f e. A Fun f )   &    |- D = ( dom f i^i dom g )   &    |- ( ps <-> ( ph /\ A. f e. A A. g e. A ( f |` D ) = ( g |` D ) ) )   &    |- ( ch <-> ( ps /\ <. x , y >. e. U. A /\ <. x , z >. e. U. A ) )   &    |- ( th <-> ( ch /\ f e. A /\ <. x , y >. e. f ) )   &    |- ( ta <-> ( th /\ g e. A /\ <. x , z >. e. g ) )   =>    |- ( ps -> Fun U. A )
Theorem	bnj1383 30902*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
|- ( ph <-> A. f e. A Fun f )   &    |- D = ( dom f i^i dom g )   &    |- ( ps <-> ( ph /\ A. f e. A A. g e. A ( f |` D ) = ( g |` D ) ) )   =>    |- ( ps -> Fun U. A )
Theorem	bnj1385 30903*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
|- ( ph <-> A. f e. A Fun f )   &    |- D = ( dom f i^i dom g )   &    |- ( ps <-> ( ph /\ A. f e. A A. g e. A ( f |` D ) = ( g |` D ) ) )   &    |- ( x e. A -> A. f x e. A )   &    |- ( ph' <-> A. h e. A Fun h )   &    |- E = ( dom h i^i dom g )   &    |- ( ps' <-> ( ph' /\ A. h e. A A. g e. A ( h |` E ) = ( g |` E ) ) )   =>    |- ( ps -> Fun U. A )
Theorem	bnj1386 30904*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
|- ( ph <-> A. f e. A Fun f )   &    |- D = ( dom f i^i dom g )   &    |- ( ps <-> ( ph /\ A. f e. A A. g e. A ( f |` D ) = ( g |` D ) ) )   &    |- ( x e. A -> A. f x e. A )   =>    |- ( ps -> Fun U. A )
Theorem	bnj1397 30905	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
|- ( ph -> E. x ps )   &    |- ( ps -> A. x ps )   =>    |- ( ph -> ps )
Theorem	bnj1400 30906*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
|- ( y e. A -> A. x y e. A )   =>    |- dom U. A = U_ x e. A dom x
Theorem	bnj1405 30907*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
|- ( ph -> X e. U_ y e. A B )   =>    |- ( ph -> E. y e. A X e. B )
Theorem	bnj1422 30908	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
|- ( ph -> Fun A )   &    |- ( ph -> dom A = B )   =>    |- ( ph -> A Fn B )
Theorem	bnj1424 30909	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
|- A = ( B u. C )   =>    |- ( D e. A -> ( D e. B \/ D e. C ) )
Theorem	bnj1436 30910	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
|- A = { x | ph }   =>    |- ( x e. A -> ph )
Theorem	bnj1441 30911*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
|- ( x e. A -> A. y x e. A )   &    |- ( ph -> A. y ph )   =>    |- ( z e. { x e. A | ph } -> A. y z e. { x e. A | ph } )
Theorem	bnj1454 30912	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
|- A = { x | ph }   =>    |- ( B e. _V -> ( B e. A <-> [. B / x ]. ph ) )
Theorem	bnj1459 30913*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
|- ( ps <-> ( ph /\ x e. A ) )   &    |- ( ps -> ch )   =>    |- ( ph -> A. x e. A ch )
Theorem	bnj1464 30914*	Conversion of implicit substitution to explicit class substitution. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
|- ( ps -> A. x ps )   &    |- ( x = A -> ( ph <-> ps ) )   =>    |- ( A e. V -> ( [. A / x ]. ph <-> ps ) )
Theorem	bnj1465 30915*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
|- ( x = A -> ( ph <-> ps ) )   &    |- ( ps -> A. x ps )   &    |- ( ch -> ps )   =>    |- ( ( ch /\ A e. V ) -> E. x ph )
Theorem	bnj1468 30916*	Conversion of implicit substitution to explicit class substitution. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
|- ( ps -> A. x ps )   &    |- ( x = A -> ( ph <-> ps ) )   &    |- ( y e. A -> A. x y e. A )   =>    |- ( A e. V -> ( [. A / x ]. ph <-> ps ) )
Theorem	bnj1476 30917	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
|- D = { x e. A | -. ph }   &    |- ( ps -> D = (/) )   =>    |- ( ps -> A. x e. A ph )
Theorem	bnj1502 30918	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
|- ( ph -> Fun F )   &    |- ( ph -> G C_ F )   &    |- ( ph -> A e. dom G )   =>    |- ( ph -> ( F ` A ) = ( G ` A ) )
Theorem	bnj1503 30919	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
|- ( ph -> Fun F )   &    |- ( ph -> G C_ F )   &    |- ( ph -> A C_ dom G )   =>    |- ( ph -> ( F |` A ) = ( G |` A ) )
Theorem	bnj1517 30920	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
|- A = { x | ( ph /\ ps ) }   =>    |- ( x e. A -> ps )
Theorem	bnj1521 30921	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
|- ( ch -> E. x e. B ph )   &    |- ( th <-> ( ch /\ x e. B /\ ph ) )   &    |- ( ch -> A. x ch )   =>    |- ( ch -> E. x th )
Theorem	bnj1533 30922	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
|- ( th -> A. z e. B -. z e. D )   &    |- B C_ A   &    |- D = { z e. A | C =/= E }   =>    |- ( th -> A. z e. B C = E )
Theorem	bnj1534 30923*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
|- D = { x e. A | ( F ` x ) =/= ( H ` x ) }   &    |- ( w e. F -> A. x w e. F )   =>    |- D = { z e. A | ( F ` z ) =/= ( H ` z ) }
Theorem	bnj1536 30924*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
|- ( ph -> F Fn A )   &    |- ( ph -> G Fn A )   &    |- ( ph -> B C_ A )   &    |- ( ph -> A. x e. B ( F ` x ) = ( G ` x ) )   =>    |- ( ph -> ( F |` B ) = ( G |` B ) )
Theorem	bnj1538 30925	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
|- A = { x e. B | ph }   =>    |- ( x e. A -> ph )
Theorem	bnj1541 30926	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
|- ( ph <-> ( ps /\ A =/= B ) )   &    |- -. ph   =>    |- ( ps -> A = B )
Theorem	bnj1542 30927*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
|- ( ph -> F Fn A )   &    |- ( ph -> G Fn A )   &    |- ( ph -> F =/= G )   &    |- ( w e. F -> A. x w e. F )   =>    |- ( ph -> E. x e. A ( F ` x ) =/= ( G ` x ) )
20.4.2  Well founded induction and recursion
Theorem	bnj110 30928*	Well-founded induction restricted to a set ( A e. _V). 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.)
|- A e. _V   &    |- ( ps <-> A. y e. A ( y R x -> [. y / x ]. ph ) )   =>    |- ( ( R Fr A /\ A. x e. A ( ps -> ph ) ) -> A. x e. A ph )
Theorem	bnj157 30929*	Well-founded induction restricted to a set ( A e. _V). 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 ) )   &    |- A e. _V   &    |- R Fr A   =>    |- ( A. x e. A ( ps -> ph ) -> A. x e. A ph )
Theorem	bnj66 30930*	Technical lemma for bnj60 31130. 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 ) ) }   =>    |- ( g e. C -> Rel g )
Theorem	bnj91 30931*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
|- ( ph <-> ( f ` (/) ) = pred ( x , A , R ) )   &    |- Z e. _V   =>    |- ( [. Z / y ]. ph <-> ( f ` (/) ) = pred ( x , A , R ) )
Theorem	bnj92 30932*	First-order logic and set theory. (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 ) ) )   &    |- Z e. _V   =>    |- ( [. Z / n ]. ps <-> A. i e. om ( suc i e. Z -> ( f ` suc i ) = U_ y e. ( f ` i ) pred ( y , A , R ) ) )
Theorem	bnj93 30933*	Technical lemma for bnj97 30936. 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.)
|- ( ( R FrSe A /\ x e. A ) -> pred ( x , A , R ) e. _V )
Theorem	bnj95 30934	Technical lemma for bnj124 30941. 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.)
|- F = { <. (/) , pred ( x , A , R ) >. }   =>    |- F e. _V
Theorem	bnj96 30935*	Technical lemma for bnj150 30946. 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.) (Revised by Mario Carneiro, 6-May-2015.) (New usage is discouraged.)
|- F = { <. (/) , pred ( x , A , R ) >. }   =>    |- ( ( R FrSe A /\ x e. A ) -> dom F = 1o )
Theorem	bnj97 30936*	Technical lemma for bnj150 30946. 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.)
|- F = { <. (/) , pred ( x , A , R ) >. }   =>    |- ( ( R FrSe A /\ x e. A ) -> ( F ` (/) ) = pred ( x , A , R ) )
Theorem	bnj98 30937	Technical lemma for bnj150 30946. 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.)
|- A. i e. om ( suc i e. 1o -> ( F ` suc i ) = U_ y e. ( F ` i ) pred ( y , A , R ) )
Theorem	bnj106 30938*	First-order logic and set theory. (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 ) ) )   &    |- F e. _V   =>    |- ( [. F / f ]. [. 1o / n ]. ps <-> A. i e. om ( suc i e. 1o -> ( F ` suc i ) = U_ y e. ( F ` i ) pred ( y , A , R ) ) )
Theorem	bnj118 30939*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
|- ( ph <-> ( f ` (/) ) = pred ( x , A , R ) )   &    |- ( ph' <-> [. 1o / n ]. ph )   =>    |- ( ph' <-> ( f ` (/) ) = pred ( x , A , R ) )
Theorem	bnj121 30940*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
|- ( ze <-> ( ( R FrSe A /\ x e. A ) -> ( f Fn n /\ ph /\ ps ) ) )   &    |- ( ze' <-> [. 1o / n ]. ze )   &    |- ( ph' <-> [. 1o / n ]. ph )   &    |- ( ps' <-> [. 1o / n ]. ps )   =>    |- ( ze' <-> ( ( R FrSe A /\ x e. A ) -> ( f Fn 1o /\ ph' /\ ps' ) ) )
Theorem	bnj124 30941*	Technical lemma for bnj150 30946. 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.)
|- F = { <. (/) , pred ( x , A , R ) >. }   &    |- ( ph" <-> [. F / f ]. ph' )   &    |- ( ps" <-> [. F / f ]. ps' )   &    |- ( ze" <-> [. F / f ]. ze' )   &    |- ( ze' <-> ( ( R FrSe A /\ x e. A ) -> ( f Fn 1o /\ ph' /\ ps' ) ) )   =>    |- ( ze" <-> ( ( R FrSe A /\ x e. A ) -> ( F Fn 1o /\ ph" /\ ps" ) ) )
Theorem	bnj125 30942*	Technical lemma for bnj150 30946. 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 ) )   &    |- ( ph' <-> [. 1o / n ]. ph )   &    |- ( ph" <-> [. F / f ]. ph' )   &    |- F = { <. (/) , pred ( x , A , R ) >. }   =>    |- ( ph" <-> ( F ` (/) ) = pred ( x , A , R ) )
Theorem	bnj126 30943*	Technical lemma for bnj150 30946. 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' <-> [. 1o / n ]. ps )   &    |- ( ps" <-> [. F / f ]. ps' )   &    |- F = { <. (/) , pred ( x , A , R ) >. }   =>    |- ( ps" <-> A. i e. om ( suc i e. 1o -> ( F ` suc i ) = U_ y e. ( F ` i ) pred ( y , A , R ) ) )
Theorem	bnj130 30944*	Technical lemma for bnj151 30947. 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 ) -> E! f ( f Fn n /\ ph /\ ps ) ) )   &    |- ( ph' <-> [. 1o / n ]. ph )   &    |- ( ps' <-> [. 1o / n ]. ps )   &    |- ( th' <-> [. 1o / n ]. th )   =>    |- ( th' <-> ( ( R FrSe A /\ x e. A ) -> E! f ( f Fn 1o /\ ph' /\ ps' ) ) )
Theorem	bnj149 30945*	Technical lemma for bnj151 30947. 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.)
|- ( th1 <-> ( ( R FrSe A /\ x e. A ) -> E* f ( f Fn 1o /\ ph' /\ ps' ) ) )   &    |- ( ze0 <-> ( f Fn 1o /\ ph' /\ ps' ) )   &    |- ( ze1 <-> [. g / f ]. ze0 )   &    |- ( ph1 <-> [. g / f ]. ph' )   &    |- ( ps1 <-> [. g / f ]. ps' )   &    |- ( ph' <-> ( f ` (/) ) = pred ( x , A , R ) )   =>    |- th1
Theorem	bnj150 30946*	Technical lemma for bnj151 30947. 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 ) ) )   &    |- ( ze <-> ( ( R FrSe A /\ x e. A ) -> ( f Fn n /\ ph /\ ps ) ) )   &    |- ( ph' <-> [. 1o / n ]. ph )   &    |- ( ps' <-> [. 1o / n ]. ps )   &    |- ( th0 <-> ( ( R FrSe A /\ x e. A ) -> E. f ( f Fn 1o /\ ph' /\ ps' ) ) )   &    |- ( ze' <-> [. 1o / n ]. ze )   &    |- F = { <. (/) , pred ( x , A , R ) >. }   &    |- ( ph" <-> [. F / f ]. ph' )   &    |- ( ps" <-> [. F / f ]. ps' )   &    |- ( ze" <-> [. F / f ]. ze' )   =>    |- th0
Theorem	bnj151 30947*	Technical lemma for bnj153 30950. 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 \ { (/) } )   &    |- ( th <-> ( ( R FrSe A /\ x e. A ) -> E! f ( f Fn n /\ ph /\ ps ) ) )   &    |- ( ta <-> A. m e. D ( m _E n -> [. m / n ]. th ) )   &    |- ( ze <-> ( ( R FrSe A /\ x e. A ) -> ( f Fn n /\ ph /\ ps ) ) )   &    |- ( ph' <-> [. 1o / n ]. ph )   &    |- ( ps' <-> [. 1o / n ]. ps )   &    |- ( th' <-> [. 1o / n ]. th )   &    |- ( th0 <-> ( ( R FrSe A /\ x e. A ) -> E. f ( f Fn 1o /\ ph' /\ ps' ) ) )   &    |- ( th1 <-> ( ( R FrSe A /\ x e. A ) -> E* f ( f Fn 1o /\ ph' /\ ps' ) ) )   &    |- ( ze' <-> [. 1o / n ]. ze )   &    |- F = { <. (/) , pred ( x , A , R ) >. }   &    |- ( ph" <-> [. F / f ]. ph' )   &    |- ( ps" <-> [. F / f ]. ps' )   &    |- ( ze" <-> [. F / f ]. ze' )   &    |- ( ze0 <-> ( f Fn 1o /\ ph' /\ ps' ) )   &    |- ( ze1 <-> [. g / f ]. ze0 )   &    |- ( ph1 <-> [. g / f ]. ph' )   &    |- ( ps1 <-> [. g / f ]. ps' )   =>    |- ( n = 1o -> ( ( n e. D /\ ta ) -> th ) )
Theorem	bnj154 30948*	Technical lemma for bnj153 30950. 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.)
|- ( ph1 <-> [. g / f ]. ph' )   &    |- ( ph' <-> ( f ` (/) ) = pred ( x , A , R ) )   =>    |- ( ph1 <-> ( g ` (/) ) = pred ( x , A , R ) )
Theorem	bnj155 30949*	Technical lemma for bnj153 30950. 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.)
|- ( ps1 <-> [. g / f ]. ps' )   &    |- ( ps' <-> A. i e. om ( suc i e. 1o -> ( f ` suc i ) = U_ y e. ( f ` i ) pred ( y , A , R ) ) )   =>    |- ( ps1 <-> A. i e. om ( suc i e. 1o -> ( g ` suc i ) = U_ y e. ( g ` i ) pred ( y , A , R ) ) )
Theorem	bnj153 30950*	Technical lemma for bnj852 30991. 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 \ { (/) } )   &    |- ( th <-> ( ( R FrSe A /\ x e. A ) -> E! f ( f Fn n /\ ph /\ ps ) ) )   &    |- ( ta <-> A. m e. D ( m _E n -> [. m / n ]. th ) )   =>    |- ( n = 1o -> ( ( n e. D /\ ta ) -> th ) )
Theorem	bnj207 30951*	Technical lemma for bnj852 30991. 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 <-> ( ( R FrSe A /\ x e. A ) -> E! f ( f Fn n /\ ph /\ ps ) ) )   &    |- ( ph' <-> [. M / n ]. ph )   &    |- ( ps' <-> [. M / n ]. ps )   &    |- ( ch' <-> [. M / n ]. ch )   &    |- M e. _V   =>    |- ( ch' <-> ( ( R FrSe A /\ x e. A ) -> E! f ( f Fn M /\ ph' /\ ps' ) ) )
Theorem	bnj213 30952	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
|- pred ( X , A , R ) C_ A
Theorem	bnj222 30953*	Technical lemma for bnj229 30954. 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. m e. om ( suc m e. N -> ( F ` suc m ) = U_ y e. ( F ` m ) pred ( y , A , R ) ) )
Theorem	bnj229 30954*	Technical lemma for bnj517 30955. 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 ) ) )   =>    |- ( ( n e. N /\ ( suc m = n /\ m e. om /\ ps ) ) -> ( F ` n ) C_ A )
Theorem	bnj517 30955*	Technical lemma for bnj518 30956. 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 <-> ( 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 ) ) )   =>    |- ( ( N e. om /\ ph /\ ps ) -> A. n e. N ( F ` n ) C_ A )
Theorem	bnj518 30956*	Technical lemma for bnj852 30991. 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 ) ) )   &    |- ( ta <-> ( ph /\ ps /\ n e. om /\ p e. n ) )   =>    |- ( ( R FrSe A /\ ta ) -> A. y e. ( f ` p ) pred ( y , A , R ) e. _V )
Theorem	bnj523 30957*	Technical lemma for bnj852 30991. 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 ) )   &    |- ( ph' <-> [. M / n ]. ph )   &    |- M e. _V   =>    |- ( ph' <-> ( F ` (/) ) = pred ( X , A , R ) )
Theorem	bnj526 30958*	Technical lemma for bnj852 30991. 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 ) )   &    |- ( ph" <-> [. G / f ]. ph )   &    |- G e. _V   =>    |- ( ph" <-> ( G ` (/) ) = pred ( X , A , R ) )
Theorem	bnj528 30959	Technical lemma for bnj852 30991. 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.)
|- G = ( f u. { <. m , U_ y e. ( f ` p ) pred ( y , A , R ) >. } )   =>    |- G e. _V
Theorem	bnj535 30960*	Technical lemma for bnj852 30991. 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. m -> ( f ` suc i ) = U_ y e. ( f ` i ) pred ( y , A , R ) ) )   &    |- G = ( f u. { <. m , U_ y e. ( f ` p ) pred ( y , A , R ) >. } )   &    |- ( ta <-> ( ph' /\ ps' /\ m e. om /\ p e. m ) )   =>    |- ( ( R FrSe A /\ ta /\ n = ( m u. { m } ) /\ f Fn m ) -> G Fn n )
Theorem	bnj539 30961*	Technical lemma for bnj852 30991. 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' <-> [. M / n ]. ps )   &    |- M e. _V   =>    |- ( ps' <-> A. i e. om ( suc i e. M -> ( F ` suc i ) = U_ y e. ( F ` i ) pred ( y , A , R ) ) )
Theorem	bnj540 30962*	Technical lemma for bnj852 30991. 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" <-> [. G / f ]. ps )   &    |- G e. _V   =>    |- ( ps" <-> A. i e. om ( suc i e. N -> ( G ` suc i ) = U_ y e. ( G ` i ) pred ( y , A , R ) ) )
Theorem	bnj543 30963*	Technical lemma for bnj852 30991. 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. m -> ( f ` suc i ) = U_ y e. ( f ` i ) pred ( y , A , R ) ) )   &    |- G = ( f u. { <. m , U_ y e. ( f ` p ) pred ( y , A , R ) >. } )   &    |- ( ta <-> ( f Fn m /\ ph' /\ ps' ) )   &    |- ( si <-> ( m e. om /\ n = suc m /\ p e. m ) )   =>    |- ( ( R FrSe A /\ ta /\ si ) -> G Fn n )
Theorem	bnj544 30964*	Technical lemma for bnj852 30991. 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. m -> ( f ` suc i ) = U_ y e. ( f ` i ) pred ( y , A , R ) ) )   &    |- D = ( om \ { (/) } )   &    |- G = ( f u. { <. m , U_ y e. ( f ` p ) pred ( y , A , R ) >. } )   &    |- ( ta <-> ( f Fn m /\ ph' /\ ps' ) )   &    |- ( si <-> ( m e. D /\ n = suc m /\ p e. m ) )   =>    |- ( ( R FrSe A /\ ta /\ si ) -> G Fn n )
Theorem	bnj545 30965	Technical lemma for bnj852 30991. 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 ) )   &    |- D = ( om \ { (/) } )   &    |- G = ( f u. { <. m , U_ y e. ( f ` p ) pred ( y , A , R ) >. } )   &    |- ( ta <-> ( f Fn m /\ ph' /\ ps' ) )   &    |- ( si <-> ( m e. D /\ n = suc m /\ p e. m ) )   &    |- ( ( R FrSe A /\ ta /\ si ) -> G Fn n )   &    |- ( ph" <-> ( G ` (/) ) = pred ( x , A , R ) )   =>    |- ( ( R FrSe A /\ ta /\ si ) -> ph" )
Theorem	bnj546 30966*	Technical lemma for bnj852 30991. 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 \ { (/) } )   &    |- ( ta <-> ( f Fn m /\ ph' /\ ps' ) )   &    |- ( si <-> ( m e. D /\ n = suc m /\ p e. m ) )   &    |- ( ph' <-> ( f ` (/) ) = pred ( x , A , R ) )   &    |- ( ps' <-> A. i e. om ( suc i e. m -> ( f ` suc i ) = U_ y e. ( f ` i ) pred ( y , A , R ) ) )   =>    |- ( ( R FrSe A /\ ta /\ si ) -> U_ y e. ( f ` p ) pred ( y , A , R ) e. _V )
Theorem	bnj548 30967*	Technical lemma for bnj852 30991. 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.)
|- ( ta <-> ( f Fn m /\ ph' /\ ps' ) )   &    |- B = U_ y e. ( f ` i ) pred ( y , A , R )   &    |- K = U_ y e. ( G ` i ) pred ( y , A , R )   &    |- G = ( f u. { <. m , C >. } )   &    |- ( ( R FrSe A /\ ta /\ si ) -> G Fn n )   =>    |- ( ( ( R FrSe A /\ ta /\ si ) /\ i e. m ) -> B = K )
Theorem	bnj553 30968*	Technical lemma for bnj852 30991. 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. m -> ( f ` suc i ) = U_ y e. ( f ` i ) pred ( y , A , R ) ) )   &    |- D = ( om \ { (/) } )   &    |- G = ( f u. { <. m , U_ y e. ( f ` p ) pred ( y , A , R ) >. } )   &    |- ( ta <-> ( f Fn m /\ ph' /\ ps' ) )   &    |- ( si <-> ( m e. D /\ n = suc m /\ p e. m ) )   &    |- C = U_ y e. ( f ` p ) pred ( y , A , R )   &    |- G = ( f u. { <. m , C >. } )   &    |- B = U_ y e. ( f ` i ) pred ( y , A , R )   &    |- K = U_ y e. ( G ` i ) pred ( y , A , R )   &    |- L = U_ y e. ( G ` p ) pred ( y , A , R )   &    |- ( ( R FrSe A /\ ta /\ si ) -> G Fn n )   =>    |- ( ( ( R FrSe A /\ ta /\ si ) /\ i e. m /\ p = i ) -> ( G ` m ) = L )
Theorem	bnj554 30969*	Technical lemma for bnj852 30991. 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 <-> ( m e. D /\ n = suc m /\ p e. om /\ m = suc p ) )   &    |- ( ze <-> ( i e. om /\ suc i e. n /\ m = suc i ) )   &    |- K = U_ y e. ( G ` i ) pred ( y , A , R )   &    |- L = U_ y e. ( G ` p ) pred ( y , A , R )   &    |- K = U_ y e. ( G ` i ) pred ( y , A , R )   &    |- L = U_ y e. ( G ` p ) pred ( y , A , R )   =>    |- ( ( et /\ ze ) -> ( ( G ` m ) = L <-> ( G ` suc i ) = K ) )
Theorem	bnj556 30970	Technical lemma for bnj852 30991. 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.)
|- ( si <-> ( m e. D /\ n = suc m /\ p e. m ) )   &    |- ( et <-> ( m e. D /\ n = suc m /\ p e. om /\ m = suc p ) )   =>    |- ( et -> si )
Theorem	bnj557 30971*	Technical lemma for bnj852 30991. 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 \ { (/) } )   &    |- G = ( f u. { <. m , U_ y e. ( f ` p ) pred ( y , A , R ) >. } )   &    |- ( ta <-> ( f Fn m /\ ph' /\ ps' ) )   &    |- ( si <-> ( m e. D /\ n = suc m /\ p e. m ) )   &    |- ( et <-> ( m e. D /\ n = suc m /\ p e. om /\ m = suc p ) )   &    |- ( ze <-> ( i e. om /\ suc i e. n /\ m = suc i ) )   &    |- B = U_ y e. ( f ` i ) pred ( y , A , R )   &    |- C = U_ y e. ( f ` p ) pred ( y , A , R )   &    |- K = U_ y e. ( G ` i ) pred ( y , A , R )   &    |- L = U_ y e. ( G ` p ) pred ( y , A , R )   &    |- G = ( f u. { <. m , C >. } )   &    |- ( ph' <-> ( f ` (/) ) = pred ( x , A , R ) )   &    |- ( ps' <-> A. i e. om ( suc i e. m -> ( f ` suc i ) = U_ y e. ( f ` i ) pred ( y , A , R ) ) )   &    |- ( ( R FrSe A /\ ta /\ si ) -> G Fn n )   =>    |- ( ( R FrSe A /\ ta /\ et /\ ze ) -> ( G ` m ) = L )
Theorem	bnj558 30972*	Technical lemma for bnj852 30991. 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 \ { (/) } )   &    |- G = ( f u. { <. m , U_ y e. ( f ` p ) pred ( y , A , R ) >. } )   &    |- ( ta <-> ( f Fn m /\ ph' /\ ps' ) )   &    |- ( si <-> ( m e. D /\ n = suc m /\ p e. m ) )   &    |- ( et <-> ( m e. D /\ n = suc m /\ p e. om /\ m = suc p ) )   &    |- ( ze <-> ( i e. om /\ suc i e. n /\ m = suc i ) )   &    |- B = U_ y e. ( f ` i ) pred ( y , A , R )   &    |- C = U_ y e. ( f ` p ) pred ( y , A , R )   &    |- K = U_ y e. ( G ` i ) pred ( y , A , R )   &    |- L = U_ y e. ( G ` p ) pred ( y , A , R )   &    |- G = ( f u. { <. m , C >. } )   &    |- ( ph' <-> ( f ` (/) ) = pred ( x , A , R ) )   &    |- ( ps' <-> A. i e. om ( suc i e. m -> ( f ` suc i ) = U_ y e. ( f ` i ) pred ( y , A , R ) ) )   &    |- ( ( R FrSe A /\ ta /\ si ) -> G Fn n )   =>    |- ( ( R FrSe A /\ ta /\ et /\ ze ) -> ( G ` suc i ) = K )
Theorem	bnj561 30973	Technical lemma for bnj852 30991. 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.)
|- ( si <-> ( m e. D /\ n = suc m /\ p e. m ) )   &    |- ( et <-> ( m e. D /\ n = suc m /\ p e. om /\ m = suc p ) )   &    |- ( ( R FrSe A /\ ta /\ si ) -> G Fn n )   =>    |- ( ( R FrSe A /\ ta /\ et ) -> G Fn n )
Theorem	bnj562 30974	Technical lemma for bnj852 30991. 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.)
|- ( si <-> ( m e. D /\ n = suc m /\ p e. m ) )   &    |- ( et <-> ( m e. D /\ n = suc m /\ p e. om /\ m = suc p ) )   &    |- ( ( R FrSe A /\ ta /\ si ) -> ph" )   =>    |- ( ( R FrSe A /\ ta /\ et ) -> ph" )
Theorem	bnj570 30975*	Technical lemma for bnj852 30991. 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 \ { (/) } )   &    |- ( ta <-> ( f Fn m /\ ph' /\ ps' ) )   &    |- ( et <-> ( m e. D /\ n = suc m /\ p e. om /\ m = suc p ) )   &    |- ( rh <-> ( i e. om /\ suc i e. n /\ m =/= suc i ) )   &    |- K = U_ y e. ( G ` i ) pred ( y , A , R )   &    |- G = ( f u. { <. m , C >. } )   &    |- ( ( R FrSe A /\ ta /\ et ) -> G Fn n )   &    |- ( ps' <-> A. i e. om ( suc i e. m -> ( f ` suc i ) = U_ y e. ( f ` i ) pred ( y , A , R ) ) )   =>    |- ( ( R FrSe A /\ ta /\ et /\ rh ) -> ( G ` suc i ) = K )
Theorem	bnj571 30976*	Technical lemma for bnj852 30991. 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 \ { (/) } )   &    |- G = ( f u. { <. m , U_ y e. ( f ` p ) pred ( y , A , R ) >. } )   &    |- ( ta <-> ( f Fn m /\ ph' /\ ps' ) )   &    |- ( si <-> ( m e. D /\ n = suc m /\ p e. m ) )   &    |- ( et <-> ( m e. D /\ n = suc m /\ p e. om /\ m = suc p ) )   &    |- ( ze <-> ( i e. om /\ suc i e. n /\ m = suc i ) )   &    |- B = U_ y e. ( f ` i ) pred ( y , A , R )   &    |- C = U_ y e. ( f ` p ) pred ( y , A , R )   &    |- K = U_ y e. ( G ` i ) pred ( y , A , R )   &    |- L = U_ y e. ( G ` p ) pred ( y , A , R )   &    |- G = ( f u. { <. m , C >. } )   &    |- ( ph' <-> ( f ` (/) ) = pred ( x , A , R ) )   &    |- ( ps' <-> A. i e. om ( suc i e. m -> ( f ` suc i ) = U_ y e. ( f ` i ) pred ( y , A , R ) ) )   &    |- ( ( R FrSe A /\ ta /\ si ) -> G Fn n )   &    |- ( rh <-> ( i e. om /\ suc i e. n /\ m =/= suc i ) )   &    |- ( ( R FrSe A /\ ta /\ et ) -> G Fn n )   &    |- ( ps" <-> A. i e. om ( suc i e. n -> ( G ` suc i ) = U_ y e. ( G ` i ) pred ( y , A , R ) ) )   =>    |- ( ( R FrSe A /\ ta /\ et ) -> ps" )
Theorem	bnj605 30977*	Technical lemma. 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 <-> A. m e. D ( m _E n -> [. m / n ]. ch ) )   &    |- ( ph" <-> [. f / f ]. ph )   &    |- ( ps" <-> [. f / f ]. ps )   &    |- ( ta <-> ( f Fn m /\ ph' /\ ps' ) )   &    |- ( et <-> ( m e. D /\ n = suc m /\ p e. om /\ m = suc p ) )   &    |- f e. _V   &    |- ( ch' <-> ( ( R FrSe A /\ x e. A ) -> E! f ( f Fn m /\ ph' /\ ps' ) ) )   &    |- ( 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 ) ) )   &    |- ( ( n =/= 1o /\ n e. D ) -> E. m E. p et )   &    |- ( ( th /\ m e. D /\ m _E n ) -> ch' )   &    |- ( ( R FrSe A /\ ta /\ et ) -> f Fn n )   &    |- ( ( R FrSe A /\ ta /\ et ) -> ph" )   &    |- ( ( R FrSe A /\ ta /\ et ) -> ps" )   =>    |- ( ( n =/= 1o /\ n e. D /\ th ) -> ( ( R FrSe A /\ x e. A ) -> E. f ( f Fn n /\ ph /\ ps ) ) )
Theorem	bnj581 30978*	Technical lemma for bnj580 30983. 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). (Unnecessary distinct variable restrictions were removed by Andrew Salmon, 9-Jul-2011.) (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
|- ( ch <-> ( f Fn n /\ ph /\ ps ) )   &    |- ( ph' <-> [. g / f ]. ph )   &    |- ( ps' <-> [. g / f ]. ps )   &    |- ( ch' <-> [. g / f ]. ch )   =>    |- ( ch' <-> ( g Fn n /\ ph' /\ ps' ) )
Theorem	bnj589 30979*	Technical lemma for bnj852 30991. 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. k e. om ( suc k e. n -> ( f ` suc k ) = U_ y e. ( f ` k ) pred ( y , A , R ) ) )
Theorem	bnj590 30980	Technical lemma for bnj852 30991. 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 ) ) )   =>    |- ( ( B = suc i /\ ps ) -> ( i e. om -> ( B e. n -> ( f ` B ) = U_ y e. ( f ` i ) pred ( y , A , R ) ) ) )
Theorem	bnj591 30981*	Technical lemma for bnj852 30991. 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 <-> ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) )   =>    |- ( [. k / j ]. th <-> ( ( n e. D /\ ch /\ ch' ) -> ( f ` k ) = ( g ` k ) ) )
Theorem	bnj594 30982*	Technical lemma for bnj852 30991. 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 <-> ( f Fn n /\ ph /\ ps ) )   &    |- D = ( om \ { (/) } )   &    |- ( ph' <-> ( g ` (/) ) = pred ( x , A , R ) )   &    |- ( ps' <-> A. i e. om ( suc i e. n -> ( g ` suc i ) = U_ y e. ( g ` i ) pred ( y , A , R ) ) )   &    |- ( ch' <-> ( g Fn n /\ ph' /\ ps' ) )   &    |- ( th <-> ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) )   &    |- ( [. k / j ]. th <-> ( ( n e. D /\ ch /\ ch' ) -> ( f ` k ) = ( g ` k ) ) )   &    |- ( ta <-> A. k e. n ( k _E j -> [. k / j ]. th ) )   =>    |- ( ( j e. n /\ ta ) -> th )
Theorem	bnj580 30983*	Technical lemma for bnj579 30984. 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 <-> ( f Fn n /\ ph /\ ps ) )   &    |- ( ph' <-> [. g / f ]. ph )   &    |- ( ps' <-> [. g / f ]. ps )   &    |- ( ch' <-> [. g / f ]. ch )   &    |- D = ( om \ { (/) } )   &    |- ( th <-> ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) )   &    |- ( ta <-> A. k e. n ( k _E j -> [. k / j ]. th ) )   =>    |- ( n e. D -> E* f ch )
Theorem	bnj579 30984*	Technical lemma for bnj852 30991. 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 \ { (/) } )   =>    |- ( n e. D -> E* f ( f Fn n /\ ph /\ ps ) )
Theorem	bnj602 30985	Equality theorem for the pred function constant. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
|- ( X = Y -> pred ( X , A , R ) = pred ( Y , A , R ) )
Theorem	bnj607 30986*	Technical lemma for bnj852 30991. 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 <-> A. m e. D ( m _E n -> [. m / n ]. ch ) )   &    |- ( ph" <-> [. G / f ]. ph )   &    |- ( ps" <-> [. G / f ]. ps )   &    |- ( ta <-> ( f Fn m /\ ph' /\ ps' ) )   &    |- ( et <-> ( m e. D /\ n = suc m /\ p e. om /\ m = suc p ) )   &    |- G e. _V   &    |- ( ch' <-> ( ( R FrSe A /\ x e. A ) -> E! f ( f Fn m /\ ph' /\ ps' ) ) )   &    |- ( ph" <-> ( G ` (/) ) = pred ( x , A , R ) )   &    |- ( ps" <-> A. i e. om ( suc i e. n -> ( G ` suc i ) = U_ y e. ( G ` i ) pred ( y , A , R ) ) )   &    |- ( ( n =/= 1o /\ n e. D ) -> E. m E. p et )   &    |- ( ( th /\ m e. D /\ m _E n ) -> ch' )   &    |- ( ( R FrSe A /\ ta /\ et ) -> G Fn n )   &    |- ( ( R FrSe A /\ ta /\ et ) -> ph" )   &    |- ( ( R FrSe A /\ ta /\ et ) -> ps" )   &    |- ( 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 ) ) )   &    |- ( ph0 <-> [. h / f ]. ph )   &    |- ( ps0 <-> [. h / f ]. ps )   &    |- ( ph1 <-> [. G / h ]. ph0 )   &    |- ( ps1 <-> [. G / h ]. ps0 )   =>    |- ( ( n =/= 1o /\ n e. D /\ th ) -> ( ( R FrSe A /\ x e. A ) -> E. f ( f Fn n /\ ph /\ ps ) ) )
Theorem	bnj609 30987*	Technical lemma for bnj852 30991. 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 ) )   &    |- ( ph" <-> [. G / f ]. ph )   &    |- G e. _V   =>    |- ( ph" <-> ( G ` (/) ) = pred ( X , A , R ) )
Theorem	bnj611 30988*	Technical lemma for bnj852 30991. 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" <-> [. G / f ]. ps )   &    |- G e. _V   =>    |- ( ps" <-> A. i e. om ( suc i e. N -> ( G ` suc i ) = U_ y e. ( G ` i ) pred ( y , A , R ) ) )
Theorem	bnj600 30989*	Technical lemma for bnj852 30991. 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 \ { (/) } )   &    |- ( ch <-> ( ( R FrSe A /\ x e. A ) -> E! f ( f Fn n /\ ph /\ ps ) ) )   &    |- ( th <-> A. m e. D ( m _E n -> [. m / n ]. ch ) )   &    |- ( ph' <-> [. m / n ]. ph )   &    |- ( ps' <-> [. m / n ]. ps )   &    |- ( ch' <-> [. m / n ]. ch )   &    |- ( ph" <-> [. G / f ]. ph )   &    |- ( ps" <-> [. G / f ]. ps )   &    |- ( ch" <-> [. G / f ]. ch )   &    |- G = ( f u. { <. m , U_ y e. ( f ` p ) pred ( y , A , R ) >. } )   &    |- ( ta <-> ( f Fn m /\ ph' /\ ps' ) )   &    |- ( si <-> ( m e. D /\ n = suc m /\ p e. m ) )   &    |- ( et <-> ( m e. D /\ n = suc m /\ p e. om /\ m = suc p ) )   &    |- ( ze <-> ( i e. om /\ suc i e. n /\ m = suc i ) )   &    |- ( rh <-> ( i e. om /\ suc i e. n /\ m =/= suc i ) )   &    |- B = U_ y e. ( f ` i ) pred ( y , A , R )   &    |- C = U_ y e. ( f ` p ) pred ( y , A , R )   &    |- K = U_ y e. ( G ` i ) pred ( y , A , R )   &    |- L = U_ y e. ( G ` p ) pred ( y , A , R )   &    |- G = ( f u. { <. m , C >. } )   =>    |- ( n =/= 1o -> ( ( n e. D /\ th ) -> ch ) )
Theorem	bnj601 30990*	Technical lemma for bnj852 30991. 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 \ { (/) } )   &    |- ( ch <-> ( ( R FrSe A /\ x e. A ) -> E! f ( f Fn n /\ ph /\ ps ) ) )   &    |- ( th <-> A. m e. D ( m _E n -> [. m / n ]. ch ) )   =>    |- ( n =/= 1o -> ( ( n e. D /\ th ) -> ch ) )
Theorem	bnj852 30991*	Technical lemma for bnj69 31078. 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 \ { (/) } )   =>    |- ( ( R FrSe A /\ X e. A ) -> A. n e. D E! f ( f Fn n /\ ph /\ ps ) )
Theorem	bnj864 30992*	Technical lemma for bnj69 31078. 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 \ { (/) } )   &    |- ( ch <-> ( R FrSe A /\ X e. A /\ n e. D ) )   &    |- ( th <-> ( f Fn n /\ ph /\ ps ) )   =>    |- ( ch -> E! f th )
Theorem	bnj865 30993*	Technical lemma for bnj69 31078. 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 \ { (/) } )   &    |- ( ch <-> ( R FrSe A /\ X e. A /\ n e. D ) )   &    |- ( th <-> ( f Fn n /\ ph /\ ps ) )   =>    |- E. w A. n ( ch -> E. f e. w th )
Theorem	bnj873 30994*	Technical lemma for bnj69 31078. 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 = { f | E. n e. D ( f Fn n /\ ph /\ ps ) }   &    |- ( ph' <-> [. g / f ]. ph )   &    |- ( ps' <-> [. g / f ]. ps )   =>    |- B = { g | E. n e. D ( g Fn n /\ ph' /\ ps' ) }
Theorem	bnj849 30995*	Technical lemma for bnj69 31078. 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 <-> ( 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 <-> ( R FrSe A /\ X e. A /\ n e. D ) )   &    |- ( th <-> ( f Fn n /\ ph /\ ps ) )   &    |- ( ph' <-> [. g / f ]. ph )   &    |- ( ps' <-> [. g / f ]. ps )   &    |- ( th' <-> [. g / f ]. th )   &    |- ( ta <-> ( R FrSe A /\ X e. A ) )   =>    |- ( ( R FrSe A /\ X e. A ) -> B e. _V )
Theorem	bnj882 30996*	Definition (using hypotheses for readability) of the function giving the transitive closure of X in A by R. (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 ) }   =>    |- trCl ( X , A , R ) = U_ f e. B U_ i e. dom f ( f ` i )
Theorem	bnj18eq1 30997	Equality theorem for transitive closure. (Contributed by Mario Carneiro, 22-Dec-2016.) (New usage is discouraged.)
|- ( X = Y -> trCl ( X , A , R ) = trCl ( Y , A , R ) )
Theorem	bnj893 30998	Property of trCl. Under certain conditions, the transitive closure of X in A by R is a set. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
|- ( ( R FrSe A /\ X e. A ) -> trCl ( X , A , R ) e. _V )
Theorem	bnj900 30999*	Technical lemma for bnj69 31078. 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 \ { (/) } )   &    |- B = { f | E. n e. D ( f Fn n /\ ph /\ ps ) }   =>    |- ( f e. B -> (/) e. dom f )
Theorem	bnj906 31000	Property of trCl. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
|- ( ( R FrSe A /\ X e. A ) -> pred ( X , A , R ) C_ trCl ( X , A , R ) )