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

Theorem noinfbnd2 27682
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 3273 . . . . . . . . . 10 𝑥𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥
4 nfriota1 7379 . . . . . . . . . . 11 𝑥(𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)
54nfdm 5947 . . . . . . . . . . . . 13 𝑥dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)
6 nfcv 2892 . . . . . . . . . . . . 13 𝑥1o
75, 6nfop 4885 . . . . . . . . . . . 12 𝑥⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o
87nfsn 4707 . . . . . . . . . . 11 𝑥{⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩}
94, 8nfun 4158 . . . . . . . . . 10 𝑥((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩})
10 nfcv 2892 . . . . . . . . . . 11 𝑥{𝑦 ∣ ∃𝑢𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))}
11 nfiota1 6497 . . . . . . . . . . 11 𝑥(℩𝑥𝑢𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))
1210, 11nfmpt 5250 . . . . . . . . . 10 𝑥(𝑔 ∈ {𝑦 ∣ ∃𝑢𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥)))
133, 9, 12nfif 4554 . . . . . . . . 9 𝑥if(∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥, ((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))))
142, 13nfcxfr 2890 . . . . . . . 8 𝑥𝑇
15 nfcv 2892 . . . . . . . 8 𝑥 <s
16 nfcv 2892 . . . . . . . . 9 𝑥𝑍
1714nfdm 5947 . . . . . . . . 9 𝑥dom 𝑇
1816, 17nfres 5981 . . . . . . . 8 𝑥(𝑍 ↾ dom 𝑇)
1914, 15, 18nfbr 5190 . . . . . . 7 𝑥 𝑇 <s (𝑍 ↾ dom 𝑇)
2019nfn 1852 . . . . . 6 𝑥 ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)
211, 20nfim 1891 . . . . 5 𝑥(((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) → ¬ 𝑇 <s (𝑍 ↾ dom 𝑇))
22 noinfbnd2lem1 27681 . . . . . . . 8 (((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) → ¬ (𝑥 ∪ {⟨dom 𝑥, 1o⟩}) <s (𝑍 ↾ suc dom 𝑥))
23223expb 1117 . . . . . . 7 (((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → ¬ (𝑥 ∪ {⟨dom 𝑥, 1o⟩}) <s (𝑍 ↾ suc dom 𝑥))
24 rspe 3237 . . . . . . . . . . . 12 ((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) → ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)
2524adantr 479 . . . . . . . . . . 11 (((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)
2625iftrued 4532 . . . . . . . . . 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 481 . . . . . . . . . . . 12 (((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → (𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥))
28 simprl1 1215 . . . . . . . . . . . . . . 15 (((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → 𝐵 No )
29 nominmo 27650 . . . . . . . . . . . . . . 15 (𝐵 No → ∃*𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)
3028, 29syl 17 . . . . . . . . . . . . . 14 (((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → ∃*𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)
31 reu5 3366 . . . . . . . . . . . . . 14 (∃!𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ↔ (∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ∃*𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥))
3225, 30, 31sylanbrc 581 . . . . . . . . . . . . 13 (((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → ∃!𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)
33 riota1 7394 . . . . . . . . . . . . 13 (∃!𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 → ((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) ↔ (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) = 𝑥))
3432, 33syl 17 . . . . . . . . . . . 12 (((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → ((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) ↔ (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) = 𝑥))
3527, 34mpbid 231 . . . . . . . . . . 11 (((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) = 𝑥)
3635dmeqd 5902 . . . . . . . . . . . . 13 (((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) = dom 𝑥)
3736opeq1d 4875 . . . . . . . . . . . 12 (((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → ⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩ = ⟨dom 𝑥, 1o⟩)
3837sneqd 4636 . . . . . . . . . . 11 (((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → {⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩} = {⟨dom 𝑥, 1o⟩})
3935, 38uneq12d 4157 . . . . . . . . . 10 (((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → ((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩}) = (𝑥 ∪ {⟨dom 𝑥, 1o⟩}))
4026, 39eqtrd 2765 . . . . . . . . 9 (((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → if(∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥, ((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥)))) = (𝑥 ∪ {⟨dom 𝑥, 1o⟩}))
412, 40eqtrid 2777 . . . . . . . 8 (((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → 𝑇 = (𝑥 ∪ {⟨dom 𝑥, 1o⟩}))
4241dmeqd 5902 . . . . . . . . . 10 (((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → dom 𝑇 = dom (𝑥 ∪ {⟨dom 𝑥, 1o⟩}))
43 1oex 8495 . . . . . . . . . . . . 13 1o ∈ V
4443dmsnop 6215 . . . . . . . . . . . 12 dom {⟨dom 𝑥, 1o⟩} = {dom 𝑥}
4544uneq2i 4153 . . . . . . . . . . 11 (dom 𝑥 ∪ dom {⟨dom 𝑥, 1o⟩}) = (dom 𝑥 ∪ {dom 𝑥})
46 dmun 5907 . . . . . . . . . . 11 dom (𝑥 ∪ {⟨dom 𝑥, 1o⟩}) = (dom 𝑥 ∪ dom {⟨dom 𝑥, 1o⟩})
47 df-suc 6370 . . . . . . . . . . 11 suc dom 𝑥 = (dom 𝑥 ∪ {dom 𝑥})
4845, 46, 473eqtr4ri 2764 . . . . . . . . . 10 suc dom 𝑥 = dom (𝑥 ∪ {⟨dom 𝑥, 1o⟩})
4942, 48eqtr4di 2783 . . . . . . . . 9 (((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → dom 𝑇 = suc dom 𝑥)
5049reseq2d 5979 . . . . . . . 8 (((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → (𝑍 ↾ dom 𝑇) = (𝑍 ↾ suc dom 𝑥))
5141, 50breq12d 5156 . . . . . . 7 (((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → (𝑇 <s (𝑍 ↾ dom 𝑇) ↔ (𝑥 ∪ {⟨dom 𝑥, 1o⟩}) <s (𝑍 ↾ suc dom 𝑥)))
5223, 51mtbird 324 . . . . . 6 (((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → ¬ 𝑇 <s (𝑍 ↾ dom 𝑇))
5352exp31 418 . . . . 5 (𝑥𝐵 → (∀𝑦𝐵 ¬ 𝑦 <s 𝑥 → (((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) → ¬ 𝑇 <s (𝑍 ↾ dom 𝑇))))
5421, 53rexlimi 3247 . . . 4 (∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 → (((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) → ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)))
5554imp 405 . . 3 ((∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → ¬ 𝑇 <s (𝑍 ↾ dom 𝑇))
56 simprl3 1217 . . . . . 6 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → 𝑍 No )
572noinfno 27669 . . . . . . . . 9 ((𝐵 No 𝐵𝑉) → 𝑇 No )
58573adant3 1129 . . . . . . . 8 ((𝐵 No 𝐵𝑉𝑍 No ) → 𝑇 No )
5958ad2antrl 726 . . . . . . 7 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → 𝑇 No )
60 nodmon 27601 . . . . . . 7 (𝑇 No → dom 𝑇 ∈ On)
6159, 60syl 17 . . . . . 6 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → dom 𝑇 ∈ On)
62 noreson 27611 . . . . . 6 ((𝑍 No ∧ dom 𝑇 ∈ On) → (𝑍 ↾ dom 𝑇) ∈ No )
6356, 61, 62syl2anc 582 . . . . 5 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → (𝑍 ↾ dom 𝑇) ∈ No )
64 nofun 27600 . . . . . . . . 9 (𝑇 No → Fun 𝑇)
65 funrel 6565 . . . . . . . . 9 (Fun 𝑇 → Rel 𝑇)
6658, 64, 653syl 18 . . . . . . . 8 ((𝐵 No 𝐵𝑉𝑍 No ) → Rel 𝑇)
6766ad2antrl 726 . . . . . . 7 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → Rel 𝑇)
68 resdm 6025 . . . . . . 7 (Rel 𝑇 → (𝑇 ↾ dom 𝑇) = 𝑇)
6967, 68syl 17 . . . . . 6 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → (𝑇 ↾ dom 𝑇) = 𝑇)
7069, 59eqeltrd 2825 . . . . 5 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → (𝑇 ↾ dom 𝑇) ∈ No )
71 resdmss 6234 . . . . . 6 dom (𝑍 ↾ dom 𝑇) ⊆ dom 𝑇
7271a1i 11 . . . . 5 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → dom (𝑍 ↾ dom 𝑇) ⊆ dom 𝑇)
73 resdmss 6234 . . . . . 6 dom (𝑇 ↾ dom 𝑇) ⊆ dom 𝑇
7473a1i 11 . . . . 5 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → dom (𝑇 ↾ dom 𝑇) ⊆ dom 𝑇)
752noinfdm 27670 . . . . . . . . . . 11 (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 → dom 𝑇 = {𝑔 ∣ ∃𝑝𝐵 (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐵𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔)))})
7675eqabrd 2868 . . . . . . . . . 10 (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 → (𝑔 ∈ dom 𝑇 ↔ ∃𝑝𝐵 (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐵𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔)))))
7776adantr 479 . . . . . . . . 9 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → (𝑔 ∈ dom 𝑇 ↔ ∃𝑝𝐵 (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐵𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔)))))
78 simpll 765 . . . . . . . . . . . 12 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) ∧ (𝑝𝐵 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐵𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → ¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)
79 simprl1 1215 . . . . . . . . . . . . 13 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → 𝐵 No )
8079adantr 479 . . . . . . . . . . . 12 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) ∧ (𝑝𝐵 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐵𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → 𝐵 No )
81 simprl2 1216 . . . . . . . . . . . . 13 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → 𝐵𝑉)
8281adantr 479 . . . . . . . . . . . 12 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) ∧ (𝑝𝐵 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐵𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → 𝐵𝑉)
83 simprl 769 . . . . . . . . . . . 12 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) ∧ (𝑝𝐵 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐵𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → 𝑝𝐵)
84 simprrl 779 . . . . . . . . . . . 12 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) ∧ (𝑝𝐵 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐵𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → 𝑔 ∈ dom 𝑝)
85 simprrr 780 . . . . . . . . . . . . 13 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) ∧ (𝑝𝐵 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐵𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → ∀𝑞𝐵𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔)))
86 breq2 5147 . . . . . . . . . . . . . . . 16 (𝑞 = 𝑣 → (𝑝 <s 𝑞𝑝 <s 𝑣))
8786notbid 317 . . . . . . . . . . . . . . 15 (𝑞 = 𝑣 → (¬ 𝑝 <s 𝑞 ↔ ¬ 𝑝 <s 𝑣))
88 reseq1 5973 . . . . . . . . . . . . . . . 16 (𝑞 = 𝑣 → (𝑞 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔))
8988eqeq2d 2736 . . . . . . . . . . . . . . 15 (𝑞 = 𝑣 → ((𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔) ↔ (𝑝 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)))
9087, 89imbi12d 343 . . . . . . . . . . . . . 14 (𝑞 = 𝑣 → ((¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔)) ↔ (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔))))
9190cbvralvw 3225 . . . . . . . . . . . . 13 (∀𝑞𝐵𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔)) ↔ ∀𝑣𝐵𝑝 <s 𝑣 → (𝑝 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)))
9285, 91sylib 217 . . . . . . . . . . . 12 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) ∧ (𝑝𝐵 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐵𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → ∀𝑣𝐵𝑝 <s 𝑣 → (𝑝 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)))
932noinfres 27673 . . . . . . . . . . . 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 5147 . . . . . . . . . . . . . 14 (𝑏 = 𝑝 → (𝑍 <s 𝑏𝑍 <s 𝑝))
96 simplrr 776 . . . . . . . . . . . . . 14 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) ∧ (𝑝𝐵 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐵𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → ∀𝑏𝐵 𝑍 <s 𝑏)
9795, 96, 83rspcdva 3602 . . . . . . . . . . . . 13 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) ∧ (𝑝𝐵 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐵𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → 𝑍 <s 𝑝)
9856adantr 479 . . . . . . . . . . . . . 14 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) ∧ (𝑝𝐵 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐵𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → 𝑍 No )
9980, 83sseldd 3973 . . . . . . . . . . . . . 14 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) ∧ (𝑝𝐵 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐵𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → 𝑝 No )
100 sltso 27627 . . . . . . . . . . . . . . 15 <s Or No
101 soasym 5615 . . . . . . . . . . . . . . 15 (( <s Or No ∧ (𝑍 No 𝑝 No )) → (𝑍 <s 𝑝 → ¬ 𝑝 <s 𝑍))
102100, 101mpan 688 . . . . . . . . . . . . . 14 ((𝑍 No 𝑝 No ) → (𝑍 <s 𝑝 → ¬ 𝑝 <s 𝑍))
10398, 99, 102syl2anc 582 . . . . . . . . . . . . 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 27601 . . . . . . . . . . . . . . . 16 (𝑝 No → dom 𝑝 ∈ On)
10699, 105syl 17 . . . . . . . . . . . . . . 15 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) ∧ (𝑝𝐵 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐵𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → dom 𝑝 ∈ On)
107 onelon 6389 . . . . . . . . . . . . . . 15 ((dom 𝑝 ∈ On ∧ 𝑔 ∈ dom 𝑝) → 𝑔 ∈ On)
108106, 84, 107syl2anc 582 . . . . . . . . . . . . . 14 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) ∧ (𝑝𝐵 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐵𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → 𝑔 ∈ On)
109 onsucb 7818 . . . . . . . . . . . . . 14 (𝑔 ∈ On ↔ suc 𝑔 ∈ On)
110108, 109sylib 217 . . . . . . . . . . . . 13 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) ∧ (𝑝𝐵 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐵𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → suc 𝑔 ∈ On)
111 sltres 27613 . . . . . . . . . . . . 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 5161 . . . . . . . . . 10 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) ∧ (𝑝𝐵 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐵𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → ¬ (𝑇 ↾ suc 𝑔) <s (𝑍 ↾ suc 𝑔))
115114rexlimdvaa 3146 . . . . . . . . 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 405 . . . . . . 7 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) ∧ 𝑔 ∈ dom 𝑇) → ¬ (𝑇 ↾ suc 𝑔) <s (𝑍 ↾ suc 𝑔))
118 nodmord 27604 . . . . . . . . . . 11 (𝑇 No → Ord dom 𝑇)
119 ordsucss 7819 . . . . . . . . . . 11 (Ord dom 𝑇 → (𝑔 ∈ dom 𝑇 → suc 𝑔 ⊆ dom 𝑇))
12059, 118, 1193syl 18 . . . . . . . . . 10 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → (𝑔 ∈ dom 𝑇 → suc 𝑔 ⊆ dom 𝑇))
121120imp 405 . . . . . . . . 9 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) ∧ 𝑔 ∈ dom 𝑇) → suc 𝑔 ⊆ dom 𝑇)
122121resabs1d 6007 . . . . . . . 8 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) ∧ 𝑔 ∈ dom 𝑇) → ((𝑇 ↾ dom 𝑇) ↾ suc 𝑔) = (𝑇 ↾ suc 𝑔))
123121resabs1d 6007 . . . . . . . 8 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) ∧ 𝑔 ∈ dom 𝑇) → ((𝑍 ↾ dom 𝑇) ↾ suc 𝑔) = (𝑍 ↾ suc 𝑔))
124122, 123breq12d 5156 . . . . . . 7 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) ∧ 𝑔 ∈ dom 𝑇) → (((𝑇 ↾ dom 𝑇) ↾ suc 𝑔) <s ((𝑍 ↾ dom 𝑇) ↾ suc 𝑔) ↔ (𝑇 ↾ suc 𝑔) <s (𝑍 ↾ suc 𝑔)))
125117, 124mtbird 324 . . . . . 6 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) ∧ 𝑔 ∈ dom 𝑇) → ¬ ((𝑇 ↾ dom 𝑇) ↾ suc 𝑔) <s ((𝑍 ↾ dom 𝑇) ↾ suc 𝑔))
126125ralrimiva 3136 . . . . 5 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → ∀𝑔 ∈ dom 𝑇 ¬ ((𝑇 ↾ dom 𝑇) ↾ suc 𝑔) <s ((𝑍 ↾ dom 𝑇) ↾ suc 𝑔))
127 noresle 27648 . . . . 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 5153 . . . 4 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → ((𝑇 ↾ dom 𝑇) <s (𝑍 ↾ dom 𝑇) ↔ 𝑇 <s (𝑍 ↾ dom 𝑇)))
130128, 129mtbid 323 . . 3 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → ¬ 𝑇 <s (𝑍 ↾ dom 𝑇))
13155, 130pm2.61ian 810 . 2 (((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) → ¬ 𝑇 <s (𝑍 ↾ dom 𝑇))
132 simplr 767 . . . . 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 483 . . . . . 6 ((((𝐵 No 𝐵𝑉𝑍 No ) ∧ ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)) ∧ 𝑏𝐵) → 𝑏𝐵)
1362noinfbnd1 27680 . . . . . 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 582 . . . . . . . . 9 (((𝐵 No 𝐵𝑉𝑍 No ) ∧ ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)) → 𝑇 No )
142141, 60syl 17 . . . . . . . 8 (((𝐵 No 𝐵𝑉𝑍 No ) ∧ ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)) → dom 𝑇 ∈ On)
143138, 142, 62syl2anc 582 . . . . . . 7 (((𝐵 No 𝐵𝑉𝑍 No ) ∧ ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)) → (𝑍 ↾ dom 𝑇) ∈ No )
144143adantr 479 . . . . . 6 ((((𝐵 No 𝐵𝑉𝑍 No ) ∧ ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)) ∧ 𝑏𝐵) → (𝑍 ↾ dom 𝑇) ∈ No )
145141adantr 479 . . . . . 6 ((((𝐵 No 𝐵𝑉𝑍 No ) ∧ ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)) ∧ 𝑏𝐵) → 𝑇 No )
146139sselda 3972 . . . . . . 7 ((((𝐵 No 𝐵𝑉𝑍 No ) ∧ ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)) ∧ 𝑏𝐵) → 𝑏 No )
147142adantr 479 . . . . . . 7 ((((𝐵 No 𝐵𝑉𝑍 No ) ∧ ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)) ∧ 𝑏𝐵) → dom 𝑇 ∈ On)
148 noreson 27611 . . . . . . 7 ((𝑏 No ∧ dom 𝑇 ∈ On) → (𝑏 ↾ dom 𝑇) ∈ No )
149146, 147, 148syl2anc 582 . . . . . 6 ((((𝐵 No 𝐵𝑉𝑍 No ) ∧ ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)) ∧ 𝑏𝐵) → (𝑏 ↾ dom 𝑇) ∈ No )
150 sotr2 5616 . . . . . . 7 (( <s Or No ∧ ((𝑍 ↾ dom 𝑇) ∈ No 𝑇 No ∧ (𝑏 ↾ dom 𝑇) ∈ No )) → ((¬ 𝑇 <s (𝑍 ↾ dom 𝑇) ∧ 𝑇 <s (𝑏 ↾ dom 𝑇)) → (𝑍 ↾ dom 𝑇) <s (𝑏 ↾ dom 𝑇)))
151100, 150mpan 688 . . . . . 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 697 . . . 4 ((((𝐵 No 𝐵𝑉𝑍 No ) ∧ ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)) ∧ 𝑏𝐵) → (𝑍 ↾ dom 𝑇) <s (𝑏 ↾ dom 𝑇))
154 simpll3 1211 . . . . 5 ((((𝐵 No 𝐵𝑉𝑍 No ) ∧ ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)) ∧ 𝑏𝐵) → 𝑍 No )
155 sltres 27613 . . . . 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 3136 . 2 (((𝐵 No 𝐵𝑉𝑍 No ) ∧ ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)) → ∀𝑏𝐵 𝑍 <s 𝑏)
159131, 158impbida 799 1 ((𝐵 No 𝐵𝑉𝑍 No ) → (∀𝑏𝐵 𝑍 <s 𝑏 ↔ ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 394  w3a 1084   = wceq 1533  wcel 2098  {cab 2702  wral 3051  wrex 3060  ∃!wreu 3362  ∃*wrmo 3363  cun 3937  wss 3939  ifcif 4524  {csn 4624  cop 4630   class class class wbr 5143  cmpt 5226   Or wor 5583  dom cdm 5672  cres 5674  Rel wrel 5677  Ord word 6363  Oncon0 6364  suc csuc 6366  cio 6493  Fun wfun 6537  cfv 6543  crio 7371  1oc1o 8478   No csur 27591   <s cslt 27592
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 2166  ax-ext 2696  ax-rep 5280  ax-sep 5294  ax-nul 5301  ax-pr 5423  ax-un 7738
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  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 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2931  df-ral 3052  df-rex 3061  df-rmo 3364  df-reu 3365  df-rab 3420  df-v 3465  df-sbc 3769  df-csb 3885  df-dif 3942  df-un 3944  df-in 3946  df-ss 3956  df-pss 3959  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-tp 4629  df-op 4631  df-uni 4904  df-int 4945  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5227  df-tr 5261  df-id 5570  df-eprel 5576  df-po 5584  df-so 5585  df-fr 5627  df-we 5629  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-ord 6367  df-on 6368  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-riota 7372  df-1o 8485  df-2o 8486  df-no 27594  df-slt 27595  df-bday 27596
This theorem is referenced by:  nosupinfsep  27683  noetainflem4  27691
  Copyright terms: Public domain W3C validator