P. 465 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 46401-46500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	mdandyvrx9 46401	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	mdandyvrx10 46402	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 46403	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 46404	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 46405	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 46406	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 46407	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 46408	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 46409	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 46410	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 ↔ ⊥)))
21.44  Mathbox for Adhemar
Theorem	adh-jarrsc 46411	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.)
⊢ (((𝜑 → 𝜓) → 𝜒) → (𝜃 → (𝜓 → 𝜒)))
21.44.1  Minimal implicational calculus 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 46412, or with the single axiom adh-minimp 46424. This section proves first adh-minim 46412 from { ax-1 6, ax-2 7 }, followed by the converse, due to Ivo Thomas; and then it proves adh-minimp 46424 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 46412 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 46412 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 46412	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 46413	First lemma for the derivation of ax-1 6 and ax-2 7 from adh-minim 46412 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 46414	Second lemma for the derivation of ax-1 6 and ax-2 7 from adh-minim 46412 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 46415	Third lemma for the derivation of ax-1 6 and ax-2 7 from adh-minim 46412 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 46416	Fourth lemma for the derivation of ax-1 6 and ax-2 7 from adh-minim 46412 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 46417	Derivation of ax-1 6 from adh-minim 46412 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 46418	Fifth lemma for the derivation of ax-2 7 from adh-minim 46412 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 46419	Sixth lemma for the derivation of ax-2 7 from adh-minim 46412 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 46420	Derivation of a commuted form of ax-2 7 from adh-minim 46412 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 46421	Derivation of ax-2 7 from adh-minim 46412 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 46422	Derivation of id 22 (reflexivity of implication, PM *2.08 WhiteheadRussell p. 101) from adh-minim-ax1 46417, adh-minim-ax2 46421, 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 46423	Derivation of pm2.43 56 WhiteheadRussell p. 106 (also called "hilbert" or "W") from adh-minim-ax1 46417, adh-minim-ax2 46421, 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 46424	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 46425	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 46424 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 46426	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 46424 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 46427	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 46424 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 46428	Derivation of jarr 106 (also called "syll-simp") from minimp 1615 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 46429	Derivation of ax-1 6 from adh-minimp 46424 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 46430	Derivation of imim1 83 ("left antimonotonicity of implication", theorem *2.06 of [WhiteheadRussell] p. 100) from adh-minimp 46424 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 46431	Derivation of a commuted form of ax-2 7 from adh-minimp 46424 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 46432	Fourth lemma for the derivation of ax-2 7 from adh-minimp 46424 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 46433	Derivation of ax-2 7 from adh-minimp 46424 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 46434	Derivation of id 22 (reflexivity of implication, PM *2.08 WhiteheadRussell p. 101) from adh-minimp-ax1 46429, adh-minimp-ax2 46433, 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 46435	Derivation of pm2.43 56 WhiteheadRussell p. 106 (also called "hilbert" or "W") from adh-minimp-ax1 46429, adh-minimp-ax2 46433, 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.)
⊢ ((𝜑 → (𝜑 → 𝜓)) → (𝜑 → 𝜓))
21.45  Mathbox for Alexander van der Vekens
21.45.1  General auxiliary theorems (1)
21.45.1.1  Unordered and ordered pairs - extension for singletons
Theorem	n0nsn2el 46436*	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 46437*	There is a unique element of a singleton which is equal to another singleton. (Contributed by AV, 24-Aug-2022.)
⊢ ∃!𝑥{𝑥} = {𝑦}
Theorem	absnsb 46438*	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 46439*	Another way to express existential uniqueness of a wff 𝜑: its associated class abstraction {𝑥 ∣ 𝜑} is a singleton. Variant of euabsn2 4734 using existential uniqueness for the singleton element instead of existence only. (Contributed by AV, 24-Aug-2022.)
⊢ (∃!𝑥𝜑 ↔ ∃!𝑦{𝑥 ∣ 𝜑} = {𝑦})
21.45.1.2  Unordered and ordered pairs - extension for unordered pairs
Theorem	elprneb 46440	An element of a proper unordered pair is the first element iff it is not the second element. (Contributed by AV, 18-Jun-2020.)
⊢ ((𝐴 ∈ {𝐵, 𝐶} ∧ 𝐵 ≠ 𝐶) → (𝐴 = 𝐵 ↔ 𝐴 ≠ 𝐶))
21.45.1.3  Unordered and ordered pairs - extension for ordered pairs
Theorem	oppr 46441	Equality for ordered pairs implies equality of unordered pairs with the same elements. (Contributed by AV, 9-Jul-2023.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → {𝐴, 𝐵} = {𝐶, 𝐷}))
Theorem	opprb 46442	Equality for unordered pairs corresponds to equality of unordered pairs with the same elements. (Contributed by AV, 9-Jul-2023.)
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌)) → ({𝐴, 𝐵} = {𝐶, 𝐷} ↔ (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ ∨ ⟨𝐴, 𝐵⟩ = ⟨𝐷, 𝐶⟩)))
Theorem	or2expropbilem1 46443*	Lemma 1 for or2expropbi 46445 and ich2exprop 46840. (Contributed by AV, 16-Jul-2023.)
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝐴 = 𝑎 ∧ 𝐵 = 𝑏) → (𝜑 → ∃𝑥∃𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ [𝑦 / 𝑏][𝑥 / 𝑎]𝜑))))
Theorem	or2expropbilem2 46444*	Lemma 2 for or2expropbi 46445 and ich2exprop 46840. (Contributed by AV, 16-Jul-2023.)
⊢ (∃𝑎∃𝑏(⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ↔ ∃𝑥∃𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ [𝑦 / 𝑏][𝑥 / 𝑎]𝜑))
Theorem	or2expropbi 46445*	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 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴𝑅𝐵)) → (∃𝑎∃𝑏({𝐴, 𝐵} = {𝑎, 𝑏} ∧ (𝑎𝑅𝑏 ∧ 𝜑)) ↔ ∃𝑎∃𝑏(⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ (𝑎𝑅𝑏 ∧ 𝜑))))
21.45.1.4  Relations - extension
Theorem	eubrv 46446*	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 46447*	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 46448	Element of the domain of a restriction to a singleton. (Contributed by Alexander van der Vekens, 2-Jul-2017.)
⊢ (𝐵 ∈ dom (𝐹 ↾ {𝐴}) → 𝐵 = 𝐴)
21.45.1.5  Definite description binder (inverted iota) - extension
Theorem	iota0def 46449*	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 46450*	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.)
⊢ (℩𝑥∀𝑦 𝑦 ∈ 𝑥) = ∅
21.45.1.6  Functions - extension
Theorem	fveqvfvv 46451	If a function's value at an argument is the universal class (which can never be the case because of fvex 6915), 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 46452	Composition of two functions, similar to fnco 6677. (Contributed by Alexander van der Vekens, 25-Jul-2017.)
⊢ (((𝐹 ↾ ran 𝐺) Fn ran 𝐺 ∧ 𝐺 Fn 𝐵) → (𝐹 ∘ 𝐺) Fn 𝐵)
Theorem	funcoressn 46453	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 46454	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 46455	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 46456*	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 46457*	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 46458*	There is exactly one value of a class which is a function restricted to a singleton, analogous to funeu 6583. 𝐴 ∈ V is required because otherwise ∃!𝑦𝐴𝐹𝑦, see brprcneu 6892. (Contributed by AV, 7-Sep-2022.)
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ Fun (𝐹 ↾ {𝐴}) ∧ 𝐴𝐹𝐵) → ∃!𝑦 𝐴𝐹𝑦)
Theorem	fresfo 46459	Conditions for a restriction to be an onto function. Part of fresf1o 32437. (Contributed by AV, 29-Sep-2024.)
⊢ ((Fun 𝐹 ∧ 𝐶 ⊆ ran 𝐹) → (𝐹 ↾ (◡𝐹 “ 𝐶)):(◡𝐹 “ 𝐶)–onto→𝐶)
Theorem	fsetsniunop 46460*	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 46461*	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 46462*	The mapping of an element of a class to a singleton function is a function. (Contributed by AV, 13-Sep-2024.)
⊢ 𝐴 = {𝑦 ∣ ∃𝑏 ∈ 𝐵 𝑦 = {⟨𝑆, 𝑏⟩}}    &   ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ {⟨𝑆, 𝑥⟩})    ⇒   ⊢ (𝑆 ∈ 𝑉 → 𝐹:𝐵⟶𝐴)
Theorem	fsetsnf1 46463*	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 46464*	The mapping of an element of a class to a singleton function is a surjection. (Contributed by AV, 13-Sep-2024.)
⊢ 𝐴 = {𝑦 ∣ ∃𝑏 ∈ 𝐵 𝑦 = {⟨𝑆, 𝑏⟩}}    &   ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ {⟨𝑆, 𝑥⟩})    ⇒   ⊢ (𝑆 ∈ 𝑉 → 𝐹:𝐵–onto→𝐴)
Theorem	fsetsnf1o 46465*	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 46466*	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 46467	The class of constant functions is a subclass of the class of functions. (Contributed by AV, 13-Sep-2024.)
⊢ 𝐹 = {𝑓 ∣ (𝑓:𝐴⟶𝐵 ∧ ∃𝑏 ∈ 𝐵 ∀𝑧 ∈ 𝐴 (𝑓‘𝑧) = 𝑏)}    ⇒   ⊢ 𝐹 ⊆ {𝑓 ∣ 𝑓:𝐴⟶𝐵}
Theorem	cfsetsnfsetfv 46468*	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 46469*	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 46470*	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 46471*	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 46472*	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 46473*	First version of proof for fsetprcnex 8887, which was much more complicated. (Contributed by AV, 14-Sep-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐴 ≠ ∅) ∧ 𝐵 ∉ V) → {𝑓 ∣ 𝑓:𝐴⟶𝐵} ∉ V)
Theorem	fcoreslem1 46474	Lemma 1 for fcores 46478. (Contributed by AV, 17-Sep-2024.)
⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ 𝐸 = (ran 𝐹 ∩ 𝐶)    &   ⊢ 𝑃 = (◡𝐹 “ 𝐶)    ⇒   ⊢ (𝜑 → 𝑃 = (◡𝐹 “ 𝐸))
Theorem	fcoreslem2 46475	Lemma 2 for fcores 46478. (Contributed by AV, 17-Sep-2024.)
⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ 𝐸 = (ran 𝐹 ∩ 𝐶)    &   ⊢ 𝑃 = (◡𝐹 “ 𝐶)    &   ⊢ 𝑋 = (𝐹 ↾ 𝑃)    ⇒   ⊢ (𝜑 → ran 𝑋 = 𝐸)
Theorem	fcoreslem3 46476	Lemma 3 for fcores 46478. (Contributed by AV, 13-Sep-2024.)
⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ 𝐸 = (ran 𝐹 ∩ 𝐶)    &   ⊢ 𝑃 = (◡𝐹 “ 𝐶)    &   ⊢ 𝑋 = (𝐹 ↾ 𝑃)    ⇒   ⊢ (𝜑 → 𝑋:𝑃–onto→𝐸)
Theorem	fcoreslem4 46477	Lemma 4 for fcores 46478. (Contributed by AV, 17-Sep-2024.)
⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ 𝐸 = (ran 𝐹 ∩ 𝐶)    &   ⊢ 𝑃 = (◡𝐹 “ 𝐶)    &   ⊢ 𝑋 = (𝐹 ↾ 𝑃)    &   ⊢ (𝜑 → 𝐺:𝐶⟶𝐷)    &   ⊢ 𝑌 = (𝐺 ↾ 𝐸)    ⇒   ⊢ (𝜑 → (𝑌 ∘ 𝑋) Fn 𝑃)
Theorem	fcores 46478	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 46479	Lemma for fcoresf1 46480. (Contributed by AV, 18-Sep-2024.)
⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ 𝐸 = (ran 𝐹 ∩ 𝐶)    &   ⊢ 𝑃 = (◡𝐹 “ 𝐶)    &   ⊢ 𝑋 = (𝐹 ↾ 𝑃)    &   ⊢ (𝜑 → 𝐺:𝐶⟶𝐷)    &   ⊢ 𝑌 = (𝐺 ↾ 𝐸)    ⇒   ⊢ ((𝜑 ∧ 𝑍 ∈ 𝑃) → ((𝐺 ∘ 𝐹)‘𝑍) = (𝑌‘(𝑋‘𝑍)))
Theorem	fcoresf1 46480	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 46481	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 46482	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 46483	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 46484	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 46485	Lemma for f1cof1b 46486 and focofob 46489. (Contributed by AV, 18-Sep-2024.)
⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ 𝐸 = (ran 𝐹 ∩ 𝐶)    &   ⊢ 𝑃 = (◡𝐹 “ 𝐶)    &   ⊢ 𝑋 = (𝐹 ↾ 𝑃)    &   ⊢ (𝜑 → 𝐺:𝐶⟶𝐷)    &   ⊢ 𝑌 = (𝐺 ↾ 𝐸)    &   ⊢ (𝜑 → ran 𝐹 = 𝐶)    ⇒   ⊢ (𝜑 → ((𝑃 = 𝐴 ∧ 𝐸 = 𝐶) ∧ (𝑋 = 𝐹 ∧ 𝑌 = 𝐺)))
Theorem	f1cof1b 46486	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 46487	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 46488	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 46489	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 46488 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 46490	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 46491	If the range of 𝐹 equals the domain of 𝐺, then the composition (𝐺 ∘ 𝐹) is bijective iff 𝐹 and 𝐺 are both bijective. Symmetric version of f1ocof1ob 46490 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→𝐷)))
21.45.2  Alternative for Russell's definition of a description binder
Syntax	caiota 46492	Extend class notation with an alternative for Russell's definition of a description binder (inverted iota).
class (℩'𝑥𝜑)
Theorem	aiotajust 46493*	Soundness justification theorem for df-aiota 46494. (Contributed by AV, 24-Aug-2022.)
⊢ ∩ {𝑦 ∣ {𝑥 ∣ 𝜑} = {𝑦}} = ∩ {𝑧 ∣ {𝑥 ∣ 𝜑} = {𝑧}}
Definition	df-aiota 46494*	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 46504); otherwise, it is not a set (see aiotaexb 46498), or even more concrete, it is the universe V (see aiotavb 46499). Since this is an alternative for df-iota 6505, 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 46498). With the original definition, there is no corresponding theorem (∃!𝑥𝜑 ↔ (℩𝑥𝜑) ≠ ∅), because ∅ can be a valid unique set satisfying a wff (see, for example, iota0def 46449). Only the right to left implication would hold, see (negated) iotanul 6531. For defined cases, however, both definitions df-iota 6505 and df-aiota 46494 are equivalent, see reuaiotaiota 46497. (Proposed by BJ, 13-Aug-2022.) (Contributed by AV, 24-Aug-2022.)
⊢ (℩'𝑥𝜑) = ∩ {𝑦 ∣ {𝑥 ∣ 𝜑} = {𝑦}}
Theorem	dfaiota2 46495*	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 46496*	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 46497	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 46498	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 46499	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 46500	This is to df-aiota 46494 what iotauni 6528 is to df-iota 6505 (it uses intersection like df-aiota 46494, similar to iotauni 6528 using union like df-iota 6505; we could also prove an analogous result using union here too, in the same way that we have iotaint 6529). (Contributed by BJ, 31-Aug-2024.)
⊢ (∃!𝑥𝜑 → (℩'𝑥𝜑) = ∩ {𝑥 ∣ 𝜑})