Theorem List for Intuitionistic Logic Explorer - 4901-5000 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Syntax | wf1o 4901 |
Extend the definition of a wff to include one-to-one onto functions.
(Read: maps one-to-one onto .) The notation
("1-1"
above the arrow and "onto" below the arrow) is from Definition
6.15(6) of
[TakeutiZaring] p. 27.
|
|
|
Syntax | cfv 4902 |
Extend the definition of a class to include the value of a function.
(Read: The value of at , or
" of .")
|
|
|
Syntax | wiso 4903 |
Extend the definition of a wff to include the isomorphism property.
(Read: is an
, isomorphism of onto .)
|
|
|
Definition | df-fun 4904 |
Define predicate that determines if some class is a function.
Definition 10.1 of [Quine] p. 65. For
example, the expression
is true (funi 4932). This is not the same as defining a
specific function's mapping, which is typically done using the format of
cmpt 3818 with the maps-to notation (see df-mpt 3820). Contrast this
predicate with the predicates to determine if some class is a function
with a given domain (df-fn 4905), a function with a given domain and
codomain (df-f 4906), a one-to-one function (df-f1 4907), an onto function
(df-fo 4908), or a one-to-one onto function (df-f1o 4909). For alternate
definitions, see dffun2 4912, dffun4 4913, dffun6 4916, dffun7 4928, dffun8 4929,
and dffun9 4930. (Contributed by NM, 1-Aug-1994.)
|
|
|
Definition | df-fn 4905 |
Define a function with domain. Definition 6.15(1) of [TakeutiZaring]
p. 27. (Contributed by NM, 1-Aug-1994.)
|
|
|
Definition | df-f 4906 |
Define a function (mapping) with domain and codomain. Definition
6.15(3) of [TakeutiZaring] p. 27.
(Contributed by NM, 1-Aug-1994.)
|
|
|
Definition | df-f1 4907 |
Define a one-to-one function. Compare Definition 6.15(5) of
[TakeutiZaring] p. 27. We use
their notation ("1-1" above the arrow).
(Contributed by NM, 1-Aug-1994.)
|
|
|
Definition | df-fo 4908 |
Define an onto function. Definition 6.15(4) of [TakeutiZaring] p. 27.
We use their notation ("onto" under the arrow). (Contributed
by NM,
1-Aug-1994.)
|
|
|
Definition | df-f1o 4909 |
Define a one-to-one onto function. Compare Definition 6.15(6) of
[TakeutiZaring] p. 27. We use
their notation ("1-1" above the arrow and
"onto" below the arrow). (Contributed by NM, 1-Aug-1994.)
|
|
|
Definition | df-fv 4910* |
Define the value of a function, , also known as function
application. For example, . Typically,
function is
defined using maps-to notation (see df-mpt 3820), but
this is not required. For example, F = { 2 , 6 ,
3 , 9 } -> ( F 3 ) = 9 . We will later define
two-argument functions using ordered pairs as
. This
particular definition is
quite convenient: it can be applied to any class and evaluates to the
empty set when it is not meaningful. The left apostrophe notation
originated with Peano and was adopted in Definition *30.01 of
[WhiteheadRussell] p. 235,
Definition 10.11 of [Quine] p. 68, and
Definition 6.11 of [TakeutiZaring]
p. 26. It means the same thing as
the more familiar notation for a function's value at ,
i.e. " of
," but without
context-dependent notational
ambiguity. (Contributed by NM, 1-Aug-1994.) Revised to use .
(Revised by Scott Fenton, 6-Oct-2017.)
|
|
|
Definition | df-isom 4911* |
Define the isomorphism predicate. We read this as " is an ,
isomorphism of
onto ." Normally, and are
ordering relations on and
respectively. Definition 6.28 of
[TakeutiZaring] p. 32, whose
notation is the same as ours except that
and are subscripts.
(Contributed by NM, 4-Mar-1997.)
|
|
|
Theorem | dffun2 4912* |
Alternate definition of a function. (Contributed by NM,
29-Dec-1996.)
|
|
|
Theorem | dffun4 4913* |
Alternate definition of a function. Definition 6.4(4) of
[TakeutiZaring] p. 24.
(Contributed by NM, 29-Dec-1996.)
|
|
|
Theorem | dffun5r 4914* |
A way of proving a relation is a function, analogous to mo2r 1952.
(Contributed by Jim Kingdon, 27-May-2020.)
|
|
|
Theorem | dffun6f 4915* |
Definition of function, using bound-variable hypotheses instead of
distinct variable conditions. (Contributed by NM, 9-Mar-1995.)
(Revised by Mario Carneiro, 15-Oct-2016.)
|
|
|
Theorem | dffun6 4916* |
Alternate definition of a function using "at most one" notation.
(Contributed by NM, 9-Mar-1995.)
|
|
|
Theorem | funmo 4917* |
A function has at most one value for each argument. (Contributed by NM,
24-May-1998.)
|
|
|
Theorem | dffun4f 4918* |
Definition of function like dffun4 4913 but using bound-variable hypotheses
instead of distinct variable conditions. (Contributed by Jim Kingdon,
17-Mar-2019.)
|
|
|
Theorem | funrel 4919 |
A function is a relation. (Contributed by NM, 1-Aug-1994.)
|
|
|
Theorem | funss 4920 |
Subclass theorem for function predicate. (Contributed by NM,
16-Aug-1994.) (Proof shortened by Mario Carneiro, 24-Jun-2014.)
|
|
|
Theorem | funeq 4921 |
Equality theorem for function predicate. (Contributed by NM,
16-Aug-1994.)
|
|
|
Theorem | funeqi 4922 |
Equality inference for the function predicate. (Contributed by Jonathan
Ben-Naim, 3-Jun-2011.)
|
|
|
Theorem | funeqd 4923 |
Equality deduction for the function predicate. (Contributed by NM,
23-Feb-2013.)
|
|
|
Theorem | nffun 4924 |
Bound-variable hypothesis builder for a function. (Contributed by NM,
30-Jan-2004.)
|
|
|
Theorem | sbcfung 4925 |
Distribute proper substitution through the function predicate.
(Contributed by Alexander van der Vekens, 23-Jul-2017.)
|
|
|
Theorem | funeu 4926* |
There is exactly one value of a function. (Contributed by NM,
22-Apr-2004.) (Proof shortened by Andrew Salmon, 17-Sep-2011.)
|
|
|
Theorem | funeu2 4927* |
There is exactly one value of a function. (Contributed by NM,
3-Aug-1994.)
|
|
|
Theorem | dffun7 4928* |
Alternate definition of a function. One possibility for the definition
of a function in [Enderton] p. 42.
(Enderton's definition is ambiguous
because "there is only one" could mean either "there is
at most one" or
"there is exactly one." However, dffun8 4929 shows that it doesn't matter
which meaning we pick.) (Contributed by NM, 4-Nov-2002.)
|
|
|
Theorem | dffun8 4929* |
Alternate definition of a function. One possibility for the definition
of a function in [Enderton] p. 42.
Compare dffun7 4928. (Contributed by
NM, 4-Nov-2002.) (Proof shortened by Andrew Salmon, 17-Sep-2011.)
|
|
|
Theorem | dffun9 4930* |
Alternate definition of a function. (Contributed by NM, 28-Mar-2007.)
(Revised by NM, 16-Jun-2017.)
|
|
|
Theorem | funfn 4931 |
An equivalence for the function predicate. (Contributed by NM,
13-Aug-2004.)
|
|
|
Theorem | funi 4932 |
The identity relation is a function. Part of Theorem 10.4 of [Quine]
p. 65. (Contributed by NM, 30-Apr-1998.)
|
|
|
Theorem | nfunv 4933 |
The universe is not a function. (Contributed by Raph Levien,
27-Jan-2004.)
|
|
|
Theorem | funopg 4934 |
A Kuratowski ordered pair is a function only if its components are
equal. (Contributed by NM, 5-Jun-2008.) (Revised by Mario Carneiro,
26-Apr-2015.)
|
|
|
Theorem | funopab 4935* |
A class of ordered pairs is a function when there is at most one second
member for each pair. (Contributed by NM, 16-May-1995.)
|
|
|
Theorem | funopabeq 4936* |
A class of ordered pairs of values is a function. (Contributed by NM,
14-Nov-1995.)
|
|
|
Theorem | funopab4 4937* |
A class of ordered pairs of values in the form used by df-mpt 3820 is a
function. (Contributed by NM, 17-Feb-2013.)
|
|
|
Theorem | funmpt 4938 |
A function in maps-to notation is a function. (Contributed by Mario
Carneiro, 13-Jan-2013.)
|
|
|
Theorem | funmpt2 4939 |
Functionality of a class given by a "maps to" notation. (Contributed
by
FL, 17-Feb-2008.) (Revised by Mario Carneiro, 31-May-2014.)
|
|
|
Theorem | funco 4940 |
The composition of two functions is a function. Exercise 29 of
[TakeutiZaring] p. 25.
(Contributed by NM, 26-Jan-1997.) (Proof
shortened by Andrew Salmon, 17-Sep-2011.)
|
|
|
Theorem | funres 4941 |
A restriction of a function is a function. Compare Exercise 18 of
[TakeutiZaring] p. 25. (Contributed
by NM, 16-Aug-1994.)
|
|
|
Theorem | funssres 4942 |
The restriction of a function to the domain of a subclass equals the
subclass. (Contributed by NM, 15-Aug-1994.)
|
|
|
Theorem | fun2ssres 4943 |
Equality of restrictions of a function and a subclass. (Contributed by
NM, 16-Aug-1994.)
|
|
|
Theorem | funun 4944 |
The union of functions with disjoint domains is a function. Theorem 4.6
of [Monk1] p. 43. (Contributed by NM,
12-Aug-1994.)
|
|
|
Theorem | funcnvsn 4945 |
The converse singleton of an ordered pair is a function. This is
equivalent to funsn 4948 via cnvsn 4803, but stating it this way allows us to
skip the sethood assumptions on and . (Contributed by NM,
30-Apr-2015.)
|
|
|
Theorem | funsng 4946 |
A singleton of an ordered pair is a function. Theorem 10.5 of [Quine]
p. 65. (Contributed by NM, 28-Jun-2011.)
|
|
|
Theorem | fnsng 4947 |
Functionality and domain of the singleton of an ordered pair.
(Contributed by Mario Carneiro, 30-Apr-2015.)
|
|
|
Theorem | funsn 4948 |
A singleton of an ordered pair is a function. Theorem 10.5 of [Quine]
p. 65. (Contributed by NM, 12-Aug-1994.)
|
|
|
Theorem | funprg 4949 |
A set of two pairs is a function if their first members are different.
(Contributed by FL, 26-Jun-2011.)
|
|
|
Theorem | funtpg 4950 |
A set of three pairs is a function if their first members are different.
(Contributed by Alexander van der Vekens, 5-Dec-2017.)
|
|
|
Theorem | funpr 4951 |
A function with a domain of two elements. (Contributed by Jeff Madsen,
20-Jun-2010.)
|
|
|
Theorem | funtp 4952 |
A function with a domain of three elements. (Contributed by NM,
14-Sep-2011.)
|
|
|
Theorem | fnsn 4953 |
Functionality and domain of the singleton of an ordered pair.
(Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
|
|
|
Theorem | fnprg 4954 |
Function with a domain of two different values. (Contributed by FL,
26-Jun-2011.) (Revised by Mario Carneiro, 26-Apr-2015.)
|
|
|
Theorem | fntpg 4955 |
Function with a domain of three different values. (Contributed by
Alexander van der Vekens, 5-Dec-2017.)
|
|
|
Theorem | fntp 4956 |
A function with a domain of three elements. (Contributed by NM,
14-Sep-2011.) (Revised by Mario Carneiro, 26-Apr-2015.)
|
|
|
Theorem | fun0 4957 |
The empty set is a function. Theorem 10.3 of [Quine] p. 65. (Contributed
by NM, 7-Apr-1998.)
|
|
|
Theorem | funcnvcnv 4958 |
The double converse of a function is a function. (Contributed by NM,
21-Sep-2004.)
|
|
|
Theorem | funcnv2 4959* |
A simpler equivalence for single-rooted (see funcnv 4960). (Contributed
by NM, 9-Aug-2004.)
|
|
|
Theorem | funcnv 4960* |
The converse of a class is a function iff the class is single-rooted,
which means that for any in the range of there is at most
one such that
. Definition of single-rooted in
[Enderton] p. 43. See funcnv2 4959 for a simpler version. (Contributed by
NM, 13-Aug-2004.)
|
|
|
Theorem | funcnv3 4961* |
A condition showing a class is single-rooted. (See funcnv 4960).
(Contributed by NM, 26-May-2006.)
|
|
|
Theorem | funcnveq 4962* |
Another way of expressing that a class is single-rooted. Counterpart to
dffun2 4912. (Contributed by Jim Kingdon, 24-Dec-2018.)
|
|
|
Theorem | fun2cnv 4963* |
The double converse of a class is a function iff the class is
single-valued. Each side is equivalent to Definition 6.4(2) of
[TakeutiZaring] p. 23, who use the
notation "Un(A)" for single-valued.
Note that is
not necessarily a function. (Contributed by NM,
13-Aug-2004.)
|
|
|
Theorem | svrelfun 4964 |
A single-valued relation is a function. (See fun2cnv 4963 for
"single-valued.") Definition 6.4(4) of [TakeutiZaring] p. 24.
(Contributed by NM, 17-Jan-2006.)
|
|
|
Theorem | fncnv 4965* |
Single-rootedness (see funcnv 4960) of a class cut down by a cross
product. (Contributed by NM, 5-Mar-2007.)
|
|
|
Theorem | fun11 4966* |
Two ways of stating that is one-to-one (but not necessarily a
function). Each side is equivalent to Definition 6.4(3) of
[TakeutiZaring] p. 24, who use the
notation "Un2 (A)" for one-to-one
(but not necessarily a function). (Contributed by NM, 17-Jan-2006.)
|
|
|
Theorem | fununi 4967* |
The union of a chain (with respect to inclusion) of functions is a
function. (Contributed by NM, 10-Aug-2004.)
|
|
|
Theorem | funcnvuni 4968* |
The union of a chain (with respect to inclusion) of single-rooted sets
is single-rooted. (See funcnv 4960 for "single-rooted"
definition.)
(Contributed by NM, 11-Aug-2004.)
|
|
|
Theorem | fun11uni 4969* |
The union of a chain (with respect to inclusion) of one-to-one functions
is a one-to-one function. (Contributed by NM, 11-Aug-2004.)
|
|
|
Theorem | funin 4970 |
The intersection with a function is a function. Exercise 14(a) of
[Enderton] p. 53. (Contributed by NM,
19-Mar-2004.) (Proof shortened
by Andrew Salmon, 17-Sep-2011.)
|
|
|
Theorem | funres11 4971 |
The restriction of a one-to-one function is one-to-one. (Contributed by
NM, 25-Mar-1998.)
|
|
|
Theorem | funcnvres 4972 |
The converse of a restricted function. (Contributed by NM,
27-Mar-1998.)
|
|
|
Theorem | cnvresid 4973 |
Converse of a restricted identity function. (Contributed by FL,
4-Mar-2007.)
|
|
|
Theorem | funcnvres2 4974 |
The converse of a restriction of the converse of a function equals the
function restricted to the image of its converse. (Contributed by NM,
4-May-2005.)
|
|
|
Theorem | funimacnv 4975 |
The image of the preimage of a function. (Contributed by NM,
25-May-2004.)
|
|
|
Theorem | funimass1 4976 |
A kind of contraposition law that infers a subclass of an image from a
preimage subclass. (Contributed by NM, 25-May-2004.)
|
|
|
Theorem | funimass2 4977 |
A kind of contraposition law that infers an image subclass from a subclass
of a preimage. (Contributed by NM, 25-May-2004.)
|
|
|
Theorem | imadiflem 4978 |
One direction of imadif 4979. This direction does not require
. (Contributed by Jim Kingdon,
25-Dec-2018.)
|
|
|
Theorem | imadif 4979 |
The image of a difference is the difference of images. (Contributed by
NM, 24-May-1998.)
|
|
|
Theorem | imainlem 4980 |
One direction of imain 4981. This direction does not require
. (Contributed by Jim Kingdon,
25-Dec-2018.)
|
|
|
Theorem | imain 4981 |
The image of an intersection is the intersection of images.
(Contributed by Paul Chapman, 11-Apr-2009.)
|
|
|
Theorem | funimaexglem 4982 |
Lemma for funimaexg 4983. It constitutes the interesting part of
funimaexg 4983, in which
. (Contributed by Jim
Kingdon,
27-Dec-2018.)
|
|
|
Theorem | funimaexg 4983 |
Axiom of Replacement using abbreviations. Axiom 39(vi) of [Quine] p. 284.
Compare Exercise 9 of [TakeutiZaring] p. 29. (Contributed by NM,
10-Sep-2006.)
|
|
|
Theorem | funimaex 4984 |
The image of a set under any function is also a set. Equivalent of
Axiom of Replacement. Axiom 39(vi) of [Quine] p. 284. Compare Exercise
9 of [TakeutiZaring] p. 29.
(Contributed by NM, 17-Nov-2002.)
|
|
|
Theorem | isarep1 4985* |
Part of a study of the Axiom of Replacement used by the Isabelle prover.
The object PrimReplace is apparently the image of the function encoded
by i.e. the class .
If so, we can prove Isabelle's "Axiom of Replacement"
conclusion without
using the Axiom of Replacement, for which I (N. Megill) currently have
no explanation. (Contributed by NM, 26-Oct-2006.) (Proof shortened by
Mario Carneiro, 4-Dec-2016.)
|
|
|
Theorem | isarep2 4986* |
Part of a study of the Axiom of Replacement used by the Isabelle prover.
In Isabelle, the sethood of PrimReplace is apparently postulated
implicitly by its type signature " i, i, i
=> o
=> i", which automatically asserts that it is a set without
using any
axioms. To prove that it is a set in Metamath, we need the hypotheses
of Isabelle's "Axiom of Replacement" as well as the Axiom of
Replacement
in the form funimaex 4984. (Contributed by NM, 26-Oct-2006.)
|
|
|
Theorem | fneq1 4987 |
Equality theorem for function predicate with domain. (Contributed by NM,
1-Aug-1994.)
|
|
|
Theorem | fneq2 4988 |
Equality theorem for function predicate with domain. (Contributed by NM,
1-Aug-1994.)
|
|
|
Theorem | fneq1d 4989 |
Equality deduction for function predicate with domain. (Contributed by
Paul Chapman, 22-Jun-2011.)
|
|
|
Theorem | fneq2d 4990 |
Equality deduction for function predicate with domain. (Contributed by
Paul Chapman, 22-Jun-2011.)
|
|
|
Theorem | fneq12d 4991 |
Equality deduction for function predicate with domain. (Contributed by
NM, 26-Jun-2011.)
|
|
|
Theorem | fneq12 4992 |
Equality theorem for function predicate with domain. (Contributed by
Thierry Arnoux, 31-Jan-2017.)
|
|
|
Theorem | fneq1i 4993 |
Equality inference for function predicate with domain. (Contributed by
Paul Chapman, 22-Jun-2011.)
|
|
|
Theorem | fneq2i 4994 |
Equality inference for function predicate with domain. (Contributed by
NM, 4-Sep-2011.)
|
|
|
Theorem | nffn 4995 |
Bound-variable hypothesis builder for a function with domain.
(Contributed by NM, 30-Jan-2004.)
|
|
|
Theorem | fnfun 4996 |
A function with domain is a function. (Contributed by NM, 1-Aug-1994.)
|
|
|
Theorem | fnrel 4997 |
A function with domain is a relation. (Contributed by NM, 1-Aug-1994.)
|
|
|
Theorem | fndm 4998 |
The domain of a function. (Contributed by NM, 2-Aug-1994.)
|
|
|
Theorem | funfni 4999 |
Inference to convert a function and domain antecedent. (Contributed by
NM, 22-Apr-2004.)
|
|
|
Theorem | fndmu 5000 |
A function has a unique domain. (Contributed by NM, 11-Aug-1994.)
|
|