Theorem fodomfi 4650

Description: An onto function implies dominance of domain over range, for finite sets. Unlike fodom 4884 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		domentr 4508	. . . . . 6 |- ((B ~<_ m /\ m ~~ A) -> B ~<_ A)
2		fex 3727	. . . . . . . . . 10 |- ((F:A-->B /\ A e. V) -> F e. V)
3	2	ancoms 438	. . . . . . . . 9 |- ((A e. V /\ F:A-->B) -> F e. V)
4		relen 4459	. . . . . . . . . 10 |- Rel ~~
5	4	brrelexi 3265	. . . . . . . . 9 |- (A ~~ m -> A e. V)
6		fof 3747	. . . . . . . . 9 |- (F:A-onto->B -> F:A-->B)
7	3, 5, 6	syl2an 456	. . . . . . . 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 1851	. . . . . . . . . . . . . 14 |- g e. V
10		coexg 3599	. . . . . . . . . . . . . 14 |- ((F e. V /\ g e. V) -> (F o. g) e. V)
11	9, 10	mpan2 699	. . . . . . . . . . . . 13 |- (F e. V -> (F o. g) e. V)
12		foeq1 3743	. . . . . . . . . . . . . 14 |- (f = (F o. g) -> (f:m-onto->B <-> (F o. g):m-onto->B))
13	12	cla4egv 1901	. . . . . . . . . . . . 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 1851	. . . . . . . . . . . . . . . 16 |- m e. V
16		fornex 3755	. . . . . . . . . . . . . . . 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 1328	. . . . . . . . . . . . . 14 |- (E.f f:m-onto->B -> B e. V)
19		foeq3 3745	. . . . . . . . . . . . . . . . . 18 |- (x = B -> (f:m-onto->x <-> f:m-onto->B))
20	19	exbidv 1312	. . . . . . . . . . . . . . . . 17 |- (x = B -> (E.f f:m-onto->x <-> E.f f:m-onto->B))
21		breq1 2672	. . . . . . . . . . . . . . . . 17 |- (x = B -> (x ~<_ m <-> B ~<_ m))
22	20, 21	imbi12d 628	. . . . . . . . . . . . . . . 16 |- (x = B -> ((E.f f:m-onto->x -> x ~<_ m) <-> (E.f f:m-onto->B -> B ~<_ m)))
23	22	cla4gv 1900	. . . . . . . . . . . . . . 15 |- (B e. V -> (A.x(E.f f:m-onto->x -> x ~<_ m) -> (E.f f:m-onto->B -> B ~<_ m)))
24		foeq2 3744	. . . . . . . . . . . . . . . . . . 19 |- (m = (/) -> (f:m-onto->x <-> f:(/)-onto->x))
25	24	exbidv 1312	. . . . . . . . . . . . . . . . . 18 |- (m = (/) -> (E.f f:m-onto->x <-> E.f f:(/)-onto->x))
26		breq2 2673	. . . . . . . . . . . . . . . . . 18 |- (m = (/) -> (x ~<_ m <-> x ~<_ (/)))
27	25, 26	imbi12d 628	. . . . . . . . . . . . . . . . 17 |- (m = (/) -> ((E.f f:m-onto->x -> x ~<_ m) <-> (E.f f:(/)-onto->x -> x ~<_ (/))))
28	27	albidv 1311	. . . . . . . . . . . . . . . 16 |- (m = (/) -> (A.x(E.f f:m-onto->x -> x ~<_ m) <-> A.x(E.f f:(/)-onto->x -> x ~<_ (/))))
29		foeq2 3744	. . . . . . . . . . . . . . . . . . 19 |- (m = k -> (f:m-onto->x <-> f:k-onto->x))
30	29	exbidv 1312	. . . . . . . . . . . . . . . . . 18 |- (m = k -> (E.f f:m-onto->x <-> E.f f:k-onto->x))
31		breq2 2673	. . . . . . . . . . . . . . . . . 18 |- (m = k -> (x ~<_ m <-> x ~<_ k))
32	30, 31	imbi12d 628	. . . . . . . . . . . . . . . . 17 |- (m = k -> ((E.f f:m-onto->x -> x ~<_ m) <-> (E.f f:k-onto->x -> x ~<_ k)))
33	32	albidv 1311	. . . . . . . . . . . . . . . 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 3744	. . . . . . . . . . . . . . . . . . 19 |- (m = suc k -> (f:m-onto->x <-> f:suc k-onto->x))
35	34	exbidv 1312	. . . . . . . . . . . . . . . . . 18 |- (m = suc k -> (E.f f:m-onto->x <-> E.f f:suc k-onto->x))
36		breq2 2673	. . . . . . . . . . . . . . . . . 18 |- (m = suc k -> (x ~<_ m <-> x ~<_ suc k))
37	35, 36	imbi12d 628	. . . . . . . . . . . . . . . . 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 1311	. . . . . . . . . . . . . . . 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 3791	. . . . . . . . . . . . . . . . . . . 20 |- (f:(/)-onto->x <-> (f = (/) /\ x = (/)))
40	39	pm3.27bi 324	. . . . . . . . . . . . . . . . . . 19 |- (f:(/)-onto->x -> x = (/))
41		0dom 4551	. . . . . . . . . . . . . . . . . . 19 |- (/) ~<_ (/)
42	40, 41	syl6eqbr 2702	. . . . . . . . . . . . . . . . . 18 |- (f:(/)-onto->x -> x ~<_ (/))
43	42	19.23aiv 1328	. . . . . . . . . . . . . . . . 17 |- (E.f f:(/)-onto->x -> x ~<_ (/))
44	43	ax-gen 995	. . . . . . . . . . . . . . . 16 |- A.x(E.f f:(/)-onto->x -> x ~<_ (/))
45		fofn 3749	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (f:suc k-onto->x -> f Fn suc k)
46		visset 1851	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- k e. V
47	46	sucid 3106	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- k e. suc k
48		fnsnfv 3843	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((f Fn suc k /\ k e. suc k) -> {(f` k)} = (f"{k}))
49	47, 48	mpan2 699	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (f Fn suc k -> {(f` k)} = (f"{k}))
50	45, 49	syl 10	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (f:suc k-onto->x -> {(f` k)} = (f"{k}))
51	50	uneq2d 2228	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (f:suc k-onto->x -> ((f"k) u. {(f` k)}) = ((f"k) u. (f"{k})))
52		foima 3752	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (f:suc k-onto->x -> (f"suc k) = x)
53		df-suc 3009	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- suc k = (k u. {k})
54	53	imaeq2i 3465	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (f"suc k) = (f"(k u. {k}))
55		imaundi 3516	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (f"(k u. {k})) = ((f"k) u. (f"{k}))
56	54, 55	eqtr2i 1533	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((f"k) u. (f"{k})) = (f"suc k)
57	52, 56	syl5eq 1556	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (f:suc k-onto->x -> ((f"k) u. (f"{k})) = x)
58	51, 57	eqtrd 1544	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (f:suc k-onto->x -> ((f"k) u. {(f` k)}) = x)
59	58	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)
60		snex 2802	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- {(f` k)} e. V
61		snex 2802	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- {k} e. V
62	46, 60, 61	undom 4525	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((((f"k) ~<_ k /\ {(f` k)} ~<_ {k}) /\ (k i^i {k}) = (/)) -> ((f"k) u. {(f` k)}) ~<_ (k u. {k}))
63		visset 1851	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- f e. V
64		imaexg 3479	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (f e. V -> (f"k) e. V)
65	63, 64	ax-mp 7	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (f"k) e. V
66		foeq3 3745	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (y = (f"k) -> (g:k-onto->y <-> g:k-onto->(f"k)))
67	66	exbidv 1312	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (y = (f"k) -> (E.g g:k-onto->y <-> E.g g:k-onto->(f"k)))
68		breq1 2672	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (y = (f"k) -> (y ~<_ k <-> (f"k) ~<_ k))
69	67, 68	imbi12d 628	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (y = (f"k) -> ((E.g g:k-onto->y -> y ~<_ k) <-> (E.g g:k-onto->(f"k) -> (f"k) ~<_ k)))
70	65, 69	cla4v 1906	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (A.y(E.g g:k-onto->y -> y ~<_ k) -> (E.g g:k-onto->(f"k) -> (f"k) ~<_ k))
71	70	imp 348	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((A.y(E.g g:k-onto->y -> y ~<_ k) /\ E.g g:k-onto->(f"k)) -> (f"k) ~<_ k)
72		fores 3757	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((Fun f /\ k (_ dom f) -> (f |` k):k-onto->(f"k))
73		fofun 3748	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (f:suc k-onto->x -> Fun f)
74		fof 3747	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (f:suc k-onto->x -> f:suc k-->x)
75		sssucid 3102	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- k (_ suc k
76		fdm 3706	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (f:suc k-->x -> dom f = suc k)
77	76	sseq2d 2133	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (f:suc k-->x -> (k (_ dom f <-> k (_ suc k))
78	75, 77	mpbiri 192	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (f:suc k-->x -> k (_ dom f)
79	74, 78	syl 10	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (f:suc k-onto->x -> k (_ dom f)
80	72, 73, 79	sylanc 473	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (f:suc k-onto->x -> (f |` k):k-onto->(f"k))
81		resexg 3455	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (f e. V -> (f |` k) e. V)
82	63, 81	ax-mp 7	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (f |` k) e. V
83		foeq1 3743	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (g = (f |` k) -> (g:k-onto->(f"k) <-> (f |` k):k-onto->(f"k)))
84	82, 83	cla4ev 1907	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((f |` k):k-onto->(f"k) -> E.g g:k-onto->(f"k))