Theorem List for Intuitionistic Logic Explorer - 5001-5100 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | poirr2 5001 |
A partial order relation is irreflexive. (Contributed by Mario
Carneiro, 2-Nov-2015.)
|
⊢ (𝑅 Po 𝐴 → (𝑅 ∩ ( I ↾ 𝐴)) = ∅) |
|
Theorem | trinxp 5002 |
The relation induced by a transitive relation on a part of its field is
transitive. (Taking the intersection of a relation with a square cross
product is a way to restrict it to a subset of its field.) (Contributed
by FL, 31-Jul-2009.)
|
⊢ ((𝑅 ∘ 𝑅) ⊆ 𝑅 → ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ (𝑅 ∩ (𝐴 × 𝐴))) |
|
Theorem | soirri 5003 |
A strict order relation is irreflexive. (Contributed by NM,
10-Feb-1996.) (Revised by Mario Carneiro, 10-May-2013.)
|
⊢ 𝑅 Or 𝑆
& ⊢ 𝑅 ⊆ (𝑆 × 𝑆) ⇒ ⊢ ¬ 𝐴𝑅𝐴 |
|
Theorem | sotri 5004 |
A strict order relation is a transitive relation. (Contributed by NM,
10-Feb-1996.) (Revised by Mario Carneiro, 10-May-2013.)
|
⊢ 𝑅 Or 𝑆
& ⊢ 𝑅 ⊆ (𝑆 × 𝑆) ⇒ ⊢ ((𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶) → 𝐴𝑅𝐶) |
|
Theorem | son2lpi 5005 |
A strict order relation has no 2-cycle loops. (Contributed by NM,
10-Feb-1996.) (Revised by Mario Carneiro, 10-May-2013.)
|
⊢ 𝑅 Or 𝑆
& ⊢ 𝑅 ⊆ (𝑆 × 𝑆) ⇒ ⊢ ¬ (𝐴𝑅𝐵 ∧ 𝐵𝑅𝐴) |
|
Theorem | sotri2 5006 |
A transitivity relation. (Read ¬ B < A and B
< C implies A < C .)
(Contributed by Mario Carneiro, 10-May-2013.)
|
⊢ 𝑅 Or 𝑆
& ⊢ 𝑅 ⊆ (𝑆 × 𝑆) ⇒ ⊢ ((𝐴 ∈ 𝑆 ∧ ¬ 𝐵𝑅𝐴 ∧ 𝐵𝑅𝐶) → 𝐴𝑅𝐶) |
|
Theorem | sotri3 5007 |
A transitivity relation. (Read A < B and ¬ C
< B implies A < C .)
(Contributed by Mario Carneiro, 10-May-2013.)
|
⊢ 𝑅 Or 𝑆
& ⊢ 𝑅 ⊆ (𝑆 × 𝑆) ⇒ ⊢ ((𝐶 ∈ 𝑆 ∧ 𝐴𝑅𝐵 ∧ ¬ 𝐶𝑅𝐵) → 𝐴𝑅𝐶) |
|
Theorem | poleloe 5008 |
Express "less than or equals" for general strict orders.
(Contributed by
Stefan O'Rear, 17-Jan-2015.)
|
⊢ (𝐵 ∈ 𝑉 → (𝐴(𝑅 ∪ I )𝐵 ↔ (𝐴𝑅𝐵 ∨ 𝐴 = 𝐵))) |
|
Theorem | poltletr 5009 |
Transitive law for general strict orders. (Contributed by Stefan O'Rear,
17-Jan-2015.)
|
⊢ ((𝑅 Po 𝑋 ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝑅𝐵 ∧ 𝐵(𝑅 ∪ I )𝐶) → 𝐴𝑅𝐶)) |
|
Theorem | cnvopab 5010* |
The converse of a class abstraction of ordered pairs. (Contributed by
NM, 11-Dec-2003.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
|
⊢ ◡{〈𝑥, 𝑦〉 ∣ 𝜑} = {〈𝑦, 𝑥〉 ∣ 𝜑} |
|
Theorem | mptcnv 5011* |
The converse of a mapping function. (Contributed by Thierry Arnoux,
16-Jan-2017.)
|
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵) ↔ (𝑦 ∈ 𝐶 ∧ 𝑥 = 𝐷))) ⇒ ⊢ (𝜑 → ◡(𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐶 ↦ 𝐷)) |
|
Theorem | cnv0 5012 |
The converse of the empty set. (Contributed by NM, 6-Apr-1998.)
|
⊢ ◡∅ = ∅ |
|
Theorem | cnvi 5013 |
The converse of the identity relation. Theorem 3.7(ii) of [Monk1]
p. 36. (Contributed by NM, 26-Apr-1998.) (Proof shortened by Andrew
Salmon, 27-Aug-2011.)
|
⊢ ◡ I
= I |
|
Theorem | cnvun 5014 |
The converse of a union is the union of converses. Theorem 16 of
[Suppes] p. 62. (Contributed by NM,
25-Mar-1998.) (Proof shortened by
Andrew Salmon, 27-Aug-2011.)
|
⊢ ◡(𝐴 ∪ 𝐵) = (◡𝐴 ∪ ◡𝐵) |
|
Theorem | cnvdif 5015 |
Distributive law for converse over set difference. (Contributed by
Mario Carneiro, 26-Jun-2014.)
|
⊢ ◡(𝐴 ∖ 𝐵) = (◡𝐴 ∖ ◡𝐵) |
|
Theorem | cnvin 5016 |
Distributive law for converse over intersection. Theorem 15 of [Suppes]
p. 62. (Contributed by NM, 25-Mar-1998.) (Revised by Mario Carneiro,
26-Jun-2014.)
|
⊢ ◡(𝐴 ∩ 𝐵) = (◡𝐴 ∩ ◡𝐵) |
|
Theorem | rnun 5017 |
Distributive law for range over union. Theorem 8 of [Suppes] p. 60.
(Contributed by NM, 24-Mar-1998.)
|
⊢ ran (𝐴 ∪ 𝐵) = (ran 𝐴 ∪ ran 𝐵) |
|
Theorem | rnin 5018 |
The range of an intersection belongs the intersection of ranges. Theorem
9 of [Suppes] p. 60. (Contributed by NM,
15-Sep-2004.)
|
⊢ ran (𝐴 ∩ 𝐵) ⊆ (ran 𝐴 ∩ ran 𝐵) |
|
Theorem | rniun 5019 |
The range of an indexed union. (Contributed by Mario Carneiro,
29-May-2015.)
|
⊢ ran ∪
𝑥 ∈ 𝐴 𝐵 = ∪
𝑥 ∈ 𝐴 ran 𝐵 |
|
Theorem | rnuni 5020* |
The range of a union. Part of Exercise 8 of [Enderton] p. 41.
(Contributed by NM, 17-Mar-2004.) (Revised by Mario Carneiro,
29-May-2015.)
|
⊢ ran ∪ 𝐴 = ∪ 𝑥 ∈ 𝐴 ran 𝑥 |
|
Theorem | imaundi 5021 |
Distributive law for image over union. Theorem 35 of [Suppes] p. 65.
(Contributed by NM, 30-Sep-2002.)
|
⊢ (𝐴 “ (𝐵 ∪ 𝐶)) = ((𝐴 “ 𝐵) ∪ (𝐴 “ 𝐶)) |
|
Theorem | imaundir 5022 |
The image of a union. (Contributed by Jeff Hoffman, 17-Feb-2008.)
|
⊢ ((𝐴 ∪ 𝐵) “ 𝐶) = ((𝐴 “ 𝐶) ∪ (𝐵 “ 𝐶)) |
|
Theorem | dminss 5023 |
An upper bound for intersection with a domain. Theorem 40 of [Suppes]
p. 66, who calls it "somewhat surprising". (Contributed by
NM,
11-Aug-2004.)
|
⊢ (dom 𝑅 ∩ 𝐴) ⊆ (◡𝑅 “ (𝑅 “ 𝐴)) |
|
Theorem | imainss 5024 |
An upper bound for intersection with an image. Theorem 41 of [Suppes]
p. 66. (Contributed by NM, 11-Aug-2004.)
|
⊢ ((𝑅 “ 𝐴) ∩ 𝐵) ⊆ (𝑅 “ (𝐴 ∩ (◡𝑅 “ 𝐵))) |
|
Theorem | inimass 5025 |
The image of an intersection. (Contributed by Thierry Arnoux,
16-Dec-2017.)
|
⊢ ((𝐴 ∩ 𝐵) “ 𝐶) ⊆ ((𝐴 “ 𝐶) ∩ (𝐵 “ 𝐶)) |
|
Theorem | inimasn 5026 |
The intersection of the image of singleton. (Contributed by Thierry
Arnoux, 16-Dec-2017.)
|
⊢ (𝐶 ∈ 𝑉 → ((𝐴 ∩ 𝐵) “ {𝐶}) = ((𝐴 “ {𝐶}) ∩ (𝐵 “ {𝐶}))) |
|
Theorem | cnvxp 5027 |
The converse of a cross product. Exercise 11 of [Suppes] p. 67.
(Contributed by NM, 14-Aug-1999.) (Proof shortened by Andrew Salmon,
27-Aug-2011.)
|
⊢ ◡(𝐴 × 𝐵) = (𝐵 × 𝐴) |
|
Theorem | xp0 5028 |
The cross product with the empty set is empty. Part of Theorem 3.13(ii)
of [Monk1] p. 37. (Contributed by NM,
12-Apr-2004.)
|
⊢ (𝐴 × ∅) =
∅ |
|
Theorem | xpmlem 5029* |
The cross product of inhabited classes is inhabited. (Contributed by
Jim Kingdon, 11-Dec-2018.)
|
⊢ ((∃𝑥 𝑥 ∈ 𝐴 ∧ ∃𝑦 𝑦 ∈ 𝐵) ↔ ∃𝑧 𝑧 ∈ (𝐴 × 𝐵)) |
|
Theorem | xpm 5030* |
The cross product of inhabited classes is inhabited. (Contributed by
Jim Kingdon, 13-Dec-2018.)
|
⊢ ((∃𝑥 𝑥 ∈ 𝐴 ∧ ∃𝑦 𝑦 ∈ 𝐵) ↔ ∃𝑧 𝑧 ∈ (𝐴 × 𝐵)) |
|
Theorem | xpeq0r 5031 |
A cross product is empty if at least one member is empty. (Contributed by
Jim Kingdon, 12-Dec-2018.)
|
⊢ ((𝐴 = ∅ ∨ 𝐵 = ∅) → (𝐴 × 𝐵) = ∅) |
|
Theorem | sqxpeq0 5032 |
A Cartesian square is empty iff its member is empty. (Contributed by Jim
Kingdon, 21-Apr-2023.)
|
⊢ ((𝐴 × 𝐴) = ∅ ↔ 𝐴 = ∅) |
|
Theorem | xpdisj1 5033 |
Cross products with disjoint sets are disjoint. (Contributed by NM,
13-Sep-2004.)
|
⊢ ((𝐴 ∩ 𝐵) = ∅ → ((𝐴 × 𝐶) ∩ (𝐵 × 𝐷)) = ∅) |
|
Theorem | xpdisj2 5034 |
Cross products with disjoint sets are disjoint. (Contributed by NM,
13-Sep-2004.)
|
⊢ ((𝐴 ∩ 𝐵) = ∅ → ((𝐶 × 𝐴) ∩ (𝐷 × 𝐵)) = ∅) |
|
Theorem | xpsndisj 5035 |
Cross products with two different singletons are disjoint. (Contributed
by NM, 28-Jul-2004.)
|
⊢ (𝐵 ≠ 𝐷 → ((𝐴 × {𝐵}) ∩ (𝐶 × {𝐷})) = ∅) |
|
Theorem | djudisj 5036* |
Disjoint unions with disjoint index sets are disjoint. (Contributed by
Stefan O'Rear, 21-Nov-2014.)
|
⊢ ((𝐴 ∩ 𝐵) = ∅ → (∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐶) ∩ ∪
𝑦 ∈ 𝐵 ({𝑦} × 𝐷)) = ∅) |
|
Theorem | resdisj 5037 |
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 5038* |
The range of a cross product. Part of Theorem 3.13(x) of [Monk1] p. 37,
with nonempty changed to inhabited. (Contributed by Jim Kingdon,
12-Dec-2018.)
|
⊢ (∃𝑥 𝑥 ∈ 𝐴 → ran (𝐴 × 𝐵) = 𝐵) |
|
Theorem | dmxpss 5039 |
The domain of a cross product is a subclass of the first factor.
(Contributed by NM, 19-Mar-2007.)
|
⊢ dom (𝐴 × 𝐵) ⊆ 𝐴 |
|
Theorem | rnxpss 5040 |
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 | dmxpss2 5041 |
Upper bound for the domain of a binary relation. (Contributed by BJ,
10-Jul-2022.)
|
⊢ (𝑅 ⊆ (𝐴 × 𝐵) → dom 𝑅 ⊆ 𝐴) |
|
Theorem | rnxpss2 5042 |
Upper bound for the range of a binary relation. (Contributed by BJ,
10-Jul-2022.)
|
⊢ (𝑅 ⊆ (𝐴 × 𝐵) → ran 𝑅 ⊆ 𝐵) |
|
Theorem | rnxpid 5043 |
The range of a square cross product. (Contributed by FL,
17-May-2010.)
|
⊢ ran (𝐴 × 𝐴) = 𝐴 |
|
Theorem | ssxpbm 5044* |
A cross-product subclass relationship is equivalent to the relationship
for its components. (Contributed by Jim Kingdon, 12-Dec-2018.)
|
⊢ (∃𝑥 𝑥 ∈ (𝐴 × 𝐵) → ((𝐴 × 𝐵) ⊆ (𝐶 × 𝐷) ↔ (𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐷))) |
|
Theorem | ssxp1 5045* |
Cross product subset cancellation. (Contributed by Jim Kingdon,
14-Dec-2018.)
|
⊢ (∃𝑥 𝑥 ∈ 𝐶 → ((𝐴 × 𝐶) ⊆ (𝐵 × 𝐶) ↔ 𝐴 ⊆ 𝐵)) |
|
Theorem | ssxp2 5046* |
Cross product subset cancellation. (Contributed by Jim Kingdon,
14-Dec-2018.)
|
⊢ (∃𝑥 𝑥 ∈ 𝐶 → ((𝐶 × 𝐴) ⊆ (𝐶 × 𝐵) ↔ 𝐴 ⊆ 𝐵)) |
|
Theorem | xp11m 5047* |
The cross product of inhabited classes is one-to-one. (Contributed by
Jim Kingdon, 13-Dec-2018.)
|
⊢ ((∃𝑥 𝑥 ∈ 𝐴 ∧ ∃𝑦 𝑦 ∈ 𝐵) → ((𝐴 × 𝐵) = (𝐶 × 𝐷) ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))) |
|
Theorem | xpcanm 5048* |
Cancellation law for cross-product. (Contributed by Jim Kingdon,
14-Dec-2018.)
|
⊢ (∃𝑥 𝑥 ∈ 𝐶 → ((𝐶 × 𝐴) = (𝐶 × 𝐵) ↔ 𝐴 = 𝐵)) |
|
Theorem | xpcan2m 5049* |
Cancellation law for cross-product. (Contributed by Jim Kingdon,
14-Dec-2018.)
|
⊢ (∃𝑥 𝑥 ∈ 𝐶 → ((𝐴 × 𝐶) = (𝐵 × 𝐶) ↔ 𝐴 = 𝐵)) |
|
Theorem | xpexr2m 5050* |
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 5051 |
Subset of the range of a restriction. (Contributed by NM,
16-Jan-2006.)
|
⊢ (𝐵 ⊆ ran (𝐶 ↾ 𝐴) ↔ ran (𝐶 ∩ (𝐴 × 𝐵)) = 𝐵) |
|
Theorem | rninxp 5052* |
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 5053* |
Domain of the intersection with a cross product. (Contributed by NM,
17-Jan-2006.)
|
⊢ (dom (𝐶 ∩ (𝐴 × 𝐵)) = 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥𝐶𝑦) |
|
Theorem | imainrect 5054 |
Image of a relation restricted to a rectangular region. (Contributed by
Stefan O'Rear, 19-Feb-2015.)
|
⊢ ((𝐺 ∩ (𝐴 × 𝐵)) “ 𝑌) = ((𝐺 “ (𝑌 ∩ 𝐴)) ∩ 𝐵) |
|
Theorem | xpima1 5055 |
The image by a cross product. (Contributed by Thierry Arnoux,
16-Dec-2017.)
|
⊢ ((𝐴 ∩ 𝐶) = ∅ → ((𝐴 × 𝐵) “ 𝐶) = ∅) |
|
Theorem | xpima2m 5056* |
The image by a cross product. (Contributed by Thierry Arnoux,
16-Dec-2017.)
|
⊢ (∃𝑥 𝑥 ∈ (𝐴 ∩ 𝐶) → ((𝐴 × 𝐵) “ 𝐶) = 𝐵) |
|
Theorem | xpimasn 5057 |
The image of a singleton by a cross product. (Contributed by Thierry
Arnoux, 14-Jan-2018.)
|
⊢ (𝑋 ∈ 𝐴 → ((𝐴 × 𝐵) “ {𝑋}) = 𝐵) |
|
Theorem | cnvcnv3 5058* |
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 5059 |
Alternate definition of relation. Exercise 2 of [TakeutiZaring] p. 25.
(Contributed by NM, 29-Dec-1996.)
|
⊢ (Rel 𝑅 ↔ ◡◡𝑅 = 𝑅) |
|
Theorem | dfrel4v 5060* |
A relation can be expressed as the set of ordered pairs in it.
(Contributed by Mario Carneiro, 16-Aug-2015.)
|
⊢ (Rel 𝑅 ↔ 𝑅 = {〈𝑥, 𝑦〉 ∣ 𝑥𝑅𝑦}) |
|
Theorem | cnvcnv 5061 |
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 5062 |
The double converse of a class equals its restriction to the universe.
(Contributed by NM, 8-Oct-2007.)
|
⊢ ◡◡𝐴 = (𝐴 ↾ V) |
|
Theorem | cnvcnvss 5063 |
The double converse of a class is a subclass. Exercise 2 of
[TakeutiZaring] p. 25. (Contributed
by NM, 23-Jul-2004.)
|
⊢ ◡◡𝐴 ⊆ 𝐴 |
|
Theorem | cnveqb 5064 |
Equality theorem for converse. (Contributed by FL, 19-Sep-2011.)
|
⊢ ((Rel 𝐴 ∧ Rel 𝐵) → (𝐴 = 𝐵 ↔ ◡𝐴 = ◡𝐵)) |
|
Theorem | cnveq0 5065 |
A relation empty iff its converse is empty. (Contributed by FL,
19-Sep-2011.)
|
⊢ (Rel 𝐴 → (𝐴 = ∅ ↔ ◡𝐴 = ∅)) |
|
Theorem | dfrel3 5066 |
Alternate definition of relation. (Contributed by NM, 14-May-2008.)
|
⊢ (Rel 𝑅 ↔ (𝑅 ↾ V) = 𝑅) |
|
Theorem | dmresv 5067 |
The domain of a universal restriction. (Contributed by NM,
14-May-2008.)
|
⊢ dom (𝐴 ↾ V) = dom 𝐴 |
|
Theorem | rnresv 5068 |
The range of a universal restriction. (Contributed by NM,
14-May-2008.)
|
⊢ ran (𝐴 ↾ V) = ran 𝐴 |
|
Theorem | dfrn4 5069 |
Range defined in terms of image. (Contributed by NM, 14-May-2008.)
|
⊢ ran 𝐴 = (𝐴 “ V) |
|
Theorem | csbrng 5070 |
Distribute proper substitution through the range of a class.
(Contributed by Alan Sare, 10-Nov-2012.)
|
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌ran 𝐵 = ran ⦋𝐴 / 𝑥⦌𝐵) |
|
Theorem | rescnvcnv 5071 |
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 5072 |
The double converse of the restriction of a class. (Contributed by NM,
3-Jun-2007.)
|
⊢ ◡◡(𝐴 ↾ 𝐵) = (◡◡𝐴 ↾ 𝐵) |
|
Theorem | imacnvcnv 5073 |
The image of the double converse of a class. (Contributed by NM,
8-Apr-2007.)
|
⊢ (◡◡𝐴 “ 𝐵) = (𝐴 “ 𝐵) |
|
Theorem | dmsnm 5074* |
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 5075* |
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 5076 |
The domain of the singleton of the empty set is empty. (Contributed by
NM, 30-Jan-2004.)
|
⊢ dom {∅} = ∅ |
|
Theorem | cnvsn0 5077 |
The converse of the singleton of the empty set is empty. (Contributed by
Mario Carneiro, 30-Aug-2015.)
|
⊢ ◡{∅} = ∅ |
|
Theorem | dmsn0el 5078 |
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 5079* |
A singleton is a relation iff it has an inhabited domain. (Contributed
by Jim Kingdon, 16-Dec-2018.)
|
⊢ 𝐴 ∈ V ⇒ ⊢ (Rel {𝐴} ↔ ∃𝑥 𝑥 ∈ dom {𝐴}) |
|
Theorem | dmsnopg 5080 |
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 5081 |
The domain of an unordered pair of ordered pairs. (Contributed by Mario
Carneiro, 26-Apr-2015.)
|
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐷 ∈ 𝑊) → dom {〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉} = {𝐴, 𝐶}) |
|
Theorem | dmsnop 5082 |
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 5083 |
The domain of an unordered pair of ordered pairs. (Contributed by NM,
13-Sep-2011.)
|
⊢ 𝐵 ∈ V & ⊢ 𝐷 ∈
V ⇒ ⊢ dom {〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉} = {𝐴, 𝐶} |
|
Theorem | dmtpop 5084 |
The domain of an unordered triple of ordered pairs. (Contributed by NM,
14-Sep-2011.)
|
⊢ 𝐵 ∈ V & ⊢ 𝐷 ∈ V & ⊢ 𝐹 ∈
V ⇒ ⊢ dom {〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉, 〈𝐸, 𝐹〉} = {𝐴, 𝐶, 𝐸} |
|
Theorem | cnvcnvsn 5085 |
Double converse of a singleton of an ordered pair. (Unlike cnvsn 5091,
this does not need any sethood assumptions on 𝐴 and 𝐵.)
(Contributed by Mario Carneiro, 26-Apr-2015.)
|
⊢ ◡◡{〈𝐴, 𝐵〉} = ◡{〈𝐵, 𝐴〉} |
|
Theorem | dmsnsnsng 5086 |
The domain of the singleton of the singleton of a singleton.
(Contributed by Jim Kingdon, 16-Dec-2018.)
|
⊢ (𝐴 ∈ V → dom {{{𝐴}}} = {𝐴}) |
|
Theorem | rnsnopg 5087 |
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 5088 |
The range of a pair of ordered pairs is the pair of second members.
(Contributed by Thierry Arnoux, 3-Jan-2017.)
|
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ran {〈𝐴, 𝐶〉, 〈𝐵, 𝐷〉} = {𝐶, 𝐷}) |
|
Theorem | rnsnop 5089 |
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 5090 |
Extract the first member of an ordered pair. (See op2nda 5093 to extract
the second member and op1stb 4461 for an alternate version.)
(Contributed
by Raph Levien, 4-Dec-2003.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈
V ⇒ ⊢ ∪
dom {〈𝐴, 𝐵〉} = 𝐴 |
|
Theorem | cnvsn 5091 |
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 5092 |
Extract the second member of an ordered pair. Theorem 5.12(ii) of
[Monk1] p. 52. (See op1stb 4461 to extract the first member and op2nda 5093
for an alternate version.) (Contributed by NM, 25-Nov-2003.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈
V ⇒ ⊢ ∩
∩ ∩ ◡{〈𝐴, 𝐵〉} = 𝐵 |
|
Theorem | op2nda 5093 |
Extract the second member of an ordered pair. (See op1sta 5090 to extract
the first member and op2ndb 5092 for an alternate version.) (Contributed
by NM, 17-Feb-2004.) (Proof shortened by Andrew Salmon,
27-Aug-2011.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈
V ⇒ ⊢ ∪
ran {〈𝐴, 𝐵〉} = 𝐵 |
|
Theorem | cnvsng 5094 |
Converse of a singleton of an ordered pair. (Contributed by NM,
23-Jan-2015.)
|
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ◡{〈𝐴, 𝐵〉} = {〈𝐵, 𝐴〉}) |
|
Theorem | opswapg 5095 |
Swap the members of an ordered pair. (Contributed by Jim Kingdon,
16-Dec-2018.)
|
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ∪ ◡{〈𝐴, 𝐵〉} = 〈𝐵, 𝐴〉) |
|
Theorem | elxp4 5096 |
Membership in a cross product. This version requires no quantifiers or
dummy variables. See also elxp5 5097. (Contributed by NM,
17-Feb-2004.)
|
⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ (𝐴 = 〈∪ dom
{𝐴}, ∪ ran {𝐴}〉 ∧ (∪
dom {𝐴} ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶))) |
|
Theorem | elxp5 5097 |
Membership in a cross product requiring no quantifiers or dummy
variables. Provides a slightly shorter version of elxp4 5096 when the
double intersection does not create class existence problems (caused by
int0 3843). (Contributed by NM, 1-Aug-2004.)
|
⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ (𝐴 = 〈∩ ∩ 𝐴,
∪ ran {𝐴}〉 ∧ (∩
∩ 𝐴 ∈ 𝐵 ∧ ∪ ran
{𝐴} ∈ 𝐶))) |
|
Theorem | cnvresima 5098 |
An image under the converse of a restriction. (Contributed by Jeff
Hankins, 12-Jul-2009.)
|
⊢ (◡(𝐹 ↾ 𝐴) “ 𝐵) = ((◡𝐹 “ 𝐵) ∩ 𝐴) |
|
Theorem | resdm2 5099 |
A class restricted to its domain equals its double converse. (Contributed
by NM, 8-Apr-2007.)
|
⊢ (𝐴 ↾ dom 𝐴) = ◡◡𝐴 |
|
Theorem | resdmres 5100 |
Restriction to the domain of a restriction. (Contributed by NM,
8-Apr-2007.)
|
⊢ (𝐴 ↾ dom (𝐴 ↾ 𝐵)) = (𝐴 ↾ 𝐵) |