Theorem List for Intuitionistic Logic Explorer - 4001-4100 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | brabga 4001* |
The law of concretion for a binary relation. (Contributed by Mario
Carneiro, 19-Dec-2013.)
|
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) & ⊢ 𝑅 = {〈𝑥, 𝑦〉 ∣ 𝜑} ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴𝑅𝐵 ↔ 𝜓)) |
|
Theorem | opelopab2a 4002* |
Ordered pair membership in an ordered pair class abstraction.
(Contributed by Mario Carneiro, 19-Dec-2013.)
|
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (〈𝐴, 𝐵〉 ∈ {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) ∧ 𝜑)} ↔ 𝜓)) |
|
Theorem | opelopaba 4003* |
The law of concretion. Theorem 9.5 of [Quine] p.
61. (Contributed by
Mario Carneiro, 19-Dec-2013.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) ⇒ ⊢ (〈𝐴, 𝐵〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ↔ 𝜓) |
|
Theorem | braba 4004* |
The law of concretion for a binary relation. (Contributed by NM,
19-Dec-2013.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) & ⊢ 𝑅 = {〈𝑥, 𝑦〉 ∣ 𝜑} ⇒ ⊢ (𝐴𝑅𝐵 ↔ 𝜓) |
|
Theorem | opelopabg 4005* |
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 4006* |
The law of concretion for a binary relation. (Contributed by NM,
16-Aug-1999.) (Revised by Mario Carneiro, 19-Dec-2013.)
|
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ 𝑅 = {〈𝑥, 𝑦〉 ∣ 𝜑} ⇒ ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴𝑅𝐵 ↔ 𝜒)) |
|
Theorem | opelopab2 4007* |
Ordered pair membership in an ordered pair class abstraction.
(Contributed by NM, 14-Oct-2007.) (Revised by Mario Carneiro,
19-Dec-2013.)
|
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) ⇒ ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (〈𝐴, 𝐵〉 ∈ {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) ∧ 𝜑)} ↔ 𝜒)) |
|
Theorem | opelopab 4008* |
The law of concretion. Theorem 9.5 of [Quine] p.
61. (Contributed by
NM, 16-May-1995.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (〈𝐴, 𝐵〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ↔ 𝜒) |
|
Theorem | brab 4009* |
The law of concretion for a binary relation. (Contributed by NM,
16-Aug-1999.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ 𝑅 = {〈𝑥, 𝑦〉 ∣ 𝜑} ⇒ ⊢ (𝐴𝑅𝐵 ↔ 𝜒) |
|
Theorem | opelopabaf 4010* |
The law of concretion. Theorem 9.5 of [Quine] p.
61. This version of
opelopab 4008 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 4011* |
The law of concretion. Theorem 9.5 of [Quine] p.
61. This version of
opelopab 4008 uses bound-variable hypotheses in place of
distinct variable
conditions." (Contributed by NM, 19-Dec-2008.)
|
⊢ Ⅎ𝑥𝜓
& ⊢ Ⅎ𝑦𝜒
& ⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (〈𝐴, 𝐵〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ↔ 𝜒) |
|
Theorem | ssopab2 4012 |
Equivalence of ordered pair abstraction subclass and implication.
(Contributed by NM, 27-Dec-1996.) (Revised by Mario Carneiro,
19-May-2013.)
|
⊢ (∀𝑥∀𝑦(𝜑 → 𝜓) → {〈𝑥, 𝑦〉 ∣ 𝜑} ⊆ {〈𝑥, 𝑦〉 ∣ 𝜓}) |
|
Theorem | ssopab2b 4013 |
Equivalence of ordered pair abstraction subclass and implication.
(Contributed by NM, 27-Dec-1996.) (Proof shortened by Mario Carneiro,
18-Nov-2016.)
|
⊢ ({〈𝑥, 𝑦〉 ∣ 𝜑} ⊆ {〈𝑥, 𝑦〉 ∣ 𝜓} ↔ ∀𝑥∀𝑦(𝜑 → 𝜓)) |
|
Theorem | ssopab2i 4014 |
Inference of ordered pair abstraction subclass from implication.
(Contributed by NM, 5-Apr-1995.)
|
⊢ (𝜑 → 𝜓) ⇒ ⊢ {〈𝑥, 𝑦〉 ∣ 𝜑} ⊆ {〈𝑥, 𝑦〉 ∣ 𝜓} |
|
Theorem | ssopab2dv 4015* |
Inference of ordered pair abstraction subclass from implication.
(Contributed by NM, 19-Jan-2014.) (Revised by Mario Carneiro,
24-Jun-2014.)
|
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → {〈𝑥, 𝑦〉 ∣ 𝜓} ⊆ {〈𝑥, 𝑦〉 ∣ 𝜒}) |
|
Theorem | eqopab2b 4016 |
Equivalence of ordered pair abstraction equality and biconditional.
(Contributed by Mario Carneiro, 4-Jan-2017.)
|
⊢ ({〈𝑥, 𝑦〉 ∣ 𝜑} = {〈𝑥, 𝑦〉 ∣ 𝜓} ↔ ∀𝑥∀𝑦(𝜑 ↔ 𝜓)) |
|
Theorem | opabm 4017* |
Inhabited ordered pair class abstraction. (Contributed by Jim Kingdon,
29-Sep-2018.)
|
⊢ (∃𝑧 𝑧 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ↔ ∃𝑥∃𝑦𝜑) |
|
Theorem | iunopab 4018* |
Move indexed union inside an ordered-pair abstraction. (Contributed by
Stefan O'Rear, 20-Feb-2015.)
|
⊢ ∪ 𝑧 ∈ 𝐴 {〈𝑥, 𝑦〉 ∣ 𝜑} = {〈𝑥, 𝑦〉 ∣ ∃𝑧 ∈ 𝐴 𝜑} |
|
2.3.5 Power class of union and
intersection
|
|
Theorem | pwin 4019 |
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 4020 |
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 4021 |
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 4022 |
Break up the power class of a union into a union of smaller classes.
(Contributed by Jim Kingdon, 30-Sep-2018.)
|
⊢ ((𝒫 (𝐴 ∪ 𝐵) ∖ 𝒫 𝐴) ∪ 𝒫 𝐴) ⊆ 𝒫 (𝐴 ∪ 𝐵) |
|
Theorem | pwunim 4023 |
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.6 Epsilon and identity
relations
|
|
Syntax | cep 4024 |
Extend class notation to include the epsilon relation.
|
class E |
|
Syntax | cid 4025 |
Extend the definition of a class to include identity relation.
|
class I |
|
Definition | df-eprel 4026* |
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 4027. Thus, 5 E { 1 , 5
}. (Contributed by NM,
13-Aug-1995.)
|
⊢ E = {〈𝑥, 𝑦〉 ∣ 𝑥 ∈ 𝑦} |
|
Theorem | epelg 4027 |
The epsilon relation and membership are the same. General version of
epel 4029. (Contributed by Scott Fenton, 27-Mar-2011.)
(Revised by Mario
Carneiro, 28-Apr-2015.)
|
⊢ (𝐵 ∈ 𝑉 → (𝐴 E 𝐵 ↔ 𝐴 ∈ 𝐵)) |
|
Theorem | epelc 4028 |
The epsilon relationship and the membership relation are the same.
(Contributed by Scott Fenton, 11-Apr-2012.)
|
⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴 E 𝐵 ↔ 𝐴 ∈ 𝐵) |
|
Theorem | epel 4029 |
The epsilon relation and the membership relation are the same.
(Contributed by NM, 13-Aug-1995.)
|
⊢ (𝑥 E 𝑦 ↔ 𝑥 ∈ 𝑦) |
|
Definition | df-id 4030* |
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.7 Partial and complete ordering
|
|
Syntax | wpo 4031 |
Extend wff notation to include the strict partial ordering predicate.
Read: ' 𝑅 is a partial order on 𝐴.'
|
wff 𝑅 Po 𝐴 |
|
Syntax | wor 4032 |
Extend wff notation to include the strict linear ordering predicate.
Read: ' 𝑅 orders 𝐴.'
|
wff 𝑅 Or 𝐴 |
|
Definition | df-po 4033* |
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 4034* |
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 4035 |
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 4036 |
Equality theorem for partial ordering predicate. (Contributed by NM,
27-Mar-1997.)
|
⊢ (𝑅 = 𝑆 → (𝑅 Po 𝐴 ↔ 𝑆 Po 𝐴)) |
|
Theorem | poeq2 4037 |
Equality theorem for partial ordering predicate. (Contributed by NM,
27-Mar-1997.)
|
⊢ (𝐴 = 𝐵 → (𝑅 Po 𝐴 ↔ 𝑅 Po 𝐵)) |
|
Theorem | nfpo 4038 |
Bound-variable hypothesis builder for partial orders. (Contributed by
Stefan O'Rear, 20-Jan-2015.)
|
⊢ Ⅎ𝑥𝑅
& ⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥 𝑅 Po 𝐴 |
|
Theorem | nfso 4039 |
Bound-variable hypothesis builder for total orders. (Contributed by
Stefan O'Rear, 20-Jan-2015.)
|
⊢ Ⅎ𝑥𝑅
& ⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥 𝑅 Or 𝐴 |
|
Theorem | pocl 4040 |
Properties of partial order relation in class notation. (Contributed by
NM, 27-Mar-1997.)
|
⊢ (𝑅 Po 𝐴 → ((𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴) → (¬ 𝐵𝑅𝐵 ∧ ((𝐵𝑅𝐶 ∧ 𝐶𝑅𝐷) → 𝐵𝑅𝐷)))) |
|
Theorem | ispod 4041* |
Sufficient conditions for a partial order. (Contributed by NM,
9-Jul-2014.)
|
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ¬ 𝑥𝑅𝑥)
& ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)) ⇒ ⊢ (𝜑 → 𝑅 Po 𝐴) |
|
Theorem | swopolem 4042* |
Perform the substitutions into the strict weak ordering law.
(Contributed by Mario Carneiro, 31-Dec-2014.)
|
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → (𝑥𝑅𝑦 → (𝑥𝑅𝑧 ∨ 𝑧𝑅𝑦))) ⇒ ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑍 ∈ 𝐴)) → (𝑋𝑅𝑌 → (𝑋𝑅𝑍 ∨ 𝑍𝑅𝑌))) |
|
Theorem | swopo 4043* |
A strict weak order is a partial order. (Contributed by Mario Carneiro,
9-Jul-2014.)
|
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → (𝑦𝑅𝑧 → ¬ 𝑧𝑅𝑦))
& ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → (𝑥𝑅𝑦 → (𝑥𝑅𝑧 ∨ 𝑧𝑅𝑦))) ⇒ ⊢ (𝜑 → 𝑅 Po 𝐴) |
|
Theorem | poirr 4044 |
A partial order relation is irreflexive. (Contributed by NM,
27-Mar-1997.)
|
⊢ ((𝑅 Po 𝐴 ∧ 𝐵 ∈ 𝐴) → ¬ 𝐵𝑅𝐵) |
|
Theorem | potr 4045 |
A partial order relation is a transitive relation. (Contributed by NM,
27-Mar-1997.)
|
⊢ ((𝑅 Po 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → ((𝐵𝑅𝐶 ∧ 𝐶𝑅𝐷) → 𝐵𝑅𝐷)) |
|
Theorem | po2nr 4046 |
A partial order relation has no 2-cycle loops. (Contributed by NM,
27-Mar-1997.)
|
⊢ ((𝑅 Po 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → ¬ (𝐵𝑅𝐶 ∧ 𝐶𝑅𝐵)) |
|
Theorem | po3nr 4047 |
A partial order relation has no 3-cycle loops. (Contributed by NM,
27-Mar-1997.)
|
⊢ ((𝑅 Po 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → ¬ (𝐵𝑅𝐶 ∧ 𝐶𝑅𝐷 ∧ 𝐷𝑅𝐵)) |
|
Theorem | po0 4048 |
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 4049* |
A function preserves a partial order relation. (Contributed by Jeff
Madsen, 18-Jun-2011.)
|
⊢ 𝑆 = {〈𝑥, 𝑦〉 ∣ 𝑋𝑅𝑌}
& ⊢ (𝑥 = 𝑦 → 𝑋 = 𝑌) ⇒ ⊢ ((𝑅 Po 𝐵 ∧ ∀𝑥 ∈ 𝐴 𝑋 ∈ 𝐵) → 𝑆 Po 𝐴) |
|
Theorem | sopo 4050 |
A strict linear order is a strict partial order. (Contributed by NM,
28-Mar-1997.)
|
⊢ (𝑅 Or 𝐴 → 𝑅 Po 𝐴) |
|
Theorem | soss 4051 |
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 4052 |
Equality theorem for the strict ordering predicate. (Contributed by NM,
16-Mar-1997.)
|
⊢ (𝑅 = 𝑆 → (𝑅 Or 𝐴 ↔ 𝑆 Or 𝐴)) |
|
Theorem | soeq2 4053 |
Equality theorem for the strict ordering predicate. (Contributed by NM,
16-Mar-1997.)
|
⊢ (𝐴 = 𝐵 → (𝑅 Or 𝐴 ↔ 𝑅 Or 𝐵)) |
|
Theorem | sonr 4054 |
A strict order relation is irreflexive. (Contributed by NM,
24-Nov-1995.)
|
⊢ ((𝑅 Or 𝐴 ∧ 𝐵 ∈ 𝐴) → ¬ 𝐵𝑅𝐵) |
|
Theorem | sotr 4055 |
A strict order relation is a transitive relation. (Contributed by NM,
21-Jan-1996.)
|
⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → ((𝐵𝑅𝐶 ∧ 𝐶𝑅𝐷) → 𝐵𝑅𝐷)) |
|
Theorem | issod 4056* |
An irreflexive, transitive, trichotomous relation is a linear ordering
(in the sense of df-iso 4034). (Contributed by NM, 21-Jan-1996.)
(Revised by Mario Carneiro, 9-Jul-2014.)
|
⊢ (𝜑 → 𝑅 Po 𝐴)
& ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)) ⇒ ⊢ (𝜑 → 𝑅 Or 𝐴) |
|
Theorem | sowlin 4057 |
A strict order relation satisfies weak linearity. (Contributed by Jim
Kingdon, 6-Oct-2018.)
|
⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → (𝐵𝑅𝐶 → (𝐵𝑅𝐷 ∨ 𝐷𝑅𝐶))) |
|
Theorem | so2nr 4058 |
A strict order relation has no 2-cycle loops. (Contributed by NM,
21-Jan-1996.)
|
⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → ¬ (𝐵𝑅𝐶 ∧ 𝐶𝑅𝐵)) |
|
Theorem | so3nr 4059 |
A strict order relation has no 3-cycle loops. (Contributed by NM,
21-Jan-1996.)
|
⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → ¬ (𝐵𝑅𝐶 ∧ 𝐶𝑅𝐷 ∧ 𝐷𝑅𝐵)) |
|
Theorem | sotricim 4060 |
One direction of sotritric 4061 holds for all weakly linear orders.
(Contributed by Jim Kingdon, 28-Sep-2019.)
|
⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → (𝐵𝑅𝐶 → ¬ (𝐵 = 𝐶 ∨ 𝐶𝑅𝐵))) |
|
Theorem | sotritric 4061 |
A trichotomy relationship, given a trichotomous order. (Contributed by
Jim Kingdon, 28-Sep-2019.)
|
⊢ 𝑅 Or 𝐴
& ⊢ ((𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴) → (𝐵𝑅𝐶 ∨ 𝐵 = 𝐶 ∨ 𝐶𝑅𝐵)) ⇒ ⊢ ((𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴) → (𝐵𝑅𝐶 ↔ ¬ (𝐵 = 𝐶 ∨ 𝐶𝑅𝐵))) |
|
Theorem | sotritrieq 4062 |
A trichotomy relationship, given a trichotomous order. (Contributed by
Jim Kingdon, 13-Dec-2019.)
|
⊢ 𝑅 Or 𝐴
& ⊢ ((𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴) → (𝐵𝑅𝐶 ∨ 𝐵 = 𝐶 ∨ 𝐶𝑅𝐵)) ⇒ ⊢ ((𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴) → (𝐵 = 𝐶 ↔ ¬ (𝐵𝑅𝐶 ∨ 𝐶𝑅𝐵))) |
|
Theorem | so0 4063 |
Any relation is a strict ordering of the empty set. (Contributed by NM,
16-Mar-1997.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
|
⊢ 𝑅 Or ∅ |
|
2.3.8 Founded and set-like
relations
|
|
Syntax | wfrfor 4064 |
Extend wff notation to include the well-founded predicate.
|
wff FrFor 𝑅𝐴𝑆 |
|
Syntax | wfr 4065 |
Extend wff notation to include the well-founded predicate. Read: ' 𝑅
is a well-founded relation on 𝐴.'
|
wff 𝑅 Fr 𝐴 |
|
Syntax | wse 4066 |
Extend wff notation to include the set-like predicate. Read: ' 𝑅 is
set-like on 𝐴.'
|
wff 𝑅 Se 𝐴 |
|
Syntax | wwe 4067 |
Extend wff notation to include the well-ordering predicate. Read:
' 𝑅 well-orders 𝐴.'
|
wff 𝑅 We 𝐴 |
|
Definition | df-frfor 4068* |
Define the well-founded relation predicate where 𝐴 might be a proper
class. By passing in 𝑆 we allow it potentially to be a
proper class
rather than a set. (Contributed by Jim Kingdon and Mario Carneiro,
22-Sep-2021.)
|
⊢ ( FrFor 𝑅𝐴𝑆 ↔ (∀𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → 𝑦 ∈ 𝑆) → 𝑥 ∈ 𝑆) → 𝐴 ⊆ 𝑆)) |
|
Definition | df-frind 4069* |
Define the well-founded relation predicate. In the presence of excluded
middle, there are a variety of equivalent ways to define this. In our
case, this definition, in terms of an inductive principle, works better
than one along the lines of "there is an element which is minimal
when A
is ordered by R". Because 𝑠 is constrained to be a set (not a
proper class) here, sometimes it may be necessary to use FrFor
directly rather than via Fr. (Contributed by
Jim Kingdon and Mario
Carneiro, 21-Sep-2021.)
|
⊢ (𝑅 Fr 𝐴 ↔ ∀𝑠 FrFor 𝑅𝐴𝑠) |
|
Definition | df-se 4070* |
Define the set-like predicate. (Contributed by Mario Carneiro,
19-Nov-2014.)
|
⊢ (𝑅 Se 𝐴 ↔ ∀𝑥 ∈ 𝐴 {𝑦 ∈ 𝐴 ∣ 𝑦𝑅𝑥} ∈ V) |
|
Definition | df-wetr 4071* |
Define the well-ordering predicate. It is unusual to define
"well-ordering" in the absence of excluded middle, but we mean
an
ordering which is like the ordering which we have for ordinals (for
example, it does not entail trichotomy because ordinals don't have that
as seen at ordtriexmid 4247). Given excluded middle, well-ordering is
usually defined to require trichotomy (and the defintion of Fr is
typically also different). (Contributed by Mario Carneiro and Jim
Kingdon, 23-Sep-2021.)
|
⊢ (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧))) |
|
Theorem | seex 4072* |
The 𝑅-preimage of an element of the base
set in a set-like relation
is a set. (Contributed by Mario Carneiro, 19-Nov-2014.)
|
⊢ ((𝑅 Se 𝐴 ∧ 𝐵 ∈ 𝐴) → {𝑥 ∈ 𝐴 ∣ 𝑥𝑅𝐵} ∈ V) |
|
Theorem | exse 4073 |
Any relation on a set is set-like on it. (Contributed by Mario
Carneiro, 22-Jun-2015.)
|
⊢ (𝐴 ∈ 𝑉 → 𝑅 Se 𝐴) |
|
Theorem | sess1 4074 |
Subset theorem for the set-like predicate. (Contributed by Mario
Carneiro, 24-Jun-2015.)
|
⊢ (𝑅 ⊆ 𝑆 → (𝑆 Se 𝐴 → 𝑅 Se 𝐴)) |
|
Theorem | sess2 4075 |
Subset theorem for the set-like predicate. (Contributed by Mario
Carneiro, 24-Jun-2015.)
|
⊢ (𝐴 ⊆ 𝐵 → (𝑅 Se 𝐵 → 𝑅 Se 𝐴)) |
|
Theorem | seeq1 4076 |
Equality theorem for the set-like predicate. (Contributed by Mario
Carneiro, 24-Jun-2015.)
|
⊢ (𝑅 = 𝑆 → (𝑅 Se 𝐴 ↔ 𝑆 Se 𝐴)) |
|
Theorem | seeq2 4077 |
Equality theorem for the set-like predicate. (Contributed by Mario
Carneiro, 24-Jun-2015.)
|
⊢ (𝐴 = 𝐵 → (𝑅 Se 𝐴 ↔ 𝑅 Se 𝐵)) |
|
Theorem | nfse 4078 |
Bound-variable hypothesis builder for set-like relations. (Contributed
by Mario Carneiro, 24-Jun-2015.) (Revised by Mario Carneiro,
14-Oct-2016.)
|
⊢ Ⅎ𝑥𝑅
& ⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥 𝑅 Se 𝐴 |
|
Theorem | epse 4079 |
The epsilon relation is set-like on any class. (This is the origin of
the term "set-like": a set-like relation "acts like"
the epsilon
relation of sets and their elements.) (Contributed by Mario Carneiro,
22-Jun-2015.)
|
⊢ E Se 𝐴 |
|
Theorem | frforeq1 4080 |
Equality theorem for the well-founded predicate. (Contributed by Jim
Kingdon, 22-Sep-2021.)
|
⊢ (𝑅 = 𝑆 → ( FrFor 𝑅𝐴𝑇 ↔ FrFor 𝑆𝐴𝑇)) |
|
Theorem | freq1 4081 |
Equality theorem for the well-founded predicate. (Contributed by NM,
9-Mar-1997.)
|
⊢ (𝑅 = 𝑆 → (𝑅 Fr 𝐴 ↔ 𝑆 Fr 𝐴)) |
|
Theorem | frforeq2 4082 |
Equality theorem for the well-founded predicate. (Contributed by Jim
Kingdon, 22-Sep-2021.)
|
⊢ (𝐴 = 𝐵 → ( FrFor 𝑅𝐴𝑇 ↔ FrFor 𝑅𝐵𝑇)) |
|
Theorem | freq2 4083 |
Equality theorem for the well-founded predicate. (Contributed by NM,
3-Apr-1994.)
|
⊢ (𝐴 = 𝐵 → (𝑅 Fr 𝐴 ↔ 𝑅 Fr 𝐵)) |
|
Theorem | frforeq3 4084 |
Equality theorem for the well-founded predicate. (Contributed by Jim
Kingdon, 22-Sep-2021.)
|
⊢ (𝑆 = 𝑇 → ( FrFor 𝑅𝐴𝑆 ↔ FrFor 𝑅𝐴𝑇)) |
|
Theorem | nffrfor 4085 |
Bound-variable hypothesis builder for well-founded relations.
(Contributed by Stefan O'Rear, 20-Jan-2015.) (Revised by Mario
Carneiro, 14-Oct-2016.)
|
⊢ Ⅎ𝑥𝑅
& ⊢ Ⅎ𝑥𝐴
& ⊢ Ⅎ𝑥𝑆 ⇒ ⊢ Ⅎ𝑥 FrFor 𝑅𝐴𝑆 |
|
Theorem | nffr 4086 |
Bound-variable hypothesis builder for well-founded relations.
(Contributed by Stefan O'Rear, 20-Jan-2015.) (Revised by Mario
Carneiro, 14-Oct-2016.)
|
⊢ Ⅎ𝑥𝑅
& ⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥 𝑅 Fr 𝐴 |
|
Theorem | frirrg 4087 |
A well-founded relation is irreflexive. This is the case where 𝐴
exists. (Contributed by Jim Kingdon, 21-Sep-2021.)
|
⊢ ((𝑅 Fr 𝐴 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝐴) → ¬ 𝐵𝑅𝐵) |
|
Theorem | fr0 4088 |
Any relation is well-founded on the empty set. (Contributed by NM,
17-Sep-1993.)
|
⊢ 𝑅 Fr ∅ |
|
Theorem | frind 4089* |
Induction over a well-founded set. (Contributed by Jim Kingdon,
28-Sep-2021.)
|
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) & ⊢ ((𝜒 ∧ 𝑥 ∈ 𝐴) → (∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → 𝜓) → 𝜑)) & ⊢ (𝜒 → 𝑅 Fr 𝐴)
& ⊢ (𝜒 → 𝐴 ∈ 𝑉) ⇒ ⊢ ((𝜒 ∧ 𝑥 ∈ 𝐴) → 𝜑) |
|
Theorem | efrirr 4090 |
Irreflexivity of the epsilon relation: a class founded by epsilon is not
a member of itself. (Contributed by NM, 18-Apr-1994.) (Revised by
Mario Carneiro, 22-Jun-2015.)
|
⊢ ( E Fr 𝐴 → ¬ 𝐴 ∈ 𝐴) |
|
Theorem | tz7.2 4091 |
Similar to Theorem 7.2 of [TakeutiZaring]
p. 35, of except that the Axiom
of Regularity is not required due to antecedent E Fr
𝐴.
(Contributed by NM, 4-May-1994.)
|
⊢ ((Tr 𝐴 ∧ E Fr 𝐴 ∧ 𝐵 ∈ 𝐴) → (𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ 𝐴)) |
|
Theorem | nfwe 4092 |
Bound-variable hypothesis builder for well-orderings. (Contributed by
Stefan O'Rear, 20-Jan-2015.) (Revised by Mario Carneiro,
14-Oct-2016.)
|
⊢ Ⅎ𝑥𝑅
& ⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥 𝑅 We 𝐴 |
|
Theorem | weeq1 4093 |
Equality theorem for the well-ordering predicate. (Contributed by NM,
9-Mar-1997.)
|
⊢ (𝑅 = 𝑆 → (𝑅 We 𝐴 ↔ 𝑆 We 𝐴)) |
|
Theorem | weeq2 4094 |
Equality theorem for the well-ordering predicate. (Contributed by NM,
3-Apr-1994.)
|
⊢ (𝐴 = 𝐵 → (𝑅 We 𝐴 ↔ 𝑅 We 𝐵)) |
|
Theorem | wefr 4095 |
A well-ordering is well-founded. (Contributed by NM, 22-Apr-1994.)
|
⊢ (𝑅 We 𝐴 → 𝑅 Fr 𝐴) |
|
Theorem | wepo 4096 |
A well-ordering is a partial ordering. (Contributed by Jim Kingdon,
23-Sep-2021.)
|
⊢ ((𝑅 We 𝐴 ∧ 𝐴 ∈ 𝑉) → 𝑅 Po 𝐴) |
|
Theorem | wetrep 4097* |
An epsilon well-ordering is a transitive relation. (Contributed by NM,
22-Apr-1994.)
|
⊢ (( E We 𝐴 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝑧) → 𝑥 ∈ 𝑧)) |
|
Theorem | we0 4098 |
Any relation is a well-ordering of the empty set. (Contributed by NM,
16-Mar-1997.)
|
⊢ 𝑅 We ∅ |
|
2.3.9 Ordinals
|
|
Syntax | word 4099 |
Extend the definition of a wff to include the ordinal predicate.
|
wff Ord 𝐴 |
|
Syntax | con0 4100 |
Extend the definition of a class to include the class of all ordinal
numbers. (The 0 in the name prevents creating a file called con.html,
which causes problems in Windows.)
|
class On |