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 27690

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 27688	. . . 4 ⊢ ((𝐴 ⊆ No ∧ 𝐴 ∈ V) → 𝑆 ∈ No )
3	2	adantr 480	. . 3 ⊢ (((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝑂 ∈ On ∧ ( bday “ 𝐴) ⊆ 𝑂)) → 𝑆 ∈ No )
4		bdayval 27633	. . 3 ⊢ (𝑆 ∈ No → ( bday ‘𝑆) = dom 𝑆)
5	3, 4	syl 17	. 2 ⊢ (((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝑂 ∈ On ∧ ( bday “ 𝐴) ⊆ 𝑂)) → ( bday ‘𝑆) = dom 𝑆)
6		iftrue 4487	. . . . . . . 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 2784	. . . . . . 7 ⊢ (∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 → 𝑆 = ((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2_o⟩}))
8	7	dmeqd 5864	. . . . . 6 ⊢ (∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 → dom 𝑆 = dom ((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2_o⟩}))
9		2oex 8420	. . . . . . . . 9 ⊢ 2_o ∈ V
10	9	dmsnop 6184	. . . . . . . 8 ⊢ dom {⟨dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2_o⟩} = {dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦)}
11	10	uneq2i 4119	. . . . . . 7 ⊢ (dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ dom {⟨dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2_o⟩}) = (dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ {dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦)})
12		dmun 5869	. . . . . . 7 ⊢ dom ((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2_o⟩}) = (dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ dom {⟨dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2_o⟩})
13		df-suc 6333	. . . . . . 7 ⊢ suc dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) = (dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ {dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦)})
14	11, 12, 13	3eqtr4i 2770	. . . . . 6 ⊢ dom ((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2_o⟩}) = suc dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦)
15	8, 14	eqtrdi 2788	. . . . 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 6337	. . . . . 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 27683	. . . . . . . . . . . . 13 ⊢ (𝐴 ⊆ No → ∃*𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦)
23	22	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝐴 ⊆ No ∧ 𝐴 ∈ V) → ∃*𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦)
24	23	adantl 481	. . . . . . . . . . 11 ⊢ ((∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V)) → ∃*𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦)
25		reu5 3354	. . . . . . . . . . 11 ⊢ (∃!𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ↔ (∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ∃*𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦))
26	21, 24, 25	sylanbrc 584	. . . . . . . . . 10 ⊢ ((∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V)) → ∃!𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦)
27	26	adantrr 718	. . . . . . . . 9 ⊢ ((∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝑂 ∈ On ∧ ( bday “ 𝐴) ⊆ 𝑂))) → ∃!𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦)
28		riotacl 7344	. . . . . . . . 9 ⊢ (∃!𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 → (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∈ 𝐴)
29	27, 28	syl 17	. . . . . . . 8 ⊢ ((∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝑂 ∈ On ∧ ( bday “ 𝐴) ⊆ 𝑂))) → (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∈ 𝐴)
30	20, 29	sseldd 3936	. . . . . . 7 ⊢ ((∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝑂 ∈ On ∧ ( bday “ 𝐴) ⊆ 𝑂))) → (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∈ No )
31		bdayval 27633	. . . . . . 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 27662	. . . . . . . . 9 ⊢ bday : No –onto→On
35		fofn 6758	. . . . . . . . 9 ⊢ ( bday : No –onto→On → bday Fn No )
36	34, 35	ax-mp 5	. . . . . . . 8 ⊢ bday Fn No
37		fnfvima 7191	. . . . . . . 8 ⊢ (( bday Fn No ∧ 𝐴 ⊆ No ∧ (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∈ 𝐴) → ( bday ‘(℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦)) ∈ ( bday “ 𝐴))
38	36, 20, 29, 37	mp3an2i 1469	. . . . . . 7 ⊢ ((∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝑂 ∈ On ∧ ( bday “ 𝐴) ⊆ 𝑂))) → ( bday ‘(℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦)) ∈ ( bday “ 𝐴))
39	33, 38	sseldd 3936	. . . . . 6 ⊢ ((∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝑂 ∈ On ∧ ( bday “ 𝐴) ⊆ 𝑂))) → ( bday ‘(℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦)) ∈ 𝑂)
40	32, 39	eqeltrrd 2838	. . . . 5 ⊢ ((∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝑂 ∈ On ∧ ( bday “ 𝐴) ⊆ 𝑂))) → dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∈ 𝑂)
41		ordsucss 7772	. . . . 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 3970	. . 3 ⊢ ((∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝑂 ∈ On ∧ ( bday “ 𝐴) ⊆ 𝑂))) → dom 𝑆 ⊆ 𝑂)
44		iffalse 4490	. . . . . . . 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 2784	. . . . . . 7 ⊢ (¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 → 𝑆 = (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))))
46	45	dmeqd 5864	. . . . . 6 ⊢ (¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 → dom 𝑆 = dom (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))))
47		iotaex 6478	. . . . . . 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 6646	. . . . . 6 ⊢ dom (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))) = {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))}
50	46, 49	eqtrdi 2788	. . . . 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 3930	. . . . . . . . . . . . 13 ⊢ ((𝐴 ⊆ No ∧ 𝑢 ∈ 𝐴) → 𝑢 ∈ No )
54	53	ad4ant14 753	. . . . . . . . . . . 12 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝑂 ∈ On ∧ ( bday “ 𝐴) ⊆ 𝑂)) ∧ 𝑢 ∈ 𝐴) → 𝑢 ∈ No )
55		bdayval 27633	. . . . . . . . . . . 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 7191	. . . . . . . . . . . . . 14 ⊢ (( bday Fn No ∧ 𝐴 ⊆ No ∧ 𝑢 ∈ 𝐴) → ( bday ‘𝑢) ∈ ( bday “ 𝐴))
59	36, 58	mp3an1 1451	. . . . . . . . . . . . 13 ⊢ ((𝐴 ⊆ No ∧ 𝑢 ∈ 𝐴) → ( bday ‘𝑢) ∈ ( bday “ 𝐴))
60	59	ad4ant14 753	. . . . . . . . . . . 12 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝑂 ∈ On ∧ ( bday “ 𝐴) ⊆ 𝑂)) ∧ 𝑢 ∈ 𝐴) → ( bday ‘𝑢) ∈ ( bday “ 𝐴))
61	57, 60	sseldd 3936	. . . . . . . . . . 11 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝑂 ∈ On ∧ ( bday “ 𝐴) ⊆ 𝑂)) ∧ 𝑢 ∈ 𝐴) → ( bday ‘𝑢) ∈ 𝑂)
62	56, 61	eqeltrrd 2838	. . . . . . . . . 10 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝑂 ∈ On ∧ ( bday “ 𝐴) ⊆ 𝑂)) ∧ 𝑢 ∈ 𝐴) → dom 𝑢 ∈ 𝑂)
63		onelss 6369	. . . . . . . . . 10 ⊢ (𝑂 ∈ On → (dom 𝑢 ∈ 𝑂 → dom 𝑢 ⊆ 𝑂))
64	52, 62, 63	sylc 65	. . . . . . . . 9 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝑂 ∈ On ∧ ( bday “ 𝐴) ⊆ 𝑂)) ∧ 𝑢 ∈ 𝐴) → dom 𝑢 ⊆ 𝑂)
65	64	sseld 3934	. . . . . . . 8 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝑂 ∈ On ∧ ( bday “ 𝐴) ⊆ 𝑂)) ∧ 𝑢 ∈ 𝐴) → (𝑦 ∈ dom 𝑢 → 𝑦 ∈ 𝑂))
66	65	adantrd 491	. . . . . . 7 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝑂 ∈ On ∧ ( bday “ 𝐴) ⊆ 𝑂)) ∧ 𝑢 ∈ 𝐴) → ((𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦))) → 𝑦 ∈ 𝑂))
67	66	rexlimdva 3139	. . . . . 6 ⊢ (((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝑂 ∈ On ∧ ( bday “ 𝐴) ⊆ 𝑂)) → (∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦))) → 𝑦 ∈ 𝑂))
68	67	abssdv 4021	. . . . 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 3970	. . 3 ⊢ ((¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝑂 ∈ On ∧ ( bday “ 𝐴) ⊆ 𝑂))) → dom 𝑆 ⊆ 𝑂)
71	43, 70	pm2.61ian 812	. 2 ⊢ (((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝑂 ∈ On ∧ ( bday “ 𝐴) ⊆ 𝑂)) → dom 𝑆 ⊆ 𝑂)
72	5, 71	eqsstrd 3970	1 ⊢ (((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝑂 ∈ On ∧ ( bday “ 𝐴) ⊆ 𝑂)) → ( bday ‘𝑆) ⊆ 𝑂)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 395 ∧ w3a 1087 = wceq 1542 ∈ wcel 2114 {cab 2715 ∀wral 3052 ∃wrex 3062 ∃!wreu 3350 ∃*wrmo 3351 Vcvv 3442 ∪ cun 3901 ⊆ wss 3903 ifcif 4481 {csn 4582 ⟨cop 4588 class class class wbr 5100 ↦ cmpt 5181 dom cdm 5634 ↾ cres 5636 “ cima 5637 Ord word 6326 Oncon0 6327 suc csuc 6329 ℩cio 6456 Fn wfn 6497 –onto→wfo 6500 ‘cfv 6502 ℩crio 7326 2_oc2o 8403 No csur 27624 <s clts 27625 bday cbday 27626

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 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-rep 5226 ax-sep 5245 ax-nul 5255 ax-pow 5314 ax-pr 5381 ax-un 7692

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-ral 3053 df-rex 3063 df-rmo 3352 df-reu 3353 df-rab 3402 df-v 3444 df-sbc 3743 df-csb 3852 df-dif 3906 df-un 3908 df-in 3910 df-ss 3920 df-pss 3923 df-nul 4288 df-if 4482 df-pw 4558 df-sn 4583 df-pr 4585 df-tp 4587 df-op 4589 df-uni 4866 df-br 5101 df-opab 5163 df-mpt 5182 df-tr 5208 df-id 5529 df-eprel 5534 df-po 5542 df-so 5543 df-fr 5587 df-we 5589 df-xp 5640 df-rel 5641 df-cnv 5642 df-co 5643 df-dm 5644 df-rn 5645 df-res 5646 df-ima 5647 df-ord 6330 df-on 6331 df-suc 6333 df-iota 6458 df-fun 6504 df-fn 6505 df-f 6506 df-fo 6508 df-fv 6510 df-riota 7327 df-1o 8409 df-2o 8410 df-no 27627 df-lts 27628 df-bday 27629

This theorem is referenced by: noetalem1 27726

W3C validator