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

Theorem nosupbnd1 27062
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 1196 . . . . . 6 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → 𝑈𝐴)
2 nfv 1917 . . . . . . . . 9 𝑥(𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)
3 nfcv 2907 . . . . . . . . . 10 𝑥𝐴
4 nfriota1 7320 . . . . . . . . . . . 12 𝑥(𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
5 nfcv 2907 . . . . . . . . . . . 12 𝑥 <s
6 nfcv 2907 . . . . . . . . . . . 12 𝑥𝑦
74, 5, 6nfbr 5152 . . . . . . . . . . 11 𝑥(𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s 𝑦
87nfn 1860 . . . . . . . . . 10 𝑥 ¬ (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s 𝑦
93, 8nfralw 3294 . . . . . . . . 9 𝑥𝑦𝐴 ¬ (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s 𝑦
102, 9nfim 1899 . . . . . . . 8 𝑥((𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴) → ∀𝑦𝐴 ¬ (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s 𝑦)
11 simpl 483 . . . . . . . . . . 11 (((𝑥𝐴 ∧ ∀𝑦𝐴 ¬ 𝑥 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → (𝑥𝐴 ∧ ∀𝑦𝐴 ¬ 𝑥 <s 𝑦))
12 rspe 3232 . . . . . . . . . . . . . 14 ((𝑥𝐴 ∧ ∀𝑦𝐴 ¬ 𝑥 <s 𝑦) → ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
1312adantr 481 . . . . . . . . . . . . 13 (((𝑥𝐴 ∧ ∀𝑦𝐴 ¬ 𝑥 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
14 nomaxmo 27046 . . . . . . . . . . . . . . 15 (𝐴 No → ∃*𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
15143ad2ant1 1133 . . . . . . . . . . . . . 14 ((𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴) → ∃*𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
1615adantl 482 . . . . . . . . . . . . 13 (((𝑥𝐴 ∧ ∀𝑦𝐴 ¬ 𝑥 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → ∃*𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
17 reu5 3355 . . . . . . . . . . . . 13 (∃!𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ↔ (∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ∃*𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦))
1813, 16, 17sylanbrc 583 . . . . . . . . . . . 12 (((𝑥𝐴 ∧ ∀𝑦𝐴 ¬ 𝑥 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → ∃!𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
19 riota1 7335 . . . . . . . . . . . 12 (∃!𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 → ((𝑥𝐴 ∧ ∀𝑦𝐴 ¬ 𝑥 <s 𝑦) ↔ (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) = 𝑥))
2018, 19syl 17 . . . . . . . . . . 11 (((𝑥𝐴 ∧ ∀𝑦𝐴 ¬ 𝑥 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → ((𝑥𝐴 ∧ ∀𝑦𝐴 ¬ 𝑥 <s 𝑦) ↔ (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) = 𝑥))
2111, 20mpbid 231 . . . . . . . . . 10 (((𝑥𝐴 ∧ ∀𝑦𝐴 ¬ 𝑥 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) = 𝑥)
22 simplr 767 . . . . . . . . . 10 (((𝑥𝐴 ∧ ∀𝑦𝐴 ¬ 𝑥 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → ∀𝑦𝐴 ¬ 𝑥 <s 𝑦)
23 nfra1 3267 . . . . . . . . . . . . . 14 𝑦𝑦𝐴 ¬ 𝑥 <s 𝑦
24 nfcv 2907 . . . . . . . . . . . . . 14 𝑦𝐴
2523, 24nfriota 7326 . . . . . . . . . . . . 13 𝑦(𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
26 nfcv 2907 . . . . . . . . . . . . 13 𝑦𝑥
2725, 26nfeq 2920 . . . . . . . . . . . 12 𝑦(𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) = 𝑥
28 breq1 5108 . . . . . . . . . . . . 13 ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) = 𝑥 → ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s 𝑦𝑥 <s 𝑦))
2928notbid 317 . . . . . . . . . . . 12 ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) = 𝑥 → (¬ (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s 𝑦 ↔ ¬ 𝑥 <s 𝑦))
3027, 29ralbid 3256 . . . . . . . . . . 11 ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) = 𝑥 → (∀𝑦𝐴 ¬ (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s 𝑦 ↔ ∀𝑦𝐴 ¬ 𝑥 <s 𝑦))
3130biimprd 247 . . . . . . . . . 10 ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) = 𝑥 → (∀𝑦𝐴 ¬ 𝑥 <s 𝑦 → ∀𝑦𝐴 ¬ (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s 𝑦))
3221, 22, 31sylc 65 . . . . . . . . 9 (((𝑥𝐴 ∧ ∀𝑦𝐴 ¬ 𝑥 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → ∀𝑦𝐴 ¬ (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s 𝑦)
3332exp31 420 . . . . . . . 8 (𝑥𝐴 → (∀𝑦𝐴 ¬ 𝑥 <s 𝑦 → ((𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴) → ∀𝑦𝐴 ¬ (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s 𝑦)))
3410, 33rexlimi 3242 . . . . . . 7 (∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 → ((𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴) → ∀𝑦𝐴 ¬ (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s 𝑦))
3534imp 407 . . . . . 6 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → ∀𝑦𝐴 ¬ (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s 𝑦)
36 nfcv 2907 . . . . . . . . 9 𝑦 <s
37 nfcv 2907 . . . . . . . . 9 𝑦𝑈
3825, 36, 37nfbr 5152 . . . . . . . 8 𝑦(𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s 𝑈
3938nfn 1860 . . . . . . 7 𝑦 ¬ (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s 𝑈
40 breq2 5109 . . . . . . . 8 (𝑦 = 𝑈 → ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s 𝑦 ↔ (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s 𝑈))
4140notbid 317 . . . . . . 7 (𝑦 = 𝑈 → (¬ (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s 𝑦 ↔ ¬ (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s 𝑈))
4239, 41rspc 3569 . . . . . 6 (𝑈𝐴 → (∀𝑦𝐴 ¬ (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s 𝑦 → ¬ (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s 𝑈))
431, 35, 42sylc 65 . . . . 5 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → ¬ (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s 𝑈)
44 simpr1 1194 . . . . . . . . . 10 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → 𝐴 No )
45 simpl 483 . . . . . . . . . . . 12 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
4615adantl 482 . . . . . . . . . . . 12 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → ∃*𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
4745, 46, 17sylanbrc 583 . . . . . . . . . . 11 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → ∃!𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
48 riotacl 7331 . . . . . . . . . . 11 (∃!𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 → (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∈ 𝐴)
4947, 48syl 17 . . . . . . . . . 10 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∈ 𝐴)
5044, 49sseldd 3945 . . . . . . . . 9 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∈ No )
51 nofun 26997 . . . . . . . . 9 ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∈ No → Fun (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦))
52 funrel 6518 . . . . . . . . 9 (Fun (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) → Rel (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦))
5350, 51, 523syl 18 . . . . . . . 8 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → Rel (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦))
54 sssucid 6397 . . . . . . . 8 dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ⊆ suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
55 relssres 5978 . . . . . . . 8 ((Rel (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∧ dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ⊆ suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)) → ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ↾ suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)) = (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦))
5653, 54, 55sylancl 586 . . . . . . 7 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ↾ suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)) = (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦))
5756breq1d 5115 . . . . . 6 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → (((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ↾ suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)) <s (𝑈 ↾ suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)) ↔ (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s (𝑈 ↾ suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦))))
5844, 1sseldd 3945 . . . . . . 7 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → 𝑈 No )
59 nodmon 26998 . . . . . . . . 9 ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∈ No → dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∈ On)
6050, 59syl 17 . . . . . . . 8 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∈ On)
61 onsucb 7752 . . . . . . . 8 (dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∈ On ↔ suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∈ On)
6260, 61sylib 217 . . . . . . 7 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∈ On)
63 sltres 27010 . . . . . . 7 (((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∈ No 𝑈 No ∧ suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∈ On) → (((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ↾ suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)) <s (𝑈 ↾ suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)) → (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s 𝑈))
6450, 58, 62, 63syl3anc 1371 . . . . . 6 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → (((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ↾ suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)) <s (𝑈 ↾ suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)) → (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s 𝑈))
6557, 64sylbird 259 . . . . 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 27018 . . . . 5 ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∈ No → (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}))
6850, 67syl 17 . . . 4 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) <s ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}))
69 noreson 27008 . . . . . 6 ((𝑈 No ∧ suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∈ On) → (𝑈 ↾ suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)) ∈ No )
7058, 62, 69syl2anc 584 . . . . 5 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → (𝑈 ↾ suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)) ∈ No )
71 2on 8426 . . . . . . . . 9 2o ∈ On
7271elexi 3464 . . . . . . . 8 2o ∈ V
7372prid2 4724 . . . . . . 7 2o ∈ {1o, 2o}
7473noextend 27014 . . . . . 6 ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∈ No → ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}) ∈ No )
7550, 74syl 17 . . . . 5 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}) ∈ No )
76 sltso 27024 . . . . . 6 <s Or No
77 sotr2 5577 . . . . . 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 688 . . . . 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 1371 . . . 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 697 . . 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 4492 . . . . . . . 8 (∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 → if(∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦, ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥)))) = ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}))
8381, 82eqtrid 2788 . . . . . . 7 (∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦𝑆 = ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}))
8483dmeqd 5861 . . . . . 6 (∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 → dom 𝑆 = dom ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}))
8572dmsnop 6168 . . . . . . . 8 dom {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩} = {dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)}
8685uneq2i 4120 . . . . . . 7 (dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ dom {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}) = (dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)})
87 dmun 5866 . . . . . . 7 dom ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}) = (dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ dom {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩})
88 df-suc 6323 . . . . . . 7 suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) = (dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)})
8986, 87, 883eqtr4i 2774 . . . . . 6 dom ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}) = suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
9084, 89eqtrdi 2792 . . . . 5 (∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 → dom 𝑆 = suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦))
9190adantr 481 . . . 4 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → dom 𝑆 = suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦))
9291reseq2d 5937 . . 3 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → (𝑈 ↾ dom 𝑆) = (𝑈 ↾ suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)))
9383adantr 481 . . 3 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → 𝑆 = ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}))
9480, 92, 933brtr4d 5137 . 2 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → (𝑈 ↾ dom 𝑆) <s 𝑆)
95 simpl 483 . . 3 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → ¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
96 simpr1 1194 . . 3 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → 𝐴 No )
97 simpr2 1195 . . 3 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → 𝐴 ∈ V)
98 simpr3 1196 . . 3 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → 𝑈𝐴)
9981nosupbnd1lem6 27061 . . 3 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) → (𝑈 ↾ dom 𝑆) <s 𝑆)
10095, 96, 97, 98, 99syl121anc 1375 . 2 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴)) → (𝑈 ↾ dom 𝑆) <s 𝑆)
10194, 100pm2.61ian 810 1 ((𝐴 No 𝐴 ∈ V ∧ 𝑈𝐴) → (𝑈 ↾ dom 𝑆) <s 𝑆)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  w3a 1087   = wceq 1541  wcel 2106  {cab 2713  wral 3064  wrex 3073  ∃!wreu 3351  ∃*wrmo 3352  Vcvv 3445  cun 3908  wss 3910  ifcif 4486  {csn 4586  cop 4592   class class class wbr 5105  cmpt 5188   Or wor 5544  dom cdm 5633  cres 5635  Rel wrel 5638  Oncon0 6317  suc csuc 6319  cio 6446  Fun wfun 6490  cfv 6496  crio 7312  1oc1o 8405  2oc2o 8406   No csur 26988   <s cslt 26989
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pr 5384  ax-un 7672
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-tp 4591  df-op 4593  df-uni 4866  df-int 4908  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-ord 6320  df-on 6321  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-riota 7313  df-1o 8412  df-2o 8413  df-no 26991  df-slt 26992  df-bday 26993
This theorem is referenced by:  nosupbnd2  27064  noetasuplem3  27083
  Copyright terms: Public domain W3C validator