Theorem upixp 15729

Description: Universal property of the indexed Cartesian product.

Hypotheses

Ref	Expression
upixp.1	|- X = X_b e. A (C` b)
upixp.2	|- P = {<.w, z>. | (w e. A /\ z = {<.x, y>. | (x e. X /\ y = (x` w))})}

Assertion

Ref	Expression
upixp	|- ((A e. R /\ B e. S /\ A.a e. A (F` a):B-->(C` a)) -> E!h(h:B-->X /\ A.a e. A (F` a) = ((P` a) o. h)))

Distinct variable groups:   A,a,b,h,w,x,y,z   R,a,b,h,w,x,y,z   S,a,b,h,w,x,y,z   F,a,b,h,w,x,y,z   B,a,b,h,w,x,y,z   C,a,b,h,w,x,y,z   X,a,h,w,x,y,z   P,a,h

Proof of Theorem upixp

Step	Hyp	Ref	Expression
1		opabex2g 4540	. . . 4 |- (B e. S -> {<.u, v>. | (u e. B /\ v = {<.s, t>. | (s e. A /\ t = ((F` s)` u))})} e. _V)
2		eueq 2427	. . . 4 |- ({<.u, v>. | (u e. B /\ v = {<.s, t>. | (s e. A /\ t = ((F` s)` u))})} e. _V <-> E!h h = {<.u, v>. | (u e. B /\ v = {<.s, t>. | (s e. A /\ t = ((F` s)` u))})})
3	1, 2	sylib 215	. . 3 |- (B e. S -> E!h h = {<.u, v>. | (u e. B /\ v = {<.s, t>. | (s e. A /\ t = ((F` s)` u))})})
4	3	3ad2ant2 898	. 2 |- ((A e. R /\ B e. S /\ A.a e. A (F` a):B-->(C` a)) -> E!h h = {<.u, v>. | (u e. B /\ v = {<.s, t>. | (s e. A /\ t = ((F` s)` u))})})
5		ffn 4562	. . . . . . . 8 |- (h:B-->X -> h Fn B)
6	5	ad2antrl 442	. . . . . . 7 |- (((A e. R /\ B e. S /\ A.a e. A (F` a):B-->(C` a)) /\ (h:B-->X /\ A.a e. A (F` a) = ((P` a) o. h))) -> h Fn B)
7		opabex2g 4540	. . . . . . . . . . . 12 |- (A e. R -> {<.s, t>. | (s e. A /\ t = ((F` s)` u))} e. _V)
8	7	adantr 425	. . . . . . . . . . 11 |- ((A e. R /\ u e. B) -> {<.s, t>. | (s e. A /\ t = ((F` s)` u))} e. _V)
9	8	r19.21aiva 2176	. . . . . . . . . 10 |- (A e. R -> A.u e. B {<.s, t>. | (s e. A /\ t = ((F` s)` u))} e. _V)
10		eqid 1884	. . . . . . . . . . 11 |- {<.u, v>. | (u e. B /\ v = {<.s, t>. | (s e. A /\ t = ((F` s)` u))})} = {<.u, v>. | (u e. B /\ v = {<.s, t>. | (s e. A /\ t = ((F` s)` u))})}
11	10	fnopab2g 4547	. . . . . . . . . 10 |- (A.u e. B {<.s, t>. | (s e. A /\ t = ((F` s)` u))} e. _V <-> {<.u, v>. | (u e. B /\ v = {<.s, t>. | (s e. A /\ t = ((F` s)` u))})} Fn B)
12	9, 11	sylib 215	. . . . . . . . 9 |- (A e. R -> {<.u, v>. | (u e. B /\ v = {<.s, t>. | (s e. A /\ t = ((F` s)` u))})} Fn B)
13	12	3ad2ant1 897	. . . . . . . 8 |- ((A e. R /\ B e. S /\ A.a e. A (F` a):B-->(C` a)) -> {<.u, v>. | (u e. B /\ v = {<.s, t>. | (s e. A /\ t = ((F` s)` u))})} Fn B)
14	13	adantr 425	. . . . . . 7 |- (((A e. R /\ B e. S /\ A.a e. A (F` a):B-->(C` a)) /\ (h:B-->X /\ A.a e. A (F` a) = ((P` a) o. h))) -> {<.u, v>. | (u e. B /\ v = {<.s, t>. | (s e. A /\ t = ((F` s)` u))})} Fn B)
15		eqfnfv 4766	. . . . . . 7 |- ((h Fn B /\ {<.u, v>. | (u e. B /\ v = {<.s, t>. | (s e. A /\ t = ((F` s)` u))})} Fn B) -> (h = {<.u, v>. | (u e. B /\ v = {<.s, t>. | (s e. A /\ t = ((F` s)` u))})} <-> (B = B /\ A.c e. B (h` c) = ({<.u, v>. | (u e. B /\ v = {<.s, t>. | (s e. A /\ t = ((F` s)` u))})}` c))))
16	6, 14, 15	syl11anc 524	. . . . . 6 |- (((A e. R /\ B e. S /\ A.a e. A (F` a):B-->(C` a)) /\ (h:B-->X /\ A.a e. A (F` a) = ((P` a) o. h))) -> (h = {<.u, v>. | (u e. B /\ v = {<.s, t>. | (s e. A /\ t = ((F` s)` u))})} <-> (B = B /\ A.c e. B (h` c) = ({<.u, v>. | (u e. B /\ v = {<.s, t>. | (s e. A /\ t = ((F` s)` u))})}` c))))
17		eqidd 1885	. . . . . 6 |- (((A e. R /\ B e. S /\ A.a e. A (F` a):B-->(C` a)) /\ (h:B-->X /\ A.a e. A (F` a) = ((P` a) o. h))) -> B = B)
18		fveq2 4681	. . . . . . . . . . . . . . . 16 |- (u = c -> ((F` s)` u) = ((F` s)` c))
19	18	eqeq2d 1895	. . . . . . . . . . . . . . 15 |- (u = c -> (t = ((F` s)` u) <-> t = ((F` s)` c)))
20	19	anbi2d 678	. . . . . . . . . . . . . 14 |- (u = c -> ((s e. A /\ t = ((F` s)` u)) <-> (s e. A /\ t = ((F` s)` c))))
21	20	opabbidv 3401	. . . . . . . . . . . . 13 |- (u = c -> {<.s, t>. | (s e. A /\ t = ((F` s)` u))} = {<.s, t>. | (s e. A /\ t = ((F` s)` c))})
22	21, 10	fvopab4g 4742	. . . . . . . . . . . 12 |- ((c e. B /\ {<.s, t>. | (s e. A /\ t = ((F` s)` c))} e. _V) -> ({<.u, v>. | (u e. B /\ v = {<.s, t>. | (s e. A /\ t = ((F` s)` u))})}` c) = {<.s, t>. | (s e. A /\ t = ((F` s)` c))})
23		opabex2g 4540	. . . . . . . . . . . 12 |- (A e. R -> {<.s, t>. | (s e. A /\ t = ((F` s)` c))} e. _V)
24	22, 23	sylan2 500	. . . . . . . . . . 11 |- ((c e. B /\ A e. R) -> ({<.u, v>. | (u e. B /\ v = {<.s, t>. | (s e. A /\ t = ((F` s)` u))})}` c) = {<.s, t>. | (s e. A /\ t = ((F` s)` c))})
25	24	ancoms 484	. . . . . . . . . 10 |- ((A e. R /\ c e. B) -> ({<.u, v>. | (u e. B /\ v = {<.s, t>. | (s e. A /\ t = ((F` s)` u))})}` c) = {<.s, t>. | (s e. A /\ t = ((F` s)` c))})
26	25	3ad2antl1 1038	. . . . . . . . 9 |- (((A e. R /\ B e. S /\ A.a e. A (F` a):B-->(C` a)) /\ c e. B) -> ({<.u, v>. | (u e. B /\ v = {<.s, t>. | (s e. A /\ t = ((F` s)` u))})}` c) = {<.s, t>. | (s e. A /\ t = ((F` s)` c))})
27	26	adantlr 429	. . . . . . . 8 |- ((((A e. R /\ B e. S /\ A.a e. A (F` a):B-->(C` a)) /\ (h:B-->X /\ A.a e. A (F` a) = ((P` a) o. h))) /\ c e. B) -> ({<.u, v>. | (u e. B /\ v = {<.s, t>. | (s e. A /\ t = ((F` s)` u))})}` c) = {<.s, t>. | (s e. A /\ t = ((F` s)` c))})
28		eqfnfv 4766	. . . . . . . . . 10 |- (({<.s, t>. | (s e. A /\ t = ((F` s)` c))} Fn A /\ (h` c) Fn A) -> ({<.s, t>. | (s e. A /\ t = ((F` s)` c))} = (h` c) <-> (A = A /\ A.d e. A ({<.s, t>. | (s e. A /\ t = ((F` s)` c))}` d) = ((h` c)` d))))
29		fvex 4689	. . . . . . . . . . 11 |- ((F` s)` c) e. _V
30		eqid 1884	. . . . . . . . . . 11 |- {<.s, t>. | (s e. A /\ t = ((F` s)` c))} = {<.s, t>. | (s e. A /\ t = ((F` s)` c))}
31	29, 30	fnopab2 4549	. . . . . . . . . 10 |- {<.s, t>. | (s e. A /\ t = ((F` s)` c))} Fn A
32		ffvelrn 4787	. . . . . . . . . . . . 13 |- ((h:B-->X /\ c e. B) -> (h` c) e. X)
33		upixp.1	. . . . . . . . . . . . . . 15 |- X = X_b e. A (C` b)
34	33	eleq2i 1961	. . . . . . . . . . . . . 14 |- ((h` c) e. X <-> (h` c) e. X_b e. A (C` b))
35		ixpf 5415	. . . . . . . . . . . . . . 15 |- ((h` c) e. X_b e. A (C` b) -> (h` c):A-->U_b e. A (C` b))
36		ffn 4562	. . . . . . . . . . . . . . 15 |- ((h` c):A-->U_b e. A (C` b) -> (h` c) Fn A)
37	35, 36	syl 12	. . . . . . . . . . . . . 14 |- ((h` c) e. X_b e. A (C` b) -> (h` c) Fn A)
38	34, 37	sylbi 216	. . . . . . . . . . . . 13 |- ((h` c) e. X -> (h` c) Fn A)
39	32, 38	syl 12	. . . . . . . . . . . 12 |- ((h:B-->X /\ c e. B) -> (h` c) Fn A)
40	39	adantlr 429	. . . . . . . . . . 11 |- (((h:B-->X /\ A.a e. A (F` a) = ((P` a) o. h)) /\ c e. B) -> (h` c) Fn A)
41	40	adantll 428	. . . . . . . . . 10 |- ((((A e. R /\ B e. S /\ A.a e. A (F` a):B-->(C` a)) /\ (h:B-->X /\ A.a e. A (F` a) = ((P` a) o. h))) /\ c e. B) -> (h` c) Fn A)
42	28, 31, 41	sylancr 526	. . . . . . . . 9 |- ((((A e. R /\ B e. S /\ A.a e. A (F` a):B-->(C` a)) /\ (h:B-->X /\ A.a e. A (F` a) = ((P` a) o. h))) /\ c e. B) -> ({<.s, t>. | (s e. A /\ t = ((F` s)` c))} = (h` c) <-> (A = A /\ A.d e. A ({<.s, t>. | (s e. A /\ t = ((F` s)` c))}` d) = ((h` c)` d))))
43		eqidd 1885	. . . . . . . . 9 |- ((((A e. R /\ B e. S /\ A.a e. A (F` a):B-->(C` a)) /\ (h:B-->X /\ A.a e. A (F` a) = ((P` a) o. h))) /\ c e. B) -> A = A)
44		fveq2 4681	. . . . . . . . . . . . . 14 |- (s = d -> (F` s) = (F` d))
45	44	fveq1d 4683	. . . . . . . . . . . . 13 |- (s = d -> ((F` s)` c) = ((F` d)` c))
46		fvex 4689	. . . . . . . . . . . . 13 |- ((F` d)` c) e. _V
47	45, 30, 46	fvopab4 4743	. . . . . . . . . . . 12 |- (d e. A -> ({<.s, t>. | (s e. A /\ t = ((F` s)` c))}` d) = ((F` d)` c))
48	47	adantl 424	. . . . . . . . . . 11 |- (((((A e. R /\ B e. S /\ A.a e. A (F` a):B-->(C` a)) /\ (h:B-->X /\ A.a e. A (F` a) = ((P` a) o. h))) /\ c e. B) /\ d e. A) -> ({<.s, t>. | (s e. A /\ t = ((F` s)` c))}` d) = ((F` d)` c))
49		fveq2 4681	. . . . . . . . . . . . . . . . 17 |- (a = d -> (F` a) = (F` d))
50		fveq2 4681	. . . . . . . . . . . . . . . . . 18 |- (a = d -> (P` a) = (P` d))
51	50	coeq1d 4127	. . . . . . . . . . . . . . . . 17 |- (a = d -> ((P` a) o. h) = ((P` d) o. h))
52	49, 51	eqeq12d 1899	. . . . . . . . . . . . . . . 16 |- (a = d -> ((F` a) = ((P` a) o. h) <-> (F` d) = ((P` d) o. h)))
53	52	rcla4cva 2379	. . . . . . . . . . . . . . 15 |- ((A.a e. A (F` a) = ((P` a) o. h) /\ d e. A) -> (F` d) = ((P` d) o. h))
54	53	adantll 428	. . . . . . . . . . . . . 14 |- (((h:B-->X /\ A.a e. A (F` a) = ((P` a) o. h)) /\ d e. A) -> (F` d) = ((P` d) o. h))
55	54	adantll 428	. . . . . . . . . . . . 13 |- ((((A e. R /\ B e. S /\ A.a e. A (F` a):B-->(C` a)) /\ (h:B-->X /\ A.a e. A (F` a) = ((P` a) o. h))) /\ d e. A) -> (F` d) = ((P` d) o. h))
56	55	adantlr 429	. . . . . . . . . . . 12 |- (((((A e. R /\ B e. S /\ A.a e. A (F` a):B-->(C` a)) /\ (h:B-->X /\ A.a e. A (F` a) = ((P` a) o. h))) /\ c e. B) /\ d e. A) -> (F` d) = ((P` d) o. h))
57	56	fveq1d 4683	. . . . . . . . . . 11 |- (((((A e. R /\ B e. S /\ A.a e. A (F` a):B-->(C` a)) /\ (h:B-->X /\ A.a e. A (F` a) = ((P` a) o. h))) /\ c e. B) /\ d e. A) -> ((F` d)` c) = (((P` d) o. h)` c))
58		fvex 4689	. . . . . . . . . . . . . . . 16 |- (x` d) e. _V
59		eqid 1884	. . . . . . . . . . . . . . . 16 |- {<.x, y>. | (x e. X /\ y = (x` d))} = {<.x, y>. | (x e. X /\ y = (x` d))}
60	58, 59	fnopab2 4549	. . . . . . . . . . . . . . 15 |- {<.x, y>. | (x e. X /\ y = (x` d))} Fn X
61		fnfun 4510	. . . . . . . . . . . . . . 15 |- ({<.x, y>. | (x e. X /\ y = (x` d))} Fn X -> Fun {<.x, y>. | (x e. X /\ y = (x` d))})
62	60, 61	ax-mp 7	. . . . . . . . . . . . . 14 |- Fun {<.x, y>. | (x e. X /\ y = (x` d))}
63		fveq2 4681	. . . . . . . . . . . . . . . . . . . . 21 |- (w = d -> (x` w) = (x` d))
64	63	eqeq2d 1895	. . . . . . . . . . . . . . . . . . . 20 |- (w = d -> (y = (x` w) <-> y = (x` d)))
65	64	anbi2d 678	. . . . . . . . . . . . . . . . . . 19 |- (w = d -> ((x e. X /\ y = (x` w)) <-> (x e. X /\ y = (x` d))))
66	65	opabbidv 3401	. . . . . . . . . . . . . . . . . 18 |- (w = d -> {<.x, y>. | (x e. X /\ y = (x` w))} = {<.x, y>. | (x e. X /\ y = (x` d))})
67		upixp.2	. . . . . . . . . . . . . . . . . 18 |- P = {<.w, z>. | (w e. A /\ z = {<.x, y>. | (x e. X /\ y = (x` w))})}
68	66, 67	fvopab4g 4742	. . . . . . . . . . . . . . . . 17 |- ((d e. A /\ {<.x, y>. | (x e. X /\ y = (x` d))} e. _V) -> (P` d) = {<.x, y>. | (x e. X /\ y = (x` d))})
69	68	ancoms 484	. . . . . . . . . . . . . . . 16 |- (({<.x, y>. | (x e. X /\ y = (x` d))} e. _V /\ d e. A) -> (P` d) = {<.x, y>. | (x e. X /\ y = (x` d))})
70		fvex 4689	. . . . . . . . . . . . . . . . . . . . . . 23 |- (C` b) e. _V
71	70	a1i 8	. . . . . . . . . . . . . . . . . . . . . 22 |- (b e. A -> (C` b) e. _V)
72	71	rgen 2159	. . . . . . . . . . . . . . . . . . . . 21 |- A.b e. A (C` b) e. _V
73		ixpexg 5417	. . . . . . . . . . . . . . . . . . . . 21 |- ((A e. R /\ A.b e. A (C` b) e. _V) -> X_b e. A (C` b) e. _V)
74	72, 73	mpan2 760	. . . . . . . . . . . . . . . . . . . 20 |- (A e. R -> X_b e. A (C` b) e. _V)
75	74, 33	syl5eqel 1975	. . . . . . . . . . . . . . . . . . 19 |- (A e. R -> X e. _V)
76		opabex2g 4540	. . . . . . . . . . . . . . . . . . 19 |- (X e. _V -> {<.x, y>. | (x e. X /\ y = (x` d))} e. _V)
77	75, 76	syl 12	. . . . . . . . . . . . . . . . . 18 |- (A e. R -> {<.x, y>. | (x e. X /\ y = (x` d))} e. _V)
78	77	3ad2ant1 897	. . . . . . . . . . . . . . . . 17 |- ((A e. R /\ B e. S /\ A.a e. A (F` a):B-->(C` a)) -> {<.x, y>. | (x e. X /\ y = (x` d))} e. _V)
79	78	ad2antrr 440	. . . . . . . . . . . . . . . 16 |- ((((A e. R /\ B e. S /\ A.a e. A (F` a):B-->(C` a)) /\ (h:B-->X /\ A.a e. A (F` a) = ((P` a) o. h))) /\ c e. B) -> {<.x, y>. | (x e. X /\ y = (x` d))} e. _V)
80	69, 79	sylan 497	. . . . . . . . . . . . . . 15 |- (((((A e. R /\ B e. S /\ A.a e. A (F` a):B-->(C` a)) /\ (h:B-->X /\ A.a e. A (F` a) = ((P` a) o. h))) /\ c e. B) /\ d e. A) -> (P` d) = {<.x, y>. | (x e. X /\ y = (x` d))})
81		funeq 4441	. . . . . . . . . . . . . . 15 |- ((P` d) = {<.x, y>. | (x e. X /\ y = (x` d))} -> (Fun (P` d) <-> Fun {<.x, y>. | (x e. X /\ y = (x` d))}))
82	80, 81	syl 12	. . . . . . . . . . . . . 14 |- (((((A e. R /\ B e. S /\ A.a e. A (F` a):B-->(C` a)) /\ (h:B-->X /\ A.a e. A (F` a) = ((P` a) o. h))) /\ c e. B) /\ d e. A) -> (Fun (P` d) <-> Fun {<.x, y>. | (x e. X /\ y = (x` d))}))
83	62, 82	mpbiri 211	. . . . . . . . . . . . 13 |- (((((A e. R /\ B e. S /\ A.a e. A (F` a):B-->(C` a)) /\ (h:B-->X /\ A.a e. A (F` a) = ((P` a) o. h))) /\ c e. B) /\ d e. A) -> Fun (P` d))
84		ffun 4565	. . . . . . . . . . . . . . 15 |- (h:B-->X -> Fun h)
85	84	ad2antrl 442	. . . . . . . . . . . . . 14 |- (((A e. R /\ B e. S /\ A.a e. A (F` a):B-->(C` a)) /\ (h:B-->X /\ A.a e. A (F` a) = ((P` a) o. h))) -> Fun h)
86	85	ad2antrr 440	. . . . . . . . . . . . 13 |- (((((A e. R /\ B e. S /\ A.a e. A (F` a):B-->(C` a)) /\ (h:B-->X /\ A.a e. A (F` a) = ((P` a) o. h))) /\ c e. B) /\ d e. A) -> Fun h)
87		fdm 4567	. . . . . . . . . . . . . . . . . 18 |- (h:B-->X -> dom h = B)
88	87	eleq2d 1964	. . . . . . . . . . . . . . . . 17 |- (h:B-->X -> (c e. dom h <-> c e. B))
89	88	biimpar 461	. . . . . . . . . . . . . . . 16 |- ((h:B-->X /\ c e. B) -> c e. dom h)
90	89	adantlr 429	. . . . . . . . . . . . . . 15 |- (((h:B-->X /\ A.a e. A (F` a) = ((P` a) o. h)) /\ c e. B) -> c e. dom h)
91	90	adantll 428	. . . . . . . . . . . . . 14 |- ((((A e. R /\ B e. S /\ A.a e. A (F` a):B-->(C` a)) /\ (h:B-->X /\ A.a e. A (F` a) = ((P` a) o. h))) /\ c e. B) -> c e. dom h)
92	91	adantr 425	. . . . . . . . . . . . 13 |- (((((A e. R /\ B e. S /\ A.a e. A (F` a):B-->(C` a)) /\ (h:B-->X /\ A.a e. A (F` a) = ((P` a) o. h))) /\ c e. B) /\ d e. A) -> c e. dom h)
93		fvco 4736	. . . . . . . . . . . . 13 |- ((Fun (P` d) /\ Fun h /\ c e. dom h) -> (((P` d) o. h)` c) = ((P` d)` (h` c)))
94	83, 86, 92, 93	syl111anc 1100	. . . . . . . . . . . 12 |- (((((A e. R /\ B e. S /\ A.a e. A (F` a):B-->(C` a)) /\ (h:B-->X /\ A.a e. A (F` a) = ((P` a) o. h))) /\ c e. B) /\ d e. A) -> (((P` d) o. h)` c) = ((P` d)` (h` c)))
95	80	fveq1d 4683	. . . . . . . . . . . 12 |- (((((A e. R /\ B e. S /\ A.a e. A (F` a):B-->(C` a)) /\ (h:B-->X /\ A.a e. A (F` a) = ((P` a) o. h))) /\ c e. B) /\ d e. A) -> ((P` d)` (h` c)) = ({<.x, y>. | (x e. X /\ y = (x` d))}` (h` c)))
96		fveq1 4680	. . . . . . . . . . . . . . . . 17 |- (x = (h` c) -> (x` d) = ((h` c)` d))
97		fvex 4689	. . . . . . . . . . . . . . . . 17 |- ((h` c)` d) e. _V
98	96, 59, 97	fvopab4 4743	. . . . . . . . . . . . . . . 16 |- ((h` c) e. X -> ({<.x, y>. | (x e. X /\ y = (x` d))}` (h` c)) = ((h` c)` d))
99	32, 98	syl 12	. . . . . . . . . . . . . . 15 |- ((h:B-->X /\ c e. B) -> ({<.x, y>. | (x e. X /\ y = (x` d))}` (h` c)) = ((h` c)` d))
100	99	adantlr 429	. . . . . . . . . . . . . 14 |- (((h:B-->X /\ A.a e. A (F` a) = ((P` a) o. h)) /\ c e. B) -> ({<.x, y>. | (x e. X /\ y = (x` d))}` (h` c)) = ((h` c)` d))
101	100	adantll 428	. . . . . . . . . . . . 13 |- ((((A e. R /\ B e. S /\ A.a e. A (F` a):B-->(C` a)) /\ (h:B-->X /\ A.a e. A (F` a) = ((P` a) o. h))) /\ c e. B) -> ({<.x, y>. | (x e. X /\ y = (x` d))}` (h` c)) = ((h` c)` d))
102	101	adantr 425	. . . . . . . . . . . 12 |- (((((A e. R /\ B e. S /\ A.a e. A (F` a):B-->(C` a)) /\ (h:B-->X /\ A.a e. A (F` a) = ((P` a) o. h))) /\ c e. B) /\ d e. A) -> ({<.x, y>. | (x e. X /\ y = (x` d))}` (h` c)) = ((h` c)` d))
103	94, 95, 102	3eqtrd 1929	. . . . . . . . . . 11 |- (((((A e. R /\ B e. S /\ A.a e. A (F` a):B-->(C` a)) /\ (h:B-->X /\ A.a e. A (F` a) = ((P` a) o. h))) /\ c e. B) /\ d e. A) -> (((P` d) o. h)` c) = ((h` c)` d))
104	48, 57, 103	3eqtrd 1929	. . . . . . . . . 10 |- (((((A e. R /\ B e. S /\ A.a e. A (F` a):B-->(C` a)) /\ (h:B-->X /\ A.a e. A (F` a) = ((P` a) o. h))) /\ c e. B) /\ d e. A) -> ({<.s, t>. | (s e. A /\ t = ((F` s)` c))}` d) = ((h` c)` d))
105	104	r19.21aiva 2176	. . . . . . . . 9 |- ((((A e. R /\ B e. S /\ A.a e. A (F` a):B-->(C` a)) /\ (h:B-->X /\ A.a e. A (F` a) = ((P` a) o. h))) /\ c e. B) -> A.d e. A ({<.s, t>. | (s e. A /\ t = ((F` s)` c))}` d) = ((h` c)` d))
106	42, 43, 105	mpbir2and 802	. . . . . . . 8 |- ((((A e. R /\ B e. S /\ A.a e. A (F` a):B-->(C` a)) /\ (h:B-->X /\ A.a e. A (F` a) = ((P` a) o. h))) /\ c e. B) -> {<.s, t>. | (s e. A /\ t = ((F` s)` c))} = (h` c))
107	27, 106	eqtr2d 1926	. . . . . . 7 |- ((((A e. R /\ B e. S /\ A.a e. A (F` a):B-->(C` a)) /\ (h:B-->X /\ A.a e. A (F` a) = ((P` a) o. h))) /\ c e. B) -> (h` c) = ({<.u, v>. | (u e. B /\ v = {<.s, t>. | (s e. A /\ t = ((F` s)` u))})}` c))
108	107	r19.21aiva 2176	. . . . . 6 |- (((A e. R /\ B e. S /\ A.a e. A (F` a):B-->(C` a)) /\ (h:B-->X /\ A.a e. A (F` a) = ((P` a) o. h))) -> A.c e. B (h` c) = ({<.u, v>. | (u e. B /\ v = {<.s, t>. | (s e. A /\ t = ((F` s)` u))})}` c))
109	16, 17, 108	mpbir2and 802	. . . . 5 |- (((A e. R /\ B e. S /\ A.a e. A (F` a):B-->(C` a)) /\ (h:B-->X /\ A.a e. A (F` a) = ((P` a) o. h))) -> h = {<.u, v>. | (u e. B /\ v = {<.s, t>. | (s e. A /\ t = ((F` s)` u))})})
110	109	ex 402	. . . 4 |- ((A e. R /\ B e. S /\ A.a e. A (F` a):B-->(C` a)) -> ((h:B-->X /\ A.a e. A (F` a) = ((P` a) o. h)) -> h = {<.u, v>. | (u e. B /\ v = {<.s, t>. | (s e. A /\ t = ((F` s)` u))})}))
111		feq1 4551	. . . . . 6 |- (h = {<.u, v>. | (u e. B /\ v = {<.s, t>. | (s e. A /\ t = ((F` s)` u))})} -> (h:B-->X <-> {<.u, v>. | (u e. B /\ v = {<.s, t>. | (s e. A /\ t = ((F` s)` u))})}:B-->X))
112		coeq2 4124	. . . . . . . 8 |- (h = {<.u, v>. | (u e. B /\ v = {<.s, t>. | (s e. A /\ t = ((F` s)` u))})} -> ((P` a) o. h) = ((P` a) o. {<.u, v>. | (u e. B /\ v = {<.s, t>. | (s e. A /\ t = ((F` s)` u))})}))
113	112	eqeq2d 1895	. . . . . . 7 |- (h = {<.u, v>. | (u e. B /\ v = {<.s, t>. | (s e. A /\ t = ((F` s)` u))})} -> ((F` a) = ((P` a) o. h) <-> (F` a) = ((P` a) o. {<.u, v>. | (u e. B /\ v = {<.s, t>. | (s e. A /\ t = ((F` s)` u))})})))
114	113	ralbidv 2123	. . . . . 6 |- (h = {<.u, v>. | (u e. B /\ v = {<.s, t>. | (s e. A /\ t = ((F` s)` u))})} -> (A.a e. A (F` a) = ((P` a) o. h) <-> A.a e. A (F` a) = ((P` a) o. {<.u, v>. | (u e. B /\ v = {<.s, t>. | (s e. A /\ t = ((F` s)` u))})})))
115	111, 114	anbi12d 690	. . . . 5 |- (h = {<.u, v>. | (u e. B /\ v = {<.s, t>. | (s e. A /\ t = ((F` s)` u))})} -> ((h:B-->X /\ A.a e. A (F` a) = ((P` a) o. h)) <-> ({<.u, v>. | (u e. B /\ v = {<.s, t>. | (s e. A /\ t = ((F` s)` u))})}:B-->X /\ A.a e. A (F` a) = ((P` a) o. {<.u, v>. | (u e. B /\ v = {<.s, t>. | (s e. A /\ t = ((F` s)` u))})}))))
116	7	3ad2ant1 897	. . . . . . . . . . . 12 |- ((A e. R /\ B e. S /\ A.a e. A (F` a):B-->(C` a)) -> {<.s, t>. | (s e. A /\ t = ((F` s)` u))} e. _V)
117	116	adantr 425	. . . . . . . . . . 11 |- (((A e. R /\ B e. S /\ A.a e. A (F` a):B-->(C` a)) /\ u e. B) -> {<.s, t>. | (s e. A /\ t = ((F` s)` u))} e. _V)
118		fvex 4689	. . . . . . . . . . . . 13 |- ((F` s)` u) e. _V
119		eqid 1884	. . . . . . . . . . . . 13 |- {<.s, t>. | (s e. A /\ t = ((F` s)` u))} = {<.s, t>. | (s e. A /\ t = ((F` s)` u))}
120	118, 119	fnopab2 4549	. . . . . . . . . . . 12 |- {<.s, t>. | (s e. A /\ t = ((F` s)` u))} Fn A
121	120	a1i 8	. . . . . . . . . . 11 |- (((A e. R /\ B e. S /\ A.a e. A (F` a):B-->(C` a)) /\ u e. B) -> {<.s, t>. | (s e. A /\ t = ((F` s)` u))} Fn A)
122		fveq2 4681	. . . . . . . . . . . . . . . 16 |- (s = b -> (F` s) = (F` b))
123	122	fveq1d 4683	. . . . . . . . . . . . . . 15 |- (s = b -> ((F` s)` u) = ((F` b)` u))
124		fvex 4689	. . . . . . . . . . . . . . 15 |- ((F` b)` u) e. _V
125	123, 119, 124	fvopab4 4743	. . . . . . . . . . . . . 14 |- (b e. A -> ({<.s, t>. | (s e. A /\ t = ((F` s)` u))}` b) = ((F` b)` u))
126	125	adantl 424	. . . . . . . . . . . . 13 |- ((((A e. R /\ B e. S /\ A.a e. A (F` a):B-->(C` a)) /\ u e. B) /\ b e. A) -> ({<.s, t>. | (s e. A /\ t = ((F` s)` u))}` b) = ((F` b)` u))
127		ffvelrn 4787	. . . . . . . . . . . . . . . . . 18 |- (((F` b):B-->(C` b) /\ u e. B) -> ((F` b)` u) e. (C` b))
128		fveq2 4681	. . . . . . . . . . . . . . . . . . . . 21 |- (a = b -> (F` a) = (F` b))
129	128	feq1d 4556	. . . . . . . . . . . . . . . . . . . 20 |- (a = b -> ((F` a):B-->(C` a) <-> (F` b):B-->(C` a)))
130		fveq2 4681	. . . . . . . . . . . . . . . . . . . . 21 |- (a = b -> (C` a) = (C` b))
131		feq3 4553	. . . . . . . . . . . . . . . . . . . . 21 |- ((C` a) = (C` b) -> ((F` b):B-->(C` a) <-> (F` b):B-->(C` b)))
132	130, 131	syl 12	. . . . . . . . . . . . . . . . . . . 20 |- (a = b -> ((F` b):B-->(C` a) <-> (F` b):B-->(C` b)))
133	129, 132	bitrd 587	. . . . . . . . . . . . . . . . . . 19 |- (a = b -> ((F` a):B-->(C` a) <-> (F` b):B-->(C` b)))
134	133	rcla4cva 2379	. . . . . . . . . . . . . . . . . 18 |- ((A.a e. A (F` a):B-->(C` a) /\ b e. A) -> (F` b):B-->(C` b))
135	127, 134	sylan 497	. . . . . . . . . . . . . . . . 17 |- (((A.a e. A (F` a):B-->(C` a) /\ b e. A) /\ u e. B) -> ((F` b)` u) e. (C` b))
136	135	anasss 488	. . . . . . . . . . . . . . . 16 |- ((A.a e. A (F` a):B-->(C` a) /\ (b e. A /\ u e. B)) -> ((F` b)` u) e. (C` b))
137	136	ancom2s 545	. . . . . . . . . . . . . . 15 |- ((A.a e. A (F` a):B-->(C` a) /\ (u e. B /\ b e. A)) -> ((F` b)` u) e. (C` b))
138	137	3ad2antl3 1040	. . . . . . . . . . . . . 14 |- (((A e. R /\ B e. S /\ A.a e. A (F` a):B-->(C` a)) /\ (u e. B /\ b e. A)) -> ((F` b)` u) e. (C` b))
139	138	anassrs 489	. . . . . . . . . . . . 13 |- ((((A e. R /\ B e. S /\ A.a e. A (F` a):B-->(C` a)) /\ u e. B) /\ b e. A) -> ((F` b)` u) e. (C` b))
140	126, 139	eqeltrd 1971	. . . . . . . . . . . 12 |- ((((A e. R /\ B e. S /\ A.a e. A (F` a):B-->(C` a)) /\ u e. B) /\ b e. A) -> ({<.s, t>. | (s e. A /\ t = ((F` s)` u))}` b) e. (C` b))
141	140	r19.21aiva 2176	. . . . . . . . . . 11 |- (((A e. R /\ B e. S /\ A.a e. A (F` a):B-->(C` a)) /\ u e. B) -> A.b e. A ({<.s, t>. | (s e. A /\ t = ((F` s)` u))}` b) e. (C` b))
142	117, 121, 141	3jca 1050	. . . . . . . . . 10 |- (((A e. R /\ B e. S /\ A.a e. A (F` a):B-->(C` a)) /\ u e. B) -> ({<.s, t>. | (s e. A /\ t = ((F` s)` u))} e. _V /\ {<.s, t>. | (s e. A /\ t = ((F` s)` u))} Fn A /\ A.b e. A ({<.s, t>. | (s e. A /\ t = ((F` s)` u))}` b) e. (C` b)))
143		elixp2 5408	. . . . . . . . . 10 |- ({<.s, t>. | (s e. A /\ t = ((F` s)` u))} e. X_b e. A (C` b) <-> ({<.s, t>. | (s e. A /\ t = ((F` s)` u))} e. _V /\ {<.s, t>. | (s e. A /\ t = ((F` s)` u))} Fn A /\ A.b e. A ({<.s, t>. | (s e. A /\ t = ((F` s)` u))}` b) e. (C` b)))
144	142, 143	sylibr 217	. . . . . . . . 9 |- (((A e. R /\ B e. S /\ A.a e. A (F` a):B-->(C` a)) /\ u e. B) -> {<.s, t>. | (s e. A /\ t = ((F` s)` u))} e. X_b e. A (C` b))
145	144, 33	syl6eleqr 1982	. . . . . . . 8 |- (((A e. R /\ B e. S /\ A.a e. A (F` a):B-->(C` a)) /\ u e. B) -> {<.s, t>. | (s e. A /\ t = ((F` s)` u))} e. X)
146	145	r19.21aiva 2176	. . . . . . 7 |- ((A e. R /\ B e. S /\ A.a e. A (F` a):B-->(C` a)) -> A.u e. B {<.s, t>. | (s e. A /\ t = ((F` s)` u))} e. X)
147	10	fopab2 4796	. . . . . . 7 |- (A.u e. B {<.s, t>. | (s e. A /\ t = ((F` s)` u))} e. X <-> {<.u, v>. | (u e. B /\ v = {<.s, t>. | (s e. A /\ t = ((F` s)` u))})}:B-->X)
148	146, 147	sylib 215	. . . . . 6 |- ((A e. R /\ B e. S /\ A.a e. A (F` a):B-->(C` a)) -> {<.u, v>. | (u e. B /\ v = {<.s, t>. | (s e. A /\ t = ((F` s)` u))})}:B-->X)
149		fveq2 4681	. . . . . . . . . . . . . . . 16 |- (a = c -> (F` a) = (F` c))
150	149	feq1d 4556	. . . . . . . . . . . . . . 15 |- (a = c -> ((F` a):B-->(C` a) <-> (F` c):B-->(C` a)))
151		fveq2 4681	. . . . . . . . . . . . . . . 16 |- (a = c -> (C` a) = (C` c))
152		feq3 4553	. . . . . . . . . . . . . . . 16 |- ((C` a) = (C` c) -> ((F` c):B-->(C` a) <-> (F` c):B-->(C` c)))
153	151, 152	syl 12	. . . . . . . . . . . . . . 15 |- (a = c -> ((F` c):B-->(C` a) <-> (F` c):B-->(C` c)))
154	150, 153	bitrd 587	. . . . . . . . . . . . . 14 |- (a = c -> ((F` a):B-->(C` a) <-> (F` c):B-->(C` c)))
155	154	rcla4cva 2379	. . . . . . . . . . . . 13 |- ((A.a e. A (F` a):B-->(C` a) /\ c e. A) -> (F` c):B-->(C` c))
156		ffn 4562	. . . . . . . . . . . . 13 |- ((F` c):B-->(C` c) -> (F` c) Fn B)
157	155, 156	syl 12	. . . . . . . . . . . 12 |- ((A.a e. A (F` a):B-->(C` a) /\ c e. A) -> (F` c) Fn B)
158	157	adantll 428	. . . . . . . . . . 11 |- (((A e. R /\ A.a e. A (F` a):B-->(C` a)) /\ c e. A) -> (F` c) Fn B)
159		fvex 4689	. . . . . . . . . . . . . 14 |- (x` c) e. _V
160		eqid 1884	. . . . . . . . . . . . . 14 |- {<.x, y>. | (x e. X /\ y = (x` c))} = {<.x, y>. | (x e. X /\ y = (x` c))}
161	159, 160	fnopab2 4549	. . . . . . . . . . . . 13 |- {<.x, y>. | (x e. X /\ y = (x` c))} Fn X
162		fveq2 4681	. . . . . . . . . . . . . . . . . . . . 21 |- (w = c -> (x` w) = (x` c))
163	162	eqeq2d 1895	. . . . . . . . . . . . . . . . . . . 20 |- (w = c -> (y = (x` w) <-> y = (x` c)))
164	163	anbi2d 678	. . . . . . . . . . . . . . . . . . 19 |- (w = c -> ((x e. X /\ y = (x` w)) <-> (x e. X /\ y = (x` c))))
165	164	opabbidv 3401	. . . . . . . . . . . . . . . . . 18 |- (w = c -> {<.x, y>. | (x e. X /\ y = (x` w))} = {<.x, y>. | (x e. X /\ y = (x` c))})
166	165, 67	fvopab4g 4742	. . . . . . . . . . . . . . . . 17 |- ((c e. A /\ {<.x, y>. | (x e. X /\ y = (x` c))} e. _V) -> (P` c) = {<.x, y>. | (x e. X /\ y = (x` c))})
167		opabex2g 4540	. . . . . . . . . . . . . . . . . 18 |- (X e. _V -> {<.x, y>. | (x e. X /\ y = (x` c))} e. _V)
168	75, 167	syl 12	. . . . . . . . . . . . . . . . 17 |- (A e. R -> {<.x, y>. | (x e. X /\ y = (x` c))} e. _V)
169	166, 168	sylan2 500	. . . . . . . . . . . . . . . 16 |- ((c e. A /\ A e. R) -> (P` c) = {<.x, y>. | (x e. X /\ y = (x` c))})
170	169	ancoms 484	. . . . . . . . . . . . . . 15 |- ((A e. R /\ c e. A) -> (P` c) = {<.x, y>. | (x e. X /\ y = (x` c))})
171	170	adantlr 429	. . . . . . . . . . . . . 14 |- (((A e. R /\ A.a e. A (F` a):B-->(C` a)) /\ c e. A) -> (P` c) = {<.x, y>. | (x e. X /\ y = (x` c))})
172	171	fneq1d 4505	. . . . . . . . . . . . 13 |- (((A e. R /\ A.a e. A (F` a):B-->(C` a)) /\ c e. A) -> ((P` c) Fn X <-> {<.x, y>. | (x e. X /\ y = (x` c))} Fn X))
173	161, 172	mpbiri 211	. . . . . . . . . . . 12 |- (((A e. R /\ A.a e. A (F` a):B-->(C` a)) /\ c e. A) -> (P` c) Fn X)
174	12	ad2antrr 440	. . . . . . . . . . . 12 |- (((A e. R /\ A.a e. A (F` a):B-->(C` a)) /\ c e. A) -> {<.u, v>. | (u e. B /\ v = {<.s, t>. | (s e. A /\ t = ((F` s)` u))})} Fn B)
175	7	adantr 425	. . . . . . . . . . . . . . . . . . 19 |- ((A e. R /\ A.a e. A (F` a):B-->(C` a)) -> {<.s, t>. | (s e. A /\ t = ((F` s)` u))} e. _V)
176	175	ad2antrr 440	. . . . . . . . . . . . . . . . . 18 |- ((((A e. R /\ A.a e. A (F` a):B-->(C` a)) /\ c e. A) /\ u e. B) -> {<.s, t>. | (s e. A /\ t = ((F` s)` u))} e. _V)
177	120	a1i 8	. . . . . . . . . . . . . . . . . 18 |- ((((A e. R /\ A.a e. A (F` a):B-->(C` a)) /\ c e. A) /\ u e. B) -> {<.s, t>. | (s e. A /\ t = ((F` s)` u))} Fn A)
178	125	adantl 424	. . . . . . . . . . . . . . . . . . . 20 |- (((((A e. R /\ A.a e. A (F` a):B-->(C` a)) /\ c e. A) /\ u e. B) /\ b e. A) -> ({<.s, t>. | (s e. A /\ t = ((F` s)` u))}` b) = ((F` b)` u))
179	135	an1rs 547	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((A.a e. A (F` a):B-->(C` a) /\ u e. B) /\ b e. A) -> ((F` b)` u) e. (C` b))
180	179	anasss 488	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((A.a e. A (F` a):B-->(C` a) /\ (u e. B /\ b e. A)) -> ((F` b)` u) e. (C` b))
181	180	adantll 428	. . . . . . . . . . . . . . . . . . . . . 22 |- (((A e. R /\ A.a e. A (F` a):B-->(C` a)) /\ (u e. B /\ b e. A)) -> ((F` b)` u) e. (C` b))
182	181	adantlr 429	. . . . . . . . . . . . . . . . . . . . 21 |- ((((A e. R /\ A.a e. A (F` a):B-->(C` a)) /\ c e. A) /\ (u e. B /\ b e. A)) -> ((F` b)` u) e. (C` b))
183	182	anassrs 489	. . . . . . . . . . . . . . . . . . . 20 |- (((((A e. R /\ A.a e. A (F` a):B-->(C` a)) /\ c e. A) /\ u e. B) /\ b e. A) -> ((F` b)` u) e. (C` b))
184	178, 183	eqeltrd 1971	. . . . . . . . . . . . . . . . . . 19 |- (((((A e. R /\ A.a e. A (F` a):B-->(C` a)) /\ c e. A) /\ u e. B) /\ b e. A) -> ({<.s, t>. | (s e. A /\ t = ((F` s)` u))}` b) e. (C` b))
185	184	r19.21aiva 2176	. . . . . . . . . . . . . . . . . 18 |- ((((A e. R /\ A.a e. A (F` a):B-->(C` a)) /\ c e. A) /\ u e. B) -> A.b e. A ({<.s, t>. | (s e. A /\ t = ((F` s)` u))}` b) e. (C` b))
186	176, 177, 185	3jca 1050	. . . . . . . . . . . . . . . . 17 |- ((((A e. R /\ A.a e. A (F` a):B-->(C` a)) /\ c e. A) /\ u e. B) -> ({<.s, t>. | (s e. A /\ t = ((F` s)` u))} e. _V /\ {<.s, t>. | (s e. A /\ t = ((F` s)` u))} Fn A /\ A.b e. A ({<.s, t>. | (s e. A /\ t = ((F` s)` u))}` b) e. (C` b)))
187	186, 143	sylibr 217	. . . . . . . . . . . . . . . 16 |- ((((A e. R /\ A.a e. A (F` a):B-->(C` a)) /\ c e. A) /\ u e. B) -> {<.s, t>. | (s e. A /\ t = ((F` s)` u))} e. X_b e. A (C` b))
188	187, 33	syl6eleqr 1982	. . . . . . . . . . . . . . 15 |- ((((A e. R /\ A.a e. A (F` a):B-->(C` a)) /\ c e. A) /\ u e. B) -> {<.s, t>. | (s e. A /\ t = ((F` s)` u))} e. X)
189	188	r19.21aiva 2176	. . . . . . . . . . . . . 14 |- (((A e. R /\ A.a e. A (F` a):B-->(C` a)) /\ c e. A) -> A.u e. B {<.s, t>. | (s e. A /\ t = ((F` s)` u))} e. X)
190	189, 147	sylib 215	. . . . . . . . . . . . 13 |- (((A e. R /\ A.a e. A (F` a):B-->(C` a)) /\ c e. A) -> {<.u, v>. | (u e. B /\ v = {<.s, t>. | (s e. A /\ t = ((F` s)` u))})}:B-->X)
191		frn 4569	. . . . . . . . . . . . 13 |- ({<.u, v>. | (u e. B /\ v = {<.s, t>. | (s e. A /\ t = ((F` s)` u))})}:B-->X -> ran {<.u, v>. | (u e. B /\ v = {<.s, t>. | (s e. A /\ t = ((F` s)` u))})} C_ X)
192	190, 191	syl 12	. . . . . . . . . . . 12 |- (((A e. R /\ A.a e. A (F` a):B-->(C` a)) /\ c e. A) -> ran {<.u, v>. | (u e. B /\ v = {<.s, t>. | (s e. A /\ t = ((F` s)` u))})} C_ X)
193		fnco 4521	. . . . . . . . . . . 12 |- (((P` c) Fn X /\ {<.u, v>. | (u e. B /\ v = {<.s, t>. | (s e. A /\ t = ((F` s)` u))})} Fn B /\ ran {<.u, v>. | (u e. B /\ v = {<.s, t>. | (s e. A /\ t = ((F` s)` u))})} C_ X) -> ((P` c) o. {<.u, v>. | (u e. B /\ v = {<.s, t>. | (s e. A /\ t = ((F` s)` u))})}) Fn B)
194	173, 174, 192, 193	syl111anc 1100	. . . . . . . . . . 11 |- (((A e. R /\ A.a e. A (F` a):B-->(C` a)) /\ c e. A) -> ((P` c) o. {<.u, v>. | (u e. B /\ v = {<.s, t>. | (s e. A /\ t = ((F` s)` u))})}) Fn B)
195		eqfnfv 4766	. . . . . . . . . . 11 |- (((F` c) Fn B /\ ((P` c) o. {<.u, v>. | (u e. B /\ v = {<.s, t>. | (s e. A /\ t = ((F` s)` u))})}) Fn B) -> ((F` c) = ((P` c) o. {<.u, v>. | (u e. B /\ v = {<.s, t>. | (s e. A /\ t = ((F` s)` u))})}) <-> (B = B /\ A.d e. B ((F` c)` d) = (((P` c) o. {<.u, v>. | (u e. B /\ v = {<.s, t>. | (s e. A /\ t = ((F` s)` u))})})` d))))
196	158, 194, 195	syl11anc 524	. . . . . . . . . 10 |- (((A e. R /\ A.a e. A (F` a):B-->(C` a)) /\ c e. A) -> ((F` c) = ((P` c) o. {<.u, v>. | (u e. B /\ v = {<.s, t>. | (s e. A /\ t = ((F` s)` u))})}) <-> (B = B /\ A.d e. B ((F` c)` d) = (((P` c) o. {<.u, v>. | (u e. B /\ v = {<.s, t>. | (s e. A /\ t = ((F` s)` u))})})` d))))
197		eqidd 1885	. . . . . . . . . 10 |- (((A e. R /\ A.a e. A (F` a):B-->(C` a)) /\ c e. A) -> B = B)
198	173	adantr 425	. . . . . . . . . . . . . 14 |- ((((A e. R /\ A.a e. A (F` a):B-->(C` a)) /\ c e. A) /\ d e. B) -> (P` c) Fn X)
199		fnfun 4510	. . . . . . . . . . . . . 14 |- ((P` c) Fn X -> Fun (P` c))
200	198, 199	syl 12	. . . . . . . . . . . . 13 |- ((((A e. R /\ A.a e. A (F` a):B-->(C` a)) /\ c e. A) /\ d e. B) -> Fun (P` c))
201	174	adantr 425	. . . . . . . . . . . . . 14 |- ((((A e. R /\ A.a e. A (F` a):B-->(C` a)) /\ c e. A) /\ d e. B) -> {<.u, v>. | (u e. B /\ v = {<.s, t>. | (s e. A /\ t = ((F` s)` u))})} Fn B)
202		fnfun 4510	. . . . . . . . . . . . . 14 |- ({<.u, v>. | (u e. B /\ v = {<.s, t>. | (s e. A /\ t = ((F` s)` u))})} Fn B -> Fun {<.u, v>. | (u e. B /\ v = {<.s, t>. | (s e. A /\ t = ((F` s)` u))})})
203	201, 202	syl 12	. . . . . . . . . . . . 13 |- ((((A e. R /\ A.a e. A (F` a):B-->(C` a)) /\ c e. A) /\ d e. B) -> Fun {<.u, v>. | (u e. B /\ v = {<.s, t>. | (s e. A /\ t = ((F` s)` u))})})
204		fndm 4512	. . . . . . . . . . . . . . . 16 |- ({<.u, v>. | (u e. B /\ v = {<.s, t>. | (s e. A /\ t = ((F` s)` u))})} Fn B -> dom {<.u, v>. | (u e. B /\ v = {<.s, t>. | (s e. A /\ t = ((F` s)` u))})} = B)
205	174, 204	syl 12	. . . . . . . . . . . . . . 15 |- (((A e. R /\ A.a e. A (F` a):B-->(C` a)) /\ c e. A) -> dom {<.u, v>. | (u e. B /\ v = {<.s, t>. | (s e. A /\ t = ((F` s)` u))})} = B)
206	205	eleq2d 1964	. . . . . . . . . . . . . 14 |- (((A e. R /\ A.a e. A (F` a):B-->(C` a)) /\ c e. A) -> (d e. dom {<.u, v>. | (u e. B /\ v = {<.s, t>. | (s e. A /\ t = ((F` s)` u))})} <-> d e. B))
207	206	biimpar 461	. . . . . . . . . . . . 13 |- ((((A e. R /\ A.a e. A (F` a):B-->(C` a)) /\ c e. A) /\ d e. B) -> d e. dom {<.u, v>. | (u e. B /\ v = {<.s, t>. | (s e. A /\ t = ((F` s)` u))})})
208		fvco 4736	. . . . . . . . . . . . 13 |- ((Fun (P` c) /\ Fun {<.u, v>. | (u e. B /\ v = {<.s, t>. | (s e. A /\ t = ((F` s)` u))})} /\ d e. dom {<.u, v>. | (u e. B /\ v = {<.s, t>. | (s e. A /\ t = ((F` s)` u))})}) -> (((P` c) o. {<.u, v>. | (u e. B /\ v = {<.s, t>. | (s e. A /\ t = ((F` s)` u))})})` d) = ((P` c)` ({<.u, v>. | (u e. B /\ v = {<.s, t>. | (s e. A /\ t = ((F` s)` u))})}` d)))
209	200, 203, 207, 208	syl111anc 1100	. . . . . . . . . . . 12 |- ((((A e. R /\ A.a e. A (F` a):B-->(C` a)) /\ c e. A) /\ d e. B) -> (((P` c) o. {<.u, v>. | (u e. B /\ v = {<.s, t>. | (s e. A /\ t = ((F` s)` u))})})` d) = ((P` c)` ({<.u, v>. | (u e. B /\ v = {<.s, t>. | (s e. A /\ t = ((F` s)` u))})}` d)))
210		fveq2 4681	. . . . . . . . . . . . . . . . . . . . . 22 |- (u = d -> ((F` s)` u) = ((F` s)` d))
211	210	eqeq2d 1895	. . . . . . . . . . . . . . . . . . . . 21 |- (u = d -> (t = ((F` s)` u) <-> t = ((F` s)` d)))
212	211	anbi2d 678	. . . . . . . . . . . . . . . . . . . 20 |- (u = d -> ((s e. A /\ t = ((F` s)` u)) <-> (s e. A /\ t = ((F` s)` d))))
213	212	opabbidv 3401	. . . . . . . . . . . . . . . . . . 19 |- (u = d -> {<.s, t>. | (s e. A /\ t = ((F` s)` u))} = {<.s, t>. | (s e. A /\ t = ((F` s)` d))})
214	213, 10	fvopab4g 4742	. . . . . . . . . . . . . . . . . 18 |- ((d e. B /\ {<.s, t>. | (s e. A /\ t = ((F` s)` d))} e. _V) -> ({<.u, v>. | (u e. B /\ v = {<.s, t>. | (s e. A /\ t = ((F` s)` u))})}` d) = {<.s, t>. | (s e. A /\ t = ((F` s)` d))})
215		opabex2g 4540	. . . . . . . . . . . . . . . . . 18 |- (A e. R -> {<.s, t>. | (s e. A /\ t = ((F` s)` d))} e. _V)
216	214, 215	sylan2 500	. . . . . . . . . . . . . . . . 17 |- ((d e. B /\ A e. R) -> ({<.u, v>. | (u e. B /\ v = {<.s, t>. | (s e. A /\ t = ((F` s)` u))})}` d) = {<.s, t>. | (s e. A /\ t = ((F` s)` d))})
217	216	ancoms 484	. . . . . . . . . . . . . . . 16 |- ((A e. R /\ d e. B) -> ({<.u, v>. | (u e. B /\ v = {<.s, t>. | (s e. A /\ t = ((F` s)` u))})}` d) = {<.s, t>. | (s e. A /\ t = ((F` s)` d))})
218	217	adantlr 429	. . . . . . . . . . . . . . 15 |- (((A e. R /\ A.a e. A (F` a):B-->(C` a)) /\ d e. B) -> ({<.u, v>. | (u e. B /\ v = {<.s, t>. | (s e. A /\ t = ((F` s)` u))})}` d) = {<.s, t>. | (s e. A /\ t = ((F` s)` d))})
219	218	adantlr 429	. . . . . . . . . . . . . 14 |- ((((A e. R /\ A.a e. A (F` a):B-->(C` a)) /\ c e. A) /\ d e. B) -> ({<.u, v>. | (u e. B /\ v = {<.s, t>. | (s e. A /\ t = ((F` s)` u))})}` d) = {<.s, t>. | (s e. A /\ t = ((F` s)` d))})
220	219	fveq2d 4685	. . . . . . . . . . . . 13 |- ((((A e. R /\ A.a e. A (F` a):B-->(C` a)) /\ c e. A) /\ d e. B) -> ((P` c)` ({<.u, v>. | (u e. B /\ v = {<.s, t>. | (s e. A /\ t = ((F` s)` u))})}` d)) = ((P` c)` {<.s, t>. | (s e. A /\ t = ((F` s)` d))}))
221	171	adantr 425	. . . . . . . . . . . . . 14 |- ((((A e. R /\ A.a e. A (F` a):B-->(C` a)) /\ c e. A) /\ d e. B) -> (P` c) = {<.x, y>. | (x e. X /\ y = (x` c))})
222	221	fveq1d 4683	. . . . . . . . . . . . 13 |- ((((A e. R /\ A.a e. A (F` a):B-->(C` a)) /\ c e. A) /\ d e. B) -> ((P` c)` {<.s, t>. | (s e. A /\ t = ((F` s)` d))}) = ({<.x, y>. | (x e. X /\ y = (x` c))}` {<.s, t>. | (s e. A /\ t = ((F` s)` d))}))
223	215	ad2antrr 440	. . . . . . . . . . . . . . . . . . 19 |- (((A e. R /\ A.a e. A (F` a):B-->(C` a)) /\ d e. B) -> {<.s, t>. | (s e. A /\ t = ((F` s)` d))} e. _V)
224		fvex 4689	. . . . . . . . . . . . . . . . . . . . 21 |- ((F` s)` d) e. _V
225		eqid 1884	. . . . . . . . . . . . . . . . . . . . 21 |- {<.s, t>. | (s e. A /\ t = ((F` s)` d))} = {<.s, t>. | (s e. A /\ t = ((F` s)` d))}
226	224, 225	fnopab2 4549	. . . . . . . . . . . . . . . . . . . 20 |- {<.s, t>. | (s e. A /\ t = ((F` s)` d))} Fn A
227	226	a1i 8	. . . . . . . . . . . . . . . . . . 19 |- (((A e. R /\ A.a e. A (F` a):B-->(C` a)) /\ d e. B) -> {<.s, t>. | (s e. A /\ t = ((F` s)` d))} Fn A)
228	122	fveq1d 4683	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (s = b -> ((F` s)` d) = ((F` b)` d))
229		fvex 4689	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((F` b)` d) e. _V
230	228, 225, 229	fvopab4 4743	. . . . . . . . . . . . . . . . . . . . . . 23 |- (b e. A -> ({<.s, t>. | (s e. A /\ t = ((F` s)` d))}` b) = ((F` b)` d))
231	230	adantl 424	. . . . . . . . . . . . . . . . . . . . . 22 |- (((A.a e. A (F` a):B-->(C` a) /\ d e. B) /\ b e. A) -> ({<.s, t>. | (s e. A /\ t = ((F` s)` d))}` b) = ((F` b)` d))
232		ffvelrn 4787	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((F` b):B-->(C` b) /\ d e. B) -> ((F` b)` d) e. (C` b))
233	232, 134	sylan 497	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((A.a e. A (F` a):B-->(C` a) /\ b e. A) /\ d e. B) -> ((F` b)` d) e. (C` b))
234	233	an1rs 547	. . . . . . . . . . . . . . . . . . . . . 22 |- (((A.a e. A (F` a):B-->(C` a) /\ d e. B) /\ b e. A) -> ((F` b)` d) e. (C` b))
235	231, 234	eqeltrd 1971	. . . . . . . . . . . . . . . . . . . . 21 |- (((A.a e. A (F` a):B-->(C` a) /\ d e. B) /\ b e. A) -> ({<.s, t>. | (s e. A /\ t = ((F` s)` d))}` b) e. (C` b))
236	235	r19.21aiva 2176	. . . . . . . . . . . . . . . . . . . 20 |- ((A.a e. A (F` a):B-->(C` a) /\ d e. B) -> A.b e. A ({<.s, t>. | (s e. A /\ t = ((F` s)` d))}` b) e. (C` b))
237	236	adantll 428	. . . . . . . . . . . . . . . . . . 19 |- (((A e. R /\ A.a e. A (F` a):B-->(C` a)) /\ d e. B) -> A.b e. A ({<.s, t>. | (s e. A /\ t = ((F` s)` d))}` b) e. (C` b))
238	223, 227, 237	3jca 1050	. . . . . . . . . . . . . . . . . 18 |- (((A e. R /\ A.a e. A (F` a):B-->(C` a)) /\ d e. B) -> ({<.s, t>. | (s e. A /\ t = ((F` s)` d))} e. _V /\ {<.s, t>. | (s e. A /\ t = ((F` s)` d))} Fn A /\ A.b e. A ({<.s, t>. | (s e. A /\ t = ((F` s)` d))}` b) e. (C` b)))
239		elixp2 5408	. . . . . . . . . . . . . . . . . 18 |- ({<.s, t>. | (s e. A /\ t = ((F` s)` d))} e. X_b e. A (C` b) <-> ({<.s, t>. | (s e. A /\ t = ((F` s)` d))} e. _V /\ {<.s, t>. | (s e. A /\ t = ((F` s)` d))} Fn A /\ A.b e. A ({<.s, t>. | (s e. A /\ t = ((F` s)` d))}` b) e. (C` b)))
240	238, 239	sylibr 217	. . . . . . . . . . . . . . . . 17 |- (((A e. R /\ A.a e. A (F` a):B-->(C` a)) /\ d e. B) -> {<.s, t>. | (s e. A /\ t = ((F` s)` d))} e. X_b e. A (C` b))
241	240, 33	syl6eleqr 1982	. . . . . . . . . . . . . . . 16 |- (((A e. R /\ A.a e. A (F` a):B-->(C` a)) /\ d e. B) -> {<.s, t>. | (s e. A /\ t = ((F` s)` d))} e. X)
242		fveq1 4680	. . . . . . . . . . . . . . . . 17 |- (x = {<.s, t>. | (s e. A /\ t = ((F` s)` d))} -> (x` c) = ({<.s, t>. | (s e. A /\ t = ((F` s)` d))}` c))
243		fvex 4689	. . . . . . . . . . . . . . . . 17 |- ({<.s, t>. | (s e. A /\ t = ((F` s)` d))}` c) e. _V
244	242, 160, 243	fvopab4 4743	. . . . . . . . . . . . . . . 16 |- ({<.s, t>. | (s e. A /\ t = ((F` s)` d))} e. X -> ({<.x, y>. | (x e. X /\ y = (x` c))}` {<.s, t>. | (s e. A /\ t = ((F` s)` d))}) = ({<.s, t>. | (s e. A /\ t = ((F` s)` d))}` c))
245	241, 244	syl 12	. . . . . . . . . . . . . . 15 |- (((A e. R /\ A.a e. A (F` a):B-->(C` a)) /\ d e. B) -> ({<.x, y>. | (x e. X /\ y = (x` c))}` {<.s, t>. | (s e. A /\ t = ((F` s)` d))}) = ({<.s, t>. | (s e. A /\ t = ((F` s)` d))}` c))
246	245	adantlr 429	. . . . . . . . . . . . . 14 |- ((((A e. R /\ A.a e. A (F` a):B-->(C` a)) /\ c e. A) /\ d e. B) -> ({<.x, y>. | (x e. X /\ y = (x` c))}` {<.s, t>. | (s e. A /\ t = ((F` s)` d))}) = ({<.s, t>. | (s e. A /\ t = ((F` s)` d))}` c))
247		fveq2 4681	. . . . . . . . . . . . . . . . 17 |- (s = c -> (F` s) = (F` c))
248	247	fveq1d 4683	. . . . . . . . . . . . . . . 16 |- (s = c -> ((F` s)` d) = ((F` c)` d))
249		fvex 4689	. . . . . . . . . . . . . . . 16 |- ((F` c)` d) e. _V
250	248, 225, 249	fvopab4 4743	. . . . . . . . . . . . . . 15 |- (c e. A -> ({<.s, t>. | (s e. A /\ t = ((F` s)` d))}` c) = ((F` c)` d))
251	250	ad2antlr 441	. . . . . . . . . . . . . 14 |- ((((A e. R /\ A.a e. A (F` a):B-->(C` a)) /\ c e. A) /\ d e. B) -> ({<.s, t>. | (s e. A /\ t = ((F` s)` d))}` c) = ((F` c)` d))
252	246, 251	eqtrd 1925	. . . . . . . . . . . . 13 |- ((((A e. R /\ A.a e. A (F` a):B-->(C` a)) /\ c e. A) /\ d e. B) -> ({<.x, y>. | (x e. X /\ y = (x` c))}` {<.s, t>. | (s e. A /\ t = ((F` s)` d))}) = ((F` c)` d))
253	220, 222, 252	3eqtrd 1929	. . . . . . . . . . . 12 |- ((((A e. R /\ A.a e. A (F` a):B-->(C` a)) /\ c e. A) /\ d e. B) -> ((P` c)` ({<.u, v>. | (u e. B /\ v = {<.s, t>. | (s e. A /\ t = ((F` s)` u))})}` d)) = ((F` c)` d))
254	209, 253	eqtr2d 1926	. . . . . . . . . . 11 |- ((((A e. R /\ A.a e. A (F` a):B-->(C` a)) /\ c e. A) /\ d e. B) -> ((F` c)` d) = (((P` c) o. {<.u, v>. | (u e. B /\ v = {<.s, t>. | (s e. A /\ t = ((F` s)` u))})})` d))
255	254	r19.21aiva 2176	. . . . . . . . . 10 |- (((A e. R /\ A.a e. A (F` a):B-->(C` a)) /\ c e. A) -> A.d e. B ((F` c)` d) = (((P` c) o. {<.u, v>. | (u e. B /\ v = {<.s, t>. | (s e. A /\ t = ((F` s)` u))})})` d))
256	196, 197, 255	mpbir2and 802	. . . . . . . . 9 |- (((A e. R /\ A.a e. A (F` a):B-->(C` a)) /\ c e. A) -> (F` c) = ((P` c) o. {<.u, v>. | (u e. B /\ v = {<.s, t>. | (s e. A /\ t = ((F` s)` u))})}))
257	256	r19.21aiva 2176	. . . . . . . 8 |- ((A e. R /\ A.a e. A (F` a):B-->(C` a)) -> A.c e. A (F` c) = ((P` c) o. {<.u, v>. | (u e. B /\ v = {<.s, t>. | (s e. A /\ t = ((F` s)` u))})}))
258		fveq2 4681	. . . . . . . . . 10 |- (c = a -> (F` c) = (F` a))
259		fveq2 4681	. . . . . . . . . . 11 |- (c = a -> (P` c) = (P` a))
260	259	coeq1d 4127	. . . . . . . . . 10 |- (c = a -> ((P` c) o. {<.u, v>. | (u e. B /\ v = {<.s, t>. | (s e. A /\ t = ((F` s)` u))})}) = ((P` a) o. {<.u, v>. | (u e. B /\ v = {<.s, t>. | (s e. A /\ t = ((F` s)` u))})}))
261	258, 260	eqeq12d 1899	. . . . . . . . 9 |- (c = a -> ((F` c) = ((P` c) o. {<.u, v>. | (u e. B /\ v = {<.s, t>. | (s e. A /\ t = ((F` s)` u))})}) <-> (F` a) = ((P` a) o. {<.u, v>. | (u e. B /\ v = {<.s, t>. | (s e. A /\ t = ((F` s)` u))})})))
262	261	cbvralv 2280	. . . . . . . 8 |- (A.c e. A (F` c) = ((P` c) o. {<.u, v>. | (u e. B /\ v = {<.s, t>. | (s e. A /\ t = ((F` s)` u))})}) <-> A.a e. A (F` a) = ((P` a) o. {<.u, v>. | (u e. B /\ v = {<.s, t>. | (s e. A /\ t = ((F` s)` u))})}))
263	257, 262	sylib 215	. . . . . . 7 |- ((A e. R /\ A.a e. A (F` a):B-->(C` a)) -> A.a e. A (F` a) = ((P` a) o. {<.u, v>. | (u e. B /\ v = {<.s, t>. | (s e. A /\ t = ((F` s)` u))})}))
264	263	3adant2 895	. . . . . 6 |- ((A e. R /\ B e. S /\ A.a e. A (F` a):B-->(C` a)) -> A.a e. A (F` a) = ((P` a) o. {<.u, v>. | (u e. B /\ v = {<.s, t>. | (s e. A /\ t = ((F` s)` u))})}))
265	148, 264	jca 310	. . . . 5 |- ((A e. R /\ B e. S /\ A.a e. A (F` a):B-->(C` a)) -> ({<.u, v>. | (u e. B /\ v = {<.s, t>. | (s e. A /\ t = ((F` s)` u))})}:B-->X /\ A.a e. A (F` a) = ((P` a) o. {<.u, v>. | (u e. B /\ v = {<.s, t>. | (s e. A /\ t = ((F` s)` u))})})))
266	115, 265	syl5cbir 228	. . . 4 |- ((A e. R /\ B e. S /\ A.a e. A (F` a):B-->(C` a)) -> (h = {<.u, v>. | (u e. B /\ v = {<.s, t>. | (s e. A /\ t = ((F` s)` u))})} -> (h:B-->X /\ A.a e. A (F` a) = ((P` a) o. h))))
267	110, 266	impbid 574	. . 3 |- ((A e. R /\ B e. S /\ A.a e. A (F` a):B-->(C` a)) -> ((h:B-->X /\ A.a e. A (F` a) = ((P` a) o. h)) <-> h = {<.u, v>. | (u e. B /\ v = {<.s, t>. | (s e. A /\ t = ((F` s)` u))})}))
268	267	eubidv 1779	. 2 |- ((A e. R /\ B e. S /\ A.a e. A (F` a):B-->(C` a)) -> (E!h(h:B-->X /\ A.a e. A (F` a) = ((P` a) o. h)) <-> E!h h = {<.u, v>. | (u e. B /\ v = {<.s, t>. | (s e. A /\ t = ((F` s)` u))})}))
269	4, 268	mpbird 213	1 |- ((A e. R /\ B e. S /\ A.a e. A (F` a):B-->(C` a)) -> E!h(h:B-->X /\ A.a e. A (F` a) = ((P` a) o. h)))

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240   /\ w3a 858   = wceq 1298   e. wcel 1300  E!weu 1771  A.wral 2105  _Vcvv 2292   C_ wss 2593  U_ciun 3255  {copab 3395  dom cdm 3986  ran crn 3987   o. ccom 3990  Fun wfun 3992   Fn wfn 3993  -->wf 3994  ` cfv 3998  X_cixp 5406

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-rep 3428  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-3an 860  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-rab 2112  df-v 2294  df-sbc 2454  df-csb 2541  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-iun 3257  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  df-ixp 5407

Copyright terms: Public domain