 Intuitionistic Logic Explorer Most Recent Proofs Mirrors  >  Home  >  ILE Home  >  Th. List  >  Recent MPE Most Recent             Other  >  MM 100

Most recent proofs    These are the 100 (Unicode, GIF) or 1000 (Unicode, GIF) most recent proofs in the iset.mm database for the Intuitionistic Logic Explorer. The iset.mm database is maintained on GitHub with master (stable) and develop (development) versions. This page was created from the commit given on the MPE Most Recent Proofs page. The database from that commit is also available here: iset.mm.

See the MPE Most Recent Proofs page for news and some useful links.

 Color key: Intuitionistic Logic Explorer User Mathboxes

Last updated on 9-Aug-2022 at 12:04 PM ET.
Recent Additions to the Intuitionistic Logic Explorer
DateLabelDescription
Theorem

29-Jul-2022fodjuomnilemres 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-2022eqifdc 3404 Expansion of an equality with a conditional operator. (Contributed by Jim Kingdon, 28-Jul-2022.)
(DECID 𝜑 → (𝐴 = if(𝜑, 𝐵, 𝐶) ↔ ((𝜑𝐴 = 𝐵) ∨ (¬ 𝜑𝐴 = 𝐶))))

27-Jul-2022fodjuomni 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-2022fodjuomnilem0 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-2022fodjuomnilemm 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-2022fodjuomnilemf 6704 Lemma for fodjuomni 6708. Domain and range of 𝑃. (Contributed by Jim Kingdon, 27-Jul-2022.)
(𝜑𝑂 ∈ Omni)    &   (𝜑𝐹:𝑂onto→(𝐴𝐵))    &   𝑃 = (𝑦𝑂 ↦ if(∃𝑧𝐴 (𝐹𝑦) = (inl‘𝑧), ∅, 1𝑜))       (𝜑𝑃 ∈ (2𝑜𝑚 𝑂))

27-Jul-2022fodjuomnilemdc 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-2022djudom 6693 Dominance law for disjoint union. (Contributed by Jim Kingdon, 25-Jul-2022.)
((𝐴𝐵𝐶𝐷) → (𝐴𝐶) ≼ (𝐵𝐷))

17-Jul-2022inftonninf 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-20221tonninf 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-20220tonninf 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-2022fxnn0nninf 9732 A function from 0* into . (Contributed by Jim Kingdon, 16-Jul-2022.)
𝐺 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)    &   𝐹 = (𝑛 ∈ ω ↦ (𝑖 ∈ ω ↦ if(𝑖𝑛, 1𝑜, ∅)))    &   𝐼 = ((𝐹𝐺) ∪ {⟨+∞, (ω × {1𝑜})⟩})       𝐼:ℕ0*⟶ℕ

16-Jul-2022fnn0nninf 9731 A function from 0 into . (Contributed by Jim Kingdon, 16-Jul-2022.)
𝐺 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)    &   𝐹 = (𝑛 ∈ ω ↦ (𝑖 ∈ ω ↦ if(𝑖𝑛, 1𝑜, ∅)))       (𝐹𝐺):ℕ0⟶ℕ

15-Jul-2022mapdom1g 6492 Order-preserving property of set exponentiation. (Contributed by Jim Kingdon, 15-Jul-2022.)
((𝐴𝐵𝐶𝑉) → (𝐴𝑚 𝐶) ≼ (𝐵𝑚 𝐶))

14-Jul-2022nnnninf 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-2022infnninf 8643 The point at infinity in (the constant sequence equal to 1𝑜). (Contributed by Jim Kingdon, 14-Jul-2022.)
(ω × {1𝑜}) ∈ ℕ

14-Jul-2022df-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-2022enomni 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-2022enomnilem 6698 Lemma for enomni 6699. One direction of the biconditional. (Contributed by Jim Kingdon, 13-Jul-2022.)
(𝐴𝐵 → (𝐴 ∈ Omni → 𝐵 ∈ Omni))

13-Jul-2022isomnimap 6697 The predicate of being omniscient stated in terms of set exponentiation. (Contributed by Jim Kingdon, 13-Jul-2022.)
(𝐴𝑉 → (𝐴 ∈ Omni ↔ ∀𝑓 ∈ (2𝑜𝑚 𝐴)(∃𝑥𝐴 (𝑓𝑥) = ∅ ∨ ∀𝑥𝐴 (𝑓𝑥) = 1𝑜)))

