nosupbday - Metamath Proof Explorer

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

Theorem nosupbday 27750

Description: Birthday bounding law for surreal supremum. (Contributed by Scott Fenton, 5-Dec-2021.)

**Hypothesis**
Ref	Expression
nosupbday.1	⊢ 𝑆 = if(∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦, ((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2_o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))))

**Assertion**
Ref	Expression
nosupbday	⊢ (((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝑂 ∈ On ∧ ( bday “ 𝐴) ⊆ 𝑂)) → ( bday ‘𝑆) ⊆ 𝑂)

Distinct variable groups: 𝐴,𝑔,𝑢,𝑣,𝑥,𝑦 𝑢,𝑂,𝑦 Allowed substitution hints: 𝑆(𝑥,𝑦,𝑣,𝑢,𝑔) 𝑂(𝑥,𝑣,𝑔)

**Proof of Theorem nosupbday**
Step	Hyp	Ref	Expression
1		nosupbday.1	. . . . 5 ⊢ 𝑆 = if(∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦, ((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2_o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))))
2	1	nosupno 27748	. . . 4 ⊢ ((𝐴 ⊆ No ∧ 𝐴 ∈ V) → 𝑆 ∈ No )
3	2	adantr 480	. . 3 ⊢ (((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝑂 ∈ On ∧ ( bday “ 𝐴) ⊆ 𝑂)) → 𝑆 ∈ No )
4		bdayval 27693	. . 3 ⊢ (𝑆 ∈ No → ( bday ‘𝑆) = dom 𝑆)
5	3, 4	syl 17	. 2 ⊢ (((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝑂 ∈ On ∧ ( bday “ 𝐴) ⊆ 𝑂)) → ( bday ‘𝑆) = dom 𝑆)
6		iftrue 4531	. . . . . . . 8 ⊢ (∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 → if(∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦, ((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2_o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥)))) = ((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2_o⟩}))
7	1, 6	eqtrid 2789	. . . . . . 7 ⊢ (∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 → 𝑆 = ((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2_o⟩}))
8	7	dmeqd 5916	. . . . . 6 ⊢ (∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 → dom 𝑆 = dom ((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2_o⟩}))
9		2oex 8517	. . . . . . . . 9 ⊢ 2_o ∈ V
10	9	dmsnop 6236	. . . . . . . 8 ⊢ dom {⟨dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2_o⟩} = {dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦)}
11	10	uneq2i 4165	. . . . . . 7 ⊢ (dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ dom {⟨dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2_o⟩}) = (dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ {dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦)})
12		dmun 5921	. . . . . . 7 ⊢ dom ((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2_o⟩}) = (dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ dom {⟨dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2_o⟩})
13		df-suc 6390	. . . . . . 7 ⊢ suc dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) = (dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ {dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦)})
14	11, 12, 13	3eqtr4i 2775	. . . . . 6 ⊢ dom ((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2_o⟩}) = suc dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦)
15	8, 14	eqtrdi 2793	. . . . 5 ⊢ (∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 → dom 𝑆 = suc dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦))
16	15	adantr 480	. . . 4 ⊢ ((∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝑂 ∈ On ∧ ( bday “ 𝐴) ⊆ 𝑂))) → dom 𝑆 = suc dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦))
17		simprrl 781	. . . . . 6 ⊢ ((∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝑂 ∈ On ∧ ( bday “ 𝐴) ⊆ 𝑂))) → 𝑂 ∈ On)
18		eloni 6394	. . . . . 6 ⊢ (𝑂 ∈ On → Ord 𝑂)
19	17, 18	syl 17	. . . . 5 ⊢ ((∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝑂 ∈ On ∧ ( bday “ 𝐴) ⊆ 𝑂))) → Ord 𝑂)
20		simprll 779	. . . . . . . 8 ⊢ ((∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝑂 ∈ On ∧ ( bday “ 𝐴) ⊆ 𝑂))) → 𝐴 ⊆ No )
21		simpl 482	. . . . . . . . . . 11 ⊢ ((∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V)) → ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦)
22		nomaxmo 27743	. . . . . . . . . . . . 13 ⊢ (𝐴 ⊆ No → ∃*𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦)
23	22	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝐴 ⊆ No ∧ 𝐴 ∈ V) → ∃*𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦)
24	23	adantl 481	. . . . . . . . . . 11 ⊢ ((∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V)) → ∃*𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦)
25		reu5 3382	. . . . . . . . . . 11 ⊢ (∃!𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ↔ (∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ∃*𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦))
26	21, 24, 25	sylanbrc 583	. . . . . . . . . 10 ⊢ ((∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V)) → ∃!𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦)
27	26	adantrr 717	. . . . . . . . 9 ⊢ ((∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝑂 ∈ On ∧ ( bday “ 𝐴) ⊆ 𝑂))) → ∃!𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦)
28		riotacl 7405	. . . . . . . . 9 ⊢ (∃!𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 → (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∈ 𝐴)
29	27, 28	syl 17	. . . . . . . 8 ⊢ ((∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝑂 ∈ On ∧ ( bday “ 𝐴) ⊆ 𝑂))) → (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∈ 𝐴)
30	20, 29	sseldd 3984	. . . . . . 7 ⊢ ((∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝑂 ∈ On ∧ ( bday “ 𝐴) ⊆ 𝑂))) → (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∈ No )
31		bdayval 27693	. . . . . . 7 ⊢ ((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∈ No → ( bday ‘(℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦)) = dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦))
32	30, 31	syl 17	. . . . . 6 ⊢ ((∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝑂 ∈ On ∧ ( bday “ 𝐴) ⊆ 𝑂))) → ( bday ‘(℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦)) = dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦))
33		simprrr 782	. . . . . . 7 ⊢ ((∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝑂 ∈ On ∧ ( bday “ 𝐴) ⊆ 𝑂))) → ( bday “ 𝐴) ⊆ 𝑂)
34		bdayfo 27722	. . . . . . . . 9 ⊢ bday : No –onto→On
35		fofn 6822	. . . . . . . . 9 ⊢ ( bday : No –onto→On → bday Fn No )
36	34, 35	ax-mp 5	. . . . . . . 8 ⊢ bday Fn No
37		fnfvima 7253	. . . . . . . 8 ⊢ (( bday Fn No ∧ 𝐴 ⊆ No ∧ (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∈ 𝐴) → ( bday ‘(℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦)) ∈ ( bday “ 𝐴))
38	36, 20, 29, 37	mp3an2i 1468	. . . . . . 7 ⊢ ((∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝑂 ∈ On ∧ ( bday “ 𝐴) ⊆ 𝑂))) → ( bday ‘(℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦)) ∈ ( bday “ 𝐴))
39	33, 38	sseldd 3984	. . . . . 6 ⊢ ((∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝑂 ∈ On ∧ ( bday “ 𝐴) ⊆ 𝑂))) → ( bday ‘(℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦)) ∈ 𝑂)
40	32, 39	eqeltrrd 2842	. . . . 5 ⊢ ((∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝑂 ∈ On ∧ ( bday “ 𝐴) ⊆ 𝑂))) → dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∈ 𝑂)
41		ordsucss 7838	. . . . 5 ⊢ (Ord 𝑂 → (dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∈ 𝑂 → suc dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ⊆ 𝑂))
42	19, 40, 41	sylc 65	. . . 4 ⊢ ((∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝑂 ∈ On ∧ ( bday “ 𝐴) ⊆ 𝑂))) → suc dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ⊆ 𝑂)
43	16, 42	eqsstrd 4018	. . 3 ⊢ ((∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝑂 ∈ On ∧ ( bday “ 𝐴) ⊆ 𝑂))) → dom 𝑆 ⊆ 𝑂)
44		iffalse 4534	. . . . . . . 8 ⊢ (¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 → if(∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦, ((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2_o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥)))) = (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))))
45	1, 44	eqtrid 2789	. . . . . . 7 ⊢ (¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 → 𝑆 = (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))))
46	45	dmeqd 5916	. . . . . 6 ⊢ (¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 → dom 𝑆 = dom (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))))
47		iotaex 6534	. . . . . . 7 ⊢ (℩𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥)) ∈ V
48		eqid 2737	. . . . . . 7 ⊢ (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))) = (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥)))
49	47, 48	dmmpti 6712	. . . . . 6 ⊢ dom (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))) = {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))}
50	46, 49	eqtrdi 2793	. . . . 5 ⊢ (¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 → dom 𝑆 = {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))})
51	50	adantr 480	. . . 4 ⊢ ((¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝑂 ∈ On ∧ ( bday “ 𝐴) ⊆ 𝑂))) → dom 𝑆 = {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))})
52		simplrl 777	. . . . . . . . . 10 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝑂 ∈ On ∧ ( bday “ 𝐴) ⊆ 𝑂)) ∧ 𝑢 ∈ 𝐴) → 𝑂 ∈ On)
53		ssel2 3978	. . . . . . . . . . . . 13 ⊢ ((𝐴 ⊆ No ∧ 𝑢 ∈ 𝐴) → 𝑢 ∈ No )
54	53	ad4ant14 752	. . . . . . . . . . . 12 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝑂 ∈ On ∧ ( bday “ 𝐴) ⊆ 𝑂)) ∧ 𝑢 ∈ 𝐴) → 𝑢 ∈ No )
55		bdayval 27693	. . . . . . . . . . . 12 ⊢ (𝑢 ∈ No → ( bday ‘𝑢) = dom 𝑢)
56	54, 55	syl 17	. . . . . . . . . . 11 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝑂 ∈ On ∧ ( bday “ 𝐴) ⊆ 𝑂)) ∧ 𝑢 ∈ 𝐴) → ( bday ‘𝑢) = dom 𝑢)
57		simplrr 778	. . . . . . . . . . . 12 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝑂 ∈ On ∧ ( bday “ 𝐴) ⊆ 𝑂)) ∧ 𝑢 ∈ 𝐴) → ( bday “ 𝐴) ⊆ 𝑂)
58		fnfvima 7253	. . . . . . . . . . . . . 14 ⊢ (( bday Fn No ∧ 𝐴 ⊆ No ∧ 𝑢 ∈ 𝐴) → ( bday ‘𝑢) ∈ ( bday “ 𝐴))
59	36, 58	mp3an1 1450	. . . . . . . . . . . . 13 ⊢ ((𝐴 ⊆ No ∧ 𝑢 ∈ 𝐴) → ( bday ‘𝑢) ∈ ( bday “ 𝐴))
60	59	ad4ant14 752	. . . . . . . . . . . 12 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝑂 ∈ On ∧ ( bday “ 𝐴) ⊆ 𝑂)) ∧ 𝑢 ∈ 𝐴) → ( bday ‘𝑢) ∈ ( bday “ 𝐴))
61	57, 60	sseldd 3984	. . . . . . . . . . 11 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝑂 ∈ On ∧ ( bday “ 𝐴) ⊆ 𝑂)) ∧ 𝑢 ∈ 𝐴) → ( bday ‘𝑢) ∈ 𝑂)
62	56, 61	eqeltrrd 2842	. . . . . . . . . 10 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝑂 ∈ On ∧ ( bday “ 𝐴) ⊆ 𝑂)) ∧ 𝑢 ∈ 𝐴) → dom 𝑢 ∈ 𝑂)
63		onelss 6426	. . . . . . . . . 10 ⊢ (𝑂 ∈ On → (dom 𝑢 ∈ 𝑂 → dom 𝑢 ⊆ 𝑂))
64	52, 62, 63	sylc 65	. . . . . . . . 9 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝑂 ∈ On ∧ ( bday “ 𝐴) ⊆ 𝑂)) ∧ 𝑢 ∈ 𝐴) → dom 𝑢 ⊆ 𝑂)
65	64	sseld 3982	. . . . . . . 8 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝑂 ∈ On ∧ ( bday “ 𝐴) ⊆ 𝑂)) ∧ 𝑢 ∈ 𝐴) → (𝑦 ∈ dom 𝑢 → 𝑦 ∈ 𝑂))
66	65	adantrd 491	. . . . . . 7 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝑂 ∈ On ∧ ( bday “ 𝐴) ⊆ 𝑂)) ∧ 𝑢 ∈ 𝐴) → ((𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦))) → 𝑦 ∈ 𝑂))
67	66	rexlimdva 3155	. . . . . 6 ⊢ (((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝑂 ∈ On ∧ ( bday “ 𝐴) ⊆ 𝑂)) → (∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦))) → 𝑦 ∈ 𝑂))
68	67	abssdv 4068	. . . . 5 ⊢ (((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝑂 ∈ On ∧ ( bday “ 𝐴) ⊆ 𝑂)) → {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ⊆ 𝑂)
69	68	adantl 481	. . . 4 ⊢ ((¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝑂 ∈ On ∧ ( bday “ 𝐴) ⊆ 𝑂))) → {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ⊆ 𝑂)
70	51, 69	eqsstrd 4018	. . 3 ⊢ ((¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝑂 ∈ On ∧ ( bday “ 𝐴) ⊆ 𝑂))) → dom 𝑆 ⊆ 𝑂)
71	43, 70	pm2.61ian 812	. 2 ⊢ (((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝑂 ∈ On ∧ ( bday “ 𝐴) ⊆ 𝑂)) → dom 𝑆 ⊆ 𝑂)
72	5, 71	eqsstrd 4018	1 ⊢ (((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝑂 ∈ On ∧ ( bday “ 𝐴) ⊆ 𝑂)) → ( bday ‘𝑆) ⊆ 𝑂)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 395 ∧ w3a 1087 = wceq 1540 ∈ wcel 2108 {cab 2714 ∀wral 3061 ∃wrex 3070 ∃!wreu 3378 ∃*wrmo 3379 Vcvv 3480 ∪ cun 3949 ⊆ wss 3951 ifcif 4525 {csn 4626 ⟨cop 4632 class class class wbr 5143 ↦ cmpt 5225 dom cdm 5685 ↾ cres 5687 “ cima 5688 Ord word 6383 Oncon0 6384 suc csuc 6386 ℩cio 6512 Fn wfn 6556 –onto→wfo 6559 ‘cfv 6561 ℩crio 7387 2_oc2o 8500 No csur 27684 <s cslt 27685 bday cbday 27686

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2708 ax-rep 5279 ax-sep 5296 ax-nul 5306 ax-pow 5365 ax-pr 5432 ax-un 7755

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2892 df-ne 2941 df-ral 3062 df-rex 3071 df-rmo 3380 df-reu 3381 df-rab 3437 df-v 3482 df-sbc 3789 df-csb 3900 df-dif 3954 df-un 3956 df-in 3958 df-ss 3968 df-pss 3971 df-nul 4334 df-if 4526 df-pw 4602 df-sn 4627 df-pr 4629 df-tp 4631 df-op 4633 df-uni 4908 df-br 5144 df-opab 5206 df-mpt 5226 df-tr 5260 df-id 5578 df-eprel 5584 df-po 5592 df-so 5593 df-fr 5637 df-we 5639 df-xp 5691 df-rel 5692 df-cnv 5693 df-co 5694 df-dm 5695 df-rn 5696 df-res 5697 df-ima 5698 df-ord 6387 df-on 6388 df-suc 6390 df-iota 6514 df-fun 6563 df-fn 6564 df-f 6565 df-fo 6567 df-fv 6569 df-riota 7388 df-1o 8506 df-2o 8507 df-no 27687 df-slt 27688 df-bday 27689

This theorem is referenced by: noetalem1 27786

W3C validator