Metamath Proof Explorer - mmtheorems25

Jump to page: 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-5787

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 = (/) -> (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 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 -> (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 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 -> (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 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]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 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 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 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 = (/) -> (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 ))
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 e. On | -. Lim x}) -> A (_ om)
Syntax	cxp 2408	Extend the definition of a class to include the cross product.
class (A X. 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 o. 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 X. B) = {<.x, y>. | (x e. A /\ y e. 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 X. 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 o., and calls the operation "relative product."
|- (A o. B) = {<.x, y>. | E.z(xBz /\ zAy)}
Definition	df-dm 2428	Define the domain of a class. Definition 3 of [Suppes] p. 59.
|- dom A = {x | E.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 i^i (B X. 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 o. `'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) = U.{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 /\ A.x e. A A.y e. A (xRy <-> (H` x)S(H` y))))
Theorem	xpeq1 2440	Equality theorem for cross product.
|- (A = B -> (A X. C) = (B X. C))
Theorem	xpeq2 2441	Equality theorem for cross product.
|- (A = B -> (C X. A) = (C X. B))
Theorem	elxp 2442	Membership in a cross product.
|- (A e. (B X. C) <-> E.xE.y(A = <.x, y>. /\ (x e. B /\ y e. C)))
Theorem	elxp2 2443	Membership in a cross product.
|- (A e. (B X. C) <-> E.x e. B E.y e. C A = <.x, y>.)
Theorem	hbxp 2444	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	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>. e. (C X. D) -> A e. 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 e. V)
Theorem	brrelexi 2447	The first argument of a binary relation exists. (An artifact of our ordered pair definition.)
|- Rel R   =>   |- (ARB -> A e. V)
Theorem	fconstopab 2448	Representation of a constant function using ordered pairs.
|- (A X. {B}) = {<.x, y>. | (x e. A /\ y = B)}
Theorem	vtoclr 2449	Variable to class conversion of transitive relation.
|- Rel R   &   |- ((xRy /\ yRz) -> xRz)   =>   |- (C e. 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 e. V   =>   |- (<.A, B>. e. (C X. D) <-> (A e. C /\ B e. D))
Theorem	brxp 2453	Binary relation on a cross product.
|- B e. V   =>   |- (A(C X. D)B <-> (A e. C /\ B e. D))
Theorem	opelxpg 2454	Ordered pair membership in a cross product.
|- (B e. R -> (<.A, B>. e. (C X. D) <-> (A e. C /\ B e. D)))
Theorem	opelxpi 2455	Ordered pair membership in a cross product (implication).
|- ((A e. C /\ B e. D) -> <.A, B>. e. (C X. 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>. -> (ph <-> ps