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

Theorem nosupbnd1 27598
Description: Bounding law from below for the surreal supremum. Proposition 4.2 of [Lipparini] p. 6. (Contributed by Scott Fenton, 6-Dec-2021.)
Hypothesis
Ref Expression
nosupbnd1.1 𝑆 = if(∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦, ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))))
Assertion
Ref Expression
nosupbnd1 ((𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴) → (𝑈 ↾ dom 𝑆) <s 𝑆)
Distinct variable groups:   𝐴,𝑔,𝑢,𝑣,𝑥,𝑦   𝑢,𝑈,𝑣,𝑥,𝑦
Allowed substitution hints:   𝑆(𝑥,𝑦,𝑣,𝑢,𝑔)   𝑈(𝑔)

Proof of Theorem nosupbnd1
StepHypRef Expression
1 simpr3 1193 . . . . . 6 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → 𝑈𝐴)
2 nfv 1909 . . . . . . . . 9 𝑥(𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)
3 nfcv 2897 . . . . . . . . . 10 𝑥𝐴
4 nfriota1 7367 . . . . . . . . . . . 12 𝑥(𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
5 nfcv 2897 . . . . . . . . . . . 12 𝑥 <s
6 nfcv 2897 . . . . . . . . . . . 12 𝑥𝑦
74, 5, 6nfbr 5188 . . . . . . . . . . 11 𝑥(𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s 𝑦
87nfn 1852 . . . . . . . . . 10 𝑥 ¬ (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s 𝑦
93, 8nfralw 3302 . . . . . . . . 9 𝑥𝑦𝐴 ¬ (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s 𝑦
102, 9nfim 1891 . . . . . . . 8 𝑥((𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴) → ∀𝑦𝐴 ¬ (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s 𝑦)
11 simpl 482 . . . . . . . . . . 11 (((𝑥𝐴 ∧ ∀𝑦𝐴 ¬ 𝑥 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → (𝑥𝐴 ∧ ∀𝑦𝐴 ¬ 𝑥 <s 𝑦))
12 rspe 3240 . . . . . . . . . . . . . 14 ((𝑥𝐴 ∧ ∀𝑦𝐴 ¬ 𝑥 <s 𝑦) → ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
1312adantr 480 . . . . . . . . . . . . 13 (((𝑥𝐴 ∧ ∀𝑦𝐴 ¬ 𝑥 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
14 nomaxmo 27582 . . . . . . . . . . . . . . 15 (𝐴 No → ∃*𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
15143ad2ant1 1130 . . . . . . . . . . . . . 14 ((𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴) → ∃*𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
1615adantl 481 . . . . . . . . . . . . 13 (((𝑥𝐴 ∧ ∀𝑦𝐴 ¬ 𝑥 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → ∃*𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
17 reu5 3372 . . . . . . . . . . . . 13 (∃!𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ↔ (∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ∃*𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦))
1813, 16, 17sylanbrc 582 . . . . . . . . . . . 12 (((𝑥𝐴 ∧ ∀𝑦𝐴 ¬ 𝑥 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → ∃!𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
19 riota1 7382 . . . . . . . . . . . 12 (∃!𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 → ((𝑥𝐴 ∧ ∀𝑦𝐴 ¬ 𝑥 <s 𝑦) ↔ (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) = 𝑥))
2018, 19syl 17 . . . . . . . . . . 11 (((𝑥𝐴 ∧ ∀𝑦𝐴 ¬ 𝑥 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → ((𝑥𝐴 ∧ ∀𝑦𝐴 ¬ 𝑥 <s 𝑦) ↔ (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) = 𝑥))
2111, 20mpbid 231 . . . . . . . . . 10 (((𝑥𝐴 ∧ ∀𝑦𝐴 ¬ 𝑥 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) = 𝑥)
22 simplr 766 . . . . . . . . . 10 (((𝑥𝐴 ∧ ∀𝑦𝐴 ¬ 𝑥 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → ∀𝑦𝐴 ¬ 𝑥 <s 𝑦)
23 nfra1 3275 . . . . . . . . . . . . . 14 𝑦𝑦𝐴 ¬ 𝑥 <s 𝑦
24 nfcv 2897 . . . . . . . . . . . . . 14 𝑦𝐴
2523, 24nfriota 7373 . . . . . . . . . . . . 13 𝑦(𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
26 nfcv 2897 . . . . . . . . . . . . 13 𝑦𝑥
2725, 26nfeq 2910 . . . . . . . . . . . 12 𝑦(𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) = 𝑥
28 breq1 5144 . . . . . . . . . . . . 13 ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) = 𝑥 → ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s 𝑦𝑥 <s 𝑦))
2928notbid 318 . . . . . . . . . . . 12 ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) = 𝑥 → (¬ (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s 𝑦 ↔ ¬ 𝑥 <s 𝑦))
3027, 29ralbid 3264 . . . . . . . . . . 11 ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) = 𝑥 → (∀𝑦𝐴 ¬ (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s 𝑦 ↔ ∀𝑦𝐴 ¬ 𝑥 <s 𝑦))
3130biimprd 247 . . . . . . . . . 10 ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) = 𝑥 → (∀𝑦𝐴 ¬ 𝑥 <s 𝑦 → ∀𝑦𝐴 ¬ (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s 𝑦))
3221, 22, 31sylc 65 . . . . . . . . 9 (((𝑥𝐴 ∧ ∀𝑦𝐴 ¬ 𝑥 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → ∀𝑦𝐴 ¬ (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s 𝑦)
3332exp31 419 . . . . . . . 8 (𝑥𝐴 → (∀𝑦𝐴 ¬ 𝑥 <s 𝑦 → ((𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴) → ∀𝑦𝐴 ¬ (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s 𝑦)))
3410, 33rexlimi 3250 . . . . . . 7 (∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 → ((𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴) → ∀𝑦𝐴 ¬ (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s 𝑦))
3534imp 406 . . . . . 6 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → ∀𝑦𝐴 ¬ (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s 𝑦)
36 nfcv 2897 . . . . . . . . 9 𝑦 <s
37 nfcv 2897 . . . . . . . . 9 𝑦𝑈
3825, 36, 37nfbr 5188 . . . . . . . 8 𝑦(𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s 𝑈
3938nfn 1852 . . . . . . 7 𝑦 ¬ (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s 𝑈
40 breq2 5145 . . . . . . . 8 (𝑦 = 𝑈 → ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s 𝑦 ↔ (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s 𝑈))
4140notbid 318 . . . . . . 7 (𝑦 = 𝑈 → (¬ (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s 𝑦 ↔ ¬ (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s 𝑈))
4239, 41rspc 3594 . . . . . 6 (𝑈𝐴 → (∀𝑦𝐴 ¬ (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s 𝑦 → ¬ (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s 𝑈))
431, 35, 42sylc 65 . . . . 5 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → ¬ (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s 𝑈)
44 simpr1 1191 . . . . . . . . . 10 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → 𝐴 No )
45 simpl 482 . . . . . . . . . . . 12 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
4615adantl 481 . . . . . . . . . . . 12 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → ∃*𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
4745, 46, 17sylanbrc 582 . . . . . . . . . . 11 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → ∃!𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
48 riotacl 7378 . . . . . . . . . . 11 (∃!𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 → (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∈ 𝐴)
4947, 48syl 17 . . . . . . . . . 10 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∈ 𝐴)
5044, 49sseldd 3978 . . . . . . . . 9 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∈ No )
51 nofun 27533 . . . . . . . . 9 ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∈ No → Fun (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦))
52 funrel 6558 . . . . . . . . 9 (Fun (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) → Rel (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦))
5350, 51, 523syl 18 . . . . . . . 8 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → Rel (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦))
54 sssucid 6437 . . . . . . . 8 dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ⊆ suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
55 relssres 6015 . . . . . . . 8 ((Rel (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∧ dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ⊆ suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)) → ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ↾ suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)) = (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦))
5653, 54, 55sylancl 585 . . . . . . 7 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ↾ suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)) = (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦))
5756breq1d 5151 . . . . . 6 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → (((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ↾ suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)) <s (𝑈 ↾ suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)) ↔ (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s (𝑈 ↾ suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦))))
5844, 1sseldd 3978 . . . . . . 7 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → 𝑈 No )
59 nodmon 27534 . . . . . . . . 9 ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∈ No → dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∈ On)
6050, 59syl 17 . . . . . . . 8 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∈ On)
61 onsucb 7801 . . . . . . . 8 (dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∈ On ↔ suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∈ On)
6260, 61sylib 217 . . . . . . 7 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∈ On)
63 sltres 27546 . . . . . . 7 (((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∈ No 𝑈 No ∧ suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∈ On) → (((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ↾ suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)) <s (𝑈 ↾ suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)) → (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s 𝑈))
6450, 58, 62, 63syl3anc 1368 . . . . . 6 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → (((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ↾ suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)) <s (𝑈 ↾ suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)) → (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s 𝑈))
6557, 64sylbird 260 . . . . 5 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s (𝑈 ↾ suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)) → (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s 𝑈))
6643, 65mtod 197 . . . 4 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → ¬ (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s (𝑈 ↾ suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)))
67 noextendgt 27554 . . . . 5 ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∈ No → (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}))
6850, 67syl 17 . . . 4 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}))
69 noreson 27544 . . . . . 6 ((𝑈 No ∧ suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∈ On) → (𝑈 ↾ suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)) ∈ No )
7058, 62, 69syl2anc 583 . . . . 5 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → (𝑈 ↾ suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)) ∈ No )
71 2on 8478 . . . . . . . . 9 2o ∈ On
7271elexi 3488 . . . . . . . 8 2o ∈ V
7372prid2 4762 . . . . . . 7 2o ∈ {1o, 2o}
7473noextend 27550 . . . . . 6 ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∈ No → ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}) ∈ No )
7550, 74syl 17 . . . . 5 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}) ∈ No )
76 sltso 27560 . . . . . 6 <s Or No
77 sotr2 5613 . . . . . 6 (( <s Or No ∧ ((𝑈 ↾ suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)) ∈ No ∧ (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∈ No ∧ ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}) ∈ No )) → ((¬ (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s (𝑈 ↾ suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)) ∧ (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩})) → (𝑈 ↾ suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)) <s ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩})))
7876, 77mpan 687 . . . . 5 (((𝑈 ↾ suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)) ∈ No ∧ (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∈ No ∧ ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}) ∈ No ) → ((¬ (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s (𝑈 ↾ suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)) ∧ (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩})) → (𝑈 ↾ suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)) <s ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩})))
7970, 50, 75, 78syl3anc 1368 . . . 4 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → ((¬ (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s (𝑈 ↾ suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)) ∧ (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩})) → (𝑈 ↾ suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)) <s ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩})))
8066, 68, 79mp2and 696 . . 3 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → (𝑈 ↾ suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)) <s ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}))
81 nosupbnd1.1 . . . . . . . 8 𝑆 = if(∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦, ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))))
82 iftrue 4529 . . . . . . . 8 (∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 → if(∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦, ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥)))) = ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}))
8381, 82eqtrid 2778 . . . . . . 7 (∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦𝑆 = ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}))
8483dmeqd 5898 . . . . . 6 (∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 → dom 𝑆 = dom ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}))
8572dmsnop 6208 . . . . . . . 8 dom {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩} = {dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)}
8685uneq2i 4155 . . . . . . 7 (dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ dom {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}) = (dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)})
87 dmun 5903 . . . . . . 7 dom ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}) = (dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ dom {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩})
88 df-suc 6363 . . . . . . 7 suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) = (dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)})
8986, 87, 883eqtr4i 2764 . . . . . 6 dom ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}) = suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
9084, 89eqtrdi 2782 . . . . 5 (∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 → dom 𝑆 = suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦))
9190adantr 480 . . . 4 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → dom 𝑆 = suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦))
9291reseq2d 5974 . . 3 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → (𝑈 ↾ dom 𝑆) = (𝑈 ↾ suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)))
9383adantr 480 . . 3 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → 𝑆 = ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}))
9480, 92, 933brtr4d 5173 . 2 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → (𝑈 ↾ dom 𝑆) <s 𝑆)
95 simpl 482 . . 3 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → ¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
96 simpr1 1191 . . 3 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → 𝐴 No )
97 simpr2 1192 . . 3 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → 𝐴 ∈ V)
98 simpr3 1193 . . 3 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → 𝑈𝐴)
9981nosupbnd1lem6 27597 . . 3 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) → (𝑈 ↾ dom 𝑆) <s 𝑆)
10095, 96, 97, 98, 99syl121anc 1372 . 2 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → (𝑈 ↾ dom 𝑆) <s 𝑆)
10194, 100pm2.61ian 809 1 ((𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴) → (𝑈 ↾ dom 𝑆) <s 𝑆)
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  Vcvv 3468  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 6357  suc csuc 6359  cio 6486  Fun wfun 6530  cfv 6536  crio 7359  1oc1o 8457  2oc2o 8458   No csur 27524   <s cslt 27525
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 7721
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 6360  df-on 6361  df-suc 6363  df-iota 6488  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-riota 7360  df-1o 8464  df-2o 8465  df-no 27527  df-slt 27528  df-bday 27529
This theorem is referenced by:  nosupbnd2  27600  noetasuplem3  27619
  Copyright terms: Public domain W3C validator