Theorem ssslts1

Description: Relation between surreal set less-than and subset. (Contributed by Scott Fenton, 9-Dec-2021)

	Ref	Expression
Assertion	ssslts1	⊢ ( ( 𝐴 <<s 𝐵 ∧ 𝐶 ⊆ 𝐴 ) → 𝐶 <<s 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		sltsex1	⊢ ( 𝐴 <<s 𝐵 → 𝐴 ∈ V )
2	1	adantr	⊢ ( ( 𝐴 <<s 𝐵 ∧ 𝐶 ⊆ 𝐴 ) → 𝐴 ∈ V )
3		simpr	⊢ ( ( 𝐴 <<s 𝐵 ∧ 𝐶 ⊆ 𝐴 ) → 𝐶 ⊆ 𝐴 )
4	2 3	ssexd	⊢ ( ( 𝐴 <<s 𝐵 ∧ 𝐶 ⊆ 𝐴 ) → 𝐶 ∈ V )
5		sltsex2	⊢ ( 𝐴 <<s 𝐵 → 𝐵 ∈ V )
6	5	adantr	⊢ ( ( 𝐴 <<s 𝐵 ∧ 𝐶 ⊆ 𝐴 ) → 𝐵 ∈ V )
7		sltsss1	⊢ ( 𝐴 <<s 𝐵 → 𝐴 ⊆ No )
8	7	adantr	⊢ ( ( 𝐴 <<s 𝐵 ∧ 𝐶 ⊆ 𝐴 ) → 𝐴 ⊆ No )
9	3 8	sstrd	⊢ ( ( 𝐴 <<s 𝐵 ∧ 𝐶 ⊆ 𝐴 ) → 𝐶 ⊆ No )
10		sltsss2	⊢ ( 𝐴 <<s 𝐵 → 𝐵 ⊆ No )
11	10	adantr	⊢ ( ( 𝐴 <<s 𝐵 ∧ 𝐶 ⊆ 𝐴 ) → 𝐵 ⊆ No )
12		sltssep	⊢ ( 𝐴 <<s 𝐵 → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 <s 𝑦 )
13		ssralv	⊢ ( 𝐶 ⊆ 𝐴 → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 <s 𝑦 → ∀ 𝑥 ∈ 𝐶 ∀ 𝑦 ∈ 𝐵 𝑥 <s 𝑦 ) )
14	12 13	mpan9	⊢ ( ( 𝐴 <<s 𝐵 ∧ 𝐶 ⊆ 𝐴 ) → ∀ 𝑥 ∈ 𝐶 ∀ 𝑦 ∈ 𝐵 𝑥 <s 𝑦 )
15	9 11 14	3jca	⊢ ( ( 𝐴 <<s 𝐵 ∧ 𝐶 ⊆ 𝐴 ) → ( 𝐶 ⊆ No ∧ 𝐵 ⊆ No ∧ ∀ 𝑥 ∈ 𝐶 ∀ 𝑦 ∈ 𝐵 𝑥 <s 𝑦 ) )
16		brslts	⊢ ( 𝐶 <<s 𝐵 ↔ ( ( 𝐶 ∈ V ∧ 𝐵 ∈ V ) ∧ ( 𝐶 ⊆ No ∧ 𝐵 ⊆ No ∧ ∀ 𝑥 ∈ 𝐶 ∀ 𝑦 ∈ 𝐵 𝑥 <s 𝑦 ) ) )
17	4 6 15 16	syl21anbrc	⊢ ( ( 𝐴 <<s 𝐵 ∧ 𝐶 ⊆ 𝐴 ) → 𝐶 <<s 𝐵 )