Theorem rankcf 9233

Description: Any set must be at least as large as the cofinality of its rank, because the ranks of the elements of A form a cofinal map into ( rank ` A ). (Contributed by Mario Carneiro, 27-May-2013.)

Assertion

Ref	Expression
rankcf	|- -. A ~< ( cf ` ( rank ` A ) )

Proof of Theorem rankcf

Dummy variables w x y z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		rankon 8297	. . 3 |- ( rank ` A ) e. On
2		onzsl 6705	. . 3 |- ( ( rank ` A ) e. On <-> ( ( rank ` A ) = (/) \/ E. x e. On ( rank ` A ) = suc x \/ ( ( rank ` A ) e. _V /\ Lim ( rank ` A ) ) ) )
3	1, 2	mpbi 213	. 2 |- ( ( rank ` A ) = (/) \/ E. x e. On ( rank ` A ) = suc x \/ ( ( rank ` A ) e. _V /\ Lim ( rank ` A ) ) )
4		sdom0 7735	. . . 4 |- -. A ~< (/)
5		fveq2 5892	. . . . . 6 |- ( ( rank ` A ) = (/) -> ( cf ` ( rank ` A ) ) = ( cf ` (/) ) )
6		cf0 8712	. . . . . 6 |- ( cf ` (/) ) = (/)
7	5, 6	syl6eq 2512	. . . . 5 |- ( ( rank ` A ) = (/) -> ( cf ` ( rank ` A ) ) = (/) )
8	7	breq2d 4430	. . . 4 |- ( ( rank ` A ) = (/) -> ( A ~< ( cf ` ( rank ` A ) ) <-> A ~< (/) ) )
9	4, 8	mtbiri 309	. . 3 |- ( ( rank ` A ) = (/) -> -. A ~< ( cf ` ( rank ` A ) ) )
10		fveq2 5892	. . . . . . 7 |- ( ( rank ` A ) = suc x -> ( cf ` ( rank ` A ) ) = ( cf ` suc x ) )
11		cfsuc 8718	. . . . . . 7 |- ( x e. On -> ( cf ` suc x ) = 1o )
12	10, 11	sylan9eqr 2518	. . . . . 6 |- ( ( x e. On /\ ( rank ` A ) = suc x ) -> ( cf ` ( rank ` A ) ) = 1o )
13		nsuceq0 5526	. . . . . . . . 9 |- suc x =/= (/)
14		neeq1 2698	. . . . . . . . 9 |- ( ( rank ` A ) = suc x -> ( ( rank ` A ) =/= (/) <-> suc x =/= (/) ) )
15	13, 14	mpbiri 241	. . . . . . . 8 |- ( ( rank ` A ) = suc x -> ( rank ` A ) =/= (/) )
16		fveq2 5892	. . . . . . . . . . 11 |- ( A = (/) -> ( rank ` A ) = ( rank ` (/) ) )
17		0elon 5499	. . . . . . . . . . . . 13 |- (/) e. On
18		r1fnon 8269	. . . . . . . . . . . . . 14 |- R1 Fn On
19		fndm 5701	. . . . . . . . . . . . . 14 |- ( R1 Fn On -> dom R1 = On )
20	18, 19	ax-mp 5	. . . . . . . . . . . . 13 |- dom R1 = On
21	17, 20	eleqtrri 2539	. . . . . . . . . . . 12 |- (/) e. dom R1
22		rankonid 8331	. . . . . . . . . . . 12 |- ( (/) e. dom R1 <-> ( rank ` (/) ) = (/) )
23	21, 22	mpbi 213	. . . . . . . . . . 11 |- ( rank ` (/) ) = (/)
24	16, 23	syl6eq 2512	. . . . . . . . . 10 |- ( A = (/) -> ( rank ` A ) = (/) )
25	24	necon3i 2668	. . . . . . . . 9 |- ( ( rank ` A ) =/= (/) -> A =/= (/) )
26		rankvaln 8301	. . . . . . . . . . 11 |- ( -. A e. U. ( R1 " On ) -> ( rank ` A ) = (/) )
27	26	necon1ai 2663	. . . . . . . . . 10 |- ( ( rank ` A ) =/= (/) -> A e. U. ( R1 " On ) )
28		breq2 4422	. . . . . . . . . . 11 |- ( y = A -> ( 1o ~<_ y <-> 1o ~<_ A ) )
29		neeq1 2698	. . . . . . . . . . 11 |- ( y = A -> ( y =/= (/) <-> A =/= (/) ) )
30		0sdom1dom 7801	. . . . . . . . . . . 12 |- ( (/) ~< y <-> 1o ~<_ y )
31		vex 3060	. . . . . . . . . . . . 13 |- y e. _V
32	31	0sdom 7734	. . . . . . . . . . . 12 |- ( (/) ~< y <-> y =/= (/) )
33	30, 32	bitr3i 259	. . . . . . . . . . 11 |- ( 1o ~<_ y <-> y =/= (/) )
34	28, 29, 33	vtoclbg 3120	. . . . . . . . . 10 |- ( A e. U. ( R1 " On ) -> ( 1o ~<_ A <-> A =/= (/) ) )
35	27, 34	syl 17	. . . . . . . . 9 |- ( ( rank ` A ) =/= (/) -> ( 1o ~<_ A <-> A =/= (/) ) )
36	25, 35	mpbird 240	. . . . . . . 8 |- ( ( rank ` A ) =/= (/) -> 1o ~<_ A )
37	15, 36	syl 17	. . . . . . 7 |- ( ( rank ` A ) = suc x -> 1o ~<_ A )
38	37	adantl 472	. . . . . 6 |- ( ( x e. On /\ ( rank ` A ) = suc x ) -> 1o ~<_ A )
39	12, 38	eqbrtrd 4439	. . . . 5 |- ( ( x e. On /\ ( rank ` A ) = suc x ) -> ( cf ` ( rank ` A ) ) ~<_ A )
40	39	rexlimiva 2887	. . . 4 |- ( E. x e. On ( rank ` A ) = suc x -> ( cf ` ( rank ` A ) ) ~<_ A )
41		domnsym 7729	. . . 4 |- ( ( cf ` ( rank ` A ) ) ~<_ A -> -. A ~< ( cf ` ( rank ` A ) ) )
42	40, 41	syl 17	. . 3 |- ( E. x e. On ( rank ` A ) = suc x -> -. A ~< ( cf ` ( rank ` A ) ) )
43		nlim0 5504	. . . . . . . . . . . . . . . . 17 |- -. Lim (/)
44		limeq 5458	. . . . . . . . . . . . . . . . 17 |- ( ( rank ` A ) = (/) -> ( Lim ( rank ` A ) <-> Lim (/) ) )
45	43, 44	mtbiri 309	. . . . . . . . . . . . . . . 16 |- ( ( rank ` A ) = (/) -> -. Lim ( rank ` A ) )
46	26, 45	syl 17	. . . . . . . . . . . . . . 15 |- ( -. A e. U. ( R1 " On ) -> -. Lim ( rank ` A ) )
47	46	con4i 135	. . . . . . . . . . . . . 14 |- ( Lim ( rank ` A ) -> A e. U. ( R1 " On ) )
48		r1elssi 8307	. . . . . . . . . . . . . 14 |- ( A e. U. ( R1 " On ) -> A C_ U. ( R1 " On ) )
49	47, 48	syl 17	. . . . . . . . . . . . 13 |- ( Lim ( rank ` A ) -> A C_ U. ( R1 " On ) )
50	49	sselda 3444	. . . . . . . . . . . 12 |- ( ( Lim ( rank ` A ) /\ x e. A ) -> x e. U. ( R1 " On ) )
51		ranksnb 8329	. . . . . . . . . . . 12 |- ( x e. U. ( R1 " On ) -> ( rank ` { x } ) = suc ( rank ` x ) )
52	50, 51	syl 17	. . . . . . . . . . 11 |- ( ( Lim ( rank ` A ) /\ x e. A ) -> ( rank ` { x } ) = suc ( rank ` x ) )
53		rankelb 8326	. . . . . . . . . . . . . 14 |- ( A e. U. ( R1 " On ) -> ( x e. A -> ( rank ` x ) e. ( rank ` A ) ) )
54	47, 53	syl 17	. . . . . . . . . . . . 13 |- ( Lim ( rank ` A ) -> ( x e. A -> ( rank ` x ) e. ( rank ` A ) ) )
55		limsuc 6708	. . . . . . . . . . . . 13 |- ( Lim ( rank ` A ) -> ( ( rank ` x ) e. ( rank ` A ) <-> suc ( rank ` x ) e. ( rank ` A ) ) )
56	54, 55	sylibd 222	. . . . . . . . . . . 12 |- ( Lim ( rank ` A ) -> ( x e. A -> suc ( rank ` x ) e. ( rank ` A ) ) )
57	56	imp 435	. . . . . . . . . . 11 |- ( ( Lim ( rank ` A ) /\ x e. A ) -> suc ( rank ` x ) e. ( rank ` A ) )
58	52, 57	eqeltrd 2540	. . . . . . . . . 10 |- ( ( Lim ( rank ` A ) /\ x e. A ) -> ( rank ` { x } ) e. ( rank ` A ) )
59		eleq1a 2535	. . . . . . . . . 10 |- ( ( rank ` { x } ) e. ( rank ` A ) -> ( w = ( rank ` { x } ) -> w e. ( rank ` A ) ) )
60	58, 59	syl 17	. . . . . . . . 9 |- ( ( Lim ( rank ` A ) /\ x e. A ) -> ( w = ( rank ` { x } ) -> w e. ( rank ` A ) ) )
61	60	rexlimdva 2891	. . . . . . . 8 |- ( Lim ( rank ` A ) -> ( E. x e. A w = ( rank ` { x } ) -> w e. ( rank ` A ) ) )
62	61	abssdv 3515	. . . . . . 7 |- ( Lim ( rank ` A ) -> { w | E. x e. A w = ( rank ` { x } ) } C_ ( rank ` A ) )
63		snex 4658	. . . . . . . . . . . . 13 |- { x } e. _V
64	63	dfiun2 4326	. . . . . . . . . . . 12 |- U_ x e. A { x } = U. { y | E. x e. A y = { x } }
65		iunid 4347	. . . . . . . . . . . 12 |- U_ x e. A { x } = A
66	64, 65	eqtr3i 2486	. . . . . . . . . . 11 |- U. { y | E. x e. A y = { x } } = A
67	66	fveq2i 5895	. . . . . . . . . 10 |- ( rank ` U. { y | E. x e. A y = { x } } ) = ( rank ` A )
68	48	sselda 3444	. . . . . . . . . . . . . . 15 |- ( ( A e. U. ( R1 " On ) /\ x e. A ) -> x e. U. ( R1 " On ) )
69		snwf 8311	. . . . . . . . . . . . . . 15 |- ( x e. U. ( R1 " On ) -> { x } e. U. ( R1 " On ) )
70		eleq1a 2535	. . . . . . . . . . . . . . 15 |- ( { x } e. U. ( R1 " On ) -> ( y = { x } -> y e. U. ( R1 " On ) ) )
71	68, 69, 70	3syl 18	. . . . . . . . . . . . . 14 |- ( ( A e. U. ( R1 " On ) /\ x e. A ) -> ( y = { x } -> y e. U. ( R1 " On ) ) )
72	71	rexlimdva 2891	. . . . . . . . . . . . 13 |- ( A e. U. ( R1 " On ) -> ( E. x e. A y = { x } -> y e. U. ( R1 " On ) ) )
73	72	abssdv 3515	. . . . . . . . . . . 12 |- ( A e. U. ( R1 " On ) -> { y | E. x e. A y = { x } } C_ U. ( R1 " On ) )
74		abrexexg 6800	. . . . . . . . . . . . 13 |- ( A e. U. ( R1 " On ) -> { y | E. x e. A y = { x } } e. _V )
75		eleq1 2528	. . . . . . . . . . . . . 14 |- ( z = { y | E. x e. A y = { x } } -> ( z e. U. ( R1 " On ) <-> { y | E. x e. A y = { x } } e. U. ( R1 " On ) ) )
76		sseq1 3465	. . . . . . . . . . . . . 14 |- ( z = { y | E. x e. A y = { x } } -> ( z C_ U. ( R1 " On ) <-> { y | E. x e. A y = { x } } C_ U. ( R1 " On ) ) )
77		vex 3060	. . . . . . . . . . . . . . 15 |- z e. _V
78	77	r1elss 8308	. . . . . . . . . . . . . 14 |- ( z e. U. ( R1 " On ) <-> z C_ U. ( R1 " On ) )
79	75, 76, 78	vtoclbg 3120	. . . . . . . . . . . . 13 |- ( { y | E. x e. A y = { x } } e. _V -> ( { y | E. x e. A y = { x } } e. U. ( R1 " On ) <-> { y | E. x e. A y = { x } } C_ U. ( R1 " On ) ) )
80	74, 79	syl 17	. . . . . . . . . . . 12 |- ( A e. U. ( R1 " On ) -> ( { y | E. x e. A y = { x } } e. U. ( R1 " On ) <-> { y | E. x e. A y = { x } } C_ U. ( R1 " On ) ) )
81	73, 80	mpbird 240	. . . . . . . . . . 11 |- ( A e. U. ( R1 " On ) -> { y | E. x e. A y = { x } } e. U. ( R1 " On ) )
82		rankuni2b 8355	. . . . . . . . . . 11 |- ( { y | E. x e. A y = { x } } e. U. ( R1 " On ) -> ( rank ` U. { y | E. x e. A y = { x } } ) = U_ z e. { y | E. x e. A y = { x } } ( rank ` z ) )
83	81, 82	syl 17	. . . . . . . . . 10 |- ( A e. U. ( R1 " On ) -> ( rank ` U. { y | E. x e. A y = { x } } ) = U_ z e. { y | E. x e. A y = { x } } ( rank ` z ) )
84	67, 83	syl5eqr 2510	. . . . . . . . 9 |- ( A e. U. ( R1 " On ) -> ( rank ` A ) = U_ z e. { y | E. x e. A y = { x } } ( rank ` z ) )
85		fvex 5902	. . . . . . . . . . 11 |- ( rank ` z ) e. _V
86	85	dfiun2 4326	. . . . . . . . . 10 |- U_ z e. { y | E. x e. A y = { x } } ( rank ` z ) = U. { w | E. z e. { y | E. x e. A y = { x } } w = ( rank ` z ) }
87		fveq2 5892	. . . . . . . . . . . 12 |- ( z = { x } -> ( rank ` z ) = ( rank ` { x } ) )
88	63, 87	abrexco 6179	. . . . . . . . . . 11 |- { w | E. z e. { y | E. x e. A y = { x } } w = ( rank ` z ) } = { w | E. x e. A w = ( rank ` { x } ) }
89	88	unieqi 4221	. . . . . . . . . 10 |- U. { w | E. z e. { y | E. x e. A y = { x } } w = ( rank ` z ) } = U. { w | E. x e. A w = ( rank ` { x } ) }
90	86, 89	eqtri 2484	. . . . . . . . 9 |- U_ z e. { y | E. x e. A y = { x } } ( rank ` z ) = U. { w | E. x e. A w = ( rank ` { x } ) }
91	84, 90	syl6req 2513	. . . . . . . 8 |- ( A e. U. ( R1 " On ) -> U. { w | E. x e. A w = ( rank ` { x } ) } = ( rank ` A ) )
92	47, 91	syl 17	. . . . . . 7 |- ( Lim ( rank ` A ) -> U. { w | E. x e. A w = ( rank ` { x } ) } = ( rank ` A ) )
93		fvex 5902	. . . . . . . 8 |- ( rank ` A ) e. _V
94	93	cfslb 8727	. . . . . . 7 |- ( ( Lim ( rank ` A ) /\ { w | E. x e. A w = ( rank ` { x } ) } C_ ( rank ` A ) /\ U. { w | E. x e. A w = ( rank ` { x } ) } = ( rank ` A ) ) -> ( cf ` ( rank ` A ) ) ~<_ { w | E. x e. A w = ( rank ` { x } ) } )
95	62, 92, 94	mpd3an23 1375	. . . . . 6 |- ( Lim ( rank ` A ) -> ( cf ` ( rank ` A ) ) ~<_ { w | E. x e. A w = ( rank ` { x } ) } )
96		fveq2 5892	. . . . . . . . . . 11 |- ( y = A -> ( rank ` y ) = ( rank ` A ) )
97	96	fveq2d 5896	. . . . . . . . . 10 |- ( y = A -> ( cf ` ( rank ` y ) ) = ( cf ` ( rank ` A ) ) )
98		breq12 4423	. . . . . . . . . 10 |- ( ( y = A /\ ( cf ` ( rank ` y ) ) = ( cf ` ( rank ` A ) ) ) -> ( y ~< ( cf ` ( rank ` y ) ) <-> A ~< ( cf ` ( rank ` A ) ) ) )
99	97, 98	mpdan 679	. . . . . . . . 9 |- ( y = A -> ( y ~< ( cf ` ( rank ` y ) ) <-> A ~< ( cf ` ( rank ` A ) ) ) )
100		rexeq 3000	. . . . . . . . . . 11 |- ( y = A -> ( E. x e. y w = ( rank ` { x } ) <-> E. x e. A w = ( rank ` { x } ) ) )
101	100	abbidv 2580	. . . . . . . . . 10 |- ( y = A -> { w | E. x e. y w = ( rank ` { x } ) } = { w | E. x e. A w = ( rank ` { x } ) } )
102		breq12 4423	. . . . . . . . . 10 |- ( ( { w | E. x e. y w = ( rank ` { x } ) } = { w | E. x e. A w = ( rank ` { x } ) } /\ y = A ) -> ( { w | E. x e. y w = ( rank ` { x } ) } ~<_ y <-> { w | E. x e. A w = ( rank ` { x } ) } ~<_ A ) )
103	101, 102	mpancom 680	. . . . . . . . 9 |- ( y = A -> ( { w | E. x e. y w = ( rank ` { x } ) } ~<_ y <-> { w | E. x e. A w = ( rank ` { x } ) } ~<_ A ) )
104	99, 103	imbi12d 326	. . . . . . . 8 |- ( y = A -> ( ( y ~< ( cf ` ( rank ` y ) ) -> { w | E. x e. y w = ( rank ` { x } ) } ~<_ y ) <-> ( A ~< ( cf ` ( rank ` A ) ) -> { w | E. x e. A w = ( rank ` { x } ) } ~<_ A ) ) )
105		eqid 2462	. . . . . . . . . 10 |- ( x e. y |-> ( rank ` { x } ) ) = ( x e. y |-> ( rank ` { x } ) )
106	105	rnmpt 5102	. . . . . . . . 9 |- ran ( x e. y |-> ( rank ` { x } ) ) = { w | E. x e. y w = ( rank ` { x } ) }
107		cfon 8716	. . . . . . . . . . 11 |- ( cf ` ( rank ` y ) ) e. On
108		sdomdom 7628	. . . . . . . . . . 11 |- ( y ~< ( cf ` ( rank ` y ) ) -> y ~<_ ( cf ` ( rank ` y ) ) )
109		ondomen 8499	. . . . . . . . . . 11 |- ( ( ( cf ` ( rank ` y ) ) e. On /\ y ~<_ ( cf ` ( rank ` y ) ) ) -> y e. dom card )
110	107, 108, 109	sylancr 674	. . . . . . . . . 10 |- ( y ~< ( cf ` ( rank ` y ) ) -> y e. dom card )
111		fvex 5902	. . . . . . . . . . . 12 |- ( rank ` { x } ) e. _V
112	111, 105	fnmpti 5732	. . . . . . . . . . 11 |- ( x e. y |-> ( rank ` { x } ) ) Fn y
113		dffn4 5826	. . . . . . . . . . 11 |- ( ( x e. y |-> ( rank ` { x } ) ) Fn y <-> ( x e. y |-> ( rank ` { x } ) ) : y -onto-> ran ( x e. y |-> ( rank ` { x } ) ) )
114	112, 113	mpbi 213	. . . . . . . . . 10 |- ( x e. y |-> ( rank ` { x } ) ) : y -onto-> ran ( x e. y |-> ( rank ` { x } ) )
115		fodomnum 8519	. . . . . . . . . 10 |- ( y e. dom card -> ( ( x e. y |-> ( rank ` { x } ) ) : y -onto-> ran ( x e. y |-> ( rank ` { x } ) ) -> ran ( x e. y |-> ( rank ` { x } ) ) ~<_ y ) )
116	110, 114, 115	mpisyl 21	. . . . . . . . 9 |- ( y ~< ( cf ` ( rank ` y ) ) -> ran ( x e. y |-> ( rank ` { x } ) ) ~<_ y )
117	106, 116	syl5eqbrr 4453	. . . . . . . 8 |- ( y ~< ( cf ` ( rank ` y ) ) -> { w | E. x e. y w = ( rank ` { x } ) } ~<_ y )
118	104, 117	vtoclg 3119	. . . . . . 7 |- ( A e. U. ( R1 " On ) -> ( A ~< ( cf ` ( rank ` A ) ) -> { w | E. x e. A w = ( rank ` { x } ) } ~<_ A ) )
119	47, 118	syl 17	. . . . . 6 |- ( Lim ( rank ` A ) -> ( A ~< ( cf ` ( rank ` A ) ) -> { w | E. x e. A w = ( rank ` { x } ) } ~<_ A ) )
120		domtr 7653	. . . . . . 7 |- ( ( ( cf ` ( rank ` A ) ) ~<_ { w | E. x e. A w = ( rank ` { x } ) } /\ { w | E. x e. A w = ( rank ` { x } ) } ~<_ A ) -> ( cf ` ( rank ` A ) ) ~<_ A )
121	120, 41	syl 17	. . . . . 6 |- ( ( ( cf ` ( rank ` A ) ) ~<_ { w | E. x e. A w = ( rank ` { x } ) } /\ { w | E. x e. A w = ( rank ` { x } ) } ~<_ A ) -> -. A ~< ( cf ` ( rank ` A ) ) )
122	95, 119, 121	syl6an 552	. . . . 5 |- ( Lim ( rank ` A ) -> ( A ~< ( cf ` ( rank ` A ) ) -> -. A ~< ( cf ` ( rank ` A ) ) ) )
123	122	pm2.01d 174	. . . 4 |- ( Lim ( rank ` A ) -> -. A ~< ( cf ` ( rank ` A ) ) )
124	123	adantl 472	. . 3 |- ( ( ( rank ` A ) e. _V /\ Lim ( rank ` A ) ) -> -. A ~< ( cf ` ( rank ` A ) ) )
125	9, 42, 124	3jaoi 1340	. 2 |- ( ( ( rank ` A ) = (/) \/ E. x e. On ( rank ` A ) = suc x \/ ( ( rank ` A ) e. _V /\ Lim ( rank ` A ) ) ) -> -. A ~< ( cf ` ( rank ` A ) ) )
126	3, 125	ax-mp 5	1 |- -. A ~< ( cf ` ( rank ` A ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 189   /\ wa 375   \/ w3o 990   = wceq 1455   e. wcel 1898   {cab 2448   =/= wne 2633   E.wrex 2750   _Vcvv 3057   C_ wss 3416   (/)c0 3743   {csn 3980   U.cuni 4212   U_ciun 4292   class class class wbr 4418   |-> cmpt 4477   dom cdm 4856   ran crn 4857   "cima 4859   Oncon0 5446   Lim wlim 5447   suc csuc 5448   Fn wfn 5600   -onto->wfo 5603   ` cfv 5605   1oc1o 7206   ~<_ cdom 7598   ~< csdm 7599   R1cr1 8264   rankcrnk 8265   cardccrd 8400   cfccf 8402

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-rep 4531  ax-sep 4541  ax-nul 4550  ax-pow 4598  ax-pr 4656  ax-un 6615

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-ral 2754  df-rex 2755  df-reu 2756  df-rmo 2757  df-rab 2758  df-v 3059  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-pss 3432  df-nul 3744  df-if 3894  df-pw 3965  df-sn 3981  df-pr 3983  df-tp 3985  df-op 3987  df-uni 4213  df-int 4249  df-iun 4294  df-iin 4295  df-br 4419  df-opab 4478  df-mpt 4479  df-tr 4514  df-eprel 4767  df-id 4771  df-po 4777  df-so 4778  df-fr 4815  df-se 4816  df-we 4817  df-xp 4862  df-rel 4863  df-cnv 4864  df-co 4865  df-dm 4866  df-rn 4867  df-res 4868  df-ima 4869  df-pred 5403  df-ord 5449  df-on 5450  df-lim 5451  df-suc 5452  df-iota 5569  df-fun 5607  df-fn 5608  df-f 5609  df-f1 5610  df-fo 5611  df-f1o 5612  df-fv 5613  df-isom 5614  df-riota 6282  df-ov 6323  df-oprab 6324  df-mpt2 6325  df-om 6725  df-1st 6825  df-2nd 6826  df-wrecs 7059  df-recs 7121  df-rdg 7159  df-1o 7213  df-er 7394  df-map 7505  df-en 7601  df-dom 7602  df-sdom 7603  df-fin 7604  df-r1 8266  df-rank 8267  df-card 8404  df-cf 8406  df-acn 8407

This theorem is referenced by:  inatsk  9234  grur1  9276