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

Theorem noinfbnd2 27095
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 1918 . . . . . 6 𝑥((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)
2 noinfbnd2.1 . . . . . . . . 9 𝑇 = if(∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥, ((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))))
3 nfre1 3267 . . . . . . . . . 10 𝑥𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥
4 nfriota1 7321 . . . . . . . . . . 11 𝑥(𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)
54nfdm 5907 . . . . . . . . . . . . 13 𝑥dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)
6 nfcv 2904 . . . . . . . . . . . . 13 𝑥1o
75, 6nfop 4847 . . . . . . . . . . . 12 𝑥⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o
87nfsn 4669 . . . . . . . . . . 11 𝑥{⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩}
94, 8nfun 4126 . . . . . . . . . 10 𝑥((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩})
10 nfcv 2904 . . . . . . . . . . 11 𝑥{𝑦 ∣ ∃𝑢𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))}
11 nfiota1 6451 . . . . . . . . . . 11 𝑥(℩𝑥𝑢𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))
1210, 11nfmpt 5213 . . . . . . . . . 10 𝑥(𝑔 ∈ {𝑦 ∣ ∃𝑢𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥)))
133, 9, 12nfif 4517 . . . . . . . . 9 𝑥if(∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥, ((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))))
142, 13nfcxfr 2902 . . . . . . . 8 𝑥𝑇
15 nfcv 2904 . . . . . . . 8 𝑥 <s
16 nfcv 2904 . . . . . . . . 9 𝑥𝑍
1714nfdm 5907 . . . . . . . . 9 𝑥dom 𝑇
1816, 17nfres 5940 . . . . . . . 8 𝑥(𝑍 ↾ dom 𝑇)
1914, 15, 18nfbr 5153 . . . . . . 7 𝑥 𝑇 <s (𝑍 ↾ dom 𝑇)
2019nfn 1861 . . . . . 6 𝑥 ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)
211, 20nfim 1900 . . . . 5 𝑥(((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) → ¬ 𝑇 <s (𝑍 ↾ dom 𝑇))
22 noinfbnd2lem1 27094 . . . . . . . 8 (((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) ∧ (𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) → ¬ (𝑥 ∪ {⟨dom 𝑥, 1o⟩}) <s (𝑍 ↾ suc dom 𝑥))
23223expb 1121 . . . . . . 7 (((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → ¬ (𝑥 ∪ {⟨dom 𝑥, 1o⟩}) <s (𝑍 ↾ suc dom 𝑥))
24 rspe 3231 . . . . . . . . . . . 12 ((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) → ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)
2524adantr 482 . . . . . . . . . . 11 (((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)
2625iftrued 4495 . . . . . . . . . 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 484 . . . . . . . . . . . 12 (((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → (𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥))
28 simprl1 1219 . . . . . . . . . . . . . . 15 (((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → 𝐵 No )
29 nominmo 27063 . . . . . . . . . . . . . . 15 (𝐵 No → ∃*𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)
3028, 29syl 17 . . . . . . . . . . . . . 14 (((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → ∃*𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)
31 reu5 3354 . . . . . . . . . . . . . 14 (∃!𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ↔ (∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ∃*𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥))
3225, 30, 31sylanbrc 584 . . . . . . . . . . . . 13 (((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → ∃!𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)
33 riota1 7336 . . . . . . . . . . . . 13 (∃!𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 → ((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) ↔ (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) = 𝑥))
3432, 33syl 17 . . . . . . . . . . . 12 (((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → ((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) ↔ (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) = 𝑥))
3527, 34mpbid 231 . . . . . . . . . . 11 (((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) = 𝑥)
3635dmeqd 5862 . . . . . . . . . . . . 13 (((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) = dom 𝑥)
3736opeq1d 4837 . . . . . . . . . . . 12 (((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → ⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩ = ⟨dom 𝑥, 1o⟩)
3837sneqd 4599 . . . . . . . . . . 11 (((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → {⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩} = {⟨dom 𝑥, 1o⟩})
3935, 38uneq12d 4125 . . . . . . . . . 10 (((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → ((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩}) = (𝑥 ∪ {⟨dom 𝑥, 1o⟩}))
4026, 39eqtrd 2773 . . . . . . . . 9 (((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → if(∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥, ((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥)))) = (𝑥 ∪ {⟨dom 𝑥, 1o⟩}))
412, 40eqtrid 2785 . . . . . . . 8 (((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → 𝑇 = (𝑥 ∪ {⟨dom 𝑥, 1o⟩}))
4241dmeqd 5862 . . . . . . . . . 10 (((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → dom 𝑇 = dom (𝑥 ∪ {⟨dom 𝑥, 1o⟩}))
43 1oex 8423 . . . . . . . . . . . . 13 1o ∈ V
4443dmsnop 6169 . . . . . . . . . . . 12 dom {⟨dom 𝑥, 1o⟩} = {dom 𝑥}
4544uneq2i 4121 . . . . . . . . . . 11 (dom 𝑥 ∪ dom {⟨dom 𝑥, 1o⟩}) = (dom 𝑥 ∪ {dom 𝑥})
46 dmun 5867 . . . . . . . . . . 11 dom (𝑥 ∪ {⟨dom 𝑥, 1o⟩}) = (dom 𝑥 ∪ dom {⟨dom 𝑥, 1o⟩})
47 df-suc 6324 . . . . . . . . . . 11 suc dom 𝑥 = (dom 𝑥 ∪ {dom 𝑥})
4845, 46, 473eqtr4ri 2772 . . . . . . . . . 10 suc dom 𝑥 = dom (𝑥 ∪ {⟨dom 𝑥, 1o⟩})
4942, 48eqtr4di 2791 . . . . . . . . 9 (((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → dom 𝑇 = suc dom 𝑥)
5049reseq2d 5938 . . . . . . . 8 (((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → (𝑍 ↾ dom 𝑇) = (𝑍 ↾ suc dom 𝑥))
5141, 50breq12d 5119 . . . . . . 7 (((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → (𝑇 <s (𝑍 ↾ dom 𝑇) ↔ (𝑥 ∪ {⟨dom 𝑥, 1o⟩}) <s (𝑍 ↾ suc dom 𝑥)))
5223, 51mtbird 325 . . . . . 6 (((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → ¬ 𝑇 <s (𝑍 ↾ dom 𝑇))
5352exp31 421 . . . . 5 (𝑥𝐵 → (∀𝑦𝐵 ¬ 𝑦 <s 𝑥 → (((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) → ¬ 𝑇 <s (𝑍 ↾ dom 𝑇))))
5421, 53rexlimi 3241 . . . 4 (∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 → (((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏) → ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)))
5554imp 408 . . 3 ((∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → ¬ 𝑇 <s (𝑍 ↾ dom 𝑇))
56 simprl3 1221 . . . . . 6 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → 𝑍 No )
572noinfno 27082 . . . . . . . . 9 ((𝐵 No 𝐵𝑉) → 𝑇 No )
58573adant3 1133 . . . . . . . 8 ((𝐵 No 𝐵𝑉𝑍 No ) → 𝑇 No )
5958ad2antrl 727 . . . . . . 7 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → 𝑇 No )
60 nodmon 27014 . . . . . . 7 (𝑇 No → dom 𝑇 ∈ On)
6159, 60syl 17 . . . . . 6 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → dom 𝑇 ∈ On)
62 noreson 27024 . . . . . 6 ((𝑍 No ∧ dom 𝑇 ∈ On) → (𝑍 ↾ dom 𝑇) ∈ No )
6356, 61, 62syl2anc 585 . . . . 5 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → (𝑍 ↾ dom 𝑇) ∈ No )
64 nofun 27013 . . . . . . . . 9 (𝑇 No → Fun 𝑇)
65 funrel 6519 . . . . . . . . 9 (Fun 𝑇 → Rel 𝑇)
6658, 64, 653syl 18 . . . . . . . 8 ((𝐵 No 𝐵𝑉𝑍 No ) → Rel 𝑇)
6766ad2antrl 727 . . . . . . 7 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → Rel 𝑇)
68 resdm 5983 . . . . . . 7 (Rel 𝑇 → (𝑇 ↾ dom 𝑇) = 𝑇)
6967, 68syl 17 . . . . . 6 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → (𝑇 ↾ dom 𝑇) = 𝑇)
7069, 59eqeltrd 2834 . . . . 5 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → (𝑇 ↾ dom 𝑇) ∈ No )
71 resdmss 6188 . . . . . 6 dom (𝑍 ↾ dom 𝑇) ⊆ dom 𝑇
7271a1i 11 . . . . 5 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → dom (𝑍 ↾ dom 𝑇) ⊆ dom 𝑇)
73 resdmss 6188 . . . . . 6 dom (𝑇 ↾ dom 𝑇) ⊆ dom 𝑇
7473a1i 11 . . . . 5 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → dom (𝑇 ↾ dom 𝑇) ⊆ dom 𝑇)
752noinfdm 27083 . . . . . . . . . . 11 (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 → dom 𝑇 = {𝑔 ∣ ∃𝑝𝐵 (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐵𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔)))})
7675eqabd 2877 . . . . . . . . . 10 (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 → (𝑔 ∈ dom 𝑇 ↔ ∃𝑝𝐵 (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐵𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔)))))
7776adantr 482 . . . . . . . . 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 1219 . . . . . . . . . . . . 13 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → 𝐵 No )
8079adantr 482 . . . . . . . . . . . 12 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) ∧ (𝑝𝐵 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐵𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → 𝐵 No )
81 simprl2 1220 . . . . . . . . . . . . 13 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → 𝐵𝑉)
8281adantr 482 . . . . . . . . . . . 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 5110 . . . . . . . . . . . . . . . 16 (𝑞 = 𝑣 → (𝑝 <s 𝑞𝑝 <s 𝑣))
8786notbid 318 . . . . . . . . . . . . . . 15 (𝑞 = 𝑣 → (¬ 𝑝 <s 𝑞 ↔ ¬ 𝑝 <s 𝑣))
88 reseq1 5932 . . . . . . . . . . . . . . . 16 (𝑞 = 𝑣 → (𝑞 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔))
8988eqeq2d 2744 . . . . . . . . . . . . . . 15 (𝑞 = 𝑣 → ((𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔) ↔ (𝑝 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)))
9087, 89imbi12d 345 . . . . . . . . . . . . . 14 (𝑞 = 𝑣 → ((¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔)) ↔ (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔))))
9190cbvralvw 3224 . . . . . . . . . . . . 13 (∀𝑞𝐵𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔)) ↔ ∀𝑣𝐵𝑝 <s 𝑣 → (𝑝 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)))
9285, 91sylib 217 . . . . . . . . . . . 12 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) ∧ (𝑝𝐵 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐵𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → ∀𝑣𝐵𝑝 <s 𝑣 → (𝑝 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)))
932noinfres 27086 . . . . . . . . . . . 12 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑝𝐵𝑔 ∈ dom 𝑝 ∧ ∀𝑣𝐵𝑝 <s 𝑣 → (𝑝 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)))) → (𝑇 ↾ suc 𝑔) = (𝑝 ↾ suc 𝑔))
9478, 80, 82, 83, 84, 92, 93syl123anc 1388 . . . . . . . . . . 11 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) ∧ (𝑝𝐵 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐵𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → (𝑇 ↾ suc 𝑔) = (𝑝 ↾ suc 𝑔))
95 breq2 5110 . . . . . . . . . . . . . 14 (𝑏 = 𝑝 → (𝑍 <s 𝑏𝑍 <s 𝑝))
96 simplrr 777 . . . . . . . . . . . . . 14 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) ∧ (𝑝𝐵 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐵𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → ∀𝑏𝐵 𝑍 <s 𝑏)
9795, 96, 83rspcdva 3581 . . . . . . . . . . . . 13 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) ∧ (𝑝𝐵 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐵𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → 𝑍 <s 𝑝)
9856adantr 482 . . . . . . . . . . . . . 14 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) ∧ (𝑝𝐵 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐵𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → 𝑍 No )
9980, 83sseldd 3946 . . . . . . . . . . . . . 14 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) ∧ (𝑝𝐵 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐵𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → 𝑝 No )
100 sltso 27040 . . . . . . . . . . . . . . 15 <s Or No
101 soasym 5577 . . . . . . . . . . . . . . 15 (( <s Or No ∧ (𝑍 No 𝑝 No )) → (𝑍 <s 𝑝 → ¬ 𝑝 <s 𝑍))
102100, 101mpan 689 . . . . . . . . . . . . . 14 ((𝑍 No 𝑝 No ) → (𝑍 <s 𝑝 → ¬ 𝑝 <s 𝑍))
10398, 99, 102syl2anc 585 . . . . . . . . . . . . 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 27014 . . . . . . . . . . . . . . . 16 (𝑝 No → dom 𝑝 ∈ On)
10699, 105syl 17 . . . . . . . . . . . . . . 15 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) ∧ (𝑝𝐵 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐵𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → dom 𝑝 ∈ On)
107 onelon 6343 . . . . . . . . . . . . . . 15 ((dom 𝑝 ∈ On ∧ 𝑔 ∈ dom 𝑝) → 𝑔 ∈ On)
108106, 84, 107syl2anc 585 . . . . . . . . . . . . . 14 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) ∧ (𝑝𝐵 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐵𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → 𝑔 ∈ On)
109 onsucb 7753 . . . . . . . . . . . . . 14 (𝑔 ∈ On ↔ suc 𝑔 ∈ On)
110108, 109sylib 217 . . . . . . . . . . . . 13 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) ∧ (𝑝𝐵 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐵𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → suc 𝑔 ∈ On)
111 sltres 27026 . . . . . . . . . . . . 13 ((𝑝 No 𝑍 No ∧ suc 𝑔 ∈ On) → ((𝑝 ↾ suc 𝑔) <s (𝑍 ↾ suc 𝑔) → 𝑝 <s 𝑍))
11299, 98, 110, 111syl3anc 1372 . . . . . . . . . . . 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 5124 . . . . . . . . . 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 408 . . . . . . 7 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) ∧ 𝑔 ∈ dom 𝑇) → ¬ (𝑇 ↾ suc 𝑔) <s (𝑍 ↾ suc 𝑔))
118 nodmord 27017 . . . . . . . . . . 11 (𝑇 No → Ord dom 𝑇)
119 ordsucss 7754 . . . . . . . . . . 11 (Ord dom 𝑇 → (𝑔 ∈ dom 𝑇 → suc 𝑔 ⊆ dom 𝑇))
12059, 118, 1193syl 18 . . . . . . . . . 10 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → (𝑔 ∈ dom 𝑇 → suc 𝑔 ⊆ dom 𝑇))
121120imp 408 . . . . . . . . 9 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) ∧ 𝑔 ∈ dom 𝑇) → suc 𝑔 ⊆ dom 𝑇)
122121resabs1d 5969 . . . . . . . 8 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) ∧ 𝑔 ∈ dom 𝑇) → ((𝑇 ↾ dom 𝑇) ↾ suc 𝑔) = (𝑇 ↾ suc 𝑔))
123121resabs1d 5969 . . . . . . . 8 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) ∧ 𝑔 ∈ dom 𝑇) → ((𝑍 ↾ dom 𝑇) ↾ suc 𝑔) = (𝑍 ↾ suc 𝑔))
124122, 123breq12d 5119 . . . . . . 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 27061 . . . . 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 1378 . . . 4 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → ¬ (𝑇 ↾ dom 𝑇) <s (𝑍 ↾ dom 𝑇))
12969breq1d 5116 . . . 4 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 No 𝐵𝑉𝑍 No ) ∧ ∀𝑏𝐵 𝑍 <s 𝑏)) → ((𝑇 ↾ dom 𝑇) <s (𝑍 ↾ dom 𝑇) ↔ 𝑇 <s (𝑍 ↾ dom 𝑇)))
130128, 129mtbid 324 . . 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 1213 . . . . . 6 ((((𝐵 No 𝐵𝑉𝑍 No ) ∧ ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)) ∧ 𝑏𝐵) → 𝐵 No )
134 simpll2 1214 . . . . . 6 ((((𝐵 No 𝐵𝑉𝑍 No ) ∧ ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)) ∧ 𝑏𝐵) → 𝐵𝑉)
135 simpr 486 . . . . . 6 ((((𝐵 No 𝐵𝑉𝑍 No ) ∧ ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)) ∧ 𝑏𝐵) → 𝑏𝐵)
1362noinfbnd1 27093 . . . . . 6 ((𝐵 No 𝐵𝑉𝑏𝐵) → 𝑇 <s (𝑏 ↾ dom 𝑇))
137133, 134, 135, 136syl3anc 1372 . . . . 5 ((((𝐵 No 𝐵𝑉𝑍 No ) ∧ ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)) ∧ 𝑏𝐵) → 𝑇 <s (𝑏 ↾ dom 𝑇))
138 simpl3 1194 . . . . . . . 8 (((𝐵 No 𝐵𝑉𝑍 No ) ∧ ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)) → 𝑍 No )
139 simpl1 1192 . . . . . . . . . 10 (((𝐵 No 𝐵𝑉𝑍 No ) ∧ ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)) → 𝐵 No )
140 simpl2 1193 . . . . . . . . . 10 (((𝐵 No 𝐵𝑉𝑍 No ) ∧ ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)) → 𝐵𝑉)
141139, 140, 57syl2anc 585 . . . . . . . . 9 (((𝐵 No 𝐵𝑉𝑍 No ) ∧ ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)) → 𝑇 No )
142141, 60syl 17 . . . . . . . 8 (((𝐵 No 𝐵𝑉𝑍 No ) ∧ ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)) → dom 𝑇 ∈ On)
143138, 142, 62syl2anc 585 . . . . . . 7 (((𝐵 No 𝐵𝑉𝑍 No ) ∧ ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)) → (𝑍 ↾ dom 𝑇) ∈ No )
144143adantr 482 . . . . . 6 ((((𝐵 No 𝐵𝑉𝑍 No ) ∧ ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)) ∧ 𝑏𝐵) → (𝑍 ↾ dom 𝑇) ∈ No )
145141adantr 482 . . . . . 6 ((((𝐵 No 𝐵𝑉𝑍 No ) ∧ ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)) ∧ 𝑏𝐵) → 𝑇 No )
146139sselda 3945 . . . . . . 7 ((((𝐵 No 𝐵𝑉𝑍 No ) ∧ ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)) ∧ 𝑏𝐵) → 𝑏 No )
147142adantr 482 . . . . . . 7 ((((𝐵 No 𝐵𝑉𝑍 No ) ∧ ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)) ∧ 𝑏𝐵) → dom 𝑇 ∈ On)
148 noreson 27024 . . . . . . 7 ((𝑏 No ∧ dom 𝑇 ∈ On) → (𝑏 ↾ dom 𝑇) ∈ No )
149146, 147, 148syl2anc 585 . . . . . 6 ((((𝐵 No 𝐵𝑉𝑍 No ) ∧ ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)) ∧ 𝑏𝐵) → (𝑏 ↾ dom 𝑇) ∈ No )
150 sotr2 5578 . . . . . . 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 1372 . . . . 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 1215 . . . . 5 ((((𝐵 No 𝐵𝑉𝑍 No ) ∧ ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)) ∧ 𝑏𝐵) → 𝑍 No )
155 sltres 27026 . . . . 5 ((𝑍 No 𝑏 No ∧ dom 𝑇 ∈ On) → ((𝑍 ↾ dom 𝑇) <s (𝑏 ↾ dom 𝑇) → 𝑍 <s 𝑏))
156154, 146, 147, 155syl3anc 1372 . . . 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 800 1 ((𝐵 No 𝐵𝑉𝑍 No ) → (∀𝑏𝐵 𝑍 <s 𝑏 ↔ ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 397  w3a 1088   = wceq 1542  wcel 2107  {cab 2710  wral 3061  wrex 3070  ∃!wreu 3350  ∃*wrmo 3351  cun 3909  wss 3911  ifcif 4487  {csn 4587  cop 4593   class class class wbr 5106  cmpt 5189   Or wor 5545  dom cdm 5634  cres 5636  Rel wrel 5639  Ord word 6317  Oncon0 6318  suc csuc 6320  cio 6447  Fun wfun 6491  cfv 6497  crio 7313  1oc1o 8406   No csur 27004   <s cslt 27005
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5243  ax-sep 5257  ax-nul 5264  ax-pr 5385  ax-un 7673
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2941  df-ral 3062  df-rex 3071  df-rmo 3352  df-reu 3353  df-rab 3407  df-v 3446  df-sbc 3741  df-csb 3857  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3930  df-nul 4284  df-if 4488  df-pw 4563  df-sn 4588  df-pr 4590  df-tp 4592  df-op 4594  df-uni 4867  df-int 4909  df-iun 4957  df-br 5107  df-opab 5169  df-mpt 5190  df-tr 5224  df-id 5532  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5589  df-we 5591  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-ord 6321  df-on 6322  df-suc 6324  df-iota 6449  df-fun 6499  df-fn 6500  df-f 6501  df-f1 6502  df-fo 6503  df-f1o 6504  df-fv 6505  df-riota 7314  df-1o 8413  df-2o 8414  df-no 27007  df-slt 27008  df-bday 27009
This theorem is referenced by:  nosupinfsep  27096  noetainflem4  27104
  Copyright terms: Public domain W3C validator