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