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

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

Proof of Theorem noinfbnd1
StepHypRef Expression
1 simpr1 1195 . . . . . 6 ((∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉𝑈𝐵)) → 𝐵 No )
2 simpl 484 . . . . . . . 8 ((∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉𝑈𝐵)) → ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)
3 nominmo 27070 . . . . . . . . 9 (𝐵 No → ∃*𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)
41, 3syl 17 . . . . . . . 8 ((∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉𝑈𝐵)) → ∃*𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)
5 reu5 3354 . . . . . . . 8 (∃!𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ↔ (∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ∃*𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥))
62, 4, 5sylanbrc 584 . . . . . . 7 ((∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉𝑈𝐵)) → ∃!𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)
7 riotacl 7335 . . . . . . 7 (∃!𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 → (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∈ 𝐵)
86, 7syl 17 . . . . . 6 ((∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉𝑈𝐵)) → (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∈ 𝐵)
91, 8sseldd 3949 . . . . 5 ((∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉𝑈𝐵)) → (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∈ No )
10 noextendlt 27040 . . . . 5 ((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∈ No → ((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩}) <s (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥))
119, 10syl 17 . . . 4 ((∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉𝑈𝐵)) → ((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩}) <s (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥))
12 simpr3 1197 . . . . . 6 ((∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉𝑈𝐵)) → 𝑈𝐵)
13 nfv 1918 . . . . . . . . 9 𝑥(𝐵 No 𝐵𝑉𝑈𝐵)
14 nfcv 2904 . . . . . . . . . 10 𝑥𝐵
15 nfcv 2904 . . . . . . . . . . . 12 𝑥𝑦
16 nfcv 2904 . . . . . . . . . . . 12 𝑥 <s
17 nfriota1 7324 . . . . . . . . . . . 12 𝑥(𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)
1815, 16, 17nfbr 5156 . . . . . . . . . . 11 𝑥 𝑦 <s (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)
1918nfn 1861 . . . . . . . . . 10 𝑥 ¬ 𝑦 <s (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)
2014, 19nfralw 3293 . . . . . . . . 9 𝑥𝑦𝐵 ¬ 𝑦 <s (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)
2113, 20nfim 1900 . . . . . . . 8 𝑥((𝐵 No 𝐵𝑉𝑈𝐵) → ∀𝑦𝐵 ¬ 𝑦 <s (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥))
22 simpl 484 . . . . . . . . . . 11 (((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) ∧ (𝐵 No 𝐵𝑉𝑈𝐵)) → (𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥))
23 rspe 3231 . . . . . . . . . . . . . 14 ((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) → ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)
2423adantr 482 . . . . . . . . . . . . 13 (((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) ∧ (𝐵 No 𝐵𝑉𝑈𝐵)) → ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)
25 simpr1 1195 . . . . . . . . . . . . . 14 (((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) ∧ (𝐵 No 𝐵𝑉𝑈𝐵)) → 𝐵 No )
2625, 3syl 17 . . . . . . . . . . . . 13 (((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) ∧ (𝐵 No 𝐵𝑉𝑈𝐵)) → ∃*𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)
2724, 26, 5sylanbrc 584 . . . . . . . . . . . 12 (((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) ∧ (𝐵 No 𝐵𝑉𝑈𝐵)) → ∃!𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)
28 riota1 7339 . . . . . . . . . . . 12 (∃!𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 → ((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) ↔ (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) = 𝑥))
2927, 28syl 17 . . . . . . . . . . 11 (((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) ∧ (𝐵 No 𝐵𝑉𝑈𝐵)) → ((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) ↔ (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) = 𝑥))
3022, 29mpbid 231 . . . . . . . . . 10 (((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) ∧ (𝐵 No 𝐵𝑉𝑈𝐵)) → (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) = 𝑥)
31 simplr 768 . . . . . . . . . 10 (((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) ∧ (𝐵 No 𝐵𝑉𝑈𝐵)) → ∀𝑦𝐵 ¬ 𝑦 <s 𝑥)
32 nfra1 3266 . . . . . . . . . . . . . 14 𝑦𝑦𝐵 ¬ 𝑦 <s 𝑥
33 nfcv 2904 . . . . . . . . . . . . . 14 𝑦𝐵
3432, 33nfriota 7330 . . . . . . . . . . . . 13 𝑦(𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)
3534nfeq1 2919 . . . . . . . . . . . 12 𝑦(𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) = 𝑥
36 breq2 5113 . . . . . . . . . . . . 13 ((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) = 𝑥 → (𝑦 <s (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ↔ 𝑦 <s 𝑥))
3736notbid 318 . . . . . . . . . . . 12 ((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) = 𝑥 → (¬ 𝑦 <s (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ↔ ¬ 𝑦 <s 𝑥))
3835, 37ralbid 3255 . . . . . . . . . . 11 ((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) = 𝑥 → (∀𝑦𝐵 ¬ 𝑦 <s (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ↔ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥))
3938biimprd 248 . . . . . . . . . 10 ((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) = 𝑥 → (∀𝑦𝐵 ¬ 𝑦 <s 𝑥 → ∀𝑦𝐵 ¬ 𝑦 <s (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)))
4030, 31, 39sylc 65 . . . . . . . . 9 (((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) ∧ (𝐵 No 𝐵𝑉𝑈𝐵)) → ∀𝑦𝐵 ¬ 𝑦 <s (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥))
4140exp31 421 . . . . . . . 8 (𝑥𝐵 → (∀𝑦𝐵 ¬ 𝑦 <s 𝑥 → ((𝐵 No 𝐵𝑉𝑈𝐵) → ∀𝑦𝐵 ¬ 𝑦 <s (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥))))
4221, 41rexlimi 3241 . . . . . . 7 (∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 → ((𝐵 No 𝐵𝑉𝑈𝐵) → ∀𝑦𝐵 ¬ 𝑦 <s (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)))
4342imp 408 . . . . . 6 ((∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉𝑈𝐵)) → ∀𝑦𝐵 ¬ 𝑦 <s (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥))
44 nfcv 2904 . . . . . . . . 9 𝑦𝑈
45 nfcv 2904 . . . . . . . . 9 𝑦 <s
4644, 45, 34nfbr 5156 . . . . . . . 8 𝑦 𝑈 <s (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)
4746nfn 1861 . . . . . . 7 𝑦 ¬ 𝑈 <s (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)
48 breq1 5112 . . . . . . . 8 (𝑦 = 𝑈 → (𝑦 <s (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ↔ 𝑈 <s (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)))
4948notbid 318 . . . . . . 7 (𝑦 = 𝑈 → (¬ 𝑦 <s (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ↔ ¬ 𝑈 <s (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)))
5047, 49rspc 3571 . . . . . 6 (𝑈𝐵 → (∀𝑦𝐵 ¬ 𝑦 <s (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) → ¬ 𝑈 <s (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)))
5112, 43, 50sylc 65 . . . . 5 ((∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉𝑈𝐵)) → ¬ 𝑈 <s (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥))
52 nofun 27020 . . . . . . . . 9 ((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∈ No → Fun (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥))
53 funrel 6522 . . . . . . . . 9 (Fun (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) → Rel (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥))
549, 52, 533syl 18 . . . . . . . 8 ((∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉𝑈𝐵)) → Rel (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥))
55 sssucid 6401 . . . . . . . 8 dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ⊆ suc dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)
56 relssres 5982 . . . . . . . 8 ((Rel (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∧ dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ⊆ suc dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)) → ((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ↾ suc dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)) = (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥))
5754, 55, 56sylancl 587 . . . . . . 7 ((∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉𝑈𝐵)) → ((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ↾ suc dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)) = (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥))
5857breq2d 5121 . . . . . 6 ((∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉𝑈𝐵)) → ((𝑈 ↾ suc dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)) <s ((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ↾ suc dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)) ↔ (𝑈 ↾ suc dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)) <s (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)))
591, 12sseldd 3949 . . . . . . 7 ((∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉𝑈𝐵)) → 𝑈 No )
60 nodmon 27021 . . . . . . . . 9 ((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∈ No → dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∈ On)
619, 60syl 17 . . . . . . . 8 ((∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉𝑈𝐵)) → dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∈ On)
62 onsucb 7756 . . . . . . . 8 (dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∈ On ↔ suc dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∈ On)
6361, 62sylib 217 . . . . . . 7 ((∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉𝑈𝐵)) → suc dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∈ On)
64 sltres 27033 . . . . . . 7 ((𝑈 No ∧ (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∈ No ∧ suc dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∈ On) → ((𝑈 ↾ suc dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)) <s ((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ↾ suc dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)) → 𝑈 <s (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)))
6559, 9, 63, 64syl3anc 1372 . . . . . 6 ((∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉𝑈𝐵)) → ((𝑈 ↾ suc dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)) <s ((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ↾ suc dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)) → 𝑈 <s (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)))
6658, 65sylbird 260 . . . . 5 ((∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉𝑈𝐵)) → ((𝑈 ↾ suc dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)) <s (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) → 𝑈 <s (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)))
6751, 66mtod 197 . . . 4 ((∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉𝑈𝐵)) → ¬ (𝑈 ↾ suc dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)) <s (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥))
68 1oex 8426 . . . . . . . 8 1o ∈ V
6968prid1 4727 . . . . . . 7 1o ∈ {1o, 2o}
7069noextend 27037 . . . . . 6 ((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∈ No → ((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩}) ∈ No )
719, 70syl 17 . . . . 5 ((∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉𝑈𝐵)) → ((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩}) ∈ No )
72 noreson 27031 . . . . . 6 ((𝑈 No ∧ suc dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∈ On) → (𝑈 ↾ suc dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)) ∈ No )
7359, 63, 72syl2anc 585 . . . . 5 ((∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉𝑈𝐵)) → (𝑈 ↾ suc dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)) ∈ No )
74 sltso 27047 . . . . . 6 <s Or No
75 sotr3 5588 . . . . . 6 (( <s Or No ∧ (((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩}) ∈ No ∧ (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∈ No ∧ (𝑈 ↾ suc dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)) ∈ No )) → ((((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩}) <s (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∧ ¬ (𝑈 ↾ suc dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)) <s (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)) → ((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩}) <s (𝑈 ↾ suc dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥))))
7674, 75mpan 689 . . . . 5 ((((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩}) ∈ No ∧ (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∈ No ∧ (𝑈 ↾ suc dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)) ∈ No ) → ((((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩}) <s (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∧ ¬ (𝑈 ↾ suc dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)) <s (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)) → ((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩}) <s (𝑈 ↾ suc dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥))))
7771, 9, 73, 76syl3anc 1372 . . . 4 ((∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉𝑈𝐵)) → ((((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩}) <s (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∧ ¬ (𝑈 ↾ suc dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)) <s (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)) → ((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩}) <s (𝑈 ↾ suc dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥))))
7811, 67, 77mp2and 698 . . 3 ((∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉𝑈𝐵)) → ((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩}) <s (𝑈 ↾ suc dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)))
79 noinfbnd1.1 . . . . 5 𝑇 = if(∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥, ((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))))
80 iftrue 4496 . . . . 5 (∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 → if(∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥, ((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥)))) = ((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩}))
8179, 80eqtrid 2785 . . . 4 (∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥𝑇 = ((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩}))
8281adantr 482 . . 3 ((∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉𝑈𝐵)) → 𝑇 = ((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩}))
8381dmeqd 5865 . . . . . 6 (∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 → dom 𝑇 = dom ((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩}))
8468dmsnop 6172 . . . . . . . 8 dom {⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩} = {dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)}
8584uneq2i 4124 . . . . . . 7 (dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∪ dom {⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩}) = (dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∪ {dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)})
86 dmun 5870 . . . . . . 7 dom ((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩}) = (dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∪ dom {⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩})
87 df-suc 6327 . . . . . . 7 suc dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) = (dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∪ {dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)})
8885, 86, 873eqtr4i 2771 . . . . . 6 dom ((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩}) = suc dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)
8983, 88eqtrdi 2789 . . . . 5 (∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 → dom 𝑇 = suc dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥))
9089reseq2d 5941 . . . 4 (∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 → (𝑈 ↾ dom 𝑇) = (𝑈 ↾ suc dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)))
9190adantr 482 . . 3 ((∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉𝑈𝐵)) → (𝑈 ↾ dom 𝑇) = (𝑈 ↾ suc dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)))
9278, 82, 913brtr4d 5141 . 2 ((∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉𝑈𝐵)) → 𝑇 <s (𝑈 ↾ dom 𝑇))
93 simpl 484 . . 3 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉𝑈𝐵)) → ¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)
94 simpr1 1195 . . 3 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉𝑈𝐵)) → 𝐵 No )
95 simpr2 1196 . . 3 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉𝑈𝐵)) → 𝐵𝑉)
96 simpr3 1197 . . 3 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉𝑈𝐵)) → 𝑈𝐵)
9779noinfbnd1lem6 27099 . . 3 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) → 𝑇 <s (𝑈 ↾ dom 𝑇))
9893, 94, 95, 96, 97syl121anc 1376 . 2 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉𝑈𝐵)) → 𝑇 <s (𝑈 ↾ dom 𝑇))
9992, 98pm2.61ian 811 1 ((𝐵 No 𝐵𝑉𝑈𝐵) → 𝑇 <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 3912  wss 3914  ifcif 4490  {csn 4590  cop 4596   class class class wbr 5109  cmpt 5192   Or wor 5548  dom cdm 5637  cres 5639  Rel wrel 5642  Oncon0 6321  suc csuc 6323  cio 6450  Fun wfun 6494  cfv 6500  crio 7316  1oc1o 8409  2oc2o 8410   No csur 27011   <s cslt 27012
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 5246  ax-sep 5260  ax-nul 5267  ax-pr 5388  ax-un 7676
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 3449  df-sbc 3744  df-csb 3860  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-pss 3933  df-nul 4287  df-if 4491  df-pw 4566  df-sn 4591  df-pr 4593  df-tp 4595  df-op 4597  df-uni 4870  df-int 4912  df-iun 4960  df-br 5110  df-opab 5172  df-mpt 5193  df-tr 5227  df-id 5535  df-eprel 5541  df-po 5549  df-so 5550  df-fr 5592  df-we 5594  df-xp 5643  df-rel 5644  df-cnv 5645  df-co 5646  df-dm 5647  df-rn 5648  df-res 5649  df-ima 5650  df-ord 6324  df-on 6325  df-suc 6327  df-iota 6452  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-riota 7317  df-1o 8416  df-2o 8417  df-no 27014  df-slt 27015  df-bday 27016
This theorem is referenced by:  noinfbnd2  27102  noetainflem3  27110
  Copyright terms: Public domain W3C validator