Theorem fopab2 3899

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		elisset 1855	. . . . . . 7 |- (C e. B -> C e. V)
2		eueq 1954	. . . . . . 7 |- (C e. V <-> E!y y = C)
3	1, 2	sylib 196	. . . . . 6 |- (C e. B -> E!y y = C)
4	3	r19.20si 1744	. . . . 5 |- (A.x e. A C e. B -> A.x e. A E!y y = C)
5		fopab2.1	. . . . . 6 |- F = {<.x, y>. | (x e. A /\ y = C)}
6	5	fnopabg 3690	. . . . 5 |- (A.x e. A E!y y = C <-> F Fn A)
7	4, 6	sylib 196	. . . 4 |- (A.x e. A C e. B -> F Fn A)
8		hbra1 1725	. . . . . . . . 9 |- (A.x e. A C e. B -> A.xA.x e. A C e. B)
9		ax-17 1003	. . . . . . . . 9 |- (y e. B -> A.x y e. B)
10		ra4 1732	. . . . . . . . . 10 |- (A.x e. A C e. B -> (x e. A -> C e. B))
11		eleq1a 1580	. . . . . . . . . . . 12 |- (C e. B -> (y = C -> y e. B))
12	11	imim2i 17	. . . . . . . . . . 11 |- ((x e. A -> C e. B) -> (x e. A -> (y = C -> y e. B)))
13	12	imp3a 359	. . . . . . . . . 10 |- ((x e. A -> C e. B) -> ((x e. A /\ y = C) -> y e. B))
14	10, 13	syl 10	. . . . . . . . 9 |- (A.x e. A C e. B -> ((x e. A /\ y = C) -> y e. B))
15	8, 9, 14	19.23ad 1098	. . . . . . . 8 |- (A.x e. A C e. B -> (E.x(x e. A /\ y = C) -> y e. B))
16		rnopab 3413	. . . . . . . . 9 |- ran {<.x, y>. | (x e. A /\ y = C)} = {y | E.x(x e. A /\ y = C)}
17	16	abeq2i 1607	. . . . . . . 8 |- (y e. ran {<.x, y>. | (x e. A /\ y = C)} <-> E.x(x e. A /\ y = C))
18	15, 17	syl5ib 204	. . . . . . 7 |- (A.x e. A C e. B -> (y e. ran {<.x, y>. | (x e. A /\ y = C)} -> y e. B))
19	18	19.21aiv 1319	. . . . . 6 |- (A.x e. A C e. B -> A.y(y e. ran {<.x, y>. | (x e. A /\ y = C)} -> y e. B))
20		hbopab2 2867	. . . . . . . 8 |- (z e. {<.x, y>. | (x e. A /\ y = C)} -> A.y z e. {<.x, y>. | (x e. A /\ y = C)})
21	20	hbrn 3411	. . . . . . 7 |- (z e. ran {<.x, y>. | (x e. A /\ y = C)} -> A.y z e. ran {<.x, y>. | (x e. A /\ y = C)})
22		ax-17 1003	. . . . . . 7 |- (z e. B -> A.y z e. B)
23	21, 22	dfss2f 2104	. . . . . 6 |- (ran {<.x, y>. | (x e. A /\ y = C)} (_ B <-> A.y(y e. ran {<.x, y>. | (x e. A /\ y = C)} -> y e. B))
24	19, 23	sylibr 198	. . . . 5 |- (A.x e. A C e. B -> ran {<.x, y>. | (x e. A /\ y = C)} (_ B)
25	5	rneqi 3400	. . . . 5 |- ran F = ran {<.x, y>. | (x e. A /\ y = C)}
26	24, 25	syl5ss 2149	. . . 4 |- (A.x e. A C e. B -> ran F (_ B)
27	7, 26	jca 286	. . 3 |- (A.x e. A C e. B -> (F Fn A /\ ran F (_ B))
28		df-f 3249	. . 3 |- (F:A-->B <-> (F Fn A /\ ran F (_ B))
29	27, 28	sylibr 198	. 2 |- (A.x e. A C e. B -> F:A-->B)
30		fdm 3706	. . . 4 |- (F:A-->B -> dom F = A)
31		dmopab3 3386	. . . . 5 |- (A.x e. A E.y y = C <-> dom {<.x, y>. | (x e. A /\ y = C)} = A)
32		isset 1852	. . . . . 6 |- (C e. V <-> E.y y = C)
33	32	ralbii 1705	. . . . 5 |- (A.x e. A C e. V <-> A.x e. A E.y y = C)
34	5	dmeqi 3376	. . . . . 6 |- dom F = dom {<.x, y>. | (x e. A /\ y = C)}
35	34	eqeq1i 1519	. . . . 5 |- (dom F = A <-> dom {<.x, y>. | (x e. A /\ y = C)} = A)
36	31, 33, 35	3bitr4ri 182	. . . 4 |- (dom F = A <-> A.x e. A C e. V)
37	30, 36	sylib 196	. . 3 |- (F:A-->B -> A.x e. A C e. V)
38		hbopab1 2866	. . . . . 6 |- (z e. {<.x, y>. | (x e. A /\ y = C)} -> A.x z e. {<.x, y>. | (x e. A /\ y = C)})
39		ax-17 1003	. . . . . 6 |- (z e. A -> A.x z e. A)
40		ax-17 1003	. . . . . 6 |- (z e. B -> A.x z e. B)
41	38, 39, 40	hbf 3700	. . . . 5 |- ({<.x, y>. | (x e. A /\ y = C)}:A-->B -> A.x{<.x, y>. | (x e. A /\ y = C)}:A-->B)
42		feq1 3695	. . . . . 6 |- (F = {<.x, y>. | (x e. A /\ y = C)} -> (F:A-->B <-> {<.x, y>. | (x e. A /\ y = C)}:A-->B))
43	5, 42	ax-mp 7	. . . . 5 |- (F:A-->B <-> {<.x, y>. | (x e. A /\ y = C)}:A-->B)
44	43	albii 1031	. . . . 5 |- (A.x F:A-->B <-> A.x{<.x, y>. | (x e. A /\ y = C)}:A-->B)
45	41, 43, 44	3imtr4i 217	. . . 4 |- (F:A-->B -> A.x F:A-->B)
46		ffvelrn 3890	. . . . . . 7 |- ((F:A-->B /\ x e. A) -> (F` x) e. B)
47	46	adantr 389	. . . . . 6 |- (((F:A-->B /\ x e. A) /\ C e. V) -> (F` x) e. B)
48		fvopab2 3867	. . . . . . . . 9 |- ((x e. A /\ C e. V) -> ({<.x, y>. | (x e. A /\ y = C)}` x) = C)
49	5	fveq1i 3801	. . . . . . . . 9 |- (F` x) = ({<.x, y>. | (x e. A /\ y = C)}` x)
50	48, 49	syl5eq 1556	. . . . . . . 8 |- ((x e. A /\ C e. V) -> (F` x) = C)
51	50	eleq1d 1577	. . . . . . 7 |- ((x e. A /\ C e. V) -> ((F` x) e. B <-> C e. B))
52	51	adantll 392	. . . . . 6 |- (((F:A-->B /\ x e. A) /\ C e. V) -> ((F` x) e. B <-> C e. B))
53	47, 52	mpbid 193	. . . . 5 |- (((F:A-->B /\ x e. A) /\ C e. V) -> C e. B)
54	53	ex 371	. . . 4 |- ((F:A-->B /\ x e. A) -> (C e. V -> C e. B))
55	45, 54	r19.20da 1746	. . 3 |- (F:A-->B -> (A.x e. A C e. V -> A.x e. A C e. B))
56	37, 55	mpd 26	. 2 |- (F:A-->B -> A.x e. A C e. B)
57	29, 56	impbii 155	1 |- (A.x e. A C e. B <-> F:A-->B)

Syntax hints:   -> wi 3   <-> wb 144   /\ wa 221  A.wal 986   = wceq 988   e. wcel 990  E.wex 1012  E!weu 1413  A.wral 1683  Vcvv 1849   (_ wss 2091  {copab 2717  dom cdm 3225  ran crn 3226   Fn wfn 3232  -->wf 3233  ` cfv 3237

This theorem is referenced by:  fopabssxp 3900  rnssopab 3901  fopab3 3902  fopab 3903  f1stres 4171  f2ndres 4172  foprab2 4199  curry1f 4209  dom2d 4491  mapenlem2 4579  xpmapenlem4 4588  ser1cl2i 6626  cvgratlem5 7377  negfcncfi 7392  mulc1cncf 7402  efseq0ex 7434  lmfexlem1 8076  metcnp4 8090  xplmi 8093  xpcn 8096  bopcnlem4 8104  grplactf1o 8217  sqcn 8454  va1cnlem 8464  ipblnfi 8635  ubthlem3 8650  sincolem 8783  occllem4 9296  projlem24 9329  hoaddcl 9804  homulcl 9805  brafn 9989  kbop 9995  cnlnadjlem2 10118  strlem3a 10297  hstrlem3a 10305  cayleylem2 10531  fopab2a 10584

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 994  ax-gen 995  ax-8 996  ax-9 997  ax-10 998  ax-11 999  ax-12 1000  ax-13 1001  ax-14 1002  ax-17 1003  ax-4 1005  ax-5o 1007  ax-6o 1010  ax-9o 1155  ax-10o 1173  ax-16 1243  ax-11o 1251  ax-ext 1494  ax-sep 2754  ax-pow 2794  ax-pr 2832  ax-un 2920

This theorem depends on definitions:  df-bi 145  df-or 222  df-an 223  df-ex 1013  df-sb 1205  df-eu 1415  df-mo 1416  df-clab 1500  df-cleq 1505  df-clel 1508  df-ne 1624  df-ral 1687  df-rex 1688  df-v 1850  df-dif 2093  df-un 2094  df-in 2095  df-ss 2097  df-nul 2325  df-pw 2447  df-sn 2457  df-pr 2458  df-op 2461  df-uni 2552  df-br 2670  df-opab 2718  df-id 2889  df-xp 3239  df-rel 3240  df-cnv 3241  df-co 3242  df-dm 3243  df-rn 3244  df-res 3245  df-ima 3246  df-fun 3247  df-fn 3248  df-f 3249  df-fv 3253

Copyright terms: Public domain