Theorem fodomfi 5656

Description: An onto function implies dominance of domain over range, for finite sets. Unlike fodom 5960 for arbitrary sets, this theorem does not require the Axiom of Choice for its proof.

Assertion

Ref	Expression
fodomfi	|- ((A e. Fin /\ F:A-onto->B) -> B ~<_ A)

Proof of Theorem fodomfi

Step	Hyp	Ref	Expression
1		fex 4595	. . . . . . . . . 10 |- ((F:A-->B /\ A e. _V) -> F e. _V)
2	1	ancoms 484	. . . . . . . . 9 |- ((A e. _V /\ F:A-->B) -> F e. _V)
3		relen 5431	. . . . . . . . . 10 |- Rel ~~
4	3	brrelexi 4029	. . . . . . . . 9 |- (A ~~ m -> A e. _V)
5		fof 4617	. . . . . . . . 9 |- (F:A-onto->B -> F:A-->B)
6	2, 4, 5	syl2an 503	. . . . . . . 8 |- ((A ~~ m /\ F:A-onto->B) -> F e. _V)
7	6	adantl 424	. . . . . . 7 |- ((m e. om /\ (A ~~ m /\ F:A-onto->B)) -> F e. _V)
8		visset 2295	. . . . . . . . . . . . 13 |- g e. _V
9		coexg 4429	. . . . . . . . . . . . 13 |- ((F e. _V /\ g e. _V) -> (F o. g) e. _V)
10	8, 9	mpan2 760	. . . . . . . . . . . 12 |- (F e. _V -> (F o. g) e. _V)
11		foeq1 4613	. . . . . . . . . . . . 13 |- (f = (F o. g) -> (f:m-onto->B <-> (F o. g):m-onto->B))
12	11	cla4egv 2365	. . . . . . . . . . . 12 |- ((F o. g) e. _V -> ((F o. g):m-onto->B -> E.f f:m-onto->B))
13	10, 12	syl 12	. . . . . . . . . . 11 |- (F e. _V -> ((F o. g):m-onto->B -> E.f f:m-onto->B))
14		visset 2295	. . . . . . . . . . . . . . 15 |- m e. _V
15		fornex 4625	. . . . . . . . . . . . . . 15 |- (m e. _V -> (f:m-onto->B -> B e. _V))
16	14, 15	ax-mp 7	. . . . . . . . . . . . . 14 |- (f:m-onto->B -> B e. _V)
17	16	19.23aiv 1674	. . . . . . . . . . . . 13 |- (E.f f:m-onto->B -> B e. _V)
18		foeq3 4615	. . . . . . . . . . . . . . . . 17 |- (x = B -> (f:m-onto->x <-> f:m-onto->B))
19	18	exbidv 1657	. . . . . . . . . . . . . . . 16 |- (x = B -> (E.f f:m-onto->x <-> E.f f:m-onto->B))
20		breq1 3341	. . . . . . . . . . . . . . . 16 |- (x = B -> (x ~<_ m <-> B ~<_ m))
21	19, 20	imbi12d 688	. . . . . . . . . . . . . . 15 |- (x = B -> ((E.f f:m-onto->x -> x ~<_ m) <-> (E.f f:m-onto->B -> B ~<_ m)))
22	21	cla4gv 2364	. . . . . . . . . . . . . 14 |- (B e. _V -> (A.x(E.f f:m-onto->x -> x ~<_ m) -> (E.f f:m-onto->B -> B ~<_ m)))
23		foeq2 4614	. . . . . . . . . . . . . . . . . 18 |- (m = (/) -> (f:m-onto->x <-> f:(/)-onto->x))
24	23	exbidv 1657	. . . . . . . . . . . . . . . . 17 |- (m = (/) -> (E.f f:m-onto->x <-> E.f f:(/)-onto->x))
25		breq2 3342	. . . . . . . . . . . . . . . . 17 |- (m = (/) -> (x ~<_ m <-> x ~<_ (/)))
26	24, 25	imbi12d 688	. . . . . . . . . . . . . . . 16 |- (m = (/) -> ((E.f f:m-onto->x -> x ~<_ m) <-> (E.f f:(/)-onto->x -> x ~<_ (/))))
27	26	albidv 1656	. . . . . . . . . . . . . . 15 |- (m = (/) -> (A.x(E.f f:m-onto->x -> x ~<_ m) <-> A.x(E.f f:(/)-onto->x -> x ~<_ (/))))
28		foeq2 4614	. . . . . . . . . . . . . . . . . 18 |- (m = k -> (f:m-onto->x <-> f:k-onto->x))
29	28	exbidv 1657	. . . . . . . . . . . . . . . . 17 |- (m = k -> (E.f f:m-onto->x <-> E.f f:k-onto->x))
30		breq2 3342	. . . . . . . . . . . . . . . . 17 |- (m = k -> (x ~<_ m <-> x ~<_ k))
31	29, 30	imbi12d 688	. . . . . . . . . . . . . . . 16 |- (m = k -> ((E.f f:m-onto->x -> x ~<_ m) <-> (E.f f:k-onto->x -> x ~<_ k)))
32	31	albidv 1656	. . . . . . . . . . . . . . 15 |- (m = k -> (A.x(E.f f:m-onto->x -> x ~<_ m) <-> A.x(E.f f:k-onto->x -> x ~<_ k)))
33		foeq2 4614	. . . . . . . . . . . . . . . . . 18 |- (m = suc k -> (f:m-onto->x <-> f:suc k-onto->x))
34	33	exbidv 1657	. . . . . . . . . . . . . . . . 17 |- (m = suc k -> (E.f f:m-onto->x <-> E.f f:suc k-onto->x))
35		breq2 3342	. . . . . . . . . . . . . . . . 17 |- (m = suc k -> (x ~<_ m <-> x ~<_ suc k))
36	34, 35	imbi12d 688	. . . . . . . . . . . . . . . 16 |- (m = suc k -> ((E.f f:m-onto->x -> x ~<_ m) <-> (E.f f:suc k-onto->x -> x ~<_ suc k)))
37	36	albidv 1656	. . . . . . . . . . . . . . 15 |- (m = suc k -> (A.x(E.f f:m-onto->x -> x ~<_ m) <-> A.x(E.f f:suc k-onto->x -> x ~<_ suc k)))
38		fo00 4669	. . . . . . . . . . . . . . . . . . 19 |- (f:(/)-onto->x <-> (f = (/) /\ x = (/)))
39	38	simprbi 353	. . . . . . . . . . . . . . . . . 18 |- (f:(/)-onto->x -> x = (/))
40		0dom 5527	. . . . . . . . . . . . . . . . . 18 |- (/) ~<_ (/)
41	39, 40	syl6eqbr 3374	. . . . . . . . . . . . . . . . 17 |- (f:(/)-onto->x -> x ~<_ (/))
42	41	19.23aiv 1674	. . . . . . . . . . . . . . . 16 |- (E.f f:(/)-onto->x -> x ~<_ (/))
43	42	ax-gen 1305	. . . . . . . . . . . . . . 15 |- A.x(E.f f:(/)-onto->x -> x ~<_ (/))
44		fnsnfv 4728	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((f Fn suc k /\ k e. suc k) -> {(f` k)} = (f"{k}))
45		fofn 4619	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (f:suc k-onto->x -> f Fn suc k)
46		visset 2295	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- k e. _V
47	46	sucid 3744	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- k e. suc k
48	44, 45, 47	sylancl 525	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (f:suc k-onto->x -> {(f` k)} = (f"{k}))
49	48	uneq2d 2755	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (f:suc k-onto->x -> ((f"k) u. {(f` k)}) = ((f"k) u. (f"{k})))
50		foima 4622	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (f:suc k-onto->x -> (f"suc k) = x)
51		df-suc 3663	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- suc k = (k u. {k})
52	51	imaeq2i 4262	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (f"suc k) = (f"(k u. {k}))
53		imaundi 4328	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (f"(k u. {k})) = ((f"k) u. (f"{k}))
54	52, 53	eqtr2i 1909	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((f"k) u. (f"{k})) = (f"suc k)
55	50, 54	syl5eq 1940	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (f:suc k-onto->x -> ((f"k) u. (f"{k})) = x)
56	49, 55	eqtrd 1925	. . . . . . . . . . . . . . . . . . . . . . 23 |- (f:suc k-onto->x -> ((f"k) u. {(f` k)}) = x)
57	56	adantl 424	. . . . . . . . . . . . . . . . . . . . . 22 |- (((k e. om /\ A.y(E.g g:k-onto->y -> y ~<_ k)) /\ f:suc k-onto->x) -> ((f"k) u. {(f` k)}) = x)
58		visset 2295	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- f e. _V
59		imaexg 4279	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (f e. _V -> (f"k) e. _V)
60	58, 59	ax-mp 7	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (f"k) e. _V
61		foeq3 4615	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (y = (f"k) -> (g:k-onto->y <-> g:k-onto->(f"k)))
62	61	exbidv 1657	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (y = (f"k) -> (E.g g:k-onto->y <-> E.g g:k-onto->(f"k)))
63		breq1 3341	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (y = (f"k) -> (y ~<_ k <-> (f"k) ~<_ k))
64	62, 63	imbi12d 688	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (y = (f"k) -> ((E.g g:k-onto->y -> y ~<_ k) <-> (E.g g:k-onto->(f"k) -> (f"k) ~<_ k)))
65	60, 64	cla4v 2370	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (A.y(E.g g:k-onto->y -> y ~<_ k) -> (E.g g:k-onto->(f"k) -> (f"k) ~<_ k))
66	65	imp 377	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((A.y(E.g g:k-onto->y -> y ~<_ k) /\ E.g g:k-onto->(f"k)) -> (f"k) ~<_ k)
67		fofun 4618	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (f:suc k-onto->x -> Fun f)
68		fof 4617	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (f:suc k-onto->x -> f:suc k-->x)
69		sssucid 3742	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- k C_ suc k
70		fdm 4567	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (f:suc k-->x -> dom f = suc k)
71	70	sseq2d 2645	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (f:suc k-->x -> (k C_ dom f <-> k C_ suc k))
72	69, 71	mpbiri 211	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (f:suc k-->x -> k C_ dom f)
73	68, 72	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (f:suc k-onto->x -> k C_ dom f)
74		fores 4627	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((Fun f /\ k C_ dom f) -> (f |` k):k-onto->(f"k))
75	67, 73, 74	syl11anc 524	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (f:suc k-onto->x -> (f |` k):k-onto->(f"k))
76		resexg 4250	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (f e. _V -> (f |` k) e. _V)
77	58, 76	ax-mp 7	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (f |` k) e. _V
78		foeq1 4613	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (g = (f |` k) -> (g:k-onto->(f"k) <-> (f |` k):k-onto->(f"k)))
79	77, 78	cla4ev 2371	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((f |` k):k-onto->(f"k) -> E.g g:k-onto->(f"k))
80	75, 79	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (f:suc k-onto->x -> E.g g:k-onto->(f"k))
81	66, 80	sylan2 500	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((A.y(E.g g:k-onto->y -> y ~<_ k) /\ f:suc k-onto->x) -> (f"k) ~<_ k)
82	81	adantll 428	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((k e. om /\ A.y(E.g g:k-onto->y -> y ~<_ k)) /\ f:suc k-onto->x) -> (f"k) ~<_ k)
83		fvex 4689	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (f` k) e. _V
84		en2sn 5490	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (((f` k) e. _V /\ k e. _V) -> {(f` k)} ~~ {k})
85	83, 46, 84	mp2an 761	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- {(f` k)} ~~ {k}
86		endom 5444	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ({(f` k)} ~~ {k} -> {(f` k)} ~<_ {k})
87	85, 86	ax-mp 7	. . . . . . . . . . . . . . . . . . . . . . . 24 |- {(f` k)} ~<_ {k}
88	82, 87	jctir 317	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((k e. om /\ A.y(E.g g:k-onto->y -> y ~<_ k)) /\ f:suc k-onto->x) -> ((f"k) ~<_ k /\ {(f` k)} ~<_ {k}))
89		nnord 3959	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (k e. om -> Ord k)
90		orddisj 3701	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (Ord k -> (k i^i {k}) = (/))
91	89, 90	syl 12	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (k e. om -> (k i^i {k}) = (/))
92	91	ad2antrr 440	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((k e. om /\ A.y(E.g g:k-onto->y -> y ~<_ k)) /\ f:suc k-onto->x) -> (k i^i {k}) = (/))
93		snex 3492	. . . . . . . . . . . . . . . . . . . . . . . 24 |- {(f` k)} e. _V
94		snex 3492	. . . . . . . . . . . . . . . . . . . . . . . 24 |- {k} e. _V
95	46, 93, 94	undom 5497	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((((f"k) ~<_ k /\ {(f` k)} ~<_ {k}) /\ (k i^i {k}) = (/)) -> ((f"k) u. {(f` k)}) ~<_ (k u. {k}))
96	88, 92, 95	syl11anc 524	. . . . . . . . . . . . . . . . . . . . . 22 |- (((k e. om /\ A.y(E.g g:k-onto->y -> y ~<_ k)) /\ f:suc k-onto->x) -> ((f"k) u. {(f` k)}) ~<_ (k u. {k}))
97	57, 96	eqbrtrrd 3359	. . . . . . . . . . . . . . . . . . . . 21 |- (((k e. om /\ A.y(E.g g:k-onto->y -> y ~<_ k)) /\ f:suc k-onto->x) -> x ~<_ (k u. {k}))
98	97, 51	syl6breqr 3377	. . . . . . . . . . . . . . . . . . . 20 |- (((k e. om /\ A.y(E.g g:k-onto->y -> y ~<_ k)) /\ f:suc k-onto->x) -> x ~<_ suc k)
99	98	ex 402	. . . . . . . . . . . . . . . . . . 19 |- ((k e. om /\ A.y(E.g g:k-onto->y -> y ~<_ k)) -> (f:suc k-onto->x -> x ~<_ suc k))
100	99	19.23adv 1584	. . . . . . . . . . . . . . . . . 18 |- ((k e. om /\ A.y(E.g g:k-onto->y -> y ~<_ k)) -> (E.f f:suc k-onto->x -> x ~<_ suc k))
101	100	ex 402	. . . . . . . . . . . . . . . . 17 |- (k e. om -> (A.y(E.g g:k-onto->y -> y ~<_ k) -> (E.f f:suc k-onto->x -> x ~<_ suc k)))
102	101	19.21adv 1666	. . . . . . . . . . . . . . . 16 |- (k e. om -> (A.y(E.g g:k-onto->y -> y ~<_ k) -> A.x(E.f f:suc k-onto->x -> x ~<_ suc k)))
103		foeq3 4615	. . . . . . . . . . . . . . . . . . . 20 |- (x = y -> (f:k-onto->x <-> f:k-onto->y))
104	103	exbidv 1657	. . . . . . . . . . . . . . . . . . 19 |- (x = y -> (E.f f:k-onto->x <-> E.f f:k-onto->y))
105		foeq1 4613	. . . . . . . . . . . . . . . . . . . 20 |- (f = g -> (f:k-onto->y <-> g:k-onto->y))
106	105	cbvexv 1697	. . . . . . . . . . . . . . . . . . 19 |- (E.f f:k-onto->y <-> E.g g:k-onto->y)
107	104, 106	syl6bb 595	. . . . . . . . . . . . . . . . . 18 |- (x = y -> (E.f f:k-onto->x <-> E.g g:k-onto->y))
108		breq1 3341	. . . . . . . . . . . . . . . . . 18 |- (x = y -> (x ~<_ k <-> y ~<_ k))
109	107, 108	imbi12d 688	. . . . . . . . . . . . . . . . 17 |- (x = y -> ((E.f f:k-onto->x -> x ~<_ k) <-> (E.g g:k-onto->y -> y ~<_ k)))
110	109	cbvalv 1696	. . . . . . . . . . . . . . . 16 |- (A.x(E.f f:k-onto->x -> x ~<_ k) <-> A.y(E.g g:k-onto->y -> y ~<_ k))
111	102, 110	syl5ib 223	. . . . . . . . . . . . . . 15 |- (k e. om -> (A.x(E.f f:k-onto->x -> x ~<_ k) -> A.x(E.f f:suc k-onto->x -> x ~<_ suc k)))
112	27, 32, 37, 43, 111	finds1 3982	. . . . . . . . . . . . . 14 |- (m e. om -> A.x(E.f f:m-onto->x -> x ~<_ m))
113	22, 112	syl5 20	. . . . . . . . . . . . 13 |- (B e. _V -> (m e. om -> (E.f f:m-onto->B -> B ~<_ m)))
114	17, 113	syl 12	. . . . . . . . . . . 12 |- (E.f f:m-onto->B -> (m e. om -> (E.f f:m-onto->B -> B ~<_ m)))
115	114	pm2.43b 81	. . . . . . . . . . 11 |- (m e. om -> (E.f f:m-onto->B -> B ~<_ m))
116	13, 115	sylan9 517	. . . . . . . . . 10 |- ((F e. _V /\ m e. om) -> ((F o. g):m-onto->B -> B ~<_ m))
117	116	19.23adv 1584	. . . . . . . . 9 |- ((F e. _V /\ m e. om) -> (E.g(F o. g):m-onto->B -> B ~<_ m))
118		19.42v 1688	. . . . . . . . . . . 12 |- (E.g(F:A-onto->B /\ g:m-onto->A) <-> (F:A-onto->B /\ E.g g:m-onto->A))
119		foco 4628	. . . . . . . . . . . . 13 |- ((F:A-onto->B /\ g:m-onto->A) -> (F o. g):m-onto->B)
120	119	eximi 1387	. . . . . . . . . . . 12 |- (E.g(F:A-onto->B /\ g:m-onto->A) -> E.g(F o. g):m-onto->B)
121	118, 120	sylbir 218	. . . . . . . . . . 11 |- ((F:A-onto->B /\ E.g g:m-onto->A) -> E.g(F o. g):m-onto->B)
122	14	bren 5436	. . . . . . . . . . . 12 |- (A ~~ m <-> E.f f:A-1-1-onto->m)
123		f1ocnv 4651	. . . . . . . . . . . . . 14 |- (f:A-1-1-onto->m -> `'f:m-1-1-onto->A)
124		f1ofo 4643	. . . . . . . . . . . . . 14 |- (`'f:m-1-1-onto->A -> `'f:m-onto->A)
125	58	cnvex 4425	. . . . . . . . . . . . . . 15 |- `'f e. _V
126		foeq1 4613	. . . . . . . . . . . . . . 15 |- (g = `'f -> (g:m-onto->A <-> `'f:m-onto->A))
127	125, 126	cla4ev 2371	. . . . . . . . . . . . . 14 |- (`'f:m-onto->A -> E.g g:m-onto->A)
128	123, 124, 127	3syl 24	. . . . . . . . . . . . 13 |- (f:A-1-1-onto->m -> E.g g:m-onto->A)
129	128	19.23aiv 1674	. . . . . . . . . . . 12 |- (E.f f:A-1-1-onto->m -> E.g g:m-onto->A)
130	122, 129	sylbi 216	. . . . . . . . . . 11 |- (A ~~ m -> E.g g:m-onto->A)
131	121, 130	sylan2 500	. . . . . . . . . 10 |- ((F:A-onto->B /\ A ~~ m) -> E.g(F o. g):m-onto->B)
132	131	ancoms 484	. . . . . . . . 9 |- ((A ~~ m /\ F:A-onto->B) -> E.g(F o. g):m-onto->B)
133	117, 132	syl5 20	. . . . . . . 8 |- ((F e. _V /\ m e. om) -> ((A ~~ m /\ F:A-onto->B) -> B ~<_ m))
134	133	impr 422	. . . . . . 7 |- ((F e. _V /\ (m e. om /\ (A ~~ m /\ F:A-onto->B))) -> B ~<_ m)
135	7, 134	mpancom 769	. . . . . 6 |- ((m e. om /\ (A ~~ m /\ F:A-onto->B)) -> B ~<_ m)
136	14	ensym 5471	. . . . . . 7 |- (A ~~ m -> m ~~ A)
137	136	ad2antrl 442	. . . . . 6 |- ((m e. om /\ (A ~~ m /\ F:A-onto->B)) -> m ~~ A)
138		domentr 5480	. . . . . 6 |- ((B ~<_ m /\ m ~~ A) -> B ~<_ A)
139	135, 137, 138	syl11anc 524	. . . . 5 |- ((m e. om /\ (A ~~ m /\ F:A-onto->B)) -> B ~<_ A)
140	139	exp32 408	. . . 4 |- (m e. om -> (A ~~ m -> (F:A-onto->B -> B ~<_ A)))
141	140	r19.23aiv 2211	. . 3 |- (E.m e. om A ~~ m -> (F:A-onto->B -> B ~<_ A))
142	141	imp 377	. 2 |- ((E.m e. om A ~~ m /\ F:A-onto->B) -> B ~<_ A)
143		isfi 5441	. 2 |- (A e. Fin <-> E.m e. om A ~~ m)
144	142, 143	sylanb 498	1 |- ((A e. Fin /\ F:A-onto->B) -> B ~<_ A)

Syntax hints:   -> wi 3   /\ wa 240  A.wal 1296   = wceq 1298   e. wcel 1300  E.wex 1326  E.wrex 2106  _Vcvv 2292   u. cun 2591   i^i cin 2592   C_ wss 2593  (/)c0 2875  {csn 3044   class class class wbr 3338  Ord word 3656  suc csuc 3659  omcom 3949  `'ccnv 3985  dom cdm 3986   |` cres 3988  "cima 3989   o. ccom 3990  Fun wfun 3992   Fn wfn 3993  -->wf 3994  -onto->wfo 3996  -1-1-onto->wf1o 3997  ` cfv 3998   ~~ cen 5423   ~<_ cdom 5424  Fincfn 5426

This theorem is referenced by:  fodomfib 5657  fofi 5658  iunfi 5659  pwfilem 5660  cncomp 10331  compsublem 15430  compsub 15431  hscptsscld 15434  alexsub 15441  comppfsc 15517

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-rep 3428  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3or 859  df-3an 860  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-ral 2109  df-rex 2110  df-rab 2112  df-v 2294  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-pss 2607  df-nul 2876  df-if 2983  df-pw 3035  df-sn 3049  df-pr 3050  df-tp 3052  df-op 3053  df-uni 3178  df-br 3339  df-opab 3396  df-tr 3412  df-eprel 3583  df-id 3586  df-po 3591  df-so 3604  df-fr 3625  df-we 3644  df-ord 3660  df-on 3661  df-lim 3662  df-suc 3663  df-om 3950  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fun 4008  df-fn 4009  df-f 4010  df-f1 4011  df-fo 4012  df-f1o 4013  df-fv 4014  df-1o 5177  df-er 5318  df-en 5427  df-dom 5428  df-fin 5430

Copyright terms: Public domain