![]() |
Metamath
Proof Explorer Theorem List (p. 461 of 480) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30439) |
![]() (30440-31962) |
![]() (31963-47940) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | mdandyvrx11 46001 | Given the exclusivities set in the hypotheses, there exist a proof where ch, th, ta, et exclude ze, si accordingly. (Contributed by Jarvin Udandy, 7-Sep-2016.) |
⊢ (𝜑 ⊻ 𝜁) & ⊢ (𝜓 ⊻ 𝜎) & ⊢ (𝜒 ↔ 𝜓) & ⊢ (𝜃 ↔ 𝜓) & ⊢ (𝜏 ↔ 𝜑) & ⊢ (𝜂 ↔ 𝜓) ⇒ ⊢ ((((𝜒 ⊻ 𝜎) ∧ (𝜃 ⊻ 𝜎)) ∧ (𝜏 ⊻ 𝜁)) ∧ (𝜂 ⊻ 𝜎)) | ||
Theorem | mdandyvrx12 46002 | Given the exclusivities set in the hypotheses, there exist a proof where ch, th, ta, et exclude ze, si accordingly. (Contributed by Jarvin Udandy, 7-Sep-2016.) |
⊢ (𝜑 ⊻ 𝜁) & ⊢ (𝜓 ⊻ 𝜎) & ⊢ (𝜒 ↔ 𝜑) & ⊢ (𝜃 ↔ 𝜑) & ⊢ (𝜏 ↔ 𝜓) & ⊢ (𝜂 ↔ 𝜓) ⇒ ⊢ ((((𝜒 ⊻ 𝜁) ∧ (𝜃 ⊻ 𝜁)) ∧ (𝜏 ⊻ 𝜎)) ∧ (𝜂 ⊻ 𝜎)) | ||
Theorem | mdandyvrx13 46003 | Given the exclusivities set in the hypotheses, there exist a proof where ch, th, ta, et exclude ze, si accordingly. (Contributed by Jarvin Udandy, 7-Sep-2016.) |
⊢ (𝜑 ⊻ 𝜁) & ⊢ (𝜓 ⊻ 𝜎) & ⊢ (𝜒 ↔ 𝜓) & ⊢ (𝜃 ↔ 𝜑) & ⊢ (𝜏 ↔ 𝜓) & ⊢ (𝜂 ↔ 𝜓) ⇒ ⊢ ((((𝜒 ⊻ 𝜎) ∧ (𝜃 ⊻ 𝜁)) ∧ (𝜏 ⊻ 𝜎)) ∧ (𝜂 ⊻ 𝜎)) | ||
Theorem | mdandyvrx14 46004 | Given the exclusivities set in the hypotheses, there exist a proof where ch, th, ta, et exclude ze, si accordingly. (Contributed by Jarvin Udandy, 7-Sep-2016.) |
⊢ (𝜑 ⊻ 𝜁) & ⊢ (𝜓 ⊻ 𝜎) & ⊢ (𝜒 ↔ 𝜑) & ⊢ (𝜃 ↔ 𝜓) & ⊢ (𝜏 ↔ 𝜓) & ⊢ (𝜂 ↔ 𝜓) ⇒ ⊢ ((((𝜒 ⊻ 𝜁) ∧ (𝜃 ⊻ 𝜎)) ∧ (𝜏 ⊻ 𝜎)) ∧ (𝜂 ⊻ 𝜎)) | ||
Theorem | mdandyvrx15 46005 | Given the exclusivities set in the hypotheses, there exist a proof where ch, th, ta, et exclude ze, si accordingly. (Contributed by Jarvin Udandy, 7-Sep-2016.) |
⊢ (𝜑 ⊻ 𝜁) & ⊢ (𝜓 ⊻ 𝜎) & ⊢ (𝜒 ↔ 𝜓) & ⊢ (𝜃 ↔ 𝜓) & ⊢ (𝜏 ↔ 𝜓) & ⊢ (𝜂 ↔ 𝜓) ⇒ ⊢ ((((𝜒 ⊻ 𝜎) ∧ (𝜃 ⊻ 𝜎)) ∧ (𝜏 ⊻ 𝜎)) ∧ (𝜂 ⊻ 𝜎)) | ||
Theorem | H15NH16TH15IH16 46006 | Given 15 hypotheses and a 16th hypothesis, there exists a proof the 15 imply the 16th. (Contributed by Jarvin Udandy, 8-Sep-2016.) |
⊢ 𝜑 & ⊢ 𝜓 & ⊢ 𝜒 & ⊢ 𝜃 & ⊢ 𝜏 & ⊢ 𝜂 & ⊢ 𝜁 & ⊢ 𝜎 & ⊢ 𝜌 & ⊢ 𝜇 & ⊢ 𝜆 & ⊢ 𝜅 & ⊢ jph & ⊢ jps & ⊢ jch & ⊢ jth ⇒ ⊢ (((((((((((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) ∧ 𝜇) ∧ 𝜆) ∧ 𝜅) ∧ jph) ∧ jps) ∧ jch) → jth) | ||
Theorem | dandysum2p2e4 46007 |
CONTRADICTION PROVED AT 1 + 1 = 2 .
Given the right hypotheses we can prove a dandysum of 2+2=4. The qed step is the value '4' in Decimal BEING IMPLIED by the hypotheses. Note: Values that when added would exceed a 4bit value are not supported. Note: Digits begin from left (least) to right (greatest). E.g., 1000 would be '1', 0100 would be '2', 0010 would be '4'. How to perceive the hypotheses' bits in order: ( th <-> F. ), ( ta <-> F. ) Would be input value X's first bit, and input value Y's first bit. ( et <-> F ), ( ze <-> F. ) would be input value X's second bit, and input value Y's second bit. (Contributed by Jarvin Udandy, 6-Sep-2016.) |
⊢ (𝜑 ↔ (𝜃 ∧ 𝜏)) & ⊢ (𝜓 ↔ (𝜂 ∧ 𝜁)) & ⊢ (𝜒 ↔ (𝜎 ∧ 𝜌)) & ⊢ (𝜃 ↔ ⊥) & ⊢ (𝜏 ↔ ⊥) & ⊢ (𝜂 ↔ ⊤) & ⊢ (𝜁 ↔ ⊤) & ⊢ (𝜎 ↔ ⊥) & ⊢ (𝜌 ↔ ⊥) & ⊢ (𝜇 ↔ ⊥) & ⊢ (𝜆 ↔ ⊥) & ⊢ (𝜅 ↔ ((𝜃 ⊻ 𝜏) ⊻ (𝜃 ∧ 𝜏))) & ⊢ (jph ↔ ((𝜂 ⊻ 𝜁) ∨ 𝜑)) & ⊢ (jps ↔ ((𝜎 ⊻ 𝜌) ∨ 𝜓)) & ⊢ (jch ↔ ((𝜇 ⊻ 𝜆) ∨ 𝜒)) ⇒ ⊢ ((((((((((((((((𝜑 ↔ (𝜃 ∧ 𝜏)) ∧ (𝜓 ↔ (𝜂 ∧ 𝜁))) ∧ (𝜒 ↔ (𝜎 ∧ 𝜌))) ∧ (𝜃 ↔ ⊥)) ∧ (𝜏 ↔ ⊥)) ∧ (𝜂 ↔ ⊤)) ∧ (𝜁 ↔ ⊤)) ∧ (𝜎 ↔ ⊥)) ∧ (𝜌 ↔ ⊥)) ∧ (𝜇 ↔ ⊥)) ∧ (𝜆 ↔ ⊥)) ∧ (𝜅 ↔ ((𝜃 ⊻ 𝜏) ⊻ (𝜃 ∧ 𝜏)))) ∧ (jph ↔ ((𝜂 ⊻ 𝜁) ∨ 𝜑))) ∧ (jps ↔ ((𝜎 ⊻ 𝜌) ∨ 𝜓))) ∧ (jch ↔ ((𝜇 ⊻ 𝜆) ∨ 𝜒))) → ((((𝜅 ↔ ⊥) ∧ (jph ↔ ⊥)) ∧ (jps ↔ ⊤)) ∧ (jch ↔ ⊥))) | ||
Theorem | mdandysum2p2e4 46008 |
CONTRADICTION PROVED AT 1 + 1 = 2 . Luckily Mario Carneiro did a
successful version of his own.
See Mario's Relevant Work: Half adder and full adder in propositional calculus. Given the right hypotheses we can prove a dandysum of 2+2=4. The qed step is the value '4' in Decimal BEING IMPLIED by the hypotheses. Note: Values that when added would exceed a 4bit value are not supported. Note: Digits begin from left (least) to right (greatest). E.g., 1000 would be '1', 0100 would be '2'. 0010 would be '4'. How to perceive the hypotheses' bits in order: ( th <-> F. ), ( ta <-> F. ) Would be input value X's first bit, and input value Y's first bit. ( et <-> F. ), ( ze <-> F. ) would be input value X's second bit, and input value Y's second bit. In mdandysum2p2e4, one might imagine what jth or jta could be then do the math with their truths. Also limited to the restriction jth, jta are having opposite truths equivalent to the stated truth constants. (Contributed by Jarvin Udandy, 6-Sep-2016.) |
⊢ (jth ↔ ⊥) & ⊢ (jta ↔ ⊤) & ⊢ (𝜑 ↔ (𝜃 ∧ 𝜏)) & ⊢ (𝜓 ↔ (𝜂 ∧ 𝜁)) & ⊢ (𝜒 ↔ (𝜎 ∧ 𝜌)) & ⊢ (𝜃 ↔ jth) & ⊢ (𝜏 ↔ jth) & ⊢ (𝜂 ↔ jta) & ⊢ (𝜁 ↔ jta) & ⊢ (𝜎 ↔ jth) & ⊢ (𝜌 ↔ jth) & ⊢ (𝜇 ↔ jth) & ⊢ (𝜆 ↔ jth) & ⊢ (𝜅 ↔ ((𝜃 ⊻ 𝜏) ⊻ (𝜃 ∧ 𝜏))) & ⊢ (jph ↔ ((𝜂 ⊻ 𝜁) ∨ 𝜑)) & ⊢ (jps ↔ ((𝜎 ⊻ 𝜌) ∨ 𝜓)) & ⊢ (jch ↔ ((𝜇 ⊻ 𝜆) ∨ 𝜒)) ⇒ ⊢ ((((((((((((((((𝜑 ↔ (𝜃 ∧ 𝜏)) ∧ (𝜓 ↔ (𝜂 ∧ 𝜁))) ∧ (𝜒 ↔ (𝜎 ∧ 𝜌))) ∧ (𝜃 ↔ ⊥)) ∧ (𝜏 ↔ ⊥)) ∧ (𝜂 ↔ ⊤)) ∧ (𝜁 ↔ ⊤)) ∧ (𝜎 ↔ ⊥)) ∧ (𝜌 ↔ ⊥)) ∧ (𝜇 ↔ ⊥)) ∧ (𝜆 ↔ ⊥)) ∧ (𝜅 ↔ ((𝜃 ⊻ 𝜏) ⊻ (𝜃 ∧ 𝜏)))) ∧ (jph ↔ ((𝜂 ⊻ 𝜁) ∨ 𝜑))) ∧ (jps ↔ ((𝜎 ⊻ 𝜌) ∨ 𝜓))) ∧ (jch ↔ ((𝜇 ⊻ 𝜆) ∨ 𝜒))) → ((((𝜅 ↔ ⊥) ∧ (jph ↔ ⊥)) ∧ (jps ↔ ⊤)) ∧ (jch ↔ ⊥))) | ||
Theorem | adh-jarrsc 46009 | Replacement of a nested antecedent with an outer antecedent. Commuted simplificated form of elimination of a nested antecedent. Also holds intuitionistically. Polish prefix notation: CCCpqrCsCqr . (Contributed by ADH, 10-Nov-2023.) (Proof modification is discouraged.) |
⊢ (((𝜑 → 𝜓) → 𝜒) → (𝜃 → (𝜓 → 𝜒))) | ||
Minimal implicational calculus, or intuitionistic implicational calculus, or positive implicational calculus, is the implicational fragment of minimal calculus (which is also the implicational fragment of intuitionistic calculus and of positive calculus). It is sometimes called "C-pure intuitionism" since the letter C is used to denote implication in Polish prefix notation. It can be axiomatized by the inference rule of modus ponens ax-mp 5 together with the axioms { ax-1 6, ax-2 7 } (sometimes written KS), or with { imim1 83, ax-1 6, pm2.43 56 } (written B'KW), or with { imim2 58, pm2.04 90, ax-1 6, pm2.43 56 } (written BCKW), or with the single axiom adh-minim 46010, or with the single axiom adh-minimp 46022. This section proves first adh-minim 46010 from { ax-1 6, ax-2 7 }, followed by the converse, due to Ivo Thomas; and then it proves adh-minimp 46022 from { ax-1 6, ax-2 7 }, also followed by the converse, also due to Ivo Thomas. Sources for this section are * Carew Arthur Meredith, A single axiom of positive logic, The Journal of Computing Systems, volume 1, issue 3, July 1953, pages 169--170; * Ivo Thomas, On Meredith's sole positive axiom, Notre Dame Journal of Formal Logic, volume XV, number 3, July 1974, page 477, in which the derivations of { ax-1 6, ax-2 7 } from adh-minim 46010 are shortened (compared to Meredith's derivations in the aforementioned paper); * Carew Arthur Meredith and Arthur Norman Prior, Notes on the axiomatics of the propositional calculus, Notre Dame Journal of Formal Logic, volume IV, number 3, July 1963, pages 171--187; and * the webpage https://web.ics.purdue.edu/~dulrich/C-pure-intuitionism-page.htm 46010 on Dolph Edward "Ted" Ulrich's website, where these and other single axioms for the minimal implicational calculus are listed. This entire section also holds intuitionistically. Users of the Polish prefix notation also often use a compact notation for proof derivations known as the D-notation where "D" stands for "condensed Detachment". For instance, "D21" means detaching ax-1 6 from ax-2 7, that is, using modus ponens ax-mp 5 with ax-1 6 as minor premise and ax-2 7 as major premise. When the numbered lemmas surpass 10, dots are added between the numbers. D-strings are accepted by the grammar Dundotted := digit | "D" Dundotted Dundotted ; Ddotted := digit + | "D" Ddotted "." Ddotted ; Dstr := Dundotted | Ddotted . (Contributed by BJ, 11-Apr-2021.) (Revised by ADH, 10-Nov-2023.) | ||
Theorem | adh-minim 46010 | A single axiom for minimal implicational calculus, due to Meredith. Other single axioms of the same length are known, but it is thought to be the minimal length. This is the axiom from Carew Arthur Meredith, A single axiom of positive logic, The Journal of Computing Systems, volume 1, issue 3, July 1953, pages 169--170. A two-line review by Alonzo Church of this article can be found in The Journal of Symbolic Logic, volume 19, issue 2, June 1954, page 144, https://doi.org/10.2307/2268914. Known as "HI-1" on Dolph Edward "Ted" Ulrich's web page. In the next 6 lemmas and 3 theorems, ax-1 6 and ax-2 7 are derived from this single axiom in 16 detachments (instances of ax-mp 5) in total. Polish prefix notation: CCCpqrCsCCqCrtCqt . (Contributed by ADH, 10-Nov-2023.) |
⊢ (((𝜑 → 𝜓) → 𝜒) → (𝜃 → ((𝜓 → (𝜒 → 𝜏)) → (𝜓 → 𝜏)))) | ||
Theorem | adh-minim-ax1-ax2-lem1 46011 | First lemma for the derivation of ax-1 6 and ax-2 7 from adh-minim 46010 and ax-mp 5. Polish prefix notation: CpCCqCCrCCsCqtCstuCqu . (Contributed by ADH, 10-Nov-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → ((𝜓 → ((𝜒 → ((𝜃 → (𝜓 → 𝜏)) → (𝜃 → 𝜏))) → 𝜂)) → (𝜓 → 𝜂))) | ||
Theorem | adh-minim-ax1-ax2-lem2 46012 | Second lemma for the derivation of ax-1 6 and ax-2 7 from adh-minim 46010 and ax-mp 5. Polish prefix notation: CCpCCqCCrCpsCrstCpt . (Contributed by ADH, 10-Nov-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜑 → ((𝜓 → ((𝜒 → (𝜑 → 𝜃)) → (𝜒 → 𝜃))) → 𝜏)) → (𝜑 → 𝜏)) | ||
Theorem | adh-minim-ax1-ax2-lem3 46013 | Third lemma for the derivation of ax-1 6 and ax-2 7 from adh-minim 46010 and ax-mp 5. Polish prefix notation: CCpCqrCqCsCpr . (Contributed by ADH, 10-Nov-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜑 → (𝜓 → 𝜒)) → (𝜓 → (𝜃 → (𝜑 → 𝜒)))) | ||
Theorem | adh-minim-ax1-ax2-lem4 46014 | Fourth lemma for the derivation of ax-1 6 and ax-2 7 from adh-minim 46010 and ax-mp 5. Polish prefix notation: CCCpqrCCqCrsCqs . (Contributed by ADH, 10-Nov-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (((𝜑 → 𝜓) → 𝜒) → ((𝜓 → (𝜒 → 𝜃)) → (𝜓 → 𝜃))) | ||
Theorem | adh-minim-ax1 46015 | Derivation of ax-1 6 from adh-minim 46010 and ax-mp 5. Carew Arthur Meredith derived ax-1 6 in A single axiom of positive logic, The Journal of Computing Systems, volume 1, issue 3, July 1953, pages 169--170. However, here we follow the shortened derivation by Ivo Thomas, On Meredith's sole positive axiom, Notre Dame Journal of Formal Logic, volume XV, number 3, July 1974, page 477. Polish prefix notation: CpCqp . (Contributed by ADH, 10-Nov-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → (𝜓 → 𝜑)) | ||
Theorem | adh-minim-ax2-lem5 46016 | Fifth lemma for the derivation of ax-2 7 from adh-minim 46010 and ax-mp 5. Polish prefix notation: CpCCCqrsCCrCstCrt . (Contributed by ADH, 10-Nov-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → (((𝜓 → 𝜒) → 𝜃) → ((𝜒 → (𝜃 → 𝜏)) → (𝜒 → 𝜏)))) | ||
Theorem | adh-minim-ax2-lem6 46017 | Sixth lemma for the derivation of ax-2 7 from adh-minim 46010 and ax-mp 5. Polish prefix notation: CCpCCCCqrsCCrCstCrtuCpu . (Contributed by ADH, 10-Nov-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜑 → ((((𝜓 → 𝜒) → 𝜃) → ((𝜒 → (𝜃 → 𝜏)) → (𝜒 → 𝜏))) → 𝜂)) → (𝜑 → 𝜂)) | ||
Theorem | adh-minim-ax2c 46018 | Derivation of a commuted form of ax-2 7 from adh-minim 46010 and ax-mp 5. Polish prefix notation: CCpqCCpCqrCpr . (Contributed by ADH, 10-Nov-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜑 → 𝜓) → ((𝜑 → (𝜓 → 𝜒)) → (𝜑 → 𝜒))) | ||
Theorem | adh-minim-ax2 46019 | Derivation of ax-2 7 from adh-minim 46010 and ax-mp 5. Carew Arthur Meredith derived ax-2 7 in A single axiom of positive logic, The Journal of Computing Systems, volume 1, issue 3, July 1953, pages 169--170. However, here we follow the shortened derivation by Ivo Thomas, On Meredith's sole positive axiom, Notre Dame Journal of Formal Logic, volume XV, number 3, July 1974, page 477. Polish prefix notation: CCpCqrCCpqCpr . (Contributed by ADH, 10-Nov-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜑 → (𝜓 → 𝜒)) → ((𝜑 → 𝜓) → (𝜑 → 𝜒))) | ||
Theorem | adh-minim-idALT 46020 | Derivation of id 22 (reflexivity of implication, PM *2.08 WhiteheadRussell p. 101) from adh-minim-ax1 46015, adh-minim-ax2 46019, and ax-mp 5. It uses the derivation written DD211 in D-notation. (See head comment for an explanation.) Polish prefix notation: Cpp . (Contributed by ADH, 10-Nov-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → 𝜑) | ||
Theorem | adh-minim-pm2.43 46021 | Derivation of pm2.43 56 WhiteheadRussell p. 106 (also called "hilbert" or "W") from adh-minim-ax1 46015, adh-minim-ax2 46019, and ax-mp 5. It uses the derivation written DD22D21 in D-notation. (See head comment for an explanation.) (Contributed by ADH, 10-Nov-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜑 → (𝜑 → 𝜓)) → (𝜑 → 𝜓)) | ||
Theorem | adh-minimp 46022 | Another single axiom for minimal implicational calculus, due to Meredith. Other single axioms of the same length are known, but it is thought to be the minimal length. Among single axioms of this length, it is the one with simplest antecedents (i.e., in the corresponding ordering of binary trees which first compares left subtrees, it is the first one). Known as "HI-2" on Dolph Edward "Ted" Ulrich's web page. In the next 4 lemmas and 5 theorems, ax-1 6 and ax-2 7 are derived from this other single axiom in 20 detachments (instances of ax-mp 5) in total. Polish prefix notation: CpCCqrCCCsqCrtCqt ; or CtCCpqCCCspCqrCpr in Carew Arthur Meredith and Arthur Norman Prior, Notes on the axiomatics of the propositional calculus, Notre Dame Journal of Formal Logic, volume IV, number 3, July 1963, pages 171--187, on page 180. (Contributed by BJ, 4-Apr-2021.) (Revised by ADH, 10-Nov-2023.) |
⊢ (𝜑 → ((𝜓 → 𝜒) → (((𝜃 → 𝜓) → (𝜒 → 𝜏)) → (𝜓 → 𝜏)))) | ||
Theorem | adh-minimp-jarr-imim1-ax2c-lem1 46023 | First lemma for the derivation of jarr 106, imim1 83, and a commuted form of ax-2 7, and indirectly ax-1 6 and ax-2 7, from adh-minimp 46022 and ax-mp 5. Polish prefix notation: CCpqCCCrpCqsCps . (Contributed by ADH, 10-Nov-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜑 → 𝜓) → (((𝜒 → 𝜑) → (𝜓 → 𝜃)) → (𝜑 → 𝜃))) | ||
Theorem | adh-minimp-jarr-lem2 46024 | Second lemma for the derivation of jarr 106, and indirectly ax-1 6, a commuted form of ax-2 7, and ax-2 7 proper, from adh-minimp 46022 and ax-mp 5. Polish prefix notation: CCCpqCCCrsCCCtrCsuCruvCqv . (Contributed by ADH, 10-Nov-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (((𝜑 → 𝜓) → (((𝜒 → 𝜃) → (((𝜏 → 𝜒) → (𝜃 → 𝜂)) → (𝜒 → 𝜂))) → 𝜁)) → (𝜓 → 𝜁)) | ||
Theorem | adh-minimp-jarr-ax2c-lem3 46025 | Third lemma for the derivation of jarr 106 and a commuted form of ax-2 7, and indirectly ax-1 6 and ax-2 7 proper , from adh-minimp 46022 and ax-mp 5. Polish prefix notation: CCCCpqCCCrpCqsCpstt . (Contributed by ADH, 10-Nov-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((((𝜑 → 𝜓) → (((𝜒 → 𝜑) → (𝜓 → 𝜃)) → (𝜑 → 𝜃))) → 𝜏) → 𝜏) | ||
Theorem | adh-minimp-sylsimp 46026 | Derivation of jarr 106 (also called "syll-simp") from minimp 1622 and ax-mp 5. Polish prefix notation: CCCpqrCqr . (Contributed by BJ, 4-Apr-2021.) (Revised by ADH, 10-Nov-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (((𝜑 → 𝜓) → 𝜒) → (𝜓 → 𝜒)) | ||
Theorem | adh-minimp-ax1 46027 | Derivation of ax-1 6 from adh-minimp 46022 and ax-mp 5. Polish prefix notation: CpCqp . (Contributed by BJ, 4-Apr-2021.) (Revised by ADH, 10-Nov-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → (𝜓 → 𝜑)) | ||
Theorem | adh-minimp-imim1 46028 | Derivation of imim1 83 ("left antimonotonicity of implication", theorem *2.06 of [WhiteheadRussell] p. 100) from adh-minimp 46022 and ax-mp 5. Polish prefix notation: CCpqCCqrCpr . (Contributed by ADH, 10-Nov-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜑 → 𝜓) → ((𝜓 → 𝜒) → (𝜑 → 𝜒))) | ||
Theorem | adh-minimp-ax2c 46029 | Derivation of a commuted form of ax-2 7 from adh-minimp 46022 and ax-mp 5. Polish prefix notation: CCpqCCpCqrCpr . (Contributed by BJ, 4-Apr-2021.) (Revised by ADH, 10-Nov-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜑 → 𝜓) → ((𝜑 → (𝜓 → 𝜒)) → (𝜑 → 𝜒))) | ||
Theorem | adh-minimp-ax2-lem4 46030 | Fourth lemma for the derivation of ax-2 7 from adh-minimp 46022 and ax-mp 5. Polish prefix notation: CpCCqCprCqr . (Contributed by ADH, 10-Nov-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → ((𝜓 → (𝜑 → 𝜒)) → (𝜓 → 𝜒))) | ||
Theorem | adh-minimp-ax2 46031 | Derivation of ax-2 7 from adh-minimp 46022 and ax-mp 5. Polish prefix notation: CCpCqrCCpqCpr . (Contributed by BJ, 4-Apr-2021.) (Revised by ADH, 10-Nov-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜑 → (𝜓 → 𝜒)) → ((𝜑 → 𝜓) → (𝜑 → 𝜒))) | ||
Theorem | adh-minimp-idALT 46032 | Derivation of id 22 (reflexivity of implication, PM *2.08 WhiteheadRussell p. 101) from adh-minimp-ax1 46027, adh-minimp-ax2 46031, and ax-mp 5. It uses the derivation written DD211 in D-notation. (See head comment for an explanation.) Polish prefix notation: Cpp . (Contributed by ADH, 10-Nov-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → 𝜑) | ||
Theorem | adh-minimp-pm2.43 46033 | Derivation of pm2.43 56 WhiteheadRussell p. 106 (also called "hilbert" or "W") from adh-minimp-ax1 46027, adh-minimp-ax2 46031, and ax-mp 5. It uses the derivation written DD22D21 in D-notation. (See head comment for an explanation.) Polish prefix notation: CCpCpqCpq . (Contributed by BJ, 31-May-2021.) (Revised by ADH, 10-Nov-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜑 → (𝜑 → 𝜓)) → (𝜑 → 𝜓)) | ||
Theorem | n0nsn2el 46034* | If a class with one element is not a singleton, there is at least another element in this class. (Contributed by AV, 6-Mar-2025.) |
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ≠ {𝐴}) → ∃𝑥 ∈ 𝐵 𝑥 ≠ 𝐴) | ||
Theorem | eusnsn 46035* | There is a unique element of a singleton which is equal to another singleton. (Contributed by AV, 24-Aug-2022.) |
⊢ ∃!𝑥{𝑥} = {𝑦} | ||
Theorem | absnsb 46036* | If the class abstraction {𝑥 ∣ 𝜑} associated with the wff 𝜑 is a singleton, the wff is true for the singleton element. (Contributed by AV, 24-Aug-2022.) |
⊢ ({𝑥 ∣ 𝜑} = {𝑦} → [𝑦 / 𝑥]𝜑) | ||
Theorem | euabsneu 46037* | Another way to express existential uniqueness of a wff 𝜑: its associated class abstraction {𝑥 ∣ 𝜑} is a singleton. Variant of euabsn2 4729 using existential uniqueness for the singleton element instead of existence only. (Contributed by AV, 24-Aug-2022.) |
⊢ (∃!𝑥𝜑 ↔ ∃!𝑦{𝑥 ∣ 𝜑} = {𝑦}) | ||
Theorem | elprneb 46038 | An element of a proper unordered pair is the first element iff it is not the second element. (Contributed by AV, 18-Jun-2020.) |
⊢ ((𝐴 ∈ {𝐵, 𝐶} ∧ 𝐵 ≠ 𝐶) → (𝐴 = 𝐵 ↔ 𝐴 ≠ 𝐶)) | ||
Theorem | oppr 46039 | Equality for ordered pairs implies equality of unordered pairs with the same elements. (Contributed by AV, 9-Jul-2023.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → {𝐴, 𝐵} = {𝐶, 𝐷})) | ||
Theorem | opprb 46040 | Equality for unordered pairs corresponds to equality of unordered pairs with the same elements. (Contributed by AV, 9-Jul-2023.) |
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌)) → ({𝐴, 𝐵} = {𝐶, 𝐷} ↔ (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ ∨ ⟨𝐴, 𝐵⟩ = ⟨𝐷, 𝐶⟩))) | ||
Theorem | or2expropbilem1 46041* | Lemma 1 for or2expropbi 46043 and ich2exprop 46438. (Contributed by AV, 16-Jul-2023.) |
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝐴 = 𝑎 ∧ 𝐵 = 𝑏) → (𝜑 → ∃𝑥∃𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ [𝑦 / 𝑏][𝑥 / 𝑎]𝜑)))) | ||
Theorem | or2expropbilem2 46042* | Lemma 2 for or2expropbi 46043 and ich2exprop 46438. (Contributed by AV, 16-Jul-2023.) |
⊢ (∃𝑎∃𝑏(⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ↔ ∃𝑥∃𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ [𝑦 / 𝑏][𝑥 / 𝑎]𝜑)) | ||
Theorem | or2expropbi 46043* | If two classes are strictly ordered, there is an ordered pair of both classes fulfilling a wff iff there is an unordered pair of both classes fulfilling the wff. (Contributed by AV, 26-Aug-2023.) |
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑅 Or 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴𝑅𝐵)) → (∃𝑎∃𝑏({𝐴, 𝐵} = {𝑎, 𝑏} ∧ (𝑎𝑅𝑏 ∧ 𝜑)) ↔ ∃𝑎∃𝑏(⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ (𝑎𝑅𝑏 ∧ 𝜑)))) | ||
Theorem | eubrv 46044* | If there is a unique set which is related to a class, then the class must be a set. (Contributed by AV, 25-Aug-2022.) |
⊢ (∃!𝑏 𝐴𝑅𝑏 → 𝐴 ∈ V) | ||
Theorem | eubrdm 46045* | If there is a unique set which is related to a class, then the class is an element of the domain of the relation. (Contributed by AV, 25-Aug-2022.) |
⊢ (∃!𝑏 𝐴𝑅𝑏 → 𝐴 ∈ dom 𝑅) | ||
Theorem | eldmressn 46046 | Element of the domain of a restriction to a singleton. (Contributed by Alexander van der Vekens, 2-Jul-2017.) |
⊢ (𝐵 ∈ dom (𝐹 ↾ {𝐴}) → 𝐵 = 𝐴) | ||
Theorem | iota0def 46047* | Example for a defined iota being the empty set, i.e., ∀𝑦𝑥 ⊆ 𝑦 is a wff satisfied by a unique value 𝑥, namely 𝑥 = ∅ (the empty set is the one and only set which is a subset of every set). (Contributed by AV, 24-Aug-2022.) |
⊢ (℩𝑥∀𝑦 𝑥 ⊆ 𝑦) = ∅ | ||
Theorem | iota0ndef 46048* | Example for an undefined iota being the empty set, i.e., ∀𝑦𝑦 ∈ 𝑥 is a wff not satisfied by a (unique) value 𝑥 (there is no set, and therefore certainly no unique set, which contains every set). (Contributed by AV, 24-Aug-2022.) |
⊢ (℩𝑥∀𝑦 𝑦 ∈ 𝑥) = ∅ | ||
Theorem | fveqvfvv 46049 | If a function's value at an argument is the universal class (which can never be the case because of fvex 6904), the function's value at this argument is any set (especially the empty set). In short "If a function's value is a proper class, it is a set", which sounds strange/contradictory, but which is a consequence of that a contradiction implies anything (see pm2.21i 119). (Contributed by Alexander van der Vekens, 26-May-2017.) |
⊢ ((𝐹‘𝐴) = V → (𝐹‘𝐴) = 𝐵) | ||
Theorem | fnresfnco 46050 | Composition of two functions, similar to fnco 6667. (Contributed by Alexander van der Vekens, 25-Jul-2017.) |
⊢ (((𝐹 ↾ ran 𝐺) Fn ran 𝐺 ∧ 𝐺 Fn 𝐵) → (𝐹 ∘ 𝐺) Fn 𝐵) | ||
Theorem | funcoressn 46051 | A composition restricted to a singleton is a function under certain conditions. (Contributed by Alexander van der Vekens, 25-Jul-2017.) |
⊢ ((((𝐺‘𝑋) ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {(𝐺‘𝑋)})) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴)) → Fun ((𝐹 ∘ 𝐺) ↾ {𝑋})) | ||
Theorem | funressnfv 46052 | A restriction to a singleton with a function value is a function under certain conditions. (Contributed by Alexander van der Vekens, 25-Jul-2017.) (Proof shortened by Peter Mazsa, 2-Oct-2022.) |
⊢ (((𝑋 ∈ dom (𝐹 ∘ 𝐺) ∧ Fun ((𝐹 ∘ 𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴)) → Fun (𝐹 ↾ {(𝐺‘𝑋)})) | ||
Theorem | funressndmfvrn 46053 | The value of a function 𝐹 at a set 𝐴 is in the range of the function 𝐹 if 𝐴 is in the domain of the function 𝐹. It is sufficient that 𝐹 is a function at 𝐴. (Contributed by AV, 1-Sep-2022.) |
⊢ ((Fun (𝐹 ↾ {𝐴}) ∧ 𝐴 ∈ dom 𝐹) → (𝐹‘𝐴) ∈ ran 𝐹) | ||
Theorem | funressnvmo 46054* | A function restricted to a singleton has at most one value for the singleton element as argument. (Contributed by AV, 2-Sep-2022.) |
⊢ (Fun (𝐹 ↾ {𝑥}) → ∃*𝑦 𝑥𝐹𝑦) | ||
Theorem | funressnmo 46055* | A function restricted to a singleton has at most one value for the singleton element as argument. (Contributed by AV, 2-Sep-2022.) |
⊢ ((𝐴 ∈ 𝑉 ∧ Fun (𝐹 ↾ {𝐴})) → ∃*𝑦 𝐴𝐹𝑦) | ||
Theorem | funressneu 46056* | There is exactly one value of a class which is a function restricted to a singleton, analogous to funeu 6573. 𝐴 ∈ V is required because otherwise ∃!𝑦𝐴𝐹𝑦, see brprcneu 6881. (Contributed by AV, 7-Sep-2022.) |
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ Fun (𝐹 ↾ {𝐴}) ∧ 𝐴𝐹𝐵) → ∃!𝑦 𝐴𝐹𝑦) | ||
Theorem | fresfo 46057 | Conditions for a restriction to be an onto function. Part of fresf1o 32123. (Contributed by AV, 29-Sep-2024.) |
⊢ ((Fun 𝐹 ∧ 𝐶 ⊆ ran 𝐹) → (𝐹 ↾ (◡𝐹 “ 𝐶)):(◡𝐹 “ 𝐶)–onto→𝐶) | ||
Theorem | fsetsniunop 46058* | The class of all functions from a (proper) singleton into 𝐵 is the union of all the singletons of (proper) ordered pairs over the elements of 𝐵 as second component. (Contributed by AV, 13-Sep-2024.) |
⊢ (𝑆 ∈ 𝑉 → {𝑓 ∣ 𝑓:{𝑆}⟶𝐵} = ∪ 𝑏 ∈ 𝐵 {{⟨𝑆, 𝑏⟩}}) | ||
Theorem | fsetabsnop 46059* | The class of all functions from a (proper) singleton into 𝐵 is the class of all the singletons of (proper) ordered pairs over the elements of 𝐵 as second component. (Contributed by AV, 13-Sep-2024.) |
⊢ (𝑆 ∈ 𝑉 → {𝑓 ∣ 𝑓:{𝑆}⟶𝐵} = {𝑦 ∣ ∃𝑏 ∈ 𝐵 𝑦 = {⟨𝑆, 𝑏⟩}}) | ||
Theorem | fsetsnf 46060* | The mapping of an element of a class to a singleton function is a function. (Contributed by AV, 13-Sep-2024.) |
⊢ 𝐴 = {𝑦 ∣ ∃𝑏 ∈ 𝐵 𝑦 = {⟨𝑆, 𝑏⟩}} & ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ {⟨𝑆, 𝑥⟩}) ⇒ ⊢ (𝑆 ∈ 𝑉 → 𝐹:𝐵⟶𝐴) | ||
Theorem | fsetsnf1 46061* | The mapping of an element of a class to a singleton function is an injection. (Contributed by AV, 13-Sep-2024.) |
⊢ 𝐴 = {𝑦 ∣ ∃𝑏 ∈ 𝐵 𝑦 = {⟨𝑆, 𝑏⟩}} & ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ {⟨𝑆, 𝑥⟩}) ⇒ ⊢ (𝑆 ∈ 𝑉 → 𝐹:𝐵–1-1→𝐴) | ||
Theorem | fsetsnfo 46062* | The mapping of an element of a class to a singleton function is a surjection. (Contributed by AV, 13-Sep-2024.) |
⊢ 𝐴 = {𝑦 ∣ ∃𝑏 ∈ 𝐵 𝑦 = {⟨𝑆, 𝑏⟩}} & ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ {⟨𝑆, 𝑥⟩}) ⇒ ⊢ (𝑆 ∈ 𝑉 → 𝐹:𝐵–onto→𝐴) | ||
Theorem | fsetsnf1o 46063* | The mapping of an element of a class to a singleton function is a bijection. (Contributed by AV, 13-Sep-2024.) |
⊢ 𝐴 = {𝑦 ∣ ∃𝑏 ∈ 𝐵 𝑦 = {⟨𝑆, 𝑏⟩}} & ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ {⟨𝑆, 𝑥⟩}) ⇒ ⊢ (𝑆 ∈ 𝑉 → 𝐹:𝐵–1-1-onto→𝐴) | ||
Theorem | fsetsnprcnex 46064* | The class of all functions from a (proper) singleton into a proper class 𝐵 is not a set. (Contributed by AV, 13-Sep-2024.) |
⊢ ((𝑆 ∈ 𝑉 ∧ 𝐵 ∉ V) → {𝑓 ∣ 𝑓:{𝑆}⟶𝐵} ∉ V) | ||
Theorem | cfsetssfset 46065 | The class of constant functions is a subclass of the class of functions. (Contributed by AV, 13-Sep-2024.) |
⊢ 𝐹 = {𝑓 ∣ (𝑓:𝐴⟶𝐵 ∧ ∃𝑏 ∈ 𝐵 ∀𝑧 ∈ 𝐴 (𝑓‘𝑧) = 𝑏)} ⇒ ⊢ 𝐹 ⊆ {𝑓 ∣ 𝑓:𝐴⟶𝐵} | ||
Theorem | cfsetsnfsetfv 46066* | The function value of the mapping of the class of singleton functions into the class of constant functions. (Contributed by AV, 13-Sep-2024.) |
⊢ 𝐹 = {𝑓 ∣ (𝑓:𝐴⟶𝐵 ∧ ∃𝑏 ∈ 𝐵 ∀𝑧 ∈ 𝐴 (𝑓‘𝑧) = 𝑏)} & ⊢ 𝐺 = {𝑥 ∣ 𝑥:{𝑌}⟶𝐵} & ⊢ 𝐻 = (𝑔 ∈ 𝐺 ↦ (𝑎 ∈ 𝐴 ↦ (𝑔‘𝑌))) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐺) → (𝐻‘𝑋) = (𝑎 ∈ 𝐴 ↦ (𝑋‘𝑌))) | ||
Theorem | cfsetsnfsetf 46067* | The mapping of the class of singleton functions into the class of constant functions is a function. (Contributed by AV, 14-Sep-2024.) |
⊢ 𝐹 = {𝑓 ∣ (𝑓:𝐴⟶𝐵 ∧ ∃𝑏 ∈ 𝐵 ∀𝑧 ∈ 𝐴 (𝑓‘𝑧) = 𝑏)} & ⊢ 𝐺 = {𝑥 ∣ 𝑥:{𝑌}⟶𝐵} & ⊢ 𝐻 = (𝑔 ∈ 𝐺 ↦ (𝑎 ∈ 𝐴 ↦ (𝑔‘𝑌))) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴) → 𝐻:𝐺⟶𝐹) | ||
Theorem | cfsetsnfsetf1 46068* | The mapping of the class of singleton functions into the class of constant functions is an injection. (Contributed by AV, 14-Sep-2024.) |
⊢ 𝐹 = {𝑓 ∣ (𝑓:𝐴⟶𝐵 ∧ ∃𝑏 ∈ 𝐵 ∀𝑧 ∈ 𝐴 (𝑓‘𝑧) = 𝑏)} & ⊢ 𝐺 = {𝑥 ∣ 𝑥:{𝑌}⟶𝐵} & ⊢ 𝐻 = (𝑔 ∈ 𝐺 ↦ (𝑎 ∈ 𝐴 ↦ (𝑔‘𝑌))) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴) → 𝐻:𝐺–1-1→𝐹) | ||
Theorem | cfsetsnfsetfo 46069* | The mapping of the class of singleton functions into the class of constant functions is a surjection. (Contributed by AV, 14-Sep-2024.) |
⊢ 𝐹 = {𝑓 ∣ (𝑓:𝐴⟶𝐵 ∧ ∃𝑏 ∈ 𝐵 ∀𝑧 ∈ 𝐴 (𝑓‘𝑧) = 𝑏)} & ⊢ 𝐺 = {𝑥 ∣ 𝑥:{𝑌}⟶𝐵} & ⊢ 𝐻 = (𝑔 ∈ 𝐺 ↦ (𝑎 ∈ 𝐴 ↦ (𝑔‘𝑌))) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴) → 𝐻:𝐺–onto→𝐹) | ||
Theorem | cfsetsnfsetf1o 46070* | The mapping of the class of singleton functions into the class of constant functions is a bijection. (Contributed by AV, 14-Sep-2024.) |
⊢ 𝐹 = {𝑓 ∣ (𝑓:𝐴⟶𝐵 ∧ ∃𝑏 ∈ 𝐵 ∀𝑧 ∈ 𝐴 (𝑓‘𝑧) = 𝑏)} & ⊢ 𝐺 = {𝑥 ∣ 𝑥:{𝑌}⟶𝐵} & ⊢ 𝐻 = (𝑔 ∈ 𝐺 ↦ (𝑎 ∈ 𝐴 ↦ (𝑔‘𝑌))) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴) → 𝐻:𝐺–1-1-onto→𝐹) | ||
Theorem | fsetprcnexALT 46071* | First version of proof for fsetprcnex 8860, which was much more complicated. (Contributed by AV, 14-Sep-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐴 ≠ ∅) ∧ 𝐵 ∉ V) → {𝑓 ∣ 𝑓:𝐴⟶𝐵} ∉ V) | ||
Theorem | fcoreslem1 46072 | Lemma 1 for fcores 46076. (Contributed by AV, 17-Sep-2024.) |
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ 𝐸 = (ran 𝐹 ∩ 𝐶) & ⊢ 𝑃 = (◡𝐹 “ 𝐶) ⇒ ⊢ (𝜑 → 𝑃 = (◡𝐹 “ 𝐸)) | ||
Theorem | fcoreslem2 46073 | Lemma 2 for fcores 46076. (Contributed by AV, 17-Sep-2024.) |
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ 𝐸 = (ran 𝐹 ∩ 𝐶) & ⊢ 𝑃 = (◡𝐹 “ 𝐶) & ⊢ 𝑋 = (𝐹 ↾ 𝑃) ⇒ ⊢ (𝜑 → ran 𝑋 = 𝐸) | ||
Theorem | fcoreslem3 46074 | Lemma 3 for fcores 46076. (Contributed by AV, 13-Sep-2024.) |
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ 𝐸 = (ran 𝐹 ∩ 𝐶) & ⊢ 𝑃 = (◡𝐹 “ 𝐶) & ⊢ 𝑋 = (𝐹 ↾ 𝑃) ⇒ ⊢ (𝜑 → 𝑋:𝑃–onto→𝐸) | ||
Theorem | fcoreslem4 46075 | Lemma 4 for fcores 46076. (Contributed by AV, 17-Sep-2024.) |
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ 𝐸 = (ran 𝐹 ∩ 𝐶) & ⊢ 𝑃 = (◡𝐹 “ 𝐶) & ⊢ 𝑋 = (𝐹 ↾ 𝑃) & ⊢ (𝜑 → 𝐺:𝐶⟶𝐷) & ⊢ 𝑌 = (𝐺 ↾ 𝐸) ⇒ ⊢ (𝜑 → (𝑌 ∘ 𝑋) Fn 𝑃) | ||
Theorem | fcores 46076 | Every composite function (𝐺 ∘ 𝐹) can be written as composition of restrictions of the composed functions (to their minimum domains). (Contributed by GL and AV, 17-Sep-2024.) |
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ 𝐸 = (ran 𝐹 ∩ 𝐶) & ⊢ 𝑃 = (◡𝐹 “ 𝐶) & ⊢ 𝑋 = (𝐹 ↾ 𝑃) & ⊢ (𝜑 → 𝐺:𝐶⟶𝐷) & ⊢ 𝑌 = (𝐺 ↾ 𝐸) ⇒ ⊢ (𝜑 → (𝐺 ∘ 𝐹) = (𝑌 ∘ 𝑋)) | ||
Theorem | fcoresf1lem 46077 | Lemma for fcoresf1 46078. (Contributed by AV, 18-Sep-2024.) |
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ 𝐸 = (ran 𝐹 ∩ 𝐶) & ⊢ 𝑃 = (◡𝐹 “ 𝐶) & ⊢ 𝑋 = (𝐹 ↾ 𝑃) & ⊢ (𝜑 → 𝐺:𝐶⟶𝐷) & ⊢ 𝑌 = (𝐺 ↾ 𝐸) ⇒ ⊢ ((𝜑 ∧ 𝑍 ∈ 𝑃) → ((𝐺 ∘ 𝐹)‘𝑍) = (𝑌‘(𝑋‘𝑍))) | ||
Theorem | fcoresf1 46078 | If a composition is injective, then the restrictions of its components to the minimum domains are injective. (Contributed by GL and AV, 18-Sep-2024.) (Revised by AV, 7-Oct-2024.) |
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ 𝐸 = (ran 𝐹 ∩ 𝐶) & ⊢ 𝑃 = (◡𝐹 “ 𝐶) & ⊢ 𝑋 = (𝐹 ↾ 𝑃) & ⊢ (𝜑 → 𝐺:𝐶⟶𝐷) & ⊢ 𝑌 = (𝐺 ↾ 𝐸) & ⊢ (𝜑 → (𝐺 ∘ 𝐹):𝑃–1-1→𝐷) ⇒ ⊢ (𝜑 → (𝑋:𝑃–1-1→𝐸 ∧ 𝑌:𝐸–1-1→𝐷)) | ||
Theorem | fcoresf1b 46079 | A composition is injective iff the restrictions of its components to the minimum domains are injective. (Contributed by GL and AV, 7-Oct-2024.) |
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ 𝐸 = (ran 𝐹 ∩ 𝐶) & ⊢ 𝑃 = (◡𝐹 “ 𝐶) & ⊢ 𝑋 = (𝐹 ↾ 𝑃) & ⊢ (𝜑 → 𝐺:𝐶⟶𝐷) & ⊢ 𝑌 = (𝐺 ↾ 𝐸) ⇒ ⊢ (𝜑 → ((𝐺 ∘ 𝐹):𝑃–1-1→𝐷 ↔ (𝑋:𝑃–1-1→𝐸 ∧ 𝑌:𝐸–1-1→𝐷))) | ||
Theorem | fcoresfo 46080 | If a composition is surjective, then the restriction of its first component to the minimum domain is surjective. (Contributed by AV, 17-Sep-2024.) |
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ 𝐸 = (ran 𝐹 ∩ 𝐶) & ⊢ 𝑃 = (◡𝐹 “ 𝐶) & ⊢ 𝑋 = (𝐹 ↾ 𝑃) & ⊢ (𝜑 → 𝐺:𝐶⟶𝐷) & ⊢ 𝑌 = (𝐺 ↾ 𝐸) & ⊢ (𝜑 → (𝐺 ∘ 𝐹):𝑃–onto→𝐷) ⇒ ⊢ (𝜑 → 𝑌:𝐸–onto→𝐷) | ||
Theorem | fcoresfob 46081 | A composition is surjective iff the restriction of its first component to the minimum domain is surjective. (Contributed by GL and AV, 7-Oct-2024.) |
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ 𝐸 = (ran 𝐹 ∩ 𝐶) & ⊢ 𝑃 = (◡𝐹 “ 𝐶) & ⊢ 𝑋 = (𝐹 ↾ 𝑃) & ⊢ (𝜑 → 𝐺:𝐶⟶𝐷) & ⊢ 𝑌 = (𝐺 ↾ 𝐸) ⇒ ⊢ (𝜑 → ((𝐺 ∘ 𝐹):𝑃–onto→𝐷 ↔ 𝑌:𝐸–onto→𝐷)) | ||
Theorem | fcoresf1ob 46082 | A composition is bijective iff the restriction of its first component to the minimum domain is bijective and the restriction of its second component to the minimum domain is injective. (Contributed by GL and AV, 7-Oct-2024.) |
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ 𝐸 = (ran 𝐹 ∩ 𝐶) & ⊢ 𝑃 = (◡𝐹 “ 𝐶) & ⊢ 𝑋 = (𝐹 ↾ 𝑃) & ⊢ (𝜑 → 𝐺:𝐶⟶𝐷) & ⊢ 𝑌 = (𝐺 ↾ 𝐸) ⇒ ⊢ (𝜑 → ((𝐺 ∘ 𝐹):𝑃–1-1-onto→𝐷 ↔ (𝑋:𝑃–1-1→𝐸 ∧ 𝑌:𝐸–1-1-onto→𝐷))) | ||
Theorem | f1cof1blem 46083 | Lemma for f1cof1b 46084 and focofob 46087. (Contributed by AV, 18-Sep-2024.) |
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ 𝐸 = (ran 𝐹 ∩ 𝐶) & ⊢ 𝑃 = (◡𝐹 “ 𝐶) & ⊢ 𝑋 = (𝐹 ↾ 𝑃) & ⊢ (𝜑 → 𝐺:𝐶⟶𝐷) & ⊢ 𝑌 = (𝐺 ↾ 𝐸) & ⊢ (𝜑 → ran 𝐹 = 𝐶) ⇒ ⊢ (𝜑 → ((𝑃 = 𝐴 ∧ 𝐸 = 𝐶) ∧ (𝑋 = 𝐹 ∧ 𝑌 = 𝐺))) | ||
Theorem | f1cof1b 46084 | If the range of 𝐹 equals the domain of 𝐺, then the composition (𝐺 ∘ 𝐹) is injective iff 𝐹 and 𝐺 are both injective. (Contributed by GL and AV, 19-Sep-2024.) |
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐺:𝐶⟶𝐷 ∧ ran 𝐹 = 𝐶) → ((𝐺 ∘ 𝐹):𝐴–1-1→𝐷 ↔ (𝐹:𝐴–1-1→𝐵 ∧ 𝐺:𝐶–1-1→𝐷))) | ||
Theorem | funfocofob 46085 | If the domain of a function 𝐺 is a subset of the range of a function 𝐹, then the composition (𝐺 ∘ 𝐹) is surjective iff 𝐺 is surjective. (Contributed by GL and AV, 29-Sep-2024.) |
⊢ ((Fun 𝐹 ∧ 𝐺:𝐴⟶𝐵 ∧ 𝐴 ⊆ ran 𝐹) → ((𝐺 ∘ 𝐹):(◡𝐹 “ 𝐴)–onto→𝐵 ↔ 𝐺:𝐴–onto→𝐵)) | ||
Theorem | fnfocofob 46086 | If the domain of a function 𝐺 equals the range of a function 𝐹, then the composition (𝐺 ∘ 𝐹) is surjective iff 𝐺 is surjective. (Contributed by GL and AV, 29-Sep-2024.) |
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺:𝐵⟶𝐶 ∧ ran 𝐹 = 𝐵) → ((𝐺 ∘ 𝐹):𝐴–onto→𝐶 ↔ 𝐺:𝐵–onto→𝐶)) | ||
Theorem | focofob 46087 | If the domain of a function 𝐺 equals the range of a function 𝐹, then the composition (𝐺 ∘ 𝐹) is surjective iff 𝐺 and 𝐹 as function to the domain of 𝐺 are both surjective. Symmetric version of fnfocofob 46086 including the fact that 𝐹 is a surjection onto its range. (Contributed by GL and AV, 20-Sep-2024.) (Proof shortened by AV, 29-Sep-2024.) |
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐺:𝐶⟶𝐷 ∧ ran 𝐹 = 𝐶) → ((𝐺 ∘ 𝐹):𝐴–onto→𝐷 ↔ (𝐹:𝐴–onto→𝐶 ∧ 𝐺:𝐶–onto→𝐷))) | ||
Theorem | f1ocof1ob 46088 | If the range of 𝐹 equals the domain of 𝐺, then the composition (𝐺 ∘ 𝐹) is bijective iff 𝐹 and 𝐺 are both bijective. (Contributed by GL and AV, 7-Oct-2024.) |
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐺:𝐶⟶𝐷 ∧ ran 𝐹 = 𝐶) → ((𝐺 ∘ 𝐹):𝐴–1-1-onto→𝐷 ↔ (𝐹:𝐴–1-1→𝐶 ∧ 𝐺:𝐶–1-1-onto→𝐷))) | ||
Theorem | f1ocof1ob2 46089 | If the range of 𝐹 equals the domain of 𝐺, then the composition (𝐺 ∘ 𝐹) is bijective iff 𝐹 and 𝐺 are both bijective. Symmetric version of f1ocof1ob 46088 including the fact that 𝐹 is a surjection onto its range. (Contributed by GL and AV, 20-Sep-2024.) (Proof shortened by AV, 7-Oct-2024.) |
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐺:𝐶⟶𝐷 ∧ ran 𝐹 = 𝐶) → ((𝐺 ∘ 𝐹):𝐴–1-1-onto→𝐷 ↔ (𝐹:𝐴–1-1-onto→𝐶 ∧ 𝐺:𝐶–1-1-onto→𝐷))) | ||
Syntax | caiota 46090 | Extend class notation with an alternative for Russell's definition of a description binder (inverted iota). |
class (℩'𝑥𝜑) | ||
Theorem | aiotajust 46091* | Soundness justification theorem for df-aiota 46092. (Contributed by AV, 24-Aug-2022.) |
⊢ ∩ {𝑦 ∣ {𝑥 ∣ 𝜑} = {𝑦}} = ∩ {𝑧 ∣ {𝑥 ∣ 𝜑} = {𝑧}} | ||
Definition | df-aiota 46092* |
Alternate version of Russell's definition of a description binder, which
can be read as "the unique 𝑥 such that 𝜑", where 𝜑
ordinarily contains 𝑥 as a free variable. Our definition
is
meaningful only when there is exactly one 𝑥 such that 𝜑 is true
(see aiotaval 46102); otherwise, it is not a set (see aiotaexb 46096), or even
more concrete, it is the universe V (see aiotavb 46097). Since this
is an alternative for df-iota 6495, we call this symbol ℩'
alternate iota in the following.
The advantage of this definition is the clear distinguishability of the defined and undefined cases: the alternate iota over a wff is defined iff it is a set (see aiotaexb 46096). With the original definition, there is no corresponding theorem (∃!𝑥𝜑 ↔ (℩𝑥𝜑) ≠ ∅), because ∅ can be a valid unique set satisfying a wff (see, for example, iota0def 46047). Only the right to left implication would hold, see (negated) iotanul 6521. For defined cases, however, both definitions df-iota 6495 and df-aiota 46092 are equivalent, see reuaiotaiota 46095. (Proposed by BJ, 13-Aug-2022.) (Contributed by AV, 24-Aug-2022.) |
⊢ (℩'𝑥𝜑) = ∩ {𝑦 ∣ {𝑥 ∣ 𝜑} = {𝑦}} | ||
Theorem | dfaiota2 46093* | Alternate definition of the alternate version of Russell's definition of a description binder. Definition 8.18 in [Quine] p. 56. (Contributed by AV, 24-Aug-2022.) |
⊢ (℩'𝑥𝜑) = ∩ {𝑦 ∣ ∀𝑥(𝜑 ↔ 𝑥 = 𝑦)} | ||
Theorem | reuabaiotaiota 46094* | The iota and the alternate iota over a wff 𝜑 are equal iff there is a unique satisfying value of {𝑥 ∣ 𝜑} = {𝑦}. (Contributed by AV, 25-Aug-2022.) |
⊢ (∃!𝑦{𝑥 ∣ 𝜑} = {𝑦} ↔ (℩𝑥𝜑) = (℩'𝑥𝜑)) | ||
Theorem | reuaiotaiota 46095 | The iota and the alternate iota over a wff 𝜑 are equal iff there is a unique value 𝑥 satisfying 𝜑. (Contributed by AV, 25-Aug-2022.) |
⊢ (∃!𝑥𝜑 ↔ (℩𝑥𝜑) = (℩'𝑥𝜑)) | ||
Theorem | aiotaexb 46096 | The alternate iota over a wff 𝜑 is a set iff there is a unique value 𝑥 satisfying 𝜑. (Contributed by AV, 25-Aug-2022.) |
⊢ (∃!𝑥𝜑 ↔ (℩'𝑥𝜑) ∈ V) | ||
Theorem | aiotavb 46097 | The alternate iota over a wff 𝜑 is the universe iff there is no unique value 𝑥 satisfying 𝜑. (Contributed by AV, 25-Aug-2022.) |
⊢ (¬ ∃!𝑥𝜑 ↔ (℩'𝑥𝜑) = V) | ||
Theorem | aiotaint 46098 | This is to df-aiota 46092 what iotauni 6518 is to df-iota 6495 (it uses intersection like df-aiota 46092, similar to iotauni 6518 using union like df-iota 6495; we could also prove an analogous result using union here too, in the same way that we have iotaint 6519). (Contributed by BJ, 31-Aug-2024.) |
⊢ (∃!𝑥𝜑 → (℩'𝑥𝜑) = ∩ {𝑥 ∣ 𝜑}) | ||
Theorem | dfaiota3 46099 | Alternate definition of ℩': this is to df-aiota 46092 what dfiota4 6535 is to df-iota 6495. operation using the if operator. It is simpler than df-aiota 46092 and uses no dummy variables, so it would be the preferred definition if ℩' becomes the description binder used in set.mm. (Contributed by BJ, 31-Aug-2024.) |
⊢ (℩'𝑥𝜑) = if(∃!𝑥𝜑, ∩ {𝑥 ∣ 𝜑}, V) | ||
Theorem | iotan0aiotaex 46100 | If the iota over a wff 𝜑 is not empty, the alternate iota over 𝜑 is a set. (Contributed by AV, 25-Aug-2022.) |
⊢ ((℩𝑥𝜑) ≠ ∅ → (℩'𝑥𝜑) ∈ V) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |