ssimaex

		Ref	Expression
	Hypothesis	ssimaex.1	$⊢ A \in V$
	Assertion	ssimaex	$⊢ (Fun F \land B \subseteq F [A]) \to \exists x (x \subseteq A \land B = F [x])$

Proof

Step	Hyp	Ref	Expression
1		ssimaex.1	$⊢ A \in V$
2		dmres	$⊢ dom ({F ↾}_{A}) = A \cap dom F$
3	2	imaeq2i	$⊢ F [dom ({F ↾}_{A})] = F [A \cap dom F]$
4		imadmres	$⊢ F [dom ({F ↾}_{A})] = F [A]$
5	3 4	eqtr3i	$⊢ F [A \cap dom F] = F [A]$
6	5	sseq2i	$⊢ B \subseteq F [A \cap dom F] \leftrightarrow B \subseteq F [A]$
7		ssrab2	$⊢ \{y \in (A \cap dom F) \| F (y) \in B\} \subseteq A \cap dom F$
8		ssel2	$⊢ (B \subseteq F [A \cap dom F] \land z \in B) \to z \in F [A \cap dom F]$
9	8	adantll	$⊢ ((Fun F \land B \subseteq F [A \cap dom F]) \land z \in B) \to z \in F [A \cap dom F]$
10		fvelima	$⊢ (Fun F \land z \in F [A \cap dom F]) \to \exists w \in (A \cap dom F) F (w) = z$
11	10	ex	$⊢ Fun F \to (z \in F [A \cap dom F] \to \exists w \in (A \cap dom F) F (w) = z)$
12	11	adantr	$⊢ (Fun F \land z \in B) \to (z \in F [A \cap dom F] \to \exists w \in (A \cap dom F) F (w) = z)$
13		eleq1a	$⊢ z \in B \to (F (w) = z \to F (w) \in B)$
14	13	anim2d	$⊢ z \in B \to ((w \in (A \cap dom F) \land F (w) = z) \to (w \in (A \cap dom F) \land F (w) \in B))$
15		fveq2	$⊢ y = w \to F (y) = F (w)$
16	15	eleq1d	$⊢ y = w \to (F (y) \in B \leftrightarrow F (w) \in B)$
17	16	elrab	$⊢ w \in \{y \in (A \cap dom F) \| F (y) \in B\} \leftrightarrow (w \in (A \cap dom F) \land F (w) \in B)$
18	14 17	syl6ibr	$⊢ z \in B \to ((w \in (A \cap dom F) \land F (w) = z) \to w \in \{y \in (A \cap dom F) \| F (y) \in B\})$
19		simpr	$⊢ (w \in (A \cap dom F) \land F (w) = z) \to F (w) = z$
20	18 19	jca2	$⊢ z \in B \to ((w \in (A \cap dom F) \land F (w) = z) \to (w \in \{y \in (A \cap dom F) \| F (y) \in B\} \land F (w) = z))$
21	20	reximdv2	$⊢ z \in B \to (\exists w \in (A \cap dom F) F (w) = z \to \exists w \in \{y \in (A \cap dom F) \| F (y) \in B\} F (w) = z)$
22	21	adantl	$⊢ (Fun F \land z \in B) \to (\exists w \in (A \cap dom F) F (w) = z \to \exists w \in \{y \in (A \cap dom F) \| F (y) \in B\} F (w) = z)$
23		funfn	$⊢ Fun F \leftrightarrow F Fn dom F$
24		inss2	$⊢ A \cap dom F \subseteq dom F$
25	7 24	sstri	$⊢ \{y \in (A \cap dom F) \| F (y) \in B\} \subseteq dom F$
26		fvelimab	$⊢ (F Fn dom F \land \{y \in (A \cap dom F) \| F (y) \in B\} \subseteq dom F) \to (z \in F [\{y \in (A \cap dom F) \| F (y) \in B\}] \leftrightarrow \exists w \in \{y \in (A \cap dom F) \| F (y) \in B\} F (w) = z)$
27	25 26	mpan2	$⊢ F Fn dom F \to (z \in F [\{y \in (A \cap dom F) \| F (y) \in B\}] \leftrightarrow \exists w \in \{y \in (A \cap dom F) \| F (y) \in B\} F (w) = z)$
28	23 27	sylbi	$⊢ Fun F \to (z \in F [\{y \in (A \cap dom F) \| F (y) \in B\}] \leftrightarrow \exists w \in \{y \in (A \cap dom F) \| F (y) \in B\} F (w) = z)$
29	28	adantr	$⊢ (Fun F \land z \in B) \to (z \in F [\{y \in (A \cap dom F) \| F (y) \in B\}] \leftrightarrow \exists w \in \{y \in (A \cap dom F) \| F (y) \in B\} F (w) = z)$
30	22 29	sylibrd	$⊢ (Fun F \land z \in B) \to (\exists w \in (A \cap dom F) F (w) = z \to z \in F [\{y \in (A \cap dom F) \| F (y) \in B\}])$
31	12 30	syld	$⊢ (Fun F \land z \in B) \to (z \in F [A \cap dom F] \to z \in F [\{y \in (A \cap dom F) \| F (y) \in B\}])$
32	31	adantlr	$⊢ ((Fun F \land B \subseteq F [A \cap dom F]) \land z \in B) \to (z \in F [A \cap dom F] \to z \in F [\{y \in (A \cap dom F) \| F (y) \in B\}])$
33	9 32	mpd	$⊢ ((Fun F \land B \subseteq F [A \cap dom F]) \land z \in B) \to z \in F [\{y \in (A \cap dom F) \| F (y) \in B\}]$
34	33	ex	$⊢ (Fun F \land B \subseteq F [A \cap dom F]) \to (z \in B \to z \in F [\{y \in (A \cap dom F) \| F (y) \in B\}])$
35		fvelima	$⊢ (Fun F \land z \in F [\{y \in (A \cap dom F) \| F (y) \in B\}]) \to \exists w \in \{y \in (A \cap dom F) \| F (y) \in B\} F (w) = z$
36	35	ex	$⊢ Fun F \to (z \in F [\{y \in (A \cap dom F) \| F (y) \in B\}] \to \exists w \in \{y \in (A \cap dom F) \| F (y) \in B\} F (w) = z)$
37		eleq1	$⊢ F (w) = z \to (F (w) \in B \leftrightarrow z \in B)$
38	37	biimpcd	$⊢ F (w) \in B \to (F (w) = z \to z \in B)$
39	38	adantl	$⊢ (w \in (A \cap dom F) \land F (w) \in B) \to (F (w) = z \to z \in B)$
40	17 39	sylbi	$⊢ w \in \{y \in (A \cap dom F) \| F (y) \in B\} \to (F (w) = z \to z \in B)$
41	40	rexlimiv	$⊢ \exists w \in \{y \in (A \cap dom F) \| F (y) \in B\} F (w) = z \to z \in B$
42	36 41	syl6	$⊢ Fun F \to (z \in F [\{y \in (A \cap dom F) \| F (y) \in B\}] \to z \in B)$
43	42	adantr	$⊢ (Fun F \land B \subseteq F [A \cap dom F]) \to (z \in F [\{y \in (A \cap dom F) \| F (y) \in B\}] \to z \in B)$
44	34 43	impbid	$⊢ (Fun F \land B \subseteq F [A \cap dom F]) \to (z \in B \leftrightarrow z \in F [\{y \in (A \cap dom F) \| F (y) \in B\}])$
45	44	eqrdv	$⊢ (Fun F \land B \subseteq F [A \cap dom F]) \to B = F [\{y \in (A \cap dom F) \| F (y) \in B\}]$
46	1	inex1	$⊢ A \cap dom F \in V$
47	46	rabex	$⊢ \{y \in (A \cap dom F) \| F (y) \in B\} \in V$
48		sseq1	$⊢ x = \{y \in (A \cap dom F) \| F (y) \in B\} \to (x \subseteq A \cap dom F \leftrightarrow \{y \in (A \cap dom F) \| F (y) \in B\} \subseteq A \cap dom F)$
49		imaeq2	$⊢ x = \{y \in (A \cap dom F) \| F (y) \in B\} \to F [x] = F [\{y \in (A \cap dom F) \| F (y) \in B\}]$
50	49	eqeq2d	$⊢ x = \{y \in (A \cap dom F) \| F (y) \in B\} \to (B = F [x] \leftrightarrow B = F [\{y \in (A \cap dom F) \| F (y) \in B\}])$
51	48 50	anbi12d	$⊢ x = \{y \in (A \cap dom F) \| F (y) \in B\} \to ((x \subseteq A \cap dom F \land B = F [x]) \leftrightarrow (\{y \in (A \cap dom F) \| F (y) \in B\} \subseteq A \cap dom F \land B = F [\{y \in (A \cap dom F) \| F (y) \in B\}]))$
52	47 51	spcev	$⊢ (\{y \in (A \cap dom F) \| F (y) \in B\} \subseteq A \cap dom F \land B = F [\{y \in (A \cap dom F) \| F (y) \in B\}]) \to \exists x (x \subseteq A \cap dom F \land B = F [x])$
53	7 45 52	sylancr	$⊢ (Fun F \land B \subseteq F [A \cap dom F]) \to \exists x (x \subseteq A \cap dom F \land B = F [x])$
54		inss1	$⊢ A \cap dom F \subseteq A$
55		sstr	$⊢ (x \subseteq A \cap dom F \land A \cap dom F \subseteq A) \to x \subseteq A$
56	54 55	mpan2	$⊢ x \subseteq A \cap dom F \to x \subseteq A$
57	56	anim1i	$⊢ (x \subseteq A \cap dom F \land B = F [x]) \to (x \subseteq A \land B = F [x])$
58	57	eximi	$⊢ \exists x (x \subseteq A \cap dom F \land B = F [x]) \to \exists x (x \subseteq A \land B = F [x])$
59	53 58	syl	$⊢ (Fun F \land B \subseteq F [A \cap dom F]) \to \exists x (x \subseteq A \land B = F [x])$
60	6 59	sylan2br	$⊢ (Fun F \land B \subseteq F [A]) \to \exists x (x \subseteq A \land B = F [x])$

Metamath Proof Explorer

Theorem ssimaex

Proof