Statement List for Metamath Proof Explorer - 4401-4500 - Page 45 of 107
| Type | Label | Description |
|---|
| Statement |
|---|
| |
| Theorem | ensymg 4401 |
Symmetry of equinumerosity. Theorem 2 of [Suppes] p. 92.
|
| ⊢
(B ∈ C → (A
≈ B → B ≈ A)) |
| |
| Theorem | ensym 4402 |
Symmetry of equinumerosity. Theorem 2 of [Suppes] p. 92.
|
| ⊢
B ∈ V
⇒ ⊢ (A ≈ B
→ B ≈ A) |
| |
| Theorem | ensymi 4403 |
Symmetry of equinumerosity. Theorem 2 of [Suppes] p. 92.
|
| ⊢
B ∈ V
& ⊢ A ≈ B ⇒ ⊢ B ≈
A |
| |
| Theorem | entrt 4404 |
Transitivity of equinumerosity. Theorem 3 of [Suppes] p. 92.
|
| ⊢
((A ≈ B ⋀ B
≈ C) → A ≈ C) |
| |
| Theorem | domtr 4405 |
Transitivity of dominance relation. Theorem 17 of [Suppes] p. 94.
|
| ⊢
((A ≼ B ⋀ B
≼ C) → A ≼ C) |
| |
| Theorem | entr 4406 |
A chained equinumerosity inference.
|
| ⊢
A ≈ B & ⊢ B ≈
C
⇒ ⊢ A ≈ C |
| |
| Theorem | entr2 4407 |
A chained equinumerosity inference.
|
| ⊢
C ∈ V
& ⊢ A ≈ B & ⊢ B ≈
C
⇒ ⊢ C ≈ A |
| |
| Theorem | entr3 4408 |
A chained equinumerosity inference.
|
| ⊢
B ∈ V
& ⊢ A ≈ B & ⊢ A ≈
C
⇒ ⊢ B ≈ C |
| |
| Theorem | entr4 4409 |
A chained equinumerosity inference.
|
| ⊢
B ∈ V
& ⊢ A ≈ B & ⊢ C ≈
B
⇒ ⊢ A ≈ C |
| |
| Theorem | endomtr 4410 |
Transitivity of equinumerosity and dominance.
|
| ⊢
((A ≈ B ⋀ B
≼ C) → A ≼ C) |
| |
| Theorem | domentr 4411 |
Transitivity of dominance and equinumerosity.
|
| ⊢
((A ≼ B ⋀ B
≈ C) → A ≼ C) |
| |
| Theorem | f1imaen 4412 |
A one-to-one function's image under a subset of its domain is
equinumerous to the subset.
|
| ⊢
C ∈ V
⇒ ⊢ ((F:A–1-1→B
⋀ C ⊆ A) → (F
“ C) ≈ C) |
| |
| Theorem | en0 4413 |
The empty set is equinumerous only to itself. Exercise 1 of
[TakeutiZaring] p. 88.
|
| ⊢
(A ≈ ∅ ↔ A = ∅) |
| |
| Theorem | ensn1 4414 |
A singleton is equinumerous to ordinal one.
|
| ⊢
A ∈ V
⇒ ⊢ {A} ≈ 1o |
| |
| Theorem | ensn1g 4415 |
A singleton is equinumerous to ordinal one.
|
| ⊢
(A ∈ B → {A}
≈ 1o) |
| |
| Theorem | en1 4416 |
A set is equinumerous to ordinal one iff it is a singleton.
|
| ⊢
(A ≈ 1o
↔ ∃x A = {x}) |
| |
| Theorem | 2dom 4417 |
A set that dominates ordinal 2 has at least 2 different members.
|
| ⊢
A ∈ V
⇒ ⊢
(2o ≼ A
→ ∃x ∈ A ∃y
∈ A ¬ x = y) |
| |
| Theorem | fundmen 4418 |
A function is equinumerous to its domain. Exercise 4 of [Suppes]
p. 98.
|
| ⊢
F ∈ V
⇒ ⊢ (Fun F → dom F
≈ F) |
| |
| Theorem | mapsnen 4419 |
Set exponentiation to a singleton exponent is equinumerous to its base.
Exercise 4.43 of [Mendelson] p. 255.
|
| ⊢
A ∈ V
& ⊢ B ∈ V
⇒ ⊢ (A ↑m {B}) ≈ A |
| |
| Theorem | map1 4420 |
Set exponentiation: ordinal 1 to any set is equinumerous to ordinal 1.
Exercise 4.42(b) of [Mendelson] p.
255.
|
| ⊢
A ∈ V
⇒ ⊢
(1o ↑m A) ≈ 1o |
| |
| Theorem | en2sn 4421 |
Two singletons are equinumerous.
|
| ⊢
((A ∈ C ⋀ B
∈ D) → {A} ≈ {B}) |
| |
| Theorem | snfi 4422 |
A singleton is finite.
|
| ⊢
∃x ∈ ω {A} ≈ x |
| |
| Theorem | unen 4423 |
Equinumerosity of union of disjoint sets. Theorem 4 of [Suppes]
p. 92.
|
| ⊢
(((A ≈ B ⋀ C
≈ D) ⋀ ((A ∩ C) =
∅ ⋀ (B ∩ D) = ∅)) → (A ∪ C)
≈ (B ∪ D)) |
| |
| Theorem | xpsnen 4424 |
A set is equinumerous to its cross-product with a singleton.
Proposition 4.22(c) of [Mendelson] p.
254.
|
| ⊢
A ∈ V
& ⊢ B ∈ V
⇒ ⊢ (A × {B})
≈ A |
| |
| Theorem | xpsneng 4425 |
A set is equinumerous to its cross-product with a singleton.
Proposition 4.22(c) of [Mendelson] p.
254.
|
| ⊢
((A ∈ C ⋀ B
∈ D) → (A × {B})
≈ A) |
| |
| Theorem | endisj 4426 |
Any two sets are equinumerous to disjoint sets. Exercise 4.39 of
[Mendelson] p. 255.
|
| ⊢
A ∈ V
& ⊢ B ∈ V
⇒ ⊢ ∃x∃y((x ≈
A ⋀ y ≈ B)
⋀ (x ∩ y) = ∅) |
| |
| Theorem | undom 4427 |
Dominance law for union. Proposition 4.24(a) of [Mendelson] p. 257.
|
| ⊢
B ∈ V
& ⊢ C ∈ V
& ⊢ D ∈ V
⇒ ⊢ (((A ≼ B
⋀ C ≼ D) ⋀ (B
∩ D) = ∅) → (A ∪ C)
≼ (B ∪ D)) |
| |
| Theorem | xpcomen 4428 |
Commutative law for equinumerosity of cross product. Proposition
4.22(d) of [Mendelson] p. 254.
|
| ⊢
A ∈ V
& ⊢ B ∈ V
⇒ ⊢ (A × B)
≈ (B × A) |
| |
| Theorem | xpcomeng 4429 |
Commutative law for equinumerosity of cross product. Proposition
4.22(d) of [Mendelson] p. 254.
|
| ⊢
((A ∈ C ⋀ B
∈ D) → (A × B)
≈ (B × A)) |
| |
| Theorem | xpassen 4430 |
Associative law for equinumerosity of cross product. Proposition
4.22(e) of [Mendelson] p. 254.
|
| ⊢
A ∈ V
& ⊢ B ∈ V
& ⊢ C ∈ V
⇒ ⊢ ((A × B)
× C) ≈ (A × (B
× C)) |
| |
| Theorem | xpdom2 4431 |
Dominance law for cross product. Proposition 10.33(2) of
[TakeutiZaring] p. 92.
|
| ⊢
B ∈ V
& ⊢ C ∈ V
⇒ ⊢ (A ≼ B
→ (C × A) ≼ (C
× B)) |
| |
| Theorem | xpdom1 4432 |
Dominance law for cross product. Theorem 6L(c) of [Enderton] p. 149.
|
| ⊢
B ∈ V
& ⊢ C ∈ V
⇒ ⊢ (A ≼ B
→ (A × C) ≼ (B
× C)) |
| |
| Theorem | xpdom1g 4433 |
Dominance law for cross product. Theorem 6L(c) of [Enderton] p. 149.
|
| ⊢
((B ∈ R ⋀ C
∈ S ⋀ A ≼ B)
→ (A × C) ≼ (B
× C)) |
| |
| Theorem | xpdom3 4434 |
A set is dominated by its cross product with a non-empty set. Exercise
6 of [Suppes] p. 98.
|
| ⊢
A ∈ V
⇒ ⊢ (B ≠ ∅ → A ≼ (A
× B)) |
| |
| Theorem | pw2en 4435 |
The power set of a set is equinumerous to set exponentiation with a base
of ordinal 2. Proposition 10.44 of [TakeutiZaring] p. 96. (This proof
seems excessively long. An attempt to find a shorter one is on my to-do
list.)
|
| ⊢
A ∈ V
⇒ ⊢ ℘A ≈ (2o
↑m A) |
| |
| Schroeder-Bernstein Theorem |
| |
| Theorem | sbthlem1 4436 |
Lemma for sbth 4446.
|
| |
| Theorem | sbthlem2 4437 |
Lemma for sbth 4446.
|
| |
| Theorem | sbthlem3 4438 |
Lemma for sbth 4446.
|
| |
| Theorem | sbthlem4 4439 |
Lemma for sbth 4446.
|
| |
| Theorem | sbthlem5 4440 |
Lemma for sbth 4446.
|
| |
| Theorem | sbthlem6 4441 |
Lemma for sbth 4446.
|
| |
| Theorem | sbthlem7 4442 |
Lemma for sbth 4446.
|
| |
| Theorem | sbthlem8 4443 |
Lemma for sbth 4446.
|
| |
| Theorem | sbthlem9 4444 |
Lemma for sbth 4446.
|
| |
| Theorem | sbthlem10 4445 |
Lemma for sbth 4446.
|
| |
| Theorem | sbth 4446 |
Schroeder-Bernstein Theorem. Theorem 18 of [Suppes] p. 95. This
theorem states that if set A is
smaller (has lower cardinality) than
B and vice-versa, then A and B are
equinumerous (have the
same cardinality). The interesting thing is that this can be proved
without invoking the Axiom of Choice, as we do here, but the proof as
you can see is quite difficult. (The theorem can be proved more easily
if we allow AC.) The main proof consists of lemmas sbthlem1 4436 through
sbthlem10 4445; this final piece mainly changes bound
variables to
eliminate the hypotheses of sbthlem10 4445. We follow closely the proof
in Suppes, which you should consult to understand our proof at a higher
level.
|
| ⊢
((A ≼ B ⋀ B
≼ A) → A ≈ B) |
| |
| Theorem | sbthbg 4447 |
Schroeder-Bernstein Theorem and its converse.
|
| ⊢
(B ∈ C → ((A
≼ B ⋀ B ≼ A)
↔ A ≈ B)) |
| |
| Theorem | sbthcl 4448 |
Schroeder-Bernstein Theorem in class form.
|
| ⊢
≈ = ( ≼ ∩ ◡ ≼
) |
| |
| Theorem | dfsdom2 4449 |
Alternate definition of strict dominance. Compare Definition 3 of
[Suppes] p. 97.
|
| ⊢
≺ = ( ≼ ∖ ◡ ≼
) |
| |
| Theorem | brsdom2 4450 |
Alternate definition of strict dominance. Definition 3 of [Suppes]
p. 97.
|
| ⊢
A ∈ V
& ⊢ B ∈ V
⇒ ⊢ (A ≺ B
↔ (A ≼ B ⋀ ¬ B ≼ A)) |
| |
| Theorem | sdomnsym 4451 |
Strict dominance is not symmetric. Theorem 21(ii) of [Suppes] p. 97.
|
| ⊢
(A ≺ B → ¬ B ≺ A) |
| |
| Theorem | domnsym 4452 |
Theorem 22(i) of [Suppes] p. 97.
|
| ⊢
(A ≼ B → ¬ B ≺ A) |
| |
| Theorem | 0dom 4453 |
Any set dominates the empty set.
|
| ⊢
∅ ≼ A |
| |
| Theorem | dom0 4454 |
A set dominated by the empty set is empty.
|
| ⊢
(A ≼ ∅ ↔ A = ∅) |
| |
| Theorem | 0sdomg 4455 |
A set strictly dominates the empty set iff it is not empty.
|
| ⊢
(A ∈ B → (∅ ≺ A ↔ A ≠
∅)) |
| |
| Theorem | 0sdom 4456 |
A set strictly dominates the empty set iff it is not empty.
|
| ⊢
A ∈ V
⇒ ⊢ (∅ ≺
A ↔ A ≠ ∅) |
| |
| Theorem | sdom0 4457 |
The empty set does not strictly dominate any set.
|
| ⊢
¬ A ≺ ∅ |
| |
| Theorem | sdomdomtr 4458 |
Transitivity of strict dominance and dominance. Theorem 22(iii) of
[Suppes] p. 97.
|
| ⊢
(C ∈ D → ((A
≺ B ⋀ B ≼ C)
→ A ≺ C)) |
| |
| Theorem | sdomentr 4459 |
Transitivity of strict dominance and equinumerosity. Exercise 11 of
[Suppes] p. 98.
|
| ⊢
(C ∈ D → ((A
≺ B ⋀ B ≈ C)
→ A ≺ C)) |
| |
| Theorem | ensdomtr 4460 |
Transitivity of equinumerosity and strict dominance.
|
| ⊢
((A ≈ B ⋀ B
≺ C) → A ≺ C) |
| |
| Theorem | sdomirr 4461 |
Strict dominance is irreflexive. Theorem 21(i) of [Suppes] p. 97.
|
| ⊢
¬ A ≺ A |
| |
| Theorem | sdomex 4462 |
Technical lemma for simplifying proofs involving strict dominance.
|
| ⊢
(A ≺ B → (A
∈ V ⋀ B ∈
V)) |
| |
| Theorem | sdomtr 4463 |
Strict dominance is transitive. Theorem 21(iii) of [Suppes] p. 97.
|
| ⊢
((A ≺ B ⋀ B
≺ C) → A ≺ C) |
| |
| Theorem | sdomn2lp 4464 |
Strict dominance has no 2-cycle loops.
|
| ⊢
¬ (A ≺ B ⋀ B
≺ A) |
| |
| Theorem | domsdomtr 4465 |
Transitivity of dominance and strict dominance. Theorem 22(ii) of
[Suppes] p. 97.
|
| ⊢
((A ≼ B ⋀ B
≺ C) → A ≺ C) |
| |
| Theorem | enen1 4466 |
Equality-like theorem for equinumerosity.
|
| ⊢
((B ∈ D ⋀ A
≈ B) → (A ≈ C
↔ B ≈ C)) |
| |
| Theorem | enen2 4467 |
Equality-like theorem for equinumerosity.
|
| ⊢
((B ∈ D ⋀ A
≈ B) → (C ≈ A
↔ C ≈ B)) |
| |
| Theorem | domen1 4468 |
Equality-like theorem for equinumerosity and dominance.
|
| ⊢
((B ∈ D ⋀ A
≈ B) → (A ≼ C
↔ B ≼ C)) |
| |
| Theorem | domen2 4469 |
Equality-like theorem for equinumerosity and dominance.
|
| ⊢
((B ∈ D ⋀ A
≈ B) → (C ≼ A
↔ C ≼ B)) |
| |
| Theorem | sdomen1 4470 |
Equality-like theorem for equinumerosity and strict dominance.
|
| ⊢
((B ∈ D ⋀ A
≈ B) → (A ≺ C
↔ B ≺ C)) |
| |
| Theorem | sdomen2 4471 |
Equality-like theorem for equinumerosity and strict dominance.
|
| ⊢
((B ∈ D ⋀ A
≈ B) → (C ≺ A
↔ C ≺ B)) |
| |
| Theorem | fodomr 4472 |
There exists a mapping from a set onto any (non-empty) set that it
dominates.
|
| ⊢
((A ∈ C ⋀ ∅ ≺ B ⋀ B
≼ A) → ∃f f:A–onto→B) |
| |
| Theorem | canth2 4473 |
Cantor's Theorem. No set is equinumerous to its power set.
Specifically, any set has a cardinality (size) strictly less than the
cardinality of its power set. For example, the cardinality of real
numbers is the same as the cardinality of the power set of integers,
so real numbers cannot be put into a one-to-one correspondence
with integers. Theorem 23 of [Suppes]
p. 97. For the function version,
see canth 3902.
|
| ⊢
A ∈ V
⇒ ⊢ A ≺ ℘A |
| |
| Theorem | canth2g 4474 |
Cantor's theorem with the sethood requirement expressed as an
antecedent. Theorem 23 of [Suppes] p.
97.
|
| ⊢
(A ∈ B → A
≺ ℘A) |
| |
| Theorem | pwuninel 4475 |
The power set of the union of a set does not belong to the set. This
theorem provides a way of constructing a new set that doesn't belong to
a given set.
|
| ⊢
¬ ℘∪A ∈ A |
| |
| Theorem | 2pwuninel 4476 |
The power set of the power set of the union of a set does not belong to
the set. This theorem provides a way of constructing a new set that
doesn't belong to a given set.
|
| ⊢
¬ ℘℘∪A ∈ A |
| |
| Theorem | xpen 4477 |
Equinumerosity law for cross product. Proposition 4.22(b) of
[Mendelson] p. 254.
|
| ⊢
A ∈ V
& ⊢ B ∈ V
& ⊢ C ∈ V
& ⊢ D ∈ V
⇒ ⊢ ((A ≈ B
⋀ C ≈ D) → (A
× C) ≈ (B × D)) |
| |
| Theorem | mapenlem1 4478 |
Lemma for mapen 4480.
|
| |
| Theorem | mapenlem2 4479 |
Lemma for mapen 4480.
|
| |
| Theorem | mapen 4480 |
Two set exponentiations are equinumerous when their bases and exponents
are equinumerous. Theorem 6H(c) of [Enderton] p. 139.
|
| ⊢
A ∈ V
& ⊢ B ∈ V
& ⊢ C ∈ V
& ⊢ D ∈ V
⇒ ⊢ ((A ≈ B
⋀ C ≈ D) → (A
↑m C) ≈
(B ↑m D)) |
| |
| Theorem | mapdom1 4481 |
Order-preserving property of set exponentiation. Theorem 6L(c) of
[Enderton] p. 149.
|
| ⊢
A ∈ V
& ⊢ B ∈ V
& ⊢ C ∈ V
⇒ ⊢ (A ≼ B
→ (A ↑m
C) ≼ (B ↑m C)) |
| |
| Theorem | mapdom2lem 4482 |
Lemma for mapdom2 4483.
|
| |
| Theorem | mapdom2 4483 |
Order-preserving property of set exponentiation. Theorem 6L(d) of
[Enderton] p. 149.
|
| ⊢
A ∈ V
& ⊢ B ∈ V
& ⊢ C ∈ V
⇒ ⊢ ((A ≼ B
⋀ ¬ (A = ∅ ⋀
C = ∅)) → (C ↑m A) ≼ (C
↑m B)) |
| |
| Theorem | mapxpen 4484 |
Equinumerosity law for double set exponentiation. Proposition 10.45 of
[TakeutiZaring] p. 96.
|
| ⊢
A ∈ V
& ⊢ B ∈ V
& ⊢ C ∈ V
⇒ ⊢ ((A ↑m B) ↑m C) ≈ (A
↑m (B ×
C)) |
| |
| Theorem | xpmapenlem1 4485 |
Lemma for xpmapen 4490.
|
| |
| Theorem | xpmapenlem2 4486 |
Lemma for xpmapen 4490.
|
| |
| Theorem | xpmapenlem3 4487 |
Lemma for xpmapen 4490.
|
| |
| Theorem | xpmapenlem4 4488 |
Lemma for xpmapen 4490.
|
| |
| Theorem | xpmapenlem5 4489 |
Lemma for xpmapen 4490.
|
| |
| Theorem | xpmapen 4490 |
Equinumerosity law for set exponentiation of a cross product.
Exercise 4.47 of [Mendelson] p. 255.
|
| ⊢
A ∈ V
& ⊢ B ∈ V
& ⊢ C ∈ V
⇒ ⊢ ((A × B)
↑m C) ≈
((A ↑m C) × (B
↑m C)) |
| |
| Theorem | mapunen 4491 |
Equinumerosity law for set exponentiation of a disjoint union.
Exercise 4.45 of [Mendelson] p. 255.
|
| ⊢
A ∈ V
& ⊢ B ∈ V
& ⊢ C ∈ V
⇒ ⊢ ((A ∩ B) =
∅ → (C
↑m (A ∪
B)) ≈ ((C ↑m A) × (C
↑m B))) |
| |
| Theorem | pwen 4492 |
If two sets are equinumerous, then their power sets are equinumerous.
Proposition 10.15 of [TakeutiZaring] p. 87.
|
| ⊢
B ∈ V
⇒ ⊢ (A ≈ B
→ ℘A ≈ ℘B) |
| |
| Theorem | ssenen 4493 |
Equinumerosity of equinumerous subsets of a set.
|
| ⊢
A ∈ V
& ⊢ B ∈ V
⇒ ⊢ (A ≈ B
→ {x∣(x ⊆ A
⋀ x ≈ C)} ≈ {x∣(x
⊆ B ⋀ x ≈ C)}) |
| |
| Theorem | limenpsi 4494 |
A limit ordinal is equinumerous to a proper subset of itself.
|
| ⊢
Lim A
⇒ ⊢ (A ∈ B
→ A ≈ (A ∖ {∅})) |
| |
| Theorem | limensuci 4495 |
A limit ordinal is equinumerous to its successor.
|
| ⊢
Lim A
⇒ ⊢ (A ∈ B
→ A ≈ suc A) |
| |
| Theorem | limensuc 4496 |
A limit ordinal is equinumerous to its successor.
|
| ⊢
((A ∈ B ⋀ Lim A) → A
≈ suc A) |
| |
| Pigeonhole Principle |
| |
| Theorem | phplem1 4497 |
Lemma for Pigeonhole Principle. If we join a natural number to itself
minus an element, we end up with its successor minus the same element.
|
| |
| Theorem | phplem2 4498 |
Lemma for Pigeonhole Principle. A natural number is equinumerous to its
successor minus one of its elements.
|
| |
| Theorem | phplem3 4499 |
Lemma for Pigeonhole Principle. A natural number is equinumerous
to its successor minus any element of the successor.
|
| |
| Theorem | phplem4 4500 |
Lemma for Pigeonhole Principle. Equinumerosity of successors implies
equinumerosity of the original natural numbers.
|
Home
Hilbert Space Explorer
(8744-10691)