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:(α → (βγ))    &   A:α    &   B:β    &   R⊧[B = T]       R⊧[[AFB] = [AFT]]

Theoremoveq 102 Equality theorem for binary operation. (Contributed by Mario Carneiro, 7-Oct-2014.)
F:(α → (βγ))    &   A:α    &   B:β    &   R⊧[F = S]       R⊧[[AFB] = [ASB]]

Axiomax-hbl1 103 x is bound in λxA. (Contributed by Mario Carneiro, 8-Oct-2014.)
A:γ    &   B:α       ⊤⊧[(λx:α λx:β AB) = λx:β A]

Theoremhbl1 104 Inference form of ax-hbl1 103. (Contributed by Mario Carneiro, 8-Oct-2014.)
A:γ    &   B:α    &   R:∗       R⊧[(λx:α λx:β AB) = λx:β 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:β    &   B:α       ⊤⊧[(λx:α AB) = A]

Theorema17i 106* Inference form of ax-17 105. (Contributed by Mario Carneiro, 8-Oct-2014.)
A:β    &   B:α    &   R:∗       R⊧[(λx:α AB) = A]

Theoremhbxfrf 107* Transfer a hypothesis builder to an equivalent expression. (Contributed by Mario Carneiro, 8-Oct-2014.)
T:β    &   B:α    &   R⊧[T = A]    &   (S, R)⊧[(λx:α AB) = A]       (S, R)⊧[(λx:α TB) = T]

Theoremhbxfr 108* Transfer a hypothesis builder to an equivalent expression. (Contributed by Mario Carneiro, 8-Oct-2014.)
T:β    &   B:α    &   R⊧[T = A]    &   R⊧[(λx:α AB) = A]       R⊧[(λx:α TB) = T]

Theoremhbth 109* Hypothesis builder for a theorem. (Contributed by Mario Carneiro, 8-Oct-2014.)
B:α    &   RA       R⊧[(λx:α AB) = A]

Theoremhbc 110 Hypothesis builder for combination. (Contributed by Mario Carneiro, 8-Oct-2014.)
F:(βγ)    &   A:β    &   B:α    &   R⊧[(λx:α FB) = F]    &   R⊧[(λx:α AB) = A]       R⊧[(λx:α (FA)B) = (FA)]

Theoremhbov 111 Hypothesis builder for binary operation. (Contributed by Mario Carneiro, 8-Oct-2014.)
F:(β → (γδ))    &   A:β    &   B:α    &   C:γ    &   R⊧[(λx:α FB) = F]    &   R⊧[(λx:α AB) = A]    &   R⊧[(λx:α CB) = C]       R⊧[(λx:α [AFC]B) = [AFC]]

Theoremhbl 112* Hypothesis builder for lambda abstraction. (Contributed by Mario Carneiro, 8-Oct-2014.)
A:γ    &   B:α    &   R⊧[(λx:α AB) = A]       R⊧[(λx:α λy:β AB) = λy:β 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.)
RA    &   ⊤⊧[(λx:α By:α) = B]    &   ⊤⊧[(λx:α Sy:α) = S]    &   [x:α = C]⊧[A = B]    &   [x:α = C]⊧[R = S]       SB

Theoreminsti 114* Instantiate a theorem with a new term. (Contributed by Mario Carneiro, 8-Oct-2014.)
C:α    &   B:∗    &   RA    &   ⊤⊧[(λx:α By:α) = B]    &   [x:α = C]⊧[A = B]       RB

Theoremclf 115* Evaluate a lambda expression. (Contributed by Mario Carneiro, 8-Oct-2014.)
A:β    &   C:α    &   [x:α = C]⊧[A = B]    &   ⊤⊧[(λx:α By:α) = B]    &   ⊤⊧[(λx:α Cy:α) = C]       ⊤⊧[(λx:α AC) = B]

Theoremcl 116* Evaluate a lambda expression. (Contributed by Mario Carneiro, 8-Oct-2014.)
A:β    &   C:α    &   [x:α = C]⊧[A = B]       ⊤⊧[(λx:α AC) = B]

Theoremovl 117* Evaluate a lambda expression in a binary operation. (Contributed by Mario Carneiro, 8-Oct-2014.)
A:γ    &   S:α    &   T:β    &   [x:α = S]⊧[A = B]    &   [y:β = T]⊧[B = C]       ⊤⊧[[Sλx:α λy:β AT] = C]

term

Syntaxtan 119 Conjunction term.
term

Syntaxtne 120 Negation term.
term ¬

Syntaxtim 121 Implication term.
term

Syntaxtal 122 For all term.
term

Syntaxtex 123 There exists term.
term

Syntaxtor 124 Disjunction term.
term

Syntaxteu 125 There exists unique term.
term ∃!

Definitiondf-al 126* Define the for all operator. (Contributed by Mario Carneiro, 8-Oct-2014.)
⊤⊧[ = λp:(α → ∗) [p:(α → ∗) = λx:α ⊤]]

Definitiondf-fal 127 Define the constant false. (Contributed by Mario Carneiro, 8-Oct-2014.)
⊤⊧[⊥ = (λp:∗ p:∗)]

Definitiondf-an 128* Define the 'and' operator. (Contributed by Mario Carneiro, 8-Oct-2014.)
⊤⊧[ = λp:∗ λq:∗ [λf:(∗ → (∗ → ∗)) [p:∗f:(∗ → (∗ → ∗))q:∗] = λf:(∗ → (∗ → ∗)) [⊤f:(∗ → (∗ → ∗))⊤]]]

Definitiondf-im 129* Define the implication operator. (Contributed by Mario Carneiro, 8-Oct-2014.)
⊤⊧[ ⇒ = λp:∗ λq:∗ [[p:∗ q:∗] = p:∗]]

Definitiondf-not 130 Define the negation operator. (Contributed by Mario Carneiro, 8-Oct-2014.)
⊤⊧[¬ = λp:∗ [p:∗ ⇒ ⊥]]

Definitiondf-ex 131* Define the existence operator. (Contributed by Mario Carneiro, 8-Oct-2014.)
⊤⊧[ = λp:(α → ∗) (λq:∗ [(λx:α [(p:(α → ∗)x:α) ⇒ q:∗]) ⇒ q:∗])]

Definitiondf-or 132* Define the 'or' operator. (Contributed by Mario Carneiro, 8-Oct-2014.)
⊤⊧[ = λp:∗ λq:∗ (λx:∗ [[p:∗ ⇒ x:∗] ⇒ [[q:∗ ⇒ x:∗] ⇒ x:∗]])]

Definitiondf-eu 133* Define the 'exists unique' operator. (Contributed by Mario Carneiro, 8-Oct-2014.)
⊤⊧[∃! = λp:(α → ∗) (λy:α (λx:α [(p:(α → ∗)x:α) = [x:α = y:α]]))]

Theoremwal 134 For all type. (Contributed by Mario Carneiro, 8-Oct-2014.)
:((α → ∗) → ∗)

Theoremwfal 135 Contradiction type. (Contributed by Mario Carneiro, 8-Oct-2014.)
⊥:∗

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.)
:((α → ∗) → ∗)

