Theorem nobndup 31099

Description: Any set of surreals is bounded above 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
nobndup	⊢ ((𝐴 ⊆ No ∧ 𝐴 ∈ 𝑉) → ∃𝑥 ∈ No (∀𝑦 ∈ 𝐴 𝑦 <s 𝑥 ∧ ( bday ‘𝑥) ⊆ suc ∪ ( bday “ 𝐴)))

Distinct variable group:   𝑥,𝐴,𝑦

Allowed substitution hints:   𝑉(𝑥,𝑦)

Proof of Theorem nobndup

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

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