Theorem fodomb 3615

Description: Equivalence of an onto mapping and dominance for a non-empty set. Proposition 10.35 of [TakeutiZaring] p. 93.

Hypotheses

Ref	Expression
fodomb.1	|- A e. V
fodomb.2	|- B e. V

Assertion

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

Distinct variable group(s):   A,f   B,f

Proof of Theorem fodomb

Step	Hyp	Ref	Expression
1		fof 2788	. . . . . . . . . . 11 |- (f:A-onto->B -> f:A-->B)
2		fdm 2756	. . . . . . . . . . 11 |- (f:A-->B -> dom f = A)
3	1, 2	syl 12	. . . . . . . . . 10 |- (f:A-onto->B -> dom f = A)
4	3	cleq1d 1109	. . . . . . . . 9 |- (f:A-onto->B -> (dom f = (/) <-> A = (/)))
5		forn 2789	. . . . . . . . . . 11 |- (f:A-onto->B -> ran f = B)
6	5	cleq1d 1109	. . . . . . . . . 10 |- (f:A-onto->B -> (ran f = (/) <-> B = (/)))
7		dm0rn0 2549	. . . . . . . . . 10 |- (dom f = (/) <-> ran f = (/))
8	6, 7	syl5bb 410	. . . . . . . . 9 |- (f:A-onto->B -> (dom f = (/) <-> B = (/)))
9	4, 8	bitr3d 408	. . . . . . . 8 |- (f:A-onto->B -> (A = (/) <-> B = (/)))
10	9	negbid 463	. . . . . . 7 |- (f:A-onto->B -> (-. A = (/) <-> -. B = (/)))
11	10	biimpcd 137	. . . . . 6 |- (-. A = (/) -> (f:A-onto->B -> -. B = (/)))
12		fodomb.2	. . . . . . 7 |- B e. V
13	12	0sdom 3368	. . . . . 6 |- ((/) ~< B <-> -. B = (/))
14	11, 13	syl6ibr 186	. . . . 5 |- (-. A = (/) -> (f:A-onto->B -> (/) ~< B))
15		fodomb.1	. . . . . . 7 |- A e. V
16	15	fodom 3613	. . . . . 6 |- (f:A-onto->B -> B ~<_ A)
17	16	a1i 7	. . . . 5 |- (-. A = (/) -> (f:A-onto->B -> B ~<_ A))
18	14, 17	jcad 455	. . . 4 |- (-. A = (/) -> (f:A-onto->B -> ((/) ~< B /\ B ~<_ A)))
19	18	19.23adv 954	. . 3 |- (-. A = (/) -> (E.f f:A-onto->B -> ((/) ~< B /\ B ~<_ A)))
20	19	imp 277	. 2 |- ((-. A = (/) /\ E.f f:A-onto->B) -> ((/) ~< B /\ B ~<_ A))
21		sdomdomtr 3370	. . . . 5 |- (A e. V -> (((/) ~< B /\ B ~<_ A) -> (/) ~< A))
22	15, 21	ax-mp 6	. . . 4 |- (((/) ~< B /\ B ~<_ A) -> (/) ~< A)
23	15	0sdom 3368	. . . 4 |- ((/) ~< A <-> -. A = (/))
24	22, 23	sylib 173	. . 3 |- (((/) ~< B /\ B ~<_ A) -> -. A = (/))
25		df-f1 2435	. . . . . . . . . . . . . . . . 17 |- (g:B-1-1->A <-> (g:B-->A /\ Fun `'g))
26	25	pm3.27bd 263	. . . . . . . . . . . . . . . 16 |- (g:B-1-1->A -> Fun `'g)
27		visset 1350	. . . . . . . . . . . . . . . . . 18 |- z e. V
28	27	fconst 2774	. . . . . . . . . . . . . . . . 17 |- ((A \ ran g) X. {z}):(A \ ran g)-->{z}
29		ffun 2754	. . . . . . . . . . . . . . . . 17 |- (((A \ ran g) X. {z}):(A \ ran g)-->{z} -> Fun ((A \ ran g) X. {z}))
30	28, 29	ax-mp 6	. . . . . . . . . . . . . . . 16 |- Fun ((A \ ran g) X. {z})
31	26, 30	jctir 241	. . . . . . . . . . . . . . 15 |- (g:B-1-1->A -> (Fun `'g /\ Fun ((A \ ran g) X. {z})))
32		df-rn 2429	. . . . . . . . . . . . . . . . . . 19 |- ran g = dom `'g
33	32	cleqcomi 1105	. . . . . . . . . . . . . . . . . 18 |- dom `'g = ran g
34	27	snnz 1846	. . . . . . . . . . . . . . . . . . 19 |- -. {z} = (/)
35		dmxp 2552	. . . . . . . . . . . . . . . . . . 19 |- (-. {z} = (/) -> dom ((A \ ran g) X. {z}) = (A \ ran g))
36	34, 35	ax-mp 6	. . . . . . . . . . . . . . . . . 18 |- dom ((A \ ran g) X. {z}) = (A \ ran g)
37	33, 36	ineq12i 1643	. . . . . . . . . . . . . . . . 17 |- (dom `'g i^i dom ((A \ ran g) X. {z})) = (ran g i^i (A \ ran g))
38		difdisj 1758	. . . . . . . . . . . . . . . . 17 |- (ran g i^i (A \ ran g)) = (/)
39	37, 38	eqtr 1119	. . . . . . . . . . . . . . . 16 |- (dom `'g i^i dom ((A \ ran g) X. {z})) = (/)
40		funun 2700	. . . . . . . . . . . . . . . 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})))
41	39, 40	mpan2 519	. . . . . . . . . . . . . . 15 |- ((Fun `'g /\ Fun ((A \ ran g) X. {z})) -> Fun (`'g u. ((A \ ran g) X. {z})))
42	31, 41	syl 12	. . . . . . . . . . . . . 14 |- (g:B-1-1->A -> Fun (`'g u. ((A \ ran g) X. {z})))
43	42	adantl 305	. . . . . . . . . . . . 13 |- ((z e. B /\ g:B-1-1->A) -> Fun (`'g u. ((A \ ran g) X. {z})))
44		f1f 2781	. . . . . . . . . . . . . . . . 17 |- (g:B-1-1->A -> g:B-->A)
45		frn 2757	. . . . . . . . . . . . . . . . 17 |- (g:B-->A -> ran g (_ A)
46	44, 45	syl 12	. . . . . . . . . . . . . . . 16 |- (g:B-1-1->A -> ran g (_ A)
47		ssundif 1764	. . . . . . . . . . . . . . . 16 |- (ran g (_ A <-> (ran g u. (A \ ran g)) = A)
48	46, 47	sylib 173	. . . . . . . . . . . . . . 15 |- (g:B-1-1->A -> (ran g u. (A \ ran g)) = A)
49		dmun 2536	. . . . . . . . . . . . . . . 16 |- dom (`'g u. ((A \ ran g) X. {z})) = (dom `'g u. dom ((A \ ran g) X. {z}))
50	32	uneq1i 1607	. . . . . . . . . . . . . . . . 17 |- (ran g u. dom ((A \ ran g) X. {z})) = (dom `'g u. dom ((A \ ran g) X. {z}))
51	36	uneq2i 1608	. . . . . . . . . . . . . . . . 17 |- (ran g u. dom ((A \ ran g) X. {z})) = (ran g u. (A \ ran g))
52	50, 51	eqtr3 1121	. . . . . . . . . . . . . . . 16 |- (dom `'g u. dom ((A \ ran g) X. {z})) = (ran g u. (A \ ran g))
53	49, 52	eqtr 1119	. . . . . . . . . . . . . . 15 |- dom (`'g u. ((A \ ran g) X. {z})) = (ran g u. (A \ ran g))
54	48, 53	syl5eq 1136	. . . . . . . . . . . . . 14 |- (g:B-1-1->A -> dom (`'g u. ((A \ ran g) X. {z})) = A)
55	54	adantl 305	. . . . . . . . . . . . 13 |- ((z e. B /\ g:B-1-1->A) -> dom (`'g u. ((A \ ran g) X. {z})) = A)
56	43, 55	jca 236	. . . . . . . . . . . 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))
57		df-fn 2433	. . . . . . . . . . . 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))
58	56, 57	sylibr 175	. . . . . . . . . . 11 |- ((z e. B /\ g:B-1-1->A) -> (`'g u. ((A \ ran g) X. {z})) Fn A)
59		fdm 2756	. . . . . . . . . . . . . . . . 17 |- (g:B-->A -> dom g = B)
60	44, 59	syl 12	. . . . . . . . . . . . . . . 16 |- (g:B-1-1->A -> dom g = B)
61		dfdm4 2525	. . . . . . . . . . . . . . . 16 |- dom g = ran `'g
62	60, 61	syl5eqr 1138	. . . . . . . . . . . . . . 15 |- (g:B-1-1->A -> ran `'g = B)
63	62	uneq1d 1610	. . . . . . . . . . . . . 14 |- (g:B-1-1->A -> (ran `'g u. ran ((A \ ran g) X. {z})) = (B u. ran ((A \ ran g) X. {z})))
64	63	adantl 305	. . . . . . . . . . . . 13 |- ((z e. B /\ g:B-1-1->A) -> (ran `'g u. ran ((A \ ran g) X. {z})) = (B u. ran ((A \ ran g) X. {z})))
65		0ss 1725	. . . . . . . . . . . . . . . . . 18 |- (/) (_ B
66		xpeq1 2440	. . . . . . . . . . . . . . . . . . . . . 22 |- ((A \ ran g) = (/) -> ((A \ ran g) X. {z}) = ((/) X. {z}))
67		xp0r 2474	. . . . . . . . . . . . . . . . . . . . . 22 |- ((/) X. {z}) = (/)
68	66, 67	syl6eq 1140	. . . . . . . . . . . . . . . . . . . . 21 |- ((A \ ran g) = (/) -> ((A \ ran g) X. {z}) = (/))
69	68	rneqd 2557	. . . . . . . . . . . . . . . . . . . 20 |- ((A \ ran g) = (/) -> ran ((A \ ran g) X. {z}) = ran (/))
70		rn0 2567	. . . . . . . . . . . . . . . . . . . 20 |- ran (/) = (/)
71	69, 70	syl6eq 1140	. . . . . . . . . . . . . . . . . . 19 |- ((A \ ran g) = (/) -> ran ((A \ ran g) X. {z}) = (/))
72	71	sseq1d 1527	. . . . . . . . . . . . . . . . . 18 |- ((A \ ran g) = (/) -> (ran ((A \ ran g) X. {z}) (_ B <-> (/) (_ B))
73	65, 72	mpbiri 169	. . . . . . . . . . . . . . . . 17 |- ((A \ ran g) = (/) -> ran ((A \ ran g) X. {z}) (_ B)
74	73	a1d 14	. . . . . . . . . . . . . . . 16 |- ((A \ ran g) = (/) -> (z e. B -> ran ((A \ ran g) X. {z}) (_ B))
75		rnxp 2657	. . . . . . . . . . . . . . . . . . 19 |- (-. (A \ ran g) = (/) -> ran ((A \ ran g) X. {z}) = {z})
76	75	adantr 306	. . . . . . . . . . . . . . . . . 18 |- ((-. (A \ ran g) = (/) /\ z e. B) -> ran ((A \ ran g) X. {z}) = {z})
77		snssi 1851	. . . . . . . . . . . . . . . . . . 19 |- (z e. B -> {z} (_ B)
78	77	adantl 305	. . . . . . . . . . . . . . . . . 18 |- ((-. (A \ ran g) = (/) /\ z e. B) -> {z} (_ B)
79	76, 78	eqsstrd 1534	. . . . . . . . . . . . . . . . 17 |- ((-. (A \ ran g) = (/) /\ z e. B) -> ran ((A \ ran g) X. {z}) (_ B)
80	79	exp 291	. . . . . . . . . . . . . . . 16 |- (-. (A \ ran g) = (/) -> (z e. B -> ran ((A \ ran g) X. {z}) (_ B))
81	74, 80	pm2.61i 110	. . . . . . . . . . . . . . 15 |- (z e. B -> ran ((A \ ran g) X. {z}) (_ B)
82		ssequn2 1631	. . . . . . . . . . . . . . 15 |- (ran ((A \ ran g) X. {z}) (_ B <-> (B u. ran ((A \ ran g) X. {z})) = B