Theoremwor 140 Disjunction type. (Contributed by Mario Carneiro, 8-Oct-2014.)
:(∗ → (∗ → ∗))

Theoremweu 141 There exists unique type. (Contributed by Mario Carneiro, 8-Oct-2014.)
∃!:((α → ∗) → ∗)

Theoremalval 142* Value of the for all predicate. (Contributed by Mario Carneiro, 8-Oct-2014.)
F:(α → ∗)       ⊤⊧[(F) = [F = λx:α ⊤]]

Theoremexval 143* Value of the 'there exists' predicate. (Contributed by Mario Carneiro, 8-Oct-2014.)
F:(α → ∗)       ⊤⊧[(F) = (λq:∗ [(λx:α [(Fx:α) ⇒ q:∗]) ⇒ q:∗])]

Theoremeuval 144* Value of the 'exists unique' predicate. (Contributed by Mario Carneiro, 8-Oct-2014.)
F:(α → ∗)       ⊤⊧[(∃!F) = (λy:α (λx:α [(Fx:α) = [x:α = y:α]]))]

Theoremnotval 145 Value of negation. (Contributed by Mario Carneiro, 8-Oct-2014.)
A:∗       ⊤⊧[(¬ A) = [A ⇒ ⊥]]

Theoremimval 146 Value of the implication. (Contributed by Mario Carneiro, 9-Oct-2014.)
A:∗    &   B:∗       ⊤⊧[[AB] = [[A B] = A]]

Theoremorval 147* Value of the disjunction. (Contributed by Mario Carneiro, 9-Oct-2014.)
A:∗    &   B:∗       ⊤⊧[[A B] = (λx:∗ [[Ax:∗] ⇒ [[Bx:∗] ⇒ x:∗]])]

Theoremanval 148* Value of the conjunction. (Contributed by Mario Carneiro, 9-Oct-2014.)
A:∗    &   B:∗       ⊤⊧[[A B] = [λf:(∗ → (∗ → ∗)) [Af:(∗ → (∗ → ∗))B] = λf:(∗ → (∗ → ∗)) [⊤f:(∗ → (∗ → ∗))⊤]]]

