Metamath Proof Explorer

Theorem ssimaex

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

Ref Expression
Hypothesis ssimaex.1 ⊢ 𝐴 ∈ V
Assertion ssimaex ( ( Fun 𝐹 ∧ 𝐵 ⊆ ( 𝐹 “ 𝐴 ) ) → ∃ 𝑥 ( 𝑥 ⊆ 𝐴 ∧ 𝐵 = ( 𝐹 “ 𝑥 ) ) )

Proof

Step Hyp Ref Expression
1 ssimaex.1 ⊢ 𝐴 ∈ V
2 dmres ⊢ dom ( 𝐹 ↾ 𝐴 ) = ( 𝐴 ∩ dom 𝐹 )
3 2 imaeq2i ⊢ ( 𝐹 “ dom ( 𝐹 ↾ 𝐴 ) ) = ( 𝐹 “ ( 𝐴 ∩ dom 𝐹 ) )
4 imadmres ⊢ ( 𝐹 “ dom ( 𝐹 ↾ 𝐴 ) ) = ( 𝐹 “ 𝐴 )
5 3 4 eqtr3i ⊢ ( 𝐹 “ ( 𝐴 ∩ dom 𝐹 ) ) = ( 𝐹 “ 𝐴 )
6 5 sseq2i ⊢ ( 𝐵 ⊆ ( 𝐹 “ ( 𝐴 ∩ dom 𝐹 ) ) ↔ 𝐵 ⊆ ( 𝐹 “ 𝐴 ) )
7 ssrab2 ⊢ { 𝑦 ∈ ( 𝐴 ∩ dom 𝐹 ) ∣ ( 𝐹 ‘ 𝑦 ) ∈ 𝐵 } ⊆ ( 𝐴 ∩ dom 𝐹 )
8 ssel2 ⊢ ( ( 𝐵 ⊆ ( 𝐹 “ ( 𝐴 ∩ dom 𝐹 ) ) ∧ 𝑧 ∈ 𝐵 ) → 𝑧 ∈ ( 𝐹 “ ( 𝐴 ∩ dom 𝐹 ) ) )
9 8 adantll ⊢ ( ( ( Fun 𝐹 ∧ 𝐵 ⊆ ( 𝐹 “ ( 𝐴 ∩ dom 𝐹 ) ) ) ∧ 𝑧 ∈ 𝐵 ) → 𝑧 ∈ ( 𝐹 “ ( 𝐴 ∩ dom 𝐹 ) ) )
10 fvelima ⊢ ( ( Fun 𝐹 ∧ 𝑧 ∈ ( 𝐹 “ ( 𝐴 ∩ dom 𝐹 ) ) ) → ∃ 𝑤 ∈ ( 𝐴 ∩ dom 𝐹 ) ( 𝐹 ‘ 𝑤 ) = 𝑧 )
11 10 ex ⊢ ( Fun 𝐹 → ( 𝑧 ∈ ( 𝐹 “ ( 𝐴 ∩ dom 𝐹 ) ) → ∃ 𝑤 ∈ ( 𝐴 ∩ dom 𝐹 ) ( 𝐹 ‘ 𝑤 ) = 𝑧 ) )
12 11 adantr ⊢ ( ( Fun 𝐹 ∧ 𝑧 ∈ 𝐵 ) → ( 𝑧 ∈ ( 𝐹 “ ( 𝐴 ∩ dom 𝐹 ) ) → ∃ 𝑤 ∈ ( 𝐴 ∩ dom 𝐹 ) ( 𝐹 ‘ 𝑤 ) = 𝑧 ) )
13 eleq1a ⊢ ( 𝑧 ∈ 𝐵 → ( ( 𝐹 ‘ 𝑤 ) = 𝑧 → ( 𝐹 ‘ 𝑤 ) ∈ 𝐵 ) )
14 13 anim2d ⊢ ( 𝑧 ∈ 𝐵 → ( ( 𝑤 ∈ ( 𝐴 ∩ dom 𝐹 ) ∧ ( 𝐹 ‘ 𝑤 ) = 𝑧 ) → ( 𝑤 ∈ ( 𝐴 ∩ dom 𝐹 ) ∧ ( 𝐹 ‘ 𝑤 ) ∈ 𝐵 ) ) )
15 fveq2 ⊢ ( 𝑦 = 𝑤 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑤 ) )
16 15 eleq1d ⊢ ( 𝑦 = 𝑤 → ( ( 𝐹 ‘ 𝑦 ) ∈ 𝐵 ↔ ( 𝐹 ‘ 𝑤 ) ∈ 𝐵 ) )
17 16 elrab ⊢ ( 𝑤 ∈ { 𝑦 ∈ ( 𝐴 ∩ dom 𝐹 ) ∣ ( 𝐹 ‘ 𝑦 ) ∈ 𝐵 } ↔ ( 𝑤 ∈ ( 𝐴 ∩ dom 𝐹 ) ∧ ( 𝐹 ‘ 𝑤 ) ∈ 𝐵 ) )
18 14 17 imbitrrdi ⊢ ( 𝑧 ∈ 𝐵 → ( ( 𝑤 ∈ ( 𝐴 ∩ dom 𝐹 ) ∧ ( 𝐹 ‘ 𝑤 ) = 𝑧 ) → 𝑤 ∈ { 𝑦 ∈ ( 𝐴 ∩ dom 𝐹 ) ∣ ( 𝐹 ‘ 𝑦 ) ∈ 𝐵 } ) )
19 simpr ⊢ ( ( 𝑤 ∈ ( 𝐴 ∩ dom 𝐹 ) ∧ ( 𝐹 ‘ 𝑤 ) = 𝑧 ) → ( 𝐹 ‘ 𝑤 ) = 𝑧 )
20 18 19 jca2 ⊢ ( 𝑧 ∈ 𝐵 → ( ( 𝑤 ∈ ( 𝐴 ∩ dom 𝐹 ) ∧ ( 𝐹 ‘ 𝑤 ) = 𝑧 ) → ( 𝑤 ∈ { 𝑦 ∈ ( 𝐴 ∩ dom 𝐹 ) ∣ ( 𝐹 ‘ 𝑦 ) ∈ 𝐵 } ∧ ( 𝐹 ‘ 𝑤 ) = 𝑧 ) ) )
21 20 reximdv2 ⊢ ( 𝑧 ∈ 𝐵 → ( ∃ 𝑤 ∈ ( 𝐴 ∩ dom 𝐹 ) ( 𝐹 ‘ 𝑤 ) = 𝑧 → ∃ 𝑤 ∈ { 𝑦 ∈ ( 𝐴 ∩ dom 𝐹 ) ∣ ( 𝐹 ‘ 𝑦 ) ∈ 𝐵 } ( 𝐹 ‘ 𝑤 ) = 𝑧 ) )
22 21 adantl ⊢ ( ( Fun 𝐹 ∧ 𝑧 ∈ 𝐵 ) → ( ∃ 𝑤 ∈ ( 𝐴 ∩ dom 𝐹 ) ( 𝐹 ‘ 𝑤 ) = 𝑧 → ∃ 𝑤 ∈ { 𝑦 ∈ ( 𝐴 ∩ dom 𝐹 ) ∣ ( 𝐹 ‘ 𝑦 ) ∈ 𝐵 } ( 𝐹 ‘ 𝑤 ) = 𝑧 ) )
23 funfn ⊢ ( Fun 𝐹 ↔ 𝐹 Fn dom 𝐹 )
24 inss2 ⊢ ( 𝐴 ∩ dom 𝐹 ) ⊆ dom 𝐹
25 7 24 sstri ⊢ { 𝑦 ∈ ( 𝐴 ∩ dom 𝐹 ) ∣ ( 𝐹 ‘ 𝑦 ) ∈ 𝐵 } ⊆ dom 𝐹
26 fvelimab ⊢ ( ( 𝐹 Fn dom 𝐹 ∧ { 𝑦 ∈ ( 𝐴 ∩ dom 𝐹 ) ∣ ( 𝐹 ‘ 𝑦 ) ∈ 𝐵 } ⊆ dom 𝐹 ) → ( 𝑧 ∈ ( 𝐹 “ { 𝑦 ∈ ( 𝐴 ∩ dom 𝐹 ) ∣ ( 𝐹 ‘ 𝑦 ) ∈ 𝐵 } ) ↔ ∃ 𝑤 ∈ { 𝑦 ∈ ( 𝐴 ∩ dom 𝐹 ) ∣ ( 𝐹 ‘ 𝑦 ) ∈ 𝐵 } ( 𝐹 ‘ 𝑤 ) = 𝑧 ) )
27 25 26 mpan2 ⊢ ( 𝐹 Fn dom 𝐹 → ( 𝑧 ∈ ( 𝐹 “ { 𝑦 ∈ ( 𝐴 ∩ dom 𝐹 ) ∣ ( 𝐹 ‘ 𝑦 ) ∈ 𝐵 } ) ↔ ∃ 𝑤 ∈ { 𝑦 ∈ ( 𝐴 ∩ dom 𝐹 ) ∣ ( 𝐹 ‘ 𝑦 ) ∈ 𝐵 } ( 𝐹 ‘ 𝑤 ) = 𝑧 ) )
28 23 27 sylbi ⊢ ( Fun 𝐹 → ( 𝑧 ∈ ( 𝐹 “ { 𝑦 ∈ ( 𝐴 ∩ dom 𝐹 ) ∣ ( 𝐹 ‘ 𝑦 ) ∈ 𝐵 } ) ↔ ∃ 𝑤 ∈ { 𝑦 ∈ ( 𝐴 ∩ dom 𝐹 ) ∣ ( 𝐹 ‘ 𝑦 ) ∈ 𝐵 } ( 𝐹 ‘ 𝑤 ) = 𝑧 ) )
29 28 adantr ⊢ ( ( Fun 𝐹 ∧ 𝑧 ∈ 𝐵 ) → ( 𝑧 ∈ ( 𝐹 “ { 𝑦 ∈ ( 𝐴 ∩ dom 𝐹 ) ∣ ( 𝐹 ‘ 𝑦 ) ∈ 𝐵 } ) ↔ ∃ 𝑤 ∈ { 𝑦 ∈ ( 𝐴 ∩ dom 𝐹 ) ∣ ( 𝐹 ‘ 𝑦 ) ∈ 𝐵 } ( 𝐹 ‘ 𝑤 ) = 𝑧 ) )
30 22 29 sylibrd ⊢ ( ( Fun 𝐹 ∧ 𝑧 ∈ 𝐵 ) → ( ∃ 𝑤 ∈ ( 𝐴 ∩ dom 𝐹 ) ( 𝐹 ‘ 𝑤 ) = 𝑧 → 𝑧 ∈ ( 𝐹 “ { 𝑦 ∈ ( 𝐴 ∩ dom 𝐹 ) ∣ ( 𝐹 ‘ 𝑦 ) ∈ 𝐵 } ) ) )
31 12 30 syld ⊢ ( ( Fun 𝐹 ∧ 𝑧 ∈ 𝐵 ) → ( 𝑧 ∈ ( 𝐹 “ ( 𝐴 ∩ dom 𝐹 ) ) → 𝑧 ∈ ( 𝐹 “ { 𝑦 ∈ ( 𝐴 ∩ dom 𝐹 ) ∣ ( 𝐹 ‘ 𝑦 ) ∈ 𝐵 } ) ) )
32 31 adantlr ⊢ ( ( ( Fun 𝐹 ∧ 𝐵 ⊆ ( 𝐹 “ ( 𝐴 ∩ dom 𝐹 ) ) ) ∧ 𝑧 ∈ 𝐵 ) → ( 𝑧 ∈ ( 𝐹 “ ( 𝐴 ∩ dom 𝐹 ) ) → 𝑧 ∈ ( 𝐹 “ { 𝑦 ∈ ( 𝐴 ∩ dom 𝐹 ) ∣ ( 𝐹 ‘ 𝑦 ) ∈ 𝐵 } ) ) )
33 9 32 mpd ⊢ ( ( ( Fun 𝐹 ∧ 𝐵 ⊆ ( 𝐹 “ ( 𝐴 ∩ dom 𝐹 ) ) ) ∧ 𝑧 ∈ 𝐵 ) → 𝑧 ∈ ( 𝐹 “ { 𝑦 ∈ ( 𝐴 ∩ dom 𝐹 ) ∣ ( 𝐹 ‘ 𝑦 ) ∈ 𝐵 } ) )
34 33 ex ⊢ ( ( Fun 𝐹 ∧ 𝐵 ⊆ ( 𝐹 “ ( 𝐴 ∩ dom 𝐹 ) ) ) → ( 𝑧 ∈ 𝐵 → 𝑧 ∈ ( 𝐹 “ { 𝑦 ∈ ( 𝐴 ∩ dom 𝐹 ) ∣ ( 𝐹 ‘ 𝑦 ) ∈ 𝐵 } ) ) )
35 fvelima ⊢ ( ( Fun 𝐹 ∧ 𝑧 ∈ ( 𝐹 “ { 𝑦 ∈ ( 𝐴 ∩ dom 𝐹 ) ∣ ( 𝐹 ‘ 𝑦 ) ∈ 𝐵 } ) ) → ∃ 𝑤 ∈ { 𝑦 ∈ ( 𝐴 ∩ dom 𝐹 ) ∣ ( 𝐹 ‘ 𝑦 ) ∈ 𝐵 } ( 𝐹 ‘ 𝑤 ) = 𝑧 )
36 35 ex ⊢ ( Fun 𝐹 → ( 𝑧 ∈ ( 𝐹 “ { 𝑦 ∈ ( 𝐴 ∩ dom 𝐹 ) ∣ ( 𝐹 ‘ 𝑦 ) ∈ 𝐵 } ) → ∃ 𝑤 ∈ { 𝑦 ∈ ( 𝐴 ∩ dom 𝐹 ) ∣ ( 𝐹 ‘ 𝑦 ) ∈ 𝐵 } ( 𝐹 ‘ 𝑤 ) = 𝑧 ) )
37 eleq1 ⊢ ( ( 𝐹 ‘ 𝑤 ) = 𝑧 → ( ( 𝐹 ‘ 𝑤 ) ∈ 𝐵 ↔ 𝑧 ∈ 𝐵 ) )
38 37 biimpcd ⊢ ( ( 𝐹 ‘ 𝑤 ) ∈ 𝐵 → ( ( 𝐹 ‘ 𝑤 ) = 𝑧 → 𝑧 ∈ 𝐵 ) )
39 38 adantl ⊢ ( ( 𝑤 ∈ ( 𝐴 ∩ dom 𝐹 ) ∧ ( 𝐹 ‘ 𝑤 ) ∈ 𝐵 ) → ( ( 𝐹 ‘ 𝑤 ) = 𝑧 → 𝑧 ∈ 𝐵 ) )
40 17 39 sylbi ⊢ ( 𝑤 ∈ { 𝑦 ∈ ( 𝐴 ∩ dom 𝐹 ) ∣ ( 𝐹 ‘ 𝑦 ) ∈ 𝐵 } → ( ( 𝐹 ‘ 𝑤 ) = 𝑧 → 𝑧 ∈ 𝐵 ) )
41 40 rexlimiv ⊢ ( ∃ 𝑤 ∈ { 𝑦 ∈ ( 𝐴 ∩ dom 𝐹 ) ∣ ( 𝐹 ‘ 𝑦 ) ∈ 𝐵 } ( 𝐹 ‘ 𝑤 ) = 𝑧 → 𝑧 ∈ 𝐵 )
42 36 41 syl6 ⊢ ( Fun 𝐹 → ( 𝑧 ∈ ( 𝐹 “ { 𝑦 ∈ ( 𝐴 ∩ dom 𝐹 ) ∣ ( 𝐹 ‘ 𝑦 ) ∈ 𝐵 } ) → 𝑧 ∈ 𝐵 ) )
43 42 adantr ⊢ ( ( Fun 𝐹 ∧ 𝐵 ⊆ ( 𝐹 “ ( 𝐴 ∩ dom 𝐹 ) ) ) → ( 𝑧 ∈ ( 𝐹 “ { 𝑦 ∈ ( 𝐴 ∩ dom 𝐹 ) ∣ ( 𝐹 ‘ 𝑦 ) ∈ 𝐵 } ) → 𝑧 ∈ 𝐵 ) )
44 34 43 impbid ⊢ ( ( Fun 𝐹 ∧ 𝐵 ⊆ ( 𝐹 “ ( 𝐴 ∩ dom 𝐹 ) ) ) → ( 𝑧 ∈ 𝐵 ↔ 𝑧 ∈ ( 𝐹 “ { 𝑦 ∈ ( 𝐴 ∩ dom 𝐹 ) ∣ ( 𝐹 ‘ 𝑦 ) ∈ 𝐵 } ) ) )
45 44 eqrdv ⊢ ( ( Fun 𝐹 ∧ 𝐵 ⊆ ( 𝐹 “ ( 𝐴 ∩ dom 𝐹 ) ) ) → 𝐵 = ( 𝐹 “ { 𝑦 ∈ ( 𝐴 ∩ dom 𝐹 ) ∣ ( 𝐹 ‘ 𝑦 ) ∈ 𝐵 } ) )
46 1 inex1 ⊢ ( 𝐴 ∩ dom 𝐹 ) ∈ V
47 46 rabex ⊢ { 𝑦 ∈ ( 𝐴 ∩ dom 𝐹 ) ∣ ( 𝐹 ‘ 𝑦 ) ∈ 𝐵 } ∈ V
48 sseq1 ⊢ ( 𝑥 = { 𝑦 ∈ ( 𝐴 ∩ dom 𝐹 ) ∣ ( 𝐹 ‘ 𝑦 ) ∈ 𝐵 } → ( 𝑥 ⊆ ( 𝐴 ∩ dom 𝐹 ) ↔ { 𝑦 ∈ ( 𝐴 ∩ dom 𝐹 ) ∣ ( 𝐹 ‘ 𝑦 ) ∈ 𝐵 } ⊆ ( 𝐴 ∩ dom 𝐹 ) ) )
49 imaeq2 ⊢ ( 𝑥 = { 𝑦 ∈ ( 𝐴 ∩ dom 𝐹 ) ∣ ( 𝐹 ‘ 𝑦 ) ∈ 𝐵 } → ( 𝐹 “ 𝑥 ) = ( 𝐹 “ { 𝑦 ∈ ( 𝐴 ∩ dom 𝐹 ) ∣ ( 𝐹 ‘ 𝑦 ) ∈ 𝐵 } ) )
50 49 eqeq2d ⊢ ( 𝑥 = { 𝑦 ∈ ( 𝐴 ∩ dom 𝐹 ) ∣ ( 𝐹 ‘ 𝑦 ) ∈ 𝐵 } → ( 𝐵 = ( 𝐹 “ 𝑥 ) ↔ 𝐵 = ( 𝐹 “ { 𝑦 ∈ ( 𝐴 ∩ dom 𝐹 ) ∣ ( 𝐹 ‘ 𝑦 ) ∈ 𝐵 } ) ) )
51 48 50 anbi12d ⊢ ( 𝑥 = { 𝑦 ∈ ( 𝐴 ∩ dom 𝐹 ) ∣ ( 𝐹 ‘ 𝑦 ) ∈ 𝐵 } → ( ( 𝑥 ⊆ ( 𝐴 ∩ dom 𝐹 ) ∧ 𝐵 = ( 𝐹 “ 𝑥 ) ) ↔ ( { 𝑦 ∈ ( 𝐴 ∩ dom 𝐹 ) ∣ ( 𝐹 ‘ 𝑦 ) ∈ 𝐵 } ⊆ ( 𝐴 ∩ dom 𝐹 ) ∧ 𝐵 = ( 𝐹 “ { 𝑦 ∈ ( 𝐴 ∩ dom 𝐹 ) ∣ ( 𝐹 ‘ 𝑦 ) ∈ 𝐵 } ) ) ) )
52 47 51 spcev ⊢ ( ( { 𝑦 ∈ ( 𝐴 ∩ dom 𝐹 ) ∣ ( 𝐹 ‘ 𝑦 ) ∈ 𝐵 } ⊆ ( 𝐴 ∩ dom 𝐹 ) ∧ 𝐵 = ( 𝐹 “ { 𝑦 ∈ ( 𝐴 ∩ dom 𝐹 ) ∣ ( 𝐹 ‘ 𝑦 ) ∈ 𝐵 } ) ) → ∃ 𝑥 ( 𝑥 ⊆ ( 𝐴 ∩ dom 𝐹 ) ∧ 𝐵 = ( 𝐹 “ 𝑥 ) ) )
53 7 45 52 sylancr ⊢ ( ( Fun 𝐹 ∧ 𝐵 ⊆ ( 𝐹 “ ( 𝐴 ∩ dom 𝐹 ) ) ) → ∃ 𝑥 ( 𝑥 ⊆ ( 𝐴 ∩ dom 𝐹 ) ∧ 𝐵 = ( 𝐹 “ 𝑥 ) ) )
54 inss1 ⊢ ( 𝐴 ∩ dom 𝐹 ) ⊆ 𝐴
55 sstr ⊢ ( ( 𝑥 ⊆ ( 𝐴 ∩ dom 𝐹 ) ∧ ( 𝐴 ∩ dom 𝐹 ) ⊆ 𝐴 ) → 𝑥 ⊆ 𝐴 )
56 54 55 mpan2 ⊢ ( 𝑥 ⊆ ( 𝐴 ∩ dom 𝐹 ) → 𝑥 ⊆ 𝐴 )
57 56 anim1i ⊢ ( ( 𝑥 ⊆ ( 𝐴 ∩ dom 𝐹 ) ∧ 𝐵 = ( 𝐹 “ 𝑥 ) ) → ( 𝑥 ⊆ 𝐴 ∧ 𝐵 = ( 𝐹 “ 𝑥 ) ) )
58 57 eximi ⊢ ( ∃ 𝑥 ( 𝑥 ⊆ ( 𝐴 ∩ dom 𝐹 ) ∧ 𝐵 = ( 𝐹 “ 𝑥 ) ) → ∃ 𝑥 ( 𝑥 ⊆ 𝐴 ∧ 𝐵 = ( 𝐹 “ 𝑥 ) ) )
59 53 58 syl ⊢ ( ( Fun 𝐹 ∧ 𝐵 ⊆ ( 𝐹 “ ( 𝐴 ∩ dom 𝐹 ) ) ) → ∃ 𝑥 ( 𝑥 ⊆ 𝐴 ∧ 𝐵 = ( 𝐹 “ 𝑥 ) ) )
60 6 59 sylan2br ⊢ ( ( Fun 𝐹 ∧ 𝐵 ⊆ ( 𝐹 “ 𝐴 ) ) → ∃ 𝑥 ( 𝑥 ⊆ 𝐴 ∧ 𝐵 = ( 𝐹 “ 𝑥 ) ) )