Theorem List for New Foundations Explorer - 5001-5100 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | resopab2 5001* |
Restriction of a class abstraction of ordered pairs. (Contributed by
set.mm contributors, 24-Aug-2007.)
|
⊢ (A ⊆ B →
({〈x,
y〉 ∣ (x ∈ B ∧ φ)} ↾ A) = {〈x, y〉 ∣ (x ∈ A ∧ φ)}) |
|
Theorem | dfres2 5002* |
Alternate definition of the restriction operation. (Contributed by
Mario Carneiro, 5-Nov-2013.)
|
⊢ (R ↾ A) = {〈x, y〉 ∣ (x ∈ A ∧ xRy)} |
|
Theorem | opabresid 5003* |
The restricted identity expressed with the class builder. (Contributed
by FL, 25-Apr-2012.)
|
⊢ {〈x, y〉 ∣ (x ∈ A ∧ y = x)} = ( I
↾ A) |
|
Theorem | dmresi 5004 |
The domain of a restricted identity function. (Contributed by set.mm
contributors, 27-Aug-2004.)
|
⊢ dom ( I ↾
A) = A |
|
Theorem | resid 5005 |
Any class restricted to the universe is itself. (Contributed by set.mm
contributors, 16-Mar-2004.) (Revised by Scott Fenton, 18-Apr-2021.)
|
⊢ (A ↾ V) = A |
|
Theorem | resima 5006 |
A restriction to an image. (Contributed by set.mm contributors,
29-Sep-2004.)
|
⊢ ((A ↾ B) “
B) = (A “ B) |
|
Theorem | resima2 5007 |
Image under a restricted class. (Contributed by FL, 31-Aug-2009.)
|
⊢ (B ⊆ C →
((A ↾
C) “ B) = (A “
B)) |
|
Theorem | imadmrn 5008 |
The image of the domain of a class is the range of the class.
(Contributed by set.mm contributors, 14-Aug-1994.)
|
⊢ (A “
dom A) = ran A |
|
Theorem | imassrn 5009 |
The image of a class is a subset of its range. Theorem 3.16(xi) of
[Monk1] p. 39. (Contributed by set.mm
contributors, 31-Mar-1995.)
|
⊢ (A “
B) ⊆
ran A |
|
Theorem | imai 5010 |
Image under the identity relation. Theorem 3.16(viii) of [Monk1] p. 38.
(Contributed by set.mm contributors, 30-Apr-1998.)
|
⊢ ( I “ A) = A |
|
Theorem | rnresi 5011 |
The range of the restricted identity function. (Contributed by set.mm
contributors, 27-Aug-2004.)
|
⊢ ran ( I ↾
A) = A |
|
Theorem | resiima 5012 |
The image of a restriction of the identity function. (Contributed by FL,
31-Dec-2006.)
|
⊢ (B ⊆ A → ((
I ↾ A)
“ B) = B) |
|
Theorem | ima0 5013 |
Image of the empty set. Theorem 3.16(ii) of [Monk1] p. 38. (Contributed
by set.mm contributors, 20-May-1998.)
|
⊢ (A “
∅) = ∅ |
|
Theorem | 0ima 5014 |
Image under the empty relation. (Contributed by FL, 11-Jan-2007.)
|
⊢ (∅ “
A) = ∅ |
|
Theorem | imadisj 5015 |
A class whose image under another is empty is disjoint with the other's
domain. (Contributed by FL, 24-Jan-2007.)
|
⊢ ((A “
B) = ∅
↔ (dom A ∩ B) = ∅) |
|
Theorem | cnvimass 5016 |
A preimage under any class is included in the domain of the class.
(Contributed by FL, 29-Jan-2007.)
|
⊢ (◡A
“ B) ⊆ dom A |
|
Theorem | cnvimarndm 5017 |
The preimage of the range of a class is the domain of the class.
(Contributed by Jeff Hankins, 15-Jul-2009.)
|
⊢ (◡A
“ ran A) = dom A |
|
Theorem | imasn 5018* |
The image of a singleton. (Contributed by set.mm contributors,
9-Jan-2015.)
|
⊢ (R “
{A}) = {y ∣ ARy} |
|
Theorem | elimasn 5019 |
Membership in an image of a singleton. (The proof was shortened by
Andrew Salmon, 27-Aug-2011.) (Contributed by set.mm contributors,
15-Mar-2004.) (Revised by set.mm contributors, 27-Aug-2011.)
|
⊢ (C ∈ (A “
{B}) ↔ 〈B, C〉 ∈ A) |
|
Theorem | eliniseg 5020 |
Membership in an initial segment. The idiom (◡A
“ {B}),
meaning {x ∣ xAB}, is
used to specify an initial segment in (for
example) Definition 6.21 of [TakeutiZaring] p. 30. (The proof was
shortened by Andrew Salmon, 27-Aug-2011.) (Contributed by set.mm
contributors, 28-Apr-2004.) (Revised by set.mm contributors,
27-Aug-2011.)
|
⊢ (C ∈ (◡A
“ {B}) ↔ CAB) |
|
Theorem | epini 5021 |
Any set is equal to its preimage under the converse epsilon relation.
(Contributed by Mario Carneiro, 9-Mar-2013.)
|
⊢ A ∈ V ⇒ ⊢ (◡ E
“ {A}) = A |
|
Theorem | iniseg 5022* |
An idiom that signifies an initial segment of an ordering, used, for
example, in Definition 6.21 of [TakeutiZaring] p. 30. (Contributed by
set.mm contributors, 28-Apr-2004.)
|
⊢ (◡A
“ {B}) = {x ∣ xAB} |
|
Theorem | imass1 5023 |
Subset theorem for image. (Contributed by set.mm contributors,
16-Mar-2004.)
|
⊢ (A ⊆ B →
(A “ C) ⊆ (B “ C)) |
|
Theorem | imass2 5024 |
Subset theorem for image. Exercise 22(a) of [Enderton] p. 53.
(Contributed by set.mm contributors, 22-Mar-1998.)
|
⊢ (A ⊆ B →
(C “ A) ⊆ (C “ B)) |
|
Theorem | ndmima 5025 |
The image of a singleton outside the domain is empty. (Contributed by
set.mm contributors, 22-May-1998.)
|
⊢ (¬ A
∈ dom B
→ (B “ {A}) = ∅) |
|
Theorem | cotr 5026* |
Two ways of saying a relation is transitive. Definition of transitivity
in [Schechter] p. 51. (The proof was
shortened by Andrew Salmon,
27-Aug-2011.) (Contributed by set.mm contributors, 27-Dec-1996.)
(Revised by set.mm contributors, 27-Aug-2011.)
|
⊢ ((R ∘ R) ⊆ R ↔
∀x∀y∀z((xRy ∧ yRz) →
xRz)) |
|
Theorem | cnvsym 5027* |
Two ways of saying a relation is symmetric. Similar to definition of
symmetry in [Schechter] p. 51. (The
proof was shortened by Andrew
Salmon, 27-Aug-2011.) (Contributed by set.mm contributors,
28-Dec-1996.) (Revised by set.mm contributors, 27-Aug-2011.)
|
⊢ (◡R ⊆ R ↔
∀x∀y(xRy →
yRx)) |
|
Theorem | intasym 5028* |
Two ways of saying a relation is antisymmetric. Definition of
antisymmetry in [Schechter] p. 51.
(The proof was shortened by Andrew
Salmon, 27-Aug-2011.) (Contributed by set.mm contributors, 9-Sep-2004.)
(Revised by set.mm contributors, 27-Aug-2011.)
|
⊢ ((R ∩
◡R) ⊆ I ↔
∀x∀y((xRy ∧ yRx) →
x = y)) |
|
Theorem | intirr 5029* |
Two ways of saying a relation is irreflexive. Definition of
irreflexivity in [Schechter] p. 51.
(Contributed by NM, 9-Sep-2004.)
(Revised by Andrew Salmon, 27-Aug-2011.)
|
⊢ ((R ∩ I
) = ∅ ↔ ∀x ¬
xRx) |
|
Theorem | cnvopab 5030* |
The converse of a class abstraction of ordered pairs. (The proof was
shortened by Andrew Salmon, 27-Aug-2011.) (Contributed by set.mm
contributors, 11-Dec-2003.) (Revised by set.mm contributors,
27-Aug-2011.)
|
⊢ ◡{〈x, y〉 ∣ φ} =
{〈y,
x〉 ∣ φ} |
|
Theorem | cnv0 5031 |
The converse of the empty set. (Contributed by set.mm contributors,
6-Apr-1998.)
|
⊢ ◡∅ = ∅ |
|
Theorem | cnvi 5032 |
The converse of the identity relation. Theorem 3.7(ii) of [Monk1]
p. 36. (The proof was shortened by Andrew Salmon, 27-Aug-2011.)
(Contributed by set.mm contributors, 26-Apr-1998.) (Revised by set.mm
contributors, 27-Aug-2011.)
|
⊢ ◡ I =
I |
|
Theorem | cnvun 5033 |
The converse of a union is the union of converses. Theorem 16 of
[Suppes] p. 62. (The proof was shortened
by Andrew Salmon,
27-Aug-2011.) (Contributed by set.mm contributors, 25-Mar-1998.)
(Revised by set.mm contributors, 27-Aug-2011.)
|
⊢ ◡(A
∪ B) = (◡A ∪
◡B) |
|
Theorem | cnvdif 5034 |
Distributive law for converse over set difference. (Contributed by
set.mm contributors, 26-Jun-2014.)
|
⊢ ◡(A
∖ B) =
(◡A ∖ ◡B) |
|
Theorem | cnvin 5035 |
Distributive law for converse over intersection. Theorem 15 of [Suppes]
p. 62. (Contributed by set.mm contributors, 25-Mar-1998.) (Revised by
set.mm contributors, 26-Jun-2014.)
|
⊢ ◡(A
∩ B) = (◡A ∩
◡B) |
|
Theorem | rnun 5036 |
Distributive law for range over union. Theorem 8 of [Suppes] p. 60.
(Contributed by set.mm contributors, 24-Mar-1998.)
|
⊢ ran (A
∪ B) = (ran A ∪ ran B) |
|
Theorem | rnin 5037 |
The range of an intersection belongs the intersection of ranges. Theorem
9 of [Suppes] p. 60. (Contributed by
set.mm contributors,
15-Sep-2004.)
|
⊢ ran (A
∩ B) ⊆ (ran A
∩ ran B) |
|
Theorem | rnuni 5038* |
The range of a union. Part of Exercise 8 of [Enderton] p. 41.
(Contributed by set.mm contributors, 17-Mar-2004.)
|
⊢ ran ∪A = ∪x ∈ A ran x |
|
Theorem | imaundi 5039 |
Distributive law for image over union. Theorem 35 of [Suppes] p. 65.
(Contributed by set.mm contributors, 30-Sep-2002.)
|
⊢ (A “
(B ∪ C)) = ((A
“ B) ∪ (A “ C)) |
|
Theorem | imaundir 5040 |
The image of a union. (Contributed by Jeff Hoffman, 17-Feb-2008.)
|
⊢ ((A ∪
B) “ C) = ((A
“ C) ∪ (B “ C)) |
|
Theorem | dminss 5041 |
An upper bound for intersection with a domain. Theorem 40 of [Suppes]
p. 66, who calls it "somewhat surprising." (Contributed by
set.mm
contributors, 11-Aug-2004.)
|
⊢ (dom R
∩ A) ⊆ (◡R
“ (R “ A)) |
|
Theorem | imainss 5042 |
An upper bound for intersection with an image. Theorem 41 of [Suppes]
p. 66. (Contributed by set.mm contributors, 11-Aug-2004.)
|
⊢ ((R “
A) ∩ B) ⊆ (R “ (A
∩ (◡R “ B))) |
|
Theorem | cnvxp 5043 |
The converse of a cross product. Exercise 11 of [Suppes] p. 67. (The
proof was shortened by Andrew Salmon, 27-Aug-2011.) (Contributed by
set.mm contributors, 14-Aug-1999.) (Revised by set.mm contributors,
27-Aug-2011.)
|
⊢ ◡(A
× B) = (B × A) |
|
Theorem | xp0 5044 |
The cross product with the empty set is empty. Part of Theorem 3.13(ii)
of [Monk1] p. 37. (Contributed by set.mm
contributors, 12-Apr-2004.)
|
⊢ (A ×
∅) = ∅ |
|
Theorem | xpnz 5045 |
The cross product of nonempty classes is nonempty. (Variation of a
theorem contributed by Raph Levien, 30-Jun-2006.) (Contributed by
set.mm contributors, 30-Jun-2006.) (Revised by set.mm contributors,
19-Apr-2007.)
|
⊢ ((A ≠
∅ ∧
B ≠ ∅) ↔ (A
× B) ≠ ∅) |
|
Theorem | xpeq0 5046 |
At least one member of an empty cross product is empty. (Contributed by
set.mm contributors, 27-Aug-2006.)
|
⊢ ((A ×
B) = ∅
↔ (A = ∅ ∨ B = ∅)) |
|
Theorem | xpdisj1 5047 |
Cross products with disjoint sets are disjoint. (Contributed by set.mm
contributors, 13-Sep-2004.)
|
⊢ ((A ∩
B) = ∅
→ ((A × C) ∩ (B
× D)) = ∅) |
|
Theorem | xpdisj2 5048 |
Cross products with disjoint sets are disjoint. (Contributed by set.mm
contributors, 13-Sep-2004.)
|
⊢ ((A ∩
B) = ∅
→ ((C × A) ∩ (D
× B)) = ∅) |
|
Theorem | xpsndisj 5049 |
Cross products with two different singletons are disjoint. (Contributed
by set.mm contributors, 28-Jul-2004.) (Revised by set.mm contributors,
3-Jun-2007.)
|
⊢ (B ≠
D → ((A × {B})
∩ (C × {D})) = ∅) |
|
Theorem | resdisj 5050 |
A double restriction to disjoint classes is the empty set. (The proof was
shortened by Andrew Salmon, 27-Aug-2011.) (Contributed by set.mm
contributors, 7-Oct-2004.) (Revised by set.mm contributors,
27-Aug-2011.)
|
⊢ ((A ∩
B) = ∅
→ ((C ↾ A) ↾ B) = ∅) |
|
Theorem | rnxp 5051 |
The range of a cross product. Part of Theorem 3.13(x) of [Monk1] p. 37.
(Contributed by set.mm contributors, 12-Apr-2004.) (Revised by set.mm
contributors, 9-Apr-2007.)
|
⊢ (A ≠
∅ → ran (A × B) =
B) |
|
Theorem | dmxpss 5052 |
The domain of a cross product is a subclass of the first factor.
(Contributed by set.mm contributors, 19-Mar-2007.)
|
⊢ dom (A
× B) ⊆ A |
|
Theorem | rnxpss 5053 |
The range of a cross product is a subclass of the second factor. (The
proof was shortened by Andrew Salmon, 27-Aug-2011.) (Contributed by
set.mm contributors, 16-Jan-2006.) (Revised by set.mm contributors,
27-Aug-2011.)
|
⊢ ran (A
× B) ⊆ B |
|
Theorem | rnxpid 5054 |
The range of a square cross product. (Contributed by FL, 17-May-2010.)
|
⊢ ran (A
× A) = A |
|
Theorem | ssxpb 5055 |
A cross-product subclass relationship is equivalent to the relationship
for it components. (Contributed by set.mm contributors, 17-Dec-2008.)
|
⊢ ((A ×
B) ≠ ∅ → ((A
× B) ⊆ (C ×
D) ↔ (A ⊆ C ∧ B ⊆ D))) |
|
Theorem | xp11 5056 |
The cross product of nonempty classes is one-to-one. (Contributed by
set.mm contributors, 31-May-2008.)
|
⊢ ((A ≠
∅ ∧
B ≠ ∅) → ((A
× B) = (C × D)
↔ (A = C ∧ B = D))) |
|
Theorem | xpcan 5057 |
Cancellation law for cross-product. (Contributed by set.mm contributors,
30-Aug-2011.)
|
⊢ (C ≠
∅ → ((C × A) =
(C × B) ↔ A =
B)) |
|
Theorem | xpcan2 5058 |
Cancellation law for cross-product. (Contributed by set.mm contributors,
30-Aug-2011.)
|
⊢ (C ≠
∅ → ((A × C) =
(B × C) ↔ A =
B)) |
|
Theorem | ssrnres 5059 |
Subset of the range of a restriction. (Contributed by set.mm
contributors, 16-Jan-2006.)
|
⊢ (B ⊆ ran (C
↾ A)
↔ ran (C ∩ (A × B)) =
B) |
|
Theorem | rninxp 5060* |
Range of the intersection with a cross product. (The proof was
shortened by Andrew Salmon, 27-Aug-2011.) (Contributed by set.mm
contributors, 17-Jan-2006.) (Revised by set.mm contributors,
27-Aug-2011.)
|
⊢ (ran (C
∩ (A × B)) = B ↔
∀y
∈ B
∃x
∈ A
xCy) |
|
Theorem | dminxp 5061* |
Domain of the intersection with a cross product. (Contributed by set.mm
contributors, 17-Jan-2006.)
|
⊢ (dom (C
∩ (A × B)) = A ↔
∀x
∈ A
∃y
∈ B
xCy) |
|
Theorem | cnvcnv 5062 |
The double converse of a class is the original class. (Contributed by
Scott Fenton, 17-Apr-2021.)
|
⊢ ◡◡R =
R |
|
Theorem | cnveqb 5063 |
Equality theorem for converse. (Contributed by FL, 19-Sep-2011.)
(Revised by Scott Fenton, 17-Apr-2021.)
|
⊢ (A =
B ↔ ◡A =
◡B) |
|
Theorem | dmsnn0 5064 |
The domain of a singleton is nonzero iff the singleton argument is a
set. (Contributed by NM, 14-Dec-2008.) (Proof shortened by Andrew
Salmon, 27-Aug-2011.) (Revised by Scott Fenton, 19-Apr-2021.)
|
⊢ (A ∈ V ↔ dom {A} ≠ ∅) |
|
Theorem | rnsnn0 5065 |
The range of a singleton is nonzero iff the singleton argument is a set.
(Contributed by set.mm contributors, 14-Dec-2008.) (Revised by Scott
Fenton, 19-Apr-2021.)
|
⊢ (A ∈ V ↔ ran {A} ≠ ∅) |
|
Theorem | dmsnopg 5066 |
The domain of a singleton of an ordered pair is the singleton of the
first member. (Contributed by Mario Carneiro, 26-Apr-2015.)
|
⊢ (B ∈ V → dom
{〈A,
B〉} =
{A}) |
|
Theorem | dmsnopss 5067 |
The domain of a singleton of an ordered pair is a subset of the
singleton of the first member (with no sethood assumptions on B).
(Contributed by Mario Carneiro, 30-Apr-2015.)
|
⊢ dom {〈A, B〉} ⊆ {A} |
|
Theorem | dmpropg 5068 |
The domain of an unordered pair of ordered pairs. (Contributed by Mario
Carneiro, 26-Apr-2015.)
|
⊢ ((B ∈ V ∧ D ∈ W) →
dom {〈A,
B〉,
〈C,
D〉} =
{A, C}) |
|
Theorem | dmsnop 5069 |
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.)
|
⊢ B ∈ V ⇒ ⊢ dom {〈A, B〉} = {A} |
|
Theorem | dmprop 5070 |
The domain of an unordered pair of ordered pairs. (Contributed by NM,
13-Sep-2011.)
|
⊢ B ∈ V
& ⊢ D ∈ V ⇒ ⊢ dom {〈A, B〉, 〈C, D〉} = {A, C} |
|
Theorem | dmtpop 5071 |
The domain of an unordered triple of ordered pairs. (Contributed by NM,
14-Sep-2011.)
|
⊢ B ∈ V
& ⊢ D ∈ V
& ⊢ F ∈ V ⇒ ⊢ dom {〈A, B〉, 〈C, D〉, 〈E, F〉} = {A, C, E} |
|
Theorem | op1sta 5072 |
Extract the first member of an ordered pair. (Contributed by Raph
Levien, 4-Dec-2003.)
|
⊢ A ∈ V
& ⊢ B ∈ V ⇒ ⊢ ∪dom {〈A, B〉} = A |
|
Theorem | cnvsn 5073 |
Converse of a singleton of an ordered pair. (Contributed by NM,
11-May-1998.)
|
⊢ A ∈ V
& ⊢ B ∈ V ⇒ ⊢ ◡{〈A, B〉} = {〈B, A〉} |
|
Theorem | opswap 5074 |
Swap the members of an ordered pair. (Contributed by set.mm
contributors, 14-Dec-2008.)
|
⊢ A ∈ V
& ⊢ B ∈ V ⇒ ⊢ ∪◡{〈A, B〉} = 〈B, A〉 |
|
Theorem | rnsnop 5075 |
The range of a singleton of an ordered pair is the singleton of the
second member. (Contributed by set.mm contributors, 24-Jul-2004.)
|
⊢ A ∈ V ⇒ ⊢ ran {〈A, B〉} = {B} |
|
Theorem | op2nda 5076 |
Extract the second member of an ordered pair. (Contributed by set.mm
contributors, 9-Jan-2015.)
|
⊢ A ∈ V
& ⊢ B ∈ V ⇒ ⊢ ∪ran {〈A, B〉} = B |
|
Theorem | cnvresima 5077 |
An image under the converse of a restriction. (Contributed by Jeff
Hankins, 12-Jul-2009.)
|
⊢ (◡(F
↾ A)
“ B) = ((◡F
“ B) ∩ A) |
|
Theorem | resdmres 5078 |
Restriction to the domain of a restriction. (Contributed by set.mm
contributors, 8-Apr-2007.)
|
⊢ (A ↾ dom (A
↾ B)) =
(A ↾
B) |
|
Theorem | imadmres 5079 |
The image of the domain of a restriction. (Contributed by set.mm
contributors, 8-Apr-2007.)
|
⊢ (A “
dom (A ↾ B)) =
(A “ B) |
|
Theorem | dfco2 5080* |
Alternate definition of a class composition, using only one bound
variable. (Contributed by set.mm contributors, 19-Dec-2008.)
|
⊢ (A ∘ B) =
∪x ∈ V ((◡B
“ {x}) × (A “ {x})) |
|
Theorem | dfco2a 5081* |
Generalization of dfco2 5080, where C can have any value between
dom A ∩ ran B and V. (The proof was
shortened by Andrew
Salmon, 27-Aug-2011.) (Contributed by set.mm contributors,
21-Dec-2008.) (Revised by set.mm contributors, 27-Aug-2011.)
|
⊢ ((dom A
∩ ran B) ⊆ C →
(A ∘
B) = ∪x ∈ C ((◡B
“ {x}) × (A “ {x}))) |
|
Theorem | coundi 5082 |
Class composition distributes over union. (The proof was shortened by
Andrew Salmon, 27-Aug-2011.) (Contributed by set.mm contributors,
21-Dec-2008.) (Revised by set.mm contributors, 27-Aug-2011.)
|
⊢ (A ∘ (B ∪
C)) = ((A ∘ B) ∪ (A
∘ C)) |
|
Theorem | coundir 5083 |
Class composition distributes over union. (The proof was shortened by
Andrew Salmon, 27-Aug-2011.) (Contributed by set.mm contributors,
21-Dec-2008.) (Revised by set.mm contributors, 27-Aug-2011.)
|
⊢ ((A ∪
B) ∘
C) = ((A ∘ C) ∪ (B
∘ C)) |
|
Theorem | cores 5084 |
Restricted first member of a class composition. (The proof was
shortened by Andrew Salmon, 27-Aug-2011.) (Contributed by set.mm
contributors, 12-Oct-2004.) (Revised by set.mm contributors,
27-Aug-2011.)
|
⊢ (ran B
⊆ C
→ ((A ↾ C) ∘ B) =
(A ∘
B)) |
|
Theorem | resco 5085 |
Associative law for the restriction of a composition. (Contributed by
set.mm contributors, 12-Dec-2006.)
|
⊢ ((A ∘ B) ↾ C) =
(A ∘
(B ↾
C)) |
|
Theorem | imaco 5086 |
Image of the composition of two classes. (Contributed by Jason
Orendorff, 12-Dec-2006.)
|
⊢ ((A ∘ B) “
C) = (A “ (B
“ C)) |
|
Theorem | rnco 5087 |
The range of the composition of two classes. (Contributed by set.mm
contributors, 12-Dec-2006.)
|
⊢ ran (A
∘ B) =
ran (A ↾ ran B) |
|
Theorem | rnco2 5088 |
The range of the composition of two classes. (Contributed by set.mm
contributors, 27-Mar-2008.)
|
⊢ ran (A
∘ B) =
(A “ ran B) |
|
Theorem | dmco 5089 |
The domain of a composition. Exercise 27 of [Enderton] p. 53.
(Contributed by set.mm contributors, 4-Feb-2004.)
|
⊢ dom (A
∘ B) =
(◡B “ dom A) |
|
Theorem | coiun 5090* |
Composition with an indexed union. (Contributed by set.mm contributors,
21-Dec-2008.)
|
⊢ (A ∘ ∪x ∈ C B) = ∪x ∈ C (A ∘ B) |
|
Theorem | cores2 5091 |
Absorption of a reverse (preimage) restriction of the second member of a
class composition. (Contributed by set.mm contributors, 11-Dec-2006.)
|
⊢ (dom A
⊆ C
→ (A ∘ ◡(◡B ↾ C)) =
(A ∘
B)) |
|
Theorem | co02 5092 |
Composition with the empty set. Theorem 20 of [Suppes] p. 63.
(Contributed by set.mm contributors, 24-Apr-2004.)
|
⊢ (A ∘ ∅) = ∅ |
|
Theorem | co01 5093 |
Composition with the empty set. (Contributed by set.mm contributors,
24-Apr-2004.)
|
⊢ (∅ ∘ A) = ∅ |
|
Theorem | coi1 5094 |
Composition with the identity relation. Part of Theorem 3.7(i) of
[Monk1] p. 36. (Contributed by set.mm
contributors, 22-Apr-2004.)
(Revised by Scott Fenton, 14-Apr-2021.)
|
⊢ (A ∘ I ) = A |
|
Theorem | coi2 5095 |
Composition with the identity relation. Part of Theorem 3.7(i) of
[Monk1] p. 36. (Contributed by set.mm
contributors, 22-Apr-2004.)
(Revised by Scott Fenton, 17-Apr-2021.)
|
⊢ ( I ∘
A) = A |
|
Theorem | coires1 5096 |
Composition with a restricted identity relation. (Contributed by FL,
19-Jun-2011.) (Revised by Scott Fenton, 17-Apr-2021.)
|
⊢ (A ∘ ( I ↾
B)) = (A ↾ B) |
|
Theorem | coass 5097 |
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 set.mm contributors, 27-Jan-1997.)
|
⊢ ((A ∘ B) ∘ C) =
(A ∘
(B ∘
C)) |
|
Theorem | cnvtr 5098 |
A class is transitive iff its converse is transitive. (Contributed by FL,
19-Sep-2011.) (Revised by Scott Fenton, 18-Apr-2021.)
|
⊢ ((R ∘ R) ⊆ R ↔
(◡R ∘ ◡R)
⊆ ◡R) |
|
Theorem | ssdmrn 5099 |
A class is included in the cross product of its domain and range.
Exercise 4.12(t) of [Mendelson] p.
235. (Contributed by set.mm
contributors, 3-Aug-1994.) (Revised by Scott Fenton, 15-Apr-2021.)
|
⊢ A ⊆ (dom A
× ran A) |
|
Theorem | dfcnv2 5100 |
Definition of converse in terms of image and Swap
. (Contributed by
set.mm contributors, 8-Jan-2015.)
|
⊢ ◡A =
( Swap “ A) |