mmtheorems33 - Metamath Proof Explorer

Jump to page: Contents + 1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9500 96 9501-9600 97 9601-9700 98 9701-9800 99 9801-9900 100 9901-10000 101 10001-10100 102 10101-10200 103 10201-10300 104 10301-10400 105 10401-10500 106 10501-10600 107 10601-10700 108 10701-10800 109 10801-10900 110 10901-11000 111 11001-11100 112 11101-11200 113 11201-11300 114 11301-11400 115 11401-11500 116 11501-11600 117 11601-11700 118 11701-11800 119 11801-11900 120 11901-12000 121 12001-12100 122 12101-12200 123 12201-12229

Statement List for Metamath Proof Explorer - 3201-3300 - Page 33 of 123

Type	Label	Description
Statement
Theorem	dflim3 3201	An alternate definition of a limit ordinal, which is any ordinal that is neither zero nor a successor.
|- (Lim A <-> (Ord A /\ -. (A = (/) \/ E.x e. On A = suc x)))
Theorem	dflim4 3202	An alternate definition of a limit ordinal.
|- (Lim A <-> (Ord A /\ (/) e. A /\ A.x e. A suc x e. A))
Theorem	limsuc 3203	The successor of a member of a limit ordinal is also a member.
|- (Lim A -> (B e. A <-> suc B e. A))
Theorem	limsssuc 3204	A class includes a limit ordinal iff the successor of the class includes it.
|- (Lim A -> (A (_ B <-> A (_ suc B))
Theorem	nlimon 3205	Two ways to express the class of non-limit ordinal numbers. Part of Definition 7.27 of [TakeutiZaring] p. 42, who use the symbol KI for this class.
|- {x e. On | (x = (/) \/ E.y e. On x = suc y)} = {x e. On | -. Lim x}
Theorem	limuni3 3206	The union of a nonempty class of limit ordinals is a limit ordinal.
|- ((A =/= (/) /\ A.x e. A Lim x) -> Lim U.A)
Transfinite induction
Theorem	tfi 3207	The Principle of Transfinite Induction. Theorem 7.17 of [TakeutiZaring] p. 39. This principle states that if A is a class of ordinal numbers with the property that every ordinal number included in A also belongs to A, then every ordinal number is in A. See theorem tfindes 3215 or tfinds 3212 for the version involving basis and induction hypotheses.
|- ((A (_ On /\ A.x e. On (x (_ A -> x e. A)) -> A = On)
Theorem	tfis 3208	Transfinite Induction Schema. If all ordinal numbers less than a given number x have a property (induction hypothesis), then all ordinal numbers have the property (conclusion). Exercise 25 of [Enderton] p. 200.
|- (x e. On -> (A.y e. x [y / x]ph -> ph))   =>   |- (x e. On -> ph)
Theorem	tfis2f 3209	Transfinite Induction Schema, using implicit substitition.
|- (ps -> A.xps)   &   |- (x = y -> (ph <-> ps))   &   |- (x e. On -> (A.y e. x ps -> ph))   =>   |- (x e. On -> ph)
Theorem	tfis2 3210	Transfinite Induction Schema, using implicit substitition.
|- (x = y -> (ph <-> ps))   &   |- (x e. On -> (A.y e. x ps -> ph))   =>   |- (x e. On -> ph)
Theorem	tfis3 3211	Transfinite Induction Schema, using implicit substitition.
|- (x = y -> (ph <-> ps))   &   |- (x = A -> (ph <-> ch))   &   |- (x e. On -> (A.y e. x ps -> ph))   =>   |- (A e. On -> ch)
Theorem	tfinds 3212	Principle of Transfinite Induction (inference schema), using 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 = (/) -> (ph <-> ps))   &   |- (x = y -> (ph <-> ch))   &   |- (x = suc y -> (ph <-> th))   &   |- (x = A -> (ph <-> ta))   &   |- ps   &   |- (y e. On -> (ch -> th))   &   |- (Lim x -> (A.y e. x ch -> ph))   =>   |- (A e. On -> ta)
Theorem	tfindsg 3213	Transfinite Induction (inference schema), using implicit substititions. 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 in [TakeutiZaring] p. 57.
|- (x = B -> (ph <-> ps))   &   |- (x = y -> (ph <-> ch))   &   |- (x = suc y -> (ph <-> th))   &   |- (x = A -> (ph <-> ta))   &   |- (B e. On -> ps)   &   |- (((y e. On /\ B e. On) /\ B (_ y) -> (ch -> th))   &   |- (((Lim x /\ B e. On) /\ B (_ x) -> (A.y e. x (B (_ y -> ch) -> ph))   =>   |- (((A e. On /\ B e. On) /\ B (_ A) -> ta)
Theorem	tfindsg2 3214	Transfinite Induction (inference schema), using implicit substititions. 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 -> (ph <-> ps))   &   |- (x = y -> (ph <-> ch))   &   |- (x = suc y -> (ph <-> th))   &   |- (x = A -> (ph <-> ta))   &   |- (B e. On -> ps)   &   |- ((y e. On /\ B e. y) -> (ch -> th))   &   |- ((Lim x /\ B e. x) -> (A.y e. x (B e. y -> ch) -> ph))   =>   |- ((A e. On /\ B e. A) -> ta)
Theorem	tfindes 3215	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]ph   &   |- (x e. On -> (ph -> [suc x / x]ph))   &   |- (Lim y -> (A.x e. y ph -> [y / x]ph))   =>   |- (x e. On -> ph)
Theorem	tfinds2 3216	Transfinite Induction (inference schema), using implicit substititions. 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 ta is an auxiliary antecedent to help shorten proofs using this theorem.
|- (x = (/) -> (ph <-> ps))   &   |- (x = y -> (ph <-> ch))   &   |- (x = suc y -> (ph <-> th))   &   |- (ta -> ps)   &   |- (y e. On -> (ta -> (ch -> th)))   &   |- (Lim x -> (ta -> (A.y e. x ch -> ph)))   =>   |- (x e. On -> (ta -> ph))
Theorem	tfinds3 3217	Principle of Transfinite Induction (inference schema), using 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 = (/) -> (ph <-> ps))   &   |- (x = y -> (ph <-> ch))   &   |- (x = suc y -> (ph <-> th))   &   |- (x = A -> (ph <-> ta))   &   |- (et -> ps)   &   |- (y e. On -> (et -> (ch -> th)))   &   |- (Lim x -> (et -> (A.y e. x ch -> ph)))   =>   |- (A e. On -> (et -> ta))
The natural numbers (i.e. finite ordinals)
Syntax	com 3218	Extend class notation to include the class of natural numbers.
class om
Definition	df-om 3219	Define the class of natural numbers, which are all ordinal numbers that are less than every limit ordinal, i.e. all finite ordinals. Our definition is a variant of the Definition of N of [BellMachover] p. 471. See dfom2 3220 for an alternate definition. Later, when we assume the Axiom of Infinity, we show om is a set in omex 4772, and om can then be defined per dfom3 4776 (the smallest inductive set) and dfom4 4778. Note: the natural numbers om are a subset of the ordinal numbers df-on 2979. They are completely different from the natural numbers NN (df-n 6070) that are a subset of the complex numbers defined much later in our development, although the two sets have analogous properties and operations defined on them.
|- om = {x | (Ord x /\ A.y(Lim y -> x e. y))}
Theorem	dfom2 3220	An alternate definition of the set of natural numbers om. Definition 7.28 of [TakeutiZaring] p. 42, who use the symbol KI for the inner class builder of non-limit ordinal numbers (see nlimon 3205).
|- om = {x e. On | suc x (_ {y e. On | -. Lim y}}
Theorem	elom 3221	Membership in omega. The hypothesis can be eliminated if we assume the Axiom of Infinity; see elom3 4777.
|- A e. V   =>   |- (A e. om <-> (Ord A /\ A.x(Lim x -> A e. x)))
Theorem	elomg 3222	Membership in omega. The antecedent can be eliminated if we assume the Axiom of Infinity; see elom3 4777.
|- (A e. B -> (A e. om <-> (Ord A /\ A.x(Lim x -> A e. x))))
Theorem	omsson 3223	Omega is a subset of On.
|- om (_ On
Theorem	limomss 3224	The class of natural numbers is a subclass of any (infinite) limit ordinal. Exercise 1 of [TakeutiZaring] p. 44. Remarkably, our proof does not require the Axiom of Infinity.
|- (Lim A -> om (_ A)
Theorem	nnon 3225	A natural number is an ordinal number.
|- (A e. om -> A e. On)
Theorem	nnoni 3226	A natural number is an ordinal number.
|- A e. om   =>   |- A e. On
Theorem	nnord 3227	A natural number is ordinal.
|- (A e. om -> Ord A)
Theorem	ordom 3228	Omega is ordinal. Theorem 7.32 of [TakeutiZaring] p. 43.
|- Ord om
Theorem	elnn 3229	A member of a natural number is a natural number.
|- ((A e. B /\ B e. om) -> A e. om)
Theorem	omon 3230	The class of natural numbers om is either an ordinal number (if we accept the Axiom of Infinity) or the proper class of all ordinal numbers (if we deny the Axiom of Infinity). Remark in [TakeutiZaring] p. 43.
|- (om e. On \/ om = On)
Theorem	nnlim 3231	A natural number is not a limit ordinal.
|- (A e. om -> -. Lim A)
Theorem	omssnlim 3232	The class of natural numbers is a subclass of the class of non-limit ordinal numbers. Exercise 4 of [TakeutiZaring] p. 42.
|- om (_ {x e. On | -. Lim x}
Theorem	limom 3233	Omega is a limit ordinal. Theorem 2.8 of [BellMachover] p. 473. Our proof, however, does not require the Axiom of Infinity.
|- Lim om
Theorem	peano2b 3234	A class belongs to omega iff its successor does.
|- (A e. om <-> suc A e. om)
Theorem	nnsuc 3235	A non-zero natural number is a successor.
|- ((A e. om /\ A =/= (/)) -> E.x e. om A = suc x)
Theorem	ssnlim 3236	An ordinal subclass of non-limit ordinals is a class of natural numbers. Exercise 7 of [TakeutiZaring] p. 42.
|- ((Ord A /\ A (_ {x e. On | -. Lim x}) -> A (_ om)
Peano's postulates
Theorem	peano1 3237	Zero is a natural number. One of Peano's 5 postulates for arithmetic. Proposition 7.30(1) of [TakeutiZaring] p. 42. Note: Unlike most textbooks, our proofs of peano1 3237 through peano5 3241 do not use the Axiom of Infinity. Unlike Takeuti and Zaring, they also do not use the Axiom of Regularity.
|- (/) e. om
Theorem	peano2 3238	The successor of any natural number is a natural number. One of Peano's 5 postulates for arithmetic. Proposition 7.30(2) of [TakeutiZaring] p. 42.
|- (A e. om -> suc A e. om)
Theorem	peano3 3239	The successor of any natural number is not zero. One of Peano's 5 postulates for arithmetic. Proposition 7.30(3) of [TakeutiZaring] p. 42.
|- (A e. om -> suc A =/= (/))
Theorem	peano4 3240	Two natural numbers are equal iff their successors are equal, i.e. the successor function is one-to-one. One of Peano's 5 postulates for arithmetic. Proposition 7.30(4) of [TakeutiZaring] p. 43.
|- ((A e. om /\ B e. om) -> (suc A = suc B <-> A = B))
Theorem	peano5 3241	The induction postulate: any class containing zero and closed under the successor operation contains all natural numbers. One of Peano's 5 postulates for arithmetic. Proposition 7.30(5) of [TakeutiZaring] p. 43, except our proof does not require the Axiom of Infinity. The more traditional statement of mathematical induction as a theorem schema, with a basis and an induction hypothesis, is derived from this theorem as theorem findes 3248.
|- (((/) e. A /\ A.x e. om (x e. A -> suc x e. A)) -> om (_ A)
Theorem	nn0suc 3242	A natural number is either 0 or a successor.
|- (A e. om -> (A = (/) \/ E.x e. om A = suc x))
Finite induction (for finite ordinals)
Theorem	find 3243	The Principle of Finite Induction (mathematical induction). Corollary 7.31 of [TakeutiZaring] p. 43. The simpler hypothesis shown here was suggested in an email from "Colin" on 1-Oct-2001. The hypothesis states that A is a set of natural numbers, zero belongs to A, and given any member of A the member's successor also belongs to A. The conclusion is that every natural number is in A.
|- (A (_ om /\ (/) e. A /\ A.x e. A suc x e. A)   =>   |- A = om
Theorem	finds 3244	Principle of Finite Induction (inference schema), using implicit substitutions. The first four hypotheses establish the substitutions we need. The last two are the basis and the induction hypothesis. Theorem Schema 22 of [Suppes] p. 136.
|- (x = (/) -> (ph <-> ps))   &   |- (x = y -> (ph <-> ch))   &   |- (x = suc y -> (ph <-> th))   &   |- (x = A -> (ph <-> ta))   &   |- ps   &   |- (y e. om -> (ch -> th))   =>   |- (A e. om -> ta)
Theorem	findsg 3245	Principle of Finite Induction (inference schema), using implicit substitutions. The first four hypotheses establish the substitutions we need. The last two are the basis and the induction hypothesis. The basis of this version is an arbitrary natural number B instead of zero.
|- (x = B -> (ph <-> ps))   &   |- (x = y -> (ph <-> ch))   &   |- (x = suc y -> (ph <-> th))   &   |- (x = A -> (ph <-> ta))   &   |- (B e. om -> ps)   &   |- (((y e. om /\ B e. om) /\ B (_ y) -> (ch -> th))   =>   |- (((A e. om /\ B e. om) /\ B (_ A) -> ta)
Theorem	finds2 3246	Principle of Finite Induction (inference schema), using implicit substitutions. The first three hypotheses establish the substitutions we need. The last two are the basis and the induction hypothesis. Theorem Schema 22 of [Suppes] p. 136.
|- (x = (/) -> (ph <-> ps))   &   |- (x = y -> (ph <-> ch))   &   |- (x = suc y -> (ph <-> th))   &   |- (ta -> ps)   &   |- (y e. om -> (ta -> (ch -> th)))   =>   |- (x e. om -> (ta -> ph))
Theorem	finds1 3247	Principle of Finite Induction (inference schema), using implicit substitutions. The first three hypotheses establish the substitutions we need. The last two are the basis and the induction hypothesis. Theorem Schema 22 of [Suppes] p. 136.
|- (x = (/) -> (ph <-> ps))   &   |- (x = y -> (ph <-> ch))   &   |- (x = suc y -> (ph <-> th))   &   |- ps   &   |- (y e. om -> (ch -> th))   =>   |- (x e. om -> ph)
Theorem	findes 3248	Finite induction with explicit substitution. The first hypothesis is the basis and the second is the induction hypothesis. Theorem Schema 22 of [Suppes] p. 136. See tfindes 3215 for the transfinite version. (Contributed by Raph Levien, 9-Jul-2003.)
|- [(/) / x]ph   &   |- (x e. om -> (ph -> [suc x / x]ph))   =>   |- (x e. om -> ph)
Functions and relations
Syntax	cxp 3249	Extend the definition of a class to include the cross product.
class (A X. B)
Syntax	ccnv 3250	Extend the definition of a class to include the converse of a class.
class `'A
Syntax	cdm 3251	Extend the definition of a class to include the domain of a class.
class dom A
Syntax	crn 3252	Extend the definition of a class to include the range of a class.
class ran A
Syntax	cres 3253	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 3254	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 3255	Extend the definition of a class to include the composition of two classes. (Read: The composition of A and B.)
class (A o. B)
Syntax	wrel 3256	Extend the definition of a wff to include the relation predicate. (Read: A is a relation.)
wff Rel A
Syntax	wfun 3257	Extend the definition of a wff to include the function predicate. (Read: A is a function.)
wff Fun A
Syntax	wfn 3258	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 3259	Extend the definition of a wff to include the function predicate with domain and codomain. (Read: F maps A into B.)
wff F:A-->B
Syntax	wf1 3260	Extend the definition of a wff to include one-to-one functions. (Read: F maps A one-to-one into B.) The notation ("1-1" above the arrow) is from Definition 6.15(5) of [TakeutiZaring] p. 27.
wff F:A-1-1->B
Syntax	wfo 3261	Extend the definition of a wff to include onto functions. (Read: F maps A onto B.) The notation ("onto" below the arrow) is from Definition 6.15(4) of [TakeutiZaring] p. 27.
wff F:A-onto->B
Syntax	wf1o 3262	Extend the definition of a wff to include one-to-one onto functions. (Read: F maps A one-to-one onto B.) The notation ("1-1" above the arrow and "onto" below the arrow) is from Definition 6.15(6) of [TakeutiZaring] p. 27.
wff F:A-1-1-onto->B
Syntax	cfv 3263	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 3264	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 3265	Define the cross product of two classes. Definition 9.11 of [Quine] p. 64.
|- (A X. B) = {<.x, y>. | (x e. A /\ y e. B)}
Definition	df-rel 3266	Define a relation. Definition 6.4(1) of [TakeutiZaring] p. 23. For alternate definitions, see dfrel2 3569 and dfrel3 3587.
|- (Rel A <-> A (_ (V X. V))
Definition	df-cnv 3267	Define the converse of a class. Definition 9.12 of [Quine] p. 64. We use Quine's breve accent (smile) notation. Like Quine, we use it as a prefix, which eliminates the need for parentheses. Many authors use the postfix superscript "to the minus one." "Converse" is Quine's terminology; some authors call it "inverse," especially when the argument is a function.
|- `'A = {<.x, y>. | yAx}
Definition	df-co 3268	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 o., and calls the operation "relative product."
|- (A o. B) = {<.x, y>. | E.z(xBz /\ zAy)}
Definition	df-dm 3269	Define the domain of a class. Definition 3 of [Suppes] p. 59.
|- dom A = {x | E.y xAy}
Definition	df-rn 3270	Define the range of a class. For an alternate definitions, see dfrn2 3394, dfrn3 3395, and dfrn4 3590.
|- ran A = dom `' A
Definition	df-res 3271	Define the restriction of a class. Definition 6.6(1) of [TakeutiZaring] p. 24.
|- (A |` B) = (A i^i (B X. V))
Definition	df-ima 3272	Define the image of a class. Definition 6.6(2) of [TakeutiZaring] p. 24. For an alternate definition, see dfima2 3497.
|- (A"B) = ran ( A |` B)
Definition	df-fun 3273	Define a function. Definition 10.1 of [Quine] p. 65. For alternate definitions, see dffun2 3631, dffun3 3632, dffun4 3633, dffun5 3634, dffun6 3636, dffun7 3644, dffun8 3645, and dffun9 3646.
|- (Fun A <-> (Rel A /\ (A o. `'A) (_ I))
Definition	df-fn 3274	Define a function with domain. Definition 6.15(1) of [TakeutiZaring] p. 27. For alternate definitions, see dffn2 3735, dffn3 3741, dffn4 3785, and dffn5 3869.
|- (A Fn B <-> (Fun A /\ dom A = B))
Definition	df-f 3275	Define a function (mapping) with domain and codomain. Definition 6.15(3) of [TakeutiZaring] p. 27. For alternate definitions, see dff2 3930, dff3 3931, and dff4 3932.
|- (F:A-->B <-> (F Fn A /\ ran F (_ B))
Definition	df-f1 3276	Define a one-to-one function. For equivalent definitions see dff12 3771 and dff13 3988. Compare Definition 6.15(5) of [TakeutiZaring] p. 27. We use their notation ("1-1" above the arrow).
|- (F:A-1-1->B <-> (F:A-->B /\ Fun `'F))
Definition	df-fo 3277	Define an onto function. Definition 6.15(4) of [TakeutiZaring] p. 27. We use their notation ("onto" under the arrow). For alternate definitions, see dffo2 3783, dffo3 3933, dffo4 3934, and dffo5 3935.
|- (F:A-onto->B <-> (F Fn A /\ ran F = B))
Definition	df-f1o 3278	Define a one-to-one onto function. For equivalent definitions see dff1o2 3801, dff1o3 3802, dff1o4 3804, and dff1o5 3805. Compare Definition 6.15(6) of [TakeutiZaring] p. 27. We use their notation ("1-1" above the arrow and "onto" below the arrow).
|- (F:A-1-1-onto->B <-> (F:A-1-1->B /\ F:A-onto->B))
Definition	df-fv 3279	Define the value of a function. Although based on the idea embodied by Definition 10.2 of [Quine] p. 65 (see args 3520), our definition apparently does not appear in the literature; but it is quite convenient: it can be applied to any class and evaluates to the empty set when it is not meaningful (as shown by ndmfv 3856 and fvprc 3832). The left apostrophe notation originated with Peano and was adopted in Definition *30.01 of [WhiteheadRussell] p. 235, Definition 10.11 of [Quine] p. 68, and Definition 6.11 of [TakeutiZaring] p. 26. It 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 conventional alternate definitions (that fail to evaluate to the empty set for proper classes), see fv2 3831 and fv3 3844. Restricted equivalents that require F to be a function are shown in funfv 3881 and funfv2 3882. For the familiar definition of function value in terms of ordered pair membership, see funopfvb 3867.
|- (F` A) = U.{x | (F"{A}) = {x}}
Definition	df-iso 3280	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 /\ A.x e. A A.y e. A (xRy <-> (H` x)S(H` y))))
Theorem	xpeq1 3281	Equality theorem for cross product.
|- (A = B -> (A X. C) = (B X. C))
Theorem	xpeq2 3282	Equality theorem for cross product.
|- (A = B -> (C X. A) = (C X. B))
Theorem	elxp 3283	Membership in a cross product.
|- (A e. (B X. C) <-> E.xE.y(A = <.x, y>. /\ (x e. B /\ y e. C)))
Theorem	elxp2 3284	Membership in a cross product.
|- (A e. (B X. C) <-> E.x e. B E.y e. C A = <.x, y>.)
Theorem	xpeq1i 3285	Equality theorem for cross product.
|- A = B   =>   |- (A X. C) = (B X. C)
Theorem	xpeq2i 3286	Equality theorem for cross product.
|- A = B   =>   |- (C X. A) = (C X. B)
Theorem	hbxp 3287	Bound-variable hypothesis builder for cross product.
|- (y e. A -> A.x y e. A)   &   |- (y e. B -> A.x y e. B)   =>   |- (y e. (A X. B) -> A.x y e. (A X. B))
Theorem	opelxp1 3288	The first member of an ordered pair of classes in a cross product belongs to first cross product argument.
|- (<.A, B>. e. (C X. D) -> A e. C)
Theorem	otelxp1 3289	The first member of an ordered triple of classes in a cross product belongs to first cross product argument.
|- (<.<.A, B>., C>. e. ((R X. S) X. T) -> A e. R)
Theorem	brrelex 3290	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 e. V)
Theorem	brrelexi 3291	The first argument of a binary relation exists. (An artifact of our ordered pair definition.)
|- Rel R   =>   |- (ARB -> A e. V)
Theorem	nprrel 3292	No proper class is related to anything via any relation. (Contributed by Roy F. Longton, 30-Jul-2005.)
|- Rel R   &   |- -. A e. V   =>   |- -. ARB
Theorem	fconstopab 3293	Representation of a constant function using ordered pairs.
|- (A X. {B}) = {<.x, y>. | (x e. A /\ y = B)}
Theorem	vtoclr 3294	Variable to class conversion of transitive relation.
|- Rel R   &   |- ((xRy /\ yRz) -> xRz)   =>   |- (C e. D -> ((ARB /\ BRC) -> ARC))
Theorem	vtoclrbr 3295	Variable to class conversion of transitive, reflexive relation.
|- Rel R   &   |- ((xRy /\ yRz) -> xRz)   &   |- xRx   =>   |- ((ARB /\ BRC) -> ARC)
Theorem	vtoclibr 3296	Variable to class conversion of transitive, irreflexive relation.
|- Rel R   &   |- ((xRy /\ yRz) -> xRz)   &   |- -. xRx   =>   |- ((ARB /\ BRC) -> ARC)
Theorem	opelxp 3297	Ordered pair membership in a cross product.
|- B e. V   =>   |- (<.A, B>. e. (C X. D) <-> (A e. C /\ B e. D))
Theorem	brxp 3298	Binary relation on a cross product.
|- B e. V   =>   |- (A(C X. D)B <-> (A e. C /\ B e. D))
Theorem	opelxpg 3299	Ordered pair membership in a cross product.
|- (B e. R -> (<.A, B>. e. (C X. D) <-> (A e. C /\ B e. D)))
Theorem	opelxpi 3300	Ordered pair membership in a cross product (implication).
|- ((A e. C /\ B e. D) -> <.A, B>. e. (C X. D))