Theorem fodomr 4628

Description: There exists a mapping from a set onto any (non-empty) set that it dominates.

Assertion

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

Distinct variable groups:   A,f   B,f

Proof of Theorem fodomr

Step	Hyp	Ref	Expression
1		difexg 2796	. . . . . . . . . . . 12 |- (A e. V -> (A \ ran g) e. V)
2		snex 2826	. . . . . . . . . . . . 13 |- {z} e. V
3		xpexg 3348	. . . . . . . . . . . . 13 |- (((A \ ran g) e. V /\ {z} e. V) -> ((A \ ran g) X. {z}) e. V)
4	2, 3	mpan2 700	. . . . . . . . . . . 12 |- ((A \ ran g) e. V -> ((A \ ran g) X. {z}) e. V)
5	1, 4	syl 10	. . . . . . . . . . 11 |- (A e. V -> ((A \ ran g) X. {z}) e. V)
6		visset 1859	. . . . . . . . . . . 12 |- g e. V
7	6	cnvex 3625	. . . . . . . . . . 11 |- `'g e. V
8	5, 7	jctil 290	. . . . . . . . . 10 |- (A e. V -> (`'g e. V /\ ((A \ ran g) X. {z}) e. V))
9		unexb 3096	. . . . . . . . . 10 |- ((`'g e. V /\ ((A \ ran g) X. {z}) e. V) <-> (`'g u. ((A \ ran g) X. {z})) e. V)
10	8, 9	sylib 196	. . . . . . . . 9 |- (A e. V -> (`'g u. ((A \ ran g) X. {z})) e. V)
11		foeq1 3775	. . . . . . . . . 10 |- (f = (`'g u. ((A \ ran g) X. {z})) -> (f:A-onto->B <-> (`'g u. ((A \ ran g) X. {z})):A-onto->B))
12	11	cla4egv 1909	. . . . . . . . 9 |- ((`'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))
13	10, 12	syl 10	. . . . . . . 8 |- (A e. V -> ((`'g u. ((A \ ran g) X. {z})):A-onto->B -> E.f f:A-onto->B))
14		df-f1 3276	. . . . . . . . . . . . . . . 16 |- (g:B-1-1->A <-> (g:B-->A /\ Fun `'g))
15	14	pm3.27bi 324	. . . . . . . . . . . . . . 15 |- (g:B-1-1->A -> Fun `'g)
16		visset 1859	. . . . . . . . . . . . . . . . 17 |- z e. V
17	16	fconst 3765	. . . . . . . . . . . . . . . 16 |- ((A \ ran g) X. {z}):(A \ ran g)-->{z}
18		ffun 3736	. . . . . . . . . . . . . . . 16 |- (((A \ ran g) X. {z}):(A \ ran g)-->{z} -> Fun ((A \ ran g) X. {z}))
19	17, 18	ax-mp 7	. . . . . . . . . . . . . . 15 |- Fun ((A \ ran g) X. {z})
20	15, 19	jctir 291	. . . . . . . . . . . . . 14 |- (g:B-1-1->A -> (Fun `'g /\ Fun ((A \ ran g) X. {z})))
21		df-rn 3270	. . . . . . . . . . . . . . . . . 18 |- ran g = dom `' g
22	21	eqcomi 1522	. . . . . . . . . . . . . . . . 17 |- dom `' g = ran g
23	16	snnz 2522	. . . . . . . . . . . . . . . . . 18 |- {z} =/= (/)
24		dmxp 3419	. . . . . . . . . . . . . . . . . 18 |- ({z} =/= (/) -> dom ((A \ ran g) X. {z}) = (A \ ran g))
25	23, 24	ax-mp 7	. . . . . . . . . . . . . . . . 17 |- dom ((A \ ran g) X. {z}) = (A \ ran g)
26	22, 25	ineq12i 2267	. . . . . . . . . . . . . . . 16 |- (dom `' g i^i dom ((A \ ran g) X. {z})) = (ran g i^i (A \ ran g))
27		difdisj 2390	. . . . . . . . . . . . . . . 16 |- (ran g i^i (A \ ran g)) = (/)
28	26, 27	eqtri 1538	. . . . . . . . . . . . . . 15 |- (dom `' g i^i dom ((A \ ran g) X. {z})) = (/)
29		funun 3659	. . . . . . . . . . . . . . 15 |- (((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})))
30	28, 29	mpan2 700	. . . . . . . . . . . . . 14 |- ((Fun `'g /\ Fun ((A \ ran g) X. {z})) -> Fun (`'g u. ((A \ ran g) X. {z})))
31	20, 30	syl 10	. . . . . . . . . . . . 13 |- (g:B-1-1->A -> Fun (`'g u. ((A \ ran g) X. {z})))
32	31	adantl 388	. . . . . . . . . . . 12 |- ((z e. B /\ g:B-1-1->A) -> Fun (`'g u. ((A \ ran g) X. {z})))
33		f1f 3772	. . . . . . . . . . . . . . . 16 |- (g:B-1-1->A -> g:B-->A)
34		frn 3740	. . . . . . . . . . . . . . . 16 |- (g:B-->A -> ran g (_ A)
35	33, 34	syl 10	. . . . . . . . . . . . . . 15 |- (g:B-1-1->A -> ran g (_ A)
36		undif 2397	. . . . . . . . . . . . . . 15 |- (ran g (_ A <-> (ran g u. (A \ ran g)) = A)
37	35, 36	sylib 196	. . . . . . . . . . . . . 14 |- (g:B-1-1->A -> (ran g u. (A \ ran g)) = A)
38		dmun 3408	. . . . . . . . . . . . . . 15 |- dom (`'g u. ((A \ ran g) X. {z})) = (dom `' g u. dom ((A \ ran g) X. {z}))
39	21	uneq1i 2232	. . . . . . . . . . . . . . 15 |- (ran g u. dom ((A \ ran g) X. {z})) = (dom `' g u. dom ((A \ ran g) X. {z}))
40	25	uneq2i 2233	. . . . . . . . . . . . . . 15 |- (ran g u. dom ((A \ ran g) X. {z})) = (ran g u. (A \ ran g))
41	38, 39, 40	3eqtr2i 1544	. . . . . . . . . . . . . 14 |- dom (`'g u. ((A \ ran g) X. {z})) = (ran g u. (A \ ran g))
42	37, 41	syl5eq 1562	. . . . . . . . . . . . 13 |- (g:B-1-1->A -> dom (`'g u. ((A \ ran g) X. {z})) = A)
43	42	adantl 388	. . . . . . . . . . . 12 |- ((z e. B /\ g:B-1-1->A) -> dom (`'g u. ((A \ ran g) X. {z})) = A)
44	32, 43	jca 286	. . . . . . . . . . 11 |- ((z e. B /\ g:B-1-1->A) -> (Fun (`'g u. ((A \ ran g) X. {z})) /\ dom (`'g u. ((A \ ran g) X. {z})) = A))
45		df-fn 3274	. . . . . . . . . . 11 |- ((`'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))
46	44, 45	sylibr 198	. . . . . . . . . 10 |- ((z e. B /\ g:B-1-1->A) -> (`'g u. ((A \ ran g) X. {z})) Fn A)
47		fdm 3738	. . . . . . . . . . . . . . 15 |- (g:B-->A -> dom g = B)
48	33, 47	syl 10	. . . . . . . . . . . . . 14 |- (g:B-1-1->A -> dom g = B)
49		dfdm4 3396	. . . . . . . . . . . . . 14 |- dom g = ran `' g
50	48, 49	syl5eqr 1564	. . . . . . . . . . . . 13 |- (g:B-1-1->A -> ran `' g = B)
51	50	uneq1d 2235	. . . . . . . . . . . 12 |- (g:B-1-1->A -> (ran `' g u. ran ((A \ ran g) X. {z})) = (B u. ran ((A \ ran g) X. {z})))
52		0ss 2354	. . . . . . . . . . . . . . . 16 |- (/) (_ B
53		xpeq1 3281	. . . . . . . . . . . . . . . . . . . 20 |- ((A \ ran g) = (/) -> ((A \ ran g) X. {z}) = ((/) X. {z}))
54		xp0r 3325	. . . . . . . . . . . . . . . . . . . 20 |- ((/) X. {z}) = (/)
55	53, 54	syl6eq 1566	. . . . . . . . . . . . . . . . . . 19 |- ((A \ ran g) = (/) -> ((A \ ran g) X. {z}) = (/))
56	55	rneqd 3428	. . . . . . . . . . . . . . . . . 18 |- ((A \ ran g) = (/) -> ran ((A \ ran g) X. {z}) = ran (/))
57		rn0 3442	. . . . . . . . . . . . . . . . . 18 |- ran (/) = (/)
58	56, 57	syl6eq 1566	. . . . . . . . . . . . . . . . 17 |- ((A \ ran g) = (/) -> ran ((A \ ran g) X. {z}) = (/))
59	58	sseq1d 2140	. . . . . . . . . . . . . . . 16 |- ((A \ ran g) = (/) -> (ran ((A \ ran g) X. {z}) (_ B <-> (/) (_ B))
60	52, 59	mpbiri 192	. . . . . . . . . . . . . . 15 |- ((A \ ran g) = (/) -> ran ((A \ ran g) X. {z}) (_ B)
61	60	a1d 12	. . . . . . . . . . . . . 14 |- ((A \ ran g) = (/) -> (z e. B -> ran ((A \ ran g) X. {z}) (_ B))
62		rnxp 3557	. . . . . . . . . . . . . . . . 17 |- ((A \ ran g) =/= (/) -> ran ((A \ ran g) X. {z}) = {z})
63	62	adantr 389	. . . . . . . . . . . . . . . 16 |- (((A \ ran g) =/= (/) /\ z e. B) -> ran ((A \ ran g) X. {z}) = {z})
64		snssi 2530	. . . . . . . . . . . . . . . . 17 |- (z e. B -> {z} (_ B)
65	64	adantl 388	. . . . . . . . . . . . . . . 16 |- (((A \ ran g) =/= (/) /\ z e. B) -> {z} (_ B)
66	63, 65	eqsstrd 2147	. . . . . . . . . . . . . . 15 |- (((A \ ran g) =/= (/) /\ z e. B) -> ran ((A \ ran g) X. {z}) (_ B)
67	66	ex 371	. . . . . . . . . . . . . 14 |- ((A \ ran g) =/= (/) -> (z e. B -> ran ((A \ ran g) X. {z}) (_ B))
68	61, 67	pm2.61ine 1680	. . . . . . . . . . . . 13 |- (z e. B -> ran ((A \ ran g) X. {z}) (_ B)
69		ssequn2 2255	. . . . . . . . . . . . 13 |- (ran ((A \ ran g) X. {z}) (_ B <-> (B u. ran ((A \ ran g) X. {z})) = B)
70	68, 69	sylib 196	. . . . . . . . . . . 12 |- (z e. B -> (B u. ran ((A \ ran g) X. {z})) = B)
71	51, 70	sylan9eqr 1572	. . . . . . . . . . 11 |- ((z e. B /\ g:B-1-1->A) -> (ran `' g u. ran ((A \ ran g) X. {z})) = B)
72		rnun 3542	. . . . . . . . . . 11 |- ran (`'g u. ((A \ ran g) X. {z})) = (ran `' g u. ran ((A \ ran g) X. {z}))
73	71, 72	syl5eq 1562	. . . . . . . . . 10 |- ((z e. B /\ g:B-1-1->A) -> ran (`'g u. ((A \ ran g) X. {z})) = B)
74	46, 73	jca 286	. . . . . . . . 9 |- ((z e. B /\ g:B-1-1->A) -> ((`'g u. ((A \ ran g) X. {z})) Fn A /\ ran (`'g u. ((A \ ran g) X. {z})) = B))
75		df-fo 3277	. . . . . . . . 9 |- ((`'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))
76	74, 75	sylibr 198	. . . . . . . 8 |- ((z e. B /\ g:B-1-1->A) -> (`'g u. ((A \ ran g) X. {z})):A-onto->B)
77	13, 76	syl5 21	. . . . . . 7 |- (A e. V -> ((z e. B /\ g:B-1-1->A) -> E.f f:A-onto->B))
78	77	expdimp 375	. . . . . 6 |- ((A e. V /\ z e. B) -> (g:B-1-1->A -> E.f f:A-onto->B))
79	78	19.23adv 1251	. . . . 5 |- ((A e. V /\ z e. B) -> (E.g g:B-1-1->A -> E.f f:A-onto->B))
80	79	ex 371	. . . 4 |- (A e. V -> (z e. B -> (E.g g:B-1-1->A -> E.f f:A-onto->B)))
81	80	19.23adv 1251	. . 3 |- (A e. V -> (E.z z e. B -> (E.g g:B-1-1->A -> E.f f:A-onto->B)))
82	81	3imp 833	. 2 |- ((A e. V /\ E.z z e. B /\ E.g g:B-1-1->A) -> E.f f:A-onto->B)
83		elisset 1863	. . 3 |- (A e. C -> A e. V)
84	83	3ad2ant1 806	. 2 |- ((A e. C /\ (/) ~< B /\ B ~<_ A) -> A e. V)
85		reldom 4514	. . . . . 6 |- Rel ~<_
86	85	brrelexi 3291	. . . . 5 |- (B ~<_ A -> B e. V)
87		0sdomg 4611	. . . . . 6 |- (B e. V -> ((/) ~< B <-> B =/= (/)))
88		n0 2341	. . . . . 6 |- (B =/= (/) <-> E.z z e. B)
89	87, 88	syl6bb 539	. . . . 5 |- (B e. V -> ((/) ~< B <-> E.z z e. B))
90	86, 89	syl 10	. . . 4 |- (B ~<_ A -> ((/) ~< B <-> E.z z e. B))
91	90	biimpac 418	. . 3 |- (((/) ~< B /\ B ~<_ A) -> E.z z e. B)
92	91	3adant1 803	. 2 |- ((A e. C /\ (/) ~< B /\ B ~<_ A) -> E.z z e. B)
93		brdomg 4517	. . . 4 |- (A e. C -> (B ~<_ A <-> E.g g:B-1-1->A))
94	93	biimpa 416	. . 3 |- ((A e. C /\ B ~<_ A) -> E.g g:B-1-1->A)
95	94	3adant2 804	. 2 |- ((A e. C /\ (/) ~< B /\ B ~<_ A) -> E.g g:B-1-1->A)
96	82, 84, 92, 95	syl3anc 864	1 |- ((A e. C /\ (/) ~< B /\ B ~<_ A) -> E.f f:A-onto->B)

Syntax hints:   -> wi 3   <-> wb 144   /\ wa 221   /\ w3a 781   = wceq 992   e. wcel 994  E.wex 1016   =/= wne 1628  Vcvv 1857   \ cdif 2096   u. cun 2097   i^i cin 2098   (_ wss 2099  (/)c0 2332  {csn 2467   class class class wbr 2692   X. cxp 3249  `'ccnv 3250  dom cdm 3251  ran crn 3252  Fun wfun 3257   Fn wfn 3258  -->wf 3259  -1-1->wf1 3260  -onto->wfo 3261   ~<_ cdom 4506   ~< csdm 4507

This theorem is referenced by:  fodomfib 4710  fodomb 4946  brdom3 4947

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 998  ax-gen 999  ax-8 1000  ax-9 1001  ax-10 1002  ax-11 1003  ax-12 1004  ax-13 1005  ax-14 1006  ax-17 1007  ax-4 1009  ax-5o 1011  ax-6o 1014  ax-9o 1159  ax-10o 1177  ax-16 1247  ax-11o 1255  ax-ext 1500  ax-rep 2767  ax-sep 2777  ax-nul 2784  ax-pow 2818  ax-pr 2855  ax-un 3089

This theorem depends on definitions:  df-bi 145  df-or 222  df-an 223  df-3an 783  df-ex 1017  df-sb 1209  df-eu 1421  df-mo 1422  df-clab 1506  df-cleq 1511  df-clel 1514  df-ne 1630  df-ral 1695  df-rex 1696  df-v 1858  df-dif 2101  df-un 2102  df-in 2103  df-ss 2105  df-nul 2333  df-pw 2459  df-sn 2470  df-pr 2471  df-op 2474  df-uni 2570  df-br 2693  df-opab 2741  df-id 2913  df-xp 3265  df-rel 3266  df-cnv 3267  df-co 3268  df-dm 3269  df-rn 3270  df-res 3271  df-ima 3272  df-fun 3273  df-fn 3274  df-f 3275  df-f1 3276  df-fo 3277  df-f1o 3278  df-er 4401  df-en 4509  df-dom 4510  df-sdom 4511

Copyright terms: Public domain