Theoremax4g 149 If F is true for all x:α, then it is true for A. (Contributed by Mario Carneiro, 9-Oct-2014.)
F:(α → ∗)    &   A:α       (F)⊧(FA)

Theoremax4 150 If A is true for all x:α, then it is true for A. (Contributed by Mario Carneiro, 9-Oct-2014.)
A:∗       (λx:α A)⊧A

Theoremalrimiv 151* If one can prove RA where R does not contain x, then A is true for all x. (Contributed by Mario Carneiro, 9-Oct-2014.)
RA       R⊧(λx:α A)

Theoremcla4v 152* If A(x) is true for all x:α, then it is true for C = A(B). (Contributed by Mario Carneiro, 9-Oct-2014.)
A:∗    &   B:α    &   [x:α = B]⊧[A = C]       (λx:α A)⊧C

Theorempm2.21 153 A falsehood implies anything. (Contributed by Mario Carneiro, 9-Oct-2014.)
A:∗       ⊥⊧A

Theoremdfan2 154 An alternative defintion of the "and" term in terms of the context conjunction. (Contributed by Mario Carneiro, 9-Oct-2014.)
A:∗    &   B:∗       ⊤⊧[[A B] = (A, B)]

Theoremhbct 155 Hypothesis builder for context conjunction. (Contributed by Mario Carneiro, 8-Oct-2014.)
A:∗    &   B:α    &   C:∗    &   R⊧[(λx:α AB) = A]    &   R⊧[(λx:α CB) = C]       R⊧[(λx:α (A, C)B) = (A, C)]

Theoremmpd 156 Modus ponens. (Contributed by Mario Carneiro, 9-Oct-2014.)
T:∗    &   RS    &   R⊧[ST]       RT

Theoremimp 157 Importation deduction. (Contributed by Mario Carneiro, 9-Oct-2014.)
S:∗    &   T:∗    &   R⊧[ST]       (R, S)⊧T

Theoremex 158 Exportation deduction. (Contributed by Mario Carneiro, 9-Oct-2014.)
(R, S)⊧T       R⊧[ST]

Theoremnotval2 159 Another way two write ¬ A, the negation of A. (Contributed by Mario Carneiro, 9-Oct-2014.)
A:∗       ⊤⊧[(¬ A) = [A = ⊥]]

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       RT

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:(α → ∗)    &   (R, (Fx:α))⊧T       (R, (F))⊧T

Theoremexlimdv 167* Existential elimination. (Contributed by Mario Carneiro, 9-Oct-2014.)
(R, A)⊧T       (R, (λx:α A))⊧T

Theoremax4e 168 Existential introduction. (Contributed by Mario Carneiro, 9-Oct-2014.)
F:(α → ∗)    &   A:α       (FA)⊧(F)

Theoremcla4ev 169* Existential introduction. (Contributed by Mario Carneiro, 9-Oct-2014.)
A:∗    &   B:α    &   [x:α = B]⊧[A = C]       C⊧(λx:α A)

Theorem19.8a 170 Existential introduction. (Contributed by Mario Carneiro, 9-Oct-2014.)
A:∗       A⊧(λx:α A)

0.3  Type definition mechanism

SyntaxwffMMJ2d 171 Internal axiom for mmj2 use.
wff typedef α(A, B)C

Axiomax-wabs 172 Type of the abstraction function. (New usage is discouraged.) (Contributed by Mario Carneiro, 8-Oct-2014.)
B:α    &   F:(α → ∗)    &   ⊤⊧(FB)    &   typedef β(A, R)F       A:(αβ)

Axiomax-wrep 173 Type of the representation function. (New usage is discouraged.) (Contributed by Mario Carneiro, 8-Oct-2014.)
B:α    &   F:(α → ∗)    &   ⊤⊧(FB)    &   typedef β(A, R)F       R:(βα)

Theoremwabs 174 Type of the abstraction function. (Contributed by Mario Carneiro, 8-Oct-2014.)
B:α    &   F:(α → ∗)    &   ⊤⊧(FB)    &   typedef β(A, R)F       A:(αβ)

Theoremwrep 175 Type of the representation function. (Contributed by Mario Carneiro, 8-Oct-2014.)
B:α    &   F:(α → ∗)    &   ⊤⊧(FB)    &   typedef β(A, R)F       R:(βα)

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 β and the definition will provide us with pair of bijections A, R mapping the new type β to the subset of the old type α such that Fx is true. In order for this to be a valid (conservative) extension, we must ensure that the new type is non-empty, and for that purpose we need a witness B that F is not always false. (Contributed by Mario Carneiro, 8-Oct-2014.)
B:α    &   F:(α → ∗)    &   ⊤⊧(FB)    &   typedef β(A, R)F       ⊤⊧((λx:β [(A(Rx:β)) = x:β]), (λx:α [(Fx:α) = [(R(Ax:α)) = x:α]]))

