Theorem ssimaex 5579

Description: The existence of a subimage. (Contributed by NM, 8-Apr-2007.)

Hypothesis

Ref	Expression
ssimaex.1	⊢ 𝐴 ∈ V

Assertion

Ref	Expression
ssimaex	⊢ ((Fun 𝐹 ∧ 𝐵 ⊆ (𝐹 “ 𝐴)) → ∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝐵 = (𝐹 “ 𝑥)))

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝑥,𝐹

Proof of Theorem ssimaex

Dummy variables 𝑤 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		dmres 4930	. . . . 5 ⊢ dom (𝐹 ↾ 𝐴) = (𝐴 ∩ dom 𝐹)
2	1	imaeq2i 4970	. . . 4 ⊢ (𝐹 “ dom (𝐹 ↾ 𝐴)) = (𝐹 “ (𝐴 ∩ dom 𝐹))
3		imadmres 5123	. . . 4 ⊢ (𝐹 “ dom (𝐹 ↾ 𝐴)) = (𝐹 “ 𝐴)
4	2, 3	eqtr3i 2200	. . 3 ⊢ (𝐹 “ (𝐴 ∩ dom 𝐹)) = (𝐹 “ 𝐴)
5	4	sseq2i 3184	. 2 ⊢ (𝐵 ⊆ (𝐹 “ (𝐴 ∩ dom 𝐹)) ↔ 𝐵 ⊆ (𝐹 “ 𝐴))
6		ssrab2 3242	. . . 4 ⊢ {𝑦 ∈ (𝐴 ∩ dom 𝐹) ∣ (𝐹‘𝑦) ∈ 𝐵} ⊆ (𝐴 ∩ dom 𝐹)
7		ssel2 3152	. . . . . . . . 9 ⊢ ((𝐵 ⊆ (𝐹 “ (𝐴 ∩ dom 𝐹)) ∧ 𝑧 ∈ 𝐵) → 𝑧 ∈ (𝐹 “ (𝐴 ∩ dom 𝐹)))
8	7	adantll 476	. . . . . . . 8 ⊢ (((Fun 𝐹 ∧ 𝐵 ⊆ (𝐹 “ (𝐴 ∩ dom 𝐹))) ∧ 𝑧 ∈ 𝐵) → 𝑧 ∈ (𝐹 “ (𝐴 ∩ dom 𝐹)))
9		fvelima 5569	. . . . . . . . . . . 12 ⊢ ((Fun 𝐹 ∧ 𝑧 ∈ (𝐹 “ (𝐴 ∩ dom 𝐹))) → ∃𝑤 ∈ (𝐴 ∩ dom 𝐹)(𝐹‘𝑤) = 𝑧)
10	9	ex 115	. . . . . . . . . . 11 ⊢ (Fun 𝐹 → (𝑧 ∈ (𝐹 “ (𝐴 ∩ dom 𝐹)) → ∃𝑤 ∈ (𝐴 ∩ dom 𝐹)(𝐹‘𝑤) = 𝑧))
11	10	adantr 276	. . . . . . . . . 10 ⊢ ((Fun 𝐹 ∧ 𝑧 ∈ 𝐵) → (𝑧 ∈ (𝐹 “ (𝐴 ∩ dom 𝐹)) → ∃𝑤 ∈ (𝐴 ∩ dom 𝐹)(𝐹‘𝑤) = 𝑧))
12		eleq1a 2249	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ 𝐵 → ((𝐹‘𝑤) = 𝑧 → (𝐹‘𝑤) ∈ 𝐵))
13	12	anim2d 337	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ 𝐵 → ((𝑤 ∈ (𝐴 ∩ dom 𝐹) ∧ (𝐹‘𝑤) = 𝑧) → (𝑤 ∈ (𝐴 ∩ dom 𝐹) ∧ (𝐹‘𝑤) ∈ 𝐵)))
14		fveq2 5517	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑤 → (𝐹‘𝑦) = (𝐹‘𝑤))
15	14	eleq1d 2246	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑤 → ((𝐹‘𝑦) ∈ 𝐵 ↔ (𝐹‘𝑤) ∈ 𝐵))
16	15	elrab 2895	. . . . . . . . . . . . . . 15 ⊢ (𝑤 ∈ {𝑦 ∈ (𝐴 ∩ dom 𝐹) ∣ (𝐹‘𝑦) ∈ 𝐵} ↔ (𝑤 ∈ (𝐴 ∩ dom 𝐹) ∧ (𝐹‘𝑤) ∈ 𝐵))
17	13, 16	imbitrrdi 162	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ 𝐵 → ((𝑤 ∈ (𝐴 ∩ dom 𝐹) ∧ (𝐹‘𝑤) = 𝑧) → 𝑤 ∈ {𝑦 ∈ (𝐴 ∩ dom 𝐹) ∣ (𝐹‘𝑦) ∈ 𝐵}))
18		simpr 110	. . . . . . . . . . . . . . 15 ⊢ ((𝑤 ∈ (𝐴 ∩ dom 𝐹) ∧ (𝐹‘𝑤) = 𝑧) → (𝐹‘𝑤) = 𝑧)
19	18	a1i 9	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ 𝐵 → ((𝑤 ∈ (𝐴 ∩ dom 𝐹) ∧ (𝐹‘𝑤) = 𝑧) → (𝐹‘𝑤) = 𝑧))
20	17, 19	jcad 307	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ 𝐵 → ((𝑤 ∈ (𝐴 ∩ dom 𝐹) ∧ (𝐹‘𝑤) = 𝑧) → (𝑤 ∈ {𝑦 ∈ (𝐴 ∩ dom 𝐹) ∣ (𝐹‘𝑦) ∈ 𝐵} ∧ (𝐹‘𝑤) = 𝑧)))
21	20	reximdv2 2576	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ 𝐵 → (∃𝑤 ∈ (𝐴 ∩ dom 𝐹)(𝐹‘𝑤) = 𝑧 → ∃𝑤 ∈ {𝑦 ∈ (𝐴 ∩ dom 𝐹) ∣ (𝐹‘𝑦) ∈ 𝐵} (𝐹‘𝑤) = 𝑧))
22	21	adantl 277	. . . . . . . . . . 11 ⊢ ((Fun 𝐹 ∧ 𝑧 ∈ 𝐵) → (∃𝑤 ∈ (𝐴 ∩ dom 𝐹)(𝐹‘𝑤) = 𝑧 → ∃𝑤 ∈ {𝑦 ∈ (𝐴 ∩ dom 𝐹) ∣ (𝐹‘𝑦) ∈ 𝐵} (𝐹‘𝑤) = 𝑧))
23		funfn 5248	. . . . . . . . . . . . 13 ⊢ (Fun 𝐹 ↔ 𝐹 Fn dom 𝐹)
24		inss2 3358	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∩ dom 𝐹) ⊆ dom 𝐹
25	6, 24	sstri 3166	. . . . . . . . . . . . . 14 ⊢ {𝑦 ∈ (𝐴 ∩ dom 𝐹) ∣ (𝐹‘𝑦) ∈ 𝐵} ⊆ dom 𝐹
26		fvelimab 5574	. . . . . . . . . . . . . 14 ⊢ ((𝐹 Fn dom 𝐹 ∧ {𝑦 ∈ (𝐴 ∩ dom 𝐹) ∣ (𝐹‘𝑦) ∈ 𝐵} ⊆ dom 𝐹) → (𝑧 ∈ (𝐹 “ {𝑦 ∈ (𝐴 ∩ dom 𝐹) ∣ (𝐹‘𝑦) ∈ 𝐵}) ↔ ∃𝑤 ∈ {𝑦 ∈ (𝐴 ∩ dom 𝐹) ∣ (𝐹‘𝑦) ∈ 𝐵} (𝐹‘𝑤) = 𝑧))
27	25, 26	mpan2 425	. . . . . . . . . . . . 13 ⊢ (𝐹 Fn dom 𝐹 → (𝑧 ∈ (𝐹 “ {𝑦 ∈ (𝐴 ∩ dom 𝐹) ∣ (𝐹‘𝑦) ∈ 𝐵}) ↔ ∃𝑤 ∈ {𝑦 ∈ (𝐴 ∩ dom 𝐹) ∣ (𝐹‘𝑦) ∈ 𝐵} (𝐹‘𝑤) = 𝑧))
28	23, 27	sylbi 121	. . . . . . . . . . . 12 ⊢ (Fun 𝐹 → (𝑧 ∈ (𝐹 “ {𝑦 ∈ (𝐴 ∩ dom 𝐹) ∣ (𝐹‘𝑦) ∈ 𝐵}) ↔ ∃𝑤 ∈ {𝑦 ∈ (𝐴 ∩ dom 𝐹) ∣ (𝐹‘𝑦) ∈ 𝐵} (𝐹‘𝑤) = 𝑧))
29	28	adantr 276	. . . . . . . . . . 11 ⊢ ((Fun 𝐹 ∧ 𝑧 ∈ 𝐵) → (𝑧 ∈ (𝐹 “ {𝑦 ∈ (𝐴 ∩ dom 𝐹) ∣ (𝐹‘𝑦) ∈ 𝐵}) ↔ ∃𝑤 ∈ {𝑦 ∈ (𝐴 ∩ dom 𝐹) ∣ (𝐹‘𝑦) ∈ 𝐵} (𝐹‘𝑤) = 𝑧))
30	22, 29	sylibrd 169	. . . . . . . . . 10 ⊢ ((Fun 𝐹 ∧ 𝑧 ∈ 𝐵) → (∃𝑤 ∈ (𝐴 ∩ dom 𝐹)(𝐹‘𝑤) = 𝑧 → 𝑧 ∈ (𝐹 “ {𝑦 ∈ (𝐴 ∩ dom 𝐹) ∣ (𝐹‘𝑦) ∈ 𝐵})))
31	11, 30	syld 45	. . . . . . . . 9 ⊢ ((Fun 𝐹 ∧ 𝑧 ∈ 𝐵) → (𝑧 ∈ (𝐹 “ (𝐴 ∩ dom 𝐹)) → 𝑧 ∈ (𝐹 “ {𝑦 ∈ (𝐴 ∩ dom 𝐹) ∣ (𝐹‘𝑦) ∈ 𝐵})))
32	31	adantlr 477	. . . . . . . 8 ⊢ (((Fun 𝐹 ∧ 𝐵 ⊆ (𝐹 “ (𝐴 ∩ dom 𝐹))) ∧ 𝑧 ∈ 𝐵) → (𝑧 ∈ (𝐹 “ (𝐴 ∩ dom 𝐹)) → 𝑧 ∈ (𝐹 “ {𝑦 ∈ (𝐴 ∩ dom 𝐹) ∣ (𝐹‘𝑦) ∈ 𝐵})))
33	8, 32	mpd 13	. . . . . . 7 ⊢ (((Fun 𝐹 ∧ 𝐵 ⊆ (𝐹 “ (𝐴 ∩ dom 𝐹))) ∧ 𝑧 ∈ 𝐵) → 𝑧 ∈ (𝐹 “ {𝑦 ∈ (𝐴 ∩ dom 𝐹) ∣ (𝐹‘𝑦) ∈ 𝐵}))
34	33	ex 115	. . . . . 6 ⊢ ((Fun 𝐹 ∧ 𝐵 ⊆ (𝐹 “ (𝐴 ∩ dom 𝐹))) → (𝑧 ∈ 𝐵 → 𝑧 ∈ (𝐹 “ {𝑦 ∈ (𝐴 ∩ dom 𝐹) ∣ (𝐹‘𝑦) ∈ 𝐵})))
35		fvelima 5569	. . . . . . . . 9 ⊢ ((Fun 𝐹 ∧ 𝑧 ∈ (𝐹 “ {𝑦 ∈ (𝐴 ∩ dom 𝐹) ∣ (𝐹‘𝑦) ∈ 𝐵})) → ∃𝑤 ∈ {𝑦 ∈ (𝐴 ∩ dom 𝐹) ∣ (𝐹‘𝑦) ∈ 𝐵} (𝐹‘𝑤) = 𝑧)
36	35	ex 115	. . . . . . . 8 ⊢ (Fun 𝐹 → (𝑧 ∈ (𝐹 “ {𝑦 ∈ (𝐴 ∩ dom 𝐹) ∣ (𝐹‘𝑦) ∈ 𝐵}) → ∃𝑤 ∈ {𝑦 ∈ (𝐴 ∩ dom 𝐹) ∣ (𝐹‘𝑦) ∈ 𝐵} (𝐹‘𝑤) = 𝑧))
37		eleq1 2240	. . . . . . . . . . . 12 ⊢ ((𝐹‘𝑤) = 𝑧 → ((𝐹‘𝑤) ∈ 𝐵 ↔ 𝑧 ∈ 𝐵))
38	37	biimpcd 159	. . . . . . . . . . 11 ⊢ ((𝐹‘𝑤) ∈ 𝐵 → ((𝐹‘𝑤) = 𝑧 → 𝑧 ∈ 𝐵))
39	38	adantl 277	. . . . . . . . . 10 ⊢ ((𝑤 ∈ (𝐴 ∩ dom 𝐹) ∧ (𝐹‘𝑤) ∈ 𝐵) → ((𝐹‘𝑤) = 𝑧 → 𝑧 ∈ 𝐵))
40	16, 39	sylbi 121	. . . . . . . . 9 ⊢ (𝑤 ∈ {𝑦 ∈ (𝐴 ∩ dom 𝐹) ∣ (𝐹‘𝑦) ∈ 𝐵} → ((𝐹‘𝑤) = 𝑧 → 𝑧 ∈ 𝐵))
41	40	rexlimiv 2588	. . . . . . . 8 ⊢ (∃𝑤 ∈ {𝑦 ∈ (𝐴 ∩ dom 𝐹) ∣ (𝐹‘𝑦) ∈ 𝐵} (𝐹‘𝑤) = 𝑧 → 𝑧 ∈ 𝐵)
42	36, 41	syl6 33	. . . . . . 7 ⊢ (Fun 𝐹 → (𝑧 ∈ (𝐹 “ {𝑦 ∈ (𝐴 ∩ dom 𝐹) ∣ (𝐹‘𝑦) ∈ 𝐵}) → 𝑧 ∈ 𝐵))
43	42	adantr 276	. . . . . 6 ⊢ ((Fun 𝐹 ∧ 𝐵 ⊆ (𝐹 “ (𝐴 ∩ dom 𝐹))) → (𝑧 ∈ (𝐹 “ {𝑦 ∈ (𝐴 ∩ dom 𝐹) ∣ (𝐹‘𝑦) ∈ 𝐵}) → 𝑧 ∈ 𝐵))
44	34, 43	impbid 129	. . . . 5 ⊢ ((Fun 𝐹 ∧ 𝐵 ⊆ (𝐹 “ (𝐴 ∩ dom 𝐹))) → (𝑧 ∈ 𝐵 ↔ 𝑧 ∈ (𝐹 “ {𝑦 ∈ (𝐴 ∩ dom 𝐹) ∣ (𝐹‘𝑦) ∈ 𝐵})))
45	44	eqrdv 2175	. . . 4 ⊢ ((Fun 𝐹 ∧ 𝐵 ⊆ (𝐹 “ (𝐴 ∩ dom 𝐹))) → 𝐵 = (𝐹 “ {𝑦 ∈ (𝐴 ∩ dom 𝐹) ∣ (𝐹‘𝑦) ∈ 𝐵}))
46		ssimaex.1	. . . . . . 7 ⊢ 𝐴 ∈ V
47	46	inex1 4139	. . . . . 6 ⊢ (𝐴 ∩ dom 𝐹) ∈ V
48	47	rabex 4149	. . . . 5 ⊢ {𝑦 ∈ (𝐴 ∩ dom 𝐹) ∣ (𝐹‘𝑦) ∈ 𝐵} ∈ V
49		sseq1 3180	. . . . . 6 ⊢ (𝑥 = {𝑦 ∈ (𝐴 ∩ dom 𝐹) ∣ (𝐹‘𝑦) ∈ 𝐵} → (𝑥 ⊆ (𝐴 ∩ dom 𝐹) ↔ {𝑦 ∈ (𝐴 ∩ dom 𝐹) ∣ (𝐹‘𝑦) ∈ 𝐵} ⊆ (𝐴 ∩ dom 𝐹)))
50		imaeq2 4968	. . . . . . 7 ⊢ (𝑥 = {𝑦 ∈ (𝐴 ∩ dom 𝐹) ∣ (𝐹‘𝑦) ∈ 𝐵} → (𝐹 “ 𝑥) = (𝐹 “ {𝑦 ∈ (𝐴 ∩ dom 𝐹) ∣ (𝐹‘𝑦) ∈ 𝐵}))
51	50	eqeq2d 2189	. . . . . 6 ⊢ (𝑥 = {𝑦 ∈ (𝐴 ∩ dom 𝐹) ∣ (𝐹‘𝑦) ∈ 𝐵} → (𝐵 = (𝐹 “ 𝑥) ↔ 𝐵 = (𝐹 “ {𝑦 ∈ (𝐴 ∩ dom 𝐹) ∣ (𝐹‘𝑦) ∈ 𝐵})))
52	49, 51	anbi12d 473	. . . . 5 ⊢ (𝑥 = {𝑦 ∈ (𝐴 ∩ dom 𝐹) ∣ (𝐹‘𝑦) ∈ 𝐵} → ((𝑥 ⊆ (𝐴 ∩ dom 𝐹) ∧ 𝐵 = (𝐹 “ 𝑥)) ↔ ({𝑦 ∈ (𝐴 ∩ dom 𝐹) ∣ (𝐹‘𝑦) ∈ 𝐵} ⊆ (𝐴 ∩ dom 𝐹) ∧ 𝐵 = (𝐹 “ {𝑦 ∈ (𝐴 ∩ dom 𝐹) ∣ (𝐹‘𝑦) ∈ 𝐵}))))
53	48, 52	spcev 2834	. . . 4 ⊢ (({𝑦 ∈ (𝐴 ∩ dom 𝐹) ∣ (𝐹‘𝑦) ∈ 𝐵} ⊆ (𝐴 ∩ dom 𝐹) ∧ 𝐵 = (𝐹 “ {𝑦 ∈ (𝐴 ∩ dom 𝐹) ∣ (𝐹‘𝑦) ∈ 𝐵})) → ∃𝑥(𝑥 ⊆ (𝐴 ∩ dom 𝐹) ∧ 𝐵 = (𝐹 “ 𝑥)))
54	6, 45, 53	sylancr 414	. . 3 ⊢ ((Fun 𝐹 ∧ 𝐵 ⊆ (𝐹 “ (𝐴 ∩ dom 𝐹))) → ∃𝑥(𝑥 ⊆ (𝐴 ∩ dom 𝐹) ∧ 𝐵 = (𝐹 “ 𝑥)))
55		inss1 3357	. . . . . 6 ⊢ (𝐴 ∩ dom 𝐹) ⊆ 𝐴
56		sstr 3165	. . . . . 6 ⊢ ((𝑥 ⊆ (𝐴 ∩ dom 𝐹) ∧ (𝐴 ∩ dom 𝐹) ⊆ 𝐴) → 𝑥 ⊆ 𝐴)
57	55, 56	mpan2 425	. . . . 5 ⊢ (𝑥 ⊆ (𝐴 ∩ dom 𝐹) → 𝑥 ⊆ 𝐴)
58	57	anim1i 340	. . . 4 ⊢ ((𝑥 ⊆ (𝐴 ∩ dom 𝐹) ∧ 𝐵 = (𝐹 “ 𝑥)) → (𝑥 ⊆ 𝐴 ∧ 𝐵 = (𝐹 “ 𝑥)))
59	58	eximi 1600	. . 3 ⊢ (∃𝑥(𝑥 ⊆ (𝐴 ∩ dom 𝐹) ∧ 𝐵 = (𝐹 “ 𝑥)) → ∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝐵 = (𝐹 “ 𝑥)))
60	54, 59	syl 14	. 2 ⊢ ((Fun 𝐹 ∧ 𝐵 ⊆ (𝐹 “ (𝐴 ∩ dom 𝐹))) → ∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝐵 = (𝐹 “ 𝑥)))
61	5, 60	sylan2br 288	1 ⊢ ((Fun 𝐹 ∧ 𝐵 ⊆ (𝐹 “ 𝐴)) → ∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝐵 = (𝐹 “ 𝑥)))

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105   = wceq 1353  ∃wex 1492   ∈ wcel 2148  ∃wrex 2456  {crab 2459  Vcvv 2739   ∩ cin 3130   ⊆ wss 3131  dom cdm 4628   ↾ cres 4630   “ cima 4631  Fun wfun 5212   Fn wfn 5213  ‘cfv 5218

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-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-rab 2464  df-v 2741  df-sbc 2965  df-un 3135  df-in 3137  df-ss 3144  df-pw 3579  df-sn 3600  df-pr 3601  df-op 3603  df-uni 3812  df-br 4006  df-opab 4067  df-id 4295  df-xp 4634  df-rel 4635  df-cnv 4636  df-co 4637  df-dm 4638  df-rn 4639  df-res 4640  df-ima 4641  df-iota 5180  df-fun 5220  df-fn 5221  df-fv 5226

This theorem is referenced by:  ssimaexg  5580