Theorem fodomr 7731

Description: There exists a mapping from a set onto any (nonempty) set that it dominates. (Contributed by NM, 23-Mar-2006.)

Assertion

Ref	Expression
fodomr	|- ( ( (/) ~< B /\ B ~<_ A ) -> E. f f : A -onto-> B )

Distinct variable groups:   A, f   B, f

Proof of Theorem fodomr

Dummy variables g z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		reldom 7585	. . . 4 |- Rel ~<_
2	1	brrelex2i 4894	. . 3 |- ( B ~<_ A -> A e. _V )
3	2	adantl 468	. 2 |- ( ( (/) ~< B /\ B ~<_ A ) -> A e. _V )
4	1	brrelexi 4893	. . . 4 |- ( B ~<_ A -> B e. _V )
5		0sdomg 7709	. . . . 5 |- ( B e. _V -> ( (/) ~< B <-> B =/= (/) ) )
6		n0 3773	. . . . 5 |- ( B =/= (/) <-> E. z z e. B )
7	5, 6	syl6bb 265	. . . 4 |- ( B e. _V -> ( (/) ~< B <-> E. z z e. B ) )
8	4, 7	syl 17	. . 3 |- ( B ~<_ A -> ( (/) ~< B <-> E. z z e. B ) )
9	8	biimpac 489	. 2 |- ( ( (/) ~< B /\ B ~<_ A ) -> E. z z e. B )
10		brdomi 7590	. . 3 |- ( B ~<_ A -> E. g g : B -1-1-> A )
11	10	adantl 468	. 2 |- ( ( (/) ~< B /\ B ~<_ A ) -> E. g g : B -1-1-> A )
12		difexg 4571	. . . . . . . . . 10 |- ( A e. _V -> ( A \ ran g ) e. _V )
13		snex 4661	. . . . . . . . . 10 |- { z } e. _V
14		xpexg 6606	. . . . . . . . . 10 |- ( ( ( A \ ran g ) e. _V /\ { z } e. _V ) -> ( ( A \ ran g ) X. { z } ) e. _V )
15	12, 13, 14	sylancl 667	. . . . . . . . 9 |- ( A e. _V -> ( ( A \ ran g ) X. { z } ) e. _V )
16		vex 3085	. . . . . . . . . 10 |- g e. _V
17	16	cnvex 6753	. . . . . . . . 9 |- `' g e. _V
18	15, 17	jctil 540	. . . . . . . 8 |- ( A e. _V -> ( `' g e. _V /\ ( ( A \ ran g ) X. { z } ) e. _V ) )
19		unexb 6604	. . . . . . . 8 |- ( ( `' g e. _V /\ ( ( A \ ran g ) X. { z } ) e. _V ) <-> ( `' g u. ( ( A \ ran g ) X. { z } ) ) e. _V )
20	18, 19	sylib 200	. . . . . . 7 |- ( A e. _V -> ( `' g u. ( ( A \ ran g ) X. { z } ) ) e. _V )
21		df-f1 5605	. . . . . . . . . . . . 13 |- ( g : B -1-1-> A <-> ( g : B --> A /\ Fun `' g ) )
22	21	simprbi 466	. . . . . . . . . . . 12 |- ( g : B -1-1-> A -> Fun `' g )
23		vex 3085	. . . . . . . . . . . . . 14 |- z e. _V
24	23	fconst 5785	. . . . . . . . . . . . 13 |- ( ( A \ ran g ) X. { z } ) : ( A \ ran g ) --> { z }
25		ffun 5747	. . . . . . . . . . . . 13 |- ( ( ( A \ ran g ) X. { z } ) : ( A \ ran g ) --> { z } -> Fun ( ( A \ ran g ) X. { z } ) )
26	24, 25	ax-mp 5	. . . . . . . . . . . 12 |- Fun ( ( A \ ran g ) X. { z } )
27	22, 26	jctir 541	. . . . . . . . . . 11 |- ( g : B -1-1-> A -> ( Fun `' g /\ Fun ( ( A \ ran g ) X. { z } ) ) )
28		df-rn 4863	. . . . . . . . . . . . . 14 |- ran g = dom `' g
29	28	eqcomi 2436	. . . . . . . . . . . . 13 |- dom `' g = ran g
30	23	snnz 4117	. . . . . . . . . . . . . 14 |- { z } =/= (/)
31		dmxp 5071	. . . . . . . . . . . . . 14 |- ( { z } =/= (/) -> dom ( ( A \ ran g ) X. { z } ) = ( A \ ran g ) )
32	30, 31	ax-mp 5	. . . . . . . . . . . . 13 |- dom ( ( A \ ran g ) X. { z } ) = ( A \ ran g )
33	29, 32	ineq12i 3664	. . . . . . . . . . . 12 |- ( dom `' g i^i dom ( ( A \ ran g ) X. { z } ) ) = ( ran g i^i ( A \ ran g ) )
34		disjdif 3869	. . . . . . . . . . . 12 |- ( ran g i^i ( A \ ran g ) ) = (/)
35	33, 34	eqtri 2452	. . . . . . . . . . 11 |- ( dom `' g i^i dom ( ( A \ ran g ) X. { z } ) ) = (/)
36		funun 5642	. . . . . . . . . . 11 |- ( ( ( Fun `' g /\ Fun ( ( A \ ran g ) X. { z } ) ) /\ ( dom `' g i^i dom ( ( A \ ran g ) X. { z } ) ) = (/) ) -> Fun ( `' g u. ( ( A \ ran g ) X. { z } ) ) )
37	27, 35, 36	sylancl 667	. . . . . . . . . 10 |- ( g : B -1-1-> A -> Fun ( `' g u. ( ( A \ ran g ) X. { z } ) ) )
38	37	adantl 468	. . . . . . . . 9 |- ( ( z e. B /\ g : B -1-1-> A ) -> Fun ( `' g u. ( ( A \ ran g ) X. { z } ) ) )
39		dmun 5059	. . . . . . . . . . . 12 |- dom ( `' g u. ( ( A \ ran g ) X. { z } ) ) = ( dom `' g u. dom ( ( A \ ran g ) X. { z } ) )
40	28	uneq1i 3618	. . . . . . . . . . . 12 |- ( ran g u. dom ( ( A \ ran g ) X. { z } ) ) = ( dom `' g u. dom ( ( A \ ran g ) X. { z } ) )
41	32	uneq2i 3619	. . . . . . . . . . . 12 |- ( ran g u. dom ( ( A \ ran g ) X. { z } ) ) = ( ran g u. ( A \ ran g ) )
42	39, 40, 41	3eqtr2i 2458	. . . . . . . . . . 11 |- dom ( `' g u. ( ( A \ ran g ) X. { z } ) ) = ( ran g u. ( A \ ran g ) )
43		f1f 5795	. . . . . . . . . . . . 13 |- ( g : B -1-1-> A -> g : B --> A )
44		frn 5751	. . . . . . . . . . . . 13 |- ( g : B --> A -> ran g C_ A )
45	43, 44	syl 17	. . . . . . . . . . . 12 |- ( g : B -1-1-> A -> ran g C_ A )
46		undif 3878	. . . . . . . . . . . 12 |- ( ran g C_ A <-> ( ran g u. ( A \ ran g ) ) = A )
47	45, 46	sylib 200	. . . . . . . . . . 11 |- ( g : B -1-1-> A -> ( ran g u. ( A \ ran g ) ) = A )
48	42, 47	syl5eq 2476	. . . . . . . . . 10 |- ( g : B -1-1-> A -> dom ( `' g u. ( ( A \ ran g ) X. { z } ) ) = A )
49	48	adantl 468	. . . . . . . . 9 |- ( ( z e. B /\ g : B -1-1-> A ) -> dom ( `' g u. ( ( A \ ran g ) X. { z } ) ) = A )
50		df-fn 5603	. . . . . . . . 9 |- ( ( `' g u. ( ( A \ ran g ) X. { z } ) ) Fn A <-> ( Fun ( `' g u. ( ( A \ ran g ) X. { z } ) ) /\ dom ( `' g u. ( ( A \ ran g ) X. { z } ) ) = A ) )
51	38, 49, 50	sylanbrc 669	. . . . . . . 8 |- ( ( z e. B /\ g : B -1-1-> A ) -> ( `' g u. ( ( A \ ran g ) X. { z } ) ) Fn A )
52		rnun 5262	. . . . . . . . 9 |- ran ( `' g u. ( ( A \ ran g ) X. { z } ) ) = ( ran `' g u. ran ( ( A \ ran g ) X. { z } ) )
53		dfdm4 5045	. . . . . . . . . . . 12 |- dom g = ran `' g
54		f1dm 5799	. . . . . . . . . . . 12 |- ( g : B -1-1-> A -> dom g = B )
55	53, 54	syl5eqr 2478	. . . . . . . . . . 11 |- ( g : B -1-1-> A -> ran `' g = B )
56	55	uneq1d 3621	. . . . . . . . . 10 |- ( g : B -1-1-> A -> ( ran `' g u. ran ( ( A \ ran g ) X. { z } ) ) = ( B u. ran ( ( A \ ran g ) X. { z } ) ) )
57		xpeq1 4866	. . . . . . . . . . . . . . . . 17 |- ( ( A \ ran g ) = (/) -> ( ( A \ ran g ) X. { z } ) = ( (/) X. { z } ) )
58		0xp 4933	. . . . . . . . . . . . . . . . 17 |- ( (/) X. { z } ) = (/)
59	57, 58	syl6eq 2480	. . . . . . . . . . . . . . . 16 |- ( ( A \ ran g ) = (/) -> ( ( A \ ran g ) X. { z } ) = (/) )
60	59	rneqd 5080	. . . . . . . . . . . . . . 15 |- ( ( A \ ran g ) = (/) -> ran ( ( A \ ran g ) X. { z } ) = ran (/) )
61		rn0 5104	. . . . . . . . . . . . . . 15 |- ran (/) = (/)
62	60, 61	syl6eq 2480	. . . . . . . . . . . . . 14 |- ( ( A \ ran g ) = (/) -> ran ( ( A \ ran g ) X. { z } ) = (/) )
63		0ss 3793	. . . . . . . . . . . . . 14 |- (/) C_ B
64	62, 63	syl6eqss 3516	. . . . . . . . . . . . 13 |- ( ( A \ ran g ) = (/) -> ran ( ( A \ ran g ) X. { z } ) C_ B )
65	64	a1d 27	. . . . . . . . . . . 12 |- ( ( A \ ran g ) = (/) -> ( z e. B -> ran ( ( A \ ran g ) X. { z } ) C_ B ) )
66		rnxp 5285	. . . . . . . . . . . . . . 15 |- ( ( A \ ran g ) =/= (/) -> ran ( ( A \ ran g ) X. { z } ) = { z } )
67	66	adantr 467	. . . . . . . . . . . . . 14 |- ( ( ( A \ ran g ) =/= (/) /\ z e. B ) -> ran ( ( A \ ran g ) X. { z } ) = { z } )
68		snssi 4143	. . . . . . . . . . . . . . 15 |- ( z e. B -> { z } C_ B )
69	68	adantl 468	. . . . . . . . . . . . . 14 |- ( ( ( A \ ran g ) =/= (/) /\ z e. B ) -> { z } C_ B )
70	67, 69	eqsstrd 3500	. . . . . . . . . . . . 13 |- ( ( ( A \ ran g ) =/= (/) /\ z e. B ) -> ran ( ( A \ ran g ) X. { z } ) C_ B )
71	70	ex 436	. . . . . . . . . . . 12 |- ( ( A \ ran g ) =/= (/) -> ( z e. B -> ran ( ( A \ ran g ) X. { z } ) C_ B ) )
72	65, 71	pm2.61ine 2738	. . . . . . . . . . 11 |- ( z e. B -> ran ( ( A \ ran g ) X. { z } ) C_ B )
73		ssequn2 3641	. . . . . . . . . . 11 |- ( ran ( ( A \ ran g ) X. { z } ) C_ B <-> ( B u. ran ( ( A \ ran g ) X. { z } ) ) = B )
74	72, 73	sylib 200	. . . . . . . . . 10 |- ( z e. B -> ( B u. ran ( ( A \ ran g ) X. { z } ) ) = B )
75	56, 74	sylan9eqr 2486	. . . . . . . . 9 |- ( ( z e. B /\ g : B -1-1-> A ) -> ( ran `' g u. ran ( ( A \ ran g ) X. { z } ) ) = B )
76	52, 75	syl5eq 2476	. . . . . . . 8 |- ( ( z e. B /\ g : B -1-1-> A ) -> ran ( `' g u. ( ( A \ ran g ) X. { z } ) ) = B )
77		df-fo 5606	. . . . . . . 8 |- ( ( `' g u. ( ( A \ ran g ) X. { z } ) ) : A -onto-> B <-> ( ( `' g u. ( ( A \ ran g ) X. { z } ) ) Fn A /\ ran ( `' g u. ( ( A \ ran g ) X. { z } ) ) = B ) )
78	51, 76, 77	sylanbrc 669	. . . . . . 7 |- ( ( z e. B /\ g : B -1-1-> A ) -> ( `' g u. ( ( A \ ran g ) X. { z } ) ) : A -onto-> B )
79		foeq1 5805	. . . . . . . 8 |- ( f = ( `' g u. ( ( A \ ran g ) X. { z } ) ) -> ( f : A -onto-> B <-> ( `' g u. ( ( A \ ran g ) X. { z } ) ) : A -onto-> B ) )
80	79	spcegv 3168	. . . . . . 7 |- ( ( `' g u. ( ( A \ ran g ) X. { z } ) ) e. _V -> ( ( `' g u. ( ( A \ ran g ) X. { z } ) ) : A -onto-> B -> E. f f : A -onto-> B ) )
81	20, 78, 80	syl2im 40	. . . . . 6 |- ( A e. _V -> ( ( z e. B /\ g : B -1-1-> A ) -> E. f f : A -onto-> B ) )
82	81	expdimp 439	. . . . 5 |- ( ( A e. _V /\ z e. B ) -> ( g : B -1-1-> A -> E. f f : A -onto-> B ) )
83	82	exlimdv 1769	. . . 4 |- ( ( A e. _V /\ z e. B ) -> ( E. g g : B -1-1-> A -> E. f f : A -onto-> B ) )
84	83	ex 436	. . 3 |- ( A e. _V -> ( z e. B -> ( E. g g : B -1-1-> A -> E. f f : A -onto-> B ) ) )
85	84	exlimdv 1769	. 2 |- ( A e. _V -> ( E. z z e. B -> ( E. g g : B -1-1-> A -> E. f f : A -onto-> B ) ) )
86	3, 9, 11, 85	syl3c 64	1 |- ( ( (/) ~< B /\ B ~<_ A ) -> E. f f : A -onto-> B )

Syntax hints:   -> wi 4   <-> wb 188   /\ wa 371   = wceq 1438   E.wex 1660   e. wcel 1869   =/= wne 2619   _Vcvv 3082   \ cdif 3435   u. cun 3436   i^i cin 3437   C_ wss 3438   (/)c0 3763   {csn 3998   class class class wbr 4422   X. cxp 4850   `'ccnv 4851   dom cdm 4852   ran crn 4853   Fun wfun 5594   Fn wfn 5595   -->wf 5596   -1-1->wf1 5597   -onto->wfo 5598   ~<_ cdom 7577   ~< csdm 7578

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-8 1871  ax-9 1873  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401  ax-sep 4545  ax-nul 4554  ax-pow 4601  ax-pr 4659  ax-un 6596

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 985  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-eu 2270  df-mo 2271  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-ne 2621  df-ral 2781  df-rex 2782  df-rab 2785  df-v 3084  df-dif 3441  df-un 3443  df-in 3445  df-ss 3452  df-nul 3764  df-if 3912  df-pw 3983  df-sn 3999  df-pr 4001  df-op 4005  df-uni 4219  df-br 4423  df-opab 4482  df-mpt 4483  df-id 4767  df-xp 4858  df-rel 4859  df-cnv 4860  df-co 4861  df-dm 4862  df-rn 4863  df-res 4864  df-ima 4865  df-fun 5602  df-fn 5603  df-f 5604  df-f1 5605  df-fo 5606  df-f1o 5607  df-er 7373  df-en 7580  df-dom 7581  df-sdom 7582

This theorem is referenced by:  pwdom  7732  fodomfib  7859  domwdom  8097  iunfictbso  8551  fodomb  8960  brdom3  8962  konigthlem  8999  1stcfb  20456  ovoliunnul  22456  sigapildsys  28990  carsgclctunlem3  29158  ovoliunnfl  31944  voliunnfl  31946  volsupnfl  31947  nnfoctb  37292  caragenunicl  38172