| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | unss 4190 | . . . 4
⊢ ((dom
𝑈 ⊆ 𝐴 ∧ dom 𝑆 ⊆ 𝐴) ↔ (dom 𝑈 ∪ dom 𝑆) ⊆ 𝐴) | 
| 2 |  | ssralv 4052 | . . . 4
⊢ ((dom
𝑈 ∪ dom 𝑆) ⊆ 𝐴 → (∀𝑔 ∈ 𝐴 ¬ (𝑆 ↾ suc 𝑔) <s (𝑈 ↾ suc 𝑔) → ∀𝑔 ∈ (dom 𝑈 ∪ dom 𝑆) ¬ (𝑆 ↾ suc 𝑔) <s (𝑈 ↾ suc 𝑔))) | 
| 3 | 1, 2 | sylbi 217 | . . 3
⊢ ((dom
𝑈 ⊆ 𝐴 ∧ dom 𝑆 ⊆ 𝐴) → (∀𝑔 ∈ 𝐴 ¬ (𝑆 ↾ suc 𝑔) <s (𝑈 ↾ suc 𝑔) → ∀𝑔 ∈ (dom 𝑈 ∪ dom 𝑆) ¬ (𝑆 ↾ suc 𝑔) <s (𝑈 ↾ suc 𝑔))) | 
| 4 | 3 | 3impia 1118 | . 2
⊢ ((dom
𝑈 ⊆ 𝐴 ∧ dom 𝑆 ⊆ 𝐴 ∧ ∀𝑔 ∈ 𝐴 ¬ (𝑆 ↾ suc 𝑔) <s (𝑈 ↾ suc 𝑔)) → ∀𝑔 ∈ (dom 𝑈 ∪ dom 𝑆) ¬ (𝑆 ↾ suc 𝑔) <s (𝑈 ↾ suc 𝑔)) | 
| 5 |  | breq1 5146 | . . . . . . . 8
⊢ (𝑈 = 𝑆 → (𝑈 <s 𝑈 ↔ 𝑆 <s 𝑈)) | 
| 6 | 5 | notbid 318 | . . . . . . 7
⊢ (𝑈 = 𝑆 → (¬ 𝑈 <s 𝑈 ↔ ¬ 𝑆 <s 𝑈)) | 
| 7 | 6 | biimpd 229 | . . . . . 6
⊢ (𝑈 = 𝑆 → (¬ 𝑈 <s 𝑈 → ¬ 𝑆 <s 𝑈)) | 
| 8 |  | sltso 27721 | . . . . . . . 8
⊢  <s Or
 No | 
| 9 |  | sonr 5616 | . . . . . . . 8
⊢ (( <s
Or  No  ∧ 𝑈 ∈  No )
→ ¬ 𝑈 <s 𝑈) | 
| 10 | 8, 9 | mpan 690 | . . . . . . 7
⊢ (𝑈 ∈ 
No  → ¬ 𝑈
<s 𝑈) | 
| 11 | 10 | adantr 480 | . . . . . 6
⊢ ((𝑈 ∈ 
No  ∧ 𝑆 ∈
 No ) → ¬ 𝑈 <s 𝑈) | 
