Theorem List for Intuitionistic Logic Explorer - 4101-4200 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | pwtr 4101 |
A class is transitive iff its power class is transitive. (Contributed by
Alan Sare, 25-Aug-2011.) (Revised by Mario Carneiro, 15-Jun-2014.)
|
⊢ (Tr 𝐴 ↔ Tr 𝒫 𝐴) |
|
Theorem | ssextss 4102* |
An extensionality-like principle defining subclass in terms of subsets.
(Contributed by NM, 30-Jun-2004.)
|
⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ⊆ 𝐴 → 𝑥 ⊆ 𝐵)) |
|
Theorem | ssext 4103* |
An extensionality-like principle that uses the subset instead of the
membership relation: two classes are equal iff they have the same
subsets. (Contributed by NM, 30-Jun-2004.)
|
⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ⊆ 𝐴 ↔ 𝑥 ⊆ 𝐵)) |
|
Theorem | nssssr 4104* |
Negation of subclass relationship. Compare nssr 3123.
(Contributed by
Jim Kingdon, 17-Sep-2018.)
|
⊢ (∃𝑥(𝑥 ⊆ 𝐴 ∧ ¬ 𝑥 ⊆ 𝐵) → ¬ 𝐴 ⊆ 𝐵) |
|
Theorem | pweqb 4105 |
Classes are equal if and only if their power classes are equal. Exercise
19 of [TakeutiZaring] p. 18.
(Contributed by NM, 13-Oct-1996.)
|
⊢ (𝐴 = 𝐵 ↔ 𝒫 𝐴 = 𝒫 𝐵) |
|
Theorem | intid 4106* |
The intersection of all sets to which a set belongs is the singleton of
that set. (Contributed by NM, 5-Jun-2009.)
|
⊢ 𝐴 ∈ V ⇒ ⊢ ∩
{𝑥 ∣ 𝐴 ∈ 𝑥} = {𝐴} |
|
Theorem | euabex 4107 |
The abstraction of a wff with existential uniqueness exists.
(Contributed by NM, 25-Nov-1994.)
|
⊢ (∃!𝑥𝜑 → {𝑥 ∣ 𝜑} ∈ V) |
|
Theorem | mss 4108* |
An inhabited class (even if proper) has an inhabited subset.
(Contributed by Jim Kingdon, 17-Sep-2018.)
|
⊢ (∃𝑦 𝑦 ∈ 𝐴 → ∃𝑥(𝑥 ⊆ 𝐴 ∧ ∃𝑧 𝑧 ∈ 𝑥)) |
|
Theorem | exss 4109* |
Restricted existence in a class (even if proper) implies restricted
existence in a subset. (Contributed by NM, 23-Aug-2003.)
|
⊢ (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑦(𝑦 ⊆ 𝐴 ∧ ∃𝑥 ∈ 𝑦 𝜑)) |
|
Theorem | opexg 4110 |
An ordered pair of sets is a set. (Contributed by Jim Kingdon,
11-Jan-2019.)
|
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 〈𝐴, 𝐵〉 ∈ V) |
|
Theorem | opex 4111 |
An ordered pair of sets is a set. (Contributed by Jim Kingdon,
24-Sep-2018.) (Revised by Mario Carneiro, 24-May-2019.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈
V ⇒ ⊢ 〈𝐴, 𝐵〉 ∈ V |
|
Theorem | otexg 4112 |
An ordered triple of sets is a set. (Contributed by Jim Kingdon,
19-Sep-2018.)
|
⊢ ((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → 〈𝐴, 𝐵, 𝐶〉 ∈ V) |
|
Theorem | elop 4113 |
An ordered pair has two elements. Exercise 3 of [TakeutiZaring] p. 15.
(Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro,
26-Apr-2015.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈
V ⇒ ⊢ (𝐴 ∈ 〈𝐵, 𝐶〉 ↔ (𝐴 = {𝐵} ∨ 𝐴 = {𝐵, 𝐶})) |
|
Theorem | opi1 4114 |
One of the two elements in an ordered pair. (Contributed by NM,
5-Aug-1993.) (Revised by Mario Carneiro, 26-Apr-2015.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈
V ⇒ ⊢ {𝐴} ∈ 〈𝐴, 𝐵〉 |
|
Theorem | opi2 4115 |
One of the two elements of an ordered pair. (Contributed by NM,
5-Aug-1993.) (Revised by Mario Carneiro, 26-Apr-2015.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈
V ⇒ ⊢ {𝐴, 𝐵} ∈ 〈𝐴, 𝐵〉 |
|
2.3.4 Ordered pair theorem
|
|
Theorem | opm 4116* |
An ordered pair is inhabited iff the arguments are sets. (Contributed
by Jim Kingdon, 21-Sep-2018.)
|
⊢ (∃𝑥 𝑥 ∈ 〈𝐴, 𝐵〉 ↔ (𝐴 ∈ V ∧ 𝐵 ∈ V)) |
|
Theorem | opnzi 4117 |
An ordered pair is nonempty if the arguments are sets (it is also
inhabited; see opm 4116). (Contributed by Mario Carneiro,
26-Apr-2015.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈
V ⇒ ⊢ 〈𝐴, 𝐵〉 ≠ ∅ |
|
Theorem | opth1 4118 |
Equality of the first members of equal ordered pairs. (Contributed by
NM, 28-May-2008.) (Revised by Mario Carneiro, 26-Apr-2015.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈
V ⇒ ⊢ (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 → 𝐴 = 𝐶) |
|
Theorem | opth 4119 |
The ordered pair theorem. If two ordered pairs are equal, their first
elements are equal and their second elements are equal. Exercise 6 of
[TakeutiZaring] p. 16. Note that
𝐶
and 𝐷 are not required to be
sets due our specific ordered pair definition. (Contributed by NM,
28-May-1995.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈
V ⇒ ⊢ (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)) |
|
Theorem | opthg 4120 |
Ordered pair theorem. 𝐶 and 𝐷 are not required to be
sets under
our specific ordered pair definition. (Contributed by NM, 14-Oct-2005.)
(Revised by Mario Carneiro, 26-Apr-2015.)
|
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))) |
|
Theorem | opthg2 4121 |
Ordered pair theorem. (Contributed by NM, 14-Oct-2005.) (Revised by
Mario Carneiro, 26-Apr-2015.)
|
⊢ ((𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑊) → (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))) |
|
Theorem | opth2 4122 |
Ordered pair theorem. (Contributed by NM, 21-Sep-2014.)
|
⊢ 𝐶 ∈ V & ⊢ 𝐷 ∈
V ⇒ ⊢ (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)) |
|
Theorem | otth2 4123 |
Ordered triple theorem, with triple express with ordered pairs.
(Contributed by NM, 1-May-1995.) (Revised by Mario Carneiro,
26-Apr-2015.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝑅 ∈
V ⇒ ⊢ (〈〈𝐴, 𝐵〉, 𝑅〉 = 〈〈𝐶, 𝐷〉, 𝑆〉 ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ∧ 𝑅 = 𝑆)) |
|
Theorem | otth 4124 |
Ordered triple theorem. (Contributed by NM, 25-Sep-2014.) (Revised by
Mario Carneiro, 26-Apr-2015.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝑅 ∈
V ⇒ ⊢ (〈𝐴, 𝐵, 𝑅〉 = 〈𝐶, 𝐷, 𝑆〉 ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ∧ 𝑅 = 𝑆)) |
|
Theorem | eqvinop 4125* |
A variable introduction law for ordered pairs. Analog of Lemma 15 of
[Monk2] p. 109. (Contributed by NM,
28-May-1995.)
|
⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈
V ⇒ ⊢ (𝐴 = 〈𝐵, 𝐶〉 ↔ ∃𝑥∃𝑦(𝐴 = 〈𝑥, 𝑦〉 ∧ 〈𝑥, 𝑦〉 = 〈𝐵, 𝐶〉)) |
|
Theorem | copsexg 4126* |
Substitution of class 𝐴 for ordered pair 〈𝑥, 𝑦〉.
(Contributed by NM, 27-Dec-1996.) (Revised by Andrew Salmon,
11-Jul-2011.)
|
⊢ (𝐴 = 〈𝑥, 𝑦〉 → (𝜑 ↔ ∃𝑥∃𝑦(𝐴 = 〈𝑥, 𝑦〉 ∧ 𝜑))) |
|
Theorem | copsex2t 4127* |
Closed theorem form of copsex2g 4128. (Contributed by NM,
17-Feb-2013.)
|
⊢ ((∀𝑥∀𝑦((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊)) → (∃𝑥∃𝑦(〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 ∧ 𝜑) ↔ 𝜓)) |
|
Theorem | copsex2g 4128* |
Implicit substitution inference for ordered pairs. (Contributed by NM,
28-May-1995.)
|
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∃𝑥∃𝑦(〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 ∧ 𝜑) ↔ 𝜓)) |
|
Theorem | copsex4g 4129* |
An implicit substitution inference for 2 ordered pairs. (Contributed by
NM, 5-Aug-1995.)
|
⊢ (((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∧ (𝑧 = 𝐶 ∧ 𝑤 = 𝐷)) → (𝜑 ↔ 𝜓)) ⇒ ⊢ (((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑅 ∧ 𝐷 ∈ 𝑆)) → (∃𝑥∃𝑦∃𝑧∃𝑤((〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 ∧ 〈𝐶, 𝐷〉 = 〈𝑧, 𝑤〉) ∧ 𝜑) ↔ 𝜓)) |
|
Theorem | 0nelop 4130 |
A property of ordered pairs. (Contributed by Mario Carneiro,
26-Apr-2015.)
|
⊢ ¬ ∅ ∈ 〈𝐴, 𝐵〉 |
|
Theorem | opeqex 4131 |
Equivalence of existence implied by equality of ordered pairs.
(Contributed by NM, 28-May-2008.)
|
⊢ (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 → ((𝐴 ∈ V ∧ 𝐵 ∈ V) ↔ (𝐶 ∈ V ∧ 𝐷 ∈ V))) |
|
Theorem | opcom 4132 |
An ordered pair commutes iff its members are equal. (Contributed by NM,
28-May-2009.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈
V ⇒ ⊢ (〈𝐴, 𝐵〉 = 〈𝐵, 𝐴〉 ↔ 𝐴 = 𝐵) |
|
Theorem | moop2 4133* |
"At most one" property of an ordered pair. (Contributed by NM,
11-Apr-2004.) (Revised by Mario Carneiro, 26-Apr-2015.)
|
⊢ 𝐵 ∈ V ⇒ ⊢ ∃*𝑥 𝐴 = 〈𝐵, 𝑥〉 |
|
Theorem | opeqsn 4134 |
Equivalence for an ordered pair equal to a singleton. (Contributed by
NM, 3-Jun-2008.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈
V ⇒ ⊢ (〈𝐴, 𝐵〉 = {𝐶} ↔ (𝐴 = 𝐵 ∧ 𝐶 = {𝐴})) |
|
Theorem | opeqpr 4135 |
Equivalence for an ordered pair equal to an unordered pair.
(Contributed by NM, 3-Jun-2008.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V & ⊢ 𝐷 ∈
V ⇒ ⊢ (〈𝐴, 𝐵〉 = {𝐶, 𝐷} ↔ ((𝐶 = {𝐴} ∧ 𝐷 = {𝐴, 𝐵}) ∨ (𝐶 = {𝐴, 𝐵} ∧ 𝐷 = {𝐴}))) |
|
Theorem | euotd 4136* |
Prove existential uniqueness for an ordered triple. (Contributed by
Mario Carneiro, 20-May-2015.)
|
⊢ (𝜑 → 𝐴 ∈ V) & ⊢ (𝜑 → 𝐵 ∈ V) & ⊢ (𝜑 → 𝐶 ∈ V) & ⊢ (𝜑 → (𝜓 ↔ (𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ∧ 𝑐 = 𝐶))) ⇒ ⊢ (𝜑 → ∃!𝑥∃𝑎∃𝑏∃𝑐(𝑥 = 〈𝑎, 𝑏, 𝑐〉 ∧ 𝜓)) |
|
Theorem | uniop 4137 |
The union of an ordered pair. Theorem 65 of [Suppes] p. 39.
(Contributed by NM, 17-Aug-2004.) (Revised by Mario Carneiro,
26-Apr-2015.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈
V ⇒ ⊢ ∪
〈𝐴, 𝐵〉 = {𝐴, 𝐵} |
|
Theorem | uniopel 4138 |
Ordered pair membership is inherited by class union. (Contributed by
NM, 13-May-2008.) (Revised by Mario Carneiro, 26-Apr-2015.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈
V ⇒ ⊢ (〈𝐴, 𝐵〉 ∈ 𝐶 → ∪
〈𝐴, 𝐵〉 ∈ ∪
𝐶) |
|
2.3.5 Ordered-pair class abstractions
(cont.)
|
|
Theorem | opabid 4139 |
The law of concretion. Special case of Theorem 9.5 of [Quine] p. 61.
(Contributed by NM, 14-Apr-1995.) (Proof shortened by Andrew Salmon,
25-Jul-2011.)
|
⊢ (〈𝑥, 𝑦〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ↔ 𝜑) |
|
Theorem | elopab 4140* |
Membership in a class abstraction of pairs. (Contributed by NM,
24-Mar-1998.)
|
⊢ (𝐴 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ↔ ∃𝑥∃𝑦(𝐴 = 〈𝑥, 𝑦〉 ∧ 𝜑)) |
|
Theorem | opelopabsbALT 4141* |
The law of concretion in terms of substitutions. Less general than
opelopabsb 4142, but having a much shorter proof.
(Contributed by NM,
30-Sep-2002.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
(New usage is discouraged.) (Proof modification is discouraged.)
|
⊢ (〈𝑧, 𝑤〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ↔ [𝑤 / 𝑦][𝑧 / 𝑥]𝜑) |
|
Theorem | opelopabsb 4142* |
The law of concretion in terms of substitutions. (Contributed by NM,
30-Sep-2002.) (Revised by Mario Carneiro, 18-Nov-2016.)
|
⊢ (〈𝐴, 𝐵〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ↔ [𝐴 / 𝑥][𝐵 / 𝑦]𝜑) |
|
Theorem | brabsb 4143* |
The law of concretion in terms of substitutions. (Contributed by NM,
17-Mar-2008.)
|
⊢ 𝑅 = {〈𝑥, 𝑦〉 ∣ 𝜑} ⇒ ⊢ (𝐴𝑅𝐵 ↔ [𝐴 / 𝑥][𝐵 / 𝑦]𝜑) |
|
Theorem | opelopabt 4144* |
Closed theorem form of opelopab 4153. (Contributed by NM,
19-Feb-2013.)
|
⊢ ((∀𝑥∀𝑦(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ ∀𝑥∀𝑦(𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊)) → (〈𝐴, 𝐵〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ↔ 𝜒)) |
|
Theorem | opelopabga 4145* |
The law of concretion. Theorem 9.5 of [Quine] p.
61. (Contributed by
Mario Carneiro, 19-Dec-2013.)
|
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (〈𝐴, 𝐵〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ↔ 𝜓)) |
|
Theorem | brabga 4146* |
The law of concretion for a binary relation. (Contributed by Mario
Carneiro, 19-Dec-2013.)
|
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) & ⊢ 𝑅 = {〈𝑥, 𝑦〉 ∣ 𝜑} ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴𝑅𝐵 ↔ 𝜓)) |
|
Theorem | opelopab2a 4147* |
Ordered pair membership in an ordered pair class abstraction.
(Contributed by Mario Carneiro, 19-Dec-2013.)
|
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (〈𝐴, 𝐵〉 ∈ {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) ∧ 𝜑)} ↔ 𝜓)) |
|
Theorem | opelopaba 4148* |
The law of concretion. Theorem 9.5 of [Quine] p.
61. (Contributed by
Mario Carneiro, 19-Dec-2013.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) ⇒ ⊢ (〈𝐴, 𝐵〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ↔ 𝜓) |
|
Theorem | braba 4149* |
The law of concretion for a binary relation. (Contributed by NM,
19-Dec-2013.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) & ⊢ 𝑅 = {〈𝑥, 𝑦〉 ∣ 𝜑} ⇒ ⊢ (𝐴𝑅𝐵 ↔ 𝜓) |
|
Theorem | opelopabg 4150* |
The law of concretion. Theorem 9.5 of [Quine] p.
61. (Contributed by
NM, 28-May-1995.) (Revised by Mario Carneiro, 19-Dec-2013.)
|
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (〈𝐴, 𝐵〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ↔ 𝜒)) |
|
Theorem | brabg 4151* |
The law of concretion for a binary relation. (Contributed by NM,
16-Aug-1999.) (Revised by Mario Carneiro, 19-Dec-2013.)
|
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ 𝑅 = {〈𝑥, 𝑦〉 ∣ 𝜑} ⇒ ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴𝑅𝐵 ↔ 𝜒)) |
|
Theorem | opelopab2 4152* |
Ordered pair membership in an ordered pair class abstraction.
(Contributed by NM, 14-Oct-2007.) (Revised by Mario Carneiro,
19-Dec-2013.)
|
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) ⇒ ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (〈𝐴, 𝐵〉 ∈ {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) ∧ 𝜑)} ↔ 𝜒)) |
|
Theorem | opelopab 4153* |
The law of concretion. Theorem 9.5 of [Quine] p.
61. (Contributed by
NM, 16-May-1995.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (〈𝐴, 𝐵〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ↔ 𝜒) |
|
Theorem | brab 4154* |
The law of concretion for a binary relation. (Contributed by NM,
16-Aug-1999.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ 𝑅 = {〈𝑥, 𝑦〉 ∣ 𝜑} ⇒ ⊢ (𝐴𝑅𝐵 ↔ 𝜒) |
|
Theorem | opelopabaf 4155* |
The law of concretion. Theorem 9.5 of [Quine] p.
61. This version of
opelopab 4153 uses bound-variable hypotheses in place of
distinct variable
conditions." (Contributed by Mario Carneiro, 19-Dec-2013.) (Proof
shortened by Mario Carneiro, 18-Nov-2016.)
|
⊢ Ⅎ𝑥𝜓
& ⊢ Ⅎ𝑦𝜓
& ⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) ⇒ ⊢ (〈𝐴, 𝐵〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ↔ 𝜓) |
|
Theorem | opelopabf 4156* |
The law of concretion. Theorem 9.5 of [Quine] p.
61. This version of
opelopab 4153 uses bound-variable hypotheses in place of
distinct variable
conditions." (Contributed by NM, 19-Dec-2008.)
|
⊢ Ⅎ𝑥𝜓
& ⊢ Ⅎ𝑦𝜒
& ⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (〈𝐴, 𝐵〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ↔ 𝜒) |
|
Theorem | ssopab2 4157 |
Equivalence of ordered pair abstraction subclass and implication.
(Contributed by NM, 27-Dec-1996.) (Revised by Mario Carneiro,
19-May-2013.)
|
⊢ (∀𝑥∀𝑦(𝜑 → 𝜓) → {〈𝑥, 𝑦〉 ∣ 𝜑} ⊆ {〈𝑥, 𝑦〉 ∣ 𝜓}) |
|
Theorem | ssopab2b 4158 |
Equivalence of ordered pair abstraction subclass and implication.
(Contributed by NM, 27-Dec-1996.) (Proof shortened by Mario Carneiro,
18-Nov-2016.)
|
⊢ ({〈𝑥, 𝑦〉 ∣ 𝜑} ⊆ {〈𝑥, 𝑦〉 ∣ 𝜓} ↔ ∀𝑥∀𝑦(𝜑 → 𝜓)) |
|
Theorem | ssopab2i 4159 |
Inference of ordered pair abstraction subclass from implication.
(Contributed by NM, 5-Apr-1995.)
|
⊢ (𝜑 → 𝜓) ⇒ ⊢ {〈𝑥, 𝑦〉 ∣ 𝜑} ⊆ {〈𝑥, 𝑦〉 ∣ 𝜓} |
|
Theorem | ssopab2dv 4160* |
Inference of ordered pair abstraction subclass from implication.
(Contributed by NM, 19-Jan-2014.) (Revised by Mario Carneiro,
24-Jun-2014.)
|
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → {〈𝑥, 𝑦〉 ∣ 𝜓} ⊆ {〈𝑥, 𝑦〉 ∣ 𝜒}) |
|
Theorem | eqopab2b 4161 |
Equivalence of ordered pair abstraction equality and biconditional.
(Contributed by Mario Carneiro, 4-Jan-2017.)
|
⊢ ({〈𝑥, 𝑦〉 ∣ 𝜑} = {〈𝑥, 𝑦〉 ∣ 𝜓} ↔ ∀𝑥∀𝑦(𝜑 ↔ 𝜓)) |
|
Theorem | opabm 4162* |
Inhabited ordered pair class abstraction. (Contributed by Jim Kingdon,
29-Sep-2018.)
|
⊢ (∃𝑧 𝑧 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ↔ ∃𝑥∃𝑦𝜑) |
|
Theorem | iunopab 4163* |
Move indexed union inside an ordered-pair abstraction. (Contributed by
Stefan O'Rear, 20-Feb-2015.)
|
⊢ ∪ 𝑧 ∈ 𝐴 {〈𝑥, 𝑦〉 ∣ 𝜑} = {〈𝑥, 𝑦〉 ∣ ∃𝑧 ∈ 𝐴 𝜑} |
|
2.3.6 Power class of union and
intersection
|
|
Theorem | pwin 4164 |
The power class of the intersection of two classes is the intersection
of their power classes. Exercise 4.12(j) of [Mendelson] p. 235.
(Contributed by NM, 23-Nov-2003.)
|
⊢ 𝒫 (𝐴 ∩ 𝐵) = (𝒫 𝐴 ∩ 𝒫 𝐵) |
|
Theorem | pwunss 4165 |
The power class of the union of two classes includes the union of their
power classes. Exercise 4.12(k) of [Mendelson] p. 235. (Contributed by
NM, 23-Nov-2003.)
|
⊢ (𝒫 𝐴 ∪ 𝒫 𝐵) ⊆ 𝒫 (𝐴 ∪ 𝐵) |
|
Theorem | pwssunim 4166 |
The power class of the union of two classes is a subset of the union of
their power classes, if one class is a subclass of the other. One
direction of Exercise 4.12(l) of [Mendelson] p. 235. (Contributed by
Jim Kingdon, 30-Sep-2018.)
|
⊢ ((𝐴 ⊆ 𝐵 ∨ 𝐵 ⊆ 𝐴) → 𝒫 (𝐴 ∪ 𝐵) ⊆ (𝒫 𝐴 ∪ 𝒫 𝐵)) |
|
Theorem | pwundifss 4167 |
Break up the power class of a union into a union of smaller classes.
(Contributed by Jim Kingdon, 30-Sep-2018.)
|
⊢ ((𝒫 (𝐴 ∪ 𝐵) ∖ 𝒫 𝐴) ∪ 𝒫 𝐴) ⊆ 𝒫 (𝐴 ∪ 𝐵) |
|
Theorem | pwunim 4168 |
The power class of the union of two classes equals the union of their
power classes, iff one class is a subclass of the other. Part of Exercise
7(b) of [Enderton] p. 28. (Contributed
by Jim Kingdon, 30-Sep-2018.)
|
⊢ ((𝐴 ⊆ 𝐵 ∨ 𝐵 ⊆ 𝐴) → 𝒫 (𝐴 ∪ 𝐵) = (𝒫 𝐴 ∪ 𝒫 𝐵)) |
|
2.3.7 Epsilon and identity
relations
|
|
Syntax | cep 4169 |
Extend class notation to include the epsilon relation.
|
class E |
|
Syntax | cid 4170 |
Extend the definition of a class to include identity relation.
|
class I |
|
Definition | df-eprel 4171* |
Define the epsilon relation. Similar to Definition 6.22 of
[TakeutiZaring] p. 30. The
epsilon relation and set membership are the
same, that is, (𝐴 E 𝐵 ↔ 𝐴 ∈ 𝐵) when 𝐵 is a set by
epelg 4172. Thus, 5 E { 1 , 5
}. (Contributed by NM,
13-Aug-1995.)
|
⊢ E = {〈𝑥, 𝑦〉 ∣ 𝑥 ∈ 𝑦} |
|
Theorem | epelg 4172 |
The epsilon relation and membership are the same. General version of
epel 4174. (Contributed by Scott Fenton, 27-Mar-2011.)
(Revised by Mario
Carneiro, 28-Apr-2015.)
|
⊢ (𝐵 ∈ 𝑉 → (𝐴 E 𝐵 ↔ 𝐴 ∈ 𝐵)) |
|
Theorem | epelc 4173 |
The epsilon relationship and the membership relation are the same.
(Contributed by Scott Fenton, 11-Apr-2012.)
|
⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴 E 𝐵 ↔ 𝐴 ∈ 𝐵) |
|
Theorem | epel 4174 |
The epsilon relation and the membership relation are the same.
(Contributed by NM, 13-Aug-1995.)
|
⊢ (𝑥 E 𝑦 ↔ 𝑥 ∈ 𝑦) |
|
Definition | df-id 4175* |
Define the identity relation. Definition 9.15 of [Quine] p. 64. For
example, 5 I 5 and ¬
4 I 5. (Contributed by NM,
13-Aug-1995.)
|
⊢ I = {〈𝑥, 𝑦〉 ∣ 𝑥 = 𝑦} |
|
2.3.8 Partial and complete ordering
|
|
Syntax | wpo 4176 |
Extend wff notation to include the strict partial ordering predicate.
Read: ' 𝑅 is a partial order on 𝐴.'
|
wff 𝑅 Po 𝐴 |
|
Syntax | wor 4177 |
Extend wff notation to include the strict linear ordering predicate.
Read: ' 𝑅 orders 𝐴.'
|
wff 𝑅 Or 𝐴 |
|
Definition | df-po 4178* |
Define the strict partial order predicate. Definition of [Enderton]
p. 168. The expression 𝑅 Po 𝐴 means 𝑅 is a partial order on
𝐴. (Contributed by NM, 16-Mar-1997.)
|
⊢ (𝑅 Po 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧))) |
|
Definition | df-iso 4179* |
Define the strict linear order predicate. The expression 𝑅 Or 𝐴 is
true if relationship 𝑅 orders 𝐴. The property
𝑥𝑅𝑦 → (𝑥𝑅𝑧 ∨ 𝑧𝑅𝑦) is called weak linearity by
Proposition
11.2.3 of [HoTT], p. (varies). If we
assumed excluded middle, it would
be equivalent to trichotomy, 𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥. (Contributed
by NM, 21-Jan-1996.) (Revised by Jim Kingdon, 4-Oct-2018.)
|
⊢ (𝑅 Or 𝐴 ↔ (𝑅 Po 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (𝑥𝑅𝑦 → (𝑥𝑅𝑧 ∨ 𝑧𝑅𝑦)))) |
|
Theorem | poss 4180 |
Subset theorem for the partial ordering predicate. (Contributed by NM,
27-Mar-1997.) (Proof shortened by Mario Carneiro, 18-Nov-2016.)
|
⊢ (𝐴 ⊆ 𝐵 → (𝑅 Po 𝐵 → 𝑅 Po 𝐴)) |
|
Theorem | poeq1 4181 |
Equality theorem for partial ordering predicate. (Contributed by NM,
27-Mar-1997.)
|
⊢ (𝑅 = 𝑆 → (𝑅 Po 𝐴 ↔ 𝑆 Po 𝐴)) |
|
Theorem | poeq2 4182 |
Equality theorem for partial ordering predicate. (Contributed by NM,
27-Mar-1997.)
|
⊢ (𝐴 = 𝐵 → (𝑅 Po 𝐴 ↔ 𝑅 Po 𝐵)) |
|
Theorem | nfpo 4183 |
Bound-variable hypothesis builder for partial orders. (Contributed by
Stefan O'Rear, 20-Jan-2015.)
|
⊢ Ⅎ𝑥𝑅
& ⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥 𝑅 Po 𝐴 |
|
Theorem | nfso 4184 |
Bound-variable hypothesis builder for total orders. (Contributed by
Stefan O'Rear, 20-Jan-2015.)
|
⊢ Ⅎ𝑥𝑅
& ⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥 𝑅 Or 𝐴 |
|
Theorem | pocl 4185 |
Properties of partial order relation in class notation. (Contributed by
NM, 27-Mar-1997.)
|
⊢ (𝑅 Po 𝐴 → ((𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴) → (¬ 𝐵𝑅𝐵 ∧ ((𝐵𝑅𝐶 ∧ 𝐶𝑅𝐷) → 𝐵𝑅𝐷)))) |
|
Theorem | ispod 4186* |
Sufficient conditions for a partial order. (Contributed by NM,
9-Jul-2014.)
|
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ¬ 𝑥𝑅𝑥)
& ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)) ⇒ ⊢ (𝜑 → 𝑅 Po 𝐴) |
|
Theorem | swopolem 4187* |
Perform the substitutions into the strict weak ordering law.
(Contributed by Mario Carneiro, 31-Dec-2014.)
|
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → (𝑥𝑅𝑦 → (𝑥𝑅𝑧 ∨ 𝑧𝑅𝑦))) ⇒ ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑍 ∈ 𝐴)) → (𝑋𝑅𝑌 → (𝑋𝑅𝑍 ∨ 𝑍𝑅𝑌))) |
|
Theorem | swopo 4188* |
A strict weak order is a partial order. (Contributed by Mario Carneiro,
9-Jul-2014.)
|
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → (𝑦𝑅𝑧 → ¬ 𝑧𝑅𝑦))
& ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → (𝑥𝑅𝑦 → (𝑥𝑅𝑧 ∨ 𝑧𝑅𝑦))) ⇒ ⊢ (𝜑 → 𝑅 Po 𝐴) |
|
Theorem | poirr 4189 |
A partial order relation is irreflexive. (Contributed by NM,
27-Mar-1997.)
|
⊢ ((𝑅 Po 𝐴 ∧ 𝐵 ∈ 𝐴) → ¬ 𝐵𝑅𝐵) |
|
Theorem | potr 4190 |
A partial order relation is a transitive relation. (Contributed by NM,
27-Mar-1997.)
|
⊢ ((𝑅 Po 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → ((𝐵𝑅𝐶 ∧ 𝐶𝑅𝐷) → 𝐵𝑅𝐷)) |
|
Theorem | po2nr 4191 |
A partial order relation has no 2-cycle loops. (Contributed by NM,
27-Mar-1997.)
|
⊢ ((𝑅 Po 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → ¬ (𝐵𝑅𝐶 ∧ 𝐶𝑅𝐵)) |
|
Theorem | po3nr 4192 |
A partial order relation has no 3-cycle loops. (Contributed by NM,
27-Mar-1997.)
|
⊢ ((𝑅 Po 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → ¬ (𝐵𝑅𝐶 ∧ 𝐶𝑅𝐷 ∧ 𝐷𝑅𝐵)) |
|
Theorem | po0 4193 |
Any relation is a partial ordering of the empty set. (Contributed by
NM, 28-Mar-1997.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
|
⊢ 𝑅 Po ∅ |
|
Theorem | pofun 4194* |
A function preserves a partial order relation. (Contributed by Jeff
Madsen, 18-Jun-2011.)
|
⊢ 𝑆 = {〈𝑥, 𝑦〉 ∣ 𝑋𝑅𝑌}
& ⊢ (𝑥 = 𝑦 → 𝑋 = 𝑌) ⇒ ⊢ ((𝑅 Po 𝐵 ∧ ∀𝑥 ∈ 𝐴 𝑋 ∈ 𝐵) → 𝑆 Po 𝐴) |
|
Theorem | sopo 4195 |
A strict linear order is a strict partial order. (Contributed by NM,
28-Mar-1997.)
|
⊢ (𝑅 Or 𝐴 → 𝑅 Po 𝐴) |
|
Theorem | soss 4196 |
Subset theorem for the strict ordering predicate. (Contributed by NM,
16-Mar-1997.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
|
⊢ (𝐴 ⊆ 𝐵 → (𝑅 Or 𝐵 → 𝑅 Or 𝐴)) |
|
Theorem | soeq1 4197 |
Equality theorem for the strict ordering predicate. (Contributed by NM,
16-Mar-1997.)
|
⊢ (𝑅 = 𝑆 → (𝑅 Or 𝐴 ↔ 𝑆 Or 𝐴)) |
|
Theorem | soeq2 4198 |
Equality theorem for the strict ordering predicate. (Contributed by NM,
16-Mar-1997.)
|
⊢ (𝐴 = 𝐵 → (𝑅 Or 𝐴 ↔ 𝑅 Or 𝐵)) |
|
Theorem | sonr 4199 |
A strict order relation is irreflexive. (Contributed by NM,
24-Nov-1995.)
|
⊢ ((𝑅 Or 𝐴 ∧ 𝐵 ∈ 𝐴) → ¬ 𝐵𝑅𝐵) |
|
Theorem | sotr 4200 |
A strict order relation is a transitive relation. (Contributed by NM,
21-Jan-1996.)
|
⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → ((𝐵𝑅𝐶 ∧ 𝐶𝑅𝐷) → 𝐵𝑅𝐷)) |