Home | Intuitionistic Logic Explorer Theorem List (p. 48 of 74) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | cnvcnv2 4701 | The double converse of a class equals its restriction to the universe. (Contributed by NM, 8-Oct-2007.) |
⊢ ^{◡}^{◡}A = (A ↾ V) | ||
Theorem | cnvcnvss 4702 | The double converse of a class is a subclass. Exercise 2 of [TakeutiZaring] p. 25. (Contributed by NM, 23-Jul-2004.) |
⊢ ^{◡}^{◡}A ⊆ A | ||
Theorem | cnveqb 4703 | Equality theorem for converse. (Contributed by FL, 19-Sep-2011.) |
⊢ ((Rel A ∧ Rel B) → (A = B ↔ ^{◡}A = ^{◡}B)) | ||
Theorem | cnveq0 4704 | A relation empty iff its converse is empty. (Contributed by FL, 19-Sep-2011.) |
⊢ (Rel A → (A = ∅ ↔ ^{◡}A = ∅)) | ||
Theorem | dfrel3 4705 | Alternate definition of relation. (Contributed by NM, 14-May-2008.) |
⊢ (Rel 𝑅 ↔ (𝑅 ↾ V) = 𝑅) | ||
Theorem | dmresv 4706 | The domain of a universal restriction. (Contributed by NM, 14-May-2008.) |
⊢ dom (A ↾ V) = dom A | ||
Theorem | rnresv 4707 | The range of a universal restriction. (Contributed by NM, 14-May-2008.) |
⊢ ran (A ↾ V) = ran A | ||
Theorem | dfrn4 4708 | Range defined in terms of image. (Contributed by NM, 14-May-2008.) |
⊢ ran A = (A “ V) | ||
Theorem | csbrng 4709 | Distribute proper substitution through the range of a class. (Contributed by Alan Sare, 10-Nov-2012.) |
⊢ (A ∈ 𝑉 → ⦋A / x⦌ran B = ran ⦋A / x⦌B) | ||
Theorem | rescnvcnv 4710 | The restriction of the double converse of a class. (Contributed by NM, 8-Apr-2007.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
⊢ (^{◡}^{◡}A ↾ B) = (A ↾ B) | ||
Theorem | cnvcnvres 4711 | The double converse of the restriction of a class. (Contributed by NM, 3-Jun-2007.) |
⊢ ^{◡}^{◡}(A ↾ B) = (^{◡}^{◡}A ↾ B) | ||
Theorem | imacnvcnv 4712 | The image of the double converse of a class. (Contributed by NM, 8-Apr-2007.) |
⊢ (^{◡}^{◡}A “ B) = (A “ B) | ||
Theorem | dmsnm 4713* | The domain of a singleton is inhabited iff the singleton argument is an ordered pair. (Contributed by Jim Kingdon, 15-Dec-2018.) |
⊢ (A ∈ (V × V) ↔ ∃x x ∈ dom {A}) | ||
Theorem | rnsnm 4714* | The range of a singleton is inhabited iff the singleton argument is an ordered pair. (Contributed by Jim Kingdon, 15-Dec-2018.) |
⊢ (A ∈ (V × V) ↔ ∃x x ∈ ran {A}) | ||
Theorem | dmsn0 4715 | The domain of the singleton of the empty set is empty. (Contributed by NM, 30-Jan-2004.) |
⊢ dom {∅} = ∅ | ||
Theorem | cnvsn0 4716 | The converse of the singleton of the empty set is empty. (Contributed by Mario Carneiro, 30-Aug-2015.) |
⊢ ^{◡}{∅} = ∅ | ||
Theorem | dmsn0el 4717 | The domain of a singleton is empty if the singleton's argument contains the empty set. (Contributed by NM, 15-Dec-2008.) |
⊢ (∅ ∈ A → dom {A} = ∅) | ||
Theorem | relsn2m 4718* | A singleton is a relation iff it has an inhabited domain. (Contributed by Jim Kingdon, 16-Dec-2018.) |
⊢ A ∈ V ⇒ ⊢ (Rel {A} ↔ ∃x x ∈ dom {A}) | ||
Theorem | dmsnopg 4719 | The domain of a singleton of an ordered pair is the singleton of the first member. (Contributed by Mario Carneiro, 26-Apr-2015.) |
⊢ (B ∈ 𝑉 → dom {⟨A, B⟩} = {A}) | ||
Theorem | dmpropg 4720 | The domain of an unordered pair of ordered pairs. (Contributed by Mario Carneiro, 26-Apr-2015.) |
⊢ ((B ∈ 𝑉 ∧ 𝐷 ∈ 𝑊) → dom {⟨A, B⟩, ⟨𝐶, 𝐷⟩} = {A, 𝐶}) | ||
Theorem | dmsnop 4721 | The domain of a singleton of an ordered pair is the singleton of the first member. (Contributed by NM, 30-Jan-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) (Revised by Mario Carneiro, 26-Apr-2015.) |
⊢ B ∈ V ⇒ ⊢ dom {⟨A, B⟩} = {A} | ||
Theorem | dmprop 4722 | The domain of an unordered pair of ordered pairs. (Contributed by NM, 13-Sep-2011.) |
⊢ B ∈ V & ⊢ 𝐷 ∈ V ⇒ ⊢ dom {⟨A, B⟩, ⟨𝐶, 𝐷⟩} = {A, 𝐶} | ||
Theorem | dmtpop 4723 | The domain of an unordered triple of ordered pairs. (Contributed by NM, 14-Sep-2011.) |
⊢ B ∈ V & ⊢ 𝐷 ∈ V & ⊢ 𝐹 ∈ V ⇒ ⊢ dom {⟨A, B⟩, ⟨𝐶, 𝐷⟩, ⟨𝐸, 𝐹⟩} = {A, 𝐶, 𝐸} | ||
Theorem | cnvcnvsn 4724 | Double converse of a singleton of an ordered pair. (Unlike cnvsn 4730, this does not need any sethood assumptions on A and B.) (Contributed by Mario Carneiro, 26-Apr-2015.) |
⊢ ^{◡}^{◡}{⟨A, B⟩} = ^{◡}{⟨B, A⟩} | ||
Theorem | dmsnsnsng 4725 | The domain of the singleton of the singleton of a singleton. (Contributed by Jim Kingdon, 16-Dec-2018.) |
⊢ (A ∈ V → dom {{{A}}} = {A}) | ||
Theorem | rnsnopg 4726 | The range of a singleton of an ordered pair is the singleton of the second member. (Contributed by NM, 24-Jul-2004.) (Revised by Mario Carneiro, 30-Apr-2015.) |
⊢ (A ∈ 𝑉 → ran {⟨A, B⟩} = {B}) | ||
Theorem | rnpropg 4727 | The range of a pair of ordered pairs is the pair of second members. (Contributed by Thierry Arnoux, 3-Jan-2017.) |
⊢ ((A ∈ 𝑉 ∧ B ∈ 𝑊) → ran {⟨A, 𝐶⟩, ⟨B, 𝐷⟩} = {𝐶, 𝐷}) | ||
Theorem | rnsnop 4728 | The range of a singleton of an ordered pair is the singleton of the second member. (Contributed by NM, 24-Jul-2004.) (Revised by Mario Carneiro, 26-Apr-2015.) |
⊢ A ∈ V ⇒ ⊢ ran {⟨A, B⟩} = {B} | ||
Theorem | op1sta 4729 | Extract the first member of an ordered pair. (See op2nda 4732 to extract the second member and op1stb 4159 for an alternate version.) (Contributed by Raph Levien, 4-Dec-2003.) |
⊢ A ∈ V & ⊢ B ∈ V ⇒ ⊢ ∪ dom {⟨A, B⟩} = A | ||
Theorem | cnvsn 4730 | Converse of a singleton of an ordered pair. (Contributed by NM, 11-May-1998.) (Revised by Mario Carneiro, 26-Apr-2015.) |
⊢ A ∈ V & ⊢ B ∈ V ⇒ ⊢ ^{◡}{⟨A, B⟩} = {⟨B, A⟩} | ||
Theorem | op2ndb 4731 | Extract the second member of an ordered pair. Theorem 5.12(ii) of [Monk1] p. 52. (See op1stb 4159 to extract the first member and op2nda 4732 for an alternate version.) (Contributed by NM, 25-Nov-2003.) |
⊢ A ∈ V & ⊢ B ∈ V ⇒ ⊢ ∩ ∩ ∩ ^{◡}{⟨A, B⟩} = B | ||
Theorem | op2nda 4732 | Extract the second member of an ordered pair. (See op1sta 4729 to extract the first member and op2ndb 4731 for an alternate version.) (Contributed by NM, 17-Feb-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
⊢ A ∈ V & ⊢ B ∈ V ⇒ ⊢ ∪ ran {⟨A, B⟩} = B | ||
Theorem | cnvsng 4733 | Converse of a singleton of an ordered pair. (Contributed by NM, 23-Jan-2015.) |
⊢ ((A ∈ 𝑉 ∧ B ∈ 𝑊) → ^{◡}{⟨A, B⟩} = {⟨B, A⟩}) | ||
Theorem | opswapg 4734 | Swap the members of an ordered pair. (Contributed by Jim Kingdon, 16-Dec-2018.) |
⊢ ((A ∈ 𝑉 ∧ B ∈ 𝑊) → ∪ ^{◡}{⟨A, B⟩} = ⟨B, A⟩) | ||
Theorem | elxp4 4735 | Membership in a cross product. This version requires no quantifiers or dummy variables. See also elxp5 4736. (Contributed by NM, 17-Feb-2004.) |
⊢ (A ∈ (B × 𝐶) ↔ (A = ⟨∪ dom {A}, ∪ ran {A}⟩ ∧ (∪ dom {A} ∈ B ∧ ∪ ran {A} ∈ 𝐶))) | ||
Theorem | elxp5 4736 | Membership in a cross product requiring no quantifiers or dummy variables. Provides a slightly shorter version of elxp4 4735 when the double intersection does not create class existence problems (caused by int0 3603). (Contributed by NM, 1-Aug-2004.) |
⊢ (A ∈ (B × 𝐶) ↔ (A = ⟨∩ ∩ A, ∪ ran {A}⟩ ∧ (∩ ∩ A ∈ B ∧ ∪ ran {A} ∈ 𝐶))) | ||
Theorem | cnvresima 4737 | An image under the converse of a restriction. (Contributed by Jeff Hankins, 12-Jul-2009.) |
⊢ (^{◡}(𝐹 ↾ A) “ B) = ((^{◡}𝐹 “ B) ∩ A) | ||
Theorem | resdm2 4738 | A class restricted to its domain equals its double converse. (Contributed by NM, 8-Apr-2007.) |
⊢ (A ↾ dom A) = ^{◡}^{◡}A | ||
Theorem | resdmres 4739 | Restriction to the domain of a restriction. (Contributed by NM, 8-Apr-2007.) |
⊢ (A ↾ dom (A ↾ B)) = (A ↾ B) | ||
Theorem | imadmres 4740 | The image of the domain of a restriction. (Contributed by NM, 8-Apr-2007.) |
⊢ (A “ dom (A ↾ B)) = (A “ B) | ||
Theorem | mptpreima 4741* | The preimage of a function in maps-to notation. (Contributed by Stefan O'Rear, 25-Jan-2015.) |
⊢ 𝐹 = (x ∈ A ↦ B) ⇒ ⊢ (^{◡}𝐹 “ 𝐶) = {x ∈ A ∣ B ∈ 𝐶} | ||
Theorem | mptiniseg 4742* | Converse singleton image of a function defined by maps-to. (Contributed by Stefan O'Rear, 25-Jan-2015.) |
⊢ 𝐹 = (x ∈ A ↦ B) ⇒ ⊢ (𝐶 ∈ 𝑉 → (^{◡}𝐹 “ {𝐶}) = {x ∈ A ∣ B = 𝐶}) | ||
Theorem | dmmpt 4743 | The domain of the mapping operation in general. (Contributed by NM, 16-May-1995.) (Revised by Mario Carneiro, 22-Mar-2015.) |
⊢ 𝐹 = (x ∈ A ↦ B) ⇒ ⊢ dom 𝐹 = {x ∈ A ∣ B ∈ V} | ||
Theorem | dmmptss 4744* | The domain of a mapping is a subset of its base class. (Contributed by Scott Fenton, 17-Jun-2013.) |
⊢ 𝐹 = (x ∈ A ↦ B) ⇒ ⊢ dom 𝐹 ⊆ A | ||
Theorem | dmmptg 4745* | The domain of the mapping operation is the stated domain, if the function value is always a set. (Contributed by Mario Carneiro, 9-Feb-2013.) (Revised by Mario Carneiro, 14-Sep-2013.) |
⊢ (∀x ∈ A B ∈ 𝑉 → dom (x ∈ A ↦ B) = A) | ||
Theorem | relco 4746 | A composition is a relation. Exercise 24 of [TakeutiZaring] p. 25. (Contributed by NM, 26-Jan-1997.) |
⊢ Rel (A ∘ B) | ||
Theorem | dfco2 4747* | Alternate definition of a class composition, using only one bound variable. (Contributed by NM, 19-Dec-2008.) |
⊢ (A ∘ B) = ∪ x ∈ V ((^{◡}B “ {x}) × (A “ {x})) | ||
Theorem | dfco2a 4748* | Generalization of dfco2 4747, where 𝐶 can have any value between dom A ∩ ran B and V. (Contributed by NM, 21-Dec-2008.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
⊢ ((dom A ∩ ran B) ⊆ 𝐶 → (A ∘ B) = ∪ x ∈ 𝐶 ((^{◡}B “ {x}) × (A “ {x}))) | ||
Theorem | coundi 4749 | Class composition distributes over union. (Contributed by NM, 21-Dec-2008.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
⊢ (A ∘ (B ∪ 𝐶)) = ((A ∘ B) ∪ (A ∘ 𝐶)) | ||
Theorem | coundir 4750 | Class composition distributes over union. (Contributed by NM, 21-Dec-2008.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
⊢ ((A ∪ B) ∘ 𝐶) = ((A ∘ 𝐶) ∪ (B ∘ 𝐶)) | ||
Theorem | cores 4751 | Restricted first member of a class composition. (Contributed by NM, 12-Oct-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
⊢ (ran B ⊆ 𝐶 → ((A ↾ 𝐶) ∘ B) = (A ∘ B)) | ||
Theorem | resco 4752 | Associative law for the restriction of a composition. (Contributed by NM, 12-Dec-2006.) |
⊢ ((A ∘ B) ↾ 𝐶) = (A ∘ (B ↾ 𝐶)) | ||
Theorem | imaco 4753 | Image of the composition of two classes. (Contributed by Jason Orendorff, 12-Dec-2006.) |
⊢ ((A ∘ B) “ 𝐶) = (A “ (B “ 𝐶)) | ||
Theorem | rnco 4754 | The range of the composition of two classes. (Contributed by NM, 12-Dec-2006.) |
⊢ ran (A ∘ B) = ran (A ↾ ran B) | ||
Theorem | rnco2 4755 | The range of the composition of two classes. (Contributed by NM, 27-Mar-2008.) |
⊢ ran (A ∘ B) = (A “ ran B) | ||
Theorem | dmco 4756 | The domain of a composition. Exercise 27 of [Enderton] p. 53. (Contributed by NM, 4-Feb-2004.) |
⊢ dom (A ∘ B) = (^{◡}B “ dom A) | ||
Theorem | coiun 4757* | Composition with an indexed union. (Contributed by NM, 21-Dec-2008.) |
⊢ (A ∘ ∪ x ∈ 𝐶 B) = ∪ x ∈ 𝐶 (A ∘ B) | ||
Theorem | cocnvcnv1 4758 | A composition is not affected by a double converse of its first argument. (Contributed by NM, 8-Oct-2007.) |
⊢ (^{◡}^{◡}A ∘ B) = (A ∘ B) | ||
Theorem | cocnvcnv2 4759 | A composition is not affected by a double converse of its second argument. (Contributed by NM, 8-Oct-2007.) |
⊢ (A ∘ ^{◡}^{◡}B) = (A ∘ B) | ||
Theorem | cores2 4760 | Absorption of a reverse (preimage) restriction of the second member of a class composition. (Contributed by NM, 11-Dec-2006.) |
⊢ (dom A ⊆ 𝐶 → (A ∘ ^{◡}(^{◡}B ↾ 𝐶)) = (A ∘ B)) | ||
Theorem | co02 4761 | Composition with the empty set. Theorem 20 of [Suppes] p. 63. (Contributed by NM, 24-Apr-2004.) |
⊢ (A ∘ ∅) = ∅ | ||
Theorem | co01 4762 | Composition with the empty set. (Contributed by NM, 24-Apr-2004.) |
⊢ (∅ ∘ A) = ∅ | ||
Theorem | coi1 4763 | Composition with the identity relation. Part of Theorem 3.7(i) of [Monk1] p. 36. (Contributed by NM, 22-Apr-2004.) |
⊢ (Rel A → (A ∘ I ) = A) | ||
Theorem | coi2 4764 | Composition with the identity relation. Part of Theorem 3.7(i) of [Monk1] p. 36. (Contributed by NM, 22-Apr-2004.) |
⊢ (Rel A → ( I ∘ A) = A) | ||
Theorem | coires1 4765 | Composition with a restricted identity relation. (Contributed by FL, 19-Jun-2011.) (Revised by Stefan O'Rear, 7-Mar-2015.) |
⊢ (A ∘ ( I ↾ B)) = (A ↾ B) | ||
Theorem | coass 4766 | 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. (Contributed by NM, 27-Jan-1997.) |
⊢ ((A ∘ B) ∘ 𝐶) = (A ∘ (B ∘ 𝐶)) | ||
Theorem | relcnvtr 4767 | A relation is transitive iff its converse is transitive. (Contributed by FL, 19-Sep-2011.) |
⊢ (Rel 𝑅 → ((𝑅 ∘ 𝑅) ⊆ 𝑅 ↔ (^{◡}𝑅 ∘ ^{◡}𝑅) ⊆ ^{◡}𝑅)) | ||
Theorem | relssdmrn 4768 | A relation is included in the cross product of its domain and range. Exercise 4.12(t) of [Mendelson] p. 235. (Contributed by NM, 3-Aug-1994.) |
⊢ (Rel A → A ⊆ (dom A × ran A)) | ||
Theorem | cnvssrndm 4769 | The converse is a subset of the cartesian product of range and domain. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ ^{◡}A ⊆ (ran A × dom A) | ||
Theorem | cossxp 4770 | Composition as a subset of the cross product of factors. (Contributed by Mario Carneiro, 12-Jan-2017.) |
⊢ (A ∘ B) ⊆ (dom B × ran A) | ||
Theorem | relrelss 4771 | Two ways to describe the structure of a two-place operation. (Contributed by NM, 17-Dec-2008.) |
⊢ ((Rel A ∧ Rel dom A) ↔ A ⊆ ((V × V) × V)) | ||
Theorem | unielrel 4772 | The membership relation for a relation is inherited by class union. (Contributed by NM, 17-Sep-2006.) |
⊢ ((Rel 𝑅 ∧ A ∈ 𝑅) → ∪ A ∈ ∪ 𝑅) | ||
Theorem | relfld 4773 | The double union of a relation is its field. (Contributed by NM, 17-Sep-2006.) |
⊢ (Rel 𝑅 → ∪ ∪ 𝑅 = (dom 𝑅 ∪ ran 𝑅)) | ||
Theorem | relresfld 4774 | Restriction of a relation to its field. (Contributed by FL, 15-Apr-2012.) |
⊢ (Rel 𝑅 → (𝑅 ↾ ∪ ∪ 𝑅) = 𝑅) | ||
Theorem | relcoi2 4775 | Composition with the identity relation restricted to a relation's field. (Contributed by FL, 2-May-2011.) |
⊢ (Rel 𝑅 → (( I ↾ ∪ ∪ 𝑅) ∘ 𝑅) = 𝑅) | ||
Theorem | relcoi1 4776 | Composition with the identity relation restricted to a relation's field. (Contributed by FL, 8-May-2011.) |
⊢ (Rel 𝑅 → (𝑅 ∘ ( I ↾ ∪ ∪ 𝑅)) = 𝑅) | ||
Theorem | unidmrn 4777 | The double union of the converse of a class is its field. (Contributed by NM, 4-Jun-2008.) |
⊢ ∪ ∪ ^{◡}A = (dom A ∪ ran A) | ||
Theorem | relcnvfld 4778 | if 𝑅 is a relation, its double union equals the double union of its converse. (Contributed by FL, 5-Jan-2009.) |
⊢ (Rel 𝑅 → ∪ ∪ 𝑅 = ∪ ∪ ^{◡}𝑅) | ||
Theorem | dfdm2 4779 | Alternate definition of domain df-dm 4282 that doesn't require dummy variables. (Contributed by NM, 2-Aug-2010.) |
⊢ dom A = ∪ ∪ (^{◡}A ∘ A) | ||
Theorem | unixpm 4780* | The double class union of an inhabited cross product is the union of its members. (Contributed by Jim Kingdon, 18-Dec-2018.) |
⊢ (∃x x ∈ (A × B) → ∪ ∪ (A × B) = (A ∪ B)) | ||
Theorem | unixp0im 4781 | The union of an empty cross product is empty. (Contributed by Jim Kingdon, 18-Dec-2018.) |
⊢ ((A × B) = ∅ → ∪ (A × B) = ∅) | ||
Theorem | cnvexg 4782 | The converse of a set is a set. Corollary 6.8(1) of [TakeutiZaring] p. 26. (Contributed by NM, 17-Mar-1998.) |
⊢ (A ∈ 𝑉 → ^{◡}A ∈ V) | ||
Theorem | cnvex 4783 | The converse of a set is a set. Corollary 6.8(1) of [TakeutiZaring] p. 26. (Contributed by NM, 19-Dec-2003.) |
⊢ A ∈ V ⇒ ⊢ ^{◡}A ∈ V | ||
Theorem | relcnvexb 4784 | A relation is a set iff its converse is a set. (Contributed by FL, 3-Mar-2007.) |
⊢ (Rel 𝑅 → (𝑅 ∈ V ↔ ^{◡}𝑅 ∈ V)) | ||
Theorem | ressn 4785 | Restriction of a class to a singleton. (Contributed by Mario Carneiro, 28-Dec-2014.) |
⊢ (A ↾ {B}) = ({B} × (A “ {B})) | ||
Theorem | cnviinm 4786* | The converse of an intersection is the intersection of the converse. (Contributed by Jim Kingdon, 18-Dec-2018.) |
⊢ (∃y y ∈ A → ^{◡}∩ x ∈ A B = ∩ x ∈ A ^{◡}B) | ||
Theorem | cnvpom 4787* | The converse of a partial order relation is a partial order relation. (Contributed by NM, 15-Jun-2005.) |
⊢ (∃x x ∈ A → (𝑅 Po A ↔ ^{◡}𝑅 Po A)) | ||
Theorem | cnvsom 4788* | The converse of a strict order relation is a strict order relation. (Contributed by Jim Kingdon, 19-Dec-2018.) |
⊢ (∃x x ∈ A → (𝑅 Or A ↔ ^{◡}𝑅 Or A)) | ||
Theorem | coexg 4789 | The composition of two sets is a set. (Contributed by NM, 19-Mar-1998.) |
⊢ ((A ∈ 𝑉 ∧ B ∈ 𝑊) → (A ∘ B) ∈ V) | ||
Theorem | coex 4790 | The composition of two sets is a set. (Contributed by NM, 15-Dec-2003.) |
⊢ A ∈ V & ⊢ B ∈ V ⇒ ⊢ (A ∘ B) ∈ V | ||
Theorem | xpcom 4791* | Composition of two cross products. (Contributed by Jim Kingdon, 20-Dec-2018.) |
⊢ (∃x x ∈ B → ((B × 𝐶) ∘ (A × B)) = (A × 𝐶)) | ||
Syntax | cio 4792 | Extend class notation with Russell's definition description binder (inverted iota). |
class (℩xφ) | ||
Theorem | iotajust 4793* | Soundness justification theorem for df-iota 4794. (Contributed by Andrew Salmon, 29-Jun-2011.) |
⊢ ∪ {y ∣ {x ∣ φ} = {y}} = ∪ {z ∣ {x ∣ φ} = {z}} | ||
Definition | df-iota 4794* |
Define Russell's definition description binder, which can be read as
"the unique x such that φ," where φ ordinarily contains
x as a free
variable. Our definition is meaningful only when there
is exactly one x such that φ is true (see iotaval 4805);
otherwise, it evaluates to the empty set (see iotanul 4809). Russell used
the inverted iota symbol ℩ to represent
the binder.
Sometimes proofs need to expand an iota-based definition. That is, given "X = the x for which ... x ... x ..." holds, the proof needs to get to "... X ... X ...". A general strategy to do this is to use iotacl 4817 (for unbounded iota). This can be easier than applying a version that applies an explicit substitution, because substituting an iota into its own property always has a bound variable clash which must be first renamed or else guarded with NF. (Contributed by Andrew Salmon, 30-Jun-2011.) |
⊢ (℩xφ) = ∪ {y ∣ {x ∣ φ} = {y}} | ||
Theorem | dfiota2 4795* | Alternate definition for descriptions. Definition 8.18 in [Quine] p. 56. (Contributed by Andrew Salmon, 30-Jun-2011.) |
⊢ (℩xφ) = ∪ {y ∣ ∀x(φ ↔ x = y)} | ||
Theorem | nfiota1 4796 | Bound-variable hypothesis builder for the ℩ class. (Contributed by Andrew Salmon, 11-Jul-2011.) (Revised by Mario Carneiro, 15-Oct-2016.) |
⊢ Ⅎx(℩xφ) | ||
Theorem | nfiotadxy 4797* | Deduction version of nfiotaxy 4798. (Contributed by Jim Kingdon, 21-Dec-2018.) |
⊢ Ⅎyφ & ⊢ (φ → Ⅎxψ) ⇒ ⊢ (φ → Ⅎx(℩yψ)) | ||
Theorem | nfiotaxy 4798* | Bound-variable hypothesis builder for the ℩ class. (Contributed by NM, 23-Aug-2011.) |
⊢ Ⅎxφ ⇒ ⊢ Ⅎx(℩yφ) | ||
Theorem | cbviota 4799 | Change bound variables in a description binder. (Contributed by Andrew Salmon, 1-Aug-2011.) |
⊢ (x = y → (φ ↔ ψ)) & ⊢ Ⅎyφ & ⊢ Ⅎxψ ⇒ ⊢ (℩xφ) = (℩yψ) | ||
Theorem | cbviotav 4800* | Change bound variables in a description binder. (Contributed by Andrew Salmon, 1-Aug-2011.) |
⊢ (x = y → (φ ↔ ψ)) ⇒ ⊢ (℩xφ) = (℩yψ) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |