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 𝑌 ) ) )