Metamath Proof Explorer

Theorem sltstr

Description: Transitive law for surreal set less-than. (Contributed by Scott Fenton, 9-Dec-2021)

Ref Expression
Assertion sltstr ( ( 𝐴 <<s 𝐵 ∧ 𝐵 <<s 𝐶 ∧ 𝐵 ≠ ∅ ) → 𝐴 <<s 𝐶 )

Proof

Step Hyp Ref Expression
1 n0 ⊢ ( 𝐵 ≠ ∅ ↔ ∃ 𝑦 𝑦 ∈ 𝐵 )
2 sltsex1 ⊢ ( 𝐴 <<s 𝐵 → 𝐴 ∈ V )
3 2 3ad2ant2 ⊢ ( ( 𝑦 ∈ 𝐵 ∧ 𝐴 <<s 𝐵 ∧ 𝐵 <<s 𝐶 ) → 𝐴 ∈ V )
4 sltsex2 ⊢ ( 𝐵 <<s 𝐶 → 𝐶 ∈ V )
5 4 3ad2ant3 ⊢ ( ( 𝑦 ∈ 𝐵 ∧ 𝐴 <<s 𝐵 ∧ 𝐵 <<s 𝐶 ) → 𝐶 ∈ V )
6 sltsss1 ⊢ ( 𝐴 <<s 𝐵 → 𝐴 ⊆ No )
7 6 3ad2ant2 ⊢ ( ( 𝑦 ∈ 𝐵 ∧ 𝐴 <<s 𝐵 ∧ 𝐵 <<s 𝐶 ) → 𝐴 ⊆ No )
8 sltsss2 ⊢ ( 𝐵 <<s 𝐶 → 𝐶 ⊆ No )
9 8 3ad2ant3 ⊢ ( ( 𝑦 ∈ 𝐵 ∧ 𝐴 <<s 𝐵 ∧ 𝐵 <<s 𝐶 ) → 𝐶 ⊆ No )
10 7 3ad2ant1 ⊢ ( ( ( 𝑦 ∈ 𝐵 ∧ 𝐴 <<s 𝐵 ∧ 𝐵 <<s 𝐶 ) ∧ 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶 ) → 𝐴 ⊆ No )
11 simp2 ⊢ ( ( ( 𝑦 ∈ 𝐵 ∧ 𝐴 <<s 𝐵 ∧ 𝐵 <<s 𝐶 ) ∧ 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶 ) → 𝑥 ∈ 𝐴 )
12 10 11 sseldd ⊢ ( ( ( 𝑦 ∈ 𝐵 ∧ 𝐴 <<s 𝐵 ∧ 𝐵 <<s 𝐶 ) ∧ 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶 ) → 𝑥 ∈ No )
13 sltsss2 ⊢ ( 𝐴 <<s 𝐵 → 𝐵 ⊆ No )
14 13 3ad2ant2 ⊢ ( ( 𝑦 ∈ 𝐵 ∧ 𝐴 <<s 𝐵 ∧ 𝐵 <<s 𝐶 ) → 𝐵 ⊆ No )
15 14 3ad2ant1 ⊢ ( ( ( 𝑦 ∈ 𝐵 ∧ 𝐴 <<s 𝐵 ∧ 𝐵 <<s 𝐶 ) ∧ 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶 ) → 𝐵 ⊆ No )
16 simp11 ⊢ ( ( ( 𝑦 ∈ 𝐵 ∧ 𝐴 <<s 𝐵 ∧ 𝐵 <<s 𝐶 ) ∧ 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶 ) → 𝑦 ∈ 𝐵 )
17 15 16 sseldd ⊢ ( ( ( 𝑦 ∈ 𝐵 ∧ 𝐴 <<s 𝐵 ∧ 𝐵 <<s 𝐶 ) ∧ 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶 ) → 𝑦 ∈ No )
18 9 3ad2ant1 ⊢ ( ( ( 𝑦 ∈ 𝐵 ∧ 𝐴 <<s 𝐵 ∧ 𝐵 <<s 𝐶 ) ∧ 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶 ) → 𝐶 ⊆ No )
19 simp3 ⊢ ( ( ( 𝑦 ∈ 𝐵 ∧ 𝐴 <<s 𝐵 ∧ 𝐵 <<s 𝐶 ) ∧ 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶 ) → 𝑧 ∈ 𝐶 )
20 18 19 sseldd ⊢ ( ( ( 𝑦 ∈ 𝐵 ∧ 𝐴 <<s 𝐵 ∧ 𝐵 <<s 𝐶 ) ∧ 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶 ) → 𝑧 ∈ No )
21 simp12 ⊢ ( ( ( 𝑦 ∈ 𝐵 ∧ 𝐴 <<s 𝐵 ∧ 𝐵 <<s 𝐶 ) ∧ 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶 ) → 𝐴 <<s 𝐵 )
22 21 11 16 sltssepcd ⊢ ( ( ( 𝑦 ∈ 𝐵 ∧ 𝐴 <<s 𝐵 ∧ 𝐵 <<s 𝐶 ) ∧ 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶 ) → 𝑥 <s 𝑦 )
23 simp13 ⊢ ( ( ( 𝑦 ∈ 𝐵 ∧ 𝐴 <<s 𝐵 ∧ 𝐵 <<s 𝐶 ) ∧ 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶 ) → 𝐵 <<s 𝐶 )
24 23 16 19 sltssepcd ⊢ ( ( ( 𝑦 ∈ 𝐵 ∧ 𝐴 <<s 𝐵 ∧ 𝐵 <<s 𝐶 ) ∧ 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶 ) → 𝑦 <s 𝑧 )
25 12 17 20 22 24 ltstrd ⊢ ( ( ( 𝑦 ∈ 𝐵 ∧ 𝐴 <<s 𝐵 ∧ 𝐵 <<s 𝐶 ) ∧ 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶 ) → 𝑥 <s 𝑧 )
26 3 5 7 9 25 sltsd ⊢ ( ( 𝑦 ∈ 𝐵 ∧ 𝐴 <<s 𝐵 ∧ 𝐵 <<s 𝐶 ) → 𝐴 <<s 𝐶 )
27 26 3exp ⊢ ( 𝑦 ∈ 𝐵 → ( 𝐴 <<s 𝐵 → ( 𝐵 <<s 𝐶 → 𝐴 <<s 𝐶 ) ) )
28 27 exlimiv ⊢ ( ∃ 𝑦 𝑦 ∈ 𝐵 → ( 𝐴 <<s 𝐵 → ( 𝐵 <<s 𝐶 → 𝐴 <<s 𝐶 ) ) )
29 1 28 sylbi ⊢ ( 𝐵 ≠ ∅ → ( 𝐴 <<s 𝐵 → ( 𝐵 <<s 𝐶 → 𝐴 <<s 𝐶 ) ) )
30 29 3imp231 ⊢ ( ( 𝐴 <<s 𝐵 ∧ 𝐵 <<s 𝐶 ∧ 𝐵 ≠ ∅ ) → 𝐴 <<s 𝐶 )