Theorem dff3 4790

Description: Alternate definition of a mapping.

Assertion

Ref	Expression
dff3	|- (F:A-->B <-> (F C_ (A X. B) /\ A.x e. A E!y xFy))

Distinct variable groups:   x,y,A   x,B,y   x,F,y

Proof of Theorem dff3

Step	Hyp	Ref	Expression
1		fssxp 4575	. . 3 |- (F:A-->B -> F C_ (A X. B))
2		eu5 1805	. . . . 5 |- (E!y xFy <-> (E.y xFy /\ E*y xFy))
3		ffun 4565	. . . . . . . . 9 |- (F:A-->B -> Fun F)
4	3	adantr 425	. . . . . . . 8 |- ((F:A-->B /\ x e. A) -> Fun F)
5		fdm 4567	. . . . . . . . . 10 |- (F:A-->B -> dom F = A)
6	5	eleq2d 1964	. . . . . . . . 9 |- (F:A-->B -> (x e. dom F <-> x e. A))
7	6	biimpar 461	. . . . . . . 8 |- ((F:A-->B /\ x e. A) -> x e. dom F)
8		funfvop 4776	. . . . . . . 8 |- ((Fun F /\ x e. dom F) -> <.x, (F` x)>. e. F)
9	4, 7, 8	syl11anc 524	. . . . . . 7 |- ((F:A-->B /\ x e. A) -> <.x, (F` x)>. e. F)
10		df-br 3339	. . . . . . 7 |- (xF(F` x) <-> <.x, (F` x)>. e. F)
11	9, 10	sylibr 217	. . . . . 6 |- ((F:A-->B /\ x e. A) -> xF(F` x))
12		fvex 4689	. . . . . . 7 |- (F` x) e. _V
13		breq2 3342	. . . . . . 7 |- (y = (F` x) -> (xFy <-> xF(F` x)))
14	12, 13	cla4ev 2371	. . . . . 6 |- (xF(F` x) -> E.y xFy)
15	11, 14	syl 12	. . . . 5 |- ((F:A-->B /\ x e. A) -> E.y xFy)
16		funmo 4437	. . . . . . 7 |- (Fun F -> E*y xFy)
17	3, 16	syl 12	. . . . . 6 |- (F:A-->B -> E*y xFy)
18	17	adantr 425	. . . . 5 |- ((F:A-->B /\ x e. A) -> E*y xFy)
19	2, 15, 18	sylanbrc 527	. . . 4 |- ((F:A-->B /\ x e. A) -> E!y xFy)
20	19	r19.21aiva 2176	. . 3 |- (F:A-->B -> A.x e. A E!y xFy)
21	1, 20	jca 310	. 2 |- (F:A-->B -> (F C_ (A X. B) /\ A.x e. A E!y xFy))
22		df-f 4010	. . 3 |- (F:A-->B <-> (F Fn A /\ ran F C_ B))
23		df-fn 4009	. . . 4 |- (F Fn A <-> (Fun F /\ dom F = A))
24		dffun6 4436	. . . . 5 |- (Fun F <-> (Rel F /\ A.xE*y xFy))
25		xpss 4056	. . . . . . . 8 |- (A X. B) C_ (_V X. _V)
26		sstr 2625	. . . . . . . 8 |- ((F C_ (A X. B) /\ (A X. B) C_ (_V X. _V)) -> F C_ (_V X. _V))
27	25, 26	mpan2 760	. . . . . . 7 |- (F C_ (A X. B) -> F C_ (_V X. _V))
28		df-rel 4001	. . . . . . 7 |- (Rel F <-> F C_ (_V X. _V))
29	27, 28	sylibr 217	. . . . . 6 |- (F C_ (A X. B) -> Rel F)
30	29	adantr 425	. . . . 5 |- ((F C_ (A X. B) /\ A.x e. A E!y xFy) -> Rel F)
31		eumo 1807	. . . . . . . . . . . 12 |- (E!y xFy -> E*y xFy)
32	31	imim2i 11	. . . . . . . . . . 11 |- ((x e. A -> E!y xFy) -> (x e. A -> E*y xFy))
33	32	adantl 424	. . . . . . . . . 10 |- ((F C_ (A X. B) /\ (x e. A -> E!y xFy)) -> (x e. A -> E*y xFy))
34		ssel 2615	. . . . . . . . . . . . . . . 16 |- (F C_ (A X. B) -> (<.x, y>. e. F -> <.x, y>. e. (A X. B)))
35		df-br 3339	. . . . . . . . . . . . . . . 16 |- (xFy <-> <.x, y>. e. F)
36	34, 35	syl5ib 223	. . . . . . . . . . . . . . 15 |- (F C_ (A X. B) -> (xFy -> <.x, y>. e. (A X. B)))
37		visset 2295	. . . . . . . . . . . . . . . . 17 |- y e. _V
38	37	opelxp 4036	. . . . . . . . . . . . . . . 16 |- (<.x, y>. e. (A X. B) <-> (x e. A /\ y e. B))
39	38	simplbi 349	. . . . . . . . . . . . . . 15 |- (<.x, y>. e. (A X. B) -> x e. A)
40	36, 39	syl6 25	. . . . . . . . . . . . . 14 |- (F C_ (A X. B) -> (xFy -> x e. A))
41	40	19.23adv 1584	. . . . . . . . . . . . 13 |- (F C_ (A X. B) -> (E.y xFy -> x e. A))
42	41	con3d 111	. . . . . . . . . . . 12 |- (F C_ (A X. B) -> (-. x e. A -> -. E.y xFy))
43		exmo 1812	. . . . . . . . . . . . 13 |- (E.y xFy \/ E*y xFy)
44	43	ori 247	. . . . . . . . . . . 12 |- (-. E.y xFy -> E*y xFy)
45	42, 44	syl6 25	. . . . . . . . . . 11 |- (F C_ (A X. B) -> (-. x e. A -> E*y xFy))
46	45	adantr 425	. . . . . . . . . 10 |- ((F C_ (A X. B) /\ (x e. A -> E!y xFy)) -> (-. x e. A -> E*y xFy))
47	33, 46	pm2.61d 141	. . . . . . . . 9 |- ((F C_ (A X. B) /\ (x e. A -> E!y xFy)) -> E*y xFy)
48	47	ex 402	. . . . . . . 8 |- (F C_ (A X. B) -> ((x e. A -> E!y xFy) -> E*y xFy))
49	48	alimdv 1668	. . . . . . 7 |- (F C_ (A X. B) -> (A.x(x e. A -> E!y xFy) -> A.xE*y xFy))
50		df-ral 2109	. . . . . . 7 |- (A.x e. A E!y xFy <-> A.x(x e. A -> E!y xFy))
51	49, 50	syl5ib 223	. . . . . 6 |- (F C_ (A X. B) -> (A.x e. A E!y xFy -> A.xE*y xFy))
52	51	imp 377	. . . . 5 |- ((F C_ (A X. B) /\ A.x e. A E!y xFy) -> A.xE*y xFy)
53	24, 30, 52	sylanbrc 527	. . . 4 |- ((F C_ (A X. B) /\ A.x e. A E!y xFy) -> Fun F)
54		sstr 2625	. . . . . . 7 |- ((dom F C_ dom ( A X. B) /\ dom ( A X. B) C_ A) -> dom F C_ A)
55		dmss 4156	. . . . . . 7 |- (F C_ (A X. B) -> dom F C_ dom ( A X. B))
56		dmxpss 4343	. . . . . . 7 |- dom ( A X. B) C_ A
57	54, 55, 56	sylancl 525	. . . . . 6 |- (F C_ (A X. B) -> dom F C_ A)
58		breq1 3341	. . . . . . . . . 10 |- (x = z -> (xFy <-> zFy))
59	58	eubidv 1779	. . . . . . . . 9 |- (x = z -> (E!y xFy <-> E!y zFy))
60	59	rcla4cv 2377	. . . . . . . 8 |- (A.x e. A E!y xFy -> (z e. A -> E!y zFy))
61		euex 1788	. . . . . . . . 9 |- (E!y zFy -> E.y zFy)
62		visset 2295	. . . . . . . . . 10 |- z e. _V
63	62	eldm 4153	. . . . . . . . 9 |- (z e. dom F <-> E.y zFy)
64	61, 63	sylibr 217	. . . . . . . 8 |- (E!y zFy -> z e. dom F)
65	60, 64	syl6 25	. . . . . . 7 |- (A.x e. A E!y xFy -> (z e. A -> z e. dom F))
66	65	ssrdv 2622	. . . . . 6 |- (A.x e. A E!y xFy -> A C_ dom F)
67	57, 66	anim12i 360	. . . . 5 |- ((F C_ (A X. B) /\ A.x e. A E!y xFy) -> (dom F C_ A /\ A C_ dom F))
68		eqss 2631	. . . . 5 |- (dom F = A <-> (dom F C_ A /\ A C_ dom F))
69	67, 68	sylibr 217	. . . 4 |- ((F C_ (A X. B) /\ A.x e. A E!y xFy) -> dom F = A)
70	23, 53, 69	sylanbrc 527	. . 3 |- ((F C_ (A X. B) /\ A.x e. A E!y xFy) -> F Fn A)
71		sstr 2625	. . . . 5 |- ((ran F C_ ran ( A X. B) /\ ran ( A X. B) C_ B) -> ran F C_ B)
72		rnss 4189	. . . . 5 |- (F C_ (A X. B) -> ran F C_ ran ( A X. B))
73		rnxpss 4344	. . . . 5 |- ran ( A X. B) C_ B
74	71, 72, 73	sylancl 525	. . . 4 |- (F C_ (A X. B) -> ran F C_ B)
75	74	adantr 425	. . 3 |- ((F C_ (A X. B) /\ A.x e. A E!y xFy) -> ran F C_ B)
76	22, 70, 75	sylanbrc 527	. 2 |- ((F C_ (A X. B) /\ A.x e. A E!y xFy) -> F:A-->B)
77	21, 76	impbii 174	1 |- (F:A-->B <-> (F C_ (A X. B) /\ A.x e. A E!y xFy))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 163   /\ wa 240  A.wal 1296   = wceq 1298   e. wcel 1300  E.wex 1326  E!weu 1771  E*wmo 1772  A.wral 2105  _Vcvv 2292   C_ wss 2593  <.cop 3046   class class class wbr 3338   X. cxp 3984  dom cdm 3986  ran crn 3987  Rel wrel 3991  Fun wfun 3992   Fn wfn 3993  -->wf 3994  ` cfv 3998

This theorem is referenced by:  dff4 4791

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-ral 2109  df-rex 2110  df-v 2294  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-nul 2876  df-pw 3035  df-sn 3049  df-pr 3050  df-op 3053  df-uni 3178  df-br 3339  df-opab 3396  df-id 3586  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fun 4008  df-fn 4009  df-f 4010  df-fv 4014

Copyright terms: Public domain