Theorem fnopabco2b 14734

Description: Composition of a function with a function abstraction. Adapted from fnopabco 15711.

Hypotheses

Ref	Expression
fnopabco2b.2	|- F = {<.x, y>. | (x e. A /\ y = B)}
fnopabco2b.	|- G = {<.x, y>. | (x e. A /\ y = (H` B))}

Assertion

Ref	Expression
fnopabco2b	|- ((A.x e. A B e. C /\ H Fn C) -> G = (H o. F))

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

Proof of Theorem fnopabco2b

Step	Hyp	Ref	Expression
1		hbra1 2147	. . . 4 |- (A.x e. A B e. C -> A.xA.x e. A B e. C)
2		ax-17 1317	. . . 4 |- (H Fn C -> A.x H Fn C)
3	1, 2	hban 1356	. . 3 |- ((A.x e. A B e. C /\ H Fn C) -> A.x(A.x e. A B e. C /\ H Fn C))
4		ra4 2155	. . . . . . . . 9 |- (A.x e. A B e. C -> (x e. A -> B e. C))
5		fvopab2 4754	. . . . . . . . . . . . . . . 16 |- ((x e. A /\ B e. C) -> ({<.x, y>. | (x e. A /\ y = B)}` x) = B)
6		fnopabco2b.2	. . . . . . . . . . . . . . . . . 18 |- F = {<.x, y>. | (x e. A /\ y = B)}
7	6	eqcomi 1888	. . . . . . . . . . . . . . . . 17 |- {<.x, y>. | (x e. A /\ y = B)} = F
8	7	fveq1i 4682	. . . . . . . . . . . . . . . 16 |- ({<.x, y>. | (x e. A /\ y = B)}` x) = (F` x)
9	5, 8	syl5eqr 1942	. . . . . . . . . . . . . . 15 |- ((x e. A /\ B e. C) -> (F` x) = B)
10	9	ancoms 484	. . . . . . . . . . . . . 14 |- ((B e. C /\ x e. A) -> (F` x) = B)
11	10	3adant3 896	. . . . . . . . . . . . 13 |- ((B e. C /\ x e. A /\ H Fn C) -> (F` x) = B)
12	11	fveq2d 4685	. . . . . . . . . . . 12 |- ((B e. C /\ x e. A /\ H Fn C) -> (H` (F` x)) = (H` B))
13	12	3adant2r 1093	. . . . . . . . . . 11 |- ((B e. C /\ (x e. A /\ A.x e. A B e. C) /\ H Fn C) -> (H` (F` x)) = (H` B))
14		fnfun 4510	. . . . . . . . . . . . 13 |- (H Fn C -> Fun H)
15	14	3ad2ant3 899	. . . . . . . . . . . 12 |- ((B e. C /\ (x e. A /\ A.x e. A B e. C) /\ H Fn C) -> Fun H)
16		elisset 2299	. . . . . . . . . . . . . . . 16 |- (B e. C -> B e. _V)
17	16	ralimi 2168	. . . . . . . . . . . . . . 15 |- (A.x e. A B e. C -> A.x e. A B e. _V)
18	6	fnopab2g 4547	. . . . . . . . . . . . . . 15 |- (A.x e. A B e. _V <-> F Fn A)
19	17, 18	sylib 215	. . . . . . . . . . . . . 14 |- (A.x e. A B e. C -> F Fn A)
20	19	adantl 424	. . . . . . . . . . . . 13 |- ((x e. A /\ A.x e. A B e. C) -> F Fn A)
21	20	3ad2ant2 898	. . . . . . . . . . . 12 |- ((B e. C /\ (x e. A /\ A.x e. A B e. C) /\ H Fn C) -> F Fn A)
22		simp2l 902	. . . . . . . . . . . 12 |- ((B e. C /\ (x e. A /\ A.x e. A B e. C) /\ H Fn C) -> x e. A)
23		fvco2 4737	. . . . . . . . . . . 12 |- ((Fun H /\ F Fn A /\ x e. A) -> ((H o. F)` x) = (H` (F` x)))
24	15, 21, 22, 23	syl111anc 1100	. . . . . . . . . . 11 |- ((B e. C /\ (x e. A /\ A.x e. A B e. C) /\ H Fn C) -> ((H o. F)` x) = (H` (F` x)))
25		simpl 346	. . . . . . . . . . . . . . 15 |- ((x e. A /\ A.x e. A B e. C) -> x e. A)
26		fvex 4689	. . . . . . . . . . . . . . 15 |- (H` B) e. _V
27	25, 26	jctir 317	. . . . . . . . . . . . . 14 |- ((x e. A /\ A.x e. A B e. C) -> (x e. A /\ (H` B) e. _V))
28	27	3ad2ant2 898	. . . . . . . . . . . . 13 |- ((B e. C /\ (x e. A /\ A.x e. A B e. C) /\ H Fn C) -> (x e. A /\ (H` B) e. _V))
29		fvopab2 4754	. . . . . . . . . . . . 13 |- ((x e. A /\ (H` B) e. _V) -> ({<.x, y>. | (x e. A /\ y = (H` B))}` x) = (H` B))
30	28, 29	syl 12	. . . . . . . . . . . 12 |- ((B e. C /\ (x e. A /\ A.x e. A B e. C) /\ H Fn C) -> ({<.x, y>. | (x e. A /\ y = (H` B))}` x) = (H` B))
31		fnopabco2b.	. . . . . . . . . . . . 13 |- G = {<.x, y>. | (x e. A /\ y = (H` B))}
32	31	fveq1i 4682	. . . . . . . . . . . 12 |- (G` x) = ({<.x, y>. | (x e. A /\ y = (H` B))}` x)
33	30, 32	syl5eq 1940	. . . . . . . . . . 11 |- ((B e. C /\ (x e. A /\ A.x e. A B e. C) /\ H Fn C) -> (G` x) = (H` B))
34	13, 24, 33	3eqtr4rd 1939	. . . . . . . . . 10 |- ((B e. C /\ (x e. A /\ A.x e. A B e. C) /\ H Fn C) -> (G` x) = ((H o. F)` x))
35	34	3exp 1066	. . . . . . . . 9 |- (B e. C -> ((x e. A /\ A.x e. A B e. C) -> (H Fn C -> (G` x) = ((H o. F)` x))))
36	4, 35	syl6com 64	. . . . . . . 8 |- (x e. A -> (A.x e. A B e. C -> ((x e. A /\ A.x e. A B e. C) -> (H Fn C -> (G` x) = ((H o. F)` x)))))
37	36	imp 377	. . . . . . 7 |- ((x e. A /\ A.x e. A B e. C) -> ((x e. A /\ A.x e. A B e. C) -> (H Fn C -> (G` x) = ((H o. F)` x))))
38	37	pm2.43i 78	. . . . . 6 |- ((x e. A /\ A.x e. A B e. C) -> (H Fn C -> (G` x) = ((H o. F)` x)))
39	38	ex 402	. . . . 5 |- (x e. A -> (A.x e. A B e. C -> (H Fn C -> (G` x) = ((H o. F)` x))))
40	39	com3l 38	. . . 4 |- (A.x e. A B e. C -> (H Fn C -> (x e. A -> (G` x) = ((H o. F)` x))))
41	40	imp 377	. . 3 |- ((A.x e. A B e. C /\ H Fn C) -> (x e. A -> (G` x) = ((H o. F)` x)))
42	3, 41	r19.21ai 2174	. 2 |- ((A.x e. A B e. C /\ H Fn C) -> A.x e. A (G` x) = ((H o. F)` x))
43		hbopab1 3562	. . . . 5 |- (t e. {<.x, y>. | (x e. A /\ y = (H` B))} -> A.x t e. {<.x, y>. | (x e. A /\ y = (H` B))})
44	31, 43	hbxfr 1992	. . . 4 |- (t e. G -> A.x t e. G)
45		ax-17 1317	. . . . 5 |- (t e. H -> A.x t e. H)
46		hbopab1 3562	. . . . . 6 |- (t e. {<.x, y>. | (x e. A /\ y = B)} -> A.x t e. {<.x, y>. | (x e. A /\ y = B)})
47	6, 46	hbxfr 1992	. . . . 5 |- (t e. F -> A.x t e. F)
48	45, 47	hbco 4129	. . . 4 |- (t e. (H o. F) -> A.x t e. (H o. F))
49	44, 48	eqfnfv2f 4770	. . 3 |- ((G Fn A /\ (H o. F) Fn A) -> (G = (H o. F) <-> A.x e. A (G` x) = ((H o. F)` x)))
50	26, 31	fnopab2 4549	. . 3 |- G Fn A
51		simpr 350	. . . 4 |- ((A.x e. A B e. C /\ H Fn C) -> H Fn C)
52	19	adantr 425	. . . 4 |- ((A.x e. A B e. C /\ H Fn C) -> F Fn A)
53	6	fopab2 4796	. . . . . . 7 |- (A.x e. A B e. C <-> F:A-->C)
54	53	biimpi 168	. . . . . 6 |- (A.x e. A B e. C -> F:A-->C)
55	54	adantr 425	. . . . 5 |- ((A.x e. A B e. C /\ H Fn C) -> F:A-->C)
56		frn 4569	. . . . 5 |- (F:A-->C -> ran F C_ C)
57	55, 56	syl 12	. . . 4 |- ((A.x e. A B e. C /\ H Fn C) -> ran F C_ C)
58		fnco 4521	. . . 4 |- ((H Fn C /\ F Fn A /\ ran F C_ C) -> (H o. F) Fn A)
59	51, 52, 57, 58	syl111anc 1100	. . 3 |- ((A.x e. A B e. C /\ H Fn C) -> (H o. F) Fn A)
60	49, 50, 59	sylancr 526	. 2 |- ((A.x e. A B e. C /\ H Fn C) -> (G = (H o. F) <-> A.x e. A (G` x) = ((H o. F)` x)))
61	42, 60	mpbird 213	1 |- ((A.x e. A B e. C /\ H Fn C) -> G = (H o. F))

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

This theorem is referenced by:  curgrpact 14735  trhom 14983

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-f 4010  df-fv 4014

Copyright terms: Public domain