Theorem fodomfi 7590

Description: An onto function implies dominance of domain over range, for finite sets. Unlike fodom 8691 for arbitrary sets, this theorem does not require the Axiom of Choice for its proof. (Contributed by NM, 23-Mar-2006.) (Proof shortened by Mario Carneiro, 16-Nov-2014.)

Assertion

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

Proof of Theorem fodomfi

Dummy variables x y z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		foima 5625	. . 3 |- ( F : A -onto-> B -> ( F " A ) = B )
2	1	adantl 466	. 2 |- ( ( A e. Fin /\ F : A -onto-> B ) -> ( F " A ) = B )
3		fofn 5622	. . . 4 |- ( F : A -onto-> B -> F Fn A )
4		imaeq2 5165	. . . . . . . 8 |- ( x = (/) -> ( F " x ) = ( F " (/) ) )
5		ima0 5184	. . . . . . . 8 |- ( F " (/) ) = (/)
6	4, 5	syl6eq 2491	. . . . . . 7 |- ( x = (/) -> ( F " x ) = (/) )
7		id 22	. . . . . . 7 |- ( x = (/) -> x = (/) )
8	6, 7	breq12d 4305	. . . . . 6 |- ( x = (/) -> ( ( F " x ) ~<_ x <-> (/) ~<_ (/) ) )
9	8	imbi2d 316	. . . . 5 |- ( x = (/) -> ( ( F Fn A -> ( F " x ) ~<_ x ) <-> ( F Fn A -> (/) ~<_ (/) ) ) )
10		imaeq2 5165	. . . . . . 7 |- ( x = y -> ( F " x ) = ( F " y ) )
11		id 22	. . . . . . 7 |- ( x = y -> x = y )
12	10, 11	breq12d 4305	. . . . . 6 |- ( x = y -> ( ( F " x ) ~<_ x <-> ( F " y ) ~<_ y ) )
13	12	imbi2d 316	. . . . 5 |- ( x = y -> ( ( F Fn A -> ( F " x ) ~<_ x ) <-> ( F Fn A -> ( F " y ) ~<_ y ) ) )
14		imaeq2 5165	. . . . . . 7 |- ( x = ( y u. { z } ) -> ( F " x ) = ( F " ( y u. { z } ) ) )
15		id 22	. . . . . . 7 |- ( x = ( y u. { z } ) -> x = ( y u. { z } ) )
16	14, 15	breq12d 4305	. . . . . 6 |- ( x = ( y u. { z } ) -> ( ( F " x ) ~<_ x <-> ( F " ( y u. { z } ) ) ~<_ ( y u. { z } ) ) )
17	16	imbi2d 316	. . . . 5 |- ( x = ( y u. { z } ) -> ( ( F Fn A -> ( F " x ) ~<_ x ) <-> ( F Fn A -> ( F " ( y u. { z } ) ) ~<_ ( y u. { z } ) ) ) )
18		imaeq2 5165	. . . . . . 7 |- ( x = A -> ( F " x ) = ( F " A ) )
19		id 22	. . . . . . 7 |- ( x = A -> x = A )
20	18, 19	breq12d 4305	. . . . . 6 |- ( x = A -> ( ( F " x ) ~<_ x <-> ( F " A ) ~<_ A ) )
21	20	imbi2d 316	. . . . 5 |- ( x = A -> ( ( F Fn A -> ( F " x ) ~<_ x ) <-> ( F Fn A -> ( F " A ) ~<_ A ) ) )
22		0ex 4422	. . . . . . 7 |- (/) e. _V
23	22	0dom 7441	. . . . . 6 |- (/) ~<_ (/)
24	23	a1i 11	. . . . 5 |- ( F Fn A -> (/) ~<_ (/) )
25		fnfun 5508	. . . . . . . . . . . . . . 15 |- ( F Fn A -> Fun F )
26	25	ad2antrl 727	. . . . . . . . . . . . . 14 |- ( ( ( y e. Fin /\ -. z e. y ) /\ ( F Fn A /\ ( F " y ) ~<_ y ) ) -> Fun F )
27		funressn 5895	. . . . . . . . . . . . . 14 |- ( Fun F -> ( F |` { z } ) C_ { <. z , ( F ` z ) >. } )
28		rnss 5068	. . . . . . . . . . . . . 14 |- ( ( F |` { z } ) C_ { <. z , ( F ` z ) >. } -> ran ( F |` { z } ) C_ ran { <. z , ( F ` z ) >. } )
29	26, 27, 28	3syl 20	. . . . . . . . . . . . 13 |- ( ( ( y e. Fin /\ -. z e. y ) /\ ( F Fn A /\ ( F " y ) ~<_ y ) ) -> ran ( F |` { z } ) C_ ran { <. z , ( F ` z ) >. } )
30		df-ima 4853	. . . . . . . . . . . . 13 |- ( F " { z } ) = ran ( F |` { z } )
31		vex 2975	. . . . . . . . . . . . . . 15 |- z e. _V
32	31	rnsnop 5320	. . . . . . . . . . . . . 14 |- ran { <. z , ( F ` z ) >. } = { ( F ` z ) }
33	32	eqcomi 2447	. . . . . . . . . . . . 13 |- { ( F ` z ) } = ran { <. z , ( F ` z ) >. }
34	29, 30, 33	3sstr4g 3397	. . . . . . . . . . . 12 |- ( ( ( y e. Fin /\ -. z e. y ) /\ ( F Fn A /\ ( F " y ) ~<_ y ) ) -> ( F " { z } ) C_ { ( F ` z ) } )
35		snex 4533	. . . . . . . . . . . 12 |- { ( F ` z ) } e. _V
36		ssexg 4438	. . . . . . . . . . . 12 |- ( ( ( F " { z } ) C_ { ( F ` z ) } /\ { ( F ` z ) } e. _V ) -> ( F " { z } ) e. _V )
37	34, 35, 36	sylancl 662	. . . . . . . . . . 11 |- ( ( ( y e. Fin /\ -. z e. y ) /\ ( F Fn A /\ ( F " y ) ~<_ y ) ) -> ( F " { z } ) e. _V )
38		fvi 5748	. . . . . . . . . . 11 |- ( ( F " { z } ) e. _V -> ( _I ` ( F " { z } ) ) = ( F " { z } ) )
39	37, 38	syl 16	. . . . . . . . . 10 |- ( ( ( y e. Fin /\ -. z e. y ) /\ ( F Fn A /\ ( F " y ) ~<_ y ) ) -> ( _I ` ( F " { z } ) ) = ( F " { z } ) )
40	39	uneq2d 3510	. . . . . . . . 9 |- ( ( ( y e. Fin /\ -. z e. y ) /\ ( F Fn A /\ ( F " y ) ~<_ y ) ) -> ( ( F " y ) u. ( _I ` ( F " { z } ) ) ) = ( ( F " y ) u. ( F " { z } ) ) )
41		imaundi 5249	. . . . . . . . 9 |- ( F " ( y u. { z } ) ) = ( ( F " y ) u. ( F " { z } ) )
42	40, 41	syl6eqr 2493	. . . . . . . 8 |- ( ( ( y e. Fin /\ -. z e. y ) /\ ( F Fn A /\ ( F " y ) ~<_ y ) ) -> ( ( F " y ) u. ( _I ` ( F " { z } ) ) ) = ( F " ( y u. { z } ) ) )
43		simprr 756	. . . . . . . . 9 |- ( ( ( y e. Fin /\ -. z e. y ) /\ ( F Fn A /\ ( F " y ) ~<_ y ) ) -> ( F " y ) ~<_ y )
44		ssdomg 7355	. . . . . . . . . . . 12 |- ( { ( F ` z ) } e. _V -> ( ( F " { z } ) C_ { ( F ` z ) } -> ( F " { z } ) ~<_ { ( F ` z ) } ) )
45	35, 34, 44	mpsyl 63	. . . . . . . . . . 11 |- ( ( ( y e. Fin /\ -. z e. y ) /\ ( F Fn A /\ ( F " y ) ~<_ y ) ) -> ( F " { z } ) ~<_ { ( F ` z ) } )
46		fvex 5701	. . . . . . . . . . . . 13 |- ( F ` z ) e. _V
47	46	ensn1 7373	. . . . . . . . . . . 12 |- { ( F ` z ) } ~~ 1o
48	31	ensn1 7373	. . . . . . . . . . . 12 |- { z } ~~ 1o
49	47, 48	entr4i 7366	. . . . . . . . . . 11 |- { ( F ` z ) } ~~ { z }
50		domentr 7368	. . . . . . . . . . 11 |- ( ( ( F " { z } ) ~<_ { ( F ` z ) } /\ { ( F ` z ) } ~~ { z } ) -> ( F " { z } ) ~<_ { z } )
51	45, 49, 50	sylancl 662	. . . . . . . . . 10 |- ( ( ( y e. Fin /\ -. z e. y ) /\ ( F Fn A /\ ( F " y ) ~<_ y ) ) -> ( F " { z } ) ~<_ { z } )
52	39, 51	eqbrtrd 4312	. . . . . . . . 9 |- ( ( ( y e. Fin /\ -. z e. y ) /\ ( F Fn A /\ ( F " y ) ~<_ y ) ) -> ( _I ` ( F " { z } ) ) ~<_ { z } )
53		simplr 754	. . . . . . . . . 10 |- ( ( ( y e. Fin /\ -. z e. y ) /\ ( F Fn A /\ ( F " y ) ~<_ y ) ) -> -. z e. y )
54		disjsn 3936	. . . . . . . . . 10 |- ( ( y i^i { z } ) = (/) <-> -. z e. y )
55	53, 54	sylibr 212	. . . . . . . . 9 |- ( ( ( y e. Fin /\ -. z e. y ) /\ ( F Fn A /\ ( F " y ) ~<_ y ) ) -> ( y i^i { z } ) = (/) )
56		undom 7399	. . . . . . . . 9 |- ( ( ( ( F " y ) ~<_ y /\ ( _I ` ( F " { z } ) ) ~<_ { z } ) /\ ( y i^i { z } ) = (/) ) -> ( ( F " y ) u. ( _I ` ( F " { z } ) ) ) ~<_ ( y u. { z } ) )
57	43, 52, 55, 56	syl21anc 1217	. . . . . . . 8 |- ( ( ( y e. Fin /\ -. z e. y ) /\ ( F Fn A /\ ( F " y ) ~<_ y ) ) -> ( ( F " y ) u. ( _I ` ( F " { z } ) ) ) ~<_ ( y u. { z } ) )
58	42, 57	eqbrtrrd 4314	. . . . . . 7 |- ( ( ( y e. Fin /\ -. z e. y ) /\ ( F Fn A /\ ( F " y ) ~<_ y ) ) -> ( F " ( y u. { z } ) ) ~<_ ( y u. { z } ) )
59	58	exp32 605	. . . . . 6 |- ( ( y e. Fin /\ -. z e. y ) -> ( F Fn A -> ( ( F " y ) ~<_ y -> ( F " ( y u. { z } ) ) ~<_ ( y u. { z } ) ) ) )
60	59	a2d 26	. . . . 5 |- ( ( y e. Fin /\ -. z e. y ) -> ( ( F Fn A -> ( F " y ) ~<_ y ) -> ( F Fn A -> ( F " ( y u. { z } ) ) ~<_ ( y u. { z } ) ) ) )
61	9, 13, 17, 21, 24, 60	findcard2s 7553	. . . 4 |- ( A e. Fin -> ( F Fn A -> ( F " A ) ~<_ A ) )
62	3, 61	syl5 32	. . 3 |- ( A e. Fin -> ( F : A -onto-> B -> ( F " A ) ~<_ A ) )
63	62	imp 429	. 2 |- ( ( A e. Fin /\ F : A -onto-> B ) -> ( F " A ) ~<_ A )
64	2, 63	eqbrtrrd 4314	1 |- ( ( A e. Fin /\ F : A -onto-> B ) -> B ~<_ A )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 369   = wceq 1369   e. wcel 1756   _Vcvv 2972   u. cun 3326   i^i cin 3327   C_ wss 3328   (/)c0 3637   {csn 3877   <.cop 3883   class class class wbr 4292   _I cid 4631   ran crn 4841   |` cres 4842   "cima 4843   Fun wfun 5412   Fn wfn 5413   -onto->wfo 5416   ` cfv 5418   1oc1o 6913   ~~ cen 7307   ~<_ cdom 7308   Fincfn 7310

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4413  ax-nul 4421  ax-pow 4470  ax-pr 4531  ax-un 6372

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-ne 2608  df-ral 2720  df-rex 2721  df-reu 2722  df-rab 2724  df-v 2974  df-sbc 3187  df-dif 3331  df-un 3333  df-in 3335  df-ss 3342  df-pss 3344  df-nul 3638  df-if 3792  df-pw 3862  df-sn 3878  df-pr 3880  df-tp 3882  df-op 3884  df-uni 4092  df-br 4293  df-opab 4351  df-tr 4386  df-eprel 4632  df-id 4636  df-po 4641  df-so 4642  df-fr 4679  df-we 4681  df-ord 4722  df-on 4723  df-lim 4724  df-suc 4725  df-xp 4846  df-rel 4847  df-cnv 4848  df-co 4849  df-dm 4850  df-rn 4851  df-res 4852  df-ima 4853  df-iota 5381  df-fun 5420  df-fn 5421  df-f 5422  df-f1 5423  df-fo 5424  df-f1o 5425  df-fv 5426  df-om 6477  df-1o 6920  df-er 7101  df-en 7311  df-dom 7312  df-fin 7314

This theorem is referenced by:  fodomfib  7591  fofinf1o  7592  fidomdm  7593  fofi  7597  pwfilem  7605  cmpsub  19003  alexsubALT  19623