mmtheorems105 - 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-10688

Statement List for Metamath Proof Explorer - 10401-10500 - Page 105 of 107

Type	Label	Description
Statement
Theorem	intn3an3d 10401	Introduction of a conjunct inside a contradiction.
|- (ph -> -. ps)   =>   |- (ph -> -. (ch /\ th /\ ps))
Theorem	rcla4devOLD 10402	Restricted existential specialization with implicit substitution.
|- ((ph /\ x = A) -> (ps <-> ch))   =>   |- ((ph /\ A e. B) -> (ps -> E.x e. B ch))
Theorem	and4as 10403	/\ associativity.
|- ((ph /\ ps /\ (ch /\ th)) <-> ((ph /\ ps /\ ch) /\ th))
Theorem	and4com 10404	/\ associativity.
|- ((ph /\ (ps /\ ch /\ th)) <-> ((ph /\ ps /\ ch) /\ th))
Theorem	anidmdbi 10405	Conjunct idempotence deduction equivalency. (Contributed by Roy F. Longton, 8-Aug-2005.)
|- ((ph -> (ps /\ ps)) <-> (ph -> ps))
Theorem	19.41vvvv 10406	Theorem 19.41 of [Margaris] p. 90 with 4 quantifiers.
|- (E.wE.xE.yE.z(ph /\ ps) <-> (E.wE.xE.yE.zph /\ ps))
Theorem	eeeeanv 10407	Rearrange existential quantifiers.
|- (E.wE.xE.yE.z((ph /\ ps /\ ch) /\ th) <-> ((E.wph /\ E.xps /\ E.ych) /\ E.zth))
Theorem	r19.3rzvb 10408	A more general version of r19.3rzv 2344.
|- (ph -> A.xph)   =>   |- (A =/= (/) -> (ph <-> A.x e. A ph))
Theorem	cbvrexf 10409	Rule used to change bound variables with implicit substitution. More general than cbvrex 1795.
|- (z e. A -> A.x z e. A)   &   |- (z e. A -> A.y z e. A)   &   |- (ph -> A.yph)   &   |- (ps -> A.xps)   &   |- (x = y -> (ph <-> ps))   =>   |- (E.x e. A ph <-> E.y e. A ps)
Theorem	faimpex 10410	"Restricted for all" implies "restricted there exists".
|- (A =/= (/) -> (A.x e. A ph -> E.x e. A ph))
Basic Set theory
Theorem	ntunte 10411	The intersection of a union U.A with a set B is equal to the union of the intersections of each element of A with B.
|- (U.A i^i B) = U.{x | E.y e. A x = (y i^i B)}
Theorem	oprabvaligg 10412	The value of an operation class abstraction (weak version).
|- (x = A -> (ph <-> ps))   &   |- (y = B -> (ps <-> ch))   &   |- (z = C -> (ch <-> th))   &   |- E*zph   &   |- F = {<.<.x, y>., z>. | ph}   =>   |- ((A e. R /\ B e. S /\ C e. D) -> (th -> (AFB) = C))
Theorem	uninqs 10413	The class union of the intersection of two subclasses of a quotient space. Compare uniin 2516.
|- Er R   =>   |- ((B (_ (A/.R) /\ C (_ (A/.R)) -> U.(B i^i C) = (U.B i^i U.C))
Theorem	erdisj2 10414	Equivalence classes do not overlap.
|- A e. V   &   |- B e. V   =>   |- (Er R -> ([A]R = [B]R \/ ([A]R i^i [B]R) = (/)))
Theorem	difeqri2 10415	Inference from membership to difference.
|- (A.x((x e. A /\ -. x e. B) <-> x e. C) -> (A \ B) = C)
Theorem	elo 10416	See eloprabg 4008. Note: to be used with categories.
|- (y = A -> (ph <-> ps))   &   |- (z = B -> (ps <-> ch))   &   |- (v = C -> (ch <-> th))   &   |- (w = D -> (th <-> ta))   =>   |- (((A e. Q /\ B e. R /\ C e. S) /\ D e. T) -> (<.<.A, B>., <.C, D>.>. e. {x | E.yE.zE.vE.w(x = <.<.y, z>., <.v, w>.>. /\ ph)} <-> ta))
Theorem	spfi 10417	Specific properties of a finite intersection.
|- (A e. B -> (A e. {x | E.y(y (_ C /\ E.z e. om y ~~ z /\ x = |^|y)} <-> E.y(y (_ C /\ E.z e. om y ~~ z /\ A = |^|y)))
Theorem	infi1 10418	The intersection of two finite intersections is a finite intersection.
|- ((A e. {x | E.y(y (_ C /\ E.z e. om y ~~ z /\ x = |^|y)} /\ B e. {x | E.y(y (_ C /\ E.z e. om y ~~ z /\ x = |^|y)}) -> (A i^i B) e. {x | E.y(y (_ C /\ E.z e. om y ~~ z /\ x = |^|y)})
Theorem	fine 10419	Condition to have a non empty finite intersections class.
|- (A =/= (/) -> {x | E.y(y (_ A /\ E.z e. om y ~~ z /\ x = |^|y)} =/= (/))
Theorem	abfi 10420	Any element of A is the intersection of a finite subclass of A.
|- A (_ {x | E.y(y (_ A /\ E.z e. om y ~~ z /\ x = |^|y)}
Theorem	fiiu 10421	If A is the intersection of a finite set of elements of B then A (_ U.B.
|- (A e. {x | E.y(y (_ B /\ E.z e. om y ~~ z /\ x = |^|y)} -> A (_ U.B)
Theorem	inpws1 10422	An intersection with a member of a powerset belongs to this powerset.
|- (A e. P~C -> (A i^i B) e. P~C)
Theorem	inpws2 10423	An intersection with a member of a powerset belongs to this powerset.
|- (B e. P~C -> (A i^i B) e. P~C)
Theorem	stcat 10424	Structure of the class abstraction used by Alg, Cat and Ded.
|- {x | E.yE.zE.vE.w(x = <.<.y, z>., <.v, w>.>. /\ ph)} (_ ((V X. V) X. (V X. V))
Theorem	11st22nd 10425	A theorem of the 1st2nd 4108 family.
|- (((Rel B /\ Rel dom B /\ Rel ran B) /\ A e. B) -> A = <.<.(1st` (1st` A)), (2nd` (1st` A))>., <.(1st` (2nd` A)), (2nd` (2nd` A))>.>.)
Theorem	ump 10426	The union of a part of a powerset belongs to it.
|- (A e. B -> U.{x e. P~A | ph} e. P~A)
Theorem	boe 10427	{A, A} has only one element.
|- A e. B   =>   |- {A, A} ~~ 1o
Theorem	moec 10428	Moving an element out from the intersection of a class.
|- (B e. A -> |^|A = (B i^i |^|(A \ {B})))
Theorem	hbcmpt 10429	Bound-variable hypothesis builder for the "maps to" notation.
|- (y e. (x e. A |-> B) -> A.x y e. (x e. A |-> B))
Theorem	fvopab2a 10430	Value of a function given by the "maps to" notation.
|- ((x e. A /\ B e. C) -> ((x e. A |-> B)` x) = B)
Theorem	cmpbva 10431	Rule to change a bound variable int the "maps to" notation.
|- F = (x e. A |-> C)   =>   |- F = (y e. A |-> C)
Theorem	fopab2ga 10432	Functionality and domain of a class given by the "maps to" notation.
|- F = (x e. A |-> C)   =>   |- (A.x e. A C e. V <-> F Fn A)
Theorem	fopab2a 10433	Functionality of a class given by the "maps to" notation.
|- F = (x e. A |-> C)   =>   |- (A.x e. A C e. B <-> F:A-->B)
Theorem	cmpfun 10434	Functionality of a class given by a "maps to" notation.
|- F = (x e. A |-> B)   =>   |- Fun F
Theorem	cmpdom 10435	Domain of a class given by the "maps to" notation.
|- F = (x e. A |-> B)   =>   |- (A.x e. A B e. V <-> dom F = A)
Theorem	cmpran 10436	Range of a class given by the "maps to" notation.
|- F = (x e. A |-> B)   =>   |- ran F = {y | E.x e. A y = B}
Theorem	fnoprvalrn2 10437	A function's value belongs to its range. A more general version of fnoprvalrn 4039. To be used with partial operations.
|- ((Fun F /\ <.A, B>. e. dom F) -> (AFB) e. ran F)
Theorem	intprd 10438	The intersection of a pair is the intersection of its members. Closed for of intpr 2559.Theorem 71 of [Suppes] p. 42.
|- ((A e. V /\ B e. V) -> |^|{A, B} = (A i^i B))
Theorem	ficli 10439	The class of finite intersections of a class L are closed under intersection.
|- F = {x | E.y(y (_ L /\ E.z e. om y ~~ z /\ x = |^|y)}   =>   |- ((A e. F /\ B e. F) -> (A i^i B) e. F)
Theorem	neiopne 10440	If an intersection is not empty its operands are not empty.
|- ((A i^i B) =/= (/) -> (A =/= (/) /\ B =/= (/)))
Theorem	f2imacnv 10441	Image of a pre-image.
|- ((F:A-1-1-onto->B /\ C (_ B) -> (F"(`'F"C)) = C)
Theorem	oooeqim2 10442	Symmetrical equality of the images and of their antecedents when the mapping is one to one.
|- ((F:A-1-1->B /\ X (_ A /\ Y (_ A) -> ((F"X) = (F"Y) <-> X = Y))
Finite intersection stuff using function fi
Syntax	cfi 10443	Extend class notation with the function whose value is the class of all the finite intersections of the elements of a given set.
class fi
Definition	df-fiNEW 10444	Function whose value is the class of all the finite intersections of the elements of x.
|- fi = {<.x, y>. | y = {u | E.z(z (_ x /\ E.a e. om z ~~ a /\ u = |^|z)}}
Theorem	fiv 10445	The set of all the finite intersections of the elements of A.
|- (A e. B -> (fi` A) = {u | E.z(z (_ A /\ E.a e. om z ~~ a /\ u = |^|z)})
Theorem	fine2 10446	If A is not empty, the class of all the finite intersections of A is not empty either.
|- (A e. B -> (A =/= (/) -> (fi` A) =/= (/)))
Theorem	sppfi 10447	Specific properties of an element of (fi` C).