12-Jul-2022finexdc 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-2022dfrex2fin 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-2022djuinj 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-2022djudm 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-2022djufun 6690 The "domain-disjoint-union" of two functions is a function. (Contributed by BJ, 10-Jul-2022.)
(𝜑 → Fun 𝐹)    &   (𝜑 → Fun 𝐺)       (𝜑 → Fun (𝐹d 𝐺))

10-Jul-2022df-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-2022casef1 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-2022caseinj 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-2022casef 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-2022caserel 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-2022casedm 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-2022casefun 6682 The "case" construction of two functions is a function. (Contributed by BJ, 10-Jul-2022.)
(𝜑 → Fun 𝐹)    &   (𝜑 → Fun 𝐺)       (𝜑 → Fun case(𝐹, 𝐺))

10-Jul-2022df-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-2022cocnvss 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-2022cocnvres 4908 Restricting a relation and a converse relation when they are composed together (Contributed by BJ, 10-Jul-2022.)
(𝑆𝑅) = ((𝑆 ↾ dom 𝑅) ∘ (𝑅 ↾ dom 𝑆))

10-Jul-2022cossxp2 4907 The composition of two relations is a relation, with bounds on its domain and codomain. (Contributed by BJ, 10-Jul-2022.)
(𝜑𝑅 ⊆ (𝐴 × 𝐵))    &   (𝜑𝑆 ⊆ (𝐵 × 𝐶))       (𝜑 → (𝑆𝑅) ⊆ (𝐴 × 𝐶))

10-Jul-2022rnxpss2 4817 Upper bound for the range of a binary relation. (Contributed by BJ, 10-Jul-2022.)
(𝑅 ⊆ (𝐴 × 𝐵) → ran 𝑅𝐵)

10-Jul-2022dmxpss2 4816 Upper bound for the domain of a binary relation. (Contributed by BJ, 10-Jul-2022.)
(𝑅 ⊆ (𝐴 × 𝐵) → dom 𝑅𝐴)

10-Jul-2022elco 4559 Elements of a composed relation. (Contributed by BJ, 10-Jul-2022.)
(𝐴 ∈ (𝑅𝑆) ↔ ∃𝑥𝑦𝑧(𝐴 = ⟨𝑥, 𝑧⟩ ∧ (𝑥𝑆𝑦𝑦𝑅𝑧)))

9-Jul-2022exmidfodomrlemrALT 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-2022exmidfodomrlemreseldju 6728 Lemma for exmidfodomrlemrALT 6731. A variant of eldju 6665. (Contributed by Jim Kingdon, 9-Jul-2022.)
(𝜑𝐴 ⊆ 1𝑜)    &   (𝜑𝐵 ∈ (𝐴 ⊔ 1𝑜))       (𝜑 → ((∅ ∈ 𝐴𝐵 = ((inl ↾ 𝐴)‘∅)) ∨ 𝐵 = ((inr ↾ 1𝑜)‘∅)))

8-Jul-2022abn0m 3291 Inhabited class abstraction. (Contributed by Jim Kingdon, 8-Jul-2022.)
(∃𝑦 𝑦 ∈ {𝑥𝜑} ↔ ∃𝑥𝜑)

7-Jul-2022fvco4 5320 Value of a composition. (Contributed by BJ, 7-Jul-2022.)
(((𝐾:𝐴𝑋 ∧ (𝐻𝐾) = 𝐹) ∧ (𝑢𝐴𝑥 = (𝐾𝑢))) → (𝐻𝑥) = (𝐹𝑢))

6-Jul-2022djuun 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-2022djuunr 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-2022djurclr 6648 Right closure of disjoint union. (Contributed by Jim Kingdon, 21-Jun-2022.) (Revised by BJ, 6-Jul-2022.)
(𝐶𝐵 → ((inr ↾ 𝐵)‘𝐶) ∈ (𝐴𝐵))

6-Jul-2022djulclr 6647 Left closure of disjoint union. (Contributed by Jim Kingdon, 21-Jun-2022.) (Revised by BJ, 6-Jul-2022.)
(𝐶𝐴 → ((inl ↾ 𝐴)‘𝐶) ∈ (𝐴𝐵))

6-Jul-2022foelrn 5470 Property of a surjective function. (Contributed by Jeff Madsen, 4-Jan-2011.) (Proof shortened by BJ, 6-Jul-2022.)
((𝐹:𝐴onto𝐵𝐶𝐵) → ∃𝑥𝐴 𝐶 = (𝐹𝑥))

6-Jul-2022foima2 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-2022f1rn 5164 The range of a one-to-one mapping. (Contributed by BJ, 6-Jul-2022.)
(𝐹:𝐴1-1𝐵 → ran 𝐹𝐵)

