Mathbox for Scott Fenton < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  noresle Structured version   Visualization version   GIF version

Theorem noresle 33208
 Description: Restriction law for surreals. Lemma 2.1.4 of [Lipparini] p. 3. (Contributed by Scott Fenton, 5-Dec-2021.)
Assertion
Ref Expression
noresle (((𝑈 No 𝑆 No ) ∧ (dom 𝑈𝐴 ∧ dom 𝑆𝐴 ∧ ∀𝑔𝐴 ¬ (𝑆 ↾ suc 𝑔) <s (𝑈 ↾ suc 𝑔))) → ¬ 𝑆 <s 𝑈)
Distinct variable groups:   𝑆,𝑔   𝑈,𝑔   𝐴,𝑔

Proof of Theorem noresle
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 unss 4139 . . . 4 ((dom 𝑈𝐴 ∧ dom 𝑆𝐴) ↔ (dom 𝑈 ∪ dom 𝑆) ⊆ 𝐴)
2 ssralv 4012 . . . 4 ((dom 𝑈 ∪ dom 𝑆) ⊆ 𝐴 → (∀𝑔𝐴 ¬ (𝑆 ↾ suc 𝑔) <s (𝑈 ↾ suc 𝑔) → ∀𝑔 ∈ (dom 𝑈 ∪ dom 𝑆) ¬ (𝑆 ↾ suc 𝑔) <s (𝑈 ↾ suc 𝑔)))
31, 2sylbi 219 . . 3 ((dom 𝑈𝐴 ∧ dom 𝑆𝐴) → (∀𝑔𝐴 ¬ (𝑆 ↾ suc 𝑔) <s (𝑈 ↾ suc 𝑔) → ∀𝑔 ∈ (dom 𝑈 ∪ dom 𝑆) ¬ (𝑆 ↾ suc 𝑔) <s (𝑈 ↾ suc 𝑔)))
433impia 1113 . 2 ((dom 𝑈𝐴 ∧ dom 𝑆𝐴 ∧ ∀𝑔𝐴 ¬ (𝑆 ↾ suc 𝑔) <s (𝑈 ↾ suc 𝑔)) → ∀𝑔 ∈ (dom 𝑈 ∪ dom 𝑆) ¬ (𝑆 ↾ suc 𝑔) <s (𝑈 ↾ suc 𝑔))
5 breq1 5045 . . . . . . . 8 (𝑈 = 𝑆 → (𝑈 <s 𝑈𝑆 <s 𝑈))
65notbid 320 . . . . . . 7 (𝑈 = 𝑆 → (¬ 𝑈 <s 𝑈 ↔ ¬ 𝑆 <s 𝑈))
76biimpd 231 . . . . . 6 (𝑈 = 𝑆 → (¬ 𝑈 <s 𝑈 → ¬ 𝑆 <s 𝑈))
8 sltso 33189 . . . . . . . 8 <s Or No
9 sonr 5472 . . . . . . . 8 (( <s Or No 𝑈 No ) → ¬ 𝑈 <s 𝑈)
108, 9mpan 688 . . . . . . 7 (𝑈 No → ¬ 𝑈 <s 𝑈)
1110adantr 483 . . . . . 6 ((𝑈 No 𝑆 No ) → ¬ 𝑈 <s 𝑈)
127, 11impel 508 . . . . 5 ((𝑈 = 𝑆 ∧ (𝑈 No 𝑆 No )) → ¬ 𝑆 <s 𝑈)
1312adantrr 715 . . . 4 ((𝑈 = 𝑆 ∧ ((𝑈 No 𝑆 No ) ∧ ∀𝑔 ∈ (dom 𝑈 ∪ dom 𝑆) ¬ (𝑆 ↾ suc 𝑔) <s (𝑈 ↾ suc 𝑔))) → ¬ 𝑆 <s 𝑈)
1413ex 415 . . 3 (𝑈 = 𝑆 → (((𝑈 No 𝑆 No ) ∧ ∀𝑔 ∈ (dom 𝑈 ∪ dom 𝑆) ¬ (𝑆 ↾ suc 𝑔) <s (𝑈 ↾ suc 𝑔)) → ¬ 𝑆 <s 𝑈))
15 simprl 769 . . . . 5 ((𝑈𝑆 ∧ ((𝑈 No 𝑆 No ) ∧ ∀𝑔 ∈ (dom 𝑈 ∪ dom 𝑆) ¬ (𝑆 ↾ suc 𝑔) <s (𝑈 ↾ suc 𝑔))) → (𝑈 No 𝑆 No ))
16 simprll 777 . . . . . . . . . . 11 ((𝑈𝑆 ∧ ((𝑈 No 𝑆 No ) ∧ ∀𝑔 ∈ (dom 𝑈 ∪ dom 𝑆) ¬ (𝑆 ↾ suc 𝑔) <s (𝑈 ↾ suc 𝑔))) → 𝑈 No )
17 simprlr 778 . . . . . . . . . . 11 ((𝑈𝑆 ∧ ((𝑈 No 𝑆 No ) ∧ ∀𝑔 ∈ (dom 𝑈 ∪ dom 𝑆) ¬ (𝑆 ↾ suc 𝑔) <s (𝑈 ↾ suc 𝑔))) → 𝑆 No )
18 simpl 485 . . . . . . . . . . 11 ((𝑈𝑆 ∧ ((𝑈 No 𝑆 No ) ∧ ∀𝑔 ∈ (dom 𝑈 ∪ dom 𝑆) ¬ (𝑆 ↾ suc 𝑔) <s (𝑈 ↾ suc 𝑔))) → 𝑈𝑆)
19 nosepne 33193 . . . . . . . . . . 11 ((𝑈 No 𝑆 No 𝑈𝑆) → (𝑈 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑆𝑥)}) ≠ (𝑆 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑆𝑥)}))
2016, 17, 18, 19syl3anc 1367 . . . . . . . . . 10 ((𝑈𝑆 ∧ ((𝑈 No 𝑆 No ) ∧ ∀𝑔 ∈ (dom 𝑈 ∪ dom 𝑆) ¬ (𝑆 ↾ suc 𝑔) <s (𝑈 ↾ suc 𝑔))) → (𝑈 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑆𝑥)}) ≠ (𝑆 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑆𝑥)}))
21 nosepon 33180 . . . . . . . . . . . . 13 ((𝑈 No 𝑆 No 𝑈𝑆) → {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑆𝑥)} ∈ On)
2216, 17, 18, 21syl3anc 1367 . . . . . . . . . . . 12 ((𝑈𝑆 ∧ ((𝑈 No 𝑆 No ) ∧ ∀𝑔 ∈ (dom 𝑈 ∪ dom 𝑆) ¬ (𝑆 ↾ suc 𝑔) <s (𝑈 ↾ suc 𝑔))) → {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑆𝑥)} ∈ On)
23 sucidg 6245 . . . . . . . . . . . 12 ( {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑆𝑥)} ∈ On → {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑆𝑥)} ∈ suc {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑆𝑥)})
2422, 23syl 17 . . . . . . . . . . 11 ((𝑈𝑆 ∧ ((𝑈 No 𝑆 No ) ∧ ∀𝑔 ∈ (dom 𝑈 ∪ dom 𝑆) ¬ (𝑆 ↾ suc 𝑔) <s (𝑈 ↾ suc 𝑔))) → {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑆𝑥)} ∈ suc {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑆𝑥)})
2524fvresd 6666 . . . . . . . . . 10 ((𝑈𝑆 ∧ ((𝑈 No 𝑆 No ) ∧ ∀𝑔 ∈ (dom 𝑈 ∪ dom 𝑆) ¬ (𝑆 ↾ suc 𝑔) <s (𝑈 ↾ suc 𝑔))) → ((𝑈 ↾ suc {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑆𝑥)})‘ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑆𝑥)}) = (𝑈 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑆𝑥)}))
2624fvresd 6666 . . . . . . . . . 10 ((𝑈𝑆 ∧ ((𝑈 No 𝑆 No ) ∧ ∀𝑔 ∈ (dom 𝑈 ∪ dom 𝑆) ¬ (𝑆 ↾ suc 𝑔) <s (𝑈 ↾ suc 𝑔))) → ((𝑆 ↾ suc {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑆𝑥)})‘ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑆𝑥)}) = (𝑆 {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑆𝑥)}))
2720, 25, 263netr4d 3083 . . . . . . . . 9 ((𝑈𝑆 ∧ ((𝑈 No 𝑆 No ) ∧ ∀𝑔 ∈ (dom 𝑈 ∪ dom 𝑆) ¬ (𝑆 ↾ suc 𝑔) <s (𝑈 ↾ suc 𝑔))) → ((𝑈 ↾ suc {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑆𝑥)})‘ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑆𝑥)}) ≠ ((𝑆 ↾ suc {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑆𝑥)})‘ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑆𝑥)}))
2827neneqd 3011 . . . . . . . 8 ((𝑈𝑆 ∧ ((𝑈 No 𝑆 No ) ∧ ∀𝑔 ∈ (dom 𝑈 ∪ dom 𝑆) ¬ (𝑆 ↾ suc 𝑔) <s (𝑈 ↾ suc 𝑔))) → ¬ ((𝑈 ↾ suc {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑆𝑥)})‘ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑆𝑥)}) = ((𝑆 ↾ suc {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑆𝑥)})‘ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑆𝑥)}))
29 fveq1 6645 . . . . . . . 8 ((𝑈 ↾ suc {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑆𝑥)}) = (𝑆 ↾ suc {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑆𝑥)}) → ((𝑈 ↾ suc {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑆𝑥)})‘ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑆𝑥)}) = ((𝑆 ↾ suc {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑆𝑥)})‘ {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑆𝑥)}))
3028, 29nsyl 142 . . . . . . 7 ((𝑈𝑆 ∧ ((𝑈 No 𝑆 No ) ∧ ∀𝑔 ∈ (dom 𝑈 ∪ dom 𝑆) ¬ (𝑆 ↾ suc 𝑔) <s (𝑈 ↾ suc 𝑔))) → ¬ (𝑈 ↾ suc {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑆𝑥)}) = (𝑆 ↾ suc {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑆𝑥)}))
31 nosepdm 33196 . . . . . . . . 9 ((𝑈 No 𝑆 No 𝑈𝑆) → {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑆𝑥)} ∈ (dom 𝑈 ∪ dom 𝑆))
3216, 17, 18, 31syl3anc 1367 . . . . . . . 8 ((𝑈𝑆 ∧ ((𝑈 No 𝑆 No ) ∧ ∀𝑔 ∈ (dom 𝑈 ∪ dom 𝑆) ¬ (𝑆 ↾ suc 𝑔) <s (𝑈 ↾ suc 𝑔))) → {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑆𝑥)} ∈ (dom 𝑈 ∪ dom 𝑆))
33 simprr 771 . . . . . . . 8 ((𝑈𝑆 ∧ ((𝑈 No 𝑆 No ) ∧ ∀𝑔 ∈ (dom 𝑈 ∪ dom 𝑆) ¬ (𝑆 ↾ suc 𝑔) <s (𝑈 ↾ suc 𝑔))) → ∀𝑔 ∈ (dom 𝑈 ∪ dom 𝑆) ¬ (𝑆 ↾ suc 𝑔) <s (𝑈 ↾ suc 𝑔))
34 suceq 6232 . . . . . . . . . . . 12 (𝑔 = {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑆𝑥)} → suc 𝑔 = suc {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑆𝑥)})
3534reseq2d 5829 . . . . . . . . . . 11 (𝑔 = {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑆𝑥)} → (𝑆 ↾ suc 𝑔) = (𝑆 ↾ suc {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑆𝑥)}))
3634reseq2d 5829 . . . . . . . . . . 11 (𝑔 = {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑆𝑥)} → (𝑈 ↾ suc 𝑔) = (𝑈 ↾ suc {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑆𝑥)}))
3735, 36breq12d 5055 . . . . . . . . . 10 (𝑔 = {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑆𝑥)} → ((𝑆 ↾ suc 𝑔) <s (𝑈 ↾ suc 𝑔) ↔ (𝑆 ↾ suc {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑆𝑥)}) <s (𝑈 ↾ suc {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑆𝑥)})))
3837notbid 320 . . . . . . . . 9 (𝑔 = {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑆𝑥)} → (¬ (𝑆 ↾ suc 𝑔) <s (𝑈 ↾ suc 𝑔) ↔ ¬ (𝑆 ↾ suc {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑆𝑥)}) <s (𝑈 ↾ suc {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑆𝑥)})))
3938rspcv 3597 . . . . . . . 8 ( {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑆𝑥)} ∈ (dom 𝑈 ∪ dom 𝑆) → (∀𝑔 ∈ (dom 𝑈 ∪ dom 𝑆) ¬ (𝑆 ↾ suc 𝑔) <s (𝑈 ↾ suc 𝑔) → ¬ (𝑆 ↾ suc {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑆𝑥)}) <s (𝑈 ↾ suc {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑆𝑥)})))
4032, 33, 39sylc 65 . . . . . . 7 ((𝑈𝑆 ∧ ((𝑈 No 𝑆 No ) ∧ ∀𝑔 ∈ (dom 𝑈 ∪ dom 𝑆) ¬ (𝑆 ↾ suc 𝑔) <s (𝑈 ↾ suc 𝑔))) → ¬ (𝑆 ↾ suc {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑆𝑥)}) <s (𝑈 ↾ suc {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑆𝑥)}))
41 suceloni 7506 . . . . . . . . . 10 ( {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑆𝑥)} ∈ On → suc {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑆𝑥)} ∈ On)
4222, 41syl 17 . . . . . . . . 9 ((𝑈𝑆 ∧ ((𝑈 No 𝑆 No ) ∧ ∀𝑔 ∈ (dom 𝑈 ∪ dom 𝑆) ¬ (𝑆 ↾ suc 𝑔) <s (𝑈 ↾ suc 𝑔))) → suc {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑆𝑥)} ∈ On)
43 noreson 33175 . . . . . . . . 9 ((𝑈 No ∧ suc {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑆𝑥)} ∈ On) → (𝑈 ↾ suc {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑆𝑥)}) ∈ No )
4416, 42, 43syl2anc 586 . . . . . . . 8 ((𝑈𝑆 ∧ ((𝑈 No 𝑆 No ) ∧ ∀𝑔 ∈ (dom 𝑈 ∪ dom 𝑆) ¬ (𝑆 ↾ suc 𝑔) <s (𝑈 ↾ suc 𝑔))) → (𝑈 ↾ suc {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑆𝑥)}) ∈ No )
45 noreson 33175 . . . . . . . . 9 ((𝑆 No ∧ suc {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑆𝑥)} ∈ On) → (𝑆 ↾ suc {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑆𝑥)}) ∈ No )
4617, 42, 45syl2anc 586 . . . . . . . 8 ((𝑈𝑆 ∧ ((𝑈 No 𝑆 No ) ∧ ∀𝑔 ∈ (dom 𝑈 ∪ dom 𝑆) ¬ (𝑆 ↾ suc 𝑔) <s (𝑈 ↾ suc 𝑔))) → (𝑆 ↾ suc {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑆𝑥)}) ∈ No )
47 solin 5474 . . . . . . . . 9 (( <s Or No ∧ ((𝑈 ↾ suc {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑆𝑥)}) ∈ No ∧ (𝑆 ↾ suc {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑆𝑥)}) ∈ No )) → ((𝑈 ↾ suc {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑆𝑥)}) <s (𝑆 ↾ suc {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑆𝑥)}) ∨ (𝑈 ↾ suc {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑆𝑥)}) = (𝑆 ↾ suc {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑆𝑥)}) ∨ (𝑆 ↾ suc {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑆𝑥)}) <s (𝑈 ↾ suc {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑆𝑥)})))
488, 47mpan 688 . . . . . . . 8 (((𝑈 ↾ suc {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑆𝑥)}) ∈ No ∧ (𝑆 ↾ suc {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑆𝑥)}) ∈ No ) → ((𝑈 ↾ suc {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑆𝑥)}) <s (𝑆 ↾ suc {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑆𝑥)}) ∨ (𝑈 ↾ suc {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑆𝑥)}) = (𝑆 ↾ suc {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑆𝑥)}) ∨ (𝑆 ↾ suc {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑆𝑥)}) <s (𝑈 ↾ suc {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑆𝑥)})))
4944, 46, 48syl2anc 586 . . . . . . 7 ((𝑈𝑆 ∧ ((𝑈 No 𝑆 No ) ∧ ∀𝑔 ∈ (dom 𝑈 ∪ dom 𝑆) ¬ (𝑆 ↾ suc 𝑔) <s (𝑈 ↾ suc 𝑔))) → ((𝑈 ↾ suc {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑆𝑥)}) <s (𝑆 ↾ suc {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑆𝑥)}) ∨ (𝑈 ↾ suc {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑆𝑥)}) = (𝑆 ↾ suc {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑆𝑥)}) ∨ (𝑆 ↾ suc {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑆𝑥)}) <s (𝑈 ↾ suc {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑆𝑥)})))
5030, 40, 49ecase23d 1469 . . . . . 6 ((𝑈𝑆 ∧ ((𝑈 No 𝑆 No ) ∧ ∀𝑔 ∈ (dom 𝑈 ∪ dom 𝑆) ¬ (𝑆 ↾ suc 𝑔) <s (𝑈 ↾ suc 𝑔))) → (𝑈 ↾ suc {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑆𝑥)}) <s (𝑆 ↾ suc {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑆𝑥)}))
51 sltres 33177 . . . . . . 7 ((𝑈 No 𝑆 No ∧ suc {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑆𝑥)} ∈ On) → ((𝑈 ↾ suc {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑆𝑥)}) <s (𝑆 ↾ suc {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑆𝑥)}) → 𝑈 <s 𝑆))
5216, 17, 42, 51syl3anc 1367 . . . . . 6 ((𝑈𝑆 ∧ ((𝑈 No 𝑆 No ) ∧ ∀𝑔 ∈ (dom 𝑈 ∪ dom 𝑆) ¬ (𝑆 ↾ suc 𝑔) <s (𝑈 ↾ suc 𝑔))) → ((𝑈 ↾ suc {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑆𝑥)}) <s (𝑆 ↾ suc {𝑥 ∈ On ∣ (𝑈𝑥) ≠ (𝑆𝑥)}) → 𝑈 <s 𝑆))
5350, 52mpd 15 . . . . 5 ((𝑈𝑆 ∧ ((𝑈 No 𝑆 No ) ∧ ∀𝑔 ∈ (dom 𝑈 ∪ dom 𝑆) ¬ (𝑆 ↾ suc 𝑔) <s (𝑈 ↾ suc 𝑔))) → 𝑈 <s 𝑆)
54 soasym 5480 . . . . . 6 (( <s Or No ∧ (𝑈 No 𝑆 No )) → (𝑈 <s 𝑆 → ¬ 𝑆 <s 𝑈))
558, 54mpan 688 . . . . 5 ((𝑈 No 𝑆 No ) → (𝑈 <s 𝑆 → ¬ 𝑆 <s 𝑈))
5615, 53, 55sylc 65 . . . 4 ((𝑈𝑆 ∧ ((𝑈 No 𝑆 No ) ∧ ∀𝑔 ∈ (dom 𝑈 ∪ dom 𝑆) ¬ (𝑆 ↾ suc 𝑔) <s (𝑈 ↾ suc 𝑔))) → ¬ 𝑆 <s 𝑈)
5756ex 415 . . 3 (𝑈𝑆 → (((𝑈 No 𝑆 No ) ∧ ∀𝑔 ∈ (dom 𝑈 ∪ dom 𝑆) ¬ (𝑆 ↾ suc 𝑔) <s (𝑈 ↾ suc 𝑔)) → ¬ 𝑆 <s 𝑈))
5814, 57pm2.61ine 3089 . 2 (((𝑈 No 𝑆 No ) ∧ ∀𝑔 ∈ (dom 𝑈 ∪ dom 𝑆) ¬ (𝑆 ↾ suc 𝑔) <s (𝑈 ↾ suc 𝑔)) → ¬ 𝑆 <s 𝑈)
594, 58sylan2 594 1 (((𝑈 No 𝑆 No ) ∧ (dom 𝑈𝐴 ∧ dom 𝑆𝐴 ∧ ∀𝑔𝐴 ¬ (𝑆 ↾ suc 𝑔) <s (𝑈 ↾ suc 𝑔))) → ¬ 𝑆 <s 𝑈)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 398   ∨ w3o 1082   ∧ w3a 1083   = wceq 1537   ∈ wcel 2114   ≠ wne 3006  ∀wral 3125  {crab 3129   ∪ cun 3911   ⊆ wss 3913  ∩ cint 4852   class class class wbr 5042   Or wor 5449  dom cdm 5531   ↾ cres 5533  Oncon0 6167  suc csuc 6169  ‘cfv 6331   No csur 33155
 Copyright terms: Public domain W3C validator