![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ssltd | Structured version Visualization version GIF version |
Description: Deduce surreal set less-than. (Contributed by Scott Fenton, 24-Sep-2024.) |
Ref | Expression |
---|---|
ssltd.1 | ⊢ (𝜑 → 𝐴 ∈ 𝑉) |
ssltd.2 | ⊢ (𝜑 → 𝐵 ∈ 𝑊) |
ssltd.3 | ⊢ (𝜑 → 𝐴 ⊆ No ) |
ssltd.4 | ⊢ (𝜑 → 𝐵 ⊆ No ) |
ssltd.5 | ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝑥 <s 𝑦) |
Ref | Expression |
---|---|
ssltd | ⊢ (𝜑 → 𝐴 <<s 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ssltd.1 | . . 3 ⊢ (𝜑 → 𝐴 ∈ 𝑉) | |
2 | 1 | elexd 3495 | . 2 ⊢ (𝜑 → 𝐴 ∈ V) |
3 | ssltd.2 | . . 3 ⊢ (𝜑 → 𝐵 ∈ 𝑊) | |
4 | 3 | elexd 3495 | . 2 ⊢ (𝜑 → 𝐵 ∈ V) |
5 | ssltd.3 | . . 3 ⊢ (𝜑 → 𝐴 ⊆ No ) | |
6 | ssltd.4 | . . 3 ⊢ (𝜑 → 𝐵 ⊆ No ) | |
7 | ssltd.5 | . . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝑥 <s 𝑦) | |
8 | 7 | 3expb 1121 | . . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → 𝑥 <s 𝑦) |
9 | 8 | ralrimivva 3201 | . . 3 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 <s 𝑦) |
10 | 5, 6, 9 | 3jca 1129 | . 2 ⊢ (𝜑 → (𝐴 ⊆ No ∧ 𝐵 ⊆ No ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 <s 𝑦)) |
11 | brsslt 27267 | . 2 ⊢ (𝐴 <<s 𝐵 ↔ ((𝐴 ∈ V ∧ 𝐵 ∈ V) ∧ (𝐴 ⊆ No ∧ 𝐵 ⊆ No ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 <s 𝑦))) | |
12 | 2, 4, 10, 11 | syl21anbrc 1345 | 1 ⊢ (𝜑 → 𝐴 <<s 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1088 ∈ wcel 2107 ∀wral 3062 Vcvv 3475 ⊆ wss 3947 class class class wbr 5147 No csur 27123 <s cslt 27124 <<s csslt 27262 |
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 2704 ax-sep 5298 ax-nul 5305 ax-pr 5426 |
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 2711 df-cleq 2725 df-clel 2811 df-ral 3063 df-rex 3072 df-rab 3434 df-v 3477 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-nul 4322 df-if 4528 df-sn 4628 df-pr 4630 df-op 4634 df-br 5148 df-opab 5210 df-xp 5681 df-sslt 27263 |
This theorem is referenced by: nulsslt 27278 nulssgt 27279 sslttr 27288 ssltun1 27289 ssltun2 27290 ssltleft 27345 ssltright 27346 cofsslt 27385 coinitsslt 27386 cofcutr 27391 addsproplem2 27434 addsuniflem 27464 negsproplem2 27483 negsid 27495 negsunif 27509 mulsproplem9 27560 ssltmul1 27582 ssltmul2 27583 precsexlem10 27642 precsexlem11 27643 |
Copyright terms: Public domain | W3C validator |