4-Jul-2022djurclALT 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-2022djulclALT 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-2022djucllem 11042 Lemma for djulcl 6649 and djurcl 6650. (Contributed by BJ, 4-Jul-2022.)
𝑋 ∈ V    &   𝐹 = (𝑥 ∈ V ↦ ⟨𝑋, 𝑥⟩)       (𝐴𝐵 → ((𝐹𝐵)‘𝐴) ∈ ({𝑋} × 𝐵))

4-Jul-2022inresflem 6658 Lemma for inlresf1 6659 and inrresf1 6660. (Contributed by BJ, 4-Jul-2022.)
𝐹:𝐴1-1-onto→({𝑋} × 𝐴)    &   (𝑥𝐴 → (𝐹𝑥) ∈ 𝐵)       𝐹:𝐴1-1𝐵

4-Jul-2022djuf1olemr 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-2022djuf1olem 6651 Lemma for djulf1o 6656 and djurf1o 6657. (Contributed by BJ and Jim Kingdon, 4-Jul-2022.)
𝑋 ∈ V    &   𝐹 = (𝑥𝐴 ↦ ⟨𝑋, 𝑥⟩)       𝐹:𝐴1-1-onto→({𝑋} × 𝐴)

4-Jul-2022snexxph 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-20221oex 6120 Ordinal 1 is a set. (Contributed by BJ, 4-Jul-2022.)
1𝑜 ∈ V

4-Jul-2022resflem 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-2022f1ff1 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-2022dcextest 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-2022notnotsnex 3985 A singleton is never a proper class. (Contributed by Mario Carneiro and Jim Kingdon, 3-Jul-2022.)
¬ ¬ {𝐴} ∈ V

2-Jul-2022exmidfodomrlemeldju 6727 Lemma for exmidfodomr 6732. A variant of djur 6663. (Contributed by Jim Kingdon, 2-Jul-2022.)
(𝜑𝐴 ⊆ 1𝑜)    &   (𝜑𝐵 ∈ (𝐴 ⊔ 1𝑜))       (𝜑 → (𝐵 = (inl‘∅) ∨ 𝐵 = (inr‘∅)))

2-Jul-2022djune 6675 Left and right injection never produce equal values. (Contributed by Jim Kingdon, 2-Jul-2022.)
((𝐴𝑉𝐵𝑊) → (inl‘𝐴) ≠ (inr‘𝐵))

2-Jul-2022djulclb 6653 Left biconditional closure of disjoint union. (Contributed by Jim Kingdon, 2-Jul-2022.)
(𝐶𝑉 → (𝐶𝐴 ↔ (inl‘𝐶) ∈ (𝐴𝐵)))

1-Jul-2022exmidfodomr 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-2022exmidfodomrlemr 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-2022exmidfodomrlemim 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-2022dju1p1e2 6725 Disjoint union version of one plus one equals two. (Contributed by Jim Kingdon, 1-Jul-2022.)
(1𝑜 ⊔ 1𝑜) ≈ 2𝑜

1-Jul-2022notm0 3286 A class is not inhabited if and only if it is empty. (Contributed by Jim Kingdon, 1-Jul-2022.)
(¬ ∃𝑥 𝑥𝐴𝐴 = ∅)

30-Jun-2022exmidomni 6702 Excluded middle is equivalent to every set being omniscient. (Contributed by BJ and Jim Kingdon, 30-Jun-2022.)
(EXMID ↔ ∀𝑥 𝑥 ∈ Omni)

30-Jun-2022exmidpw 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-2022exmidomniim 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-2022dfrex2dc 2365 Relationship between restricted universal and existential quantifiers. (Contributed by Jim Kingdon, 29-Jun-2022.)
(DECID𝑥𝐴 𝜑 → (∃𝑥𝐴 𝜑 ↔ ¬ ∀𝑥𝐴 ¬ 𝜑))

28-Jun-2022finomni 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-2022isomni 6696 The predicate of being omniscient. (Contributed by Jim Kingdon, 28-Jun-2022.)
(𝐴𝑉 → (𝐴 ∈ Omni ↔ ∀𝑓(𝑓:𝐴⟶2𝑜 → (∃𝑥𝐴 (𝑓𝑥) = ∅ ∨ ∀𝑥𝐴 (𝑓𝑥) = 1𝑜))))

