Theorem List for New Foundations Explorer - 4501-4600 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | tfinltfin 4501 |
Ordering rule for the finite T operation. Corollary to theorem X.1.33
of [Rosser] p. 529. (Contributed by SF,
1-Feb-2015.)
|
⊢ ((M ∈ Nn ∧ N ∈ Nn ) →
(⟪M, N⟫ ∈
<fin ↔ ⟪ Tfin M,
Tfin N⟫ ∈
<fin )) |
|
Theorem | tfinlefin 4502 |
Ordering rule for the finite T operation. Theorem X.1.33 of [Rosser]
p. 529. (Contributed by SF, 2-Feb-2015.)
|
⊢ ((M ∈ Nn ∧ N ∈ Nn ) →
(⟪M, N⟫ ∈
≤fin ↔ ⟪ Tfin M,
Tfin N⟫ ∈
≤fin )) |
|
Theorem | evenfinex 4503 |
The set of all even naturals exists. (Contributed by SF,
20-Jan-2015.)
|
⊢ Evenfin ∈
V |
|
Theorem | oddfinex 4504 |
The set of all odd naturals exists. (Contributed by SF,
20-Jan-2015.)
|
⊢ Oddfin
∈ V |
|
Theorem | 0ceven 4505 |
Cardinal zero is even. (Contributed by SF, 20-Jan-2015.)
|
⊢ 0c ∈ Evenfin |
|
Theorem | evennn 4506 |
An even finite cardinal is a finite cardinal. (Contributed by SF,
20-Jan-2015.)
|
⊢ (A ∈ Evenfin
→ A ∈ Nn
) |
|
Theorem | oddnn 4507 |
An odd finite cardinal is a finite cardinal. (Contributed by SF,
20-Jan-2015.)
|
⊢ (A ∈ Oddfin
→ A ∈ Nn
) |
|
Theorem | evennnul 4508 |
An even number is nonempty. (Contributed by SF, 22-Jan-2015.)
|
⊢ (A ∈ Evenfin
→ A ≠ ∅) |
|
Theorem | oddnnul 4509 |
An odd number is nonempty. (Contributed by SF, 22-Jan-2015.)
|
⊢ (A ∈ Oddfin
→ A ≠ ∅) |
|
Theorem | sucevenodd 4510 |
The successor of an even natural is odd. (Contributed by SF,
20-Jan-2015.)
|
⊢ ((A ∈ Evenfin
∧ (A
+c 1c) ≠ ∅) → (A
+c 1c) ∈
Oddfin ) |
|
Theorem | sucoddeven 4511 |
The successor of an odd natural is even. (Contributed by SF,
22-Jan-2015.)
|
⊢ ((A ∈ Oddfin
∧ (A
+c 1c) ≠ ∅) → (A
+c 1c) ∈
Evenfin ) |
|
Theorem | dfevenfin2 4512* |
Alternate definition of even number. (Contributed by SF,
25-Jan-2015.)
|
⊢ Evenfin = {x ∣ ∃n ∈ Nn (x = (n
+c n) ∧ (n
+c n) ≠ ∅)} |
|
Theorem | dfoddfin2 4513* |
Alternate definition of odd number. (Contributed by SF,
25-Jan-2015.)
|
⊢ Oddfin
= {x ∣
∃n
∈ Nn (x = ((n
+c n)
+c 1c) ∧
((n +c n) +c 1c) ≠
∅)} |
|
Theorem | evenoddnnnul 4514 |
Every nonempty finite cardinal is either even or odd. Theorem X.1.35 of
[Rosser] p. 529. (Contributed by SF,
20-Jan-2015.)
|
⊢ ( Evenfin ∪ Oddfin ) = ( Nn
∖ {∅}) |
|
Theorem | evenodddisjlem1 4515* |
Lemma for evenodddisj 4516. Establish stratification for induction.
(Contributed by SF, 25-Jan-2015.)
|
⊢ {j ∣ ((j
+c j) ≠ ∅ → ∀n ∈ Nn (((n +c n) +c 1c) ≠
∅ → (j +c j) ≠ ((n
+c n)
+c 1c)))} ∈ V |
|
Theorem | evenodddisj 4516 |
The even finite cardinals and the odd ones are disjoint. Theorem X.1.36
of [Rosser] p. 529. (Contributed by SF,
22-Jan-2015.)
|
⊢ ( Evenfin ∩ Oddfin ) = ∅ |
|
Theorem | eventfin 4517 |
If M is even , then so is
Tfin M. Theorem X.1.37 of
[Rosser] p. 530. (Contributed by SF,
26-Jan-2015.)
|
⊢ (M ∈ Evenfin
→ Tfin M ∈ Evenfin ) |
|
Theorem | oddtfin 4518 |
If M is odd , then so is
Tfin M. Theorem X.1.38 of [Rosser]
p. 530. (Contributed by SF, 26-Jan-2015.)
|
⊢ (M ∈ Oddfin
→ Tfin M ∈ Oddfin ) |
|
Theorem | nnadjoinlem1 4519* |
Lemma for nnadjoin 4520. Establish stratification. (Contributed by
SF,
29-Jan-2015.)
|
⊢ {n ∣ ∀l ∈ n (y ∈ ∼ ∪l → {x
∣ ∃b ∈ l x = (b ∪
{y})} ∈
n)} ∈
V |
|
Theorem | nnadjoin 4520* |
Adjoining a new element to every member of L does not change its
size. Theorem X.1.39 of [Rosser] p. 530.
(Contributed by SF,
29-Jan-2015.)
|
⊢ ((N ∈ Nn ∧ L ∈ N ∧ X ∈ ∼ ∪L) → {x
∣ ∃b ∈ L x = (b ∪
{X})} ∈
N) |
|
Theorem | nnadjoinpw 4521 |
Adjoining an element to a power class. Theorem X.1.40 of [Rosser]
p. 530. (Contributed by SF, 27-Jan-2015.)
|
⊢ (((M ∈ Nn ∧ N ∈ Nn ) ∧ (A ∈ M ∧ X ∈ ∼ A)
∧ ℘A ∈ N) →
℘(A
∪ {X}) ∈ (N
+c N)) |
|
Theorem | nnpweqlem1 4522* |
Lemma for nnpweq 4523. Establish stratification for induction.
(Contributed by SF, 26-Jan-2015.)
|
⊢ {m ∣ ∀a ∈ m ∀b ∈ m ∃n ∈ Nn (℘a ∈ n ∧ ℘b ∈ n)} ∈ V |
|
Theorem | nnpweq 4523* |
If two sets are the same finite size, then so are their power classes.
Theorem X.1.41 of [Rosser] p. 530.
(Contributed by SF, 26-Jan-2015.)
|
⊢ ((M ∈ Nn ∧ A ∈ M ∧ B ∈ M) →
∃n
∈ Nn (℘A ∈ n ∧ ℘B ∈ n)) |
|
Theorem | srelk 4524 |
Binary relationship form of the Sfin relationship. (Contributed
by SF, 23-Jan-2015.)
|
⊢ A ∈ V
& ⊢ B ∈ V ⇒ ⊢ (⟪A,
B⟫ ∈ (( Nn
×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k
V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c))
“k ℘1℘1℘11c)) ↔ Sfin (A,
B)) |
|
Theorem | srelkex 4525 |
The expression at the core of srelk 4524 exists. (Contributed by SF,
30-Jan-2015.)
|
⊢ (( Nn
×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((℘1c ×k
V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c))
“k ℘1℘1℘11c)) ∈ V |
|
Theorem | sfineq1 4526 |
Equality theorem for the finite S relationship. (Contributed by SF,
27-Jan-2015.)
|
⊢ (A =
B → ( Sfin (A,
C) ↔ Sfin (B,
C))) |
|
Theorem | sfineq2 4527 |
Equality theorem for the finite S relationship. (Contributed by SF,
27-Jan-2015.)
|
⊢ (A =
B → ( Sfin (C,
A) ↔ Sfin (C,
B))) |
|
Theorem | sfin01 4528 |
Zero and one satisfy Sfin. Theorem X.1.42 of [Rosser] p. 530.
(Contributed by SF, 30-Jan-2015.)
|
⊢ Sfin
(0c, 1c) |
|
Theorem | sfin112 4529 |
Equality law for the finite S operator. Theorem X.1.43 of [Rosser]
p. 530. (Contributed by SF, 27-Jan-2015.)
|
⊢ (( Sfin
(M, N)
∧ Sfin (M,
P)) → N = P) |
|
Theorem | sfindbl 4530* |
If the unit power set of a set is in the successor of a finite cardinal,
then there is a natural that is smaller than the finite cardinal and
whose double is smaller than the successor of the cardinal. Theorem
X.1.44 of [Rosser] p. 531. (Contributed
by SF, 30-Jan-2015.)
|
⊢ ((M ∈ Nn ∧ ℘1A ∈ (M +c 1c))
→ ∃n ∈ Nn ( Sfin
(M, n)
∧ Sfin ((M
+c 1c), (n +c n)))) |
|
Theorem | sfintfinlem1 4531* |
Lemma for sfintfin 4532. Set up induction stratification.
(Contributed
by SF, 31-Jan-2015.)
|
⊢ {m ∣ ∀n( Sfin
(m, n)
→ Sfin ( Tfin m,
Tfin n))} ∈
V |
|
Theorem | sfintfin 4532 |
If two numbers obey Sfin,
then do their T raisings. Theorem
X.1.45 of [Rosser] p. 532. (Contributed
by SF, 30-Jan-2015.)
|
⊢ ( Sfin
(M, N)
→ Sfin ( Tfin M,
Tfin N)) |
|
Theorem | tfinnnlem1 4533* |
Lemma for tfinnn 4534. Establish stratification. (Contributed by
SF,
30-Jan-2015.)
|
⊢ {n ∣ ∀y ∈ n (y ⊆ Nn →
{a ∣
∃x
∈ y
a = Tfin x}
∈ Tfin n)}
∈ V |
|
Theorem | tfinnn 4534* |
T-raising of a set of naturals. Theorem X.1.46 of [Rosser] p. 532.
(Contributed by SF, 30-Jan-2015.)
|
⊢ ((N ∈ Nn ∧ A ⊆ Nn ∧ A ∈ N) →
{a ∣
∃x
∈ A
a = Tfin x}
∈ Tfin N) |
|
Theorem | sfinltfin 4535 |
Ordering law for finite smaller than. Theorem X.1.47 of [Rosser]
p. 532. (Contributed by SF, 30-Jan-2015.)
|
⊢ ((( Sfin (M,
N) ∧
Sfin (P, Q)) ∧ ⟪M,
P⟫ ∈ <fin ) → ⟪N, Q⟫
∈ <fin ) |
|
Theorem | sfin111 4536 |
The finite smaller relationship is one-to-one in its first argument.
Theorem X.1.48 of [Rosser] p. 533.
(Contributed by SF, 29-Jan-2015.)
|
⊢ (( Sfin
(M, P)
∧ Sfin (N,
P)) → M = N) |
|
Theorem | spfinex 4537 |
Spfin is a set.
(Contributed by SF, 20-Jan-2015.)
|
⊢ Spfin
∈ V |
|
Theorem | ncvspfin 4538 |
The cardinality of the universe is in the finite Sp set. Theorem X.1.49
of [Rosser] p. 534. (Contributed by SF,
27-Jan-2015.)
|
⊢ Ncfin
V ∈ Spfin |
|
Theorem | spfinsfincl 4539 |
If X is in Spfin and Z is smaller than X, then Z
is also in Spfin.
Theorem X.1.50 of [Rosser] p. 534.
(Contributed by SF, 27-Jan-2015.)
|
⊢ ((X ∈ Spfin
∧ Sfin (Z,
X)) → Z ∈ Spfin ) |
|
Theorem | spfininduct 4540* |
Inductive principle for Spfin. Theorem X.1.51 of [Rosser]
p. 534. (Contributed by SF, 27-Jan-2015.)
|
⊢ ((B ∈ V ∧ Ncfin V
∈ B
∧ ∀x ∈ Spfin
∀z((x ∈ B ∧ Sfin
(z, x)) → z
∈ B))
→ Spfin ⊆ B) |
|
Theorem | vfinspnn 4541 |
If the universe is finite, then Spfin is a subset of the nonempty
naturals. Theorem X.1.53 of [Rosser] p.
534. (Contributed by SF,
27-Jan-2015.)
|
⊢ (V ∈ Fin → Spfin ⊆ (
Nn ∖ {∅})) |
|
Theorem | 1cvsfin 4542 |
If the universe is finite, then Ncfin 1c is the base
two log of
Ncfin V. Theorem
X.1.54 of [Rosser] p. 534. (Contributed by SF,
29-Jan-2015.)
|
⊢ (V ∈ Fin → Sfin
( Ncfin 1c, Ncfin V)) |
|
Theorem | 1cspfin 4543 |
If the universe is finite, then the size of 1c
is in Spfin.
Corollary of Theorem X.1.54 of [Rosser] p.
534. (Contributed by SF,
29-Jan-2015.)
|
⊢ (V ∈ Fin → Ncfin 1c ∈ Spfin
) |
|
Theorem | tncveqnc1fin 4544 |
If the universe is finite, then the T-raising of the size of the universe
is equal to the size of 1c. Theorem
X.1.55 of [Rosser] p. 534.
(Contributed by SF, 29-Jan-2015.)
|
⊢ (V ∈ Fin → Tfin
Ncfin V = Ncfin 1c) |
|
Theorem | t1csfin1c 4545 |
If the universe is finite, then the T-raising of the size of 1c is
smaller than the size itself. Corollary of theorem X.1.56 of [Rosser]
p. 534. (Contributed by SF, 29-Jan-2015.)
|
⊢ (V ∈ Fin → Sfin
( Tfin Ncfin 1c, Ncfin
1c)) |
|
Theorem | vfintle 4546 |
If the universe is finite, then the T-raising of all nonempty naturals
are no greater than the size of 1c.
Theorem X.1.56 of [Rosser]
p. 534. (Contributed by SF, 30-Jan-2015.)
|
⊢ ((V ∈ Fin ∧ N ∈ Nn ∧ N ≠ ∅) →
⟪ Tfin N, Ncfin
1c⟫ ∈
≤fin ) |
|
Theorem | vfin1cltv 4547 |
If the universe is finite, then 1c is strictly
smaller than the
universe. Theorem X.1.57 of [Rosser] p.
534. (Contributed by SF,
30-Jan-2015.)
|
⊢ (V ∈ Fin → ⟪ Ncfin 1c, Ncfin V⟫ ∈ <fin ) |
|
Theorem | vfinncvntnn 4548 |
If the universe is finite, then the size of the universe is not the
T-raising of a natural. Theorem X.1.58 of [Rosser] p. 534.
(Contributed by SF, 29-Jan-2015.)
|
⊢ ((V ∈ Fin ∧ N ∈ Nn ) → Tfin N
≠ Ncfin V) |
|
Theorem | vfinncvntsp 4549* |
If the universe is finite, then its size is not a T raising of an
element of Spfin.
Corollary of theorem X.1.58 of [Rosser]
p. 534. (Contributed by SF, 27-Jan-2015.)
|
⊢ (V ∈ Fin → ¬ Ncfin V ∈
{a ∣
∃x
∈ Spfin a
= Tfin x}) |
|
Theorem | vfinspsslem1 4550* |
Lemma for vfinspss 4551. Establish part of the inductive step.
(Contributed by SF, 3-Feb-2015.)
|
⊢ (((V ∈ Fin ∧ Tfin n
∈ Spfin ) ∧
(n ∈
Spfin ∧ Sfin
(z, Tfin n))) → ∃x ∈ Spfin
z = Tfin x) |
|
Theorem | vfinspss 4551* |
If the universe is finite, then Spfin is a subset of its T
raisings and the cardinality of the universe. Theorem X.1.59 of
[Rosser] p. 534. (Contributed by SF,
29-Jan-2015.)
|
⊢ (V ∈ Fin → Spfin ⊆
({a ∣
∃x
∈ Spfin a
= Tfin x} ∪ { Ncfin V})) |
|
Theorem | vfinspclt 4552 |
If the universe is finite, then Spfin is closed under T-raising.
Theorem X.1.60 of [Rosser] p. 536.
(Contributed by SF, 30-Jan-2015.)
|
⊢ ((V ∈ Fin ∧ X ∈ Spfin ) → Tfin X
∈ Spfin ) |
|
Theorem | vfinspeqtncv 4553* |
If the universe is finite, then Spfin is equal to its T raisings
and the cardinality of the universe. Theorem X.1.61 of [Rosser] p. 536.
(Contributed by SF, 29-Jan-2015.)
|
⊢ (V ∈ Fin → Spfin = ({a ∣ ∃x ∈ Spfin
a = Tfin x}
∪ { Ncfin V})) |
|
Theorem | vfinncsp 4554 |
If the universe is finite, then the size of Spfin is equal to the
successor of its T-raising. Theorem X.1.62 of [Rosser] p. 536.
(Contributed by SF, 20-Jan-2015.)
|
⊢ (V ∈ Fin → Ncfin Spfin = ( Tfin Ncfin Spfin +c
1c)) |
|
Theorem | vinf 4555 |
The universe is infinite. Theorem X.1.63 of [Rosser] p. 536.
(Contributed by SF, 20-Jan-2015.)
|
⊢ ¬ V ∈
Fin |
|
Theorem | nulnnn 4556 |
The empty class is not a natural. Theorem X.1.65 of [Rosser] p. 536.
(Contributed by SF, 20-Jan-2015.)
|
⊢ ¬ ∅
∈ Nn |
|
Theorem | peano4 4557 |
The successor operation is one-to-one over the finite cardinals. Theorem
X.1.66 of [Rosser] p. 537. (Contributed by
SF, 20-Jan-2015.)
|
⊢ ((M ∈ Nn ∧ N ∈ Nn ∧ (M
+c 1c) = (N +c 1c))
→ M = N) |
|
Theorem | suc11nnc 4558 |
Successor cancellation law for finite cardinals. (Contributed by SF,
3-Feb-2015.)
|
⊢ ((M ∈ Nn ∧ N ∈ Nn ) →
((M +c
1c) = (N
+c 1c) ↔ M = N)) |
|
Theorem | addccan2 4559 |
Cancellation law for natural addition. (Contributed by SF,
3-Feb-2015.)
|
⊢ ((M ∈ Nn ∧ N ∈ Nn ∧ P ∈ Nn ) →
((M +c N) = (M
+c P) ↔ N = P)) |
|
Theorem | addccan1 4560 |
Cancellation law for natural addition. (Contributed by SF,
3-Feb-2015.)
|
⊢ ((M ∈ Nn ∧ N ∈ Nn ∧ P ∈ Nn ) →
((M +c P) = (N
+c P) ↔ M = N)) |
|
2.3 Ordered Pairs, Relationships, and
Functions
|
|
2.3.1 Ordered Pairs
|
|
Syntax | cop 4561 |
Declare the syntax for an ordered pair.
|
class
〈A, B〉 |
|
Syntax | cphi 4562 |
Declare the syntax for the Phi operation.
|
class
Phi A |
|
Syntax | cproj1 4563 |
Declare the syntax for the first projection operation.
|
class
Proj1 A |
|
Syntax | cproj2 4564 |
Declare the syntax for the second projection operation.
|
class
Proj2 A |
|
Definition | df-phi 4565* |
Define the phi operator. This operation increments all the naturals in
A and leaves all its
other members the same. (Contributed by SF,
3-Feb-2015.)
|
⊢ Phi A = {y ∣ ∃x ∈ A y =
if(x ∈
Nn , (x
+c 1c), x)} |
|
Definition | df-op 4566* |
Define the type-level ordered pair. Definition from [Rosser] p. 281.
(Contributed by SF, 3-Feb-2015.)
|
⊢ 〈A, B〉 = ({x ∣ ∃y ∈ A x = Phi y} ∪
{x ∣
∃y
∈ B
x = ( Phi
y ∪
{0c})}) |
|
Definition | df-proj1 4567* |
Define the first projection operation. This operation recovers the
first element of an ordered pair. Definition from [Rosser] p. 281.
(Contributed by SF, 3-Feb-2015.)
|
⊢ Proj1 A = {x ∣ Phi x ∈ A} |
|
Definition | df-proj2 4568* |
Define the second projection operation. This operation recovers the
second element of an ordered pair. Definition from [Rosser] p. 281.
(Contributed by SF, 3-Feb-2015.)
|
⊢ Proj2 A = {x ∣ ( Phi x ∪ {0c}) ∈ A} |
|
Theorem | dfphi2 4569 |
Express the phi operator in terms of the Kuratowski set construction
functions. (Contributed by SF, 3-Feb-2015.)
|
⊢ Phi A = (((Imagek(( Ins3k ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k
℘1℘1℘1℘11c))
“k ℘1℘11c) ∩ ( Nn ×k V)) ∪ (
Ik ∩ ( ∼ Nn
×k V))) “k A) |
|
Theorem | phieq 4570 |
Equality law for the Phi operation. (Contributed by SF, 3-Feb-2015.)
|
⊢ (A =
B → Phi
A = Phi
B) |
|
Theorem | phiexg 4571 |
The phi operator preserves sethood. (Contributed by SF, 3-Feb-2015.)
|
⊢ (A ∈ V →
Phi A ∈ V) |
|
Theorem | phiex 4572 |
The phi operator preserves sethood. (Contributed by SF, 3-Feb-2015.)
|
⊢ A ∈ V ⇒ ⊢ Phi A ∈
V |
|
Theorem | dfop2lem1 4573* |
Lemma for dfop2 4575 and dfproj22 4577. (Contributed by SF, 2-Jan-2015.)
|
⊢ (⟪x,
y⟫ ∈ ∼ (( Ins2k Sk ⊕ Ins3k ((◡kImagek((Imagek((
Ins3k ∼ (( Ins3k Sk ∩
Ins2k Sk )
“k ℘1℘11c) ∖ ((
Ins2k Ins2k
Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k
SIk SIk
Sk )) “k ℘1℘1℘1℘11c)) “k ℘1℘11c) ∩ ( Nn
×k V)) ∪ ( Ik ∩ ( ∼ Nn
×k V))) ∘k Sk ) ∪ ({{0c}} ×k
V))) “k ℘1℘11c) ↔ y = ( Phi x
∪ {0c})) |
|
Theorem | dfop2lem2 4574* |
Lemma for dfop2 4575. (Contributed by SF, 2-Jan-2015.)
|
⊢ ( ∼ (( Ins2k Sk ⊕ Ins3k ((◡kImagek((Imagek((
Ins3k ∼ (( Ins3k Sk ∩
Ins2k Sk )
“k ℘1℘11c) ∖ ((
Ins2k Ins2k
Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k
SIk SIk
Sk )) “k ℘1℘1℘1℘11c)) “k ℘1℘11c) ∩ ( Nn
×k V)) ∪ ( Ik ∩ ( ∼ Nn
×k V))) ∘k Sk ) ∪ ({{0c}} ×k
V))) “k ℘1℘11c) “k B) = {x ∣ ∃y
∈ B x = ( Phi y
∪ {0c})} |
|
Theorem | dfop2 4575 |
Express the ordered pair via the set construction functors.
(Contributed by SF, 2-Jan-2015.)
|
⊢ 〈A, B〉 =
((Imagek((Imagek(( Ins3k ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k
℘1℘1℘1℘11c))
“k ℘1℘11c) ∩ ( Nn ×k V)) ∪ (
Ik ∩ ( ∼ Nn
×k V))) “k A) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k ((◡kImagek((Imagek((
Ins3k ∼ (( Ins3k Sk ∩
Ins2k Sk )
“k ℘1℘11c) ∖ ((
Ins2k Ins2k
Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k
SIk SIk
Sk )) “k ℘1℘1℘1℘11c)) “k ℘1℘11c) ∩ ( Nn
×k V)) ∪ ( Ik ∩ ( ∼ Nn
×k V))) ∘k Sk ) ∪ ({{0c}} ×k
V))) “k ℘1℘11c) “k B)) |
|
Theorem | dfproj12 4576 |
Express the first projection operator via the set construction functors.
(Contributed by SF, 2-Jan-2015.)
|
⊢ Proj1 A = (◡kImagek((Imagek((
Ins3k ∼ (( Ins3k Sk ∩
Ins2k Sk )
“k ℘1℘11c) ∖ ((
Ins2k Ins2k
Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k
SIk SIk
Sk )) “k ℘1℘1℘1℘11c)) “k ℘1℘11c) ∩ ( Nn
×k V)) ∪ ( Ik ∩ ( ∼ Nn
×k V))) “k A) |
|
Theorem | dfproj22 4577 |
Express the second projection operator via the set construction
functors. (Contributed by SF, 2-Jan-2015.)
|
⊢ Proj2 A = (◡k ∼ (( Ins2k Sk ⊕ Ins3k ((◡kImagek((Imagek((
Ins3k ∼ (( Ins3k Sk ∩
Ins2k Sk )
“k ℘1℘11c) ∖ ((
Ins2k Ins2k
Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k
SIk SIk
Sk )) “k ℘1℘1℘1℘11c)) “k ℘1℘11c) ∩ ( Nn
×k V)) ∪ ( Ik ∩ ( ∼ Nn
×k V))) ∘k Sk ) ∪ ({{0c}} ×k
V))) “k ℘1℘11c) “k A) |
|
Theorem | opeq1 4578 |
Equality theorem for ordered pairs. (Contributed by SF, 2-Jan-2015.)
|
⊢ (A =
B → 〈A, C〉 = 〈B, C〉) |
|
Theorem | opeq2 4579 |
Equality theorem for ordered pairs. (Contributed by SF, 2-Jan-2015.)
|
⊢ (A =
B → 〈C, A〉 = 〈C, B〉) |
|
Theorem | opeq12 4580 |
Equality theorem for ordered pairs. (Contributed by SF, 2-Jan-2015.)
|
⊢ ((A =
B ∧
C = D)
→ 〈A, C〉 = 〈B, D〉) |
|
Theorem | opeq1i 4581 |
Equality inference for ordered pairs. (Contributed by SF,
16-Dec-2006.)
|
⊢ A =
B ⇒ ⊢ 〈A, C〉 = 〈B, C〉 |
|
Theorem | opeq2i 4582 |
Equality inference for ordered pairs. (Contributed by SF,
16-Dec-2006.)
|
⊢ A =
B ⇒ ⊢ 〈C, A〉 = 〈C, B〉 |
|
Theorem | opeq12i 4583 |
Equality inference for ordered pairs. (The proof was shortened by
Eric Schmidt, 4-Apr-2007.) (Contributed by SF, 16-Dec-2006.)
|
⊢ A =
B
& ⊢ C =
D ⇒ ⊢ 〈A, C〉 = 〈B, D〉 |
|
Theorem | opeq1d 4584 |
Equality deduction for ordered pairs. (Contributed by SF,
16-Dec-2006.)
|
⊢ (φ
→ A = B) ⇒ ⊢ (φ
→ 〈A, C〉 = 〈B, C〉) |
|
Theorem | opeq2d 4585 |
Equality deduction for ordered pairs. (Contributed by SF,
16-Dec-2006.)
|
⊢ (φ
→ A = B) ⇒ ⊢ (φ
→ 〈C, A〉 = 〈C, B〉) |
|
Theorem | opeq12d 4586 |
Equality deduction for ordered pairs. (The proof was shortened by
Andrew Salmon, 29-Jun-2011.) (Contributed by SF, 16-Dec-2006.)
(Revised by SF, 29-Jun-2011.)
|
⊢ (φ
→ A = B)
& ⊢ (φ
→ C = D) ⇒ ⊢ (φ
→ 〈A, C〉 = 〈B, D〉) |
|
Theorem | opexg 4587 |
An ordered pair of two sets is a set. (Contributed by SF, 2-Jan-2015.)
|
⊢ ((A ∈ V ∧ B ∈ W) →
〈A,
B〉 ∈ V) |
|
Theorem | opex 4588 |
An ordered pair of two sets is a set. (Contributed by SF,
5-Jan-2015.)
|
⊢ A ∈ V
& ⊢ B ∈ V ⇒ ⊢ 〈A, B〉 ∈
V |
|
Theorem | proj1eq 4589 |
Equality theorem for first projection operator. (Contributed by SF,
2-Jan-2015.)
|
⊢ (A =
B → Proj1
A = Proj1
B) |
|
Theorem | proj2eq 4590 |
Equality theorem for second projection operator. (Contributed by SF,
2-Jan-2015.)
|
⊢ (A =
B → Proj2
A = Proj2
B) |
|
Theorem | proj1exg 4591 |
The first projection of a set is a set. (Contributed by SF,
2-Jan-2015.)
|
⊢ (A ∈ V →
Proj1 A
∈ V) |
|
Theorem | proj2exg 4592 |
The second projection of a set is a set. (Contributed by SF,
2-Jan-2015.)
|
⊢ (A ∈ V →
Proj2 A
∈ V) |
|
Theorem | proj1ex 4593 |
The first projection of a set is a set. (Contributed by Scott Fenton,
16-Apr-2021.)
|
⊢ A ∈ V ⇒ ⊢ Proj1 A ∈
V |
|
Theorem | proj2ex 4594 |
The second projection of a set is a set. (Contributed by Scott Fenton,
16-Apr-2021.)
|
⊢ A ∈ V ⇒ ⊢ Proj2 A ∈
V |
|
Theorem | phi11lem1 4595 |
Lemma for phi11 4596. (Contributed by SF, 3-Feb-2015.)
|
⊢ ( Phi A = Phi B → A
⊆ B) |
|
Theorem | phi11 4596 |
The phi operator is one-to-one. Theorem X.2.2 of [Rosser] p. 282.
(Contributed by SF, 3-Feb-2015.)
|
⊢ (A =
B ↔ Phi
A = Phi
B) |
|
Theorem | 0cnelphi 4597 |
Cardinal zero is not a member of a phi operation. Theorem X.2.3 of
[Rosser] p. 282. (Contributed by SF,
3-Feb-2015.)
|
⊢ ¬ 0c ∈ Phi A |
|
Theorem | phi011lem1 4598 |
Lemma for phi011 4599. (Contributed by SF, 3-Feb-2015.)
|
⊢ (( Phi A ∪ {0c}) = ( Phi B ∪
{0c}) → Phi A ⊆ Phi B) |
|
Theorem | phi011 4599 |
( Phi A
∪ {0c}) is one-to-one. Theorem X.2.4 of [Rosser] p. 282.
(Contributed by SF, 3-Feb-2015.)
|
⊢ (A =
B ↔ ( Phi
A ∪ {0c}) =
( Phi B ∪
{0c})) |
|
Theorem | proj1op 4600 |
The first projection operator applied to an ordered pair yields its
first member. Theorem X.2.7 of [Rosser]
p. 282. (Contributed by SF,
3-Feb-2015.)
|
⊢ Proj1 〈A, B〉 = A |