Theorem ssimaex 3753

Description: The existence of a subimage.

Hypothesis

Ref	Expression
ssimaex.1	|- A e. V

Assertion

Ref	Expression
ssimaex	|- ((Fun F /\ B (_ (F"A)) -> E.x(x (_ A /\ B = (F"x)))

Distinct variable groups:   x,A   x,B   x,F

Proof of Theorem ssimaex

Step	Hyp	Ref	Expression
1		ssel2 2054	. . . . . . . . . 10 |- ((B (_ (F"(A i^i dom F)) /\ z e. B) -> z e. (F"(A i^i dom F)))
2	1	adantll 392	. . . . . . . . 9 |- (((Fun F /\ B (_ (F"(A i^i dom F))) /\ z e. B) -> z e. (F"(A i^i dom F)))
3		fvelima 3749	. . . . . . . . . . . . 13 |- ((Fun F /\ z e. (F"(A i^i dom F))) -> E.w e. (A i^i dom F)(F` w) = z)
4	3	ex 373	. . . . . . . . . . . 12 |- (Fun F -> (z e. (F"(A i^i dom F)) -> E.w e. (A i^i dom F)(F` w) = z))
5	4	adantr 389	. . . . . . . . . . 11 |- ((Fun F /\ z e. B) -> (z e. (F"(A i^i dom F)) -> E.w e. (A i^i dom F)(F` w) = z))
6		eleq1a 1535	. . . . . . . . . . . . . . . . 17 |- (z e. B -> ((F` w) = z -> (F` w) e. B))
7	6	anim2d 559	. . . . . . . . . . . . . . . 16 |- (z e. B -> ((w e. (A i^i dom F) /\ (F` w) = z) -> (w e. (A i^i dom F) /\ (F` w) e. B)))
8		fveq2 3709	. . . . . . . . . . . . . . . . . 18 |- (y = w -> (F` y) = (F` w))
9	8	eleq1d 1532	. . . . . . . . . . . . . . . . 17 |- (y = w -> ((F` y) e. B <-> (F` w) e. B))
10	9	elrab 1896	. . . . . . . . . . . . . . . 16 |- (w e. {y e. (A i^i dom F) | (F` y) e. B} <-> (w e. (A i^i dom F) /\ (F` w) e. B))
11	7, 10	syl6ibr 213	. . . . . . . . . . . . . . 15 |- (z e. B -> ((w e. (A i^i dom F) /\ (F` w) = z) -> w e. {y e. (A i^i dom F) | (F` y) e. B}))
12		pm3.27 323	. . . . . . . . . . . . . . . 16 |- ((w e. (A i^i dom F) /\ (F` w) = z) -> (F` w) = z)
13	12	a1i 8	. . . . . . . . . . . . . . 15 |- (z e. B -> ((w e. (A i^i dom F) /\ (F` w) = z) -> (F` w) = z))
14	11, 13	jcad 598	. . . . . . . . . . . . . 14 |- (z e. B -> ((w e. (A i^i dom F) /\ (F` w) = z) -> (w e. {y e. (A i^i dom F) | (F` y) e. B} /\ (F` w) = z)))
15	14	r19.22dv2 1728	. . . . . . . . . . . . 13 |- (z e. B -> (E.w e. (A i^i dom F)(F` w) = z -> E.w e. {y e. (A i^i dom F) | (F` y) e. B} (F` w) = z))
16	15	adantl 388	. . . . . . . . . . . 12 |- ((Fun F /\ z e. B) -> (E.w e. (A i^i dom F)(F` w) = z -> E.w e. {y e. (A i^i dom F) | (F` y) e. B} (F` w) = z))
17		funfn 3528	. . . . . . . . . . . . . 14 |- (Fun F <-> F Fn dom F)
18		ssrab2 2121	. . . . . . . . . . . . . . . 16 |- {y e. (A i^i dom F) | (F` y) e. B} (_ (A i^i dom F)
19		inss2 2221	. . . . . . . . . . . . . . . 16 |- (A i^i dom F) (_ dom F
20	18, 19	sstri 2063	. . . . . . . . . . . . . . 15 |- {y e. (A i^i dom F) | (F` y) e. B} (_ dom F
21		fvelimab 3750	. . . . . . . . . . . . . . 15 |- ((F Fn dom F /\ {y e. (A i^i dom F) | (F` y) e. B} (_ dom F) -> (z e. (F"{y e. (A i^i dom F) | (F` y) e. B}) <-> E.w e. {y e. (A i^i dom F) | (F` y) e. B} (F` w) = z))
22	20, 21	mpan2 694	. . . . . . . . . . . . . 14 |- (F Fn dom F -> (z e. (F"{y e. (A i^i dom F) | (F` y) e. B}) <-> E.w e. {y e. (A i^i dom F) | (F` y) e. B} (F` w) = z))
23	17, 22	sylbi 199	. . . . . . . . . . . . 13 |- (Fun F -> (z e. (F"{y e. (A i^i dom F) | (F` y) e. B}) <-> E.w e. {y e. (A i^i dom F) | (F` y) e. B} (F` w) = z))
24	23	adantr 389	. . . . . . . . . . . 12 |- ((Fun F /\ z e. B) -> (z e. (F"{y e. (A i^i dom F) | (F` y) e. B}) <-> E.w e. {y e. (A i^i dom F) | (F` y) e. B} (F` w) = z))
25	16, 24	sylibrd 204	. . . . . . . . . . 11 |- ((Fun F /\ z e. B) -> (E.w e. (A i^i dom F)(F` w) = z -> z e. (F"{y e. (A i^i dom F) | (F` y) e. B})))
26	5, 25	syld 27	. . . . . . . . . 10 |- ((Fun F /\ z e. B) -> (z e. (F"(A i^i dom F)) -> z e. (F"{y e. (A i^i dom F) | (F` y) e. B})))
27	26	adantlr 393	. . . . . . . . 9 |- (((Fun F /\ B (_ (F"(A i^i dom F))) /\ z e. B) -> (z e. (F"(A i^i dom F)) -> z e. (F"{y e. (A i^i dom F) | (F` y) e. B})))
28	2, 27	mpd 26	. . . . . . . 8 |- (((Fun F /\ B (_ (F"(A i^i dom F))) /\ z e. B) -> z e. (F"{y e. (A i^i dom F) | (F` y) e. B}))
29	28	ex 373	. . . . . . 7 |- ((Fun F /\ B (_ (F"(A i^i dom F))) -> (z e. B -> z e. (F"{y e. (A i^i dom F) | (F` y) e. B})))
30		fvelima 3749	. . . . . . . . . 10 |- ((Fun F /\ z e. (F"{y e. (A i^i dom F) | (F` y) e. B})) -> E.w e. {y e. (A i^i dom F) | (F` y) e. B} (F` w) = z)
31	30	ex 373	. . . . . . . . 9 |- (Fun F -> (z e. (F"{y e. (A i^i dom F) | (F` y) e. B}) -> E.w e. {y e. (A i^i dom F) | (F` y) e. B} (F` w) = z))
32		eleq1 1526	. . . . . . . . . . . . 13 |- ((F` w) = z -> ((F` w) e. B <-> z e. B))
33	32	biimpcd 155	. . . . . . . . . . . 12 |- ((F` w) e. B -> ((F` w) = z -> z e. B))
34	33	adantl 388	. . . . . . . . . . 11 |- ((w e. (A i^i dom F) /\ (F` w) e. B) -> ((F` w) = z -> z e. B))
35	10, 34	sylbi 199	. . . . . . . . . 10 |- (w e. {y e. (A i^i dom F) | (F` y) e. B} -> ((F` w) = z -> z e. B))
36	35	r19.23aiv 1735	. . . . . . . . 9 |- (E.w e. {y e. (A i^i dom F) | (F` y) e. B} (F` w) = z -> z e. B)
37	31, 36	syl6 22	. . . . . . . 8 |- (Fun F -> (z e. (F"{y e. (A i^i dom F) | (F` y) e. B}) -> z e. B))
38	37	adantr 389	. . . . . . 7 |- ((Fun F /\ B (_ (F"(A i^i dom F))) -> (z e. (F"{y e. (A i^i dom F) | (F` y) e. B}) -> z e. B))
39	29, 38	impbid 514	. . . . . 6 |- ((Fun F /\ B (_ (F"(A i^i dom F))) -> (z e. B <-> z e. (F"{y e. (A i^i dom F) | (F` y) e. B})))
40	39	eqrdv 1466	. . . . 5 |- ((Fun F /\ B (_ (F"(A i^i dom F))) -> B = (F"{y e. (A i^i dom F) | (F` y) e. B}))
41	40, 18	jctil 292	. . . 4 |- ((Fun F /\ B (_ (F"(A i^i dom F))) -> ({y e. (A i^i dom F) | (F` y) e. B} (_ (A i^i dom F) /\ B = (F"{y e. (A i^i dom F) | (F` y) e. B})))
42		ssimaex.1	. . . . . . 7 |- A e. V
43	42	inex1 2706	. . . . . 6 |- (A i^i dom F) e. V
44	43	rabex 2715	. . . . 5 |- {y e. (A i^i dom F) | (F` y) e. B} e. V
45		sseq1 2072	. . . . . 6 |- (x = {y e. (A i^i dom F) | (F` y) e. B} -> (x (_ (A i^i dom F) <-> {y e. (A i^i dom F) | (F` y) e. B} (_ (A i^i dom F)))
46		imaeq2 3386	. . . . . . 7 |- (x = {y e. (A i^i dom F) | (F` y) e. B} -> (F"x) = (F"{y e. (A i^i dom F) | (F` y) e. B}))
47	46	eqeq2d 1478	. . . . . 6 |- (x = {y e. (A i^i dom F) | (F` y) e. B} -> (B = (F"x) <-> B = (F"{y e. (A i^i dom F) | (F` y) e. B})))
48	45, 47	anbi12d 626	. . . . 5 |- (x = {y e. (A i^i dom F) | (F` y) e. B}