Statement List for Metamath Proof Explorer - 3301-3400 - Page 34 of 58
| Type | Label | Description |
|---|
| Statement |
|---|
| |
| Theorem | f1oen 3301 |
The domain and range of a one-to-one, onto function are equinumerous.
|
| ⊢
A ∈ V
⇒ ⊢ (F:A–1-1-onto→B →
A ≈ B) |
| |
| Theorem | f1dom 3302 |
The domain of a one-to-one function is dominated by its range.
|
| ⊢
A ∈ V
⇒ ⊢ (F:A–1-1→B
→ A ≼ B) |
| |
| Theorem | en2d 3303 |
Equinumerosity inference from an implicit one-to-one onto function.
|
| ⊢
(φ → A ∈ V)
& ⊢ (φ → (x ∈ A
→ C ∈
V)) & ⊢ (φ
→ (y ∈ B → D
∈ V)) & ⊢ (φ
→ ((x ∈ A ∧ y =
C) ↔ (y ∈ B
∧ x = D)))
⇒ ⊢ (φ → A ≈ B) |
| |
| Theorem | en3d 3304 |
Equinumerosity inference from an implicit one-to-one onto function.
|
| ⊢
(φ → A ∈ V)
& ⊢ (φ → (x ∈ A
→ C ∈ B)) & ⊢ (φ
→ (y ∈ B → D
∈ A))
& ⊢ (φ → ((x ∈ A
∧ y ∈ B) → (x =
D ↔ y = C)))
⇒ ⊢ (φ → A ≈ B) |
| |
| Theorem | en2 3305 |
Equinumerosity inference from an implicit one-to-one onto function.
|
| ⊢
A ∈ V
& ⊢ (x ∈ A
→ C ∈
V) & ⊢ (y ∈
B → D ∈ V)
& ⊢ ((x ∈ A
∧ y = C) ↔ (y
∈ B ∧ x = D))
⇒ ⊢ A ≈ B |
| |
| Theorem | en3 3306 |
Equinumerosity inference from an implicit one-to-one onto function.
|
| ⊢
A ∈ V
& ⊢ (x ∈ A
→ C ∈ B) & ⊢ (y ∈
B → D ∈ A) & ⊢ ((x ∈
A ∧ y ∈ B)
→ (x = D ↔ y =
C))
⇒ ⊢ A ≈ B |
| |
| Theorem | dom2d 3307 |
A mapping (first hypothesis) that is one-to-one (second hypothesis)
implies its domain is dominated by its range.
|
| ⊢
(φ → (x ∈ A
→ C ∈ B)) & ⊢ (φ
→ ((x ∈ A ∧ y
∈ A) → (C = D ↔
x = y)))
⇒ ⊢ (φ → (A ∈ R
→ A ≼ B)) |
| |
| Theorem | dom2 3308 |
A mapping (first hypothesis) that is one-to-one (second hypothesis)
implies its domain is dominated by its range.
|
| ⊢
(x ∈ A → C
∈ B)
& ⊢ ((x ∈ A
∧ y ∈ A) → (C =
D ↔ x = y))
⇒ ⊢ (A ∈ R
→ A ≼ B) |
| |
| Theorem | idssen 3309 |
Equality implies equinumerosity.
|
| ⊢
I ⊆ ≈ |
| |
| Theorem | dmen 3310 |
The domain of equinumerosity.
|
| ⊢
dom ≈ = V |
| |
| Theorem | ssdomg 3311 |
A set dominates its subsets. Theorem 16 of [Suppes] p. 94.
|
| ⊢
(A ∈ C → (A
⊆ B → A ≼ B)) |
| |
| Theorem | ssdom2g 3312 |
A set dominates its subsets. Theorem 16 of [Suppes] p. 94.
|
| ⊢
(B ∈ C → (A
⊆ B → A ≼ B)) |
| |
| Theorem | ener 3313 |
Equinumerosity is an equivalence relation.
|
| ⊢
Er ≈ |
| |
| Theorem | sdomirr 3314 |
Strict dominance is irreflexive. Theorem 21(i) of [Suppes] p. 97.
|
| ⊢
¬ A ≺ A |
| |
| Theorem | sdomex 3315 |
Technical lemma for simplifying proofs involving strict dominance.
|
| ⊢
(A ≺ B → (A
∈ V ∧ B ∈
V)) |
| |
| Theorem | ensymg 3316 |
Symmetry of equinumerosity. Theorem 2 of [Suppes] p. 92.
|
| ⊢
(B ∈ C → (A
≈ B → B ≈ A)) |
| |
| Theorem | ensym 3317 |
Symmetry of equinumerosity. Theorem 2 of [Suppes] p. 92.
|
| ⊢
B ∈ V
⇒ ⊢ (A ≈ B
→ B ≈ A) |
| |
| Theorem | ensymi 3318 |
Symmetry of equinumerosity. Theorem 2 of [Suppes] p. 92.
|
| ⊢
B ∈ V
& ⊢ A ≈ B ⇒ ⊢ B ≈
A |
| |
| Theorem | entrt 3319 |
Transitivity of equinumerosity. Theorem 3 of [Suppes] p. 92.
|
| ⊢
((A ≈ B ∧ B
≈ C) → A ≈ C) |
| |
| Theorem | domtr 3320 |
Transitivity of dominance relation. Theorem 17 of [Suppes] p. 94.
|
| ⊢
((A ≼ B ∧ B
≼ C) → A ≼ C) |
| |
| Theorem | entr 3321 |
A chained equinumerosity inference.
|
| ⊢
A ≈ B & ⊢ B ≈
C
⇒ ⊢ A ≈ C |
| |
| Theorem | entr2 3322 |
A chained equinumerosity inference.
|
| ⊢
C ∈ V
& ⊢ A ≈ B & ⊢ B ≈
C
⇒ ⊢ C ≈ A |
| |
| Theorem | entr3 3323 |
A chained equinumerosity inference.
|
| ⊢
B ∈ V
& ⊢ A ≈ B & ⊢ A ≈
C
⇒ ⊢ B ≈ C |
| |
| Theorem | entr4 3324 |
A chained equinumerosity inference.
|
| ⊢
B ∈ V
& ⊢ A ≈ B & ⊢ C ≈
B
⇒ ⊢ A ≈ C |
| |
| Theorem | endomtr 3325 |
Transitivity of equinumerosity and dominance.
|
| ⊢
((A ≈ B ∧ B
≼ C) → A ≼ C) |
| |
| Theorem | domentr 3326 |
Transitivity of dominance and equinumerosity.
|
| ⊢
((A ≼ B ∧ B
≈ C) → A ≼ C) |
| |
| Theorem | f1imaen 3327 |
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 3328 |
The empty set is equinumerous only to itself. Exercise 1 of
[TakeutiZaring] p. 88.
|
| ⊢
(A ≈ ∅ ↔ A = ∅) |
| |
| Theorem | ensn1 3329 |
A singleton is equinumerous to ordinal one.
|
| ⊢
A ∈ V
⇒ ⊢ {A} ≈ 1o |
| |
| Theorem | ensn1g 3330 |
A singleton is equinumerous to ordinal one.
|
| ⊢
(A ∈ B → {A}
≈ 1o) |
| |
| Theorem | en1 3331 |
A set is equinumerous to ordinal one iff it is a singleton.
|
| ⊢
(A ≈ 1o
↔ ∃x A = {x}) |
| |
| Theorem | 2dom 3332 |
A set that dominates ordinal 2 has at least 2 different members.
|
| ⊢
A ∈ V
⇒ ⊢
(2o ≼ A
→ ∃x ∈ A ∃y
∈ A ¬ x = y) |
| |
| Theorem | fundmen 3333 |
A function is equinumerous to its domain. Exercise 4 of [Suppes]
p. 98.
|
| ⊢
F ∈ V
⇒ ⊢ (Fun F → dom F
≈ F) |
| |
| Theorem | mapsnen 3334 |
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 3335 |
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 3336 |
Two singletons are equinumerous.
|
| ⊢
((A ∈ C ∧ B
∈ D) → {A} ≈ {B}) |
| |
| Theorem | snfi 3337 |
A singleton is finite.
|
| ⊢
∃x ∈ ω {A} ≈ x |
| |
| Theorem | unen 3338 |
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 3339 |
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 3340 |
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 3341 |
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 3342 |
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 3343 |
Commutative law for equinumerosity of cross product. Proposition
4.22(d) of [Mendelson] p. 254.
|
| ⊢
A ∈ V
& ⊢ B ∈ V
⇒ ⊢ (A × B)
≈ (B × A) |
| |
| Theorem | xpassen 3344 |
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 3345 |
Dominance law for cross product. Proposition 10.33(2) of
[TakeutiZaring] p. 92.
|
| ⊢
A ∈ V
& ⊢ B ∈ V
& ⊢ C ∈ V
⇒ ⊢ (A ≼ B
→ (C × A) ≼ (C
× B)) |
| |
| Theorem | xpdom1 3346 |
Dominance law for cross product. Theorem 6L(c) of [Enderton] p. 149.
|
| ⊢
A ∈ V
& ⊢ B ∈ V
& ⊢ C ∈ V
⇒ ⊢ (A ≼ B
→ (A × C) ≼ (B
× C)) |
| |
| Theorem | xpdom3 3347 |
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 3348 |
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) |
| |
| Theorem | sbthlem1 3349 |
Lemma for Schroeder-Bernstein Theorem.
|
| ⊢
A ∈ V
& ⊢ D = {x∣(x
⊆ A ∧ (g “ (B
∖ (f “ x))) ⊆ (A
∖ x))}
⇒ ⊢ ∪D ⊆ (A ∖ (g
“ (B ∖ (f “ ∪D)))) |
| |
| Theorem | sbthlem2 3350 |
Lemma for Schroeder-Bernstein Theorem.
|
| ⊢
A ∈ V
& ⊢ D = {x∣(x
⊆ A ∧ (g “ (B
∖ (f “ x))) ⊆ (A
∖ x))}
⇒ ⊢ (ran g ⊆ A
→ (A ∖ (g “ (B
∖ (f “ ∪D)))) ⊆ ∪D) |
| |
| Theorem | sbthlem3 3351 |
Lemma for Schroeder-Bernstein Theorem.
|
| ⊢
A ∈ V
& ⊢ D = {x∣(x
⊆ A ∧ (g “ (B
∖ (f “ x))) ⊆ (A
∖ x))}
⇒ ⊢ (ran g ⊆ A
→ (g “ (B ∖ (f
“ ∪D))) =
(A ∖ ∪D)) |
| |
| Theorem | sbthlem4 3352 |
Lemma for Schroeder-Bernstein Theorem.
|
| ⊢
A ∈ V
& ⊢ D = {x∣(x
⊆ A ∧ (g “ (B
∖ (f “ x))) ⊆ (A
∖ x))}
⇒ ⊢ (((dom g = B ∧ ran
g ⊆ A) ∧ Fun ◡g)
→ (◡g “ (A
∖ ∪D)) =
(B ∖ (f “ ∪D))) |
| |
| Theorem | sbthlem5 3353 |
Lemma for Schroeder-Bernstein Theorem.
|
| ⊢
A ∈ V
& ⊢ D = {x∣(x
⊆ A ∧ (g “ (B
∖ (f “ x))) ⊆ (A
∖ x))}
& ⊢ H = ((f ↾
∪D) ∪
(◡g ↾ (A
∖ ∪D)))
⇒ ⊢ ((dom f = A ∧ ran
g ⊆ A) → dom H
= A) |
| |
| Theorem | sbthlem6 3354 |
Lemma for Schroeder-Bernstein Theorem.
|
| ⊢
A ∈ V
& ⊢ D = {x∣(x
⊆ A ∧ (g “ (B
∖ (f “ x))) ⊆ (A
∖ x))}
& ⊢ H = ((f ↾
∪D) ∪
(◡g ↾ (A
∖ ∪D)))
⇒ ⊢ ((ran f ⊆ B
∧ ((dom g = B ∧ ran g
⊆ A) ∧ Fun ◡g))
→ ran H = B) |
| |
| Theorem | sbthlem7 3355 |
Lemma for Schroeder-Bernstein Theorem.
|
| ⊢
A ∈ V
& ⊢ D = {x∣(x
⊆ A ∧ (g “ (B
∖ (f “ x))) ⊆ (A
∖ x))}
& ⊢ H = ((f ↾
∪D) ∪
(◡g ↾ (A
∖ ∪D)))
⇒ ⊢ ((Fun f ∧ Fun ◡g)
→ Fun H) |
| |
| Theorem | sbthlem8 3356 |
Lemma for Schroeder-Bernstein Theorem.
|
| ⊢
A ∈ V
& ⊢ D = {x∣(x
⊆ A ∧ (g “ (B
∖ (f “ x))) ⊆ (A
∖ x))}
& ⊢ H = ((f ↾
∪D) ∪
(◡g ↾ (A
∖ ∪D)))
⇒ ⊢ ((Fun ◡f ∧
(((Fun g ∧ dom g = B) ∧
ran g ⊆ A) ∧ Fun ◡g))
→ Fun ◡H) |
| |
| Theorem | sbthlem9 3357 |
Lemma for Schroeder-Bernstein Theorem.
|
| ⊢
A ∈ V
& ⊢ D = {x∣(x
⊆ A ∧ (g “ (B
∖ (f “ x))) ⊆ (A
∖ x))}
& ⊢ H = ((f ↾
∪D) ∪
(◡g ↾ (A
∖ ∪D)))
⇒ ⊢ ((f:A–1-1→B
∧ g:B–1-1→A) →
H:A–1-1-onto→B) |
| |
| Theorem | sbthlem10 3358 |
Lemma for Schroeder-Bernstein Theorem.
|
| ⊢
A ∈ V
& ⊢ D = {x∣(x
⊆ A ∧ (g “ (B
∖ (f “ x))) ⊆ (A
∖ x))}
& ⊢ H = ((f ↾
∪D) ∪
(◡g ↾ (A
∖ ∪D))) & ⊢ B ∈
V ⇒ ⊢ ((A ≼
B ∧ B ≼ A)
→ A ≈ B) |
| |
| Theorem | sbth 3359 |
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 3349 through
sbthlem10 3358; this final piece mainly changes bound
variables to
eliminate the hypotheses of sbthlem10 3358. We closely follow the proof in
Suppes, which you should consult to understand our proof at a higher
level.
|
| ⊢
((A ≼ B ∧ B
≼ A) → A ≈ B) |
| |
| Theorem | sbthbg 3360 |
Schroeder-Bernstein Theorem and its converse.
|
| ⊢
(B ∈ C → ((A
≼ B ∧ B ≼ A)
↔ A ≈ B)) |
| |
| Theorem | sbthcl 3361 |
Schroeder-Bernstein Theorem in class form.
|
| ⊢
≈ = ( ≼ ∩ ◡ ≼
) |
| |
| Theorem | dfsdom2 3362 |
Alternate definition of strict dominance. Compare Definition 3 of
[Suppes] p. 97.
|
| ⊢
≺ = ( ≼ ∖ ◡ ≼
) |
| |
| Theorem | brsdom2 3363 |
Alternate definition of strict dominance. Definition 3 of [Suppes]
p. 97.
|
| ⊢
A ∈ V
& ⊢ B ∈ V
⇒ ⊢ (A ≺ B
↔ (A ≼ B ∧ ¬ B
≼ A)) |
| |
| Theorem | sdomnsym 3364 |
Strict dominance is not symmetric. Theorem 21(ii) of [Suppes] p. 97.
|
| ⊢
(A ≺ B → ¬ B ≺ A) |
| |
| Theorem | domnsym 3365 |
Theorem 22(i) of [Suppes] p. 97.
|
| ⊢
(A ≼ B → ¬ B ≺ A) |
| |
| Theorem | 0dom 3366 |
Any set dominates the empty set.
|
| ⊢
∅ ≼ A |
| |
| Theorem | dom0 3367 |
A set dominated by the empty set is empty.
|
| ⊢
(A ≼ ∅ ↔ A = ∅) |
| |
| Theorem | 0sdom 3368 |
A set strictly dominates the empty set iff it is not empty.
|
| ⊢
A ∈ V
⇒ ⊢ (∅ ≺
A ↔ ¬ A = ∅) |
| |
| Theorem | sdom0 3369 |
The empty set does not strictly dominate any set.
|
| ⊢
¬ A ≺ ∅ |
| |
| Theorem | sdomdomtr 3370 |
Transitivity of strict dominance and dominance. Theorem 22(iii) of
[Suppes] p. 97.
|
| ⊢
(C ∈ D → ((A
≺ B ∧ B ≼ C)
→ A ≺ C)) |
| |
| Theorem | sdomentr 3371 |
Transitivity of strict dominance and equinumerosity. Exercise 11 of
[Suppes] p. 98.
|
| ⊢
(C ∈ D → ((A
≺ B ∧ B ≈ C)
→ A ≺ C)) |
| |
| Theorem | ensdomtr 3372 |
Transitivity of equinumerosity and strict dominance.
|
| ⊢
((A ≈ B ∧ B
≺ C) → A ≺ C) |
| |
| Theorem | sdomtr 3373 |
Strict dominance is transitive. Theorem 21(iii) of [Suppes] p. 97.
|
| ⊢
((A ≺ B ∧ B
≺ C) → A ≺ C) |
| |
| Theorem | domsdomtr 3374 |
Transitivity of dominance and strict dominance. Theorem 22(ii) of
[Suppes] p. 97.
|
| ⊢
((A ≼ B ∧ B
≺ C) → A ≺ C) |
| |
| Theorem | enen1 3375 |
Equality-like theorem for equinumerosity.
|
| ⊢
((B ∈ D ∧ A
≈ B) → (A ≈ C
↔ B ≈ C)) |
| |
| Theorem | enen2 3376 |
Equality-like theorem for equinumerosity.
|
| ⊢
((B ∈ D ∧ A
≈ B) → (C ≈ A
↔ C ≈ B)) |
| |
| Theorem | domen1 3377 |
Equality-like theorem for equinumerosity and dominance.
|
| ⊢
((B ∈ D ∧ A
≈ B) → (A ≼ C
↔ B ≼ C)) |
| |
| Theorem | domen2 3378 |
Equality-like theorem for equinumerosity and dominance.
|
| ⊢
((B ∈ D ∧ A
≈ B) → (C ≼ A
↔ C ≼ B)) |
| |
| Theorem | sdomen1 3379 |
Equality-like theorem for equinumerosity and strict dominance.
|
| ⊢
((B ∈ D ∧ A
≈ B) → (A ≺ C
↔ B ≺ C)) |
| |
| Theorem | sdomen2 3380 |
Equality-like theorem for equinumerosity and strict dominance.
|
| ⊢
((B ∈ D ∧ A
≈ B) → (C ≺ A
↔ C ≺ B)) |
| |
| Theorem | canth2 3381 |
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 2945.
|
| ⊢
A ∈ V
⇒ ⊢ A ≺ ℘A |
| |
| Theorem | canth2g 3382 |
Cantor's theorem with the sethood requirement expressed as an
antecedent. Theorem 23 of [Suppes] p.
97.
|
| ⊢
(A ∈ B → A
≺ ℘A) |
| |
| Theorem | xpen 3383 |
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 3384 |
Lemma for mapen 3386.
|
| ⊢
A ∈ V
& ⊢ B ∈ V
& ⊢ C ∈ V
& ⊢ D ∈ V
& ⊢ H = {⟨x,
y⟩∣(x ∈ (A
↑m C) ∧
y = ((f ∘ x)
∘ ◡g))}
⇒ ⊢ ((((f:A–1-1-onto→B ∧
g:C–1-1-onto→D) ∧
z:C–→A) ∧ v
∈ C) → ((H ‘z)
‘(g ‘v)) = (f
‘(z ‘v))) |
| |
| Theorem | mapenlem2 3385 |
Lemma for mapen 3386.
|
| ⊢
A ∈ V
& ⊢ B ∈ V
& ⊢ C ∈ V
& ⊢ D ∈ V
& ⊢ H = {⟨x,
y⟩∣(x ∈ (A
↑m C) ∧
y = ((f ∘ x)
∘ ◡g))}
⇒ ⊢ ((f:A–1-1-onto→B ∧
g:C–1-1-onto→D) →
H:(A
↑m C)–1-1-onto→(B
↑m D)) |
| |
| Theorem | mapen 3386 |
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 3387 |
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 3388 |
Lemma for mapdom2 3389.
|
| ⊢
A ∈ V
& ⊢ B ∈ V
& ⊢ C ∈ V
⇒ ⊢ (x ∈ (C
↑m z) →
(x ∩ ((B ∖ z)
× {w})) = ∅) |
| |
| Theorem | mapdom2 3389 |
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 3390 |
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 3391 |
Lemma for xpmapen 3396.
|
| ⊢
A ∈ V
& ⊢ B ∈ V
& ⊢ C ∈ V
& ⊢ D = {⟨z,
w⟩∣(z ∈ C
∧ w = ∪dom
{(x ‘z)})}
& ⊢ R = {⟨z,
w⟩∣(z ∈ C
∧ w = ∪ran
{(x ‘z)})}
& ⊢ S = {⟨z,
w⟩∣(z ∈ C
∧ w = ⟨(∪dom {y}
‘z), (∪ran {y}
‘z)⟩)}
⇒ ⊢ ((y = ⟨D,
R⟩ → ∀z y =
⟨D, R⟩) ∧ (y = ⟨D,
R⟩ → ∀w y =
⟨D, R⟩)) |
| |
| Theorem | xpmapenlem2 3392 |
Lemma for xpmapen 3396.
|
| ⊢
A ∈ V
& ⊢ B ∈ V
& ⊢ C ∈ V
& ⊢ D = {⟨z,
w⟩∣(z ∈ C
∧ w = ∪dom
{(x ‘z)})}
& ⊢ R = {⟨z,
w⟩∣(z ∈ C
∧ w = ∪ran
{(x ‘z)})}
& ⊢ S = {⟨z,
w⟩∣(z ∈ C
∧ w = ⟨(∪dom {y}
‘z), (∪ran {y}
‘z)⟩)}
⇒ ⊢ ((y = ⟨D,
R⟩ ∧ z ∈ C)
→ ((∪dom {y} ‘z) =
∪dom {(x
‘z)} ∧ (∪ran {y}
‘z) = ∪ran {(x
‘z)})) |
| |
| Theorem | xpmapenlem3 3393 |
Lemma for xpmapen 3396.
|
| ⊢
A ∈ V
& ⊢ B ∈ V
& ⊢ C ∈ V
& ⊢ D = {⟨z,
w⟩∣(z ∈ C
∧ w = ∪dom
{(x ‘z)})}
& ⊢ R = {⟨z,
w⟩∣(z ∈ C
∧ w = ∪ran
{(x ‘z)})}
& ⊢ S = {⟨z,
w⟩∣(z ∈ C
∧ w = ⟨(∪dom {y}
‘z), (∪ran {y}
‘z)⟩)}
⇒ ⊢ ((x:C–→(A × B)
∧ y = ⟨D, R⟩)
→ x = S) |
| |
| Theorem | xpmapenlem4 3394 |
Lemma for xpmapen 3396.
|
| ⊢
A ∈ V
& ⊢ B ∈ V
& ⊢ C ∈ V
& ⊢ D = {⟨z,
w⟩∣(z ∈ C
∧ w = ∪dom
{(x ‘z)})}
& ⊢ R = {⟨z,
w⟩∣(z ∈ C
∧ w = ∪ran
{(x ‘z)})}
& ⊢ S = {⟨z,
w⟩∣(z ∈ C
∧ w = ⟨(∪dom {y}
‘z), (∪ran {y}
‘z)⟩)}
⇒ ⊢ (((y = ⟨∪dom {y}, ∪ran {y}⟩ ∧ (∪dom
{y}:C–→A
∧ ∪ran {y}:C–→B)) ∧ x =
S) → (x:C–→(A × B)
∧ y = ⟨D, R⟩)) |
| |
| Theorem | xpmapenlem5 3395 |
Lemma for xpmapen 3396.
|
| ⊢
A ∈ V
& ⊢ B ∈ V
& ⊢ C ∈ V
& ⊢ D = {⟨z,
w⟩∣(z ∈ C
∧ w = ∪dom
{(x ‘z)})}
& ⊢ R = {⟨z,
w⟩∣(z ∈ C
∧ w = ∪ran
{(x ‘z)})}
& ⊢ S = {⟨z,
w⟩∣(z ∈ C
∧ w = ⟨(∪dom {y}
‘z), (∪ran {y}
‘z)⟩)}
⇒ ⊢ ((A × B)
↑m C) ≈
((A ↑m C) × (B
↑m C)) |
| |
| Theorem | xpmapen 3396 |
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 3397 |
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 3398 |
If two sets are equinumerous, then their power sets are equinumerous.
Proposition 10.15 of [TakeutiZaring] p. 87.
|
| ⊢
A ∈ V
& ⊢ B ∈ V
⇒ ⊢ (A ≈ B
→ ℘A ≈ ℘B) |
| |
| Theorem | ssenen 3399 |
Equinumerosity of equinumerous subsets of a set.
|
| ⊢
A ∈ V
& ⊢ B ∈ V
& ⊢ C ∈ V
⇒ ⊢ (A ≈ B
→ {x∣(x ⊆ A
∧ x ≈ C)} ≈ {x∣(x
⊆ B ∧ x ≈ C)}) |
| |
| Theorem | limenpsi 3400 |
A limit ordinal is equinumerous to a proper subset of itself.
|
| ⊢
Lim A
⇒ ⊢ (A ∈ B
→ A ≈ (A ∖ {∅})) |
Home
Hilbert Space Explorer
(4958-5787)