P. 363 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 36201-36300   *Has distinct variable group(s)

Type	Label	Description
Statement
21.25.1.2  Sophisms
Theorem	rp-fakeimass 36201	A special case where implication appears to conform to a mixed associative law. (Contributed by Richard Penner, 29-Feb-2020.)
|- ( ( ph \/ ch ) <-> ( ( ( ph -> ps ) -> ch ) <-> ( ph -> ( ps -> ch ) ) ) )
Theorem	rp-fakeanorass 36202	A special case where a mixture of and and or appears to conform to a mixed associative law. (Contributed by Richard Penner, 26-Feb-2020.)
|- ( ( ch -> ph ) <-> ( ( ( ph /\ ps ) \/ ch ) <-> ( ph /\ ( ps \/ ch ) ) ) )
Theorem	rp-fakeoranass 36203	A special case where a mixture of or and and appears to conform to a mixed associative law. (Contributed by Richard Penner, 29-Feb-2020.)
|- ( ( ph -> ch ) <-> ( ( ( ph \/ ps ) /\ ch ) <-> ( ph \/ ( ps /\ ch ) ) ) )
Theorem	rp-fakenanass 36204	A special case where nand appears to conform to a mixed associative law. (Contributed by Richard Penner, 29-Feb-2020.)
|- ( ( ph <-> ch ) <-> ( ( ( ph -/\ ps ) -/\ ch ) <-> ( ph -/\ ( ps -/\ ch ) ) ) )
Theorem	rp-fakeinunass 36205	A special case where a mixture of intersection and union appears to conform to a mixed associative law. (Contributed by Richard Penner, 26-Feb-2020.)
|- ( C C_ A <-> ( ( A i^i B ) u. C ) = ( A i^i ( B u. C ) ) )
Theorem	rp-fakeuninass 36206	A special case where a mixture of union and intersection appears to conform to a mixed associative law. (Contributed by Richard Penner, 29-Feb-2020.)
|- ( A C_ C <-> ( ( A u. B ) i^i C ) = ( A u. ( B i^i C ) ) )
21.25.1.3  Finite Sets Membership in the class of finite sets can be expressed in many ways.
Theorem	rp-isfinite5 36207*	A set is said to be finite if it can be put in one-to-one correspondence with all the natural numbers between 1 and some n e. NN0. (Contributed by Richard Penner, 3-Mar-2020.)
|- ( A e. Fin <-> E. n e. NN0 ( 1 ... n ) ~~ A )
Theorem	rp-isfinite6 36208*	A set is said to be finite if it is either empty or it can be put in one-to-one correspondence with all the natural numbers between 1 and some n e. NN. (Contributed by Richard Penner, 10-Mar-2020.)
|- ( A e. Fin <-> ( A = (/) \/ E. n e. NN ( 1 ... n ) ~~ A ) )
21.25.1.4  Infinite Sets
Theorem	pwelg 36209*	The powerclass is an element of a class closed under union and powerclass operations iff the element is a member of that class. (Contributed by RP, 21-Mar-2020.)
|- ( A. x e. B ( U. x e. B /\ ~P x e. B ) -> ( A e. B <-> ~P A e. B ) )
Theorem	pwinfig 36210*	The powerclass of an infinite set is an infinite set, and vice-versa. Here B is a class which is closed under both the union and the powerclass operations and which may have infinite sets as members. (Contributed by RP, 21-Mar-2020.)
|- ( A. x e. B ( U. x e. B /\ ~P x e. B ) -> ( A e. ( B \ Fin ) <-> ~P A e. ( B \ Fin ) ) )
Theorem	pwinfi2 36211	The powerclass of an infinite set is an infinite set, and vice-versa. Here U is a weak universe. (Contributed by RP, 21-Mar-2020.)
|- ( U e. WUni -> ( A e. ( U \ Fin ) <-> ~P A e. ( U \ Fin ) ) )
Theorem	pwinfi3 36212	The powerclass of an infinite set is an infinite set, and vice-versa. Here T is a transitive Tarski universe. (Contributed by RP, 21-Mar-2020.)
|- ( ( T e. Tarski /\ Tr T ) -> ( A e. ( T \ Fin ) <-> ~P A e. ( T \ Fin ) ) )
Theorem	pwinfi 36213	The powerclass of an infinite set is an infinite set, and vice-versa. (Contributed by RP, 21-Mar-2020.)
|- ( A e. ( _V \ Fin ) <-> ~P A e. ( _V \ Fin ) )
21.25.1.5  Finite intersection property While there is not yet a definition, the finite intersection property of a class is introduced by fiint 7874 where two textbook definitions are shown to be equivalent. This property is seen often with ordinal numbers (onin 5473, ordelinel 5540 ), chains of sets ordered by the proper subset relation (sorpssin 6606), various sets in the field of topology (inopn 19978, incld 20107, innei 20190, ... ) and "universal" classes like weak universes (wunin 9164, tskin 9210) and the class of all sets (inex1g 4560) .
Theorem	fipjust 36214*	A definition of the finite intersection property of a class based on closure under pair-wise intersection of its elements is independent of the dummy variables. (Contributed by Richard Penner, 1-Jan-2020.)
|- ( A. u e. A A. v e. A ( u i^i v ) e. A <-> A. x e. A A. y e. A ( x i^i y ) e. A )
Theorem	cllem0 36215*	The class of all sets with property ph ( z ) is closed under the binary operation on sets defined in R ( x , y ). (Contributed by Richard Penner, 3-Jan-2020.)
|- V = { z | ph }   &    |- R e. U   &    |- ( z = R -> ( ph <-> ps ) )   &    |- ( z = x -> ( ph <-> ch ) )   &    |- ( z = y -> ( ph <-> th ) )   &    |- ( ( ch /\ th ) -> ps )   =>    |- A. x e. V A. y e. V R e. V
Theorem	superficl 36216*	The class of all supersets of a class has the finite intersection property. (Contributed by Richard Penner, 1-Jan-2020.) (Proof shortened by Richard Penner, 3-Jan-2020.)
|- A = { z | B C_ z }   =>    |- A. x e. A A. y e. A ( x i^i y ) e. A
Theorem	superuncl 36217*	The class of all supersets of a class is closed under binary union. (Contributed by Richard Penner, 3-Jan-2020.)
|- A = { z | B C_ z }   =>    |- A. x e. A A. y e. A ( x u. y ) e. A
Theorem	ssficl 36218*	The class of all subsets of a class has the finite intersection property. (Contributed by Richard Penner, 1-Jan-2020.) (Proof shortened by Richard Penner, 3-Jan-2020.)
|- A = { z | z C_ B }   =>    |- A. x e. A A. y e. A ( x i^i y ) e. A
Theorem	ssuncl 36219*	The class of all subsets of a class is closed under binary union. (Contributed by Richard Penner, 3-Jan-2020.)
|- A = { z | z C_ B }   =>    |- A. x e. A A. y e. A ( x u. y ) e. A
Theorem	ssdifcl 36220*	The class of all subsets of a class is closed under class difference. (Contributed by Richard Penner, 3-Jan-2020.)
|- A = { z | z C_ B }   =>    |- A. x e. A A. y e. A ( x \ y ) e. A
Theorem	sssymdifcl 36221*	The class of all subsets of a class is closed under symmetric difference. (Contributed by Richard Penner, 3-Jan-2020.)
|- A = { z | z C_ B }   =>    |- A. x e. A A. y e. A ( ( x \ y ) u. ( y \ x ) ) e. A
Theorem	fiinfi 36222*	If two classes have the finite intersection property, then so does their intersection. (Contributed by Richard Penner, 1-Jan-2020.)
|- ( ph -> A. x e. A A. y e. A ( x i^i y ) e. A )   &    |- ( ph -> A. x e. B A. y e. B ( x i^i y ) e. B )   &    |- ( ph -> C = ( A i^i B ) )   =>    |- ( ph -> A. x e. C A. y e. C ( x i^i y ) e. C )
21.25.1.6  RP ADDTO: The universal class
Theorem	elabd 36223*	Explicit demonstration the class { x | ps } is not empty by the example X. (Contributed by RP, 12-Aug-2020.)
|- ( ph -> X e. _V )   &    |- ( ph -> ch )   &    |- ( x = X -> ( ps <-> ch ) )   =>    |- ( ph -> E. x ps )
21.25.1.7  RP ADDTO: Subclasses and subsets
Theorem	rababg 36224	Condition when restricted class is equal to unrestricted class. (Contributed by RP, 13-Aug-2020.)
|- ( A. x ( ph -> x e. A ) <-> { x e. A | ph } = { x | ph } )
21.25.1.8  RP ADDTO: The intersection of a class
Theorem	elintabg 36225*	Two ways of saying a set is an element of the intersection of a class. (Contributed by RP, 13-Aug-2020.)
|- ( A e. V -> ( A e. |^| { x | ph } <-> A. x ( ph -> A e. x ) ) )
Theorem	elinintab 36226*	Two ways of saying a set is an element of the intersection of a class with the intersection of a class. (Contributed by RP, 13-Aug-2020.)
|- ( A e. ( B i^i |^| { x | ph } ) <-> ( A e. B /\ A. x ( ph -> A e. x ) ) )
Theorem	elmapintrab 36227*	Two ways to say a set is an element of the intersection of a class of images. (Contributed by RP, 16-Aug-2020.)
|- C e. _V   &    |- C C_ B   =>    |- ( A e. V -> ( A e. |^| { w e. ~P B | E. x ( w = C /\ ph ) } <-> ( ( E. x ph -> A e. B ) /\ A. x ( ph -> A e. C ) ) ) )
21.25.1.9  RP ADDTO: Theorems requiring subset and intersection existence
Theorem	elinintrab 36228*	Two ways of saying a set is an element of the intersection of a class with the intersection of a class. (Contributed by RP, 14-Aug-2020.)
|- ( A e. V -> ( A e. |^| { w e. ~P B | E. x ( w = ( B i^i x ) /\ ph ) } <-> ( ( E. x ph -> A e. B ) /\ A. x ( ph -> A e. x ) ) ) )
Theorem	inintabss 36229*	Upper bound on intersection of class and the intersection of a class. (Contributed by RP, 13-Aug-2020.)
|- ( A i^i |^| { x | ph } ) C_ |^| { w e. ~P A | E. x ( w = ( A i^i x ) /\ ph ) }
Theorem	inintabd 36230*	Value of the intersection of class with the intersection of a non-empty class. (Contributed by RP, 13-Aug-2020.)
|- ( ph -> E. x ps )   =>    |- ( ph -> ( A i^i |^| { x | ps } ) = |^| { w e. ~P A | E. x ( w = ( A i^i x ) /\ ps ) } )
21.25.1.10  RP ADDTO: Relations
Theorem	xpinintabd 36231*	Value of the intersection of cross-product with the intersection of a non-empty class. (Contributed by RP, 12-Aug-2020.)
|- ( ph -> E. x ps )   =>    |- ( ph -> ( ( A X. B ) i^i |^| { x | ps } ) = |^| { w e. ~P ( A X. B ) | E. x ( w = ( ( A X. B ) i^i x ) /\ ps ) } )
Theorem	relintabex 36232	If the intersection of a class is a relation, then the class is non-empty. (Contributed by RP, 12-Aug-2020.)
|- ( Rel |^| { x | ph } -> E. x ph )
Theorem	elcnvcnvintab 36233*	Two ways of saying a set is an element of the converse of the converse of the intersection of a class. (Contributed by RP, 20-Aug-2020.)
|- ( A e. `' `' |^| { x | ph } <-> ( A e. ( _V X. _V ) /\ A. x ( ph -> A e. x ) ) )
Theorem	relintab 36234*	Value of the intersection of a class when it is a relation. (Contributed by RP, 12-Aug-2020.)
|- ( Rel |^| { x | ph } -> |^| { x | ph } = |^| { w e. ~P ( _V X. _V ) | E. x ( w = `' `' x /\ ph ) } )
Theorem	nonrel 36235	A non-relation is equal to the base class with all ordered pairs removed. (Contributed by RP, 25-Oct-2020.)
|- ( A \ `' `' A ) = ( A \ ( _V X. _V ) )
Theorem	elnonrel 36236	Only an ordered pair where not both entries are sets could be an element of the non-relation part of class. (Contributed by RP, 25-Oct-2020.)
|- ( <. X , Y >. e. ( A \ `' `' A ) <-> ( (/) e. A /\ -. ( X e. _V /\ Y e. _V ) ) )
Theorem	cnvssb 36237	Subclass theorem for converse. (Contributed by RP, 22-Oct-2020.)
|- ( Rel A -> ( A C_ B <-> `' A C_ `' B ) )
Theorem	relnonrel 36238	The non-relation part of a relation is empty. (Contributed by RP, 22-Oct-2020.)
|- ( Rel A <-> ( A \ `' `' A ) = (/) )
Theorem	cnvnonrel 36239	The converse of the non-relation part of a class is empty. (Contributed by RP, 18-Oct-2020.)
|- `' ( A \ `' `' A ) = (/)
Theorem	brnonrel 36240	A non-relation cannot relate any two classes. (Contributed by RP, 23-Oct-2020.)
|- ( ( X e. U /\ Y e. V ) -> -. X ( A \ `' `' A ) Y )
Theorem	dmnonrel 36241	The domain of the non-relation part of a class is empty. (Contributed by RP, 22-Oct-2020.)
|- dom ( A \ `' `' A ) = (/)
Theorem	rnnonrel 36242	The range of the non-relation part of a class is empty. (Contributed by RP, 22-Oct-2020.)
|- ran ( A \ `' `' A ) = (/)
Theorem	resnonrel 36243	A restriction of the non-relation part of a class is empty. (Contributed by RP, 22-Oct-2020.)
|- ( ( A \ `' `' A ) |` B ) = (/)
Theorem	imanonrel 36244	An image under the non-relation part of a class is empty. (Contributed by RP, 22-Oct-2020.)
|- ( ( A \ `' `' A ) " B ) = (/)
Theorem	cononrel1 36245	Composition with the non-relation part of a class is empty. (Contributed by RP, 22-Oct-2020.)
|- ( ( A \ `' `' A ) o. B ) = (/)
Theorem	cononrel2 36246	Composition with the non-relation part of a class is empty. (Contributed by RP, 22-Oct-2020.)
|- ( A o. ( B \ `' `' B ) ) = (/)
21.25.1.11  RP ADDTO: Functions See also idssxp 28276 by Thierry Arnoux.
Theorem	elmapintab 36247*	Two ways to say a set is an element of mapped intersection of a class. Here F maps elements of C to elements of |^| { x | ph } or x. (Contributed by RP, 19-Aug-2020.)
|- ( A e. B <-> ( A e. C /\ ( F ` A ) e. |^| { x | ph } ) )   &    |- ( A e. E <-> ( A e. C /\ ( F ` A ) e. x ) )   =>    |- ( A e. B <-> ( A e. C /\ A. x ( ph -> A e. E ) ) )
Theorem	fvnonrel 36248	The function value of any class under a non-relation is empty. (Contributed by RP, 23-Oct-2020.)
|- ( ( A \ `' `' A ) ` X ) = (/)
Theorem	elinlem 36249	Two ways to say a set is a member of an intersection. (Contributed by RP, 19-Aug-2020.)
|- ( A e. ( B i^i C ) <-> ( A e. B /\ ( _I ` A ) e. C ) )
Theorem	elcnvcnvlem 36250	Two ways to say a set is a member of the converse of the converse of a class. (Contributed by RP, 20-Aug-2020.)
|- ( A e. `' `' B <-> ( A e. ( _V X. _V ) /\ ( _I ` A ) e. B ) )
21.25.1.12  RP ADDTO: Finite induction (for finite ordinals) Original probably needs new subsection for Relation-related existence theorems.
Theorem	cnvcnvintabd 36251*	Value of the relationship content of the intersection of a class. (Contributed by RP, 20-Aug-2020.)
|- ( ph -> E. x ps )   =>    |- ( ph -> `' `' |^| { x | ps } = |^| { w e. ~P ( _V X. _V ) | E. x ( w = `' `' x /\ ps ) } )
21.25.1.13  RP ADDTO: First and second members of an ordered pair
Theorem	elcnvlem 36252	Two ways to say a set is a member of the converse of a class. (Contributed by RP, 19-Aug-2020.)
|- F = ( x e. ( _V X. _V ) |-> <. ( 2nd ` x ) , ( 1st ` x ) >. )   =>    |- ( A e. `' B <-> ( A e. ( _V X. _V ) /\ ( F ` A ) e. B ) )
Theorem	elcnvintab 36253*	Two ways of saying a set is an element of the converse of the intersection of a class. (Contributed by RP, 19-Aug-2020.)
|- ( A e. `' |^| { x | ph } <-> ( A e. ( _V X. _V ) /\ A. x ( ph -> A e. `' x ) ) )
Theorem	cnvintabd 36254*	Value of the converse of the intersection of a non-empty class. (Contributed by RP, 20-Aug-2020.)
|- ( ph -> E. x ps )   =>    |- ( ph -> `' |^| { x | ps } = |^| { w e. ~P ( _V X. _V ) | E. x ( w = `' x /\ ps ) } )
21.25.1.14  RP ADDTO: The reflexive and transitive properties of relations
Theorem	undmrnresiss 36255*	Two ways of saying the identity relation restricted to the union of the domain and range of a relation is a subset of a relation. Generalization of reflexg 36256. (Contributed by RP, 26-Sep-2020.)
|- ( ( _I |` ( dom A u. ran A ) ) C_ B <-> A. x A. y ( x A y -> ( x B x /\ y B y ) ) )
Theorem	reflexg 36256*	Two ways of saying a relation is reflexive over its domain and range. (Contributed by RP, 4-Aug-2020.)
|- ( ( _I |` ( dom A u. ran A ) ) C_ A <-> A. x A. y ( x A y -> ( x A x /\ y A y ) ) )
Theorem	cnvssco 36257*	A condition weaker than reflexivity. (Contributed by RP, 3-Aug-2020.)
|- ( `' A C_ `' ( B o. C ) <-> A. x A. y E. z ( x A y -> ( x C z /\ z B y ) ) )
Theorem	refimssco 36258	Reflexive relations are subsets of their self-composition. (Contributed by RP, 4-Aug-2020.)
|- ( ( _I |` ( dom A u. ran A ) ) C_ A -> `' A C_ `' ( A o. A ) )
21.25.1.15  RP ADDTO: Basic properties of closures
Theorem	cleq2lem 36259	Equality implies bijection. (Contributed by RP, 24-Jul-2020.)
|- ( A = B -> ( ph <-> ps ) )   =>    |- ( A = B -> ( ( R C_ A /\ ph ) <-> ( R C_ B /\ ps ) ) )
Theorem	cbvcllem 36260*	Change of bound variable in class of supersets of a with a property. (Contributed by RP, 24-Jul-2020.)
|- ( x = y -> ( ph <-> ps ) )   =>    |- { x | ( X C_ x /\ ph ) } = { y | ( X C_ y /\ ps ) }
Theorem	intabssd 36261*	When for each element y there is a subset A which may substituted for x such that y satisfying ch implies x satisfies ps then the intersection of all x that satisfy ps is a subclass the intersection of all y that satisfy ch. (Contributed by RP, 17-Oct-2020.)
|- ( ph -> A e. V )   &    |- ( ( ph /\ x = A ) -> ( ch -> ps ) )   &    |- ( ph -> A C_ y )   =>    |- ( ph -> |^| { x | ps } C_ |^| { y | ch } )
Theorem	clublem 36262*	If a superset Y of X possesses the property parameterized in x in ps, then Y is a superset of the closure of that property for the set X. (Contributed by RP, 23-Jul-2020.)
|- ( ph -> Y e. _V )   &    |- ( x = Y -> ( ps <-> ch ) )   &    |- ( ph -> X C_ Y )   &    |- ( ph -> ch )   =>    |- ( ph -> |^| { x | ( X C_ x /\ ps ) } C_ Y )
Theorem	clss2lem 36263*	The closure of a property is a superset of the closure of a less restrictive property. (Contributed by RP, 24-Jul-2020.)
|- ( ph -> ( ch -> ps ) )   =>    |- ( ph -> |^| { x | ( X C_ x /\ ps ) } C_ |^| { x | ( X C_ x /\ ch ) } )
Theorem	dfid7 36264*	Definition of identity relation as the trivial closure. (Contributed by RP, 26-Jul-2020.)
|- _I = ( x e. _V |-> |^| { y | ( x C_ y /\ T. ) } )
Theorem	mptrcllem 36265*	Show two versions of a closure with reflexive properties are equal. (Contributed by RP, 19-Oct-2020.)
|- ( x e. V -> |^| { y | ( x C_ y /\ ( ph /\ ( _I |` ( dom y u. ran y ) ) C_ y ) ) } e. _V )   &    |- ( x e. V -> |^| { z | ( ( x u. ( _I |` ( dom x u. ran x ) ) ) C_ z /\ ps ) } e. _V )   &    |- ( x e. V -> ch )   &    |- ( x e. V -> th )   &    |- ( x e. V -> ta )   &    |- ( y = |^| { z | ( ( x u. ( _I |` ( dom x u. ran x ) ) ) C_ z /\ ps ) } -> ( ph <-> ch ) )   &    |- ( y = |^| { z | ( ( x u. ( _I |` ( dom x u. ran x ) ) ) C_ z /\ ps ) } -> ( ( _I |` ( dom y u. ran y ) ) C_ y <-> th ) )   &    |- ( z = |^| { y | ( x C_ y /\ ( ph /\ ( _I |` ( dom y u. ran y ) ) C_ y ) ) } -> ( ps <-> ta ) )   =>    |- ( x e. V |-> |^| { y | ( x C_ y /\ ( ph /\ ( _I |` ( dom y u. ran y ) ) C_ y ) ) } ) = ( x e. V |-> |^| { z | ( ( x u. ( _I |` ( dom x u. ran x ) ) ) C_ z /\ ps ) } )
Theorem	cotrintab 36266	The intersection of a class is a transitive relation if membership in the class implies the member is a transitive relation. (Contributed by RP, 28-Oct-2020.)
|- ( ph -> ( x o. x ) C_ x )   =>    |- ( |^| { x | ph } o. |^| { x | ph } ) C_ |^| { x | ph }
Theorem	rclexi 36267*	The reflexive closure of a set exists. (Contributed by RP, 27-Oct-2020.)
|- A e. V   =>    |- |^| { x | ( A C_ x /\ ( _I |` ( dom x u. ran x ) ) C_ x ) } e. _V
Theorem	rtrclexlem 36268	Existence of relation implies existence of union with Cartesian product of domain and range. (Contributed by RP, 1-Nov-2020.)
|- ( R e. V -> ( R u. ( ( dom R u. ran R ) X. ( dom R u. ran R ) ) ) e. _V )
Theorem	rtrclex 36269*	The reflexive-transitive closure of a set exists. (Contributed by RP, 1-Nov-2020.)
|- ( A e. _V <-> |^| { x | ( A C_ x /\ ( ( x o. x ) C_ x /\ ( _I |` ( dom x u. ran x ) ) C_ x ) ) } e. _V )
Theorem	trclubgNEW 36270*	If a relation exists then the transitive closure has an upper bound. (Contributed by RP, 24-Jul-2020.)
|- ( ph -> R e. _V )   =>    |- ( ph -> |^| { x | ( R C_ x /\ ( x o. x ) C_ x ) } C_ ( R u. ( dom R X. ran R ) ) )
Theorem	trclubNEW 36271*	If a relation exists then the transitive closure has an upper bound. (Contributed by RP, 24-Jul-2020.)
|- ( ph -> R e. _V )   &    |- ( ph -> Rel R )   =>    |- ( ph -> |^| { x | ( R C_ x /\ ( x o. x ) C_ x ) } C_ ( dom R X. ran R ) )
Theorem	trclexi 36272*	The transitive closure of a set exists. (Contributed by RP, 27-Oct-2020.)
|- A e. V   =>    |- |^| { x | ( A C_ x /\ ( x o. x ) C_ x ) } e. _V
Theorem	rtrclexi 36273*	The reflexive-transitive closure of a set exists. (Contributed by RP, 27-Oct-2020.)
|- A e. V   =>    |- |^| { x | ( A C_ x /\ ( ( x o. x ) C_ x /\ ( _I |` ( dom x u. ran x ) ) C_ x ) ) } e. _V
Theorem	clrellem 36274*	When the property ps holds for a relation substituted for x, then the closure on that property is a relation if the base set is a relation. (Contributed by RP, 30-Jul-2020.)
|- ( ph -> Y e. _V )   &    |- ( ph -> Rel X )   &    |- ( x = `' `' Y -> ( ps <-> ch ) )   &    |- ( ph -> X C_ Y )   &    |- ( ph -> ch )   =>    |- ( ph -> Rel |^| { x | ( X C_ x /\ ps ) } )
Theorem	clcnvlem 36275*	When A, an upper bound of the closure, exists and certain substitutions hold the converse of the closure is equal to the closure of the converse. (Contributed by RP, 18-Oct-2020.)
|- ( ( ph /\ x = ( `' y u. ( X \ `' `' X ) ) ) -> ( ch -> ps ) )   &    |- ( ( ph /\ y = `' x ) -> ( ps -> ch ) )   &    |- ( x = A -> ( ps <-> th ) )   &    |- ( ph -> X C_ A )   &    |- ( ph -> A e. _V )   &    |- ( ph -> th )   =>    |- ( ph -> `' |^| { x | ( X C_ x /\ ps ) } = |^| { y | ( `' X C_ y /\ ch ) } )
Theorem	cnvtrucl0 36276*	The converse of the trivial closure is equal to the closure of the converse. (Contributed by RP, 18-Oct-2020.)
|- ( X e. V -> `' |^| { x | ( X C_ x /\ T. ) } = |^| { y | ( `' X C_ y /\ T. ) } )
Theorem	cnvrcl0 36277*	The converse of the reflexive closure is equal to the closure of the converse. (Contributed by RP, 18-Oct-2020.)
|- ( X e. V -> `' |^| { x | ( X C_ x /\ ( _I |` ( dom x u. ran x ) ) C_ x ) } = |^| { y | ( `' X C_ y /\ ( _I |` ( dom y u. ran y ) ) C_ y ) } )
Theorem	cnvtrcl0 36278*	The converse of the transitive closure is equal to the closure of the converse. (Contributed by RP, 18-Oct-2020.)
|- ( X e. V -> `' |^| { x | ( X C_ x /\ ( x o. x ) C_ x ) } = |^| { y | ( `' X C_ y /\ ( y o. y ) C_ y ) } )
Theorem	dmtrcl 36279*	The domain of the transitive closure is equal to the domain of its base relation. (Contributed by RP, 1-Nov-2020.)
|- ( X e. V -> dom |^| { x | ( X C_ x /\ ( x o. x ) C_ x ) } = dom X )
Theorem	rntrcl 36280*	The range of the transitive closure is equal to the range of its base relation. (Contributed by RP, 1-Nov-2020.)
|- ( X e. V -> ran |^| { x | ( X C_ x /\ ( x o. x ) C_ x ) } = ran X )
Theorem	dfrtrcl5 36281*	Definition of reflexive-transitive closure as a standard closure. (Contributed by RP, 1-Nov-2020.)
|- t* = ( x e. _V |-> |^| { y | ( x C_ y /\ ( ( _I |` ( dom y u. ran y ) ) C_ y /\ ( y o. y ) C_ y ) ) } )
21.25.1.16  RP REPLACE: Definitions and basic properties of transitive closures
Theorem	trcleq2lemRP 36282	Equality implies bijection. (Contributed by RP, 5-May-2020.) (Proof modification is discouraged.)
|- ( A = B -> ( ( R C_ A /\ ( A o. A ) C_ A ) <-> ( R C_ B /\ ( B o. B ) C_ B ) ) )
21.25.2  Additional statements on relations and subclasses
Theorem	al3im 36283	Version of ax-4 1693 for a nested implication. (Contributed by RP, 13-Apr-2020.)
|- ( A. x ( ph -> ( ps -> ( ch -> th ) ) ) -> ( A. x ph -> ( A. x ps -> ( A. x ch -> A. x th ) ) ) )
Theorem	intima0 36284*	Two ways of expressing the intersection of images of a class. (Contributed by RP, 13-Apr-2020.)
|- |^|_ a e. A ( a " B ) = |^| { x | E. a e. A x = ( a " B ) }
Theorem	elimaint 36285*	Element of image of intersection. (Contributed by RP, 13-Apr-2020.)
|- ( y e. ( |^| A " B ) <-> E. b e. B A. a e. A <. b , y >. e. a )
Theorem	csbcog 36286	Distribute proper substitution through a composition of relations. (Contributed by RP, 28-Jun-2020.)
|- ( A e. V -> [_ A / x ]_ ( B o. C ) = ( [_ A / x ]_ B o. [_ A / x ]_ C ) )
Theorem	cnviun 36287*	Converse of indexed union. (Contributed by RP, 20-Jun-2020.)
|- `' U_ x e. A B = U_ x e. A `' B
Theorem	imaiun1 36288*	The image of an indexed union is the indexed union of the images. (Contributed by RP, 29-Jun-2020.)
|- ( U_ x e. A B " C ) = U_ x e. A ( B " C )
Theorem	coiun1 36289*	Composition with an indexed union. Proof analgous to that of coiun 5364. (Contributed by RP, 20-Jun-2020.)
|- ( U_ x e. C A o. B ) = U_ x e. C ( A o. B )
Theorem	elintima 36290*	Element of intersection of images. (Contributed by RP, 13-Apr-2020.)
|- ( y e. |^| { x | E. a e. A x = ( a " B ) } <-> A. a e. A E. b e. B <. b , y >. e. a )
Theorem	intimass 36291*	The image under the intersection of relations is a subset of the intersection of the images. (Contributed by RP, 13-Apr-2020.)
|- ( |^| A " B ) C_ |^| { x | E. a e. A x = ( a " B ) }
Theorem	intimass2 36292*	The image under the intersection of relations is a subset of the intersection of the images. (Contributed by RP, 13-Apr-2020.)
|- ( |^| A " B ) C_ |^|_ x e. A ( x " B )
Theorem	intimag 36293*	Requirement for the image under the intersection of relations to equal the intersection of the images of those relations. (Contributed by RP, 13-Apr-2020.)
|- ( A. y ( A. a e. A E. b e. B <. b , y >. e. a -> E. b e. B A. a e. A <. b , y >. e. a ) -> ( |^| A " B ) = |^| { x | E. a e. A x = ( a " B ) } )
Theorem	intimasn 36294*	Two ways to express the image of a singleton when the relation is an intersection. (Contributed by RP, 13-Apr-2020.)
|- ( B e. V -> ( |^| A " { B } ) = |^| { x | E. a e. A x = ( a " { B } ) } )
Theorem	intimasn2 36295*	Two ways to express the image of a singleton when the relation is an intersection. (Contributed by RP, 13-Apr-2020.)
|- ( B e. V -> ( |^| A " { B } ) = |^|_ x e. A ( x " { B } ) )
Theorem	ss2iundf 36296*	Subclass theorem for indexed union. (Contributed by RP, 17-Jul-2020.)
|- F/ x ph   &    |- F/ y ph   &    |- F/_ y Y   &    |- F/_ y A   &    |- F/_ y B   &    |- F/_ x C   &    |- F/_ y C   &    |- F/_ x D   &    |- F/_ y G   &    |- ( ( ph /\ x e. A ) -> Y e. C )   &    |- ( ( ph /\ x e. A /\ y = Y ) -> D = G )   &    |- ( ( ph /\ x e. A ) -> B C_ G )   =>    |- ( ph -> U_ x e. A B C_ U_ y e. C D )
Theorem	ss2iundv 36297*	Subclass theorem for indexed union. (Contributed by RP, 17-Jul-2020.)
|- ( ( ph /\ x e. A ) -> Y e. C )   &    |- ( ( ph /\ x e. A /\ y = Y ) -> D = G )   &    |- ( ( ph /\ x e. A ) -> B C_ G )   =>    |- ( ph -> U_ x e. A B C_ U_ y e. C D )
Theorem	cbviuneq12df 36298*	Rule used to change the bound variables and classes in an indexed union, with the substitution specified implicitly by the hypothesis. (Contributed by RP, 17-Jul-2020.)
|- F/ x ph   &    |- F/ y ph   &    |- F/_ x X   &    |- F/_ y Y   &    |- F/_ x A   &    |- F/_ y A   &    |- F/_ y B   &    |- F/_ x C   &    |- F/_ y C   &    |- F/_ x D   &    |- F/_ x F   &    |- F/_ y G   &    |- ( ( ph /\ y e. C ) -> X e. A )   &    |- ( ( ph /\ x e. A ) -> Y e. C )   &    |- ( ( ph /\ y e. C /\ x = X ) -> B = F )   &    |- ( ( ph /\ x e. A /\ y = Y ) -> D = G )   &    |- ( ( ph /\ x e. A ) -> B = G )   &    |- ( ( ph /\ y e. C ) -> D = F )   =>    |- ( ph -> U_ x e. A B = U_ y e. C D )
Theorem	cbviuneq12dv 36299*	Rule used to change the bound variables and classes in an indexed union, with the substitution specified implicitly by the hypothesis. (Contributed by RP, 17-Jul-2020.)
|- ( ( ph /\ y e. C ) -> X e. A )   &    |- ( ( ph /\ x e. A ) -> Y e. C )   &    |- ( ( ph /\ y e. C /\ x = X ) -> B = F )   &    |- ( ( ph /\ x e. A /\ y = Y ) -> D = G )   &    |- ( ( ph /\ x e. A ) -> B = G )   &    |- ( ( ph /\ y e. C ) -> D = F )   =>    |- ( ph -> U_ x e. A B = U_ y e. C D )
Theorem	conrel1d 36300	Deduction about composition with a class with no relational content. (Contributed by Richard Penner, 24-Dec-2019.)
|- ( ph -> `' A = (/) )   =>    |- ( ph -> ( A o. B ) = (/) )