Home | Metamath
Proof Explorer Theorem List (p. 311 of 424) | < 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: | Metamath Proof Explorer
(1-27159) |
Hilbert Space Explorer
(27160-28684) |
Users' Mathboxes
(28685-42360) |
Type | Label | Description |
---|---|---|
Statement | ||
Definition | df-wsucOLD 31001 | Define the concept of a successor in a well-founded set. (Contributed by Scott Fenton, 13-Jun-2018.) Obsolete version of df-wsuc 31000 as of 10-Oct-2021. (New usage is discouraged.) |
⊢ wsucOLD(𝑅, 𝐴, 𝑋) = sup(Pred(◡𝑅, 𝐴, 𝑋), 𝐴, ◡𝑅) | ||
Definition | df-wlim 31002* | Define the class of limit points of a well-founded set. (Contributed by Scott Fenton, 15-Jun-2018.) (Revised by AV, 10-Oct-2021.) |
⊢ WLim(𝑅, 𝐴) = {𝑥 ∈ 𝐴 ∣ (𝑥 ≠ inf(𝐴, 𝐴, 𝑅) ∧ 𝑥 = sup(Pred(𝑅, 𝐴, 𝑥), 𝐴, 𝑅))} | ||
Definition | df-wlimOLD 31003* | Define the class of limit points of a well-founded set. (Contributed by Scott Fenton, 15-Jun-2018.) Obsolete version of df-wlim 31002 as of 10-Oct-2021. (New usage is discouraged.) |
⊢ WLimOLD(𝑅, 𝐴) = {𝑥 ∈ 𝐴 ∣ (𝑥 ≠ sup(𝐴, 𝐴, ◡𝑅) ∧ 𝑥 = sup(Pred(𝑅, 𝐴, 𝑥), 𝐴, 𝑅))} | ||
Theorem | wsuceq123 31004 | Equality theorem for well-founded successor. (Contributed by Scott Fenton, 13-Jun-2018.) (Proof shortened by AV, 10-Oct-2021.) |
⊢ ((𝑅 = 𝑆 ∧ 𝐴 = 𝐵 ∧ 𝑋 = 𝑌) → wsuc(𝑅, 𝐴, 𝑋) = wsuc(𝑆, 𝐵, 𝑌)) | ||
Theorem | wsuceq1 31005 | Equality theorem for well-founded successor. (Contributed by Scott Fenton, 13-Jun-2018.) |
⊢ (𝑅 = 𝑆 → wsuc(𝑅, 𝐴, 𝑋) = wsuc(𝑆, 𝐴, 𝑋)) | ||
Theorem | wsuceq2 31006 | Equality theorem for well-founded successor. (Contributed by Scott Fenton, 13-Jun-2018.) |
⊢ (𝐴 = 𝐵 → wsuc(𝑅, 𝐴, 𝑋) = wsuc(𝑅, 𝐵, 𝑋)) | ||
Theorem | wsuceq3 31007 | Equality theorem for well-founded successor. (Contributed by Scott Fenton, 13-Jun-2018.) |
⊢ (𝑋 = 𝑌 → wsuc(𝑅, 𝐴, 𝑋) = wsuc(𝑅, 𝐴, 𝑌)) | ||
Theorem | nfwsuc 31008 | Bound-variable hypothesis builder for well-founded successor. (Contributed by Scott Fenton, 13-Jun-2018.) (Proof shortened by AV, 10-Oct-2021.) |
⊢ Ⅎ𝑥𝑅 & ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝑋 ⇒ ⊢ Ⅎ𝑥wsuc(𝑅, 𝐴, 𝑋) | ||
Theorem | wlimeq12 31009 | Equality theorem for the limit class. (Contributed by Scott Fenton, 15-Jun-2018.) (Proof shortened by AV, 10-Oct-2021.) |
⊢ ((𝑅 = 𝑆 ∧ 𝐴 = 𝐵) → WLim(𝑅, 𝐴) = WLim(𝑆, 𝐵)) | ||
Theorem | wlimeq1 31010 | Equality theorem for the limit class. (Contributed by Scott Fenton, 15-Jun-2018.) |
⊢ (𝑅 = 𝑆 → WLim(𝑅, 𝐴) = WLim(𝑆, 𝐴)) | ||
Theorem | wlimeq2 31011 | Equality theorem for the limit class. (Contributed by Scott Fenton, 15-Jun-2018.) |
⊢ (𝐴 = 𝐵 → WLim(𝑅, 𝐴) = WLim(𝑅, 𝐵)) | ||
Theorem | nfwlim 31012 | Bound-variable hypothesis builder for the limit class. (Contributed by Scott Fenton, 15-Jun-2018.) (Proof shortened by AV, 10-Oct-2021.) |
⊢ Ⅎ𝑥𝑅 & ⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥WLim(𝑅, 𝐴) | ||
Theorem | elwlim 31013 | Membership in the limit class. (Contributed by Scott Fenton, 15-Jun-2018.) (Revised by AV, 10-Oct-2021.) |
⊢ (𝑋 ∈ WLim(𝑅, 𝐴) ↔ (𝑋 ∈ 𝐴 ∧ 𝑋 ≠ inf(𝐴, 𝐴, 𝑅) ∧ 𝑋 = sup(Pred(𝑅, 𝐴, 𝑋), 𝐴, 𝑅))) | ||
Theorem | elwlimOLD 31014 | Membership in the limit class. (Contributed by Scott Fenton, 15-Jun-2018.) Obsolete version of elwlim 31013 as of 10-Oct-2021. (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (𝑋 ∈ WLimOLD(𝑅, 𝐴) ↔ (𝑋 ∈ 𝐴 ∧ 𝑋 ≠ sup(𝐴, 𝐴, ◡𝑅) ∧ 𝑋 = sup(Pred(𝑅, 𝐴, 𝑋), 𝐴, 𝑅))) | ||
Theorem | wzel 31015 | The zero of a well-founded set is a member of that set. (Contributed by Scott Fenton, 13-Jun-2018.) (Revised by AV, 10-Oct-2021.) |
⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐴 ≠ ∅) → inf(𝐴, 𝐴, 𝑅) ∈ 𝐴) | ||
Theorem | wzelOLD 31016 | The zero of a well-founded set is a member of that set. (Contributed by Scott Fenton, 13-Jun-2018.) Obsolete version of wzel 31015 as of 10-Oct-2021. (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐴 ≠ ∅) → sup(𝐴, 𝐴, ◡𝑅) ∈ 𝐴) | ||
Theorem | wsuclem 31017* | Lemma for the supremum properties of well-founded successor. (Contributed by Scott Fenton, 15-Jun-2018.) (Revised by AV, 10-Oct-2021.) |
⊢ (𝜑 → 𝑅 We 𝐴) & ⊢ (𝜑 → 𝑅 Se 𝐴) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → ∃𝑤 ∈ 𝐴 𝑋𝑅𝑤) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ Pred (◡𝑅, 𝐴, 𝑋) ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ Pred (◡𝑅, 𝐴, 𝑋)𝑧𝑅𝑦))) | ||
Theorem | wsuclemOLD 31018* | Obsolete version of wsuclem 31017 as of 10-Oct-2021. (Contributed by Scott Fenton, 15-Jun-2018.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (𝜑 → 𝑅 We 𝐴) & ⊢ (𝜑 → 𝑅 Se 𝐴) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → ∃𝑤 ∈ 𝐴 𝑋𝑅𝑤) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ Pred (◡𝑅, 𝐴, 𝑋) ¬ 𝑥◡𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦◡𝑅𝑥 → ∃𝑧 ∈ Pred (◡𝑅, 𝐴, 𝑋)𝑦◡𝑅𝑧))) | ||
Theorem | wsucex 31019 | Existence theorem for well-founded successor. (Contributed by Scott Fenton, 16-Jun-2018.) (Proof shortened by AV, 10-Oct-2021.) |
⊢ (𝜑 → 𝑅 Or 𝐴) ⇒ ⊢ (𝜑 → wsuc(𝑅, 𝐴, 𝑋) ∈ V) | ||
Theorem | wsuccl 31020* | If 𝑋 is a set with an 𝑅 successor in 𝐴, then its well-founded successor is a member of 𝐴. (Contributed by Scott Fenton, 15-Jun-2018.) (Proof shortened by AV, 10-Oct-2021.) |
⊢ (𝜑 → 𝑅 We 𝐴) & ⊢ (𝜑 → 𝑅 Se 𝐴) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → ∃𝑦 ∈ 𝐴 𝑋𝑅𝑦) ⇒ ⊢ (𝜑 → wsuc(𝑅, 𝐴, 𝑋) ∈ 𝐴) | ||
Theorem | wsuclb 31021 | A well-founded successor is a lower bound on points after 𝑋. (Contributed by Scott Fenton, 16-Jun-2018.) (Proof shortened by AV, 10-Oct-2021.) |
⊢ (𝜑 → 𝑅 We 𝐴) & ⊢ (𝜑 → 𝑅 Se 𝐴) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝐴) & ⊢ (𝜑 → 𝑋𝑅𝑌) ⇒ ⊢ (𝜑 → ¬ 𝑌𝑅wsuc(𝑅, 𝐴, 𝑋)) | ||
Theorem | wlimss 31022 | The class of limit points is a subclass of the base class. (Contributed by Scott Fenton, 16-Jun-2018.) |
⊢ WLim(𝑅, 𝐴) ⊆ 𝐴 | ||
Theorem | frr3g 31023* | Functions defined by founded recursion are identical up to relation, domain, and characteristic function. General version of frr3. (Contributed by Scott Fenton, 10-Feb-2011.) (Revised by Mario Carneiro, 26-Jun-2015.) |
⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝐹 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝐹‘𝑦) = (𝑦𝐻(𝐹 ↾ Pred(𝑅, 𝐴, 𝑦)))) ∧ (𝐺 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝐺‘𝑦) = (𝑦𝐻(𝐺 ↾ Pred(𝑅, 𝐴, 𝑦))))) → 𝐹 = 𝐺) | ||
Theorem | frrlem1 31024* | Lemma for founded recursion. The final item we are interested in is the union of acceptable functions 𝐵. This lemma just changes bound variables for later use. (Contributed by Paul Chapman, 21-Apr-2012.) |
⊢ 𝐵 = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦)))))} ⇒ ⊢ 𝐵 = {𝑔 ∣ ∃𝑧(𝑔 Fn 𝑧 ∧ (𝑧 ⊆ 𝐴 ∧ ∀𝑤 ∈ 𝑧 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑧 ∧ ∀𝑤 ∈ 𝑧 (𝑔‘𝑤) = (𝑤𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑤)))))} | ||
Theorem | frrlem2 31025* | Lemma for founded recursion. An acceptable function is a function. (Contributed by Paul Chapman, 21-Apr-2012.) |
⊢ 𝐵 = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦)))))} ⇒ ⊢ (𝑔 ∈ 𝐵 → Fun 𝑔) | ||
Theorem | frrlem3 31026* | Lemma for founded recursion. An acceptable function's domain is a subset of 𝐴. (Contributed by Paul Chapman, 21-Apr-2012.) |
⊢ 𝐵 = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦)))))} ⇒ ⊢ (𝑔 ∈ 𝐵 → dom 𝑔 ⊆ 𝐴) | ||
Theorem | frrlem4 31027* | Lemma for founded recursion. Properties of the restriction of an acceptable function to the domain of another acceptable function. (Contributed by Paul Chapman, 21-Apr-2012.) |
⊢ 𝐵 = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦)))))} ⇒ ⊢ ((𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵) → ((𝑔 ↾ (dom 𝑔 ∩ dom ℎ)) Fn (dom 𝑔 ∩ dom ℎ) ∧ ∀𝑎 ∈ (dom 𝑔 ∩ dom ℎ)((𝑔 ↾ (dom 𝑔 ∩ dom ℎ))‘𝑎) = (𝑎𝐺((𝑔 ↾ (dom 𝑔 ∩ dom ℎ)) ↾ Pred(𝑅, (dom 𝑔 ∩ dom ℎ), 𝑎))))) | ||
Theorem | frrlem5 31028* | Lemma for founded recursion. The values of two acceptable functions agree within their domains. (Contributed by Paul Chapman, 21-Apr-2012.) (Revised by Mario Carneiro, 26-Jun-2015.) |
⊢ 𝑅 Fr 𝐴 & ⊢ 𝑅 Se 𝐴 & ⊢ 𝐵 = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦)))))} ⇒ ⊢ ((𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵) → ((𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣) → 𝑢 = 𝑣)) | ||
Theorem | frrlem5b 31029* | Lemma for founded recursion. The union of a subclass of 𝐵 is a relationship. (Contributed by Paul Chapman, 29-Apr-2012.) |
⊢ 𝑅 Fr 𝐴 & ⊢ 𝑅 Se 𝐴 & ⊢ 𝐵 = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦)))))} ⇒ ⊢ (𝐶 ⊆ 𝐵 → Rel ∪ 𝐶) | ||
Theorem | frrlem5c 31030* | Lemma for founded recursion. The union of a subclass of 𝐵 is a function. (Contributed by Paul Chapman, 29-Apr-2012.) |
⊢ 𝑅 Fr 𝐴 & ⊢ 𝑅 Se 𝐴 & ⊢ 𝐵 = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦)))))} ⇒ ⊢ (𝐶 ⊆ 𝐵 → Fun ∪ 𝐶) | ||
Theorem | frrlem5d 31031* | Lemma for founded recursion. The domain of the union of a subset of 𝐵 is a subset of 𝐴. (Contributed by Paul Chapman, 29-Apr-2012.) |
⊢ 𝑅 Fr 𝐴 & ⊢ 𝑅 Se 𝐴 & ⊢ 𝐵 = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦)))))} ⇒ ⊢ (𝐶 ⊆ 𝐵 → dom ∪ 𝐶 ⊆ 𝐴) | ||
Theorem | frrlem5e 31032* | Lemma for founded recursion. The domain of the union of a subset of 𝐵 is closed under predecessors. (Contributed by Paul Chapman, 1-May-2012.) |
⊢ 𝑅 Fr 𝐴 & ⊢ 𝑅 Se 𝐴 & ⊢ 𝐵 = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦)))))} ⇒ ⊢ (𝐶 ⊆ 𝐵 → (𝑋 ∈ dom ∪ 𝐶 → Pred(𝑅, 𝐴, 𝑋) ⊆ dom ∪ 𝐶)) | ||
Theorem | frrlem6 31033* | Lemma for founded recursion. The union of all acceptable functions is a relationship. (Contributed by Paul Chapman, 21-Apr-2012.) |
⊢ 𝐵 = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦)))))} & ⊢ 𝐹 = ∪ 𝐵 ⇒ ⊢ Rel 𝐹 | ||
Theorem | frrlem7 31034* | Lemma for founded recursion. The domain of 𝐹 is a subclass of 𝐴. (Contributed by Paul Chapman, 21-Apr-2012.) |
⊢ 𝐵 = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦)))))} & ⊢ 𝐹 = ∪ 𝐵 ⇒ ⊢ dom 𝐹 ⊆ 𝐴 | ||
Theorem | frrlem10 31035* | Lemma for founded recursion. The union of all acceptable functions is a function. (Contributed by Paul Chapman, 21-Apr-2012.) |
⊢ 𝑅 Fr 𝐴 & ⊢ 𝑅 Se 𝐴 & ⊢ 𝐵 = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦)))))} & ⊢ 𝐹 = ∪ 𝐵 ⇒ ⊢ Fun 𝐹 | ||
Theorem | frrlem11 31036* | Lemma for founded recursion. Here, we calculate the value of 𝐹 (the union of all acceptable functions). (Contributed by Paul Chapman, 21-Apr-2012.) |
⊢ 𝑅 Fr 𝐴 & ⊢ 𝑅 Se 𝐴 & ⊢ 𝐵 = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦)))))} & ⊢ 𝐹 = ∪ 𝐵 ⇒ ⊢ (𝑦 ∈ dom 𝐹 → (𝐹‘𝑦) = (𝑦𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑦)))) | ||
Syntax | csur 31037 | Declare the class of all surreal numbers (see df-no 31040). |
class No | ||
Syntax | cslt 31038 | Declare the less than relationship over surreal numbers (see df-slt 31041). |
class <s | ||
Syntax | cbday 31039 | Declare the birthday function for surreal numbers (see df-bday 31042). |
class bday | ||
Definition | df-no 31040* |
Define the class of surreal numbers. The surreal numbers are a proper
class of numbers developed by John H. Conway and introduced by Donald
Knuth in 1975. They form a proper class into which all ordered fields
can be embedded. The approach we take to defining them was first
introduced by Hary Goshnor, and is based on the conception of a
"sign
expansion" of a surreal number. We define the surreals as
ordinal-indexed sequences of 1𝑜 and 2𝑜, analagous to Goshnor's
( − ) and ( + ).
After introducing this definition, we will abstract away from it using axioms that Norman Alling developed in "Foundations of Analysis over Surreal Number Fields." This is done in an effort to be agnostic towards the exact implementation of surreals. (Contributed by Scott Fenton, 9-Jun-2011.) |
⊢ No = {𝑓 ∣ ∃𝑎 ∈ On 𝑓:𝑎⟶{1𝑜, 2𝑜}} | ||
Definition | df-slt 31041* | Next, we introduce surreal less-than, a comparison relationship over the surreals by lexicographically ordering them. (Contributed by Scott Fenton, 9-Jun-2011.) |
⊢ <s = {〈𝑓, 𝑔〉 ∣ ((𝑓 ∈ No ∧ 𝑔 ∈ No ) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥){〈1𝑜, ∅〉, 〈1𝑜, 2𝑜〉, 〈∅, 2𝑜〉} (𝑔‘𝑥)))} | ||
Definition | df-bday 31042 | Finally, we introduce the birthday function. This function maps each surreal to an ordinal. In our implementation, this is the domain of the sign function. The important properties of this function are established later. (Contributed by Scott Fenton, 11-Jun-2011.) |
⊢ bday = (𝑥 ∈ No ↦ dom 𝑥) | ||
Theorem | elno 31043* | Membership in the surreals. (Shortened proof on 2012-Apr-14, SF). (Contributed by Scott Fenton, 11-Jun-2011.) |
⊢ (𝐴 ∈ No ↔ ∃𝑥 ∈ On 𝐴:𝑥⟶{1𝑜, 2𝑜}) | ||
Theorem | sltval 31044* | The value of the surreal less than relationship. (Contributed by Scott Fenton, 14-Jun-2011.) |
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴 <s 𝐵 ↔ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) ∧ (𝐴‘𝑥){〈1𝑜, ∅〉, 〈1𝑜, 2𝑜〉, 〈∅, 2𝑜〉} (𝐵‘𝑥)))) | ||
Theorem | bdayval 31045 | The value of the birthday function within the surreals. (Contributed by Scott Fenton, 14-Jun-2011.) |
⊢ (𝐴 ∈ No → ( bday ‘𝐴) = dom 𝐴) | ||
Theorem | nofun 31046 | A surreal is a function. (Contributed by Scott Fenton, 16-Jun-2011.) |
⊢ (𝐴 ∈ No → Fun 𝐴) | ||
Theorem | nodmon 31047 | The domain of a surreal is an ordinal. (Contributed by Scott Fenton, 16-Jun-2011.) |
⊢ (𝐴 ∈ No → dom 𝐴 ∈ On) | ||
Theorem | norn 31048 | The range of a surreal is a subset of the surreal signs. (Contributed by Scott Fenton, 16-Jun-2011.) |
⊢ (𝐴 ∈ No → ran 𝐴 ⊆ {1𝑜, 2𝑜}) | ||
Theorem | nofnbday 31049 | A surreal is a function over its birthday. (Contributed by Scott Fenton, 16-Jun-2011.) |
⊢ (𝐴 ∈ No → 𝐴 Fn ( bday ‘𝐴)) | ||
Theorem | nodmord 31050 | The domain of a surreal has the ordinal property. (Contributed by Scott Fenton, 16-Jun-2011.) |
⊢ (𝐴 ∈ No → Ord dom 𝐴) | ||
Theorem | elno2 31051 | An alternative condition for membership in No . (Contributed by Scott Fenton, 21-Mar-2012.) |
⊢ (𝐴 ∈ No ↔ (Fun 𝐴 ∧ dom 𝐴 ∈ On ∧ ran 𝐴 ⊆ {1𝑜, 2𝑜})) | ||
Theorem | elno3 31052 | Another condition for membership in No . (Contributed by Scott Fenton, 14-Apr-2012.) |
⊢ (𝐴 ∈ No ↔ (𝐴:dom 𝐴⟶{1𝑜, 2𝑜} ∧ dom 𝐴 ∈ On)) | ||
Theorem | sltval2 31053* | Alternate expression for surreal less than. Two surreals obey surreal less than iff they obey the sign ordering at the first place they differ. (Contributed by Scott Fenton, 17-Jun-2011.) |
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴 <s 𝐵 ↔ (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}){〈1𝑜, ∅〉, 〈1𝑜, 2𝑜〉, 〈∅, 2𝑜〉} (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}))) | ||
Theorem | nofv 31054 | The function value of a surreal is either a sign or the empty set. (Contributed by Scott Fenton, 22-Jun-2011.) |
⊢ (𝐴 ∈ No → ((𝐴‘𝑋) = ∅ ∨ (𝐴‘𝑋) = 1𝑜 ∨ (𝐴‘𝑋) = 2𝑜)) | ||
Theorem | nosgnn0 31055 | ∅ is not a surreal sign. (Contributed by Scott Fenton, 16-Jun-2011.) |
⊢ ¬ ∅ ∈ {1𝑜, 2𝑜} | ||
Theorem | nosgnn0i 31056 | If 𝑋 is a surreal sign, then it is not null. (Contributed by Scott Fenton, 3-Aug-2011.) |
⊢ 𝑋 ∈ {1𝑜, 2𝑜} ⇒ ⊢ ∅ ≠ 𝑋 | ||
Theorem | noreson 31057 | The restriction of a surreal to an ordinal is still a surreal. (Contributed by Scott Fenton, 4-Sep-2011.) |
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ On) → (𝐴 ↾ 𝐵) ∈ No ) | ||
Theorem | sltsgn1 31058* | If 𝐴 <s 𝐵, then the sign of 𝐴 at the first place they differ is either undefined or 1𝑜. (Contributed by Scott Fenton, 4-Sep-2011.) |
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴 <s 𝐵 → ((𝐴‘∩ {𝑘 ∈ On ∣ (𝐴‘𝑘) ≠ (𝐵‘𝑘)}) = ∅ ∨ (𝐴‘∩ {𝑘 ∈ On ∣ (𝐴‘𝑘) ≠ (𝐵‘𝑘)}) = 1𝑜))) | ||
Theorem | sltsgn2 31059* | If 𝐴 <s 𝐵, then the sign of 𝐵 at the first place they differ is either undefined or 2𝑜. (Contributed by Scott Fenton, 4-Sep-2011.) |
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴 <s 𝐵 → ((𝐵‘∩ {𝑘 ∈ On ∣ (𝐴‘𝑘) ≠ (𝐵‘𝑘)}) = ∅ ∨ (𝐵‘∩ {𝑘 ∈ On ∣ (𝐴‘𝑘) ≠ (𝐵‘𝑘)}) = 2𝑜))) | ||
Theorem | sltintdifex 31060* | If 𝐴 <s 𝐵, then the intersection of all the ordinals that have differing signs in 𝐴 and 𝐵 exists. (Contributed by Scott Fenton, 22-Feb-2012.) |
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴 <s 𝐵 → ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ V)) | ||
Theorem | sltres 31061 | If the restrictions of two surreals to a given ordinal obey surreal less than, then so do the two surreals themselves. (Contributed by Scott Fenton, 4-Sep-2011.) |
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) → ((𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋) → 𝐴 <s 𝐵)) | ||
Theorem | noxpsgn 31062 | The Cartesian product of an ordinal and the singleton of a sign is a surreal. (Contributed by Scott Fenton, 21-Jun-2011.) |
⊢ 𝑋 ∈ {1𝑜, 2𝑜} ⇒ ⊢ (𝐴 ∈ On → (𝐴 × {𝑋}) ∈ No ) | ||
Theorem | noxp1o 31063 | The Cartesian product of an ordinal and {1𝑜} is a surreal. (Contributed by Scott Fenton, 12-Jun-2011.) |
⊢ (𝐴 ∈ On → (𝐴 × {1𝑜}) ∈ No ) | ||
Theorem | noxp2o 31064 | The Cartesian product of an ordinal and {2𝑜} is a surreal. (Contributed by Scott Fenton, 12-Jun-2011.) |
⊢ (𝐴 ∈ On → (𝐴 × {2𝑜}) ∈ No ) | ||
Theorem | noseponlem 31065* | Lemma for nosepon 31066. Consider a case of proper subset domain. (Contributed by Scott Fenton, 21-Sep-2020.) |
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ dom 𝐴 ∈ dom 𝐵) → ¬ ∀𝑥 ∈ On (𝐴‘𝑥) = (𝐵‘𝑥)) | ||
Theorem | nosepon 31066* | Given two unequal surreals, the minimal ordinal at which they differ is an ordinal. (Contributed by Scott Fenton, 21-Sep-2020.) |
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 ≠ 𝐵) → ∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)} ∈ On) | ||
Theorem | sltsolem1 31067 | Lemma for sltso 31068. The sign expansion relationship totally orders the surreal signs. (Contributed by Scott Fenton, 8-Jun-2011.) |
⊢ {〈1𝑜, ∅〉, 〈1𝑜, 2𝑜〉, 〈∅, 2𝑜〉} Or ({1𝑜, 2𝑜} ∪ {∅}) | ||
Theorem | sltso 31068 | Surreal less than totally orders the surreals. Alling's axiom (O). (Contributed by Scott Fenton, 9-Jun-2011.) |
⊢ <s Or No | ||
Theorem | sltirr 31069 | Surreal less than is irreflexive. (Contributed by Scott Fenton, 16-Jun-2011.) |
⊢ (𝐴 ∈ No → ¬ 𝐴 <s 𝐴) | ||
Theorem | slttr 31070 | Surreal less than is transitive. (Contributed by Scott Fenton, 16-Jun-2011.) |
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → ((𝐴 <s 𝐵 ∧ 𝐵 <s 𝐶) → 𝐴 <s 𝐶)) | ||
Theorem | sltasym 31071 | Surreal less than is asymmetric. (Contributed by Scott Fenton, 16-Jun-2011.) |
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴 <s 𝐵 → ¬ 𝐵 <s 𝐴)) | ||
Theorem | slttri 31072 | Surreal less than obeys trichotomy. (Contributed by Scott Fenton, 16-Jun-2011.) |
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴 <s 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 <s 𝐴)) | ||
Theorem | slttrieq2 31073 | Trichotomy law for surreal less than. (Contributed by Scott Fenton, 22-Apr-2012.) |
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴 = 𝐵 ↔ (¬ 𝐴 <s 𝐵 ∧ ¬ 𝐵 <s 𝐴))) | ||
Theorem | bdayfo 31074 | The birthday function maps the surreals onto the ordinals. Alling's axiom (B). (Shortened proof on 2012-Apr-14, SF). (Contributed by Scott Fenton, 11-Jun-2011.) |
⊢ bday : No –onto→On | ||
Theorem | bdayfun 31075 | The birthday function is a function. (Contributed by Scott Fenton, 14-Jun-2011.) |
⊢ Fun bday | ||
Theorem | bdayrn 31076 | The birthday function's range is On. (Contributed by Scott Fenton, 14-Jun-2011.) |
⊢ ran bday = On | ||
Theorem | bdaydm 31077 | The birthday function's domain is No . (Contributed by Scott Fenton, 14-Jun-2011.) |
⊢ dom bday = No | ||
Theorem | bdayfn 31078 | The birthday function is a function over No . (Contributed by Scott Fenton, 30-Jun-2011.) |
⊢ bday Fn No | ||
Theorem | bdayelon 31079 | The value of the birthday function is always an ordinal. (Contributed by Scott Fenton, 14-Jun-2011.) |
⊢ ( bday ‘𝐴) ∈ On | ||
Theorem | noprc 31080 | The surreal numbers are a proper class. (Contributed by Scott Fenton, 16-Jun-2011.) |
⊢ ¬ No ∈ V | ||
Theorem | fvnobday 31081 | The value of a surreal at its birthday is ∅. (Contributed by Scott Fenton, 14-Jun-2011.) (Proof shortened by SF, 14-Apr-2012.) |
⊢ (𝐴 ∈ No → (𝐴‘( bday ‘𝐴)) = ∅) | ||
Theorem | nodenselem3 31082* | Lemma for nodense 31088. If one surreal is older than another, then there is an ordinal at which they are not equal. (Contributed by Scott Fenton, 16-Jun-2011.) |
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (( bday ‘𝐴) ∈ ( bday ‘𝐵) → ∃𝑎 ∈ On (𝐴‘𝑎) ≠ (𝐵‘𝑎))) | ||
Theorem | nodenselem4 31083* | Lemma for nodense 31088. Show that a particular abstraction is an ordinal. (Contributed by Scott Fenton, 16-Jun-2011.) |
⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝐴 <s 𝐵) → ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ On) | ||
Theorem | nodenselem5 31084* | Lemma for nodense 31088. If the birthdays of two distinct surreals are equal, then the ordinal from nodenselem4 31083 is an element of that birthday. (Contributed by Scott Fenton, 16-Jun-2011.) |
⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ (( bday ‘𝐴) = ( bday ‘𝐵) ∧ 𝐴 <s 𝐵)) → ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ ( bday ‘𝐴)) | ||
Theorem | nodenselem6 31085* | The restriction of a surreal to the abstraction from nodenselem4 31083 is still a surreal. (Contributed by Scott Fenton, 16-Jun-2011.) |
⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ (( bday ‘𝐴) = ( bday ‘𝐵) ∧ 𝐴 <s 𝐵)) → (𝐴 ↾ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) ∈ No ) | ||
Theorem | nodenselem7 31086* | Lemma for nodense 31088. 𝐴 and 𝐵 are equal at all elements of the abstraction. (Contributed by Scott Fenton, 17-Jun-2011.) |
⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ (( bday ‘𝐴) = ( bday ‘𝐵) ∧ 𝐴 <s 𝐵)) → (𝐶 ∈ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} → (𝐴‘𝐶) = (𝐵‘𝐶))) | ||
Theorem | nodenselem8 31087* | Lemma for nodense 31088. Give a condition for surreal less than when two surreals have the same birthday. (Contributed by Scott Fenton, 19-Jun-2011.) |
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ ( bday ‘𝐴) = ( bday ‘𝐵)) → (𝐴 <s 𝐵 ↔ ((𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = 1𝑜 ∧ (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = 2𝑜))) | ||
Theorem | nodense 31088* | Given two distinct surreals with the same birthday, there is an older surreal lying between the two of them. Alling's axiom (SD). (Contributed by Scott Fenton, 16-Jun-2011.) |
⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ (( bday ‘𝐴) = ( bday ‘𝐵) ∧ 𝐴 <s 𝐵)) → ∃𝑥 ∈ No (( bday ‘𝑥) ∈ ( bday ‘𝐴) ∧ 𝐴 <s 𝑥 ∧ 𝑥 <s 𝐵)) | ||
Theorem | nocvxminlem 31089* | Lemma for nocvxmin 31090. Given two birthday-minimal elements of a convex class of surreals, they are not comparable. (Contributed by Scott Fenton, 30-Jun-2011.) |
⊢ ((𝐴 ⊆ No ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ No ((𝑥 <s 𝑧 ∧ 𝑧 <s 𝑦) → 𝑧 ∈ 𝐴)) → (((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) ∧ (( bday ‘𝑋) = ∩ ( bday “ 𝐴) ∧ ( bday ‘𝑌) = ∩ ( bday “ 𝐴))) → ¬ 𝑋 <s 𝑌)) | ||
Theorem | nocvxmin 31090* | Given a nonempty convex class of surreals, there is a unique birthday-minimal element of that class. (Contributed by Scott Fenton, 30-Jun-2011.) |
⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ⊆ No ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ No ((𝑥 <s 𝑧 ∧ 𝑧 <s 𝑦) → 𝑧 ∈ 𝐴)) → ∃!𝑤 ∈ 𝐴 ( bday ‘𝑤) = ∩ ( bday “ 𝐴)) | ||
Theorem | nobndlem1 31091 | Lemma for nobndup 31099 and nobnddown 31100. The successor of the union of the image of the birthday function under a set is an ordinal. (Contributed by Scott Fenton, 20-Aug-2011.) |
⊢ (𝐴 ∈ 𝑉 → suc ∪ ( bday “ 𝐴) ∈ On) | ||
Theorem | nobndlem2 31092* | Lemma for nobndup 31099 and nobnddown 31100. Show a particular abstraction is an ordinal. (Contributed by Scott Fenton, 17-Aug-2011.) |
⊢ 𝑋 ∈ {1𝑜, 2𝑜} & ⊢ 𝐶 = ∩ {𝑎 ∈ On ∣ ∀𝑛 ∈ 𝐹 ∃𝑏 ∈ 𝑎 (𝑛‘𝑏) ≠ 𝑋} ⇒ ⊢ ((𝐹 ⊆ No ∧ 𝐹 ∈ 𝐴) → 𝐶 ∈ On) | ||
Theorem | nobndlem3 31093* | Lemma for nobndup 31099 and nobnddown 31100. Calculate the birthday of (𝐶 × {𝑋}). (Contributed by Scott Fenton, 17-Aug-2011.) |
⊢ 𝑋 ∈ {1𝑜, 2𝑜} & ⊢ 𝐶 = ∩ {𝑎 ∈ On ∣ ∀𝑛 ∈ 𝐹 ∃𝑏 ∈ 𝑎 (𝑛‘𝑏) ≠ 𝑋} ⇒ ⊢ ((𝐹 ⊆ No ∧ 𝐹 ∈ 𝐴) → ( bday ‘(𝐶 × {𝑋})) = 𝐶) | ||
Theorem | nobndlem4 31094* | Lemma for nobndup 31099 and nobnddown 31100. The infimum of the class of all ordinals such that 𝐴 is not 𝑋 is an ordinal. (Contributed by Scott Fenton, 17-Aug-2011.) |
⊢ 𝑋 ∈ {1𝑜, 2𝑜} ⇒ ⊢ (𝐴 ∈ No → ∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ 𝑋} ∈ On) | ||
Theorem | nobndlem5 31095* | Lemma for nobndup 31099 and nobnddown 31100. There is always a minimal value of a surreal that is not a given sign. (Contributed by Scott Fenton, 3-Aug-2011.) |
⊢ 𝑋 ∈ {1𝑜, 2𝑜} ⇒ ⊢ (𝐴 ∈ No → (𝐴‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ 𝑋}) ≠ 𝑋) | ||
Theorem | nobndlem6 31096* | Lemma for nobndup 31099 and nobnddown 31100. Given an element 𝐴 of 𝐹, then the first position where it differs from 𝑋 is strictly less than 𝐶. (Contributed by Scott Fenton, 3-Aug-2011.) |
⊢ 𝑋 ∈ {1𝑜, 2𝑜} & ⊢ 𝐶 = ∩ {𝑎 ∈ On ∣ ∀𝑛 ∈ 𝐹 ∃𝑏 ∈ 𝑎 (𝑛‘𝑏) ≠ 𝑋} ⇒ ⊢ ((𝐹 ⊆ No ∧ 𝐴 ∈ 𝐹) → ∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ 𝑋} ∈ 𝐶) | ||
Theorem | nobndlem7 31097* | Lemma for nobndup 31099 and nobnddown 31100. Calculate the value of (𝐶 × {𝑋}) at the minimal ordinal whose value is different from 𝑋. (Contributed by Scott Fenton, 3-Aug-2011.) |
⊢ 𝑋 ∈ {1𝑜, 2𝑜} & ⊢ 𝐶 = ∩ {𝑎 ∈ On ∣ ∀𝑛 ∈ 𝐹 ∃𝑏 ∈ 𝑎 (𝑛‘𝑏) ≠ 𝑋} ⇒ ⊢ ((𝐹 ⊆ No ∧ 𝐴 ∈ 𝐹) → ((𝐶 × {𝑋})‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ 𝑋}) = 𝑋) | ||
Theorem | nobndlem8 31098* | Lemma for nobndup 31099 and nobnddown 31100. Bound the birthday of (𝐶 × {𝑆}) above. (Contributed by Scott Fenton, 10-Apr-2017.) |
⊢ 𝑆 ∈ {1𝑜, 2𝑜} & ⊢ 𝐶 = ∩ {𝑎 ∈ On ∣ ∀𝑛 ∈ 𝐹 ∃𝑏 ∈ 𝑎 (𝑛‘𝑏) ≠ 𝑆} ⇒ ⊢ ((𝐹 ⊆ No ∧ 𝐹 ∈ 𝐴) → ( bday ‘(𝐶 × {𝑆})) ⊆ suc ∪ ( bday “ 𝐹)) | ||
Theorem | nobndup 31099* | Any set of surreals is bounded above by a surreal with a birthday no greater than the successor of their maximum birthday. (Contributed by Scott Fenton, 10-Apr-2017.) |
⊢ ((𝐴 ⊆ No ∧ 𝐴 ∈ 𝑉) → ∃𝑥 ∈ No (∀𝑦 ∈ 𝐴 𝑦 <s 𝑥 ∧ ( bday ‘𝑥) ⊆ suc ∪ ( bday “ 𝐴))) | ||
Theorem | nobnddown 31100* | Any set of surreals is bounded below by a surreal with a birthday no greater than the successor of their maximum birthday. (Contributed by Scott Fenton, 10-Apr-2017.) |
⊢ ((𝐴 ⊆ No ∧ 𝐴 ∈ 𝑉) → ∃𝑥 ∈ No (∀𝑦 ∈ 𝐴 𝑥 <s 𝑦 ∧ ( bday ‘𝑥) ⊆ suc ∪ ( bday “ 𝐴))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |