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 𝐶 ) ) )

Metamath Proof Explorer

Theorem difmap

Proof