Theorem dff2 3802

Description: Alternate definition of a mapping.

Assertion

Ref	Expression
dff2	|- (F:A-->B <-> (F (_ (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 dff2

Step	Hyp	Ref	Expression
1		fssxp 3622	. . 3 |- (F:A-->B -> F (_ (A X. B))
2		funfvop 3788	. . . . . . . . 9 |- ((Fun F /\ x e. dom F) -> <.x, (F` x)>. e. F)
3		ffun 3615	. . . . . . . . . 10 |- (F:A-->B -> Fun F)
4	3	adantr 389	. . . . . . . . 9 |- ((F:A-->B /\ x e. A) -> Fun F)
5		fdm 3617	. . . . . . . . . . 11 |- (F:A-->B -> dom F = A)
6	5	eleq2d 1533	. . . . . . . . . 10 |- (F:A-->B -> (x e. dom F <-> x e. A))
7	6	biimpar 417	. . . . . . . . 9 |- ((F:A-->B /\ x e. A) -> x e. dom F)
8	2, 4, 7	sylanc 471	. . . . . . . 8 |- ((F:A-->B /\ x e. A) -> <.x, (F` x)>. e. F)
9		df-br 2610	. . . . . . . 8 |- (xF(F` x) <-> <.x, (F` x)>. e. F)
10	8, 9	sylibr 200	. . . . . . 7 |- ((F:A-->B /\ x e. A) -> xF(F` x))
11		fvex 3717	. . . . . . . 8 |- (F` x) e. V
12		breq2 2613	. . . . . . . 8 |- (y = (F` x) -> (xFy <-> xF(F` x)))
13	11, 12	cla4ev 1860	. . . . . . 7 |- (xF(F` x) -> E.y xFy)
14	10, 13	syl 10	. . . . . 6 |- ((F:A-->B /\ x e. A) -> E.y xFy)
15		funmo 3518	. . . . . . . 8 |- (Fun F -> E*y xFy)
16	3, 15	syl 10	. . . . . . 7 |- (F:A-->B -> E*y xFy)
17	16	adantr 389	. . . . . 6 |- ((F:A-->B /\ x e. A) -> E*y xFy)
18	14, 17	jca 288	. . . . 5 |- ((F:A-->B /\ x e. A) -> (E.y xFy /\ E*y xFy))
19		eu5 1402	. . . . 5 |- (E!y xFy <-> (E.y xFy /\ E*y xFy))
20	18, 19	sylibr 200	. . . 4 |- ((F:A-->B /\ x e. A) -> E!y xFy)
21	20	r19.21aiva 1706	. . 3 |- (F:A-->B -> A.x e. A E!y xFy)
22	1, 21	jca 288	. 2 |- (F:A-->B -> (F (_ (A X. B) /\ A.x e. A E!y xFy))
23		xpss 3220	. . . . . . . . . . 11 |- (A X. B) (_ (V X. V)
24		sstr 2062	. . . . . . . . . . 11 |- ((F (_ (A X. B) /\ (A X. B) (_ (V X. V)) -> F (_ (V X. V))
25	23, 24	mpan2 694	. . . . . . . . . 10 |- (F (_ (A X. B) -> F (_ (V X. V))
26		df-rel 3175	. . . . . . . . . 10 |- (Rel F <-> F (_ (V X. V))
27	25, 26	sylibr 200	. . . . . . . . 9 |- (F (_ (A X. B) -> Rel F)
28	27	adantr 389	. . . . . . . 8 |- ((F (_ (A X. B) /\ A.x e. A E!y xFy) -> Rel F)
29		eumo 1404	. . . . . . . . . . . . . . 15 |- (E!y xFy -> E*y xFy)
30	29	imim2i 17	. . . . . . . . . . . . . 14 |- ((x e. A -> E!y xFy) -> (x e. A -> E*y xFy))
31	30	adantl 388	. . . . . . . . . . . . 13 |- ((F (_ (A X. B) /\ (x e. A -> E!y xFy)) -> (x e. A -> E*y xFy))
32		ssel 2053	. . . . . . . . . . . . . . . . . . 19 |- (F (_ (A X. B) -> (<.x, y>. e. F -> <.x, y>. e. (A X. B)))
33		df-br 2610	. . . . . . . . . . . . . . . . . . 19 |- (xFy <-> <.x, y>. e. F)
34	32, 33	syl5ib 206	. . . . . . . . . . . . . . . . . 18 |- (F (_ (A X. B) -> (xFy -> <.x, y>. e. (A X. B)))
35		visset 1804	. . . . . . . . . . . . . . . . . . . 20 |- y e. V
36	35	opelxp 3204	. . . . . . . . . . . . . . . . . . 19 |- (<.x, y>. e. (A X. B) <-> (x e. A /\ y e. B))
37	36	pm3.26bi 322	. . . . . . . . . . . . . . . . . 18 |- (<.x, y>. e. (A X. B) -> x e. A)
38	34, 37	syl6 22	. . . . . . . . . . . . . . . . 17 |- (F (_ (A X. B) -> (xFy -> x e. A))
39	38	19.23adv 1209	. . . . . . . . . . . . . . . 16 |- (F (_ (A X. B) -> (E.y xFy -> x e. A))
40	39	con3d 95	. . . . . . . . . . . . . . 15 |- (F (_ (A X. B) -> (-. x e. A -> -. E.y xFy))
41		exmo 1409	. . . . . . . . . . . . . . . 16 |- (E.y xFy \/ E*y xFy)
42	41	ori 230	. . . . . . . . . . . . . . 15 |- (-. E.y xFy -> E*y xFy)
43	40, 42	syl6 22	. . . . . . . . . . . . . 14 |- (F (_ (A X. B) -> (-. x e. A -> E*y xFy))
44	43	adantr 389	. . . . . . . . . . . . 13 |- ((F (_ (A X. B) /\ (x e. A -> E!y xFy)) -> (-. x e. A -> E*y xFy))
45	31, 44	pm2.61d 127	. . . . . . . . . . . 12 |- ((F (_ (A X. B) /\ (x e. A -> E!y xFy)) -> E*y xFy)
46	45	ex 373	. . . . . . . . . . 11 |- (F (_ (A X. B) -> ((x e. A -> E!y xFy) -> E*y xFy))
47	46	19.20dv 1284	. . . . . . . . . 10 |- (F (_ (A X. B) -> (A.x(x e. A -> E!y xFy) -> A.xE*y xFy))
48		df-ral 1641	. . . . . . . . . 10 |- (A.x e. A E!y xFy <-> A.x(x e. A -> E!y xFy))
49	47, 48	syl5ib 206	. . . . . . . . 9 |- (F (_ (A X. B) -> (A.x e. A E!y xFy -> A.xE*y xFy))
50	49	imp 350	. . . . . . . 8 |- ((F (_ (A X. B) /\ A.x e. A E!y xFy) -> A.xE*y xFy)
51	28, 50	jca 288	. . . . . . 7 |- ((F (_ (A X. B) /\ A.x e. A E!y xFy) -> (Rel F /\ A.xE*y xFy))
52		dffunmo 3517	. . . . . . 7 |- (Fun F <-> (Rel F /\ A.xE*y xFy))
53	51, 52	sylibr 200	. . . . . 6 |- ((F (_ (A X. B) /\ A.x e. A E!y xFy) -> Fun F)
54		dmss 3299	. . . . . . . . 9 |- (F (_ (A X. B) -> dom F (_ dom ( A X. B))
55		dmxpss 3459	. . . . . . . . . 10 |- dom ( A X. B) (_ A
56		sstr 2062	. . . . . . . . . 10 |- ((dom F (_ dom ( A X. B) /\ dom ( A X. B) (_ A) -> dom F (_ A)
57	55, 56	mpan2 694	. . . . . . . . 9 |- (dom F (_ dom ( A X. B) -> dom F (_ A)
58	54, 57	syl 10	. . . . . . . 8 |- (F (_ (A X. B) -> dom F (_ A)
59		breq1 2612	. . . . . . . . . . . 12 |- (x = z -> (xFy <-> zFy))
60	59	eubidv 1379	. . . . . . . . . . 11 |- (x = z -> (E!y xFy <-> E!y zFy))
61	60	rcla4cv 1865	. . . . . . . . . 10 |- (A.x e. A E!y xFy -> (z e. A -> E!y zFy))
62		euex 1387	. . . . . . . . . . 11 |- (E!y zFy -> E.y zFy)
63		visset 1804	. . . . . . . . . . . 12 |- z e. V
64	63	eldm 3296	. . . . . . . . . . 11 |- (z e. dom F <-> E.y zFy)
65	62, 64	sylibr 200	. . . . . . . . . 10 |- (E!y zFy -> z e. dom F)
66	61, 65	syl6 22	. . . . . . . . 9 |- (A.x e. A E!y xFy -> (z e. A -> z e. dom F))
67	66	ssrdv 2060	. . . . . . . 8 |- (A.x e. A E!y xFy -> A (_ dom F)
68	58, 67	anim12i 333	. . . . . . 7 |- ((F (_ (A X. B) /\ A.x e. A E!y xFy) -> (dom F (_ A /\ A (_ dom F))
69		eqss 2067	. . . . . . 7 |- (dom F = A <-> (dom F (_ A /\ A (_ dom F))
70	68, 69	sylibr 200	. . . . . 6 |- ((F (_ (A X. B) /\ A.x e. A E!y xFy) -> dom F = A)
71	53, 70	jca 288	. . . . 5 |- ((F (_ (A X. B) /\ A.x e. A E!y xFy) -> (Fun F /\ dom F = A))
72		df-fn 3183	. . . . 5 |- (F Fn A <-> (Fun F /\ dom F = A))
73	71, 72	sylibr 200	. . . 4 |- ((F (_ (A X. B) /\ A.x e. A E!y xFy) -> F Fn A)
74		rnss 3331	. . . . . 6 |- (F (_ (A X. B) -> ran F (_ ran ( A X. B))
75		rnxpss 3460	. . . . . . 7 |- ran ( A X. B) (_ B
76		sstr 2062	. . . . . . 7 |- ((ran F (_ ran ( A X. B) /\ ran ( A X. B) (_ B) -> ran F (_ B)
77	75, 76	mpan2 694	. . . . . 6 |- (ran F (_ ran ( A X. B) -> ran F (_ B)
78	74, 77	syl 10	. . . . 5 |- (F (_ (A X. B) -> ran F (_ B)
79	78	adantr 389	. . . 4 |- ((F (_ (A X. B) /\ A.x e. A E!y xFy) -> ran F (_ B)
80	73, 79	jca 288	. . 3 |- ((F (_ (A X. B) /\ A.x e. A E!y xFy) -> (F Fn A /\ ran F (_ B))
81		df-f 3184	. . 3 |- (F:A-->B <-> (F Fn A /\ ran F (_ B))
82	80, 81	sylibr 200	. 2 |- ((F (_ (A X. B) /\ A.x e. A E!y xFy) -> F:A-->B)
83	22, 82	impbi 157	1 |- (F:A-->B <-> (F (_ (A X. B) /\ A.x e. A E!y xFy))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 146   /\ wa 223  A.wal 951   = wceq 953   e. wcel 955  E.wex 977  E!weu 1373  E*wmo 1374  A.wral 1637  Vcvv 1802   (_ wss 2037  <.cop 2401   class class class wbr 2609   X. cxp 3158  dom cdm 3160  ran crn 3161  Rel wrel 3165  Fun wfun 3166   Fn wfn 3167  -->wf 3168  ` cfv 3172

This theorem is referenced by:  dff3 3803

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-9 962  ax-10 963  ax-11 964  ax-12 965  ax-13 966  ax-14 967  ax-17 <