P. 87 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 8601-8700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	cnfcom3 8601*	Any infinite ordinal B is equinumerous to a power of om. (We are being careful here to show explicit bijections rather than simple equinumerosity because we want a uniform construction for cnfcom3c 8603.) (Contributed by Mario Carneiro, 28-May-2015.) (Revised by AV, 4-Jul-2019.)
|- S = dom ( om CNF A )   &    |- ( ph -> A e. On )   &    |- ( ph -> B e. ( om ^o A ) )   &    |- F = ( `' ( om CNF A ) ` B )   &    |- G = OrdIso ( _E , ( F supp (/) ) )   &    |- H = seq𝜔 ( ( k e. _V , z e. _V |-> ( M +o z ) ) , (/) )   &    |- T = seq𝜔 ( ( k e. _V , f e. _V |-> K ) , (/) )   &    |- M = ( ( om ^o ( G ` k ) ) .o ( F ` ( G ` k ) ) )   &    |- K = ( ( x e. M |-> ( dom f +o x ) ) u. `' ( x e. dom f |-> ( M +o x ) ) )   &    |- W = ( G ` U. dom G )   &    |- ( ph -> om C_ B )   &    |- X = ( u e. ( F ` W ) , v e. ( om ^o W ) |-> ( ( ( F ` W ) .o v ) +o u ) )   &    |- Y = ( u e. ( F ` W ) , v e. ( om ^o W ) |-> ( ( ( om ^o W ) .o u ) +o v ) )   &    |- N = ( ( X o. `' Y ) o. ( T ` dom G ) )   =>    |- ( ph -> N : B -1-1-onto-> ( om ^o W ) )
Theorem	cnfcom3clem 8602*	Lemma for cnfcom3c 8603. (Contributed by Mario Carneiro, 30-May-2015.) (Revised by AV, 4-Jul-2019.)
|- S = dom ( om CNF A )   &    |- F = ( `' ( om CNF A ) ` b )   &    |- G = OrdIso ( _E , ( F supp (/) ) )   &    |- H = seq𝜔 ( ( k e. _V , z e. _V |-> ( M +o z ) ) , (/) )   &    |- T = seq𝜔 ( ( k e. _V , f e. _V |-> K ) , (/) )   &    |- M = ( ( om ^o ( G ` k ) ) .o ( F ` ( G ` k ) ) )   &    |- K = ( ( x e. M |-> ( dom f +o x ) ) u. `' ( x e. dom f |-> ( M +o x ) ) )   &    |- W = ( G ` U. dom G )   &    |- X = ( u e. ( F ` W ) , v e. ( om ^o W ) |-> ( ( ( F ` W ) .o v ) +o u ) )   &    |- Y = ( u e. ( F ` W ) , v e. ( om ^o W ) |-> ( ( ( om ^o W ) .o u ) +o v ) )   &    |- N = ( ( X o. `' Y ) o. ( T ` dom G ) )   &    |- L = ( b e. ( om ^o A ) |-> N )   =>    |- ( A e. On -> E. g A. b e. A ( om C_ b -> E. w e. ( On \ 1o ) ( g ` b ) : b -1-1-onto-> ( om ^o w ) ) )
Theorem	cnfcom3c 8603*	Wrap the construction of cnfcom3 8601 into an existence quantifier. For any om C_ b, there is a bijection from b to some power of om. Furthermore, this bijection is canonical , which means that we can find a single function g which will give such bijections for every b less than some arbitrarily large bound A. (Contributed by Mario Carneiro, 30-May-2015.)
|- ( A e. On -> E. g A. b e. A ( om C_ b -> E. w e. ( On \ 1o ) ( g ` b ) : b -1-1-onto-> ( om ^o w ) ) )
2.6.4  Transitive closure
Theorem	trcl 8604*	For any set A, show the properties of its transitive closure C. Similar to Theorem 9.1 of [TakeutiZaring] p. 73 except that we show an explicit expression for the transitive closure rather than just its existence. See tz9.1 8605 for an abbreviated version showing existence. (Contributed by NM, 14-Sep-2003.) (Revised by Mario Carneiro, 11-Sep-2015.)
|- A e. _V   &    |- F = ( rec ( ( z e. _V |-> ( z u. U. z ) ) , A ) |` om )   &    |- C = U_ y e. om ( F ` y )   =>    |- ( A C_ C /\ Tr C /\ A. x ( ( A C_ x /\ Tr x ) -> C C_ x ) )
Theorem	tz9.1 8605*	Every set has a transitive closure (the smallest transitive extension). Theorem 9.1 of [TakeutiZaring] p. 73. See trcl 8604 for an explicit expression for the transitive closure. Apparently open problems are whether this theorem can be proved without the Axiom of Infinity; if not, then whether it implies Infinity; and if not, what is the "property" that Infinity has that the other axioms don't have that is weaker than Infinity itself? (Added 22-Mar-2011) The following article seems to answer the first question, that it can't be proved without Infinity, in the affirmative: Mancini, Antonella and Zambella, Domenico (2001). "A note on recursive models of set theories." Notre Dame Journal of Formal Logic, 42(2):109-115. (Thanks to Scott Fenton.) (Contributed by NM, 15-Sep-2003.)
|- A e. _V   =>    |- E. x ( A C_ x /\ Tr x /\ A. y ( ( A C_ y /\ Tr y ) -> x C_ y ) )
Theorem	tz9.1c 8606*	Alternate expression for the existence of transitive closures tz9.1 8605: the intersection of all transitive sets containing A is a set. (Contributed by Mario Carneiro, 22-Mar-2013.)
|- A e. _V   =>    |- |^| { x | ( A C_ x /\ Tr x ) } e. _V
Theorem	epfrs 8607*	The strong form of the Axiom of Regularity (no sethood requirement on A), with the axiom itself present as an antecedent. See also zfregs 8608. (Contributed by Mario Carneiro, 22-Mar-2013.)
|- ( ( _E Fr A /\ A =/= (/) ) -> E. x e. A ( x i^i A ) = (/) )
Theorem	zfregs 8608*	The strong form of the Axiom of Regularity, which does not require that A be a set. Axiom 6' of [TakeutiZaring] p. 21. See also epfrs 8607. (Contributed by NM, 17-Sep-2003.)
|- ( A =/= (/) -> E. x e. A ( x i^i A ) = (/) )
Theorem	zfregs2 8609*	Alternate strong form of the Axiom of Regularity. Not every element of a nonempty class contains some element of that class. (Contributed by Alan Sare, 24-Oct-2011.) (Proof shortened by Wolf Lammen, 27-Sep-2013.)
|- ( A =/= (/) -> -. A. x e. A E. y ( y e. A /\ y e. x ) )
Theorem	setind 8610*	Set (epsilon) induction. Theorem 5.22 of [TakeutiZaring] p. 21. (Contributed by NM, 17-Sep-2003.)
|- ( A. x ( x C_ A -> x e. A ) -> A = _V )
Theorem	setind2 8611	Set (epsilon) induction, stated compactly. Given as a homework problem in 1992 by George Boolos (1940-1996). (Contributed by NM, 17-Sep-2003.)
|- ( ~P A C_ A -> A = _V )
Syntax	ctc 8612	Extend class notation to include the transitive closure function.
class TC
Definition	df-tc 8613*	The transitive closure function. (Contributed by Mario Carneiro, 23-Jun-2013.)
|- TC = ( x e. _V |-> |^| { y | ( x C_ y /\ Tr y ) } )
Theorem	tcvalg 8614*	Value of the transitive closure function. (The fact that this intersection exists is a non-trivial fact that depends on ax-inf 8535; see tz9.1 8605.) (Contributed by Mario Carneiro, 23-Jun-2013.)
|- ( A e. V -> ( TC ` A ) = |^| { x | ( A C_ x /\ Tr x ) } )
Theorem	tcid 8615	Defining property of the transitive closure function: it contains its argument as a subset. (Contributed by Mario Carneiro, 23-Jun-2013.)
|- ( A e. V -> A C_ ( TC ` A ) )
Theorem	tctr 8616	Defining property of the transitive closure function: it is transitive. (Contributed by Mario Carneiro, 23-Jun-2013.)
|- Tr ( TC ` A )
Theorem	tcmin 8617	Defining property of the transitive closure function: it is a subset of any transitive class containing A. (Contributed by Mario Carneiro, 23-Jun-2013.)
|- ( A e. V -> ( ( A C_ B /\ Tr B ) -> ( TC ` A ) C_ B ) )
Theorem	tc2 8618*	A variant of the definition of the transitive closure function, using instead the smallest transitive set containing A as a member, gives almost the same set, except that A itself must be added because it is not usually a member of ( TC ` A ) (and it is never a member if A is well-founded). (Contributed by Mario Carneiro, 23-Jun-2013.)
|- A e. _V   =>    |- ( ( TC ` A ) u. { A } ) = |^| { x | ( A e. x /\ Tr x ) }
Theorem	tcsni 8619	The transitive closure of a singleton. Proof suggested by Gérard Lang. (Contributed by Mario Carneiro, 4-Jun-2015.)
|- A e. _V   =>    |- ( TC ` { A } ) = ( ( TC ` A ) u. { A } )
Theorem	tcss 8620	The transitive closure function inherits the subset relation. (Contributed by Mario Carneiro, 23-Jun-2013.)
|- A e. _V   =>    |- ( B C_ A -> ( TC ` B ) C_ ( TC ` A ) )
Theorem	tcel 8621	The transitive closure function converts the element relation to the subset relation. (Contributed by Mario Carneiro, 23-Jun-2013.)
|- A e. _V   =>    |- ( B e. A -> ( TC ` B ) C_ ( TC ` A ) )
Theorem	tcidm 8622	The transitive closure function is idempotent. (Contributed by Mario Carneiro, 23-Jun-2013.)
|- ( TC ` ( TC ` A ) ) = ( TC ` A )
Theorem	tc0 8623	The transitive closure of the empty set. (Contributed by Mario Carneiro, 4-Jun-2015.)
|- ( TC ` (/) ) = (/)
Theorem	tc00 8624	The transitive closure is empty iff its argument is. Proof suggested by Gérard Lang. (Contributed by Mario Carneiro, 4-Jun-2015.)
|- ( A e. V -> ( ( TC ` A ) = (/) <-> A = (/) ) )
2.6.5  Rank
Syntax	cr1 8625	Extend class definition to include the cumulative hierarchy of sets function.
class R1
Syntax	crnk 8626	Extend class definition to include rank function.
class rank
Definition	df-r1 8627	Define the cumulative hierarchy of sets function, using Takeuti and Zaring's notation ( R1). Starting with the empty set, this function builds up layers of sets where the next layer is the power set of the previous layer (and the union of previous layers when the argument is a limit ordinal). Using the Axiom of Regularity, we can show that any set whatsoever belongs to one of the layers of this hierarchy (see tz9.13 8654). Our definition expresses Definition 9.9 of [TakeutiZaring] p. 76 in a closed form, from which we derive the recursive definition as theorems r10 8631, r1suc 8633, and r1lim 8635. Theorem r1val1 8649 shows a recursive definition that works for all values, and theorems r1val2 8700 and r1val3 8701 show the value expressed in terms of rank. Other notations for this function are R with the argument as a subscript (Equation 3.1 of [BellMachover] p. 477), _V with a subscript (Definition of [Enderton] p. 202), M with a subscript (Definition 15.19 of [Monk1] p. 113), the capital Greek letter psi (Definition of [Mendelson] p. 281), and bold-face R (Definition 2.1 of [Kunen] p. 95). (Contributed by NM, 2-Sep-2003.)
|- R1 = rec ( ( x e. _V |-> ~P x ) , (/) )
Definition	df-rank 8628*	Define the rank function. See rankval 8679, rankval2 8681, rankval3 8703, or rankval4 8730 its value. The rank is a kind of "inverse" of the cumulative hierarchy of sets function R1: given a set, it returns an ordinal number telling us the smallest layer of the hierarchy to which the set belongs. Based on Definition 9.14 of [TakeutiZaring] p. 79. Theorem rankid 8696 illustrates the "inverse" concept. Another nice theorem showing the relationship is rankr1a 8699. (Contributed by NM, 11-Oct-2003.)
|- rank = ( x e. _V |-> |^| { y e. On | x e. ( R1 ` suc y ) } )
Theorem	r1funlim 8629	The cumulative hierarchy of sets function is a function on a limit ordinal. (This weak form of r1fnon 8630 avoids ax-rep 4771.) (Contributed by Mario Carneiro, 16-Nov-2014.)
|- ( Fun R1 /\ Lim dom R1 )
Theorem	r1fnon 8630	The cumulative hierarchy of sets function is a function on the class of ordinal numbers. (Contributed by NM, 5-Oct-2003.) (Revised by Mario Carneiro, 10-Sep-2013.)
|- R1 Fn On
Theorem	r10 8631	Value of the cumulative hierarchy of sets function at (/). Part of Definition 9.9 of [TakeutiZaring] p. 76. (Contributed by NM, 2-Sep-2003.) (Revised by Mario Carneiro, 10-Sep-2013.)
|- ( R1 ` (/) ) = (/)
Theorem	r1sucg 8632	Value of the cumulative hierarchy of sets function at a successor ordinal. Part of Definition 9.9 of [TakeutiZaring] p. 76. (Contributed by Mario Carneiro, 16-Nov-2014.)
|- ( A e. dom R1 -> ( R1 ` suc A ) = ~P ( R1 ` A ) )
Theorem	r1suc 8633	Value of the cumulative hierarchy of sets function at a successor ordinal. Part of Definition 9.9 of [TakeutiZaring] p. 76. (Contributed by NM, 2-Sep-2003.) (Revised by Mario Carneiro, 10-Sep-2013.)
|- ( A e. On -> ( R1 ` suc A ) = ~P ( R1 ` A ) )
Theorem	r1limg 8634*	Value of the cumulative hierarchy of sets function at a limit ordinal. Part of Definition 9.9 of [TakeutiZaring] p. 76. (Contributed by Mario Carneiro, 16-Nov-2014.)
|- ( ( A e. dom R1 /\ Lim A ) -> ( R1 ` A ) = U_ x e. A ( R1 ` x ) )
Theorem	r1lim 8635*	Value of the cumulative hierarchy of sets function at a limit ordinal. Part of Definition 9.9 of [TakeutiZaring] p. 76. (Contributed by NM, 4-Oct-2003.) (Revised by Mario Carneiro, 16-Nov-2014.)
|- ( ( A e. B /\ Lim A ) -> ( R1 ` A ) = U_ x e. A ( R1 ` x ) )
Theorem	r1fin 8636	The first om levels of the cumulative hierarchy are all finite. (Contributed by Mario Carneiro, 15-May-2013.)
|- ( A e. om -> ( R1 ` A ) e. Fin )
Theorem	r1sdom 8637	Each stage in the cumulative hierarchy is strictly larger than the last. (Contributed by Mario Carneiro, 19-Apr-2013.)
|- ( ( A e. On /\ B e. A ) -> ( R1 ` B ) ~< ( R1 ` A ) )
Theorem	r111 8638	The cumulative hierarchy is a one-to-one function. (Contributed by Mario Carneiro, 19-Apr-2013.)
|- R1 : On -1-1-> _V
Theorem	r1tr 8639	The cumulative hierarchy of sets is transitive. Lemma 7T of [Enderton] p. 202. (Contributed by NM, 8-Sep-2003.) (Revised by Mario Carneiro, 16-Nov-2014.)
|- Tr ( R1 ` A )
Theorem	r1tr2 8640	The union of a cumulative hierarchy of sets at ordinal A is a subset of the hierarchy at A. JFM CLASSES1 th. 40. (Contributed by FL, 20-Apr-2011.)
|- U. ( R1 ` A ) C_ ( R1 ` A )
Theorem	r1ordg 8641	Ordering relation for the cumulative hierarchy of sets. Part of Proposition 9.10(2) of [TakeutiZaring] p. 77. (Contributed by NM, 8-Sep-2003.)
|- ( B e. dom R1 -> ( A e. B -> ( R1 ` A ) e. ( R1 ` B ) ) )
Theorem	r1ord3g 8642	Ordering relation for the cumulative hierarchy of sets. Part of Theorem 3.3(i) of [BellMachover] p. 478. (Contributed by NM, 22-Sep-2003.)
|- ( ( A e. dom R1 /\ B e. dom R1 ) -> ( A C_ B -> ( R1 ` A ) C_ ( R1 ` B ) ) )
Theorem	r1ord 8643	Ordering relation for the cumulative hierarchy of sets. Part of Proposition 9.10(2) of [TakeutiZaring] p. 77. (Contributed by NM, 8-Sep-2003.) (Revised by Mario Carneiro, 16-Nov-2014.)
|- ( B e. On -> ( A e. B -> ( R1 ` A ) e. ( R1 ` B ) ) )
Theorem	r1ord2 8644	Ordering relation for the cumulative hierarchy of sets. Part of Proposition 9.10(2) of [TakeutiZaring] p. 77. (Contributed by NM, 22-Sep-2003.)
|- ( B e. On -> ( A e. B -> ( R1 ` A ) C_ ( R1 ` B ) ) )
Theorem	r1ord3 8645	Ordering relation for the cumulative hierarchy of sets. Part of Theorem 3.3(i) of [BellMachover] p. 478. (Contributed by NM, 22-Sep-2003.)
|- ( ( A e. On /\ B e. On ) -> ( A C_ B -> ( R1 ` A ) C_ ( R1 ` B ) ) )
Theorem	r1sssuc 8646	The value of the cumulative hierarchy of sets function is a subset of its value at the successor. JFM CLASSES1 Th. 39. (Contributed by FL, 20-Apr-2011.)
|- ( A e. On -> ( R1 ` A ) C_ ( R1 ` suc A ) )
Theorem	r1pwss 8647	Each set of the cumulative hierarchy is closed under subsets. (Contributed by Mario Carneiro, 16-Nov-2014.)
|- ( A e. ( R1 ` B ) -> ~P A C_ ( R1 ` B ) )
Theorem	r1sscl 8648	Each set of the cumulative hierarchy is closed under subsets. (Contributed by Mario Carneiro, 16-Nov-2014.)
|- ( ( A e. ( R1 ` B ) /\ C C_ A ) -> C e. ( R1 ` B ) )
Theorem	r1val1 8649*	The value of the cumulative hierarchy of sets function expressed recursively. Theorem 7Q of [Enderton] p. 202. (Contributed by NM, 25-Nov-2003.) (Revised by Mario Carneiro, 17-Nov-2014.)
|- ( A e. dom R1 -> ( R1 ` A ) = U_ x e. A ~P ( R1 ` x ) )
Theorem	tz9.12lem1 8650*	Lemma for tz9.12 8653. (Contributed by NM, 22-Sep-2003.) (Revised by Mario Carneiro, 11-Sep-2015.)
|- A e. _V   &    |- F = ( z e. _V |-> |^| { v e. On | z e. ( R1 ` v ) } )   =>    |- ( F " A ) C_ On
Theorem	tz9.12lem2 8651*	Lemma for tz9.12 8653. (Contributed by NM, 22-Sep-2003.)
|- A e. _V   &    |- F = ( z e. _V |-> |^| { v e. On | z e. ( R1 ` v ) } )   =>    |- suc U. ( F " A ) e. On
Theorem	tz9.12lem3 8652*	Lemma for tz9.12 8653. (Contributed by NM, 22-Sep-2003.) (Revised by Mario Carneiro, 11-Sep-2015.)
|- A e. _V   &    |- F = ( z e. _V |-> |^| { v e. On | z e. ( R1 ` v ) } )   =>    |- ( A. x e. A E. y e. On x e. ( R1 ` y ) -> A e. ( R1 ` suc suc U. ( F " A ) ) )
Theorem	tz9.12 8653*	A set is well-founded if all of its elements are well-founded. Proposition 9.12 of [TakeutiZaring] p. 78. The main proof consists of tz9.12lem1 8650 through tz9.12lem3 8652. (Contributed by NM, 22-Sep-2003.)
|- A e. _V   =>    |- ( A. x e. A E. y e. On x e. ( R1 ` y ) -> E. y e. On A e. ( R1 ` y ) )
Theorem	tz9.13 8654*	Every set is well-founded, assuming the Axiom of Regularity. In other words, every set belongs to a layer of the cumulative hierarchy of sets. Proposition 9.13 of [TakeutiZaring] p. 78. (Contributed by NM, 23-Sep-2003.)
|- A e. _V   =>    |- E. x e. On A e. ( R1 ` x )
Theorem	tz9.13g 8655*	Every set is well-founded, assuming the Axiom of Regularity. Proposition 9.13 of [TakeutiZaring] p. 78. This variant of tz9.13 8654 expresses the class existence requirement as an antecedent. (Contributed by NM, 4-Oct-2003.)
|- ( A e. V -> E. x e. On A e. ( R1 ` x ) )
Theorem	rankwflemb 8656*	Two ways of saying a set is well-founded. (Contributed by NM, 11-Oct-2003.) (Revised by Mario Carneiro, 16-Nov-2014.)
|- ( A e. U. ( R1 " On ) <-> E. x e. On A e. ( R1 ` suc x ) )
Theorem	rankf 8657	The domain and range of the rank function. (Contributed by Mario Carneiro, 28-May-2013.) (Revised by Mario Carneiro, 12-Sep-2013.)
|- rank : U. ( R1 " On ) --> On
Theorem	rankon 8658	The rank of a set is an ordinal number. Proposition 9.15(1) of [TakeutiZaring] p. 79. (Contributed by NM, 5-Oct-2003.) (Revised by Mario Carneiro, 12-Sep-2013.)
|- ( rank ` A ) e. On
Theorem	r1elwf 8659	Any member of the cumulative hierarchy is well-founded. (Contributed by Mario Carneiro, 28-May-2013.) (Revised by Mario Carneiro, 16-Nov-2014.)
|- ( A e. ( R1 ` B ) -> A e. U. ( R1 " On ) )
Theorem	rankvalb 8660*	Value of the rank function. Definition 9.14 of [TakeutiZaring] p. 79 (proved as a theorem from our definition). This variant of rankval 8679 does not use Regularity, and so requires the assumption that A is in the range of R1. (Contributed by NM, 11-Oct-2003.) (Revised by Mario Carneiro, 10-Sep-2013.)
|- ( A e. U. ( R1 " On ) -> ( rank ` A ) = |^| { x e. On | A e. ( R1 ` suc x ) } )
Theorem	rankr1ai 8661	One direction of rankr1a 8699. (Contributed by Mario Carneiro, 28-May-2013.) (Revised by Mario Carneiro, 17-Nov-2014.)
|- ( A e. ( R1 ` B ) -> ( rank ` A ) e. B )
Theorem	rankvaln 8662	Value of the rank function at a non-well-founded set. (The antecedent is always false under Foundation, by unir1 8676, unless A is a proper class.) (Contributed by Mario Carneiro, 22-Mar-2013.) (Revised by Mario Carneiro, 10-Sep-2013.)
|- ( -. A e. U. ( R1 " On ) -> ( rank ` A ) = (/) )
Theorem	rankidb 8663	Identity law for the rank function. (Contributed by NM, 3-Oct-2003.) (Revised by Mario Carneiro, 22-Mar-2013.)
|- ( A e. U. ( R1 " On ) -> A e. ( R1 ` suc ( rank ` A ) ) )
Theorem	rankdmr1 8664	A rank is a member of the cumulative hierarchy. (Contributed by Mario Carneiro, 17-Nov-2014.)
|- ( rank ` A ) e. dom R1
Theorem	rankr1ag 8665	A version of rankr1a 8699 that is suitable without assuming Regularity or Replacement. (Contributed by Mario Carneiro, 3-Jun-2013.) (Revised by Mario Carneiro, 17-Nov-2014.)
|- ( ( A e. U. ( R1 " On ) /\ B e. dom R1 ) -> ( A e. ( R1 ` B ) <-> ( rank ` A ) e. B ) )
Theorem	rankr1bg 8666	A relationship between rank and R1. See rankr1ag 8665 for the membership version. (Contributed by Mario Carneiro, 17-Nov-2014.)
|- ( ( A e. U. ( R1 " On ) /\ B e. dom R1 ) -> ( A C_ ( R1 ` B ) <-> ( rank ` A ) C_ B ) )
Theorem	r1rankidb 8667	Any set is a subset of the hierarchy of its rank. (Contributed by Mario Carneiro, 3-Jun-2013.) (Revised by Mario Carneiro, 17-Nov-2014.)
|- ( A e. U. ( R1 " On ) -> A C_ ( R1 ` ( rank ` A ) ) )
Theorem	r1elssi 8668	The range of the R1 function is transitive. Lemma 2.10 of [Kunen] p. 97. One direction of r1elss 8669 that doesn't need A to be a set. (Contributed by Mario Carneiro, 22-Mar-2013.) (Revised by Mario Carneiro, 16-Nov-2014.)
|- ( A e. U. ( R1 " On ) -> A C_ U. ( R1 " On ) )
Theorem	r1elss 8669	The range of the R1 function is transitive. Lemma 2.10 of [Kunen] p. 97. (Contributed by Mario Carneiro, 22-Mar-2013.) (Revised by Mario Carneiro, 16-Nov-2014.)
|- A e. _V   =>    |- ( A e. U. ( R1 " On ) <-> A C_ U. ( R1 " On ) )
Theorem	pwwf 8670	A power set is well-founded iff the base set is. (Contributed by Mario Carneiro, 8-Jun-2013.) (Revised by Mario Carneiro, 16-Nov-2014.)
|- ( A e. U. ( R1 " On ) <-> ~P A e. U. ( R1 " On ) )
Theorem	sswf 8671	A subset of a well-founded set is well-founded. (Contributed by Mario Carneiro, 17-Nov-2014.)
|- ( ( A e. U. ( R1 " On ) /\ B C_ A ) -> B e. U. ( R1 " On ) )
Theorem	snwf 8672	A singleton is well-founded if its element is. (Contributed by Mario Carneiro, 10-Jun-2013.) (Revised by Mario Carneiro, 16-Nov-2014.)
|- ( A e. U. ( R1 " On ) -> { A } e. U. ( R1 " On ) )
Theorem	unwf 8673	A binary union is well-founded iff its elements are. (Contributed by Mario Carneiro, 10-Jun-2013.) (Revised by Mario Carneiro, 17-Nov-2014.)
|- ( ( A e. U. ( R1 " On ) /\ B e. U. ( R1 " On ) ) <-> ( A u. B ) e. U. ( R1 " On ) )
Theorem	prwf 8674	An unordered pair is well-founded if its elements are. (Contributed by Mario Carneiro, 10-Jun-2013.) (Revised by Mario Carneiro, 17-Nov-2014.)
|- ( ( A e. U. ( R1 " On ) /\ B e. U. ( R1 " On ) ) -> { A , B } e. U. ( R1 " On ) )
Theorem	opwf 8675	An ordered pair is well-founded if its elements are. (Contributed by Mario Carneiro, 10-Jun-2013.)
|- ( ( A e. U. ( R1 " On ) /\ B e. U. ( R1 " On ) ) -> <. A , B >. e. U. ( R1 " On ) )
Theorem	unir1 8676	The cumulative hierarchy of sets covers the universe. Proposition 4.45 (b) to (a) of [Mendelson] p. 281. (Contributed by NM, 27-Sep-2004.) (Revised by Mario Carneiro, 8-Jun-2013.)
|- U. ( R1 " On ) = _V
Theorem	jech9.3 8677	Every set belongs to some value of the cumulative hierarchy of sets function R1, i.e. the indexed union of all values of R1 is the universe. Lemma 9.3 of [Jech] p. 71. (Contributed by NM, 4-Oct-2003.) (Revised by Mario Carneiro, 8-Jun-2013.)
|- U_ x e. On ( R1 ` x ) = _V
Theorem	rankwflem 8678*	Every set is well-founded, assuming the Axiom of Regularity. Proposition 9.13 of [TakeutiZaring] p. 78. This variant of tz9.13g 8655 is useful in proofs of theorems about the rank function. (Contributed by NM, 4-Oct-2003.)
|- ( A e. V -> E. x e. On A e. ( R1 ` suc x ) )
Theorem	rankval 8679*	Value of the rank function. Definition 9.14 of [TakeutiZaring] p. 79 (proved as a theorem from our definition). (Contributed by NM, 24-Sep-2003.) (Revised by Mario Carneiro, 10-Sep-2013.)
|- A e. _V   =>    |- ( rank ` A ) = |^| { x e. On | A e. ( R1 ` suc x ) }
Theorem	rankvalg 8680*	Value of the rank function. Definition 9.14 of [TakeutiZaring] p. 79 (proved as a theorem from our definition). This variant of rankval 8679 expresses the class existence requirement as an antecedent instead of a hypothesis. (Contributed by NM, 5-Oct-2003.)
|- ( A e. V -> ( rank ` A ) = |^| { x e. On | A e. ( R1 ` suc x ) } )
Theorem	rankval2 8681*	Value of an alternate definition of the rank function. Definition of [BellMachover] p. 478. (Contributed by NM, 8-Oct-2003.)
|- ( A e. B -> ( rank ` A ) = |^| { x e. On | A C_ ( R1 ` x ) } )
Theorem	uniwf 8682	A union is well-founded iff the base set is. (Contributed by Mario Carneiro, 8-Jun-2013.) (Revised by Mario Carneiro, 17-Nov-2014.)
|- ( A e. U. ( R1 " On ) <-> U. A e. U. ( R1 " On ) )
Theorem	rankr1clem 8683	Lemma for rankr1c 8684. (Contributed by NM, 6-Oct-2003.) (Revised by Mario Carneiro, 17-Nov-2014.)
|- ( ( A e. U. ( R1 " On ) /\ B e. dom R1 ) -> ( -. A e. ( R1 ` B ) <-> B C_ ( rank ` A ) ) )
Theorem	rankr1c 8684	A relationship between the rank function and the cumulative hierarchy of sets function R1. Proposition 9.15(2) of [TakeutiZaring] p. 79. (Contributed by Mario Carneiro, 22-Mar-2013.) (Revised by Mario Carneiro, 17-Nov-2014.)
|- ( A e. U. ( R1 " On ) -> ( B = ( rank ` A ) <-> ( -. A e. ( R1 ` B ) /\ A e. ( R1 ` suc B ) ) ) )
Theorem	rankidn 8685	A relationship between the rank function and the cumulative hierarchy of sets function R1. (Contributed by Mario Carneiro, 17-Nov-2014.)
|- ( A e. U. ( R1 " On ) -> -. A e. ( R1 ` ( rank ` A ) ) )
Theorem	rankpwi 8686	The rank of a power set. Part of Exercise 30 of [Enderton] p. 207. (Contributed by Mario Carneiro, 3-Jun-2013.)
|- ( A e. U. ( R1 " On ) -> ( rank ` ~P A ) = suc ( rank ` A ) )
Theorem	rankelb 8687	The membership relation is inherited by the rank function. Proposition 9.16 of [TakeutiZaring] p. 79. (Contributed by NM, 4-Oct-2003.) (Revised by Mario Carneiro, 17-Nov-2014.)
|- ( B e. U. ( R1 " On ) -> ( A e. B -> ( rank ` A ) e. ( rank ` B ) ) )
Theorem	wfelirr 8688	A well-founded set is not a member of itself. This proof does not require the axiom of regularity, unlike elirr 8505. (Contributed by Mario Carneiro, 2-Jan-2017.)
|- ( A e. U. ( R1 " On ) -> -. A e. A )
Theorem	rankval3b 8689*	The value of the rank function expressed recursively: the rank of a set is the smallest ordinal number containing the ranks of all members of the set. Proposition 9.17 of [TakeutiZaring] p. 79. (Contributed by Mario Carneiro, 17-Nov-2014.)
|- ( A e. U. ( R1 " On ) -> ( rank ` A ) = |^| { x e. On | A. y e. A ( rank ` y ) e. x } )
Theorem	ranksnb 8690	The rank of a singleton. Theorem 15.17(v) of [Monk1] p. 112. (Contributed by Mario Carneiro, 10-Jun-2013.)
|- ( A e. U. ( R1 " On ) -> ( rank ` { A } ) = suc ( rank ` A ) )
Theorem	rankonidlem 8691	Lemma for rankonid 8692. (Contributed by NM, 14-Oct-2003.) (Revised by Mario Carneiro, 22-Mar-2013.)
|- ( A e. dom R1 -> ( A e. U. ( R1 " On ) /\ ( rank ` A ) = A ) )
Theorem	rankonid 8692	The rank of an ordinal number is itself. Proposition 9.18 of [TakeutiZaring] p. 79 and its converse. (Contributed by NM, 14-Oct-2003.) (Revised by Mario Carneiro, 17-Nov-2014.)
|- ( A e. dom R1 <-> ( rank ` A ) = A )
Theorem	onwf 8693	The ordinals are all well-founded. (Contributed by Mario Carneiro, 22-Mar-2013.) (Revised by Mario Carneiro, 17-Nov-2014.)
|- On C_ U. ( R1 " On )
Theorem	onssr1 8694	Initial segments of the ordinals are contained in initial segments of the cumulative hierarchy. (Contributed by FL, 20-Apr-2011.) (Revised by Mario Carneiro, 17-Nov-2014.)
|- ( A e. dom R1 -> A C_ ( R1 ` A ) )
Theorem	rankr1g 8695	A relationship between the rank function and the cumulative hierarchy of sets function R1. Proposition 9.15(2) of [TakeutiZaring] p. 79. (Contributed by NM, 6-Oct-2003.) (Revised by Mario Carneiro, 17-Nov-2014.)
|- ( A e. V -> ( B = ( rank ` A ) <-> ( -. A e. ( R1 ` B ) /\ A e. ( R1 ` suc B ) ) ) )
Theorem	rankid 8696	Identity law for the rank function. (Contributed by NM, 3-Oct-2003.) (Revised by Mario Carneiro, 17-Nov-2014.)
|- A e. _V   =>    |- A e. ( R1 ` suc ( rank ` A ) )
Theorem	rankr1 8697	A relationship between the rank function and the cumulative hierarchy of sets function R1. Proposition 9.15(2) of [TakeutiZaring] p. 79. (Contributed by NM, 6-Oct-2003.) (Proof shortened by Mario Carneiro, 17-Nov-2014.)
|- A e. _V   =>    |- ( B = ( rank ` A ) <-> ( -. A e. ( R1 ` B ) /\ A e. ( R1 ` suc B ) ) )
Theorem	ssrankr1 8698	A relationship between an ordinal number less than or equal to a rank, and the cumulative hierarchy of sets R1. Proposition 9.15(3) of [TakeutiZaring] p. 79. (Contributed by NM, 8-Oct-2003.) (Revised by Mario Carneiro, 17-Nov-2014.)
|- A e. _V   =>    |- ( B e. On -> ( B C_ ( rank ` A ) <-> -. A e. ( R1 ` B ) ) )
Theorem	rankr1a 8699	A relationship between rank and R1, clearly equivalent to ssrankr1 8698 and friends through trichotomy, but in Raph's opinion considerably more intuitive. See rankr1b 8727 for the subset version. (Contributed by Raph Levien, 29-May-2004.)
|- A e. _V   =>    |- ( B e. On -> ( A e. ( R1 ` B ) <-> ( rank ` A ) e. B ) )
Theorem	r1val2 8700*	The value of the cumulative hierarchy of sets function expressed in terms of rank. Definition 15.19 of [Monk1] p. 113. (Contributed by NM, 30-Nov-2003.)
|- ( A e. On -> ( R1 ` A ) = { x | ( rank ` x ) e. A } )