Statement List for Metamath Proof Explorer - 4201-4300 - Page 43 of 107
| Type | Label | Description |
|---|
| Statement |
|---|
| |
| Theorem | omordlim 4201 |
Ordering involving the product of a limit ordinal. Proposition 8.23 of
[TakeutiZaring] p. 64.
|
| ⊢
(((A ∈ On ⋀ (B ∈ D
⋀ Lim B)) ⋀ C ∈ (A
·o B)) →
∃x ∈ B C ∈
(A ·o x)) |
| |
| Theorem | omlimcl 4202 |
The product of any nonzero ordinal with a limit ordinal is a limit
ordinal. Proposition 8.24 of [TakeutiZaring] p. 64.
|
| ⊢
(((A ∈ On ⋀ (B ∈ C
⋀ Lim B)) ⋀ ∅ ∈
A) → Lim (A ·o B)) |
| |
| Theorem | odi 4203 |
Distributive law for ordinal arithmetic. Proposition 8.25 of
[TakeutiZaring] p. 64.
Warning: The HTML proof page is 3/4 megabyte
in size.
|
| ⊢
((A ∈ On ⋀ B ∈ On ⋀ C ∈ On) → (A ·o (B +o C)) = ((A
·o B)
+o (A
·o C))) |
| |
| Theorem | omass 4204 |
Multiplication of ordinal numbers is associative. Theorem 8.26 of
[TakeutiZaring] p. 65.
|
| ⊢
((A ∈ On ⋀ B ∈ On ⋀ C ∈ On) → ((A ·o B) ·o C) = (A
·o (B
·o C))) |
| |
| Theorem | oneo 4205 |
If an ordinal number is even, its successor is odd.
|
| ⊢
((A ∈ On ⋀ B ∈ On ⋀ C = (2o
·o A)) →
¬ suc C = (2o
·o B)) |
| |
| Theorem | oen0 4206 |
Ordinal exponentiation with a nonzero mantissa is nonzero. Proposition
8.32 of [TakeutiZaring] p. 67.
|
| ⊢
(((A ∈ On ⋀ B ∈ On) ⋀ ∅ ∈ A) → ∅ ∈ (A ↑o B)) |
| |
| Theorem | oeordi 4207 |
Ordering law for ordinal exponentiation. Proposition 8.33 of
[TakeutiZaring] p. 67.
|
| ⊢
(((B ∈ On ⋀ C ∈ On) ⋀ 1o ∈
C) → (A ∈ B
→ (C ↑o
A) ∈ (C ↑o B))) |
| |
| Theorem | oeord 4208 |
Ordering property of ordinal exponentiation. Corollary 8.34 of
[TakeutiZaring] p. 68 and its
converse.
|
| ⊢
(((A ∈ On ⋀ B ∈ On ⋀ C ∈ On) ⋀ 1o ∈
C) → (A ∈ B
↔ (C ↑o
A) ∈ (C ↑o B))) |
| |
| Theorem | oecan 4209 |
Left cancellation law for ordinal exponentiation.
|
| ⊢
(((A ∈ On ⋀ B ∈ On ⋀ C ∈ On) ⋀ 1o ∈
A) → ((A ↑o B) = (A
↑o C) ↔
B = C)) |
| |
| Theorem | oeword 4210 |
Weak ordering property of ordinal exponentiation.
|
| ⊢
(((A ∈ On ⋀ B ∈ On ⋀ C ∈ On) ⋀ 1o ∈
C) → (A ⊆ B
↔ (C ↑o
A) ⊆ (C ↑o B))) |
| |
| Theorem | oewordi 4211 |
Weak ordering property of ordinal exponentiation.
|
| ⊢
(((A ∈ On ⋀ B ∈ On ⋀ C ∈ On) ⋀ ∅ ∈ C) → (A
⊆ B → (C ↑o A) ⊆ (C
↑o B))) |
| |
| Theorem | oewordri 4212 |
Weak ordering property of ordinal exponentiation. Proposition 8.35 of
[TakeutiZaring] p. 68.
|
| ⊢
((B ∈ On ⋀ C ∈ On) → (A ∈ B
→ (A ↑o
C) ⊆ (B ↑o C))) |
| |
| Theorem | oeworde 4213 |
Ordinal exponentiation compared to its exponent. Proposition 8.37 of
[TakeutiZaring] p. 68.
|
| ⊢
(((A ∈ On ⋀ B ∈ On) ⋀ 1o ∈
A) → B ⊆ (A
↑o B)) |
| |
| Theorem | oeordsuc 4214 |
Ordering property of ordinal exponentiation with a successor exponent.
Corollary 8.36 of [TakeutiZaring]
p. 68.
|
| ⊢
((B ∈ On ⋀ C ∈ On) → (A ∈ B
→ (A ↑o suc
C) ∈ (B ↑o suc C))) |
| |
| Theorem | oelim2 4215 |
Ordinal exponentiation with a limit exponent. Part of Exercise 4.36 of
[Mendelson] p. 250.
|
| ⊢
((A ∈ On ⋀ (B ∈ C
⋀ Lim B)) → (A ↑o B) = ∪x ∈ (B
∖ 1o)(A
↑o x)) |
| |
| Natural number arithmetic |
| |
| Theorem | nna0 4216 |
Addition with zero. Theorem 4I(A1) of [Enderton] p. 79.
|
| ⊢
(A ∈ ω → (A +o ∅) = A) |
| |
| Theorem | nnm0 4217 |
Multiplication with zero. Theorem 4J(A1) of [Enderton] p. 80.
|
| ⊢
(A ∈ ω → (A ·o ∅) =
∅) |
| |
| Theorem | nnasuc 4218 |
Addition with successor. Theorem 4I(A2) of [Enderton] p. 79.
|
| ⊢
((A ∈ ω ⋀ B ∈ ω) → (A +o suc B) = suc (A
+o B)) |
| |
| Theorem | nnmsuc 4219 |
Multiplication with successor. Theorem 4J(A2) of [Enderton] p. 80.
|
| ⊢
((A ∈ ω ⋀ B ∈ ω) → (A ·o suc B) = ((A
·o B)
+o A)) |
| |
| Theorem | nna0r 4220 |
Addition to zero. Remark in proof of Theorem 4K(2) of [Enderton]
p. 81.
|
| ⊢
(A ∈ ω → (∅
+o A) = A) |
| |
| Theorem | nnm0r 4221 |
Multiplication with zero. Exercise 16 of [Enderton] p. 82.
|
| ⊢
(A ∈ ω → (∅
·o A) =
∅) |
| |
| Theorem | nnacl 4222 |
Closure of addition of natural numbers. Proposition 8.9 of
[TakeutiZaring] p. 59.
|
| ⊢
((A ∈ ω ⋀ B ∈ ω) → (A +o B) ∈ ω) |
| |
| Theorem | nnmcl 4223 |
Closure of multiplication of natural numbers. Proposition 8.17 of
[TakeutiZaring] p. 63.
|
| ⊢
((A ∈ ω ⋀ B ∈ ω) → (A ·o B) ∈ ω) |
| |
| Theorem | nnecl 4224 |
Closure of exponentiation of natural numbers. Proposition 8.17 of
[TakeutiZaring] p. 63.
|
| ⊢
((A ∈ ω ⋀ B ∈ ω) → (A ↑o B) ∈ ω) |
| |
| Theorem | nnarcl 4225 |
Reverse closure law for addition of natural numbers. Exercise 1 of
[TakeutiZaring] p. 62 and its
converse.
|
| ⊢
((A ∈ On ⋀ B ∈ On) → ((A +o B) ∈ ω ↔ (A ∈ ω ⋀ B ∈ ω))) |
| |
| Theorem | nnacom 4226 |
Addition of natural numbers is commutative. Theorem 4K(2) of
[Enderton] p. 81.
|
| ⊢
((A ∈ ω ⋀ B ∈ ω) → (A +o B) = (B
+o A)) |
| |
| Theorem | nnaordi 4227 |
Ordering property of addition. Proposition 8.4 of [TakeutiZaring] p. 58,
limited to natural numbers.
|
| ⊢
((B ∈ ω ⋀ C ∈ ω) → (A ∈ B
→ (C +o A) ∈ (C
+o B))) |
| |
| Theorem | nnaord 4228 |
Ordering property of addition. Proposition 8.4 of [TakeutiZaring] p. 58,
limited to natural numbers, and its converse.
|
| ⊢
((A ∈ ω ⋀ B ∈ ω ⋀ C ∈ ω) → (A ∈ B
↔ (C +o A) ∈ (C
+o B))) |
| |
| Theorem | nnaordr 4229 |
Ordering property of addition of natural numbers.
|
| ⊢
((A ∈ ω ⋀ B ∈ ω ⋀ C ∈ ω) → (A ∈ B
↔ (A +o C) ∈ (B
+o C))) |
| |
| Theorem | nnaass 4230 |
Addition of natural numbers is associative. (For brevity, this is just a
special case of the proof for ordinals. A direct proof would be about 1/3
the size of the ordinal proof, since it would use finite induction and not
require the limit ordinal case..) Theorem 4K(1) of [Enderton] p. 81.
|
| ⊢
((A ∈ ω ⋀ B ∈ ω ⋀ C ∈ ω) → ((A +o B) +o C) = (A
+o (B
+o C))) |
| |
| Theorem | nndi 4231 |
Distributive law for natural numbers. (For brevity, this is just a
special case of the proof for ordinals. A direct proof would be about 1/4
the size of the ordinal proof, since it would use finite induction and not
require the limit ordinal case.) Theorem 4K(3) of [Enderton] p. 81.
|
| ⊢
((A ∈ ω ⋀ B ∈ ω ⋀ C ∈ ω) → (A ·o (B +o C)) = ((A
·o B)
+o (A
·o C))) |
| |
| Theorem | nnmass 4232 |
Multiplication of natural numbers is associative. (For brevity, this is
just a special case of the proof for ordinals. A direct proof would be
about 1/3 the size of the ordinal proof, since it would use finite
induction and not require the limit ordinal case..) Theorem 4K(4) of
[Enderton] p. 81.
|
| ⊢
((A ∈ ω ⋀ B ∈ ω ⋀ C ∈ ω) → ((A ·o B) ·o C) = (A
·o (B
·o C))) |
| |
| Theorem | nnmsucr 4233 |
Multiplication with successor. Exercise 16 of [Enderton] p. 82.
|
| ⊢
((A ∈ ω ⋀ B ∈ ω) → (suc A ·o B) = ((A
·o B)
+o B)) |
| |
| Theorem | nnmcom 4234 |
Multiplication of natural numbers is commutative. Theorem 4K(5) of
[Enderton] p. 81.
|
| ⊢
((A ∈ ω ⋀ B ∈ ω) → (A ·o B) = (B
·o A)) |
| |
| Theorem | nnacan 4235 |
Cancellation law for addition of natural numbers.
|
| ⊢
((A ∈ ω ⋀ B ∈ ω ⋀ C ∈ ω) → ((A +o B) = (A
+o C) ↔ B = C)) |
| |
| Theorem | nnaword 4236 |
Weak ordering property of addition.
|
| ⊢
((A ∈ ω ⋀ B ∈ ω ⋀ C ∈ ω) → (A ⊆ B
↔ (C +o A) ⊆ (C
+o B))) |
| |
| Theorem | nnaword1 4237 |
Weak ordering property of addition.
|
| ⊢
((A ∈ ω ⋀ B ∈ ω) → A ⊆ (A
+o B)) |
| |
| Theorem | nnaword2 4238 |
Weak ordering property of addition.
|
| ⊢
((A ∈ ω ⋀ B ∈ ω) → A ⊆ (B
+o A)) |
| |
| Theorem | nnmordi 4239 |
Ordering property of multiplication. Half of Proposition 8.19 of
[TakeutiZaring] p. 63, limited to
natural numbers.
|
| ⊢
((A ∈ ω ⋀ B ∈ ω ⋀ C ∈ ω) → ((A ∈ B
⋀ ∅ ∈ C) → (C ·o A) ∈ (C
·o B))) |
| |
| Theorem | nnmord 4240 |
Ordering property of multiplication. Proposition 8.19 of
[TakeutiZaring] p. 63, limited to
natural numbers.
|
| ⊢
((A ∈ ω ⋀ B ∈ ω ⋀ C ∈ ω) → ((A ∈ B
⋀ ∅ ∈ C) ↔ (C ·o A) ∈ (C
·o B))) |
| |
| Theorem | nnmcan 4241 |
Cancellation law for multiplication of natural numbers.
|
| ⊢
(((A ∈ ω ⋀
B ∈ ω ⋀ C ∈ ω) ⋀ ∅ ∈ A) → ((A
·o B) = (A ·o C) ↔ B =
C)) |
| |
| Theorem | nnaordex 4242 |
Equivalence for ordering. Compare Exercise 23 of [Enderton] p. 88.
|
| ⊢
((A ∈ ω ⋀ B ∈ ω) → (A ∈ B
↔ ∃x ∈ ω (∅
∈ x ⋀ (A +o x) = B))) |
| |
| Theorem | nnawordex 4243 |
Equivalence for weak ordering of natural numbers.
|
| ⊢
((A ∈ ω ⋀ B ∈ ω) → (A ⊆ B
↔ ∃x ∈ ω (A +o x) = B)) |
| |
| Theorem | oaabslem 4244 |
Lemma for oaabs 4245.
|
| |
| Theorem | oaabs 4245 |
Ordinal addition absorbs a natural number added to the left of a
transfinite number. Proposition 8.10 of [TakeutiZaring] p. 59.
|
| ⊢
(((A ∈ ω ⋀
B ∈ On) ⋀ ω ⊆
B) → (A +o B) = B) |
| |
| Theorem | 1onn 4246 |
One is a natural number.
|
| ⊢
1o ∈ ω |
| |
| Theorem | 2onn 4247 |
The ordinal 2 is a natural number.
|
| ⊢
2o ∈ ω |
| |
| Theorem | nneob 4248 |
A natural number is even iff its successor is odd.
|
| ⊢
(A ∈ ω →
(∃x ∈ ω A = (2o
·o x) ↔
¬ ∃x ∈ ω suc A = (2o
·o x))) |
| |
| Theorem | omsmolem 4249 |
Lemma for omsmo 4250.
|
| |
| Theorem | omsmo 4250 |
A strictly monotonic ordinal function on the set of natural numbers
is one-to-one.
|
| ⊢
(((A ⊆ On ⋀ F:ω–→A) ⋀ ∀x ∈ ω (F ‘x)
∈ (F ‘suc x)) → F:ω–1-1→A) |
| |
| Equivalence relations and classes |
| |
| Syntax | wer 4251 |
Extend the definition of a wff to include the equivalence predicate.
|
| wff Er
R |
| |
| Syntax | cec 4252 |
Extend the definition of a class to include equivalence class.
|
| class
[A]R |
| |
| Syntax | cqs 4253 |
Extend the definition of a class to include quotient set.
|
| class
(A / R) |
| |
| Definition | df-er 4254 |
Define the equivalence predicate. R need
not be a relation but
ordinarily will be, in which case we call it an equivalence relation.
Our notation is not standard. A formal notation doesn't seem to exist
in the literature; instead only informal English tends to be used. Some
definitions in the literature may also require that R be a relation.
The present definition, although somewhat cryptic, nicely avoids dummy
variables. In dfer2 4255 we derive a more typical definition. We show
that
an equivalence relation is reflexive, symmetric, and transitive in
erref 4268, ersymb 4266, and ertr 4267.
|
| ⊢
(Er R ↔ (◡R ∪
(R ∘ R)) ⊆ R) |
| |
| Theorem | dfer2 4255 |
Alternate definition of equivalence predicate.
|
| ⊢
(Er R ↔ ∀x∀y∀z((xRy →
yRx) ⋀
((xRy ⋀
yRz) →
xRz))) |
| |
| Definition | df-ec 4256 |
Define the R -coset of A. Exercise 35 of [Enderton] p. 61. This
is called the equivalence class of A
modulo R when R is an
equivalence relation. The Definition of [Enderton] p. 57 uses the
notation [A] (subscript) R, although we simply follow the
brackets by R since we don't have
subscripts.
For an alternate definition, see dfec2 4257.
|
| ⊢
[A]R = (R “
{A}) |
| |
| Theorem | dfec2 4257 |
Alternate definition of R-coset of A. Definition 34 of
[Suppes] p. 81.
|
| ⊢
A ∈ V
⇒ ⊢ [A]R = {y∣ARy} |
| |
| Theorem | ecexg 4258 |
An equivalence class modulo a set is a set.
|
| ⊢
(R ∈ B → [A]R ∈
V) |
| |
| Definition | df-qs 4259 |
Define quotient set. R is usually an
equivalence relation.
Definition of [Enderton] p. 58.
|
| ⊢
(A / R) = {y∣∃x ∈ A
y = [x]R} |
| |
| Theorem | ereq 4260 |
Equality theorem for equivalence predicate.
|
| ⊢
(R = S → (Er R
↔ Er S)) |
| |
| Theorem | ster 4261 |
A symmetric, transitive relation is an equivalence relation.
|
| ⊢
(xRy →
yRx) & ⊢ ((xRy ⋀
yRz) →
xRz) ⇒ ⊢ Er R |
| |
| Theorem | ider 4262 |
The identity relation is an equivalence relation.
|
| ⊢
Er I |
| |
| Theorem | eqerlem 4263 |
Lemma for eqer 4264.
|
| |
| Theorem | eqer 4264 |
Equivalence relation involving equality of dependent classes
A(x) and B(y).
|
| ⊢
(x = y → A =
B)
& ⊢ R = {⟨x,
y⟩∣A = B} ⇒ ⊢ Er R |
| |
| Theorem | ersym 4265 |
An equivalence relation is symmetric.
|
| ⊢
A ∈ V
& ⊢ B ∈ V
& ⊢ Er R ⇒ ⊢ (ARB →
BRA) |
| |
| Theorem | ersymb 4266 |
An equivalence relation is symmetric.
|
| ⊢
A ∈ V
& ⊢ B ∈ V
& ⊢ Er R ⇒ ⊢ (ARB ↔
BRA) |
| |
| Theorem | ertr 4267 |
An equivalence relation is transitive.
|
| ⊢
A ∈ V
& ⊢ B ∈ V
& ⊢ C ∈ V
& ⊢ Er R ⇒ ⊢ ((ARB ⋀
BRC) →
ARC) |
| |
| Theorem | erref 4268 |
An equivalence relation is reflexive on its field. Compare
Theorem 3M of [Enderton] p. 56.
|
| ⊢
Er R
⇒ ⊢ (A ∈ (dom R
∪ ran R) → ARA) |
| |
| Theorem | erdmrn 4269 |
The range and domain of an equivalence relation are equal.
|
| ⊢
Er R
⇒ ⊢ dom R = ran R |
| |
| Theorem | eceq1 4270 |
Equality theorem for equivalence class.
|
| ⊢
(A = B → [C]A = [C]B) |
| |
| Theorem | eceq2 4271 |
Equality theorem for equivalence class.
|
| ⊢
(A = B → [A]C = [B]C) |
| |
| Theorem | elec 4272 |
Membership in an equivalence class. Theorem 72 of [Suppes] p. 82.
|
| ⊢
A ∈ V
& ⊢ B ∈ V
⇒ ⊢ (A ∈ [B]R ↔
BRA) |
| |
| Theorem | ecdmn0 4273 |
An equivalence class is not empty in its domain.
|
| ⊢
A ∈ V
⇒ ⊢ (A ∈ dom R
↔ ¬ [A]R = ∅) |
| |
| Theorem | erthi 4274 |
Basic property of equivalence relations. Part of Lemma 3N of [Enderton]
p. 57.
|
| ⊢
A ∈ V
& ⊢ B ∈ V
& ⊢ Er R ⇒ ⊢ (ARB →
[A]R =
[B]R) |
| |
| Theorem | erth 4275 |
Basic property of equivalence relations. Theorem 73 of [Suppes]
p. 82.
|
| ⊢
B ∈ V
& ⊢ Er R ⇒ ⊢ (A ∈
(dom R ∪ ran R) → ([A]R = [B]R ↔
ARB)) |
| |
| Theorem | erthdm 4276 |
Basic property of equivalence relations. Compare Theorem 73 of [Suppes]
p. 82. Assumes membership in the domain instead of just the field.
|
| ⊢
B ∈ V
& ⊢ Er R ⇒ ⊢ (A ∈
dom R → ([A]R = [B]R ↔
ARB)) |
| |
| Theorem | erthdmr 4277 |
Basic property of equivalence relations. Compare Theorem 73 of [Suppes]
p. 82. Assumes membership of the second argument in the domain.
|
| ⊢
A ∈ V
& ⊢ B ∈ V
& ⊢ Er R ⇒ ⊢ (B ∈
dom R → ([A]R = [B]R ↔
ARB)) |
| |
| Theorem | ereldm 4278 |
Equality of equivalence classes implies equivalence of domain
membership.
|
| ⊢
A ∈ V
& ⊢ B ∈ V
& ⊢ Er R & ⊢ dom R =
D
⇒ ⊢ ([A]R = [B]R →
(A ∈ D ↔ B
∈ D)) |
| |
| Theorem | erdisj 4279 |
Equivalence classes do not overlap. In other words, two equivalence
classes are either equal or disjoint. Theorem 74 of [Suppes] p. 83.
|
| ⊢
A ∈ V
& ⊢ B ∈ V
& ⊢ Er R ⇒ ⊢ ([A]R = [B]R ⋁
([A]R
∩ [B]R) = ∅) |
| |
| Theorem | ecidsn 4280 |
An equivalence class modulo the identity relation is a singleton.
|
| ⊢
[A]I = {A} |
| |
| Theorem | qseq1 4281 |
Equality theorem for quotient set.
|
| ⊢
(A = B → (A
/ C) = (B / C)) |
| |
| Theorem | qseq2 4282 |
Equality theorem for quotient set.
|
| ⊢
(A = B → (C
/ A) = (C / B)) |
| |
| Theorem | elqs 4283 |
Membership in a quotient set.
|
| ⊢
B ∈ V
⇒ ⊢ (B ∈ (A
/ R) ↔ ∃x(x ∈
A ⋀ B = [x]R)) |
| |
| Theorem | elqsi 4284 |
Membership in a quotient set.
|
| ⊢
(B ∈ (A / R)
→ ∃x(x ∈ A
⋀ B = [x]R)) |
| |
| Theorem | ecelqsi 4285 |
Membership of an equivalence class in a quotient set.
|
| ⊢
R ∈ V
⇒ ⊢ (B ∈ A
→ [B]R ∈ (A
/ R)) |
| |
| Theorem | ecopqsi 4286 |
"Closure" law for equivalence class of ordered pairs.
|
| ⊢
R ∈ V
& ⊢ S = ((A ×
A) / R) ⇒ ⊢ ((B ∈
A ⋀ C ∈ A)
→ [⟨B, C⟩]R
∈ S) |
| |
| Theorem | qsexg 4287 |
A quotient set exists. (Contributed by FL, 19-May-2007.)
|
| ⊢
(A ∈ V → (A / R)
∈ V) |
| |
| Theorem | qsex 4288 |
A quotient set exists.
|
| ⊢
A ∈ V
⇒ ⊢ (A / R)
∈ V |
| |
| Theorem | snec 4289 |
The singleton of an equivalence class.
|
| ⊢
A ∈ V
⇒ ⊢ {[A]R} =
({A} / R) |
| |
| Theorem | ecqs 4290 |
Equivalence class in terms of quotient set.
|
| ⊢
A ∈ V
& ⊢ R ∈ V
⇒ ⊢ [A]R = ∪({A} /
R) |
| |
| Theorem | 0nelqs 4291 |
A quotient set doesn't contain the empty set.
|
| ⊢
dom R = A ⇒ ⊢ ¬ ∅ ∈ (A / R) |
| |
| Theorem | ecelqsdm 4292 |
Membership of an equivalence class in a quotient set.
|
| ⊢
B ∈ V
& ⊢ dom R = A ⇒ ⊢ ([B]R ∈
(A / R) → B
∈ A) |
| |
| Theorem | ecid 4293 |
A set is equal to its converse epsilon coset. (Note: converse epsilon
is not an equivalence relation.)
|
| ⊢
A ∈ V
⇒ ⊢ [A]◡E
= A |
| |
| Theorem | qsid 4294 |
A set is equal to its quotient set mod converse epsilon. (Note: converse
epsilon is not an equivalence relation.)
|
| ⊢
(A / ◡E) = A |
| |
| Theorem | ectocl 4295 |
Implicit substitution of class for equivalence class.
|
| ⊢
S = (B / R) & ⊢ ([x]R = A → (φ
↔ ψ))
& ⊢ (x ∈ B
→ φ)
⇒ ⊢ (A ∈ S
→ ψ) |
| |
| Theorem | ecoptocl 4296 |
Implicit substitution of class for equivalence class of ordered pair.
|
| ⊢
S = ((B × C)
/ R)
& ⊢ ([⟨x, y⟩]R =
A → (φ ↔ ψ))
& ⊢ ((x ∈ B
⋀ y ∈ C) → φ)
⇒ ⊢ (A ∈ S
→ ψ) |
| |
| Theorem | 2ecoptocl 4297 |
Implicit substitution of classes for equivalence classes of ordered
pairs.
|
| ⊢
S = ((C × D)
/ R)
& ⊢ ([⟨x, y⟩]R =
A → (φ ↔ ψ))
& ⊢ ([⟨z, w⟩]R =
B → (ψ ↔ χ))
& ⊢ (((x ∈ C
⋀ y ∈ D) ⋀ (z
∈ C ⋀ w ∈ D))
→ φ)
⇒ ⊢ ((A ∈ S
⋀ B ∈ S) → χ) |
| |
| Theorem | 3ecoptocl 4298 |
Implicit substitution of classes for equivalence classes of ordered
pairs.
|
| ⊢
S = ((D × D)
/ R)
& ⊢ ([⟨x, y⟩]R =
A → (φ ↔ ψ))
& ⊢ ([⟨z, w⟩]R =
B → (ψ ↔ χ))
& ⊢ ([⟨v, u⟩]R =
C → (χ ↔ θ))
& ⊢ (((x ∈ D
⋀ y ∈ D) ⋀ (z
∈ D ⋀ w ∈ D)
⋀ (v ∈ D ⋀ u
∈ D)) → φ)
⇒ ⊢ ((A ∈ S
⋀ B ∈ S ⋀ C
∈ S) → θ) |
| |
| Theorem | brecop 4299 |
Binary relation on a quotient set. Lemma for real number
construction.
|
| ⊢
S ∈ V
& ⊢ Er S & ⊢ dom S =
(G × G) & ⊢ H =
((G × G) / S) & ⊢ R =
{⟨x, y⟩∣((x ∈ H
⋀ y ∈ H) ⋀ ∃z∃w∃v∃u((x =
[⟨z, w⟩]S
⋀ y = [⟨v, u⟩]S)
⋀ φ))}
& ⊢ ((((z ∈ G
⋀ w ∈ G) ⋀ (A
∈ G ⋀ B ∈ G))
⋀ ((v ∈ G ⋀ u
∈ G) ⋀ (C ∈ G
⋀ D ∈ G))) → (([⟨z, w⟩]S =
[⟨A, B⟩]S
⋀ [⟨v, u⟩]S =
[⟨C, D⟩]S)
→ (φ ↔ ψ)))
⇒ ⊢ (((A ∈ G
⋀ B ∈ G) ⋀ (C
∈ G ⋀ D ∈ G))
→ ([⟨A, B⟩]SR[⟨C,
D⟩]S ↔ ψ)) |
| |
| Theorem | brecop2 4300 |
Binary relation on a quotient set. Lemma for real number
construction. Eliminates antecedent from last hypothesis.
|
| ⊢
S ∈ V
& ⊢ B ∈ V
& ⊢ C ∈ V
& ⊢ D ∈ V
& ⊢ dom S = (G ×
G)
& ⊢ H = ((G ×
G) / S) & ⊢ R ⊆
(H × H) & ⊢ Q ⊆
(G × G) & ⊢ ¬ ∅ ∈ G & ⊢ dom F =
(G × G) & ⊢ (((A ∈
G ⋀ B ∈ G)
⋀ (C ∈ G ⋀ D
∈ G)) → ([⟨A, B⟩]SR[⟨C,
D⟩]S ↔ (AFD)Q(BFC)))
⇒ ⊢ ([⟨A, B⟩]SR[⟨C,
D⟩]S ↔ (AFD)Q(BFC)) |
Home
Hilbert Space Explorer
(8744-10691)