Metamath Proof Explorer


Theorem difmap

Description: Difference of two sets exponentiations. (Contributed by Glauco Siliprandi, 3-Mar-2021)

Ref Expression
Hypotheses difmap.a ( 𝜑𝐴𝑉 )
difmap.b ( 𝜑𝐵𝑊 )
difmap.v ( 𝜑𝐶𝑍 )
difmap.n ( 𝜑𝐶 ≠ ∅ )
Assertion difmap ( 𝜑 → ( ( 𝐴𝐵 ) ↑m 𝐶 ) ⊆ ( ( 𝐴m 𝐶 ) ∖ ( 𝐵m 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 difmap.a ( 𝜑𝐴𝑉 )
2 difmap.b ( 𝜑𝐵𝑊 )
3 difmap.v ( 𝜑𝐶𝑍 )
4 difmap.n ( 𝜑𝐶 ≠ ∅ )
5 difssd ( 𝜑 → ( 𝐴𝐵 ) ⊆ 𝐴 )
6 mapss ( ( 𝐴𝑉 ∧ ( 𝐴𝐵 ) ⊆ 𝐴 ) → ( ( 𝐴𝐵 ) ↑m 𝐶 ) ⊆ ( 𝐴m 𝐶 ) )
7 1 5 6 syl2anc ( 𝜑 → ( ( 𝐴𝐵 ) ↑m 𝐶 ) ⊆ ( 𝐴m 𝐶 ) )
8 7 adantr ( ( 𝜑𝑓 ∈ ( ( 𝐴𝐵 ) ↑m 𝐶 ) ) → ( ( 𝐴𝐵 ) ↑m 𝐶 ) ⊆ ( 𝐴m 𝐶 ) )
9 simpr ( ( 𝜑𝑓 ∈ ( ( 𝐴𝐵 ) ↑m 𝐶 ) ) → 𝑓 ∈ ( ( 𝐴𝐵 ) ↑m 𝐶 ) )
10 8 9 sseldd ( ( 𝜑𝑓 ∈ ( ( 𝐴𝐵 ) ↑m 𝐶 ) ) → 𝑓 ∈ ( 𝐴m 𝐶 ) )
11 n0 ( 𝐶 ≠ ∅ ↔ ∃ 𝑥 𝑥𝐶 )
12 4 11 sylib ( 𝜑 → ∃ 𝑥 𝑥𝐶 )
13 12 adantr ( ( 𝜑𝑓 ∈ ( ( 𝐴𝐵 ) ↑m 𝐶 ) ) → ∃ 𝑥 𝑥𝐶 )
14 simpr ( ( 𝑥𝐶𝑓 : 𝐶𝐵 ) → 𝑓 : 𝐶𝐵 )
15 simpl ( ( 𝑥𝐶𝑓 : 𝐶𝐵 ) → 𝑥𝐶 )
16 14 15 ffvelrnd ( ( 𝑥𝐶𝑓 : 𝐶𝐵 ) → ( 𝑓𝑥 ) ∈ 𝐵 )
17 16 adantll ( ( ( ( 𝜑𝑓 ∈ ( ( 𝐴𝐵 ) ↑m 𝐶 ) ) ∧ 𝑥𝐶 ) ∧ 𝑓 : 𝐶𝐵 ) → ( 𝑓𝑥 ) ∈ 𝐵 )
18 elmapi ( 𝑓 ∈ ( ( 𝐴𝐵 ) ↑m 𝐶 ) → 𝑓 : 𝐶 ⟶ ( 𝐴𝐵 ) )
19 18 adantr ( ( 𝑓 ∈ ( ( 𝐴𝐵 ) ↑m 𝐶 ) ∧ 𝑥𝐶 ) → 𝑓 : 𝐶 ⟶ ( 𝐴𝐵 ) )
20 simpr ( ( 𝑓 ∈ ( ( 𝐴𝐵 ) ↑m 𝐶 ) ∧ 𝑥𝐶 ) → 𝑥𝐶 )
21 19 20 ffvelrnd ( ( 𝑓 ∈ ( ( 𝐴𝐵 ) ↑m 𝐶 ) ∧ 𝑥𝐶 ) → ( 𝑓𝑥 ) ∈ ( 𝐴𝐵 ) )
22 eldifn ( ( 𝑓𝑥 ) ∈ ( 𝐴𝐵 ) → ¬ ( 𝑓𝑥 ) ∈ 𝐵 )
23 21 22 syl ( ( 𝑓 ∈ ( ( 𝐴𝐵 ) ↑m 𝐶 ) ∧ 𝑥𝐶 ) → ¬ ( 𝑓𝑥 ) ∈ 𝐵 )
24 23 ad4ant23 ( ( ( ( 𝜑𝑓 ∈ ( ( 𝐴𝐵 ) ↑m 𝐶 ) ) ∧ 𝑥𝐶 ) ∧ 𝑓 : 𝐶𝐵 ) → ¬ ( 𝑓𝑥 ) ∈ 𝐵 )
25 17 24 pm2.65da ( ( ( 𝜑𝑓 ∈ ( ( 𝐴𝐵 ) ↑m 𝐶 ) ) ∧ 𝑥𝐶 ) → ¬ 𝑓 : 𝐶𝐵 )
26 25 ex ( ( 𝜑𝑓 ∈ ( ( 𝐴𝐵 ) ↑m 𝐶 ) ) → ( 𝑥𝐶 → ¬ 𝑓 : 𝐶𝐵 ) )
27 26 exlimdv ( ( 𝜑𝑓 ∈ ( ( 𝐴𝐵 ) ↑m 𝐶 ) ) → ( ∃ 𝑥 𝑥𝐶 → ¬ 𝑓 : 𝐶𝐵 ) )
28 13 27 mpd ( ( 𝜑𝑓 ∈ ( ( 𝐴𝐵 ) ↑m 𝐶 ) ) → ¬ 𝑓 : 𝐶𝐵 )
29 elmapg ( ( 𝐵𝑊𝐶𝑍 ) → ( 𝑓 ∈ ( 𝐵m 𝐶 ) ↔ 𝑓 : 𝐶𝐵 ) )
30 2 3 29 syl2anc ( 𝜑 → ( 𝑓 ∈ ( 𝐵m 𝐶 ) ↔ 𝑓 : 𝐶𝐵 ) )
31 30 adantr ( ( 𝜑𝑓 ∈ ( ( 𝐴𝐵 ) ↑m 𝐶 ) ) → ( 𝑓 ∈ ( 𝐵m 𝐶 ) ↔ 𝑓 : 𝐶𝐵 ) )
32 28 31 mtbird ( ( 𝜑𝑓 ∈ ( ( 𝐴𝐵 ) ↑m 𝐶 ) ) → ¬ 𝑓 ∈ ( 𝐵m 𝐶 ) )
33 10 32 eldifd ( ( 𝜑𝑓 ∈ ( ( 𝐴𝐵 ) ↑m 𝐶 ) ) → 𝑓 ∈ ( ( 𝐴m 𝐶 ) ∖ ( 𝐵m 𝐶 ) ) )
34 33 ralrimiva ( 𝜑 → ∀ 𝑓 ∈ ( ( 𝐴𝐵 ) ↑m 𝐶 ) 𝑓 ∈ ( ( 𝐴m 𝐶 ) ∖ ( 𝐵m 𝐶 ) ) )
35 dfss3 ( ( ( 𝐴𝐵 ) ↑m 𝐶 ) ⊆ ( ( 𝐴m 𝐶 ) ∖ ( 𝐵m 𝐶 ) ) ↔ ∀ 𝑓 ∈ ( ( 𝐴𝐵 ) ↑m 𝐶 ) 𝑓 ∈ ( ( 𝐴m 𝐶 ) ∖ ( 𝐵m 𝐶 ) ) )
36 34 35 sylibr ( 𝜑 → ( ( 𝐴𝐵 ) ↑m 𝐶 ) ⊆ ( ( 𝐴m 𝐶 ) ∖ ( 𝐵m 𝐶 ) ) )