Theorem ackbij1lem18 9262

Description: Lemma for ackbij1 9263. (Contributed by Stefan O'Rear, 18-Nov-2014.)

Hypothesis

Ref	Expression
ackbij.f	⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦)))

Assertion

Ref	Expression
ackbij1lem18	⊢ (𝐴 ∈ (𝒫 ω ∩ Fin) → ∃𝑏 ∈ (𝒫 ω ∩ Fin)(𝐹‘𝑏) = suc (𝐹‘𝐴))

Distinct variable groups:   𝐹,𝑏,𝑥,𝑦   𝐴,𝑏,𝑥,𝑦

Proof of Theorem ackbij1lem18

Dummy variable 𝑎 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		difss 3889	. . . 4 ⊢ (𝐴 ∖ ∩ (ω ∖ 𝐴)) ⊆ 𝐴
2		ackbij.f	. . . . 5 ⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦)))
3	2	ackbij1lem11 9255	. . . 4 ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ (𝐴 ∖ ∩ (ω ∖ 𝐴)) ⊆ 𝐴) → (𝐴 ∖ ∩ (ω ∖ 𝐴)) ∈ (𝒫 ω ∩ Fin))
4	1, 3	mpan2 665	. . 3 ⊢ (𝐴 ∈ (𝒫 ω ∩ Fin) → (𝐴 ∖ ∩ (ω ∖ 𝐴)) ∈ (𝒫 ω ∩ Fin))
5		difss 3889	. . . . . . 7 ⊢ (ω ∖ 𝐴) ⊆ ω
6		omsson 7217	. . . . . . 7 ⊢ ω ⊆ On
7	5, 6	sstri 3762	. . . . . 6 ⊢ (ω ∖ 𝐴) ⊆ On
8		ominf 8329	. . . . . . . 8 ⊢ ¬ ω ∈ Fin
9		inss2 3983	. . . . . . . . 9 ⊢ (𝒫 ω ∩ Fin) ⊆ Fin
10	9	sseli 3749	. . . . . . . 8 ⊢ (𝐴 ∈ (𝒫 ω ∩ Fin) → 𝐴 ∈ Fin)
11		difinf 8387	. . . . . . . 8 ⊢ ((¬ ω ∈ Fin ∧ 𝐴 ∈ Fin) → ¬ (ω ∖ 𝐴) ∈ Fin)
12	8, 10, 11	sylancr 569	. . . . . . 7 ⊢ (𝐴 ∈ (𝒫 ω ∩ Fin) → ¬ (ω ∖ 𝐴) ∈ Fin)
13		0fin 8345	. . . . . . . . 9 ⊢ ∅ ∈ Fin
14		eleq1 2838	. . . . . . . . 9 ⊢ ((ω ∖ 𝐴) = ∅ → ((ω ∖ 𝐴) ∈ Fin ↔ ∅ ∈ Fin))
15	13, 14	mpbiri 248	. . . . . . . 8 ⊢ ((ω ∖ 𝐴) = ∅ → (ω ∖ 𝐴) ∈ Fin)
16	15	necon3bi 2969	. . . . . . 7 ⊢ (¬ (ω ∖ 𝐴) ∈ Fin → (ω ∖ 𝐴) ≠ ∅)
17	12, 16	syl 17	. . . . . 6 ⊢ (𝐴 ∈ (𝒫 ω ∩ Fin) → (ω ∖ 𝐴) ≠ ∅)
18		onint 7143	. . . . . 6 ⊢ (((ω ∖ 𝐴) ⊆ On ∧ (ω ∖ 𝐴) ≠ ∅) → ∩ (ω ∖ 𝐴) ∈ (ω ∖ 𝐴))
19	7, 17, 18	sylancr 569	. . . . 5 ⊢ (𝐴 ∈ (𝒫 ω ∩ Fin) → ∩ (ω ∖ 𝐴) ∈ (ω ∖ 𝐴))
20	19	eldifad 3736	. . . 4 ⊢ (𝐴 ∈ (𝒫 ω ∩ Fin) → ∩ (ω ∖ 𝐴) ∈ ω)
21		ackbij1lem4 9248	. . . 4 ⊢ (∩ (ω ∖ 𝐴) ∈ ω → {∩ (ω ∖ 𝐴)} ∈ (𝒫 ω ∩ Fin))
22	20, 21	syl 17	. . 3 ⊢ (𝐴 ∈ (𝒫 ω ∩ Fin) → {∩ (ω ∖ 𝐴)} ∈ (𝒫 ω ∩ Fin))
23		ackbij1lem6 9250	. . 3 ⊢ (((𝐴 ∖ ∩ (ω ∖ 𝐴)) ∈ (𝒫 ω ∩ Fin) ∧ {∩ (ω ∖ 𝐴)} ∈ (𝒫 ω ∩ Fin)) → ((𝐴 ∖ ∩ (ω ∖ 𝐴)) ∪ {∩ (ω ∖ 𝐴)}) ∈ (𝒫 ω ∩ Fin))
24	4, 22, 23	syl2anc 567	. 2 ⊢ (𝐴 ∈ (𝒫 ω ∩ Fin) → ((𝐴 ∖ ∩ (ω ∖ 𝐴)) ∪ {∩ (ω ∖ 𝐴)}) ∈ (𝒫 ω ∩ Fin))
25	19	eldifbd 3737	. . . . . 6 ⊢ (𝐴 ∈ (𝒫 ω ∩ Fin) → ¬ ∩ (ω ∖ 𝐴) ∈ 𝐴)
26		disjsn 4384	. . . . . 6 ⊢ ((𝐴 ∩ {∩ (ω ∖ 𝐴)}) = ∅ ↔ ¬ ∩ (ω ∖ 𝐴) ∈ 𝐴)
27	25, 26	sylibr 224	. . . . 5 ⊢ (𝐴 ∈ (𝒫 ω ∩ Fin) → (𝐴 ∩ {∩ (ω ∖ 𝐴)}) = ∅)
28		ssdisj 4171	. . . . 5 ⊢ (((𝐴 ∖ ∩ (ω ∖ 𝐴)) ⊆ 𝐴 ∧ (𝐴 ∩ {∩ (ω ∖ 𝐴)}) = ∅) → ((𝐴 ∖ ∩ (ω ∖ 𝐴)) ∩ {∩ (ω ∖ 𝐴)}) = ∅)
29	1, 27, 28	sylancr 569	. . . 4 ⊢ (𝐴 ∈ (𝒫 ω ∩ Fin) → ((𝐴 ∖ ∩ (ω ∖ 𝐴)) ∩ {∩ (ω ∖ 𝐴)}) = ∅)
30	2	ackbij1lem9 9253	. . . 4 ⊢ (((𝐴 ∖ ∩ (ω ∖ 𝐴)) ∈ (𝒫 ω ∩ Fin) ∧ {∩ (ω ∖ 𝐴)} ∈ (𝒫 ω ∩ Fin) ∧ ((𝐴 ∖ ∩ (ω ∖ 𝐴)) ∩ {∩ (ω ∖ 𝐴)}) = ∅) → (𝐹‘((𝐴 ∖ ∩ (ω ∖ 𝐴)) ∪ {∩ (ω ∖ 𝐴)})) = ((𝐹‘(𝐴 ∖ ∩ (ω ∖ 𝐴))) +𝑜 (𝐹‘{∩ (ω ∖ 𝐴)})))
31	4, 22, 29, 30	syl3anc 1476	. . 3 ⊢ (𝐴 ∈ (𝒫 ω ∩ Fin) → (𝐹‘((𝐴 ∖ ∩ (ω ∖ 𝐴)) ∪ {∩ (ω ∖ 𝐴)})) = ((𝐹‘(𝐴 ∖ ∩ (ω ∖ 𝐴))) +𝑜 (𝐹‘{∩ (ω ∖ 𝐴)})))
32	2	ackbij1lem14 9258	. . . . 5 ⊢ (∩ (ω ∖ 𝐴) ∈ ω → (𝐹‘{∩ (ω ∖ 𝐴)}) = suc (𝐹‘∩ (ω ∖ 𝐴)))
33	20, 32	syl 17	. . . 4 ⊢ (𝐴 ∈ (𝒫 ω ∩ Fin) → (𝐹‘{∩ (ω ∖ 𝐴)}) = suc (𝐹‘∩ (ω ∖ 𝐴)))
34	33	oveq2d 6810	. . 3 ⊢ (𝐴 ∈ (𝒫 ω ∩ Fin) → ((𝐹‘(𝐴 ∖ ∩ (ω ∖ 𝐴))) +𝑜 (𝐹‘{∩ (ω ∖ 𝐴)})) = ((𝐹‘(𝐴 ∖ ∩ (ω ∖ 𝐴))) +𝑜 suc (𝐹‘∩ (ω ∖ 𝐴))))
35	2	ackbij1lem10 9254	. . . . . . 7 ⊢ 𝐹:(𝒫 ω ∩ Fin)⟶ω
36	35	ffvelrni 6502	. . . . . 6 ⊢ ((𝐴 ∖ ∩ (ω ∖ 𝐴)) ∈ (𝒫 ω ∩ Fin) → (𝐹‘(𝐴 ∖ ∩ (ω ∖ 𝐴))) ∈ ω)
37	4, 36	syl 17	. . . . 5 ⊢ (𝐴 ∈ (𝒫 ω ∩ Fin) → (𝐹‘(𝐴 ∖ ∩ (ω ∖ 𝐴))) ∈ ω)
38		ackbij1lem3 9247	. . . . . . 7 ⊢ (∩ (ω ∖ 𝐴) ∈ ω → ∩ (ω ∖ 𝐴) ∈ (𝒫 ω ∩ Fin))
39	20, 38	syl 17	. . . . . 6 ⊢ (𝐴 ∈ (𝒫 ω ∩ Fin) → ∩ (ω ∖ 𝐴) ∈ (𝒫 ω ∩ Fin))
40	35	ffvelrni 6502	. . . . . 6 ⊢ (∩ (ω ∖ 𝐴) ∈ (𝒫 ω ∩ Fin) → (𝐹‘∩ (ω ∖ 𝐴)) ∈ ω)
41	39, 40	syl 17	. . . . 5 ⊢ (𝐴 ∈ (𝒫 ω ∩ Fin) → (𝐹‘∩ (ω ∖ 𝐴)) ∈ ω)
42		nnasuc 7841	. . . . 5 ⊢ (((𝐹‘(𝐴 ∖ ∩ (ω ∖ 𝐴))) ∈ ω ∧ (𝐹‘∩ (ω ∖ 𝐴)) ∈ ω) → ((𝐹‘(𝐴 ∖ ∩ (ω ∖ 𝐴))) +𝑜 suc (𝐹‘∩ (ω ∖ 𝐴))) = suc ((𝐹‘(𝐴 ∖ ∩ (ω ∖ 𝐴))) +𝑜 (𝐹‘∩ (ω ∖ 𝐴))))
43	37, 41, 42	syl2anc 567	. . . 4 ⊢ (𝐴 ∈ (𝒫 ω ∩ Fin) → ((𝐹‘(𝐴 ∖ ∩ (ω ∖ 𝐴))) +𝑜 suc (𝐹‘∩ (ω ∖ 𝐴))) = suc ((𝐹‘(𝐴 ∖ ∩ (ω ∖ 𝐴))) +𝑜 (𝐹‘∩ (ω ∖ 𝐴))))
44		incom 3957	. . . . . . . . 9 ⊢ ((𝐴 ∖ ∩ (ω ∖ 𝐴)) ∩ ∩ (ω ∖ 𝐴)) = (∩ (ω ∖ 𝐴) ∩ (𝐴 ∖ ∩ (ω ∖ 𝐴)))
45		disjdif 4183	. . . . . . . . 9 ⊢ (∩ (ω ∖ 𝐴) ∩ (𝐴 ∖ ∩ (ω ∖ 𝐴))) = ∅
46	44, 45	eqtri 2793	. . . . . . . 8 ⊢ ((𝐴 ∖ ∩ (ω ∖ 𝐴)) ∩ ∩ (ω ∖ 𝐴)) = ∅
47	46	a1i 11	. . . . . . 7 ⊢ (𝐴 ∈ (𝒫 ω ∩ Fin) → ((𝐴 ∖ ∩ (ω ∖ 𝐴)) ∩ ∩ (ω ∖ 𝐴)) = ∅)
48	2	ackbij1lem9 9253	. . . . . . 7 ⊢ (((𝐴 ∖ ∩ (ω ∖ 𝐴)) ∈ (𝒫 ω ∩ Fin) ∧ ∩ (ω ∖ 𝐴) ∈ (𝒫 ω ∩ Fin) ∧ ((𝐴 ∖ ∩ (ω ∖ 𝐴)) ∩ ∩ (ω ∖ 𝐴)) = ∅) → (𝐹‘((𝐴 ∖ ∩ (ω ∖ 𝐴)) ∪ ∩ (ω ∖ 𝐴))) = ((𝐹‘(𝐴 ∖ ∩ (ω ∖ 𝐴))) +𝑜 (𝐹‘∩ (ω ∖ 𝐴))))
49	4, 39, 47, 48	syl3anc 1476	. . . . . 6 ⊢ (𝐴 ∈ (𝒫 ω ∩ Fin) → (𝐹‘((𝐴 ∖ ∩ (ω ∖ 𝐴)) ∪ ∩ (ω ∖ 𝐴))) = ((𝐹‘(𝐴 ∖ ∩ (ω ∖ 𝐴))) +𝑜 (𝐹‘∩ (ω ∖ 𝐴))))
50		uncom 3909	. . . . . . . 8 ⊢ ((𝐴 ∖ ∩ (ω ∖ 𝐴)) ∪ ∩ (ω ∖ 𝐴)) = (∩ (ω ∖ 𝐴) ∪ (𝐴 ∖ ∩ (ω ∖ 𝐴)))
51		onnmin 7151	. . . . . . . . . . . . . . 15 ⊢ (((ω ∖ 𝐴) ⊆ On ∧ 𝑎 ∈ (ω ∖ 𝐴)) → ¬ 𝑎 ∈ ∩ (ω ∖ 𝐴))
52	7, 51	mpan 664	. . . . . . . . . . . . . 14 ⊢ (𝑎 ∈ (ω ∖ 𝐴) → ¬ 𝑎 ∈ ∩ (ω ∖ 𝐴))
53	52	con2i 136	. . . . . . . . . . . . 13 ⊢ (𝑎 ∈ ∩ (ω ∖ 𝐴) → ¬ 𝑎 ∈ (ω ∖ 𝐴))
54	53	adantl 467	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝑎 ∈ ∩ (ω ∖ 𝐴)) → ¬ 𝑎 ∈ (ω ∖ 𝐴))
55		ordom 7222	. . . . . . . . . . . . . . 15 ⊢ Ord ω
56		ordelss 5883	. . . . . . . . . . . . . . 15 ⊢ ((Ord ω ∧ ∩ (ω ∖ 𝐴) ∈ ω) → ∩ (ω ∖ 𝐴) ⊆ ω)
57	55, 20, 56	sylancr 569	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ (𝒫 ω ∩ Fin) → ∩ (ω ∖ 𝐴) ⊆ ω)
58	57	sselda 3753	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝑎 ∈ ∩ (ω ∖ 𝐴)) → 𝑎 ∈ ω)
59		eldif 3734	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 ∈ (ω ∖ 𝐴) ↔ (𝑎 ∈ ω ∧ ¬ 𝑎 ∈ 𝐴))
60	59	simplbi2 484	. . . . . . . . . . . . . . 15 ⊢ (𝑎 ∈ ω → (¬ 𝑎 ∈ 𝐴 → 𝑎 ∈ (ω ∖ 𝐴)))
61	60	orrd 844	. . . . . . . . . . . . . 14 ⊢ (𝑎 ∈ ω → (𝑎 ∈ 𝐴 ∨ 𝑎 ∈ (ω ∖ 𝐴)))
62	61	orcomd 852	. . . . . . . . . . . . 13 ⊢ (𝑎 ∈ ω → (𝑎 ∈ (ω ∖ 𝐴) ∨ 𝑎 ∈ 𝐴))
63	58, 62	syl 17	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝑎 ∈ ∩ (ω ∖ 𝐴)) → (𝑎 ∈ (ω ∖ 𝐴) ∨ 𝑎 ∈ 𝐴))
64		orel1 867	. . . . . . . . . . . 12 ⊢ (¬ 𝑎 ∈ (ω ∖ 𝐴) → ((𝑎 ∈ (ω ∖ 𝐴) ∨ 𝑎 ∈ 𝐴) → 𝑎 ∈ 𝐴))
65	54, 63, 64	sylc 65	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝑎 ∈ ∩ (ω ∖ 𝐴)) → 𝑎 ∈ 𝐴)
66	65	ex 397	. . . . . . . . . 10 ⊢ (𝐴 ∈ (𝒫 ω ∩ Fin) → (𝑎 ∈ ∩ (ω ∖ 𝐴) → 𝑎 ∈ 𝐴))
67	66	ssrdv 3759	. . . . . . . . 9 ⊢ (𝐴 ∈ (𝒫 ω ∩ Fin) → ∩ (ω ∖ 𝐴) ⊆ 𝐴)
68		undif 4192	. . . . . . . . 9 ⊢ (∩ (ω ∖ 𝐴) ⊆ 𝐴 ↔ (∩ (ω ∖ 𝐴) ∪ (𝐴 ∖ ∩ (ω ∖ 𝐴))) = 𝐴)
69	67, 68	sylib 208	. . . . . . . 8 ⊢ (𝐴 ∈ (𝒫 ω ∩ Fin) → (∩ (ω ∖ 𝐴) ∪ (𝐴 ∖ ∩ (ω ∖ 𝐴))) = 𝐴)
70	50, 69	syl5eq 2817	. . . . . . 7 ⊢ (𝐴 ∈ (𝒫 ω ∩ Fin) → ((𝐴 ∖ ∩ (ω ∖ 𝐴)) ∪ ∩ (ω ∖ 𝐴)) = 𝐴)
71	70	fveq2d 6337	. . . . . 6 ⊢ (𝐴 ∈ (𝒫 ω ∩ Fin) → (𝐹‘((𝐴 ∖ ∩ (ω ∖ 𝐴)) ∪ ∩ (ω ∖ 𝐴))) = (𝐹‘𝐴))
72	49, 71	eqtr3d 2807	. . . . 5 ⊢ (𝐴 ∈ (𝒫 ω ∩ Fin) → ((𝐹‘(𝐴 ∖ ∩ (ω ∖ 𝐴))) +𝑜 (𝐹‘∩ (ω ∖ 𝐴))) = (𝐹‘𝐴))
73		suceq 5934	. . . . 5 ⊢ (((𝐹‘(𝐴 ∖ ∩ (ω ∖ 𝐴))) +𝑜 (𝐹‘∩ (ω ∖ 𝐴))) = (𝐹‘𝐴) → suc ((𝐹‘(𝐴 ∖ ∩ (ω ∖ 𝐴))) +𝑜 (𝐹‘∩ (ω ∖ 𝐴))) = suc (𝐹‘𝐴))
74	72, 73	syl 17	. . . 4 ⊢ (𝐴 ∈ (𝒫 ω ∩ Fin) → suc ((𝐹‘(𝐴 ∖ ∩ (ω ∖ 𝐴))) +𝑜 (𝐹‘∩ (ω ∖ 𝐴))) = suc (𝐹‘𝐴))
75	43, 74	eqtrd 2805	. . 3 ⊢ (𝐴 ∈ (𝒫 ω ∩ Fin) → ((𝐹‘(𝐴 ∖ ∩ (ω ∖ 𝐴))) +𝑜 suc (𝐹‘∩ (ω ∖ 𝐴))) = suc (𝐹‘𝐴))
76	31, 34, 75	3eqtrd 2809	. 2 ⊢ (𝐴 ∈ (𝒫 ω ∩ Fin) → (𝐹‘((𝐴 ∖ ∩ (ω ∖ 𝐴)) ∪ {∩ (ω ∖ 𝐴)})) = suc (𝐹‘𝐴))
77		fveq2 6333	. . . 4 ⊢ (𝑏 = ((𝐴 ∖ ∩ (ω ∖ 𝐴)) ∪ {∩ (ω ∖ 𝐴)}) → (𝐹‘𝑏) = (𝐹‘((𝐴 ∖ ∩ (ω ∖ 𝐴)) ∪ {∩ (ω ∖ 𝐴)})))
78	77	eqeq1d 2773	. . 3 ⊢ (𝑏 = ((𝐴 ∖ ∩ (ω ∖ 𝐴)) ∪ {∩ (ω ∖ 𝐴)}) → ((𝐹‘𝑏) = suc (𝐹‘𝐴) ↔ (𝐹‘((𝐴 ∖ ∩ (ω ∖ 𝐴)) ∪ {∩ (ω ∖ 𝐴)})) = suc (𝐹‘𝐴)))
79	78	rspcev 3461	. 2 ⊢ ((((𝐴 ∖ ∩ (ω ∖ 𝐴)) ∪ {∩ (ω ∖ 𝐴)}) ∈ (𝒫 ω ∩ Fin) ∧ (𝐹‘((𝐴 ∖ ∩ (ω ∖ 𝐴)) ∪ {∩ (ω ∖ 𝐴)})) = suc (𝐹‘𝐴)) → ∃𝑏 ∈ (𝒫 ω ∩ Fin)(𝐹‘𝑏) = suc (𝐹‘𝐴))
80	24, 76, 79	syl2anc 567	1 ⊢ (𝐴 ∈ (𝒫 ω ∩ Fin) → ∃𝑏 ∈ (𝒫 ω ∩ Fin)(𝐹‘𝑏) = suc (𝐹‘𝐴))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 382   ∨ wo 828   = wceq 1631   ∈ wcel 2145   ≠ wne 2943  ∃wrex 3062   ∖ cdif 3721   ∪ cun 3722   ∩ cin 3723   ⊆ wss 3724  ∅c0 4064  𝒫 cpw 4298  {csn 4317  ∩ cint 4612  ∪ ciun 4655   ↦ cmpt 4864   × cxp 5248  Ord word 5866  Oncon0 5867  suc csuc 5869  ‘cfv 6032  (class class class)co 6794  ωcom 7213   +_𝑜 coa 7711  Fincfn 8110  cardccrd 8962

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-rep 4905  ax-sep 4916  ax-nul 4924  ax-pow 4975  ax-pr 5035  ax-un 7097

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 829  df-3or 1072  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3353  df-sbc 3589  df-csb 3684  df-dif 3727  df-un 3729  df-in 3731  df-ss 3738  df-pss 3740  df-nul 4065  df-if 4227  df-pw 4300  df-sn 4318  df-pr 4320  df-tp 4322  df-op 4324  df-uni 4576  df-int 4613  df-iun 4657  df-br 4788  df-opab 4848  df-mpt 4865  df-tr 4888  df-id 5158  df-eprel 5163  df-po 5171  df-so 5172  df-fr 5209  df-we 5211  df-xp 5256  df-rel 5257  df-cnv 5258  df-co 5259  df-dm 5260  df-rn 5261  df-res 5262  df-ima 5263  df-pred 5824  df-ord 5870  df-on 5871  df-lim 5872  df-suc 5873  df-iota 5995  df-fun 6034  df-fn 6035  df-f 6036  df-f1 6037  df-fo 6038  df-f1o 6039  df-fv 6040  df-ov 6797  df-oprab 6798  df-mpt2 6799  df-om 7214  df-1st 7316  df-2nd 7317  df-wrecs 7560  df-recs 7622  df-rdg 7660  df-1o 7714  df-2o 7715  df-oadd 7718  df-er 7897  df-map 8012  df-en 8111  df-dom 8112  df-sdom 8113  df-fin 8114  df-card 8966  df-cda 9193

This theorem is referenced by:  ackbij1  9263