Theorem cfflb 10231

Description: If there is a cofinal map from 𝐵 to 𝐴, then 𝐵 is at least (cf‘𝐴). This theorem and cff1 10230 motivate the picture of (cf‘𝐴) as the greatest lower bound of the domain of cofinal maps into 𝐴. (Contributed by Mario Carneiro, 28-Feb-2013.)

Assertion

Ref	Expression
cfflb	⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (∃𝑓(𝑓:𝐵⟶𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤)) → (cf‘𝐴) ⊆ 𝐵))

Distinct variable groups:   𝐴,𝑓,𝑤,𝑧   𝐵,𝑓,𝑤,𝑧

Proof of Theorem cfflb

Dummy variables 𝑠 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		frn 6703	. . . . . . 7 ⊢ (𝑓:𝐵⟶𝐴 → ran 𝑓 ⊆ 𝐴)
2	1	adantr 485	. . . . . 6 ⊢ ((𝑓:𝐵⟶𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤)) → ran 𝑓 ⊆ 𝐴)
3		ffn 6695	. . . . . . . . . . 11 ⊢ (𝑓:𝐵⟶𝐴 → 𝑓 Fn 𝐵)
4		fnfvelrn 7065	. . . . . . . . . . 11 ⊢ ((𝑓 Fn 𝐵 ∧ 𝑤 ∈ 𝐵) → (𝑓‘𝑤) ∈ ran 𝑓)
5	3, 4	sylan 591	. . . . . . . . . 10 ⊢ ((𝑓:𝐵⟶𝐴 ∧ 𝑤 ∈ 𝐵) → (𝑓‘𝑤) ∈ ran 𝑓)
6		sseq2 3965	. . . . . . . . . . 11 ⊢ (𝑠 = (𝑓‘𝑤) → (𝑧 ⊆ 𝑠 ↔ 𝑧 ⊆ (𝑓‘𝑤)))
7	6	rspcev 3584	. . . . . . . . . 10 ⊢ (((𝑓‘𝑤) ∈ ran 𝑓 ∧ 𝑧 ⊆ (𝑓‘𝑤)) → ∃𝑠 ∈ ran 𝑓 𝑧 ⊆ 𝑠)
8	5, 7	sylan 591	. . . . . . . . 9 ⊢ (((𝑓:𝐵⟶𝐴 ∧ 𝑤 ∈ 𝐵) ∧ 𝑧 ⊆ (𝑓‘𝑤)) → ∃𝑠 ∈ ran 𝑓 𝑧 ⊆ 𝑠)
9	8	rexlimdva2 3168	. . . . . . . 8 ⊢ (𝑓:𝐵⟶𝐴 → (∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤) → ∃𝑠 ∈ ran 𝑓 𝑧 ⊆ 𝑠))
10	9	ralimdv 3179	. . . . . . 7 ⊢ (𝑓:𝐵⟶𝐴 → (∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤) → ∀𝑧 ∈ 𝐴 ∃𝑠 ∈ ran 𝑓 𝑧 ⊆ 𝑠))
11	10	imp 411	. . . . . 6 ⊢ ((𝑓:𝐵⟶𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤)) → ∀𝑧 ∈ 𝐴 ∃𝑠 ∈ ran 𝑓 𝑧 ⊆ 𝑠)
12	2, 11	jca 520	. . . . 5 ⊢ ((𝑓:𝐵⟶𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤)) → (ran 𝑓 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑠 ∈ ran 𝑓 𝑧 ⊆ 𝑠))
13		fvex 6884	. . . . . 6 ⊢ (card‘ran 𝑓) ∈ V
14		cfval 10218	. . . . . . . . . . 11 ⊢ (𝐴 ∈ On → (cf‘𝐴) = ∩ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑠 ∈ 𝑦 𝑧 ⊆ 𝑠))})
15	14	adantr 485	. . . . . . . . . 10 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (cf‘𝐴) = ∩ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑠 ∈ 𝑦 𝑧 ⊆ 𝑠))})
16	15	3ad2ant2 1150	. . . . . . . . 9 ⊢ ((𝑥 = (card‘ran 𝑓) ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (ran 𝑓 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑠 ∈ ran 𝑓 𝑧 ⊆ 𝑠)) → (cf‘𝐴) = ∩ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑠 ∈ 𝑦 𝑧 ⊆ 𝑠))})
17		vex 3461	. . . . . . . . . . . . . 14 ⊢ 𝑓 ∈ V
18	17	rnex 7895	. . . . . . . . . . . . 13 ⊢ ran 𝑓 ∈ V
19		fveq2 6871	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = ran 𝑓 → (card‘𝑦) = (card‘ran 𝑓))
20	19	eqeq2d 2776	. . . . . . . . . . . . . 14 ⊢ (𝑦 = ran 𝑓 → (𝑥 = (card‘𝑦) ↔ 𝑥 = (card‘ran 𝑓)))
21		sseq1 3964	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = ran 𝑓 → (𝑦 ⊆ 𝐴 ↔ ran 𝑓 ⊆ 𝐴))
22		rexeq 3319	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = ran 𝑓 → (∃𝑠 ∈ 𝑦 𝑧 ⊆ 𝑠 ↔ ∃𝑠 ∈ ran 𝑓 𝑧 ⊆ 𝑠))
23	22	ralbidv 3188	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = ran 𝑓 → (∀𝑧 ∈ 𝐴 ∃𝑠 ∈ 𝑦 𝑧 ⊆ 𝑠 ↔ ∀𝑧 ∈ 𝐴 ∃𝑠 ∈ ran 𝑓 𝑧 ⊆ 𝑠))
24	21, 23	anbi12d 643	. . . . . . . . . . . . . 14 ⊢ (𝑦 = ran 𝑓 → ((𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑠 ∈ 𝑦 𝑧 ⊆ 𝑠) ↔ (ran 𝑓 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑠 ∈ ran 𝑓 𝑧 ⊆ 𝑠)))
25	20, 24	anbi12d 643	. . . . . . . . . . . . 13 ⊢ (𝑦 = ran 𝑓 → ((𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑠 ∈ 𝑦 𝑧 ⊆ 𝑠)) ↔ (𝑥 = (card‘ran 𝑓) ∧ (ran 𝑓 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑠 ∈ ran 𝑓 𝑧 ⊆ 𝑠))))
26	18, 25	spcev 3568	. . . . . . . . . . . 12 ⊢ ((𝑥 = (card‘ran 𝑓) ∧ (ran 𝑓 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑠 ∈ ran 𝑓 𝑧 ⊆ 𝑠)) → ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑠 ∈ 𝑦 𝑧 ⊆ 𝑠)))
27		abid 2747	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑠 ∈ 𝑦 𝑧 ⊆ 𝑠))} ↔ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑠 ∈ 𝑦 𝑧 ⊆ 𝑠)))
28	26, 27	sylibr 237	. . . . . . . . . . 11 ⊢ ((𝑥 = (card‘ran 𝑓) ∧ (ran 𝑓 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑠 ∈ ran 𝑓 𝑧 ⊆ 𝑠)) → 𝑥 ∈ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑠 ∈ 𝑦 𝑧 ⊆ 𝑠))})
29		intss1 4924	. . . . . . . . . . 11 ⊢ (𝑥 ∈ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑠 ∈ 𝑦 𝑧 ⊆ 𝑠))} → ∩ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑠 ∈ 𝑦 𝑧 ⊆ 𝑠))} ⊆ 𝑥)
30	28, 29	syl 18	. . . . . . . . . 10 ⊢ ((𝑥 = (card‘ran 𝑓) ∧ (ran 𝑓 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑠 ∈ ran 𝑓 𝑧 ⊆ 𝑠)) → ∩ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑠 ∈ 𝑦 𝑧 ⊆ 𝑠))} ⊆ 𝑥)
31	30	3adant2 1147	. . . . . . . . 9 ⊢ ((𝑥 = (card‘ran 𝑓) ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (ran 𝑓 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑠 ∈ ran 𝑓 𝑧 ⊆ 𝑠)) → ∩ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑠 ∈ 𝑦 𝑧 ⊆ 𝑠))} ⊆ 𝑥)
32	16, 31	eqsstrd 3973	. . . . . . . 8 ⊢ ((𝑥 = (card‘ran 𝑓) ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (ran 𝑓 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑠 ∈ ran 𝑓 𝑧 ⊆ 𝑠)) → (cf‘𝐴) ⊆ 𝑥)
33	32	3expib 1138	. . . . . . 7 ⊢ (𝑥 = (card‘ran 𝑓) → (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (ran 𝑓 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑠 ∈ ran 𝑓 𝑧 ⊆ 𝑠)) → (cf‘𝐴) ⊆ 𝑥))
34		sseq2 3965	. . . . . . 7 ⊢ (𝑥 = (card‘ran 𝑓) → ((cf‘𝐴) ⊆ 𝑥 ↔ (cf‘𝐴) ⊆ (card‘ran 𝑓)))
35	33, 34	sylibd 242	. . . . . 6 ⊢ (𝑥 = (card‘ran 𝑓) → (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (ran 𝑓 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑠 ∈ ran 𝑓 𝑧 ⊆ 𝑠)) → (cf‘𝐴) ⊆ (card‘ran 𝑓)))
36	13, 35	vtocle 3526	. . . . 5 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (ran 𝑓 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑠 ∈ ran 𝑓 𝑧 ⊆ 𝑠)) → (cf‘𝐴) ⊆ (card‘ran 𝑓))
37	12, 36	sylan2 604	. . . 4 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑓:𝐵⟶𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤))) → (cf‘𝐴) ⊆ (card‘ran 𝑓))
38		cardidm 9933	. . . . . . 7 ⊢ (card‘(card‘ran 𝑓)) = (card‘ran 𝑓)
39		onss 7772	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ On → 𝐴 ⊆ On)
40	1, 39	sylan9ssr 3953	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ On ∧ 𝑓:𝐵⟶𝐴) → ran 𝑓 ⊆ On)
41	40	3adant2 1147	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑓:𝐵⟶𝐴) → ran 𝑓 ⊆ On)
42		onssnum 10012	. . . . . . . . . . . 12 ⊢ ((ran 𝑓 ∈ V ∧ ran 𝑓 ⊆ On) → ran 𝑓 ∈ dom card)
43	18, 41, 42	sylancr 598	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑓:𝐵⟶𝐴) → ran 𝑓 ∈ dom card)
44		cardid2 9927	. . . . . . . . . . 11 ⊢ (ran 𝑓 ∈ dom card → (card‘ran 𝑓) ≈ ran 𝑓)
45	43, 44	syl 18	. . . . . . . . . 10 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑓:𝐵⟶𝐴) → (card‘ran 𝑓) ≈ ran 𝑓)
46		onenon 9923	. . . . . . . . . . . . 13 ⊢ (𝐵 ∈ On → 𝐵 ∈ dom card)
47		dffn4 6788	. . . . . . . . . . . . . 14 ⊢ (𝑓 Fn 𝐵 ↔ 𝑓:𝐵–onto→ran 𝑓)
48	3, 47	sylib 221	. . . . . . . . . . . . 13 ⊢ (𝑓:𝐵⟶𝐴 → 𝑓:𝐵–onto→ran 𝑓)
49		fodomnum 10029	. . . . . . . . . . . . 13 ⊢ (𝐵 ∈ dom card → (𝑓:𝐵–onto→ran 𝑓 → ran 𝑓 ≼ 𝐵))
50	46, 48, 49	syl2im 41	. . . . . . . . . . . 12 ⊢ (𝐵 ∈ On → (𝑓:𝐵⟶𝐴 → ran 𝑓 ≼ 𝐵))
51	50	imp 411	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ On ∧ 𝑓:𝐵⟶𝐴) → ran 𝑓 ≼ 𝐵)
52	51	3adant1 1146	. . . . . . . . . 10 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑓:𝐵⟶𝐴) → ran 𝑓 ≼ 𝐵)
53		endomtr 8997	. . . . . . . . . 10 ⊢ (((card‘ran 𝑓) ≈ ran 𝑓 ∧ ran 𝑓 ≼ 𝐵) → (card‘ran 𝑓) ≼ 𝐵)
54	45, 52, 53	syl2anc 595	. . . . . . . . 9 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑓:𝐵⟶𝐴) → (card‘ran 𝑓) ≼ 𝐵)
55		cardon 9918	. . . . . . . . . . . 12 ⊢ (card‘ran 𝑓) ∈ On
56		onenon 9923	. . . . . . . . . . . 12 ⊢ ((card‘ran 𝑓) ∈ On → (card‘ran 𝑓) ∈ dom card)
57	55, 56	ax-mp 5	. . . . . . . . . . 11 ⊢ (card‘ran 𝑓) ∈ dom card
58		carddom2 9951	. . . . . . . . . . 11 ⊢ (((card‘ran 𝑓) ∈ dom card ∧ 𝐵 ∈ dom card) → ((card‘(card‘ran 𝑓)) ⊆ (card‘𝐵) ↔ (card‘ran 𝑓) ≼ 𝐵))
59	57, 46, 58	sylancr 598	. . . . . . . . . 10 ⊢ (𝐵 ∈ On → ((card‘(card‘ran 𝑓)) ⊆ (card‘𝐵) ↔ (card‘ran 𝑓) ≼ 𝐵))
60	59	3ad2ant2 1150	. . . . . . . . 9 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑓:𝐵⟶𝐴) → ((card‘(card‘ran 𝑓)) ⊆ (card‘𝐵) ↔ (card‘ran 𝑓) ≼ 𝐵))
61	54, 60	mpbird 260	. . . . . . . 8 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑓:𝐵⟶𝐴) → (card‘(card‘ran 𝑓)) ⊆ (card‘𝐵))
62		cardonle 9931	. . . . . . . . 9 ⊢ (𝐵 ∈ On → (card‘𝐵) ⊆ 𝐵)
63	62	3ad2ant2 1150	. . . . . . . 8 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑓:𝐵⟶𝐴) → (card‘𝐵) ⊆ 𝐵)
64	61, 63	sstrd 3949	. . . . . . 7 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑓:𝐵⟶𝐴) → (card‘(card‘ran 𝑓)) ⊆ 𝐵)
65	38, 64	eqsstrrid 3978	. . . . . 6 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑓:𝐵⟶𝐴) → (card‘ran 𝑓) ⊆ 𝐵)
66	65	3expa 1134	. . . . 5 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) → (card‘ran 𝑓) ⊆ 𝐵)
67	66	adantrr 729	. . . 4 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑓:𝐵⟶𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤))) → (card‘ran 𝑓) ⊆ 𝐵)
68	37, 67	sstrd 3949	. . 3 ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑓:𝐵⟶𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤))) → (cf‘𝐴) ⊆ 𝐵)
69	68	ex 417	. 2 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝑓:𝐵⟶𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤)) → (cf‘𝐴) ⊆ 𝐵))
70	69	exlimdv 1956	1 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (∃𝑓(𝑓:𝐵⟶𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤)) → (cf‘𝐴) ⊆ 𝐵))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   ∧ w3a 1101   = wceq 1563  ∃wex 1802   ∈ wcel 2145  {cab 2743  ∀wral 3079  ∃wrex 3089  Vcvv 3457   ⊆ wss 3907  ∩ cint 4908   class class class wbr 5105  dom cdm 5652  ran crn 5653  Oncon0 6350   Fn wfn 6520  ⟶wf 6521  –onto→wfo 6523  ‘cfv 6525   ≈ cen 8928   ≼ cdom 8929  cardccrd 9909  cfccf 9911

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737  ax-rep 5232  ax-sep 5251  ax-nul 5261  ax-pow 5327  ax-pr 5395  ax-un 7722

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3080  df-rex 3090  df-rmo 3370  df-reu 3371  df-rab 3418  df-v 3459  df-sbc 3748  df-csb 3856  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-pss 3927  df-nul 4289  df-if 4484  df-pw 4560  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4869  df-int 4909  df-iun 4954  df-br 5106  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5547  df-eprel 5552  df-po 5560  df-so 5561  df-fr 5605  df-se 5606  df-we 5607  df-xp 5658  df-rel 5659  df-cnv 5660  df-co 5661  df-dm 5662  df-rn 5663  df-res 5664  df-ima 5665  df-pred 6292  df-ord 6353  df-on 6354  df-suc 6356  df-iota 6481  df-fun 6527  df-fn 6528  df-f 6529  df-f1 6530  df-fo 6531  df-f1o 6532  df-fv 6533  df-isom 6534  df-riota 7357  df-ov 7403  df-oprab 7404  df-mpo 7405  df-1st 7974  df-2nd 7975  df-frecs 8266  df-wrecs 8297  df-recs 8346  df-er 8682  df-map 8814  df-en 8932  df-dom 8933  df-sdom 8934  df-card 9913  df-cf 9915  df-acn 9916

This theorem is referenced by:  cfsmolem  10242  cfcoflem  10244  cfcof  10246  inar1  10748