P. 367 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 36601-36700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	frege71 36601*	Lemma for frege72 36602. 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 36602	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 36603	Lemma for frege87 36617. 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 36604	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 36605*	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 36606 through frege98 36628 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 36606*	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 36607*	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 36608*	Commuted form of of frege77 36607. 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 36609*	Distributed form of frege78 36608. 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 36610*	Add additional condition to both clauses of frege79 36609. 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 36611	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 36612	Closed-form deduction based on frege81 36611. 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 36613	Apply commuted form of frege81 36611 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 36614	Commuted form of frege81 36611. 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 36615*	Commuted form of frege77 36607. 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 36616*	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 36617*	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 36618*	Commuted form of frege87 36617. 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 36619*	One direction of dffrege76 36606. 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 36620*	Add antecedent to frege89 36619. 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 36621	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 36622	Inference from frege91 36621. 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 36623*	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 36624*	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 36625	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 36626	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 36627	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 36628	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 36629 through frege114 36644 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 36629	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 36630	One direction of dffrege99 36629. 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 36631	Lemma for frege102 36632. 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 36632	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 36633	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 36634	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 36635	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 36636	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 36637	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 36638	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 36639	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 36640*	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 36641	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 36642	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 36643	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 36644	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 36645 through frege133 36663 develop this and how functions relate to transitive and transitive-reflexive closures.
Theorem	dffrege115 36645*	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 36646*	One direction of dffrege115 36645. 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 36647*	Lemma for frege118 36648. 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 36648*	Simplified application of one direction of dffrege115 36645. 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 36649*	Lemma for frege120 36650. 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 36650	Simplified application of one direction of dffrege115 36645. 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 36651	Lemma for frege122 36652. 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 36652	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 36653*	Lemma for frege124 36654. 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 36654	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 36655	Lemma for frege126 36656. 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 36656	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 36657	Communte antecedents of frege126 36656. 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 36658	Lemma for frege129 36659. 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 36659	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 36660*	Lemma for frege131 36661. 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 36661	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 36662	Lemma for frege133 36663. 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 36663	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 36664	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 36665	Natural deduction form of lemul2d 11405. (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 36666	Specialization of breq1d 4405 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 36667	Specialization of breq2d 4407 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 36668	Specialization of absmuld with absidd 13561. (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 36669	Natural dduction form of one side of imadisj 5193. (Contributed by Stanislas Polu, 9-Mar-2020.)
|- ( ph -> ( dom A i^i B ) = (/) )   =>    |- ( ph -> ( A " B ) = (/) )
Theorem	imadisjlnd 36670	Natural deduction form of one negated side of imadisj 5193. (Contributed by Stanislas Polu, 9-Mar-2020.)
|- ( ph -> ( dom A i^i B ) =/= (/) )   =>    |- ( ph -> ( A " B ) =/= (/) )
Theorem	wnefimgd 36671	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 ) =/= (/) )
Theorem	fco2d 36672	Natural deduction form of fco2 5752. (Contributed by Stanislas Polu, 9-Mar-2020.)
|- ( ph -> G : A --> B )   &    |- ( ph -> ( F |` B ) : B --> C )   =>    |- ( ph -> ( F o. G ) : A --> C )
Theorem	suprubd 36673*	Natural deduction form of suprubd 36673. (Contributed by Stanislas Polu, 9-Mar-2020.)
|- ( ph -> A C_ RR )   &    |- ( ph -> A =/= (/) )   &    |- ( ph -> E. x e. RR A. y e. A y <_ x )   &    |- ( ph -> B e. A )   =>    |- ( ph -> B <_ sup ( A , RR , < ) )
Theorem	suprcld 36674*	Natural deduction form of suprcl 10591. (Contributed by Stanislas Polu, 9-Mar-2020.)
|- ( ph -> A C_ RR )   &    |- ( ph -> A =/= (/) )   &    |- ( ph -> E. x e. RR A. y e. A y <_ x )   =>    |- ( ph -> sup ( A , RR , < ) e. RR )
Theorem	fvco3d 36675	Natural deduction form of fvco3 5957. (Contributed by Stanislas Polu, 9-Mar-2020.)
|- ( ph -> G : A --> B )   &    |- ( ph -> C e. A )   =>    |- ( ph -> ( ( F o. G ) ` C ) = ( F ` ( G ` C ) ) )
Theorem	wfximgfd 36676	The value of a function on its domain is in the image of the function. (Contributed by Stanislas Polu, 9-Mar-2020.)
|- ( ph -> C e. A )   &    |- ( ph -> F : A --> B )   =>    |- ( ph -> ( F ` C ) e. ( F " A ) )
Theorem	fvelimabd 36677*	Natural deduction form of fvelimab 5936. (Contributed by Stanislas Polu, 9-Mar-2020.)
|- ( ph -> F Fn A )   &    |- ( ph -> B C_ A )   =>    |- ( ph -> ( C e. ( F " B ) <-> E. x e. B ( F ` x ) = C ) )
Theorem	extoimad 36678*	If |f(x)| <= C for all x then it applies to all x in the image of |f(x)| (Contributed by Stanislas Polu, 9-Mar-2020.)
|- ( ph -> F : RR --> RR )   &    |- ( ph -> A. y e. RR ( abs ` ( F ` y ) ) <_ C )   =>    |- ( ph -> A. x e. ( abs " ( F " RR ) ) x <_ C )
Theorem	imo72b2lem0 36679*	Lemma for imo72b2 36689. (Contributed by Stanislas Polu, 9-Mar-2020.)
|- ( ph -> F : RR --> RR )   &    |- ( ph -> G : RR --> RR )   &    |- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> ( ( F ` ( A + B ) ) + ( F ` ( A - B ) ) ) = ( 2 x. ( ( F ` A ) x. ( G ` B ) ) ) )   &    |- ( ph -> A. y e. RR ( abs ` ( F ` y ) ) <_ 1 )   =>    |- ( ph -> ( ( abs ` ( F ` A ) ) x. ( abs ` ( G ` B ) ) ) <_ sup ( ( abs " ( F " RR ) ) , RR , < ) )
Theorem	suprleubrd 36680*	Natural deduction form of specialized suprleub 10595. (Contributed by Stanislas Polu, 9-Mar-2020.)
|- ( ph -> A C_ RR )   &    |- ( ph -> A =/= (/) )   &    |- ( ph -> E. x e. RR A. y e. A y <_ x )   &    |- ( ph -> B e. RR )   &    |- ( ph -> A. z e. A z <_ B )   =>    |- ( ph -> sup ( A , RR , < ) <_ B )
Theorem	imo72b2lem2 36681*	Lemma for imo72b2 36689. (Contributed by Stanislas Polu, 9-Mar-2020.)
|- ( ph -> F : RR --> RR )   &    |- ( ph -> C e. RR )   &    |- ( ph -> A. z e. RR ( abs ` ( F ` z ) ) <_ C )   =>    |- ( ph -> sup ( ( abs " ( F " RR ) ) , RR , < ) <_ C )
Theorem	syldbl2 36682	Stacked hypotheseis implies goal. (Contributed by Stanislas Polu, 9-Mar-2020.)
|- ( ( ph /\ ps ) -> ( ps -> th ) )   =>    |- ( ( ph /\ ps ) -> th )
Theorem	funfvima2d 36683	A function's value in a preimage belongs to the image. (Contributed by Stanislas Polu, 9-Mar-2020.)
|- ( ph -> F : A --> B )   =>    |- ( ( ph /\ x e. A ) -> ( F ` x ) e. ( F " A ) )
Theorem	suprlubrd 36684*	Natural deduction form of specialized suprlub 10593. (Contributed by Stanislas Polu, 9-Mar-2020.)
|- ( ph -> A C_ RR )   &    |- ( ph -> A =/= (/) )   &    |- ( ph -> E. x e. RR A. y e. A y <_ x )   &    |- ( ph -> B e. RR )   &    |- ( ph -> E. z e. A B < z )   =>    |- ( ph -> B < sup ( A , RR , < ) )
Theorem	imo72b2lem1 36685*	Lemma for imo72b2 36689. (Contributed by Stanislas Polu, 9-Mar-2020.)
|- ( ph -> F : RR --> RR )   &    |- ( ph -> E. x e. RR ( F ` x ) =/= 0 )   &    |- ( ph -> A. y e. RR ( abs ` ( F ` y ) ) <_ 1 )   =>    |- ( ph -> 0 < sup ( ( abs " ( F " RR ) ) , RR , < ) )
Theorem	lemuldiv3d 36686	'Less than or equal to' relationship between division and multiplication. (Contributed by Stanislas Polu, 9-Mar-2020.)
|- ( ph -> ( B x. A ) <_ C )   &    |- ( ph -> 0 < A )   &    |- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   =>    |- ( ph -> B <_ ( C / A ) )
Theorem	lemuldiv4d 36687	'Less than or equal to' relationship between division and multiplication. (Contributed by Stanislas Polu, 9-Mar-2020.)
|- ( ph -> B <_ ( C / A ) )   &    |- ( ph -> 0 < A )   &    |- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   =>    |- ( ph -> ( B x. A ) <_ C )
Theorem	rspcdvinvd 36688*	If something is true for all then it's true for some class. (Contributed by Stanislas Polu, 9-Mar-2020.)
|- ( ( ph /\ x = A ) -> ( ps <-> ch ) )   &    |- ( ph -> A e. B )   &    |- ( ph -> A. x e. B ps )   =>    |- ( ph -> ch )
Theorem	imo72b2 36689*	IMO 1972 B2. (14th International Mathemahics Olympiad in Poland, problem B2). (Contributed by Stanislas Polu, 9-Mar-2020.)
|- ( ph -> F : RR --> RR )   &    |- ( ph -> G : RR --> RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> A. u e. RR A. v e. RR ( ( F ` ( u + v ) ) + ( F ` ( u - v ) ) ) = ( 2 x. ( ( F ` u ) x. ( G ` v ) ) ) )   &    |- ( ph -> A. y e. RR ( abs ` ( F ` y ) ) <_ 1 )   &    |- ( ph -> E. x e. RR ( F ` x ) =/= 0 )   =>    |- ( ph -> ( abs ` ( G ` B ) ) <_ 1 )
21.26.2  INT Inequalities Proof Generator This section formalizes theorems necessary to reproduce the equality and inequality generator described in "Neural Theorem Proving on Inequality Problems" http://aitp-conference.org/2020/abstract/paper_18.pdf. Other theorems required: 0red 9662 1red 9676 readdcld 9688 remulcld 9689 eqcomd 2477.
Theorem	int-addcomd 36690	AdditionCommutativity generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
|- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   &    |- ( ph -> A = B )   =>    |- ( ph -> ( B + C ) = ( C + A ) )
Theorem	int-addassocd 36691	AdditionAssociativity generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
|- ( ph -> A e. RR )   &    |- ( ph -> C e. RR )   &    |- ( ph -> D e. RR )   &    |- ( ph -> A = B )   =>    |- ( ph -> ( B + ( C + D ) ) = ( ( A + C ) + D ) )
Theorem	int-addsimpd 36692	AdditionSimplification generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
|- ( ph -> A e. RR )   &    |- ( ph -> A = B )   =>    |- ( ph -> 0 = ( A - B ) )
Theorem	int-mulcomd 36693	MultiplicationCommutativity generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
|- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   &    |- ( ph -> A = B )   =>    |- ( ph -> ( B x. C ) = ( C x. A ) )
Theorem	int-mulassocd 36694	MultiplicationAssociativity generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
|- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   &    |- ( ph -> D e. RR )   &    |- ( ph -> A = B )   =>    |- ( ph -> ( B x. ( C x. D ) ) = ( ( A x. C ) x. D ) )
Theorem	int-mulsimpd 36695	MultiplicationSimplification generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
|- ( ph -> B e. RR )   &    |- ( ph -> A = B )   &    |- ( ph -> B =/= 0 )   =>    |- ( ph -> 1 = ( A / B ) )
Theorem	int-leftdistd 36696	AdditionMultiplicationLeftDistribution generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
|- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   &    |- ( ph -> D e. RR )   &    |- ( ph -> A = B )   =>    |- ( ph -> ( ( C + D ) x. B ) = ( ( C x. A ) + ( D x. A ) ) )
Theorem	int-rightdistd 36697	AdditionMultiplicationRightDistribution generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
|- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   &    |- ( ph -> D e. RR )   &    |- ( ph -> A = B )   =>    |- ( ph -> ( B x. ( C + D ) ) = ( ( A x. C ) + ( A x. D ) ) )
Theorem	int-sqdefd 36698	SquareDefinition generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
|- ( ph -> B e. RR )   &    |- ( ph -> A = B )   =>    |- ( ph -> ( A x. B ) = ( A ^ 2 ) )
Theorem	int-mul11d 36699	First MultiplicationOne generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
|- ( ph -> A e. RR )   &    |- ( ph -> A = B )   =>    |- ( ph -> ( A x. 1 ) = B )
Theorem	int-mul12d 36700	Second MultiplicationOne generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
|- ( ph -> A e. RR )   &    |- ( ph -> A = B )   =>    |- ( ph -> ( 1 x. A ) = B )