![]() |
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 3492 | . 2 ⊢ (𝜑 → 𝐴 ∈ V) |
3 | ssltd.2 | . . 3 ⊢ (𝜑 → 𝐵 ∈ 𝑊) | |
4 | 3 | elexd 3492 | . 2 ⊢ (𝜑 → 𝐵 ∈ V) |
5 | ssltd.3 | . . 3 ⊢ (𝜑 → 𝐴 ⊆ No ) | |
6 | ssltd.4 | . . 3 ⊢ (𝜑 → 𝐵 ⊆ No ) | |
7 | ssltd.5 | . . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝑥 <s 𝑦) | |
8 | 7 | 3expb 1118 | . . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → 𝑥 <s 𝑦) |
9 | 8 | ralrimivva 3197 | . . 3 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 <s 𝑦) |
10 | 5, 6, 9 | 3jca 1126 | . 2 ⊢ (𝜑 → (𝐴 ⊆ No ∧ 𝐵 ⊆ No ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 <s 𝑦)) |
11 | brsslt 27717 | . 2 ⊢ (𝐴 <<s 𝐵 ↔ ((𝐴 ∈ V ∧ 𝐵 ∈ V) ∧ (𝐴 ⊆ No ∧ 𝐵 ⊆ No ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 <s 𝑦))) | |
12 | 2, 4, 10, 11 | syl21anbrc 1342 | 1 ⊢ (𝜑 → 𝐴 <<s 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1085 ∈ wcel 2099 ∀wral 3058 Vcvv 3471 ⊆ wss 3947 class class class wbr 5148 No csur 27572 <s cslt 27573 <<s csslt 27712 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2699 ax-sep 5299 ax-nul 5306 ax-pr 5429 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 847 df-3an 1087 df-tru 1537 df-fal 1547 df-ex 1775 df-sb 2061 df-clab 2706 df-cleq 2720 df-clel 2806 df-ral 3059 df-rex 3068 df-rab 3430 df-v 3473 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-nul 4324 df-if 4530 df-sn 4630 df-pr 4632 df-op 4636 df-br 5149 df-opab 5211 df-xp 5684 df-sslt 27713 |
This theorem is referenced by: ssltsn 27724 nulsslt 27729 nulssgt 27730 sslttr 27739 ssltun1 27740 ssltun2 27741 ssltleft 27796 ssltright 27797 cofsslt 27837 coinitsslt 27838 cofcutr 27843 addsproplem2 27886 addsuniflem 27917 negsproplem2 27940 negsid 27952 negsunif 27966 mulsproplem9 28023 ssltmul1 28046 ssltmul2 28047 precsexlem10 28113 precsexlem11 28114 recut 28223 0reno 28224 |
Copyright terms: Public domain | W3C validator |