nosupbnd1 - Mathbox for Scott Fenton

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

Theorem nosupbnd1 33216

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_o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ 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**
Step	Hyp	Ref	Expression
1		simpr3 1192	. . . . . 6 ⊢ ((∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑈 ∈ 𝐴)) → 𝑈 ∈ 𝐴)
2		nfv 1915	. . . . . . . . 9 ⊢ Ⅎ𝑥(𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑈 ∈ 𝐴)
3		nfcv 2979	. . . . . . . . . 10 ⊢ Ⅎ𝑥𝐴
4		nfriota1 7123	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥(℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦)
5		nfcv 2979	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥 <s
6		nfcv 2979	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥𝑦
7	4, 5, 6	nfbr 5115	. . . . . . . . . . 11 ⊢ Ⅎ𝑥(℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) <s 𝑦
8	7	nfn 1857	. . . . . . . . . 10 ⊢ Ⅎ𝑥 ¬ (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) <s 𝑦
9	3, 8	nfralw 3227	. . . . . . . . 9 ⊢ Ⅎ𝑥∀𝑦 ∈ 𝐴 ¬ (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) <s 𝑦
10	2, 9	nfim 1897	. . . . . . . 8 ⊢ Ⅎ𝑥((𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑈 ∈ 𝐴) → ∀𝑦 ∈ 𝐴 ¬ (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) <s 𝑦)
11		simpl 485	. . . . . . . . . . 11 ⊢ (((𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑈 ∈ 𝐴)) → (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦))
12		rspe 3306	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) → ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦)
13	12	adantr 483	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑈 ∈ 𝐴)) → ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦)
14		nomaxmo 33203	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ⊆ No → ∃*𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦)
15	14	3ad2ant1 1129	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑈 ∈ 𝐴) → ∃*𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦)
16	15	adantl 484	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑈 ∈ 𝐴)) → ∃*𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦)
17		reu5 3432	. . . . . . . . . . . . 13 ⊢ (∃!𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ↔ (∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ∃*𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦))
18	13, 16, 17	sylanbrc 585	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑈 ∈ 𝐴)) → ∃!𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦)
19		riota1 7137	. . . . . . . . . . . 12 ⊢ (∃!𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 → ((𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ↔ (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) = 𝑥))
20	18, 19	syl 17	. . . . . . . . . . 11 ⊢ (((𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑈 ∈ 𝐴)) → ((𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ↔ (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) = 𝑥))
21	11, 20	mpbid 234	. . . . . . . . . 10 ⊢ (((𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑈 ∈ 𝐴)) → (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) = 𝑥)
22		simplr 767	. . . . . . . . . 10 ⊢ (((𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑈 ∈ 𝐴)) → ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦)
23		nfra1 3221	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑦∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦
24		nfcv 2979	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑦𝐴
25	23, 24	nfriota 7128	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦(℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦)
26		nfcv 2979	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦𝑥
27	25, 26	nfeq 2993	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦(℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) = 𝑥
28		breq1 5071	. . . . . . . . . . . . 13 ⊢ ((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) = 𝑥 → ((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) <s 𝑦 ↔ 𝑥 <s 𝑦))
29	28	notbid 320	. . . . . . . . . . . 12 ⊢ ((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) = 𝑥 → (¬ (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) <s 𝑦 ↔ ¬ 𝑥 <s 𝑦))
30	27, 29	ralbid 3233	. . . . . . . . . . 11 ⊢ ((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) = 𝑥 → (∀𝑦 ∈ 𝐴 ¬ (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) <s 𝑦 ↔ ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦))
31	30	biimprd 250	. . . . . . . . . 10 ⊢ ((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) = 𝑥 → (∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 → ∀𝑦 ∈ 𝐴 ¬ (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) <s 𝑦))
32	21, 22, 31	sylc 65	. . . . . . . . 9 ⊢ (((𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑈 ∈ 𝐴)) → ∀𝑦 ∈ 𝐴 ¬ (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) <s 𝑦)
33	32	exp31 422	. . . . . . . 8 ⊢ (𝑥 ∈ 𝐴 → (∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 → ((𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑈 ∈ 𝐴) → ∀𝑦 ∈ 𝐴 ¬ (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) <s 𝑦)))
34	10, 33	rexlimi 3317	. . . . . . 7 ⊢ (∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 → ((𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑈 ∈ 𝐴) → ∀𝑦 ∈ 𝐴 ¬ (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) <s 𝑦))
35	34	imp 409	. . . . . 6 ⊢ ((∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑈 ∈ 𝐴)) → ∀𝑦 ∈ 𝐴 ¬ (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) <s 𝑦)
36		nfcv 2979	. . . . . . . . 9 ⊢ Ⅎ𝑦 <s
37		nfcv 2979	. . . . . . . . 9 ⊢ Ⅎ𝑦𝑈
38	25, 36, 37	nfbr 5115	. . . . . . . 8 ⊢ Ⅎ𝑦(℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) <s 𝑈
39	38	nfn 1857	. . . . . . 7 ⊢ Ⅎ𝑦 ¬ (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) <s 𝑈
40		breq2 5072	. . . . . . . 8 ⊢ (𝑦 = 𝑈 → ((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) <s 𝑦 ↔ (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) <s 𝑈))
41	40	notbid 320	. . . . . . 7 ⊢ (𝑦 = 𝑈 → (¬ (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) <s 𝑦 ↔ ¬ (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) <s 𝑈))
42	39, 41	rspc 3613	. . . . . 6 ⊢ (𝑈 ∈ 𝐴 → (∀𝑦 ∈ 𝐴 ¬ (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) <s 𝑦 → ¬ (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) <s 𝑈))
43	1, 35, 42	sylc 65	. . . . 5 ⊢ ((∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑈 ∈ 𝐴)) → ¬ (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) <s 𝑈)
44		simpr1 1190	. . . . . . . . . 10 ⊢ ((∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑈 ∈ 𝐴)) → 𝐴 ⊆ No )
45		simpl 485	. . . . . . . . . . . 12 ⊢ ((∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑈 ∈ 𝐴)) → ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦)
46	15	adantl 484	. . . . . . . . . . . 12 ⊢ ((∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑈 ∈ 𝐴)) → ∃*𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦)
47	45, 46, 17	sylanbrc 585	. . . . . . . . . . 11 ⊢ ((∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑈 ∈ 𝐴)) → ∃!𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦)
48		riotacl 7133	. . . . . . . . . . 11 ⊢ (∃!𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 → (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∈ 𝐴)
49	47, 48	syl 17	. . . . . . . . . 10 ⊢ ((∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑈 ∈ 𝐴)) → (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∈ 𝐴)
50	44, 49	sseldd 3970	. . . . . . . . 9 ⊢ ((∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑈 ∈ 𝐴)) → (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∈ No )
51		nofun 33158	. . . . . . . . 9 ⊢ ((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∈ No → Fun (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦))
52		funrel 6374	. . . . . . . . 9 ⊢ (Fun (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) → Rel (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦))
53	50, 51, 52	3syl 18	. . . . . . . 8 ⊢ ((∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑈 ∈ 𝐴)) → Rel (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦))
54		sssucid 6270	. . . . . . . 8 ⊢ dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ⊆ suc dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦)
55		relssres 5895	. . . . . . . 8 ⊢ ((Rel (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∧ dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ⊆ suc dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦)) → ((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ↾ suc dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦)) = (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦))
56	53, 54, 55	sylancl 588	. . . . . . 7 ⊢ ((∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑈 ∈ 𝐴)) → ((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ↾ suc dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦)) = (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦))
57	56	breq1d 5078	. . . . . 6 ⊢ ((∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑈 ∈ 𝐴)) → (((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ↾ suc dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦)) <s (𝑈 ↾ suc dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦)) ↔ (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) <s (𝑈 ↾ suc dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦))))
58	44, 1	sseldd 3970	. . . . . . 7 ⊢ ((∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑈 ∈ 𝐴)) → 𝑈 ∈ No )
59		nodmon 33159	. . . . . . . . 9 ⊢ ((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∈ No → dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∈ On)
60	50, 59	syl 17	. . . . . . . 8 ⊢ ((∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑈 ∈ 𝐴)) → dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∈ On)
61		sucelon 7534	. . . . . . . 8 ⊢ (dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∈ On ↔ suc dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∈ On)
62	60, 61	sylib 220	. . . . . . 7 ⊢ ((∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑈 ∈ 𝐴)) → suc dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∈ On)
63		sltres 33171	. . . . . . 7 ⊢ (((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∈ No ∧ 𝑈 ∈ No ∧ suc dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∈ On) → (((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ↾ suc dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦)) <s (𝑈 ↾ suc dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦)) → (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) <s 𝑈))
64	50, 58, 62, 63	syl3anc 1367	. . . . . 6 ⊢ ((∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑈 ∈ 𝐴)) → (((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ↾ suc dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦)) <s (𝑈 ↾ suc dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦)) → (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) <s 𝑈))
65	57, 64	sylbird 262	. . . . 5 ⊢ ((∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑈 ∈ 𝐴)) → ((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) <s (𝑈 ↾ suc dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦)) → (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) <s 𝑈))
66	43, 65	mtod 200	. . . 4 ⊢ ((∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑈 ∈ 𝐴)) → ¬ (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) <s (𝑈 ↾ suc dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦)))
67		noextendgt 33179	. . . . 5 ⊢ ((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∈ No → (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) <s ((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2_o⟩}))
68	50, 67	syl 17	. . . 4 ⊢ ((∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑈 ∈ 𝐴)) → (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) <s ((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2_o⟩}))
69		noreson 33169	. . . . . 6 ⊢ ((𝑈 ∈ No ∧ suc dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∈ On) → (𝑈 ↾ suc dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦)) ∈ No )
70	58, 62, 69	syl2anc 586	. . . . 5 ⊢ ((∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑈 ∈ 𝐴)) → (𝑈 ↾ suc dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦)) ∈ No )
71		2on 8113	. . . . . . . . 9 ⊢ 2_o ∈ On
72	71	elexi 3515	. . . . . . . 8 ⊢ 2_o ∈ V
73	72	prid2 4701	. . . . . . 7 ⊢ 2_o ∈ {1_o, 2_o}
74	73	noextend 33175	. . . . . 6 ⊢ ((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∈ No → ((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2_o⟩}) ∈ No )
75	50, 74	syl 17	. . . . 5 ⊢ ((∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑈 ∈ 𝐴)) → ((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2_o⟩}) ∈ No )
76		sltso 33183	. . . . . 6 ⊢ <s Or No
77		sotr2 5507	. . . . . 6 ⊢ (( <s Or No ∧ ((𝑈 ↾ suc dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦)) ∈ No ∧ (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∈ No ∧ ((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2_o⟩}) ∈ No )) → ((¬ (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) <s (𝑈 ↾ suc dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦)) ∧ (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) <s ((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2_o⟩})) → (𝑈 ↾ suc dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦)) <s ((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2_o⟩})))
78	76, 77	mpan 688	. . . . 5 ⊢ (((𝑈 ↾ suc dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦)) ∈ No ∧ (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∈ No ∧ ((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2_o⟩}) ∈ No ) → ((¬ (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) <s (𝑈 ↾ suc dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦)) ∧ (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) <s ((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2_o⟩})) → (𝑈 ↾ suc dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦)) <s ((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2_o⟩})))
79	70, 50, 75, 78	syl3anc 1367	. . . 4 ⊢ ((∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑈 ∈ 𝐴)) → ((¬ (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) <s (𝑈 ↾ suc dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦)) ∧ (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) <s ((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2_o⟩})) → (𝑈 ↾ suc dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦)) <s ((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2_o⟩})))
80	66, 68, 79	mp2and 697	. . 3 ⊢ ((∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑈 ∈ 𝐴)) → (𝑈 ↾ suc dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦)) <s ((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2_o⟩}))
81		nosupbnd1.1	. . . . . . . 8 ⊢ 𝑆 = if(∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦, ((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2_o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))))
82		iftrue 4475	. . . . . . . 8 ⊢ (∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 → if(∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦, ((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2_o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥)))) = ((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2_o⟩}))
83	81, 82	syl5eq 2870	. . . . . . 7 ⊢ (∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 → 𝑆 = ((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2_o⟩}))
84	83	dmeqd 5776	. . . . . 6 ⊢ (∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 → dom 𝑆 = dom ((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2_o⟩}))
85	72	dmsnop 6075	. . . . . . . 8 ⊢ dom {⟨dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2_o⟩} = {dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦)}
86	85	uneq2i 4138	. . . . . . 7 ⊢ (dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ dom {⟨dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2_o⟩}) = (dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ {dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦)})
87		dmun 5781	. . . . . . 7 ⊢ dom ((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2_o⟩}) = (dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ dom {⟨dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2_o⟩})
88		df-suc 6199	. . . . . . 7 ⊢ suc dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) = (dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ {dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦)})
89	86, 87, 88	3eqtr4i 2856	. . . . . 6 ⊢ dom ((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2_o⟩}) = suc dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦)
90	84, 89	syl6eq 2874	. . . . 5 ⊢ (∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 → dom 𝑆 = suc dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦))
91	90	adantr 483	. . . 4 ⊢ ((∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑈 ∈ 𝐴)) → dom 𝑆 = suc dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦))
92	91	reseq2d 5855	. . 3 ⊢ ((∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑈 ∈ 𝐴)) → (𝑈 ↾ dom 𝑆) = (𝑈 ↾ suc dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦)))
93	83	adantr 483	. . 3 ⊢ ((∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑈 ∈ 𝐴)) → 𝑆 = ((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2_o⟩}))
94	80, 92, 93	3brtr4d 5100	. 2 ⊢ ((∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑈 ∈ 𝐴)) → (𝑈 ↾ dom 𝑆) <s 𝑆)
95		simpl 485	. . 3 ⊢ ((¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑈 ∈ 𝐴)) → ¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦)
96		simpr1 1190	. . 3 ⊢ ((¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑈 ∈ 𝐴)) → 𝐴 ⊆ No )
97		simpr2 1191	. . 3 ⊢ ((¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑈 ∈ 𝐴)) → 𝐴 ∈ V)
98		simpr3 1192	. . 3 ⊢ ((¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑈 ∈ 𝐴)) → 𝑈 ∈ 𝐴)
99	81	nosupbnd1lem6 33215	. . 3 ⊢ ((¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ 𝑈 ∈ 𝐴) → (𝑈 ↾ dom 𝑆) <s 𝑆)
100	95, 96, 97, 98, 99	syl121anc 1371	. 2 ⊢ ((¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑈 ∈ 𝐴)) → (𝑈 ↾ dom 𝑆) <s 𝑆)
101	94, 100	pm2.61ian 810	1 ⊢ ((𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝑈 ∈ 𝐴) → (𝑈 ↾ dom 𝑆) <s 𝑆)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 208 ∧ wa 398 ∧ w3a 1083 = wceq 1537 ∈ wcel 2114 {cab 2801 ∀wral 3140 ∃wrex 3141 ∃!wreu 3142 ∃*wrmo 3143 Vcvv 3496 ∪ cun 3936 ⊆ wss 3938 ifcif 4469 {csn 4569 ⟨cop 4575 class class class wbr 5068 ↦ cmpt 5148 Or wor 5475 dom cdm 5557 ↾ cres 5559 Rel wrel 5562 Oncon0 6193 suc csuc 6195 ℩cio 6314 Fun wfun 6351 ‘cfv 6357 ℩crio 7115 1_oc1o 8097 2_oc2o 8098 No csur 33149 <s cslt 33150

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 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2795 ax-rep 5192 ax-sep 5205 ax-nul 5212 ax-pow 5268 ax-pr 5332 ax-un 7463

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3or 1084 df-3an 1085 df-tru 1540 df-ex 1781 df-nf 1785 df-sb 2070 df-mo 2622 df-eu 2654 df-clab 2802 df-cleq 2816 df-clel 2895 df-nfc 2965 df-ne 3019 df-ral 3145 df-rex 3146 df-reu 3147 df-rmo 3148 df-rab 3149 df-v 3498 df-sbc 3775 df-csb 3886 df-dif 3941 df-un 3943 df-in 3945 df-ss 3954 df-pss 3956 df-nul 4294 df-if 4470 df-pw 4543 df-sn 4570 df-pr 4572 df-tp 4574 df-op 4576 df-uni 4841 df-int 4879 df-iun 4923 df-br 5069 df-opab 5131 df-mpt 5149 df-tr 5175 df-id 5462 df-eprel 5467 df-po 5476 df-so 5477 df-fr 5516 df-we 5518 df-xp 5563 df-rel 5564 df-cnv 5565 df-co 5566 df-dm 5567 df-rn 5568 df-res 5569 df-ima 5570 df-ord 6196 df-on 6197 df-suc 6199 df-iota 6316 df-fun 6359 df-fn 6360 df-f 6361 df-f1 6362 df-fo 6363 df-f1o 6364 df-fv 6365 df-riota 7116 df-1o 8104 df-2o 8105 df-no 33152 df-slt 33153 df-bday 33154

This theorem is referenced by: nosupbnd2 33218 noetalem2 33220

W3C validator