Theorem fodomr 4483

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 2722	. . . . . . . . . . . . 13 |- (A e. V -> (A \ ran g) e. V)
2		snex 2750	. . . . . . . . . . . . . 14 |- {z} e. V
3		xpexg 3259	. . . . . . . . . . . . . 14 |- (((A \ ran g) e. V /\ {z} e. V) -> ((A \ ran g) X. {z}) e. V)
4	2, 3	mpan2 696	. . . . . . . . . . . . 13 |- ((A \ ran g) e. V -> ((A \ ran g) X. {z}) e. V)
5	1, 4	syl 10	. . . . . . . . . . . 12 |- (A e. V -> ((A \ ran g) X. {z}) e. V)
6		visset 1813	. . . . . . . . . . . . 13 |- g e. V
7	6	cnvex 3520	. . . . . . . . . . . 12 |- `'g e. V
8	5, 7	jctil 292	. . . . . . . . . . 11 |- (A e. V -> (`'g e. V /\ ((A \ ran g) X. {z}) e. V))
9		unexb 2873	. . . . . . . . . . 11 |- ((`'g e. V /\ ((A \ ran g) X. {z}) e. V) <-> (`'g u. ((A \ ran g) X. {z})) e. V)
10	8, 9	sylib 198	. . . . . . . . . 10 |- (A e. V -> (`'g u. ((A \ ran g) X. {z})) e. V)
11		foeq1 3668	. . . . . . . . . . 11 |- (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 1863	. . . . . . . . . 10 |- ((`'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	. . . . . . . . 9 |- (A e. V -> ((`'g u. ((A \ ran g) X. {z})):A-onto->B -> E.f f:A-onto->B))
14		df-f1 3195	. . . . . . . . . . . . . . . . 17 |- (g:B-1-1->A <-> (g:B-->A /\ Fun `'g))
15	14	pm3.27bi 326	. . . . . . . . . . . . . . . 16 |- (g:B-1-1->A -> Fun `'g)
16		visset 1813	. . . . . . . . . . . . . . . . . 18 |- z e. V
17	16	fconst 3658	. . . . . . . . . . . . . . . . 17 |- ((A \ ran g) X. {z}):(A \ ran g)-->{z}
18		ffun 3629	. . . . . . . . . . . . . . . . 17 |- (((A \ ran g) X. {z}):(A \ ran g)-->{z} -> Fun ((A \ ran g) X. {z}))
19	17, 18	ax-mp 7	. . . . . . . . . . . . . . . 16 |- Fun ((A \ ran g) X. {z})
20	15, 19	jctir 293	. . . . . . . . . . . . . . 15 |- (g:B-1-1->A -> (Fun `'g /\ Fun ((A \ ran g) X. {z})))
21		df-rn 3189	. . . . . . . . . . . . . . . . . . 19 |- ran g = dom `' g
22	21	eqcomi 1479	. . . . . . . . . . . . . . . . . 18 |- dom `' g = ran g
23	16	snnz 2458	. . . . . . . . . . . . . . . . . . 19 |- {z} =/= (/)
24		dmxp 3332	. . . . . . . . . . . . . . . . . . 19 |- ({z} =/= (/) -> dom ((A \ ran g) X. {z}) = (A \ ran g))
25	23, 24	ax-mp 7	. . . . . . . . . . . . . . . . . 18 |- dom ((A \ ran g) X. {z}) = (A \ ran g)
26	22, 25	ineq12i 2215	. . . . . . . . . . . . . . . . 17 |- (dom `' g i^i dom ((A \ ran g) X. {z})) = (ran g i^i (A \ ran g))
27		difdisj 2337	. . . . . . . . . . . . . . . . 17 |- (ran g i^i (A \ ran g)) = (/)
28	26, 27	eqtr 1495	. . . . . . . . . . . . . . . 16 |- (dom `' g i^i dom ((A \ ran g) X. {z})) = (/)
29		funun 3554	. . . . . . . . . . . . . . . 16 |- (((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 696	. . . . . . . . . . . . . . 15 |- ((Fun `'g /\ Fun ((A \ ran g) X. {z})) -> Fun (`'g u. ((A \ ran g) X. {z})))
31	20, 30	syl 10	. . . . . . . . . . . . . 14 |- (g:B-1-1->A -> Fun (`'g u. ((A \ ran g) X. {z})))
32	31	adantl 388	. . . . . . . . . . . . 13 |- ((z e. B /\ g:B-1-1->A) -> Fun (`'g u. ((A \ ran g) X. {z})))
33		f1f 3665	. . . . . . . . . . . . . . . . 17 |- (g:B-1-1->A -> g:B-->A)
34		frn 3633	. . . . . . . . . . . . . . . . 17 |- (g:B-->A -> ran g (_ A)
35	33, 34	syl 10	. . . . . . . . . . . . . . . 16 |- (g:B-1-1->A -> ran g (_ A)
36		undif 2343	. . . . . . . . . . . . . . . 16 |- (ran g (_ A <-> (ran g u. (A \ ran g)) = A)
37	35, 36	sylib 198	. . . . . . . . . . . . . . 15 |- (g:B-1-1->A -> (ran g u. (A \ ran g)) = A)
38		dmun 3317	. . . . . . . . . . . . . . . 16 |- dom (`'g u. ((A \ ran g) X. {z})) = (dom `' g u. dom ((A \ ran g) X. {z}))
39	21	uneq1i 2180	. . . . . . . . . . . . . . . 16 |- (ran g u. dom ((A \ ran g) X. {z})) = (dom `' g u. dom ((A \ ran g) X. {z}))
40	25	uneq2i 2181	. . . . . . . . . . . . . . . 16 |- (ran g u. dom ((A \ ran g) X. {z})) = (ran g u. (A \ ran g))
41	38, 39, 40	3eqtr2 1501	. . . . . . . . . . . . . . 15 |- dom (`'g u. ((A \ ran g) X. {z})) = (ran g u. (A \ ran g))
42	37, 41	syl5eq 1519	. . . . . . . . . . . . . 14 |- (g:B-1-1->A -> dom (`'g u. ((A \ ran g) X. {z})) = A)
43	42	adantl 388	. . . . . . . . . . . . 13 |- ((z e. B /\ g:B-1-1->A) -> dom (`'g u. ((A \ ran g) X. {z})) = A)
44	32, 43	jca 288	. . . . . . . . . . . 12 |- ((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 3193	. . . . . . . . . . . 12 |- ((`'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 200	. . . . . . . . . . 11 |- ((z e. B /\ g:B-1-1->A) -> (`'g u. ((A \ ran g) X. {z})) Fn A)
47		fdm 3631	. . . . . . . . . . . . . . . 16 |- (g:B-->A -> dom g = B)
48	33, 47	syl 10	. . . . . . . . . . . . . . 15 |- (g:B-1-1->A -> dom g = B)
49		dfdm4 3305	. . . . . . . . . . . . . . 15 |- dom g = ran `' g
50	48, 49	syl5eqr 1521	. . . . . . . . . . . . . 14 |- (g:B-1-1->A -> ran `' g = B)
51	50	uneq1d 2183	. . . . . . . . . . . . 13 |- (g:B-1-1->A -> (ran `' g u. ran ((A \ ran g) X. {z})) = (B u. ran ((A \ ran g) X. {z})))
52		0ss 2301	. . . . . . . . . . . . . . . . 17 |- (/) (_ B
53		xpeq1 3200	. . . . . . . . . . . . . . . . . . . . 21 |- ((A \ ran g) = (/) -> ((A \ ran g) X. {z}) = ((/) X. {z}))
54		xp0r 3239	. . . . . . . . . . . . . . . . . . . . 21 |- ((/) X. {z}) = (/)
55	53, 54	syl6eq 1523	. . . . . . . . . . . . . . . . . . . 20 |- ((A \ ran g) = (/) -> ((A \ ran g) X. {z}) = (/))
56	55	rneqd 3341	. . . . . . . . . . . . . . . . . . 19 |- ((A \ ran g) = (/) -> ran ((A \ ran g) X. {z}) = ran (/))
57		rn0 3355	. . . . . . . . . . . . . . . . . . 19 |- ran (/) = (/)
58	56, 57	syl6eq 1523	. . . . . . . . . . . . . . . . . 18 |- ((A \ ran g) = (/) -> ran ((A \ ran g) X. {z}) = (/))
59	58	sseq1d 2088	. . . . . . . . . . . . . . . . 17 |- ((A \ ran g) = (/) -> (ran ((A \ ran g) X. {z}) (_ B <-> (/) (_ B))
60	52, 59	mpbiri 194	. . . . . . . . . . . . . . . 16 |- ((A \ ran g) = (/) -> ran ((A \ ran g) X. {z}) (_ B)
61	60	a1d 12	. . . . . . . . . . . . . . 15 |- ((A \ ran g) = (/) -> (z e. B -> ran ((A \ ran g) X. {z}) (_ B))
62		rnxp 3472	. . . . . . . . . . . . . . . . . 18 |- ((A \ ran g) =/= (/) -> ran ((A \ ran g) X. {z}) = {z})
63	62	adantr 389	. . . . . . . . . . . . . . . . 17 |- (((A \ ran g) =/= (/) /\ z e. B) -> ran ((A \ ran g) X. {z}) = {z})
64		snssi 2466	. . . . . . . . . . . . . . . . . 18 |- (z e. B -> {z} (_ B)
65	64	adantl 388	. . . . . . . . . . . . . . . . 17 |- (((A \ ran g) =/= (/) /\ z e. B) -> {z} (_ B)
66	63, 65	eqsstrd 2095	. . . . . . . . . . . . . . . 16 |- (((A \ ran g) =/= (/) /\ z e. B) -> ran ((A \ ran g) X. {z}) (_ B)
67	66	ex 373	. . . . . . . . . . . . . . 15 |- ((A \ ran g) =/= (/) -> (z e. B -> ran ((A \ ran g) X. {z}) (_ B))
68	61, 67	pm2.61ine 1634	. . . . . . . . . . . . . 14 |- (z e. B -> ran ((A \ ran g) X. {z}) (_ B)
69		ssequn2 2203	. . . . . . . . . . . . . 14 |- (ran ((A \ ran g) X. {z}) (_ B <-> (B u. ran ((A \ ran g) X. {z})) = B)
70	68, 69	sylib 198	. . . . . . . . . . . . 13 |- (z e. B -> (B u. ran ((A \ ran g) X. {z})) = B)
71	51, 70	sylan9eqr 1529	. . . . . . . . . . . 12 |- ((z e. B /\ g:B-1-1->A) -> (ran `' g u. ran ((A \ ran g) X. {z})) = B)
72		rnun 3457	. . . . . . . . . . . 12 |- ran (`'g u. ((A \ ran g) X. {z})) = (ran `' g u. ran ((A \ ran g) X. {z})