P. 70 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 6901-7000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ofexg 6901	A function operation restricted to a set is a set. (Contributed by NM, 28-Jul-2014.)
|- ( A e. V -> ( oF R |` A ) e. _V )
Theorem	nfof 6902*	Hypothesis builder for function operation. (Contributed by Mario Carneiro, 20-Jul-2014.)
|- F/_ x R   =>    |- F/_ x oF R
Theorem	nfofr 6903*	Hypothesis builder for function relation. (Contributed by Mario Carneiro, 28-Jul-2014.)
|- F/_ x R   =>    |- F/_ x oR R
Theorem	offval 6904*	Value of an operation applied to two functions. (Contributed by Mario Carneiro, 20-Jul-2014.)
|- ( ph -> F Fn A )   &    |- ( ph -> G Fn B )   &    |- ( ph -> A e. V )   &    |- ( ph -> B e. W )   &    |- ( A i^i B ) = S   &    |- ( ( ph /\ x e. A ) -> ( F ` x ) = C )   &    |- ( ( ph /\ x e. B ) -> ( G ` x ) = D )   =>    |- ( ph -> ( F oF R G ) = ( x e. S |-> ( C R D ) ) )
Theorem	ofrfval 6905*	Value of a relation applied to two functions. (Contributed by Mario Carneiro, 28-Jul-2014.)
|- ( ph -> F Fn A )   &    |- ( ph -> G Fn B )   &    |- ( ph -> A e. V )   &    |- ( ph -> B e. W )   &    |- ( A i^i B ) = S   &    |- ( ( ph /\ x e. A ) -> ( F ` x ) = C )   &    |- ( ( ph /\ x e. B ) -> ( G ` x ) = D )   =>    |- ( ph -> ( F oR R G <-> A. x e. S C R D ) )
Theorem	ofval 6906	Evaluate a function operation at a point. (Contributed by Mario Carneiro, 20-Jul-2014.)
|- ( ph -> F Fn A )   &    |- ( ph -> G Fn B )   &    |- ( ph -> A e. V )   &    |- ( ph -> B e. W )   &    |- ( A i^i B ) = S   &    |- ( ( ph /\ X e. A ) -> ( F ` X ) = C )   &    |- ( ( ph /\ X e. B ) -> ( G ` X ) = D )   =>    |- ( ( ph /\ X e. S ) -> ( ( F oF R G ) ` X ) = ( C R D ) )
Theorem	ofrval 6907	Exhibit a function relation at a point. (Contributed by Mario Carneiro, 28-Jul-2014.)
|- ( ph -> F Fn A )   &    |- ( ph -> G Fn B )   &    |- ( ph -> A e. V )   &    |- ( ph -> B e. W )   &    |- ( A i^i B ) = S   &    |- ( ( ph /\ X e. A ) -> ( F ` X ) = C )   &    |- ( ( ph /\ X e. B ) -> ( G ` X ) = D )   =>    |- ( ( ph /\ F oR R G /\ X e. S ) -> C R D )
Theorem	offn 6908	The function operation produces a function. (Contributed by Mario Carneiro, 22-Jul-2014.)
|- ( ph -> F Fn A )   &    |- ( ph -> G Fn B )   &    |- ( ph -> A e. V )   &    |- ( ph -> B e. W )   &    |- ( A i^i B ) = S   =>    |- ( ph -> ( F oF R G ) Fn S )
Theorem	offval2f 6909*	The function operation expressed as a mapping. (Contributed by Thierry Arnoux, 23-Jun-2017.)
|- F/ x ph   &    |- F/_ x A   &    |- ( ph -> A e. V )   &    |- ( ( ph /\ x e. A ) -> B e. W )   &    |- ( ( ph /\ x e. A ) -> C e. X )   &    |- ( ph -> F = ( x e. A |-> B ) )   &    |- ( ph -> G = ( x e. A |-> C ) )   =>    |- ( ph -> ( F oF R G ) = ( x e. A |-> ( B R C ) ) )
Theorem	ofmresval 6910	Value of a restriction of the function operation map. (Contributed by NM, 20-Oct-2014.)
|- ( ph -> F e. A )   &    |- ( ph -> G e. B )   =>    |- ( ph -> ( F ( oF R |` ( A X. B ) ) G ) = ( F oF R G ) )
Theorem	fnfvof 6911	Function value of a pointwise composition. (Contributed by Stefan O'Rear, 5-Oct-2014.) (Proof shortened by Mario Carneiro, 5-Jun-2015.)
|- ( ( ( F Fn A /\ G Fn A ) /\ ( A e. V /\ X e. A ) ) -> ( ( F oF R G ) ` X ) = ( ( F ` X ) R ( G ` X ) ) )
Theorem	off 6912*	The function operation produces a function. (Contributed by Mario Carneiro, 20-Jul-2014.)
|- ( ( ph /\ ( x e. S /\ y e. T ) ) -> ( x R y ) e. U )   &    |- ( ph -> F : A --> S )   &    |- ( ph -> G : B --> T )   &    |- ( ph -> A e. V )   &    |- ( ph -> B e. W )   &    |- ( A i^i B ) = C   =>    |- ( ph -> ( F oF R G ) : C --> U )
Theorem	ofres 6913	Restrict the operands of a function operation to the same domain as that of the operation itself. (Contributed by Mario Carneiro, 15-Sep-2014.)
|- ( ph -> F Fn A )   &    |- ( ph -> G Fn B )   &    |- ( ph -> A e. V )   &    |- ( ph -> B e. W )   &    |- ( A i^i B ) = C   =>    |- ( ph -> ( F oF R G ) = ( ( F |` C ) oF R ( G |` C ) ) )
Theorem	offval2 6914*	The function operation expressed as a mapping. (Contributed by Mario Carneiro, 20-Jul-2014.)
|- ( ph -> A e. V )   &    |- ( ( ph /\ x e. A ) -> B e. W )   &    |- ( ( ph /\ x e. A ) -> C e. X )   &    |- ( ph -> F = ( x e. A |-> B ) )   &    |- ( ph -> G = ( x e. A |-> C ) )   =>    |- ( ph -> ( F oF R G ) = ( x e. A |-> ( B R C ) ) )
Theorem	ofrfval2 6915*	The function relation acting on maps. (Contributed by Mario Carneiro, 20-Jul-2014.)
|- ( ph -> A e. V )   &    |- ( ( ph /\ x e. A ) -> B e. W )   &    |- ( ( ph /\ x e. A ) -> C e. X )   &    |- ( ph -> F = ( x e. A |-> B ) )   &    |- ( ph -> G = ( x e. A |-> C ) )   =>    |- ( ph -> ( F oR R G <-> A. x e. A B R C ) )
Theorem	ofmpteq 6916*	Value of a pointwise operation on two functions defined using maps-to notation. (Contributed by Stefan O'Rear, 5-Oct-2014.)
|- ( ( A e. V /\ ( x e. A |-> B ) Fn A /\ ( x e. A |-> C ) Fn A ) -> ( ( x e. A |-> B ) oF R ( x e. A |-> C ) ) = ( x e. A |-> ( B R C ) ) )
Theorem	ofco 6917	The composition of a function operation with another function. (Contributed by Mario Carneiro, 19-Dec-2014.)
|- ( ph -> F Fn A )   &    |- ( ph -> G Fn B )   &    |- ( ph -> H : D --> C )   &    |- ( ph -> A e. V )   &    |- ( ph -> B e. W )   &    |- ( ph -> D e. X )   &    |- ( A i^i B ) = C   =>    |- ( ph -> ( ( F oF R G ) o. H ) = ( ( F o. H ) oF R ( G o. H ) ) )
Theorem	offveq 6918*	Convert an identity of the operation to the analogous identity on the function operation. (Contributed by Mario Carneiro, 24-Jul-2014.)
|- ( ph -> A e. V )   &    |- ( ph -> F Fn A )   &    |- ( ph -> G Fn A )   &    |- ( ph -> H Fn A )   &    |- ( ( ph /\ x e. A ) -> ( F ` x ) = B )   &    |- ( ( ph /\ x e. A ) -> ( G ` x ) = C )   &    |- ( ( ph /\ x e. A ) -> ( B R C ) = ( H ` x ) )   =>    |- ( ph -> ( F oF R G ) = H )
Theorem	offveqb 6919*	Equivalent expressions for equality with a function operation. (Contributed by NM, 9-Oct-2014.) (Proof shortened by Mario Carneiro, 5-Dec-2016.)
|- ( ph -> A e. V )   &    |- ( ph -> F Fn A )   &    |- ( ph -> G Fn A )   &    |- ( ph -> H Fn A )   &    |- ( ( ph /\ x e. A ) -> ( F ` x ) = B )   &    |- ( ( ph /\ x e. A ) -> ( G ` x ) = C )   =>    |- ( ph -> ( H = ( F oF R G ) <-> A. x e. A ( H ` x ) = ( B R C ) ) )
Theorem	ofc1 6920	Left operation by a constant. (Contributed by Mario Carneiro, 24-Jul-2014.)
|- ( ph -> A e. V )   &    |- ( ph -> B e. W )   &    |- ( ph -> F Fn A )   &    |- ( ( ph /\ X e. A ) -> ( F ` X ) = C )   =>    |- ( ( ph /\ X e. A ) -> ( ( ( A X. { B } ) oF R F ) ` X ) = ( B R C ) )
Theorem	ofc2 6921	Right operation by a constant. (Contributed by NM, 7-Oct-2014.)
|- ( ph -> A e. V )   &    |- ( ph -> B e. W )   &    |- ( ph -> F Fn A )   &    |- ( ( ph /\ X e. A ) -> ( F ` X ) = C )   =>    |- ( ( ph /\ X e. A ) -> ( ( F oF R ( A X. { B } ) ) ` X ) = ( C R B ) )
Theorem	ofc12 6922	Function operation on two constant functions. (Contributed by Mario Carneiro, 28-Jul-2014.)
|- ( ph -> A e. V )   &    |- ( ph -> B e. W )   &    |- ( ph -> C e. X )   =>    |- ( ph -> ( ( A X. { B } ) oF R ( A X. { C } ) ) = ( A X. { ( B R C ) } ) )
Theorem	caofref 6923*	Transfer a reflexive law to the function relation. (Contributed by Mario Carneiro, 28-Jul-2014.)
|- ( ph -> A e. V )   &    |- ( ph -> F : A --> S )   &    |- ( ( ph /\ x e. S ) -> x R x )   =>    |- ( ph -> F oR R F )
Theorem	caofinvl 6924*	Transfer a left inverse law to the function operation. (Contributed by NM, 22-Oct-2014.)
|- ( ph -> A e. V )   &    |- ( ph -> F : A --> S )   &    |- ( ph -> B e. W )   &    |- ( ph -> N : S --> S )   &    |- ( ph -> G = ( v e. A |-> ( N ` ( F ` v ) ) ) )   &    |- ( ( ph /\ x e. S ) -> ( ( N ` x ) R x ) = B )   =>    |- ( ph -> ( G oF R F ) = ( A X. { B } ) )
Theorem	caofid0l 6925*	Transfer a left identity law to the function operation. (Contributed by NM, 21-Oct-2014.)
|- ( ph -> A e. V )   &    |- ( ph -> F : A --> S )   &    |- ( ph -> B e. W )   &    |- ( ( ph /\ x e. S ) -> ( B R x ) = x )   =>    |- ( ph -> ( ( A X. { B } ) oF R F ) = F )
Theorem	caofid0r 6926*	Transfer a right identity law to the function operation. (Contributed by NM, 21-Oct-2014.)
|- ( ph -> A e. V )   &    |- ( ph -> F : A --> S )   &    |- ( ph -> B e. W )   &    |- ( ( ph /\ x e. S ) -> ( x R B ) = x )   =>    |- ( ph -> ( F oF R ( A X. { B } ) ) = F )
Theorem	caofid1 6927*	Transfer a right absorption law to the function operation. (Contributed by Mario Carneiro, 28-Jul-2014.)
|- ( ph -> A e. V )   &    |- ( ph -> F : A --> S )   &    |- ( ph -> B e. W )   &    |- ( ph -> C e. X )   &    |- ( ( ph /\ x e. S ) -> ( x R B ) = C )   =>    |- ( ph -> ( F oF R ( A X. { B } ) ) = ( A X. { C } ) )
Theorem	caofid2 6928*	Transfer a right absorption law to the function operation. (Contributed by Mario Carneiro, 28-Jul-2014.)
|- ( ph -> A e. V )   &    |- ( ph -> F : A --> S )   &    |- ( ph -> B e. W )   &    |- ( ph -> C e. X )   &    |- ( ( ph /\ x e. S ) -> ( B R x ) = C )   =>    |- ( ph -> ( ( A X. { B } ) oF R F ) = ( A X. { C } ) )
Theorem	caofcom 6929*	Transfer a commutative law to the function operation. (Contributed by Mario Carneiro, 26-Jul-2014.)
|- ( ph -> A e. V )   &    |- ( ph -> F : A --> S )   &    |- ( ph -> G : A --> S )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x R y ) = ( y R x ) )   =>    |- ( ph -> ( F oF R G ) = ( G oF R F ) )
Theorem	caofrss 6930*	Transfer a relation subset law to the function relation. (Contributed by Mario Carneiro, 28-Jul-2014.)
|- ( ph -> A e. V )   &    |- ( ph -> F : A --> S )   &    |- ( ph -> G : A --> S )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x R y -> x T y ) )   =>    |- ( ph -> ( F oR R G -> F oR T G ) )
Theorem	caofass 6931*	Transfer an associative law to the function operation. (Contributed by Mario Carneiro, 26-Jul-2014.)
|- ( ph -> A e. V )   &    |- ( ph -> F : A --> S )   &    |- ( ph -> G : A --> S )   &    |- ( ph -> H : A --> S )   &    |- ( ( ph /\ ( x e. S /\ y e. S /\ z e. S ) ) -> ( ( x R y ) T z ) = ( x O ( y P z ) ) )   =>    |- ( ph -> ( ( F oF R G ) oF T H ) = ( F oF O ( G oF P H ) ) )
Theorem	caoftrn 6932*	Transfer a transitivity law to the function relation. (Contributed by Mario Carneiro, 28-Jul-2014.)
|- ( ph -> A e. V )   &    |- ( ph -> F : A --> S )   &    |- ( ph -> G : A --> S )   &    |- ( ph -> H : A --> S )   &    |- ( ( ph /\ ( x e. S /\ y e. S /\ z e. S ) ) -> ( ( x R y /\ y T z ) -> x U z ) )   =>    |- ( ph -> ( ( F oR R G /\ G oR T H ) -> F oR U H ) )
Theorem	caofdi 6933*	Transfer a distributive law to the function operation. (Contributed by Mario Carneiro, 26-Jul-2014.)
|- ( ph -> A e. V )   &    |- ( ph -> F : A --> K )   &    |- ( ph -> G : A --> S )   &    |- ( ph -> H : A --> S )   &    |- ( ( ph /\ ( x e. K /\ y e. S /\ z e. S ) ) -> ( x T ( y R z ) ) = ( ( x T y ) O ( x T z ) ) )   =>    |- ( ph -> ( F oF T ( G oF R H ) ) = ( ( F oF T G ) oF O ( F oF T H ) ) )
Theorem	caofdir 6934*	Transfer a reverse distributive law to the function operation. (Contributed by NM, 19-Oct-2014.)
|- ( ph -> A e. V )   &    |- ( ph -> F : A --> K )   &    |- ( ph -> G : A --> S )   &    |- ( ph -> H : A --> S )   &    |- ( ( ph /\ ( x e. S /\ y e. S /\ z e. K ) ) -> ( ( x R y ) T z ) = ( ( x T z ) O ( y T z ) ) )   =>    |- ( ph -> ( ( G oF R H ) oF T F ) = ( ( G oF T F ) oF O ( H oF T F ) ) )
Theorem	caonncan 6935*	Transfer nncan 10310-shaped laws to vectors of numbers. (Contributed by Stefan O'Rear, 27-Mar-2015.)
|- ( ph -> I e. V )   &    |- ( ph -> A : I --> S )   &    |- ( ph -> B : I --> S )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x M ( x M y ) ) = y )   =>    |- ( ph -> ( A oF M ( A oF M B ) ) = B )
2.3.21  Proper subset relation
Syntax	crpss 6936	Extend class notation to include the reified proper subset relation.
class [ C.]
Definition	df-rpss 6937*	Define a relation which corresponds to proper subsethood df-pss 3590 on sets. This allows us to use proper subsethood with general concepts that require relations, such as strict ordering, see sorpss 6942. (Contributed by Stefan O'Rear, 2-Nov-2014.)
|- [ C.] = { <. x , y >. | x C. y }
Theorem	relrpss 6938	The proper subset relation is a relation. (Contributed by Stefan O'Rear, 2-Nov-2014.)
|- Rel [ C.]
Theorem	brrpssg 6939	The proper subset relation on sets is the same as class proper subsethood. (Contributed by Stefan O'Rear, 2-Nov-2014.)
|- ( B e. V -> ( A [ C.] B <-> A C. B ) )
Theorem	brrpss 6940	The proper subset relation on sets is the same as class proper subsethood. (Contributed by Stefan O'Rear, 2-Nov-2014.)
|- B e. _V   =>    |- ( A [ C.] B <-> A C. B )
Theorem	porpss 6941	Every class is partially ordered by proper subsets. (Contributed by Stefan O'Rear, 2-Nov-2014.)
|- [ C.] Po A
Theorem	sorpss 6942*	Express strict ordering under proper subsets, i.e. the notion of a chain of sets. (Contributed by Stefan O'Rear, 2-Nov-2014.)
|- ( [ C.] Or A <-> A. x e. A A. y e. A ( x C_ y \/ y C_ x ) )
Theorem	sorpssi 6943	Property of a chain of sets. (Contributed by Stefan O'Rear, 2-Nov-2014.)
|- ( ( [ C.] Or A /\ ( B e. A /\ C e. A ) ) -> ( B C_ C \/ C C_ B ) )
Theorem	sorpssun 6944	A chain of sets is closed under binary union. (Contributed by Mario Carneiro, 16-May-2015.)
|- ( ( [ C.] Or A /\ ( B e. A /\ C e. A ) ) -> ( B u. C ) e. A )
Theorem	sorpssin 6945	A chain of sets is closed under binary intersection. (Contributed by Mario Carneiro, 16-May-2015.)
|- ( ( [ C.] Or A /\ ( B e. A /\ C e. A ) ) -> ( B i^i C ) e. A )
Theorem	sorpssuni 6946*	In a chain of sets, a maximal element is the union of the chain. (Contributed by Stefan O'Rear, 2-Nov-2014.)
|- ( [ C.] Or Y -> ( E. u e. Y A. v e. Y -. u C. v <-> U. Y e. Y ) )
Theorem	sorpssint 6947*	In a chain of sets, a minimal element is the intersection of the chain. (Contributed by Stefan O'Rear, 2-Nov-2014.)
|- ( [ C.] Or Y -> ( E. u e. Y A. v e. Y -. v C. u <-> |^| Y e. Y ) )
Theorem	sorpsscmpl 6948*	The componentwise complement of a chain of sets is also a chain of sets. (Contributed by Stefan O'Rear, 2-Nov-2014.)
|- ( [ C.] Or Y -> [ C.] Or { u e. ~P A | ( A \ u ) e. Y } )
2.4  ZF Set Theory - add the Axiom of Union
2.4.1  Introduce the Axiom of Union
Axiom	ax-un 6949*	Axiom of Union. An axiom of Zermelo-Fraenkel set theory. It states that a set y exists that includes the union of a given set x i.e. the collection of all members of the members of x. The variant axun2 6951 states that the union itself exists. A version with the standard abbreviation for union is uniex2 6952. A version using class notation is uniex 6953. The union of a class df-uni 4437 should not be confused with the union of two classes df-un 3579. Their relationship is shown in unipr 4449. (Contributed by NM, 23-Dec-1993.)
|- E. y A. z ( E. w ( z e. w /\ w e. x ) -> z e. y )
Theorem	zfun 6950*	Axiom of Union expressed with the fewest number of different variables. (Contributed by NM, 14-Aug-2003.)
|- E. x A. y ( E. x ( y e. x /\ x e. z ) -> y e. x )
Theorem	axun2 6951*	A variant of the Axiom of Union ax-un 6949. For any set x, there exists a set y whose members are exactly the members of the members of x i.e. the union of x. Axiom Union of [BellMachover] p. 466. (Contributed by NM, 4-Jun-2006.)
|- E. y A. z ( z e. y <-> E. w ( z e. w /\ w e. x ) )
Theorem	uniex2 6952*	The Axiom of Union using the standard abbreviation for union. Given any set x, its union y exists. (Contributed by NM, 4-Jun-2006.)
|- E. y y = U. x
Theorem	uniex 6953	The Axiom of Union in class notation. This says that if A is a set i.e. A e. _V (see isset 3207), then the union of A is also a set. Same as Axiom 3 of [TakeutiZaring] p. 16. (Contributed by NM, 11-Aug-1993.)
|- A e. _V   =>    |- U. A e. _V
Theorem	vuniex 6954	The union of a setvar is a set. (Contributed by BJ, 3-May-2021.)
|- U. x e. _V
Theorem	uniexg 6955	The ZF Axiom of Union in class notation, in the form of a theorem instead of an inference. We use the antecedent A e. V instead of A e. _V to make the theorem more general and thus shorten some proofs; obviously the universal class constant _V is one possible substitution for class variable V. (Contributed by NM, 25-Nov-1994.)
|- ( A e. V -> U. A e. _V )
Theorem	unex 6956	The union of two sets is a set. Corollary 5.8 of [TakeutiZaring] p. 16. (Contributed by NM, 1-Jul-1994.)
|- A e. _V   &    |- B e. _V   =>    |- ( A u. B ) e. _V
Theorem	tpex 6957	An unordered triple of classes exists. (Contributed by NM, 10-Apr-1994.)
|- { A , B , C } e. _V
Theorem	unexb 6958	Existence of union is equivalent to existence of its components. (Contributed by NM, 11-Jun-1998.)
|- ( ( A e. _V /\ B e. _V ) <-> ( A u. B ) e. _V )
Theorem	unexg 6959	A union of two sets is a set. Corollary 5.8 of [TakeutiZaring] p. 16. (Contributed by NM, 18-Sep-2006.)
|- ( ( A e. V /\ B e. W ) -> ( A u. B ) e. _V )
Theorem	xpexg 6960	The Cartesian product of two sets is a set. Proposition 6.2 of [TakeutiZaring] p. 23. See also xpexgALT 7161. (Contributed by NM, 14-Aug-1994.)
|- ( ( A e. V /\ B e. W ) -> ( A X. B ) e. _V )
Theorem	3xpexg 6961	The Cartesian product of three sets is a set. (Contributed by Alexander van der Vekens, 21-Feb-2018.)
|- ( V e. W -> ( ( V X. V ) X. V ) e. _V )
Theorem	xpex 6962	The Cartesian product of two sets is a set. Proposition 6.2 of [TakeutiZaring] p. 23. (Contributed by NM, 14-Aug-1994.)
|- A e. _V   &    |- B e. _V   =>    |- ( A X. B ) e. _V
Theorem	sqxpexg 6963	The Cartesian square of a set is a set. (Contributed by AV, 13-Jan-2020.)
|- ( A e. V -> ( A X. A ) e. _V )
Theorem	abnexg 6964*	Sufficient condition for a class abstraction to be a proper class. The class F can be thought of as an expression in x and the abstraction appearing in the statement as the class of values F as x varies through A. Assuming the antecedents, if that class is a set, then so is the "domain" A. The converse holds without antecedent, see abrexexg 7140. Note that the second antecedent A. x e. A x e. F cannot be translated to A C_ F since F may depend on x. In applications, one may take F = { x } or F = ~P x (see snnex 6966 and pwnex 6968 respectively, proved from abnex 6965, which is a consequence of abnexg 6964 with A = _V). (Contributed by BJ, 2-Dec-2021.)
|- ( A. x e. A ( F e. V /\ x e. F ) -> ( { y | E. x e. A y = F } e. W -> A e. _V ) )
Theorem	abnex 6965*	Sufficient condition for a class abstraction to be a proper class. Lemma for snnex 6966 and pwnex 6968. See the comment of abnexg 6964. (Contributed by BJ, 2-May-2021.)
|- ( A. x ( F e. V /\ x e. F ) -> -. { y | E. x y = F } e. _V )
Theorem	snnex 6966*	The class of all singletons is a proper class. See also pwnex 6968. (Contributed by NM, 10-Oct-2008.) (Proof shortened by Eric Schmidt, 7-Dec-2008.) (Proof shortened by BJ, 5-Dec-2021.)
|- { x | E. y x = { y } } e/ _V
Theorem	snnexOLD 6967*	Obsolete proof of snnex 6966 as of 5-Dec-2021. (Contributed by NM, 10-Oct-2008.) (Proof shortened by Eric Schmidt, 7-Dec-2008.) (Proof modification is discouraged.) (New usage is discouraged.)
|- { x | E. y x = { y } } e/ _V
Theorem	pwnex 6968*	The class of all power sets is a proper class. See also snnex 6966. (Contributed by BJ, 2-May-2021.)
|- { x | E. y x = ~P y } e/ _V
Theorem	difex2 6969	If the subtrahend of a class difference exists, then the minuend exists iff the difference exists. (Contributed by NM, 12-Nov-2003.) (Proof shortened by Andrew Salmon, 12-Aug-2011.)
|- ( B e. C -> ( A e. _V <-> ( A \ B ) e. _V ) )
Theorem	difsnexi 6970	If the difference of a class and a singleton is a set, the class itself is a set. (Contributed by AV, 15-Jan-2019.)
|- ( ( N \ { K } ) e. _V -> N e. _V )
Theorem	uniuni 6971*	Expression for double union that moves union into a class builder. (Contributed by FL, 28-May-2007.)
|- U. U. A = U. { x | E. y ( x = U. y /\ y e. A ) }
Theorem	uniexr 6972	Converse of the Axiom of Union. Note that it does not require ax-un 6949. (Contributed by NM, 11-Nov-2003.)
|- ( U. A e. V -> A e. _V )
Theorem	uniexb 6973	The Axiom of Union and its converse. A class is a set iff its union is a set. (Contributed by NM, 11-Nov-2003.)
|- ( A e. _V <-> U. A e. _V )
Theorem	pwexr 6974	Converse of the Axiom of Power Sets. Note that it does not require ax-pow 4843. (Contributed by NM, 11-Nov-2003.)
|- ( ~P A e. V -> A e. _V )
Theorem	pwexb 6975	The Axiom of Power Sets and its converse. A class is a set iff its power class is a set. (Contributed by NM, 11-Nov-2003.)
|- ( A e. _V <-> ~P A e. _V )
Theorem	eldifpw 6976	Membership in a power class difference. (Contributed by NM, 25-Mar-2007.)
|- C e. _V   =>    |- ( ( A e. ~P B /\ -. C C_ B ) -> ( A u. C ) e. ( ~P ( B u. C ) \ ~P B ) )
Theorem	elpwun 6977	Membership in the power class of a union. (Contributed by NM, 26-Mar-2007.)
|- C e. _V   =>    |- ( A e. ~P ( B u. C ) <-> ( A \ C ) e. ~P B )
Theorem	iunpw 6978*	An indexed union of a power class in terms of the power class of the union of its index. Part of Exercise 24(b) of [Enderton] p. 33. (Contributed by NM, 29-Nov-2003.)
|- A e. _V   =>    |- ( E. x e. A x = U. A <-> ~P U. A = U_ x e. A ~P x )
Theorem	fr3nr 6979	A well-founded relation has no 3-cycle loops. Special case of Proposition 6.23 of [TakeutiZaring] p. 30. (Contributed by NM, 10-Apr-1994.) (Revised by Mario Carneiro, 22-Jun-2015.)
|- ( ( R Fr A /\ ( B e. A /\ C e. A /\ D e. A ) ) -> -. ( B R C /\ C R D /\ D R B ) )
Theorem	epne3 6980	A set well-founded by epsilon contains no 3-cycle loops. (Contributed by NM, 19-Apr-1994.) (Revised by Mario Carneiro, 22-Jun-2015.)
|- ( ( _E Fr A /\ ( B e. A /\ C e. A /\ D e. A ) ) -> -. ( B e. C /\ C e. D /\ D e. B ) )
Theorem	dfwe2 6981*	Alternate definition of well-ordering. Definition 6.24(2) of [TakeutiZaring] p. 30. (Contributed by NM, 16-Mar-1997.) (Proof shortened by Andrew Salmon, 12-Aug-2011.)
|- ( R We A <-> ( R Fr A /\ A. x e. A A. y e. A ( x R y \/ x = y \/ y R x ) ) )
2.4.2  Ordinals (continued)
Theorem	ordon 6982	The class of all ordinal numbers is ordinal. Proposition 7.12 of [TakeutiZaring] p. 38, but without using the Axiom of Regularity. (Contributed by NM, 17-May-1994.)
|- Ord On
Theorem	epweon 6983	The epsilon relation well-orders the class of ordinal numbers. Proposition 4.8(g) of [Mendelson] p. 244. (Contributed by NM, 1-Nov-2003.)
|- _E We On
Theorem	onprc 6984	No set contains all ordinal numbers. Proposition 7.13 of [TakeutiZaring] p. 38, but without using the Axiom of Regularity. This is also known as the Burali-Forti paradox (remark in [Enderton] p. 194). In 1897, Cesare Burali-Forti noticed that since the "set" of all ordinal numbers is an ordinal class (ordon 6982), it must be both an element of the set of all ordinal numbers yet greater than every such element. ZF set theory resolves this paradox by not allowing the class of all ordinal numbers to be a set (so instead it is a proper class). Here we prove the denial of its existence. (Contributed by NM, 18-May-1994.)
|- -. On e. _V
Theorem	ssorduni 6985	The union of a class of ordinal numbers is ordinal. Proposition 7.19 of [TakeutiZaring] p. 40. (Contributed by NM, 30-May-1994.) (Proof shortened by Andrew Salmon, 12-Aug-2011.)
|- ( A C_ On -> Ord U. A )
Theorem	ssonuni 6986	The union of a set of ordinal numbers is an ordinal number. Theorem 9 of [Suppes] p. 132. (Contributed by NM, 1-Nov-2003.)
|- ( A e. V -> ( A C_ On -> U. A e. On ) )
Theorem	ssonunii 6987	The union of a set of ordinal numbers is an ordinal number. Corollary 7N(d) of [Enderton] p. 193. (Contributed by NM, 20-Sep-2003.)
|- A e. _V   =>    |- ( A C_ On -> U. A e. On )
Theorem	ordeleqon 6988	A way to express the ordinal property of a class in terms of the class of ordinal numbers. Corollary 7.14 of [TakeutiZaring] p. 38 and its converse. (Contributed by NM, 1-Jun-2003.)
|- ( Ord A <-> ( A e. On \/ A = On ) )
Theorem	ordsson 6989	Any ordinal class is a subclass of the class of ordinal numbers. Corollary 7.15 of [TakeutiZaring] p. 38. (Contributed by NM, 18-May-1994.) (Proof shortened by Andrew Salmon, 12-Aug-2011.)
|- ( Ord A -> A C_ On )
Theorem	onss 6990	An ordinal number is a subset of the class of ordinal numbers. (Contributed by NM, 5-Jun-1994.)
|- ( A e. On -> A C_ On )
Theorem	predon 6991	For an ordinal, the predecessor under _E and On is an identity relationship. (Contributed by Scott Fenton, 27-Mar-2011.)
|- ( A e. On -> Pred ( _E , On , A ) = A )
Theorem	ssonprc 6992	Two ways of saying a class of ordinals is unbounded. (Contributed by Mario Carneiro, 8-Jun-2013.)
|- ( A C_ On -> ( A e/ _V <-> U. A = On ) )
Theorem	onuni 6993	The union of an ordinal number is an ordinal number. (Contributed by NM, 29-Sep-2006.)
|- ( A e. On -> U. A e. On )
Theorem	orduni 6994	The union of an ordinal class is ordinal. (Contributed by NM, 12-Sep-2003.)
|- ( Ord A -> Ord U. A )
Theorem	onint 6995	The intersection (infimum) of a nonempty class of ordinal numbers belongs to the class. Compare Exercise 4 of [TakeutiZaring] p. 45. (Contributed by NM, 31-Jan-1997.)
|- ( ( A C_ On /\ A =/= (/) ) -> |^| A e. A )
Theorem	onint0 6996	The intersection of a class of ordinal numbers is zero iff the class contains zero. (Contributed by NM, 24-Apr-2004.)
|- ( A C_ On -> ( |^| A = (/) <-> (/) e. A ) )
Theorem	onssmin 6997*	A nonempty class of ordinal numbers has the smallest member. Exercise 9 of [TakeutiZaring] p. 40. (Contributed by NM, 3-Oct-2003.)
|- ( ( A C_ On /\ A =/= (/) ) -> E. x e. A A. y e. A x C_ y )
Theorem	onminesb 6998	If a property is true for some ordinal number, it is true for a minimal ordinal number. This version uses explicit substitution. Theorem Schema 62 of [Suppes] p. 228. (Contributed by NM, 29-Sep-2003.)
|- ( E. x e. On ph -> [. |^| { x e. On | ph } / x ]. ph )
Theorem	onminsb 6999	If a property is true for some ordinal number, it is true for a minimal ordinal number. This version uses implicit substitution. Theorem Schema 62 of [Suppes] p. 228. (Contributed by NM, 3-Oct-2003.)
|- F/ x ps   &    |- ( x = |^| { x e. On | ph } -> ( ph <-> ps ) )   =>    |- ( E. x e. On ph -> ps )
Theorem	oninton 7000	The intersection of a nonempty collection of ordinal numbers is an ordinal number. Compare Exercise 6 of [TakeutiZaring] p. 44. (Contributed by NM, 29-Jan-1997.)
|- ( ( A C_ On /\ A =/= (/) ) -> |^| A e. On )