| 12 | 7, 11 | impel 505 | . . . . 5
⊢ ((𝑈 = 𝑆 ∧ (𝑈 ∈  No 
∧ 𝑆 ∈  No )) → ¬ 𝑆 <s 𝑈) | 
| 13 | 12 | adantrr 717 | . . . 4
⊢ ((𝑈 = 𝑆 ∧ ((𝑈 ∈  No 
∧ 𝑆 ∈  No ) ∧ ∀𝑔 ∈ (dom 𝑈 ∪ dom 𝑆) ¬ (𝑆 ↾ suc 𝑔) <s (𝑈 ↾ suc 𝑔))) → ¬ 𝑆 <s 𝑈) | 
| 14 | 13 | ex 412 | . . 3
⊢ (𝑈 = 𝑆 → (((𝑈 ∈  No 
∧ 𝑆 ∈  No ) ∧ ∀𝑔 ∈ (dom 𝑈 ∪ dom 𝑆) ¬ (𝑆 ↾ suc 𝑔) <s (𝑈 ↾ suc 𝑔)) → ¬ 𝑆 <s 𝑈)) | 
| 15 |  | simprl 771 | . . . . 5
⊢ ((𝑈 ≠ 𝑆 ∧ ((𝑈 ∈  No 
∧ 𝑆 ∈  No ) ∧ ∀𝑔 ∈ (dom 𝑈 ∪ dom 𝑆) ¬ (𝑆 ↾ suc 𝑔) <s (𝑈 ↾ suc 𝑔))) → (𝑈 ∈  No 
∧ 𝑆 ∈  No )) | 
| 16 |  | simprll 779 | . . . . . . . . . . 11
⊢ ((𝑈 ≠ 𝑆 ∧ ((𝑈 ∈  No 
∧ 𝑆 ∈  No ) ∧ ∀𝑔 ∈ (dom 𝑈 ∪ dom 𝑆) ¬ (𝑆 ↾ suc 𝑔) <s (𝑈 ↾ suc 𝑔))) → 𝑈 ∈  No
) | 
| 17 |  | simprlr 780 | . . . . . . . . . . 11
⊢ ((𝑈 ≠ 𝑆 ∧ ((𝑈 ∈  No 
∧ 𝑆 ∈  No ) ∧ ∀𝑔 ∈ (dom 𝑈 ∪ dom 𝑆) ¬ (𝑆 ↾ suc 𝑔) <s (𝑈 ↾ suc 𝑔))) → 𝑆 ∈  No
) | 
| 18 |  | simpl 482 | . . . . . . . . . . 11
⊢ ((𝑈 ≠ 𝑆 ∧ ((𝑈 ∈  No 
∧ 𝑆 ∈  No ) ∧ ∀𝑔 ∈ (dom 𝑈 ∪ dom 𝑆) ¬ (𝑆 ↾ suc 𝑔) <s (𝑈 ↾ suc 𝑔))) → 𝑈 ≠ 𝑆) | 
| 19 |  | nosepne 27725 | . . . . . . . . . . 11
⊢ ((𝑈 ∈ 
No  ∧ 𝑆 ∈
 No  ∧ 𝑈 ≠ 𝑆) → (𝑈‘∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑆‘𝑥)}) ≠ (𝑆‘∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑆‘𝑥)})) | 
| 20 | 16, 17, 18, 19 | syl3anc 1373 | . . . . . . . . . 10
⊢ ((𝑈 ≠ 𝑆 ∧ ((𝑈 ∈  No 
∧ 𝑆 ∈  No ) ∧ ∀𝑔 ∈ (dom 𝑈 ∪ dom 𝑆) ¬ (𝑆 ↾ suc 𝑔) <s (𝑈 ↾ suc 𝑔))) → (𝑈‘∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑆‘𝑥)}) ≠ (𝑆‘∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑆‘𝑥)})) | 
| 21 |  | nosepon 27710 | . . . . . . . . . . . . 13
⊢ ((𝑈 ∈ 
No  ∧ 𝑆 ∈
 No  ∧ 𝑈 ≠ 𝑆) → ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑆‘𝑥)} ∈ On) | 
