Metamath Proof Explorer

Theorem noresle

Description: Restriction law for surreals. Lemma 2.1.4 of Lipparini p. 3. (Contributed by Scott Fenton, 5-Dec-2021)

Ref Expression
Assertion noresle ( ( ( 𝑈 ∈ No ∧ 𝑆 ∈ No ) ∧ ( dom 𝑈 ⊆ 𝐴 ∧ dom 𝑆 ⊆ 𝐴 ∧ ∀ 𝑔 ∈ 𝐴 ¬ ( 𝑆 ↾ suc 𝑔 ) <s ( 𝑈 ↾ suc 𝑔 ) ) ) → ¬ 𝑆 <s 𝑈 )

Proof

Step Hyp Ref Expression
1 unss ⊢ ( ( dom 𝑈 ⊆ 𝐴 ∧ dom 𝑆 ⊆ 𝐴 ) ↔ ( dom 𝑈 ∪ dom 𝑆 ) ⊆ 𝐴 )
2 ssralv ⊢ ( ( dom 𝑈 ∪ dom 𝑆 ) ⊆ 𝐴 → ( ∀ 𝑔 ∈ 𝐴 ¬ ( 𝑆 ↾ suc 𝑔 ) <s ( 𝑈 ↾ suc 𝑔 ) → ∀ 𝑔 ∈ ( dom 𝑈 ∪ dom 𝑆 ) ¬ ( 𝑆 ↾ suc 𝑔 ) <s ( 𝑈 ↾ suc 𝑔 ) ) )
3 1 2 sylbi ⊢ ( ( dom 𝑈 ⊆ 𝐴 ∧ dom 𝑆 ⊆ 𝐴 ) → ( ∀ 𝑔 ∈ 𝐴 ¬ ( 𝑆 ↾ suc 𝑔 ) <s ( 𝑈 ↾ suc 𝑔 ) → ∀ 𝑔 ∈ ( dom 𝑈 ∪ dom 𝑆 ) ¬ ( 𝑆 ↾ suc 𝑔 ) <s ( 𝑈 ↾ suc 𝑔 ) ) )
4 3 3impia ⊢ ( ( dom 𝑈 ⊆ 𝐴 ∧ dom 𝑆 ⊆ 𝐴 ∧ ∀ 𝑔 ∈ 𝐴 ¬ ( 𝑆 ↾ suc 𝑔 ) <s ( 𝑈 ↾ suc 𝑔 ) ) → ∀ 𝑔 ∈ ( dom 𝑈 ∪ dom 𝑆 ) ¬ ( 𝑆 ↾ suc 𝑔 ) <s ( 𝑈 ↾ suc 𝑔 ) )
5 breq1 ⊢ ( 𝑈 = 𝑆 → ( 𝑈 <s 𝑈 ↔ 𝑆 <s 𝑈 ) )
6 5 notbid ⊢ ( 𝑈 = 𝑆 → ( ¬ 𝑈 <s 𝑈 ↔ ¬ 𝑆 <s 𝑈 ) )
7 6 biimpd ⊢ ( 𝑈 = 𝑆 → ( ¬ 𝑈 <s 𝑈 → ¬ 𝑆 <s 𝑈 ) )
8 ltsso ⊢ <s Or No
9 sonr ⊢ ( ( <s Or No ∧ 𝑈 ∈ No ) → ¬ 𝑈 <s 𝑈 )
10 8 9 mpan ⊢ ( 𝑈 ∈ No → ¬ 𝑈 <s 𝑈 )
11 10 adantr ⊢ ( ( 𝑈 ∈ No ∧ 𝑆 ∈ No ) → ¬ 𝑈 <s 𝑈 )
12 7 11 impel ⊢ ( ( 𝑈 = 𝑆 ∧ ( 𝑈 ∈ No ∧ 𝑆 ∈ No ) ) → ¬ 𝑆 <s 𝑈 )
13 12 adantrr ⊢ ( ( 𝑈 = 𝑆 ∧ ( ( 𝑈 ∈ No ∧ 𝑆 ∈ No ) ∧ ∀ 𝑔 ∈ ( dom 𝑈 ∪ dom 𝑆 ) ¬ ( 𝑆 ↾ suc 𝑔 ) <s ( 𝑈 ↾ suc 𝑔 ) ) ) → ¬ 𝑆 <s 𝑈 )
14 13 ex ⊢ ( 𝑈 = 𝑆 → ( ( ( 𝑈 ∈ No ∧ 𝑆 ∈ No ) ∧ ∀ 𝑔 ∈ ( dom 𝑈 ∪ dom 𝑆 ) ¬ ( 𝑆 ↾ suc 𝑔 ) <s ( 𝑈 ↾ suc 𝑔 ) ) → ¬ 𝑆 <s 𝑈 ) )
15 simprl ⊢ ( ( 𝑈 ≠ 𝑆 ∧ ( ( 𝑈 ∈ No ∧ 𝑆 ∈ No ) ∧ ∀ 𝑔 ∈ ( dom 𝑈 ∪ dom 𝑆 ) ¬ ( 𝑆 ↾ suc 𝑔 ) <s ( 𝑈 ↾ suc 𝑔 ) ) ) → ( 𝑈 ∈ No ∧ 𝑆 ∈ No ) )
16 simprll ⊢ ( ( 𝑈 ≠ 𝑆 ∧ ( ( 𝑈 ∈ No ∧ 𝑆 ∈ No ) ∧ ∀ 𝑔 ∈ ( dom 𝑈 ∪ dom 𝑆 ) ¬ ( 𝑆 ↾ suc 𝑔 ) <s ( 𝑈 ↾ suc 𝑔 ) ) ) → 𝑈 ∈ No )
17 simprlr ⊢ ( ( 𝑈 ≠ 𝑆 ∧ ( ( 𝑈 ∈ No ∧ 𝑆 ∈ No ) ∧ ∀ 𝑔 ∈ ( dom 𝑈 ∪ dom 𝑆 ) ¬ ( 𝑆 ↾ suc 𝑔 ) <s ( 𝑈 ↾ suc 𝑔 ) ) ) → 𝑆 ∈ No )
18 simpl ⊢ ( ( 𝑈 ≠ 𝑆 ∧ ( ( 𝑈 ∈ No ∧ 𝑆 ∈ No ) ∧ ∀ 𝑔 ∈ ( dom 𝑈 ∪ dom 𝑆 ) ¬ ( 𝑆 ↾ suc 𝑔 ) <s ( 𝑈 ↾ suc 𝑔 ) ) ) → 𝑈 ≠ 𝑆 )
19 nosepne ⊢ ( ( 𝑈 ∈ No ∧ 𝑆 ∈ No ∧ 𝑈 ≠ 𝑆 ) → ( 𝑈 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑆 ‘ 𝑥 ) } ) ≠ ( 𝑆 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑆 ‘ 𝑥 ) } ) )
20 16 17 18 19 syl3anc ⊢ ( ( 𝑈 ≠ 𝑆 ∧ ( ( 𝑈 ∈ No ∧ 𝑆 ∈ No ) ∧ ∀ 𝑔 ∈ ( dom 𝑈 ∪ dom 𝑆 ) ¬ ( 𝑆 ↾ suc 𝑔 ) <s ( 𝑈 ↾ suc 𝑔 ) ) ) → ( 𝑈 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑆 ‘ 𝑥 ) } ) ≠ ( 𝑆 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑆 ‘ 𝑥 ) } ) )
21 nosepon ⊢ ( ( 𝑈 ∈ No ∧ 𝑆 ∈ No ∧ 𝑈 ≠ 𝑆 ) → ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑆 ‘ 𝑥 ) } ∈ On )
22 16 17 18 21 syl3anc ⊢ ( ( 𝑈 ≠ 𝑆 ∧ ( ( 𝑈 ∈ No ∧ 𝑆 ∈ No ) ∧ ∀ 𝑔 ∈ ( dom 𝑈 ∪ dom 𝑆 ) ¬ ( 𝑆 ↾ suc 𝑔 ) <s ( 𝑈 ↾ suc 𝑔 ) ) ) → ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑆 ‘ 𝑥 ) } ∈ On )
23 sucidg ⊢ ( ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑆 ‘ 𝑥 ) } ∈ On → ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑆 ‘ 𝑥 ) } ∈ suc ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑆 ‘ 𝑥 ) } )
24 22 23 syl ⊢ ( ( 𝑈 ≠ 𝑆 ∧ ( ( 𝑈 ∈ No ∧ 𝑆 ∈ No ) ∧ ∀ 𝑔 ∈ ( dom 𝑈 ∪ dom 𝑆 ) ¬ ( 𝑆 ↾ suc 𝑔 ) <s ( 𝑈 ↾ suc 𝑔 ) ) ) → ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑆 ‘ 𝑥 ) } ∈ suc ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑆 ‘ 𝑥 ) } )
25 24 fvresd ⊢ ( ( 𝑈 ≠ 𝑆 ∧ ( ( 𝑈 ∈ No ∧ 𝑆 ∈ No ) ∧ ∀ 𝑔 ∈ ( dom 𝑈 ∪ dom 𝑆 ) ¬ ( 𝑆 ↾ suc 𝑔 ) <s ( 𝑈 ↾ suc 𝑔 ) ) ) → ( ( 𝑈 ↾ suc ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑆 ‘ 𝑥 ) } ) ‘ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑆 ‘ 𝑥 ) } ) = ( 𝑈 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑆 ‘ 𝑥 ) } ) )
26 24 fvresd ⊢ ( ( 𝑈 ≠ 𝑆 ∧ ( ( 𝑈 ∈ No ∧ 𝑆 ∈ No ) ∧ ∀ 𝑔 ∈ ( dom 𝑈 ∪ dom 𝑆 ) ¬ ( 𝑆 ↾ suc 𝑔 ) <s ( 𝑈 ↾ suc 𝑔 ) ) ) → ( ( 𝑆 ↾ suc ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑆 ‘ 𝑥 ) } ) ‘ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑆 ‘ 𝑥 ) } ) = ( 𝑆 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑆 ‘ 𝑥 ) } ) )
27 20 25 26 3netr4d ⊢ ( ( 𝑈 ≠ 𝑆 ∧ ( ( 𝑈 ∈ No ∧ 𝑆 ∈ No ) ∧ ∀ 𝑔 ∈ ( dom 𝑈 ∪ dom 𝑆 ) ¬ ( 𝑆 ↾ suc 𝑔 ) <s ( 𝑈 ↾ suc 𝑔 ) ) ) → ( ( 𝑈 ↾ suc ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑆 ‘ 𝑥 ) } ) ‘ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑆 ‘ 𝑥 ) } ) ≠ ( ( 𝑆 ↾ suc ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑆 ‘ 𝑥 ) } ) ‘ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑆 ‘ 𝑥 ) } ) )
28 27 neneqd ⊢ ( ( 𝑈 ≠ 𝑆 ∧ ( ( 𝑈 ∈ No ∧ 𝑆 ∈ No ) ∧ ∀ 𝑔 ∈ ( dom 𝑈 ∪ dom 𝑆 ) ¬ ( 𝑆 ↾ suc 𝑔 ) <s ( 𝑈 ↾ suc 𝑔 ) ) ) → ¬ ( ( 𝑈 ↾ suc ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑆 ‘ 𝑥 ) } ) ‘ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑆 ‘ 𝑥 ) } ) = ( ( 𝑆 ↾ suc ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑆 ‘ 𝑥 ) } ) ‘ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑆 ‘ 𝑥 ) } ) )
29 fveq1 ⊢ ( ( 𝑈 ↾ suc ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑆 ‘ 𝑥 ) } ) = ( 𝑆 ↾ suc ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑆 ‘ 𝑥 ) } ) → ( ( 𝑈 ↾ suc ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑆 ‘ 𝑥 ) } ) ‘ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑆 ‘ 𝑥 ) } ) = ( ( 𝑆 ↾ suc ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑆 ‘ 𝑥 ) } ) ‘ ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑆 ‘ 𝑥 ) } ) )
30 28 29 nsyl ⊢ ( ( 𝑈 ≠ 𝑆 ∧ ( ( 𝑈 ∈ No ∧ 𝑆 ∈ No ) ∧ ∀ 𝑔 ∈ ( dom 𝑈 ∪ dom 𝑆 ) ¬ ( 𝑆 ↾ suc 𝑔 ) <s ( 𝑈 ↾ suc 𝑔 ) ) ) → ¬ ( 𝑈 ↾ suc ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑆 ‘ 𝑥 ) } ) = ( 𝑆 ↾ suc ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑆 ‘ 𝑥 ) } ) )
31 nosepdm ⊢ ( ( 𝑈 ∈ No ∧ 𝑆 ∈ No ∧ 𝑈 ≠ 𝑆 ) → ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑆 ‘ 𝑥 ) } ∈ ( dom 𝑈 ∪ dom 𝑆 ) )
32 16 17 18 31 syl3anc ⊢ ( ( 𝑈 ≠ 𝑆 ∧ ( ( 𝑈 ∈ No ∧ 𝑆 ∈ No ) ∧ ∀ 𝑔 ∈ ( dom 𝑈 ∪ dom 𝑆 ) ¬ ( 𝑆 ↾ suc 𝑔 ) <s ( 𝑈 ↾ suc 𝑔 ) ) ) → ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑆 ‘ 𝑥 ) } ∈ ( dom 𝑈 ∪ dom 𝑆 ) )
33 simprr ⊢ ( ( 𝑈 ≠ 𝑆 ∧ ( ( 𝑈 ∈ No ∧ 𝑆 ∈ No ) ∧ ∀ 𝑔 ∈ ( dom 𝑈 ∪ dom 𝑆 ) ¬ ( 𝑆 ↾ suc 𝑔 ) <s ( 𝑈 ↾ suc 𝑔 ) ) ) → ∀ 𝑔 ∈ ( dom 𝑈 ∪ dom 𝑆 ) ¬ ( 𝑆 ↾ suc 𝑔 ) <s ( 𝑈 ↾ suc 𝑔 ) )
34 suceq ⊢ ( 𝑔 = ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑆 ‘ 𝑥 ) } → suc 𝑔 = suc ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑆 ‘ 𝑥 ) } )
35 34 reseq2d ⊢ ( 𝑔 = ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑆 ‘ 𝑥 ) } → ( 𝑆 ↾ suc 𝑔 ) = ( 𝑆 ↾ suc ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑆 ‘ 𝑥 ) } ) )
36 34 reseq2d ⊢ ( 𝑔 = ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑆 ‘ 𝑥 ) } → ( 𝑈 ↾ suc 𝑔 ) = ( 𝑈 ↾ suc ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑆 ‘ 𝑥 ) } ) )
37 35 36 breq12d ⊢ ( 𝑔 = ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑆 ‘ 𝑥 ) } → ( ( 𝑆 ↾ suc 𝑔 ) <s ( 𝑈 ↾ suc 𝑔 ) ↔ ( 𝑆 ↾ suc ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑆 ‘ 𝑥 ) } ) <s ( 𝑈 ↾ suc ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑆 ‘ 𝑥 ) } ) ) )
38 37 notbid ⊢ ( 𝑔 = ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑆 ‘ 𝑥 ) } → ( ¬ ( 𝑆 ↾ suc 𝑔 ) <s ( 𝑈 ↾ suc 𝑔 ) ↔ ¬ ( 𝑆 ↾ suc ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑆 ‘ 𝑥 ) } ) <s ( 𝑈 ↾ suc ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑆 ‘ 𝑥 ) } ) ) )
39 38 rspcv ⊢ ( ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑆 ‘ 𝑥 ) } ∈ ( dom 𝑈 ∪ dom 𝑆 ) → ( ∀ 𝑔 ∈ ( dom 𝑈 ∪ dom 𝑆 ) ¬ ( 𝑆 ↾ suc 𝑔 ) <s ( 𝑈 ↾ suc 𝑔 ) → ¬ ( 𝑆 ↾ suc ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑆 ‘ 𝑥 ) } ) <s ( 𝑈 ↾ suc ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑆 ‘ 𝑥 ) } ) ) )
40 32 33 39 sylc ⊢ ( ( 𝑈 ≠ 𝑆 ∧ ( ( 𝑈 ∈ No ∧ 𝑆 ∈ No ) ∧ ∀ 𝑔 ∈ ( dom 𝑈 ∪ dom 𝑆 ) ¬ ( 𝑆 ↾ suc 𝑔 ) <s ( 𝑈 ↾ suc 𝑔 ) ) ) → ¬ ( 𝑆 ↾ suc ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑆 ‘ 𝑥 ) } ) <s ( 𝑈 ↾ suc ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑆 ‘ 𝑥 ) } ) )
41 onsuc ⊢ ( ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑆 ‘ 𝑥 ) } ∈ On → suc ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑆 ‘ 𝑥 ) } ∈ On )
42 22 41 syl ⊢ ( ( 𝑈 ≠ 𝑆 ∧ ( ( 𝑈 ∈ No ∧ 𝑆 ∈ No ) ∧ ∀ 𝑔 ∈ ( dom 𝑈 ∪ dom 𝑆 ) ¬ ( 𝑆 ↾ suc 𝑔 ) <s ( 𝑈 ↾ suc 𝑔 ) ) ) → suc ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑆 ‘ 𝑥 ) } ∈ On )
43 noreson ⊢ ( ( 𝑈 ∈ No ∧ suc ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑆 ‘ 𝑥 ) } ∈ On ) → ( 𝑈 ↾ suc ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑆 ‘ 𝑥 ) } ) ∈ No )
44 16 42 43 syl2anc ⊢ ( ( 𝑈 ≠ 𝑆 ∧ ( ( 𝑈 ∈ No ∧ 𝑆 ∈ No ) ∧ ∀ 𝑔 ∈ ( dom 𝑈 ∪ dom 𝑆 ) ¬ ( 𝑆 ↾ suc 𝑔 ) <s ( 𝑈 ↾ suc 𝑔 ) ) ) → ( 𝑈 ↾ suc ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑆 ‘ 𝑥 ) } ) ∈ No )
45 noreson ⊢ ( ( 𝑆 ∈ No ∧ suc ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑆 ‘ 𝑥 ) } ∈ On ) → ( 𝑆 ↾ suc ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑆 ‘ 𝑥 ) } ) ∈ No )
46 17 42 45 syl2anc ⊢ ( ( 𝑈 ≠ 𝑆 ∧ ( ( 𝑈 ∈ No ∧ 𝑆 ∈ No ) ∧ ∀ 𝑔 ∈ ( dom 𝑈 ∪ dom 𝑆 ) ¬ ( 𝑆 ↾ suc 𝑔 ) <s ( 𝑈 ↾ suc 𝑔 ) ) ) → ( 𝑆 ↾ suc ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑆 ‘ 𝑥 ) } ) ∈ No )
47 solin ⊢ ( ( <s Or No ∧ ( ( 𝑈 ↾ suc ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑆 ‘ 𝑥 ) } ) ∈ No ∧ ( 𝑆 ↾ suc ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑆 ‘ 𝑥 ) } ) ∈ No ) ) → ( ( 𝑈 ↾ suc ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑆 ‘ 𝑥 ) } ) <s ( 𝑆 ↾ suc ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑆 ‘ 𝑥 ) } ) ∨ ( 𝑈 ↾ suc ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑆 ‘ 𝑥 ) } ) = ( 𝑆 ↾ suc ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑆 ‘ 𝑥 ) } ) ∨ ( 𝑆 ↾ suc ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑆 ‘ 𝑥 ) } ) <s ( 𝑈 ↾ suc ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑆 ‘ 𝑥 ) } ) ) )
48 8 47 mpan ⊢ ( ( ( 𝑈 ↾ suc ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑆 ‘ 𝑥 ) } ) ∈ No ∧ ( 𝑆 ↾ suc ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑆 ‘ 𝑥 ) } ) ∈ No ) → ( ( 𝑈 ↾ suc ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑆 ‘ 𝑥 ) } ) <s ( 𝑆 ↾ suc ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑆 ‘ 𝑥 ) } ) ∨ ( 𝑈 ↾ suc ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑆 ‘ 𝑥 ) } ) = ( 𝑆 ↾ suc ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑆 ‘ 𝑥 ) } ) ∨ ( 𝑆 ↾ suc ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑆 ‘ 𝑥 ) } ) <s ( 𝑈 ↾ suc ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑆 ‘ 𝑥 ) } ) ) )
49 44 46 48 syl2anc ⊢ ( ( 𝑈 ≠ 𝑆 ∧ ( ( 𝑈 ∈ No ∧ 𝑆 ∈ No ) ∧ ∀ 𝑔 ∈ ( dom 𝑈 ∪ dom 𝑆 ) ¬ ( 𝑆 ↾ suc 𝑔 ) <s ( 𝑈 ↾ suc 𝑔 ) ) ) → ( ( 𝑈 ↾ suc ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑆 ‘ 𝑥 ) } ) <s ( 𝑆 ↾ suc ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑆 ‘ 𝑥 ) } ) ∨ ( 𝑈 ↾ suc ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑆 ‘ 𝑥 ) } ) = ( 𝑆 ↾ suc ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑆 ‘ 𝑥 ) } ) ∨ ( 𝑆 ↾ suc ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑆 ‘ 𝑥 ) } ) <s ( 𝑈 ↾ suc ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑆 ‘ 𝑥 ) } ) ) )
50 30 40 49 ecase23d ⊢ ( ( 𝑈 ≠ 𝑆 ∧ ( ( 𝑈 ∈ No ∧ 𝑆 ∈ No ) ∧ ∀ 𝑔 ∈ ( dom 𝑈 ∪ dom 𝑆 ) ¬ ( 𝑆 ↾ suc 𝑔 ) <s ( 𝑈 ↾ suc 𝑔 ) ) ) → ( 𝑈 ↾ suc ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑆 ‘ 𝑥 ) } ) <s ( 𝑆 ↾ suc ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑆 ‘ 𝑥 ) } ) )
51 ltsres ⊢ ( ( 𝑈 ∈ No ∧ 𝑆 ∈ No ∧ suc ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑆 ‘ 𝑥 ) } ∈ On ) → ( ( 𝑈 ↾ suc ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑆 ‘ 𝑥 ) } ) <s ( 𝑆 ↾ suc ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑆 ‘ 𝑥 ) } ) → 𝑈 <s 𝑆 ) )
52 16 17 42 51 syl3anc ⊢ ( ( 𝑈 ≠ 𝑆 ∧ ( ( 𝑈 ∈ No ∧ 𝑆 ∈ No ) ∧ ∀ 𝑔 ∈ ( dom 𝑈 ∪ dom 𝑆 ) ¬ ( 𝑆 ↾ suc 𝑔 ) <s ( 𝑈 ↾ suc 𝑔 ) ) ) → ( ( 𝑈 ↾ suc ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑆 ‘ 𝑥 ) } ) <s ( 𝑆 ↾ suc ∩ { 𝑥 ∈ On ∣ ( 𝑈 ‘ 𝑥 ) ≠ ( 𝑆 ‘ 𝑥 ) } ) → 𝑈 <s 𝑆 ) )
53 50 52 mpd ⊢ ( ( 𝑈 ≠ 𝑆 ∧ ( ( 𝑈 ∈ No ∧ 𝑆 ∈ No ) ∧ ∀ 𝑔 ∈ ( dom 𝑈 ∪ dom 𝑆 ) ¬ ( 𝑆 ↾ suc 𝑔 ) <s ( 𝑈 ↾ suc 𝑔 ) ) ) → 𝑈 <s 𝑆 )
54 soasym ⊢ ( ( <s Or No ∧ ( 𝑈 ∈ No ∧ 𝑆 ∈ No ) ) → ( 𝑈 <s 𝑆 → ¬ 𝑆 <s 𝑈 ) )
55 8 54 mpan ⊢ ( ( 𝑈 ∈ No ∧ 𝑆 ∈ No ) → ( 𝑈 <s 𝑆 → ¬ 𝑆 <s 𝑈 ) )
56 15 53 55 sylc ⊢ ( ( 𝑈 ≠ 𝑆 ∧ ( ( 𝑈 ∈ No ∧ 𝑆 ∈ No ) ∧ ∀ 𝑔 ∈ ( dom 𝑈 ∪ dom 𝑆 ) ¬ ( 𝑆 ↾ suc 𝑔 ) <s ( 𝑈 ↾ suc 𝑔 ) ) ) → ¬ 𝑆 <s 𝑈 )
57 56 ex ⊢ ( 𝑈 ≠ 𝑆 → ( ( ( 𝑈 ∈ No ∧ 𝑆 ∈ No ) ∧ ∀ 𝑔 ∈ ( dom 𝑈 ∪ dom 𝑆 ) ¬ ( 𝑆 ↾ suc 𝑔 ) <s ( 𝑈 ↾ suc 𝑔 ) ) → ¬ 𝑆 <s 𝑈 ) )
58 14 57 pm2.61ine ⊢ ( ( ( 𝑈 ∈ No ∧ 𝑆 ∈ No ) ∧ ∀ 𝑔 ∈ ( dom 𝑈 ∪ dom 𝑆 ) ¬ ( 𝑆 ↾ suc 𝑔 ) <s ( 𝑈 ↾ suc 𝑔 ) ) → ¬ 𝑆 <s 𝑈 )
59 4 58 sylan2 ⊢ ( ( ( 𝑈 ∈ No ∧ 𝑆 ∈ No ) ∧ ( dom 𝑈 ⊆ 𝐴 ∧ dom 𝑆 ⊆ 𝐴 ∧ ∀ 𝑔 ∈ 𝐴 ¬ ( 𝑆 ↾ suc 𝑔 ) <s ( 𝑈 ↾ suc 𝑔 ) ) ) → ¬ 𝑆 <s 𝑈 )