Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  nosupbnd1 Structured version   Visualization version   GIF version

Theorem nosupbnd1 32178
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 𝑦), 2𝑜⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ 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 1245 . . . . . 6 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → 𝑈𝐴)
2 nfv 2008 . . . . . . . . 9 𝑥(𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)
3 nfcv 2947 . . . . . . . . . 10 𝑥𝐴
4 nfriota1 6839 . . . . . . . . . . . 12 𝑥(𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
5 nfcv 2947 . . . . . . . . . . . 12 𝑥 <s
6 nfcv 2947 . . . . . . . . . . . 12 𝑥𝑦
74, 5, 6nfbr 4887 . . . . . . . . . . 11 𝑥(𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s 𝑦
87nfn 1947 . . . . . . . . . 10 𝑥 ¬ (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s 𝑦
93, 8nfral 3132 . . . . . . . . 9 𝑥𝑦𝐴 ¬ (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s 𝑦
102, 9nfim 1990 . . . . . . . 8 𝑥((𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴) → ∀𝑦𝐴 ¬ (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s 𝑦)
11 simpl 470 . . . . . . . . . . 11 (((𝑥𝐴 ∧ ∀𝑦𝐴 ¬ 𝑥 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → (𝑥𝐴 ∧ ∀𝑦𝐴 ¬ 𝑥 <s 𝑦))
12 rspe 3189 . . . . . . . . . . . . . 14 ((𝑥𝐴 ∧ ∀𝑦𝐴 ¬ 𝑥 <s 𝑦) → ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
1312adantr 468 . . . . . . . . . . . . 13 (((𝑥𝐴 ∧ ∀𝑦𝐴 ¬ 𝑥 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
14 nomaxmo 32165 . . . . . . . . . . . . . . 15 (𝐴 No → ∃*𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
15143ad2ant1 1156 . . . . . . . . . . . . . 14 ((𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴) → ∃*𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
1615adantl 469 . . . . . . . . . . . . 13 (((𝑥𝐴 ∧ ∀𝑦𝐴 ¬ 𝑥 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → ∃*𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
17 reu5 3347 . . . . . . . . . . . . 13 (∃!𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ↔ (∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ∃*𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦))
1813, 16, 17sylanbrc 574 . . . . . . . . . . . 12 (((𝑥𝐴 ∧ ∀𝑦𝐴 ¬ 𝑥 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → ∃!𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
19 riota1 6850 . . . . . . . . . . . 12 (∃!𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 → ((𝑥𝐴 ∧ ∀𝑦𝐴 ¬ 𝑥 <s 𝑦) ↔ (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) = 𝑥))
2018, 19syl 17 . . . . . . . . . . 11 (((𝑥𝐴 ∧ ∀𝑦𝐴 ¬ 𝑥 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → ((𝑥𝐴 ∧ ∀𝑦𝐴 ¬ 𝑥 <s 𝑦) ↔ (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) = 𝑥))
2111, 20mpbid 223 . . . . . . . . . 10 (((𝑥𝐴 ∧ ∀𝑦𝐴 ¬ 𝑥 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) = 𝑥)
22 simplr 776 . . . . . . . . . 10 (((𝑥𝐴 ∧ ∀𝑦𝐴 ¬ 𝑥 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → ∀𝑦𝐴 ¬ 𝑥 <s 𝑦)
23 nfra1 3128 . . . . . . . . . . . . . 14 𝑦𝑦𝐴 ¬ 𝑥 <s 𝑦
24 nfcv 2947 . . . . . . . . . . . . . 14 𝑦𝐴
2523, 24nfriota 6841 . . . . . . . . . . . . 13 𝑦(𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
26 nfcv 2947 . . . . . . . . . . . . 13 𝑦𝑥
2725, 26nfeq 2959 . . . . . . . . . . . 12 𝑦(𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) = 𝑥
28 breq1 4843 . . . . . . . . . . . . 13 ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) = 𝑥 → ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s 𝑦𝑥 <s 𝑦))
2928notbid 309 . . . . . . . . . . . 12 ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) = 𝑥 → (¬ (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s 𝑦 ↔ ¬ 𝑥 <s 𝑦))
3027, 29ralbid 3170 . . . . . . . . . . 11 ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) = 𝑥 → (∀𝑦𝐴 ¬ (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s 𝑦 ↔ ∀𝑦𝐴 ¬ 𝑥 <s 𝑦))
3130biimprd 239 . . . . . . . . . 10 ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) = 𝑥 → (∀𝑦𝐴 ¬ 𝑥 <s 𝑦 → ∀𝑦𝐴 ¬ (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s 𝑦))
3221, 22, 31sylc 65 . . . . . . . . 9 (((𝑥𝐴 ∧ ∀𝑦𝐴 ¬ 𝑥 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → ∀𝑦𝐴 ¬ (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s 𝑦)
3332exp31 408 . . . . . . . 8 (𝑥𝐴 → (∀𝑦𝐴 ¬ 𝑥 <s 𝑦 → ((𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴) → ∀𝑦𝐴 ¬ (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s 𝑦)))
3410, 33rexlimi 3211 . . . . . . 7 (∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 → ((𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴) → ∀𝑦𝐴 ¬ (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s 𝑦))
3534imp 395 . . . . . 6 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → ∀𝑦𝐴 ¬ (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s 𝑦)
36 nfcv 2947 . . . . . . . . 9 𝑦 <s
37 nfcv 2947 . . . . . . . . 9 𝑦𝑈
3825, 36, 37nfbr 4887 . . . . . . . 8 𝑦(𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s 𝑈
3938nfn 1947 . . . . . . 7 𝑦 ¬ (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s 𝑈
40 breq2 4844 . . . . . . . 8 (𝑦 = 𝑈 → ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s 𝑦 ↔ (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s 𝑈))
4140notbid 309 . . . . . . 7 (𝑦 = 𝑈 → (¬ (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s 𝑦 ↔ ¬ (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s 𝑈))
4239, 41rspc 3495 . . . . . 6 (𝑈𝐴 → (∀𝑦𝐴 ¬ (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s 𝑦 → ¬ (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s 𝑈))
431, 35, 42sylc 65 . . . . 5 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → ¬ (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s 𝑈)
44 simpr1 1241 . . . . . . . . . 10 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → 𝐴 No )
45 simpl 470 . . . . . . . . . . . 12 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
4615adantl 469 . . . . . . . . . . . 12 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → ∃*𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
4745, 46, 17sylanbrc 574 . . . . . . . . . . 11 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → ∃!𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
48 riotacl 6846 . . . . . . . . . . 11 (∃!𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 → (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∈ 𝐴)
4947, 48syl 17 . . . . . . . . . 10 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∈ 𝐴)
5044, 49sseldd 3796 . . . . . . . . 9 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∈ No )
51 nofun 32120 . . . . . . . . 9 ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∈ No → Fun (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦))
52 funrel 6115 . . . . . . . . 9 (Fun (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) → Rel (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦))
5350, 51, 523syl 18 . . . . . . . 8 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → Rel (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦))
54 sssucid 6012 . . . . . . . 8 dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ⊆ suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
55 relssres 5638 . . . . . . . 8 ((Rel (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∧ dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ⊆ suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)) → ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ↾ suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)) = (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦))
5653, 54, 55sylancl 576 . . . . . . 7 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ↾ suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)) = (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦))
5756breq1d 4850 . . . . . 6 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → (((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ↾ suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)) <s (𝑈 ↾ suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)) ↔ (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s (𝑈 ↾ suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦))))
5844, 1sseldd 3796 . . . . . . 7 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → 𝑈 No )
59 nodmon 32121 . . . . . . . . 9 ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∈ No → dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∈ On)
6050, 59syl 17 . . . . . . . 8 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∈ On)
61 sucelon 7244 . . . . . . . 8 (dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∈ On ↔ suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∈ On)
6260, 61sylib 209 . . . . . . 7 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∈ On)
63 sltres 32133 . . . . . . 7 (((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∈ No 𝑈 No ∧ suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∈ On) → (((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ↾ suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)) <s (𝑈 ↾ suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)) → (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s 𝑈))
6450, 58, 62, 63syl3anc 1483 . . . . . 6 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → (((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ↾ suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)) <s (𝑈 ↾ suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)) → (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s 𝑈))
6557, 64sylbird 251 . . . . 5 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s (𝑈 ↾ suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)) → (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s 𝑈))
6643, 65mtod 189 . . . 4 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → ¬ (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s (𝑈 ↾ suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)))
67 noextendgt 32141 . . . . 5 ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∈ No → (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2𝑜⟩}))
6850, 67syl 17 . . . 4 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2𝑜⟩}))
69 noreson 32131 . . . . . 6 ((𝑈 No ∧ suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∈ On) → (𝑈 ↾ suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)) ∈ No )
7058, 62, 69syl2anc 575 . . . . 5 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → (𝑈 ↾ suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)) ∈ No )
71 2on 7802 . . . . . . . . 9 2𝑜 ∈ On
7271elexi 3406 . . . . . . . 8 2𝑜 ∈ V
7372prid2 4486 . . . . . . 7 2𝑜 ∈ {1𝑜, 2𝑜}
7473noextend 32137 . . . . . 6 ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∈ No → ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2𝑜⟩}) ∈ No )
7550, 74syl 17 . . . . 5 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2𝑜⟩}) ∈ No )
76 sltso 32145 . . . . . 6 <s Or No
77 sotr2 5258 . . . . . 6 (( <s Or No ∧ ((𝑈 ↾ suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)) ∈ No ∧ (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∈ No ∧ ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2𝑜⟩}) ∈ No )) → ((¬ (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s (𝑈 ↾ suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)) ∧ (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2𝑜⟩})) → (𝑈 ↾ suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)) <s ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2𝑜⟩})))
7876, 77mpan 673 . . . . 5 (((𝑈 ↾ suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)) ∈ No ∧ (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∈ No ∧ ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2𝑜⟩}) ∈ No ) → ((¬ (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s (𝑈 ↾ suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)) ∧ (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2𝑜⟩})) → (𝑈 ↾ suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)) <s ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2𝑜⟩})))
7970, 50, 75, 78syl3anc 1483 . . . 4 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → ((¬ (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s (𝑈 ↾ suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)) ∧ (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2𝑜⟩})) → (𝑈 ↾ suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)) <s ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2𝑜⟩})))
8066, 68, 79mp2and 682 . . 3 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → (𝑈 ↾ suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)) <s ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2𝑜⟩}))
81 nosupbnd1.1 . . . . . . . 8 𝑆 = if(∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦, ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2𝑜⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))))
82 iftrue 4282 . . . . . . . 8 (∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 → if(∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦, ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2𝑜⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥)))) = ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2𝑜⟩}))
8381, 82syl5eq 2851 . . . . . . 7 (∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦𝑆 = ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2𝑜⟩}))
8483dmeqd 5524 . . . . . 6 (∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 → dom 𝑆 = dom ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2𝑜⟩}))
8572dmsnop 5818 . . . . . . . 8 dom {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2𝑜⟩} = {dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)}
8685uneq2i 3960 . . . . . . 7 (dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ dom {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2𝑜⟩}) = (dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)})
87 dmun 5529 . . . . . . 7 dom ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2𝑜⟩}) = (dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ dom {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2𝑜⟩})
88 df-suc 5939 . . . . . . 7 suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) = (dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)})
8986, 87, 883eqtr4i 2837 . . . . . 6 dom ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2𝑜⟩}) = suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
9084, 89syl6eq 2855 . . . . 5 (∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 → dom 𝑆 = suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦))
9190adantr 468 . . . 4 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → dom 𝑆 = suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦))
9291reseq2d 5594 . . 3 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → (𝑈 ↾ dom 𝑆) = (𝑈 ↾ suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)))
9383adantr 468 . . 3 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → 𝑆 = ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2𝑜⟩}))
9480, 92, 933brtr4d 4872 . 2 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → (𝑈 ↾ dom 𝑆) <s 𝑆)
95 simpl 470 . . 3 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → ¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
96 simpr1 1241 . . 3 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → 𝐴 No )
97 simpr2 1243 . . 3 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → 𝐴 ∈ V)
98 simpr3 1245 . . 3 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → 𝑈𝐴)
9981nosupbnd1lem6 32177 . . 3 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) → (𝑈 ↾ dom 𝑆) <s 𝑆)
10095, 96, 97, 98, 99syl121anc 1487 . 2 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → (𝑈 ↾ dom 𝑆) <s 𝑆)
10194, 100pm2.61ian 837 1 ((𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴) → (𝑈 ↾ dom 𝑆) <s 𝑆)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  w3a 1100   = wceq 1637  wcel 2158  {cab 2791  wral 3095  wrex 3096  ∃!wreu 3097  ∃*wrmo 3098  Vcvv 3390  cun 3764  wss 3766  ifcif 4276  {csn 4367  cop 4373   class class class wbr 4840  cmpt 4919   Or wor 5228  dom cdm 5308  cres 5310  Rel wrel 5313  Oncon0 5933  suc csuc 5935  cio 6059  Fun wfun 6092  cfv 6098  crio 6831  1𝑜c1o 7786  2𝑜c2o 7787   No csur 32111   <s cslt 32112
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1880  ax-4 1897  ax-5 2004  ax-6 2070  ax-7 2106  ax-8 2160  ax-9 2167  ax-10 2187  ax-11 2203  ax-12 2216  ax-13 2422  ax-ext 2784  ax-rep 4960  ax-sep 4971  ax-nul 4980  ax-pow 5032  ax-pr 5093  ax-un 7176
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1865  df-sb 2063  df-eu 2636  df-mo 2637  df-clab 2792  df-cleq 2798  df-clel 2801  df-nfc 2936  df-ne 2978  df-ral 3100  df-rex 3101  df-reu 3102  df-rmo 3103  df-rab 3104  df-v 3392  df-sbc 3631  df-csb 3726  df-dif 3769  df-un 3771  df-in 3773  df-ss 3780  df-pss 3782  df-nul 4114  df-if 4277  df-pw 4350  df-sn 4368  df-pr 4370  df-tp 4372  df-op 4374  df-uni 4627  df-int 4666  df-iun 4710  df-br 4841  df-opab 4903  df-mpt 4920  df-tr 4943  df-id 5216  df-eprel 5221  df-po 5229  df-so 5230  df-fr 5267  df-we 5269  df-xp 5314  df-rel 5315  df-cnv 5316  df-co 5317  df-dm 5318  df-rn 5319  df-res 5320  df-ima 5321  df-ord 5936  df-on 5937  df-suc 5939  df-iota 6061  df-fun 6100  df-fn 6101  df-f 6102  df-f1 6103  df-fo 6104  df-f1o 6105  df-fv 6106  df-riota 6832  df-1o 7793  df-2o 7794  df-no 32114  df-slt 32115  df-bday 32116
This theorem is referenced by:  nosupbnd2  32180  noetalem2  32182
  Copyright terms: Public domain W3C validator