Theorem noinfbday 27954

Description: Birthday bounding law for surreal infimum. (Contributed by Scott Fenton, 8-Aug-2024.)

Hypothesis

Ref	Expression
noinfbday.1	⊢ 𝑇 = if(∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥, ((℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥), 1o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))))

Assertion

Ref	Expression
noinfbday	⊢ (((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑂 ∈ On ∧ ( bday “ 𝐵) ⊆ 𝑂)) → ( bday ‘𝑇) ⊆ 𝑂)

Distinct variable groups:   𝐵,𝑔,𝑢,𝑣,𝑥,𝑦   𝑔,𝑉

Allowed substitution hints:   𝑇(𝑥, 𝑦, 𝑣, 𝑢, 𝑔)   𝑂(𝑥, 𝑦, 𝑣, 𝑢, 𝑔)   𝑉(𝑥, 𝑦, 𝑣, 𝑢)

Proof of Theorem noinfbday

Dummy variables 𝑝 𝑧 𝑞 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		noinfbday.1	. . . . 5 ⊢ 𝑇 = if(∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥, ((℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥), 1o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))))
2	1	noinfno 27952	. . . 4 ⊢ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) → 𝑇 ∈ No )
3		bdayval 27882	. . . 4 ⊢ (𝑇 ∈ No → ( bday ‘𝑇) = dom 𝑇)
4	2, 3	syl 18	. . 3 ⊢ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) → ( bday ‘𝑇) = dom 𝑇)
5	4	adantr 486	. 2 ⊢ (((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑂 ∈ On ∧ ( bday “ 𝐵) ⊆ 𝑂)) → ( bday ‘𝑇) = dom 𝑇)
6		iftrue 4491	. . . . . . . 8 ⊢ (∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 → if(∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥, ((℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥), 1o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥)))) = ((℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥), 1o⟩}))
7	1, 6	eqtrid 2809	. . . . . . 7 ⊢ (∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 → 𝑇 = ((℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥), 1o⟩}))
8	7	dmeqd 5893	. . . . . 6 ⊢ (∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 → dom 𝑇 = dom ((℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥), 1o⟩}))
9		1oex 8468	. . . . . . . . 9 ⊢ 1o ∈ V
10	9	dmsnop 6216	. . . . . . . 8 ⊢ dom {⟨dom (℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥), 1o⟩} = {dom (℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥)}
11	10	uneq2i 4115	. . . . . . 7 ⊢ (dom (℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∪ dom {⟨dom (℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥), 1o⟩}) = (dom (℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∪ {dom (℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥)})
12		dmun 5898	. . . . . . 7 ⊢ dom ((℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥), 1o⟩}) = (dom (℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∪ dom {⟨dom (℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥), 1o⟩})
13		df-suc 6367	. . . . . . 7 ⊢ suc dom (℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) = (dom (℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∪ {dom (℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥)})
14	11, 12, 13	3eqtr4i 2795	. . . . . 6 ⊢ dom ((℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥), 1o⟩}) = suc dom (℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥)
15	8, 14	eqtrdi 2813	. . . . 5 ⊢ (∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 → dom 𝑇 = suc dom (℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥))
16	15	adantr 486	. . . 4 ⊢ ((∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑂 ∈ On ∧ ( bday “ 𝐵) ⊆ 𝑂))) → dom 𝑇 = suc dom (℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥))
17		simprrl 793	. . . . . 6 ⊢ ((∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑂 ∈ On ∧ ( bday “ 𝐵) ⊆ 𝑂))) → 𝑂 ∈ On)
18		eloni 6371	. . . . . 6 ⊢ (𝑂 ∈ On → Ord 𝑂)
19	17, 18	syl 18	. . . . 5 ⊢ ((∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑂 ∈ On ∧ ( bday “ 𝐵) ⊆ 𝑂))) → Ord 𝑂)
20		simprll 791	. . . . . . . 8 ⊢ ((∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑂 ∈ On ∧ ( bday “ 𝐵) ⊆ 𝑂))) → 𝐵 ⊆ No )
21		simpl 488	. . . . . . . . . 10 ⊢ ((∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑂 ∈ On ∧ ( bday “ 𝐵) ⊆ 𝑂))) → ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥)
22		nominmo 27933	. . . . . . . . . . 11 ⊢ (𝐵 ⊆ No → ∃*𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥)
23	20, 22	syl 18	. . . . . . . . . 10 ⊢ ((∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑂 ∈ On ∧ ( bday “ 𝐵) ⊆ 𝑂))) → ∃*𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥)
24		reu5 3369	. . . . . . . . . 10 ⊢ (∃!𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ↔ (∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ∃*𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥))
25	21, 23, 24	sylanbrc 595	. . . . . . . . 9 ⊢ ((∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑂 ∈ On ∧ ( bday “ 𝐵) ⊆ 𝑂))) → ∃!𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥)
26		riotacl 7390	. . . . . . . . 9 ⊢ (∃!𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 → (℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∈ 𝐵)
27	25, 26	syl 18	. . . . . . . 8 ⊢ ((∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑂 ∈ On ∧ ( bday “ 𝐵) ⊆ 𝑂))) → (℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∈ 𝐵)
28	20, 27	sseldd 3935	. . . . . . 7 ⊢ ((∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑂 ∈ On ∧ ( bday “ 𝐵) ⊆ 𝑂))) → (℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∈ No )
29		bdayval 27882	. . . . . . 7 ⊢ ((℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∈ No → ( bday ‘(℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥)) = dom (℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥))
30	28, 29	syl 18	. . . . . 6 ⊢ ((∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑂 ∈ On ∧ ( bday “ 𝐵) ⊆ 𝑂))) → ( bday ‘(℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥)) = dom (℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥))
31		simprrr 794	. . . . . . 7 ⊢ ((∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑂 ∈ On ∧ ( bday “ 𝐵) ⊆ 𝑂))) → ( bday “ 𝐵) ⊆ 𝑂)
32		bdayfo 27911	. . . . . . . . 9 ⊢ bday : No –onto→On
33		fofn 6795	. . . . . . . . 9 ⊢ ( bday : No –onto→On → bday Fn No )
34	32, 33	ax-mp 5	. . . . . . . 8 ⊢ bday Fn No
35		fnfvima 7235	. . . . . . . 8 ⊢ (( bday Fn No ∧ 𝐵 ⊆ No ∧ (℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∈ 𝐵) → ( bday ‘(℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥)) ∈ ( bday “ 𝐵))
36	34, 20, 27, 35	mp3an2i 1495	. . . . . . 7 ⊢ ((∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑂 ∈ On ∧ ( bday “ 𝐵) ⊆ 𝑂))) → ( bday ‘(℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥)) ∈ ( bday “ 𝐵))
37	31, 36	sseldd 3935	. . . . . 6 ⊢ ((∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑂 ∈ On ∧ ( bday “ 𝐵) ⊆ 𝑂))) → ( bday ‘(℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥)) ∈ 𝑂)
38	30, 37	eqeltrrd 2863	. . . . 5 ⊢ ((∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑂 ∈ On ∧ ( bday “ 𝐵) ⊆ 𝑂))) → dom (℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∈ 𝑂)
39		ordsucss 7817	. . . . 5 ⊢ (Ord 𝑂 → (dom (℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∈ 𝑂 → suc dom (℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ⊆ 𝑂))
40	19, 38, 39	sylc 66	. . . 4 ⊢ ((∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑂 ∈ On ∧ ( bday “ 𝐵) ⊆ 𝑂))) → suc dom (℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ⊆ 𝑂)
41	16, 40	eqsstrd 3968	. . 3 ⊢ ((∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑂 ∈ On ∧ ( bday “ 𝐵) ⊆ 𝑂))) → dom 𝑇 ⊆ 𝑂)
42	1	noinfdm 27953	. . . . 5 ⊢ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 → dom 𝑇 = {𝑧 ∣ ∃𝑝 ∈ 𝐵 (𝑧 ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐵 (¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑧) = (𝑞 ↾ suc 𝑧)))})
43	42	adantr 486	. . . 4 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑂 ∈ On ∧ ( bday “ 𝐵) ⊆ 𝑂))) → dom 𝑇 = {𝑧 ∣ ∃𝑝 ∈ 𝐵 (𝑧 ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐵 (¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑧) = (𝑞 ↾ suc 𝑧)))})
44		simplrl 789	. . . . . . . . . . 11 ⊢ ((((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑂 ∈ On ∧ ( bday “ 𝐵) ⊆ 𝑂)) ∧ 𝑝 ∈ 𝐵) → 𝑂 ∈ On)
45	44, 18	syl 18	. . . . . . . . . 10 ⊢ ((((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑂 ∈ On ∧ ( bday “ 𝐵) ⊆ 𝑂)) ∧ 𝑝 ∈ 𝐵) → Ord 𝑂)
46		ssel2 3929	. . . . . . . . . . . . 13 ⊢ ((𝐵 ⊆ No ∧ 𝑝 ∈ 𝐵) → 𝑝 ∈ No )
47	46	ad4ant14 765	. . . . . . . . . . . 12 ⊢ ((((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑂 ∈ On ∧ ( bday “ 𝐵) ⊆ 𝑂)) ∧ 𝑝 ∈ 𝐵) → 𝑝 ∈ No )
48		bdayval 27882	. . . . . . . . . . . 12 ⊢ (𝑝 ∈ No → ( bday ‘𝑝) = dom 𝑝)
49	47, 48	syl 18	. . . . . . . . . . 11 ⊢ ((((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑂 ∈ On ∧ ( bday “ 𝐵) ⊆ 𝑂)) ∧ 𝑝 ∈ 𝐵) → ( bday ‘𝑝) = dom 𝑝)
50		simplrr 790	. . . . . . . . . . . 12 ⊢ ((((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑂 ∈ On ∧ ( bday “ 𝐵) ⊆ 𝑂)) ∧ 𝑝 ∈ 𝐵) → ( bday “ 𝐵) ⊆ 𝑂)
51		fnfvima 7235	. . . . . . . . . . . . . 14 ⊢ (( bday Fn No ∧ 𝐵 ⊆ No ∧ 𝑝 ∈ 𝐵) → ( bday ‘𝑝) ∈ ( bday “ 𝐵))
52	34, 51	mp3an1 1477	. . . . . . . . . . . . 13 ⊢ ((𝐵 ⊆ No ∧ 𝑝 ∈ 𝐵) → ( bday ‘𝑝) ∈ ( bday “ 𝐵))
53	52	ad4ant14 765	. . . . . . . . . . . 12 ⊢ ((((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑂 ∈ On ∧ ( bday “ 𝐵) ⊆ 𝑂)) ∧ 𝑝 ∈ 𝐵) → ( bday ‘𝑝) ∈ ( bday “ 𝐵))
54	50, 53	sseldd 3935	. . . . . . . . . . 11 ⊢ ((((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑂 ∈ On ∧ ( bday “ 𝐵) ⊆ 𝑂)) ∧ 𝑝 ∈ 𝐵) → ( bday ‘𝑝) ∈ 𝑂)
55	49, 54	eqeltrrd 2863	. . . . . . . . . 10 ⊢ ((((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑂 ∈ On ∧ ( bday “ 𝐵) ⊆ 𝑂)) ∧ 𝑝 ∈ 𝐵) → dom 𝑝 ∈ 𝑂)
56		ordelss 6377	. . . . . . . . . 10 ⊢ ((Ord 𝑂 ∧ dom 𝑝 ∈ 𝑂) → dom 𝑝 ⊆ 𝑂)
57	45, 55, 56	syl2anc 596	. . . . . . . . 9 ⊢ ((((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑂 ∈ On ∧ ( bday “ 𝐵) ⊆ 𝑂)) ∧ 𝑝 ∈ 𝐵) → dom 𝑝 ⊆ 𝑂)
58	57	sseld 3933	. . . . . . . 8 ⊢ ((((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑂 ∈ On ∧ ( bday “ 𝐵) ⊆ 𝑂)) ∧ 𝑝 ∈ 𝐵) → (𝑧 ∈ dom 𝑝 → 𝑧 ∈ 𝑂))
59	58	adantrd 497	. . . . . . 7 ⊢ ((((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑂 ∈ On ∧ ( bday “ 𝐵) ⊆ 𝑂)) ∧ 𝑝 ∈ 𝐵) → ((𝑧 ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐵 (¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑧) = (𝑞 ↾ suc 𝑧))) → 𝑧 ∈ 𝑂))
60	59	rexlimdva 3165	. . . . . 6 ⊢ (((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑂 ∈ On ∧ ( bday “ 𝐵) ⊆ 𝑂)) → (∃𝑝 ∈ 𝐵 (𝑧 ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐵 (¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑧) = (𝑞 ↾ suc 𝑧))) → 𝑧 ∈ 𝑂))
61	60	abssdv 4018	. . . . 5 ⊢ (((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑂 ∈ On ∧ ( bday “ 𝐵) ⊆ 𝑂)) → {𝑧 ∣ ∃𝑝 ∈ 𝐵 (𝑧 ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐵 (¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑧) = (𝑞 ↾ suc 𝑧)))} ⊆ 𝑂)
62	61	adantl 487	. . . 4 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑂 ∈ On ∧ ( bday “ 𝐵) ⊆ 𝑂))) → {𝑧 ∣ ∃𝑝 ∈ 𝐵 (𝑧 ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐵 (¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑧) = (𝑞 ↾ suc 𝑧)))} ⊆ 𝑂)
63	43, 62	eqsstrd 3968	. . 3 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑂 ∈ On ∧ ( bday “ 𝐵) ⊆ 𝑂))) → dom 𝑇 ⊆ 𝑂)
64	41, 63	pm2.61ian 824	. 2 ⊢ (((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑂 ∈ On ∧ ( bday “ 𝐵) ⊆ 𝑂)) → dom 𝑇 ⊆ 𝑂)
65	5, 64	eqsstrd 3968	1 ⊢ (((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑂 ∈ On ∧ ( bday “ 𝐵) ⊆ 𝑂)) → ( bday ‘𝑇) ⊆ 𝑂)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401   ∧ w3a 1103   = wceq 1570   ∈ wcel 2145  {cab 2740  ∀wral 3078  ∃wrex 3088  ∃!wreu 3365  ∃*wrmo 3366   ∪ cun 3900   ⊆ wss 3902  ifcif 4485  {csn 4587  ⟨cop 4593   class class class wbr 5107   ↦ cmpt 5190  dom cdm 5659   ↾ cres 5661   “ cima 5662  Ord word 6360  Oncon0 6361  suc csuc 6363  ℩cio 6491   Fn wfn 6532  –onto→wfo 6535  ‘cfv 6537  ℩crio 7372  1_oc1o 8451   No csur 27874   <s clts 27875   bday cbday 27876

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734  ax-rep 5236  ax-sep 5255  ax-nul 5267  ax-pow 5334  ax-pr 5402  ax-un 7739

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3079  df-rex 3089  df-rmo 3367  df-reu 3368  df-rab 3415  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-tp 4592  df-op 4594  df-uni 4871  df-br 5108  df-opab 5172  df-mpt 5191  df-tr 5217  df-id 5554  df-eprel 5559  df-po 5567  df-so 5568  df-fr 5612  df-we 5614  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-ord 6364  df-on 6365  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-fo 6543  df-fv 6545  df-riota 7373  df-1o 8458  df-2o 8459  df-no 27877  df-lts 27878  df-bday 27879

This theorem is used by:  noetalem1  27975