28-Jun-2022df-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-2022updjud 6679 Universal property of the disjoint union. (Proposed by BJ, 25-Jun-2022.) (Contributed by AV, 28-Jun-2022.)
(𝜑𝐹:𝐴𝐶)    &   (𝜑𝐺:𝐵𝐶)    &   (𝜑𝐴𝑉)    &   (𝜑𝐵𝑊)       (𝜑 → ∃!(:(𝐴𝐵)⟶𝐶 ∧ ( ∘ (inl ↾ 𝐴)) = 𝐹 ∧ ( ∘ (inr ↾ 𝐵)) = 𝐺))

28-Jun-2022inrresf1 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-2022inlresf1 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-2022djuex 6642 The disjoint union of sets is a set. (Contributed by AV, 28-Jun-2022.)
((𝐴𝑉𝐵𝑊) → (𝐴𝐵) ∈ V)

28-Jun-2022f1resf1 5173 The restriction of an injective function is injective. (Contributed by AV, 28-Jun-2022.)
(((𝐹:𝐴1-1𝐵𝐶𝐴) ∧ (𝐹𝐶):𝐶𝐷) → (𝐹𝐶):𝐶1-1𝐷)

27-Jun-2022updjudhcoinrg 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((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥))))       (𝜑 → (𝐻 ∘ (inr ↾ 𝐵)) = 𝐺)

27-Jun-2022updjudhcoinlf 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((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥))))       (𝜑 → (𝐻 ∘ (inl ↾ 𝐴)) = 𝐹)

27-Jun-20222ndinr 6674 The second component of the value of a right injection is its argument. (Contributed by AV, 27-Jun-2022.)
(𝑋𝑉 → (2nd ‘(inr‘𝑋)) = 𝑋)

27-Jun-20221stinr 6673 The first component of the value of a right injection is 1𝑜. (Contributed by AV, 27-Jun-2022.)
(𝑋𝑉 → (1st ‘(inr‘𝑋)) = 1𝑜)

27-Jun-20222ndinl 6672 The second component of the value of a left injection is its argument. (Contributed by AV, 27-Jun-2022.)
(𝑋𝑉 → (2nd ‘(inl‘𝑋)) = 𝑋)

27-Jun-20221stinl 6671 The first component of the value of a left injection is the empty set. (Contributed by AV, 27-Jun-2022.)
(𝑋𝑉 → (1st ‘(inl‘𝑋)) = ∅)

26-Jun-2022updjudhf 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((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥))))       (𝜑𝐻:(𝐴𝐵)⟶𝐶)

26-Jun-2022eldju2ndr 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.)
((𝑋 ∈ (𝐴𝐵) ∧ (1st𝑋) ≠ ∅) → (2nd𝑋) ∈ 𝐵)

26-Jun-2022eldju2ndl 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.)
((𝑋 ∈ (𝐴𝐵) ∧ (1st𝑋) = ∅) → (2nd𝑋) ∈ 𝐴)

26-Jun-2022eldju1st 6668 The first component of an element of a disjoint union is either or 1𝑜. (Contributed by AV, 26-Jun-2022.)
(𝑋 ∈ (𝐴𝐵) → ((1st𝑋) = ∅ ∨ (1st𝑋) = 1𝑜))

25-Jun-2022djuss 6667 A disjoint union is a subset of a Cartesian product. (Contributed by AV, 25-Jun-2022.)
(𝐴𝐵) ⊆ ({∅, 1𝑜} × (𝐴𝐵))

23-Jun-2022eldju 6665 Element of a disjoint union. (Contributed by BJ and Jim Kingdon, 23-Jun-2022.)
(𝐶 ∈ (𝐴𝐵) ↔ (∃𝑥𝐴 𝐶 = ((inl ↾ 𝐴)‘𝑥) ∨ ∃𝑥𝐵 𝐶 = ((inr ↾ 𝐵)‘𝑥)))

23-Jun-2022djur 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-2022nfdju 6641 Bound-variable hypothesis builder for disjoint union. (Contributed by Jim Kingdon, 23-Jun-2022.)
𝑥𝐴    &   𝑥𝐵       𝑥(𝐴𝐵)

23-Jun-2022djueq2 6640 Equality theorem for disjoint union. (Contributed by Jim Kingdon, 23-Jun-2022.)
(𝐴 = 𝐵 → (𝐶𝐴) = (𝐶𝐵))

23-Jun-2022djueq1 6639 Equality theorem for disjoint union. (Contributed by Jim Kingdon, 23-Jun-2022.)
(𝐴 = 𝐵 → (𝐴𝐶) = (𝐵𝐶))

23-Jun-2022djueq12 6638 Equality theorem for disjoint union. (Contributed by Jim Kingdon, 23-Jun-2022.)
((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴𝐶) = (𝐵𝐷))

22-Jun-2022djurf1o 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]