P. 366 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 36501-36600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	frege60b 36501	Swap antecedents of ax-frege58b 36497. Proposition 60 of [Frege1879] p. 52. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- ( A. x ( ph -> ( ps -> ch ) ) -> ( [ y / x ] ps -> ( [ y / x ] ph -> [ y / x ] ch ) ) )
Theorem	frege61b 36502	Lemma for frege65b 36506. Proposition 61 of [Frege1879] p. 52. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- ( ( [ x / y ] ph -> ps ) -> ( A. y ph -> ps ) )
Theorem	frege62b 36503	A kind of Aristotelian inference. This judgement replaces the mode of inference barbara 2392 when the minor premise has a particular context. Proposition 62 of [Frege1879] p. 52. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- ( [ x / y ] ph -> ( A. y ( ph -> ps ) -> [ x / y ] ps ) )
Theorem	frege63b 36504	Lemma for frege91 36550. Proposition 63 of [Frege1879] p. 52. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- ( [ x / y ] ph -> ( ps -> ( A. y ( ph -> ch ) -> [ x / y ] ch ) ) )
Theorem	frege64b 36505	Lemma for frege65b 36506. Proposition 64 of [Frege1879] p. 53. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- ( ( [ x / y ] ph -> [ z / y ] ps ) -> ( A. y ( ps -> ch ) -> ( [ x / y ] ph -> [ z / y ] ch ) ) )
Theorem	frege65b 36506	A kind of Aristotelian inference. This judgement replaces the mode of inference barbara 2392 when the minor premise has a general context. Proposition 65 of [Frege1879] p. 53. In Frege care is taken to point out that the variables in the first clauses are independent of each other and of the final term so another valid translation could be : |- ( A. x ( [ x / a ] ph -> [ x / b ] ps ) -> ( A. y ( [ y / b ] ps -> [ y / c ] ch ) -> ( [ z / a ] ph -> [ z / c ] ch ) ) ). But that is perhaps too pedantic a translation for this exploration. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- ( A. x ( ph -> ps ) -> ( A. x ( ps -> ch ) -> ( [ y / x ] ph -> [ y / x ] ch ) ) )
Theorem	frege66b 36507	Swap antecedents of frege65b 36506. Proposition 66 of [Frege1879] p. 54. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- ( A. x ( ph -> ps ) -> ( A. x ( ch -> ph ) -> ( [ y / x ] ch -> [ y / x ] ps ) ) )
Theorem	frege67b 36508	Lemma for frege68b 36509. Proposition 67 of [Frege1879] p. 54. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- ( ( ( A. x ph <-> ps ) -> ( ps -> A. x ph ) ) -> ( ( A. x ph <-> ps ) -> ( ps -> [ y / x ] ph ) ) )
Theorem	frege68b 36509	Combination of applying a definition and applying it to a specific instance. Proposition 68 of [Frege1879] p. 54. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- ( ( A. x ph <-> ps ) -> ( ps -> [ y / x ] ph ) )
21.25.3.7  _Begriffsschrift_ Chapter II with equivalence of classes (where they are sets)
Theorem	frege53c 36510	Proposition 53 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- ( [. A / x ]. ph -> ( A = B -> [. B / x ]. ph ) )
Theorem	frege54cor1c 36511*	Reflexive equality. (Contributed by RP, 24-Dec-2019.) (Revised by RP, 25-Apr-2020.)
|- A e. C   =>    |- [. A / x ]. x = A
Theorem	frege55lem1c 36512*	Necessary deduction regarding substitution of value in equality. (Contributed by RP, 24-Dec-2019.)
|- ( ( ph -> [. A / x ]. x = B ) -> ( ph -> A = B ) )
Theorem	frege55lem2c 36513*	Core proof of Proposition 55 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- ( x = A -> [. A / z ]. z = x )
Theorem	frege55c 36514	Proposition 55 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- ( x = A -> A = x )
Theorem	frege56c 36515*	Lemma for frege57c 36516. Proposition 56 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- B e. C   =>    |- ( ( A = B -> ( [. A / x ]. ph -> [. B / x ]. ph ) ) -> ( B = A -> ( [. A / x ]. ph -> [. B / x ]. ph ) ) )
Theorem	frege57c 36516*	Swap order of implication in ax-frege52c 36484. Proposition 57 of [Frege1879] p. 51. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- A e. C   =>    |- ( A = B -> ( [. B / x ]. ph -> [. A / x ]. ph ) )
Theorem	frege58c 36517	Principle related to sp 1937. Axiom 58 of [Frege1879] p. 51. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- A e. B   =>    |- ( A. x ph -> [. A / x ]. ph )
Theorem	frege59c 36518	A kind of Aristotelian inference. Proposition 59 of [Frege1879] p. 51. Note: in the Bauer-Meenfelberg translation published in van Heijenoort's collection From Frege to Goedel, this proof has the frege12 36409 incorrectly referenced where frege30 36428 is in the original. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- A e. B   =>    |- ( [. A / x ]. ph -> ( -. [. A / x ]. ps -> -. A. x ( ph -> ps ) ) )
Theorem	frege60c 36519	Swap antecedents of frege58c 36517. Proposition 60 of [Frege1879] p. 52. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- A e. B   =>    |- ( A. x ( ph -> ( ps -> ch ) ) -> ( [. A / x ]. ps -> ( [. A / x ]. ph -> [. A / x ]. ch ) ) )
Theorem	frege61c 36520	Lemma for frege65c 36524. Proposition 61 of [Frege1879] p. 52. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- A e. B   =>    |- ( ( [. A / x ]. ph -> ps ) -> ( A. x ph -> ps ) )
Theorem	frege62c 36521	A kind of Aristotelian inference. This judgement replaces the mode of inference barbara 2392 when the minor premise has a particular context. Proposition 62 of [Frege1879] p. 52. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- A e. B   =>    |- ( [. A / x ]. ph -> ( A. x ( ph -> ps ) -> [. A / x ]. ps ) )
Theorem	frege63c 36522	Analogue of frege63b 36504. Proposition 63 of [Frege1879] p. 52. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- A e. B   =>    |- ( [. A / x ]. ph -> ( ps -> ( A. x ( ph -> ch ) -> [. A / x ]. ch ) ) )
Theorem	frege64c 36523	Lemma for frege65c 36524. Proposition 64 of [Frege1879] p. 53. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- A e. B   =>    |- ( ( [. C / x ]. ph -> [. A / x ]. ps ) -> ( A. x ( ps -> ch ) -> ( [. C / x ]. ph -> [. A / x ]. ch ) ) )
Theorem	frege65c 36524	A kind of Aristotelian inference. This judgement replaces the mode of inference barbara 2392 when the minor premise has a general context. Proposition 65 of [Frege1879] p. 53. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- A e. B   =>    |- ( A. x ( ph -> ps ) -> ( A. x ( ps -> ch ) -> ( [. A / x ]. ph -> [. A / x ]. ch ) ) )
Theorem	frege66c 36525	Swap antecedents of frege65c 36524. Proposition 66 of [Frege1879] p. 54. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- A e. B   =>    |- ( A. x ( ph -> ps ) -> ( A. x ( ch -> ph ) -> ( [. A / x ]. ch -> [. A / x ]. ps ) ) )
Theorem	frege67c 36526	Lemma for frege68c 36527. Proposition 67 of [Frege1879] p. 54. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- A e. B   =>    |- ( ( ( A. x ph <-> ps ) -> ( ps -> A. x ph ) ) -> ( ( A. x ph <-> ps ) -> ( ps -> [. A / x ]. ph ) ) )
Theorem	frege68c 36527	Combination of applying a definition and applying it to a specific instance. Proposition 68 of [Frege1879] p. 54. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- A e. B   =>    |- ( ( A. x ph <-> ps ) -> ( ps -> [. A / x ]. ph ) )
21.25.3.8  _Begriffsschrift_ Chapter III Properties hereditary in a sequence ( R " A ) C_ A means membership in A is hereditary in the sequence dictated by relation R. This 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. While the above notation is modern, it is cumbersome in the case when A is complex and to more closely follow Frege, we abbreviate it with new notation R hereditary A. This greatly shortens the statements for frege97 36556 and frege109 36568. dffrege69 36528 through frege75 36534 develop this, but translation to Metamath is pending some decisions. While Frege does not limit discussion to sets, we may have to depart from Frege by limiting R or A to sets when we quantify over all hereditary relations or all classes where membership is hereditary in a sequence dictated by R.
Theorem	dffrege69 36528*	If from the proposition that x has property A it can be inferred generally, whatever x may be, that every result of an application of the procedure R to x has property A, then we say " Property A is hereditary in the R-sequence. Definition 69 of [Frege1879] p. 55. (Contributed by RP, 28-Mar-2020.)
|- ( A. x ( x e. A -> A. y ( x R y -> y e. A ) ) <-> R hereditary A )
Theorem	frege70 36529*	Lemma for frege72 36531. Proposition 70 of [Frege1879] p. 58. (Contributed by RP, 28-Mar-2020.) (Revised by RP, 3-Jul-2020.) (Proof modification is discouraged.)
|- X e. V   =>    |- ( R hereditary A -> ( X e. A -> A. y ( X R y -> y e. A ) ) )
Theorem	frege71 36530*	Lemma for frege72 36531. Proposition 71 of [Frege1879] p. 59. (Contributed by RP, 28-Mar-2020.) (Revised by RP, 3-Jul-2020.) (Proof modification is discouraged.)
|- X e. V   =>    |- ( ( A. z ( X R z -> z e. A ) -> ( X R Y -> Y e. A ) ) -> ( R hereditary A -> ( X e. A -> ( X R Y -> Y e. A ) ) ) )
Theorem	frege72 36531	If property A is hereditary in the R-sequence, if x has property A, and if y is a result of an application of the procedure R to x, then y has property A. Proposition 72 of [Frege1879] p. 59. (Contributed by RP, 28-Mar-2020.) (Revised by RP, 5-Jul-2020.) (Proof modification is discouraged.)
|- X e. U   &    |- Y e. V   =>    |- ( R hereditary A -> ( X e. A -> ( X R Y -> Y e. A ) ) )
Theorem	frege73 36532	Lemma for frege87 36546. Proposition 73 of [Frege1879] p. 59. (Contributed by RP, 28-Mar-2020.) (Revised by RP, 5-Jul-2020.) (Proof modification is discouraged.)
|- X e. U   &    |- Y e. V   =>    |- ( ( R hereditary A -> X e. A ) -> ( R hereditary A -> ( X R Y -> Y e. A ) ) )
Theorem	frege74 36533	If X has a property A that is hereditary in the R-sequence, then every result of a application of the procedure R to X has the property A. Proposition 74 of [Frege1879] p. 60. (Contributed by RP, 28-Mar-2020.) (Revised by RP, 5-Jul-2020.) (Proof modification is discouraged.)
|- X e. U   &    |- Y e. V   =>    |- ( X e. A -> ( R hereditary A -> ( X R Y -> Y e. A ) ) )
Theorem	frege75 36534*	If from the proposition that x has property A, whatever x may be, it can be inferred that every result of an application of the procedure R to x has property A, then property A is hereditary in the R-sequence. Proposition 75 of [Frege1879] p. 60. (Contributed by RP, 28-Mar-2020.) (Proof modification is discouraged.)
|- ( A. x ( x e. A -> A. y ( x R y -> y e. A ) ) -> R hereditary A )
21.25.3.9  _Begriffsschrift_ Chapter III Following in a sequence p ( t+ ` R ) c means c follows p in the R-sequence. dffrege76 36535 through frege98 36557 develop this. This will be shown to be the transitive closure of the relation R. But more work needs to be done on transitive closure of relations before this is ready for Metamath.
Theorem	dffrege76 36535*	If from the two propositions that every result of an application of the procedure R to B has property f and that property f is hereditary in the R-sequence, it can be inferred, whatever f may be, that E has property f, then we say E follows B in the R-sequence. Definition 76 of [Frege1879] p. 60. Each of B, E and R must be sets. (Contributed by RP, 2-Jul-2020.)
|- B e. U   &    |- E e. V   &    |- R e. W   =>    |- ( A. f ( R hereditary f -> ( A. a ( B R a -> a e. f ) -> E e. f ) ) <-> B ( t+ ` R ) E )
Theorem	frege77 36536*	If Y follows X in the R-sequence, if property A is hereditary in the R-sequence, and if every result of an application of the procedure R to X has the property A, then Y has property A. Proposition 77 of [Frege1879] p. 62. (Contributed by RP, 29-Jun-2020.) (Revised by RP, 2-Jul-2020.) (Proof modification is discouraged.)
|- X e. U   &    |- Y e. V   &    |- R e. W   &    |- A e. B   =>    |- ( X ( t+ ` R ) Y -> ( R hereditary A -> ( A. a ( X R a -> a e. A ) -> Y e. A ) ) )
Theorem	frege78 36537*	Commuted form of of frege77 36536. Proposition 78 of [Frege1879] p. 63. (Contributed by RP, 1-Jul-2020.) (Revised by RP, 2-Jul-2020.) (Proof modification is discouraged.)
|- X e. U   &    |- Y e. V   &    |- R e. W   &    |- A e. B   =>    |- ( R hereditary A -> ( A. a ( X R a -> a e. A ) -> ( X ( t+ ` R ) Y -> Y e. A ) ) )
Theorem	frege79 36538*	Distributed form of frege78 36537. Proposition 79 of [Frege1879] p. 63. (Contributed by RP, 1-Jul-2020.) (Revised by RP, 3-Jul-2020.) (Proof modification is discouraged.)
|- X e. U   &    |- Y e. V   &    |- R e. W   &    |- A e. B   =>    |- ( ( R hereditary A -> A. a ( X R a -> a e. A ) ) -> ( R hereditary A -> ( X ( t+ ` R ) Y -> Y e. A ) ) )
Theorem	frege80 36539*	Add additional condition to both clauses of frege79 36538. Proposition 80 of [Frege1879] p. 63. (Contributed by RP, 1-Jul-2020.) (Revised by RP, 5-Jul-2020.) (Proof modification is discouraged.)
|- X e. U   &    |- Y e. V   &    |- R e. W   &    |- A e. B   =>    |- ( ( X e. A -> ( R hereditary A -> A. a ( X R a -> a e. A ) ) ) -> ( X e. A -> ( R hereditary A -> ( X ( t+ ` R ) Y -> Y e. A ) ) ) )
Theorem	frege81 36540	If X has a property A that is hereditary in the R -sequence, and if Y follows X in the R-sequence, then Y has property A. This is a form of induction attributed to Jakob Bernoulli. Proposition 81 of [Frege1879] p. 63. (Contributed by RP, 1-Jul-2020.) (Revised by RP, 5-Jul-2020.) (Proof modification is discouraged.)
|- X e. U   &    |- Y e. V   &    |- R e. W   &    |- A e. B   =>    |- ( X e. A -> ( R hereditary A -> ( X ( t+ ` R ) Y -> Y e. A ) ) )
Theorem	frege82 36541	Closed-form deduction based on frege81 36540. Proposition 82 of [Frege1879] p. 64. (Contributed by RP, 1-Jul-2020.) (Revised by RP, 5-Jul-2020.) (Proof modification is discouraged.)
|- X e. U   &    |- Y e. V   &    |- R e. W   &    |- A e. B   =>    |- ( ( ph -> X e. A ) -> ( R hereditary A -> ( ph -> ( X ( t+ ` R ) Y -> Y e. A ) ) ) )
Theorem	frege83 36542	Apply commuted form of frege81 36540 when the property R is hereditary in a disjunction of two properties, only one of which is known to be held by X. Proposition 83 of [Frege1879] p. 65. Here we introduce the union of classes where Frege has a disjunction of properties which are represented by membership in either of the classes. (Contributed by RP, 1-Jul-2020.) (Revised by RP, 5-Jul-2020.) (Proof modification is discouraged.)
|- X e. S   &    |- Y e. T   &    |- R e. U   &    |- B e. V   &    |- C e. W   =>    |- ( R hereditary ( B u. C ) -> ( X e. B -> ( X ( t+ ` R ) Y -> Y e. ( B u. C ) ) ) )
Theorem	frege84 36543	Commuted form of frege81 36540. Proposition 84 of [Frege1879] p. 65. (Contributed by RP, 1-Jul-2020.) (Revised by RP, 5-Jul-2020.) (Proof modification is discouraged.)
|- X e. U   &    |- Y e. V   &    |- R e. W   &    |- A e. B   =>    |- ( R hereditary A -> ( X e. A -> ( X ( t+ ` R ) Y -> Y e. A ) ) )
Theorem	frege85 36544*	Commuted form of frege77 36536. Proposition 85 of [Frege1879] p. 66. (Contributed by RP, 1-Jul-2020.) (Revised by RP, 5-Jul-2020.) (Proof modification is discouraged.)
|- X e. U   &    |- Y e. V   &    |- R e. W   &    |- A e. B   =>    |- ( X ( t+ ` R ) Y -> ( A. z ( X R z -> z e. A ) -> ( R hereditary A -> Y e. A ) ) )
Theorem	frege86 36545*	Conclusion about element one past Y in the R-sequence. Proposition 86 of [Frege1879] p. 66. (Contributed by RP, 1-Jul-2020.) (Revised by RP, 7-Jul-2020.) (Proof modification is discouraged.)
|- X e. U   &    |- Y e. V   &    |- R e. W   &    |- A e. B   =>    |- ( ( ( R hereditary A -> Y e. A ) -> ( R hereditary A -> ( Y R Z -> Z e. A ) ) ) -> ( X ( t+ ` R ) Y -> ( A. w ( X R w -> w e. A ) -> ( R hereditary A -> ( Y R Z -> Z e. A ) ) ) ) )
Theorem	frege87 36546*	If Z is a result of an application of the procedure R to an object Y that follows X in the R-sequence and if every result of an application of the procedure R to X has a property A that is hereditary in the R-sequence, then Z has property A. Proposition 87 of [Frege1879] p. 66. (Contributed by RP, 1-Jul-2020.) (Revised by RP, 7-Jul-2020.) (Proof modification is discouraged.)
|- X e. U   &    |- Y e. V   &    |- Z e. W   &    |- R e. S   &    |- A e. B   =>    |- ( X ( t+ ` R ) Y -> ( A. w ( X R w -> w e. A ) -> ( R hereditary A -> ( Y R Z -> Z e. A ) ) ) )
Theorem	frege88 36547*	Commuted form of frege87 36546. Proposition 88 of [Frege1879] p. 67. (Contributed by RP, 1-Jul-2020.) (Revised by RP, 7-Jul-2020.) (Proof modification is discouraged.)
|- X e. U   &    |- Y e. V   &    |- Z e. W   &    |- R e. S   &    |- A e. B   =>    |- ( Y R Z -> ( X ( t+ ` R ) Y -> ( A. w ( X R w -> w e. A ) -> ( R hereditary A -> Z e. A ) ) ) )
Theorem	frege89 36548*	One direction of dffrege76 36535. Proposition 89 of [Frege1879] p. 68. (Contributed by RP, 1-Jul-2020.) (Revised by RP, 2-Jul-2020.) (Proof modification is discouraged.)
|- X e. U   &    |- Y e. V   &    |- R e. W   =>    |- ( A. f ( R hereditary f -> ( A. w ( X R w -> w e. f ) -> Y e. f ) ) -> X ( t+ ` R ) Y )
Theorem	frege90 36549*	Add antecedent to frege89 36548. Proposition 90 of [Frege1879] p. 68. (Contributed by RP, 1-Jul-2020.) (Revised by RP, 2-Jul-2020.) (Proof modification is discouraged.)
|- X e. U   &    |- Y e. V   &    |- R e. W   =>    |- ( ( ph -> A. f ( R hereditary f -> ( A. w ( X R w -> w e. f ) -> Y e. f ) ) ) -> ( ph -> X ( t+ ` R ) Y ) )
Theorem	frege91 36550	Every result of an application of a procedure R to an object X follows that X in the R-sequence. Proposition 91 of [Frege1879] p. 68. (Contributed by RP, 2-Jul-2020.) (Revised by RP, 5-Jul-2020.) (Proof modification is discouraged.)
|- X e. U   &    |- Y e. V   &    |- R e. W   =>    |- ( X R Y -> X ( t+ ` R ) Y )
Theorem	frege92 36551	Inference from frege91 36550. Proposition 92 of [Frege1879] p. 69. (Contributed by RP, 2-Jul-2020.) (Revised by RP, 5-Jul-2020.) (Proof modification is discouraged.)
|- X e. U   &    |- Y e. V   &    |- R e. W   =>    |- ( X = Z -> ( X R Y -> Z ( t+ ` R ) Y ) )
Theorem	frege93 36552*	Necessary condition for two elements to be related by the transitive closure. Proposition 93 of [Frege1879] p. 70. (Contributed by RP, 2-Jul-2020.) (Revised by RP, 5-Jul-2020.) (Proof modification is discouraged.)
|- X e. U   &    |- Y e. V   &    |- R e. W   =>    |- ( A. f ( A. z ( X R z -> z e. f ) -> ( R hereditary f -> Y e. f ) ) -> X ( t+ ` R ) Y )
Theorem	frege94 36553*	Looking one past a pair related by transitive closure of a relation. Proposition 94 of [Frege1879] p. 70. (Contributed by RP, 2-Jul-2020.) (Revised by RP, 5-Jul-2020.) (Proof modification is discouraged.)
|- X e. U   &    |- Z e. V   &    |- R e. W   =>    |- ( ( Y R Z -> ( X ( t+ ` R ) Y -> A. f ( A. w ( X R w -> w e. f ) -> ( R hereditary f -> Z e. f ) ) ) ) -> ( Y R Z -> ( X ( t+ ` R ) Y -> X ( t+ ` R ) Z ) ) )
Theorem	frege95 36554	Looking one past a pair related by transitive closure of a relation. Proposition 95 of [Frege1879] p. 70. (Contributed by RP, 2-Jul-2020.) (Revised by RP, 7-Jul-2020.) (Proof modification is discouraged.)
|- X e. U   &    |- Y e. V   &    |- Z e. W   &    |- R e. A   =>    |- ( Y R Z -> ( X ( t+ ` R ) Y -> X ( t+ ` R ) Z ) )
Theorem	frege96 36555	Every result of an application of the procedure R to an object that follows X in the R-sequence follows X in the R -sequence. Proposition 96 of [Frege1879] p. 71. (Contributed by RP, 2-Jul-2020.) (Revised by RP, 7-Jul-2020.) (Proof modification is discouraged.)
|- X e. U   &    |- Y e. V   &    |- Z e. W   &    |- R e. A   =>    |- ( X ( t+ ` R ) Y -> ( Y R Z -> X ( t+ ` R ) Z ) )
Theorem	frege97 36556	The property of following X in the R-sequence is hereditary in the R-sequence. Proposition 97 of [Frege1879] p. 71. Here we introduce the image of a singleton under a relation as class which stands for the property of following X in the R -sequence. (Contributed by RP, 2-Jul-2020.) (Revised by RP, 7-Jul-2020.) (Proof modification is discouraged.)
|- X e. U   &    |- R e. W   =>    |- R hereditary ( ( t+ ` R ) " { X } )
Theorem	frege98 36557	If Y follows X and Z follows Y in the R-sequence then Z follows X in the R-sequence because the transitive closure of a relation has the transitive property. Proposition 98 of [Frege1879] p. 71. (Contributed by RP, 2-Jul-2020.) (Revised by RP, 6-Jul-2020.) (Proof modification is discouraged.)
|- X e. A   &    |- Y e. B   &    |- Z e. C   &    |- R e. D   =>    |- ( X ( t+ ` R ) Y -> ( Y ( t+ ` R ) Z -> X ( t+ ` R ) Z ) )
21.25.3.10  _Begriffsschrift_ Chapter III Member of sequence p ( ( t+ ` R ) u. _I ) c means c is a member of the R -sequence begining with p and p is a member of the R -sequence ending with c. dffrege99 36558 through frege114 36573 develop this. This will be shown to be related to the transitive-reflexive closure of relation R. But more work needs to be done on transitive closure of relations before this is ready for Metamath.
Theorem	dffrege99 36558	If Z is identical with X or follows X in the R -sequence, then we say : " Z belongs to the R-sequence beginning with X " or " X belongs to the R-sequence ending with Z". Definition 99 of [Frege1879] p. 71. (Contributed by RP, 2-Jul-2020.)
|- Z e. U   =>    |- ( ( -. X ( t+ ` R ) Z -> Z = X ) <-> X ( ( t+ ` R ) u. _I ) Z )
Theorem	frege100 36559	One direction of dffrege99 36558. Proposition 100 of [Frege1879] p. 72. (Contributed by RP, 7-Jul-2020.) (Proof modification is discouraged.)
|- Z e. U   =>    |- ( X ( ( t+ ` R ) u. _I ) Z -> ( -. X ( t+ ` R ) Z -> Z = X ) )
Theorem	frege101 36560	Lemma for frege102 36561. Proposition 101 of [Frege1879] p. 72. (Contributed by RP, 7-Jul-2020.) (Proof modification is discouraged.)
|- Z e. U   =>    |- ( ( Z = X -> ( Z R V -> X ( t+ ` R ) V ) ) -> ( ( X ( t+ ` R ) Z -> ( Z R V -> X ( t+ ` R ) V ) ) -> ( X ( ( t+ ` R ) u. _I ) Z -> ( Z R V -> X ( t+ ` R ) V ) ) ) )
Theorem	frege102 36561	If Z belongs to the R-sequence beginning with X, then every result of an application of the procedure R to Z follows X in the R-sequence. Proposition 102 of [Frege1879] p. 72. (Contributed by RP, 7-Jul-2020.) (Proof modification is discouraged.)
|- X e. A   &    |- Z e. B   &    |- V e. C   &    |- R e. D   =>    |- ( X ( ( t+ ` R ) u. _I ) Z -> ( Z R V -> X ( t+ ` R ) V ) )
Theorem	frege103 36562	Proposition 103 of [Frege1879] p. 73. (Contributed by RP, 7-Jul-2020.) (Proof modification is discouraged.)
|- Z e. V   =>    |- ( ( Z = X -> X = Z ) -> ( X ( ( t+ ` R ) u. _I ) Z -> ( -. X ( t+ ` R ) Z -> X = Z ) ) )
Theorem	frege104 36563	Proposition 104 of [Frege1879] p. 73. Note: in the Bauer-Meenfelberg translation published in van Heijenoort's collection From Frege to Goedel, this proof has the minor clause and result swapped. (Contributed by RP, 7-Jul-2020.) (Proof modification is discouraged.)
|- Z e. V   =>    |- ( X ( ( t+ ` R ) u. _I ) Z -> ( -. X ( t+ ` R ) Z -> X = Z ) )
Theorem	frege105 36564	Proposition 105 of [Frege1879] p. 73. (Contributed by RP, 7-Jul-2020.) (Proof modification is discouraged.)
|- Z e. V   =>    |- ( ( -. X ( t+ ` R ) Z -> Z = X ) -> X ( ( t+ ` R ) u. _I ) Z )
Theorem	frege106 36565	Whatever follows X in the R-sequence belongs to the R -sequence beginning with X. Proposition 106 of [Frege1879] p. 73. (Contributed by RP, 7-Jul-2020.) (Proof modification is discouraged.)
|- Z e. V   =>    |- ( X ( t+ ` R ) Z -> X ( ( t+ ` R ) u. _I ) Z )
Theorem	frege107 36566	Proposition 107 of [Frege1879] p. 74. (Contributed by RP, 7-Jul-2020.) (Proof modification is discouraged.)
|- V e. A   =>    |- ( ( Z ( ( t+ ` R ) u. _I ) Y -> ( Y R V -> Z ( t+ ` R ) V ) ) -> ( Z ( ( t+ ` R ) u. _I ) Y -> ( Y R V -> Z ( ( t+ ` R ) u. _I ) V ) ) )
Theorem	frege108 36567	If Y belongs to the R-sequence beginning with Z, then every result of an application of the procedure R to Y belongs to the R-sequence beginning with Z. Proposition 108 of [Frege1879] p. 74. (Contributed by RP, 7-Jul-2020.) (Proof modification is discouraged.)
|- Z e. A   &    |- Y e. B   &    |- V e. C   &    |- R e. D   =>    |- ( Z ( ( t+ ` R ) u. _I ) Y -> ( Y R V -> Z ( ( t+ ` R ) u. _I ) V ) )
Theorem	frege109 36568	The property of belonging to the R-sequence beginning with X is hereditary in the R-sequence. Proposition 109 of [Frege1879] p. 74. (Contributed by RP, 7-Jul-2020.) (Proof modification is discouraged.)
|- X e. U   &    |- R e. V   =>    |- R hereditary ( ( ( t+ ` R ) u. _I ) " { X } )
Theorem	frege110 36569*	Proposition 110 of [Frege1879] p. 75. (Contributed by RP, 7-Jul-2020.) (Proof modification is discouraged.)
|- X e. A   &    |- Y e. B   &    |- M e. C   &    |- R e. D   =>    |- ( A. a ( Y R a -> X ( ( t+ ` R ) u. _I ) a ) -> ( Y ( t+ ` R ) M -> X ( ( t+ ` R ) u. _I ) M ) )
Theorem	frege111 36570	If Y belongs to the R-sequence beginning with Z, then every result of an application of the procedure R to Y belongs to the R-sequence beginning with Z or precedes Z in the R-sequence. Proposition 111 of [Frege1879] p. 75. (Contributed by RP, 7-Jul-2020.) (Revised by RP, 8-Jul-2020.) (Proof modification is discouraged.)
|- Z e. A   &    |- Y e. B   &    |- V e. C   &    |- R e. D   =>    |- ( Z ( ( t+ ` R ) u. _I ) Y -> ( Y R V -> ( -. V ( t+ ` R ) Z -> Z ( ( t+ ` R ) u. _I ) V ) ) )
Theorem	frege112 36571	Identity implies belonging to the R-sequence beginning with self. Proposition 112 of [Frege1879] p. 76. (Contributed by RP, 7-Jul-2020.) (Proof modification is discouraged.)
|- Z e. V   =>    |- ( Z = X -> X ( ( t+ ` R ) u. _I ) Z )
Theorem	frege113 36572	Proposition 113 of [Frege1879] p. 76. (Contributed by RP, 7-Jul-2020.) (Proof modification is discouraged.)
|- Z e. V   =>    |- ( ( Z ( ( t+ ` R ) u. _I ) X -> ( -. Z ( t+ ` R ) X -> Z = X ) ) -> ( Z ( ( t+ ` R ) u. _I ) X -> ( -. Z ( t+ ` R ) X -> X ( ( t+ ` R ) u. _I ) Z ) ) )
Theorem	frege114 36573	If X belongs to the R-sequence beginning with Z, then Z belongs to the R-sequence beginning with X or X follows Z in the R-sequence. Proposition 114 of [Frege1879] p. 76. (Contributed by RP, 7-Jul-2020.) (Proof modification is discouraged.)
|- X e. U   &    |- Z e. V   =>    |- ( Z ( ( t+ ` R ) u. _I ) X -> ( -. Z ( t+ ` R ) X -> X ( ( t+ ` R ) u. _I ) Z ) )
21.25.3.11  _Begriffsschrift_ Chapter III Single-valued procedures Fun `' `' R means the relationship content of procedure R is single-valued. The double converse allows us to simply apply this syntax in place of Frege's even though the original never explicitly limited discussion of propositional statments which vary on two variables to relations. dffrege115 36574 through frege133 36592 develop this and how functions relate to transitive and transitive-reflexive closures.
Theorem	dffrege115 36574*	If from the the circumstance that c is a result of an application of the procedure R to b, whatever b may be, it can be inferred that every result of an application of the procedure R to b is the same as c, then we say : "The procedure R is single-valued". Definition 115 of [Frege1879] p. 77. (Contributed by RP, 7-Jul-2020.)
|- ( A. c A. b ( b R c -> A. a ( b R a -> a = c ) ) <-> Fun `' `' R )
Theorem	frege116 36575*	One direction of dffrege115 36574. Proposition 116 of [Frege1879] p. 77. (Contributed by RP, 8-Jul-2020.) (Proof modification is discouraged.)
|- X e. U   =>    |- ( Fun `' `' R -> A. b ( b R X -> A. a ( b R a -> a = X ) ) )
Theorem	frege117 36576*	Lemma for frege118 36577. Proposition 117 of [Frege1879] p. 78. (Contributed by RP, 8-Jul-2020.) (Proof modification is discouraged.)
|- X e. U   =>    |- ( ( A. b ( b R X -> A. a ( b R a -> a = X ) ) -> ( Y R X -> A. a ( Y R a -> a = X ) ) ) -> ( Fun `' `' R -> ( Y R X -> A. a ( Y R a -> a = X ) ) ) )
Theorem	frege118 36577*	Simplified application of one direction of dffrege115 36574. Proposition 118 of [Frege1879] p. 78. (Contributed by RP, 8-Jul-2020.) (Proof modification is discouraged.)
|- X e. U   &    |- Y e. V   =>    |- ( Fun `' `' R -> ( Y R X -> A. a ( Y R a -> a = X ) ) )
Theorem	frege119 36578*	Lemma for frege120 36579. Proposition 119 of [Frege1879] p. 78. (Contributed by RP, 8-Jul-2020.) (Proof modification is discouraged.)
|- X e. U   &    |- Y e. V   =>    |- ( ( A. a ( Y R a -> a = X ) -> ( Y R A -> A = X ) ) -> ( Fun `' `' R -> ( Y R X -> ( Y R A -> A = X ) ) ) )
Theorem	frege120 36579	Simplified application of one direction of dffrege115 36574. Proposition 120 of [Frege1879] p. 78. (Contributed by RP, 8-Jul-2020.) (Proof modification is discouraged.)
|- X e. U   &    |- Y e. V   &    |- A e. W   =>    |- ( Fun `' `' R -> ( Y R X -> ( Y R A -> A = X ) ) )
Theorem	frege121 36580	Lemma for frege122 36581. Proposition 121 of [Frege1879] p. 79. (Contributed by RP, 8-Jul-2020.) (Proof modification is discouraged.)
|- X e. U   &    |- Y e. V   &    |- A e. W   =>    |- ( ( A = X -> X ( ( t+ ` R ) u. _I ) A ) -> ( Fun `' `' R -> ( Y R X -> ( Y R A -> X ( ( t+ ` R ) u. _I ) A ) ) ) )
Theorem	frege122 36581	If X is a result of an application of the single-valued procedure R to Y, then every result of an application of the procedure R to Y belongs to the R-sequence beginning with X. Proposition 122 of [Frege1879] p. 79. (Contributed by RP, 8-Jul-2020.) (Proof modification is discouraged.)
|- X e. U   &    |- Y e. V   &    |- A e. W   =>    |- ( Fun `' `' R -> ( Y R X -> ( Y R A -> X ( ( t+ ` R ) u. _I ) A ) ) )
Theorem	frege123 36582*	Lemma for frege124 36583. Proposition 123 of [Frege1879] p. 79. (Contributed by RP, 8-Jul-2020.) (Proof modification is discouraged.)
|- X e. U   &    |- Y e. V   =>    |- ( ( A. a ( Y R a -> X ( ( t+ ` R ) u. _I ) a ) -> ( Y ( t+ ` R ) M -> X ( ( t+ ` R ) u. _I ) M ) ) -> ( Fun `' `' R -> ( Y R X -> ( Y ( t+ ` R ) M -> X ( ( t+ ` R ) u. _I ) M ) ) ) )
Theorem	frege124 36583	If X is a result of an application of the single-valued procedure R to Y and if M follows Y in the R-sequence, then M belongs to the R-sequence beginning with X. Proposition 124 of [Frege1879] p. 80. (Contributed by RP, 8-Jul-2020.) (Proof modification is discouraged.)
|- X e. U   &    |- Y e. V   &    |- M e. W   &    |- R e. S   =>    |- ( Fun `' `' R -> ( Y R X -> ( Y ( t+ ` R ) M -> X ( ( t+ ` R ) u. _I ) M ) ) )
Theorem	frege125 36584	Lemma for frege126 36585. Proposition 125 of [Frege1879] p. 81. (Contributed by RP, 9-Jul-2020.) (Proof modification is discouraged.)
|- X e. U   &    |- Y e. V   &    |- M e. W   &    |- R e. S   =>    |- ( ( X ( ( t+ ` R ) u. _I ) M -> ( -. X ( t+ ` R ) M -> M ( ( t+ ` R ) u. _I ) X ) ) -> ( Fun `' `' R -> ( Y R X -> ( Y ( t+ ` R ) M -> ( -. X ( t+ ` R ) M -> M ( ( t+ ` R ) u. _I ) X ) ) ) ) )
Theorem	frege126 36585	If M follows Y in the R-sequence and if the procedure R is single-valued, then every result of an application of the procedure R to Y belongs to the R-sequence beginning with M or precedes M in the R-sequence. Proposition 126 of [Frege1879] p. 81. (Contributed by RP, 9-Jul-2020.) (Proof modification is discouraged.)
|- X e. U   &    |- Y e. V   &    |- M e. W   &    |- R e. S   =>    |- ( Fun `' `' R -> ( Y R X -> ( Y ( t+ ` R ) M -> ( -. X ( t+ ` R ) M -> M ( ( t+ ` R ) u. _I ) X ) ) ) )
Theorem	frege127 36586	Communte antecedents of frege126 36585. Proposition 127 of [Frege1879] p. 82. (Contributed by RP, 9-Jul-2020.) (Proof modification is discouraged.)
|- X e. U   &    |- Y e. V   &    |- M e. W   &    |- R e. S   =>    |- ( Fun `' `' R -> ( Y ( t+ ` R ) M -> ( Y R X -> ( -. X ( t+ ` R ) M -> M ( ( t+ ` R ) u. _I ) X ) ) ) )
Theorem	frege128 36587	Lemma for frege129 36588. Proposition 128 of [Frege1879] p. 83. (Contributed by RP, 9-Jul-2020.) (Proof modification is discouraged.)
|- X e. U   &    |- Y e. V   &    |- M e. W   &    |- R e. S   =>    |- ( ( M ( ( t+ ` R ) u. _I ) Y -> ( Y R X -> ( -. X ( t+ ` R ) M -> M ( ( t+ ` R ) u. _I ) X ) ) ) -> ( Fun `' `' R -> ( ( -. Y ( t+ ` R ) M -> M ( ( t+ ` R ) u. _I ) Y ) -> ( Y R X -> ( -. X ( t+ ` R ) M -> M ( ( t+ ` R ) u. _I ) X ) ) ) ) )
Theorem	frege129 36588	If the procedure R is single-valued and Y belongs to the R -sequence begining with M or precedes M in the R-sequence, then every result of an application of the procedure R to Y belongs to the R-sequence begining with M or precedes M in the R-sequence. Proposition 129 of [Frege1879] p. 83. (Contributed by RP, 9-Jul-2020.) (Proof modification is discouraged.)
|- X e. U   &    |- Y e. V   &    |- M e. W   &    |- R e. S   =>    |- ( Fun `' `' R -> ( ( -. Y ( t+ ` R ) M -> M ( ( t+ ` R ) u. _I ) Y ) -> ( Y R X -> ( -. X ( t+ ` R ) M -> M ( ( t+ ` R ) u. _I ) X ) ) ) )
Theorem	frege130 36589*	Lemma for frege131 36590. Proposition 130 of [Frege1879] p. 84. (Contributed by RP, 9-Jul-2020.) (Proof modification is discouraged.)
|- M e. U   &    |- R e. V   =>    |- ( ( A. b ( ( -. b ( t+ ` R ) M -> M ( ( t+ ` R ) u. _I ) b ) -> A. a ( b R a -> ( -. a ( t+ ` R ) M -> M ( ( t+ ` R ) u. _I ) a ) ) ) -> R hereditary ( ( `' ( t+ ` R ) " { M } ) u. ( ( ( t+ ` R ) u. _I ) " { M } ) ) ) -> ( Fun `' `' R -> R hereditary ( ( `' ( t+ ` R ) " { M } ) u. ( ( ( t+ ` R ) u. _I ) " { M } ) ) ) )
Theorem	frege131 36590	If the procedure R is single-valued, then the property of belonging to the R-sequence begining with M or preceeding M in the R-sequence is hereditary in the R-sequence. Proposition 131 of [Frege1879] p. 85. (Contributed by RP, 9-Jul-2020.) (Proof modification is discouraged.)
|- M e. U   &    |- R e. V   =>    |- ( Fun `' `' R -> R hereditary ( ( `' ( t+ ` R ) " { M } ) u. ( ( ( t+ ` R ) u. _I ) " { M } ) ) )
Theorem	frege132 36591	Lemma for frege133 36592. Proposition 132 of [Frege1879] p. 86. (Contributed by RP, 9-Jul-2020.) (Proof modification is discouraged.)
|- M e. U   &    |- R e. V   =>    |- ( ( R hereditary ( ( `' ( t+ ` R ) " { M } ) u. ( ( ( t+ ` R ) u. _I ) " { M } ) ) -> ( X ( t+ ` R ) M -> ( X ( t+ ` R ) Y -> ( -. Y ( t+ ` R ) M -> M ( ( t+ ` R ) u. _I ) Y ) ) ) ) -> ( Fun `' `' R -> ( X ( t+ ` R ) M -> ( X ( t+ ` R ) Y -> ( -. Y ( t+ ` R ) M -> M ( ( t+ ` R ) u. _I ) Y ) ) ) ) )
Theorem	frege133 36592	If the procedure R is single-valued and if M and Y follow X in the R-sequence, then Y belongs to the R-sequence beginning with M or precedes M in the R-sequence. Proposition 133 of [Frege1879] p. 86. (Contributed by RP, 9-Jul-2020.) (Proof modification is discouraged.)
|- X e. U   &    |- Y e. V   &    |- M e. W   &    |- R e. S   =>    |- ( Fun `' `' R -> ( X ( t+ ` R ) M -> ( X ( t+ ` R ) Y -> ( -. Y ( t+ ` R ) M -> M ( ( t+ ` R ) u. _I ) Y ) ) ) )
21.26  Mathbox for Stanislas Polu
Theorem	inductionexd 36593	Simple induction example. (Contributed by Stanislas Polu, 9-Mar-2020.)
|- ( N e. NN -> 3 || ( ( 4 ^ N ) + 5 ) )
21.26.1  IMO Problems
21.26.1.1  IMO 1972 B2
Theorem	wwlemuld 36594	Natural deduction form of lemul2d 11382. (Contributed by Stanislas Polu, 9-Mar-2020.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   &    |- ( ph -> ( C x. A ) <_ ( C x. B ) )   &    |- ( ph -> 0 < C )   =>    |- ( ph -> A <_ B )
Theorem	leeq1d 36595	Specialization of breq1d 4412 to reals and less than. (Contributed by Stanislas Polu, 9-Mar-2020.)
|- ( ph -> A <_ C )   &    |- ( ph -> A = B )   &    |- ( ph -> A e. RR )   &    |- ( ph -> C e. RR )   =>    |- ( ph -> B <_ C )
Theorem	leeq2d 36596	Specialization of breq2d 4414 to reals and less than. (Contributed by Stanislas Polu, 9-Mar-2020.)
|- ( ph -> A <_ C )   &    |- ( ph -> C = D )   &    |- ( ph -> A e. RR )   &    |- ( ph -> C e. RR )   =>    |- ( ph -> A <_ D )
Theorem	absmulrposd 36597	Specialization of absmuld with absidd 13484. (Contributed by Stanislas Polu, 9-Mar-2020.)
|- ( ph -> 0 <_ A )   &    |- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   =>    |- ( ph -> ( abs ` ( A x. B ) ) = ( A x. ( abs ` B ) ) )
Theorem	imadisjld 36598	Natural dduction form of one side of imadisj 5187. (Contributed by Stanislas Polu, 9-Mar-2020.)
|- ( ph -> ( dom A i^i B ) = (/) )   =>    |- ( ph -> ( A " B ) = (/) )
Theorem	imadisjlnd 36599	Natural deduction form of one negated side of imadisj 5187. (Contributed by Stanislas Polu, 9-Mar-2020.)
|- ( ph -> ( dom A i^i B ) =/= (/) )   =>    |- ( ph -> ( A " B ) =/= (/) )
Theorem	wnefimgd 36600	The image of a mapping from A is non empty if A is non empty. (Contributed by Stanislas Polu, 9-Mar-2020.)
|- ( ph -> A =/= (/) )   &    |- ( ph -> F : A --> B )   =>    |- ( ph -> ( F " A ) =/= (/) )