0.4  Extensionality

Axiomax-eta 177* The eta-axiom: a function is determined by its values. (Contributed by Mario Carneiro, 8-Oct-2014.)
⊤⊧(λf:(αβ) [λx:α (f:(αβ)x:α) = f:(αβ)])

Theoremeta 178* The eta-axiom: a function is determined by its values. (Contributed by Mario Carneiro, 8-Oct-2014.)
F:(αβ)       ⊤⊧[λx:α (Fx:α) = F]

Theoremcbvf 179* Change bound variables in a lambda abstraction. (Contributed by Mario Carneiro, 8-Oct-2014.)
A:β    &   ⊤⊧[(λy:α Az:α) = A]    &   ⊤⊧[(λx:α Bz:α) = B]    &   [x:α = y:α]⊧[A = B]       ⊤⊧[λx:α A = λy:α B]

Theoremcbv 180* Change bound variables in a lambda abstraction. (Contributed by Mario Carneiro, 8-Oct-2014.)
A:β    &   [x:α = y:α]⊧[A = B]       ⊤⊧[λx:α A = λy:α B]

Theoremleqf 181* Equality theorem for lambda abstraction, using bound variable instead of distinct variables. (Contributed by Mario Carneiro, 8-Oct-2014.)
A:β    &   R⊧[A = B]    &   ⊤⊧[(λx:α Ry:α) = R]       R⊧[λx:α A = λx:α B]

Theoremalrimi 182* If one can prove RA where R does not contain x, then A is true for all x. (Contributed by Mario Carneiro, 9-Oct-2014.)
RA    &   ⊤⊧[(λx:α Ry:α) = R]       R⊧(λx:α A)

Theoremexlimd 183* Existential elimination. (Contributed by Mario Carneiro, 9-Oct-2014.)
(R, A)⊧T    &   ⊤⊧[(λx:α Ry:α) = R]    &   ⊤⊧[(λx:α Ty:α) = T]       (R, (λx:α A))⊧T

Theoremalimdv 184* Deduction from Theorem 19.20 of [Margaris] p. 90. (Contributed by Mario Carneiro, 9-Oct-2014.)
(R, A)⊧B       (R, (λx:α A))⊧(λx:α B)

Theoremeximdv 185* Deduction from Theorem 19.22 of [Margaris] p. 90. (Contributed by Mario Carneiro, 9-Oct-2014.)
(R, A)⊧B       (R, (λx:α A))⊧(λx:α B)

Theoremalnex 186* Theorem 19.7 of [Margaris] p. 89. (Contributed by Mario Carneiro, 10-Oct-2014.)
A:∗       ⊤⊧[(λx:αA)) = (¬ (λx:α A))]

Theoremexnal1 187* Forward direction of exnal 201. (Contributed by Mario Carneiro, 10-Oct-2014.)
A:∗       (λx:αA))⊧(¬ (λx:α 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:∗    &   ⊤⊧[(λx:α Ay:α) = A]       ⊤⊧[A ⇒ (λx:α 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.)
ε:((α → ∗) → α)

Theoremwat 193 The type of the indefinite descriptor. (Contributed by Mario Carneiro, 10-Oct-2014.)
ε:((α → ∗) → α)

Definitiondf-f11 194* Define a one-to-one function. (Contributed by Mario Carneiro, 10-Oct-2014.)
⊤⊧[1-1 = λf:(αβ) (λx:α (λy:α [[(f:(αβ)x:α) = (f:(αβ)y:α)] ⇒ [x:α = y:α]]))]

Definitiondf-fo 195* Define an onto function. (Contributed by Mario Carneiro, 10-Oct-2014.)
⊤⊧[onto = λf:(αβ) (λy:β (λx:α [y:β = (f:(αβ)x:α)]))]

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.)
⊤⊧(λp:(α → ∗) (λx:α [(p:(α → ∗)x:α) ⇒ (p:(α → ∗)(εp:(α → ∗)))]))

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:(α → ∗)    &   A:α       (FA)⊧(FF))

Theoremdfex2 198 Alternative definition of the "there exists" quantifier. (Contributed by Mario Carneiro, 10-Oct-2014.)
F:(α → ∗)       ⊤⊧[(F) = (FF))]

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:∗       ⊤⊧[A A)]

Theoremnotnot 200 Rule of double negation. (Contributed by Mario Carneiro, 10-Oct-2014.)
A:∗       ⊤⊧[A = (¬ (¬ A))]

Page List