Theorem fodomfi 4492

Description: An onto function implies dominance of domain over range, for finite sets. Unlike fodom 4722 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 4356	. . . . . 6 |- ((B ~<_ m /\ m ~~ A) -> B ~<_ A)
2		fex 3591	. . . . . . . . . 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 4308	. . . . . . . . . 10 |- Rel ~~
5	4	brrelexi 3170	. . . . . . . . 9 |- (A ~~ m -> A e. V)
6		fof 3611	. . . . . . . . 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 1788	. . . . . . . . . . . . . 14 |- g e. V
10		coexg 3465	. . . . . . . . . . . . . 14 |- ((F e. V /\ g e. V) -> (F o. g) e. V)
11	9, 10	mpan2 693	. . . . . . . . . . . . 13 |- (F e. V -> (F o. g) e. V)
12		foeq1 3607	. . . . . . . . . . . . . 14 |- (f = (F o. g) -> (f:m-onto->B <-> (F o. g):m-onto->B))
13	12	cla4egv 1838	. . . . . . . . . . . . 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 1788	. . . . . . . . . . . . . . . 16 |- m e. V
16		fornex 3618	. . . . . . . . . . . . . . . 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 1277	. . . . . . . . . . . . . 14 |- (E.f f:m-onto->B -> B e. V)
19		foeq3 3609	. . . . . . . . . . . . . . . . . 18 |- (x = B -> (f:m-onto->x <-> f:m-onto->B))
20	19	exbidv 1261	. . . . . . . . . . . . . . . . 17 |- (x = B -> (E.f f:m-onto->x <-> E.f f:m-onto->B))
21		breq1 2590	. . . . . . . . . . . . . . . . 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 1837	. . . . . . . . . . . . . . 15 |- (B e. V -> (A.x(E.f f:m-onto->x -> x ~<_ m) -> (E.f f:m-onto->B -> B ~<_ m)))
24		foeq2 3608	. . . . . . . . . . . . . . . . . . 19 |- (m = (/) -> (f:m-onto->x <-> f:(/)-onto->x))
25	24	exbidv 1261	. . . . . . . . . . . . . . . . . 18 |- (m = (/) -> (E.f f:m-onto->x <-> E.f f:(/)-onto->x))
26		breq2 2591	. . . . . . . . . . . . . . . . . 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 1260	. . . . . . . . . . . . . . . 16 |- (m = (/) -> (A.x(E.f f:m-onto->x -> x ~<_ m) <-> A.x(E.f f:(/)-onto->x -> x ~<_ (/))))
29		foeq2 3608	. . . . . . . . . . . . . . . . . . 19 |- (m = k -> (f:m-onto->x <-> f:k-onto->x))
30	29	exbidv 1261	. . . . . . . . . . . . . . . . . 18 |- (m = k -> (E.f f:m-onto->x <-> E.f f:k-onto->x))
31		breq2 2591	. . . . . . . . . . . . . . . . . 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 1260	. . . . . . . . . . . . . . . 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 3608	. . . . . . . . . . . . . . . . . . 19 |- (m = suc k -> (f:m-onto->x <-> f:suc k-onto->x))
35	34	exbidv 1261	. . . . . . . . . . . . . . . . . 18 |- (m = suc k -> (E.f f:m-onto->x <-> E.f f:suc k-onto->x))
36		breq2 2591	. . . . . . . . . . . . . . . . . 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 1260	. . . . . . . . . . . . . . . 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 3654	. . . . . . . . . . . . . . . . . . . 20 |- (f:(/)-onto->x <-> (f = (/) /\ x = (/)))
40	39	pm3.27bi 326	. . . . . . . . . . . . . . . . . . 19 |- (f:(/)-onto->x -> x = (/))
41		0dom 4398	. . . . . . . . . . . . . . . . . . 19 |- (/) ~<_ (/)
42	40, 41	syl6eqbr 2620	. . . . . . . . . . . . . . . . . 18 |- (f:(/)-onto->x -> x ~<_ (/))
43	42	19.23aiv 1277	. . . . . . . . . . . . . . . . 17 |- (E.f f:(/)-onto->x -> x ~<_ (/))
44	43	ax-gen 955	. . . . . . . . . . . . . . . 16 |- A.x(E.f f:(/)-onto->x -> x ~<_ (/))
45		fof 3611	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (f:suc k-onto->x -> f:suc k-->x)
46		ffn 3567	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (f:suc k-->x -> f Fn suc k)
47		visset 1788	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- k e. V
48	47	sucid 3014	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- k e. suc k
49		fnsnfv 3706	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((f Fn suc k /\ k e. suc k) -> {(f` k)} = (f"{k}))
50	48, 49	mpan2 693	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 2155	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (f:suc k-onto->x -> ((f"k) u. {(f` k)}) = ((f"k) u. (f"{k})))
53		foima 3615	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (f:suc k-onto->x -> (f"suc k) = x)
54		df-suc 2917	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- suc k = (k u. {k})
55		imaeq2 3353	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3409	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (f"(k u. {k})) = ((f"k) u. (f"{k}))
58	56, 57	eqtr2 1472	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((f"k) u. (f"{k})) = (f"suc k)
59	53, 58	syl5eq 1495	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (f:suc k-onto->x -> ((f"k) u. (f"{k})) = x)
60	52, 59	eqtrd 1483	. . . . . . . . . . . . . . . . . . . . . . . 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 2718	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- {(f` k)} e. V
63		snex 2718	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- {k} e. V
64	47, 62, 63	undom 4372	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((((f"k) ~<_ k /\ {(f` k)} ~<_ {k}) /\ (k i^i {k}) = (/)) -> ((f"k) u. {(f` k)}) ~<_ (k u. {k}))
65		visset 1788	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- f e. V
66		imaexg 3367	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (f e. V -> (f"k) e. V)
67	65, 66	ax-mp 7	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (f"k) e. V
68		foeq3 3609	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (y = (f"k) -> (g:k-onto->y <-> g:k-onto->(f"k)))
69	68	exbidv 1261	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (y = (f"k) -> (E.g g:k-onto->y <-> E.g g:k-onto->(f"k)))
70		breq1 2590	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1841	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3620	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((Fun f /\ k (_ dom f) -> (f |` k):k-onto->(f"k))
75		fofun 3612	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (f:suc k-onto->x -> Fun f)
76		sssucid 3010	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- k (_ suc k
77		fdm 3571	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (f:suc k-->x -> dom f = suc k)
78	77	sseq2d 2060	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3345	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (f e. V -> (f |` k) e. V)
83	65, 82	ax-mp 7	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (f |` k) e. V
84		foeq1 3607	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (g = (f |` k) -> (g:k-onto->(f"k) <-> (f