Theorem ssltd 27732

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

Hypotheses

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

Assertion

Ref	Expression
ssltd	⊢ (𝜑 → 𝐴 <<s 𝐵)

Distinct variable groups:   𝑥,𝐴,𝑦   𝑥,𝐵,𝑦   𝜑,𝑥,𝑦

Allowed substitution hints:   𝑉(𝑥,𝑦)   𝑊(𝑥,𝑦)

Proof of Theorem ssltd

Step	Hyp	Ref	Expression
1		ssltd.1	. . 3 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
2	1	elexd 3460	. 2 ⊢ (𝜑 → 𝐴 ∈ V)
3		ssltd.2	. . 3 ⊢ (𝜑 → 𝐵 ∈ 𝑊)
4	3	elexd 3460	. 2 ⊢ (𝜑 → 𝐵 ∈ V)
5		ssltd.3	. . 3 ⊢ (𝜑 → 𝐴 ⊆ No )
6		ssltd.4	. . 3 ⊢ (𝜑 → 𝐵 ⊆ No )
7		ssltd.5	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝑥 <s 𝑦)
8	7	3expb 1120	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → 𝑥 <s 𝑦)
9	8	ralrimivva 3175	. . 3 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 <s 𝑦)
10	5, 6, 9	3jca 1128	. 2 ⊢ (𝜑 → (𝐴 ⊆ No ∧ 𝐵 ⊆ No ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 <s 𝑦))
11		brsslt 27726	. 2 ⊢ (𝐴 <<s 𝐵 ↔ ((𝐴 ∈ V ∧ 𝐵 ∈ V) ∧ (𝐴 ⊆ No ∧ 𝐵 ⊆ No ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 <s 𝑦)))
12	2, 4, 10, 11	syl21anbrc 1345	1 ⊢ (𝜑 → 𝐴 <<s 𝐵)

Syntax hints:   → wi 4   ∧ w3a 1086   ∈ wcel 2111  ∀wral 3047  Vcvv 3436   ⊆ wss 3902   class class class wbr 5091   No csur 27579   <s cslt 27580   <<s csslt 27721

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-sep 5234  ax-nul 5244  ax-pr 5370

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4284  df-if 4476  df-sn 4577  df-pr 4579  df-op 4583  df-br 5092  df-opab 5154  df-xp 5622  df-sslt 27722

This theorem is referenced by:  nulsslt  27739  nulssgt  27740  sslttr  27749  ssltun1  27750  ssltun2  27751  eqscut3  27766  ssltleft  27816  ssltright  27817  cofsslt  27863  coinitsslt  27864  cofcutr  27869  addsproplem2  27914  addsuniflem  27945  negsproplem2  27972  negsid  27984  negsunif  27998  mulsproplem9  28064  ssltmul1  28087  ssltmul2  28088  precsexlem10  28155  precsexlem11  28156  onscutlt  28202  n0sfincut  28283  recut  28399  0reno  28400