Metamath Proof Explorer - mmtheorems30

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 - 2901-3000 - Page 30 of 58

Type	Label	Description
Statement
Theorem	fvresi 2901	The value of a restricted identity function.
|- (B e. A -> ((I |` A)` B) = B)
Theorem	fconst2 2902	A constant function expressed as a cross product. See also fconstfv 2903.
|- B e. V   =>   |- (F:A-->{B} <-> F = (A X. {B}))
Theorem	fconstfv 2903	A constant function expressed in terms of its functionality, domain, and value. See also fconst2 2902.
|- (F:A-->{B} <-> (F Fn A /\ A.x e. A (F` x) = B))
Theorem	funfvima 2904	A function's value in a pre-image belongs to the image.
|- ((Fun F /\ B e. dom F) -> (B e. A -> (F` B) e. (F"A)))
Theorem	funfvima2 2905	A function's value in an included pre-image belongs to the image.
|- ((Fun F /\ A (_ dom F) -> (B e. A -> (F` B) e. (F"A)))
Theorem	funfvima3 2906	A class including a function contains the function's value in the image of the singleton of the argument.
|- ((Fun F /\ F (_ G) -> (A e. dom F -> (F` A) e. (G"{A})))
Theorem	fvclss 2907	Upper bound for the class of values of a class.
|- {y | E.x y = (F` x)} (_ (ran F u. {(/)})
Theorem	fvclex 2908	Existence of the class of values of a set.
|- F e. V   =>   |- {y | E.x y = (F` x)} e. V
Theorem	fvresex 2909	Existence of the class of values of a restricted class.
|- A e. V   =>   |- {y | E.x y = ((F |` A)` x)} e. V
Theorem	abrexexlem1 2910	Lemma for abrexex 2912. Shows the existence of a class of existentially restricted function values.
|- A e. V   =>   |- {y | E.x e. A y = (F` x)} e. V
Theorem	abrexexlem2 2911	Lemma for abrexex 2912. Almost there, but still requires that B be a set.
|- A e. V   &   |- B e. V   =>   |- {y | E.x e. A y = B} e. V
Theorem	abrexex 2912	Existence of a class abstraction of existentially restricted sets. x is normally a free-variable parameter in B. This simple-looking theorem is actually quite powerful and involves the Axiom of Replacement in an intrinsic way, as can be seen by tracing back through the path abrexexlem2 2911, abrexexlem1 2910, fvresex 2909, resfunexg 2717, and funimaexg 2715. See also abrexex2 2915.
|- A e. V   =>   |- {y | E.x e. A y = B} e. V
Theorem	abrexexg 2913	Existence of a class abstraction of existentially restricted sets. x is normally a free-variable parameter in B. The antecedent assures us that A is a set.
|- (A e. C -> {y | E.x e. A y = B} e. V)
Theorem	iunex 2914	The existence of an indexed union. x is normally a free-variable parameter in B.
|- A e. V   &   |- B e. V   =>   |- U.x e. A B e. V
Theorem	abrexex2 2915	Existence of an existentially restricted class abstraction. ph is normally has free-variable parameters x and y. This is a powerful generalization of abrexex 2912.
|- A e. V   &   |- {y | ph} e. V   =>   |- {y | E.x e. A ph} e. V
Theorem	f1fv 2916	A one-to-one function in terms of function values. Compare Theorem 4.8(iv) of [Monk1] p. 43.
|- (F:A-1-1->B <-> (F:A-->B /\ A.x e. A A.y e. A ((F` x) = (F` y) -> x = y)))
Theorem	f1fvf 2917	A one-to-one function in terms of function values. Compare Theorem 4.8(iv) of [Monk1] p. 43.
|- (z e. F -> A.x z e. F)   &   |- (z e. F -> A.y z e. F)   =>   |- (F:A-1-1->B <-> (F:A-->B /\ A.x e. A A.y e. A ((F` x) = (F` y) -> x = y)))
Theorem	f1fveq 2918	Equality of function values for a one-to-one function.
|- ((F:A-1-1->B /\ (C e. A /\ D e. A)) -> ((F` C) = (F` D) <-> C = D))
Theorem	f1ocnvfv1 2919	The converse value of the value of a one-to-one onto function.
|- ((F:A-1-1-onto->B /\ C e. A) -> (`'F` (F` C)) = C)
Theorem	f1ocnvfv2 2920	The value of the converse value of a one-to-one onto function.
|- ((F:A-1-1-onto->B /\ C e. B) -> (F` (`'F` C)) = C)
Theorem	f1ocnvfv 2921	Relationship between the value of a one-to-one onto function and the value of its converse. (Contributed by Raph Levien, 10-Apr-04.)
|- ((F:A-1-1-onto->B /\ C e. A) -> ((F` C) = D -> (`'F` D) = C))
Theorem	f1ocnvfvb 2922	Relationship between the value of a one-to-one onto function and the value of its converse. (Contributed by Raph Levien, 10-Apr-04.)
|- ((F:A-1-1-onto->B /\ (C e. A /\ D e. B)) -> ((F` C) = D <-> (`'F` D) = C))
Theorem	cbvfo 2923	Change bound variable between domain and range of function.
|- ((F` x) = y -> (ph <-> ps))   =>   |- (F:A-onto->B -> (A.x e. A ph <-> A.y e. B ps))
Theorem	cbvexfo 2924	Change bound variable between domain and range of function.
|- ((F` x) = y -> (ph <-> ps))   =>   |- (F:A-onto->B -> (E.x e. A ph <-> E.y e. B ps))
Theorem	isoeq1 2925	Equality theorem for isomorphisms.
|- (H = G -> (H Isom R, S (A, B) <-> G Isom R, S (A, B)))
Theorem	isoeq2 2926	Equality theorem for isomorphisms.
|- (R = T -> (H Isom R, S (A, B) <-> H Isom T, S (A, B)))
Theorem	isoeq3 2927	Equality theorem for isomorphisms.
|- (S = T -> (H Isom R, S (A, B) <-> H Isom R, T (A, B)))
Theorem	isoeq4 2928	Equality theorem for isomorphisms.
|- (A = C -> (H Isom R, S (A, B) <-> H Isom R, S (C, B)))
Theorem	isoeq5 2929	Equality theorem for isomorphisms.
|- (B = C -> (H Isom R, S (A, B) <-> H Isom R, S (A, C)))
Theorem	hbiso 2930	Bound-variable hypothesis builder for an isomorphism.
|- (y e. H -> A.x y e. H)   &   |- (y e. R -> A.x y e. R)   &   |- (y e. S -> A.x y e. S)   &   |- (y e. A -> A.x y e. A)   &   |- (y e. B -> A.x y e. B)   =>   |- (H Isom R, S (A, B) -> A.x H Isom R, S (A, B))
Theorem	isof1o 2931	An isomorphism is a one-to-one onto function.
|- (H Isom R, S (A, B) -> H:A-1-1-onto->B)
Theorem	isorel 2932	An isomorphism connects binary relations via its function values.
|- ((H Isom R, S (A, B) /\ (C e. A /\ D e. A)) -> (CRD <-> (H` C)S(H` D)))
Theorem	isoid 2933	Identity law for isomorphism. Proposition 6.30(1) of [TakeutiZaring] p. 33.
|- (I |` A) Isom R, R (A, A)
Theorem	isocnv 2934	Converse law for isomorphism. Proposition 6.30(2) of [TakeutiZaring] p. 33.
|- (H Isom R, S (A, B) -> `'H Isom S, R (B, A))
Theorem	isotr 2935	Composition (transitive) law for isomorphism. Proposition 6.30(3) of [TakeutiZaring] p. 33.
|- ((H Isom R, S (A, B) /\ G Isom S, T (B, C)) -> (G o. H) Isom R, T (A, C))
Theorem	isotrALT 2936	Composition (transitive) law for isomorphism. Proposition 6.30(3) of [TakeutiZaring] p. 33. This proof is shorter than isotr 2935 in set.mm and uses fewer dummy variables, but it takes 240K vs. 207K for the web page.
|- ((H Isom R, S (A, B) /\ G Isom S, T (B, C)) -> (G o. H) Isom R, T (A, C))
Theorem	isomin 2937	Isomorphisms preserve minimal elements. Note that (`'R"{D}) is Takeuti and Zaring's idiom for the initial segment {x | xRD}. Proposition 6.31(1) of [TakeutiZaring] p. 33.
|- ((H Isom R, S (A, B) /\ (C (_ A /\ D e. A)) -> ((C i^i (`'R"{D})) = (/) <-> ((H"C) i^i (`'S"{(H` D)})) = (/)))
Theorem	isoini 2938	Isomorphisms preserve initial segments. Proposition 6.31(2) of [TakeutiZaring] p. 33.
|- ((H Isom R, S (A, B) /\ D e. A) -> (H"(A i^i (`'R"{D}))) = (B i^i (`'S"{(H` D)})))
Theorem	isofrlem 2939	Lemma for isofr 2940.
|- (H Isom R, S (A, B) -> (S Fr B -> R Fr A))
Theorem	isofr 2940	An isomorphism preserves foundedness. Proposition 6.32(1) of [TakeutiZaring] p. 33.
|- (H Isom R, S (A, B) -> (R Fr A <-> S Fr B))
Theorem	isowe 2941	An isomorphism preserves well ordering. Proposition 6.32(3) of [TakeutiZaring] p. 33.
|- (H Isom R, S (A, B) -> (R We A <-> S We B))
Theorem	f1oiso 2942	Any one-to-one onto function determines an isomorphism with an induced relation S. Proposition 6.33 of [TakeutiZaring] p. 34.
|- ((H:A-1-1-onto->B /\ S = {<.z, w>. | E.x e. A E.y e. A ((z = (H` x) /\ w = (H` y)) /\ xRy)}) -> H Isom R, S (A, B))
Theorem	f1owe 2943	Well-ordering of isomorphic relations.
|- R = {<.x, y>. | (F` x)S(F` y)}   =>   |- (F:A-1-1-onto->B -> (S We B -> R We A))
Theorem	f1oweOLD 2944	Well-ordering of isomorphic relations.
|- R = {<.x, y>. | (F` x)S(F` y)}   =>   |- (F:A-1-1-onto->B -> (S We B -> R We A))
Theorem	canth 2945	No set A is equinumerous to its power set (Cantor's theorem), i.e. no function can map A it onto its power set. Compare Theorem 6B(b) of [Enderton] p. 132. For the equinumerosity version, see canth2 3381. Note that A must be a set: this theorem does not hold when A is too large to be a set; see ncanth 2946 for a counterexample.
|- A e. V   =>   |- -. F:A-onto->P~A
Theorem	ncanth 2946	Cantor's theorem fails for the universal class (which is not a set but a proper class by nvelv 1483). Specifically, the identity function maps the universe onto its power class. Compare canth 2945 that works for sets. See also the remark in ru 1437 about NF, in which Cantor's theorem fails for sets that are "too large." This theorem gives some intuition behind that failure, since in NF the universal class is a set.
|- I:V-onto->P~V
Theorem	iunon 2947	The indexed union of a set of ordinal numbers is an ordinal number. B normally has free variable x as a parameter.
|- A e. V   &   |- B e. V   =>   |- (A.x e. A B e. On -> U.x e. A B e. On)
Theorem	iinon 2948	The indexed intersection of a non-empty class of ordinal numbers is an ordinal number. B normally has free variable x as a parameter. Note that A may be a proper class.
|- B e. V   =>   |- ((A.x e. A B e. On /\ -. A = (/)) -> |^|x e. A B e. On)
Theorem	tfrlem1 2949	A technical lemma for transfinite recursion. Compare Lemma 1 of [TakeutiZaring] p. 47.
|- (A e. On -> ((F Fn A /\ G Fn A) -> (A.x e. A ((F` x) = (B` (F |` x)) /\ (G` x) = (B` (G |` x))) -> A.x e. A (F` x) = (G` x))))
Theorem	tfrlem2 2950	Lemma for transfinite recursion. This provides some messy details needed to link tfrlem1 2949 into the main proof.
|- ((F Fn A /\ G Fn A) -> ((<.x, y>. e. F