Theorem sltsd

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

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

Proof

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