Metamath Proof Explorer

Theorem difmapsn

Description: Difference of two sets exponentiatiated to a singleton. (Contributed by Glauco Siliprandi, 3-Mar-2021)

Ref Expression
Hypotheses difmapsn.a ⊢ φ → A ∈ V
difmapsn.b ⊢ φ → B ∈ W
difmapsn.v ⊢ φ → C ∈ Z
Assertion difmapsn ⊢ φ → A C ∖ B C = A ∖ B C

Proof

Step Hyp Ref Expression
1 difmapsn.a ⊢ φ → A ∈ V
2 difmapsn.b ⊢ φ → B ∈ W
3 difmapsn.v ⊢ φ → C ∈ Z
4 eldifi ⊢ f ∈ A C ∖ B C → f ∈ A C
5 4 adantl ⊢ φ ∧ f ∈ A C ∖ B C → f ∈ A C
6 elmapi ⊢ f ∈ A C → f : C ⟶ A
7 6 adantl ⊢ φ ∧ f ∈ A C → f : C ⟶ A
8 fsn2g ⊢ C ∈ Z → f : C ⟶ A ↔ f ⁡ C ∈ A ∧ f = C f ⁡ C
9 3 8 syl ⊢ φ → f : C ⟶ A ↔ f ⁡ C ∈ A ∧ f = C f ⁡ C
10 9 adantr ⊢ φ ∧ f ∈ A C → f : C ⟶ A ↔ f ⁡ C ∈ A ∧ f = C f ⁡ C
11 7 10 mpbid ⊢ φ ∧ f ∈ A C → f ⁡ C ∈ A ∧ f = C f ⁡ C
12 11 simpld ⊢ φ ∧ f ∈ A C → f ⁡ C ∈ A
13 5 12 syldan ⊢ φ ∧ f ∈ A C ∖ B C → f ⁡ C ∈ A
14 simpr ⊢ φ ∧ f ∈ A C ∖ B C ∧ f ⁡ C ∈ B → f ⁡ C ∈ B
15 11 simprd ⊢ φ ∧ f ∈ A C → f = C f ⁡ C
16 5 15 syldan ⊢ φ ∧ f ∈ A C ∖ B C → f = C f ⁡ C
17 16 adantr ⊢ φ ∧ f ∈ A C ∖ B C ∧ f ⁡ C ∈ B → f = C f ⁡ C
18 14 17 jca ⊢ φ ∧ f ∈ A C ∖ B C ∧ f ⁡ C ∈ B → f ⁡ C ∈ B ∧ f = C f ⁡ C
19 fsn2g ⊢ C ∈ Z → f : C ⟶ B ↔ f ⁡ C ∈ B ∧ f = C f ⁡ C
20 3 19 syl ⊢ φ → f : C ⟶ B ↔ f ⁡ C ∈ B ∧ f = C f ⁡ C
21 20 ad2antrr ⊢ φ ∧ f ∈ A C ∖ B C ∧ f ⁡ C ∈ B → f : C ⟶ B ↔ f ⁡ C ∈ B ∧ f = C f ⁡ C
22 18 21 mpbird ⊢ φ ∧ f ∈ A C ∖ B C ∧ f ⁡ C ∈ B → f : C ⟶ B
23 2 ad2antrr ⊢ φ ∧ f ∈ A C ∖ B C ∧ f ⁡ C ∈ B → B ∈ W
24 snex ⊢ C ∈ V
25 24 a1i ⊢ φ ∧ f ∈ A C ∖ B C ∧ f ⁡ C ∈ B → C ∈ V
26 23 25 elmapd ⊢ φ ∧ f ∈ A C ∖ B C ∧ f ⁡ C ∈ B → f ∈ B C ↔ f : C ⟶ B
27 22 26 mpbird ⊢ φ ∧ f ∈ A C ∖ B C ∧ f ⁡ C ∈ B → f ∈ B C
28 eldifn ⊢ f ∈ A C ∖ B C → ¬ f ∈ B C
29 28 ad2antlr ⊢ φ ∧ f ∈ A C ∖ B C ∧ f ⁡ C ∈ B → ¬ f ∈ B C
30 27 29 pm2.65da ⊢ φ ∧ f ∈ A C ∖ B C → ¬ f ⁡ C ∈ B
31 13 30 eldifd ⊢ φ ∧ f ∈ A C ∖ B C → f ⁡ C ∈ A ∖ B
32 31 16 jca ⊢ φ ∧ f ∈ A C ∖ B C → f ⁡ C ∈ A ∖ B ∧ f = C f ⁡ C
33 fsn2g ⊢ C ∈ Z → f : C ⟶ A ∖ B ↔ f ⁡ C ∈ A ∖ B ∧ f = C f ⁡ C
34 3 33 syl ⊢ φ → f : C ⟶ A ∖ B ↔ f ⁡ C ∈ A ∖ B ∧ f = C f ⁡ C
35 34 adantr ⊢ φ ∧ f ∈ A C ∖ B C → f : C ⟶ A ∖ B ↔ f ⁡ C ∈ A ∖ B ∧ f = C f ⁡ C
36 32 35 mpbird ⊢ φ ∧ f ∈ A C ∖ B C → f : C ⟶ A ∖ B
37 difssd ⊢ φ → A ∖ B ⊆ A
38 1 37 ssexd ⊢ φ → A ∖ B ∈ V
39 24 a1i ⊢ φ → C ∈ V
40 38 39 elmapd ⊢ φ → f ∈ A ∖ B C ↔ f : C ⟶ A ∖ B
41 40 adantr ⊢ φ ∧ f ∈ A C ∖ B C → f ∈ A ∖ B C ↔ f : C ⟶ A ∖ B
42 36 41 mpbird ⊢ φ ∧ f ∈ A C ∖ B C → f ∈ A ∖ B C
43 42 ralrimiva ⊢ φ → ∀ f ∈ A C ∖ B C f ∈ A ∖ B C
44 dfss3 ⊢ A C ∖ B C ⊆ A ∖ B C ↔ ∀ f ∈ A C ∖ B C f ∈ A ∖ B C
45 43 44 sylibr ⊢ φ → A C ∖ B C ⊆ A ∖ B C
46 3 snn0d ⊢ φ → C ≠ ∅
47 1 2 39 46 difmap ⊢ φ → A ∖ B C ⊆ A C ∖ B C
48 45 47 eqssd ⊢ φ → A C ∖ B C = A ∖ B C