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

Theorem noinfbnd1 27617
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 1191 . . . . . 6 ((∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉𝑈𝐵)) → 𝐵 No )
2 simpl 482 . . . . . . . 8 ((∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉𝑈𝐵)) → ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)
3 nominmo 27587 . . . . . . . . 9 (𝐵 No → ∃*𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)
41, 3syl 17 . . . . . . . 8 ((∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉𝑈𝐵)) → ∃*𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)
5 reu5 3372 . . . . . . . 8 (∃!𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ↔ (∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ∃*𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥))
62, 4, 5sylanbrc 582 . . . . . . 7 ((∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉𝑈𝐵)) → ∃!𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)
7 riotacl 7379 . . . . . . 7 (∃!𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 → (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∈ 𝐵)
86, 7syl 17 . . . . . 6 ((∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉𝑈𝐵)) → (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∈ 𝐵)
91, 8sseldd 3978 . . . . 5 ((∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉𝑈𝐵)) → (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∈ No )
10 noextendlt 27557 . . . . 5 ((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∈ No → ((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩}) <s (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥))
119, 10syl 17 . . . 4 ((∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉𝑈𝐵)) → ((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩}) <s (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥))
12 simpr3 1193 . . . . . 6 ((∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉𝑈𝐵)) → 𝑈𝐵)
13 nfv 1909 . . . . . . . . 9 𝑥(𝐵 No 𝐵𝑉𝑈𝐵)
14 nfcv 2897 . . . . . . . . . 10 𝑥𝐵
15 nfcv 2897 . . . . . . . . . . . 12 𝑥𝑦
16 nfcv 2897 . . . . . . . . . . . 12 𝑥 <s
17 nfriota1 7368 . . . . . . . . . . . 12 𝑥(𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)
1815, 16, 17nfbr 5188 . . . . . . . . . . 11 𝑥 𝑦 <s (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)
1918nfn 1852 . . . . . . . . . 10 𝑥 ¬ 𝑦 <s (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)
2014, 19nfralw 3302 . . . . . . . . 9 𝑥𝑦𝐵 ¬ 𝑦 <s (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)
2113, 20nfim 1891 . . . . . . . 8 𝑥((𝐵 No 𝐵𝑉𝑈𝐵) → ∀𝑦𝐵 ¬ 𝑦 <s (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥))
22 simpl 482 . . . . . . . . . . 11 (((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) ∧ (𝐵 No 𝐵𝑉𝑈𝐵)) → (𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥))
23 rspe 3240 . . . . . . . . . . . . . 14 ((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) → ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)
2423adantr 480 . . . . . . . . . . . . 13 (((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) ∧ (𝐵 No 𝐵𝑉𝑈𝐵)) → ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)
25 simpr1 1191 . . . . . . . . . . . . . 14 (((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) ∧ (𝐵 No 𝐵𝑉𝑈𝐵)) → 𝐵 No )
2625, 3syl 17 . . . . . . . . . . . . 13 (((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) ∧ (𝐵 No 𝐵𝑉𝑈𝐵)) → ∃*𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)
2724, 26, 5sylanbrc 582 . . . . . . . . . . . 12 (((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) ∧ (𝐵 No 𝐵𝑉𝑈𝐵)) → ∃!𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)
28 riota1 7383 . . . . . . . . . . . 12 (∃!𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 → ((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) ↔ (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) = 𝑥))
2927, 28syl 17 . . . . . . . . . . 11 (((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) ∧ (𝐵 No 𝐵𝑉𝑈𝐵)) → ((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) ↔ (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) = 𝑥))
3022, 29mpbid 231 . . . . . . . . . 10 (((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) ∧ (𝐵 No 𝐵𝑉𝑈𝐵)) → (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) = 𝑥)
31 simplr 766 . . . . . . . . . 10 (((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) ∧ (𝐵 No 𝐵𝑉𝑈𝐵)) → ∀𝑦𝐵 ¬ 𝑦 <s 𝑥)
32 nfra1 3275 . . . . . . . . . . . . . 14 𝑦𝑦𝐵 ¬ 𝑦 <s 𝑥
33 nfcv 2897 . . . . . . . . . . . . . 14 𝑦𝐵
3432, 33nfriota 7374 . . . . . . . . . . . . 13 𝑦(𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)
3534nfeq1 2912 . . . . . . . . . . . 12 𝑦(𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) = 𝑥
36 breq2 5145 . . . . . . . . . . . . 13 ((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) = 𝑥 → (𝑦 <s (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ↔ 𝑦 <s 𝑥))
3736notbid 318 . . . . . . . . . . . 12 ((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) = 𝑥 → (¬ 𝑦 <s (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ↔ ¬ 𝑦 <s 𝑥))
3835, 37ralbid 3264 . . . . . . . . . . 11 ((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) = 𝑥 → (∀𝑦𝐵 ¬ 𝑦 <s (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ↔ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥))
3938biimprd 247 . . . . . . . . . 10 ((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) = 𝑥 → (∀𝑦𝐵 ¬ 𝑦 <s 𝑥 → ∀𝑦𝐵 ¬ 𝑦 <s (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)))
4030, 31, 39sylc 65 . . . . . . . . 9 (((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) ∧ (𝐵 No 𝐵𝑉𝑈𝐵)) → ∀𝑦𝐵 ¬ 𝑦 <s (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥))
4140exp31 419 . . . . . . . 8 (𝑥𝐵 → (∀𝑦𝐵 ¬ 𝑦 <s 𝑥 → ((𝐵 No 𝐵𝑉𝑈𝐵) → ∀𝑦𝐵 ¬ 𝑦 <s (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥))))
4221, 41rexlimi 3250 . . . . . . 7 (∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 → ((𝐵 No 𝐵𝑉𝑈𝐵) → ∀𝑦𝐵 ¬ 𝑦 <s (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)))
4342imp 406 . . . . . 6 ((∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉𝑈𝐵)) → ∀𝑦𝐵 ¬ 𝑦 <s (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥))
44 nfcv 2897 . . . . . . . . 9 𝑦𝑈
45 nfcv 2897 . . . . . . . . 9 𝑦 <s
4644, 45, 34nfbr 5188 . . . . . . . 8 𝑦 𝑈 <s (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)
4746nfn 1852 . . . . . . 7 𝑦 ¬ 𝑈 <s (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)
48 breq1 5144 . . . . . . . 8 (𝑦 = 𝑈 → (𝑦 <s (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ↔ 𝑈 <s (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)))
4948notbid 318 . . . . . . 7 (𝑦 = 𝑈 → (¬ 𝑦 <s (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ↔ ¬ 𝑈 <s (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)))
5047, 49rspc 3594 . . . . . 6 (𝑈𝐵 → (∀𝑦𝐵 ¬ 𝑦 <s (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) → ¬ 𝑈 <s (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)))
5112, 43, 50sylc 65 . . . . 5 ((∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉𝑈𝐵)) → ¬ 𝑈 <s (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥))
52 nofun 27537 . . . . . . . . 9 ((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∈ No → Fun (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥))
53 funrel 6559 . . . . . . . . 9 (Fun (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) → Rel (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥))
549, 52, 533syl 18 . . . . . . . 8 ((∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉𝑈𝐵)) → Rel (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥))
55 sssucid 6438 . . . . . . . 8 dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ⊆ suc dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)
56 relssres 6016 . . . . . . . 8 ((Rel (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∧ dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ⊆ suc dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)) → ((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ↾ suc dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)) = (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥))
5754, 55, 56sylancl 585 . . . . . . 7 ((∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉𝑈𝐵)) → ((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ↾ suc dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)) = (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥))
5857breq2d 5153 . . . . . 6 ((∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉𝑈𝐵)) → ((𝑈 ↾ suc dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)) <s ((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ↾ suc dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)) ↔ (𝑈 ↾ suc dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)) <s (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)))
591, 12sseldd 3978 . . . . . . 7 ((∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉𝑈𝐵)) → 𝑈 No )
60 nodmon 27538 . . . . . . . . 9 ((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∈ No → dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∈ On)
619, 60syl 17 . . . . . . . 8 ((∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉𝑈𝐵)) → dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∈ On)
62 onsucb 7802 . . . . . . . 8 (dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∈ On ↔ suc dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∈ On)
6361, 62sylib 217 . . . . . . 7 ((∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉𝑈𝐵)) → suc dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∈ On)
64 sltres 27550 . . . . . . 7 ((𝑈 No ∧ (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∈ No ∧ suc dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∈ On) → ((𝑈 ↾ suc dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)) <s ((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ↾ suc dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)) → 𝑈 <s (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)))
6559, 9, 63, 64syl3anc 1368 . . . . . 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 8477 . . . . . . . 8 1o ∈ V
6968prid1 4761 . . . . . . 7 1o ∈ {1o, 2o}
7069noextend 27554 . . . . . 6 ((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∈ No → ((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩}) ∈ No )
719, 70syl 17 . . . . 5 ((∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉𝑈𝐵)) → ((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩}) ∈ No )
72 noreson 27548 . . . . . 6 ((𝑈 No ∧ suc dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∈ On) → (𝑈 ↾ suc dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)) ∈ No )
7359, 63, 72syl2anc 583 . . . . 5 ((∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉𝑈𝐵)) → (𝑈 ↾ suc dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)) ∈ No )
74 sltso 27564 . . . . . 6 <s Or No
75 sotr3 5620 . . . . . 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 687 . . . . 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 1368 . . . 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 696 . . 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 4529 . . . . 5 (∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 → if(∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥, ((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥)))) = ((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩}))
8179, 80eqtrid 2778 . . . 4 (∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥𝑇 = ((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩}))
8281adantr 480 . . 3 ((∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉𝑈𝐵)) → 𝑇 = ((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩}))
8381dmeqd 5899 . . . . . 6 (∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 → dom 𝑇 = dom ((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩}))
8468dmsnop 6209 . . . . . . . 8 dom {⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩} = {dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)}
8584uneq2i 4155 . . . . . . 7 (dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∪ dom {⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩}) = (dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∪ {dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)})
86 dmun 5904 . . . . . . 7 dom ((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩}) = (dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∪ dom {⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩})
87 df-suc 6364 . . . . . . 7 suc dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) = (dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∪ {dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)})
8885, 86, 873eqtr4i 2764 . . . . . 6 dom ((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩}) = suc dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)
8983, 88eqtrdi 2782 . . . . 5 (∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 → dom 𝑇 = suc dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥))
9089reseq2d 5975 . . . 4 (∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 → (𝑈 ↾ dom 𝑇) = (𝑈 ↾ suc dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)))
9190adantr 480 . . 3 ((∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉𝑈𝐵)) → (𝑈 ↾ dom 𝑇) = (𝑈 ↾ suc dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)))
9278, 82, 913brtr4d 5173 . 2 ((∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉𝑈𝐵)) → 𝑇 <s (𝑈 ↾ dom 𝑇))
93 simpl 482 . . 3 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉𝑈𝐵)) → ¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)
94 simpr1 1191 . . 3 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉𝑈𝐵)) → 𝐵 No )
95 simpr2 1192 . . 3 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉𝑈𝐵)) → 𝐵𝑉)
96 simpr3 1193 . . 3 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉𝑈𝐵)) → 𝑈𝐵)
9779noinfbnd1lem6 27616 . . 3 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) → 𝑇 <s (𝑈 ↾ dom 𝑇))
9893, 94, 95, 96, 97syl121anc 1372 . 2 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉𝑈𝐵)) → 𝑇 <s (𝑈 ↾ dom 𝑇))
9992, 98pm2.61ian 809 1 ((𝐵 No 𝐵𝑉𝑈𝐵) → 𝑇 <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  Oncon0 6358  suc csuc 6360  cio 6487  Fun wfun 6531  cfv 6537  crio 7360  1oc1o 8460  2oc2o 8461   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:  noinfbnd2  27619  noetainflem3  27627
  Copyright terms: Public domain W3C validator