MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  noinfbnd2 Structured version   Visualization version   GIF version

Theorem noinfbnd2 27619
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 1909 . . . . . 6 𝑥((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)
2 noinfbnd2.1 . . . . . . . . 9 𝑇 = if(∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥, ((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))))
3 nfre1 3276 . . . . . . . . . 10 𝑥𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥
4 nfriota1 7368 . . . . . . . . . . 11 𝑥(𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)
54nfdm 5944 . . . . . . . . . . . . 13 𝑥dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)
6 nfcv 2897 . . . . . . . . . . . . 13 𝑥1o
75, 6nfop 4884 . . . . . . . . . . . 12 𝑥⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o
87nfsn 4706 . . . . . . . . . . 11 𝑥{⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩}
94, 8nfun 4160 . . . . . . . . . 10 𝑥((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩})
10 nfcv 2897 . . . . . . . . . . 11 𝑥{𝑦 ∣ ∃𝑢𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))}
11 nfiota1 6491 . . . . . . . . . . 11 𝑥(℩𝑥𝑢𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))
1210, 11nfmpt 5248 . . . . . . . . . 10 𝑥(𝑔 ∈ {𝑦 ∣ ∃𝑢𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥)))
133, 9, 12nfif 4553 . . . . . . . . 9 𝑥if(∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥, ((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))))
142, 13nfcxfr 2895 . . . . . . . 8 𝑥𝑇
15 nfcv 2897 . . . . . . . 8 𝑥 <s
16 nfcv 2897 . . . . . . . . 9 𝑥𝑍
1714nfdm 5944 . . . . . . . . 9 𝑥dom 𝑇
1816, 17nfres 5977 . . . . . . . 8 𝑥(𝑍 ↾ dom 𝑇)
1914, 15, 18nfbr 5188 . . . . . . 7 𝑥 𝑇 <s (𝑍 ↾ dom 𝑇)
2019nfn 1852 . . . . . 6 𝑥 ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)
211, 20nfim 1891 . . . . 5 𝑥(((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) → ¬ 𝑇 <s (𝑍 ↾ dom 𝑇))
22 noinfbnd2lem1 27618 . . . . . . . 8 (((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) → ¬ (𝑥 ∪ {⟨dom 𝑥, 1o⟩}) <s (𝑍 ↾ suc dom 𝑥))
23223expb 1117 . . . . . . 7 (((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → ¬ (𝑥 ∪ {⟨dom 𝑥, 1o⟩}) <s (𝑍 ↾ suc dom 𝑥))
24 rspe 3240 . . . . . . . . . . . 12 ((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) → ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)
2524adantr 480 . . . . . . . . . . 11 (((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)
2625iftrued 4531 . . . . . . . . . 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 482 . . . . . . . . . . . 12 (((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → (𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥))
28 simprl1 1215 . . . . . . . . . . . . . . 15 (((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → 𝐵 No )
29 nominmo 27587 . . . . . . . . . . . . . . 15 (𝐵 No → ∃*𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)
3028, 29syl 17 . . . . . . . . . . . . . 14 (((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → ∃*𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)
31 reu5 3372 . . . . . . . . . . . . . 14 (∃!𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ↔ (∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ∃*𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥))
3225, 30, 31sylanbrc 582 . . . . . . . . . . . . 13 (((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → ∃!𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)
33 riota1 7383 . . . . . . . . . . . . 13 (∃!𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 → ((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) ↔ (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) = 𝑥))
3432, 33syl 17 . . . . . . . . . . . 12 (((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → ((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) ↔ (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) = 𝑥))
3527, 34mpbid 231 . . . . . . . . . . 11 (((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) = 𝑥)
3635dmeqd 5899 . . . . . . . . . . . . 13 (((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) = dom 𝑥)
3736opeq1d 4874 . . . . . . . . . . . 12 (((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → ⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩ = ⟨dom 𝑥, 1o⟩)
3837sneqd 4635 . . . . . . . . . . 11 (((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → {⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩} = {⟨dom 𝑥, 1o⟩})
3935, 38uneq12d 4159 . . . . . . . . . 10 (((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → ((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩}) = (𝑥 ∪ {⟨dom 𝑥, 1o⟩}))
4026, 39eqtrd 2766 . . . . . . . . 9 (((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → if(∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥, ((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥)))) = (𝑥 ∪ {⟨dom 𝑥, 1o⟩}))
412, 40eqtrid 2778 . . . . . . . 8 (((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → 𝑇 = (𝑥 ∪ {⟨dom 𝑥, 1o⟩}))
4241dmeqd 5899 . . . . . . . . . 10 (((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → dom 𝑇 = dom (𝑥 ∪ {⟨dom 𝑥, 1o⟩}))
43 1oex 8477 . . . . . . . . . . . . 13 1o ∈ V
4443dmsnop 6209 . . . . . . . . . . . 12 dom {⟨dom 𝑥, 1o⟩} = {dom 𝑥}
4544uneq2i 4155 . . . . . . . . . . 11 (dom 𝑥 ∪ dom {⟨dom 𝑥, 1o⟩}) = (dom 𝑥 ∪ {dom 𝑥})
46 dmun 5904 . . . . . . . . . . 11 dom (𝑥 ∪ {⟨dom 𝑥, 1o⟩}) = (dom 𝑥 ∪ dom {⟨dom 𝑥, 1o⟩})
47 df-suc 6364 . . . . . . . . . . 11 suc dom 𝑥 = (dom 𝑥 ∪ {dom 𝑥})
4845, 46, 473eqtr4ri 2765 . . . . . . . . . 10 suc dom 𝑥 = dom (𝑥 ∪ {⟨dom 𝑥, 1o⟩})
4942, 48eqtr4di 2784 . . . . . . . . 9 (((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → dom 𝑇 = suc dom 𝑥)
5049reseq2d 5975 . . . . . . . 8 (((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → (𝑍 ↾ dom 𝑇) = (𝑍 ↾ suc dom 𝑥))
5141, 50breq12d 5154 . . . . . . 7 (((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → (𝑇 <s (𝑍 ↾ dom 𝑇) ↔ (𝑥 ∪ {⟨dom 𝑥, 1o⟩}) <s (𝑍 ↾ suc dom 𝑥)))
5223, 51mtbird 325 . . . . . 6 (((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → ¬ 𝑇 <s (𝑍 ↾ dom 𝑇))
5352exp31 419 . . . . 5 (𝑥𝐵 → (∀𝑦𝐵 ¬ 𝑦 <s 𝑥 → (((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) → ¬ 𝑇 <s (𝑍 ↾ dom 𝑇))))
5421, 53rexlimi 3250 . . . 4 (∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 → (((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) → ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)))
5554imp 406 . . 3 ((∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → ¬ 𝑇 <s (𝑍 ↾ dom 𝑇))
56 simprl3 1217 . . . . . 6 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → 𝑍 No )
572noinfno 27606 . . . . . . . . 9 ((𝐵 No 𝐵𝑉) → 𝑇 No )
58573adant3 1129 . . . . . . . 8 ((𝐵 No 𝐵𝑉𝑍 No ) → 𝑇 No )
5958ad2antrl 725 . . . . . . 7 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → 𝑇 No )
60 nodmon 27538 . . . . . . 7 (𝑇 No → dom 𝑇 ∈ On)
6159, 60syl 17 . . . . . 6 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → dom 𝑇 ∈ On)
62 noreson 27548 . . . . . 6 ((𝑍 No ∧ dom 𝑇 ∈ On) → (𝑍 ↾ dom 𝑇) ∈ No )
6356, 61, 62syl2anc 583 . . . . 5 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → (𝑍 ↾ dom 𝑇) ∈ No )
64 nofun 27537 . . . . . . . . 9 (𝑇 No → Fun 𝑇)
65 funrel 6559 . . . . . . . . 9 (Fun 𝑇 → Rel 𝑇)
6658, 64, 653syl 18 . . . . . . . 8 ((𝐵 No 𝐵𝑉𝑍 No ) → Rel 𝑇)
6766ad2antrl 725 . . . . . . 7 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → Rel 𝑇)
68 resdm 6020 . . . . . . 7 (Rel 𝑇 → (𝑇 ↾ dom 𝑇) = 𝑇)
6967, 68syl 17 . . . . . 6 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → (𝑇 ↾ dom 𝑇) = 𝑇)
7069, 59eqeltrd 2827 . . . . 5 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → (𝑇 ↾ dom 𝑇) ∈ No )
71 resdmss 6228 . . . . . 6 dom (𝑍 ↾ dom 𝑇) ⊆ dom 𝑇
7271a1i 11 . . . . 5 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → dom (𝑍 ↾ dom 𝑇) ⊆ dom 𝑇)
73 resdmss 6228 . . . . . 6 dom (𝑇 ↾ dom 𝑇) ⊆ dom 𝑇
7473a1i 11 . . . . 5 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → dom (𝑇 ↾ dom 𝑇) ⊆ dom 𝑇)
752noinfdm 27607 . . . . . . . . . . 11 (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 → dom 𝑇 = {𝑔 ∣ ∃𝑝𝐵 (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐵𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔)))})
7675eqabrd 2870 . . . . . . . . . 10 (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 → (𝑔 ∈ dom 𝑇 ↔ ∃𝑝𝐵 (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐵𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔)))))
7776adantr 480 . . . . . . . . 9 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → (𝑔 ∈ dom 𝑇 ↔ ∃𝑝𝐵 (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐵𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔)))))
78 simpll 764 . . . . . . . . . . . 12 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) ∧ (𝑝𝐵 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐵𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → ¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)
79 simprl1 1215 . . . . . . . . . . . . 13 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → 𝐵 No )
8079adantr 480 . . . . . . . . . . . 12 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) ∧ (𝑝𝐵 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐵𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → 𝐵 No )
81 simprl2 1216 . . . . . . . . . . . . 13 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → 𝐵𝑉)
8281adantr 480 . . . . . . . . . . . 12 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) ∧ (𝑝𝐵 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐵𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → 𝐵𝑉)
83 simprl 768 . . . . . . . . . . . 12 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) ∧ (𝑝𝐵 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐵𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → 𝑝𝐵)
84 simprrl 778 . . . . . . . . . . . 12 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) ∧ (𝑝𝐵 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐵𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → 𝑔 ∈ dom 𝑝)
85 simprrr 779 . . . . . . . . . . . . 13 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) ∧ (𝑝𝐵 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐵𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → ∀𝑞𝐵𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔)))
86 breq2 5145 . . . . . . . . . . . . . . . 16 (𝑞 = 𝑣 → (𝑝 <s 𝑞𝑝 <s 𝑣))
8786notbid 318 . . . . . . . . . . . . . . 15 (𝑞 = 𝑣 → (¬ 𝑝 <s 𝑞 ↔ ¬ 𝑝 <s 𝑣))
88 reseq1 5969 . . . . . . . . . . . . . . . 16 (𝑞 = 𝑣 → (𝑞 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔))
8988eqeq2d 2737 . . . . . . . . . . . . . . 15 (𝑞 = 𝑣 → ((𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔) ↔ (𝑝 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)))
9087, 89imbi12d 344 . . . . . . . . . . . . . 14 (𝑞 = 𝑣 → ((¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔)) ↔ (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔))))
9190cbvralvw 3228 . . . . . . . . . . . . 13 (∀𝑞𝐵𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔)) ↔ ∀𝑣𝐵𝑝 <s 𝑣 → (𝑝 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)))
9285, 91sylib 217 . . . . . . . . . . . 12 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) ∧ (𝑝𝐵 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐵𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → ∀𝑣𝐵𝑝 <s 𝑣 → (𝑝 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)))
932noinfres 27610 . . . . . . . . . . . 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 5145 . . . . . . . . . . . . . 14 (𝑏 = 𝑝 → (𝑍 <s 𝑏𝑍 <s 𝑝))
96 simplrr 775 . . . . . . . . . . . . . 14 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) ∧ (𝑝𝐵 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐵𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → ∀𝑏𝐵 𝑍 <s 𝑏)
9795, 96, 83rspcdva 3607 . . . . . . . . . . . . 13 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) ∧ (𝑝𝐵 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐵𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → 𝑍 <s 𝑝)
9856adantr 480 . . . . . . . . . . . . . 14 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) ∧ (𝑝𝐵 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐵𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → 𝑍 No )
9980, 83sseldd 3978 . . . . . . . . . . . . . 14 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) ∧ (𝑝𝐵 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐵𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → 𝑝 No )
100 sltso 27564 . . . . . . . . . . . . . . 15 <s Or No
101 soasym 5612 . . . . . . . . . . . . . . 15 (( <s Or No ∧ (𝑍 No 𝑝 No )) → (𝑍 <s 𝑝 → ¬ 𝑝 <s 𝑍))
102100, 101mpan 687 . . . . . . . . . . . . . 14 ((𝑍 No 𝑝 No ) → (𝑍 <s 𝑝 → ¬ 𝑝 <s 𝑍))
10398, 99, 102syl2anc 583 . . . . . . . . . . . . 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 27538 . . . . . . . . . . . . . . . 16 (𝑝 No → dom 𝑝 ∈ On)
10699, 105syl 17 . . . . . . . . . . . . . . 15 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) ∧ (𝑝𝐵 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐵𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → dom 𝑝 ∈ On)
107 onelon 6383 . . . . . . . . . . . . . . 15 ((dom 𝑝 ∈ On ∧ 𝑔 ∈ dom 𝑝) → 𝑔 ∈ On)
108106, 84, 107syl2anc 583 . . . . . . . . . . . . . 14 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) ∧ (𝑝𝐵 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐵𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → 𝑔 ∈ On)
109 onsucb 7802 . . . . . . . . . . . . . 14 (𝑔 ∈ On ↔ suc 𝑔 ∈ On)
110108, 109sylib 217 . . . . . . . . . . . . 13 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) ∧ (𝑝𝐵 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐵𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → suc 𝑔 ∈ On)
111 sltres 27550 . . . . . . . . . . . . 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 197 . . . . . . . . . . 11 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) ∧ (𝑝𝐵 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐵𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → ¬ (𝑝 ↾ suc 𝑔) <s (𝑍 ↾ suc 𝑔))
11494, 113eqnbrtrd 5159 . . . . . . . . . 10 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) ∧ (𝑝𝐵 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐵𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → ¬ (𝑇 ↾ suc 𝑔) <s (𝑍 ↾ suc 𝑔))
115114rexlimdvaa 3150 . . . . . . . . 9 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → (∃𝑝𝐵 (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐵𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))) → ¬ (𝑇 ↾ suc 𝑔) <s (𝑍 ↾ suc 𝑔)))
11677, 115sylbid 239 . . . . . . . 8 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → (𝑔 ∈ dom 𝑇 → ¬ (𝑇 ↾ suc 𝑔) <s (𝑍 ↾ suc 𝑔)))
117116imp 406 . . . . . . 7 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) ∧ 𝑔 ∈ dom 𝑇) → ¬ (𝑇 ↾ suc 𝑔) <s (𝑍 ↾ suc 𝑔))
118 nodmord 27541 . . . . . . . . . . 11 (𝑇 No → Ord dom 𝑇)
119 ordsucss 7803 . . . . . . . . . . 11 (Ord dom 𝑇 → (𝑔 ∈ dom 𝑇 → suc 𝑔 ⊆ dom 𝑇))
12059, 118, 1193syl 18 . . . . . . . . . 10 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → (𝑔 ∈ dom 𝑇 → suc 𝑔 ⊆ dom 𝑇))
121120imp 406 . . . . . . . . 9 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) ∧ 𝑔 ∈ dom 𝑇) → suc 𝑔 ⊆ dom 𝑇)
122121resabs1d 6006 . . . . . . . 8 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) ∧ 𝑔 ∈ dom 𝑇) → ((𝑇 ↾ dom 𝑇) ↾ suc 𝑔) = (𝑇 ↾ suc 𝑔))
123121resabs1d 6006 . . . . . . . 8 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) ∧ 𝑔 ∈ dom 𝑇) → ((𝑍 ↾ dom 𝑇) ↾ suc 𝑔) = (𝑍 ↾ suc 𝑔))
124122, 123breq12d 5154 . . . . . . 7 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) ∧ 𝑔 ∈ dom 𝑇) → (((𝑇 ↾ dom 𝑇) ↾ suc 𝑔) <s ((𝑍 ↾ dom 𝑇) ↾ suc 𝑔) ↔ (𝑇 ↾ suc 𝑔) <s (𝑍 ↾ suc 𝑔)))
125117, 124mtbird 325 . . . . . 6 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) ∧ 𝑔 ∈ dom 𝑇) → ¬ ((𝑇 ↾ dom 𝑇) ↾ suc 𝑔) <s ((𝑍 ↾ dom 𝑇) ↾ suc 𝑔))
126125ralrimiva 3140 . . . . 5 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → ∀𝑔 ∈ dom 𝑇 ¬ ((𝑇 ↾ dom 𝑇) ↾ suc 𝑔) <s ((𝑍 ↾ dom 𝑇) ↾ suc 𝑔))
127 noresle 27585 . . . . 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 5151 . . . 4 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → ((𝑇 ↾ dom 𝑇) <s (𝑍 ↾ dom 𝑇) ↔ 𝑇 <s (𝑍 ↾ dom 𝑇)))
130128, 129mtbid 324 . . 3 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → ¬ 𝑇 <s (𝑍 ↾ dom 𝑇))
13155, 130pm2.61ian 809 . 2 (((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) → ¬ 𝑇 <s (𝑍 ↾ dom 𝑇))
132 simplr 766 . . . . 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 484 . . . . . 6 ((((𝐵 No 𝐵𝑉𝑍 No ) ∧ ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)) ∧ 𝑏𝐵) → 𝑏𝐵)
1362noinfbnd1 27617 . . . . . 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 583 . . . . . . . . 9 (((𝐵 No 𝐵𝑉𝑍 No ) ∧ ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)) → 𝑇 No )
142141, 60syl 17 . . . . . . . 8 (((𝐵 No 𝐵𝑉𝑍 No ) ∧ ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)) → dom 𝑇 ∈ On)
143138, 142, 62syl2anc 583 . . . . . . 7 (((𝐵 No 𝐵𝑉𝑍 No ) ∧ ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)) → (𝑍 ↾ dom 𝑇) ∈ No )
144143adantr 480 . . . . . 6 ((((𝐵 No 𝐵𝑉𝑍 No ) ∧ ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)) ∧ 𝑏𝐵) → (𝑍 ↾ dom 𝑇) ∈ No )
145141adantr 480 . . . . . 6 ((((𝐵 No 𝐵𝑉𝑍 No ) ∧ ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)) ∧ 𝑏𝐵) → 𝑇 No )
146139sselda 3977 . . . . . . 7 ((((𝐵 No 𝐵𝑉𝑍 No ) ∧ ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)) ∧ 𝑏𝐵) → 𝑏 No )
147142adantr 480 . . . . . . 7 ((((𝐵 No 𝐵𝑉𝑍 No ) ∧ ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)) ∧ 𝑏𝐵) → dom 𝑇 ∈ On)
148 noreson 27548 . . . . . . 7 ((𝑏 No ∧ dom 𝑇 ∈ On) → (𝑏 ↾ dom 𝑇) ∈ No )
149146, 147, 148syl2anc 583 . . . . . 6 ((((𝐵 No 𝐵𝑉𝑍 No ) ∧ ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)) ∧ 𝑏𝐵) → (𝑏 ↾ dom 𝑇) ∈ No )
150 sotr2 5613 . . . . . . 7 (( <s Or No ∧ ((𝑍 ↾ dom 𝑇) ∈ No 𝑇 No ∧ (𝑏 ↾ dom 𝑇) ∈ No )) → ((¬ 𝑇 <s (𝑍 ↾ dom 𝑇) ∧ 𝑇 <s (𝑏 ↾ dom 𝑇)) → (𝑍 ↾ dom 𝑇) <s (𝑏 ↾ dom 𝑇)))
151100, 150mpan 687 . . . . . 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 696 . . . 4 ((((𝐵 No 𝐵𝑉𝑍 No ) ∧ ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)) ∧ 𝑏𝐵) → (𝑍 ↾ dom 𝑇) <s (𝑏 ↾ dom 𝑇))
154 simpll3 1211 . . . . 5 ((((𝐵 No 𝐵𝑉𝑍 No ) ∧ ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)) ∧ 𝑏𝐵) → 𝑍 No )
155 sltres 27550 . . . . 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 3140 . 2 (((𝐵 No 𝐵𝑉𝑍 No ) ∧ ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)) → ∀𝑏𝐵 𝑍 <s 𝑏)
159131, 158impbida 798 1 ((𝐵 No 𝐵𝑉𝑍 No ) → (∀𝑏𝐵 𝑍 <s 𝑏 ↔ ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 395  w3a 1084   = wceq 1533  wcel 2098  {cab 2703  wral 3055  wrex 3064  ∃!wreu 3368  ∃*wrmo 3369  cun 3941  wss 3943  ifcif 4523  {csn 4623  cop 4629   class class class wbr 5141  cmpt 5224   Or wor 5580  dom cdm 5669  cres 5671  Rel wrel 5674  Ord word 6357  Oncon0 6358  suc csuc 6360  cio 6487  Fun wfun 6531  cfv 6537  crio 7360  1oc1o 8460   No csur 27528   <s cslt 27529
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2697  ax-rep 5278  ax-sep 5292  ax-nul 5299  ax-pr 5420  ax-un 7722
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2704  df-cleq 2718  df-clel 2804  df-nfc 2879  df-ne 2935  df-ral 3056  df-rex 3065  df-rmo 3370  df-reu 3371  df-rab 3427  df-v 3470  df-sbc 3773  df-csb 3889  df-dif 3946  df-un 3948  df-in 3950  df-ss 3960  df-pss 3962  df-nul 4318  df-if 4524  df-pw 4599  df-sn 4624  df-pr 4626  df-tp 4628  df-op 4630  df-uni 4903  df-int 4944  df-iun 4992  df-br 5142  df-opab 5204  df-mpt 5225  df-tr 5259  df-id 5567  df-eprel 5573  df-po 5581  df-so 5582  df-fr 5624  df-we 5626  df-xp 5675  df-rel 5676  df-cnv 5677  df-co 5678  df-dm 5679  df-rn 5680  df-res 5681  df-ima 5682  df-ord 6361  df-on 6362  df-suc 6364  df-iota 6489  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-riota 7361  df-1o 8467  df-2o 8468  df-no 27531  df-slt 27532  df-bday 27533
This theorem is referenced by:  nosupinfsep  27620  noetainflem4  27628
  Copyright terms: Public domain W3C validator