Metamath Proof Explorer


Theorem sltrec

Description: A comparison law for surreals considered as cuts of sets of surreals. (Contributed by Scott Fenton, 11-Dec-2021)

Ref Expression
Assertion sltrec ( ( ( 𝐴 <<s 𝐵𝐶 <<s 𝐷 ) ∧ ( 𝑋 = ( 𝐴 |s 𝐵 ) ∧ 𝑌 = ( 𝐶 |s 𝐷 ) ) ) → ( 𝑋 <s 𝑌 ↔ ( ∃ 𝑐𝐶 𝑋 ≤s 𝑐 ∨ ∃ 𝑏𝐵 𝑏 ≤s 𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 simplr ( ( ( 𝐴 <<s 𝐵𝐶 <<s 𝐷 ) ∧ ( 𝑋 = ( 𝐴 |s 𝐵 ) ∧ 𝑌 = ( 𝐶 |s 𝐷 ) ) ) → 𝐶 <<s 𝐷 )
2 simpll ( ( ( 𝐴 <<s 𝐵𝐶 <<s 𝐷 ) ∧ ( 𝑋 = ( 𝐴 |s 𝐵 ) ∧ 𝑌 = ( 𝐶 |s 𝐷 ) ) ) → 𝐴 <<s 𝐵 )
3 simprr ( ( ( 𝐴 <<s 𝐵𝐶 <<s 𝐷 ) ∧ ( 𝑋 = ( 𝐴 |s 𝐵 ) ∧ 𝑌 = ( 𝐶 |s 𝐷 ) ) ) → 𝑌 = ( 𝐶 |s 𝐷 ) )
4 simprl ( ( ( 𝐴 <<s 𝐵𝐶 <<s 𝐷 ) ∧ ( 𝑋 = ( 𝐴 |s 𝐵 ) ∧ 𝑌 = ( 𝐶 |s 𝐷 ) ) ) → 𝑋 = ( 𝐴 |s 𝐵 ) )
5 slerec ( ( ( 𝐶 <<s 𝐷𝐴 <<s 𝐵 ) ∧ ( 𝑌 = ( 𝐶 |s 𝐷 ) ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ) → ( 𝑌 ≤s 𝑋 ↔ ( ∀ 𝑏𝐵 𝑌 <s 𝑏 ∧ ∀ 𝑐𝐶 𝑐 <s 𝑋 ) ) )
6 1 2 3 4 5 syl22anc ( ( ( 𝐴 <<s 𝐵𝐶 <<s 𝐷 ) ∧ ( 𝑋 = ( 𝐴 |s 𝐵 ) ∧ 𝑌 = ( 𝐶 |s 𝐷 ) ) ) → ( 𝑌 ≤s 𝑋 ↔ ( ∀ 𝑏𝐵 𝑌 <s 𝑏 ∧ ∀ 𝑐𝐶 𝑐 <s 𝑋 ) ) )
7 ancom ( ( ∀ 𝑏𝐵 𝑌 <s 𝑏 ∧ ∀ 𝑐𝐶 𝑐 <s 𝑋 ) ↔ ( ∀ 𝑐𝐶 𝑐 <s 𝑋 ∧ ∀ 𝑏𝐵 𝑌 <s 𝑏 ) )
8 6 7 bitrdi ( ( ( 𝐴 <<s 𝐵𝐶 <<s 𝐷 ) ∧ ( 𝑋 = ( 𝐴 |s 𝐵 ) ∧ 𝑌 = ( 𝐶 |s 𝐷 ) ) ) → ( 𝑌 ≤s 𝑋 ↔ ( ∀ 𝑐𝐶 𝑐 <s 𝑋 ∧ ∀ 𝑏𝐵 𝑌 <s 𝑏 ) ) )
9 scutcut ( 𝐶 <<s 𝐷 → ( ( 𝐶 |s 𝐷 ) ∈ No 𝐶 <<s { ( 𝐶 |s 𝐷 ) } ∧ { ( 𝐶 |s 𝐷 ) } <<s 𝐷 ) )
10 9 simp1d ( 𝐶 <<s 𝐷 → ( 𝐶 |s 𝐷 ) ∈ No )
11 10 ad2antlr ( ( ( 𝐴 <<s 𝐵𝐶 <<s 𝐷 ) ∧ ( 𝑋 = ( 𝐴 |s 𝐵 ) ∧ 𝑌 = ( 𝐶 |s 𝐷 ) ) ) → ( 𝐶 |s 𝐷 ) ∈ No )
12 3 11 eqeltrd ( ( ( 𝐴 <<s 𝐵𝐶 <<s 𝐷 ) ∧ ( 𝑋 = ( 𝐴 |s 𝐵 ) ∧ 𝑌 = ( 𝐶 |s 𝐷 ) ) ) → 𝑌 No )
13 scutcut ( 𝐴 <<s 𝐵 → ( ( 𝐴 |s 𝐵 ) ∈ No 𝐴 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐵 ) )
14 13 simp1d ( 𝐴 <<s 𝐵 → ( 𝐴 |s 𝐵 ) ∈ No )
15 14 ad2antrr ( ( ( 𝐴 <<s 𝐵𝐶 <<s 𝐷 ) ∧ ( 𝑋 = ( 𝐴 |s 𝐵 ) ∧ 𝑌 = ( 𝐶 |s 𝐷 ) ) ) → ( 𝐴 |s 𝐵 ) ∈ No )
16 4 15 eqeltrd ( ( ( 𝐴 <<s 𝐵𝐶 <<s 𝐷 ) ∧ ( 𝑋 = ( 𝐴 |s 𝐵 ) ∧ 𝑌 = ( 𝐶 |s 𝐷 ) ) ) → 𝑋 No )
17 slenlt ( ( 𝑌 No 𝑋 No ) → ( 𝑌 ≤s 𝑋 ↔ ¬ 𝑋 <s 𝑌 ) )
18 12 16 17 syl2anc ( ( ( 𝐴 <<s 𝐵𝐶 <<s 𝐷 ) ∧ ( 𝑋 = ( 𝐴 |s 𝐵 ) ∧ 𝑌 = ( 𝐶 |s 𝐷 ) ) ) → ( 𝑌 ≤s 𝑋 ↔ ¬ 𝑋 <s 𝑌 ) )
19 ssltss1 ( 𝐶 <<s 𝐷𝐶 No )
20 19 ad2antlr ( ( ( 𝐴 <<s 𝐵𝐶 <<s 𝐷 ) ∧ ( 𝑋 = ( 𝐴 |s 𝐵 ) ∧ 𝑌 = ( 𝐶 |s 𝐷 ) ) ) → 𝐶 No )
21 20 sselda ( ( ( ( 𝐴 <<s 𝐵𝐶 <<s 𝐷 ) ∧ ( 𝑋 = ( 𝐴 |s 𝐵 ) ∧ 𝑌 = ( 𝐶 |s 𝐷 ) ) ) ∧ 𝑐𝐶 ) → 𝑐 No )
22 16 adantr ( ( ( ( 𝐴 <<s 𝐵𝐶 <<s 𝐷 ) ∧ ( 𝑋 = ( 𝐴 |s 𝐵 ) ∧ 𝑌 = ( 𝐶 |s 𝐷 ) ) ) ∧ 𝑐𝐶 ) → 𝑋 No )
23 sltnle ( ( 𝑐 No 𝑋 No ) → ( 𝑐 <s 𝑋 ↔ ¬ 𝑋 ≤s 𝑐 ) )
24 21 22 23 syl2anc ( ( ( ( 𝐴 <<s 𝐵𝐶 <<s 𝐷 ) ∧ ( 𝑋 = ( 𝐴 |s 𝐵 ) ∧ 𝑌 = ( 𝐶 |s 𝐷 ) ) ) ∧ 𝑐𝐶 ) → ( 𝑐 <s 𝑋 ↔ ¬ 𝑋 ≤s 𝑐 ) )
25 24 ralbidva ( ( ( 𝐴 <<s 𝐵𝐶 <<s 𝐷 ) ∧ ( 𝑋 = ( 𝐴 |s 𝐵 ) ∧ 𝑌 = ( 𝐶 |s 𝐷 ) ) ) → ( ∀ 𝑐𝐶 𝑐 <s 𝑋 ↔ ∀ 𝑐𝐶 ¬ 𝑋 ≤s 𝑐 ) )
26 12 adantr ( ( ( ( 𝐴 <<s 𝐵𝐶 <<s 𝐷 ) ∧ ( 𝑋 = ( 𝐴 |s 𝐵 ) ∧ 𝑌 = ( 𝐶 |s 𝐷 ) ) ) ∧ 𝑏𝐵 ) → 𝑌 No )
27 ssltss2 ( 𝐴 <<s 𝐵𝐵 No )
28 27 ad2antrr ( ( ( 𝐴 <<s 𝐵𝐶 <<s 𝐷 ) ∧ ( 𝑋 = ( 𝐴 |s 𝐵 ) ∧ 𝑌 = ( 𝐶 |s 𝐷 ) ) ) → 𝐵 No )
29 28 sselda ( ( ( ( 𝐴 <<s 𝐵𝐶 <<s 𝐷 ) ∧ ( 𝑋 = ( 𝐴 |s 𝐵 ) ∧ 𝑌 = ( 𝐶 |s 𝐷 ) ) ) ∧ 𝑏𝐵 ) → 𝑏 No )
30 sltnle ( ( 𝑌 No 𝑏 No ) → ( 𝑌 <s 𝑏 ↔ ¬ 𝑏 ≤s 𝑌 ) )
31 26 29 30 syl2anc ( ( ( ( 𝐴 <<s 𝐵𝐶 <<s 𝐷 ) ∧ ( 𝑋 = ( 𝐴 |s 𝐵 ) ∧ 𝑌 = ( 𝐶 |s 𝐷 ) ) ) ∧ 𝑏𝐵 ) → ( 𝑌 <s 𝑏 ↔ ¬ 𝑏 ≤s 𝑌 ) )
32 31 ralbidva ( ( ( 𝐴 <<s 𝐵𝐶 <<s 𝐷 ) ∧ ( 𝑋 = ( 𝐴 |s 𝐵 ) ∧ 𝑌 = ( 𝐶 |s 𝐷 ) ) ) → ( ∀ 𝑏𝐵 𝑌 <s 𝑏 ↔ ∀ 𝑏𝐵 ¬ 𝑏 ≤s 𝑌 ) )
33 25 32 anbi12d ( ( ( 𝐴 <<s 𝐵𝐶 <<s 𝐷 ) ∧ ( 𝑋 = ( 𝐴 |s 𝐵 ) ∧ 𝑌 = ( 𝐶 |s 𝐷 ) ) ) → ( ( ∀ 𝑐𝐶 𝑐 <s 𝑋 ∧ ∀ 𝑏𝐵 𝑌 <s 𝑏 ) ↔ ( ∀ 𝑐𝐶 ¬ 𝑋 ≤s 𝑐 ∧ ∀ 𝑏𝐵 ¬ 𝑏 ≤s 𝑌 ) ) )
34 ralnex ( ∀ 𝑐𝐶 ¬ 𝑋 ≤s 𝑐 ↔ ¬ ∃ 𝑐𝐶 𝑋 ≤s 𝑐 )
35 ralnex ( ∀ 𝑏𝐵 ¬ 𝑏 ≤s 𝑌 ↔ ¬ ∃ 𝑏𝐵 𝑏 ≤s 𝑌 )
36 34 35 anbi12i ( ( ∀ 𝑐𝐶 ¬ 𝑋 ≤s 𝑐 ∧ ∀ 𝑏𝐵 ¬ 𝑏 ≤s 𝑌 ) ↔ ( ¬ ∃ 𝑐𝐶 𝑋 ≤s 𝑐 ∧ ¬ ∃ 𝑏𝐵 𝑏 ≤s 𝑌 ) )
37 ioran ( ¬ ( ∃ 𝑐𝐶 𝑋 ≤s 𝑐 ∨ ∃ 𝑏𝐵 𝑏 ≤s 𝑌 ) ↔ ( ¬ ∃ 𝑐𝐶 𝑋 ≤s 𝑐 ∧ ¬ ∃ 𝑏𝐵 𝑏 ≤s 𝑌 ) )
38 36 37 bitr4i ( ( ∀ 𝑐𝐶 ¬ 𝑋 ≤s 𝑐 ∧ ∀ 𝑏𝐵 ¬ 𝑏 ≤s 𝑌 ) ↔ ¬ ( ∃ 𝑐𝐶 𝑋 ≤s 𝑐 ∨ ∃ 𝑏𝐵 𝑏 ≤s 𝑌 ) )
39 33 38 bitrdi ( ( ( 𝐴 <<s 𝐵𝐶 <<s 𝐷 ) ∧ ( 𝑋 = ( 𝐴 |s 𝐵 ) ∧ 𝑌 = ( 𝐶 |s 𝐷 ) ) ) → ( ( ∀ 𝑐𝐶 𝑐 <s 𝑋 ∧ ∀ 𝑏𝐵 𝑌 <s 𝑏 ) ↔ ¬ ( ∃ 𝑐𝐶 𝑋 ≤s 𝑐 ∨ ∃ 𝑏𝐵 𝑏 ≤s 𝑌 ) ) )
40 8 18 39 3bitr3d ( ( ( 𝐴 <<s 𝐵𝐶 <<s 𝐷 ) ∧ ( 𝑋 = ( 𝐴 |s 𝐵 ) ∧ 𝑌 = ( 𝐶 |s 𝐷 ) ) ) → ( ¬ 𝑋 <s 𝑌 ↔ ¬ ( ∃ 𝑐𝐶 𝑋 ≤s 𝑐 ∨ ∃ 𝑏𝐵 𝑏 ≤s 𝑌 ) ) )
41 40 con4bid ( ( ( 𝐴 <<s 𝐵𝐶 <<s 𝐷 ) ∧ ( 𝑋 = ( 𝐴 |s 𝐵 ) ∧ 𝑌 = ( 𝐶 |s 𝐷 ) ) ) → ( 𝑋 <s 𝑌 ↔ ( ∃ 𝑐𝐶 𝑋 ≤s 𝑐 ∨ ∃ 𝑏𝐵 𝑏 ≤s 𝑌 ) ) )