P. 2 of Theorem List - Higher-Order Logic Explorer

Theorem List for Higher-Order Logic Explorer - 101-200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	oveq2 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]]
Theorem	oveq 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]]
Axiom	ax-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]
Theorem	hbl1 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]
Axiom	ax-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]
Theorem	a17i 106*	Inference form of ax-17 105. (Contributed by Mario Carneiro, 8-Oct-2014.)
|- A:be   &   |- B:al   &   |- R:*   =>   |- R |= [(\x:al AB) = A]
Theorem	hbxfrf 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]
Theorem	hbxfr 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]
Theorem	hbth 109*	Hypothesis builder for a theorem. (Contributed by Mario Carneiro, 8-Oct-2014.)
|- B:al   &   |- R |= A   =>   |- R |= [(\x:al AB) = A]
Theorem	hbc 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)]
Theorem	hbov 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]]
Theorem	hbl 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]
Axiom	ax-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
Theorem	insti 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
Theorem	clf 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]
Theorem	cl 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]
Theorem	ovl 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
Syntax	tfal 118	Contradiction term.
term F.
Syntax	tan 119	Conjunction term.
term /\
Syntax	tne 120	Negation term.
term ~
Syntax	tim 121	Implication term.
term ==>
Syntax	tal 122	For all term.
term A.
Syntax	tex 123	There exists term.
term E.
Syntax	tor 124	Disjunction term.
term \/
Syntax	teu 125	There exists unique term.
term E!
Definition	df-al 126*	Define the for all operator. (Contributed by Mario Carneiro, 8-Oct-2014.)
|- T. |= [A. = \p:(al -> *) [p:(al -> *) = \x:al T.]]
Definition	df-fal 127	Define the constant false. (Contributed by Mario Carneiro, 8-Oct-2014.)
|- T. |= [F. = (A.\p:* p:*)]
Definition	df-an 128*	Define the 'and' operator. (Contributed by Mario Carneiro, 8-Oct-2014.)
|- T. |= [ /\ = \p:* \q:* [\f:(* -> (* -> *)) [p:*f:(* -> (* -> *))q:*] = \f:(* -> (* -> *)) [T.f:(* -> (* -> *))T.]]]
Definition	df-im 129*	Define the implication operator. (Contributed by Mario Carneiro, 8-Oct-2014.)
|- T. |= [ ==> = \p:* \q:* [[p:* /\ q:*] = p:*]]
Definition	df-not 130	Define the negation operator. (Contributed by Mario Carneiro, 8-Oct-2014.)
|- T. |= [~ = \p:* [p:* ==> F.]]
Definition	df-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:*])]
Definition	df-or 132*	Define the 'or' operator. (Contributed by Mario Carneiro, 8-Oct-2014.)
|- T. |= [ \/ = \p:* \q:* (A.\x:* [[p:* ==> x:*] ==> [[q:* ==> x:*] ==> x:*]])]
Definition	df-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]]))]
Theorem	wal 134	For all type. (Contributed by Mario Carneiro, 8-Oct-2014.)
|- A.:((al -> *) -> *)
Theorem	wfal 135	Contradiction type. (Contributed by Mario Carneiro, 8-Oct-2014.)
|- F.:*
Theorem	wan 136	Conjunction type. (Contributed by Mario Carneiro, 8-Oct-2014.)
|- /\ :(* -> (* -> *))
Theorem	wim 137	Implication type. (Contributed by Mario Carneiro, 8-Oct-2014.)
|- ==> :(* -> (* -> *))
Theorem	wnot 138	Negation type. (Contributed by Mario Carneiro, 8-Oct-2014.)
|- ~ :(* -> *)
Theorem	wex 139	There exists type. (Contributed by Mario Carneiro, 8-Oct-2014.)
|- E.:((al -> *) -> *)
Theorem	wor 140	Disjunction type. (Contributed by Mario Carneiro, 8-Oct-2014.)
|- \/ :(* -> (* -> *))
Theorem	weu 141	There exists unique type. (Contributed by Mario Carneiro, 8-Oct-2014.)
|- E!:((al -> *) -> *)
Theorem	alval 142*	Value of the for all predicate. (Contributed by Mario Carneiro, 8-Oct-2014.)
|- F:(al -> *)   =>   |- T. |= [(A.F) = [F = \x:al T.]]
Theorem	exval 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:*])]
Theorem	euval 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]]))]
Theorem	notval 145	Value of negation. (Contributed by Mario Carneiro, 8-Oct-2014.)
|- A:*   =>   |- T. |= [(~ A) = [A ==> F.]]
Theorem	imval 146	Value of the implication. (Contributed by Mario Carneiro, 9-Oct-2014.)
|- A:*   &   |- B:*   =>   |- T. |= [[A ==> B] = [[A /\ B] = A]]
Theorem	orval 147*	Value of the disjunction. (Contributed by Mario Carneiro, 9-Oct-2014.)
|- A:*   &   |- B:*   =>   |- T. |= [[A \/ B] = (A.\x:* [[A ==> x:*] ==> [[B ==> x:*] ==> x:*]])]
Theorem	anval 148*	Value of the conjunction. (Contributed by Mario Carneiro, 9-Oct-2014.)
|- A:*   &   |- B:*   =>   |- T. |= [[A /\ B] = [\f:(* -> (* -> *)) [Af:(* -> (* -> *))B] = \f:(* -> (* -> *)) [T.f:(* -> (* -> *))T.]]]
Theorem	ax4g 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)
Theorem	ax4 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
Theorem	alrimiv 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)
Theorem	cla4v 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
Theorem	pm2.21 153	A falsehood implies anything. (Contributed by Mario Carneiro, 9-Oct-2014.)
|- A:*   =>   |- F. |= A
Theorem	dfan2 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)]
Theorem	hbct 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)]
Theorem	mpd 156	Modus ponens. (Contributed by Mario Carneiro, 9-Oct-2014.)
|- T:*   &   |- R |= S   &   |- R |= [S ==> T]   =>   |- R |= T
Theorem	imp 157	Importation deduction. (Contributed by Mario Carneiro, 9-Oct-2014.)
|- S:*   &   |- T:*   &   |- R |= [S ==> T]   =>   |- (R, S) |= T
Theorem	ex 158	Exportation deduction. (Contributed by Mario Carneiro, 9-Oct-2014.)
|- (R, S) |= T   =>   |- R |= [S ==> T]
Theorem	notval2 159	Another way two write ~ A, the negation of A. (Contributed by Mario Carneiro, 9-Oct-2014.)
|- A:*   =>   |- T. |= [(~ A) = [A = F.]]
Theorem	notnot1 160	One side of notnot 200. (Contributed by Mario Carneiro, 10-Oct-2014.)
|- A:*   =>   |- A |= (~ (~ A))
Theorem	con2d 161	A contraposition deduction. (Contributed by Mario Carneiro, 10-Oct-2014.)
|- T:*   &   |- (R, S) |= (~ T)   =>   |- (R, T) |= (~ S)
Theorem	con3d 162	A contraposition deduction. (Contributed by Mario Carneiro, 10-Oct-2014.)
|- (R, S) |= T   =>   |- (R, (~ T)) |= (~ S)
Theorem	ecase 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
Theorem	olc 164	Or introduction. (Contributed by Mario Carneiro, 9-Oct-2014.)
|- A:*   &   |- B:*   =>   |- B |= [A \/ B]
Theorem	orc 165	Or introduction. (Contributed by Mario Carneiro, 9-Oct-2014.)
|- A:*   &   |- B:*   =>   |- A |= [A \/ B]
Theorem	exlimdv2 166*	Existential elimination. (Contributed by Mario Carneiro, 9-Oct-2014.)
|- F:(al -> *)   &   |- (R, (Fx:al)) |= T   =>   |- (R, (E.F)) |= T
Theorem	exlimdv 167*	Existential elimination. (Contributed by Mario Carneiro, 9-Oct-2014.)
|- (R, A) |= T   =>   |- (R, (E.\x:al A)) |= T
Theorem	ax4e 168	Existential introduction. (Contributed by Mario Carneiro, 9-Oct-2014.)
|- F:(al -> *)   &   |- A:al   =>   |- (FA) |= (E.F)
Theorem	cla4ev 169*	Existential introduction. (Contributed by Mario Carneiro, 9-Oct-2014.)
|- A:*   &   |- B:al   &   |- [x:al = B] |= [A = C]   =>   |- C |= (E.\x:al A)
Theorem	19.8a 170	Existential introduction. (Contributed by Mario Carneiro, 9-Oct-2014.)
|- A:*   =>   |- A |= (E.\x:al A)
0.3  Type definition mechanism
Syntax	wffMMJ2d 171	Internal axiom for mmj2 use.
wff typedef al(A, B)C
Axiom	ax-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)
Axiom	ax-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)
Theorem	wabs 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)
Theorem	wrep 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)
Axiom	ax-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
Axiom	ax-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)])
Theorem	eta 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]
Theorem	cbvf 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]
Theorem	cbv 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]
Theorem	leqf 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]
Theorem	alrimi 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)
Theorem	exlimd 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
Theorem	alimdv 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)
Theorem	eximdv 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)
Theorem	alnex 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))]
Theorem	exnal1 187*	Forward direction of exnal 201. (Contributed by Mario Carneiro, 10-Oct-2014.)
|- A:*   =>   |- (E.\x:al (~ A)) |= (~ (A.\x:al A))
Theorem	isfree 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
Syntax	tf11 189	One-to-one function.
term 1-1
Syntax	tfo 190	Onto function.
term onto
Syntax	tat 191	Indefinite descriptor.
term @
Axiom	ax-wat 192	The type of the indefinite descriptor. (New usage is discouraged.) (Contributed by Mario Carneiro, 10-Oct-2014.)
|- @:((al -> *) -> al)
Theorem	wat 193	The type of the indefinite descriptor. (Contributed by Mario Carneiro, 10-Oct-2014.)
|- @:((al -> *) -> al)
Definition	df-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]]))]
Definition	df-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)]))]
Axiom	ax-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 -> *)))]))
Theorem	ac 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))
Theorem	dfex2 198	Alternative definition of the "there exists" quantifier. (Contributed by Mario Carneiro, 10-Oct-2014.)
|- F:(al -> *)   =>   |- T. |= [(E.F) = (F(@F))]
Theorem	exmid 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)]
Theorem	notnot 200	Rule of double negation. (Contributed by Mario Carneiro, 10-Oct-2014.)
|- A:*   =>   |- T. |= [A = (~ (~ A))]