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
Theorem	iunrelexp0 36201*	Simplification of zeroth power of indexed union of powers of relations. (Contributed by RP, 19-Jun-2020.)
|- ( ( R e. V /\ Z C_ NN0 /\ ( { 0 , 1 } i^i Z ) =/= (/) ) -> ( U_ x e. Z ( R ^r x ) ^r 0 ) = ( R ^r 0 ) )
Theorem	relexpxpnnidm 36202	Any positive power of a cross product of non-disjoint sets is itself. (Contributed by RP, 13-Jun-2020.)
|- ( N e. NN -> ( ( A e. U /\ B e. V /\ ( A i^i B ) =/= (/) ) -> ( ( A X. B ) ^r N ) = ( A X. B ) ) )
Theorem	relexpiidm 36203	Any power of any restriction of the identity relation is itself. (Contributed by RP, 12-Jun-2020.)
|- ( ( A e. V /\ N e. NN0 ) -> ( ( _I |` A ) ^r N ) = ( _I |` A ) )
Theorem	relexpss1d 36204	The relational power of a subset is a subset. (Contributed by RP, 17-Jun-2020.)
|- ( ph -> A C_ B )   &    |- ( ph -> B e. _V )   &    |- ( ph -> N e. NN0 )   =>    |- ( ph -> ( A ^r N ) C_ ( B ^r N ) )
Theorem	comptiunov2i 36205*	The composition two indexed unions is sometimes a similar indexed union. (Contributed by RP, 10-Jun-2020.)
|- X = ( a e. _V |-> U_ i e. I ( a .^ i ) )   &    |- Y = ( b e. _V |-> U_ j e. J ( b .^ j ) )   &    |- Z = ( c e. _V |-> U_ k e. K ( c .^ k ) )   &    |- I e. _V   &    |- J e. _V   &    |- K = ( I u. J )   &    |- U_ k e. I ( d .^ k ) C_ U_ i e. I ( U_ j e. J ( d .^ j ) .^ i )   &    |- U_ k e. J ( d .^ k ) C_ U_ i e. I ( U_ j e. J ( d .^ j ) .^ i )   &    |- U_ i e. I ( U_ j e. J ( d .^ j ) .^ i ) C_ U_ k e. ( I u. J ) ( d .^ k )   =>    |- ( X o. Y ) = Z
Theorem	corclrcl 36206	The reflexive closure is idempotent. (Contributed by RP, 13-Jun-2020.)
|- ( r* o. r* ) = r*
Theorem	iunrelexpmin1 36207*	The indexed union of relation exponentiation over the natural numbers is the minimum transitive relation that includes the relation. (Contributed by RP, 4-Jun-2020.)
|- C = ( r e. _V |-> U_ n e. N ( r ^r n ) )   =>    |- ( ( R e. V /\ N = NN ) -> A. s ( ( R C_ s /\ ( s o. s ) C_ s ) -> ( C ` R ) C_ s ) )
Theorem	relexpmulnn 36208	With exponents limited to the counting numbers, the composition of powers of a relation is the relation raised to the product of exponents. (Contributed by RP, 13-Jun-2020.)
|- ( ( ( R e. V /\ I = ( J x. K ) ) /\ ( J e. NN /\ K e. NN ) ) -> ( ( R ^r J ) ^r K ) = ( R ^r I ) )
Theorem	relexpmulg 36209	With ordered exponents, the composition of powers of a relation is the relation raised to the product of exponents. (Contributed by RP, 13-Jun-2020.)
|- ( ( ( R e. V /\ I = ( J x. K ) /\ ( I = 0 -> J <_ K ) ) /\ ( J e. NN0 /\ K e. NN0 ) ) -> ( ( R ^r J ) ^r K ) = ( R ^r I ) )
Theorem	trclrelexplem 36210*	The union of relational powers to positive multiples of N is a subset to the transitive closure raised to the power of N. (Contributed by RP, 15-Jun-2020.)
|- ( N e. NN -> U_ k e. NN ( ( D ^r k ) ^r N ) C_ ( U_ j e. NN ( D ^r j ) ^r N ) )
Theorem	iunrelexpmin2 36211*	The indexed union of relation exponentiation over the natural numbers (including zero) is the minimum reflexive-transitive relation that includes the relation. (Contributed by RP, 4-Jun-2020.)
|- C = ( r e. _V |-> U_ n e. N ( r ^r n ) )   =>    |- ( ( R e. V /\ N = NN0 ) -> A. s ( ( ( _I |` ( dom R u. ran R ) ) C_ s /\ R C_ s /\ ( s o. s ) C_ s ) -> ( C ` R ) C_ s ) )
Theorem	relexp01min 36212	With exponents limited to 0 and 1, the composition of powers of a relation is the relation raised to the minimum of exponents. (Contributed by RP, 12-Jun-2020.)
|- ( ( ( R e. V /\ I = if ( J < K , J , K ) ) /\ ( J e. { 0 , 1 } /\ K e. { 0 , 1 } ) ) -> ( ( R ^r J ) ^r K ) = ( R ^r I ) )
Theorem	relexp1idm 36213	Repeated raising a relation to the first power is idempotent. (Contributed by RP, 12-Jun-2020.)
|- ( R e. V -> ( ( R ^r 1 ) ^r 1 ) = ( R ^r 1 ) )
Theorem	relexp0idm 36214	Repeated raising a relation to the zeroth power is idempotent. (Contributed by RP, 12-Jun-2020.)
|- ( R e. V -> ( ( R ^r 0 ) ^r 0 ) = ( R ^r 0 ) )
Theorem	relexp0a 36215	Absorbtion law for zeroth power of a relation. (Contributed by RP, 17-Jun-2020.)
|- ( ( A e. V /\ N e. NN0 ) -> ( ( A ^r N ) ^r 0 ) C_ ( A ^r 0 ) )
Theorem	relexpxpmin 36216	The composition of powers of a cross-product of non-disjoint sets is the cross product raised to the minimum exponent. (Contributed by RP, 13-Jun-2020.)
|- ( ( ( A e. U /\ B e. V /\ ( A i^i B ) =/= (/) ) /\ ( I = if ( J < K , J , K ) /\ J e. NN0 /\ K e. NN0 ) ) -> ( ( ( A X. B ) ^r J ) ^r K ) = ( ( A X. B ) ^r I ) )
Theorem	relexpaddss 36217	The composition of two powers of a relation is a subset of the relation raised to the sum of those exponents. This is equality where R is a relation as shown by relexpaddd 13054 or when the sum of the powers isn't 1 as shown by relexpaddg 13053. (Contributed by RP, 3-Jun-2020.)
|- ( ( N e. NN0 /\ M e. NN0 /\ R e. V ) -> ( ( R ^r N ) o. ( R ^r M ) ) C_ ( R ^r ( N + M ) ) )
Theorem	iunrelexpuztr 36218*	The indexed union of relation exponentiation over upper integers is a transive relation. Generalized from rtrclreclem3 13060. (Contributed by RP, 4-Jun-2020.)
|- C = ( r e. _V |-> U_ n e. N ( r ^r n ) )   =>    |- ( ( R e. V /\ N = ( ZZ>= ` M ) /\ M e. NN0 ) -> ( ( C ` R ) o. ( C ` R ) ) C_ ( C ` R ) )
21.25.2.4  Transitive closure of a relation
Theorem	dftrcl3 36219*	Transitive closure of a relation, expressed as indexed union of powers of relations. (Contributed by RP, 5-Jun-2020.)
|- t+ = ( r e. _V |-> U_ n e. NN ( r ^r n ) )
Theorem	brfvtrcld 36220*	If two elements are connected by the transitive closure of a relation, then they are connected via n instances the relation, for some counting number n. (Contributed by RP, 22-Jul-2020.)
|- ( ph -> R e. _V )   =>    |- ( ph -> ( A ( t+ ` R ) B <-> E. n e. NN A ( R ^r n ) B ) )
Theorem	fvtrcllb1d 36221	A set is a subset of its image under the transitive closure. (Contributed by RP, 22-Jul-2020.)
|- ( ph -> R e. _V )   =>    |- ( ph -> R C_ ( t+ ` R ) )
Theorem	trclfvcom 36222	The transitive closure of a relation commutes with the relation. (Contributed by RP, 18-Jul-2020.)
|- ( R e. V -> ( ( t+ ` R ) o. R ) = ( R o. ( t+ ` R ) ) )
Theorem	cnvtrclfv 36223	The converse of the transitive closure is equal to the transitive closure of the converse relation. (Contributed by RP, 19-Jul-2020.)
|- ( R e. V -> `' ( t+ ` R ) = ( t+ ` `' R ) )
Theorem	cotrcltrcl 36224	The transitive closure is idempotent. (Contributed by RP, 16-Jun-2020.)
|- ( t+ o. t+ ) = t+
Theorem	trclimalb2 36225	Lower bound for image under a transitive closure. (Contributed by RP, 1-Jul-2020.)
|- ( ( R e. V /\ ( R " ( A u. B ) ) C_ B ) -> ( ( t+ ` R ) " A ) C_ B )
Theorem	brtrclfv2 36226*	Two ways to indicate two elements are related by the transitive closure of a relation. (Contributed by RP, 1-Jul-2020.)
|- ( ( X e. U /\ Y e. V /\ R e. W ) -> ( X ( t+ ` R ) Y <-> Y e. |^| { f | ( R " ( { X } u. f ) ) C_ f } ) )
Theorem	trclfvdecomr 36227	The transitive closure of a relation may be decomposed into a union of the relation and the composition of the relation with its transitive closure. (Contributed by RP, 18-Jul-2020.)
|- ( R e. V -> ( t+ ` R ) = ( R u. ( ( t+ ` R ) o. R ) ) )
Theorem	trclfvdecoml 36228	The transitive closure of a relation may be decomposed into a union of the relation and the composition of the relation with its transitive closure. (Contributed by RP, 18-Jul-2020.)
|- ( R e. V -> ( t+ ` R ) = ( R u. ( R o. ( t+ ` R ) ) ) )
Theorem	dmtrclfvRP 36229	The domain of the transitive closure is equal to the domain of the relation. (Contributed by RP, 18-Jul-2020.) (Proof modification is discouraged.)
|- ( R e. V -> dom ( t+ ` R ) = dom R )
Theorem	rntrclfvRP 36230	The range of the transitive closure is equal to the range of the relation. (Contributed by RP, 19-Jul-2020.) (Proof modification is discouraged.)
|- ( R e. V -> ran ( t+ ` R ) = ran R )
Theorem	rntrclfv 36231	The range of the transitive closure is equal to the range of the relation. (Contributed by RP, 18-Jul-2020.) (Proof modification is discouraged.)
|- ( R e. V -> ran ( t+ ` R ) = ran R )
Theorem	dfrtrcl3 36232*	Reflexive-transitive closure of a relation, expressed as indexed union of powers of relations. Generalized from dfrtrcl2 13062. (Contributed by RP, 5-Jun-2020.)
|- t* = ( r e. _V |-> U_ n e. NN0 ( r ^r n ) )
Theorem	brfvrtrcld 36233*	If two elements are connected by the reflexive-transitive closure of a relation, then they are connected via n instances the relation, for some natural number n. Similar of dfrtrclrec2 13057. (Contributed by RP, 22-Jul-2020.)
|- ( ph -> R e. _V )   =>    |- ( ph -> ( A ( t* ` R ) B <-> E. n e. NN0 A ( R ^r n ) B ) )
Theorem	fvrtrcllb0d 36234	A restriction of the identity relation is a subset of the reflexive-transitive closure of a set. (Contributed by RP, 22-Jul-2020.)
|- ( ph -> R e. _V )   =>    |- ( ph -> ( _I |` ( dom R u. ran R ) ) C_ ( t* ` R ) )
Theorem	fvrtrcllb0da 36235	A restriction of the identity relation is a subset of the reflexive-transitive closure of a relation. (Contributed by RP, 22-Jul-2020.)
|- ( ph -> Rel R )   &    |- ( ph -> R e. _V )   =>    |- ( ph -> ( _I |` U. U. R ) C_ ( t* ` R ) )
Theorem	fvrtrcllb1d 36236	A set is a subset of its image under the reflexive-transitive closure. (Contributed by RP, 22-Jul-2020.)
|- ( ph -> R e. _V )   =>    |- ( ph -> R C_ ( t* ` R ) )
Theorem	dfrtrcl4 36237	Reflexive-transitive closure of a relation, expressed as the union of the zeroth power and the transitive closure. (Contributed by RP, 5-Jun-2020.)
|- t* = ( r e. _V |-> ( ( r ^r 0 ) u. ( t+ ` r ) ) )
Theorem	corcltrcl 36238	The composition of the reflexive and transitive closures is the reflexive-transitive closure. (Contributed by RP, 17-Jun-2020.)
|- ( r* o. t+ ) = t*
Theorem	cortrcltrcl 36239	Composition with the reflexive-transitive closure absorbs the transitive closure. (Contributed by RP, 13-Jun-2020.)
|- ( t* o. t+ ) = t*
Theorem	corclrtrcl 36240	Composition with the reflexive-transitive closure absorbs the reflexive closure. (Contributed by RP, 13-Jun-2020.)
|- ( r* o. t* ) = t*
Theorem	cotrclrcl 36241	The composition of the reflexive and transitive closures is the reflexive-transitive closure. (Contributed by RP, 21-Jun-2020.)
|- ( t+ o. r* ) = t*
Theorem	cortrclrcl 36242	Composition with the reflexive-transitive closure absorbs the reflexive closure. (Contributed by RP, 13-Jun-2020.)
|- ( t* o. r* ) = t*
Theorem	cotrclrtrcl 36243	Composition with the reflexive-transitive closure absorbs the transitive closure. (Contributed by RP, 13-Jun-2020.)
|- ( t+ o. t* ) = t*
Theorem	cortrclrtrcl 36244	The reflexive-transitive closure is idempotent. (Contributed by RP, 13-Jun-2020.)
|- ( t* o. t* ) = t*
21.25.2.5  Adapted from Frege Theorems inspired by Begriffsschrift without restricting form and content to closely parallel those in [Frege1879].
Theorem	frege77d 36245	If the images of both { A } and U are subsets of U and B follows A in the transitive closure of R, then B is an element of U. Similar to Proposition 77 of [Frege1879] p. 62. Compare with frege77 36443. (Contributed by RP, 15-Jul-2020.)
|- ( ph -> R e. _V )   &    |- ( ph -> A e. _V )   &    |- ( ph -> B e. _V )   &    |- ( ph -> A ( t+ ` R ) B )   &    |- ( ph -> ( R " U ) C_ U )   &    |- ( ph -> ( R " { A } ) C_ U )   =>    |- ( ph -> B e. U )
Theorem	frege81d 36246	If the image of U is a subset U, A is an element of U and B follows A in the transitive closure of R, then B is an element of U. Similar to Proposition 81 of [Frege1879] p. 63. Compare with frege81 36447. (Contributed by RP, 15-Jul-2020.)
|- ( ph -> R e. _V )   &    |- ( ph -> A e. U )   &    |- ( ph -> B e. _V )   &    |- ( ph -> A ( t+ ` R ) B )   &    |- ( ph -> ( R " U ) C_ U )   =>    |- ( ph -> B e. U )
Theorem	frege83d 36247	If the image of the union of U and V is a subset of the union of U and V, A is an element of U and B follows A in the transitive closure of R, then B is an element of the union of U and V. Similar to Proposition 83 of [Frege1879] p. 65. Compare with frege83 36449. (Contributed by RP, 15-Jul-2020.)
|- ( ph -> R e. _V )   &    |- ( ph -> A e. U )   &    |- ( ph -> B e. _V )   &    |- ( ph -> A ( t+ ` R ) B )   &    |- ( ph -> ( R " ( U u. V ) ) C_ ( U u. V ) )   =>    |- ( ph -> B e. ( U u. V ) )
Theorem	frege96d 36248	If C follows A in the transitive closure of R and B follows C in R, then B follows A in the transitive closure of R. Similar to Proposition 96 of [Frege1879] p. 71. Compare with frege96 36462. (Contributed by RP, 15-Jul-2020.)
|- ( ph -> R e. _V )   &    |- ( ph -> A e. _V )   &    |- ( ph -> B e. _V )   &    |- ( ph -> C e. _V )   &    |- ( ph -> A ( t+ ` R ) C )   &    |- ( ph -> C R B )   =>    |- ( ph -> A ( t+ ` R ) B )
Theorem	frege87d 36249	If the images of both { A } and U are subsets of U and C follows A in the transitive closure of R and B follows C in R, then B is an element of U. Similar to Proposition 87 of [Frege1879] p. 66. Compare with frege87 36453. (Contributed by RP, 15-Jul-2020.)
|- ( ph -> R e. _V )   &    |- ( ph -> A e. _V )   &    |- ( ph -> B e. _V )   &    |- ( ph -> C e. _V )   &    |- ( ph -> A ( t+ ` R ) C )   &    |- ( ph -> C R B )   &    |- ( ph -> ( R " { A } ) C_ U )   &    |- ( ph -> ( R " U ) C_ U )   =>    |- ( ph -> B e. U )
Theorem	frege91d 36250	If B follows A in R then B follows A in the transitive closure of R. Similar to Proposition 91 of [Frege1879] p. 68. Comparw with frege91 36457. (Contributed by RP, 15-Jul-2020.)
|- ( ph -> R e. _V )   &    |- ( ph -> A R B )   =>    |- ( ph -> A ( t+ ` R ) B )
Theorem	frege97d 36251	If A contains all elements after those in U in the transitive closure of R, then the image under R of A is a subclass of A. Similar to Proposition 97 of [Frege1879] p. 71. Compare with frege97 36463. (Contributed by RP, 15-Jul-2020.)
|- ( ph -> R e. _V )   &    |- ( ph -> A = ( ( t+ ` R ) " U ) )   =>    |- ( ph -> ( R " A ) C_ A )
Theorem	frege98d 36252	If C follows A and B follows C in the transitive closure of R, then B follows A in the transitive closure of R. Similar to Proposition 98 of [Frege1879] p. 71. Compare with frege98 36464. (Contributed by RP, 15-Jul-2020.)
|- ( ph -> A e. _V )   &    |- ( ph -> B e. _V )   &    |- ( ph -> C e. _V )   &    |- ( ph -> A ( t+ ` R ) C )   &    |- ( ph -> C ( t+ ` R ) B )   =>    |- ( ph -> A ( t+ ` R ) B )
Theorem	frege102d 36253	If either A and C are the same or C follows A in the transitive closure of R and B is the successor to C, then B follows A in the transitive closure of R. Similar to Proposition 102 of [Frege1879] p. 72. Compare with frege102 36468. (Contributed by RP, 15-Jul-2020.)
|- ( ph -> R e. _V )   &    |- ( ph -> A e. _V )   &    |- ( ph -> B e. _V )   &    |- ( ph -> C e. _V )   &    |- ( ph -> ( A ( t+ ` R ) C \/ A = C ) )   &    |- ( ph -> C R B )   =>    |- ( ph -> A ( t+ ` R ) B )
Theorem	frege106d 36254	If B follows A in R, then either A and B are the same or B follows A in R. Similar to Proposition 106 of [Frege1879] p. 73. Compare with frege106 36472. (Contributed by RP, 15-Jul-2020.)
|- ( ph -> A R B )   =>    |- ( ph -> ( A R B \/ A = B ) )
Theorem	frege108d 36255	If either A and C are the same or C follows A in the transitive closure of R and B is the successor to C, then either A and B are the same or B follows A in the transitive closure of R. Similar to Proposition 108 of [Frege1879] p. 74. Compare with frege108 36474. (Contributed by RP, 15-Jul-2020.)
|- ( ph -> R e. _V )   &    |- ( ph -> A e. _V )   &    |- ( ph -> B e. _V )   &    |- ( ph -> C e. _V )   &    |- ( ph -> ( A ( t+ ` R ) C \/ A = C ) )   &    |- ( ph -> C R B )   =>    |- ( ph -> ( A ( t+ ` R ) B \/ A = B ) )
Theorem	frege109d 36256	If A contains all elements of U and all elements after those in U in the transitive closure of R, then the image under R of A is a subclass of A. Similar to Proposition 109 of [Frege1879] p. 74. Compare with frege109 36475. (Contributed by RP, 15-Jul-2020.)
|- ( ph -> R e. _V )   &    |- ( ph -> A = ( U u. ( ( t+ ` R ) " U ) ) )   =>    |- ( ph -> ( R " A ) C_ A )
Theorem	frege114d 36257	If either R relates A and B or A and B are the same, then either A and B are the same, R relates A and B, R relates B and A. Similar to Proposition 114 of [Frege1879] p. 76. Compare with frege114 36480. (Contributed by RP, 15-Jul-2020.)
|- ( ph -> ( A R B \/ A = B ) )   =>    |- ( ph -> ( A R B \/ A = B \/ B R A ) )
Theorem	frege111d 36258	If either A and C are the same or C follows A in the transitive closure of R and B is the successor to C, then either A and B are the same or A follows B or B and A in the transitive closure of R. Similar to Proposition 111 of [Frege1879] p. 75. Compare with frege111 36477. (Contributed by RP, 15-Jul-2020.)
|- ( ph -> R e. _V )   &    |- ( ph -> A e. _V )   &    |- ( ph -> B e. _V )   &    |- ( ph -> C e. _V )   &    |- ( ph -> ( A ( t+ ` R ) C \/ A = C ) )   &    |- ( ph -> C R B )   =>    |- ( ph -> ( A ( t+ ` R ) B \/ A = B \/ B ( t+ ` R ) A ) )
Theorem	frege122d 36259	If F is a function, A is the successor of X, and B is the successor of X, then A and B are the same (or B follows A in the transitive closure of F). Similar to Proposition 122 of [Frege1879] p. 79. Compare with frege122 36488. (Contributed by RP, 15-Jul-2020.)
|- ( ph -> A = ( F ` X ) )   &    |- ( ph -> B = ( F ` X ) )   =>    |- ( ph -> ( A ( t+ ` F ) B \/ A = B ) )
Theorem	frege124d 36260	If F is a function, A is the successor of X, and B follows X in the transitive closure of F, then A and B are the same or B follows A in the transitive closure of F. Similar to Proposition 124 of [Frege1879] p. 80. Compare with frege124 36490. (Contributed by RP, 16-Jul-2020.)
|- ( ph -> F e. _V )   &    |- ( ph -> X e. dom F )   &    |- ( ph -> A = ( F ` X ) )   &    |- ( ph -> X ( t+ ` F ) B )   &    |- ( ph -> Fun F )   =>    |- ( ph -> ( A ( t+ ` F ) B \/ A = B ) )
Theorem	frege126d 36261	If F is a function, A is the successor of X, and B follows X in the transitive closure of F, then (for distinct A and B) either A follows B or B follows A in the transitive closure of F. Similar to Proposition 126 of [Frege1879] p. 81. Compare with frege126 36492. (Contributed by RP, 16-Jul-2020.)
|- ( ph -> F e. _V )   &    |- ( ph -> X e. dom F )   &    |- ( ph -> A = ( F ` X ) )   &    |- ( ph -> X ( t+ ` F ) B )   &    |- ( ph -> Fun F )   =>    |- ( ph -> ( A ( t+ ` F ) B \/ A = B \/ B ( t+ ` F ) A ) )
Theorem	frege129d 36262	If F is a function and (for distinct A and B) either A follows B or B follows A in the transitive closure of F, the successor of A is either B or it follows B or it comes before B in the transitive closure of F. Similar to Proposition 129 of [Frege1879] p. 83. Comparw with frege129 36495. (Contributed by RP, 16-Jul-2020.)
|- ( ph -> F e. _V )   &    |- ( ph -> A e. dom F )   &    |- ( ph -> C = ( F ` A ) )   &    |- ( ph -> ( A ( t+ ` F ) B \/ A = B \/ B ( t+ ` F ) A ) )   &    |- ( ph -> Fun F )   =>    |- ( ph -> ( B ( t+ ` F ) C \/ B = C \/ C ( t+ ` F ) B ) )
Theorem	frege131d 36263	If F is a function and A contains all elements of U and all elements before or after those elements of U in the transitive closure of F, then the image under F of A is a subclass of A. Similar to Proposition 131 of [Frege1879] p. 85. Compare with frege131 36497. (Contributed by RP, 17-Jul-2020.)
|- ( ph -> F e. _V )   &    |- ( ph -> A = ( U u. ( ( `' ( t+ ` F ) " U ) u. ( ( t+ ` F ) " U ) ) ) )   &    |- ( ph -> Fun F )   =>    |- ( ph -> ( F " A ) C_ A )
Theorem	frege133d 36264	If F is a function and A and B both follow X in the transitive closure of F, then (for distinct A and B) either A follows B or B follows A in the transitive closure of F (or both if it loops). Similar to Proposition 133 of [Frege1879] p. 86. Compare with frege133 36499. (Contributed by RP, 18-Jul-2020.)
|- ( ph -> F e. _V )   &    |- ( ph -> X ( t+ ` F ) A )   &    |- ( ph -> X ( t+ ` F ) B )   &    |- ( ph -> Fun F )   =>    |- ( ph -> ( A ( t+ ` F ) B \/ A = B \/ B ( t+ ` F ) A ) )
21.25.3  Propositions from _Begriffsschrift_ In 1879, Frege introduced notation for documenting formal reasoning about propositions (and classes) which covered elements of propositional logic, predicate calculus and reasoning about relations. However, due to the pitfalls of naive set theory, adapting this work for inclusion in set.mm required dividing statements about propositions from those about classes and identifying when a restriction to sets is required. For an overview comparing the details of Frege's two-dimensional notation and that used in set.mm, see mmfrege.html. See ru 3234 for discussion of an example of a class that is not a set. Numbered propositions from [Frege1879]. ax-frege1 36293, ax-frege2 36294, ax-frege8 36312, ax-frege28 36333, ax-frege31 36337, ax-frege41 36348, frege52 (see ax-frege52a 36360, frege52b 36392, and ax-frege52c 36391 for translations), frege54 (see ax-frege54a 36365, frege54b 36396 and ax-frege54c 36395 for translations) and frege58 (see ax-frege58a 36378, ax-frege58b 36404 and frege58c 36424 for translations) are considered "core" or axioms. However, at least ax-frege8 36312 can be derived from ax-frege1 36293 and ax-frege2 36294, see axfrege8 36310. Frege introduced implication, negation and the universal qualifier as primitives and did not in the numbered propositions use other logical connectives other than equivalence introduced in ax-frege52a 36360, frege52b 36392, and ax-frege52c 36391. In dffrege69 36435, Frege introduced R hereditary A to say that relation R, when restricted to operate on elements of class A, will only have elements of class A in its domain; see df-he 36275 for a definition in terms of image and subset. In dffrege76 36442, Frege introduced notation for the concept of two sets related by the transitive closure of a relation, for which we write X ( t+ ` R ) Y, which requires R to also be a set. In dffrege99 36465, Frege introduced notation for the concept of two sets either identical or related by the transitive closure of a relation, for which we write X ( ( t+ ` R ) u. _I ) Y, which is a superclass of sets related by the reflexive-transitive relation X ( t* ` R ) Y. Finally, in dffrege115 36481, Frege introduced notation for the concept of a relation having the property elements in its domain pair up with only one element each in its range, for which we write Fun `' `' R (to ignore any non-relational content of the class R). Frege did this without the expressing concept of a relation (or its transitive closure) as a class, and needed to invent conventions for discussing indeterminate propositions with two slots free and how to recognize which of the slots was domain and which was range. See mmfrege.html for details. English translations for specific propositions lifted in part from a translation by Stefan Bauer-Mengelberg as reprinted in From Frege to Goedel: A Source Book in Mathematical Logic, 1879-1931. An attempt to align these propositions in the larger set.mm database has also been made. See frege77d 36245 for an example.
21.25.3.1  _Begriffsschrift_ Chapter I Section 2 introduces the turnstile |- which turns an idea which may be true ph into an assertion that it does hold true |- ph. Section 5 introduces implication, ( ph -> ps ). Section 6 introduces the single rule of interference relied upon, modus ponens ax-mp 5. Section 7 introduces negation and with in synonyms for or ( -. ph -> ps ), and -. ( ph -> -. ps ), and two for exclusive-or corresponding to df-or 371, df-an 372, dfxor4 36265, dfxor5 36266. Section 8 introduces the problematic notation for identity of conceptual content which must be separated into cases for biimplication ( ph <-> ps ) or class equality A = B in this adaptation. Section 10 introduces "truth functions" for one or two variables in equally troubling notation, as the arguments may be understood to be logical predicates or collections. Here f( ph) is interpreted to mean if- ( ph , ps , ch ) where the content of the "function" is specified by the latter two argments or logical equivalent, while g( A) is read as A e. G and h( A , B) as A H B. This necessarily introduces a need for set theory as both A e. G and A H B cannot hold unless A is a set. (Also B.) Section 11 introduces notation for generality, but there is no standard notation for generality when the variable is a proposition because it was realized after Frege that the universe of all possible propositions includes paradoxical constructions leading to the failure of naive set theory. So adopting f( ph) as if- ( ph , ps , ch ) would result in the translation of A. ph f ( ph) as ( ps /\ ch ). For collections, we must generalize over set variables or run into the same problems; this leads to A. A g( A) being translated as A. a a e. G and so forth. Under this interpreation the text of section 11 gives us sp 1914 (or simpl 458 and simpr 462 and anifp 1428 in the propositional case) and statments similar to cbvalivw 1842, ax-gen 1663, alrimiv 1767, and alrimdv 1769. These last four introduce a generality and have no useful definition in terms of propositional variables. Section 12 introduces some combinations of primitive symbols and their human language counterparts. Using class notation, these can also be expressed without dummy variables. All are A, A. x x e. A, -. E. x -. x e. A alex 1692, A = _V eqv 3714; Some are not B, -. A. x x e. B, E. x -. x e. B exnal 1693, B C. _V pssv 3770, B =/= _V nev 36269; There are no C, A. x -. x e. C, -. E. x x e. C alnex 1659, C = (/) eq0 3713; There exist D, -. A. x -. x e. D, E. x x e. D df-ex 1658, (/) C. D 0pss 3768, D =/= (/) n0 3707. Notation for relations between expressions also can be written in various ways. All E are P, A. x ( x e. E -> x e. P ), -. E. x ( x e. E /\ -. x e. P ) dfss6 36270, E = ( E i^i P ) df-ss 3386, E C_ P dfss2 3389; No F are P, A. x ( x e. F -> -. x e. P ), -. E. x ( x e. F /\ x e. P ) alinexa 1707, ( F i^i P ) = (/) disj1 3773; Some G are not P, -. A. x ( x e. G -> x e. P ), E. x ( x e. G /\ -. x e. P ) exanali 1715, ( G i^i P ) C. G nssinpss 3641, -. G C_ P nss 3458; Some H are P, -. A. x ( x e. H -> -. x e. P ), E. x ( x e. H /\ x e. P ) bj-exnalimn 31157, (/) C. ( H i^i P ) 0pssin 36272, ( H i^i P ) =/= (/) ndisj 36271.
Theorem	dfxor4 36265	Express exclusive-or in terms of implication and negation. Statement in [Frege1879] p. 12. (Contributed by RP, 14-Apr-2020.)
|- ( ( ph \/_ ps ) <-> -. ( ( -. ph -> ps ) -> -. ( ph -> -. ps ) ) )
Theorem	dfxor5 36266	Express exclusive-or in terms of implication and negation. Statement in [Frege1879] p. 12. (Contributed by RP, 14-Apr-2020.)
|- ( ( ph \/_ ps ) <-> -. ( ( ph -> -. ps ) -> -. ( -. ph -> ps ) ) )
Theorem	df3or2 36267	Express triple-or in terms of implication and negation. Statement in [Frege1879] p. 11. (Contributed by RP, 25-Jul-2020.)
|- ( ( ph \/ ps \/ ch ) <-> ( -. ph -> ( -. ps -> ch ) ) )
Theorem	df3an2 36268	Express triple-and in terms of implication and negation. Statement in [Frege1879] p. 12. (Contributed by RP, 25-Jul-2020.)
|- ( ( ph /\ ps /\ ch ) <-> -. ( ph -> ( ps -> -. ch ) ) )
Theorem	nev 36269*	Express that not every set is in a class. (Contributed by RP, 16-Apr-2020.)
|- ( A =/= _V <-> -. A. x x e. A )
Theorem	dfss6 36270*	Another definition of subclasshood. (Contributed by RP, 16-Apr-2020.)
|- ( A C_ B <-> -. E. x ( x e. A /\ -. x e. B ) )
Theorem	ndisj 36271*	Express that an intersection is not empty. (Contributed by RP, 16-Apr-2020.)
|- ( ( A i^i B ) =/= (/) <-> E. x ( x e. A /\ x e. B ) )
Theorem	0pssin 36272*	Express that an intersection is not empty. (Contributed by RP, 16-Apr-2020.)
|- ( (/) C. ( A i^i B ) <-> E. x ( x e. A /\ x e. B ) )
21.25.3.2  _Begriffsschrift_ Notation hints The statement R hereditary A means relation R is hereditary (in the sense of Frege) in the class A or ( R " A ) C_ A. The former is only a slight reduction in the number of symbols, but this reduces the number of floating hypotheses needed to be checked. As Frege wasn't using the language of classes or sets, this naturally differs from the set-theoretic notion that a set is hereditary in a property: that all of its elements have a property and all of their elements have the property and so-on.
Theorem	rp-imass 36273	If the R-image of a class A is a subclass of B, then the restriction of R to A is a subset of the Cartesian product of A and B. (Contributed by Richard Penner, 24-Dec-2019.)
|- ( ( R " A ) C_ B <-> ( R |` A ) C_ ( A X. B ) )
Syntax	whe 36274	The property of relation R being hereditary in class A.
wff R hereditary A
Definition	df-he 36275	The property of relation R being hereditary in class A. (Contributed by RP, 27-Mar-2020.)
|- ( R hereditary A <-> ( R " A ) C_ A )
Theorem	dfhe2 36276	The property of relation R being hereditary in class A. (Contributed by RP, 27-Mar-2020.)
|- ( R hereditary A <-> ( R |` A ) C_ ( A X. A ) )
Theorem	dfhe3 36277*	The property of relation R being hereditary in class A. (Contributed by RP, 27-Mar-2020.)
|- ( R hereditary A <-> A. x ( x e. A -> A. y ( x R y -> y e. A ) ) )
Theorem	heeq12 36278	Equality law for relations being herditary over a class. (Contributed by RP, 27-Mar-2020.)
|- ( ( R = S /\ A = B ) -> ( R hereditary A <-> S hereditary B ) )
Theorem	heeq1 36279	Equality law for relations being herditary over a class. (Contributed by RP, 27-Mar-2020.)
|- ( R = S -> ( R hereditary A <-> S hereditary A ) )
Theorem	heeq2 36280	Equality law for relations being herditary over a class. (Contributed by RP, 27-Mar-2020.)
|- ( A = B -> ( R hereditary A <-> R hereditary B ) )
Theorem	sbcheg 36281	Distribute proper substitution through herditary relation. (Contributed by RP, 29-Jun-2020.)
|- ( A e. V -> ( [. A / x ]. B hereditary C <-> [_ A / x ]_ B hereditary [_ A / x ]_ C ) )
Theorem	hess 36282	Subclass law for relations being herditary over a class. (Contributed by RP, 27-Mar-2020.)
|- ( S C_ R -> ( R hereditary A -> S hereditary A ) )
Theorem	xphe 36283	Any Cartesian product is hereditary in its second class. (Contributed by RP, 27-Mar-2020.) (Proof shortened by OpenAI, 3-Jul-2020.)
|- ( A X. B ) hereditary B
Theorem	xpheOLD 36284	Any Cartesian product is hereditary in its second class. (Contributed by RP, 27-Mar-2020.) Obsolete version of xphe 36283 as of 3-Jul-2020. (New usage is discouraged.) (Proof modification is discouraged.)
|- ( A X. B ) hereditary B
Theorem	0he 36285	The empty relation is hereditary in any class. (Contributed by RP, 27-Mar-2020.)
|- (/) hereditary A
Theorem	0heALT 36286	The empty relation is hereditary in any class. (Contributed by RP, 27-Mar-2020.) (New usage is discouraged.) (Proof modification is discouraged.)
|- (/) hereditary A
Theorem	he0 36287	Any relation is hereditary in the empty set. (Contributed by RP, 27-Mar-2020.)
|- A hereditary (/)
Theorem	unhe1 36288	The union of two relations hereditary in a class is also hereditary in a class. (Contributed by RP, 28-Mar-2020.)
|- ( ( R hereditary A /\ S hereditary A ) -> ( R u. S ) hereditary A )
Theorem	snhesn 36289	Any singleton is hereditary in any singleton. (Contributed by RP, 28-Mar-2020.)
|- { <. A , A >. } hereditary { B }
Theorem	idhe 36290	The identity relation is hereditary in any class. (Contributed by RP, 28-Mar-2020.)
|- _I hereditary A
Theorem	psshepw 36291	The relation between sets and their proper subsets is hereditary in the powerclass of any class. (Contributed by RP, 28-Mar-2020.)
|- `' [ C.] hereditary ~P A
Theorem	sshepw 36292	The relation between sets and their subsets is hereditary in the powerclass of any class. (Contributed by RP, 28-Mar-2020.)
|- ( `' [ C.] u. _I ) hereditary ~P A
21.25.3.3  _Begriffsschrift_ Chapter II Implication
Axiom	ax-frege1 36293	The case in which ph is denied, ps is affirmed, and ph is affirmed is excluded. This is evident since ph cannot at the same time be denied and affirmed. Axiom 1 of [Frege1879] p. 26. Identical to ax-1 6. (Contributed by RP, 24-Dec-2019.) (New usage is discouraged.)
|- ( ph -> ( ps -> ph ) )
Axiom	ax-frege2 36294	If a proposition ch is a necessary consequence of two propositions ps and ph and one of those, ps, is in turn a necessary consequence of the other, ph, then the proposition ch is a necessary consequence of the latter one, ph, alone. Axiom 2 of [Frege1879] p. 26. Identical to ax-2 7. (Contributed by RP, 24-Dec-2019.) (New usage is discouraged.)
|- ( ( ph -> ( ps -> ch ) ) -> ( ( ph -> ps ) -> ( ph -> ch ) ) )
Theorem	rp-simp2-frege 36295	Simplification of triple conjunction. Compare with simp2 1006. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- ( ph -> ( ps -> ( ch -> ps ) ) )
Theorem	rp-simp2 36296	Simplification of triple conjunction. Identical to simp2 1006. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- ( ( ph /\ ps /\ ch ) -> ps )
Theorem	rp-frege3g 36297	Add antecedent to ax-frege2 36294. More general statement than frege3 36298. Like ax-frege2 36294, it is essentially a closed form of mpd 15, however it has an extra antecedent. It would be more natural to prove from a1i 11 and ax-frege2 36294 in Metamath. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- ( ph -> ( ( ps -> ( ch -> th ) ) -> ( ( ps -> ch ) -> ( ps -> th ) ) ) )
Theorem	frege3 36298	Add antecedent to ax-frege2 36294. Special case of rp-frege3g 36297. Proposition 3 of [Frege1879] p. 29. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- ( ( ph -> ps ) -> ( ( ch -> ( ph -> ps ) ) -> ( ( ch -> ph ) -> ( ch -> ps ) ) ) )
Theorem	rp-misc1-frege 36299	Double-use of ax-frege2 36294. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- ( ( ( ph -> ( ps -> ch ) ) -> ( ph -> ps ) ) -> ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) )
Theorem	rp-frege24 36300	Introducing an embedded antecedent. Alternate proof for frege24 36318. Closed form for a1d 26. (Contributed by RP, 24-Dec-2019.)
|- ( ( ph -> ps ) -> ( ph -> ( ch -> ps ) ) )