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∣∃x ∈ B xAy}
Theorem	dfima3 2605	Alternate definition of image. Compare definition (d) of [Enderton] p. 44.
⊢ (A “ B) = {y∣∃x(x ∈ B ∧ ⟨x, y⟩ ∈ A)}
Theorem	elima 2606	Membership in an image. Theorem 34 of [Suppes] p. 65.
⊢ A ∈ V    ⇒   ⊢ (A ∈ (B “ C) ↔ ∃x ∈ C xBA)
Theorem	elima2 2607	Membership in an image. Theorem 34 of [Suppes] p. 65.
⊢ A ∈ V    ⇒   ⊢ (A ∈ (B “ C) ↔ ∃x(x ∈ C ∧ xBA))
Theorem	elima3 2608	Membership in an image. Theorem 34 of [Suppes] p. 65.
⊢ A ∈ V    ⇒   ⊢ (A ∈ (B “ C) ↔ ∃x(x ∈ C ∧ ⟨x, A⟩ ∈ B))
Theorem	hbima 2609	Bound-variable hypothesis builder for image.
⊢ (y ∈ A → ∀x y ∈ A)    &   ⊢ (y ∈ B → ∀x y ∈ B)    ⇒   ⊢ (y ∈ (A “ B) → ∀x y ∈ (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 ∈ C → (A “ B) ∈ 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⟩ ∈ R})
Theorem	elimasn 2617	Membership in an image of a singleton.
⊢ B ∈ V    &   ⊢ C ∈ V    ⇒   ⊢ (C ∈ (A “ {B}) ↔ ⟨B, C⟩ ∈ 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 ∈ V    ⇒   ⊢ (B ∈ D → (C ∈ (◡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 ∈ C → (◡A “ {B}) = {x∣xAB})
Theorem	dffr3 2620	Alternate definition of founded relation. Definition 6.21 of [TakeutiZaring] p. 30.
⊢ (R Fr A ↔ ∀x((x ⊆ A ∧ ¬ x = ∅) → ∃y ∈ x (x ∩ (◡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 ∈ 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 ∘ R) ⊆ R ↔ ∀x∀y∀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 ↔ ∀x∀y(xRy → yRx))
Theorem	intasym 2627	Two ways of saying a relation is antisymmetric. Definition of antisymmetry in [Schechter] p. 51.
⊢ ((R ∩ ◡R) ⊆ I ↔ ∀x∀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) = ∅ ↔ ∀x ¬ xRx)
Theorem	soirri 2629	A strict order relation is irreflexive.
⊢ A ∈ V    &   ⊢ R Or S    &   ⊢ R ⊆ (S × S)    ⇒   ⊢ ¬ ARA
Theorem	sotri 2630	A strict order relation is a transitive relation.
⊢ A ∈ V    &   ⊢ R Or S    &   ⊢ R ⊆ (S × S)    &   ⊢ B ∈ V    &   ⊢ C ∈ V    ⇒   ⊢ ((ARB ∧ BRC) → ARC)
Theorem	son2lpi 2631	A strict order relation has no 2-cycle loops.
⊢ A ∈ V    &   ⊢ R Or S    &   ⊢ R ⊆ (S × S)    &   ⊢ B ∈ V    ⇒   ⊢ ¬ (ARB ∧ BRA)
Theorem	cnvopab 2632	The converse of a class abstraction of ordered pairs.
⊢ ◡{⟨x, y⟩∣φ} = {⟨y, x⟩∣φ}
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 ∈ V    ⇒   ⊢ ∪dom {⟨A, B⟩} = A
Theorem	cnvsn 2636	Converse of a singleton of an ordered pair.
⊢ A ∈ V    &   ⊢ B ∈ 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 ∈ V    &   ⊢ B ∈ 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 ∈ V    &   ⊢ B ∈ 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 ∈ V    &   ⊢ B ∈ V    ⇒   ⊢ ∪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 ∈ (B × C) ↔ (A = ⟨∪dom {A}, ∪ran {A}⟩ ∧ (∪dom {A} ∈ B ∧ ∪ran {A} ∈ 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 ∈ (B × C) ↔ (A = ⟨∩∩A, ∪ran {A}⟩ ∧ (∩∩A ∈ B ∧ ∪ran {A} ∈ C)))
Theorem	cnvun 2642	The converse of a union is the union of converses. Theorem 16 of [Suppes] p. 62.
⊢ ◡(A ∪ B) = (◡A ∪ ◡B)
Theorem	cnvin 2643	Distributive law for converse over intersection. Theorem 15 of [Suppes] p. 62.
⊢ ◡(A ∩ B) = (◡A ∩ ◡B)
Theorem	rnun 2644	Distributive law for range over union. Theorem 8 of [Suppes] p. 60.
⊢ ran (A ∪ B) = (ran A ∪ ran B)
Theorem	rnin 2645	The range of an intersection belongs the intersection of ranges. Theorem 9 of [Suppes] p. 60.
⊢ ran (A ∩ B) ⊆ (ran A ∩ ran B)
Theorem	rnuni 2646	The range of a union. Part of Exercise 8 of [Enderton] p. 41.
⊢ ran ∪A = ∪x ∈ A ran x
Theorem	imaun 2647	Distributive law for image over union. Theorem 35 of [Suppes] p. 65.
⊢ (A “ (B ∪ C)) = ((A “ B) ∪ (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 ∩ A) ⊆ (◡R “ (R “ A))
Theorem	imainss 2649	An upper bound for intersection with an image. Theorem 41 of [Suppes] p. 66.
⊢ ((R “ A) ∩ B) ⊆ (R “ (A ∩ (◡R “ B)))
Theorem	imaiun 2650	The image of a union is the union of the images. Theorem 3K(a) of [Enderton] p. 50.
⊢ (A “ ∪B) = ∪x ∈ B (A “ x)
Theorem	cnvxp 2651	The converse of a cross product. Exercise 11 of [Suppes] p. 67.
⊢ ◡(A × B) = (B × A)
Theorem	xp0 2652	The cross product with the empty set is empty. Part of Theorem 3.13(ii) of [Monk1] p. 37.
⊢ (A × ∅) = ∅
Theorem	xpdisj1 2653	Cross products with disjoint sets are disjoint.
⊢ ((A ∩ B) = ∅ → ((A × C) ∩ (B × D)) = ∅)
Theorem	xpdisj2 2654	Cross products with disjoint sets are disjoint.
⊢ ((A ∩ B) = ∅ → ((C × A) ∩ (D × B)) = ∅)
Theorem	xpsndisj 2655	Cross products with two different singletons are disjoint.
⊢ (¬ B = D → ((A × {B}) ∩ (C × {D})) = ∅)
Theorem	resdisj 2656	A double restriction to disjoint classes is the empty set.
⊢ ((A ∩ 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 × B) = B)
Theorem	relco 2658	A composition is a relation. Exercise 24 of [TakeutiZaring] p. 25.
⊢ Rel (A ∘ 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) ∘ B) = (A ∘ 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 ∩ (V × 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 ∘ ∅) = ∅
Theorem	co01 2664	Composition with the empty set.
⊢ (∅ ∘ A) = ∅
Theorem	coi1 2665	Composition with the identity relation. Part of Theorem 3.7(i) of [Monk1] p. 36.
⊢ (Rel A → (A ∘ I) = A)
Theorem	coi2 2666	Composition with the identity relation. Part of Theorem 3.7(i) of [Monk1] p. 36.
⊢ (Rel A → (I ∘ 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 ∘ B) ∘ C) = (A ∘ (B ∘ 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 × ran A))
Theorem	cnvexg 2669	The converse of a set is a set. Corollary 6.8(1) of [TakeutiZaring] p. 26.
⊢ (A ∈ B → ◡A ∈ V)
Theorem	cnvex 2670	The converse of a set is a set. Corollary 6.8(1) of [TakeutiZaring] p. 26.
⊢ A ∈ V    ⇒   ⊢ ◡A ∈ V
Theorem	coexg 2671	The composition of two sets is a set.
⊢ ((A ∈ C ∧ B ∈ D) → (A ∘ B) ∈ V)
Theorem	coex 2672	The composition of two sets is a set.
⊢ A ∈ V    &   ⊢ B ∈ V    ⇒   ⊢ (A ∘ B) ∈ V
Theorem	dmco2 2673	The domain of a composition. Exercise 27 of [Enderton] p. 53.
⊢ dom (A ∘ B) = (◡B “ dom A)
Theorem	dffun2 2674	Alternate definition of a function.
⊢ (Fun A ↔ (Rel A ∧ ∀x∀y∀z((xAy ∧ xAz) → y = z)))
Theorem	dffun3 2675	Alternate definition of function.
⊢ (Fun A ↔ (Rel A ∧ ∀x∃z∀y(xAy → y = z)))
Theorem	dffun4 2676	Alternate definition of a function. Definition 6.4(4) of [TakeutiZaring] p. 24.
⊢ (Fun A ↔ (Rel A ∧ ∀x∀y∀z((⟨x, y⟩ ∈ A ∧ ⟨x, z⟩ ∈ A) → y = z)))
Theorem	dffun5 2677	Alternate definition of function.
⊢ (Fun A ↔ (Rel A ∧ ∀x∃z∀y(⟨x, y⟩ ∈ A → y = z)))
Theorem	dffunmof 2678	Function definition requiring only that x and y not be "free" in A (but not necessarily absent from it), using "at most one" notation.
⊢ (z ∈ A → ∀x z ∈ A)    &   ⊢ (z ∈ A → ∀y z ∈ A)    ⇒   ⊢ (Fun A ↔ (Rel A ∧ ∀x∃*y xAy))
Theorem	dffunmo 2679	Alternate definition of a function using "at most one" notation.
⊢ (Fun A ↔ (Rel A ∧ ∀x∃*y xAy))
Theorem	funmo 2680	A function has at most one value for each argument.
⊢ (Fun A → ∃*y xAy)
Theorem	funrel 2681	A function is a relation.
⊢ (Fun A → Rel A)
Theorem	funss 2682	Subclass theorem for function predicate.
⊢ (A ⊆ B → (Fun B → Fun A))
Theorem	funeq 2683	Equality theorem for function predicate.
⊢ (A = B → (Fun A ↔ Fun B))
Theorem	hbfun 2684	Bound-variable hypothesis builder for a function.
⊢ (y ∈ F → ∀x y ∈ F)    ⇒   ⊢ (Fun F → ∀xFun F)
Theorem	funeu 2685	There is exactly one value of a function.
⊢ ((Fun F ∧ xFy) → ∃!y xFy)
Theorem	funeu2 2686	There is exactly one value of a function.
⊢ ((Fun F ∧ ⟨x, y⟩ ∈ F) → ∃!y⟨x, y⟩ ∈ F)
Theorem	dffun6 2687	Alternate definition of a function. One possibility for the definition of a function in [Enderton] p. 42. (Enderton's definition is ambiguous because "there is only one" could mean either "there is at most one" or "there is exactly one". However, dffun7 2688 shows that it doesn't matter which meaning we pick.)
⊢ (Fun A ↔ (Rel A ∧ ∀x ∈ dom A∃*y xAy))
Theorem	dffun7 2688	Alternate definition of a function. One possibility for the definition of a function in [Enderton] p. 42. Compare dffun6 2687.
⊢ (Fun A ↔ (Rel A ∧ ∀x ∈ dom A∃!y xAy))
Theorem	funfn 2689	An equivalence for the function predicate.
⊢ (Fun A ↔ A Fn dom A)
Theorem	funsn 2690	A singleton of an ordered pair is a function.
⊢ A ∈ V    &   ⊢ B ∈ V    ⇒   ⊢ Fun {⟨A, B⟩}
Theorem	fun0 2691	The empty set is a function.
⊢ Fun ∅
Theorem	funi 2692	The identity relation is a function.
⊢ Fun I
Theorem	nfunv 2693	The universe is not a function. (Contributed by Raph Levien, 27-Jan-04.)
⊢ ¬ Fun V
Theorem	funopab 2694	A class of ordered pairs is a function when there is at most one second member for each pair.
⊢ (Fun {⟨x, y⟩∣φ} ↔ ∀x∃*yφ)
Theorem	funopabeq 2695	A class of ordered pairs of values is a function.
⊢ Fun {⟨x, y⟩∣y = A}
Theorem	funco 2696	The composition of two functions is a function. Exercise 29 of [TakeutiZaring] p. 25.
⊢ ((Fun F ∧ Fun G) → Fun (F ∘ G))
Theorem	funres 2697	A restriction of a function is a function. Compare Exercise 18 of [TakeutiZaring] p. 25.
⊢ (Fun F → Fun (F ↾ A))
Theorem	funssres 2698	The restriction of a function to the domain of a subclass equals the subclass.
⊢ ((Fun F ∧ G ⊆ F) → (F ↾ dom G) = G)
Theorem	fun2ssres 2699	Equality of restrictions of a function and a subclass.
⊢ (((Fun F ∧ G ⊆ F) ∧ A ⊆ dom G) → (F ↾ A) = (G ↾ A))
Theorem	funun 2700	The union of functions with disjoint domains is a function. Theorem 4.6 of [Monk1] p. 43.
⊢ (((Fun F ∧ Fun G) ∧ (dom F ∩ dom G) = ∅) → Fun (F ∪ G))