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

Theorem noinfbnd2 33519
 Description: Bounding law from below for the surreal infimum. Analagous to proposition 4.3 of [Lipparini] p. 6. (Contributed by Scott Fenton, 9-Aug-2024.)
Hypothesis
Ref Expression
noinfbnd2.1 𝑇 = if(∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥, ((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))))
Assertion
Ref Expression
noinfbnd2 ((𝐵 No 𝐵𝑉𝑍 No ) → (∀𝑏𝐵 𝑍 <s 𝑏 ↔ ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)))
Distinct variable groups:   𝐵,𝑏,𝑔   𝑢,𝐵   𝑣,𝑏,𝐵,𝑥,𝑦   𝑢,𝑔,𝑣,𝑥,𝑦   𝑇,𝑏,𝑔   𝑣,𝑢,𝑥,𝑦   𝑉,𝑏,𝑔   𝑥,𝑣   𝑥,𝑉   𝑦,𝑣,𝑥   𝑍,𝑏,𝑔,𝑥
Allowed substitution hints:   𝑇(𝑥,𝑦,𝑣,𝑢)   𝑉(𝑦,𝑣,𝑢)   𝑍(𝑦,𝑣,𝑢)

Proof of Theorem noinfbnd2
Dummy variables 𝑝 𝑞 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nfv 1915 . . . . . 6 𝑥((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)
2 noinfbnd2.1 . . . . . . . . 9 𝑇 = if(∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥, ((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))))
3 nfre1 3230 . . . . . . . . . 10 𝑥𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥
4 nfriota1 7115 . . . . . . . . . . 11 𝑥(𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)
54nfdm 5792 . . . . . . . . . . . . 13 𝑥dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)
6 nfcv 2919 . . . . . . . . . . . . 13 𝑥1o
75, 6nfop 4779 . . . . . . . . . . . 12 𝑥⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o
87nfsn 4600 . . . . . . . . . . 11 𝑥{⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩}
94, 8nfun 4070 . . . . . . . . . 10 𝑥((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩})
10 nfcv 2919 . . . . . . . . . . 11 𝑥{𝑦 ∣ ∃𝑢𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))}
11 nfiota1 6296 . . . . . . . . . . 11 𝑥(℩𝑥𝑢𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))
1210, 11nfmpt 5129 . . . . . . . . . 10 𝑥(𝑔 ∈ {𝑦 ∣ ∃𝑢𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥)))
133, 9, 12nfif 4450 . . . . . . . . 9 𝑥if(∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥, ((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))))
142, 13nfcxfr 2917 . . . . . . . 8 𝑥𝑇
15 nfcv 2919 . . . . . . . 8 𝑥 <s
16 nfcv 2919 . . . . . . . . 9 𝑥𝑍
1714nfdm 5792 . . . . . . . . 9 𝑥dom 𝑇
1816, 17nfres 5825 . . . . . . . 8 𝑥(𝑍 ↾ dom 𝑇)
1914, 15, 18nfbr 5079 . . . . . . 7 𝑥 𝑇 <s (𝑍 ↾ dom 𝑇)
2019nfn 1858 . . . . . 6 𝑥 ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)
211, 20nfim 1897 . . . . 5 𝑥(((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) → ¬ 𝑇 <s (𝑍 ↾ dom 𝑇))
22 noinfbnd2lem1 33518 . . . . . . . 8 (((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) → ¬ (𝑥 ∪ {⟨dom 𝑥, 1o⟩}) <s (𝑍 ↾ suc dom 𝑥))
23223expb 1117 . . . . . . 7 (((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → ¬ (𝑥 ∪ {⟨dom 𝑥, 1o⟩}) <s (𝑍 ↾ suc dom 𝑥))
24 rspe 3228 . . . . . . . . . . . 12 ((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) → ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)
2524adantr 484 . . . . . . . . . . 11 (((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)
2625iftrued 4428 . . . . . . . . . 10 (((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → if(∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥, ((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥)))) = ((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩}))
27 simpl 486 . . . . . . . . . . . 12 (((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → (𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥))
28 simprl1 1215 . . . . . . . . . . . . . . 15 (((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → 𝐵 No )
29 nominmo 33487 . . . . . . . . . . . . . . 15 (𝐵 No → ∃*𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)
3028, 29syl 17 . . . . . . . . . . . . . 14 (((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → ∃*𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)
31 reu5 3340 . . . . . . . . . . . . . 14 (∃!𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ↔ (∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ∃*𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥))
3225, 30, 31sylanbrc 586 . . . . . . . . . . . . 13 (((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → ∃!𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)
33 riota1 7129 . . . . . . . . . . . . 13 (∃!𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 → ((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) ↔ (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) = 𝑥))
3432, 33syl 17 . . . . . . . . . . . 12 (((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → ((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) ↔ (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) = 𝑥))
3527, 34mpbid 235 . . . . . . . . . . 11 (((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) = 𝑥)
3635dmeqd 5745 . . . . . . . . . . . . 13 (((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) = dom 𝑥)
3736opeq1d 4769 . . . . . . . . . . . 12 (((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → ⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩ = ⟨dom 𝑥, 1o⟩)
3837sneqd 4534 . . . . . . . . . . 11 (((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → {⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩} = {⟨dom 𝑥, 1o⟩})
3935, 38uneq12d 4069 . . . . . . . . . 10 (((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → ((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩}) = (𝑥 ∪ {⟨dom 𝑥, 1o⟩}))
4026, 39eqtrd 2793 . . . . . . . . 9 (((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → if(∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥, ((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥)))) = (𝑥 ∪ {⟨dom 𝑥, 1o⟩}))
412, 40syl5eq 2805 . . . . . . . 8 (((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → 𝑇 = (𝑥 ∪ {⟨dom 𝑥, 1o⟩}))
4241dmeqd 5745 . . . . . . . . . 10 (((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → dom 𝑇 = dom (𝑥 ∪ {⟨dom 𝑥, 1o⟩}))
43 1oex 8120 . . . . . . . . . . . . 13 1o ∈ V
4443dmsnop 6045 . . . . . . . . . . . 12 dom {⟨dom 𝑥, 1o⟩} = {dom 𝑥}
4544uneq2i 4065 . . . . . . . . . . 11 (dom 𝑥 ∪ dom {⟨dom 𝑥, 1o⟩}) = (dom 𝑥 ∪ {dom 𝑥})
46 dmun 5750 . . . . . . . . . . 11 dom (𝑥 ∪ {⟨dom 𝑥, 1o⟩}) = (dom 𝑥 ∪ dom {⟨dom 𝑥, 1o⟩})
47 df-suc 6175 . . . . . . . . . . 11 suc dom 𝑥 = (dom 𝑥 ∪ {dom 𝑥})
4845, 46, 473eqtr4ri 2792 . . . . . . . . . 10 suc dom 𝑥 = dom (𝑥 ∪ {⟨dom 𝑥, 1o⟩})
4942, 48eqtr4di 2811 . . . . . . . . 9 (((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → dom 𝑇 = suc dom 𝑥)
5049reseq2d 5823 . . . . . . . 8 (((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → (𝑍 ↾ dom 𝑇) = (𝑍 ↾ suc dom 𝑥))
5141, 50breq12d 5045 . . . . . . 7 (((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → (𝑇 <s (𝑍 ↾ dom 𝑇) ↔ (𝑥 ∪ {⟨dom 𝑥, 1o⟩}) <s (𝑍 ↾ suc dom 𝑥)))
5223, 51mtbird 328 . . . . . 6 (((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → ¬ 𝑇 <s (𝑍 ↾ dom 𝑇))
5352exp31 423 . . . . 5 (𝑥𝐵 → (∀𝑦𝐵 ¬ 𝑦 <s 𝑥 → (((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) → ¬ 𝑇 <s (𝑍 ↾ dom 𝑇))))
5421, 53rexlimi 3239 . . . 4 (∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 → (((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) → ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)))
5554imp 410 . . 3 ((∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → ¬ 𝑇 <s (𝑍 ↾ dom 𝑇))
56 simprl3 1217 . . . . . 6 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → 𝑍 No )
572noinfno 33506 . . . . . . . . 9 ((𝐵 No 𝐵𝑉) → 𝑇 No )
58573adant3 1129 . . . . . . . 8 ((𝐵 No 𝐵𝑉𝑍 No ) → 𝑇 No )
5958ad2antrl 727 . . . . . . 7 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → 𝑇 No )
60 nodmon 33438 . . . . . . 7 (𝑇 No → dom 𝑇 ∈ On)
6159, 60syl 17 . . . . . 6 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → dom 𝑇 ∈ On)
62 noreson 33448 . . . . . 6 ((𝑍 No ∧ dom 𝑇 ∈ On) → (𝑍 ↾ dom 𝑇) ∈ No )
6356, 61, 62syl2anc 587 . . . . 5 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → (𝑍 ↾ dom 𝑇) ∈ No )
64 nofun 33437 . . . . . . . . 9 (𝑇 No → Fun 𝑇)
65 funrel 6352 . . . . . . . . 9 (Fun 𝑇 → Rel 𝑇)
6658, 64, 653syl 18 . . . . . . . 8 ((𝐵 No 𝐵𝑉𝑍 No ) → Rel 𝑇)
6766ad2antrl 727 . . . . . . 7 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → Rel 𝑇)
68 resdm 5868 . . . . . . 7 (Rel 𝑇 → (𝑇 ↾ dom 𝑇) = 𝑇)
6967, 68syl 17 . . . . . 6 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → (𝑇 ↾ dom 𝑇) = 𝑇)
7069, 59eqeltrd 2852 . . . . 5 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → (𝑇 ↾ dom 𝑇) ∈ No )
71 resdmss 6064 . . . . . 6 dom (𝑍 ↾ dom 𝑇) ⊆ dom 𝑇
7271a1i 11 . . . . 5 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → dom (𝑍 ↾ dom 𝑇) ⊆ dom 𝑇)
73 resdmss 6064 . . . . . 6 dom (𝑇 ↾ dom 𝑇) ⊆ dom 𝑇
7473a1i 11 . . . . 5 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → dom (𝑇 ↾ dom 𝑇) ⊆ dom 𝑇)
752noinfdm 33507 . . . . . . . . . . 11 (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 → dom 𝑇 = {𝑔 ∣ ∃𝑝𝐵 (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐵𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔)))})
7675abeq2d 2886 . . . . . . . . . 10 (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 → (𝑔 ∈ dom 𝑇 ↔ ∃𝑝𝐵 (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐵𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔)))))
7776adantr 484 . . . . . . . . 9 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → (𝑔 ∈ dom 𝑇 ↔ ∃𝑝𝐵 (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐵𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔)))))
78 simpll 766 . . . . . . . . . . . 12 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) ∧ (𝑝𝐵 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐵𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → ¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)
79 simprl1 1215 . . . . . . . . . . . . 13 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → 𝐵 No )
8079adantr 484 . . . . . . . . . . . 12 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) ∧ (𝑝𝐵 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐵𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → 𝐵 No )
81 simprl2 1216 . . . . . . . . . . . . 13 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → 𝐵𝑉)
8281adantr 484 . . . . . . . . . . . 12 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) ∧ (𝑝𝐵 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐵𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → 𝐵𝑉)
83 simprl 770 . . . . . . . . . . . 12 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) ∧ (𝑝𝐵 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐵𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → 𝑝𝐵)
84 simprrl 780 . . . . . . . . . . . 12 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) ∧ (𝑝𝐵 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐵𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → 𝑔 ∈ dom 𝑝)
85 simprrr 781 . . . . . . . . . . . . 13 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) ∧ (𝑝𝐵 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐵𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → ∀𝑞𝐵𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔)))
86 breq2 5036 . . . . . . . . . . . . . . . 16 (𝑞 = 𝑣 → (𝑝 <s 𝑞𝑝 <s 𝑣))
8786notbid 321 . . . . . . . . . . . . . . 15 (𝑞 = 𝑣 → (¬ 𝑝 <s 𝑞 ↔ ¬ 𝑝 <s 𝑣))
88 reseq1 5817 . . . . . . . . . . . . . . . 16 (𝑞 = 𝑣 → (𝑞 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔))
8988eqeq2d 2769 . . . . . . . . . . . . . . 15 (𝑞 = 𝑣 → ((𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔) ↔ (𝑝 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)))
9087, 89imbi12d 348 . . . . . . . . . . . . . 14 (𝑞 = 𝑣 → ((¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔)) ↔ (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔))))
9190cbvralvw 3361 . . . . . . . . . . . . 13 (∀𝑞𝐵𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔)) ↔ ∀𝑣𝐵𝑝 <s 𝑣 → (𝑝 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)))
9285, 91sylib 221 . . . . . . . . . . . 12 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) ∧ (𝑝𝐵 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐵𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → ∀𝑣𝐵𝑝 <s 𝑣 → (𝑝 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)))
932noinfres 33510 . . . . . . . . . . . 12 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑝𝐵𝑔 ∈ dom 𝑝 ∧ ∀𝑣𝐵𝑝 <s 𝑣 → (𝑝 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)))) → (𝑇 ↾ suc 𝑔) = (𝑝 ↾ suc 𝑔))
9478, 80, 82, 83, 84, 92, 93syl123anc 1384 . . . . . . . . . . 11 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) ∧ (𝑝𝐵 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐵𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → (𝑇 ↾ suc 𝑔) = (𝑝 ↾ suc 𝑔))
95 breq2 5036 . . . . . . . . . . . . . 14 (𝑏 = 𝑝 → (𝑍 <s 𝑏𝑍 <s 𝑝))
96 simplrr 777 . . . . . . . . . . . . . 14 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) ∧ (𝑝𝐵 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐵𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → ∀𝑏𝐵 𝑍 <s 𝑏)
9795, 96, 83rspcdva 3543 . . . . . . . . . . . . 13 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) ∧ (𝑝𝐵 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐵𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → 𝑍 <s 𝑝)
9856adantr 484 . . . . . . . . . . . . . 14 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) ∧ (𝑝𝐵 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐵𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → 𝑍 No )
9980, 83sseldd 3893 . . . . . . . . . . . . . 14 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) ∧ (𝑝𝐵 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐵𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → 𝑝 No )
100 sltso 33464 . . . . . . . . . . . . . . 15 <s Or No
101 soasym 5473 . . . . . . . . . . . . . . 15 (( <s Or No ∧ (𝑍 No 𝑝 No )) → (𝑍 <s 𝑝 → ¬ 𝑝 <s 𝑍))
102100, 101mpan 689 . . . . . . . . . . . . . 14 ((𝑍 No 𝑝 No ) → (𝑍 <s 𝑝 → ¬ 𝑝 <s 𝑍))
10398, 99, 102syl2anc 587 . . . . . . . . . . . . 13 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) ∧ (𝑝𝐵 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐵𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → (𝑍 <s 𝑝 → ¬ 𝑝 <s 𝑍))
10497, 103mpd 15 . . . . . . . . . . . 12 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) ∧ (𝑝𝐵 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐵𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → ¬ 𝑝 <s 𝑍)
105 nodmon 33438 . . . . . . . . . . . . . . . 16 (𝑝 No → dom 𝑝 ∈ On)
10699, 105syl 17 . . . . . . . . . . . . . . 15 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) ∧ (𝑝𝐵 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐵𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → dom 𝑝 ∈ On)
107 onelon 6194 . . . . . . . . . . . . . . 15 ((dom 𝑝 ∈ On ∧ 𝑔 ∈ dom 𝑝) → 𝑔 ∈ On)
108106, 84, 107syl2anc 587 . . . . . . . . . . . . . 14 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) ∧ (𝑝𝐵 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐵𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → 𝑔 ∈ On)
109 sucelon 7531 . . . . . . . . . . . . . 14 (𝑔 ∈ On ↔ suc 𝑔 ∈ On)
110108, 109sylib 221 . . . . . . . . . . . . 13 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) ∧ (𝑝𝐵 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐵𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → suc 𝑔 ∈ On)
111 sltres 33450 . . . . . . . . . . . . 13 ((𝑝 No 𝑍 No ∧ suc 𝑔 ∈ On) → ((𝑝 ↾ suc 𝑔) <s (𝑍 ↾ suc 𝑔) → 𝑝 <s 𝑍))
11299, 98, 110, 111syl3anc 1368 . . . . . . . . . . . 12 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) ∧ (𝑝𝐵 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐵𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → ((𝑝 ↾ suc 𝑔) <s (𝑍 ↾ suc 𝑔) → 𝑝 <s 𝑍))
113104, 112mtod 201 . . . . . . . . . . 11 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) ∧ (𝑝𝐵 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐵𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → ¬ (𝑝 ↾ suc 𝑔) <s (𝑍 ↾ suc 𝑔))
11494, 113eqnbrtrd 5050 . . . . . . . . . 10 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) ∧ (𝑝𝐵 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐵𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → ¬ (𝑇 ↾ suc 𝑔) <s (𝑍 ↾ suc 𝑔))
115114rexlimdvaa 3209 . . . . . . . . 9 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → (∃𝑝𝐵 (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐵𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))) → ¬ (𝑇 ↾ suc 𝑔) <s (𝑍 ↾ suc 𝑔)))
11677, 115sylbid 243 . . . . . . . 8 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → (𝑔 ∈ dom 𝑇 → ¬ (𝑇 ↾ suc 𝑔) <s (𝑍 ↾ suc 𝑔)))
117116imp 410 . . . . . . 7 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) ∧ 𝑔 ∈ dom 𝑇) → ¬ (𝑇 ↾ suc 𝑔) <s (𝑍 ↾ suc 𝑔))
118 nodmord 33441 . . . . . . . . . . 11 (𝑇 No → Ord dom 𝑇)
119 ordsucss 7532 . . . . . . . . . . 11 (Ord dom 𝑇 → (𝑔 ∈ dom 𝑇 → suc 𝑔 ⊆ dom 𝑇))
12059, 118, 1193syl 18 . . . . . . . . . 10 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → (𝑔 ∈ dom 𝑇 → suc 𝑔 ⊆ dom 𝑇))
121120imp 410 . . . . . . . . 9 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) ∧ 𝑔 ∈ dom 𝑇) → suc 𝑔 ⊆ dom 𝑇)
122121resabs1d 5854 . . . . . . . 8 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) ∧ 𝑔 ∈ dom 𝑇) → ((𝑇 ↾ dom 𝑇) ↾ suc 𝑔) = (𝑇 ↾ suc 𝑔))
123121resabs1d 5854 . . . . . . . 8 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) ∧ 𝑔 ∈ dom 𝑇) → ((𝑍 ↾ dom 𝑇) ↾ suc 𝑔) = (𝑍 ↾ suc 𝑔))
124122, 123breq12d 5045 . . . . . . 7 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) ∧ 𝑔 ∈ dom 𝑇) → (((𝑇 ↾ dom 𝑇) ↾ suc 𝑔) <s ((𝑍 ↾ dom 𝑇) ↾ suc 𝑔) ↔ (𝑇 ↾ suc 𝑔) <s (𝑍 ↾ suc 𝑔)))
125117, 124mtbird 328 . . . . . 6 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) ∧ 𝑔 ∈ dom 𝑇) → ¬ ((𝑇 ↾ dom 𝑇) ↾ suc 𝑔) <s ((𝑍 ↾ dom 𝑇) ↾ suc 𝑔))
126125ralrimiva 3113 . . . . 5 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → ∀𝑔 ∈ dom 𝑇 ¬ ((𝑇 ↾ dom 𝑇) ↾ suc 𝑔) <s ((𝑍 ↾ dom 𝑇) ↾ suc 𝑔))
127 noresle 33485 . . . . 5 ((((𝑍 ↾ dom 𝑇) ∈ No ∧ (𝑇 ↾ dom 𝑇) ∈ No ) ∧ (dom (𝑍 ↾ dom 𝑇) ⊆ dom 𝑇 ∧ dom (𝑇 ↾ dom 𝑇) ⊆ dom 𝑇 ∧ ∀𝑔 ∈ dom 𝑇 ¬ ((𝑇 ↾ dom 𝑇) ↾ suc 𝑔) <s ((𝑍 ↾ dom 𝑇) ↾ suc 𝑔))) → ¬ (𝑇 ↾ dom 𝑇) <s (𝑍 ↾ dom 𝑇))
12863, 70, 72, 74, 126, 127syl23anc 1374 . . . 4 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → ¬ (𝑇 ↾ dom 𝑇) <s (𝑍 ↾ dom 𝑇))
12969breq1d 5042 . . . 4 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → ((𝑇 ↾ dom 𝑇) <s (𝑍 ↾ dom 𝑇) ↔ 𝑇 <s (𝑍 ↾ dom 𝑇)))
130128, 129mtbid 327 . . 3 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → ¬ 𝑇 <s (𝑍 ↾ dom 𝑇))
13155, 130pm2.61ian 811 . 2 (((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) → ¬ 𝑇 <s (𝑍 ↾ dom 𝑇))
132 simplr 768 . . . . 5 ((((𝐵 No 𝐵𝑉𝑍 No ) ∧ ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)) ∧ 𝑏𝐵) → ¬ 𝑇 <s (𝑍 ↾ dom 𝑇))
133 simpll1 1209 . . . . . 6 ((((𝐵 No 𝐵𝑉𝑍 No ) ∧ ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)) ∧ 𝑏𝐵) → 𝐵 No )
134 simpll2 1210 . . . . . 6 ((((𝐵 No 𝐵𝑉𝑍 No ) ∧ ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)) ∧ 𝑏𝐵) → 𝐵𝑉)
135 simpr 488 . . . . . 6 ((((𝐵 No 𝐵𝑉𝑍 No ) ∧ ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)) ∧ 𝑏𝐵) → 𝑏𝐵)
1362noinfbnd1 33517 . . . . . 6 ((𝐵 No 𝐵𝑉𝑏𝐵) → 𝑇 <s (𝑏 ↾ dom 𝑇))
137133, 134, 135, 136syl3anc 1368 . . . . 5 ((((𝐵 No 𝐵𝑉𝑍 No ) ∧ ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)) ∧ 𝑏𝐵) → 𝑇 <s (𝑏 ↾ dom 𝑇))
138 simpl3 1190 . . . . . . . 8 (((𝐵 No 𝐵𝑉𝑍 No ) ∧ ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)) → 𝑍 No )
139 simpl1 1188 . . . . . . . . . 10 (((𝐵 No 𝐵𝑉𝑍 No ) ∧ ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)) → 𝐵 No )
140 simpl2 1189 . . . . . . . . . 10 (((𝐵 No 𝐵𝑉𝑍 No ) ∧ ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)) → 𝐵𝑉)
141139, 140, 57syl2anc 587 . . . . . . . . 9 (((𝐵 No 𝐵𝑉𝑍 No ) ∧ ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)) → 𝑇 No )
142141, 60syl 17 . . . . . . . 8 (((𝐵 No 𝐵𝑉𝑍 No ) ∧ ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)) → dom 𝑇 ∈ On)
143138, 142, 62syl2anc 587 . . . . . . 7 (((𝐵 No 𝐵𝑉𝑍 No ) ∧ ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)) → (𝑍 ↾ dom 𝑇) ∈ No )
144143adantr 484 . . . . . 6 ((((𝐵 No 𝐵𝑉𝑍 No ) ∧ ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)) ∧ 𝑏𝐵) → (𝑍 ↾ dom 𝑇) ∈ No )
145141adantr 484 . . . . . 6 ((((𝐵 No 𝐵𝑉𝑍 No ) ∧ ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)) ∧ 𝑏𝐵) → 𝑇 No )
146139sselda 3892 . . . . . . 7 ((((𝐵 No 𝐵𝑉𝑍 No ) ∧ ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)) ∧ 𝑏𝐵) → 𝑏 No )
147142adantr 484 . . . . . . 7 ((((𝐵 No 𝐵𝑉𝑍 No ) ∧ ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)) ∧ 𝑏𝐵) → dom 𝑇 ∈ On)
148 noreson 33448 . . . . . . 7 ((𝑏 No ∧ dom 𝑇 ∈ On) → (𝑏 ↾ dom 𝑇) ∈ No )
149146, 147, 148syl2anc 587 . . . . . 6 ((((𝐵 No 𝐵𝑉𝑍 No ) ∧ ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)) ∧ 𝑏𝐵) → (𝑏 ↾ dom 𝑇) ∈ No )
150 sotr2 5474 . . . . . . 7 (( <s Or No ∧ ((𝑍 ↾ dom 𝑇) ∈ No 𝑇 No ∧ (𝑏 ↾ dom 𝑇) ∈ No )) → ((¬ 𝑇 <s (𝑍 ↾ dom 𝑇) ∧ 𝑇 <s (𝑏 ↾ dom 𝑇)) → (𝑍 ↾ dom 𝑇) <s (𝑏 ↾ dom 𝑇)))
151100, 150mpan 689 . . . . . 6 (((𝑍 ↾ dom 𝑇) ∈ No 𝑇 No ∧ (𝑏 ↾ dom 𝑇) ∈ No ) → ((¬ 𝑇 <s (𝑍 ↾ dom 𝑇) ∧ 𝑇 <s (𝑏 ↾ dom 𝑇)) → (𝑍 ↾ dom 𝑇) <s (𝑏 ↾ dom 𝑇)))
152144, 145, 149, 151syl3anc 1368 . . . . 5 ((((𝐵 No 𝐵𝑉𝑍 No ) ∧ ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)) ∧ 𝑏𝐵) → ((¬ 𝑇 <s (𝑍 ↾ dom 𝑇) ∧ 𝑇 <s (𝑏 ↾ dom 𝑇)) → (𝑍 ↾ dom 𝑇) <s (𝑏 ↾ dom 𝑇)))
153132, 137, 152mp2and 698 . . . 4 ((((𝐵 No 𝐵𝑉𝑍 No ) ∧ ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)) ∧ 𝑏𝐵) → (𝑍 ↾ dom 𝑇) <s (𝑏 ↾ dom 𝑇))
154 simpll3 1211 . . . . 5 ((((𝐵 No 𝐵𝑉𝑍 No ) ∧ ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)) ∧ 𝑏𝐵) → 𝑍 No )
155 sltres 33450 . . . . 5 ((𝑍 No 𝑏 No ∧ dom 𝑇 ∈ On) → ((𝑍 ↾ dom 𝑇) <s (𝑏 ↾ dom 𝑇) → 𝑍 <s 𝑏))
156154, 146, 147, 155syl3anc 1368 . . . 4 ((((𝐵 No 𝐵𝑉𝑍 No ) ∧ ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)) ∧ 𝑏𝐵) → ((𝑍 ↾ dom 𝑇) <s (𝑏 ↾ dom 𝑇) → 𝑍 <s 𝑏))
157153, 156mpd 15 . . 3 ((((𝐵 No 𝐵𝑉𝑍 No ) ∧ ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)) ∧ 𝑏𝐵) → 𝑍 <s 𝑏)
158157ralrimiva 3113 . 2 (((𝐵 No 𝐵𝑉𝑍 No ) ∧ ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)) → ∀𝑏𝐵 𝑍 <s 𝑏)
159131, 158impbida 800 1 ((𝐵 No 𝐵𝑉𝑍 No ) → (∀𝑏𝐵 𝑍 <s 𝑏 ↔ ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1084   = wceq 1538   ∈ wcel 2111  {cab 2735  ∀wral 3070  ∃wrex 3071  ∃!wreu 3072  ∃*wrmo 3073   ∪ cun 3856   ⊆ wss 3858  ifcif 4420  {csn 4522  ⟨cop 4528   class class class wbr 5032   ↦ cmpt 5112   Or wor 5442  dom cdm 5524   ↾ cres 5526  Rel wrel 5529  Ord word 6168  Oncon0 6169  suc csuc 6171  ℩cio 6292  Fun wfun 6329  ‘cfv 6335  ℩crio 7107  1oc1o 8105   No csur 33428
 Copyright terms: Public domain W3C validator