Metamath Proof Explorer

Theorem imadif

Description: The image of a difference is the difference of images. (Contributed by NM, 24-May-1998)

Ref Expression
Assertion imadif ( Fun ◡ 𝐹 → ( 𝐹 “ ( 𝐴 ∖ 𝐵 ) ) = ( ( 𝐹 “ 𝐴 ) ∖ ( 𝐹 “ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 anandir ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵 ) ∧ 𝑥 𝐹 𝑦 ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝐹 𝑦 ) ∧ ( ¬ 𝑥 ∈ 𝐵 ∧ 𝑥 𝐹 𝑦 ) ) )
2 1 exbii ⊢ ( ∃ 𝑥 ( ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵 ) ∧ 𝑥 𝐹 𝑦 ) ↔ ∃ 𝑥 ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝐹 𝑦 ) ∧ ( ¬ 𝑥 ∈ 𝐵 ∧ 𝑥 𝐹 𝑦 ) ) )
3 19.40 ⊢ ( ∃ 𝑥 ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝐹 𝑦 ) ∧ ( ¬ 𝑥 ∈ 𝐵 ∧ 𝑥 𝐹 𝑦 ) ) → ( ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝐹 𝑦 ) ∧ ∃ 𝑥 ( ¬ 𝑥 ∈ 𝐵 ∧ 𝑥 𝐹 𝑦 ) ) )
4 2 3 sylbi ⊢ ( ∃ 𝑥 ( ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵 ) ∧ 𝑥 𝐹 𝑦 ) → ( ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝐹 𝑦 ) ∧ ∃ 𝑥 ( ¬ 𝑥 ∈ 𝐵 ∧ 𝑥 𝐹 𝑦 ) ) )
5 nfv ⊢ Ⅎ 𝑥 Fun ◡ 𝐹
6 nfe1 ⊢ Ⅎ 𝑥 ∃ 𝑥 ( 𝑥 𝐹 𝑦 ∧ ¬ 𝑥 ∈ 𝐵 )
7 5 6 nfan ⊢ Ⅎ 𝑥 ( Fun ◡ 𝐹 ∧ ∃ 𝑥 ( 𝑥 𝐹 𝑦 ∧ ¬ 𝑥 ∈ 𝐵 ) )
8 funmo ⊢ ( Fun ◡ 𝐹 → ∃* 𝑥 𝑦 ◡ 𝐹 𝑥 )
9 vex ⊢ 𝑦 ∈ V
10 vex ⊢ 𝑥 ∈ V
11 9 10 brcnv ⊢ ( 𝑦 ◡ 𝐹 𝑥 ↔ 𝑥 𝐹 𝑦 )
12 11 mobii ⊢ ( ∃* 𝑥 𝑦 ◡ 𝐹 𝑥 ↔ ∃* 𝑥 𝑥 𝐹 𝑦 )
13 8 12 sylib ⊢ ( Fun ◡ 𝐹 → ∃* 𝑥 𝑥 𝐹 𝑦 )
14 mopick ⊢ ( ( ∃* 𝑥 𝑥 𝐹 𝑦 ∧ ∃ 𝑥 ( 𝑥 𝐹 𝑦 ∧ ¬ 𝑥 ∈ 𝐵 ) ) → ( 𝑥 𝐹 𝑦 → ¬ 𝑥 ∈ 𝐵 ) )
15 13 14 sylan ⊢ ( ( Fun ◡ 𝐹 ∧ ∃ 𝑥 ( 𝑥 𝐹 𝑦 ∧ ¬ 𝑥 ∈ 𝐵 ) ) → ( 𝑥 𝐹 𝑦 → ¬ 𝑥 ∈ 𝐵 ) )
16 15 con2d ⊢ ( ( Fun ◡ 𝐹 ∧ ∃ 𝑥 ( 𝑥 𝐹 𝑦 ∧ ¬ 𝑥 ∈ 𝐵 ) ) → ( 𝑥 ∈ 𝐵 → ¬ 𝑥 𝐹 𝑦 ) )
17 imnan ⊢ ( ( 𝑥 ∈ 𝐵 → ¬ 𝑥 𝐹 𝑦 ) ↔ ¬ ( 𝑥 ∈ 𝐵 ∧ 𝑥 𝐹 𝑦 ) )
18 16 17 sylib ⊢ ( ( Fun ◡ 𝐹 ∧ ∃ 𝑥 ( 𝑥 𝐹 𝑦 ∧ ¬ 𝑥 ∈ 𝐵 ) ) → ¬ ( 𝑥 ∈ 𝐵 ∧ 𝑥 𝐹 𝑦 ) )
19 7 18 alrimi ⊢ ( ( Fun ◡ 𝐹 ∧ ∃ 𝑥 ( 𝑥 𝐹 𝑦 ∧ ¬ 𝑥 ∈ 𝐵 ) ) → ∀ 𝑥 ¬ ( 𝑥 ∈ 𝐵 ∧ 𝑥 𝐹 𝑦 ) )
20 19 ex ⊢ ( Fun ◡ 𝐹 → ( ∃ 𝑥 ( 𝑥 𝐹 𝑦 ∧ ¬ 𝑥 ∈ 𝐵 ) → ∀ 𝑥 ¬ ( 𝑥 ∈ 𝐵 ∧ 𝑥 𝐹 𝑦 ) ) )
21 exancom ⊢ ( ∃ 𝑥 ( 𝑥 𝐹 𝑦 ∧ ¬ 𝑥 ∈ 𝐵 ) ↔ ∃ 𝑥 ( ¬ 𝑥 ∈ 𝐵 ∧ 𝑥 𝐹 𝑦 ) )
22 alnex ⊢ ( ∀ 𝑥 ¬ ( 𝑥 ∈ 𝐵 ∧ 𝑥 𝐹 𝑦 ) ↔ ¬ ∃ 𝑥 ( 𝑥 ∈ 𝐵 ∧ 𝑥 𝐹 𝑦 ) )
23 20 21 22 3imtr3g ⊢ ( Fun ◡ 𝐹 → ( ∃ 𝑥 ( ¬ 𝑥 ∈ 𝐵 ∧ 𝑥 𝐹 𝑦 ) → ¬ ∃ 𝑥 ( 𝑥 ∈ 𝐵 ∧ 𝑥 𝐹 𝑦 ) ) )
24 23 anim2d ⊢ ( Fun ◡ 𝐹 → ( ( ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝐹 𝑦 ) ∧ ∃ 𝑥 ( ¬ 𝑥 ∈ 𝐵 ∧ 𝑥 𝐹 𝑦 ) ) → ( ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝐹 𝑦 ) ∧ ¬ ∃ 𝑥 ( 𝑥 ∈ 𝐵 ∧ 𝑥 𝐹 𝑦 ) ) ) )
25 4 24 syl5 ⊢ ( Fun ◡ 𝐹 → ( ∃ 𝑥 ( ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵 ) ∧ 𝑥 𝐹 𝑦 ) → ( ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝐹 𝑦 ) ∧ ¬ ∃ 𝑥 ( 𝑥 ∈ 𝐵 ∧ 𝑥 𝐹 𝑦 ) ) ) )
26 19.29r ⊢ ( ( ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝐹 𝑦 ) ∧ ∀ 𝑥 ¬ ( 𝑥 ∈ 𝐵 ∧ 𝑥 𝐹 𝑦 ) ) → ∃ 𝑥 ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝐹 𝑦 ) ∧ ¬ ( 𝑥 ∈ 𝐵 ∧ 𝑥 𝐹 𝑦 ) ) )
27 22 26 sylan2br ⊢ ( ( ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝐹 𝑦 ) ∧ ¬ ∃ 𝑥 ( 𝑥 ∈ 𝐵 ∧ 𝑥 𝐹 𝑦 ) ) → ∃ 𝑥 ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝐹 𝑦 ) ∧ ¬ ( 𝑥 ∈ 𝐵 ∧ 𝑥 𝐹 𝑦 ) ) )
28 andi ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝐹 𝑦 ) ∧ ( ¬ 𝑥 ∈ 𝐵 ∨ ¬ 𝑥 𝐹 𝑦 ) ) ↔ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝐹 𝑦 ) ∧ ¬ 𝑥 ∈ 𝐵 ) ∨ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝐹 𝑦 ) ∧ ¬ 𝑥 𝐹 𝑦 ) ) )
29 ianor ⊢ ( ¬ ( 𝑥 ∈ 𝐵 ∧ 𝑥 𝐹 𝑦 ) ↔ ( ¬ 𝑥 ∈ 𝐵 ∨ ¬ 𝑥 𝐹 𝑦 ) )
30 29 anbi2i ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝐹 𝑦 ) ∧ ¬ ( 𝑥 ∈ 𝐵 ∧ 𝑥 𝐹 𝑦 ) ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝐹 𝑦 ) ∧ ( ¬ 𝑥 ∈ 𝐵 ∨ ¬ 𝑥 𝐹 𝑦 ) ) )
31 an32 ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵 ) ∧ 𝑥 𝐹 𝑦 ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝐹 𝑦 ) ∧ ¬ 𝑥 ∈ 𝐵 ) )
32 pm3.24 ⊢ ¬ ( 𝑥 𝐹 𝑦 ∧ ¬ 𝑥 𝐹 𝑦 )
33 32 intnan ⊢ ¬ ( 𝑥 ∈ 𝐴 ∧ ( 𝑥 𝐹 𝑦 ∧ ¬ 𝑥 𝐹 𝑦 ) )
34 anass ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝐹 𝑦 ) ∧ ¬ 𝑥 𝐹 𝑦 ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( 𝑥 𝐹 𝑦 ∧ ¬ 𝑥 𝐹 𝑦 ) ) )
35 33 34 mtbir ⊢ ¬ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝐹 𝑦 ) ∧ ¬ 𝑥 𝐹 𝑦 )
36 35 biorfi ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝐹 𝑦 ) ∧ ¬ 𝑥 ∈ 𝐵 ) ↔ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝐹 𝑦 ) ∧ ¬ 𝑥 ∈ 𝐵 ) ∨ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝐹 𝑦 ) ∧ ¬ 𝑥 𝐹 𝑦 ) ) )
37 31 36 bitri ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵 ) ∧ 𝑥 𝐹 𝑦 ) ↔ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝐹 𝑦 ) ∧ ¬ 𝑥 ∈ 𝐵 ) ∨ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝐹 𝑦 ) ∧ ¬ 𝑥 𝐹 𝑦 ) ) )
38 28 30 37 3bitr4i ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝐹 𝑦 ) ∧ ¬ ( 𝑥 ∈ 𝐵 ∧ 𝑥 𝐹 𝑦 ) ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵 ) ∧ 𝑥 𝐹 𝑦 ) )
39 38 exbii ⊢ ( ∃ 𝑥 ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝐹 𝑦 ) ∧ ¬ ( 𝑥 ∈ 𝐵 ∧ 𝑥 𝐹 𝑦 ) ) ↔ ∃ 𝑥 ( ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵 ) ∧ 𝑥 𝐹 𝑦 ) )
40 27 39 sylib ⊢ ( ( ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝐹 𝑦 ) ∧ ¬ ∃ 𝑥 ( 𝑥 ∈ 𝐵 ∧ 𝑥 𝐹 𝑦 ) ) → ∃ 𝑥 ( ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵 ) ∧ 𝑥 𝐹 𝑦 ) )
41 25 40 impbid1 ⊢ ( Fun ◡ 𝐹 → ( ∃ 𝑥 ( ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵 ) ∧ 𝑥 𝐹 𝑦 ) ↔ ( ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝐹 𝑦 ) ∧ ¬ ∃ 𝑥 ( 𝑥 ∈ 𝐵 ∧ 𝑥 𝐹 𝑦 ) ) ) )
42 eldif ⊢ ( 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵 ) )
43 42 anbi1i ⊢ ( ( 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) ∧ 𝑥 𝐹 𝑦 ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵 ) ∧ 𝑥 𝐹 𝑦 ) )
44 43 exbii ⊢ ( ∃ 𝑥 ( 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) ∧ 𝑥 𝐹 𝑦 ) ↔ ∃ 𝑥 ( ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵 ) ∧ 𝑥 𝐹 𝑦 ) )
45 9 elima2 ⊢ ( 𝑦 ∈ ( 𝐹 “ 𝐴 ) ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝐹 𝑦 ) )
46 9 elima2 ⊢ ( 𝑦 ∈ ( 𝐹 “ 𝐵 ) ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐵 ∧ 𝑥 𝐹 𝑦 ) )
47 46 notbii ⊢ ( ¬ 𝑦 ∈ ( 𝐹 “ 𝐵 ) ↔ ¬ ∃ 𝑥 ( 𝑥 ∈ 𝐵 ∧ 𝑥 𝐹 𝑦 ) )
48 45 47 anbi12i ⊢ ( ( 𝑦 ∈ ( 𝐹 “ 𝐴 ) ∧ ¬ 𝑦 ∈ ( 𝐹 “ 𝐵 ) ) ↔ ( ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝐹 𝑦 ) ∧ ¬ ∃ 𝑥 ( 𝑥 ∈ 𝐵 ∧ 𝑥 𝐹 𝑦 ) ) )
49 41 44 48 3bitr4g ⊢ ( Fun ◡ 𝐹 → ( ∃ 𝑥 ( 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) ∧ 𝑥 𝐹 𝑦 ) ↔ ( 𝑦 ∈ ( 𝐹 “ 𝐴 ) ∧ ¬ 𝑦 ∈ ( 𝐹 “ 𝐵 ) ) ) )
50 9 elima2 ⊢ ( 𝑦 ∈ ( 𝐹 “ ( 𝐴 ∖ 𝐵 ) ) ↔ ∃ 𝑥 ( 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) ∧ 𝑥 𝐹 𝑦 ) )
51 eldif ⊢ ( 𝑦 ∈ ( ( 𝐹 “ 𝐴 ) ∖ ( 𝐹 “ 𝐵 ) ) ↔ ( 𝑦 ∈ ( 𝐹 “ 𝐴 ) ∧ ¬ 𝑦 ∈ ( 𝐹 “ 𝐵 ) ) )
52 49 50 51 3bitr4g ⊢ ( Fun ◡ 𝐹 → ( 𝑦 ∈ ( 𝐹 “ ( 𝐴 ∖ 𝐵 ) ) ↔ 𝑦 ∈ ( ( 𝐹 “ 𝐴 ) ∖ ( 𝐹 “ 𝐵 ) ) ) )
53 52 eqrdv ⊢ ( Fun ◡ 𝐹 → ( 𝐹 “ ( 𝐴 ∖ 𝐵 ) ) = ( ( 𝐹 “ 𝐴 ) ∖ ( 𝐹 “ 𝐵 ) ) )