| 22 | 16, 17, 18, 21 | syl3anc 1373 | . . . . . . . . . . . 12
⊢ ((𝑈 ≠ 𝑆 ∧ ((𝑈 ∈  No 
∧ 𝑆 ∈  No ) ∧ ∀𝑔 ∈ (dom 𝑈 ∪ dom 𝑆) ¬ (𝑆 ↾ suc 𝑔) <s (𝑈 ↾ suc 𝑔))) → ∩
{𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑆‘𝑥)} ∈ On) | 
| 23 |  | sucidg 6465 | . . . . . . . . . . . 12
⊢ (∩ {𝑥
∈ On ∣ (𝑈‘𝑥) ≠ (𝑆‘𝑥)} ∈ On → ∩ {𝑥
∈ On ∣ (𝑈‘𝑥) ≠ (𝑆‘𝑥)} ∈ suc ∩
{𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑆‘𝑥)}) | 
| 24 | 22, 23 | syl 17 | . . . . . . . . . . 11
⊢ ((𝑈 ≠ 𝑆 ∧ ((𝑈 ∈  No 
∧ 𝑆 ∈  No ) ∧ ∀𝑔 ∈ (dom 𝑈 ∪ dom 𝑆) ¬ (𝑆 ↾ suc 𝑔) <s (𝑈 ↾ suc 𝑔))) → ∩
{𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑆‘𝑥)} ∈ suc ∩
{𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑆‘𝑥)}) | 
| 25 | 24 | fvresd 6926 | . . . . . . . . . 10
⊢ ((𝑈 ≠ 𝑆 ∧ ((𝑈 ∈  No 
∧ 𝑆 ∈  No ) ∧ ∀𝑔 ∈ (dom 𝑈 ∪ dom 𝑆) ¬ (𝑆 ↾ suc 𝑔) <s (𝑈 ↾ suc 𝑔))) → ((𝑈 ↾ suc ∩
{𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑆‘𝑥)})‘∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑆‘𝑥)}) = (𝑈‘∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑆‘𝑥)})) | 
| 26 | 24 | fvresd 6926 | . . . . . . . . . 10
⊢ ((𝑈 ≠ 𝑆 ∧ ((𝑈 ∈  No 
∧ 𝑆 ∈  No ) ∧ ∀𝑔 ∈ (dom 𝑈 ∪ dom 𝑆) ¬ (𝑆 ↾ suc 𝑔) <s (𝑈 ↾ suc 𝑔))) → ((𝑆 ↾ suc ∩
{𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑆‘𝑥)})‘∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑆‘𝑥)}) = (𝑆‘∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑆‘𝑥)})) | 
| 27 | 20, 25, 26 | 3netr4d 3018 | . . . . . . . . 9
⊢ ((𝑈 ≠ 𝑆 ∧ ((𝑈 ∈  No 
∧ 𝑆 ∈  No ) ∧ ∀𝑔 ∈ (dom 𝑈 ∪ dom 𝑆) ¬ (𝑆 ↾ suc 𝑔) <s (𝑈 ↾ suc 𝑔))) → ((𝑈 ↾ suc ∩
{𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑆‘𝑥)})‘∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑆‘𝑥)}) ≠ ((𝑆 ↾ suc ∩
{𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑆‘𝑥)})‘∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑆‘𝑥)})) | 
| 28 | 27 | neneqd 2945 | . . . . . . . 8
⊢ ((𝑈 ≠ 𝑆 ∧ ((𝑈 ∈  No 
∧ 𝑆 ∈  No ) ∧ ∀𝑔 ∈ (dom 𝑈 ∪ dom 𝑆) ¬ (𝑆 ↾ suc 𝑔) <s (𝑈 ↾ suc 𝑔))) → ¬ ((𝑈 ↾ suc ∩
{𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑆‘𝑥)})‘∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑆‘𝑥)}) = ((𝑆 ↾ suc ∩
{𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑆‘𝑥)})‘∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑆‘𝑥)})) | 
| 29 |  | fveq1 6905 | . . . . . . . 8
⊢ ((𝑈 ↾ suc ∩ {𝑥
∈ On ∣ (𝑈‘𝑥) ≠ (𝑆‘𝑥)}) = (𝑆 ↾ suc ∩
{𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑆‘𝑥)}) → ((𝑈 ↾ suc ∩
{𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑆‘𝑥)})‘∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑆‘𝑥)}) = ((𝑆 ↾ suc ∩
{𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑆‘𝑥)})‘∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑆‘𝑥)})) | 
| 30 | 28, 29 | nsyl 140 | . . . . . . 7
⊢ ((𝑈 ≠ 𝑆 ∧ ((𝑈 ∈  No 
∧ 𝑆 ∈  No ) ∧ ∀𝑔 ∈ (dom 𝑈 ∪ dom 𝑆) ¬ (𝑆 ↾ suc 𝑔) <s (𝑈 ↾ suc 𝑔))) → ¬ (𝑈 ↾ suc ∩
{𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑆‘𝑥)}) = (𝑆 ↾ suc ∩
{𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑆‘𝑥)})) | 
| 31 |  | nosepdm 27729 | . . . . . . . . 9
⊢ ((𝑈 ∈ 
No  ∧ 𝑆 ∈
 No  ∧ 𝑈 ≠ 𝑆) → ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑆‘𝑥)} ∈ (dom 𝑈 ∪ dom 𝑆)) | 
