Theorem funimaexglem 5301

Description: Lemma for funimaexg 5302. It constitutes the interesting part of funimaexg 5302, in which B C_ dom A. (Contributed by Jim Kingdon, 27-Dec-2018.)

Assertion

Ref	Expression
funimaexglem	|- ( ( Fun A /\ B e. C /\ B C_ dom A ) -> ( A " B ) e. _V )

Proof of Theorem funimaexglem

Dummy variables b x y z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		dffun7 5245	. . . . . . . . . 10 |- ( Fun A <-> ( Rel A /\ A. x e. dom A E* y x A y ) )
2	1	simprbi 275	. . . . . . . . 9 |- ( Fun A -> A. x e. dom A E* y x A y )
3	2	3ad2ant1 1018	. . . . . . . 8 |- ( ( Fun A /\ B e. C /\ B C_ dom A ) -> A. x e. dom A E* y x A y )
4		ssralv 3221	. . . . . . . . 9 |- ( B C_ dom A -> ( A. x e. dom A E* y x A y -> A. x e. B E* y x A y ) )
5	4	3ad2ant3 1020	. . . . . . . 8 |- ( ( Fun A /\ B e. C /\ B C_ dom A ) -> ( A. x e. dom A E* y x A y -> A. x e. B E* y x A y ) )
6	3, 5	mpd 13	. . . . . . 7 |- ( ( Fun A /\ B e. C /\ B C_ dom A ) -> A. x e. B E* y x A y )
7	6	alrimiv 1874	. . . . . 6 |- ( ( Fun A /\ B e. C /\ B C_ dom A ) -> A. z A. x e. B E* y x A y )
8		sseq1 3180	. . . . . . . . . . . . . . . . 17 |- ( b = B -> ( b C_ dom A <-> B C_ dom A ) )
9	8	biimpar 297	. . . . . . . . . . . . . . . 16 |- ( ( b = B /\ B C_ dom A ) -> b C_ dom A )
10	9	3adant1 1015	. . . . . . . . . . . . . . 15 |- ( ( Fun A /\ b = B /\ B C_ dom A ) -> b C_ dom A )
11		simp1 997	. . . . . . . . . . . . . . 15 |- ( ( Fun A /\ b = B /\ B C_ dom A ) -> Fun A )
12	10, 11	jca 306	. . . . . . . . . . . . . 14 |- ( ( Fun A /\ b = B /\ B C_ dom A ) -> ( b C_ dom A /\ Fun A ) )
13		dffun8 5246	. . . . . . . . . . . . . . . . . 18 |- ( Fun A <-> ( Rel A /\ A. x e. dom A E! y x A y ) )
14	13	simprbi 275	. . . . . . . . . . . . . . . . 17 |- ( Fun A -> A. x e. dom A E! y x A y )
15	14	adantl 277	. . . . . . . . . . . . . . . 16 |- ( ( b C_ dom A /\ Fun A ) -> A. x e. dom A E! y x A y )
16		ssel 3151	. . . . . . . . . . . . . . . . 17 |- ( b C_ dom A -> ( x e. b -> x e. dom A ) )
17	16	adantr 276	. . . . . . . . . . . . . . . 16 |- ( ( b C_ dom A /\ Fun A ) -> ( x e. b -> x e. dom A ) )
18		rsp 2524	. . . . . . . . . . . . . . . 16 |- ( A. x e. dom A E! y x A y -> ( x e. dom A -> E! y x A y ) )
19	15, 17, 18	sylsyld 58	. . . . . . . . . . . . . . 15 |- ( ( b C_ dom A /\ Fun A ) -> ( x e. b -> E! y x A y ) )
20	19	ralrimiv 2549	. . . . . . . . . . . . . 14 |- ( ( b C_ dom A /\ Fun A ) -> A. x e. b E! y x A y )
21		zfrep6 4122	. . . . . . . . . . . . . 14 |- ( A. x e. b E! y x A y -> E. z A. x e. b E. y e. z x A y )
22	12, 20, 21	3syl 17	. . . . . . . . . . . . 13 |- ( ( Fun A /\ b = B /\ B C_ dom A ) -> E. z A. x e. b E. y e. z x A y )
23		raleq 2673	. . . . . . . . . . . . . . 15 |- ( b = B -> ( A. x e. b E. y e. z x A y <-> A. x e. B E. y e. z x A y ) )
24	23	exbidv 1825	. . . . . . . . . . . . . 14 |- ( b = B -> ( E. z A. x e. b E. y e. z x A y <-> E. z A. x e. B E. y e. z x A y ) )
25	24	3ad2ant2 1019	. . . . . . . . . . . . 13 |- ( ( Fun A /\ b = B /\ B C_ dom A ) -> ( E. z A. x e. b E. y e. z x A y <-> E. z A. x e. B E. y e. z x A y ) )
26	22, 25	mpbid 147	. . . . . . . . . . . 12 |- ( ( Fun A /\ b = B /\ B C_ dom A ) -> E. z A. x e. B E. y e. z x A y )
27	26	3com12 1207	. . . . . . . . . . 11 |- ( ( b = B /\ Fun A /\ B C_ dom A ) -> E. z A. x e. B E. y e. z x A y )
28	27	3expib 1206	. . . . . . . . . 10 |- ( b = B -> ( ( Fun A /\ B C_ dom A ) -> E. z A. x e. B E. y e. z x A y ) )
29	28	vtocleg 2810	. . . . . . . . 9 |- ( B e. C -> ( ( Fun A /\ B C_ dom A ) -> E. z A. x e. B E. y e. z x A y ) )
30	29	3impib 1201	. . . . . . . 8 |- ( ( B e. C /\ Fun A /\ B C_ dom A ) -> E. z A. x e. B E. y e. z x A y )
31	30	3com12 1207	. . . . . . 7 |- ( ( Fun A /\ B e. C /\ B C_ dom A ) -> E. z A. x e. B E. y e. z x A y )
32		df-rex 2461	. . . . . . . . . 10 |- ( E. y e. z x A y <-> E. y ( y e. z /\ x A y ) )
33		exancom 1608	. . . . . . . . . 10 |- ( E. y ( y e. z /\ x A y ) <-> E. y ( x A y /\ y e. z ) )
34	32, 33	bitri 184	. . . . . . . . 9 |- ( E. y e. z x A y <-> E. y ( x A y /\ y e. z ) )
35	34	ralbii 2483	. . . . . . . 8 |- ( A. x e. B E. y e. z x A y <-> A. x e. B E. y ( x A y /\ y e. z ) )
36	35	exbii 1605	. . . . . . 7 |- ( E. z A. x e. B E. y e. z x A y <-> E. z A. x e. B E. y ( x A y /\ y e. z ) )
37	31, 36	sylib 122	. . . . . 6 |- ( ( Fun A /\ B e. C /\ B C_ dom A ) -> E. z A. x e. B E. y ( x A y /\ y e. z ) )
38		19.29 1620	. . . . . . 7 |- ( ( A. z A. x e. B E* y x A y /\ E. z A. x e. B E. y ( x A y /\ y e. z ) ) -> E. z ( A. x e. B E* y x A y /\ A. x e. B E. y ( x A y /\ y e. z ) ) )
39		nfcv 2319	. . . . . . . . . . 11 |- F/_ y B
40		nfmo1 2038	. . . . . . . . . . 11 |- F/ y E* y x A y
41	39, 40	nfralxy 2515	. . . . . . . . . 10 |- F/ y A. x e. B E* y x A y
42		nfe1 1496	. . . . . . . . . . 11 |- F/ y E. y ( x A y /\ y e. z )
43	39, 42	nfralxy 2515	. . . . . . . . . 10 |- F/ y A. x e. B E. y ( x A y /\ y e. z )
44	41, 43	nfan 1565	. . . . . . . . 9 |- F/ y ( A. x e. B E* y x A y /\ A. x e. B E. y ( x A y /\ y e. z ) )
45		r19.26 2603	. . . . . . . . . 10 |- ( A. x e. B ( E* y x A y /\ E. y ( x A y /\ y e. z ) ) <-> ( A. x e. B E* y x A y /\ A. x e. B E. y ( x A y /\ y e. z ) ) )
46		mopick 2104	. . . . . . . . . . 11 |- ( ( E* y x A y /\ E. y ( x A y /\ y e. z ) ) -> ( x A y -> y e. z ) )
47	46	ralimi 2540	. . . . . . . . . 10 |- ( A. x e. B ( E* y x A y /\ E. y ( x A y /\ y e. z ) ) -> A. x e. B ( x A y -> y e. z ) )
48	45, 47	sylbir 135	. . . . . . . . 9 |- ( ( A. x e. B E* y x A y /\ A. x e. B E. y ( x A y /\ y e. z ) ) -> A. x e. B ( x A y -> y e. z ) )
49	44, 48	alrimi 1522	. . . . . . . 8 |- ( ( A. x e. B E* y x A y /\ A. x e. B E. y ( x A y /\ y e. z ) ) -> A. y A. x e. B ( x A y -> y e. z ) )
50	49	eximi 1600	. . . . . . 7 |- ( E. z ( A. x e. B E* y x A y /\ A. x e. B E. y ( x A y /\ y e. z ) ) -> E. z A. y A. x e. B ( x A y -> y e. z ) )
51	38, 50	syl 14	. . . . . 6 |- ( ( A. z A. x e. B E* y x A y /\ E. z A. x e. B E. y ( x A y /\ y e. z ) ) -> E. z A. y A. x e. B ( x A y -> y e. z ) )
52	7, 37, 51	syl2anc 411	. . . . 5 |- ( ( Fun A /\ B e. C /\ B C_ dom A ) -> E. z A. y A. x e. B ( x A y -> y e. z ) )
53		r19.23v 2586	. . . . . . 7 |- ( A. x e. B ( x A y -> y e. z ) <-> ( E. x e. B x A y -> y e. z ) )
54	53	albii 1470	. . . . . 6 |- ( A. y A. x e. B ( x A y -> y e. z ) <-> A. y ( E. x e. B x A y -> y e. z ) )
55	54	exbii 1605	. . . . 5 |- ( E. z A. y A. x e. B ( x A y -> y e. z ) <-> E. z A. y ( E. x e. B x A y -> y e. z ) )
56	52, 55	sylib 122	. . . 4 |- ( ( Fun A /\ B e. C /\ B C_ dom A ) -> E. z A. y ( E. x e. B x A y -> y e. z ) )
57		abss 3226	. . . . 5 |- ( { y | E. x e. B x A y } C_ z <-> A. y ( E. x e. B x A y -> y e. z ) )
58	57	exbii 1605	. . . 4 |- ( E. z { y | E. x e. B x A y } C_ z <-> E. z A. y ( E. x e. B x A y -> y e. z ) )
59	56, 58	sylibr 134	. . 3 |- ( ( Fun A /\ B e. C /\ B C_ dom A ) -> E. z { y | E. x e. B x A y } C_ z )
60		dfima2 4974	. . . . 5 |- ( A " B ) = { y | E. x e. B x A y }
61	60	sseq1i 3183	. . . 4 |- ( ( A " B ) C_ z <-> { y | E. x e. B x A y } C_ z )
62	61	exbii 1605	. . 3 |- ( E. z ( A " B ) C_ z <-> E. z { y | E. x e. B x A y } C_ z )
63	59, 62	sylibr 134	. 2 |- ( ( Fun A /\ B e. C /\ B C_ dom A ) -> E. z ( A " B ) C_ z )
64		vex 2742	. . . 4 |- z e. _V
65	64	ssex 4142	. . 3 |- ( ( A " B ) C_ z -> ( A " B ) e. _V )
66	65	exlimiv 1598	. 2 |- ( E. z ( A " B ) C_ z -> ( A " B ) e. _V )
67	63, 66	syl 14	1 |- ( ( Fun A /\ B e. C /\ B C_ dom A ) -> ( A " B ) e. _V )

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105   /\ w3a 978   A.wal 1351   = wceq 1353   E.wex 1492   E!weu 2026   E*wmo 2027   e. wcel 2148   {cab 2163   A.wral 2455   E.wrex 2456   _Vcvv 2739   C_ wss 3131   class class class wbr 4005   dom cdm 4628   "cima 4631   Rel wrel 4633   Fun wfun 5212

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-14 2151  ax-ext 2159  ax-coll 4120  ax-sep 4123  ax-pow 4176  ax-pr 4211

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460  df-rex 2461  df-v 2741  df-un 3135  df-in 3137  df-ss 3144  df-pw 3579  df-sn 3600  df-pr 3601  df-op 3603  df-br 4006  df-opab 4067  df-id 4295  df-xp 4634  df-cnv 4636  df-co 4637  df-dm 4638  df-rn 4639  df-res 4640  df-ima 4641  df-fun 5220

This theorem is referenced by:  funimaexg  5302