Theorem sssslt2

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

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

Proof

Step	Hyp	Ref	Expression
1		ssltex1	⊢ ( 𝐴 <<s 𝐵 → 𝐴 ∈ V )
2	1	adantr	⊢ ( ( 𝐴 <<s 𝐵 ∧ 𝐶 ⊆ 𝐵 ) → 𝐴 ∈ V )
3		ssltex2	⊢ ( 𝐴 <<s 𝐵 → 𝐵 ∈ V )
4	3	adantr	⊢ ( ( 𝐴 <<s 𝐵 ∧ 𝐶 ⊆ 𝐵 ) → 𝐵 ∈ V )
5		simpr	⊢ ( ( 𝐴 <<s 𝐵 ∧ 𝐶 ⊆ 𝐵 ) → 𝐶 ⊆ 𝐵 )
6	4 5	ssexd	⊢ ( ( 𝐴 <<s 𝐵 ∧ 𝐶 ⊆ 𝐵 ) → 𝐶 ∈ V )
7		ssltss1	⊢ ( 𝐴 <<s 𝐵 → 𝐴 ⊆ No )
8	7	adantr	⊢ ( ( 𝐴 <<s 𝐵 ∧ 𝐶 ⊆ 𝐵 ) → 𝐴 ⊆ No )
9		ssltss2	⊢ ( 𝐴 <<s 𝐵 → 𝐵 ⊆ No )
10	9	adantr	⊢ ( ( 𝐴 <<s 𝐵 ∧ 𝐶 ⊆ 𝐵 ) → 𝐵 ⊆ No )
11	5 10	sstrd	⊢ ( ( 𝐴 <<s 𝐵 ∧ 𝐶 ⊆ 𝐵 ) → 𝐶 ⊆ No )
12		ssltsep	⊢ ( 𝐴 <<s 𝐵 → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 <s 𝑦 )
13		ssralv	⊢ ( 𝐶 ⊆ 𝐵 → ( ∀ 𝑦 ∈ 𝐵 𝑥 <s 𝑦 → ∀ 𝑦 ∈ 𝐶 𝑥 <s 𝑦 ) )
14	13	ralimdv	⊢ ( 𝐶 ⊆ 𝐵 → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 <s 𝑦 → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐶 𝑥 <s 𝑦 ) )
15	12 14	mpan9	⊢ ( ( 𝐴 <<s 𝐵 ∧ 𝐶 ⊆ 𝐵 ) → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐶 𝑥 <s 𝑦 )
16	8 11 15	3jca	⊢ ( ( 𝐴 <<s 𝐵 ∧ 𝐶 ⊆ 𝐵 ) → ( 𝐴 ⊆ No ∧ 𝐶 ⊆ No ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐶 𝑥 <s 𝑦 ) )
17		brsslt	⊢ ( 𝐴 <<s 𝐶 ↔ ( ( 𝐴 ∈ V ∧ 𝐶 ∈ V ) ∧ ( 𝐴 ⊆ No ∧ 𝐶 ⊆ No ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐶 𝑥 <s 𝑦 ) ) )
18	2 6 16 17	syl21anbrc	⊢ ( ( 𝐴 <<s 𝐵 ∧ 𝐶 ⊆ 𝐵 ) → 𝐴 <<s 𝐶 )