Statement List for Metamath Proof Explorer - 2401-2500 - Page 25 of 58
| Type | Label | Description |
|---|
| Statement |
|---|
| |
| Theorem | tfinds 2401 |
Principle of Transfinite Induction (inference schema) with implicit
substitutions. The first four hypotheses establish the
substitutions we need. The last three are the basis, the induction
hypothesis for successors, and the induction hypothesis for limit
ordinals. Theorem Schema 4 of [Suppes]
p. 197.
|
| ⊢
(x = ∅ → (φ ↔ ψ))
& ⊢ (x = y →
(φ ↔ χ))
& ⊢ (x = suc y
→ (φ ↔ θ))
& ⊢ (x = A →
(φ ↔ τ))
& ⊢ ψ
& ⊢ (y ∈ On → (χ → θ))
& ⊢ (Lim x → (∀y ∈ x
χ → φ))
⇒ ⊢ (A ∈ On → τ) |
| |
| Theorem | tfindsg 2402 |
Transfinite Induction (inference schema) with implicit substitutions.
The first four hypotheses establish the substitutions we need. The last
three are the basis, the induction hypothesis for successors, and the
induction hypothesis for limit ordinals. The basis of this version is
an arbitrary ordinal B instead of
zero. Remark of
[TakeutiZaring] p. 57.
|
| ⊢
(x = B → (φ
↔ ψ))
& ⊢ (x = y →
(φ ↔ χ))
& ⊢ (x = suc y
→ (φ ↔ θ))
& ⊢ (x = A →
(φ ↔ τ))
& ⊢ (B ∈ On → ψ)
& ⊢ (((y ∈ On ∧ B ∈ On) ∧ B ⊆ y)
→ (χ → θ))
& ⊢ (((Lim x ∧ B
∈ On) ∧ B ⊆ x) → (∀y ∈ x
(B ⊆ y → χ)
→ φ))
⇒ ⊢ (((A ∈ On ∧ B ∈ On) ∧ B ⊆ A)
→ τ) |
| |
| Theorem | tfindsg2 2403 |
Transfinite Induction (inference schema) with implicit substitutions.
The first four hypotheses establish the substitutions we need. The last
three are the basis, the induction hypothesis for successors, and the
induction hypothesis for limit ordinals. The basis of this version is
an arbitrary ordinal suc B instead
of zero.
|
| ⊢
(x = suc B → (φ
↔ ψ))
& ⊢ (x = y →
(φ ↔ χ))
& ⊢ (x = suc y
→ (φ ↔ θ))
& ⊢ (x = A →
(φ ↔ τ))
& ⊢ (B ∈ On → ψ)
& ⊢ ((y ∈ On ∧ B ∈ y)
→ (χ → θ))
& ⊢ ((Lim x ∧ B
∈ x) → (∀y ∈ x
(B ∈ y → χ)
→ φ))
⇒ ⊢ ((A ∈ On ∧ B ∈ A)
→ τ) |
| |
| Theorem | tfindes 2404 |
Transfinite Induction with explicit substitution. The first hypothesis
is the basis, the second is the induction hypothesis for successors, and
the third is the induction hypothesis for limit ordinals. Theorem
Schema 4 of [Suppes] p. 197.
|
| ⊢
[∅ / x]φ
& ⊢ (x ∈ On → (φ → [suc x / x]φ))
& ⊢ (Lim y → (∀x ∈ y
φ → [y / x]φ))
⇒ ⊢ (x ∈ On → φ) |
| |
| Theorem | tfinds2 2405 |
Transfinite Induction (inference schema) with implicit substitutions.
The first three hypotheses establish the substitutions we need. The
last three are the basis and the induction hypotheses (for successor and
limit ordinals respectively). Theorem Schema 4 of [Suppes] p. 197. The
wff τ is an auxiliary antecedent
to help shorten proofs using this
theorem.
|
| ⊢
(x = ∅ → (φ ↔ ψ))
& ⊢ (x = y →
(φ ↔ χ))
& ⊢ (x = suc y
→ (φ ↔ θ))
& ⊢ (τ → ψ)
& ⊢ (y ∈ On → (τ → (χ → θ)))
& ⊢ (Lim x → (τ
→ (∀y ∈ x χ →
φ)))
⇒ ⊢ (x ∈ On → (τ → φ)) |
| |
| Theorem | tfinds3 2406 |
Principle of Transfinite Induction (inference schema) with implicit
substitutions. The first four hypotheses establish the
substitutions we need. The last three are the basis, the induction
hypothesis for successors, and the induction hypothesis for limit
ordinals.
|
| ⊢
(x = ∅ → (φ ↔ ψ))
& ⊢ (x = y →
(φ ↔ χ))
& ⊢ (x = suc y
→ (φ ↔ θ))
& ⊢ (x = A →
(φ ↔ τ))
& ⊢ (η → ψ)
& ⊢ (y ∈ On → (η → (χ → θ)))
& ⊢ (Lim x → (η
→ (∀y ∈ x χ →
φ)))
⇒ ⊢ (A ∈ On → (η → τ)) |
| |
| Theorem | ssnlim 2407 |
An ordinal subclass of non-limit ordinals is a class of natural numbers.
Exercise 7 of [TakeutiZaring] p.
42.
|
| ⊢
((Ord A ∧ A ⊆ {x
∈ On∣ ¬ Lim x}) →
A ⊆ ω) |
| |
| Syntax | cxp 2408 |
Extend the definition of a class to include the cross product.
|
| class
(A × B) |
| |
| Syntax | ccnv 2409 |
Extend the definition of a class to include the converse of a class.
|
| class
◡A |
| |
| Syntax | cdm 2410 |
Extend the definition of a class to include the domain of a class.
|
| class dom
A |
| |
| Syntax | crn 2411 |
Extend the definition of a class to include the range of a class.
|
| class ran
A |
| |
| Syntax | cres 2412 |
Extend the definition of a class to include the restriction of a class.
(Read: The restriction of A to
B.)
|
| class
(A ↾ B) |
| |
| Syntax | cima 2413 |
Extend the definition of a class to include the image of a class.
(Read: The image of B under A.)
|
| class
(A “ B) |
| |
| Syntax | ccom 2414 |
Extend the definition of a class to include the composition of two
classes. (Read: The composition of A
and B.)
|
| class
(A ∘ B) |
| |
| Syntax | wrel 2415 |
Extend the definition of a wff to include the relation predicate. (Read:
A is a relation.)
|
| wff Rel
A |
| |
| Syntax | wfun 2416 |
Extend the definition of a wff to include the function predicate. (Read:
A is a function.)
|
| wff Fun
A |
| |
| Syntax | wfn 2417 |
Extend the definition of a wff to include the function predicate with
a domain. (Read: A is a function on
B.)
|
| wff
A Fn B |
| |
| Syntax | wf 2418 |
Extend the definition of a wff to include the function predicate with
domain and range. (Read: F maps
A into B.)
|
| wff
F:A–→B |
| |
| Syntax | wf1 2419 |
Extend the definition of a wff to include one-to-one functions. (Read:
F maps A one-to-one into B.)
|
| wff
F:A–1-1→B |
| |
| Syntax | wfo 2420 |
Extend the definition of a wff to include onto functions. (Read: F
maps A onto B.)
|
| wff
F:A–onto→B |
| |
| Syntax | wf1o 2421 |
Extend the definition of a wff to include one-to-one onto functions.
(Read: F maps A one-to-one onto B.)
|
| wff
F:A–1-1-onto→B |
| |
| Syntax | cfv 2422 |
Extend the definition of a class to include the value of a function.
(Read: The value of F at A, or "F of
A".)
|
| class
(F ‘A) |
| |
| Syntax | wiso 2423 |
Extend the definition of a wff to include the isomorphism property.
(Read: H is an R, S isomorphism
of A onto B.)
|
| wff
H Isom R, S (A, B) |
| |
| Definition | df-xp 2424 |
Define the cross product of two classes. Definition 9.11 of [Quine]
p. 64.
|
| ⊢
(A × B) = {⟨x,
y⟩∣(x ∈ A
∧ y ∈ B)} |
| |
| Definition | df-rel 2425 |
Define a relation. Definition 6.4(1) of [TakeutiZaring] p. 23.
For an alternate definition, see dfrel2 2660.
|
| ⊢
(Rel A ↔ A ⊆ (V × V)) |
| |
| Definition | df-cnv 2426 |
Define the converse of a class. Definition 9.12 of [Quine] p. 64.
We use Quine's breve accent (smile) notation; as a prefix, it
eliminates parentheses for us. Many authors use the postfix superscript
"to the minus one".
|
| ⊢
◡A = {⟨x,
y⟩∣yAx} |
| |
| Definition | df-co 2427 |
Define the composition of two classes. Definition 6.6(3) of
[TakeutiZaring] p. 24. Note that
Definition 7 of [Suppes] p. 63
reverses A and B, uses / instead of ∘, and
calls the operation "relative product."
|
| ⊢
(A ∘ B) = {⟨x,
y⟩∣∃z(xBz ∧
zAy)} |
| |
| Definition | df-dm 2428 |
Define the domain of a class. Definition 3 of [Suppes] p. 59.
|
| ⊢
dom A = {x∣∃y xAy} |
| |
| Definition | df-rn 2429 |
Define the range of a class. For an alternate definition, see
dfrn2 2523.
|
| ⊢
ran A = dom ◡A |
| |
| Definition | df-res 2430 |
Define the restriction of a class. Definition 6.6(1) of [TakeutiZaring]
p. 24.
|
| ⊢
(A ↾ B) = (A ∩
(B × V)) |
| |
| Definition | df-ima 2431 |
Define the image of a class. Definition 6.6(2) of [TakeutiZaring]
p. 24. For an alternate definition, see dfima2 2604.
|
| ⊢
(A “ B) = ran (A
↾ B) |
| |
| Definition | df-fun 2432 |
Define a function. Definition 10.1 of [Quine]
p. 65. For alternate
definitions, see dffun2 2674, dffun3 2675, dffun4 2676, dffun5 2677, dffunmo 2679,
dffun6 2687, and dffun7 2688.
|
| ⊢
(Fun A ↔ (Rel A ∧ (A
∘ ◡A) ⊆ I)) |
| |
| Definition | df-fn 2433 |
Define a function with domain. Definition 6.15(1) of
[TakeutiZaring] p. 27.
|
| ⊢
(A Fn B ↔ (Fun A
∧ dom A = B)) |
| |
| Definition | df-f 2434 |
Define a function (mapping) with domain and co-domain. Definition
6.15(3) of [TakeutiZaring] p. 27.
|
| ⊢
(F:A–→B
↔ (F Fn A ∧ ran F
⊆ B)) |
| |
| Definition | df-f1 2435 |
Define a one-to-one function. For an equivalent definition see f11 2780.
Compare Definition 6.15(5) of [TakeutiZaring] p. 27.
|
| ⊢
(F:A–1-1→B ↔
(F:A–→B
∧ Fun ◡F)) |
| |
| Definition | df-fo 2436 |
Define an onto function. Definition 6.15(4) of [TakeutiZaring]
p. 27.
|
| ⊢
(F:A–onto→B ↔
(F Fn A ∧ ran F =
B)) |
| |
| Definition | df-f1o 2437 |
Define a one-to-one onto function. For equivalent definitions see
f1o2 2804, f1o3 2805, f1o4 2807,
and f1o5 2808. Compare Definition 6.15(6) of
[TakeutiZaring] p. 27.
|
| ⊢
(F:A–1-1-onto→B ↔
(F:A–1-1→B ∧
F:A–onto→B)) |
| |
| Definition | df-fv 2438 |
Define the value of a function. Although it has roots in Definition
10.2 of [Quine] p. 65, our definition
apparently does not appear in the
literature but is quite convenient: it can be applied to any class
and evaluates to the empty set when it is not meaningful. The left
apostrophe notation is common in set theory and means the same thing as
the more familiar F(A) notation for a function's value at A,
i.e. "F of A", but without context-dependent ambiguity.
For
more conventional alternate definitions, see fv2 2828
and fv3 2839;
restricted equivalents are shown in funfv 2862 and funfv2 2863. For the
familiar definition of function value in terms of ordered pair
membership see funfvop 2857.
|
| ⊢
(F ‘A) = ∪{x∣(F
“ {A}) = {x}} |
| |
| Definition | df-iso 2439 |
Define the isomorphism predicate. We read this as "H is an R,
S isomorphism of A onto B."
Normally, R and S
are ordering relations on A and
B respectively. Definition 6.28
of [TakeutiZaring] p. 32, whose
notation is the same as ours except
that R and S are subscripts.
|
| ⊢
(H Isom R, S (A, B) ↔
(H:A–1-1-onto→B ∧
∀x ∈ A ∀y
∈ A (xRy ↔ (H
‘x)S(H
‘y)))) |
| |
| Theorem | xpeq1 2440 |
Equality theorem for cross product.
|
| ⊢
(A = B → (A
× C) = (B × C)) |
| |
| Theorem | xpeq2 2441 |
Equality theorem for cross product.
|
| ⊢
(A = B → (C
× A) = (C × B)) |
| |
| Theorem | elxp 2442 |
Membership in a cross product.
|
| ⊢
(A ∈ (B × C)
↔ ∃x∃y(A =
⟨x, y⟩ ∧ (x ∈ B
∧ y ∈ C))) |
| |
| Theorem | elxp2 2443 |
Membership in a cross product.
|
| ⊢
(A ∈ (B × C)
↔ ∃x ∈ B ∃y
∈ C A = ⟨x,
y⟩) |
| |
| Theorem | hbxp 2444 |
Bound-variable hypothesis builder for cross product.
|
| ⊢
(y ∈ A → ∀x y ∈
A)
& ⊢ (y ∈ B
→ ∀x y ∈ B) ⇒ ⊢ (y ∈
(A × B) → ∀x y ∈
(A × B)) |
| |
| Theorem | opelxpex 2445 |
The first member of an ordered pair of classes in a cross product
exists. (This is a byproduct of our definition of ordered pair.
Unfortunately existence is not implied for the second member.)
|
| ⊢
(⟨A, B⟩ ∈ (C × D)
→ A ∈ V) |
| |
| Theorem | brrelex 2446 |
A true binary relation on a relation implies the first argument is a set.
(This is a property of our ordered pair definition.)
|
| ⊢
((Rel R ∧ ARB) → A
∈ V) |
| |
| Theorem | brrelexi 2447 |
The first argument of a binary relation exists. (An artifact of our
ordered pair definition.)
|
| ⊢
Rel R
⇒ ⊢ (ARB → A
∈ V) |
| |
| Theorem | fconstopab 2448 |
Representation of a constant function using ordered pairs.
|
| ⊢
(A × {B}) = {⟨x,
y⟩∣(x ∈ A
∧ y = B)} |
| |
| Theorem | vtoclr 2449 |
Variable to class conversion of transitive relation.
|
| ⊢
Rel R
& ⊢ ((xRy ∧ yRz) → xRz) ⇒ ⊢ (C ∈
D → ((ARB ∧ BRC) → ARC)) |
| |
| Theorem | vtoclrbr 2450 |
Variable to class conversion of transitive, reflexive relation.
|
| ⊢
Rel R
& ⊢ ((xRy ∧ yRz) → xRz) & ⊢ xRx ⇒ ⊢ ((ARB ∧
BRC) →
ARC) |
| |
| Theorem | vtoclibr 2451 |
Variable to class conversion of transitive, irreflexive relation.
|
| ⊢
Rel R
& ⊢ ((xRy ∧ yRz) → xRz) & ⊢ ¬ xRx ⇒ ⊢ ((ARB ∧
BRC) →
ARC) |
| |
| Theorem | opelxp 2452 |
Ordered pair membership in a cross product.
|
| ⊢
B ∈ V
⇒ ⊢ (⟨A, B⟩
∈ (C × D) ↔ (A
∈ C ∧ B ∈ D)) |
| |
| Theorem | brxp 2453 |
Binary relation on a cross product.
|
| ⊢
B ∈ V
⇒ ⊢ (A(C ×
D)B
↔ (A ∈ C ∧ B
∈ D)) |
| |
| Theorem | opelxpg 2454 |
Ordered pair membership in a cross product.
|
| ⊢
(B ∈ R → (⟨A, B⟩
∈ (C × D) ↔ (A
∈ C ∧ B ∈ D))) |
| |
| Theorem | opelxpi 2455 |
Ordered pair membership in a cross product (implication).
|
| ⊢
((A ∈ C ∧ B
∈ D) → ⟨A, B⟩
∈ (C × D)) |
| |
| Theorem | ralxp 2456 |
Universal quantification restricted to a cross product is equivalent
to a double restricted quantification. The hypothesis specifies an
implicit substitution.
|
| ⊢
(x = ⟨y, z⟩
→ (φ ↔ ψ))
⇒ ⊢
(∀x ∈ (A × B)φ ↔
∀y ∈ A ∀z
∈ B ψ) |
| |
| Theorem | opthprc 2457 |
Justification theorem for an ordered pair definition that works for
any classes, including proper classes. This is the definition implied
by the footnote in [Jech] p. 78, which
says, "The sophisticated reader
will not object to our use of a pair of classes."
|
| ⊢
(((A × {∅}) ∪
(B × {{∅}})) = ((C × {∅}) ∪ (D × {{∅}})) ↔ (A = C ∧
B = D)) |
| |
| Theorem | brelg 2458 |
Two things in a binary relation belong to the relation's domain.
|
| ⊢
R ⊆ (C × D) ⇒ ⊢ (B ∈
S → (ARB → (A
∈ C ∧ B ∈ D))) |
| |
| Theorem | brel 2459 |
Membership in superset of binary relation.
|
| ⊢
B ∈ V
& ⊢ R ⊆ (C
× D)
⇒ ⊢ (ARB → (A
∈ C ∧ B ∈ D)) |
| |
| Theorem | elxp3 2460 |
Membership in a cross product.
|
| ⊢
(A ∈ (B × C)
↔ ∃x∃y(⟨x,
y⟩ = A ∧ ⟨x, y⟩
∈ (B × C))) |
| |
| Theorem | xpundi 2461 |
Distributive law for cross product over union. Theorem 103 of [Suppes]
p. 52.
|
| ⊢
(A × (B ∪ C)) =
((A × B) ∪ (A
× C)) |
| |
| Theorem | xpundir 2462 |
Distributive law for cross product over union. Similar to Theorem 103
of [Suppes] p. 52.
|
| ⊢
((A ∪ B) × C) =
((A × C) ∪ (B
× C)) |
| |
| Theorem | xpun 2463 |
The cross product of two unions.
|
| ⊢
((A ∪ B) × (C
∪ D)) = (((A × C)
∪ (A × D)) ∪ ((B
× C) ∪ (B × D))) |
| |
| Theorem | elvv 2464 |
Membership in universal class of ordered pairs.
|
| ⊢
(A ∈ (V ×
V) ↔ ∃x∃y A =
⟨x, y⟩) |
| |
| Theorem | xpss 2465 |
A cross product is included in the ordered pair universe. Exercise
3 of [TakeutiZaring] p. 25.
|
| ⊢
(A × B) ⊆ (V × V) |
| |
| Theorem | brinxp 2466 |
Intersection of binary relation with cross product.
|
| ⊢
((A ∈ C ∧ B
∈ D) → (ARB ↔ A(R ∩
(C × D))B)) |
| |
| Theorem | weinxp 2467 |
Intersection of well-ordering with cross product of its field.
|
| ⊢
(R We A ↔ (R
∩ (A × A)) We A) |
| |
| Theorem | opabssxp 2468 |
An abstraction relation is a subset of a related cross product.
|
| ⊢
{⟨x, y⟩∣((x ∈ A
∧ y ∈ B) ∧ φ)} ⊆ (A × B) |
| |
| Theorem | optocl 2469 |
Implicit substitution of class for ordered pair.
|
| ⊢
D = (B × C) & ⊢ (⟨x,
y⟩ = A → (φ
↔ ψ))
& ⊢ ((x ∈ B
∧ y ∈ C) → φ)
⇒ ⊢ (A ∈ D
→ ψ) |
| |
| Theorem | 2optocl 2470 |
Implicit substitution of classes for ordered pairs.
|
| ⊢
R = (C × D) & ⊢ (⟨x,
y⟩ = A → (φ
↔ ψ))
& ⊢ (⟨z, w⟩ =
B → (ψ ↔ χ))
& ⊢ (((x ∈ C
∧ y ∈ D) ∧ (z
∈ C ∧ w ∈ D))
→ φ)
⇒ ⊢ ((A ∈ R
∧ B ∈ R) → χ) |
| |
| Theorem | 3optocl 2471 |
Implicit substitution of classes for ordered pairs.
|
| ⊢
R = (D × F) & ⊢ (⟨x,
y⟩ = A → (φ
↔ ψ))
& ⊢ (⟨z, w⟩ =
B → (ψ ↔ χ))
& ⊢ (⟨v, u⟩ =
C → (χ ↔ θ))
& ⊢ (((x ∈ D
∧ y ∈ F) ∧ (z
∈ D ∧ w ∈ F)
∧ (v ∈ D ∧ u
∈ F)) → φ)
⇒ ⊢ ((A ∈ R
∧ B ∈ R ∧ C
∈ R) → θ) |
| |
| Theorem | opbrop 2472 |
Ordered pair membership in a relation. Special case.
|
| ⊢
(((z = A ∧ w =
B) ∧ (v = C ∧
u = D)) → (φ ↔ ψ))
& ⊢ R = {⟨x,
y⟩∣((x ∈ (S
× S) ∧ y ∈ (S
× S)) ∧ ∃z∃w∃v∃u((x =
⟨z, w⟩ ∧ y
= ⟨v, u⟩) ∧ φ))}
⇒ ⊢ (((A ∈ S
∧ B ∈ S) ∧ (C
∈ S ∧ D ∈ S))
→ (⟨A, B⟩R⟨C,
D⟩ ↔ ψ)) |
| |
| Theorem | cbvop 2473 |
Change restricted bound variable to two restricted bound variables.
|
| ⊢
(x = ⟨y, z⟩
→ (φ ↔ ψ))
⇒ ⊢ (∃x ∈ (A
× B)φ ↔ ∃y ∈ A
∃z ∈ B ψ) |
| |
| Theorem | xp0r 2474 |
The cross product with the empty set is empty. Part of Theorem 3.13(ii)
of [Monk1] p. 37.
|
| ⊢
(∅ × A) =
∅ |
| |
| Theorem | 0nelxp 2475 |
The empty set is not a member of a cross product.
|
| ⊢
¬ ∅ ∈ (A × B) |
| |
| Theorem | onxpdisj 2476 |
Ordinal numbers and ordered pairs are disjoint collections. This
theorem can be used if we want to extend a set of ordinal numbers or
ordered pairs with disjoint elements. See also snsn0non 2371.
|
| ⊢
(On ∩ (V × V)) = ∅ |
| |
| Theorem | releq 2477 |
Equality theorem for relation predicate.
|
| ⊢
(A = B → (Rel A
↔ Rel B)) |
| |
| Theorem | hbrel 2478 |
Bound-variable hypothesis builder for a relation.
|
| ⊢
(y ∈ A → ∀x y ∈
A)
⇒ ⊢ (Rel A → ∀xRel A) |
| |
| Theorem | ssrel 2479 |
Subclass theorem for relation predicate. Theorem 2 of [Suppes] p. 58.
|
| ⊢
(A ⊆ B → (Rel B
→ Rel A)) |
| |
| Theorem | relss 2480 |
A subclass relationship depends only on a relation's ordered pairs.
Theorem 3.2(i) of [Monk1] p. 33.
|
| ⊢
(Rel A → (A ⊆ B
↔ ∀x∀y(⟨x,
y⟩ ∈ A → ⟨x, y⟩
∈ B))) |
| |
| Theorem | relssi 2481 |
Inference from subclass principle for relations.
|
| ⊢
Rel A
& ⊢ (⟨x, y⟩
∈ A → ⟨x, y⟩
∈ B)
⇒ ⊢ A ⊆ B |
| |
| Theorem | relssdv 2482 |
Deduction from subclass principle for relations.
|
| ⊢
(φ → Rel A) & ⊢ (φ
→ (⟨x, y⟩ ∈ A → ⟨x, y⟩
∈ B))
⇒ ⊢ (φ → A ⊆ B) |
| |
| Theorem | cleqrel 2483 |
Extensionality principle for relations. Theorem 3.2(ii) of [Monk1]
p. 33.
|
| ⊢
((Rel A ∧ Rel B) → (A =
B ↔ ∀x∀y(⟨x,
y⟩ ∈ A ↔ ⟨x, y⟩
∈ B))) |
| |
| Theorem | cleqreli 2484 |
Inference from extensionality principle for relations.
|
| ⊢
Rel A
& ⊢ Rel B & ⊢ (⟨x,
y⟩ ∈ A ↔ ⟨x, y⟩
∈ B)
⇒ ⊢ A = B |
| |
| Theorem | relsn 2485 |
A singleton of an ordered pair is a relation.
|
| ⊢
A ∈ V
⇒ ⊢ Rel
{⟨A, B⟩} |
| |
| Theorem | relxp 2486 |
A cross product is a relation. Theorem 3.13(i) of [Monk1] p. 37.
|
| ⊢
Rel (A × B) |
| |
| Theorem | ssxp 2487 |
Subset theorem for cross product. Generalization of Theorem 101 of
[Suppes] p. 52.
|
| ⊢
((A ⊆ B ∧ C
⊆ D) → (A × C)
⊆ (B × D)) |
| |
| Theorem | xpex 2488 |
The cross product of two sets is a set. Proposition 6.2 of
[TakeutiZaring] p. 23.
|
| ⊢
A ∈ V
& ⊢ B ∈ V
⇒ ⊢ (A × B)
∈ V |
| |
| Theorem | xpexg 2489 |
The cross product of two sets is a set. Generalization of Proposition
6.2 of [TakeutiZaring] p. 23.
|
| ⊢
((A ∈ C ∧ B
∈ D) → (A × B)
∈ V) |
| |
| Theorem | relun 2490 |
The union of two relations is a relation. Compare Exercise 5 of
[TakeutiZaring] p. 25.
|
| ⊢
(Rel (A ∪ B) ↔ (Rel A ∧ Rel B)) |
| |
| Theorem | relin 2491 |
The intersection with a relation is a relation.
|
| ⊢
(Rel A → Rel (A ∩ B)) |
| |
| Theorem | reldif 2492 |
A difference cutting down a relation is a relation.
|
| ⊢
(Rel A → Rel (A ∖ B)) |
| |
| Theorem | reluni 2493 |
Union law for relations. Exercise 6 of [TakeutiZaring] p. 25 and its
converse.
|
| ⊢
(Rel ∪A
↔ ∀x ∈ A Rel x) |
| |
| Theorem | relopab 2494 |
A class of ordered pairs is a relation.
|
| ⊢
Rel {⟨x, y⟩∣φ} |
| |
| Theorem | inopab 2495 |
Intersection of two ordered pair class abstractions.
|
| ⊢
({⟨x, y⟩∣φ} ∩ {⟨x, y⟩∣ψ}) = {⟨x, y⟩∣(φ ∧ ψ)} |
| |
| Theorem | inxp 2496 |
The intersection of two cross products. Exercise 9 of [TakeutiZaring]
p. 25.
|
| ⊢
((A × B) ∩ (C
× D)) = ((A ∩ C)
× (B ∩ D)) |
| |
| Theorem | xpindi 2497 |
Distributive law for cross product over intersection. Theorem 102 of
[Suppes] p. 52.
|
| ⊢
(A × (B ∩ C)) =
((A × B) ∩ (A
× C)) |
| |
| Theorem | xpindir 2498 |
Distributive law for cross product over intersection. Similar to
Theorem 102 of [Suppes] p. 52.
|
| ⊢
((A ∩ B) × C) =
((A × C) ∩ (B
× C)) |
| |
| Theorem | rel0 2499 |
The empty set is a relation.
|
| ⊢
Rel ∅ |
| |
| Theorem | reli 2500 |
The identity relation is a relation. Part of Exercise 4.12(p) of
[Mendelson] p. 235.
|
| ⊢
Rel I |
Home
Hilbert Space Explorer
(4958-5787)