Home | Intuitionistic Logic Explorer Theorem List (p. 71 of 139) | < 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 | ||
In this section, we define the left and right injections of a disjoint union and prove their main properties. These injections are restrictions of the "template" functions inl and inr, which appear in most applications in the form (inl ↾ 𝐴) and (inr ↾ 𝐵). | ||
Syntax | cinl 7001 | Extend class notation to include left injection of a disjoint union. |
class inl | ||
Syntax | cinr 7002 | Extend class notation to include right injection of a disjoint union. |
class inr | ||
Definition | df-inl 7003 | Left injection of a disjoint union. (Contributed by Mario Carneiro, 21-Jun-2022.) |
⊢ inl = (𝑥 ∈ V ↦ 〈∅, 𝑥〉) | ||
Definition | df-inr 7004 | Right injection of a disjoint union. (Contributed by Mario Carneiro, 21-Jun-2022.) |
⊢ inr = (𝑥 ∈ V ↦ 〈1o, 𝑥〉) | ||
Theorem | djulclr 7005 | Left closure of disjoint union. (Contributed by Jim Kingdon, 21-Jun-2022.) (Revised by BJ, 6-Jul-2022.) |
⊢ (𝐶 ∈ 𝐴 → ((inl ↾ 𝐴)‘𝐶) ∈ (𝐴 ⊔ 𝐵)) | ||
Theorem | djurclr 7006 | Right closure of disjoint union. (Contributed by Jim Kingdon, 21-Jun-2022.) (Revised by BJ, 6-Jul-2022.) |
⊢ (𝐶 ∈ 𝐵 → ((inr ↾ 𝐵)‘𝐶) ∈ (𝐴 ⊔ 𝐵)) | ||
Theorem | djulcl 7007 | Left closure of disjoint union. (Contributed by Jim Kingdon, 21-Jun-2022.) |
⊢ (𝐶 ∈ 𝐴 → (inl‘𝐶) ∈ (𝐴 ⊔ 𝐵)) | ||
Theorem | djurcl 7008 | Right closure of disjoint union. (Contributed by Jim Kingdon, 21-Jun-2022.) |
⊢ (𝐶 ∈ 𝐵 → (inr‘𝐶) ∈ (𝐴 ⊔ 𝐵)) | ||
Theorem | djuf1olem 7009* | Lemma for djulf1o 7014 and djurf1o 7015. (Contributed by BJ and Jim Kingdon, 4-Jul-2022.) |
⊢ 𝑋 ∈ V & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 〈𝑋, 𝑥〉) ⇒ ⊢ 𝐹:𝐴–1-1-onto→({𝑋} × 𝐴) | ||
Theorem | djuf1olemr 7010* | Lemma for djulf1or 7012 and djurf1or 7013. For a version of this lemma with 𝐹 defined on 𝐴 and no restriction in the conclusion, see djuf1olem 7009. (Contributed by BJ and Jim Kingdon, 4-Jul-2022.) |
⊢ 𝑋 ∈ V & ⊢ 𝐹 = (𝑥 ∈ V ↦ 〈𝑋, 𝑥〉) ⇒ ⊢ (𝐹 ↾ 𝐴):𝐴–1-1-onto→({𝑋} × 𝐴) | ||
Theorem | djulclb 7011 | Left biconditional closure of disjoint union. (Contributed by Jim Kingdon, 2-Jul-2022.) |
⊢ (𝐶 ∈ 𝑉 → (𝐶 ∈ 𝐴 ↔ (inl‘𝐶) ∈ (𝐴 ⊔ 𝐵))) | ||
Theorem | djulf1or 7012 | The left injection function on all sets is one to one and onto. (Contributed by BJ and Jim Kingdon, 22-Jun-2022.) |
⊢ (inl ↾ 𝐴):𝐴–1-1-onto→({∅} × 𝐴) | ||
Theorem | djurf1or 7013 | The right injection function on all sets is one to one and onto. (Contributed by BJ and Jim Kingdon, 22-Jun-2022.) |
⊢ (inr ↾ 𝐴):𝐴–1-1-onto→({1o} × 𝐴) | ||
Theorem | djulf1o 7014 | The left injection function on all sets is one to one and onto. (Contributed by Jim Kingdon, 22-Jun-2022.) |
⊢ inl:V–1-1-onto→({∅} × V) | ||
Theorem | djurf1o 7015 | The right injection function on all sets is one to one and onto. (Contributed by Jim Kingdon, 22-Jun-2022.) |
⊢ inr:V–1-1-onto→({1o} × V) | ||
Theorem | inresflem 7016* | Lemma for inlresf1 7017 and inrresf1 7018. (Contributed by BJ, 4-Jul-2022.) |
⊢ 𝐹:𝐴–1-1-onto→({𝑋} × 𝐴) & ⊢ (𝑥 ∈ 𝐴 → (𝐹‘𝑥) ∈ 𝐵) ⇒ ⊢ 𝐹:𝐴–1-1→𝐵 | ||
Theorem | inlresf1 7017 | The left injection restricted to the left class of a disjoint union is an injective function from the left class into the disjoint union. (Contributed by AV, 28-Jun-2022.) |
⊢ (inl ↾ 𝐴):𝐴–1-1→(𝐴 ⊔ 𝐵) | ||
Theorem | inrresf1 7018 | The right injection restricted to the right class of a disjoint union is an injective function from the right class into the disjoint union. (Contributed by AV, 28-Jun-2022.) |
⊢ (inr ↾ 𝐵):𝐵–1-1→(𝐴 ⊔ 𝐵) | ||
Theorem | djuinr 7019 | The ranges of any left and right injections are disjoint. Remark: the extra generality offered by the two restrictions makes the theorem more readily usable (e.g., by djudom 7049 and djufun 7060) while the simpler statement ⊢ (ran inl ∩ ran inr) = ∅ is easily recovered from it by substituting V for both 𝐴 and 𝐵 as done in casefun 7041). (Contributed by BJ and Jim Kingdon, 21-Jun-2022.) |
⊢ (ran (inl ↾ 𝐴) ∩ ran (inr ↾ 𝐵)) = ∅ | ||
Theorem | djuin 7020 | The images of any classes under right and left injection produce disjoint sets. (Contributed by Jim Kingdon, 21-Jun-2022.) (Proof shortened by BJ, 9-Jul-2023.) |
⊢ ((inl “ 𝐴) ∩ (inr “ 𝐵)) = ∅ | ||
Theorem | inl11 7021 | Left injection is one-to-one. (Contributed by Jim Kingdon, 12-Jul-2023.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ((inl‘𝐴) = (inl‘𝐵) ↔ 𝐴 = 𝐵)) | ||
Theorem | djuunr 7022 | The disjoint union of two classes is the union of the images of those two classes under right and left injection. (Contributed by Jim Kingdon, 22-Jun-2022.) (Proof shortened by BJ, 6-Jul-2022.) |
⊢ (ran (inl ↾ 𝐴) ∪ ran (inr ↾ 𝐵)) = (𝐴 ⊔ 𝐵) | ||
Theorem | djuun 7023 | The disjoint union of two classes is the union of the images of those two classes under right and left injection. (Contributed by Jim Kingdon, 22-Jun-2022.) (Proof shortened by BJ, 9-Jul-2023.) |
⊢ ((inl “ 𝐴) ∪ (inr “ 𝐵)) = (𝐴 ⊔ 𝐵) | ||
Theorem | eldju 7024* | Element of a disjoint union. (Contributed by BJ and Jim Kingdon, 23-Jun-2022.) |
⊢ (𝐶 ∈ (𝐴 ⊔ 𝐵) ↔ (∃𝑥 ∈ 𝐴 𝐶 = ((inl ↾ 𝐴)‘𝑥) ∨ ∃𝑥 ∈ 𝐵 𝐶 = ((inr ↾ 𝐵)‘𝑥))) | ||
Theorem | djur 7025* | A member of a disjoint union can be mapped from one of the classes which produced it. (Contributed by Jim Kingdon, 23-Jun-2022.) Upgrade implication to biconditional and shorten proof. (Revised by BJ, 14-Jul-2023.) |
⊢ (𝐶 ∈ (𝐴 ⊔ 𝐵) ↔ (∃𝑥 ∈ 𝐴 𝐶 = (inl‘𝑥) ∨ ∃𝑥 ∈ 𝐵 𝐶 = (inr‘𝑥))) | ||
Theorem | djuss 7026 | A disjoint union is a subset of a Cartesian product. (Contributed by AV, 25-Jun-2022.) |
⊢ (𝐴 ⊔ 𝐵) ⊆ ({∅, 1o} × (𝐴 ∪ 𝐵)) | ||
Theorem | eldju1st 7027 | The first component of an element of a disjoint union is either ∅ or 1o. (Contributed by AV, 26-Jun-2022.) |
⊢ (𝑋 ∈ (𝐴 ⊔ 𝐵) → ((1st ‘𝑋) = ∅ ∨ (1st ‘𝑋) = 1o)) | ||
Theorem | eldju2ndl 7028 | The second component of an element of a disjoint union is an element of the left class of the disjoint union if its first component is the empty set. (Contributed by AV, 26-Jun-2022.) |
⊢ ((𝑋 ∈ (𝐴 ⊔ 𝐵) ∧ (1st ‘𝑋) = ∅) → (2nd ‘𝑋) ∈ 𝐴) | ||
Theorem | eldju2ndr 7029 | The second component of an element of a disjoint union is an element of the right class of the disjoint union if its first component is not the empty set. (Contributed by AV, 26-Jun-2022.) |
⊢ ((𝑋 ∈ (𝐴 ⊔ 𝐵) ∧ (1st ‘𝑋) ≠ ∅) → (2nd ‘𝑋) ∈ 𝐵) | ||
Theorem | 1stinl 7030 | The first component of the value of a left injection is the empty set. (Contributed by AV, 27-Jun-2022.) |
⊢ (𝑋 ∈ 𝑉 → (1st ‘(inl‘𝑋)) = ∅) | ||
Theorem | 2ndinl 7031 | The second component of the value of a left injection is its argument. (Contributed by AV, 27-Jun-2022.) |
⊢ (𝑋 ∈ 𝑉 → (2nd ‘(inl‘𝑋)) = 𝑋) | ||
Theorem | 1stinr 7032 | The first component of the value of a right injection is 1o. (Contributed by AV, 27-Jun-2022.) |
⊢ (𝑋 ∈ 𝑉 → (1st ‘(inr‘𝑋)) = 1o) | ||
Theorem | 2ndinr 7033 | The second component of the value of a right injection is its argument. (Contributed by AV, 27-Jun-2022.) |
⊢ (𝑋 ∈ 𝑉 → (2nd ‘(inr‘𝑋)) = 𝑋) | ||
Theorem | djune 7034 | Left and right injection never produce equal values. (Contributed by Jim Kingdon, 2-Jul-2022.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (inl‘𝐴) ≠ (inr‘𝐵)) | ||
Theorem | updjudhf 7035* | The mapping of an element of the disjoint union to the value of the corresponding function is a function. (Contributed by AV, 26-Jun-2022.) |
⊢ (𝜑 → 𝐹:𝐴⟶𝐶) & ⊢ (𝜑 → 𝐺:𝐵⟶𝐶) & ⊢ 𝐻 = (𝑥 ∈ (𝐴 ⊔ 𝐵) ↦ if((1st ‘𝑥) = ∅, (𝐹‘(2nd ‘𝑥)), (𝐺‘(2nd ‘𝑥)))) ⇒ ⊢ (𝜑 → 𝐻:(𝐴 ⊔ 𝐵)⟶𝐶) | ||
Theorem | updjudhcoinlf 7036* | The composition of the mapping of an element of the disjoint union to the value of the corresponding function and the left injection equals the first function. (Contributed by AV, 27-Jun-2022.) |
⊢ (𝜑 → 𝐹:𝐴⟶𝐶) & ⊢ (𝜑 → 𝐺:𝐵⟶𝐶) & ⊢ 𝐻 = (𝑥 ∈ (𝐴 ⊔ 𝐵) ↦ if((1st ‘𝑥) = ∅, (𝐹‘(2nd ‘𝑥)), (𝐺‘(2nd ‘𝑥)))) ⇒ ⊢ (𝜑 → (𝐻 ∘ (inl ↾ 𝐴)) = 𝐹) | ||
Theorem | updjudhcoinrg 7037* | The composition of the mapping of an element of the disjoint union to the value of the corresponding function and the right injection equals the second function. (Contributed by AV, 27-Jun-2022.) |
⊢ (𝜑 → 𝐹:𝐴⟶𝐶) & ⊢ (𝜑 → 𝐺:𝐵⟶𝐶) & ⊢ 𝐻 = (𝑥 ∈ (𝐴 ⊔ 𝐵) ↦ if((1st ‘𝑥) = ∅, (𝐹‘(2nd ‘𝑥)), (𝐺‘(2nd ‘𝑥)))) ⇒ ⊢ (𝜑 → (𝐻 ∘ (inr ↾ 𝐵)) = 𝐺) | ||
Theorem | updjud 7038* | Universal property of the disjoint union. (Proposed by BJ, 25-Jun-2022.) (Contributed by AV, 28-Jun-2022.) |
⊢ (𝜑 → 𝐹:𝐴⟶𝐶) & ⊢ (𝜑 → 𝐺:𝐵⟶𝐶) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) ⇒ ⊢ (𝜑 → ∃!ℎ(ℎ:(𝐴 ⊔ 𝐵)⟶𝐶 ∧ (ℎ ∘ (inl ↾ 𝐴)) = 𝐹 ∧ (ℎ ∘ (inr ↾ 𝐵)) = 𝐺)) | ||
Syntax | cdjucase 7039 | Syntax for the "case" construction. |
class case(𝑅, 𝑆) | ||
Definition | df-case 7040 | The "case" construction: if 𝐹:𝐴⟶𝑋 and 𝐺:𝐵⟶𝑋 are functions, then case(𝐹, 𝐺):(𝐴 ⊔ 𝐵)⟶𝑋 is the natural function obtained by a definition by cases, hence the name. It is the unique function whose existence is asserted by the universal property of disjoint unions updjud 7038. The definition is adapted to make sense also for binary relations (where the universal property also holds). (Contributed by MC and BJ, 10-Jul-2022.) |
⊢ case(𝑅, 𝑆) = ((𝑅 ∘ ◡inl) ∪ (𝑆 ∘ ◡inr)) | ||
Theorem | casefun 7041 | The "case" construction of two functions is a function. (Contributed by BJ, 10-Jul-2022.) |
⊢ (𝜑 → Fun 𝐹) & ⊢ (𝜑 → Fun 𝐺) ⇒ ⊢ (𝜑 → Fun case(𝐹, 𝐺)) | ||
Theorem | casedm 7042 | The domain of the "case" construction is the disjoint union of the domains. TODO (although less important): ⊢ ran case(𝐹, 𝐺) = (ran 𝐹 ∪ ran 𝐺). (Contributed by BJ, 10-Jul-2022.) |
⊢ dom case(𝐹, 𝐺) = (dom 𝐹 ⊔ dom 𝐺) | ||
Theorem | caserel 7043 | The "case" construction of two relations is a relation, with bounds on its domain and codomain. Typically, the "case" construction is used when both relations have a common codomain. (Contributed by BJ, 10-Jul-2022.) |
⊢ case(𝑅, 𝑆) ⊆ ((dom 𝑅 ⊔ dom 𝑆) × (ran 𝑅 ∪ ran 𝑆)) | ||
Theorem | casef 7044 | The "case" construction of two functions is a function on the disjoint union of their domains. (Contributed by BJ, 10-Jul-2022.) |
⊢ (𝜑 → 𝐹:𝐴⟶𝑋) & ⊢ (𝜑 → 𝐺:𝐵⟶𝑋) ⇒ ⊢ (𝜑 → case(𝐹, 𝐺):(𝐴 ⊔ 𝐵)⟶𝑋) | ||
Theorem | caseinj 7045 | The "case" construction of two injective relations with disjoint ranges is an injective relation. (Contributed by BJ, 10-Jul-2022.) |
⊢ (𝜑 → Fun ◡𝑅) & ⊢ (𝜑 → Fun ◡𝑆) & ⊢ (𝜑 → (ran 𝑅 ∩ ran 𝑆) = ∅) ⇒ ⊢ (𝜑 → Fun ◡case(𝑅, 𝑆)) | ||
Theorem | casef1 7046 | The "case" construction of two injective functions with disjoint ranges is an injective function. (Contributed by BJ, 10-Jul-2022.) |
⊢ (𝜑 → 𝐹:𝐴–1-1→𝑋) & ⊢ (𝜑 → 𝐺:𝐵–1-1→𝑋) & ⊢ (𝜑 → (ran 𝐹 ∩ ran 𝐺) = ∅) ⇒ ⊢ (𝜑 → case(𝐹, 𝐺):(𝐴 ⊔ 𝐵)–1-1→𝑋) | ||
Theorem | caseinl 7047 | Applying the "case" construction to a left injection. (Contributed by Jim Kingdon, 15-Mar-2023.) |
⊢ (𝜑 → 𝐹 Fn 𝐵) & ⊢ (𝜑 → Fun 𝐺) & ⊢ (𝜑 → 𝐴 ∈ 𝐵) ⇒ ⊢ (𝜑 → (case(𝐹, 𝐺)‘(inl‘𝐴)) = (𝐹‘𝐴)) | ||
Theorem | caseinr 7048 | Applying the "case" construction to a right injection. (Contributed by Jim Kingdon, 12-Jul-2023.) |
⊢ (𝜑 → Fun 𝐹) & ⊢ (𝜑 → 𝐺 Fn 𝐵) & ⊢ (𝜑 → 𝐴 ∈ 𝐵) ⇒ ⊢ (𝜑 → (case(𝐹, 𝐺)‘(inr‘𝐴)) = (𝐺‘𝐴)) | ||
Theorem | djudom 7049 | Dominance law for disjoint union. (Contributed by Jim Kingdon, 25-Jul-2022.) |
⊢ ((𝐴 ≼ 𝐵 ∧ 𝐶 ≼ 𝐷) → (𝐴 ⊔ 𝐶) ≼ (𝐵 ⊔ 𝐷)) | ||
Theorem | omp1eomlem 7050* | Lemma for omp1eom 7051. (Contributed by Jim Kingdon, 11-Jul-2023.) |
⊢ 𝐹 = (𝑥 ∈ ω ↦ if(𝑥 = ∅, (inr‘𝑥), (inl‘∪ 𝑥))) & ⊢ 𝑆 = (𝑥 ∈ ω ↦ suc 𝑥) & ⊢ 𝐺 = case(𝑆, ( I ↾ 1o)) ⇒ ⊢ 𝐹:ω–1-1-onto→(ω ⊔ 1o) | ||
Theorem | omp1eom 7051 | Adding one to ω. (Contributed by Jim Kingdon, 10-Jul-2023.) |
⊢ (ω ⊔ 1o) ≈ ω | ||
Theorem | endjusym 7052 | Reversing right and left operands of a disjoint union produces an equinumerous result. (Contributed by Jim Kingdon, 10-Jul-2023.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ⊔ 𝐵) ≈ (𝐵 ⊔ 𝐴)) | ||
Theorem | eninl 7053 | Equinumerosity of a set and its image under left injection. (Contributed by Jim Kingdon, 30-Jul-2023.) |
⊢ (𝐴 ∈ 𝑉 → (inl “ 𝐴) ≈ 𝐴) | ||
Theorem | eninr 7054 | Equinumerosity of a set and its image under right injection. (Contributed by Jim Kingdon, 30-Jul-2023.) |
⊢ (𝐴 ∈ 𝑉 → (inr “ 𝐴) ≈ 𝐴) | ||
Theorem | difinfsnlem 7055* | Lemma for difinfsn 7056. The case where we need to swap 𝐵 and (inr‘∅) in building the mapping 𝐺. (Contributed by Jim Kingdon, 9-Aug-2023.) |
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦) & ⊢ (𝜑 → 𝐵 ∈ 𝐴) & ⊢ (𝜑 → 𝐹:(ω ⊔ 1o)–1-1→𝐴) & ⊢ (𝜑 → (𝐹‘(inr‘∅)) ≠ 𝐵) & ⊢ 𝐺 = (𝑛 ∈ ω ↦ if((𝐹‘(inl‘𝑛)) = 𝐵, (𝐹‘(inr‘∅)), (𝐹‘(inl‘𝑛)))) ⇒ ⊢ (𝜑 → 𝐺:ω–1-1→(𝐴 ∖ {𝐵})) | ||
Theorem | difinfsn 7056* | An infinite set minus one element is infinite. We require that the set has decidable equality. (Contributed by Jim Kingdon, 8-Aug-2023.) |
⊢ ((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ ω ≼ 𝐴 ∧ 𝐵 ∈ 𝐴) → ω ≼ (𝐴 ∖ {𝐵})) | ||
Theorem | difinfinf 7057* | An infinite set minus a finite subset is infinite. We require that the set has decidable equality. (Contributed by Jim Kingdon, 8-Aug-2023.) |
⊢ (((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ ω ≼ 𝐴) ∧ (𝐵 ⊆ 𝐴 ∧ 𝐵 ∈ Fin)) → ω ≼ (𝐴 ∖ 𝐵)) | ||
Syntax | cdjud 7058 | Syntax for the domain-disjoint-union of two relations. |
class (𝑅 ⊔d 𝑆) | ||
Definition | df-djud 7059 |
The "domain-disjoint-union" of two relations: if 𝑅 ⊆ (𝐴 × 𝑋) and
𝑆
⊆ (𝐵 × 𝑋) are two binary
relations, then (𝑅 ⊔d 𝑆) is the
binary relation from (𝐴 ⊔ 𝐵) to 𝑋 having the universal
property of disjoint unions (see updjud 7038 in the case of functions).
Remark: the restrictions to dom 𝑅 (resp. dom 𝑆) are not necessary since extra stuff would be thrown away in the post-composition with 𝑅 (resp. 𝑆), as in df-case 7040, but they are explicitly written for clarity. (Contributed by MC and BJ, 10-Jul-2022.) |
⊢ (𝑅 ⊔d 𝑆) = ((𝑅 ∘ ◡(inl ↾ dom 𝑅)) ∪ (𝑆 ∘ ◡(inr ↾ dom 𝑆))) | ||
Theorem | djufun 7060 | The "domain-disjoint-union" of two functions is a function. (Contributed by BJ, 10-Jul-2022.) |
⊢ (𝜑 → Fun 𝐹) & ⊢ (𝜑 → Fun 𝐺) ⇒ ⊢ (𝜑 → Fun (𝐹 ⊔d 𝐺)) | ||
Theorem | djudm 7061 | The domain of the "domain-disjoint-union" is the disjoint union of the domains. Remark: its range is the (standard) union of the ranges. (Contributed by BJ, 10-Jul-2022.) |
⊢ dom (𝐹 ⊔d 𝐺) = (dom 𝐹 ⊔ dom 𝐺) | ||
Theorem | djuinj 7062 | The "domain-disjoint-union" of two injective relations with disjoint ranges is an injective relation. (Contributed by BJ, 10-Jul-2022.) |
⊢ (𝜑 → Fun ◡𝑅) & ⊢ (𝜑 → Fun ◡𝑆) & ⊢ (𝜑 → (ran 𝑅 ∩ ran 𝑆) = ∅) ⇒ ⊢ (𝜑 → Fun ◡(𝑅 ⊔d 𝑆)) | ||
Theorem | 0ct 7063 | The empty set is countable. Remark of [BauerSwan], p. 14:3 which also has the definition of countable used here. (Contributed by Jim Kingdon, 13-Mar-2023.) |
⊢ ∃𝑓 𝑓:ω–onto→(∅ ⊔ 1o) | ||
Theorem | ctmlemr 7064* | Lemma for ctm 7065. One of the directions of the biconditional. (Contributed by Jim Kingdon, 16-Mar-2023.) |
⊢ (∃𝑥 𝑥 ∈ 𝐴 → (∃𝑓 𝑓:ω–onto→𝐴 → ∃𝑓 𝑓:ω–onto→(𝐴 ⊔ 1o))) | ||
Theorem | ctm 7065* | Two equivalent definitions of countable for an inhabited set. Remark of [BauerSwan], p. 14:3. (Contributed by Jim Kingdon, 13-Mar-2023.) |
⊢ (∃𝑥 𝑥 ∈ 𝐴 → (∃𝑓 𝑓:ω–onto→(𝐴 ⊔ 1o) ↔ ∃𝑓 𝑓:ω–onto→𝐴)) | ||
Theorem | ctssdclemn0 7066* | Lemma for ctssdc 7069. The ¬ ∅ ∈ 𝑆 case. (Contributed by Jim Kingdon, 16-Aug-2023.) |
⊢ (𝜑 → 𝑆 ⊆ ω) & ⊢ (𝜑 → ∀𝑛 ∈ ω DECID 𝑛 ∈ 𝑆) & ⊢ (𝜑 → 𝐹:𝑆–onto→𝐴) & ⊢ (𝜑 → ¬ ∅ ∈ 𝑆) ⇒ ⊢ (𝜑 → ∃𝑔 𝑔:ω–onto→(𝐴 ⊔ 1o)) | ||
Theorem | ctssdccl 7067* | A mapping from a decidable subset of the natural numbers onto a countable set. This is similar to one direction of ctssdc 7069 but expressed in terms of classes rather than ∃. (Contributed by Jim Kingdon, 30-Oct-2023.) |
⊢ (𝜑 → 𝐹:ω–onto→(𝐴 ⊔ 1o)) & ⊢ 𝑆 = {𝑥 ∈ ω ∣ (𝐹‘𝑥) ∈ (inl “ 𝐴)} & ⊢ 𝐺 = (◡inl ∘ 𝐹) ⇒ ⊢ (𝜑 → (𝑆 ⊆ ω ∧ 𝐺:𝑆–onto→𝐴 ∧ ∀𝑛 ∈ ω DECID 𝑛 ∈ 𝑆)) | ||
Theorem | ctssdclemr 7068* | Lemma for ctssdc 7069. Showing that our usual definition of countable implies the alternate one. (Contributed by Jim Kingdon, 16-Aug-2023.) |
⊢ (∃𝑓 𝑓:ω–onto→(𝐴 ⊔ 1o) → ∃𝑠(𝑠 ⊆ ω ∧ ∃𝑓 𝑓:𝑠–onto→𝐴 ∧ ∀𝑛 ∈ ω DECID 𝑛 ∈ 𝑠)) | ||
Theorem | ctssdc 7069* | A set is countable iff there is a surjection from a decidable subset of the natural numbers onto it. The decidability condition is needed as shown at ctssexmid 7105. (Contributed by Jim Kingdon, 15-Aug-2023.) |
⊢ (∃𝑠(𝑠 ⊆ ω ∧ ∃𝑓 𝑓:𝑠–onto→𝐴 ∧ ∀𝑛 ∈ ω DECID 𝑛 ∈ 𝑠) ↔ ∃𝑓 𝑓:ω–onto→(𝐴 ⊔ 1o)) | ||
Theorem | enumctlemm 7070* | Lemma for enumct 7071. The case where 𝑁 is greater than zero. (Contributed by Jim Kingdon, 13-Mar-2023.) |
⊢ (𝜑 → 𝐹:𝑁–onto→𝐴) & ⊢ (𝜑 → 𝑁 ∈ ω) & ⊢ (𝜑 → ∅ ∈ 𝑁) & ⊢ 𝐺 = (𝑘 ∈ ω ↦ if(𝑘 ∈ 𝑁, (𝐹‘𝑘), (𝐹‘∅))) ⇒ ⊢ (𝜑 → 𝐺:ω–onto→𝐴) | ||
Theorem | enumct 7071* | A finitely enumerable set is countable. Lemma 8.1.14 of [AczelRathjen], p. 73 (except that our definition of countable does not require the set to be inhabited). "Finitely enumerable" is defined as ∃𝑛 ∈ ω∃𝑓𝑓:𝑛–onto→𝐴 per Definition 8.1.4 of [AczelRathjen], p. 71 and "countable" is defined as ∃𝑔𝑔:ω–onto→(𝐴 ⊔ 1o) per [BauerSwan], p. 14:3. (Contributed by Jim Kingdon, 13-Mar-2023.) |
⊢ (∃𝑛 ∈ ω ∃𝑓 𝑓:𝑛–onto→𝐴 → ∃𝑔 𝑔:ω–onto→(𝐴 ⊔ 1o)) | ||
Theorem | finct 7072* | A finite set is countable. (Contributed by Jim Kingdon, 17-Mar-2023.) |
⊢ (𝐴 ∈ Fin → ∃𝑔 𝑔:ω–onto→(𝐴 ⊔ 1o)) | ||
Theorem | omct 7073 | ω is countable. (Contributed by Jim Kingdon, 23-Dec-2023.) |
⊢ ∃𝑓 𝑓:ω–onto→(ω ⊔ 1o) | ||
Theorem | ctfoex 7074* | A countable class is a set. (Contributed by Jim Kingdon, 25-Dec-2023.) |
⊢ (∃𝑓 𝑓:ω–onto→(𝐴 ⊔ 1o) → 𝐴 ∈ V) | ||
This section introduces the one-point compactification of the set of natural numbers, introduced by Escardo as the set of nonincreasing sequences on ω with values in 2o. The topological results justifying its name will be proved later. | ||
Syntax | xnninf 7075 | Set of nonincreasing sequences in 2o ↑𝑚 ω. |
class ℕ∞ | ||
Definition | df-nninf 7076* | Define the set of nonincreasing sequences in 2o ↑𝑚 ω. Definition in Section 3.1 of [Pierik], p. 15. If we assumed excluded middle, this would be essentially the same as ℕ0* as defined at df-xnn0 9169 but in its absence the relationship between the two is more complicated. This definition would function much the same whether we used ω or ℕ0, but the former allows us to take advantage of 2o = {∅, 1o} (df2o3 6389) so we adopt it. (Contributed by Jim Kingdon, 14-Jul-2022.) |
⊢ ℕ∞ = {𝑓 ∈ (2o ↑𝑚 ω) ∣ ∀𝑖 ∈ ω (𝑓‘suc 𝑖) ⊆ (𝑓‘𝑖)} | ||
Theorem | nninfex 7077 | ℕ∞ is a set. (Contributed by Jim Kingdon, 10-Aug-2022.) |
⊢ ℕ∞ ∈ V | ||
Theorem | nninff 7078 | An element of ℕ∞ is a sequence of zeroes and ones. (Contributed by Jim Kingdon, 4-Aug-2022.) |
⊢ (𝐴 ∈ ℕ∞ → 𝐴:ω⟶2o) | ||
Theorem | infnninf 7079 | The point at infinity in ℕ∞ is the constant sequence equal to 1o. Note that with our encoding of functions, that constant function can also be expressed as (ω × {1o}), as fconstmpt 4645 shows. (Contributed by Jim Kingdon, 14-Jul-2022.) Use maps-to notation. (Revised by BJ, 10-Aug-2024.) |
⊢ (𝑖 ∈ ω ↦ 1o) ∈ ℕ∞ | ||
Theorem | infnninfOLD 7080 | Obsolete version of infnninf 7079 as of 10-Aug-2024. (Contributed by Jim Kingdon, 14-Jul-2022.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (ω × {1o}) ∈ ℕ∞ | ||
Theorem | nnnninf 7081* | Elements of ℕ∞ corresponding to natural numbers. The natural number 𝑁 corresponds to a sequence of 𝑁 ones followed by zeroes. This can be strengthened to include infinity, see nnnninf2 7082. (Contributed by Jim Kingdon, 14-Jul-2022.) |
⊢ (𝑁 ∈ ω → (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅)) ∈ ℕ∞) | ||
Theorem | nnnninf2 7082* | Canonical embedding of suc ω into ℕ∞. (Contributed by BJ, 10-Aug-2024.) |
⊢ (𝑁 ∈ suc ω → (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅)) ∈ ℕ∞) | ||
Theorem | nnnninfeq 7083* | Mapping of a natural number to an element of ℕ∞. (Contributed by Jim Kingdon, 4-Aug-2022.) |
⊢ (𝜑 → 𝑃 ∈ ℕ∞) & ⊢ (𝜑 → 𝑁 ∈ ω) & ⊢ (𝜑 → ∀𝑥 ∈ 𝑁 (𝑃‘𝑥) = 1o) & ⊢ (𝜑 → (𝑃‘𝑁) = ∅) ⇒ ⊢ (𝜑 → 𝑃 = (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅))) | ||
Theorem | nnnninfeq2 7084* | Mapping of a natural number to an element of ℕ∞. Similar to nnnninfeq 7083 but if we have information about a single 1o digit, that gives information about all previous digits. (Contributed by Jim Kingdon, 4-Aug-2022.) |
⊢ (𝜑 → 𝑃 ∈ ℕ∞) & ⊢ (𝜑 → 𝑁 ∈ ω) & ⊢ (𝜑 → (𝑃‘∪ 𝑁) = 1o) & ⊢ (𝜑 → (𝑃‘𝑁) = ∅) ⇒ ⊢ (𝜑 → 𝑃 = (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅))) | ||
Theorem | nninfisollem0 7085* | Lemma for nninfisol 7088. The case where 𝑁 is zero. (Contributed by Jim Kingdon, 13-Sep-2024.) |
⊢ (𝜑 → 𝑋 ∈ ℕ∞) & ⊢ (𝜑 → (𝑋‘𝑁) = ∅) & ⊢ (𝜑 → 𝑁 ∈ ω) & ⊢ (𝜑 → 𝑁 = ∅) ⇒ ⊢ (𝜑 → DECID (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅)) = 𝑋) | ||
Theorem | nninfisollemne 7086* | Lemma for nninfisol 7088. A case where 𝑁 is a successor and 𝑁 and 𝑋 are not equal. (Contributed by Jim Kingdon, 13-Sep-2024.) |
⊢ (𝜑 → 𝑋 ∈ ℕ∞) & ⊢ (𝜑 → (𝑋‘𝑁) = ∅) & ⊢ (𝜑 → 𝑁 ∈ ω) & ⊢ (𝜑 → 𝑁 ≠ ∅) & ⊢ (𝜑 → (𝑋‘∪ 𝑁) = ∅) ⇒ ⊢ (𝜑 → DECID (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅)) = 𝑋) | ||
Theorem | nninfisollemeq 7087* | Lemma for nninfisol 7088. The case where 𝑁 is a successor and 𝑁 and 𝑋 are equal. (Contributed by Jim Kingdon, 13-Sep-2024.) |
⊢ (𝜑 → 𝑋 ∈ ℕ∞) & ⊢ (𝜑 → (𝑋‘𝑁) = ∅) & ⊢ (𝜑 → 𝑁 ∈ ω) & ⊢ (𝜑 → 𝑁 ≠ ∅) & ⊢ (𝜑 → (𝑋‘∪ 𝑁) = 1o) ⇒ ⊢ (𝜑 → DECID (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅)) = 𝑋) | ||
Theorem | nninfisol 7088* | Finite elements of ℕ∞ are isolated. That is, given a natural number and any element of ℕ∞, it is decidable whether the natural number (when converted to an element of ℕ∞) is equal to the given element of ℕ∞. Stated in an online post by Martin Escardo. One way to understand this theorem is that you do not need to look at an unbounded number of elements of the sequence 𝑋 to decide whether it is equal to 𝑁 (in fact, you only need to look at two elements and 𝑁 tells you where to look). (Contributed by BJ and Jim Kingdon, 12-Sep-2024.) |
⊢ ((𝑁 ∈ ω ∧ 𝑋 ∈ ℕ∞) → DECID (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅)) = 𝑋) | ||
Syntax | comni 7089 | Extend class definition to include the class of omniscient sets. |
class Omni | ||
Definition | df-omni 7090* |
An omniscient set is one where we can decide whether a predicate (here
represented by a function 𝑓) holds (is equal to 1o) for all
elements or fails to hold (is equal to ∅)
for some element.
Definition 3.1 of [Pierik], p. 14.
In particular, ω ∈ Omni is known as the Limited Principle of Omniscience (LPO). (Contributed by Jim Kingdon, 28-Jun-2022.) |
⊢ Omni = {𝑦 ∣ ∀𝑓(𝑓:𝑦⟶2o → (∃𝑥 ∈ 𝑦 (𝑓‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝑦 (𝑓‘𝑥) = 1o))} | ||
Theorem | isomni 7091* | The predicate of being omniscient. (Contributed by Jim Kingdon, 28-Jun-2022.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ Omni ↔ ∀𝑓(𝑓:𝐴⟶2o → (∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o)))) | ||
Theorem | isomnimap 7092* | The predicate of being omniscient stated in terms of set exponentiation. (Contributed by Jim Kingdon, 13-Jul-2022.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ Omni ↔ ∀𝑓 ∈ (2o ↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o))) | ||
Theorem | enomnilem 7093 | Lemma for enomni 7094. One direction of the biconditional. (Contributed by Jim Kingdon, 13-Jul-2022.) |
⊢ (𝐴 ≈ 𝐵 → (𝐴 ∈ Omni → 𝐵 ∈ Omni)) | ||
Theorem | enomni 7094 | Omniscience is invariant with respect to equinumerosity. For example, this means that we can express the Limited Principle of Omniscience as either ω ∈ Omni or ℕ0 ∈ Omni. The former is a better match to conventional notation in the sense that df2o3 6389 says that 2o = {∅, 1o} whereas the corresponding relationship does not exist between 2 and {0, 1}. (Contributed by Jim Kingdon, 13-Jul-2022.) |
⊢ (𝐴 ≈ 𝐵 → (𝐴 ∈ Omni ↔ 𝐵 ∈ Omni)) | ||
Theorem | finomni 7095 | A finite set is omniscient. Remark right after Definition 3.1 of [Pierik], p. 14. (Contributed by Jim Kingdon, 28-Jun-2022.) |
⊢ (𝐴 ∈ Fin → 𝐴 ∈ Omni) | ||
Theorem | exmidomniim 7096 | Given excluded middle, every set is omniscient. Remark following Definition 3.1 of [Pierik], p. 14. This is one direction of the biconditional exmidomni 7097. (Contributed by Jim Kingdon, 29-Jun-2022.) |
⊢ (EXMID → ∀𝑥 𝑥 ∈ Omni) | ||
Theorem | exmidomni 7097 | Excluded middle is equivalent to every set being omniscient. (Contributed by BJ and Jim Kingdon, 30-Jun-2022.) |
⊢ (EXMID ↔ ∀𝑥 𝑥 ∈ Omni) | ||
Theorem | exmidlpo 7098 | Excluded middle implies the Limited Principle of Omniscience (LPO). (Contributed by Jim Kingdon, 29-Mar-2023.) |
⊢ (EXMID → ω ∈ Omni) | ||
Theorem | fodjuomnilemdc 7099* | Lemma for fodjuomni 7104. Decidability of a condition we use in various lemmas. (Contributed by Jim Kingdon, 27-Jul-2022.) |
⊢ (𝜑 → 𝐹:𝑂–onto→(𝐴 ⊔ 𝐵)) ⇒ ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑂) → DECID ∃𝑧 ∈ 𝐴 (𝐹‘𝑋) = (inl‘𝑧)) | ||
Theorem | fodjuf 7100* | Lemma for fodjuomni 7104 and fodjumkv 7115. Domain and range of 𝑃. (Contributed by Jim Kingdon, 27-Jul-2022.) (Revised by Jim Kingdon, 25-Mar-2023.) |
⊢ (𝜑 → 𝐹:𝑂–onto→(𝐴 ⊔ 𝐵)) & ⊢ 𝑃 = (𝑦 ∈ 𝑂 ↦ if(∃𝑧 ∈ 𝐴 (𝐹‘𝑦) = (inl‘𝑧), ∅, 1o)) & ⊢ (𝜑 → 𝑂 ∈ 𝑉) ⇒ ⊢ (𝜑 → 𝑃 ∈ (2o ↑𝑚 𝑂)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |