Metamath Proof Explorer - mmtheorems31

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 - 3001-3100 - Page 31 of 58

Type	Label	Description
Statement
Syntax	co 3001	Extend class notation to include operations. Note that the syntax is simply three class symbols in a row surrounded by parentheses.
class (AFB)
Syntax	copab2 3002	Extend class notation to include class abstractions of nested ordered pairs.
class {⟨⟨x, y⟩, z⟩∣φ}
Definition	df-opr 3003	Define the result of an operation. Note that the syntax is simply three class symbols in a row bracketed by parentheses. Definition of [Enderton] p. 79. Class F normally denotes an operation such as + that operates on two classes A and B, which might be numbers such as 1 and 2. This definition is well-defined, although not very meaningful, when classes A and/or B are proper classes (i.e. are not sets). On the other hand we often find uses for this definition when F is a proper class.
⊢ (AFB) = (F ‘⟨A, B⟩)
Definition	df-oprab 3004	Define class abstraction of nested ordered pairs (for use in defining operations). A special case of Definition 4.16 of [TakeutiZaring] p. 14. Normally x, y, and z are distinct, although the definition doesn't strictly require it.
⊢ {⟨⟨x, y⟩, z⟩∣φ} = {w∣∃x∃y∃z(w = ⟨⟨x, y⟩, z⟩ ∧ φ)}
Theorem	opreq 3005	Equality theorem for operations.
⊢ (F = G → (AFB) = (AGB))
Theorem	opreq1 3006	Equality theorem for operations.
⊢ (A = B → (AFC) = (BFC))
Theorem	opreq2 3007	Equality theorem for operations.
⊢ (A = B → (CFA) = (CFB))
Theorem	opreq12 3008	Equality theorem for operations.
⊢ ((A = B ∧ C = D) → (AFC) = (BFD))
Theorem	opreq1i 3009	Equality inference for operations.
⊢ A = B    ⇒   ⊢ (AFC) = (BFC)
Theorem	opreq2i 3010	Equality inference for operations.
⊢ A = B    ⇒   ⊢ (CFA) = (CFB)
Theorem	opreq12i 3011	Equality inference for operations.
⊢ A = B    &   ⊢ C = D    ⇒   ⊢ (AFC) = (BFD)
Theorem	opreq1d 3012	Equality deduction for operations.
⊢ (φ → A = B)    ⇒   ⊢ (φ → (AFC) = (BFC))
Theorem	opreq2d 3013	Equality deduction for operations.
⊢ (φ → A = B)    ⇒   ⊢ (φ → (CFA) = (CFB))
Theorem	opreq12d 3014	Equality deduction for operations.
⊢ (φ → A = B)    &   ⊢ (φ → C = D)    ⇒   ⊢ (φ → (AFC) = (BFD))
Theorem	opreqan12d 3015	Equality deduction for operations.
⊢ (φ → A = B)    &   ⊢ (ψ → C = D)    ⇒   ⊢ ((φ ∧ ψ) → (AFC) = (BFD))
Theorem	opreqan12rd 3016	Equality deduction for operations.
⊢ (φ → A = B)    &   ⊢ (ψ → C = D)    ⇒   ⊢ ((ψ ∧ φ) → (AFC) = (BFD))
Theorem	hbopr 3017	Bound-variable hypothesis builder for operation value.
⊢ (y ∈ A → ∀x y ∈ A)    &   ⊢ (y ∈ F → ∀x y ∈ F)    &   ⊢ (y ∈ B → ∀x y ∈ B)    ⇒   ⊢ (y ∈ (AFB) → ∀x y ∈ (AFB))
Theorem	oprex 3018	The result of an operation is a set.
⊢ (AFB) ∈ V
Theorem	oprprc1 3019	The value of an operation when the first argument is a proper class. Note: this theorem is dependent on our particular definitions of operation value, function value, and ordered pair.
⊢ Rel dom F    ⇒   ⊢ (¬ A ∈ V → (AFB) = ∅)
Theorem	oprprc2 3020	The value of an operation when the second argument is a proper class. Note: this theorem is dependent on our particular definitions of operation value, function value, and ordered pair.
⊢ (¬ B ∈ V → (AFB) = (AFA))
Theorem	dfoprab2 3021	Class abstraction for operations in terms of class abstraction of ordered pairs.
⊢ {⟨⟨x, y⟩, z⟩∣φ} = {⟨w, z⟩∣∃x∃y(w = ⟨x, y⟩ ∧ φ)}
Theorem	reloprab 3022	The operation class abstraction is a relation.
⊢ Rel {⟨⟨x, y⟩, z⟩∣φ}
Theorem	hboprab1 3023	The abstraction variables in an operation abstraction are not free.
⊢ (w ∈ {⟨⟨x, y⟩, z⟩∣φ} → ∀x w ∈ {⟨⟨x, y⟩, z⟩∣φ})
Theorem	hboprab2 3024	The abstraction variables in an operation abstraction are not free.
⊢ (w ∈ {⟨⟨x, y⟩, z⟩∣φ} → ∀y w ∈ {⟨⟨x, y⟩, z⟩∣φ})
Theorem	bioprabd 3025	Equivalent wff's yield equal operation class abstractions (deduction rule).
⊢ (φ → ∀xφ)    &   ⊢ (φ → ∀yφ)    &   ⊢ (φ → ∀zφ)    &   ⊢ (φ → (ψ ↔ χ))    ⇒   ⊢ (φ → {⟨⟨x, y⟩, z⟩∣ψ} = {⟨⟨x, y⟩, z⟩∣χ})
Theorem	bioprabdv 3026	Equivalent wff's yield equal operation class abstractions (deduction rule).
⊢ (φ → (ψ ↔ χ))    ⇒   ⊢ (φ → {⟨⟨x, y⟩, z⟩∣ψ} = {⟨⟨x, y⟩, z⟩∣χ})
Theorem	bioprabi 3027	Equivalent wff's yield equal operation class abstractions.
⊢ (φ ↔ ψ)    ⇒   ⊢ {⟨⟨x, y⟩, z⟩∣φ} = {⟨⟨x, y⟩, z⟩∣ψ}
Theorem	cbvoprab12 3028	Rule used to change first two bound variables in an operation abstraction, using implicit substitution.
⊢ (φ → ∀wφ)    &   ⊢ (φ → ∀vφ)    &   ⊢ (ψ → ∀xψ)    &   ⊢ (ψ → ∀yψ)    &   ⊢ ((x = w ∧ y = v) → (φ ↔ ψ))    ⇒   ⊢ {⟨⟨x, y⟩, z⟩∣φ} = {⟨⟨w, v⟩, z⟩∣ψ}
Theorem	cbvoprab12v 3029	Rule used to change first two bound variables in an operation abstraction, using implicit substitution.
⊢ ((x = w ∧ y = v) → (φ ↔ ψ))    ⇒   ⊢ {⟨⟨x, y⟩, z⟩∣φ} = {⟨⟨w, v⟩, z⟩∣ψ}
Theorem	cbvoprab3v 3030	Rule used to change the third bound variable in an operation abstraction, using implicit substitution.
⊢ (z = w → (φ ↔ ψ))    ⇒   ⊢ {⟨⟨x, y⟩, z⟩∣φ} = {⟨⟨x, y⟩, w⟩∣ψ}
Theorem	dmoprab 3031	The domain of an operation abstraction.
⊢ dom {⟨⟨x, y⟩, z⟩∣φ} = {⟨x, y⟩∣∃zφ}
Theorem	dmoprabss 3032	The domain of an operation abstraction.
⊢ dom {⟨⟨x, y⟩, z⟩∣((x ∈ A ∧ y ∈ B) ∧ φ)} ⊆ (A × B)
Theorem	rnoprab 3033	The range of an operation class abstraction.
⊢ ran {⟨⟨x, y⟩, z⟩∣φ} = {z∣∃x∃yφ}
Theorem	reldmoprab 3034	The domain of an operation class abstraction is a relation.
⊢ Rel dom {⟨⟨x, y⟩, z⟩∣φ}
Theorem	eloprabg 3035	The law of concretion for operation class abstraction. Compare elopab 2110.
⊢ (x = A → (φ ↔ ψ))    &   ⊢ (y = B → (ψ ↔ χ))    &   ⊢ (z = C → (χ ↔ θ))    ⇒   ⊢ ((A ∈ D ∧ B ∈ R ∧ C ∈ S) → (⟨⟨A, B⟩, C⟩ ∈ {⟨⟨x, y⟩, z⟩∣φ} ↔ θ))
Theorem	ssoprab2i 3036	Inference of operation abstraction subclass from implication.
⊢ (φ → ψ)    ⇒   ⊢ {⟨⟨x, y⟩, z⟩∣φ} ⊆ {⟨⟨x, y⟩, z⟩∣ψ}
Theorem	funoprab 3037	"At most one" is sufficient condition for an operation abstraction to be a function.
⊢ ∃*zφ    ⇒   ⊢ Fun {⟨⟨x, y⟩, z⟩∣φ}
Theorem	fnoprab 3038	Functionality and domain of an operation abstraction.
⊢ (φ → ∃!zψ)    ⇒   ⊢ {⟨⟨x, y⟩, z⟩∣(φ ∧ ψ)} Fn {⟨x, y⟩∣φ}
Theorem	fnoprab2 3039	Functionality and domain of an operation abstraction.
⊢ C ∈ V    &   ⊢ F = {⟨⟨x, y⟩, z⟩∣((x ∈ A ∧ y ∈ B) ∧ z = C)}    ⇒   ⊢ F Fn (A × B)
Theorem	dmoprab2 3040	Domain of an operation abstraction.
⊢ C ∈ V    &   ⊢ F = {⟨⟨x, y⟩, z⟩∣((x ∈ A ∧ y ∈ B) ∧ z = C)}    ⇒   ⊢ dom F = (A × B)
Theorem	ffnoprval 3041	An operation maps to a class to which all values belong.
⊢ (F:(A × B)–→C ↔ (F Fn (A × B) ∧ ∀x ∈ A ∀y ∈ B (xFy) ∈ C))
Theorem	fnoprval 3042	Representation of an operation abstraction in terms of its values.
⊢ (F Fn (A × B) ↔ F = {⟨⟨x, y⟩, z⟩∣((x ∈ A ∧ y ∈ B) ∧ z = (xFy))})
Theorem	foprval 3043	Representation of an operation abstraction in terms of its values.
⊢ (F:(A × B)–→C ↔ (F = {⟨⟨x, y⟩, z⟩∣((x ∈ A ∧ y ∈ B) ∧ z = (xFy))} ∧ ∀x ∈ A ∀y ∈ B (xFy) ∈ C))
Theorem	oprabex 3044	Existence of an operation abstraction.
⊢ A ∈ V    &   ⊢ B ∈ V    &   ⊢ ((x ∈ A ∧ y ∈ B) → ∃*zφ)    &   ⊢ F = {⟨⟨x, y⟩, z⟩∣((x ∈ A ∧ y ∈ B) ∧ φ)}    ⇒   ⊢ F ∈ V
Theorem	oprabex2 3045	Existence of an operation abstraction (special case).
⊢ A ∈ V    &   ⊢ B ∈ V    &   ⊢ F = {⟨⟨x, y⟩, z⟩∣((x ∈ A ∧ y ∈ B) ∧ z = C)}    ⇒   ⊢ F ∈ V
Theorem	oprabex3 3046	Existence of an operation abstraction (special case).
⊢ H ∈ V    &   ⊢ F = {⟨⟨x, y⟩, z⟩∣((x ∈ (H × H) ∧ y ∈ (H × H)) ∧ ∃w∃v∃u∃f((x = ⟨w, v⟩ ∧ y = ⟨u, f⟩) ∧ z = R))}    ⇒   ⊢ F ∈ V
Theorem	oprabval 3047	The value of an operation abstraction.
⊢ C ∈ V    &   ⊢ (x = A → (φ ↔ ψ))    &   ⊢ (y = B → (ψ ↔ χ))    &   ⊢ (z = C → (χ ↔ θ))    &   ⊢ ((x ∈ R ∧ y ∈ S) → ∃!zφ)    &   ⊢ F = {⟨⟨x, y⟩, z⟩∣((x ∈ R ∧ y ∈ S) ∧ φ)}    ⇒   ⊢ ((A ∈ R ∧ B ∈ S) → ((AFB) = C ↔ θ))
Theorem	oprabvalig 3048	The value of an operation abstraction (weak version).
⊢ (x = A → (φ ↔ ψ))    &   ⊢ (y = B → (ψ ↔ χ))    &   ⊢ (z = C → (χ ↔ θ))    &   ⊢ ((x ∈ R ∧ y ∈ S) → ∃*zφ)    &   ⊢ F = {⟨⟨x, y⟩, z⟩∣((x ∈ R ∧ y ∈ S) ∧ φ)}    ⇒   ⊢ ((A ∈ R ∧ B ∈ S ∧ C ∈ D) → (θ → (AFB) = C))
Theorem	oprabvali 3049	The value of an operation abstraction (weak version).
⊢ C ∈ V    &   ⊢ (x = A → (φ ↔ ψ))    &   ⊢ (y = B → (ψ ↔ χ))    &   ⊢ (z = C → (χ ↔ θ))    &   ⊢ ((x ∈ R ∧ y ∈ S) → ∃*zφ)    &   ⊢ F = {⟨⟨x, y⟩, z⟩∣((x ∈ R ∧ y ∈ S) ∧ φ)}    ⇒   ⊢ ((A ∈ R ∧ B ∈ S) → (θ → (AFB) = C))
Theorem	oprabval2g 3050	The value of an operation abstraction. Special case.
⊢ (x = A → R = G)    &   ⊢ (y = B → G = S)    &   ⊢ F = {⟨⟨x, y⟩, z⟩∣((x ∈ C ∧ y ∈ D) ∧ z = R)}    ⇒   ⊢ ((A ∈ C ∧ B ∈ D ∧ S ∈ H) → (AFB) = S)
Theorem	oprabval2 3051	The value of an operation abstraction. Special case.
⊢ S ∈ V    &   ⊢ (x = A → R = G)    &   ⊢ (y = B → G = S)    &   ⊢ F = {⟨⟨x, y⟩, z⟩∣((x ∈ C ∧ y ∈ D) ∧ z = R)}    ⇒   ⊢ ((A ∈ C ∧ B ∈ D) → (AFB) = S)
Theorem	oprabval3 3052	The value of an operation abstraction. Special case.
⊢ S ∈ V    &   ⊢ (((w = A ∧ v = B) ∧ (u = C ∧ f = D)) → R = S)    &   ⊢ F = {⟨⟨x, y⟩, z⟩∣((x ∈ (H × H) ∧ y ∈ (H × H)) ∧ ∃w∃v∃u∃f((x = ⟨w, v⟩ ∧ y = ⟨u, f⟩) ∧ z = R))}    ⇒   ⊢ (((A ∈ H ∧ B ∈ H) ∧ (C ∈ H ∧ D ∈ H)) → (⟨A, B⟩F⟨C, D⟩) = S)
Theorem	oprabval4g 3053	Value of an operation given by an ordered pair abstraction. ( This is the operation analog of fvopab2 2878.)
⊢ F = {⟨⟨x, y⟩, z⟩∣((x ∈ A ∧ y ∈ B) ∧ z = C)}    ⇒   ⊢ ((x ∈ A ∧ y ∈ B ∧ C ∈ D) → (xFy) = C)
Theorem	elrnoprab 3054	Membership in the range of an operation abstraction.
⊢ C ∈ V    &   ⊢ F = {⟨⟨x, y⟩, z⟩∣((x ∈ A ∧ y ∈ B) ∧ z = C)}    ⇒   ⊢ (D ∈ ran F ↔ ∃x ∈ A ∃y ∈ B D = C)
Theorem	oprvalex 3055	Existence of a class of operation values.
⊢ A ∈ V    &   ⊢ B ∈ V    ⇒   ⊢ {z∣∃x ∈ A ∃y ∈ B z = (xFy)} ∈ V
Theorem	oprssdm 3056	Domain of closure of an operation.
⊢ ¬ ∅ ∈ S    &   ⊢ ((x ∈ S ∧ y ∈ S) → (xFy) ∈ S)    ⇒   ⊢ (S × S) ⊆ dom F
Theorem	ndmoprg 3057	The value of an operation outside its domain.
⊢ dom F = (S × S)    ⇒   ⊢ ((B ∈ C ∧ ¬ (A ∈ S ∧ B ∈ S)) → (AFB) = ∅)
Theorem	ndmoprcl 3058	The closure of an operation outside its domain, when the domain includes the empty set. This technical lemma can make the operation more convenient to work in some cases.
⊢ dom F = (S × S)    &   ⊢ ((A ∈ S ∧ x ∈ S) → (AFx) ∈ S)    &   ⊢ ∅ ∈ S    ⇒   ⊢ (AFB) ∈ S
Theorem	ndmopr 3059	The value of an operation outside its domain.
⊢ B ∈ V    &   ⊢ dom F = (S × S)    ⇒   ⊢ (¬ (A ∈ S ∧ B ∈ S) → (AFB) = ∅)
Theorem	ndmoprrcl 3060	Reverse closure law, when an operation's domain doesn't contain the empty set.
⊢ B ∈ V    &   ⊢ dom F = (S × S)    &   ⊢ ¬ ∅ ∈ S    ⇒   ⊢ ((AFB) ∈ S → (A ∈ S ∧ B ∈ S))
Theorem	ndmoprcom 3061	Any operation is commutative outside its domain.
⊢ B ∈ V    &   ⊢ dom F = (S × S)    &   ⊢ A ∈ V    ⇒   ⊢ (¬ (A ∈ S ∧ B ∈ S) → (AFB) = (BFA))
Theorem	ndmoprass 3062	Any operation is associative outside its domain, if the domain doesn't contain the empty set.
⊢ B ∈ V    &   ⊢ dom F = (S × S)    &   ⊢ C ∈ V    &   ⊢ ¬ ∅ ∈ S    ⇒   ⊢ (¬ (A ∈ S ∧ B ∈ S ∧ C ∈ S) → ((AFB)FC) = (AF(BFC)))
Theorem	ndmoprdistr 3063	Any operation is distributive outside its domain, if the domain doesn't contain the empty set.
⊢ B ∈ V    &   ⊢ dom F = (S × S)    &   ⊢ C ∈ V    &   ⊢ ¬ ∅ ∈ S    &   ⊢ dom G = (S × S)    ⇒   ⊢ (¬ (A ∈ S ∧ B ∈ S ∧ C ∈ S) → (AG(BFC)) = ((AGB)F(AGC)))
Theorem	ndmord 3064	Elimination of redundant antecedents in an ordering law.
⊢ B ∈ V    &   ⊢ dom F = (S × S)    &   ⊢ A ∈ V    &   ⊢ R ⊆ (S × S)    &   ⊢ ¬ ∅ ∈ S    &   ⊢ ((A ∈ S ∧ B ∈ S ∧ C ∈ S) → (ARB ↔ (CFA)R(CFB)))    ⇒   ⊢ (C ∈ S → (ARB ↔ (CFA)R(CFB)))
Theorem	ndmordi 3065	Elimination of redundant antecedent in an ordering law.
⊢ A ∈ V    &   ⊢ dom F = (S × S)    &   ⊢ R ⊆ (S × S)    &   ⊢ ¬ ∅ ∈ S    &   ⊢ (C ∈ S → (ARB ↔ (CFA)R(CFB)))    ⇒   ⊢ ((CFA)R(CFB) → ARB)
Theorem	caoprcl 3066	Convert an operation closure law to class notation.
⊢ ((x ∈ S ∧ y ∈ S) → (xFy) ∈ S)    ⇒   ⊢ ((A ∈ S ∧ B ∈ S) → (AFB) ∈ S)
Theorem	caoprcom 3067	Convert an operation commutative law to class notation.
⊢ A ∈ V    &   ⊢ B ∈ V    &   ⊢ (xFy) = (yFx)    ⇒   ⊢ (AFB) = (BFA)
Theorem	caoprass 3068	Convert an operation associative law to class notation.
⊢ A ∈ V    &   ⊢ B ∈ V    &   ⊢ C ∈ V    &   ⊢ ((xFy)Fz) = (xF(yFz))    ⇒   ⊢ ((AFB)FC) = (AF(BFC))
Theorem	caoprcan 3069	Convert an operation cancellation law to class notation.
⊢ C ∈ V    &   ⊢ ((x ∈ S ∧ y ∈ S) → ((xFy) = (xFz) → y = z))    ⇒   ⊢ ((A ∈ S ∧ B ∈ S) → ((AFB) = (AFC) → B = C))
Theorem	caoprord 3070	Convert an operation ordering law to class notation.
⊢ A ∈ V    &   ⊢ B ∈ V    &   ⊢ (z ∈ S → (xRy ↔ (zFx)R(zFy)))    ⇒   ⊢ (C ∈ S → (ARB ↔ (CFA)R(CFB)))
Theorem	caoprord2 3071	Operation ordering law with commuted arguments.
⊢ A ∈ V    &   ⊢ B ∈ V    &   ⊢ (z ∈ S → (xRy ↔ (zFx)R(zFy)))    &   ⊢ C ∈ V    &   ⊢ (xFy) = (yFx)    ⇒   ⊢ (C ∈ S → (ARB ↔ (AFC)R(BFC)))
Theorem	caoprord3 3072	Ordering law.
⊢ A ∈ V    &   ⊢ B ∈ V    &   ⊢ (z ∈ S → (xRy ↔ (zFx)R(zFy)))    &   ⊢ C ∈ V    &   ⊢ (xFy) = (yFx)    &   ⊢ D ∈ V    ⇒   ⊢ (((B ∈ S ∧ C ∈ S) ∧ (AFB) = (CFD)) → (ARC ↔ DRB))
Theorem	caoprdistr 3073	Convert an operation distributive law to class notation.
⊢ A ∈ V    &   ⊢ B ∈ V    &   ⊢ C ∈ V    &   ⊢ (xG(yFz)) = ((xGy)F(xGz))    ⇒   ⊢ (AG(BFC)) = ((AGB)F(AGC))
Theorem	caopr32 3074	Rearrange arguments in a commutative, associative operation.
⊢ A ∈ V    &   ⊢ B ∈ V    &   ⊢ C ∈ V    &   ⊢ (xFy) = (yFx)    &   ⊢ ((xFy)Fz) = (xF(yFz))    ⇒   ⊢ ((AFB)FC) = ((AFC)FB)
Theorem	caopr12 3075	Rearrange arguments in a commutative, associative operation.
⊢ A ∈ V    &   ⊢ B ∈ V    &   ⊢ C ∈ V    &   ⊢ (xFy) = (yFx)    &   ⊢ ((xFy)Fz) = (xF(yFz))    ⇒   ⊢ (AF(BFC)) = (BF(AFC))
Theorem	caopr31 3076	Rearrange arguments in a commutative, associative operation.
⊢ A ∈ V    &   ⊢ B ∈ V    &   ⊢ C ∈ V    &   ⊢ (xFy) = (yFx)    &   ⊢ ((xFy)Fz) = (xF(yFz))    ⇒   ⊢ ((AFB)FC) = ((CFB)FA)
Theorem	caopr13 3077	Rearrange arguments in a commutative, associative operation.
⊢ A ∈ V    &   ⊢ B ∈ V    &   ⊢ C ∈ V    &   ⊢ (xFy) = (yFx)    &   ⊢ ((xFy)Fz) = (xF(yFz))    ⇒   ⊢ (AF(BFC)) = (CF(BFA))
Theorem	caopr4 3078	Rearrange arguments in a commutative, associative operation.
⊢ A ∈ V    &   ⊢ B ∈ V    &   ⊢ C ∈ V    &   ⊢ (xFy) = (yFx)    &   ⊢ ((xFy)Fz) = (xF(yFz))    &   ⊢ D ∈ V    ⇒   ⊢ ((AFB)F(CFD)) = ((AFC)F(BFD))
Theorem	caopr411 3079	Rearrange arguments in a commutative, associative operation.
⊢ A ∈ V    &   ⊢ B ∈ V    &   ⊢ C ∈ V    &   ⊢ (xFy) = (yFx)    &   ⊢ ((xFy)Fz) = (xF(yFz))    &   ⊢ D ∈ V    ⇒   ⊢ ((AFB)F(CFD)) = ((CFB)F(AFD))
Theorem	caopr42 3080	Rearrange arguments in a commutative, associative operation.
⊢ A ∈ V    &   ⊢ B ∈ V    &   ⊢ C ∈ V    &   ⊢ (xFy) = (yFx)    &   ⊢ ((xFy)Fz) = (xF(yFz))    &   ⊢ D ∈ V    ⇒   ⊢ ((AFB)F(CFD)) = ((AFC)F(DFB))
Theorem	caoprdistrr 3081	Reverse distributive law.
⊢ A ∈ V    &   ⊢ B ∈ V    &   ⊢ C ∈ V    &   ⊢ (xGy) = (yGx)    &   ⊢ (xG(yFz)) = ((xGy)F(xGz))    ⇒   ⊢ ((AFB)GC) = ((AGC)F(BGC))
Theorem	caoprdilem 3082	Lemma used by real number construction.
⊢ A ∈ V    &   ⊢ B ∈ V    &   ⊢ C ∈ V    &   ⊢ (xGy) = (yGx)    &   ⊢ (xG(yFz)) = ((xGy)F(xGz))    &   ⊢ D ∈ V    &   ⊢ H ∈ V    &   ⊢ ((xGy)Gz) = (xG(yGz))    ⇒   ⊢ (((AGC)F(BGD))GH) = ((AG(CGH))F(BG(DGH)))
Theorem	caoprlem2 3083	Lemma used in real number construction.
⊢ A ∈ V    &   ⊢ B ∈ V    &   ⊢ C ∈ V    &   ⊢ (xGy) = (yGx)    &   ⊢ (xG(yFz)) = ((xGy)F(xGz))    &   ⊢ D ∈ V    &   ⊢ H ∈ V    &   ⊢ ((xGy)Gz) = (xG(yGz))    &   ⊢ R ∈ V    &   ⊢ (xFy) = (yFx)    &   ⊢ ((xFy)Fz) = (xF(yFz))    ⇒   ⊢ ((((AGC)F(BGD))GH)F(((AGD)F(BGC))GR)) = ((AG((CGH)F(DGR)))F(BG((CGR)F(DGH))))
Theorem	caoprmo 3084	Uniqueness of inverse element in commutative, associative operation with identity. Remark in proof of Proposition 9-2.4 of [Gleason</