ssltd - Metamath Proof Explorer

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

Theorem ssltd 27742

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 3484	. 2 ⊢ (𝜑 → 𝐴 ∈ V)
3		ssltd.2	. . 3 ⊢ (𝜑 → 𝐵 ∈ 𝑊)
4	3	elexd 3484	. 2 ⊢ (𝜑 → 𝐵 ∈ V)
5		ssltd.3	. . 3 ⊢ (𝜑 → 𝐴 ⊆ No )
6		ssltd.4	. . 3 ⊢ (𝜑 → 𝐵 ⊆ No )
7		ssltd.5	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝑥 <s 𝑦)
8	7	3expb 1117	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → 𝑥 <s 𝑦)
9	8	ralrimivva 3191	. . 3 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 <s 𝑦)
10	5, 6, 9	3jca 1125	. 2 ⊢ (𝜑 → (𝐴 ⊆ No ∧ 𝐵 ⊆ No ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 <s 𝑦))
11		brsslt 27736	. 2 ⊢ (𝐴 <<s 𝐵 ↔ ((𝐴 ∈ V ∧ 𝐵 ∈ V) ∧ (𝐴 ⊆ No ∧ 𝐵 ⊆ No ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 <s 𝑦)))
12	2, 4, 10, 11	syl21anbrc 1341	1 ⊢ (𝜑 → 𝐴 <<s 𝐵)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ w3a 1084 ∈ wcel 2098 ∀wral 3051 Vcvv 3463 ⊆ wss 3939 class class class wbr 5143 No csur 27591 <s cslt 27592 <<s csslt 27731

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2696 ax-sep 5294 ax-nul 5301 ax-pr 5423

This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-sb 2060 df-clab 2703 df-cleq 2717 df-clel 2802 df-ral 3052 df-rex 3061 df-rab 3420 df-v 3465 df-dif 3942 df-un 3944 df-ss 3956 df-nul 4319 df-if 4525 df-sn 4625 df-pr 4627 df-op 4631 df-br 5144 df-opab 5206 df-xp 5678 df-sslt 27732

This theorem is referenced by: ssltsn 27743 nulsslt 27748 nulssgt 27749 sslttr 27758 ssltun1 27759 ssltun2 27760 ssltleft 27815 ssltright 27816 cofsslt 27856 coinitsslt 27857 cofcutr 27862 addsproplem2 27905 addsuniflem 27936 negsproplem2 27959 negsid 27971 negsunif 27985 mulsproplem9 28046 ssltmul1 28069 ssltmul2 28070 precsexlem10 28136 precsexlem11 28137 recut 28268 0reno 28269

W3C validator

	
		OSZAR »