HomeHome Higher-Order Logic Explorer
Theorem List (p. 2 of 3)
< Previous  Next >
Browser slow? Try the
Unicode version.

Mirrors  >  Metamath Home Page  >  HOLE Home Page  >  Theorem List Contents       This page: Page List

Theorem List for Higher-Order Logic Explorer - 101-200   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremoveq2 101 Equality theorem for binary operation. (Contributed by Mario Carneiro, 7-Oct-2014.)
|- F:(al -> (be -> ga))   &   |- A:al   &   |- B:be   &   |- R |= [B = T]   =>   |- R |= [[AFB] = [AFT]]
 
Theoremoveq 102 Equality theorem for binary operation. (Contributed by Mario Carneiro, 7-Oct-2014.)
|- F:(al -> (be -> ga))   &   |- A:al   &   |- B:be   &   |- R |= [F = S]   =>   |- R |= [[AFB] = [ASB]]
 
Axiomax-hbl1 103 x is bound in \xA. (Contributed by Mario Carneiro, 8-Oct-2014.)
|- A:ga   &   |- B:al   =>   |- T. |= [(\x:al \x:be AB) = \x:be A]
 
Theoremhbl1 104 Inference form of ax-hbl1 103. (Contributed by Mario Carneiro, 8-Oct-2014.)
|- A:ga   &   |- B:al   &   |- R:*   =>   |- R |= [(\x:al \x:be AB) = \x:be A]
 
Axiomax-17 105* If x does not appear in A, then any substitution to A yields A again, i.e. \xA is a constant function. (Contributed by Mario Carneiro, 8-Oct-2014.)
|- A:be   &   |- B:al   =>   |- T. |= [(\x:al AB) = A]
 
Theorema17i 106* Inference form of ax-17 105. (Contributed by Mario Carneiro, 8-Oct-2014.)
|- A:be   &   |- B:al   &   |- R:*   =>   |- R |= [(\x:al AB) = A]
 
Theoremhbxfrf 107* Transfer a hypothesis builder to an equivalent expression. (Contributed by Mario Carneiro, 8-Oct-2014.)
|- T:be   &   |- B:al   &   |- R |= [T = A]   &   |- (S, R) |= [(\x:al AB) = A]   =>   |- (S, R) |= [(\x:al TB) = T]
 
Theoremhbxfr 108* Transfer a hypothesis builder to an equivalent expression. (Contributed by Mario Carneiro, 8-Oct-2014.)
|- T:be   &   |- B:al   &   |- R |= [T = A]   &   |- R |= [(\x:al AB) = A]   =>   |- R |= [(\x:al TB) = T]
 
Theoremhbth 109* Hypothesis builder for a theorem. (Contributed by Mario Carneiro, 8-Oct-2014.)
|- B:al   &   |- R |= A   =>   |- R |= [(\x:al AB) = A]
 
Theoremhbc 110 Hypothesis builder for combination. (Contributed by Mario Carneiro, 8-Oct-2014.)
|- F:(be -> ga)   &   |- A:be   &   |- B:al   &   |- R |= [(\x:al FB) = F]   &   |- R |= [(\x:al AB) = A]   =>   |- R |= [(\x:al (FA)B) = (FA)]
 
Theoremhbov 111 Hypothesis builder for binary operation. (Contributed by Mario Carneiro, 8-Oct-2014.)
|- F:(be -> (ga -> de))   &   |- A:be   &   |- B:al   &   |- C:ga   &   |- R |= [(\x:al FB) = F]   &   |- R |= [(\x:al AB) = A]   &   |- R |= [(\x:al CB) = C]   =>   |- R |= [(\x:al [AFC]B) = [AFC]]
 
Theoremhbl 112* Hypothesis builder for lambda abstraction. (Contributed by Mario Carneiro, 8-Oct-2014.)
|- A:ga   &   |- B:al   &   |- R |= [(\x:al AB) = A]   =>   |- R |= [(\x:al \y:be AB) = \y:be A]
 
