Metamath Proof Explorer - mmtheorems27

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 - 2601-2700 - Page 27 of 58

Type	Label	Description
Statement
Theorem	resid 2601	Any relation restricted to the universe is itself.
|- (Rel A -> (A |` V) = A)
Theorem	imaeq1 2602	Equality theorem for image.
|- (A = B -> (A"C) = (B"C))
Theorem	imaeq2 2603	Equality theorem for image.
|- (A = B -> (C"A) = (C"B))
Theorem	dfima2 2604	Alternate definition of image. Compare definition (d) of [Enderton] p. 44.
|- (A"B) = {y | E.x e. B xAy}
Theorem	dfima3 2605	Alternate definition of image. Compare definition (d) of [Enderton] p. 44.
|- (A"B) = {y | E.x(x e. B /\ <.x, y>. e. A)}
Theorem	elima 2606	Membership in an image. Theorem 34 of [Suppes] p. 65.
|- A e. V   =>   |- (A e. (B"C) <-> E.x e. C xBA)
Theorem	elima2 2607	Membership in an image. Theorem 34 of [Suppes] p. 65.
|- A e. V   =>   |- (A e. (B"C) <-> E.x(x e. C /\ xBA))
Theorem	elima3 2608	Membership in an image. Theorem 34 of [Suppes] p. 65.
|- A e. V   =>   |- (A e. (B"C) <-> E.x(x e. C /\ <.x, A>. e. B))
Theorem	hbima 2609	Bound-variable hypothesis builder for image.
|- (y e. A -> A.x y e. A)   &   |- (y e. B -> A.x y e. B)   =>   |- (y e. (A"B) -> A.x y e. (A"B))
Theorem	imadmrn 2610	The image of the domain of a class is the range of the class.
|- (A"dom A) = ran A
Theorem	imassrn 2611	The image of a class is a subset of its range. Theorem 3.16(xi) of [Monk1] p. 39.
|- (A"B) (_ ran A
Theorem	imaexg 2612	The image of a set is a set. Theorem 3.17 of [Monk1] p. 39.
|- (A e. C -> (A"B) e. V)
Theorem	imai 2613	Image under the identity relation. Theorem 3.16(viii) of [Monk1] p. 38.
|- (I"A) = A
Theorem	rnresi 2614	The range of the restricted identity function.
|- ran (I |` A) = A
Theorem	ima0 2615	Image of the empty set. Theorem 3.16(ii) of [Monk1] p. 38.
|- (A"(/)) = (/)
Theorem	imasn 2616	Image of a singleton.
|- (Rel R -> (R"{A}) = {y | <.A, y>. e. R})
Theorem	elimasn 2617	Membership in an image of a singleton.
|- B e. V   &   |- C e. V   =>   |- (C e. (A"{B}) <-> <.B, C>. e. A)
Theorem	eliniseg 2618	Membership in an initial segment. The idiom (`'A"{B}), meaning {x | xAB}, is used to specify an initial segment in (for example) Definition 6.21 of [TakeutiZaring] p. 30.
|- C e. V   =>   |- (B e. D -> (C e. (`'A"{B}) <-> CAB))
Theorem	iniseg 2619	An idiom that signifies an initial segment of an ordering, used, for example, in Definition 6.21 of [TakeutiZaring] p. 30.
|- (B e. C -> (`'A"{B}) = {x | xAB})
Theorem	dffr3 2620	Alternate definition of founded relation. Definition 6.21 of [TakeutiZaring] p. 30.
|- (R Fr A <-> A.x((x (_ A /\ -. x = (/)) -> E.y e. x (x i^i (`'R"{y})) = (/)))
Theorem	imass1 2621	Subset theorem for image.
|- (A (_ B -> (A"C) (_ (B"C))
Theorem	imass2 2622	Subset theorem for image. Exercise 22(a) of [Enderton] p. 53.
|- (A (_ B -> (C"A) (_ (C"B))
Theorem	ndmima 2623	The image of a singleton outside the domain is empty.
|- (-. A e. dom B -> (B"{A}) = (/))
Theorem	relcnv 2624	A converse is a relation. Theorem 12 of [Suppes] p. 62.
|- Rel `'A
Theorem	cotr 2625	Two ways of saying a relation is transitive. Definition of transitivity in [Schechter] p. 51.
|- ((R o. R) (_ R <-> A.xA.yA.z((xRy /\ yRz) -> xRz))
Theorem	cnvsym 2626	Two ways of saying a relation is symmetric. Similar to definition of symmetry in [Schechter] p. 51.
|- (`'R (_ R <-> A.xA.y(xRy -> yRx))
Theorem	intasym 2627	Two ways of saying a relation is antisymmetric. Definition of antisymmetry in [Schechter] p. 51.
|- ((R i^i `'R) (_ I <-> A.xA.y((xRy /\ yRx) -> x = y))
Theorem	intirr 2628	Two ways of saying a relation is irreflexive. Definition of irreflexivity in [Schechter] p. 51.
|- ((R i^i I) = (/) <-> A.x -. xRx)
Theorem	soirri 2629	A strict order relation is irreflexive.
|- A e. V   &   |- R Or S   &   |- R (_ (S X. S)   =>   |- -. ARA
Theorem	sotri 2630	A strict order relation is a transitive relation.
|- A e. V   &   |- R Or S   &   |- R (_ (S X. S)   &   |- B e. V   &   |- C e. V   =>   |- ((ARB /\ BRC) -> ARC)
Theorem	son2lpi 2631	A strict order relation has no 2-cycle loops.
|- A e. V   &   |- R Or S   &   |- R (_ (S X. S)   &   |- B e. V   =>   |- -. (ARB /\ BRA)
Theorem	cnvopab 2632	The converse of a class abstraction of ordered pairs.
|- `'{<.x, y>. | ph} = {<.y, x>. | ph}
Theorem	cnv0 2633	The converse of the empty set.
|- `'(/) = (/)
Theorem	cnvi 2634	The converse of the identity relation. Theorem 3.7(ii) of [Monk1] p. 36.
|- `'I = I
Theorem	op1sta 2635	Extract the first member of an ordered pair. (See op2nda 2639 to extract the second member and op1stb 1992 for an alternate version.) (Contributed by Raph Levien, 4-Dec-03.)
|- A e. V   =>   |- U.dom {<.A, B>.} = A
Theorem	cnvsn 2636	Converse of a singleton of an ordered pair.
|- A e. V   &   |- B e. V   =>   |- `'{<.A, B>.} = {<.B, A>.}
Theorem	rnsnop 2637	The range of a singleton of an ordered pair is the singleton of the second member.
|- A e. V   &   |- B e. V   =>   |- ran {<.A, B>.} = {B}
Theorem	op2ndb 2638	Extract the second member of an ordered pair. Theorem 5.12(ii) of [Monk1] p. 52. (See op1stb 1992 to extract the first member and op2nda 2639 for an alternate version.)
|- A e. V   &   |- B e. V   =>   |- |^||^||^|`'{<.A, B>.} = B
Theorem	op2nda 2639	Extract the second member of an ordered pair. (See op1sta 2635 to extract the first member and op2ndb 2638 for an alternate version.)
|- A e. V   &   |- B e. V   =>   |- U.ran {<.A, B>.} = B
Theorem	elxp4 2640	Membership in a cross product. This version requires no quantifiers or dummy variables. See also elxp5 2641 and elxp6 3093.
|- (A e. (B X. C) <-> (A = <.U.dom {A}, U.ran {A}>. /\ (U.dom {A} e. B /\ U.ran {A} e. C)))
Theorem	elxp5 2641	Membership in a cross product requiring no quantifiers or dummy variables. Provides a slightly shorter version of elxp4 2640 when the double intersection does not create class existence problems (caused by int0 1978).
|- (A e. (B X. C) <-> (A = <.|^||^|A, U.ran {A}>. /\ (|^||^|A e. B /\ U.ran {A} e. C)))
Theorem	cnvun 2642	The converse of a union is the union of converses. Theorem 16 of [Suppes] p. 62.
|- `'(A u. B) = (`'A u. `'B)
Theorem	cnvin 2643	Distributive law for converse over intersection. Theorem 15 of [Suppes] p. 62.
|- `'(A i^i B) = (`'A i^i `'B)
Theorem	rnun 2644	Distributive law for range over union. Theorem 8 of [Suppes] p. 60.
|- ran (A u. B) = (ran A u. ran B)
Theorem	rnin 2645	The range of an intersection belongs the intersection of ranges. Theorem 9 of [Suppes] p. 60.
|- ran (A i^i B) (_ (ran A i^i ran B)
Theorem	rnuni 2646	The range of a union. Part of Exercise 8 of [Enderton] p. 41.
|- ran U.A = U.x e. A ran x
Theorem	imaun 2647	Distributive law for image over union. Theorem 35 of [Suppes] p. 65.
|- (A"(B u. C)) = ((A"B) u. (A"C))
Theorem	dminss 2648	An upper bound for intersection with a domain. Theorem 40 of [Suppes] p. 66, who calls it "somewhat surprising."
|- (dom R i^i A) (_ (`'R"(R"A))
Theorem	imainss 2649	An upper bound for intersection with an image. Theorem 41 of [Suppes] p. 66.
|- ((R"A) i^i B) (_ (R"(A i^i (`'R"B)))
Theorem	imaiun 2650	The image of a union is the union of the images. Theorem 3K(a) of [Enderton] p. 50.
|- (A"U.B) = U.x e. B (A"x)
Theorem	cnvxp 2651	The converse of a cross product. Exercise 11 of [Suppes] p. 67.
|- `'(A X. B) = (B X. A)
Theorem	xp0 2652	The cross product with the empty set is empty. Part of Theorem 3.13(ii) of [Monk1] p. 37.
|- (A X. (/)) = (/)
Theorem	xpdisj1 2653	Cross products with disjoint sets are disjoint.
|- ((A i^i B) = (/) -> ((A X. C) i^i (B X. D)) = (/))
Theorem	xpdisj2 2654	Cross products with disjoint sets are disjoint.
|- ((A i^i B) = (/) -> ((C X. A) i^i (D X. B)) = (/))
Theorem	xpsndisj 2655	Cross products with two different singletons are disjoint.
|- (-. B = D -> ((A X. {B}) i^i (C X. {D})) = (/))
Theorem	resdisj 2656	A double restriction to disjoint classes is the empty set.
|- ((A i^i B) = (/) -> ((C |` A) |` B) = (/))
Theorem	rnxp 2657	The range of a cross product. Part of Theorem 3.13(x) of [Monk1] p. 37.
|- (-. A = (/) -> ran (A X. B) = B)
Theorem	relco 2658	A composition is a relation. Exercise 24 of [TakeutiZaring] p. 25.
|- Rel (A o. B)
Theorem	cores 2659	The first member of a composition may be restricted down to the range of the second without affecting the result.
|- (ran B (_ C -> ((A |` C) o. B) = (A o. B))
Theorem	dfrel2 2660	Alternate definition of relation. Exercise 2 of [TakeutiZaring] p. 25.
|- (Rel R <-> `'`'R = R)
Theorem	cnvcnv 2661	The double converse of a class strips out all elements that are not ordered pairs.
|- `'`'A = (A i^i (V X. V))
Theorem	cnvcnvss 2662	The double converse of a class is a subclass. Exercise 2 of [TakeutiZaring] p. 25.
|- `'`'A (_ A
Theorem	co02 2663	Composition with the empty set. Theorem 20 of [Suppes] p. 63.
|- (A o. (/)) = (/)
Theorem	co01 2664	Composition with the empty set.
|- ((/) o. A) = (/)
Theorem	coi1 2665	Composition with the identity relation. Part of Theorem 3.7(i) of [Monk1] p. 36.
|- (Rel A -> (A o. I) = A)
Theorem	coi2 2666	Composition with the identity relation. Part of Theorem 3.7(i) of [Monk1] p. 36.
|- (Rel A -> (I o. A) = A)
Theorem	coass 2667	Associative law for class composition. Theorem 27 of [Suppes] p. 64. Also Exercise 21 of [Enderton] p. 53. Interestingly, this law holds for any classes whatsoever, not just functions or even relations.
|- ((A o. B) o. C) = (A o. (B o. C))
Theorem	relssdr 2668	A relation is included in the cross product of its domain and range. Exercise 4.12(t) of [Mendelson] p. 235.
|- (Rel A -> A (_ (dom A X. ran A))
Theorem	cnvexg 2669	The converse of a set is a set. Corollary 6.8(1) of [TakeutiZaring] p. 26.
|- (A e. B -> `'A e. V)
Theorem	cnvex 2670	The converse of a set is a set. Corollary 6.8(1) of [TakeutiZaring] p. 26.
|- A e. V   =>   |- `'A e. V
Theorem	coexg 2671	The composition of two sets is a set.
|- ((A e. C /\ B e. D) -> (A o. B) e. V)
Theorem	coex 2672	The composition of two sets is a set.
|- A e. V   &   |- B e. V   =>   |- (A o. B) e. V
Theorem	dmco2 2673	The domain of a composition. Exercise 27 of [Enderton] p. 53.
|- dom (A o. B) = (`'B"dom A)
Theorem	dffun2 2674	Alternate definition of a function.
|- (Fun A <-> (Rel A /\ A.xA.yA.z((xAy /\ xAz) -> y = z)))
Theorem	dffun3 2675	Alternate definition of function.
|- (Fun A <-> (Rel A /\ A.xE.zA.y(xAy -> y = z)))
Theorem	dffun4 2676	Alternate definition of a function. Definition 6.4(4) of [TakeutiZaring] p. 24.
|- (Fun A <-> (Rel A /\ A.xA.yA.z((<.x, y>. e. A /\