Theorem fopab2 4796

Description: Functionality of an ordered-pair class abstraction.

Hypothesis

Ref	Expression
fopab2.1	|- F = {<.x, y>. | (x e. A /\ y = C)}

Assertion

Ref	Expression
fopab2	|- (A.x e. A C e. B <-> F:A-->B)

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

Proof of Theorem fopab2

Step	Hyp	Ref	Expression
1		df-f 4010	. . 3 |- (F:A-->B <-> (F Fn A /\ ran F C_ B))
2		elisset 2299	. . . . . 6 |- (C e. B -> C e. _V)
3		eueq 2427	. . . . . 6 |- (C e. _V <-> E!y y = C)
4	2, 3	sylib 215	. . . . 5 |- (C e. B -> E!y y = C)
5	4	ralimi 2168	. . . 4 |- (A.x e. A C e. B -> A.x e. A E!y y = C)
6		fopab2.1	. . . . 5 |- F = {<.x, y>. | (x e. A /\ y = C)}
7	6	fnopabg 4546	. . . 4 |- (A.x e. A E!y y = C <-> F Fn A)
8	5, 7	sylib 215	. . 3 |- (A.x e. A C e. B -> F Fn A)
9		hbra1 2147	. . . . . . . 8 |- (A.x e. A C e. B -> A.xA.x e. A C e. B)
10		ax-17 1317	. . . . . . . 8 |- (y e. B -> A.x y e. B)
11		ra4 2155	. . . . . . . . 9 |- (A.x e. A C e. B -> (x e. A -> C e. B))
12		eleq1a 1966	. . . . . . . . . . 11 |- (C e. B -> (y = C -> y e. B))
13	12	imim2i 11	. . . . . . . . . 10 |- ((x e. A -> C e. B) -> (x e. A -> (y = C -> y e. B)))
14	13	imp3a 388	. . . . . . . . 9 |- ((x e. A -> C e. B) -> ((x e. A /\ y = C) -> y e. B))
15	11, 14	syl 12	. . . . . . . 8 |- (A.x e. A C e. B -> ((x e. A /\ y = C) -> y e. B))
16	9, 10, 15	19.23ad 1415	. . . . . . 7 |- (A.x e. A C e. B -> (E.x(x e. A /\ y = C) -> y e. B))
17		rnopab 4201	. . . . . . . 8 |- ran {<.x, y>. | (x e. A /\ y = C)} = {y | E.x(x e. A /\ y = C)}
18	17	abeq2i 2001	. . . . . . 7 |- (y e. ran {<.x, y>. | (x e. A /\ y = C)} <-> E.x(x e. A /\ y = C))
19	16, 18	syl5ib 223	. . . . . 6 |- (A.x e. A C e. B -> (y e. ran {<.x, y>. | (x e. A /\ y = C)} -> y e. B))
20	19	19.21aiv 1664	. . . . 5 |- (A.x e. A C e. B -> A.y(y e. ran {<.x, y>. | (x e. A /\ y = C)} -> y e. B))
21		hbopab2 3563	. . . . . . 7 |- (z e. {<.x, y>. | (x e. A /\ y = C)} -> A.y z e. {<.x, y>. | (x e. A /\ y = C)})
22	21	hbrn 4198	. . . . . 6 |- (z e. ran {<.x, y>. | (x e. A /\ y = C)} -> A.y z e. ran {<.x, y>. | (x e. A /\ y = C)})
23		ax-17 1317	. . . . . 6 |- (z e. B -> A.y z e. B)
24	22, 23	dfss2f 2612	. . . . 5 |- (ran {<.x, y>. | (x e. A /\ y = C)} C_ B <-> A.y(y e. ran {<.x, y>. | (x e. A /\ y = C)} -> y e. B))
25	20, 24	sylibr 217	. . . 4 |- (A.x e. A C e. B -> ran {<.x, y>. | (x e. A /\ y = C)} C_ B)
26	6	rneqi 4187	. . . 4 |- ran F = ran {<.x, y>. | (x e. A /\ y = C)}
27	25, 26	syl5ss 2661	. . 3 |- (A.x e. A C e. B -> ran F C_ B)
28	1, 8, 27	sylanbrc 527	. 2 |- (A.x e. A C e. B -> F:A-->B)
29		fdm 4567	. . . 4 |- (F:A-->B -> dom F = A)
30		dmopab3 4169	. . . . 5 |- (A.x e. A E.y y = C <-> dom {<.x, y>. | (x e. A /\ y = C)} = A)
31		isset 2296	. . . . . 6 |- (C e. _V <-> E.y y = C)
32	31	ralbii 2127	. . . . 5 |- (A.x e. A C e. _V <-> A.x e. A E.y y = C)
33	6	dmeqi 4158	. . . . . 6 |- dom F = dom {<.x, y>. | (x e. A /\ y = C)}
34	33	eqeq1i 1891	. . . . 5 |- (dom F = A <-> dom {<.x, y>. | (x e. A /\ y = C)} = A)
35	30, 32, 34	3bitr4ri 201	. . . 4 |- (dom F = A <-> A.x e. A C e. _V)
36	29, 35	sylib 215	. . 3 |- (F:A-->B -> A.x e. A C e. _V)
37		hbopab1 3562	. . . . . 6 |- (z e. {<.x, y>. | (x e. A /\ y = C)} -> A.x z e. {<.x, y>. | (x e. A /\ y = C)})
38		ax-17 1317	. . . . . 6 |- (z e. A -> A.x z e. A)
39		ax-17 1317	. . . . . 6 |- (z e. B -> A.x z e. B)
40	37, 38, 39	hbf 4560	. . . . 5 |- ({<.x, y>. | (x e. A /\ y = C)}:A-->B -> A.x{<.x, y>. | (x e. A /\ y = C)}:A-->B)
41	6	feq1i 4558	. . . . 5 |- (F:A-->B <-> {<.x, y>. | (x e. A /\ y = C)}:A-->B)
42	41	albii 1346	. . . . 5 |- (A.x F:A-->B <-> A.x{<.x, y>. | (x e. A /\ y = C)}:A-->B)
43	40, 41, 42	3imtr4i 236	. . . 4 |- (F:A-->B -> A.x F:A-->B)
44		ffvelrn 4787	. . . . . . 7 |- ((F:A-->B /\ x e. A) -> (F` x) e. B)
45	44	adantr 425	. . . . . 6 |- (((F:A-->B /\ x e. A) /\ C e. _V) -> (F` x) e. B)
46		fvopab2 4754	. . . . . . . . 9 |- ((x e. A /\ C e. _V) -> ({<.x, y>. | (x e. A /\ y = C)}` x) = C)
47	6	fveq1i 4682	. . . . . . . . 9 |- (F` x) = ({<.x, y>. | (x e. A /\ y = C)}` x)
48	46, 47	syl5eq 1940	. . . . . . . 8 |- ((x e. A /\ C e. _V) -> (F` x) = C)
49	48	eleq1d 1963	. . . . . . 7 |- ((x e. A /\ C e. _V) -> ((F` x) e. B <-> C e. B))
50	49	adantll 428	. . . . . 6 |- (((F:A-->B /\ x e. A) /\ C e. _V) -> ((F` x) e. B <-> C e. B))
51	45, 50	mpbid 212	. . . . 5 |- (((F:A-->B /\ x e. A) /\ C e. _V) -> C e. B)
52	51	ex 402	. . . 4 |- ((F:A-->B /\ x e. A) -> (C e. _V -> C e. B))
53	43, 52	ralimdaa 2170	. . 3 |- (F:A-->B -> (A.x e. A C e. _V -> A.x e. A C e. B))
54	36, 53	mpd 29	. 2 |- (F:A-->B -> A.x e. A C e. B)
55	28, 54	impbii 174	1 |- (A.x e. A C e. B <-> F:A-->B)

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240  A.wal 1296   = wceq 1298   e. wcel 1300  E.wex 1326  E!weu 1771  A.wral 2105  _Vcvv 2292   C_ wss 2593  {copab 3395  dom cdm 3986  ran crn 3987   Fn wfn 3993  -->wf 3994  ` cfv 3998

This theorem is referenced by:  fopabssxp 4797  rnssopab 4798  fopab3 4799  fopab 4800  f1stres 5034  f2ndres 5035  foprab2 5061  curry1f 5076  curry2f 5079  dom2d 5463  mapenlem2 5584  xpmapenlem4 5593  ser1cl2i 7746  cvgratlem5 8516  negfcncfi 8531  mulc1cncf 8541  efseq0ex 8573  lmfexlem1 9234  metcnp4 9248  xplmi 9251  xpcn 9254  bopcnlem4 9262  grplactf1o 9406  sqcn 9674  va1cnlem 9684  ipblnfi 9857  ubthlem3 9874  sincolem 10014  upxp 10225  uptx 10226  txcnopab 10228  occllem4 10809  projlem24 10842  hoaddcl 11321  homulcl 11322  brafn 11508  kbop 11514  cnlnadjlem2 11638  strlem3a 11824  hstrlem3a 11832  cayleylem2 13642  fopab2a 14479  domrancur1b 14548  fnopabco2b 14734  svli2 14826  cntrsetlem 14999  dualalg 15131  upixp 15729  sdclem1 15809  sdc 15811  fdc 15812  geomcau 15849  lmclim2 15850  metdcn 15853  addccncf 15883  sub1cncf 15885  sub2cncf 15886  heiborlem33 15987  rrnmet 16016  rrncms 16019  rrntotbndlem1 16020  rrntotbndlem2 16021  rrntotbnd 16022

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