Axiomax-inst 113* Instantiate a theorem with a new term. The second and third hypotheses are the HOL equivalent of set.mm "effectively not free in" predicate (see set.mm's ax-17, or ax17m 218). (Contributed by Mario Carneiro, 8-Oct-2014.)
|- R |= A   &   |- T. |= [(\x:al By:al) = B]   &   |- T. |= [(\x:al Sy:al) = S]   &   |- [x:al = C] |= [A = B]   &   |- [x:al = C] |= [R = S]   =>   |- S |= B
 
Theoreminsti 114* Instantiate a theorem with a new term. (Contributed by Mario Carneiro, 8-Oct-2014.)
|- C:al   &   |- B:*   &   |- R |= A   &   |- T. |= [(\x:al By:al) = B]   &   |- [x:al = C] |= [A = B]   =>   |- R |= B
 
Theoremclf 115* Evaluate a lambda expression. (Contributed by Mario Carneiro, 8-Oct-2014.)
|- A:be   &   |- C:al   &   |- [x:al = C] |= [A = B]   &   |- T. |= [(\x:al By:al) = B]   &   |- T. |= [(\x:al Cy:al) = C]   =>   |- T. |= [(\x:al AC) = B]
 
Theoremcl 116* Evaluate a lambda expression. (Contributed by Mario Carneiro, 8-Oct-2014.)
|- A:be   &   |- C:al   &   |- [x:al = C] |= [A = B]   =>   |- T. |= [(\x:al AC) = B]
 
Theoremovl 117* Evaluate a lambda expression in a binary operation. (Contributed by Mario Carneiro, 8-Oct-2014.)
|- A:ga   &   |- S:al   &   |- T:be   &   |- [x:al = S] |= [A = B]   &   |- [y:be = T] |= [B = C]   =>   |- T. |= [[S\x:al \y:be AT] = C]
 
0.2  Add propositional calculus definitions
 
Syntaxtfal 118 Contradiction term.
term F.
 
Syntaxtan 119 Conjunction term.
term /\
 
Syntaxtne 120 Negation term.
term ~
 
Syntaxtim 121 Implication term.
term ==>
 
Syntaxtal 122 For all term.
term A.
 
Syntaxtex 123 There exists term.
term E.
 
Syntaxtor 124 Disjunction term.
term \/
 
Syntaxteu 125 There exists unique term.
term E!
 
Definitiondf-al 126* Define the for all operator. (Contributed by Mario Carneiro, 8-Oct-2014.)
|- T. |= [A. = \p:(al -> *) [p:(al -> *) = \x:al T.]]
 
Definitiondf-fal 127 Define the constant false. (Contributed by Mario Carneiro, 8-Oct-2014.)
|- T. |= [F. = (A.\p:* p:*)]
 
Definitiondf-an 128* Define the 'and' operator. (Contributed by Mario Carneiro, 8-Oct-2014.)
|- T. |= [ /\ = \p:* \q:* [\f:(* -> (* -> *)) [p:*f:(* -> (* -> *))q:*] = \f:(* -> (* -> *)) [T.f:(* -> (* -> *))T.]]]
 
Definitiondf-im 129* Define the implication operator. (Contributed by Mario Carneiro, 8-Oct-2014.)
|- T. |= [ ==> = \p:* \q:* [[p:* /\ q:*] = p:*]]
 
Definitiondf-not 130 Define the negation operator. (Contributed by Mario Carneiro, 8-Oct-2014.)
|- T. |= [~ = \p:* [p:* ==> F.]]
 
Definitiondf-ex 131* Define the existence operator. (Contributed by Mario Carneiro, 8-Oct-2014.)
|- T. |= [E. = \p:(al -> *) (A.\q:* [(A.\x:al [(p:(al -> *)x:al) ==> q:*]) ==> q:*])]
 
Definitiondf-or 132* Define the 'or' operator. (Contributed by Mario Carneiro, 8-Oct-2014.)
|- T. |= [ \/ = \p:* \q:* (A.\x:* [[p:* ==> x:*] ==> [[q:* ==> x:*] ==> x:*]])]
 
Definitiondf-eu 133* Define the 'exists unique' operator. (Contributed by Mario Carneiro, 8-Oct-2014.)
|- T. |= [E! = \p:(al -> *) (E.\y:al (A.\x:al [(p:(al -> *)x:al) = [x:al = y:al]]))]
 
Theoremwal 134 For all type. (Contributed by Mario Carneiro, 8-Oct-2014.)
|- A.:((al -> *) -> *)
 
Theoremwfal 135 Contradiction type. (Contributed by Mario Carneiro, 8-Oct-2014.)
|- F.:*
 
Theoremwan 136 Conjunction type. (Contributed by Mario Carneiro, 8-Oct-2014.)
|- /\ :(* -> (* -> *))
 
Theoremwim 137 Implication type. (Contributed by Mario Carneiro, 8-Oct-2014.)
|- ==> :(* -> (* -> *))
 
Theoremwnot 138 Negation type. (Contributed by Mario Carneiro, 8-Oct-2014.)
|- ~ :(* -> *)
 
Theoremwex 139 There exists type. (Contributed by Mario Carneiro, 8-Oct-2014.)
|- E.:((al -> *) -> *)
 
Theoremwor 140 Disjunction type. (Contributed by Mario Carneiro, 8-Oct-2014.)
|- \/ :(* -> (* -> *))
 
Theoremweu 141 There exists unique type. (Contributed by Mario Carneiro, 8-Oct-2014.)
|- E!:((al -> *) -> *)
 
Theoremalval 142* Value of the for all predicate. (Contributed by Mario Carneiro, 8-Oct-2014.)
|- F:(al -> *)   =>   |- T. |= [(A.F) = [F = \x:al T.]]
 
Theoremexval 143* Value of the 'there exists' predicate. (Contributed by Mario Carneiro, 8-Oct-2014.)
|- F:(al -> *)   =>   |- T. |= [(E.F) = (A.\q:* [(A.\x:al [(Fx:al) ==> q:*]) ==> q:*])]
 
Theoremeuval 144* Value of the 'exists unique' predicate. (Contributed by Mario Carneiro, 8-Oct-2014.)
|- F:(al -> *)   =>   |- T. |= [(E!F) = (E.\y:al (A.\x:al [(Fx:al) = [x:al = y:al]]))]
 
Theoremnotval 145 Value of negation. (Contributed by Mario Carneiro, 8-Oct-2014.)
|- A:*   =>   |- T. |= [(~ A) = [A ==> F.]]
 
Theoremimval 146 Value of the implication. (Contributed by Mario Carneiro, 9-Oct-2014.)
|- A:*   &   |- B:*   =>   |- T. |= [[A ==> B] = [[A /\ B] = A]]
 
Theoremorval 147* Value of the disjunction. (Contributed by Mario Carneiro, 9-Oct-2014.)
|- A:*   &   |- B:*   =>   |- T. |= [[A \/ B] = (A.\x:* [[A ==> x:*] ==> [[B ==> x:*] ==> x:*]])]
 
Theoremanval 148* Value of the conjunction. (Contributed by Mario Carneiro, 9-Oct-2014.)
|- A:*   &   |- B:*   =>   |- T. |= [[A /\ B] = [\f:(* -> (* -> *)) [Af:(* -> (* -> *))B] = \f:(* -> (* -> *)) [T.f:(* -> (* -> *))T.]]]
 
Theoremax4g 149 If F is true for all x:al, then it is true for A. (Contributed by Mario Carneiro, 9-Oct-2014.)
|- F:(al -> *)   &   |- A:al   =>   |- (A.F) |= (FA)
 
Theoremax4 150 If A is true for all x:al, then it is true for A. (Contributed by Mario Carneiro, 9-Oct-2014.)
|- A:*   =>   |- (A.\x:al A) |= A
 
Theoremalrimiv 151* If one can prove R |= A where R does not contain x, then A is true for all x. (Contributed by Mario Carneiro, 9-Oct-2014.)
|- R |= A   =>   |- R |= (A.\x:al A)
 
Theoremcla4v 152* If A(x) is true for all x:al, then it is true for C = A(B). (Contributed by Mario Carneiro, 9-Oct-2014.)
|- A:*   &   |- B:al   &   |- [x:al = B] |= [A = C]   =>   |- (A.\x:al A) |= C
 
Theorempm2.21 153 A falsehood implies anything. (Contributed by Mario Carneiro, 9-Oct-2014.)
|- A:*   =>   |- F. |= A
 
Theoremdfan2 154 An alternative definition of the "and" term in terms of the context conjunction. (Contributed by Mario Carneiro, 9-Oct-2014.)
|- A:*   &   |- B:*   =>   |- T. |= [[A /\ B] = (A, B)]
 
Theoremhbct 155 Hypothesis builder for context conjunction. (Contributed by Mario Carneiro, 8-Oct-2014.)
|- A:*   &   |- B:al   &   |- C:*   &   |- R |= [(\x:al AB) = A]   &   |- R |= [(\x:al CB) = C]   =>   |- R |= [(\x:al (A, C)B) = (A, C)]
 
Theoremmpd 156 Modus ponens. (Contributed by Mario Carneiro, 9-Oct-2014.)
|- T:*   &   |- R |= S   &   |- R |= [S ==> T]   =>   |- R |= T
 
Theoremimp 157 Importation deduction. (Contributed by Mario Carneiro, 9-Oct-2014.)
|- S:*   &   |- T:*   &   |- R |= [S ==> T]   =>   |- (R, S) |= T
 
Theoremex 158 Exportation deduction. (Contributed by Mario Carneiro, 9-Oct-2014.)
|- (R, S) |= T   =>   |- R |= [S ==> T]
 
Theoremnotval2 159 Another way two write ~ A, the negation of A. (Contributed by Mario Carneiro, 9-Oct-2014.)
|- A:*   =>   |- T. |= [(~ A) = [A = F.]]
 
Theoremnotnot1 160 One side of notnot 200. (Contributed by Mario Carneiro, 10-Oct-2014.)
|- A:*   =>   |- A |= (~ (~ A))
 
Theoremcon2d 161 A contraposition deduction. (Contributed by Mario Carneiro, 10-Oct-2014.)
|- T:*   &   |- (R, S) |= (~ T)   =>   |- (R, T) |= (~ S)
 
Theoremcon3d 162 A contraposition deduction. (Contributed by Mario Carneiro, 10-Oct-2014.)
|- (R, S) |= T   =>   |- (R, (~ T)) |= (~ S)
 
Theoremecase 163 Elimination by cases. (Contributed by Mario Carneiro, 9-Oct-2014.)
|- A:*   &   |- B:*   &   |- T:*   &   |- R |= [A \/ B]   &   |- (R, A) |= T   &   |- (R, B) |= T   =>   |- R |= T
 
Theoremolc 164 Or introduction. (Contributed by Mario Carneiro, 9-Oct-2014.)
|- A:*   &   |- B:*   =>   |- B |= [A \/ B]
 
Theoremorc 165 Or introduction. (Contributed by Mario Carneiro, 9-Oct-2014.)
|- A:*   &   |- B:*   =>   |- A |= [A \/ B]
 
Theoremexlimdv2 166* Existential elimination. (Contributed by Mario Carneiro, 9-Oct-2014.)
|- F:(al -> *)   &   |- (R, (Fx:al)) |= T   =>   |- (R, (E.F)) |= T
 
Theoremexlimdv 167* Existential elimination. (Contributed by Mario Carneiro, 9-Oct-2014.)
|- (R, A) |= T   =>   |- (R, (E.\x:al A)) |= T
 
Theoremax4e 168 Existential introduction. (Contributed by Mario Carneiro, 9-Oct-2014.)
|- F:(al -> *)   &   |- A:al   =>   |- (FA) |= (E.F)
 
Theoremcla4ev 169* Existential introduction. (Contributed by Mario Carneiro, 9-Oct-2014.)
|- A:*   &   |- B:al   &   |- [x:al = B] |= [A = C]   =>   |- C |= (E.\x:al A)
 
Theorem19.8a 170 Existential introduction. (Contributed by Mario Carneiro, 9-Oct-2014.)
|- A:*   =>   |- A |= (E.\x:al A)
 
0.3  Type definition mechanism
 
SyntaxwffMMJ2d 171 Internal axiom for mmj2 use.
wff typedef al(A, B)C
 
Axiomax-wabs 172 Type of the abstraction function. (New usage is discouraged.) (Contributed by Mario Carneiro, 8-Oct-2014.)
|- B:al   &   |- F:(al -> *)   &   |- T. |= (FB)   &   |- typedef be(A, R)F   =>   |- A:(al -> be)
 
Axiomax-wrep 173 Type of the representation function. (New usage is discouraged.) (Contributed by Mario Carneiro, 8-Oct-2014.)
|- B:al   &   |- F:(al -> *)   &   |- T. |= (FB)   &   |- typedef be(A, R)F   =>   |- R:(be -> al)
 
Theoremwabs 174 Type of the abstraction function. (Contributed by Mario Carneiro, 8-Oct-2014.)
|- B:al   &   |- F:(al -> *)   &   |- T. |= (FB)   &   |- typedef be(A, R)F   =>   |- A:(al -> be)
 
Theoremwrep 175 Type of the representation function. (Contributed by Mario Carneiro, 8-Oct-2014.)
|- B:al   &   |- F:(al -> *)   &   |- T. |= (FB)   &   |- typedef be(A, R)F   =>   |- R:(be -> al)
 
Axiomax-tdef 176* The type definition axiom. The last hypothesis corresponds to the actual definition one wants to make; here we are defining a new type be and the definition will provide us with pair of bijections A, R mapping the new type be to the subset of the old type al such that Fx is true. In order for this to be a valid (conservative) extension, we must ensure that the new type is nonempty, and for that purpose we need a witness B that F is not always false. (Contributed by Mario Carneiro, 8-Oct-2014.)
|- B:al   &   |- F:(al -> *)   &   |- T. |= (FB)   &   |- typedef be(A, R)F   =>   |- T. |= ((A.\x:be [(A(Rx:be)) = x:be]), (A.\x:al [(Fx:al) = [(R(Ax:al)) = x:al]]))
 
0.4  Extensionality
 
Axiomax-eta 177* The eta-axiom: a function is determined by its values. (Contributed by Mario Carneiro, 8-Oct-2014.)
|- T. |= (A.\f:(al -> be) [\x:al (f:(al -> be)x:al) = f:(al -> be)])
 
Theoremeta 178* The eta-axiom: a function is determined by its values. (Contributed by Mario Carneiro, 8-Oct-2014.)
|- F:(al -> be)   =>   |- T. |= [\x:al (Fx:al) = F]
 
Theoremcbvf 179* Change bound variables in a lambda abstraction. (Contributed by Mario Carneiro, 8-Oct-2014.)
|- A:be   &   |- T. |= [(\y:al Az:al) = A]   &   |- T. |= [(\x:al Bz:al) = B]   &   |- [x:al = y:al] |= [A = B]   =>   |- T. |= [\x:al A = \y:al B]
 
Theoremcbv 180* Change bound variables in a lambda abstraction. (Contributed by Mario Carneiro, 8-Oct-2014.)
|- A:be   &   |- [x:al = y:al] |= [A = B]   =>   |- T. |= [\x:al A = \y:al B]
 
Theoremleqf 181* Equality theorem for lambda abstraction, using bound variable instead of distinct variables. (Contributed by Mario Carneiro, 8-Oct-2014.)
|- A:be   &   |- R |= [A = B]   &   |- T. |= [(\x:al Ry:al) = R]   =>   |- R |= [\x:al A = \x:al B]
 
Theoremalrimi 182* If one can prove R |= A where R does not contain x, then A is true for all x. (Contributed by Mario Carneiro, 9-Oct-2014.)
|- R |= A   &   |- T. |= [(\x:al Ry:al) = R]   =>   |- R |= (A.\x:al A)
 
Theoremexlimd 183* Existential elimination. (Contributed by Mario Carneiro, 9-Oct-2014.)
|- (R, A) |= T   &   |- T. |= [(\x:al Ry:al) = R]   &   |- T. |= [(\x:al Ty:al) = T]   =>   |- (R, (E.\x:al A)) |= T
 
Theoremalimdv 184* Deduction from Theorem 19.20 of [Margaris] p. 90. (Contributed by Mario Carneiro, 9-Oct-2014.)
|- (R, A) |= B   =>   |- (R, (A.\x:al A)) |= (A.\x:al B)
 
Theoremeximdv 185* Deduction from Theorem 19.22 of [Margaris] p. 90. (Contributed by Mario Carneiro, 9-Oct-2014.)
|- (R, A) |= B   =>   |- (R, (E.\x:al A)) |= (E.\x:al B)
 
Theoremalnex 186* Theorem 19.7 of [Margaris] p. 89. (Contributed by Mario Carneiro, 10-Oct-2014.)
|- A:*   =>   |- T. |= [(A.\x:al (~ A)) = (~ (E.\x:al A))]
 
Theoremexnal1 187* Forward direction of exnal 201. (Contributed by Mario Carneiro, 10-Oct-2014.)
|- A:*   =>   |- (E.\x:al (~ A)) |= (~ (A.\x:al A))
 
Theoremisfree 188* Derive the metamath "is free" predicate in terms of the HOL "is free" predicate. (Contributed by Mario Carneiro, 9-Oct-2014.)
|- A:*   &   |- T. |= [(\x:al Ay:al) = A]   =>   |- T. |= [A ==> (A.\x:al A)]
 
0.5  Axioms of infinity and choice
 
Syntaxtf11 189 One-to-one function.
term 1-1
 
Syntaxtfo 190 Onto function.
term onto
 
Syntaxtat 191 Indefinite descriptor.
term @
 
Axiomax-wat 192 The type of the indefinite descriptor. (New usage is discouraged.) (Contributed by Mario Carneiro, 10-Oct-2014.)
|- @:((al -> *) -> al)
 
Theoremwat 193 The type of the indefinite descriptor. (Contributed by Mario Carneiro, 10-Oct-2014.)
|- @:((al -> *) -> al)
 
Definitiondf-f11 194* Define a one-to-one function. (Contributed by Mario Carneiro, 10-Oct-2014.)
|- T. |= [1-1 = \f:(al -> be) (A.\x:al (A.\y:al [[(f:(al -> be)x:al) = (f:(al -> be)y:al)] ==> [x:al = y:al]]))]
 
Definitiondf-fo 195* Define an onto function. (Contributed by Mario Carneiro, 10-Oct-2014.)
|- T. |= [onto = \f:(al -> be) (A.\y:be (E.\x:al [y:be = (f:(al -> be)x:al)]))]
 
Axiomax-ac 196* Defining property of the indefinite descriptor: it selects an element from any type. This is equivalent to global choice in ZF. (Contributed by Mario Carneiro, 10-Oct-2014.)
|- T. |= (A.\p:(al -> *) (A.\x:al [(p:(al -> *)x:al) ==> (p:(al -> *)(@p:(al -> *)))]))
 
Theoremac 197 Defining property of the indefinite descriptor: it selects an element from any type. This is equivalent to global choice in ZF. (Contributed by Mario Carneiro, 10-Oct-2014.)
|- F:(al -> *)   &   |- A:al   =>   |- (FA) |= (F(@F))
 
Theoremdfex2 198 Alternative definition of the "there exists" quantifier. (Contributed by Mario Carneiro, 10-Oct-2014.)
|- F:(al -> *)   =>   |- T. |= [(E.F) = (F(@F))]
 
Theoremexmid 199 Diaconescu's theorem, which derives the law of the excluded middle from the axiom of choice. (Contributed by Mario Carneiro, 10-Oct-2014.)
|- A:*   =>   |- T. |= [A \/ (~ A)]
 
Theoremnotnot 200 Rule of double negation. (Contributed by Mario Carneiro, 10-Oct-2014.)
|- A:*   =>   |- T. |= [A = (~ (~ A))]
    < Previous  Next >

Page List
Jump to page: Contents  1 1-100101-200 3 201-222
  Copyright terms: Public domain < Previous  Next >