sltsd - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > sltsd		Structured version Visualization version GIF version

Theorem sltsd 27785

Description: Deduce surreal set less-than. (Contributed by Scott Fenton, 24-Sep-2024.)

**Hypotheses**
Ref	Expression
sltsd.1	⊢ (𝜑 → 𝐴 ∈ 𝑉)
sltsd.2	⊢ (𝜑 → 𝐵 ∈ 𝑊)
sltsd.3	⊢ (𝜑 → 𝐴 ⊆ No )
sltsd.4	⊢ (𝜑 → 𝐵 ⊆ No )
sltsd.5	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝑥 <s 𝑦)

**Assertion**
Ref	Expression
sltsd	⊢ (𝜑 → 𝐴 <<s 𝐵)

Distinct variable groups: 𝑥,𝐴,𝑦 𝑥,𝐵,𝑦 𝜑,𝑥,𝑦 Allowed substitution hints: 𝑉(𝑥,𝑦) 𝑊(𝑥,𝑦)

**Proof of Theorem sltsd**
Step	Hyp	Ref	Expression
1		sltsd.1	. . 3 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
2	1	elexd 3456	. 2 ⊢ (𝜑 → 𝐴 ∈ V)
3		sltsd.2	. . 3 ⊢ (𝜑 → 𝐵 ∈ 𝑊)
4	3	elexd 3456	. 2 ⊢ (𝜑 → 𝐵 ∈ V)
5		sltsd.3	. . 3 ⊢ (𝜑 → 𝐴 ⊆ No )
6		sltsd.4	. . 3 ⊢ (𝜑 → 𝐵 ⊆ No )
7		sltsd.5	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝑥 <s 𝑦)
8	7	3expb 1126	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → 𝑥 <s 𝑦)
9	8	ralrimivva 3183	. . 3 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 <s 𝑦)
10	5, 6, 9	3jca 1134	. 2 ⊢ (𝜑 → (𝐴 ⊆ No ∧ 𝐵 ⊆ No ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 <s 𝑦))
11		brslts 27779	. 2 ⊢ (𝐴 <<s 𝐵 ↔ ((𝐴 ∈ V ∧ 𝐵 ∈ V) ∧ (𝐴 ⊆ No ∧ 𝐵 ⊆ No ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 <s 𝑦)))
12	2, 4, 10, 11	syl21anbrc 1351	1 ⊢ (𝜑 → 𝐴 <<s 𝐵)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ w3a 1092 ∈ wcel 2119 ∀wral 3054 Vcvv 3432 ⊆ wss 3890 class class class wbr 5079 No csur 27628 <s clts 27629 <<s cslts 27774

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1974 ax-7 2015 ax-8 2121 ax-9 2129 ax-ext 2712 ax-sep 5225 ax-pr 5369

This theorem depends on definitions: df-bi 208 df-an 397 df-or 854 df-3an 1094 df-tru 1550 df-fal 1560 df-ex 1787 df-sb 2074 df-clab 2719 df-cleq 2732 df-clel 2815 df-ral 3055 df-rex 3065 df-rab 3393 df-v 3434 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-nul 4269 df-if 4462 df-sn 4563 df-pr 4565 df-op 4569 df-br 5080 df-opab 5142 df-xp 5631 df-slts 27775

This theorem is referenced by: nulslts 27792 nulsgts 27793 sltstr 27804 sltsun1 27805 sltsun2 27806 eqcuts3 27821 sltsleft 27877 sltsright 27878 cofslts 27935 coinitslts 27936 cofcutr 27941 addsproplem2 27987 addsuniflem 28018 negsproplem2 28046 negsid 28058 negsunif 28072 mulsproplem9 28141 sltmuls1 28164 sltmuls2 28165 precsexlem10 28233 precsexlem11 28234 oncutlt 28281 n0fincut 28372 recut 28511 elreno2 28512

W3C validator