Theorem List for Intuitionistic Logic Explorer - 5601-5700 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | fvmptdv2 5601* |
Alternate deduction version of fvmpt 5589, suitable for iteration.
(Contributed by Mario Carneiro, 7-Jan-2017.)
|
⊢ (𝜑 → 𝐴 ∈ 𝐷)
& ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐵 ∈ 𝑉)
& ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → (𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵) → (𝐹‘𝐴) = 𝐶)) |
|
Theorem | mpteqb 5602* |
Bidirectional equality theorem for a mapping abstraction. Equivalent to
eqfnfv 5609. (Contributed by Mario Carneiro,
14-Nov-2014.)
|
⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → ((𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶) ↔ ∀𝑥 ∈ 𝐴 𝐵 = 𝐶)) |
|
Theorem | fvmptt 5603* |
Closed theorem form of fvmpt 5589. (Contributed by Scott Fenton,
21-Feb-2013.) (Revised by Mario Carneiro, 11-Sep-2015.)
|
⊢ ((∀𝑥(𝑥 = 𝐴 → 𝐵 = 𝐶) ∧ 𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵) ∧ (𝐴 ∈ 𝐷 ∧ 𝐶 ∈ 𝑉)) → (𝐹‘𝐴) = 𝐶) |
|
Theorem | fvmptf 5604* |
Value of a function given by an ordered-pair class abstraction. This
version of fvmptg 5588 uses bound-variable hypotheses instead of
distinct
variable conditions. (Contributed by NM, 8-Nov-2005.) (Revised by
Mario Carneiro, 15-Oct-2016.)
|
⊢ Ⅎ𝑥𝐴
& ⊢ Ⅎ𝑥𝐶
& ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶)
& ⊢ 𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵) ⇒ ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐶 ∈ 𝑉) → (𝐹‘𝐴) = 𝐶) |
|
Theorem | fvmptd3 5605* |
Deduction version of fvmpt 5589. (Contributed by Glauco Siliprandi,
23-Oct-2021.)
|
⊢ 𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵)
& ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶)
& ⊢ (𝜑 → 𝐴 ∈ 𝐷)
& ⊢ (𝜑 → 𝐶 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝐹‘𝐴) = 𝐶) |
|
Theorem | elfvmptrab1 5606* |
Implications for the value of a function defined by the maps-to notation
with a class abstraction as a result having an element. Here, the base
set of the class abstraction depends on the argument of the function.
(Contributed by Alexander van der Vekens, 15-Jul-2018.)
|
⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ {𝑦 ∈ ⦋𝑥 / 𝑚⦌𝑀 ∣ 𝜑}) & ⊢ (𝑋 ∈ 𝑉 → ⦋𝑋 / 𝑚⦌𝑀 ∈ V) ⇒ ⊢ (𝑌 ∈ (𝐹‘𝑋) → (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ ⦋𝑋 / 𝑚⦌𝑀)) |
|
Theorem | elfvmptrab 5607* |
Implications for the value of a function defined by the maps-to notation
with a class abstraction as a result having an element. (Contributed by
Alexander van der Vekens, 15-Jul-2018.)
|
⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ {𝑦 ∈ 𝑀 ∣ 𝜑}) & ⊢ (𝑋 ∈ 𝑉 → 𝑀 ∈ V) ⇒ ⊢ (𝑌 ∈ (𝐹‘𝑋) → (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑀)) |
|
Theorem | fvopab6 5608* |
Value of a function given by ordered-pair class abstraction.
(Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro,
11-Sep-2015.)
|
⊢ 𝐹 = {〈𝑥, 𝑦〉 ∣ (𝜑 ∧ 𝑦 = 𝐵)} & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶) ⇒ ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐶 ∈ 𝑅 ∧ 𝜓) → (𝐹‘𝐴) = 𝐶) |
|
Theorem | eqfnfv 5609* |
Equality of functions is determined by their values. Special case of
Exercise 4 of [TakeutiZaring] p.
28 (with domain equality omitted).
(Contributed by NM, 3-Aug-1994.) (Proof shortened by Andrew Salmon,
22-Oct-2011.) (Proof shortened by Mario Carneiro, 31-Aug-2015.)
|
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → (𝐹 = 𝐺 ↔ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘𝑥))) |
|
Theorem | eqfnfv2 5610* |
Equality of functions is determined by their values. Exercise 4 of
[TakeutiZaring] p. 28.
(Contributed by NM, 3-Aug-1994.) (Revised by
Mario Carneiro, 31-Aug-2015.)
|
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵) → (𝐹 = 𝐺 ↔ (𝐴 = 𝐵 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘𝑥)))) |
|
Theorem | eqfnfv3 5611* |
Derive equality of functions from equality of their values.
(Contributed by Jeff Madsen, 2-Sep-2009.)
|
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵) → (𝐹 = 𝐺 ↔ (𝐵 ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ 𝐵 ∧ (𝐹‘𝑥) = (𝐺‘𝑥))))) |
|
Theorem | eqfnfvd 5612* |
Deduction for equality of functions. (Contributed by Mario Carneiro,
24-Jul-2014.)
|
⊢ (𝜑 → 𝐹 Fn 𝐴)
& ⊢ (𝜑 → 𝐺 Fn 𝐴)
& ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = (𝐺‘𝑥)) ⇒ ⊢ (𝜑 → 𝐹 = 𝐺) |
|
Theorem | eqfnfv2f 5613* |
Equality of functions is determined by their values. Special case of
Exercise 4 of [TakeutiZaring] p.
28 (with domain equality omitted).
This version of eqfnfv 5609 uses bound-variable hypotheses instead of
distinct variable conditions. (Contributed by NM, 29-Jan-2004.)
|
⊢ Ⅎ𝑥𝐹
& ⊢ Ⅎ𝑥𝐺 ⇒ ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → (𝐹 = 𝐺 ↔ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘𝑥))) |
|
Theorem | eqfunfv 5614* |
Equality of functions is determined by their values. (Contributed by
Scott Fenton, 19-Jun-2011.)
|
⊢ ((Fun 𝐹 ∧ Fun 𝐺) → (𝐹 = 𝐺 ↔ (dom 𝐹 = dom 𝐺 ∧ ∀𝑥 ∈ dom 𝐹(𝐹‘𝑥) = (𝐺‘𝑥)))) |
|
Theorem | fvreseq 5615* |
Equality of restricted functions is determined by their values.
(Contributed by NM, 3-Aug-1994.)
|
⊢ (((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) ∧ 𝐵 ⊆ 𝐴) → ((𝐹 ↾ 𝐵) = (𝐺 ↾ 𝐵) ↔ ∀𝑥 ∈ 𝐵 (𝐹‘𝑥) = (𝐺‘𝑥))) |
|
Theorem | fnmptfvd 5616* |
A function with a given domain is a mapping defined by its function
values. (Contributed by AV, 1-Mar-2019.)
|
⊢ (𝜑 → 𝑀 Fn 𝐴)
& ⊢ (𝑖 = 𝑎 → 𝐷 = 𝐶)
& ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴) → 𝐷 ∈ 𝑈)
& ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → 𝐶 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝑀 = (𝑎 ∈ 𝐴 ↦ 𝐶) ↔ ∀𝑖 ∈ 𝐴 (𝑀‘𝑖) = 𝐷)) |
|
Theorem | fndmdif 5617* |
Two ways to express the locus of differences between two functions.
(Contributed by Stefan O'Rear, 17-Jan-2015.)
|
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → dom (𝐹 ∖ 𝐺) = {𝑥 ∈ 𝐴 ∣ (𝐹‘𝑥) ≠ (𝐺‘𝑥)}) |
|
Theorem | fndmdifcom 5618 |
The difference set between two functions is commutative. (Contributed
by Stefan O'Rear, 17-Jan-2015.)
|
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → dom (𝐹 ∖ 𝐺) = dom (𝐺 ∖ 𝐹)) |
|
Theorem | fndmin 5619* |
Two ways to express the locus of equality between two functions.
(Contributed by Stefan O'Rear, 17-Jan-2015.)
|
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → dom (𝐹 ∩ 𝐺) = {𝑥 ∈ 𝐴 ∣ (𝐹‘𝑥) = (𝐺‘𝑥)}) |
|
Theorem | fneqeql 5620 |
Two functions are equal iff their equalizer is the whole domain.
(Contributed by Stefan O'Rear, 7-Mar-2015.)
|
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → (𝐹 = 𝐺 ↔ dom (𝐹 ∩ 𝐺) = 𝐴)) |
|
Theorem | fneqeql2 5621 |
Two functions are equal iff their equalizer contains the whole domain.
(Contributed by Stefan O'Rear, 9-Mar-2015.)
|
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → (𝐹 = 𝐺 ↔ 𝐴 ⊆ dom (𝐹 ∩ 𝐺))) |
|
Theorem | fnreseql 5622 |
Two functions are equal on a subset iff their equalizer contains that
subset. (Contributed by Stefan O'Rear, 7-Mar-2015.)
|
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ∧ 𝑋 ⊆ 𝐴) → ((𝐹 ↾ 𝑋) = (𝐺 ↾ 𝑋) ↔ 𝑋 ⊆ dom (𝐹 ∩ 𝐺))) |
|
Theorem | chfnrn 5623* |
The range of a choice function (a function that chooses an element from
each member of its domain) is included in the union of its domain.
(Contributed by NM, 31-Aug-1999.)
|
⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝑥) → ran 𝐹 ⊆ ∪ 𝐴) |
|
Theorem | funfvop 5624 |
Ordered pair with function value. Part of Theorem 4.3(i) of [Monk1]
p. 41. (Contributed by NM, 14-Oct-1996.)
|
⊢ ((Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹) → 〈𝐴, (𝐹‘𝐴)〉 ∈ 𝐹) |
|
Theorem | funfvbrb 5625 |
Two ways to say that 𝐴 is in the domain of 𝐹.
(Contributed by
Mario Carneiro, 1-May-2014.)
|
⊢ (Fun 𝐹 → (𝐴 ∈ dom 𝐹 ↔ 𝐴𝐹(𝐹‘𝐴))) |
|
Theorem | fvimacnvi 5626 |
A member of a preimage is a function value argument. (Contributed by NM,
4-May-2007.)
|
⊢ ((Fun 𝐹 ∧ 𝐴 ∈ (◡𝐹 “ 𝐵)) → (𝐹‘𝐴) ∈ 𝐵) |
|
Theorem | fvimacnv 5627 |
The argument of a function value belongs to the preimage of any class
containing the function value. Raph Levien remarks: "This proof is
unsatisfying, because it seems to me that funimass2 5290 could probably be
strengthened to a biconditional." (Contributed by Raph Levien,
20-Nov-2006.)
|
⊢ ((Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹) → ((𝐹‘𝐴) ∈ 𝐵 ↔ 𝐴 ∈ (◡𝐹 “ 𝐵))) |
|
Theorem | funimass3 5628 |
A kind of contraposition law that infers an image subclass from a
subclass of a preimage. Raph Levien remarks: "Likely this could
be
proved directly, and fvimacnv 5627 would be the special case of 𝐴 being
a singleton, but it works this way round too." (Contributed by
Raph
Levien, 20-Nov-2006.)
|
⊢ ((Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹) → ((𝐹 “ 𝐴) ⊆ 𝐵 ↔ 𝐴 ⊆ (◡𝐹 “ 𝐵))) |
|
Theorem | funimass5 5629* |
A subclass of a preimage in terms of function values. (Contributed by
NM, 15-May-2007.)
|
⊢ ((Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹) → (𝐴 ⊆ (◡𝐹 “ 𝐵) ↔ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵)) |
|
Theorem | funconstss 5630* |
Two ways of specifying that a function is constant on a subdomain.
(Contributed by NM, 8-Mar-2007.)
|
⊢ ((Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹) → (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵 ↔ 𝐴 ⊆ (◡𝐹 “ {𝐵}))) |
|
Theorem | elpreima 5631 |
Membership in the preimage of a set under a function. (Contributed by
Jeff Madsen, 2-Sep-2009.)
|
⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) ↔ (𝐵 ∈ 𝐴 ∧ (𝐹‘𝐵) ∈ 𝐶))) |
|
Theorem | fniniseg 5632 |
Membership in the preimage of a singleton, under a function. (Contributed
by Mario Carneiro, 12-May-2014.) (Proof shortened by Mario Carneiro,
28-Apr-2015.)
|
⊢ (𝐹 Fn 𝐴 → (𝐶 ∈ (◡𝐹 “ {𝐵}) ↔ (𝐶 ∈ 𝐴 ∧ (𝐹‘𝐶) = 𝐵))) |
|
Theorem | fncnvima2 5633* |
Inverse images under functions expressed as abstractions. (Contributed
by Stefan O'Rear, 1-Feb-2015.)
|
⊢ (𝐹 Fn 𝐴 → (◡𝐹 “ 𝐵) = {𝑥 ∈ 𝐴 ∣ (𝐹‘𝑥) ∈ 𝐵}) |
|
Theorem | fniniseg2 5634* |
Inverse point images under functions expressed as abstractions.
(Contributed by Stefan O'Rear, 1-Feb-2015.)
|
⊢ (𝐹 Fn 𝐴 → (◡𝐹 “ {𝐵}) = {𝑥 ∈ 𝐴 ∣ (𝐹‘𝑥) = 𝐵}) |
|
Theorem | fnniniseg2 5635* |
Support sets of functions expressed as abstractions. (Contributed by
Stefan O'Rear, 1-Feb-2015.)
|
⊢ (𝐹 Fn 𝐴 → (◡𝐹 “ (V ∖ {𝐵})) = {𝑥 ∈ 𝐴 ∣ (𝐹‘𝑥) ≠ 𝐵}) |
|
Theorem | rexsupp 5636* |
Existential quantification restricted to a support. (Contributed by
Stefan O'Rear, 23-Mar-2015.)
|
⊢ (𝐹 Fn 𝐴 → (∃𝑥 ∈ (◡𝐹 “ (V ∖ {𝑍}))𝜑 ↔ ∃𝑥 ∈ 𝐴 ((𝐹‘𝑥) ≠ 𝑍 ∧ 𝜑))) |
|
Theorem | unpreima 5637 |
Preimage of a union. (Contributed by Jeff Madsen, 2-Sep-2009.)
|
⊢ (Fun 𝐹 → (◡𝐹 “ (𝐴 ∪ 𝐵)) = ((◡𝐹 “ 𝐴) ∪ (◡𝐹 “ 𝐵))) |
|
Theorem | inpreima 5638 |
Preimage of an intersection. (Contributed by Jeff Madsen, 2-Sep-2009.)
(Proof shortened by Mario Carneiro, 14-Jun-2016.)
|
⊢ (Fun 𝐹 → (◡𝐹 “ (𝐴 ∩ 𝐵)) = ((◡𝐹 “ 𝐴) ∩ (◡𝐹 “ 𝐵))) |
|
Theorem | difpreima 5639 |
Preimage of a difference. (Contributed by Mario Carneiro,
14-Jun-2016.)
|
⊢ (Fun 𝐹 → (◡𝐹 “ (𝐴 ∖ 𝐵)) = ((◡𝐹 “ 𝐴) ∖ (◡𝐹 “ 𝐵))) |
|
Theorem | respreima 5640 |
The preimage of a restricted function. (Contributed by Jeff Madsen,
2-Sep-2009.)
|
⊢ (Fun 𝐹 → (◡(𝐹 ↾ 𝐵) “ 𝐴) = ((◡𝐹 “ 𝐴) ∩ 𝐵)) |
|
Theorem | fimacnv 5641 |
The preimage of the codomain of a mapping is the mapping's domain.
(Contributed by FL, 25-Jan-2007.)
|
⊢ (𝐹:𝐴⟶𝐵 → (◡𝐹 “ 𝐵) = 𝐴) |
|
Theorem | fnopfv 5642 |
Ordered pair with function value. Part of Theorem 4.3(i) of [Monk1]
p. 41. (Contributed by NM, 30-Sep-2004.)
|
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → 〈𝐵, (𝐹‘𝐵)〉 ∈ 𝐹) |
|
Theorem | fvelrn 5643 |
A function's value belongs to its range. (Contributed by NM,
14-Oct-1996.)
|
⊢ ((Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹) → (𝐹‘𝐴) ∈ ran 𝐹) |
|
Theorem | fnfvelrn 5644 |
A function's value belongs to its range. (Contributed by NM,
15-Oct-1996.)
|
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → (𝐹‘𝐵) ∈ ran 𝐹) |
|
Theorem | ffvelcdm 5645 |
A function's value belongs to its codomain. (Contributed by NM,
12-Aug-1999.)
|
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) ∈ 𝐵) |
|
Theorem | ffvelcdmi 5646 |
A function's value belongs to its codomain. (Contributed by NM,
6-Apr-2005.)
|
⊢ 𝐹:𝐴⟶𝐵 ⇒ ⊢ (𝐶 ∈ 𝐴 → (𝐹‘𝐶) ∈ 𝐵) |
|
Theorem | ffvelcdmda 5647 |
A function's value belongs to its codomain. (Contributed by Mario
Carneiro, 29-Dec-2016.)
|
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) ⇒ ⊢ ((𝜑 ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) ∈ 𝐵) |
|
Theorem | ffvelcdmd 5648 |
A function's value belongs to its codomain. (Contributed by Mario
Carneiro, 29-Dec-2016.)
|
⊢ (𝜑 → 𝐹:𝐴⟶𝐵)
& ⊢ (𝜑 → 𝐶 ∈ 𝐴) ⇒ ⊢ (𝜑 → (𝐹‘𝐶) ∈ 𝐵) |
|
Theorem | rexrn 5649* |
Restricted existential quantification over the range of a function.
(Contributed by Mario Carneiro, 24-Dec-2013.) (Revised by Mario
Carneiro, 20-Aug-2014.)
|
⊢ (𝑥 = (𝐹‘𝑦) → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐹 Fn 𝐴 → (∃𝑥 ∈ ran 𝐹𝜑 ↔ ∃𝑦 ∈ 𝐴 𝜓)) |
|
Theorem | ralrn 5650* |
Restricted universal quantification over the range of a function.
(Contributed by Mario Carneiro, 24-Dec-2013.) (Revised by Mario
Carneiro, 20-Aug-2014.)
|
⊢ (𝑥 = (𝐹‘𝑦) → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐹 Fn 𝐴 → (∀𝑥 ∈ ran 𝐹𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓)) |
|
Theorem | elrnrexdm 5651* |
For any element in the range of a function there is an element in the
domain of the function for which the function value is the element of
the range. (Contributed by Alexander van der Vekens, 8-Dec-2017.)
|
⊢ (Fun 𝐹 → (𝑌 ∈ ran 𝐹 → ∃𝑥 ∈ dom 𝐹 𝑌 = (𝐹‘𝑥))) |
|
Theorem | elrnrexdmb 5652* |
For any element in the range of a function there is an element in the
domain of the function for which the function value is the element of
the range. (Contributed by Alexander van der Vekens, 17-Dec-2017.)
|
⊢ (Fun 𝐹 → (𝑌 ∈ ran 𝐹 ↔ ∃𝑥 ∈ dom 𝐹 𝑌 = (𝐹‘𝑥))) |
|
Theorem | eldmrexrn 5653* |
For any element in the domain of a function there is an element in the
range of the function which is the function value for the element of the
domain. (Contributed by Alexander van der Vekens, 8-Dec-2017.)
|
⊢ (Fun 𝐹 → (𝑌 ∈ dom 𝐹 → ∃𝑥 ∈ ran 𝐹 𝑥 = (𝐹‘𝑌))) |
|
Theorem | ralrnmpt 5654* |
A restricted quantifier over an image set. (Contributed by Mario
Carneiro, 20-Aug-2015.)
|
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)
& ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → (∀𝑦 ∈ ran 𝐹𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒)) |
|
Theorem | rexrnmpt 5655* |
A restricted quantifier over an image set. (Contributed by Mario
Carneiro, 20-Aug-2015.)
|
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)
& ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → (∃𝑦 ∈ ran 𝐹𝜓 ↔ ∃𝑥 ∈ 𝐴 𝜒)) |
|
Theorem | dff2 5656 |
Alternate definition of a mapping. (Contributed by NM, 14-Nov-2007.)
|
⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ 𝐹 ⊆ (𝐴 × 𝐵))) |
|
Theorem | dff3im 5657* |
Property of a mapping. (Contributed by Jim Kingdon, 4-Jan-2019.)
|
⊢ (𝐹:𝐴⟶𝐵 → (𝐹 ⊆ (𝐴 × 𝐵) ∧ ∀𝑥 ∈ 𝐴 ∃!𝑦 𝑥𝐹𝑦)) |
|
Theorem | dff4im 5658* |
Property of a mapping. (Contributed by Jim Kingdon, 4-Jan-2019.)
|
⊢ (𝐹:𝐴⟶𝐵 → (𝐹 ⊆ (𝐴 × 𝐵) ∧ ∀𝑥 ∈ 𝐴 ∃!𝑦 ∈ 𝐵 𝑥𝐹𝑦)) |
|
Theorem | dffo3 5659* |
An onto mapping expressed in terms of function values. (Contributed by
NM, 29-Oct-2006.)
|
⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥))) |
|
Theorem | dffo4 5660* |
Alternate definition of an onto mapping. (Contributed by NM,
20-Mar-2007.)
|
⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝑥𝐹𝑦)) |
|
Theorem | dffo5 5661* |
Alternate definition of an onto mapping. (Contributed by NM,
20-Mar-2007.)
|
⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑦 ∈ 𝐵 ∃𝑥 𝑥𝐹𝑦)) |
|
Theorem | fmpt 5662* |
Functionality of the mapping operation. (Contributed by Mario Carneiro,
26-Jul-2013.) (Revised by Mario Carneiro, 31-Aug-2015.)
|
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐶) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ↔ 𝐹:𝐴⟶𝐵) |
|
Theorem | f1ompt 5663* |
Express bijection for a mapping operation. (Contributed by Mario
Carneiro, 30-May-2015.) (Revised by Mario Carneiro, 4-Dec-2016.)
|
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐶) ⇒ ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ∃!𝑥 ∈ 𝐴 𝑦 = 𝐶)) |
|
Theorem | fmpti 5664* |
Functionality of the mapping operation. (Contributed by NM,
19-Mar-2005.) (Revised by Mario Carneiro, 1-Sep-2015.)
|
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐶)
& ⊢ (𝑥 ∈ 𝐴 → 𝐶 ∈ 𝐵) ⇒ ⊢ 𝐹:𝐴⟶𝐵 |
|
Theorem | fvmptelcdm 5665* |
The value of a function at a point of its domain belongs to its
codomain. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵):𝐴⟶𝐶) ⇒ ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶) |
|
Theorem | fmptd 5666* |
Domain and codomain of the mapping operation; deduction form.
(Contributed by Mario Carneiro, 13-Jan-2013.)
|
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶)
& ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ (𝜑 → 𝐹:𝐴⟶𝐶) |
|
Theorem | fmpttd 5667* |
Version of fmptd 5666 with inlined definition. Domain and codomain
of the
mapping operation; deduction form. (Contributed by Glauco Siliprandi,
23-Oct-2021.) (Proof shortened by BJ, 16-Aug-2022.)
|
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵):𝐴⟶𝐶) |
|
Theorem | fmpt3d 5668* |
Domain and codomain of the mapping operation; deduction form.
(Contributed by Thierry Arnoux, 4-Jun-2017.)
|
⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶) ⇒ ⊢ (𝜑 → 𝐹:𝐴⟶𝐶) |
|
Theorem | fmptdf 5669* |
A version of fmptd 5666 using bound-variable hypothesis instead of a
distinct variable condition for 𝜑. (Contributed by Glauco
Siliprandi, 29-Jun-2017.)
|
⊢ Ⅎ𝑥𝜑
& ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶)
& ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ (𝜑 → 𝐹:𝐴⟶𝐶) |
|
Theorem | ffnfv 5670* |
A function maps to a class to which all values belong. (Contributed by
NM, 3-Dec-2003.)
|
⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵)) |
|
Theorem | ffnfvf 5671 |
A function maps to a class to which all values belong. This version of
ffnfv 5670 uses bound-variable hypotheses instead of
distinct variable
conditions. (Contributed by NM, 28-Sep-2006.)
|
⊢ Ⅎ𝑥𝐴
& ⊢ Ⅎ𝑥𝐵
& ⊢ Ⅎ𝑥𝐹 ⇒ ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵)) |
|
Theorem | fnfvrnss 5672* |
An upper bound for range determined by function values. (Contributed by
NM, 8-Oct-2004.)
|
⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → ran 𝐹 ⊆ 𝐵) |
|
Theorem | rnmptss 5673* |
The range of an operation given by the maps-to notation as a subset.
(Contributed by Thierry Arnoux, 24-Sep-2017.)
|
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ran 𝐹 ⊆ 𝐶) |
|
Theorem | fmpt2d 5674* |
Domain and codomain of the mapping operation; deduction form.
(Contributed by NM, 27-Dec-2014.)
|
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)
& ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (𝐹‘𝑦) ∈ 𝐶) ⇒ ⊢ (𝜑 → 𝐹:𝐴⟶𝐶) |
|
Theorem | ffvresb 5675* |
A necessary and sufficient condition for a restricted function.
(Contributed by Mario Carneiro, 14-Nov-2013.)
|
⊢ (Fun 𝐹 → ((𝐹 ↾ 𝐴):𝐴⟶𝐵 ↔ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom 𝐹 ∧ (𝐹‘𝑥) ∈ 𝐵))) |
|
Theorem | resflem 5676* |
A lemma to bound the range of a restriction. The conclusion would also
hold with (𝑋 ∩ 𝑌) in place of 𝑌 (provided 𝑥 does
not
occur in 𝑋). If that stronger result is
needed, it is however
simpler to use the instance of resflem 5676 where (𝑋 ∩ 𝑌) is
substituted for 𝑌 (in both the conclusion and the
third hypothesis).
(Contributed by BJ, 4-Jul-2022.)
|
⊢ (𝜑 → 𝐹:𝑉⟶𝑋)
& ⊢ (𝜑 → 𝐴 ⊆ 𝑉)
& ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ 𝑌) ⇒ ⊢ (𝜑 → (𝐹 ↾ 𝐴):𝐴⟶𝑌) |
|
Theorem | f1oresrab 5677* |
Build a bijection between restricted abstract builders, given a
bijection between the base classes, deduction version. (Contributed by
Thierry Arnoux, 17-Aug-2018.)
|
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐶)
& ⊢ (𝜑 → 𝐹:𝐴–1-1-onto→𝐵)
& ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶) → (𝜒 ↔ 𝜓)) ⇒ ⊢ (𝜑 → (𝐹 ↾ {𝑥 ∈ 𝐴 ∣ 𝜓}):{𝑥 ∈ 𝐴 ∣ 𝜓}–1-1-onto→{𝑦 ∈ 𝐵 ∣ 𝜒}) |
|
Theorem | fmptco 5678* |
Composition of two functions expressed as ordered-pair class
abstractions. If 𝐹 has the equation ( x + 2 ) and 𝐺 the
equation ( 3 * z ) then (𝐺 ∘ 𝐹) has the equation ( 3 * ( x +
2 ) ) . (Contributed by FL, 21-Jun-2012.) (Revised by Mario Carneiro,
24-Jul-2014.)
|
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑅 ∈ 𝐵)
& ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝑅)) & ⊢ (𝜑 → 𝐺 = (𝑦 ∈ 𝐵 ↦ 𝑆)) & ⊢ (𝑦 = 𝑅 → 𝑆 = 𝑇) ⇒ ⊢ (𝜑 → (𝐺 ∘ 𝐹) = (𝑥 ∈ 𝐴 ↦ 𝑇)) |
|
Theorem | fmptcof 5679* |
Version of fmptco 5678 where 𝜑 needn't be distinct from 𝑥.
(Contributed by NM, 27-Dec-2014.)
|
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝑅 ∈ 𝐵)
& ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝑅)) & ⊢ (𝜑 → 𝐺 = (𝑦 ∈ 𝐵 ↦ 𝑆)) & ⊢ (𝑦 = 𝑅 → 𝑆 = 𝑇) ⇒ ⊢ (𝜑 → (𝐺 ∘ 𝐹) = (𝑥 ∈ 𝐴 ↦ 𝑇)) |
|
Theorem | fmptcos 5680* |
Composition of two functions expressed as mapping abstractions.
(Contributed by NM, 22-May-2006.) (Revised by Mario Carneiro,
31-Aug-2015.)
|
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝑅 ∈ 𝐵)
& ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝑅)) & ⊢ (𝜑 → 𝐺 = (𝑦 ∈ 𝐵 ↦ 𝑆)) ⇒ ⊢ (𝜑 → (𝐺 ∘ 𝐹) = (𝑥 ∈ 𝐴 ↦ ⦋𝑅 / 𝑦⦌𝑆)) |
|
Theorem | cofmpt 5681* |
Express composition of a maps-to function with another function in a
maps-to notation. (Contributed by Thierry Arnoux, 29-Jun-2017.)
|
⊢ (𝜑 → 𝐹:𝐶⟶𝐷)
& ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶) ⇒ ⊢ (𝜑 → (𝐹 ∘ (𝑥 ∈ 𝐴 ↦ 𝐵)) = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝐵))) |
|
Theorem | fcompt 5682* |
Express composition of two functions as a maps-to applying both in
sequence. (Contributed by Stefan O'Rear, 5-Oct-2014.) (Proof shortened
by Mario Carneiro, 27-Dec-2014.)
|
⊢ ((𝐴:𝐷⟶𝐸 ∧ 𝐵:𝐶⟶𝐷) → (𝐴 ∘ 𝐵) = (𝑥 ∈ 𝐶 ↦ (𝐴‘(𝐵‘𝑥)))) |
|
Theorem | fcoconst 5683 |
Composition with a constant function. (Contributed by Stefan O'Rear,
11-Mar-2015.)
|
⊢ ((𝐹 Fn 𝑋 ∧ 𝑌 ∈ 𝑋) → (𝐹 ∘ (𝐼 × {𝑌})) = (𝐼 × {(𝐹‘𝑌)})) |
|
Theorem | fsn 5684 |
A function maps a singleton to a singleton iff it is the singleton of an
ordered pair. (Contributed by NM, 10-Dec-2003.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈
V ⇒ ⊢ (𝐹:{𝐴}⟶{𝐵} ↔ 𝐹 = {〈𝐴, 𝐵〉}) |
|
Theorem | fsng 5685 |
A function maps a singleton to a singleton iff it is the singleton of an
ordered pair. (Contributed by NM, 26-Oct-2012.)
|
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐹:{𝐴}⟶{𝐵} ↔ 𝐹 = {〈𝐴, 𝐵〉})) |
|
Theorem | fsn2 5686 |
A function that maps a singleton to a class is the singleton of an
ordered pair. (Contributed by NM, 19-May-2004.)
|
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐹:{𝐴}⟶𝐵 ↔ ((𝐹‘𝐴) ∈ 𝐵 ∧ 𝐹 = {〈𝐴, (𝐹‘𝐴)〉})) |
|
Theorem | xpsng 5687 |
The cross product of two singletons. (Contributed by Mario Carneiro,
30-Apr-2015.)
|
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ({𝐴} × {𝐵}) = {〈𝐴, 𝐵〉}) |
|
Theorem | xpsn 5688 |
The cross product of two singletons. (Contributed by NM,
4-Nov-2006.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈
V ⇒ ⊢ ({𝐴} × {𝐵}) = {〈𝐴, 𝐵〉} |
|
Theorem | dfmpt 5689 |
Alternate definition for the maps-to notation df-mpt 4063 (although it
requires that 𝐵 be a set). (Contributed by NM,
24-Aug-2010.)
(Revised by Mario Carneiro, 30-Dec-2016.)
|
⊢ 𝐵 ∈ V ⇒ ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = ∪
𝑥 ∈ 𝐴 {〈𝑥, 𝐵〉} |
|
Theorem | fnasrn 5690 |
A function expressed as the range of another function. (Contributed by
Mario Carneiro, 22-Jun-2013.) (Proof shortened by Mario Carneiro,
31-Aug-2015.)
|
⊢ 𝐵 ∈ V ⇒ ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = ran (𝑥 ∈ 𝐴 ↦ 〈𝑥, 𝐵〉) |
|
Theorem | dfmptg 5691 |
Alternate definition for the maps-to notation df-mpt 4063 (which requires
that 𝐵 be a set). (Contributed by Jim
Kingdon, 9-Jan-2019.)
|
⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → (𝑥 ∈ 𝐴 ↦ 𝐵) = ∪
𝑥 ∈ 𝐴 {〈𝑥, 𝐵〉}) |
|
Theorem | fnasrng 5692 |
A function expressed as the range of another function. (Contributed by
Jim Kingdon, 9-Jan-2019.)
|
⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → (𝑥 ∈ 𝐴 ↦ 𝐵) = ran (𝑥 ∈ 𝐴 ↦ 〈𝑥, 𝐵〉)) |
|
Theorem | ressnop0 5693 |
If 𝐴 is not in 𝐶, then the restriction of
a singleton of
〈𝐴, 𝐵〉 to 𝐶 is null. (Contributed
by Scott Fenton,
15-Apr-2011.)
|
⊢ (¬ 𝐴 ∈ 𝐶 → ({〈𝐴, 𝐵〉} ↾ 𝐶) = ∅) |
|
Theorem | fpr 5694 |
A function with a domain of two elements. (Contributed by Jeff Madsen,
20-Jun-2010.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V & ⊢ 𝐷 ∈
V ⇒ ⊢ (𝐴 ≠ 𝐵 → {〈𝐴, 𝐶〉, 〈𝐵, 𝐷〉}:{𝐴, 𝐵}⟶{𝐶, 𝐷}) |
|
Theorem | fprg 5695 |
A function with a domain of two elements. (Contributed by FL,
2-Feb-2014.)
|
⊢ (((𝐴 ∈ 𝐸 ∧ 𝐵 ∈ 𝐹) ∧ (𝐶 ∈ 𝐺 ∧ 𝐷 ∈ 𝐻) ∧ 𝐴 ≠ 𝐵) → {〈𝐴, 𝐶〉, 〈𝐵, 𝐷〉}:{𝐴, 𝐵}⟶{𝐶, 𝐷}) |
|
Theorem | ftpg 5696 |
A function with a domain of three elements. (Contributed by Alexander van
der Vekens, 4-Dec-2017.)
|
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ∧ 𝐶 ∈ 𝐻) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → {〈𝑋, 𝐴〉, 〈𝑌, 𝐵〉, 〈𝑍, 𝐶〉}:{𝑋, 𝑌, 𝑍}⟶{𝐴, 𝐵, 𝐶}) |
|
Theorem | ftp 5697 |
A function with a domain of three elements. (Contributed by Stefan
O'Rear, 17-Oct-2014.) (Proof shortened by Alexander van der Vekens,
23-Jan-2018.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V & ⊢ 𝑋 ∈ V & ⊢ 𝑌 ∈ V & ⊢ 𝑍 ∈ V & ⊢ 𝐴 ≠ 𝐵
& ⊢ 𝐴 ≠ 𝐶
& ⊢ 𝐵 ≠ 𝐶 ⇒ ⊢ {〈𝐴, 𝑋〉, 〈𝐵, 𝑌〉, 〈𝐶, 𝑍〉}:{𝐴, 𝐵, 𝐶}⟶{𝑋, 𝑌, 𝑍} |
|
Theorem | fnressn 5698 |
A function restricted to a singleton. (Contributed by NM,
9-Oct-2004.)
|
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → (𝐹 ↾ {𝐵}) = {〈𝐵, (𝐹‘𝐵)〉}) |
|
Theorem | fressnfv 5699 |
The value of a function restricted to a singleton. (Contributed by NM,
9-Oct-2004.)
|
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → ((𝐹 ↾ {𝐵}):{𝐵}⟶𝐶 ↔ (𝐹‘𝐵) ∈ 𝐶)) |
|
Theorem | fvconst 5700 |
The value of a constant function. (Contributed by NM, 30-May-1999.)
|
⊢ ((𝐹:𝐴⟶{𝐵} ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) = 𝐵) |