Theorem fvco 4736

Description: Value of a function composition. Similar to Exercise 5 of [TakeutiZaring] p. 28.

Assertion

Ref	Expression
fvco	|- ((Fun F /\ Fun G /\ A e. dom G) -> ((F o. G)` A) = (F` (G` A)))

Proof of Theorem fvco

Step	Hyp	Ref	Expression
1		dmfco 4735	. . . . . . . . 9 |- ((Fun G /\ A e. dom G) -> (A e. dom ( F o. G) <-> (G` A) e. dom F))
2	1	anbi2d 678	. . . . . . . 8 |- ((Fun G /\ A e. dom G) -> ((Fun F /\ A e. dom ( F o. G)) <-> (Fun F /\ (G` A) e. dom F)))
3		fvex 4689	. . . . . . . . . . . 12 |- (F` (G` A)) e. _V
4		opelco2g 4133	. . . . . . . . . . . 12 |- ((A e. dom G /\ (F` (G` A)) e. _V) -> (<.A, (F` (G` A))>. e. (F o. G) <-> E.z(<.A, z>. e. G /\ <.z, (F` (G` A))>. e. F)))
5	3, 4	mpan2 760	. . . . . . . . . . 11 |- (A e. dom G -> (<.A, (F` (G` A))>. e. (F o. G) <-> E.z(<.A, z>. e. G /\ <.z, (F` (G` A))>. e. F)))
6	5	adantl 424	. . . . . . . . . 10 |- ((Fun G /\ A e. dom G) -> (<.A, (F` (G` A))>. e. (F o. G) <-> E.z(<.A, z>. e. G /\ <.z, (F` (G` A))>. e. F)))
7		visset 2295	. . . . . . . . . . . . . . 15 |- z e. _V
8	7	funopfvb 4715	. . . . . . . . . . . . . 14 |- ((Fun G /\ A e. dom G) -> ((G` A) = z <-> <.A, z>. e. G))
9		eqcom 1886	. . . . . . . . . . . . . 14 |- (z = (G` A) <-> (G` A) = z)
10	8, 9	syl5bb 591	. . . . . . . . . . . . 13 |- ((Fun G /\ A e. dom G) -> (z = (G` A) <-> <.A, z>. e. G))
11	10	anbi1d 679	. . . . . . . . . . . 12 |- ((Fun G /\ A e. dom G) -> ((z = (G` A) /\ <.z, (F` (G` A))>. e. F) <-> (<.A, z>. e. G /\ <.z, (F` (G` A))>. e. F)))
12	11	exbidv 1657	. . . . . . . . . . 11 |- ((Fun G /\ A e. dom G) -> (E.z(z = (G` A) /\ <.z, (F` (G` A))>. e. F) <-> E.z(<.A, z>. e. G /\ <.z, (F` (G` A))>. e. F)))
13		fvex 4689	. . . . . . . . . . . 12 |- (G` A) e. _V
14		opeq1 3158	. . . . . . . . . . . . 13 |- (z = (G` A) -> <.z, (F` (G` A))>. = <.(G` A), (F` (G` A))>.)
15	14	eleq1d 1963	. . . . . . . . . . . 12 |- (z = (G` A) -> (<.z, (F` (G` A))>. e. F <-> <.(G` A), (F` (G` A))>. e. F))
16	13, 15	ceqsexv 2325	. . . . . . . . . . 11 |- (E.z(z = (G` A) /\ <.z, (F` (G` A))>. e. F) <-> <.(G` A), (F` (G` A))>. e. F)
17	12, 16	syl5bbr 593	. . . . . . . . . 10 |- ((Fun G /\ A e. dom G) -> (<.(G` A), (F` (G` A))>. e. F <-> E.z(<.A, z>. e. G /\ <.z, (F` (G` A))>. e. F)))
18	6, 17	bitr4d 590	. . . . . . . . 9 |- ((Fun G /\ A e. dom G) -> (<.A, (F` (G` A))>. e. (F o. G) <-> <.(G` A), (F` (G` A))>. e. F))
19		eqid 1884	. . . . . . . . . 10 |- (F` (G` A)) = (F` (G` A))
20	3	funopfvb 4715	. . . . . . . . . 10 |- ((Fun F /\ (G` A) e. dom F) -> ((F` (G` A)) = (F` (G` A)) <-> <.(G` A), (F` (G` A))>. e. F))
21	19, 20	mpbii 210	. . . . . . . . 9 |- ((Fun F /\ (G` A) e. dom F) -> <.(G` A), (F` (G` A))>. e. F)
22	18, 21	syl5bir 227	. . . . . . . 8 |- ((Fun G /\ A e. dom G) -> ((Fun F /\ (G` A) e. dom F) -> <.A, (F` (G` A))>. e. (F o. G)))
23	2, 22	sylbid 220	. . . . . . 7 |- ((Fun G /\ A e. dom G) -> ((Fun F /\ A e. dom ( F o. G)) -> <.A, (F` (G` A))>. e. (F o. G)))
24	23	exp4b 410	. . . . . 6 |- (Fun G -> (A e. dom G -> (Fun F -> (A e. dom ( F o. G) -> <.A, (F` (G` A))>. e. (F o. G)))))
25	24	com3r 39	. . . . 5 |- (Fun F -> (Fun G -> (A e. dom G -> (A e. dom ( F o. G) -> <.A, (F` (G` A))>. e. (F o. G)))))
26	25	3imp1 1081	. . . 4 |- (((Fun F /\ Fun G /\ A e. dom G) /\ A e. dom ( F o. G)) -> <.A, (F` (G` A))>. e. (F o. G))
27	3	funopfvb 4715	. . . . . 6 |- ((Fun (F o. G) /\ A e. dom ( F o. G)) -> (((F o. G)` A) = (F` (G` A)) <-> <.A, (F` (G` A))>. e. (F o. G)))
28		funco 4457	. . . . . 6 |- ((Fun F /\ Fun G) -> Fun (F o. G))
29	27, 28	sylan 497	. . . . 5 |- (((Fun F /\ Fun G) /\ A e. dom ( F o. G)) -> (((F o. G)` A) = (F` (G` A)) <-> <.A, (F` (G` A))>. e. (F o. G)))
30	29	3adantl3 1034	. . . 4 |- (((Fun F /\ Fun G /\ A e. dom G) /\ A e. dom ( F o. G)) -> (((F o. G)` A) = (F` (G` A)) <-> <.A, (F` (G` A))>. e. (F o. G)))
31	26, 30	mpbird 213	. . 3 |- (((Fun F /\ Fun G /\ A e. dom G) /\ A e. dom ( F o. G)) -> ((F o. G)` A) = (F` (G` A)))
32	31	ex 402	. 2 |- ((Fun F /\ Fun G /\ A e. dom G) -> (A e. dom ( F o. G) -> ((F o. G)` A) = (F` (G` A))))
33		ndmfv 4702	. . . . . 6 |- (-. A e. dom ( F o. G) -> ((F o. G)` A) = (/))
34	33	adantl 424	. . . . 5 |- (((Fun G /\ A e. dom G) /\ -. A e. dom ( F o. G)) -> ((F o. G)` A) = (/))
35	1	notbid 673	. . . . . . 7 |- ((Fun G /\ A e. dom G) -> (-. A e. dom ( F o. G) <-> -. (G` A) e. dom F))
36		ndmfv 4702	. . . . . . 7 |- (-. (G` A) e. dom F -> (F` (G` A)) = (/))
37	35, 36	syl6bi 231	. . . . . 6 |- ((Fun G /\ A e. dom G) -> (-. A e. dom ( F o. G) -> (F` (G` A)) = (/)))
38	37	imp 377	. . . . 5 |- (((Fun G /\ A e. dom G) /\ -. A e. dom ( F o. G)) -> (F` (G` A)) = (/))
39	34, 38	eqtr4d 1928	. . . 4 |- (((Fun G /\ A e. dom G) /\ -. A e. dom ( F o. G)) -> ((F o. G)` A) = (F` (G` A)))
40	39	ex 402	. . 3 |- ((Fun G /\ A e. dom G) -> (-. A e. dom ( F o. G) -> ((F o. G)` A) = (F` (G` A))))
41	40	3adant1 894	. 2 |- ((Fun F /\ Fun G /\ A e. dom G) -> (-. A e. dom ( F o. G) -> ((F o. G)` A) = (F` (G` A))))
42	32, 41	pm2.61d 141	1 |- ((Fun F /\ Fun G /\ A e. dom G) -> ((F o. G)` A) = (F` (G` A)))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 163   /\ wa 240   /\ w3a 858   = wceq 1298   e. wcel 1300  E.wex 1326  _Vcvv 2292  (/)c0 2875  <.cop 3046  dom cdm 3986   o. ccom 3990  Fun wfun 3992  ` cfv 3998

This theorem is referenced by:  fvco2 4737  fvco2OLD 4738  fopabco 4805  fopabcos 4806  ac6lem 5916  uzrdgvali 7714  cnpco 9046  cnmetdval 9180  vsfval 9586  imsdval 9649  oprabco 10159  upxp 10225  uptx 10226  txcnopab 10228  2txcn 10229  hocoi 11327  adjbdlnb 11654  injrec 14461  surjsec 14462  surjsec2 14467  issubcat 15193  cocanfo 15689  fnopabco 15711  f1ocan1fv 15717  upixp 15729  heiborlem33 15987  heiborlem34 15988  ghomco 16040  phtpycolem4 16054  reparpht 16065  pcocn 16076

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-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-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-fv 4014

Copyright terms: Public domain