Theorem usgfis 40031

Description: An undirected simple graph of finite order (i.e. with a finite number of vertices) is of finite size, i.e. it has also only a finite number of edges, analogous to usgrafis 25192. Remark: The proof of this theorem is very long compared with usgrafis 25192, because the theorem brfi1ind 12685 to perform the finite induction is taylored for binary relations, so that the theorem itself and the used lemmas must be transformed accordingly. Maybe a variant of brfi1ind 12685 could be provided, which is better suitable for this theorem. (Contributed by Alexander van der Vekens, 6-Jan-2018.) (Revised by AV, 11-Jan-2018.) (Proof modification is discouraged.)

Assertion

Ref	Expression
usgfis	|- ( G e. FinUSGrph -> ( GrSize ` G ) e. NN0 )

Proof of Theorem usgfis

Dummy variables e f v w y p q n are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fusgraimpcl 40012	. 2 |- ( G e. FinUSGrph -> ( G e. USGrph /\ ( GrOrder ` G ) e. NN0 ) )
2		relusgra 25111	. . . . . . . . . . 11 |- Rel USGrph
3		1st2nd 6866	. . . . . . . . . . 11 |- ( ( Rel USGrph /\ G e. USGrph ) -> G = <. ( 1st ` G ) , ( 2nd ` G ) >. )
4	2, 3	mpan 681	. . . . . . . . . 10 |- ( G e. USGrph -> G = <. ( 1st ` G ) , ( 2nd ` G ) >. )
5		eleq1 2528	. . . . . . . . . . . 12 |- ( G = <. ( 1st ` G ) , ( 2nd ` G ) >. -> ( G e. USGrph <-> <. ( 1st ` G ) , ( 2nd ` G ) >. e. USGrph ) )
6		df-br 4417	. . . . . . . . . . . 12 |- ( ( 1st ` G ) USGrph ( 2nd ` G ) <-> <. ( 1st ` G ) , ( 2nd ` G ) >. e. USGrph )
7	5, 6	syl6bbr 271	. . . . . . . . . . 11 |- ( G = <. ( 1st ` G ) , ( 2nd ` G ) >. -> ( G e. USGrph <-> ( 1st ` G ) USGrph ( 2nd ` G ) ) )
8		mptresid 5178	. . . . . . . . . . . . . 14 |- ( q e. { p e. ( Edges ` <. v , e >. ) | n e/ p } |-> q ) = ( _I |` { p e. ( Edges ` <. v , e >. ) | n e/ p } )
9		fvex 5898	. . . . . . . . . . . . . . 15 |- ( Edges ` <. v , e >. ) e. _V
10	9	mptrabex 6162	. . . . . . . . . . . . . 14 |- ( q e. { p e. ( Edges ` <. v , e >. ) | n e/ p } |-> q ) e. _V
11	8, 10	eqeltrri 2537	. . . . . . . . . . . . 13 |- ( _I |` { p e. ( Edges ` <. v , e >. ) | n e/ p } ) e. _V
12		eleq1 2528	. . . . . . . . . . . . . 14 |- ( e = ( 2nd ` G ) -> ( e e. Fin <-> ( 2nd ` G ) e. Fin ) )
13	12	adantl 472	. . . . . . . . . . . . 13 |- ( ( v = ( 1st ` G ) /\ e = ( 2nd ` G ) ) -> ( e e. Fin <-> ( 2nd ` G ) e. Fin ) )
14		eleq1 2528	. . . . . . . . . . . . . 14 |- ( e = f -> ( e e. Fin <-> f e. Fin ) )
15	14	adantl 472	. . . . . . . . . . . . 13 |- ( ( v = w /\ e = f ) -> ( e e. Fin <-> f e. Fin ) )
16		df-br 4417	. . . . . . . . . . . . . 14 |- ( v USGrph e <-> <. v , e >. e. USGrph )
17		opex 4678	. . . . . . . . . . . . . . . . 17 |- <. v , e >. e. _V
18		vtxvalaltv 39968	. . . . . . . . . . . . . . . . 17 |- ( <. v , e >. e. _V -> ( VtxALTV ` <. v , e >. ) = ( 1st ` <. v , e >. ) )
19	17, 18	ax-mp 5	. . . . . . . . . . . . . . . 16 |- ( VtxALTV ` <. v , e >. ) = ( 1st ` <. v , e >. )
20		vex 3060	. . . . . . . . . . . . . . . . 17 |- v e. _V
21		vex 3060	. . . . . . . . . . . . . . . . 17 |- e e. _V
22	20, 21	op1st 6828	. . . . . . . . . . . . . . . 16 |- ( 1st ` <. v , e >. ) = v
23	19, 22	eqtr2i 2485	. . . . . . . . . . . . . . 15 |- v = ( VtxALTV ` <. v , e >. )
24		eqid 2462	. . . . . . . . . . . . . . 15 |- ( Edges ` <. v , e >. ) = ( Edges ` <. v , e >. )
25		eqid 2462	. . . . . . . . . . . . . . 15 |- { p e. ( Edges ` <. v , e >. ) | n e/ p } = { p e. ( Edges ` <. v , e >. ) | n e/ p }
26	23, 24, 25	usgresvm1 40028	. . . . . . . . . . . . . 14 |- ( ( <. v , e >. e. USGrph /\ n e. v ) -> ( v \ { n } ) USGrph ( _I |` { p e. ( Edges ` <. v , e >. ) | n e/ p } ) )
27	16, 26	sylanb 479	. . . . . . . . . . . . 13 |- ( ( v USGrph e /\ n e. v ) -> ( v \ { n } ) USGrph ( _I |` { p e. ( Edges ` <. v , e >. ) | n e/ p } ) )
28		eleq1 2528	. . . . . . . . . . . . . 14 |- ( f = ( _I |` { p e. ( Edges ` <. v , e >. ) | n e/ p } ) -> ( f e. Fin <-> ( _I |` { p e. ( Edges ` <. v , e >. ) | n e/ p } ) e. Fin ) )
29	28	adantl 472	. . . . . . . . . . . . 13 |- ( ( w = ( v \ { n } ) /\ f = ( _I |` { p e. ( Edges ` <. v , e >. ) | n e/ p } ) ) -> ( f e. Fin <-> ( _I |` { p e. ( Edges ` <. v , e >. ) | n e/ p } ) e. Fin ) )
30		usgrafisbaseALT 40025	. . . . . . . . . . . . 13 |- ( ( v USGrph e /\ ( # ` v ) = 0 ) -> e e. Fin )
31		residfi 39081	. . . . . . . . . . . . . . . 16 |- ( ( _I |` { p e. ( Edges ` <. v , e >. ) | n e/ p } ) e. Fin <-> { p e. ( Edges ` <. v , e >. ) | n e/ p } e. Fin )
32		simpr1 1020	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( y + 1 ) e. NN0 /\ ( v USGrph e /\ ( # ` v ) = ( y + 1 ) /\ n e. v ) ) -> v USGrph e )
33		eleq1 2528	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( y + 1 ) = ( # ` v ) -> ( ( y + 1 ) e. NN0 <-> ( # ` v ) e. NN0 ) )
34	33	eqcoms 2470	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( # ` v ) = ( y + 1 ) -> ( ( y + 1 ) e. NN0 <-> ( # ` v ) e. NN0 ) )
35		hashclb 12572	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( v e. _V -> ( v e. Fin <-> ( # ` v ) e. NN0 ) )
36	35	bicomd 206	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( v e. _V -> ( ( # ` v ) e. NN0 <-> v e. Fin ) )
37	20, 36	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( # ` v ) e. NN0 <-> v e. Fin )
38	37	biimpi 199	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( # ` v ) e. NN0 -> v e. Fin )
39	34, 38	syl6bi 236	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( # ` v ) = ( y + 1 ) -> ( ( y + 1 ) e. NN0 -> v e. Fin ) )
40	39	3ad2ant2 1036	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( v USGrph e /\ ( # ` v ) = ( y + 1 ) /\ n e. v ) -> ( ( y + 1 ) e. NN0 -> v e. Fin ) )
41	40	impcom 436	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( y + 1 ) e. NN0 /\ ( v USGrph e /\ ( # ` v ) = ( y + 1 ) /\ n e. v ) ) -> v e. Fin )
42	32, 41	jca 539	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( y + 1 ) e. NN0 /\ ( v USGrph e /\ ( # ` v ) = ( y + 1 ) /\ n e. v ) ) -> ( v USGrph e /\ v e. Fin ) )
43		usgrav 25114	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( v USGrph e -> ( v e. _V /\ e e. _V ) )
44		df-br 4417	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( v FinUSGrph e <-> <. v , e >. e. FinUSGrph )
45		isfusgra0 40010	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( v e. _V /\ e e. _V ) -> ( v FinUSGrph e <-> ( v USGrph e /\ v e. Fin ) ) )
46	44, 45	syl5bbr 267	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( v e. _V /\ e e. _V ) -> ( <. v , e >. e. FinUSGrph <-> ( v USGrph e /\ v e. Fin ) ) )
47	43, 46	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 |- ( v USGrph e -> ( <. v , e >. e. FinUSGrph <-> ( v USGrph e /\ v e. Fin ) ) )
48	47	3ad2ant1 1035	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( v USGrph e /\ ( # ` v ) = ( y + 1 ) /\ n e. v ) -> ( <. v , e >. e. FinUSGrph <-> ( v USGrph e /\ v e. Fin ) ) )
49	48	adantl 472	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( y + 1 ) e. NN0 /\ ( v USGrph e /\ ( # ` v ) = ( y + 1 ) /\ n e. v ) ) -> ( <. v , e >. e. FinUSGrph <-> ( v USGrph e /\ v e. Fin ) ) )
50	42, 49	mpbird 240	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( y + 1 ) e. NN0 /\ ( v USGrph e /\ ( # ` v ) = ( y + 1 ) /\ n e. v ) ) -> <. v , e >. e. FinUSGrph )
51	17, 18	mp1i 13	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( v USGrph e -> ( VtxALTV ` <. v , e >. ) = ( 1st ` <. v , e >. ) )
52	51, 22	syl6req 2513	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( v USGrph e -> v = ( VtxALTV ` <. v , e >. ) )
53	52	eleq2d 2525	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( v USGrph e -> ( n e. v <-> n e. ( VtxALTV ` <. v , e >. ) ) )
54	53	biimpd 212	. . . . . . . . . . . . . . . . . . . . . 22 |- ( v USGrph e -> ( n e. v -> n e. ( VtxALTV ` <. v , e >. ) ) )
55	54	a1d 26	. . . . . . . . . . . . . . . . . . . . 21 |- ( v USGrph e -> ( ( # ` v ) = ( y + 1 ) -> ( n e. v -> n e. ( VtxALTV ` <. v , e >. ) ) ) )
56	55	3imp 1208	. . . . . . . . . . . . . . . . . . . 20 |- ( ( v USGrph e /\ ( # ` v ) = ( y + 1 ) /\ n e. v ) -> n e. ( VtxALTV ` <. v , e >. ) )
57	56	adantl 472	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( y + 1 ) e. NN0 /\ ( v USGrph e /\ ( # ` v ) = ( y + 1 ) /\ n e. v ) ) -> n e. ( VtxALTV ` <. v , e >. ) )
58	50, 57	jca 539	. . . . . . . . . . . . . . . . . 18 |- ( ( ( y + 1 ) e. NN0 /\ ( v USGrph e /\ ( # ` v ) = ( y + 1 ) /\ n e. v ) ) -> ( <. v , e >. e. FinUSGrph /\ n e. ( VtxALTV ` <. v , e >. ) ) )
59		eqid 2462	. . . . . . . . . . . . . . . . . . 19 |- ( VtxALTV ` <. v , e >. ) = ( VtxALTV ` <. v , e >. )
60		df-ov 6318	. . . . . . . . . . . . . . . . . . 19 |- ( v Edges e ) = ( Edges ` <. v , e >. )
61	60	eqcomi 2471	. . . . . . . . . . . . . . . . . . . 20 |- ( Edges ` <. v , e >. ) = ( v Edges e )
62		rabeq 3050	. . . . . . . . . . . . . . . . . . . 20 |- ( ( Edges ` <. v , e >. ) = ( v Edges e ) -> { p e. ( Edges ` <. v , e >. ) | n e/ p } = { p e. ( v Edges e ) | n e/ p } )
63	61, 62	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 |- { p e. ( Edges ` <. v , e >. ) | n e/ p } = { p e. ( v Edges e ) | n e/ p }
64	59, 60, 63	usgfislem2 40030	. . . . . . . . . . . . . . . . . 18 |- ( ( <. v , e >. e. FinUSGrph /\ n e. ( VtxALTV ` <. v , e >. ) ) -> ( ( v Edges e ) e. Fin <-> { p e. ( Edges ` <. v , e >. ) | n e/ p } e. Fin ) )
65	58, 64	syl 17	. . . . . . . . . . . . . . . . 17 |- ( ( ( y + 1 ) e. NN0 /\ ( v USGrph e /\ ( # ` v ) = ( y + 1 ) /\ n e. v ) ) -> ( ( v Edges e ) e. Fin <-> { p e. ( Edges ` <. v , e >. ) | n e/ p } e. Fin ) )
66	65	biimprd 231	. . . . . . . . . . . . . . . 16 |- ( ( ( y + 1 ) e. NN0 /\ ( v USGrph e /\ ( # ` v ) = ( y + 1 ) /\ n e. v ) ) -> ( { p e. ( Edges ` <. v , e >. ) | n e/ p } e. Fin -> ( v Edges e ) e. Fin ) )
67	31, 66	syl5bi 225	. . . . . . . . . . . . . . 15 |- ( ( ( y + 1 ) e. NN0 /\ ( v USGrph e /\ ( # ` v ) = ( y + 1 ) /\ n e. v ) ) -> ( ( _I |` { p e. ( Edges ` <. v , e >. ) | n e/ p } ) e. Fin -> ( v Edges e ) e. Fin ) )
68	67	imp 435	. . . . . . . . . . . . . 14 |- ( ( ( ( y + 1 ) e. NN0 /\ ( v USGrph e /\ ( # ` v ) = ( y + 1 ) /\ n e. v ) ) /\ ( _I |` { p e. ( Edges ` <. v , e >. ) | n e/ p } ) e. Fin ) -> ( v Edges e ) e. Fin )
69		usgedgffibi 40019	. . . . . . . . . . . . . . . . 17 |- ( v USGrph e -> ( e e. Fin <-> ( v Edges e ) e. Fin ) )
70	69	3ad2ant1 1035	. . . . . . . . . . . . . . . 16 |- ( ( v USGrph e /\ ( # ` v ) = ( y + 1 ) /\ n e. v ) -> ( e e. Fin <-> ( v Edges e ) e. Fin ) )
71	70	adantl 472	. . . . . . . . . . . . . . 15 |- ( ( ( y + 1 ) e. NN0 /\ ( v USGrph e /\ ( # ` v ) = ( y + 1 ) /\ n e. v ) ) -> ( e e. Fin <-> ( v Edges e ) e. Fin ) )
72	71	adantr 471	. . . . . . . . . . . . . 14 |- ( ( ( ( y + 1 ) e. NN0 /\ ( v USGrph e /\ ( # ` v ) = ( y + 1 ) /\ n e. v ) ) /\ ( _I |` { p e. ( Edges ` <. v , e >. ) | n e/ p } ) e. Fin ) -> ( e e. Fin <-> ( v Edges e ) e. Fin ) )
73	68, 72	mpbird 240	. . . . . . . . . . . . 13 |- ( ( ( ( y + 1 ) e. NN0 /\ ( v USGrph e /\ ( # ` v ) = ( y + 1 ) /\ n e. v ) ) /\ ( _I |` { p e. ( Edges ` <. v , e >. ) | n e/ p } ) e. Fin ) -> e e. Fin )
74	2, 11, 13, 15, 27, 29, 30, 73	brfi1ind 12685	. . . . . . . . . . . 12 |- ( ( ( 1st ` G ) USGrph ( 2nd ` G ) /\ ( 1st ` G ) e. Fin ) -> ( 2nd ` G ) e. Fin )
75	74	ex 440	. . . . . . . . . . 11 |- ( ( 1st ` G ) USGrph ( 2nd ` G ) -> ( ( 1st ` G ) e. Fin -> ( 2nd ` G ) e. Fin ) )
76	7, 75	syl6bi 236	. . . . . . . . . 10 |- ( G = <. ( 1st ` G ) , ( 2nd ` G ) >. -> ( G e. USGrph -> ( ( 1st ` G ) e. Fin -> ( 2nd ` G ) e. Fin ) ) )
77	4, 76	mpcom 37	. . . . . . . . 9 |- ( G e. USGrph -> ( ( 1st ` G ) e. Fin -> ( 2nd ` G ) e. Fin ) )
78	77	imp 435	. . . . . . . 8 |- ( ( G e. USGrph /\ ( 1st ` G ) e. Fin ) -> ( 2nd ` G ) e. Fin )
79		rnfi 7883	. . . . . . . 8 |- ( ( 2nd ` G ) e. Fin -> ran ( 2nd ` G ) e. Fin )
80	78, 79	syl 17	. . . . . . 7 |- ( ( G e. USGrph /\ ( 1st ` G ) e. Fin ) -> ran ( 2nd ` G ) e. Fin )
81		edgval 25115	. . . . . . . . 9 |- ( G e. USGrph -> ( Edges ` G ) = ran ( 2nd ` G ) )
82	81	eleq1d 2524	. . . . . . . 8 |- ( G e. USGrph -> ( ( Edges ` G ) e. Fin <-> ran ( 2nd ` G ) e. Fin ) )
83	82	adantr 471	. . . . . . 7 |- ( ( G e. USGrph /\ ( 1st ` G ) e. Fin ) -> ( ( Edges ` G ) e. Fin <-> ran ( 2nd ` G ) e. Fin ) )
84	80, 83	mpbird 240	. . . . . 6 |- ( ( G e. USGrph /\ ( 1st ` G ) e. Fin ) -> ( Edges ` G ) e. Fin )
85	84	ex 440	. . . . 5 |- ( G e. USGrph -> ( ( 1st ` G ) e. Fin -> ( Edges ` G ) e. Fin ) )
86	85	a1dd 47	. . . 4 |- ( G e. USGrph -> ( ( 1st ` G ) e. Fin -> ( G e. FinUSGrph -> ( Edges ` G ) e. Fin ) ) )
87		gordval 39973	. . . . . 6 |- ( G e. USGrph -> ( GrOrder ` G ) = ( # ` ( 1st ` G ) ) )
88	87	eleq1d 2524	. . . . 5 |- ( G e. USGrph -> ( ( GrOrder ` G ) e. NN0 <-> ( # ` ( 1st ` G ) ) e. NN0 ) )
89		fvex 5898	. . . . . 6 |- ( 1st ` G ) e. _V
90		hashclb 12572	. . . . . 6 |- ( ( 1st ` G ) e. _V -> ( ( 1st ` G ) e. Fin <-> ( # ` ( 1st ` G ) ) e. NN0 ) )
91	89, 90	ax-mp 5	. . . . 5 |- ( ( 1st ` G ) e. Fin <-> ( # ` ( 1st ` G ) ) e. NN0 )
92	88, 91	syl6bbr 271	. . . 4 |- ( G e. USGrph -> ( ( GrOrder ` G ) e. NN0 <-> ( 1st ` G ) e. Fin ) )
93		usgsizedg 39980	. . . . . . 7 |- ( G e. USGrph -> ( GrSize ` G ) = ( # ` ( Edges ` G ) ) )
94	93	eleq1d 2524	. . . . . 6 |- ( G e. USGrph -> ( ( GrSize ` G ) e. NN0 <-> ( # ` ( Edges ` G ) ) e. NN0 ) )
95		fvex 5898	. . . . . . 7 |- ( Edges ` G ) e. _V
96		hashclb 12572	. . . . . . 7 |- ( ( Edges ` G ) e. _V -> ( ( Edges ` G ) e. Fin <-> ( # ` ( Edges ` G ) ) e. NN0 ) )
97	95, 96	ax-mp 5	. . . . . 6 |- ( ( Edges ` G ) e. Fin <-> ( # ` ( Edges ` G ) ) e. NN0 )
98	94, 97	syl6bbr 271	. . . . 5 |- ( G e. USGrph -> ( ( GrSize ` G ) e. NN0 <-> ( Edges ` G ) e. Fin ) )
99	98	imbi2d 322	. . . 4 |- ( G e. USGrph -> ( ( G e. FinUSGrph -> ( GrSize ` G ) e. NN0 ) <-> ( G e. FinUSGrph -> ( Edges ` G ) e. Fin ) ) )
100	86, 92, 99	3imtr4d 276	. . 3 |- ( G e. USGrph -> ( ( GrOrder ` G ) e. NN0 -> ( G e. FinUSGrph -> ( GrSize ` G ) e. NN0 ) ) )
101	100	imp 435	. 2 |- ( ( G e. USGrph /\ ( GrOrder ` G ) e. NN0 ) -> ( G e. FinUSGrph -> ( GrSize ` G ) e. NN0 ) )
102	1, 101	mpcom 37	1 |- ( G e. FinUSGrph -> ( GrSize ` G ) e. NN0 )

Syntax hints:   -> wi 4   <-> wb 189   /\ wa 375   /\ w3a 991   = wceq 1455   e. wcel 1898   e/ wnel 2634   {crab 2753   _Vcvv 3057   \ cdif 3413   {csn 3980   <.cop 3986   class class class wbr 4416   |-> cmpt 4475   _I cid 4763   ran crn 4854   |` cres 4855   Rel wrel 4858   ` cfv 5601  (class class class)co 6315   1stc1st 6818   2ndc2nd 6819   Fincfn 7595   1c1 9566   + caddc 9568   NN0cn0 10898   #chash 12547   USGrph cusg 25106   Edges cedg 25107   VtxALTV cvtxaltv 39966   GrOrder cgord 39969   GrSize cgsiz 39970   FinUSGrph cfusg 40006

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 4529  ax-sep 4539  ax-nul 4548  ax-pow 4595  ax-pr 4653  ax-un 6610  ax-cnex 9621  ax-resscn 9622  ax-1cn 9623  ax-icn 9624  ax-addcl 9625  ax-addrcl 9626  ax-mulcl 9627  ax-mulrcl 9628  ax-mulcom 9629  ax-addass 9630  ax-mulass 9631  ax-distr 9632  ax-i2m1 9633  ax-1ne0 9634  ax-1rid 9635  ax-rnegex 9636  ax-rrecex 9637  ax-cnre 9638  ax-pre-lttri 9639  ax-pre-lttrn 9640  ax-pre-ltadd 9641  ax-pre-mulgt0 9642

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-nel 2636  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-br 4417  df-opab 4476  df-mpt 4477  df-tr 4512  df-eprel 4764  df-id 4768  df-po 4774  df-so 4775  df-fr 4812  df-we 4814  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-pred 5399  df-ord 5445  df-on 5446  df-lim 5447  df-suc 5448  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-riota 6277  df-ov 6318  df-oprab 6319  df-mpt2 6320  df-om 6720  df-1st 6820  df-2nd 6821  df-wrecs 7054  df-recs 7116  df-rdg 7154  df-1o 7208  df-2o 7209  df-oadd 7212  df-er 7389  df-en 7596  df-dom 7597  df-sdom 7598  df-fin 7599  df-card 8399  df-cda 8624  df-pnf 9703  df-mnf 9704  df-xr 9705  df-ltxr 9706  df-le 9707  df-sub 9888  df-neg 9889  df-nn 10638  df-2 10696  df-n0 10899  df-z 10967  df-uz 11189  df-fz 11814  df-hash 12548  df-uhgra 25068  df-umgra 25089  df-uslgra 25108  df-usgra 25109  df-edg 25112  df-vtxALTV 39967  df-gord 39971  df-gsiz 39972  df-fusg 40007

This theorem is referenced by:  usgrafiedgALT  40036