Theorem List for Intuitionistic Logic Explorer - 4201-4300 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | eqopab2b 4201 |
Equivalence of ordered pair abstraction equality and biconditional.
(Contributed by Mario Carneiro, 4-Jan-2017.)
|
⊢ ({〈𝑥, 𝑦〉 ∣ 𝜑} = {〈𝑥, 𝑦〉 ∣ 𝜓} ↔ ∀𝑥∀𝑦(𝜑 ↔ 𝜓)) |
|
Theorem | opabm 4202* |
Inhabited ordered pair class abstraction. (Contributed by Jim Kingdon,
29-Sep-2018.)
|
⊢ (∃𝑧 𝑧 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ↔ ∃𝑥∃𝑦𝜑) |
|
Theorem | iunopab 4203* |
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 4204 |
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 4205 |
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 4206 |
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 4207 |
Break up the power class of a union into a union of smaller classes.
(Contributed by Jim Kingdon, 30-Sep-2018.)
|
⊢ ((𝒫 (𝐴 ∪ 𝐵) ∖ 𝒫 𝐴) ∪ 𝒫 𝐴) ⊆ 𝒫 (𝐴 ∪ 𝐵) |
|
Theorem | pwunim 4208 |
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 4209 |
Extend class notation to include the epsilon relation.
|
class E |
|
Syntax | cid 4210 |
Extend the definition of a class to include identity relation.
|
class I |
|
Definition | df-eprel 4211* |
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 4212. Thus, 5 E { 1 , 5
}. (Contributed by NM,
13-Aug-1995.)
|
⊢ E = {〈𝑥, 𝑦〉 ∣ 𝑥 ∈ 𝑦} |
|
Theorem | epelg 4212 |
The epsilon relation and membership are the same. General version of
epel 4214. (Contributed by Scott Fenton, 27-Mar-2011.)
(Revised by Mario
Carneiro, 28-Apr-2015.)
|
⊢ (𝐵 ∈ 𝑉 → (𝐴 E 𝐵 ↔ 𝐴 ∈ 𝐵)) |
|
Theorem | epelc 4213 |
The epsilon relationship and the membership relation are the same.
(Contributed by Scott Fenton, 11-Apr-2012.)
|
⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴 E 𝐵 ↔ 𝐴 ∈ 𝐵) |
|
Theorem | epel 4214 |
The epsilon relation and the membership relation are the same.
(Contributed by NM, 13-Aug-1995.)
|
⊢ (𝑥 E 𝑦 ↔ 𝑥 ∈ 𝑦) |
|
Definition | df-id 4215* |
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 4216 |
Extend wff notation to include the strict partial ordering predicate.
Read: ' 𝑅 is a partial order on 𝐴.'
|
wff 𝑅 Po 𝐴 |
|
Syntax | wor 4217 |
Extend wff notation to include the strict linear ordering predicate.
Read: ' 𝑅 orders 𝐴.'
|
wff 𝑅 Or 𝐴 |
|
Definition | df-po 4218* |
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 4219* |
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 4220 |
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 4221 |
Equality theorem for partial ordering predicate. (Contributed by NM,
27-Mar-1997.)
|
⊢ (𝑅 = 𝑆 → (𝑅 Po 𝐴 ↔ 𝑆 Po 𝐴)) |
|
Theorem | poeq2 4222 |
Equality theorem for partial ordering predicate. (Contributed by NM,
27-Mar-1997.)
|
⊢ (𝐴 = 𝐵 → (𝑅 Po 𝐴 ↔ 𝑅 Po 𝐵)) |
|
Theorem | nfpo 4223 |
Bound-variable hypothesis builder for partial orders. (Contributed by
Stefan O'Rear, 20-Jan-2015.)
|
⊢ Ⅎ𝑥𝑅
& ⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥 𝑅 Po 𝐴 |
|
Theorem | nfso 4224 |
Bound-variable hypothesis builder for total orders. (Contributed by
Stefan O'Rear, 20-Jan-2015.)
|
⊢ Ⅎ𝑥𝑅
& ⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥 𝑅 Or 𝐴 |
|
Theorem | pocl 4225 |
Properties of partial order relation in class notation. (Contributed by
NM, 27-Mar-1997.)
|
⊢ (𝑅 Po 𝐴 → ((𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴) → (¬ 𝐵𝑅𝐵 ∧ ((𝐵𝑅𝐶 ∧ 𝐶𝑅𝐷) → 𝐵𝑅𝐷)))) |
|
Theorem | ispod 4226* |
Sufficient conditions for a partial order. (Contributed by NM,
9-Jul-2014.)
|
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ¬ 𝑥𝑅𝑥)
& ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)) ⇒ ⊢ (𝜑 → 𝑅 Po 𝐴) |
|
Theorem | swopolem 4227* |
Perform the substitutions into the strict weak ordering law.
(Contributed by Mario Carneiro, 31-Dec-2014.)
|
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → (𝑥𝑅𝑦 → (𝑥𝑅𝑧 ∨ 𝑧𝑅𝑦))) ⇒ ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑍 ∈ 𝐴)) → (𝑋𝑅𝑌 → (𝑋𝑅𝑍 ∨ 𝑍𝑅𝑌))) |
|
Theorem | swopo 4228* |
A strict weak order is a partial order. (Contributed by Mario Carneiro,
9-Jul-2014.)
|
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → (𝑦𝑅𝑧 → ¬ 𝑧𝑅𝑦))
& ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → (𝑥𝑅𝑦 → (𝑥𝑅𝑧 ∨ 𝑧𝑅𝑦))) ⇒ ⊢ (𝜑 → 𝑅 Po 𝐴) |
|
Theorem | poirr 4229 |
A partial order relation is irreflexive. (Contributed by NM,
27-Mar-1997.)
|
⊢ ((𝑅 Po 𝐴 ∧ 𝐵 ∈ 𝐴) → ¬ 𝐵𝑅𝐵) |
|
Theorem | potr 4230 |
A partial order relation is a transitive relation. (Contributed by NM,
27-Mar-1997.)
|
⊢ ((𝑅 Po 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → ((𝐵𝑅𝐶 ∧ 𝐶𝑅𝐷) → 𝐵𝑅𝐷)) |
|
Theorem | po2nr 4231 |
A partial order relation has no 2-cycle loops. (Contributed by NM,
27-Mar-1997.)
|
⊢ ((𝑅 Po 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → ¬ (𝐵𝑅𝐶 ∧ 𝐶𝑅𝐵)) |
|
Theorem | po3nr 4232 |
A partial order relation has no 3-cycle loops. (Contributed by NM,
27-Mar-1997.)
|
⊢ ((𝑅 Po 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → ¬ (𝐵𝑅𝐶 ∧ 𝐶𝑅𝐷 ∧ 𝐷𝑅𝐵)) |
|
Theorem | po0 4233 |
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 4234* |
A function preserves a partial order relation. (Contributed by Jeff
Madsen, 18-Jun-2011.)
|
⊢ 𝑆 = {〈𝑥, 𝑦〉 ∣ 𝑋𝑅𝑌}
& ⊢ (𝑥 = 𝑦 → 𝑋 = 𝑌) ⇒ ⊢ ((𝑅 Po 𝐵 ∧ ∀𝑥 ∈ 𝐴 𝑋 ∈ 𝐵) → 𝑆 Po 𝐴) |
|
Theorem | sopo 4235 |
A strict linear order is a strict partial order. (Contributed by NM,
28-Mar-1997.)
|
⊢ (𝑅 Or 𝐴 → 𝑅 Po 𝐴) |
|
Theorem | soss 4236 |
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 4237 |
Equality theorem for the strict ordering predicate. (Contributed by NM,
16-Mar-1997.)
|
⊢ (𝑅 = 𝑆 → (𝑅 Or 𝐴 ↔ 𝑆 Or 𝐴)) |
|
Theorem | soeq2 4238 |
Equality theorem for the strict ordering predicate. (Contributed by NM,
16-Mar-1997.)
|
⊢ (𝐴 = 𝐵 → (𝑅 Or 𝐴 ↔ 𝑅 Or 𝐵)) |
|
Theorem | sonr 4239 |
A strict order relation is irreflexive. (Contributed by NM,
24-Nov-1995.)
|
⊢ ((𝑅 Or 𝐴 ∧ 𝐵 ∈ 𝐴) → ¬ 𝐵𝑅𝐵) |
|
Theorem | sotr 4240 |
A strict order relation is a transitive relation. (Contributed by NM,
21-Jan-1996.)
|
⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → ((𝐵𝑅𝐶 ∧ 𝐶𝑅𝐷) → 𝐵𝑅𝐷)) |
|
Theorem | issod 4241* |
An irreflexive, transitive, trichotomous relation is a linear ordering
(in the sense of df-iso 4219). (Contributed by NM, 21-Jan-1996.)
(Revised by Mario Carneiro, 9-Jul-2014.)
|
⊢ (𝜑 → 𝑅 Po 𝐴)
& ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)) ⇒ ⊢ (𝜑 → 𝑅 Or 𝐴) |
|
Theorem | sowlin 4242 |
A strict order relation satisfies weak linearity. (Contributed by Jim
Kingdon, 6-Oct-2018.)
|
⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → (𝐵𝑅𝐶 → (𝐵𝑅𝐷 ∨ 𝐷𝑅𝐶))) |
|
Theorem | so2nr 4243 |
A strict order relation has no 2-cycle loops. (Contributed by NM,
21-Jan-1996.)
|
⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → ¬ (𝐵𝑅𝐶 ∧ 𝐶𝑅𝐵)) |
|
Theorem | so3nr 4244 |
A strict order relation has no 3-cycle loops. (Contributed by NM,
21-Jan-1996.)
|
⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → ¬ (𝐵𝑅𝐶 ∧ 𝐶𝑅𝐷 ∧ 𝐷𝑅𝐵)) |
|
Theorem | sotricim 4245 |
One direction of sotritric 4246 holds for all weakly linear orders.
(Contributed by Jim Kingdon, 28-Sep-2019.)
|
⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → (𝐵𝑅𝐶 → ¬ (𝐵 = 𝐶 ∨ 𝐶𝑅𝐵))) |
|
Theorem | sotritric 4246 |
A trichotomy relationship, given a trichotomous order. (Contributed by
Jim Kingdon, 28-Sep-2019.)
|
⊢ 𝑅 Or 𝐴
& ⊢ ((𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴) → (𝐵𝑅𝐶 ∨ 𝐵 = 𝐶 ∨ 𝐶𝑅𝐵)) ⇒ ⊢ ((𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴) → (𝐵𝑅𝐶 ↔ ¬ (𝐵 = 𝐶 ∨ 𝐶𝑅𝐵))) |
|
Theorem | sotritrieq 4247 |
A trichotomy relationship, given a trichotomous order. (Contributed by
Jim Kingdon, 13-Dec-2019.)
|
⊢ 𝑅 Or 𝐴
& ⊢ ((𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴) → (𝐵𝑅𝐶 ∨ 𝐵 = 𝐶 ∨ 𝐶𝑅𝐵)) ⇒ ⊢ ((𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴) → (𝐵 = 𝐶 ↔ ¬ (𝐵𝑅𝐶 ∨ 𝐶𝑅𝐵))) |
|
Theorem | so0 4248 |
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.9 Founded and set-like
relations
|
|
Syntax | wfrfor 4249 |
Extend wff notation to include the well-founded predicate.
|
wff FrFor 𝑅𝐴𝑆 |
|
Syntax | wfr 4250 |
Extend wff notation to include the well-founded predicate. Read: ' 𝑅
is a well-founded relation on 𝐴.'
|
wff 𝑅 Fr 𝐴 |
|
Syntax | wse 4251 |
Extend wff notation to include the set-like predicate. Read: ' 𝑅 is
set-like on 𝐴.'
|
wff 𝑅 Se 𝐴 |
|
Syntax | wwe 4252 |
Extend wff notation to include the well-ordering predicate. Read:
' 𝑅 well-orders 𝐴.'
|
wff 𝑅 We 𝐴 |
|
Definition | df-frfor 4253* |
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 4254* |
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 4255* |
Define the set-like predicate. (Contributed by Mario Carneiro,
19-Nov-2014.)
|
⊢ (𝑅 Se 𝐴 ↔ ∀𝑥 ∈ 𝐴 {𝑦 ∈ 𝐴 ∣ 𝑦𝑅𝑥} ∈ V) |
|
Definition | df-wetr 4256* |
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 do not have that
as seen at ordtriexmid 4437). Given excluded middle, well-ordering is
usually defined to require trichotomy (and the definition of Fr is
typically also different). (Contributed by Mario Carneiro and Jim
Kingdon, 23-Sep-2021.)
|
⊢ (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧))) |
|
Theorem | seex 4257* |
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 4258 |
Any relation on a set is set-like on it. (Contributed by Mario
Carneiro, 22-Jun-2015.)
|
⊢ (𝐴 ∈ 𝑉 → 𝑅 Se 𝐴) |
|
Theorem | sess1 4259 |
Subset theorem for the set-like predicate. (Contributed by Mario
Carneiro, 24-Jun-2015.)
|
⊢ (𝑅 ⊆ 𝑆 → (𝑆 Se 𝐴 → 𝑅 Se 𝐴)) |
|
Theorem | sess2 4260 |
Subset theorem for the set-like predicate. (Contributed by Mario
Carneiro, 24-Jun-2015.)
|
⊢ (𝐴 ⊆ 𝐵 → (𝑅 Se 𝐵 → 𝑅 Se 𝐴)) |
|
Theorem | seeq1 4261 |
Equality theorem for the set-like predicate. (Contributed by Mario
Carneiro, 24-Jun-2015.)
|
⊢ (𝑅 = 𝑆 → (𝑅 Se 𝐴 ↔ 𝑆 Se 𝐴)) |
|
Theorem | seeq2 4262 |
Equality theorem for the set-like predicate. (Contributed by Mario
Carneiro, 24-Jun-2015.)
|
⊢ (𝐴 = 𝐵 → (𝑅 Se 𝐴 ↔ 𝑅 Se 𝐵)) |
|
Theorem | nfse 4263 |
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 4264 |
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 4265 |
Equality theorem for the well-founded predicate. (Contributed by Jim
Kingdon, 22-Sep-2021.)
|
⊢ (𝑅 = 𝑆 → ( FrFor 𝑅𝐴𝑇 ↔ FrFor 𝑆𝐴𝑇)) |
|
Theorem | freq1 4266 |
Equality theorem for the well-founded predicate. (Contributed by NM,
9-Mar-1997.)
|
⊢ (𝑅 = 𝑆 → (𝑅 Fr 𝐴 ↔ 𝑆 Fr 𝐴)) |
|
Theorem | frforeq2 4267 |
Equality theorem for the well-founded predicate. (Contributed by Jim
Kingdon, 22-Sep-2021.)
|
⊢ (𝐴 = 𝐵 → ( FrFor 𝑅𝐴𝑇 ↔ FrFor 𝑅𝐵𝑇)) |
|
Theorem | freq2 4268 |
Equality theorem for the well-founded predicate. (Contributed by NM,
3-Apr-1994.)
|
⊢ (𝐴 = 𝐵 → (𝑅 Fr 𝐴 ↔ 𝑅 Fr 𝐵)) |
|
Theorem | frforeq3 4269 |
Equality theorem for the well-founded predicate. (Contributed by Jim
Kingdon, 22-Sep-2021.)
|
⊢ (𝑆 = 𝑇 → ( FrFor 𝑅𝐴𝑆 ↔ FrFor 𝑅𝐴𝑇)) |
|
Theorem | nffrfor 4270 |
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 4271 |
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 4272 |
A well-founded relation is irreflexive. This is the case where 𝐴
exists. (Contributed by Jim Kingdon, 21-Sep-2021.)
|
⊢ ((𝑅 Fr 𝐴 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝐴) → ¬ 𝐵𝑅𝐵) |
|
Theorem | fr0 4273 |
Any relation is well-founded on the empty set. (Contributed by NM,
17-Sep-1993.)
|
⊢ 𝑅 Fr ∅ |
|
Theorem | frind 4274* |
Induction over a well-founded set. (Contributed by Jim Kingdon,
28-Sep-2021.)
|
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) & ⊢ ((𝜒 ∧ 𝑥 ∈ 𝐴) → (∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → 𝜓) → 𝜑)) & ⊢ (𝜒 → 𝑅 Fr 𝐴)
& ⊢ (𝜒 → 𝐴 ∈ 𝑉) ⇒ ⊢ ((𝜒 ∧ 𝑥 ∈ 𝐴) → 𝜑) |
|
Theorem | efrirr 4275 |
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 4276 |
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 4277 |
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 4278 |
Equality theorem for the well-ordering predicate. (Contributed by NM,
9-Mar-1997.)
|
⊢ (𝑅 = 𝑆 → (𝑅 We 𝐴 ↔ 𝑆 We 𝐴)) |
|
Theorem | weeq2 4279 |
Equality theorem for the well-ordering predicate. (Contributed by NM,
3-Apr-1994.)
|
⊢ (𝐴 = 𝐵 → (𝑅 We 𝐴 ↔ 𝑅 We 𝐵)) |
|
Theorem | wefr 4280 |
A well-ordering is well-founded. (Contributed by NM, 22-Apr-1994.)
|
⊢ (𝑅 We 𝐴 → 𝑅 Fr 𝐴) |
|
Theorem | wepo 4281 |
A well-ordering is a partial ordering. (Contributed by Jim Kingdon,
23-Sep-2021.)
|
⊢ ((𝑅 We 𝐴 ∧ 𝐴 ∈ 𝑉) → 𝑅 Po 𝐴) |
|
Theorem | wetrep 4282* |
An epsilon well-ordering is a transitive relation. (Contributed by NM,
22-Apr-1994.)
|
⊢ (( E We 𝐴 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝑧) → 𝑥 ∈ 𝑧)) |
|
Theorem | we0 4283 |
Any relation is a well-ordering of the empty set. (Contributed by NM,
16-Mar-1997.)
|
⊢ 𝑅 We ∅ |
|
2.3.10 Ordinals
|
|
Syntax | word 4284 |
Extend the definition of a wff to include the ordinal predicate.
|
wff Ord 𝐴 |
|
Syntax | con0 4285 |
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 |
|
Syntax | wlim 4286 |
Extend the definition of a wff to include the limit ordinal predicate.
|
wff Lim 𝐴 |
|
Syntax | csuc 4287 |
Extend class notation to include the successor function.
|
class suc 𝐴 |
|
Definition | df-iord 4288* |
Define the ordinal predicate, which is true for a class that is
transitive and whose elements are transitive. Definition of ordinal in
[Crosilla], p. "Set-theoretic
principles incompatible with
intuitionistic logic". (Contributed by Jim Kingdon, 10-Oct-2018.)
Use
its alias dford3 4289 instead for naming consistency with set.mm.
(New usage is discouraged.)
|
⊢ (Ord 𝐴 ↔ (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 Tr 𝑥)) |
|
Theorem | dford3 4289* |
Alias for df-iord 4288. Use it instead of df-iord 4288 for naming
consistency with set.mm. (Contributed by Jim Kingdon, 10-Oct-2018.)
|
⊢ (Ord 𝐴 ↔ (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 Tr 𝑥)) |
|
Definition | df-on 4290 |
Define the class of all ordinal numbers. Definition 7.11 of
[TakeutiZaring] p. 38. (Contributed
by NM, 5-Jun-1994.)
|
⊢ On = {𝑥 ∣ Ord 𝑥} |
|
Definition | df-ilim 4291 |
Define the limit ordinal predicate, which is true for an ordinal that has
the empty set as an element and is not a successor (i.e. that is the union
of itself). Our definition combines the definition of Lim of
[BellMachover] p. 471 and Exercise 1
of [TakeutiZaring] p. 42, and then
changes 𝐴 ≠ ∅ to ∅ ∈ 𝐴 (which would be equivalent given the
law of the excluded middle, but which is not for us). (Contributed by Jim
Kingdon, 11-Nov-2018.) Use its alias dflim2 4292 instead for naming
consistency with set.mm. (New usage is discouraged.)
|
⊢ (Lim 𝐴 ↔ (Ord 𝐴 ∧ ∅ ∈ 𝐴 ∧ 𝐴 = ∪ 𝐴)) |
|
Theorem | dflim2 4292 |
Alias for df-ilim 4291. Use it instead of df-ilim 4291 for naming consistency
with set.mm. (Contributed by NM, 4-Nov-2004.)
|
⊢ (Lim 𝐴 ↔ (Ord 𝐴 ∧ ∅ ∈ 𝐴 ∧ 𝐴 = ∪ 𝐴)) |
|
Definition | df-suc 4293 |
Define the successor of a class. When applied to an ordinal number, the
successor means the same thing as "plus 1". Definition 7.22 of
[TakeutiZaring] p. 41, who use
"+ 1" to denote this function. Our
definition is a generalization to classes. Although it is not
conventional to use it with proper classes, it has no effect on a proper
class (sucprc 4334). Some authors denote the successor
operation with a
prime (apostrophe-like) symbol, such as Definition 6 of [Suppes] p. 134
and the definition of successor in [Mendelson] p. 246 (who uses the symbol
"Suc" as a predicate to mean "is a successor
ordinal"). The definition of
successor of [Enderton] p. 68 denotes the
operation with a plus-sign
superscript. (Contributed by NM, 30-Aug-1993.)
|
⊢ suc 𝐴 = (𝐴 ∪ {𝐴}) |
|
Theorem | ordeq 4294 |
Equality theorem for the ordinal predicate. (Contributed by NM,
17-Sep-1993.)
|
⊢ (𝐴 = 𝐵 → (Ord 𝐴 ↔ Ord 𝐵)) |
|
Theorem | elong 4295 |
An ordinal number is an ordinal set. (Contributed by NM,
5-Jun-1994.)
|
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ On ↔ Ord 𝐴)) |
|
Theorem | elon 4296 |
An ordinal number is an ordinal set. (Contributed by NM,
5-Jun-1994.)
|
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ∈ On ↔ Ord 𝐴) |
|
Theorem | eloni 4297 |
An ordinal number has the ordinal property. (Contributed by NM,
5-Jun-1994.)
|
⊢ (𝐴 ∈ On → Ord 𝐴) |
|
Theorem | elon2 4298 |
An ordinal number is an ordinal set. (Contributed by NM, 8-Feb-2004.)
|
⊢ (𝐴 ∈ On ↔ (Ord 𝐴 ∧ 𝐴 ∈ V)) |
|
Theorem | limeq 4299 |
Equality theorem for the limit predicate. (Contributed by NM,
22-Apr-1994.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
|
⊢ (𝐴 = 𝐵 → (Lim 𝐴 ↔ Lim 𝐵)) |
|
Theorem | ordtr 4300 |
An ordinal class is transitive. (Contributed by NM, 3-Apr-1994.)
|
⊢ (Ord 𝐴 → Tr 𝐴) |