Theorem sltsd 27942

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 3478	. 2 ⊢ (𝜑 → 𝐴 ∈ V)
3		sltsd.2	. . 3 ⊢ (𝜑 → 𝐵 ∈ 𝑊)
4	3	elexd 3478	. 2 ⊢ (𝜑 → 𝐵 ∈ V)
5		sltsd.3	. . 3 ⊢ (𝜑 → 𝐴 ⊆ No )
6		sltsd.4	. . 3 ⊢ (𝜑 → 𝐵 ⊆ No )
7		sltsd.5	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝑥 <s 𝑦)
8	7	3expb 1138	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → 𝑥 <s 𝑦)
9	8	ralrimivva 3208	. . 3 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 <s 𝑦)
10	5, 6, 9	3jca 1146	. 2 ⊢ (𝜑 → (𝐴 ⊆ No ∧ 𝐵 ⊆ No ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 <s 𝑦))
11		brslts 27936	. 2 ⊢ (𝐴 <<s 𝐵 ↔ ((𝐴 ∈ V ∧ 𝐵 ∈ V) ∧ (𝐴 ⊆ No ∧ 𝐵 ⊆ No ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 <s 𝑦)))
12	2, 4, 10, 11	syl21anbrc 1363	1 ⊢ (𝜑 → 𝐴 <<s 𝐵)

Syntax hints:   → wi 4   ∧ w3a 1103   ∈ wcel 2143  ∀wral 3079  Vcvv 3455   ⊆ wss 3906   class class class wbr 5110   No csur 27785   <s clts 27786   <<s cslts 27931

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5258  ax-pr 5406

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-br 5111  df-opab 5175  df-xp 5669  df-slts 27932

This theorem is referenced by:  nulslts  27949  nulsgts  27950  sltstr  27961  sltsun1  27962  sltsun2  27963  eqcuts3  27978  sltsleft  28034  sltsright  28035  cofslts  28092  coinitslts  28093  cofcutr  28098  addsproplem2  28144  addsuniflem  28175  negsproplem2  28203  negsid  28215  negsunif  28229  mulsproplem9  28298  sltmuls1  28321  sltmuls2  28322  precsexlem10  28390  precsexlem11  28391  oncutlt  28438  n0fincut  28529  recut  28668  elreno2  28669