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

Theorem nosupbnd1 27085
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 1197 . . . . . 6 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → 𝑈𝐴)
2 nfv 1918 . . . . . . . . 9 𝑥(𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)
3 nfcv 2904 . . . . . . . . . 10 𝑥𝐴
4 nfriota1 7324 . . . . . . . . . . . 12 𝑥(𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
5 nfcv 2904 . . . . . . . . . . . 12 𝑥 <s
6 nfcv 2904 . . . . . . . . . . . 12 𝑥𝑦
74, 5, 6nfbr 5156 . . . . . . . . . . 11 𝑥(𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s 𝑦
87nfn 1861 . . . . . . . . . 10 𝑥 ¬ (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s 𝑦
93, 8nfralw 3293 . . . . . . . . 9 𝑥𝑦𝐴 ¬ (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s 𝑦
102, 9nfim 1900 . . . . . . . 8 𝑥((𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴) → ∀𝑦𝐴 ¬ (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s 𝑦)
11 simpl 484 . . . . . . . . . . 11 (((𝑥𝐴 ∧ ∀𝑦𝐴 ¬ 𝑥 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → (𝑥𝐴 ∧ ∀𝑦𝐴 ¬ 𝑥 <s 𝑦))
12 rspe 3231 . . . . . . . . . . . . . 14 ((𝑥𝐴 ∧ ∀𝑦𝐴 ¬ 𝑥 <s 𝑦) → ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
1312adantr 482 . . . . . . . . . . . . 13 (((𝑥𝐴 ∧ ∀𝑦𝐴 ¬ 𝑥 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
14 nomaxmo 27069 . . . . . . . . . . . . . . 15 (𝐴 No → ∃*𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
15143ad2ant1 1134 . . . . . . . . . . . . . 14 ((𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴) → ∃*𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
1615adantl 483 . . . . . . . . . . . . 13 (((𝑥𝐴 ∧ ∀𝑦𝐴 ¬ 𝑥 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → ∃*𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
17 reu5 3354 . . . . . . . . . . . . 13 (∃!𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ↔ (∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ∃*𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦))
1813, 16, 17sylanbrc 584 . . . . . . . . . . . 12 (((𝑥𝐴 ∧ ∀𝑦𝐴 ¬ 𝑥 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → ∃!𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
19 riota1 7339 . . . . . . . . . . . 12 (∃!𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 → ((𝑥𝐴 ∧ ∀𝑦𝐴 ¬ 𝑥 <s 𝑦) ↔ (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) = 𝑥))
2018, 19syl 17 . . . . . . . . . . 11 (((𝑥𝐴 ∧ ∀𝑦𝐴 ¬ 𝑥 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → ((𝑥𝐴 ∧ ∀𝑦𝐴 ¬ 𝑥 <s 𝑦) ↔ (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) = 𝑥))
2111, 20mpbid 231 . . . . . . . . . 10 (((𝑥𝐴 ∧ ∀𝑦𝐴 ¬ 𝑥 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) = 𝑥)
22 simplr 768 . . . . . . . . . 10 (((𝑥𝐴 ∧ ∀𝑦𝐴 ¬ 𝑥 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → ∀𝑦𝐴 ¬ 𝑥 <s 𝑦)
23 nfra1 3266 . . . . . . . . . . . . . 14 𝑦𝑦𝐴 ¬ 𝑥 <s 𝑦
24 nfcv 2904 . . . . . . . . . . . . . 14 𝑦𝐴
2523, 24nfriota 7330 . . . . . . . . . . . . 13 𝑦(𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
26 nfcv 2904 . . . . . . . . . . . . 13 𝑦𝑥
2725, 26nfeq 2917 . . . . . . . . . . . 12 𝑦(𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) = 𝑥
28 breq1 5112 . . . . . . . . . . . . 13 ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) = 𝑥 → ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s 𝑦𝑥 <s 𝑦))
2928notbid 318 . . . . . . . . . . . 12 ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) = 𝑥 → (¬ (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s 𝑦 ↔ ¬ 𝑥 <s 𝑦))
3027, 29ralbid 3255 . . . . . . . . . . 11 ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) = 𝑥 → (∀𝑦𝐴 ¬ (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s 𝑦 ↔ ∀𝑦𝐴 ¬ 𝑥 <s 𝑦))
3130biimprd 248 . . . . . . . . . 10 ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) = 𝑥 → (∀𝑦𝐴 ¬ 𝑥 <s 𝑦 → ∀𝑦𝐴 ¬ (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s 𝑦))
3221, 22, 31sylc 65 . . . . . . . . 9 (((𝑥𝐴 ∧ ∀𝑦𝐴 ¬ 𝑥 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → ∀𝑦𝐴 ¬ (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s 𝑦)
3332exp31 421 . . . . . . . 8 (𝑥𝐴 → (∀𝑦𝐴 ¬ 𝑥 <s 𝑦 → ((𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴) → ∀𝑦𝐴 ¬ (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s 𝑦)))
3410, 33rexlimi 3241 . . . . . . 7 (∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 → ((𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴) → ∀𝑦𝐴 ¬ (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s 𝑦))
3534imp 408 . . . . . 6 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → ∀𝑦𝐴 ¬ (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s 𝑦)
36 nfcv 2904 . . . . . . . . 9 𝑦 <s
37 nfcv 2904 . . . . . . . . 9 𝑦𝑈
3825, 36, 37nfbr 5156 . . . . . . . 8 𝑦(𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s 𝑈
3938nfn 1861 . . . . . . 7 𝑦 ¬ (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s 𝑈
40 breq2 5113 . . . . . . . 8 (𝑦 = 𝑈 → ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s 𝑦 ↔ (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s 𝑈))
4140notbid 318 . . . . . . 7 (𝑦 = 𝑈 → (¬ (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s 𝑦 ↔ ¬ (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s 𝑈))
4239, 41rspc 3571 . . . . . 6 (𝑈𝐴 → (∀𝑦𝐴 ¬ (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s 𝑦 → ¬ (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s 𝑈))
431, 35, 42sylc 65 . . . . 5 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → ¬ (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s 𝑈)
44 simpr1 1195 . . . . . . . . . 10 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → 𝐴 No )
45 simpl 484 . . . . . . . . . . . 12 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
4615adantl 483 . . . . . . . . . . . 12 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → ∃*𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
4745, 46, 17sylanbrc 584 . . . . . . . . . . 11 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → ∃!𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
48 riotacl 7335 . . . . . . . . . . 11 (∃!𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 → (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∈ 𝐴)
4947, 48syl 17 . . . . . . . . . 10 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∈ 𝐴)
5044, 49sseldd 3949 . . . . . . . . 9 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∈ No )
51 nofun 27020 . . . . . . . . 9 ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∈ No → Fun (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦))
52 funrel 6522 . . . . . . . . 9 (Fun (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) → Rel (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦))
5350, 51, 523syl 18 . . . . . . . 8 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → Rel (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦))
54 sssucid 6401 . . . . . . . 8 dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ⊆ suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
55 relssres 5982 . . . . . . . 8 ((Rel (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∧ dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ⊆ suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)) → ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ↾ suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)) = (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦))
5653, 54, 55sylancl 587 . . . . . . 7 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ↾ suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)) = (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦))
5756breq1d 5119 . . . . . 6 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → (((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ↾ suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)) <s (𝑈 ↾ suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)) ↔ (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s (𝑈 ↾ suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦))))
5844, 1sseldd 3949 . . . . . . 7 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → 𝑈 No )
59 nodmon 27021 . . . . . . . . 9 ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∈ No → dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∈ On)
6050, 59syl 17 . . . . . . . 8 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∈ On)
61 onsucb 7756 . . . . . . . 8 (dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∈ On ↔ suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∈ On)
6260, 61sylib 217 . . . . . . 7 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∈ On)
63 sltres 27033 . . . . . . 7 (((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∈ No 𝑈 No ∧ suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∈ On) → (((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ↾ suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)) <s (𝑈 ↾ suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)) → (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s 𝑈))
6450, 58, 62, 63syl3anc 1372 . . . . . 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 27041 . . . . 5 ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∈ No → (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}))
6850, 67syl 17 . . . 4 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}))
69 noreson 27031 . . . . . 6 ((𝑈 No ∧ suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∈ On) → (𝑈 ↾ suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)) ∈ No )
7058, 62, 69syl2anc 585 . . . . 5 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → (𝑈 ↾ suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)) ∈ No )
71 2on 8430 . . . . . . . . 9 2o ∈ On
7271elexi 3466 . . . . . . . 8 2o ∈ V
7372prid2 4728 . . . . . . 7 2o ∈ {1o, 2o}
7473noextend 27037 . . . . . 6 ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∈ No → ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}) ∈ No )
7550, 74syl 17 . . . . 5 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}) ∈ No )
76 sltso 27047 . . . . . 6 <s Or No
77 sotr2 5581 . . . . . 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 689 . . . . 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 1372 . . . 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 698 . . 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 4496 . . . . . . . 8 (∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 → if(∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦, ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥)))) = ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}))
8381, 82eqtrid 2785 . . . . . . 7 (∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦𝑆 = ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}))
8483dmeqd 5865 . . . . . 6 (∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 → dom 𝑆 = dom ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}))
8572dmsnop 6172 . . . . . . . 8 dom {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩} = {dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)}
8685uneq2i 4124 . . . . . . 7 (dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ dom {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}) = (dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)})
87 dmun 5870 . . . . . . 7 dom ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}) = (dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ dom {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩})
88 df-suc 6327 . . . . . . 7 suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) = (dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)})
8986, 87, 883eqtr4i 2771 . . . . . 6 dom ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}) = suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
9084, 89eqtrdi 2789 . . . . 5 (∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 → dom 𝑆 = suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦))
9190adantr 482 . . . 4 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → dom 𝑆 = suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦))
9291reseq2d 5941 . . 3 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → (𝑈 ↾ dom 𝑆) = (𝑈 ↾ suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)))
9383adantr 482 . . 3 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → 𝑆 = ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}))
9480, 92, 933brtr4d 5141 . 2 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → (𝑈 ↾ dom 𝑆) <s 𝑆)
95 simpl 484 . . 3 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → ¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
96 simpr1 1195 . . 3 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → 𝐴 No )
97 simpr2 1196 . . 3 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → 𝐴 ∈ V)
98 simpr3 1197 . . 3 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → 𝑈𝐴)
9981nosupbnd1lem6 27084 . . 3 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) → (𝑈 ↾ dom 𝑆) <s 𝑆)
10095, 96, 97, 98, 99syl121anc 1376 . 2 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → (𝑈 ↾ dom 𝑆) <s 𝑆)
10194, 100pm2.61ian 811 1 ((𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴) → (𝑈 ↾ dom 𝑆) <s 𝑆)
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  Vcvv 3447  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:  nosupbnd2  27087  noetasuplem3  27106
  Copyright terms: Public domain W3C validator