Theorem fodomfi 4540

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

Assertion

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

Distinct variable group:   A,n

Proof of Theorem fodomfi

Step	Hyp	Ref	Expression
1		domentr 4402	. . . . . 6 |- ((B ~<_ m /\ m ~~ A) -> B ~<_ A)
2		fex 3637	. . . . . . . . . 10 |- ((F:A-->B /\ A e. V) -> F e. V)
3	2	ancoms 436	. . . . . . . . 9 |- ((A e. V /\ F:A-->B) -> F e. V)
4		relen 4354	. . . . . . . . . 10 |- Rel ~~
5	4	brrelexi 3198	. . . . . . . . 9 |- (A ~~ m -> A e. V)
6		fof 3657	. . . . . . . . 9 |- (F:A-onto->B -> F:A-->B)
7	3, 5, 6	syl2an 454	. . . . . . . 8 |- ((A ~~ m /\ F:A-onto->B) -> F e. V)
8	7	adantl 388	. . . . . . 7 |- ((m e. om /\ (A ~~ m /\ F:A-onto->B)) -> F e. V)
9		visset 1804	. . . . . . . . . . . . . 14 |- g e. V
10		coexg 3510	. . . . . . . . . . . . . 14 |- ((F e. V /\ g e. V) -> (F o. g) e. V)
11	9, 10	mpan2 694	. . . . . . . . . . . . 13 |- (F e. V -> (F o. g) e. V)
12		foeq1 3653	. . . . . . . . . . . . . 14 |- (f = (F o. g) -> (f:m-onto->B <-> (F o. g):m-onto->B))
13	12	cla4egv 1854	. . . . . . . . . . . . 13 |- ((F o. g) e. V -> ((F o. g):m-onto->B -> E.f f:m-onto->B))
14	11, 13	syl 10	. . . . . . . . . . . 12 |- (F e. V -> ((F o. g):m-onto->B -> E.f f:m-onto->B))
15		visset 1804	. . . . . . . . . . . . . . . 16 |- m e. V
16		fornex 3664	. . . . . . . . . . . . . . . 16 |- (m e. V -> (f:m-onto->B -> B e. V))
17	15, 16	ax-mp 7	. . . . . . . . . . . . . . 15 |- (f:m-onto->B -> B e. V)
18	17	19.23aiv 1290	. . . . . . . . . . . . . 14 |- (E.f f:m-onto->B -> B e. V)
19		foeq3 3655	. . . . . . . . . . . . . . . . . 18 |- (x = B -> (f:m-onto->x <-> f:m-onto->B))
20	19	exbidv 1274	. . . . . . . . . . . . . . . . 17 |- (x = B -> (E.f f:m-onto->x <-> E.f f:m-onto->B))
21		breq1 2612	. . . . . . . . . . . . . . . . 17 |- (x = B -> (x ~<_ m <-> B ~<_ m))
22	20, 21	imbi12d 624	. . . . . . . . . . . . . . . 16 |- (x = B -> ((E.f f:m-onto->x -> x ~<_ m) <-> (E.f f:m-onto->B -> B ~<_ m)))
23	22	cla4gv 1853	. . . . . . . . . . . . . . 15 |- (B e. V -> (A.x(E.f f:m-onto->x -> x ~<_ m) -> (E.f f:m-onto->B -> B ~<_ m)))
24		foeq2 3654	. . . . . . . . . . . . . . . . . . 19 |- (m = (/) -> (f:m-onto->x <-> f:(/)-onto->x))
25	24	exbidv 1274	. . . . . . . . . . . . . . . . . 18 |- (m = (/) -> (E.f f:m-onto->x <-> E.f f:(/)-onto->x))
26		breq2 2613	. . . . . . . . . . . . . . . . . 18 |- (m = (/) -> (x ~<_ m <-> x ~<_ (/)))
27	25, 26	imbi12d 624	. . . . . . . . . . . . . . . . 17 |- (m = (/) -> ((E.f f:m-onto->x -> x ~<_ m) <-> (E.f f:(/)-onto->x -> x ~<_ (/))))
28	27	albidv 1273	. . . . . . . . . . . . . . . 16 |- (m = (/) -> (A.x(E.f f:m-onto->x -> x ~<_ m) <-> A.x(E.f f:(/)-onto->x -> x ~<_ (/))))
29		foeq2 3654	. . . . . . . . . . . . . . . . . . 19 |- (m = k -> (f:m-onto->x <-> f:k-onto->x))
30	29	exbidv 1274	. . . . . . . . . . . . . . . . . 18 |- (m = k -> (E.f f:m-onto->x <-> E.f f:k-onto->x))
31		breq2 2613	. . . . . . . . . . . . . . . . . 18 |- (m = k -> (x ~<_ m <-> x ~<_ k))
32	30, 31	imbi12d 624	. . . . . . . . . . . . . . . . 17 |- (m = k -> ((E.f f:m-onto->x -> x ~<_ m) <-> (E.f f:k-onto->x -> x ~<_ k)))
33	32	albidv 1273	. . . . . . . . . . . . . . . 16 |- (m = k -> (A.x(E.f f:m-onto->x -> x ~<_ m) <-> A.x(E.f f:k-onto->x -> x ~<_ k)))
34		foeq2 3654	. . . . . . . . . . . . . . . . . . 19 |- (m = suc k -> (f:m-onto->x <-> f:suc k-onto->x))
35	34	exbidv 1274	. . . . . . . . . . . . . . . . . 18 |- (m = suc k -> (E.f f:m-onto->x <-> E.f f:suc k-onto->x))
36		breq2 2613	. . . . . . . . . . . . . . . . . 18 |- (m = suc k -> (x ~<_ m <-> x ~<_ suc k))
37	35, 36	imbi12d 624	. . . . . . . . . . . . . . . . 17 |- (m = suc k -> ((E.f f:m-onto->x -> x ~<_ m) <-> (E.f f:suc k-onto->x -> x ~<_ suc k)))
38	37	albidv 1273	. . . . . . . . . . . . . . . 16 |- (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)))
39		fo00 3700	. . . . . . . . . . . . . . . . . . . 20 |- (f:(/)-onto->x <-> (f = (/) /\ x = (/)))
40	39	pm3.27bi 326	. . . . . . . . . . . . . . . . . . 19 |- (f:(/)-onto->x -> x = (/))
41		0dom 4444	. . . . . . . . . . . . . . . . . . 19 |- (/) ~<_ (/)
42	40, 41	syl6eqbr 2642	. . . . . . . . . . . . . . . . . 18 |- (f:(/)-onto->x -> x ~<_ (/))
43	42	19.23aiv 1290	. . . . . . . . . . . . . . . . 17 |- (E.f f:(/)-onto->x -> x ~<_ (/))
44	43	ax-gen 960	. . . . . . . . . . . . . . . 16 |- A.x(E.f f:(/)-onto->x -> x ~<_ (/))
45		fof 3657	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (f:suc k-onto->x -> f:suc k-->x)
46		ffn 3613	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (f:suc k-->x -> f Fn suc k)
47		visset 1804	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- k e. V
48	47	sucid 3041	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- k e. suc k
49		fnsnfv 3752	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((f Fn suc k /\ k e. suc k) -> {(f` k)} = (f"{k}))
50	48, 49	mpan2 694	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (f Fn suc k -> {(f` k)} = (f"{k}))
51	45, 46, 50	3syl 20	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (f:suc k-onto->x -> {(f` k)} = (f"{k}))
52	51	uneq2d 2174	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (f:suc k-onto->x -> ((f"k) u. {(f` k)}) = ((f"k) u. (f"{k})))
53		foima 3661	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (f:suc k-onto->x -> (f"suc k) = x)
54		df-suc 2944	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- suc k = (k u. {k})
55		imaeq2 3386	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (suc k = (k u. {k}) -> (f"suc k) = (f"(k u. {k})))
56	54, 55	ax-mp 7	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (f"suc k) = (f"(k u. {k}))
57		imaun 3446	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (f"(k u. {k})) = ((f"k) u. (f"{k}))
58	56, 57	eqtr2 1488	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((f"k) u. (f"{k})) = (f"suc k)
59	53, 58	syl5eq 1511	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (f:suc k-onto->x -> ((f"k) u. (f"{k})) = x)
60	52, 59	eqtrd 1499	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (f:suc k-onto->x -> ((f"k) u. {(f` k)}) = x)
61	60	adantl 388	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((k e. om /\ A.y(E.g g:k-onto->y -> y ~<_ k)) /\ f:suc k-onto->x) -> ((f"k) u. {(f` k)}) = x)
62		snex 2740	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- {(f` k)} e. V
63		snex 2740	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- {k} e. V
64	47, 62, 63	undom 4418	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((((f"k) ~<_ k /\ {(f` k)} ~<_ {k}) /\ (k i^i {k}) = (/)) -> ((f"k) u. {(f` k)}) ~<_ (k u. {k}))
65		visset 1804	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- f e. V
66		imaexg 3400	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (f e. V -> (f"k) e. V)
67	65, 66	ax-mp 7	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (f"k) e. V
68		foeq3 3655	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (y = (f"k) -> (g:k-onto->y <-> g:k-onto->(f"k)))
69	68	exbidv 1274	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (y = (f"k) -> (E.g g:k-onto->y <-> E.g g:k-onto->(f"k)))
70		breq1 2612	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (y = (f"k) -> (y ~<_ k <-> (f"k) ~<_ k))
71	69, 70	imbi12d 624	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (y = (f"k) -> ((E.g g:k-onto->y -> y ~<_ k) <-> (E.g g:k-onto->(f"k) -> (f"k) ~<_ k)))
72	67, 71	cla4v 1859	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (A.y(E.g g:k-onto->y -> y ~<_ k) -> (E.g g:k-onto->(f"k) -> (f"k) ~<_ k))
73	72	imp 350	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((A.y(E.g g:k-onto->y -> y ~<_ k) /\ E.g g:k-onto->(f"k)) -> (f"k) ~<_ k)
74		fores 3666	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((Fun f /\ k (_ dom f) -> (f |` k):k-onto->(f"k))
75		fofun 3658	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (f:suc k-onto->x -> Fun f)
76		sssucid 3037	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- k (_ suc k
77		fdm 3617	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (f:suc k-->x -> dom f = suc k)
78	77	sseq2d 2079	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (f:suc k-->x -> (k (_ dom f <-> k (_ suc k))
79	76, 78	mpbiri 194	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (f:suc k-->x -> k (_ dom f)
80	45, 79	syl 10	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (f:suc k-onto->x -> k (_ dom f)
81	74, 75, 80	sylanc 471	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (f:suc k-onto->x -> (f |` k):k-onto->(f"k))
82		resexg 3378	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (f e. V -> (f |` k) e. V)
83	65, 82	ax-mp 7	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (f |` k) e. V
84		foeq1 3653	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (g = (f |` k) -> (g:k-onto->(f"k) <-> (f |` k):