| 32 | 16, 17, 18, 31 | syl3anc 1373 | . . . . . . . 8
⊢ ((𝑈 ≠ 𝑆 ∧ ((𝑈 ∈  No 
∧ 𝑆 ∈  No ) ∧ ∀𝑔 ∈ (dom 𝑈 ∪ dom 𝑆) ¬ (𝑆 ↾ suc 𝑔) <s (𝑈 ↾ suc 𝑔))) → ∩
{𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑆‘𝑥)} ∈ (dom 𝑈 ∪ dom 𝑆)) | 
| 33 |  | simprr 773 | . . . . . . . 8
⊢ ((𝑈 ≠ 𝑆 ∧ ((𝑈 ∈  No 
∧ 𝑆 ∈  No ) ∧ ∀𝑔 ∈ (dom 𝑈 ∪ dom 𝑆) ¬ (𝑆 ↾ suc 𝑔) <s (𝑈 ↾ suc 𝑔))) → ∀𝑔 ∈ (dom 𝑈 ∪ dom 𝑆) ¬ (𝑆 ↾ suc 𝑔) <s (𝑈 ↾ suc 𝑔)) | 
| 34 |  | suceq 6450 | . . . . . . . . . . . 12
⊢ (𝑔 = ∩
{𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑆‘𝑥)} → suc 𝑔 = suc ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑆‘𝑥)}) | 
| 35 | 34 | reseq2d 5997 | . . . . . . . . . . 11
⊢ (𝑔 = ∩
{𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑆‘𝑥)} → (𝑆 ↾ suc 𝑔) = (𝑆 ↾ suc ∩
{𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑆‘𝑥)})) | 
| 36 | 34 | reseq2d 5997 | . . . . . . . . . . 11
⊢ (𝑔 = ∩
{𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑆‘𝑥)} → (𝑈 ↾ suc 𝑔) = (𝑈 ↾ suc ∩
{𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑆‘𝑥)})) | 
| 37 | 35, 36 | breq12d 5156 | . . . . . . . . . 10
⊢ (𝑔 = ∩
{𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑆‘𝑥)} → ((𝑆 ↾ suc 𝑔) <s (𝑈 ↾ suc 𝑔) ↔ (𝑆 ↾ suc ∩
{𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑆‘𝑥)}) <s (𝑈 ↾ suc ∩
{𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑆‘𝑥)}))) | 
| 38 | 37 | notbid 318 | . . . . . . . . 9
⊢ (𝑔 = ∩
{𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑆‘𝑥)} → (¬ (𝑆 ↾ suc 𝑔) <s (𝑈 ↾ suc 𝑔) ↔ ¬ (𝑆 ↾ suc ∩
{𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑆‘𝑥)}) <s (𝑈 ↾ suc ∩
{𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑆‘𝑥)}))) | 
| 39 | 38 | rspcv 3618 | . . . . . . . 8
⊢ (∩ {𝑥
∈ On ∣ (𝑈‘𝑥) ≠ (𝑆‘𝑥)} ∈ (dom 𝑈 ∪ dom 𝑆) → (∀𝑔 ∈ (dom 𝑈 ∪ dom 𝑆) ¬ (𝑆 ↾ suc 𝑔) <s (𝑈 ↾ suc 𝑔) → ¬ (𝑆 ↾ suc ∩
{𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑆‘𝑥)}) <s (𝑈 ↾ suc ∩
{𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑆‘𝑥)}))) | 
| 40 | 32, 33, 39 | sylc 65 | . . . . . . 7
⊢ ((𝑈 ≠ 𝑆 ∧ ((𝑈 ∈  No 
∧ 𝑆 ∈  No ) ∧ ∀𝑔 ∈ (dom 𝑈 ∪ dom 𝑆) ¬ (𝑆 ↾ suc 𝑔) <s (𝑈 ↾ suc 𝑔))) → ¬ (𝑆 ↾ suc ∩
{𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑆‘𝑥)}) <s (𝑈 ↾ suc ∩
{𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑆‘𝑥)})) | 
| 41 |  | onsuc 7831 | . . . . . . . . . 10
⊢ (∩ {𝑥
∈ On ∣ (𝑈‘𝑥) ≠ (𝑆‘𝑥)} ∈ On → suc ∩ {𝑥
∈ On ∣ (𝑈‘𝑥) ≠ (𝑆‘𝑥)} ∈ On) | 
| 42 | 22, 41 | syl 17 | . . . . . . . . 9
⊢ ((𝑈 ≠ 𝑆 ∧ ((𝑈 ∈  No 
∧ 𝑆 ∈  No ) ∧ ∀𝑔 ∈ (dom 𝑈 ∪ dom 𝑆) ¬ (𝑆 ↾ suc 𝑔) <s (𝑈 ↾ suc 𝑔))) → suc ∩
{𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑆‘𝑥)} ∈ On) | 
| 43 |  | noreson 27705 | . . . . . . . . 9
⊢ ((𝑈 ∈ 
No  ∧ suc ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑆‘𝑥)} ∈ On) → (𝑈 ↾ suc ∩
{𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑆‘𝑥)}) ∈  No
) | 
| 44 | 16, 42, 43 | syl2anc 584 | . . . . . . . 8
⊢ ((𝑈 ≠ 𝑆 ∧ ((𝑈 ∈  No 
∧ 𝑆 ∈  No ) ∧ ∀𝑔 ∈ (dom 𝑈 ∪ dom 𝑆) ¬ (𝑆 ↾ suc 𝑔) <s (𝑈 ↾ suc 𝑔))) → (𝑈 ↾ suc ∩
{𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑆‘𝑥)}) ∈  No
) | 
| 45 |  | noreson 27705 | . . . . . . . . 9
⊢ ((𝑆 ∈ 
No  ∧ suc ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑆‘𝑥)} ∈ On) → (𝑆 ↾ suc ∩
{𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑆‘𝑥)}) ∈  No
) | 
| 46 | 17, 42, 45 | syl2anc 584 | . . . . . . . 8
⊢ ((𝑈 ≠ 𝑆 ∧ ((𝑈 ∈  No 
∧ 𝑆 ∈  No ) ∧ ∀𝑔 ∈ (dom 𝑈 ∪ dom 𝑆) ¬ (𝑆 ↾ suc 𝑔) <s (𝑈 ↾ suc 𝑔))) → (𝑆 ↾ suc ∩
{𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑆‘𝑥)}) ∈  No
) | 
| 47 |  | solin 5619 | . . . . . . . . 9
⊢ (( <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 690 | . . . . . . . 8
⊢ (((𝑈 ↾ 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 584 | . . . . . . 7
⊢ ((𝑈 ≠ 𝑆 ∧ ((𝑈 ∈  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 1475 | . . . . . 6
⊢ ((𝑈 ≠ 𝑆 ∧ ((𝑈 ∈  No 
∧ 𝑆 ∈  No ) ∧ ∀𝑔 ∈ (dom 𝑈 ∪ dom 𝑆) ¬ (𝑆 ↾ suc 𝑔) <s (𝑈 ↾ suc 𝑔))) → (𝑈 ↾ suc ∩
{𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑆‘𝑥)}) <s (𝑆 ↾ suc ∩
{𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑆‘𝑥)})) | 
| 51 |  | sltres 27707 | . . . . . . 7
⊢ ((𝑈 ∈ 
No  ∧ 𝑆 ∈
 No  ∧ suc ∩ {𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑆‘𝑥)} ∈ On) → ((𝑈 ↾ suc ∩
{𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑆‘𝑥)}) <s (𝑆 ↾ suc ∩
{𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑆‘𝑥)}) → 𝑈 <s 𝑆)) | 
| 52 | 16, 17, 42, 51 | syl3anc 1373 | . . . . . 6
⊢ ((𝑈 ≠ 𝑆 ∧ ((𝑈 ∈  No 
∧ 𝑆 ∈  No ) ∧ ∀𝑔 ∈ (dom 𝑈 ∪ dom 𝑆) ¬ (𝑆 ↾ suc 𝑔) <s (𝑈 ↾ suc 𝑔))) → ((𝑈 ↾ suc ∩
{𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑆‘𝑥)}) <s (𝑆 ↾ suc ∩
{𝑥 ∈ On ∣ (𝑈‘𝑥) ≠ (𝑆‘𝑥)}) → 𝑈 <s 𝑆)) | 
| 53 | 50, 52 | mpd 15 | . . . . 5
⊢ ((𝑈 ≠ 𝑆 ∧ ((𝑈 ∈  No 
∧ 𝑆 ∈  No ) ∧ ∀𝑔 ∈ (dom 𝑈 ∪ dom 𝑆) ¬ (𝑆 ↾ suc 𝑔) <s (𝑈 ↾ suc 𝑔))) → 𝑈 <s 𝑆) | 
| 54 |  | soasym 5625 | . . . . . 6
⊢ (( <s
Or  No  ∧ (𝑈 ∈  No 
∧ 𝑆 ∈  No )) → (𝑈 <s 𝑆 → ¬ 𝑆 <s 𝑈)) | 
| 55 | 8, 54 | mpan 690 | . . . . 5
⊢ ((𝑈 ∈ 
No  ∧ 𝑆 ∈
 No ) → (𝑈 <s 𝑆 → ¬ 𝑆 <s 𝑈)) | 
| 56 | 15, 53, 55 | sylc 65 | . . . 4
⊢ ((𝑈 ≠ 𝑆 ∧ ((𝑈 ∈  No 
∧ 𝑆 ∈  No ) ∧ ∀𝑔 ∈ (dom 𝑈 ∪ dom 𝑆) ¬ (𝑆 ↾ suc 𝑔) <s (𝑈 ↾ suc 𝑔))) → ¬ 𝑆 <s 𝑈) | 
| 57 | 56 | ex 412 | . . 3
⊢ (𝑈 ≠ 𝑆 → (((𝑈 ∈  No 
∧ 𝑆 ∈  No ) ∧ ∀𝑔 ∈ (dom 𝑈 ∪ dom 𝑆) ¬ (𝑆 ↾ suc 𝑔) <s (𝑈 ↾ suc 𝑔)) → ¬ 𝑆 <s 𝑈)) | 
| 58 | 14, 57 | pm2.61ine 3025 | . 2
⊢ (((𝑈 ∈ 
No  ∧ 𝑆 ∈
 No ) ∧ ∀𝑔 ∈ (dom 𝑈 ∪ dom 𝑆) ¬ (𝑆 ↾ suc 𝑔) <s (𝑈 ↾ suc 𝑔)) → ¬ 𝑆 <s 𝑈) | 
| 59 | 4, 58 | sylan2 593 | 1
⊢ (((𝑈 ∈ 
No  ∧ 𝑆 ∈
 No ) ∧ (dom 𝑈 ⊆ 𝐴 ∧ dom 𝑆 ⊆ 𝐴 ∧ ∀𝑔 ∈ 𝐴 ¬ (𝑆 ↾ suc 𝑔) <s (𝑈 ↾ suc 𝑔))) → ¬ 𝑆 <s 𝑈) |