Theorem nobnddown 31100

Description: Any set of surreals is bounded below by a surreal with a birthday no greater than the successor of their maximum birthday. (Contributed by Scott Fenton, 10-Apr-2017.)

Assertion

Ref	Expression
nobnddown	⊢ ((𝐴 ⊆ No ∧ 𝐴 ∈ 𝑉) → ∃𝑥 ∈ No (∀𝑦 ∈ 𝐴 𝑥 <s 𝑦 ∧ ( bday ‘𝑥) ⊆ suc ∪ ( bday “ 𝐴)))

Distinct variable group:   𝑥,𝐴,𝑦

Allowed substitution hints:   𝑉(𝑥,𝑦)

Proof of Theorem nobnddown

Dummy variables 𝑎 𝑏 𝑐 𝑑 𝑘 𝑛 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		elex 3185	. 2 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V)
2		1on 7454	. . . . . . 7 ⊢ 1𝑜 ∈ On
3	2	elexi 3186	. . . . . 6 ⊢ 1𝑜 ∈ V
4	3	prid1 4241	. . . . 5 ⊢ 1𝑜 ∈ {1𝑜, 2𝑜}
5		eqid 2610	. . . . 5 ⊢ ∩ {𝑎 ∈ On ∣ ∀𝑛 ∈ 𝐴 ∃𝑏 ∈ 𝑎 (𝑛‘𝑏) ≠ 1𝑜} = ∩ {𝑎 ∈ On ∣ ∀𝑛 ∈ 𝐴 ∃𝑏 ∈ 𝑎 (𝑛‘𝑏) ≠ 1𝑜}
6	4, 5	nobndlem2 31092	. . . 4 ⊢ ((𝐴 ⊆ No ∧ 𝐴 ∈ V) → ∩ {𝑎 ∈ On ∣ ∀𝑛 ∈ 𝐴 ∃𝑏 ∈ 𝑎 (𝑛‘𝑏) ≠ 1𝑜} ∈ On)
7		noxp1o 31063	. . . 4 ⊢ (∩ {𝑎 ∈ On ∣ ∀𝑛 ∈ 𝐴 ∃𝑏 ∈ 𝑎 (𝑛‘𝑏) ≠ 1𝑜} ∈ On → (∩ {𝑎 ∈ On ∣ ∀𝑛 ∈ 𝐴 ∃𝑏 ∈ 𝑎 (𝑛‘𝑏) ≠ 1𝑜} × {1𝑜}) ∈ No )
8	6, 7	syl 17	. . 3 ⊢ ((𝐴 ⊆ No ∧ 𝐴 ∈ V) → (∩ {𝑎 ∈ On ∣ ∀𝑛 ∈ 𝐴 ∃𝑏 ∈ 𝑎 (𝑛‘𝑏) ≠ 1𝑜} × {1𝑜}) ∈ No )
9	8	adantr 480	. . . . 5 ⊢ (((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ 𝐴) → (∩ {𝑎 ∈ On ∣ ∀𝑛 ∈ 𝐴 ∃𝑏 ∈ 𝑎 (𝑛‘𝑏) ≠ 1𝑜} × {1𝑜}) ∈ No )
10		ssel2 3563	. . . . . 6 ⊢ ((𝐴 ⊆ No ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ No )
11	10	adantlr 747	. . . . 5 ⊢ (((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ No )
12	4	nobndlem4 31094	. . . . . . . 8 ⊢ (𝑦 ∈ No → ∩ {𝑘 ∈ On ∣ (𝑦‘𝑘) ≠ 1𝑜} ∈ On)
13	10, 12	syl 17	. . . . . . 7 ⊢ ((𝐴 ⊆ No ∧ 𝑦 ∈ 𝐴) → ∩ {𝑘 ∈ On ∣ (𝑦‘𝑘) ≠ 1𝑜} ∈ On)
14	13	adantlr 747	. . . . . 6 ⊢ (((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ 𝐴) → ∩ {𝑘 ∈ On ∣ (𝑦‘𝑘) ≠ 1𝑜} ∈ On)
15	6	adantr 480	. . . . . . . . . . 11 ⊢ (((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ 𝐴) → ∩ {𝑎 ∈ On ∣ ∀𝑛 ∈ 𝐴 ∃𝑏 ∈ 𝑎 (𝑛‘𝑏) ≠ 1𝑜} ∈ On)
16	4, 5	nobndlem6 31096	. . . . . . . . . . . 12 ⊢ ((𝐴 ⊆ No ∧ 𝑦 ∈ 𝐴) → ∩ {𝑘 ∈ On ∣ (𝑦‘𝑘) ≠ 1𝑜} ∈ ∩ {𝑎 ∈ On ∣ ∀𝑛 ∈ 𝐴 ∃𝑏 ∈ 𝑎 (𝑛‘𝑏) ≠ 1𝑜})
17	16	adantlr 747	. . . . . . . . . . 11 ⊢ (((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ 𝐴) → ∩ {𝑘 ∈ On ∣ (𝑦‘𝑘) ≠ 1𝑜} ∈ ∩ {𝑎 ∈ On ∣ ∀𝑛 ∈ 𝐴 ∃𝑏 ∈ 𝑎 (𝑛‘𝑏) ≠ 1𝑜})
18		onelss 5683	. . . . . . . . . . 11 ⊢ (∩ {𝑎 ∈ On ∣ ∀𝑛 ∈ 𝐴 ∃𝑏 ∈ 𝑎 (𝑛‘𝑏) ≠ 1𝑜} ∈ On → (∩ {𝑘 ∈ On ∣ (𝑦‘𝑘) ≠ 1𝑜} ∈ ∩ {𝑎 ∈ On ∣ ∀𝑛 ∈ 𝐴 ∃𝑏 ∈ 𝑎 (𝑛‘𝑏) ≠ 1𝑜} → ∩ {𝑘 ∈ On ∣ (𝑦‘𝑘) ≠ 1𝑜} ⊆ ∩ {𝑎 ∈ On ∣ ∀𝑛 ∈ 𝐴 ∃𝑏 ∈ 𝑎 (𝑛‘𝑏) ≠ 1𝑜}))
19	15, 17, 18	sylc 63	. . . . . . . . . 10 ⊢ (((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ 𝐴) → ∩ {𝑘 ∈ On ∣ (𝑦‘𝑘) ≠ 1𝑜} ⊆ ∩ {𝑎 ∈ On ∣ ∀𝑛 ∈ 𝐴 ∃𝑏 ∈ 𝑎 (𝑛‘𝑏) ≠ 1𝑜})
20	19	sselda 3568	. . . . . . . . 9 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ 𝐴) ∧ 𝑑 ∈ ∩ {𝑘 ∈ On ∣ (𝑦‘𝑘) ≠ 1𝑜}) → 𝑑 ∈ ∩ {𝑎 ∈ On ∣ ∀𝑛 ∈ 𝐴 ∃𝑏 ∈ 𝑎 (𝑛‘𝑏) ≠ 1𝑜})
21	3	fvconst2 6374	. . . . . . . . 9 ⊢ (𝑑 ∈ ∩ {𝑎 ∈ On ∣ ∀𝑛 ∈ 𝐴 ∃𝑏 ∈ 𝑎 (𝑛‘𝑏) ≠ 1𝑜} → ((∩ {𝑎 ∈ On ∣ ∀𝑛 ∈ 𝐴 ∃𝑏 ∈ 𝑎 (𝑛‘𝑏) ≠ 1𝑜} × {1𝑜})‘𝑑) = 1𝑜)
22	20, 21	syl 17	. . . . . . . 8 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ 𝐴) ∧ 𝑑 ∈ ∩ {𝑘 ∈ On ∣ (𝑦‘𝑘) ≠ 1𝑜}) → ((∩ {𝑎 ∈ On ∣ ∀𝑛 ∈ 𝐴 ∃𝑏 ∈ 𝑎 (𝑛‘𝑏) ≠ 1𝑜} × {1𝑜})‘𝑑) = 1𝑜)
23	14	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ 𝐴) ∧ 𝑑 ∈ ∩ {𝑘 ∈ On ∣ (𝑦‘𝑘) ≠ 1𝑜}) → ∩ {𝑘 ∈ On ∣ (𝑦‘𝑘) ≠ 1𝑜} ∈ On)
24		onss 6882	. . . . . . . . . . . . . . . . . 18 ⊢ (∩ {𝑘 ∈ On ∣ (𝑦‘𝑘) ≠ 1𝑜} ∈ On → ∩ {𝑘 ∈ On ∣ (𝑦‘𝑘) ≠ 1𝑜} ⊆ On)
25	14, 24	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ 𝐴) → ∩ {𝑘 ∈ On ∣ (𝑦‘𝑘) ≠ 1𝑜} ⊆ On)
26	25	sselda 3568	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ 𝐴) ∧ 𝑑 ∈ ∩ {𝑘 ∈ On ∣ (𝑦‘𝑘) ≠ 1𝑜}) → 𝑑 ∈ On)
27		ontri1 5674	. . . . . . . . . . . . . . . 16 ⊢ ((∩ {𝑘 ∈ On ∣ (𝑦‘𝑘) ≠ 1𝑜} ∈ On ∧ 𝑑 ∈ On) → (∩ {𝑘 ∈ On ∣ (𝑦‘𝑘) ≠ 1𝑜} ⊆ 𝑑 ↔ ¬ 𝑑 ∈ ∩ {𝑘 ∈ On ∣ (𝑦‘𝑘) ≠ 1𝑜}))
28	23, 26, 27	syl2anc 691	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ 𝐴) ∧ 𝑑 ∈ ∩ {𝑘 ∈ On ∣ (𝑦‘𝑘) ≠ 1𝑜}) → (∩ {𝑘 ∈ On ∣ (𝑦‘𝑘) ≠ 1𝑜} ⊆ 𝑑 ↔ ¬ 𝑑 ∈ ∩ {𝑘 ∈ On ∣ (𝑦‘𝑘) ≠ 1𝑜}))
29	28	biimpd 218	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ 𝐴) ∧ 𝑑 ∈ ∩ {𝑘 ∈ On ∣ (𝑦‘𝑘) ≠ 1𝑜}) → (∩ {𝑘 ∈ On ∣ (𝑦‘𝑘) ≠ 1𝑜} ⊆ 𝑑 → ¬ 𝑑 ∈ ∩ {𝑘 ∈ On ∣ (𝑦‘𝑘) ≠ 1𝑜}))
30	29	con2d 128	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ 𝐴) ∧ 𝑑 ∈ ∩ {𝑘 ∈ On ∣ (𝑦‘𝑘) ≠ 1𝑜}) → (𝑑 ∈ ∩ {𝑘 ∈ On ∣ (𝑦‘𝑘) ≠ 1𝑜} → ¬ ∩ {𝑘 ∈ On ∣ (𝑦‘𝑘) ≠ 1𝑜} ⊆ 𝑑))
31	30	ex 449	. . . . . . . . . . . 12 ⊢ (((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ 𝐴) → (𝑑 ∈ ∩ {𝑘 ∈ On ∣ (𝑦‘𝑘) ≠ 1𝑜} → (𝑑 ∈ ∩ {𝑘 ∈ On ∣ (𝑦‘𝑘) ≠ 1𝑜} → ¬ ∩ {𝑘 ∈ On ∣ (𝑦‘𝑘) ≠ 1𝑜} ⊆ 𝑑)))
32	31	pm2.43d 51	. . . . . . . . . . 11 ⊢ (((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ 𝐴) → (𝑑 ∈ ∩ {𝑘 ∈ On ∣ (𝑦‘𝑘) ≠ 1𝑜} → ¬ ∩ {𝑘 ∈ On ∣ (𝑦‘𝑘) ≠ 1𝑜} ⊆ 𝑑))
33	32	imp 444	. . . . . . . . . 10 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ 𝐴) ∧ 𝑑 ∈ ∩ {𝑘 ∈ On ∣ (𝑦‘𝑘) ≠ 1𝑜}) → ¬ ∩ {𝑘 ∈ On ∣ (𝑦‘𝑘) ≠ 1𝑜} ⊆ 𝑑)
34		intss1 4427	. . . . . . . . . 10 ⊢ (𝑑 ∈ {𝑘 ∈ On ∣ (𝑦‘𝑘) ≠ 1𝑜} → ∩ {𝑘 ∈ On ∣ (𝑦‘𝑘) ≠ 1𝑜} ⊆ 𝑑)
35	33, 34	nsyl 134	. . . . . . . . 9 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ 𝐴) ∧ 𝑑 ∈ ∩ {𝑘 ∈ On ∣ (𝑦‘𝑘) ≠ 1𝑜}) → ¬ 𝑑 ∈ {𝑘 ∈ On ∣ (𝑦‘𝑘) ≠ 1𝑜})
36		df-ne 2782	. . . . . . . . . 10 ⊢ ((𝑦‘𝑑) ≠ 1𝑜 ↔ ¬ (𝑦‘𝑑) = 1𝑜)
37		fveq2 6103	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑑 → (𝑦‘𝑘) = (𝑦‘𝑑))
38	37	neeq1d 2841	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑑 → ((𝑦‘𝑘) ≠ 1𝑜 ↔ (𝑦‘𝑑) ≠ 1𝑜))
39	38	elrab3 3332	. . . . . . . . . . . 12 ⊢ (𝑑 ∈ On → (𝑑 ∈ {𝑘 ∈ On ∣ (𝑦‘𝑘) ≠ 1𝑜} ↔ (𝑦‘𝑑) ≠ 1𝑜))
40	39	biimprd 237	. . . . . . . . . . 11 ⊢ (𝑑 ∈ On → ((𝑦‘𝑑) ≠ 1𝑜 → 𝑑 ∈ {𝑘 ∈ On ∣ (𝑦‘𝑘) ≠ 1𝑜}))
41	26, 40	syl 17	. . . . . . . . . 10 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ 𝐴) ∧ 𝑑 ∈ ∩ {𝑘 ∈ On ∣ (𝑦‘𝑘) ≠ 1𝑜}) → ((𝑦‘𝑑) ≠ 1𝑜 → 𝑑 ∈ {𝑘 ∈ On ∣ (𝑦‘𝑘) ≠ 1𝑜}))
42	36, 41	syl5bir 232	. . . . . . . . 9 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ 𝐴) ∧ 𝑑 ∈ ∩ {𝑘 ∈ On ∣ (𝑦‘𝑘) ≠ 1𝑜}) → (¬ (𝑦‘𝑑) = 1𝑜 → 𝑑 ∈ {𝑘 ∈ On ∣ (𝑦‘𝑘) ≠ 1𝑜}))
43	35, 42	mt3d 139	. . . . . . . 8 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ 𝐴) ∧ 𝑑 ∈ ∩ {𝑘 ∈ On ∣ (𝑦‘𝑘) ≠ 1𝑜}) → (𝑦‘𝑑) = 1𝑜)
44	22, 43	eqtr4d 2647	. . . . . . 7 ⊢ ((((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ 𝐴) ∧ 𝑑 ∈ ∩ {𝑘 ∈ On ∣ (𝑦‘𝑘) ≠ 1𝑜}) → ((∩ {𝑎 ∈ On ∣ ∀𝑛 ∈ 𝐴 ∃𝑏 ∈ 𝑎 (𝑛‘𝑏) ≠ 1𝑜} × {1𝑜})‘𝑑) = (𝑦‘𝑑))
45	44	ralrimiva 2949	. . . . . 6 ⊢ (((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ 𝐴) → ∀𝑑 ∈ ∩ {𝑘 ∈ On ∣ (𝑦‘𝑘) ≠ 1𝑜} ((∩ {𝑎 ∈ On ∣ ∀𝑛 ∈ 𝐴 ∃𝑏 ∈ 𝑎 (𝑛‘𝑏) ≠ 1𝑜} × {1𝑜})‘𝑑) = (𝑦‘𝑑))
46	3	fvconst2 6374	. . . . . . . 8 ⊢ (∩ {𝑘 ∈ On ∣ (𝑦‘𝑘) ≠ 1𝑜} ∈ ∩ {𝑎 ∈ On ∣ ∀𝑛 ∈ 𝐴 ∃𝑏 ∈ 𝑎 (𝑛‘𝑏) ≠ 1𝑜} → ((∩ {𝑎 ∈ On ∣ ∀𝑛 ∈ 𝐴 ∃𝑏 ∈ 𝑎 (𝑛‘𝑏) ≠ 1𝑜} × {1𝑜})‘∩ {𝑘 ∈ On ∣ (𝑦‘𝑘) ≠ 1𝑜}) = 1𝑜)
47	17, 46	syl 17	. . . . . . 7 ⊢ (((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ 𝐴) → ((∩ {𝑎 ∈ On ∣ ∀𝑛 ∈ 𝐴 ∃𝑏 ∈ 𝑎 (𝑛‘𝑏) ≠ 1𝑜} × {1𝑜})‘∩ {𝑘 ∈ On ∣ (𝑦‘𝑘) ≠ 1𝑜}) = 1𝑜)
48	4	nobndlem5 31095	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ No → (𝑦‘∩ {𝑘 ∈ On ∣ (𝑦‘𝑘) ≠ 1𝑜}) ≠ 1𝑜)
49	11, 48	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ 𝐴) → (𝑦‘∩ {𝑘 ∈ On ∣ (𝑦‘𝑘) ≠ 1𝑜}) ≠ 1𝑜)
50	49	neneqd 2787	. . . . . . . . . . . 12 ⊢ (((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ 𝐴) → ¬ (𝑦‘∩ {𝑘 ∈ On ∣ (𝑦‘𝑘) ≠ 1𝑜}) = 1𝑜)
51		nofv 31054	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ No → ((𝑦‘∩ {𝑘 ∈ On ∣ (𝑦‘𝑘) ≠ 1𝑜}) = ∅ ∨ (𝑦‘∩ {𝑘 ∈ On ∣ (𝑦‘𝑘) ≠ 1𝑜}) = 1𝑜 ∨ (𝑦‘∩ {𝑘 ∈ On ∣ (𝑦‘𝑘) ≠ 1𝑜}) = 2𝑜))
52	11, 51	syl 17	. . . . . . . . . . . 12 ⊢ (((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ 𝐴) → ((𝑦‘∩ {𝑘 ∈ On ∣ (𝑦‘𝑘) ≠ 1𝑜}) = ∅ ∨ (𝑦‘∩ {𝑘 ∈ On ∣ (𝑦‘𝑘) ≠ 1𝑜}) = 1𝑜 ∨ (𝑦‘∩ {𝑘 ∈ On ∣ (𝑦‘𝑘) ≠ 1𝑜}) = 2𝑜))
53		3orel2 30847	. . . . . . . . . . . 12 ⊢ (¬ (𝑦‘∩ {𝑘 ∈ On ∣ (𝑦‘𝑘) ≠ 1𝑜}) = 1𝑜 → (((𝑦‘∩ {𝑘 ∈ On ∣ (𝑦‘𝑘) ≠ 1𝑜}) = ∅ ∨ (𝑦‘∩ {𝑘 ∈ On ∣ (𝑦‘𝑘) ≠ 1𝑜}) = 1𝑜 ∨ (𝑦‘∩ {𝑘 ∈ On ∣ (𝑦‘𝑘) ≠ 1𝑜}) = 2𝑜) → ((𝑦‘∩ {𝑘 ∈ On ∣ (𝑦‘𝑘) ≠ 1𝑜}) = ∅ ∨ (𝑦‘∩ {𝑘 ∈ On ∣ (𝑦‘𝑘) ≠ 1𝑜}) = 2𝑜)))
54	50, 52, 53	sylc 63	. . . . . . . . . . 11 ⊢ (((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ 𝐴) → ((𝑦‘∩ {𝑘 ∈ On ∣ (𝑦‘𝑘) ≠ 1𝑜}) = ∅ ∨ (𝑦‘∩ {𝑘 ∈ On ∣ (𝑦‘𝑘) ≠ 1𝑜}) = 2𝑜))
55		eqid 2610	. . . . . . . . . . 11 ⊢ 1𝑜 = 1𝑜
56	54, 55	jctil 558	. . . . . . . . . 10 ⊢ (((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ 𝐴) → (1𝑜 = 1𝑜 ∧ ((𝑦‘∩ {𝑘 ∈ On ∣ (𝑦‘𝑘) ≠ 1𝑜}) = ∅ ∨ (𝑦‘∩ {𝑘 ∈ On ∣ (𝑦‘𝑘) ≠ 1𝑜}) = 2𝑜)))
57		andi 907	. . . . . . . . . 10 ⊢ ((1𝑜 = 1𝑜 ∧ ((𝑦‘∩ {𝑘 ∈ On ∣ (𝑦‘𝑘) ≠ 1𝑜}) = ∅ ∨ (𝑦‘∩ {𝑘 ∈ On ∣ (𝑦‘𝑘) ≠ 1𝑜}) = 2𝑜)) ↔ ((1𝑜 = 1𝑜 ∧ (𝑦‘∩ {𝑘 ∈ On ∣ (𝑦‘𝑘) ≠ 1𝑜}) = ∅) ∨ (1𝑜 = 1𝑜 ∧ (𝑦‘∩ {𝑘 ∈ On ∣ (𝑦‘𝑘) ≠ 1𝑜}) = 2𝑜)))
58	56, 57	sylib 207	. . . . . . . . 9 ⊢ (((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ 𝐴) → ((1𝑜 = 1𝑜 ∧ (𝑦‘∩ {𝑘 ∈ On ∣ (𝑦‘𝑘) ≠ 1𝑜}) = ∅) ∨ (1𝑜 = 1𝑜 ∧ (𝑦‘∩ {𝑘 ∈ On ∣ (𝑦‘𝑘) ≠ 1𝑜}) = 2𝑜)))
59	58	orcd 406	. . . . . . . 8 ⊢ (((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ 𝐴) → (((1𝑜 = 1𝑜 ∧ (𝑦‘∩ {𝑘 ∈ On ∣ (𝑦‘𝑘) ≠ 1𝑜}) = ∅) ∨ (1𝑜 = 1𝑜 ∧ (𝑦‘∩ {𝑘 ∈ On ∣ (𝑦‘𝑘) ≠ 1𝑜}) = 2𝑜)) ∨ (1𝑜 = ∅ ∧ (𝑦‘∩ {𝑘 ∈ On ∣ (𝑦‘𝑘) ≠ 1𝑜}) = 2𝑜)))
60		fvex 6113	. . . . . . . . . 10 ⊢ (𝑦‘∩ {𝑘 ∈ On ∣ (𝑦‘𝑘) ≠ 1𝑜}) ∈ V
61	3, 60	brtp 30892	. . . . . . . . 9 ⊢ (1𝑜{⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝑦‘∩ {𝑘 ∈ On ∣ (𝑦‘𝑘) ≠ 1𝑜}) ↔ ((1𝑜 = 1𝑜 ∧ (𝑦‘∩ {𝑘 ∈ On ∣ (𝑦‘𝑘) ≠ 1𝑜}) = ∅) ∨ (1𝑜 = 1𝑜 ∧ (𝑦‘∩ {𝑘 ∈ On ∣ (𝑦‘𝑘) ≠ 1𝑜}) = 2𝑜) ∨ (1𝑜 = ∅ ∧ (𝑦‘∩ {𝑘 ∈ On ∣ (𝑦‘𝑘) ≠ 1𝑜}) = 2𝑜)))
62		df-3or 1032	. . . . . . . . 9 ⊢ (((1𝑜 = 1𝑜 ∧ (𝑦‘∩ {𝑘 ∈ On ∣ (𝑦‘𝑘) ≠ 1𝑜}) = ∅) ∨ (1𝑜 = 1𝑜 ∧ (𝑦‘∩ {𝑘 ∈ On ∣ (𝑦‘𝑘) ≠ 1𝑜}) = 2𝑜) ∨ (1𝑜 = ∅ ∧ (𝑦‘∩ {𝑘 ∈ On ∣ (𝑦‘𝑘) ≠ 1𝑜}) = 2𝑜)) ↔ (((1𝑜 = 1𝑜 ∧ (𝑦‘∩ {𝑘 ∈ On ∣ (𝑦‘𝑘) ≠ 1𝑜}) = ∅) ∨ (1𝑜 = 1𝑜 ∧ (𝑦‘∩ {𝑘 ∈ On ∣ (𝑦‘𝑘) ≠ 1𝑜}) = 2𝑜)) ∨ (1𝑜 = ∅ ∧ (𝑦‘∩ {𝑘 ∈ On ∣ (𝑦‘𝑘) ≠ 1𝑜}) = 2𝑜)))
63	61, 62	bitri 263	. . . . . . . 8 ⊢ (1𝑜{⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝑦‘∩ {𝑘 ∈ On ∣ (𝑦‘𝑘) ≠ 1𝑜}) ↔ (((1𝑜 = 1𝑜 ∧ (𝑦‘∩ {𝑘 ∈ On ∣ (𝑦‘𝑘) ≠ 1𝑜}) = ∅) ∨ (1𝑜 = 1𝑜 ∧ (𝑦‘∩ {𝑘 ∈ On ∣ (𝑦‘𝑘) ≠ 1𝑜}) = 2𝑜)) ∨ (1𝑜 = ∅ ∧ (𝑦‘∩ {𝑘 ∈ On ∣ (𝑦‘𝑘) ≠ 1𝑜}) = 2𝑜)))
64	59, 63	sylibr 223	. . . . . . 7 ⊢ (((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ 𝐴) → 1𝑜{⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝑦‘∩ {𝑘 ∈ On ∣ (𝑦‘𝑘) ≠ 1𝑜}))
65	47, 64	eqbrtrd 4605	. . . . . 6 ⊢ (((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ 𝐴) → ((∩ {𝑎 ∈ On ∣ ∀𝑛 ∈ 𝐴 ∃𝑏 ∈ 𝑎 (𝑛‘𝑏) ≠ 1𝑜} × {1𝑜})‘∩ {𝑘 ∈ On ∣ (𝑦‘𝑘) ≠ 1𝑜}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝑦‘∩ {𝑘 ∈ On ∣ (𝑦‘𝑘) ≠ 1𝑜}))
66		raleq 3115	. . . . . . . 8 ⊢ (𝑐 = ∩ {𝑘 ∈ On ∣ (𝑦‘𝑘) ≠ 1𝑜} → (∀𝑑 ∈ 𝑐 ((∩ {𝑎 ∈ On ∣ ∀𝑛 ∈ 𝐴 ∃𝑏 ∈ 𝑎 (𝑛‘𝑏) ≠ 1𝑜} × {1𝑜})‘𝑑) = (𝑦‘𝑑) ↔ ∀𝑑 ∈ ∩ {𝑘 ∈ On ∣ (𝑦‘𝑘) ≠ 1𝑜} ((∩ {𝑎 ∈ On ∣ ∀𝑛 ∈ 𝐴 ∃𝑏 ∈ 𝑎 (𝑛‘𝑏) ≠ 1𝑜} × {1𝑜})‘𝑑) = (𝑦‘𝑑)))
67		fveq2 6103	. . . . . . . . 9 ⊢ (𝑐 = ∩ {𝑘 ∈ On ∣ (𝑦‘𝑘) ≠ 1𝑜} → ((∩ {𝑎 ∈ On ∣ ∀𝑛 ∈ 𝐴 ∃𝑏 ∈ 𝑎 (𝑛‘𝑏) ≠ 1𝑜} × {1𝑜})‘𝑐) = ((∩ {𝑎 ∈ On ∣ ∀𝑛 ∈ 𝐴 ∃𝑏 ∈ 𝑎 (𝑛‘𝑏) ≠ 1𝑜} × {1𝑜})‘∩ {𝑘 ∈ On ∣ (𝑦‘𝑘) ≠ 1𝑜}))
68		fveq2 6103	. . . . . . . . 9 ⊢ (𝑐 = ∩ {𝑘 ∈ On ∣ (𝑦‘𝑘) ≠ 1𝑜} → (𝑦‘𝑐) = (𝑦‘∩ {𝑘 ∈ On ∣ (𝑦‘𝑘) ≠ 1𝑜}))
69	67, 68	breq12d 4596	. . . . . . . 8 ⊢ (𝑐 = ∩ {𝑘 ∈ On ∣ (𝑦‘𝑘) ≠ 1𝑜} → (((∩ {𝑎 ∈ On ∣ ∀𝑛 ∈ 𝐴 ∃𝑏 ∈ 𝑎 (𝑛‘𝑏) ≠ 1𝑜} × {1𝑜})‘𝑐){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝑦‘𝑐) ↔ ((∩ {𝑎 ∈ On ∣ ∀𝑛 ∈ 𝐴 ∃𝑏 ∈ 𝑎 (𝑛‘𝑏) ≠ 1𝑜} × {1𝑜})‘∩ {𝑘 ∈ On ∣ (𝑦‘𝑘) ≠ 1𝑜}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝑦‘∩ {𝑘 ∈ On ∣ (𝑦‘𝑘) ≠ 1𝑜})))
70	66, 69	anbi12d 743	. . . . . . 7 ⊢ (𝑐 = ∩ {𝑘 ∈ On ∣ (𝑦‘𝑘) ≠ 1𝑜} → ((∀𝑑 ∈ 𝑐 ((∩ {𝑎 ∈ On ∣ ∀𝑛 ∈ 𝐴 ∃𝑏 ∈ 𝑎 (𝑛‘𝑏) ≠ 1𝑜} × {1𝑜})‘𝑑) = (𝑦‘𝑑) ∧ ((∩ {𝑎 ∈ On ∣ ∀𝑛 ∈ 𝐴 ∃𝑏 ∈ 𝑎 (𝑛‘𝑏) ≠ 1𝑜} × {1𝑜})‘𝑐){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝑦‘𝑐)) ↔ (∀𝑑 ∈ ∩ {𝑘 ∈ On ∣ (𝑦‘𝑘) ≠ 1𝑜} ((∩ {𝑎 ∈ On ∣ ∀𝑛 ∈ 𝐴 ∃𝑏 ∈ 𝑎 (𝑛‘𝑏) ≠ 1𝑜} × {1𝑜})‘𝑑) = (𝑦‘𝑑) ∧ ((∩ {𝑎 ∈ On ∣ ∀𝑛 ∈ 𝐴 ∃𝑏 ∈ 𝑎 (𝑛‘𝑏) ≠ 1𝑜} × {1𝑜})‘∩ {𝑘 ∈ On ∣ (𝑦‘𝑘) ≠ 1𝑜}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝑦‘∩ {𝑘 ∈ On ∣ (𝑦‘𝑘) ≠ 1𝑜}))))
71	70	rspcev 3282	. . . . . 6 ⊢ ((∩ {𝑘 ∈ On ∣ (𝑦‘𝑘) ≠ 1𝑜} ∈ On ∧ (∀𝑑 ∈ ∩ {𝑘 ∈ On ∣ (𝑦‘𝑘) ≠ 1𝑜} ((∩ {𝑎 ∈ On ∣ ∀𝑛 ∈ 𝐴 ∃𝑏 ∈ 𝑎 (𝑛‘𝑏) ≠ 1𝑜} × {1𝑜})‘𝑑) = (𝑦‘𝑑) ∧ ((∩ {𝑎 ∈ On ∣ ∀𝑛 ∈ 𝐴 ∃𝑏 ∈ 𝑎 (𝑛‘𝑏) ≠ 1𝑜} × {1𝑜})‘∩ {𝑘 ∈ On ∣ (𝑦‘𝑘) ≠ 1𝑜}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝑦‘∩ {𝑘 ∈ On ∣ (𝑦‘𝑘) ≠ 1𝑜}))) → ∃𝑐 ∈ On (∀𝑑 ∈ 𝑐 ((∩ {𝑎 ∈ On ∣ ∀𝑛 ∈ 𝐴 ∃𝑏 ∈ 𝑎 (𝑛‘𝑏) ≠ 1𝑜} × {1𝑜})‘𝑑) = (𝑦‘𝑑) ∧ ((∩ {𝑎 ∈ On ∣ ∀𝑛 ∈ 𝐴 ∃𝑏 ∈ 𝑎 (𝑛‘𝑏) ≠ 1𝑜} × {1𝑜})‘𝑐){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝑦‘𝑐)))
72	14, 45, 65, 71	syl12anc 1316	. . . . 5 ⊢ (((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ 𝐴) → ∃𝑐 ∈ On (∀𝑑 ∈ 𝑐 ((∩ {𝑎 ∈ On ∣ ∀𝑛 ∈ 𝐴 ∃𝑏 ∈ 𝑎 (𝑛‘𝑏) ≠ 1𝑜} × {1𝑜})‘𝑑) = (𝑦‘𝑑) ∧ ((∩ {𝑎 ∈ On ∣ ∀𝑛 ∈ 𝐴 ∃𝑏 ∈ 𝑎 (𝑛‘𝑏) ≠ 1𝑜} × {1𝑜})‘𝑐){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝑦‘𝑐)))
73		sltval 31044	. . . . . 6 ⊢ (((∩ {𝑎 ∈ On ∣ ∀𝑛 ∈ 𝐴 ∃𝑏 ∈ 𝑎 (𝑛‘𝑏) ≠ 1𝑜} × {1𝑜}) ∈ No ∧ 𝑦 ∈ No ) → ((∩ {𝑎 ∈ On ∣ ∀𝑛 ∈ 𝐴 ∃𝑏 ∈ 𝑎 (𝑛‘𝑏) ≠ 1𝑜} × {1𝑜}) <s 𝑦 ↔ ∃𝑐 ∈ On (∀𝑑 ∈ 𝑐 ((∩ {𝑎 ∈ On ∣ ∀𝑛 ∈ 𝐴 ∃𝑏 ∈ 𝑎 (𝑛‘𝑏) ≠ 1𝑜} × {1𝑜})‘𝑑) = (𝑦‘𝑑) ∧ ((∩ {𝑎 ∈ On ∣ ∀𝑛 ∈ 𝐴 ∃𝑏 ∈ 𝑎 (𝑛‘𝑏) ≠ 1𝑜} × {1𝑜})‘𝑐){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝑦‘𝑐))))
74	73	biimpar 501	. . . . 5 ⊢ ((((∩ {𝑎 ∈ On ∣ ∀𝑛 ∈ 𝐴 ∃𝑏 ∈ 𝑎 (𝑛‘𝑏) ≠ 1𝑜} × {1𝑜}) ∈ No ∧ 𝑦 ∈ No ) ∧ ∃𝑐 ∈ On (∀𝑑 ∈ 𝑐 ((∩ {𝑎 ∈ On ∣ ∀𝑛 ∈ 𝐴 ∃𝑏 ∈ 𝑎 (𝑛‘𝑏) ≠ 1𝑜} × {1𝑜})‘𝑑) = (𝑦‘𝑑) ∧ ((∩ {𝑎 ∈ On ∣ ∀𝑛 ∈ 𝐴 ∃𝑏 ∈ 𝑎 (𝑛‘𝑏) ≠ 1𝑜} × {1𝑜})‘𝑐){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝑦‘𝑐))) → (∩ {𝑎 ∈ On ∣ ∀𝑛 ∈ 𝐴 ∃𝑏 ∈ 𝑎 (𝑛‘𝑏) ≠ 1𝑜} × {1𝑜}) <s 𝑦)
75	9, 11, 72, 74	syl21anc 1317	. . . 4 ⊢ (((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ 𝐴) → (∩ {𝑎 ∈ On ∣ ∀𝑛 ∈ 𝐴 ∃𝑏 ∈ 𝑎 (𝑛‘𝑏) ≠ 1𝑜} × {1𝑜}) <s 𝑦)
76	75	ralrimiva 2949	. . 3 ⊢ ((𝐴 ⊆ No ∧ 𝐴 ∈ V) → ∀𝑦 ∈ 𝐴 (∩ {𝑎 ∈ On ∣ ∀𝑛 ∈ 𝐴 ∃𝑏 ∈ 𝑎 (𝑛‘𝑏) ≠ 1𝑜} × {1𝑜}) <s 𝑦)
77	4, 5	nobndlem8 31098	. . 3 ⊢ ((𝐴 ⊆ No ∧ 𝐴 ∈ V) → ( bday ‘(∩ {𝑎 ∈ On ∣ ∀𝑛 ∈ 𝐴 ∃𝑏 ∈ 𝑎 (𝑛‘𝑏) ≠ 1𝑜} × {1𝑜})) ⊆ suc ∪ ( bday “ 𝐴))
78		breq1 4586	. . . . . 6 ⊢ (𝑥 = (∩ {𝑎 ∈ On ∣ ∀𝑛 ∈ 𝐴 ∃𝑏 ∈ 𝑎 (𝑛‘𝑏) ≠ 1𝑜} × {1𝑜}) → (𝑥 <s 𝑦 ↔ (∩ {𝑎 ∈ On ∣ ∀𝑛 ∈ 𝐴 ∃𝑏 ∈ 𝑎 (𝑛‘𝑏) ≠ 1𝑜} × {1𝑜}) <s 𝑦))
79	78	ralbidv 2969	. . . . 5 ⊢ (𝑥 = (∩ {𝑎 ∈ On ∣ ∀𝑛 ∈ 𝐴 ∃𝑏 ∈ 𝑎 (𝑛‘𝑏) ≠ 1𝑜} × {1𝑜}) → (∀𝑦 ∈ 𝐴 𝑥 <s 𝑦 ↔ ∀𝑦 ∈ 𝐴 (∩ {𝑎 ∈ On ∣ ∀𝑛 ∈ 𝐴 ∃𝑏 ∈ 𝑎 (𝑛‘𝑏) ≠ 1𝑜} × {1𝑜}) <s 𝑦))
80		fveq2 6103	. . . . . 6 ⊢ (𝑥 = (∩ {𝑎 ∈ On ∣ ∀𝑛 ∈ 𝐴 ∃𝑏 ∈ 𝑎 (𝑛‘𝑏) ≠ 1𝑜} × {1𝑜}) → ( bday ‘𝑥) = ( bday ‘(∩ {𝑎 ∈ On ∣ ∀𝑛 ∈ 𝐴 ∃𝑏 ∈ 𝑎 (𝑛‘𝑏) ≠ 1𝑜} × {1𝑜})))
81	80	sseq1d 3595	. . . . 5 ⊢ (𝑥 = (∩ {𝑎 ∈ On ∣ ∀𝑛 ∈ 𝐴 ∃𝑏 ∈ 𝑎 (𝑛‘𝑏) ≠ 1𝑜} × {1𝑜}) → (( bday ‘𝑥) ⊆ suc ∪ ( bday “ 𝐴) ↔ ( bday ‘(∩ {𝑎 ∈ On ∣ ∀𝑛 ∈ 𝐴 ∃𝑏 ∈ 𝑎 (𝑛‘𝑏) ≠ 1𝑜} × {1𝑜})) ⊆ suc ∪ ( bday “ 𝐴)))
82	79, 81	anbi12d 743	. . . 4 ⊢ (𝑥 = (∩ {𝑎 ∈ On ∣ ∀𝑛 ∈ 𝐴 ∃𝑏 ∈ 𝑎 (𝑛‘𝑏) ≠ 1𝑜} × {1𝑜}) → ((∀𝑦 ∈ 𝐴 𝑥 <s 𝑦 ∧ ( bday ‘𝑥) ⊆ suc ∪ ( bday “ 𝐴)) ↔ (∀𝑦 ∈ 𝐴 (∩ {𝑎 ∈ On ∣ ∀𝑛 ∈ 𝐴 ∃𝑏 ∈ 𝑎 (𝑛‘𝑏) ≠ 1𝑜} × {1𝑜}) <s 𝑦 ∧ ( bday ‘(∩ {𝑎 ∈ On ∣ ∀𝑛 ∈ 𝐴 ∃𝑏 ∈ 𝑎 (𝑛‘𝑏) ≠ 1𝑜} × {1𝑜})) ⊆ suc ∪ ( bday “ 𝐴))))
83	82	rspcev 3282	. . 3 ⊢ (((∩ {𝑎 ∈ On ∣ ∀𝑛 ∈ 𝐴 ∃𝑏 ∈ 𝑎 (𝑛‘𝑏) ≠ 1𝑜} × {1𝑜}) ∈ No ∧ (∀𝑦 ∈ 𝐴 (∩ {𝑎 ∈ On ∣ ∀𝑛 ∈ 𝐴 ∃𝑏 ∈ 𝑎 (𝑛‘𝑏) ≠ 1𝑜} × {1𝑜}) <s 𝑦 ∧ ( bday ‘(∩ {𝑎 ∈ On ∣ ∀𝑛 ∈ 𝐴 ∃𝑏 ∈ 𝑎 (𝑛‘𝑏) ≠ 1𝑜} × {1𝑜})) ⊆ suc ∪ ( bday “ 𝐴))) → ∃𝑥 ∈ No (∀𝑦 ∈ 𝐴 𝑥 <s 𝑦 ∧ ( bday ‘𝑥) ⊆ suc ∪ ( bday “ 𝐴)))
84	8, 76, 77, 83	syl12anc 1316	. 2 ⊢ ((𝐴 ⊆ No ∧ 𝐴 ∈ V) → ∃𝑥 ∈ No (∀𝑦 ∈ 𝐴 𝑥 <s 𝑦 ∧ ( bday ‘𝑥) ⊆ suc ∪ ( bday “ 𝐴)))
85	1, 84	sylan2 490	1 ⊢ ((𝐴 ⊆ No ∧ 𝐴 ∈ 𝑉) → ∃𝑥 ∈ No (∀𝑦 ∈ 𝐴 𝑥 <s 𝑦 ∧ ( bday ‘𝑥) ⊆ suc ∪ ( bday “ 𝐴)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∨ wo 382   ∧ wa 383   ∨ w3o 1030   = wceq 1475   ∈ wcel 1977   ≠ wne 2780  ∀wral 2896  ∃wrex 2897  {crab 2900  Vcvv 3173   ⊆ wss 3540  ∅c0 3874  {csn 4125  {ctp 4129  ⟨cop 4131  ∪ cuni 4372  ∩ cint 4410   class class class wbr 4583   × cxp 5036   “ cima 5041  Oncon0 5640  suc csuc 5642  ‘cfv 5804  1_𝑜c1o 7440  2_𝑜c2o 7441   No csur 31037   <s cslt 31038   bday cbday 31039

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-reu 2903  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-ord 5643  df-on 5644  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-1o 7447  df-2o 7448  df-no 31040  df-slt 31041  df-bday 31042

This theorem is referenced by:  nofulllem2  31102