![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ssltex2 | Structured version Visualization version GIF version |
Description: The second argument of surreal set less-than exists. (Contributed by Scott Fenton, 8-Dec-2021.) |
Ref | Expression |
---|---|
ssltex2 | ⊢ (𝐴 <<s 𝐵 → 𝐵 ∈ V) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | brsslt 27077 | . 2 ⊢ (𝐴 <<s 𝐵 ↔ ((𝐴 ∈ V ∧ 𝐵 ∈ V) ∧ (𝐴 ⊆ No ∧ 𝐵 ⊆ No ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 <s 𝑦))) | |
2 | simplr 768 | . 2 ⊢ (((𝐴 ∈ V ∧ 𝐵 ∈ V) ∧ (𝐴 ⊆ No ∧ 𝐵 ⊆ No ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 <s 𝑦)) → 𝐵 ∈ V) | |
3 | 1, 2 | sylbi 216 | 1 ⊢ (𝐴 <<s 𝐵 → 𝐵 ∈ V) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 397 ∧ w3a 1088 ∈ wcel 2107 ∀wral 3063 Vcvv 3444 ⊆ wss 3909 class class class wbr 5104 No csur 26940 <s cslt 26941 <<s csslt 27072 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2709 ax-sep 5255 ax-nul 5262 ax-pr 5383 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-sb 2069 df-clab 2716 df-cleq 2730 df-clel 2816 df-ral 3064 df-rex 3073 df-rab 3407 df-v 3446 df-dif 3912 df-un 3914 df-in 3916 df-ss 3926 df-nul 4282 df-if 4486 df-sn 4586 df-pr 4588 df-op 4592 df-br 5105 df-opab 5167 df-xp 5638 df-sslt 27073 |
This theorem is referenced by: sssslt1 27086 sssslt2 27087 conway 27090 scutval 27091 sslttr 27098 ssltun1 27099 ssltun2 27100 etasslt 27104 etasslt2 27105 scutbdaybnd2lim 27108 slerec 27110 madecut 27163 cofsslt 27186 cofcut1 27188 cofcutr 27192 addsunif 34301 |
Copyright terms: Public domain | W3C validator |