Theorem List for Intuitionistic Logic Explorer - 4801-4900 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | djudisj 4801* |
Disjoint unions with disjoint index sets are disjoint. (Contributed by
Stefan O'Rear, 21-Nov-2014.)
|
⊢ ((𝐴 ∩ 𝐵) = ∅ → (∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐶) ∩ ∪
𝑦 ∈ 𝐵 ({𝑦} × 𝐷)) = ∅) |
|
Theorem | resdisj 4802 |
A double restriction to disjoint classes is the empty set. (Contributed
by NM, 7-Oct-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
|
⊢ ((𝐴 ∩ 𝐵) = ∅ → ((𝐶 ↾ 𝐴) ↾ 𝐵) = ∅) |
|
Theorem | rnxpm 4803* |
The range of a cross product. Part of Theorem 3.13(x) of [Monk1] p. 37,
with non-empty changed to inhabited. (Contributed by Jim Kingdon,
12-Dec-2018.)
|
⊢ (∃𝑥 𝑥 ∈ 𝐴 → ran (𝐴 × 𝐵) = 𝐵) |
|
Theorem | dmxpss 4804 |
The domain of a cross product is a subclass of the first factor.
(Contributed by NM, 19-Mar-2007.)
|
⊢ dom (𝐴 × 𝐵) ⊆ 𝐴 |
|
Theorem | rnxpss 4805 |
The range of a cross product is a subclass of the second factor.
(Contributed by NM, 16-Jan-2006.) (Proof shortened by Andrew Salmon,
27-Aug-2011.)
|
⊢ ran (𝐴 × 𝐵) ⊆ 𝐵 |
|
Theorem | rnxpid 4806 |
The range of a square cross product. (Contributed by FL,
17-May-2010.)
|
⊢ ran (𝐴 × 𝐴) = 𝐴 |
|
Theorem | ssxpbm 4807* |
A cross-product subclass relationship is equivalent to the relationship
for its components. (Contributed by Jim Kingdon, 12-Dec-2018.)
|
⊢ (∃𝑥 𝑥 ∈ (𝐴 × 𝐵) → ((𝐴 × 𝐵) ⊆ (𝐶 × 𝐷) ↔ (𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐷))) |
|
Theorem | ssxp1 4808* |
Cross product subset cancellation. (Contributed by Jim Kingdon,
14-Dec-2018.)
|
⊢ (∃𝑥 𝑥 ∈ 𝐶 → ((𝐴 × 𝐶) ⊆ (𝐵 × 𝐶) ↔ 𝐴 ⊆ 𝐵)) |
|
Theorem | ssxp2 4809* |
Cross product subset cancellation. (Contributed by Jim Kingdon,
14-Dec-2018.)
|
⊢ (∃𝑥 𝑥 ∈ 𝐶 → ((𝐶 × 𝐴) ⊆ (𝐶 × 𝐵) ↔ 𝐴 ⊆ 𝐵)) |
|
Theorem | xp11m 4810* |
The cross product of inhabited classes is one-to-one. (Contributed by
Jim Kingdon, 13-Dec-2018.)
|
⊢ ((∃𝑥 𝑥 ∈ 𝐴 ∧ ∃𝑦 𝑦 ∈ 𝐵) → ((𝐴 × 𝐵) = (𝐶 × 𝐷) ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))) |
|
Theorem | xpcanm 4811* |
Cancellation law for cross-product. (Contributed by Jim Kingdon,
14-Dec-2018.)
|
⊢ (∃𝑥 𝑥 ∈ 𝐶 → ((𝐶 × 𝐴) = (𝐶 × 𝐵) ↔ 𝐴 = 𝐵)) |
|
Theorem | xpcan2m 4812* |
Cancellation law for cross-product. (Contributed by Jim Kingdon,
14-Dec-2018.)
|
⊢ (∃𝑥 𝑥 ∈ 𝐶 → ((𝐴 × 𝐶) = (𝐵 × 𝐶) ↔ 𝐴 = 𝐵)) |
|
Theorem | xpexr2m 4813* |
If a nonempty cross product is a set, so are both of its components.
(Contributed by Jim Kingdon, 14-Dec-2018.)
|
⊢ (((𝐴 × 𝐵) ∈ 𝐶 ∧ ∃𝑥 𝑥 ∈ (𝐴 × 𝐵)) → (𝐴 ∈ V ∧ 𝐵 ∈ V)) |
|
Theorem | ssrnres 4814 |
Subset of the range of a restriction. (Contributed by NM,
16-Jan-2006.)
|
⊢ (𝐵 ⊆ ran (𝐶 ↾ 𝐴) ↔ ran (𝐶 ∩ (𝐴 × 𝐵)) = 𝐵) |
|
Theorem | rninxp 4815* |
Range of the intersection with a cross product. (Contributed by NM,
17-Jan-2006.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
|
⊢ (ran (𝐶 ∩ (𝐴 × 𝐵)) = 𝐵 ↔ ∀𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝑥𝐶𝑦) |
|
Theorem | dminxp 4816* |
Domain of the intersection with a cross product. (Contributed by NM,
17-Jan-2006.)
|
⊢ (dom (𝐶 ∩ (𝐴 × 𝐵)) = 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥𝐶𝑦) |
|
Theorem | imainrect 4817 |
Image of a relation restricted to a rectangular region. (Contributed by
Stefan O'Rear, 19-Feb-2015.)
|
⊢ ((𝐺 ∩ (𝐴 × 𝐵)) “ 𝑌) = ((𝐺 “ (𝑌 ∩ 𝐴)) ∩ 𝐵) |
|
Theorem | xpima1 4818 |
The image by a cross product. (Contributed by Thierry Arnoux,
16-Dec-2017.)
|
⊢ ((𝐴 ∩ 𝐶) = ∅ → ((𝐴 × 𝐵) “ 𝐶) = ∅) |
|
Theorem | xpima2m 4819* |
The image by a cross product. (Contributed by Thierry Arnoux,
16-Dec-2017.)
|
⊢ (∃𝑥 𝑥 ∈ (𝐴 ∩ 𝐶) → ((𝐴 × 𝐵) “ 𝐶) = 𝐵) |
|
Theorem | xpimasn 4820 |
The image of a singleton by a cross product. (Contributed by Thierry
Arnoux, 14-Jan-2018.)
|
⊢ (𝑋 ∈ 𝐴 → ((𝐴 × 𝐵) “ {𝑋}) = 𝐵) |
|
Theorem | cnvcnv3 4821* |
The set of all ordered pairs in a class is the same as the double
converse. (Contributed by Mario Carneiro, 16-Aug-2015.)
|
⊢ ◡◡𝑅 = {〈𝑥, 𝑦〉 ∣ 𝑥𝑅𝑦} |
|
Theorem | dfrel2 4822 |
Alternate definition of relation. Exercise 2 of [TakeutiZaring] p. 25.
(Contributed by NM, 29-Dec-1996.)
|
⊢ (Rel 𝑅 ↔ ◡◡𝑅 = 𝑅) |
|
Theorem | dfrel4v 4823* |
A relation can be expressed as the set of ordered pairs in it.
(Contributed by Mario Carneiro, 16-Aug-2015.)
|
⊢ (Rel 𝑅 ↔ 𝑅 = {〈𝑥, 𝑦〉 ∣ 𝑥𝑅𝑦}) |
|
Theorem | cnvcnv 4824 |
The double converse of a class strips out all elements that are not
ordered pairs. (Contributed by NM, 8-Dec-2003.)
|
⊢ ◡◡𝐴 = (𝐴 ∩ (V × V)) |
|
Theorem | cnvcnv2 4825 |
The double converse of a class equals its restriction to the universe.
(Contributed by NM, 8-Oct-2007.)
|
⊢ ◡◡𝐴 = (𝐴 ↾ V) |
|
Theorem | cnvcnvss 4826 |
The double converse of a class is a subclass. Exercise 2 of
[TakeutiZaring] p. 25. (Contributed
by NM, 23-Jul-2004.)
|
⊢ ◡◡𝐴 ⊆ 𝐴 |
|
Theorem | cnveqb 4827 |
Equality theorem for converse. (Contributed by FL, 19-Sep-2011.)
|
⊢ ((Rel 𝐴 ∧ Rel 𝐵) → (𝐴 = 𝐵 ↔ ◡𝐴 = ◡𝐵)) |
|
Theorem | cnveq0 4828 |
A relation empty iff its converse is empty. (Contributed by FL,
19-Sep-2011.)
|
⊢ (Rel 𝐴 → (𝐴 = ∅ ↔ ◡𝐴 = ∅)) |
|
Theorem | dfrel3 4829 |
Alternate definition of relation. (Contributed by NM, 14-May-2008.)
|
⊢ (Rel 𝑅 ↔ (𝑅 ↾ V) = 𝑅) |
|
Theorem | dmresv 4830 |
The domain of a universal restriction. (Contributed by NM,
14-May-2008.)
|
⊢ dom (𝐴 ↾ V) = dom 𝐴 |
|
Theorem | rnresv 4831 |
The range of a universal restriction. (Contributed by NM,
14-May-2008.)
|
⊢ ran (𝐴 ↾ V) = ran 𝐴 |
|
Theorem | dfrn4 4832 |
Range defined in terms of image. (Contributed by NM, 14-May-2008.)
|
⊢ ran 𝐴 = (𝐴 “ V) |
|
Theorem | csbrng 4833 |
Distribute proper substitution through the range of a class.
(Contributed by Alan Sare, 10-Nov-2012.)
|
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌ran 𝐵 = ran ⦋𝐴 / 𝑥⦌𝐵) |
|
Theorem | rescnvcnv 4834 |
The restriction of the double converse of a class. (Contributed by NM,
8-Apr-2007.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
|
⊢ (◡◡𝐴 ↾ 𝐵) = (𝐴 ↾ 𝐵) |
|
Theorem | cnvcnvres 4835 |
The double converse of the restriction of a class. (Contributed by NM,
3-Jun-2007.)
|
⊢ ◡◡(𝐴 ↾ 𝐵) = (◡◡𝐴 ↾ 𝐵) |
|
Theorem | imacnvcnv 4836 |
The image of the double converse of a class. (Contributed by NM,
8-Apr-2007.)
|
⊢ (◡◡𝐴 “ 𝐵) = (𝐴 “ 𝐵) |
|
Theorem | dmsnm 4837* |
The domain of a singleton is inhabited iff the singleton argument is an
ordered pair. (Contributed by Jim Kingdon, 15-Dec-2018.)
|
⊢ (𝐴 ∈ (V × V) ↔ ∃𝑥 𝑥 ∈ dom {𝐴}) |
|
Theorem | rnsnm 4838* |
The range of a singleton is inhabited iff the singleton argument is an
ordered pair. (Contributed by Jim Kingdon, 15-Dec-2018.)
|
⊢ (𝐴 ∈ (V × V) ↔ ∃𝑥 𝑥 ∈ ran {𝐴}) |
|
Theorem | dmsn0 4839 |
The domain of the singleton of the empty set is empty. (Contributed by
NM, 30-Jan-2004.)
|
⊢ dom {∅} = ∅ |
|
Theorem | cnvsn0 4840 |
The converse of the singleton of the empty set is empty. (Contributed by
Mario Carneiro, 30-Aug-2015.)
|
⊢ ◡{∅} = ∅ |
|
Theorem | dmsn0el 4841 |
The domain of a singleton is empty if the singleton's argument contains
the empty set. (Contributed by NM, 15-Dec-2008.)
|
⊢ (∅ ∈ 𝐴 → dom {𝐴} = ∅) |
|
Theorem | relsn2m 4842* |
A singleton is a relation iff it has an inhabited domain. (Contributed
by Jim Kingdon, 16-Dec-2018.)
|
⊢ 𝐴 ∈ V ⇒ ⊢ (Rel {𝐴} ↔ ∃𝑥 𝑥 ∈ dom {𝐴}) |
|
Theorem | dmsnopg 4843 |
The domain of a singleton of an ordered pair is the singleton of the
first member. (Contributed by Mario Carneiro, 26-Apr-2015.)
|
⊢ (𝐵 ∈ 𝑉 → dom {〈𝐴, 𝐵〉} = {𝐴}) |
|
Theorem | dmpropg 4844 |
The domain of an unordered pair of ordered pairs. (Contributed by Mario
Carneiro, 26-Apr-2015.)
|
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐷 ∈ 𝑊) → dom {〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉} = {𝐴, 𝐶}) |
|
Theorem | dmsnop 4845 |
The domain of a singleton of an ordered pair is the singleton of the
first member. (Contributed by NM, 30-Jan-2004.) (Proof shortened by
Andrew Salmon, 27-Aug-2011.) (Revised by Mario Carneiro,
26-Apr-2015.)
|
⊢ 𝐵 ∈ V ⇒ ⊢ dom {〈𝐴, 𝐵〉} = {𝐴} |
|
Theorem | dmprop 4846 |
The domain of an unordered pair of ordered pairs. (Contributed by NM,
13-Sep-2011.)
|
⊢ 𝐵 ∈ V & ⊢ 𝐷 ∈
V ⇒ ⊢ dom {〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉} = {𝐴, 𝐶} |
|
Theorem | dmtpop 4847 |
The domain of an unordered triple of ordered pairs. (Contributed by NM,
14-Sep-2011.)
|
⊢ 𝐵 ∈ V & ⊢ 𝐷 ∈ V & ⊢ 𝐹 ∈
V ⇒ ⊢ dom {〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉, 〈𝐸, 𝐹〉} = {𝐴, 𝐶, 𝐸} |
|
Theorem | cnvcnvsn 4848 |
Double converse of a singleton of an ordered pair. (Unlike cnvsn 4854,
this does not need any sethood assumptions on 𝐴 and 𝐵.)
(Contributed by Mario Carneiro, 26-Apr-2015.)
|
⊢ ◡◡{〈𝐴, 𝐵〉} = ◡{〈𝐵, 𝐴〉} |
|
Theorem | dmsnsnsng 4849 |
The domain of the singleton of the singleton of a singleton.
(Contributed by Jim Kingdon, 16-Dec-2018.)
|
⊢ (𝐴 ∈ V → dom {{{𝐴}}} = {𝐴}) |
|
Theorem | rnsnopg 4850 |
The range of a singleton of an ordered pair is the singleton of the second
member. (Contributed by NM, 24-Jul-2004.) (Revised by Mario Carneiro,
30-Apr-2015.)
|
⊢ (𝐴 ∈ 𝑉 → ran {〈𝐴, 𝐵〉} = {𝐵}) |
|
Theorem | rnpropg 4851 |
The range of a pair of ordered pairs is the pair of second members.
(Contributed by Thierry Arnoux, 3-Jan-2017.)
|
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ran {〈𝐴, 𝐶〉, 〈𝐵, 𝐷〉} = {𝐶, 𝐷}) |
|
Theorem | rnsnop 4852 |
The range of a singleton of an ordered pair is the singleton of the
second member. (Contributed by NM, 24-Jul-2004.) (Revised by Mario
Carneiro, 26-Apr-2015.)
|
⊢ 𝐴 ∈ V ⇒ ⊢ ran {〈𝐴, 𝐵〉} = {𝐵} |
|
Theorem | op1sta 4853 |
Extract the first member of an ordered pair. (See op2nda 4856 to extract
the second member and op1stb 4256 for an alternate version.)
(Contributed
by Raph Levien, 4-Dec-2003.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈
V ⇒ ⊢ ∪
dom {〈𝐴, 𝐵〉} = 𝐴 |
|
Theorem | cnvsn 4854 |
Converse of a singleton of an ordered pair. (Contributed by NM,
11-May-1998.) (Revised by Mario Carneiro, 26-Apr-2015.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈
V ⇒ ⊢ ◡{〈𝐴, 𝐵〉} = {〈𝐵, 𝐴〉} |
|
Theorem | op2ndb 4855 |
Extract the second member of an ordered pair. Theorem 5.12(ii) of
[Monk1] p. 52. (See op1stb 4256 to extract the first member and op2nda 4856
for an alternate version.) (Contributed by NM, 25-Nov-2003.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈
V ⇒ ⊢ ∩
∩ ∩ ◡{〈𝐴, 𝐵〉} = 𝐵 |
|
Theorem | op2nda 4856 |
Extract the second member of an ordered pair. (See op1sta 4853 to extract
the first member and op2ndb 4855 for an alternate version.) (Contributed
by NM, 17-Feb-2004.) (Proof shortened by Andrew Salmon,
27-Aug-2011.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈
V ⇒ ⊢ ∪
ran {〈𝐴, 𝐵〉} = 𝐵 |
|
Theorem | cnvsng 4857 |
Converse of a singleton of an ordered pair. (Contributed by NM,
23-Jan-2015.)
|
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ◡{〈𝐴, 𝐵〉} = {〈𝐵, 𝐴〉}) |
|
Theorem | opswapg 4858 |
Swap the members of an ordered pair. (Contributed by Jim Kingdon,
16-Dec-2018.)
|
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ∪ ◡{〈𝐴, 𝐵〉} = 〈𝐵, 𝐴〉) |
|
Theorem | elxp4 4859 |
Membership in a cross product. This version requires no quantifiers or
dummy variables. See also elxp5 4860. (Contributed by NM,
17-Feb-2004.)
|
⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ (𝐴 = 〈∪ dom
{𝐴}, ∪ ran {𝐴}〉 ∧ (∪
dom {𝐴} ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶))) |
|
Theorem | elxp5 4860 |
Membership in a cross product requiring no quantifiers or dummy
variables. Provides a slightly shorter version of elxp4 4859 when the
double intersection does not create class existence problems (caused by
int0 3671). (Contributed by NM, 1-Aug-2004.)
|
⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ (𝐴 = 〈∩ ∩ 𝐴,
∪ ran {𝐴}〉 ∧ (∩
∩ 𝐴 ∈ 𝐵 ∧ ∪ ran
{𝐴} ∈ 𝐶))) |
|
Theorem | cnvresima 4861 |
An image under the converse of a restriction. (Contributed by Jeff
Hankins, 12-Jul-2009.)
|
⊢ (◡(𝐹 ↾ 𝐴) “ 𝐵) = ((◡𝐹 “ 𝐵) ∩ 𝐴) |
|
Theorem | resdm2 4862 |
A class restricted to its domain equals its double converse. (Contributed
by NM, 8-Apr-2007.)
|
⊢ (𝐴 ↾ dom 𝐴) = ◡◡𝐴 |
|
Theorem | resdmres 4863 |
Restriction to the domain of a restriction. (Contributed by NM,
8-Apr-2007.)
|
⊢ (𝐴 ↾ dom (𝐴 ↾ 𝐵)) = (𝐴 ↾ 𝐵) |
|
Theorem | imadmres 4864 |
The image of the domain of a restriction. (Contributed by NM,
8-Apr-2007.)
|
⊢ (𝐴 “ dom (𝐴 ↾ 𝐵)) = (𝐴 “ 𝐵) |
|
Theorem | mptpreima 4865* |
The preimage of a function in maps-to notation. (Contributed by Stefan
O'Rear, 25-Jan-2015.)
|
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ (◡𝐹 “ 𝐶) = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ 𝐶} |
|
Theorem | mptiniseg 4866* |
Converse singleton image of a function defined by maps-to. (Contributed
by Stefan O'Rear, 25-Jan-2015.)
|
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ (𝐶 ∈ 𝑉 → (◡𝐹 “ {𝐶}) = {𝑥 ∈ 𝐴 ∣ 𝐵 = 𝐶}) |
|
Theorem | dmmpt 4867 |
The domain of the mapping operation in general. (Contributed by NM,
16-May-1995.) (Revised by Mario Carneiro, 22-Mar-2015.)
|
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ dom 𝐹 = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V} |
|
Theorem | dmmptss 4868* |
The domain of a mapping is a subset of its base class. (Contributed by
Scott Fenton, 17-Jun-2013.)
|
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ dom 𝐹 ⊆ 𝐴 |
|
Theorem | dmmptg 4869* |
The domain of the mapping operation is the stated domain, if the
function value is always a set. (Contributed by Mario Carneiro,
9-Feb-2013.) (Revised by Mario Carneiro, 14-Sep-2013.)
|
⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → dom (𝑥 ∈ 𝐴 ↦ 𝐵) = 𝐴) |
|
Theorem | relco 4870 |
A composition is a relation. Exercise 24 of [TakeutiZaring] p. 25.
(Contributed by NM, 26-Jan-1997.)
|
⊢ Rel (𝐴 ∘ 𝐵) |
|
Theorem | dfco2 4871* |
Alternate definition of a class composition, using only one bound
variable. (Contributed by NM, 19-Dec-2008.)
|
⊢ (𝐴 ∘ 𝐵) = ∪
𝑥 ∈ V ((◡𝐵 “ {𝑥}) × (𝐴 “ {𝑥})) |
|
Theorem | dfco2a 4872* |
Generalization of dfco2 4871, where 𝐶 can have any value between
dom 𝐴 ∩ ran 𝐵 and V.
(Contributed by NM, 21-Dec-2008.)
(Proof shortened by Andrew Salmon, 27-Aug-2011.)
|
⊢ ((dom 𝐴 ∩ ran 𝐵) ⊆ 𝐶 → (𝐴 ∘ 𝐵) = ∪
𝑥 ∈ 𝐶 ((◡𝐵 “ {𝑥}) × (𝐴 “ {𝑥}))) |
|
Theorem | coundi 4873 |
Class composition distributes over union. (Contributed by NM,
21-Dec-2008.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
|
⊢ (𝐴 ∘ (𝐵 ∪ 𝐶)) = ((𝐴 ∘ 𝐵) ∪ (𝐴 ∘ 𝐶)) |
|
Theorem | coundir 4874 |
Class composition distributes over union. (Contributed by NM,
21-Dec-2008.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
|
⊢ ((𝐴 ∪ 𝐵) ∘ 𝐶) = ((𝐴 ∘ 𝐶) ∪ (𝐵 ∘ 𝐶)) |
|
Theorem | cores 4875 |
Restricted first member of a class composition. (Contributed by NM,
12-Oct-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
|
⊢ (ran 𝐵 ⊆ 𝐶 → ((𝐴 ↾ 𝐶) ∘ 𝐵) = (𝐴 ∘ 𝐵)) |
|
Theorem | resco 4876 |
Associative law for the restriction of a composition. (Contributed by
NM, 12-Dec-2006.)
|
⊢ ((𝐴 ∘ 𝐵) ↾ 𝐶) = (𝐴 ∘ (𝐵 ↾ 𝐶)) |
|
Theorem | imaco 4877 |
Image of the composition of two classes. (Contributed by Jason
Orendorff, 12-Dec-2006.)
|
⊢ ((𝐴 ∘ 𝐵) “ 𝐶) = (𝐴 “ (𝐵 “ 𝐶)) |
|
Theorem | rnco 4878 |
The range of the composition of two classes. (Contributed by NM,
12-Dec-2006.)
|
⊢ ran (𝐴 ∘ 𝐵) = ran (𝐴 ↾ ran 𝐵) |
|
Theorem | rnco2 4879 |
The range of the composition of two classes. (Contributed by NM,
27-Mar-2008.)
|
⊢ ran (𝐴 ∘ 𝐵) = (𝐴 “ ran 𝐵) |
|
Theorem | dmco 4880 |
The domain of a composition. Exercise 27 of [Enderton] p. 53.
(Contributed by NM, 4-Feb-2004.)
|
⊢ dom (𝐴 ∘ 𝐵) = (◡𝐵 “ dom 𝐴) |
|
Theorem | coiun 4881* |
Composition with an indexed union. (Contributed by NM, 21-Dec-2008.)
|
⊢ (𝐴 ∘ ∪ 𝑥 ∈ 𝐶 𝐵) = ∪
𝑥 ∈ 𝐶 (𝐴 ∘ 𝐵) |
|
Theorem | cocnvcnv1 4882 |
A composition is not affected by a double converse of its first argument.
(Contributed by NM, 8-Oct-2007.)
|
⊢ (◡◡𝐴 ∘ 𝐵) = (𝐴 ∘ 𝐵) |
|
Theorem | cocnvcnv2 4883 |
A composition is not affected by a double converse of its second argument.
(Contributed by NM, 8-Oct-2007.)
|
⊢ (𝐴 ∘ ◡◡𝐵) = (𝐴 ∘ 𝐵) |
|
Theorem | cores2 4884 |
Absorption of a reverse (preimage) restriction of the second member of a
class composition. (Contributed by NM, 11-Dec-2006.)
|
⊢ (dom 𝐴 ⊆ 𝐶 → (𝐴 ∘ ◡(◡𝐵 ↾ 𝐶)) = (𝐴 ∘ 𝐵)) |
|
Theorem | co02 4885 |
Composition with the empty set. Theorem 20 of [Suppes] p. 63.
(Contributed by NM, 24-Apr-2004.)
|
⊢ (𝐴 ∘ ∅) =
∅ |
|
Theorem | co01 4886 |
Composition with the empty set. (Contributed by NM, 24-Apr-2004.)
|
⊢ (∅ ∘ 𝐴) = ∅ |
|
Theorem | coi1 4887 |
Composition with the identity relation. Part of Theorem 3.7(i) of
[Monk1] p. 36. (Contributed by NM,
22-Apr-2004.)
|
⊢ (Rel 𝐴 → (𝐴 ∘ I ) = 𝐴) |
|
Theorem | coi2 4888 |
Composition with the identity relation. Part of Theorem 3.7(i) of
[Monk1] p. 36. (Contributed by NM,
22-Apr-2004.)
|
⊢ (Rel 𝐴 → ( I ∘ 𝐴) = 𝐴) |
|
Theorem | coires1 4889 |
Composition with a restricted identity relation. (Contributed by FL,
19-Jun-2011.) (Revised by Stefan O'Rear, 7-Mar-2015.)
|
⊢ (𝐴 ∘ ( I ↾ 𝐵)) = (𝐴 ↾ 𝐵) |
|
Theorem | coass 4890 |
Associative law for class composition. Theorem 27 of [Suppes] p. 64.
Also Exercise 21 of [Enderton] p. 53.
Interestingly, this law holds for
any classes whatsoever, not just functions or even relations.
(Contributed by NM, 27-Jan-1997.)
|
⊢ ((𝐴 ∘ 𝐵) ∘ 𝐶) = (𝐴 ∘ (𝐵 ∘ 𝐶)) |
|
Theorem | relcnvtr 4891 |
A relation is transitive iff its converse is transitive. (Contributed by
FL, 19-Sep-2011.)
|
⊢ (Rel 𝑅 → ((𝑅 ∘ 𝑅) ⊆ 𝑅 ↔ (◡𝑅 ∘ ◡𝑅) ⊆ ◡𝑅)) |
|
Theorem | relssdmrn 4892 |
A relation is included in the cross product of its domain and range.
Exercise 4.12(t) of [Mendelson] p.
235. (Contributed by NM,
3-Aug-1994.)
|
⊢ (Rel 𝐴 → 𝐴 ⊆ (dom 𝐴 × ran 𝐴)) |
|
Theorem | cnvssrndm 4893 |
The converse is a subset of the cartesian product of range and domain.
(Contributed by Mario Carneiro, 2-Jan-2017.)
|
⊢ ◡𝐴 ⊆ (ran 𝐴 × dom 𝐴) |
|
Theorem | cossxp 4894 |
Composition as a subset of the cross product of factors. (Contributed by
Mario Carneiro, 12-Jan-2017.)
|
⊢ (𝐴 ∘ 𝐵) ⊆ (dom 𝐵 × ran 𝐴) |
|
Theorem | relrelss 4895 |
Two ways to describe the structure of a two-place operation. (Contributed
by NM, 17-Dec-2008.)
|
⊢ ((Rel 𝐴 ∧ Rel dom 𝐴) ↔ 𝐴 ⊆ ((V × V) ×
V)) |
|
Theorem | unielrel 4896 |
The membership relation for a relation is inherited by class union.
(Contributed by NM, 17-Sep-2006.)
|
⊢ ((Rel 𝑅 ∧ 𝐴 ∈ 𝑅) → ∪ 𝐴 ∈ ∪ 𝑅) |
|
Theorem | relfld 4897 |
The double union of a relation is its field. (Contributed by NM,
17-Sep-2006.)
|
⊢ (Rel 𝑅 → ∪ ∪ 𝑅 =
(dom 𝑅 ∪ ran 𝑅)) |
|
Theorem | relresfld 4898 |
Restriction of a relation to its field. (Contributed by FL,
15-Apr-2012.)
|
⊢ (Rel 𝑅 → (𝑅 ↾ ∪ ∪ 𝑅)
= 𝑅) |
|
Theorem | relcoi2 4899 |
Composition with the identity relation restricted to a relation's field.
(Contributed by FL, 2-May-2011.)
|
⊢ (Rel 𝑅 → (( I ↾ ∪ ∪ 𝑅) ∘ 𝑅) = 𝑅) |
|
Theorem | relcoi1 4900 |
Composition with the identity relation restricted to a relation's field.
(Contributed by FL, 8-May-2011.)
|
⊢ (Rel 𝑅 → (𝑅 ∘ ( I ↾ ∪ ∪ 𝑅)) = 𝑅) |