Intuitionistic Logic Explorer Most Recent Proofs |
||
Mirrors > Home > ILE Home > Th. List > Recent | MPE Most Recent Other > MM 100 |
See the MPE Most Recent Proofs page for news and some useful links.
Color key: | Intuitionistic Logic Explorer | User Mathboxes |
Date | Label | Description |
---|---|---|
Theorem | ||
29-Jul-2022 | fodjuomnilemres 6707 | Lemma for fodjuomni 6708. The final result with 𝑃 broken out into a hypothesis. (Contributed by Jim Kingdon, 29-Jul-2022.) |
⊢ (𝜑 → 𝑂 ∈ Omni) & ⊢ (𝜑 → 𝐹:𝑂–onto→(𝐴 ⊔ 𝐵)) & ⊢ 𝑃 = (𝑦 ∈ 𝑂 ↦ if(∃𝑧 ∈ 𝐴 (𝐹‘𝑦) = (inl‘𝑧), ∅, 1_{𝑜})) ⇒ ⊢ (𝜑 → (∃𝑥 𝑥 ∈ 𝐴 ∨ 𝐴 = ∅)) | ||
28-Jul-2022 | eqifdc 3404 | Expansion of an equality with a conditional operator. (Contributed by Jim Kingdon, 28-Jul-2022.) |
⊢ (DECID 𝜑 → (𝐴 = if(𝜑, 𝐵, 𝐶) ↔ ((𝜑 ∧ 𝐴 = 𝐵) ∨ (¬ 𝜑 ∧ 𝐴 = 𝐶)))) | ||
27-Jul-2022 | fodjuomni 6708 | A condition which ensures 𝐴 is either inhabited or empty. Lemma 3.2 of [PradicBrown2021], p. 4. (Contributed by Jim Kingdon, 27-Jul-2022.) |
⊢ (𝜑 → 𝑂 ∈ Omni) & ⊢ (𝜑 → 𝐹:𝑂–onto→(𝐴 ⊔ 𝐵)) ⇒ ⊢ (𝜑 → (∃𝑥 𝑥 ∈ 𝐴 ∨ 𝐴 = ∅)) | ||
27-Jul-2022 | fodjuomnilem0 6706 | Lemma for fodjuomni 6708. The case where A is empty. (Contributed by Jim Kingdon, 27-Jul-2022.) |
⊢ (𝜑 → 𝑂 ∈ Omni) & ⊢ (𝜑 → 𝐹:𝑂–onto→(𝐴 ⊔ 𝐵)) & ⊢ 𝑃 = (𝑦 ∈ 𝑂 ↦ if(∃𝑧 ∈ 𝐴 (𝐹‘𝑦) = (inl‘𝑧), ∅, 1_{𝑜})) & ⊢ (𝜑 → ∀𝑤 ∈ 𝑂 (𝑃‘𝑤) = 1_{𝑜}) ⇒ ⊢ (𝜑 → 𝐴 = ∅) | ||
27-Jul-2022 | fodjuomnilemm 6705 | Lemma for fodjuomni 6708. The case where A is inhabited. (Contributed by Jim Kingdon, 27-Jul-2022.) |
⊢ (𝜑 → 𝑂 ∈ Omni) & ⊢ (𝜑 → 𝐹:𝑂–onto→(𝐴 ⊔ 𝐵)) & ⊢ 𝑃 = (𝑦 ∈ 𝑂 ↦ if(∃𝑧 ∈ 𝐴 (𝐹‘𝑦) = (inl‘𝑧), ∅, 1_{𝑜})) & ⊢ (𝜑 → ∃𝑤 ∈ 𝑂 (𝑃‘𝑤) = ∅) ⇒ ⊢ (𝜑 → ∃𝑥 𝑥 ∈ 𝐴) | ||
27-Jul-2022 | fodjuomnilemf 6704 | Lemma for fodjuomni 6708. Domain and range of 𝑃. (Contributed by Jim Kingdon, 27-Jul-2022.) |
⊢ (𝜑 → 𝑂 ∈ Omni) & ⊢ (𝜑 → 𝐹:𝑂–onto→(𝐴 ⊔ 𝐵)) & ⊢ 𝑃 = (𝑦 ∈ 𝑂 ↦ if(∃𝑧 ∈ 𝐴 (𝐹‘𝑦) = (inl‘𝑧), ∅, 1_{𝑜})) ⇒ ⊢ (𝜑 → 𝑃 ∈ (2_{𝑜} ↑_{𝑚} 𝑂)) | ||
27-Jul-2022 | fodjuomnilemdc 6703 | Lemma for fodjuomni 6708. Decidability of a condition we use in various lemmas. (Contributed by Jim Kingdon, 27-Jul-2022.) |
⊢ (𝜑 → 𝐹:𝑂–onto→(𝐴 ⊔ 𝐵)) ⇒ ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑂) → DECID ∃𝑧 ∈ 𝐴 (𝐹‘𝑋) = (inl‘𝑧)) | ||
25-Jul-2022 | djudom 6693 | Dominance law for disjoint union. (Contributed by Jim Kingdon, 25-Jul-2022.) |
⊢ ((𝐴 ≼ 𝐵 ∧ 𝐶 ≼ 𝐷) → (𝐴 ⊔ 𝐶) ≼ (𝐵 ⊔ 𝐷)) | ||
17-Jul-2022 | inftonninf 9735 | The mapping of +∞ into ℕ_{∞} is the sequence of all ones. (Contributed by Jim Kingdon, 17-Jul-2022.) |
⊢ 𝐺 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0) & ⊢ 𝐹 = (𝑛 ∈ ω ↦ (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1_{𝑜}, ∅))) & ⊢ 𝐼 = ((𝐹 ∘ ^{◡}𝐺) ∪ {⟨+∞, (ω × {1_{𝑜}})⟩}) ⇒ ⊢ (𝐼‘+∞) = (𝑥 ∈ ω ↦ 1_{𝑜}) | ||
17-Jul-2022 | 1tonninf 9734 | The mapping of one into ℕ_{∞} is a sequence which is a one followed by zeroes. (Contributed by Jim Kingdon, 17-Jul-2022.) |
⊢ 𝐺 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0) & ⊢ 𝐹 = (𝑛 ∈ ω ↦ (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1_{𝑜}, ∅))) & ⊢ 𝐼 = ((𝐹 ∘ ^{◡}𝐺) ∪ {⟨+∞, (ω × {1_{𝑜}})⟩}) ⇒ ⊢ (𝐼‘1) = (𝑥 ∈ ω ↦ if(𝑥 = ∅, 1_{𝑜}, ∅)) | ||
17-Jul-2022 | 0tonninf 9733 | The mapping of zero into ℕ_{∞} is the sequence of all zeroes. (Contributed by Jim Kingdon, 17-Jul-2022.) |
⊢ 𝐺 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0) & ⊢ 𝐹 = (𝑛 ∈ ω ↦ (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1_{𝑜}, ∅))) & ⊢ 𝐼 = ((𝐹 ∘ ^{◡}𝐺) ∪ {⟨+∞, (ω × {1_{𝑜}})⟩}) ⇒ ⊢ (𝐼‘0) = (𝑥 ∈ ω ↦ ∅) | ||
16-Jul-2022 | fxnn0nninf 9732 | A function from ℕ_{0}^{*} into ℕ_{∞}. (Contributed by Jim Kingdon, 16-Jul-2022.) |
⊢ 𝐺 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0) & ⊢ 𝐹 = (𝑛 ∈ ω ↦ (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1_{𝑜}, ∅))) & ⊢ 𝐼 = ((𝐹 ∘ ^{◡}𝐺) ∪ {⟨+∞, (ω × {1_{𝑜}})⟩}) ⇒ ⊢ 𝐼:ℕ_{0}^{*}⟶ℕ_{∞} | ||
16-Jul-2022 | fnn0nninf 9731 | A function from ℕ_{0} into ℕ_{∞}. (Contributed by Jim Kingdon, 16-Jul-2022.) |
⊢ 𝐺 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0) & ⊢ 𝐹 = (𝑛 ∈ ω ↦ (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1_{𝑜}, ∅))) ⇒ ⊢ (𝐹 ∘ ^{◡}𝐺):ℕ_{0}⟶ℕ_{∞} | ||
15-Jul-2022 | mapdom1g 6492 | Order-preserving property of set exponentiation. (Contributed by Jim Kingdon, 15-Jul-2022.) |
⊢ ((𝐴 ≼ 𝐵 ∧ 𝐶 ∈ 𝑉) → (𝐴 ↑_{𝑚} 𝐶) ≼ (𝐵 ↑_{𝑚} 𝐶)) | ||
14-Jul-2022 | nnnninf 8644 | Elements of ℕ_{∞} corresponding to natural numbers. The natural number 𝑁 corresponds to a sequence of 𝑁 ones followed by zeroes. Contrast to a sequence which is all ones as seen at infnninf 8643. Remark/TODO: the theorem sill holds if 𝑁 = ω, that is, the antcedent could be weakened to 𝑁 ∈ suc ω. (Contributed by Jim Kingdon, 14-Jul-2022.) |
⊢ (𝑁 ∈ ω → (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1_{𝑜}, ∅)) ∈ ℕ_{∞}) | ||
14-Jul-2022 | infnninf 8643 | The point at infinity in ℕ_{∞} (the constant sequence equal to 1_{𝑜}). (Contributed by Jim Kingdon, 14-Jul-2022.) |
⊢ (ω × {1_{𝑜}}) ∈ ℕ_{∞} | ||
14-Jul-2022 | df-nninf 8630 | Define the set of non-increasing sequences in 2_{𝑜} ↑_{𝑚} ω. 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 8629 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 2_{𝑜} = {∅, 1_{𝑜}} (df2o3 6126) so we adopt it. (Contributed by Jim Kingdon, 14-Jul-2022.) |
⊢ ℕ_{∞} = {𝑓 ∈ (2_{𝑜} ↑_{𝑚} ω) ∣ ∀𝑖 ∈ ω (𝑓‘suc 𝑖) ⊆ (𝑓‘𝑖)} | ||
13-Jul-2022 | enomni 6699 | Omniscience is invariant with respect to equinumerosity. For example, this means that we can express the Lesser Principle of Omniscience as either ω ∈ Omni or ℕ_{0} ∈ Omni. The former is a better match to conventional notation in the sense that df2o3 6126 says that 2_{𝑜} = {∅, 1_{𝑜}} whereas the corresponding relationship does not exist between 2 and {0, 1}. (Contributed by Jim Kingdon, 13-Jul-2022.) |
⊢ (𝐴 ≈ 𝐵 → (𝐴 ∈ Omni ↔ 𝐵 ∈ Omni)) | ||
13-Jul-2022 | enomnilem 6698 | Lemma for enomni 6699. One direction of the biconditional. (Contributed by Jim Kingdon, 13-Jul-2022.) |
⊢ (𝐴 ≈ 𝐵 → (𝐴 ∈ Omni → 𝐵 ∈ Omni)) | ||
13-Jul-2022 | isomnimap 6697 | The predicate of being omniscient stated in terms of set exponentiation. (Contributed by Jim Kingdon, 13-Jul-2022.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ Omni ↔ ∀𝑓 ∈ (2_{𝑜} ↑_{𝑚} 𝐴)(∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1_{𝑜}))) | ||
12-Jul-2022 | finexdc 6544 | Decidability of existence, over a finite set and defined by a decidable proposition. (Contributed by Jim Kingdon, 12-Jul-2022.) |
⊢ ((𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 DECID 𝜑) → DECID ∃𝑥 ∈ 𝐴 𝜑) | ||
11-Jul-2022 | dfrex2fin 6545 | Relationship between universal and existential quantifiers over a finite set. Remark in Section 2.2.1 of [Pierik], p. 8. Although Pierik does not mention the decidability condition explicitly, it does say "only finitely many x to check" which means there must be some way of checking each value of x. (Contributed by Jim Kingdon, 11-Jul-2022.) |
⊢ ((𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 DECID 𝜑) → (∃𝑥 ∈ 𝐴 𝜑 ↔ ¬ ∀𝑥 ∈ 𝐴 ¬ 𝜑)) | ||
10-Jul-2022 | djuinj 6692 | 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} 𝑆)) | ||
10-Jul-2022 | djudm 6691 | 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 𝐺) | ||
10-Jul-2022 | djufun 6690 | The "domain-disjoint-union" of two functions is a function. (Contributed by BJ, 10-Jul-2022.) |
⊢ (𝜑 → Fun 𝐹) & ⊢ (𝜑 → Fun 𝐺) ⇒ ⊢ (𝜑 → Fun (𝐹 ⊔_{d} 𝐺)) | ||
10-Jul-2022 | df-djud 6689 |
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.
Remark: the restrictions to dom 𝑅 (resp. dom 𝑆) are not necessary since extra stuff would be thrown away in the post-composition with 𝑅 (resp. 𝑆), but they are explicitly written for clarity. (Contributed by MC and BJ, 10-Jul-2022.) |
⊢ (𝑅 ⊔_{d} 𝑆) = ((𝑅 ∘ ^{◡}(inl ↾ dom 𝑅)) ∪ (𝑆 ∘ ^{◡}(inr ↾ dom 𝑆))) | ||
10-Jul-2022 | casef1 6687 | 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→𝑋) | ||
10-Jul-2022 | caseinj 6686 | 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(𝑅, 𝑆)) | ||
10-Jul-2022 | casef 6685 | The "case" construction of two functions is a function on the disjoint union of their domains. (Contributed by BJ, 10-Jul-2022.) |
⊢ (𝜑 → 𝐹:𝐴⟶𝑋) & ⊢ (𝜑 → 𝐺:𝐵⟶𝑋) ⇒ ⊢ (𝜑 → case(𝐹, 𝐺):(𝐴 ⊔ 𝐵)⟶𝑋) | ||
10-Jul-2022 | caserel 6684 | 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 𝑆)) | ||
10-Jul-2022 | casedm 6683 | 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 𝐺) | ||
10-Jul-2022 | casefun 6682 | The "case" construction of two functions is a function. (Contributed by BJ, 10-Jul-2022.) |
⊢ (𝜑 → Fun 𝐹) & ⊢ (𝜑 → Fun 𝐺) ⇒ ⊢ (𝜑 → Fun case(𝐹, 𝐺)) | ||
10-Jul-2022 | df-case 6681 | 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. 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)) | ||
10-Jul-2022 | cocnvss 4909 | Upper bound for the composed of a relation and an inverse relation. (Contributed by BJ, 10-Jul-2022.) |
⊢ (𝑆 ∘ ^{◡}𝑅) ⊆ (ran (𝑅 ↾ dom 𝑆) × ran (𝑆 ↾ dom 𝑅)) | ||
10-Jul-2022 | cocnvres 4908 | Restricting a relation and a converse relation when they are composed together (Contributed by BJ, 10-Jul-2022.) |
⊢ (𝑆 ∘ ^{◡}𝑅) = ((𝑆 ↾ dom 𝑅) ∘ ^{◡}(𝑅 ↾ dom 𝑆)) | ||
10-Jul-2022 | cossxp2 4907 | The composition of two relations is a relation, with bounds on its domain and codomain. (Contributed by BJ, 10-Jul-2022.) |
⊢ (𝜑 → 𝑅 ⊆ (𝐴 × 𝐵)) & ⊢ (𝜑 → 𝑆 ⊆ (𝐵 × 𝐶)) ⇒ ⊢ (𝜑 → (𝑆 ∘ 𝑅) ⊆ (𝐴 × 𝐶)) | ||
10-Jul-2022 | rnxpss2 4817 | Upper bound for the range of a binary relation. (Contributed by BJ, 10-Jul-2022.) |
⊢ (𝑅 ⊆ (𝐴 × 𝐵) → ran 𝑅 ⊆ 𝐵) | ||
10-Jul-2022 | dmxpss2 4816 | Upper bound for the domain of a binary relation. (Contributed by BJ, 10-Jul-2022.) |
⊢ (𝑅 ⊆ (𝐴 × 𝐵) → dom 𝑅 ⊆ 𝐴) | ||
10-Jul-2022 | elco 4559 | Elements of a composed relation. (Contributed by BJ, 10-Jul-2022.) |
⊢ (𝐴 ∈ (𝑅 ∘ 𝑆) ↔ ∃𝑥∃𝑦∃𝑧(𝐴 = ⟨𝑥, 𝑧⟩ ∧ (𝑥𝑆𝑦 ∧ 𝑦𝑅𝑧))) | ||
9-Jul-2022 | exmidfodomrlemrALT 6731 | The existence of a mapping from any set onto any inhabited set that it dominates implies excluded middle. Proposition 1.2 of [PradicBrown2021], p. 2. An alternative proof of exmidfodomrlemr 6730. In particular, this proof uses eldju 6665 instead of djur 6663 and avoids djulclb 6653. (New usage is discouraged.) (Proof modification is discouraged.) (Contributed by Jim Kingdon, 9-Jul-2022.) |
⊢ (∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) → EXMID) | ||
9-Jul-2022 | exmidfodomrlemreseldju 6728 | Lemma for exmidfodomrlemrALT 6731. A variant of eldju 6665. (Contributed by Jim Kingdon, 9-Jul-2022.) |
⊢ (𝜑 → 𝐴 ⊆ 1_{𝑜}) & ⊢ (𝜑 → 𝐵 ∈ (𝐴 ⊔ 1_{𝑜})) ⇒ ⊢ (𝜑 → ((∅ ∈ 𝐴 ∧ 𝐵 = ((inl ↾ 𝐴)‘∅)) ∨ 𝐵 = ((inr ↾ 1_{𝑜})‘∅))) | ||
8-Jul-2022 | abn0m 3291 | Inhabited class abstraction. (Contributed by Jim Kingdon, 8-Jul-2022.) |
⊢ (∃𝑦 𝑦 ∈ {𝑥 ∣ 𝜑} ↔ ∃𝑥𝜑) | ||
7-Jul-2022 | fvco4 5320 | Value of a composition. (Contributed by BJ, 7-Jul-2022.) |
⊢ (((𝐾:𝐴⟶𝑋 ∧ (𝐻 ∘ 𝐾) = 𝐹) ∧ (𝑢 ∈ 𝐴 ∧ 𝑥 = (𝐾‘𝑢))) → (𝐻‘𝑥) = (𝐹‘𝑢)) | ||
6-Jul-2022 | djuun 6666 | 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.) |
⊢ ((inl “ 𝐴) ∪ (inr “ 𝐵)) = (𝐴 ⊔ 𝐵) | ||
6-Jul-2022 | djuunr 6664 | 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 ↾ 𝐵)) = (𝐴 ⊔ 𝐵) | ||
6-Jul-2022 | djurclr 6648 | Right closure of disjoint union. (Contributed by Jim Kingdon, 21-Jun-2022.) (Revised by BJ, 6-Jul-2022.) |
⊢ (𝐶 ∈ 𝐵 → ((inr ↾ 𝐵)‘𝐶) ∈ (𝐴 ⊔ 𝐵)) | ||
6-Jul-2022 | djulclr 6647 | Left closure of disjoint union. (Contributed by Jim Kingdon, 21-Jun-2022.) (Revised by BJ, 6-Jul-2022.) |
⊢ (𝐶 ∈ 𝐴 → ((inl ↾ 𝐴)‘𝐶) ∈ (𝐴 ⊔ 𝐵)) | ||
6-Jul-2022 | foelrn 5470 | Property of a surjective function. (Contributed by Jeff Madsen, 4-Jan-2011.) (Proof shortened by BJ, 6-Jul-2022.) |
⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝐶 ∈ 𝐵) → ∃𝑥 ∈ 𝐴 𝐶 = (𝐹‘𝑥)) | ||
6-Jul-2022 | foima2 5469 | Given an onto function, an element is in its codomain if and only if it is the image of an element of its domain (see foima 5185). (Contributed by BJ, 6-Jul-2022.) |
⊢ (𝐹:𝐴–onto→𝐵 → (𝑌 ∈ 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑌 = (𝐹‘𝑥))) | ||
6-Jul-2022 | f1rn 5164 | The range of a one-to-one mapping. (Contributed by BJ, 6-Jul-2022.) |
⊢ (𝐹:𝐴–1-1→𝐵 → ran 𝐹 ⊆ 𝐵) | ||
4-Jul-2022 | djurclALT 11044 | Shortening of djurcl 6650 using djucllem 11042. (Contributed by BJ, 4-Jul-2022.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝐶 ∈ 𝐵 → ((inr ↾ 𝐵)‘𝐶) ∈ (𝐴 ⊔ 𝐵)) | ||
4-Jul-2022 | djulclALT 11043 | Shortening of djulcl 6649 using djucllem 11042. (Contributed by BJ, 4-Jul-2022.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝐶 ∈ 𝐴 → ((inl ↾ 𝐴)‘𝐶) ∈ (𝐴 ⊔ 𝐵)) | ||
4-Jul-2022 | djucllem 11042 | Lemma for djulcl 6649 and djurcl 6650. (Contributed by BJ, 4-Jul-2022.) |
⊢ 𝑋 ∈ V & ⊢ 𝐹 = (𝑥 ∈ V ↦ ⟨𝑋, 𝑥⟩) ⇒ ⊢ (𝐴 ∈ 𝐵 → ((𝐹 ↾ 𝐵)‘𝐴) ∈ ({𝑋} × 𝐵)) | ||
4-Jul-2022 | inresflem 6658 | Lemma for inlresf1 6659 and inrresf1 6660. (Contributed by BJ, 4-Jul-2022.) |
⊢ 𝐹:𝐴–1-1-onto→({𝑋} × 𝐴) & ⊢ (𝑥 ∈ 𝐴 → (𝐹‘𝑥) ∈ 𝐵) ⇒ ⊢ 𝐹:𝐴–1-1→𝐵 | ||
4-Jul-2022 | djuf1olemr 6652 | Lemma for djulf1or 6654 and djurf1or 6655. Remark: maybe a version of this lemma with 𝐹 defined on 𝐴 and no restriction in the conclusion would be more usable. (Contributed by BJ and Jim Kingdon, 4-Jul-2022.) |
⊢ 𝑋 ∈ V & ⊢ 𝐹 = (𝑥 ∈ V ↦ ⟨𝑋, 𝑥⟩) ⇒ ⊢ (𝐹 ↾ 𝐴):𝐴–1-1-onto→({𝑋} × 𝐴) | ||
4-Jul-2022 | djuf1olem 6651 | Lemma for djulf1o 6656 and djurf1o 6657. (Contributed by BJ and Jim Kingdon, 4-Jul-2022.) |
⊢ 𝑋 ∈ V & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ ⟨𝑋, 𝑥⟩) ⇒ ⊢ 𝐹:𝐴–1-1-onto→({𝑋} × 𝐴) | ||
4-Jul-2022 | snexxph 6582 | A case where the antecedent of snexg 3982 is not needed. The class {𝑥 ∣ 𝜑} is from dcextest 4358. (Contributed by Mario Carneiro and Jim Kingdon, 4-Jul-2022.) |
⊢ {{𝑥 ∣ 𝜑}} ∈ V | ||
4-Jul-2022 | 1oex 6120 | Ordinal 1 is a set. (Contributed by BJ, 4-Jul-2022.) |
⊢ 1_{𝑜} ∈ V | ||
4-Jul-2022 | resflem 5403 | A lemma to bound the range of a restriction. The conclusion would also hold with (𝑋 ∩ 𝑌) in place of 𝑌 (provided 𝑥 does not occur in 𝑋). If that stronger result is needed, it is however simpler to use the instance of resflem 5403 where (𝑋 ∩ 𝑌) is substituted for 𝑌 (in both the conclusion and the third hypothesis). (Contributed by BJ, 4-Jul-2022.) |
⊢ (𝜑 → 𝐹:𝑉⟶𝑋) & ⊢ (𝜑 → 𝐴 ⊆ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ 𝑌) ⇒ ⊢ (𝜑 → (𝐹 ↾ 𝐴):𝐴⟶𝑌) | ||
4-Jul-2022 | f1ff1 5171 | If a function is one-to-one from A to B and is also a function from A to C, then it is a one-to-one function from A to C. (Contributed by BJ, 4-Jul-2022.) |
⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴⟶𝐶) → 𝐹:𝐴–1-1→𝐶) | ||
3-Jul-2022 | dcextest 4358 | If it is decidable whether {𝑥 ∣ 𝜑} is a set, then ¬ 𝜑 is decidable (where 𝑥 does not occur in 𝜑). From this fact, we can deduce (outside the formal system, since we cannot quantify over classes) that if it is decidable whether any class is a set, then "weak excluded middle" (that is, any negated proposition ¬ 𝜑 is decidable) holds. (Contributed by Jim Kingdon, 3-Jul-2022.) |
⊢ DECID {𝑥 ∣ 𝜑} ∈ V ⇒ ⊢ DECID ¬ 𝜑 | ||
3-Jul-2022 | notnotsnex 3985 | A singleton is never a proper class. (Contributed by Mario Carneiro and Jim Kingdon, 3-Jul-2022.) |
⊢ ¬ ¬ {𝐴} ∈ V | ||
2-Jul-2022 | exmidfodomrlemeldju 6727 | Lemma for exmidfodomr 6732. A variant of djur 6663. (Contributed by Jim Kingdon, 2-Jul-2022.) |
⊢ (𝜑 → 𝐴 ⊆ 1_{𝑜}) & ⊢ (𝜑 → 𝐵 ∈ (𝐴 ⊔ 1_{𝑜})) ⇒ ⊢ (𝜑 → (𝐵 = (inl‘∅) ∨ 𝐵 = (inr‘∅))) | ||
2-Jul-2022 | djune 6675 | Left and right injection never produce equal values. (Contributed by Jim Kingdon, 2-Jul-2022.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (inl‘𝐴) ≠ (inr‘𝐵)) | ||
2-Jul-2022 | djulclb 6653 | Left biconditional closure of disjoint union. (Contributed by Jim Kingdon, 2-Jul-2022.) |
⊢ (𝐶 ∈ 𝑉 → (𝐶 ∈ 𝐴 ↔ (inl‘𝐶) ∈ (𝐴 ⊔ 𝐵))) | ||
1-Jul-2022 | exmidfodomr 6732 | Excluded middle is equivalent to the existence of a mapping from any set onto any inhabited set that it dominates. (Contributed by Jim Kingdon, 1-Jul-2022.) |
⊢ (EXMID ↔ ∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦)) | ||
1-Jul-2022 | exmidfodomrlemr 6730 | The existence of a mapping from any set onto any inhabited set that it dominates implies excluded middle. Proposition 1.2 of [PradicBrown2021], p. 2. (Contributed by Jim Kingdon, 1-Jul-2022.) |
⊢ (∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) → EXMID) | ||
1-Jul-2022 | exmidfodomrlemim 6729 | Excluded middle implies the existence of a mapping from any set onto any inhabited set that it dominates. Proposition 1.1 of [PradicBrown2021], p. 2. (Contributed by Jim Kingdon, 1-Jul-2022.) |
⊢ (EXMID → ∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦)) | ||
1-Jul-2022 | dju1p1e2 6725 | Disjoint union version of one plus one equals two. (Contributed by Jim Kingdon, 1-Jul-2022.) |
⊢ (1_{𝑜} ⊔ 1_{𝑜}) ≈ 2_{𝑜} | ||
1-Jul-2022 | notm0 3286 | A class is not inhabited if and only if it is empty. (Contributed by Jim Kingdon, 1-Jul-2022.) |
⊢ (¬ ∃𝑥 𝑥 ∈ 𝐴 ↔ 𝐴 = ∅) | ||
30-Jun-2022 | exmidomni 6702 | Excluded middle is equivalent to every set being omniscient. (Contributed by BJ and Jim Kingdon, 30-Jun-2022.) |
⊢ (EXMID ↔ ∀𝑥 𝑥 ∈ Omni) | ||
30-Jun-2022 | exmidpw 6550 | Excluded middle is equivalent to the power set of 1_{𝑜} having two elements. Remark of [PradicBrown2021], p. 2. (Contributed by Jim Kingdon, 30-Jun-2022.) |
⊢ (EXMID ↔ 𝒫 1_{𝑜} ≈ 2_{𝑜}) | ||
29-Jun-2022 | exmidomniim 6701 | Given excluded middle, every set is omniscient. Remark following Definition 3.1 of [Pierik], p. 14. This is one direction of the biconditional exmidomni 6702. (Contributed by Jim Kingdon, 29-Jun-2022.) |
⊢ (EXMID → ∀𝑥 𝑥 ∈ Omni) | ||
29-Jun-2022 | dfrex2dc 2365 | Relationship between restricted universal and existential quantifiers. (Contributed by Jim Kingdon, 29-Jun-2022.) |
⊢ (DECID ∃𝑥 ∈ 𝐴 𝜑 → (∃𝑥 ∈ 𝐴 𝜑 ↔ ¬ ∀𝑥 ∈ 𝐴 ¬ 𝜑)) | ||
28-Jun-2022 | finomni 6700 | A finite set is omniscient. Remark right after Definition 3.1 of [Pierik], p. 14. (Contributed by Jim Kingdon, 28-Jun-2022.) |
⊢ (𝐴 ∈ Fin → 𝐴 ∈ Omni) | ||
28-Jun-2022 | isomni 6696 | The predicate of being omniscient. (Contributed by Jim Kingdon, 28-Jun-2022.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ Omni ↔ ∀𝑓(𝑓:𝐴⟶2_{𝑜} → (∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1_{𝑜})))) | ||
28-Jun-2022 | df-omni 6695 |
An omniscient set is one where we can decide whether a predicate (here
represented by a function 𝑓) holds (is equal to 1_{𝑜}) 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 Lesser Principle of Omniscience (LPO). (Contributed by Jim Kingdon, 28-Jun-2022.) |
⊢ Omni = {𝑦 ∣ ∀𝑓(𝑓:𝑦⟶2_{𝑜} → (∃𝑥 ∈ 𝑦 (𝑓‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝑦 (𝑓‘𝑥) = 1_{𝑜}))} | ||
28-Jun-2022 | updjud 6679 | Universal property of the disjoint union. (Proposed by BJ, 25-Jun-2022.) (Contributed by AV, 28-Jun-2022.) |
⊢ (𝜑 → 𝐹:𝐴⟶𝐶) & ⊢ (𝜑 → 𝐺:𝐵⟶𝐶) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) ⇒ ⊢ (𝜑 → ∃!ℎ(ℎ:(𝐴 ⊔ 𝐵)⟶𝐶 ∧ (ℎ ∘ (inl ↾ 𝐴)) = 𝐹 ∧ (ℎ ∘ (inr ↾ 𝐵)) = 𝐺)) | ||
28-Jun-2022 | inrresf1 6660 | 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→(𝐴 ⊔ 𝐵) | ||
28-Jun-2022 | inlresf1 6659 | 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→(𝐴 ⊔ 𝐵) | ||
28-Jun-2022 | djuex 6642 | The disjoint union of sets is a set. (Contributed by AV, 28-Jun-2022.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ⊔ 𝐵) ∈ V) | ||
28-Jun-2022 | f1resf1 5173 | The restriction of an injective function is injective. (Contributed by AV, 28-Jun-2022.) |
⊢ (((𝐹:𝐴–1-1→𝐵 ∧ 𝐶 ⊆ 𝐴) ∧ (𝐹 ↾ 𝐶):𝐶⟶𝐷) → (𝐹 ↾ 𝐶):𝐶–1-1→𝐷) | ||
27-Jun-2022 | updjudhcoinrg 6678 | 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((1^{st} ‘𝑥) = ∅, (𝐹‘(2^{nd} ‘𝑥)), (𝐺‘(2^{nd} ‘𝑥)))) ⇒ ⊢ (𝜑 → (𝐻 ∘ (inr ↾ 𝐵)) = 𝐺) | ||
27-Jun-2022 | updjudhcoinlf 6677 | 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((1^{st} ‘𝑥) = ∅, (𝐹‘(2^{nd} ‘𝑥)), (𝐺‘(2^{nd} ‘𝑥)))) ⇒ ⊢ (𝜑 → (𝐻 ∘ (inl ↾ 𝐴)) = 𝐹) | ||
27-Jun-2022 | 2ndinr 6674 | The second component of the value of a right injection is its argument. (Contributed by AV, 27-Jun-2022.) |
⊢ (𝑋 ∈ 𝑉 → (2^{nd} ‘(inr‘𝑋)) = 𝑋) | ||
27-Jun-2022 | 1stinr 6673 | The first component of the value of a right injection is 1_{𝑜}. (Contributed by AV, 27-Jun-2022.) |
⊢ (𝑋 ∈ 𝑉 → (1^{st} ‘(inr‘𝑋)) = 1_{𝑜}) | ||
27-Jun-2022 | 2ndinl 6672 | The second component of the value of a left injection is its argument. (Contributed by AV, 27-Jun-2022.) |
⊢ (𝑋 ∈ 𝑉 → (2^{nd} ‘(inl‘𝑋)) = 𝑋) | ||
27-Jun-2022 | 1stinl 6671 | The first component of the value of a left injection is the empty set. (Contributed by AV, 27-Jun-2022.) |
⊢ (𝑋 ∈ 𝑉 → (1^{st} ‘(inl‘𝑋)) = ∅) | ||
26-Jun-2022 | updjudhf 6676 | 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((1^{st} ‘𝑥) = ∅, (𝐹‘(2^{nd} ‘𝑥)), (𝐺‘(2^{nd} ‘𝑥)))) ⇒ ⊢ (𝜑 → 𝐻:(𝐴 ⊔ 𝐵)⟶𝐶) | ||
26-Jun-2022 | eldju2ndr 6670 | 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.) |
⊢ ((𝑋 ∈ (𝐴 ⊔ 𝐵) ∧ (1^{st} ‘𝑋) ≠ ∅) → (2^{nd} ‘𝑋) ∈ 𝐵) | ||
26-Jun-2022 | eldju2ndl 6669 | 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.) |
⊢ ((𝑋 ∈ (𝐴 ⊔ 𝐵) ∧ (1^{st} ‘𝑋) = ∅) → (2^{nd} ‘𝑋) ∈ 𝐴) | ||
26-Jun-2022 | eldju1st 6668 | The first component of an element of a disjoint union is either ∅ or 1_{𝑜}. (Contributed by AV, 26-Jun-2022.) |
⊢ (𝑋 ∈ (𝐴 ⊔ 𝐵) → ((1^{st} ‘𝑋) = ∅ ∨ (1^{st} ‘𝑋) = 1_{𝑜})) | ||
25-Jun-2022 | djuss 6667 | A disjoint union is a subset of a Cartesian product. (Contributed by AV, 25-Jun-2022.) |
⊢ (𝐴 ⊔ 𝐵) ⊆ ({∅, 1_{𝑜}} × (𝐴 ∪ 𝐵)) | ||
23-Jun-2022 | eldju 6665 | Element of a disjoint union. (Contributed by BJ and Jim Kingdon, 23-Jun-2022.) |
⊢ (𝐶 ∈ (𝐴 ⊔ 𝐵) ↔ (∃𝑥 ∈ 𝐴 𝐶 = ((inl ↾ 𝐴)‘𝑥) ∨ ∃𝑥 ∈ 𝐵 𝐶 = ((inr ↾ 𝐵)‘𝑥))) | ||
23-Jun-2022 | djur 6663 | A member of a disjoint union can be mapped from one of the classes which produced it. (Contributed by Jim Kingdon, 23-Jun-2022.) |
⊢ (𝐶 ∈ (𝐴 ⊔ 𝐵) → (∃𝑥 ∈ 𝐴 𝐶 = (inl‘𝑥) ∨ ∃𝑥 ∈ 𝐵 𝐶 = (inr‘𝑥))) | ||
23-Jun-2022 | nfdju 6641 | Bound-variable hypothesis builder for disjoint union. (Contributed by Jim Kingdon, 23-Jun-2022.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥(𝐴 ⊔ 𝐵) | ||
23-Jun-2022 | djueq2 6640 | Equality theorem for disjoint union. (Contributed by Jim Kingdon, 23-Jun-2022.) |
⊢ (𝐴 = 𝐵 → (𝐶 ⊔ 𝐴) = (𝐶 ⊔ 𝐵)) | ||
23-Jun-2022 | djueq1 6639 | Equality theorem for disjoint union. (Contributed by Jim Kingdon, 23-Jun-2022.) |
⊢ (𝐴 = 𝐵 → (𝐴 ⊔ 𝐶) = (𝐵 ⊔ 𝐶)) | ||
23-Jun-2022 | djueq12 6638 | Equality theorem for disjoint union. (Contributed by Jim Kingdon, 23-Jun-2022.) |
⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 ⊔ 𝐶) = (𝐵 ⊔ 𝐷)) | ||
22-Jun-2022 | djurf1o 6657 | 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→({1_{𝑜}} × V) |
Copyright terms: Public domain | W3C HTML validation [external] |