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

Theorem noinfbnd1 27575
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 1193 . . . . . 6 ((∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉𝑈𝐵)) → 𝐵 No )
2 simpl 482 . . . . . . . 8 ((∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉𝑈𝐵)) → ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)
3 nominmo 27545 . . . . . . . . 9 (𝐵 No → ∃*𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)
41, 3syl 17 . . . . . . . 8 ((∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉𝑈𝐵)) → ∃*𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)
5 reu5 3377 . . . . . . . 8 (∃!𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ↔ (∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ ∃*𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥))
62, 4, 5sylanbrc 582 . . . . . . 7 ((∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉𝑈𝐵)) → ∃!𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)
7 riotacl 7386 . . . . . . 7 (∃!𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 → (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∈ 𝐵)
86, 7syl 17 . . . . . 6 ((∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉𝑈𝐵)) → (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∈ 𝐵)
91, 8sseldd 3983 . . . . 5 ((∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉𝑈𝐵)) → (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∈ No )
10 noextendlt 27515 . . . . 5 ((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∈ No → ((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩}) <s (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥))
119, 10syl 17 . . . 4 ((∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉𝑈𝐵)) → ((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩}) <s (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥))
12 simpr3 1195 . . . . . 6 ((∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉𝑈𝐵)) → 𝑈𝐵)
13 nfv 1916 . . . . . . . . 9 𝑥(𝐵 No 𝐵𝑉𝑈𝐵)
14 nfcv 2902 . . . . . . . . . 10 𝑥𝐵
15 nfcv 2902 . . . . . . . . . . . 12 𝑥𝑦
16 nfcv 2902 . . . . . . . . . . . 12 𝑥 <s
17 nfriota1 7375 . . . . . . . . . . . 12 𝑥(𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)
1815, 16, 17nfbr 5195 . . . . . . . . . . 11 𝑥 𝑦 <s (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)
1918nfn 1859 . . . . . . . . . 10 𝑥 ¬ 𝑦 <s (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)
2014, 19nfralw 3307 . . . . . . . . 9 𝑥𝑦𝐵 ¬ 𝑦 <s (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)
2113, 20nfim 1898 . . . . . . . 8 𝑥((𝐵 No 𝐵𝑉𝑈𝐵) → ∀𝑦𝐵 ¬ 𝑦 <s (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥))
22 simpl 482 . . . . . . . . . . 11 (((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) ∧ (𝐵 No 𝐵𝑉𝑈𝐵)) → (𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥))
23 rspe 3245 . . . . . . . . . . . . . 14 ((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) → ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)
2423adantr 480 . . . . . . . . . . . . 13 (((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) ∧ (𝐵 No 𝐵𝑉𝑈𝐵)) → ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)
25 simpr1 1193 . . . . . . . . . . . . . 14 (((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) ∧ (𝐵 No 𝐵𝑉𝑈𝐵)) → 𝐵 No )
2625, 3syl 17 . . . . . . . . . . . . 13 (((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) ∧ (𝐵 No 𝐵𝑉𝑈𝐵)) → ∃*𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)
2724, 26, 5sylanbrc 582 . . . . . . . . . . . 12 (((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦 <s 𝑥) ∧ (𝐵 No 𝐵𝑉𝑈𝐵)) → ∃!𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)
28 riota1 7390 . . . . . . . . . . . 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 3280 . . . . . . . . . . . . . 14 𝑦𝑦𝐵 ¬ 𝑦 <s 𝑥
33 nfcv 2902 . . . . . . . . . . . . . 14 𝑦𝐵
3432, 33nfriota 7381 . . . . . . . . . . . . 13 𝑦(𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)
3534nfeq1 2917 . . . . . . . . . . . 12 𝑦(𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) = 𝑥
36 breq2 5152 . . . . . . . . . . . . 13 ((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) = 𝑥 → (𝑦 <s (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ↔ 𝑦 <s 𝑥))
3736notbid 318 . . . . . . . . . . . 12 ((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) = 𝑥 → (¬ 𝑦 <s (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ↔ ¬ 𝑦 <s 𝑥))
3835, 37ralbid 3269 . . . . . . . . . . 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 3255 . . . . . . 7 (∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 → ((𝐵 No 𝐵𝑉𝑈𝐵) → ∀𝑦𝐵 ¬ 𝑦 <s (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)))
4342imp 406 . . . . . 6 ((∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉𝑈𝐵)) → ∀𝑦𝐵 ¬ 𝑦 <s (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥))
44 nfcv 2902 . . . . . . . . 9 𝑦𝑈
45 nfcv 2902 . . . . . . . . 9 𝑦 <s
4644, 45, 34nfbr 5195 . . . . . . . 8 𝑦 𝑈 <s (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)
4746nfn 1859 . . . . . . 7 𝑦 ¬ 𝑈 <s (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)
48 breq1 5151 . . . . . . . 8 (𝑦 = 𝑈 → (𝑦 <s (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ↔ 𝑈 <s (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)))
4948notbid 318 . . . . . . 7 (𝑦 = 𝑈 → (¬ 𝑦 <s (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ↔ ¬ 𝑈 <s (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)))
5047, 49rspc 3600 . . . . . 6 (𝑈𝐵 → (∀𝑦𝐵 ¬ 𝑦 <s (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) → ¬ 𝑈 <s (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)))
5112, 43, 50sylc 65 . . . . 5 ((∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉𝑈𝐵)) → ¬ 𝑈 <s (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥))
52 nofun 27495 . . . . . . . . 9 ((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∈ No → Fun (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥))
53 funrel 6565 . . . . . . . . 9 (Fun (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) → Rel (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥))
549, 52, 533syl 18 . . . . . . . 8 ((∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉𝑈𝐵)) → Rel (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥))
55 sssucid 6444 . . . . . . . 8 dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ⊆ suc dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)
56 relssres 6022 . . . . . . . 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 5160 . . . . . 6 ((∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉𝑈𝐵)) → ((𝑈 ↾ suc dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)) <s ((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ↾ suc dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)) ↔ (𝑈 ↾ suc dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)) <s (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)))
591, 12sseldd 3983 . . . . . . 7 ((∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉𝑈𝐵)) → 𝑈 No )
60 nodmon 27496 . . . . . . . . 9 ((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∈ No → dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∈ On)
619, 60syl 17 . . . . . . . 8 ((∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉𝑈𝐵)) → dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∈ On)
62 onsucb 7809 . . . . . . . 8 (dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∈ On ↔ suc dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∈ On)
6361, 62sylib 217 . . . . . . 7 ((∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉𝑈𝐵)) → suc dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∈ On)
64 sltres 27508 . . . . . . 7 ((𝑈 No ∧ (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∈ No ∧ suc dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∈ On) → ((𝑈 ↾ suc dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)) <s ((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ↾ suc dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)) → 𝑈 <s (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)))
6559, 9, 63, 64syl3anc 1370 . . . . . 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 8482 . . . . . . . 8 1o ∈ V
6968prid1 4766 . . . . . . 7 1o ∈ {1o, 2o}
7069noextend 27512 . . . . . 6 ((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∈ No → ((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩}) ∈ No )
719, 70syl 17 . . . . 5 ((∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉𝑈𝐵)) → ((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩}) ∈ No )
72 noreson 27506 . . . . . 6 ((𝑈 No ∧ suc dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∈ On) → (𝑈 ↾ suc dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)) ∈ No )
7359, 63, 72syl2anc 583 . . . . 5 ((∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉𝑈𝐵)) → (𝑈 ↾ suc dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)) ∈ No )
74 sltso 27522 . . . . . 6 <s Or No
75 sotr3 5627 . . . . . 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 1370 . . . 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 4534 . . . . 5 (∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 → if(∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥, ((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥)))) = ((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩}))
8179, 80eqtrid 2783 . . . 4 (∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥𝑇 = ((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩}))
8281adantr 480 . . 3 ((∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉𝑈𝐵)) → 𝑇 = ((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩}))
8381dmeqd 5905 . . . . . 6 (∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 → dom 𝑇 = dom ((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩}))
8468dmsnop 6215 . . . . . . . 8 dom {⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩} = {dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)}
8584uneq2i 4160 . . . . . . 7 (dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∪ dom {⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩}) = (dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∪ {dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)})
86 dmun 5910 . . . . . . 7 dom ((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩}) = (dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∪ dom {⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩})
87 df-suc 6370 . . . . . . 7 suc dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) = (dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∪ {dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)})
8885, 86, 873eqtr4i 2769 . . . . . 6 dom ((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩}) = suc dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)
8983, 88eqtrdi 2787 . . . . 5 (∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 → dom 𝑇 = suc dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥))
9089reseq2d 5981 . . . 4 (∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 → (𝑈 ↾ dom 𝑇) = (𝑈 ↾ suc dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)))
9190adantr 480 . . 3 ((∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉𝑈𝐵)) → (𝑈 ↾ dom 𝑇) = (𝑈 ↾ suc dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)))
9278, 82, 913brtr4d 5180 . 2 ((∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉𝑈𝐵)) → 𝑇 <s (𝑈 ↾ dom 𝑇))
93 simpl 482 . . 3 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉𝑈𝐵)) → ¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)
94 simpr1 1193 . . 3 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉𝑈𝐵)) → 𝐵 No )
95 simpr2 1194 . . 3 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉𝑈𝐵)) → 𝐵𝑉)
96 simpr3 1195 . . 3 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉𝑈𝐵)) → 𝑈𝐵)
9779noinfbnd1lem6 27574 . . 3 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) → 𝑇 <s (𝑈 ↾ dom 𝑇))
9893, 94, 95, 96, 97syl121anc 1374 . 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 1086   = wceq 1540  wcel 2105  {cab 2708  wral 3060  wrex 3069  ∃!wreu 3373  ∃*wrmo 3374  cun 3946  wss 3948  ifcif 4528  {csn 4628  cop 4634   class class class wbr 5148  cmpt 5231   Or wor 5587  dom cdm 5676  cres 5678  Rel wrel 5681  Oncon0 6364  suc csuc 6366  cio 6493  Fun wfun 6537  cfv 6543  crio 7367  1oc1o 8465  2oc2o 8466   No csur 27486   <s cslt 27487
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pr 5427  ax-un 7729
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-ral 3061  df-rex 3070  df-rmo 3375  df-reu 3376  df-rab 3432  df-v 3475  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-tp 4633  df-op 4635  df-uni 4909  df-int 4951  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  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 7368  df-1o 8472  df-2o 8473  df-no 27489  df-slt 27490  df-bday 27491
This theorem is referenced by:  noinfbnd2  27577  noetainflem3  27585
  Copyright terms: Public domain W3C validator