![]() |
Metamath
Proof Explorer Theorem List (p. 458 of 479) | < 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-30171) |
![]() (30172-31694) |
![]() (31695-47852) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | mdandyvrx10 45701 | 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 | mdandyvrx11 45702 | 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 45703 | 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 45704 | 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 45705 | 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 45706 | 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 45707 | 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 45708 |
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 45709 |
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 45710 | 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 45711, or with the single axiom adh-minimp 45723. This section proves first adh-minim 45711 from { ax-1 6, ax-2 7 }, followed by the converse, due to Ivo Thomas; and then it proves adh-minimp 45723 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 45711 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 45711 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 45711 | 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 45712 | First lemma for the derivation of ax-1 6 and ax-2 7 from adh-minim 45711 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 45713 | Second lemma for the derivation of ax-1 6 and ax-2 7 from adh-minim 45711 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 45714 | Third lemma for the derivation of ax-1 6 and ax-2 7 from adh-minim 45711 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 45715 | Fourth lemma for the derivation of ax-1 6 and ax-2 7 from adh-minim 45711 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 45716 | Derivation of ax-1 6 from adh-minim 45711 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 45717 | Fifth lemma for the derivation of ax-2 7 from adh-minim 45711 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 45718 | Sixth lemma for the derivation of ax-2 7 from adh-minim 45711 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 45719 | Derivation of a commuted form of ax-2 7 from adh-minim 45711 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 45720 | Derivation of ax-2 7 from adh-minim 45711 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 45721 | Derivation of id 22 (reflexivity of implication, PM *2.08 WhiteheadRussell p. 101) from adh-minim-ax1 45716, adh-minim-ax2 45720, 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 45722 | Derivation of pm2.43 56 WhiteheadRussell p. 106 (also called "hilbert" or "W") from adh-minim-ax1 45716, adh-minim-ax2 45720, 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 45723 | 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 45724 | 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 45723 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 45725 | 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 45723 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 45726 | 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 45723 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 45727 | Derivation of jarr 106 (also called "syll-simp") from minimp 1624 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 45728 | Derivation of ax-1 6 from adh-minimp 45723 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 45729 | Derivation of imim1 83 ("left antimonotonicity of implication", theorem *2.06 of [WhiteheadRussell] p. 100) from adh-minimp 45723 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 45730 | Derivation of a commuted form of ax-2 7 from adh-minimp 45723 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 45731 | Fourth lemma for the derivation of ax-2 7 from adh-minimp 45723 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 45732 | Derivation of ax-2 7 from adh-minimp 45723 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 45733 | Derivation of id 22 (reflexivity of implication, PM *2.08 WhiteheadRussell p. 101) from adh-minimp-ax1 45728, adh-minimp-ax2 45732, 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 45734 | Derivation of pm2.43 56 WhiteheadRussell p. 106 (also called "hilbert" or "W") from adh-minimp-ax1 45728, adh-minimp-ax2 45732, 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 45735* | 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 45736* | There is a unique element of a singleton which is equal to another singleton. (Contributed by AV, 24-Aug-2022.) |
⊢ ∃!𝑥{𝑥} = {𝑦} | ||
Theorem | absnsb 45737* | 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 45738* | Another way to express existential uniqueness of a wff 𝜑: its associated class abstraction {𝑥 ∣ 𝜑} is a singleton. Variant of euabsn2 4730 using existential uniqueness for the singleton element instead of existence only. (Contributed by AV, 24-Aug-2022.) |
⊢ (∃!𝑥𝜑 ↔ ∃!𝑦{𝑥 ∣ 𝜑} = {𝑦}) | ||
Theorem | elprneb 45739 | 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 45740 | Equality for ordered pairs implies equality of unordered pairs with the same elements. (Contributed by AV, 9-Jul-2023.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → {𝐴, 𝐵} = {𝐶, 𝐷})) | ||
Theorem | opprb 45741 | Equality for unordered pairs corresponds to equality of unordered pairs with the same elements. (Contributed by AV, 9-Jul-2023.) |
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌)) → ({𝐴, 𝐵} = {𝐶, 𝐷} ↔ (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ ∨ ⟨𝐴, 𝐵⟩ = ⟨𝐷, 𝐶⟩))) | ||
Theorem | or2expropbilem1 45742* | Lemma 1 for or2expropbi 45744 and ich2exprop 46139. (Contributed by AV, 16-Jul-2023.) |
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝐴 = 𝑎 ∧ 𝐵 = 𝑏) → (𝜑 → ∃𝑥∃𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ [𝑦 / 𝑏][𝑥 / 𝑎]𝜑)))) | ||
Theorem | or2expropbilem2 45743* | Lemma 2 for or2expropbi 45744 and ich2exprop 46139. (Contributed by AV, 16-Jul-2023.) |
⊢ (∃𝑎∃𝑏(⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ↔ ∃𝑥∃𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ [𝑦 / 𝑏][𝑥 / 𝑎]𝜑)) | ||
Theorem | or2expropbi 45744* | 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 45745* | 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 45746* | 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 45747 | Element of the domain of a restriction to a singleton. (Contributed by Alexander van der Vekens, 2-Jul-2017.) |
⊢ (𝐵 ∈ dom (𝐹 ↾ {𝐴}) → 𝐵 = 𝐴) | ||
Theorem | iota0def 45748* | 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 45749* | 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 45750 | If a function's value at an argument is the universal class (which can never be the case because of fvex 6905), 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 45751 | Composition of two functions, similar to fnco 6668. (Contributed by Alexander van der Vekens, 25-Jul-2017.) |
⊢ (((𝐹 ↾ ran 𝐺) Fn ran 𝐺 ∧ 𝐺 Fn 𝐵) → (𝐹 ∘ 𝐺) Fn 𝐵) | ||
Theorem | funcoressn 45752 | 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 45753 | 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 45754 | 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 45755* | 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 45756* | 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 45757* | There is exactly one value of a class which is a function restricted to a singleton, analogous to funeu 6574. 𝐴 ∈ V is required because otherwise ∃!𝑦𝐴𝐹𝑦, see brprcneu 6882. (Contributed by AV, 7-Sep-2022.) |
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ Fun (𝐹 ↾ {𝐴}) ∧ 𝐴𝐹𝐵) → ∃!𝑦 𝐴𝐹𝑦) | ||
Theorem | fresfo 45758 | Conditions for a restriction to be an onto function. Part of fresf1o 31855. (Contributed by AV, 29-Sep-2024.) |
⊢ ((Fun 𝐹 ∧ 𝐶 ⊆ ran 𝐹) → (𝐹 ↾ (◡𝐹 “ 𝐶)):(◡𝐹 “ 𝐶)–onto→𝐶) | ||
Theorem | fsetsniunop 45759* | 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 45760* | 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 45761* | The mapping of an element of a class to a singleton function is a function. (Contributed by AV, 13-Sep-2024.) |
⊢ 𝐴 = {𝑦 ∣ ∃𝑏 ∈ 𝐵 𝑦 = {⟨𝑆, 𝑏⟩}} & ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ {⟨𝑆, 𝑥⟩}) ⇒ ⊢ (𝑆 ∈ 𝑉 → 𝐹:𝐵⟶𝐴) | ||
Theorem | fsetsnf1 45762* | 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 45763* | The mapping of an element of a class to a singleton function is a surjection. (Contributed by AV, 13-Sep-2024.) |
⊢ 𝐴 = {𝑦 ∣ ∃𝑏 ∈ 𝐵 𝑦 = {⟨𝑆, 𝑏⟩}} & ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ {⟨𝑆, 𝑥⟩}) ⇒ ⊢ (𝑆 ∈ 𝑉 → 𝐹:𝐵–onto→𝐴) | ||
Theorem | fsetsnf1o 45764* | 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 45765* | 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 45766 | The class of constant functions is a subclass of the class of functions. (Contributed by AV, 13-Sep-2024.) |
⊢ 𝐹 = {𝑓 ∣ (𝑓:𝐴⟶𝐵 ∧ ∃𝑏 ∈ 𝐵 ∀𝑧 ∈ 𝐴 (𝑓‘𝑧) = 𝑏)} ⇒ ⊢ 𝐹 ⊆ {𝑓 ∣ 𝑓:𝐴⟶𝐵} | ||
Theorem | cfsetsnfsetfv 45767* | 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 45768* | 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 45769* | 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 45770* | 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 45771* | 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 45772* | First version of proof for fsetprcnex 8856, which was much more complicated. (Contributed by AV, 14-Sep-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐴 ≠ ∅) ∧ 𝐵 ∉ V) → {𝑓 ∣ 𝑓:𝐴⟶𝐵} ∉ V) | ||
Theorem | fcoreslem1 45773 | Lemma 1 for fcores 45777. (Contributed by AV, 17-Sep-2024.) |
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ 𝐸 = (ran 𝐹 ∩ 𝐶) & ⊢ 𝑃 = (◡𝐹 “ 𝐶) ⇒ ⊢ (𝜑 → 𝑃 = (◡𝐹 “ 𝐸)) | ||
Theorem | fcoreslem2 45774 | Lemma 2 for fcores 45777. (Contributed by AV, 17-Sep-2024.) |
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ 𝐸 = (ran 𝐹 ∩ 𝐶) & ⊢ 𝑃 = (◡𝐹 “ 𝐶) & ⊢ 𝑋 = (𝐹 ↾ 𝑃) ⇒ ⊢ (𝜑 → ran 𝑋 = 𝐸) | ||
Theorem | fcoreslem3 45775 | Lemma 3 for fcores 45777. (Contributed by AV, 13-Sep-2024.) |
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ 𝐸 = (ran 𝐹 ∩ 𝐶) & ⊢ 𝑃 = (◡𝐹 “ 𝐶) & ⊢ 𝑋 = (𝐹 ↾ 𝑃) ⇒ ⊢ (𝜑 → 𝑋:𝑃–onto→𝐸) | ||
Theorem | fcoreslem4 45776 | Lemma 4 for fcores 45777. (Contributed by AV, 17-Sep-2024.) |
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ 𝐸 = (ran 𝐹 ∩ 𝐶) & ⊢ 𝑃 = (◡𝐹 “ 𝐶) & ⊢ 𝑋 = (𝐹 ↾ 𝑃) & ⊢ (𝜑 → 𝐺:𝐶⟶𝐷) & ⊢ 𝑌 = (𝐺 ↾ 𝐸) ⇒ ⊢ (𝜑 → (𝑌 ∘ 𝑋) Fn 𝑃) | ||
Theorem | fcores 45777 | 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 45778 | Lemma for fcoresf1 45779. (Contributed by AV, 18-Sep-2024.) |
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ 𝐸 = (ran 𝐹 ∩ 𝐶) & ⊢ 𝑃 = (◡𝐹 “ 𝐶) & ⊢ 𝑋 = (𝐹 ↾ 𝑃) & ⊢ (𝜑 → 𝐺:𝐶⟶𝐷) & ⊢ 𝑌 = (𝐺 ↾ 𝐸) ⇒ ⊢ ((𝜑 ∧ 𝑍 ∈ 𝑃) → ((𝐺 ∘ 𝐹)‘𝑍) = (𝑌‘(𝑋‘𝑍))) | ||
Theorem | fcoresf1 45779 | 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 45780 | 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 45781 | 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 45782 | 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 45783 | 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 45784 | Lemma for f1cof1b 45785 and focofob 45788. (Contributed by AV, 18-Sep-2024.) |
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ 𝐸 = (ran 𝐹 ∩ 𝐶) & ⊢ 𝑃 = (◡𝐹 “ 𝐶) & ⊢ 𝑋 = (𝐹 ↾ 𝑃) & ⊢ (𝜑 → 𝐺:𝐶⟶𝐷) & ⊢ 𝑌 = (𝐺 ↾ 𝐸) & ⊢ (𝜑 → ran 𝐹 = 𝐶) ⇒ ⊢ (𝜑 → ((𝑃 = 𝐴 ∧ 𝐸 = 𝐶) ∧ (𝑋 = 𝐹 ∧ 𝑌 = 𝐺))) | ||
Theorem | f1cof1b 45785 | 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 45786 | 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 45787 | 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 45788 | 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 45787 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 45789 | 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 45790 | If the range of 𝐹 equals the domain of 𝐺, then the composition (𝐺 ∘ 𝐹) is bijective iff 𝐹 and 𝐺 are both bijective. Symmetric version of f1ocof1ob 45789 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 45791 | Extend class notation with an alternative for Russell's definition of a description binder (inverted iota). |
class (℩'𝑥𝜑) | ||
Theorem | aiotajust 45792* | Soundness justification theorem for df-aiota 45793. (Contributed by AV, 24-Aug-2022.) |
⊢ ∩ {𝑦 ∣ {𝑥 ∣ 𝜑} = {𝑦}} = ∩ {𝑧 ∣ {𝑥 ∣ 𝜑} = {𝑧}} | ||
Definition | df-aiota 45793* |
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 45803); otherwise, it is not a set (see aiotaexb 45797), or even
more concrete, it is the universe V (see aiotavb 45798). Since this
is an alternative for df-iota 6496, 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 45797). With the original definition, there is no corresponding theorem (∃!𝑥𝜑 ↔ (℩𝑥𝜑) ≠ ∅), because ∅ can be a valid unique set satisfying a wff (see, for example, iota0def 45748). Only the right to left implication would hold, see (negated) iotanul 6522. For defined cases, however, both definitions df-iota 6496 and df-aiota 45793 are equivalent, see reuaiotaiota 45796. (Proposed by BJ, 13-Aug-2022.) (Contributed by AV, 24-Aug-2022.) |
⊢ (℩'𝑥𝜑) = ∩ {𝑦 ∣ {𝑥 ∣ 𝜑} = {𝑦}} | ||
Theorem | dfaiota2 45794* | 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 45795* | 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 45796 | 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 45797 | 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 45798 | 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 45799 | This is to df-aiota 45793 what iotauni 6519 is to df-iota 6496 (it uses intersection like df-aiota 45793, similar to iotauni 6519 using union like df-iota 6496; we could also prove an analogous result using union here too, in the same way that we have iotaint 6520). (Contributed by BJ, 31-Aug-2024.) |
⊢ (∃!𝑥𝜑 → (℩'𝑥𝜑) = ∩ {𝑥 ∣ 𝜑}) | ||
Theorem | dfaiota3 45800 | Alternate definition of ℩': this is to df-aiota 45793 what dfiota4 6536 is to df-iota 6496. operation using the if operator. It is simpler than df-aiota 45793 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) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |