difmapsn

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

	Ref	Expression
Hypotheses	difmapsn.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	difmapsn.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
	difmapsn.v	⊢ ( 𝜑 → 𝐶 ∈ 𝑍 )
Assertion	difmapsn	⊢ ( 𝜑 → ( ( 𝐴 ↑_m { 𝐶 } ) ∖ ( 𝐵 ↑_m { 𝐶 } ) ) = ( ( 𝐴 ∖ 𝐵 ) ↑_m { 𝐶 } ) )

Proof

Step	Hyp	Ref	Expression
1		difmapsn.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2		difmapsn.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
3		difmapsn.v	⊢ ( 𝜑 → 𝐶 ∈ 𝑍 )
4		eldifi	⊢ ( 𝑓 ∈ ( ( 𝐴 ↑_m { 𝐶 } ) ∖ ( 𝐵 ↑_m { 𝐶 } ) ) → 𝑓 ∈ ( 𝐴 ↑_m { 𝐶 } ) )
5	4	adantl	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( ( 𝐴 ↑_m { 𝐶 } ) ∖ ( 𝐵 ↑_m { 𝐶 } ) ) ) → 𝑓 ∈ ( 𝐴 ↑_m { 𝐶 } ) )
6		elmapi	⊢ ( 𝑓 ∈ ( 𝐴 ↑_m { 𝐶 } ) → 𝑓 : { 𝐶 } ⟶ 𝐴 )
7	6	adantl	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐴 ↑_m { 𝐶 } ) ) → 𝑓 : { 𝐶 } ⟶ 𝐴 )
8		fsn2g	⊢ ( 𝐶 ∈ 𝑍 → ( 𝑓 : { 𝐶 } ⟶ 𝐴 ↔ ( ( 𝑓 ‘ 𝐶 ) ∈ 𝐴 ∧ 𝑓 = { ⟨ 𝐶 , ( 𝑓 ‘ 𝐶 ) ⟩ } ) ) )
9	3 8	syl	⊢ ( 𝜑 → ( 𝑓 : { 𝐶 } ⟶ 𝐴 ↔ ( ( 𝑓 ‘ 𝐶 ) ∈ 𝐴 ∧ 𝑓 = { ⟨ 𝐶 , ( 𝑓 ‘ 𝐶 ) ⟩ } ) ) )
10	9	adantr	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐴 ↑_m { 𝐶 } ) ) → ( 𝑓 : { 𝐶 } ⟶ 𝐴 ↔ ( ( 𝑓 ‘ 𝐶 ) ∈ 𝐴 ∧ 𝑓 = { ⟨ 𝐶 , ( 𝑓 ‘ 𝐶 ) ⟩ } ) ) )
11	7 10	mpbid	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐴 ↑_m { 𝐶 } ) ) → ( ( 𝑓 ‘ 𝐶 ) ∈ 𝐴 ∧ 𝑓 = { ⟨ 𝐶 , ( 𝑓 ‘ 𝐶 ) ⟩ } ) )
12	11	simpld	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐴 ↑_m { 𝐶 } ) ) → ( 𝑓 ‘ 𝐶 ) ∈ 𝐴 )
13	5 12	syldan	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( ( 𝐴 ↑_m { 𝐶 } ) ∖ ( 𝐵 ↑_m { 𝐶 } ) ) ) → ( 𝑓 ‘ 𝐶 ) ∈ 𝐴 )
14		simpr	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( ( 𝐴 ↑_m { 𝐶 } ) ∖ ( 𝐵 ↑_m { 𝐶 } ) ) ) ∧ ( 𝑓 ‘ 𝐶 ) ∈ 𝐵 ) → ( 𝑓 ‘ 𝐶 ) ∈ 𝐵 )
15	11	simprd	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐴 ↑_m { 𝐶 } ) ) → 𝑓 = { ⟨ 𝐶 , ( 𝑓 ‘ 𝐶 ) ⟩ } )
16	5 15	syldan	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( ( 𝐴 ↑_m { 𝐶 } ) ∖ ( 𝐵 ↑_m { 𝐶 } ) ) ) → 𝑓 = { ⟨ 𝐶 , ( 𝑓 ‘ 𝐶 ) ⟩ } )
17	16	adantr	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( ( 𝐴 ↑_m { 𝐶 } ) ∖ ( 𝐵 ↑_m { 𝐶 } ) ) ) ∧ ( 𝑓 ‘ 𝐶 ) ∈ 𝐵 ) → 𝑓 = { ⟨ 𝐶 , ( 𝑓 ‘ 𝐶 ) ⟩ } )
18	14 17	jca	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( ( 𝐴 ↑_m { 𝐶 } ) ∖ ( 𝐵 ↑_m { 𝐶 } ) ) ) ∧ ( 𝑓 ‘ 𝐶 ) ∈ 𝐵 ) → ( ( 𝑓 ‘ 𝐶 ) ∈ 𝐵 ∧ 𝑓 = { ⟨ 𝐶 , ( 𝑓 ‘ 𝐶 ) ⟩ } ) )
19		fsn2g	⊢ ( 𝐶 ∈ 𝑍 → ( 𝑓 : { 𝐶 } ⟶ 𝐵 ↔ ( ( 𝑓 ‘ 𝐶 ) ∈ 𝐵 ∧ 𝑓 = { ⟨ 𝐶 , ( 𝑓 ‘ 𝐶 ) ⟩ } ) ) )
20	3 19	syl	⊢ ( 𝜑 → ( 𝑓 : { 𝐶 } ⟶ 𝐵 ↔ ( ( 𝑓 ‘ 𝐶 ) ∈ 𝐵 ∧ 𝑓 = { ⟨ 𝐶 , ( 𝑓 ‘ 𝐶 ) ⟩ } ) ) )
21	20	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( ( 𝐴 ↑_m { 𝐶 } ) ∖ ( 𝐵 ↑_m { 𝐶 } ) ) ) ∧ ( 𝑓 ‘ 𝐶 ) ∈ 𝐵 ) → ( 𝑓 : { 𝐶 } ⟶ 𝐵 ↔ ( ( 𝑓 ‘ 𝐶 ) ∈ 𝐵 ∧ 𝑓 = { ⟨ 𝐶 , ( 𝑓 ‘ 𝐶 ) ⟩ } ) ) )
22	18 21	mpbird	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( ( 𝐴 ↑_m { 𝐶 } ) ∖ ( 𝐵 ↑_m { 𝐶 } ) ) ) ∧ ( 𝑓 ‘ 𝐶 ) ∈ 𝐵 ) → 𝑓 : { 𝐶 } ⟶ 𝐵 )
23	2	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( ( 𝐴 ↑_m { 𝐶 } ) ∖ ( 𝐵 ↑_m { 𝐶 } ) ) ) ∧ ( 𝑓 ‘ 𝐶 ) ∈ 𝐵 ) → 𝐵 ∈ 𝑊 )
24		snex	⊢ { 𝐶 } ∈ V
25	24	a1i	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( ( 𝐴 ↑_m { 𝐶 } ) ∖ ( 𝐵 ↑_m { 𝐶 } ) ) ) ∧ ( 𝑓 ‘ 𝐶 ) ∈ 𝐵 ) → { 𝐶 } ∈ V )
26	23 25	elmapd	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( ( 𝐴 ↑_m { 𝐶 } ) ∖ ( 𝐵 ↑_m { 𝐶 } ) ) ) ∧ ( 𝑓 ‘ 𝐶 ) ∈ 𝐵 ) → ( 𝑓 ∈ ( 𝐵 ↑_m { 𝐶 } ) ↔ 𝑓 : { 𝐶 } ⟶ 𝐵 ) )
27	22 26	mpbird	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( ( 𝐴 ↑_m { 𝐶 } ) ∖ ( 𝐵 ↑_m { 𝐶 } ) ) ) ∧ ( 𝑓 ‘ 𝐶 ) ∈ 𝐵 ) → 𝑓 ∈ ( 𝐵 ↑_m { 𝐶 } ) )
28		eldifn	⊢ ( 𝑓 ∈ ( ( 𝐴 ↑_m { 𝐶 } ) ∖ ( 𝐵 ↑_m { 𝐶 } ) ) → ¬ 𝑓 ∈ ( 𝐵 ↑_m { 𝐶 } ) )
29	28	ad2antlr	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( ( 𝐴 ↑_m { 𝐶 } ) ∖ ( 𝐵 ↑_m { 𝐶 } ) ) ) ∧ ( 𝑓 ‘ 𝐶 ) ∈ 𝐵 ) → ¬ 𝑓 ∈ ( 𝐵 ↑_m { 𝐶 } ) )
30	27 29	pm2.65da	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( ( 𝐴 ↑_m { 𝐶 } ) ∖ ( 𝐵 ↑_m { 𝐶 } ) ) ) → ¬ ( 𝑓 ‘ 𝐶 ) ∈ 𝐵 )
31	13 30	eldifd	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( ( 𝐴 ↑_m { 𝐶 } ) ∖ ( 𝐵 ↑_m { 𝐶 } ) ) ) → ( 𝑓 ‘ 𝐶 ) ∈ ( 𝐴 ∖ 𝐵 ) )
32	31 16	jca	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( ( 𝐴 ↑_m { 𝐶 } ) ∖ ( 𝐵 ↑_m { 𝐶 } ) ) ) → ( ( 𝑓 ‘ 𝐶 ) ∈ ( 𝐴 ∖ 𝐵 ) ∧ 𝑓 = { ⟨ 𝐶 , ( 𝑓 ‘ 𝐶 ) ⟩ } ) )
33		fsn2g	⊢ ( 𝐶 ∈ 𝑍 → ( 𝑓 : { 𝐶 } ⟶ ( 𝐴 ∖ 𝐵 ) ↔ ( ( 𝑓 ‘ 𝐶 ) ∈ ( 𝐴 ∖ 𝐵 ) ∧ 𝑓 = { ⟨ 𝐶 , ( 𝑓 ‘ 𝐶 ) ⟩ } ) ) )
34	3 33	syl	⊢ ( 𝜑 → ( 𝑓 : { 𝐶 } ⟶ ( 𝐴 ∖ 𝐵 ) ↔ ( ( 𝑓 ‘ 𝐶 ) ∈ ( 𝐴 ∖ 𝐵 ) ∧ 𝑓 = { ⟨ 𝐶 , ( 𝑓 ‘ 𝐶 ) ⟩ } ) ) )
35	34	adantr	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( ( 𝐴 ↑_m { 𝐶 } ) ∖ ( 𝐵 ↑_m { 𝐶 } ) ) ) → ( 𝑓 : { 𝐶 } ⟶ ( 𝐴 ∖ 𝐵 ) ↔ ( ( 𝑓 ‘ 𝐶 ) ∈ ( 𝐴 ∖ 𝐵 ) ∧ 𝑓 = { ⟨ 𝐶 , ( 𝑓 ‘ 𝐶 ) ⟩ } ) ) )
36	32 35	mpbird	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( ( 𝐴 ↑_m { 𝐶 } ) ∖ ( 𝐵 ↑_m { 𝐶 } ) ) ) → 𝑓 : { 𝐶 } ⟶ ( 𝐴 ∖ 𝐵 ) )
37		difssd	⊢ ( 𝜑 → ( 𝐴 ∖ 𝐵 ) ⊆ 𝐴 )
38	1 37	ssexd	⊢ ( 𝜑 → ( 𝐴 ∖ 𝐵 ) ∈ V )
39	24	a1i	⊢ ( 𝜑 → { 𝐶 } ∈ V )
40	38 39	elmapd	⊢ ( 𝜑 → ( 𝑓 ∈ ( ( 𝐴 ∖ 𝐵 ) ↑_m { 𝐶 } ) ↔ 𝑓 : { 𝐶 } ⟶ ( 𝐴 ∖ 𝐵 ) ) )
41	40	adantr	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( ( 𝐴 ↑_m { 𝐶 } ) ∖ ( 𝐵 ↑_m { 𝐶 } ) ) ) → ( 𝑓 ∈ ( ( 𝐴 ∖ 𝐵 ) ↑_m { 𝐶 } ) ↔ 𝑓 : { 𝐶 } ⟶ ( 𝐴 ∖ 𝐵 ) ) )
42	36 41	mpbird	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( ( 𝐴 ↑_m { 𝐶 } ) ∖ ( 𝐵 ↑_m { 𝐶 } ) ) ) → 𝑓 ∈ ( ( 𝐴 ∖ 𝐵 ) ↑_m { 𝐶 } ) )
43	42	ralrimiva	⊢ ( 𝜑 → ∀ 𝑓 ∈ ( ( 𝐴 ↑_m { 𝐶 } ) ∖ ( 𝐵 ↑_m { 𝐶 } ) ) 𝑓 ∈ ( ( 𝐴 ∖ 𝐵 ) ↑_m { 𝐶 } ) )
44		dfss3	⊢ ( ( ( 𝐴 ↑_m { 𝐶 } ) ∖ ( 𝐵 ↑_m { 𝐶 } ) ) ⊆ ( ( 𝐴 ∖ 𝐵 ) ↑_m { 𝐶 } ) ↔ ∀ 𝑓 ∈ ( ( 𝐴 ↑_m { 𝐶 } ) ∖ ( 𝐵 ↑_m { 𝐶 } ) ) 𝑓 ∈ ( ( 𝐴 ∖ 𝐵 ) ↑_m { 𝐶 } ) )
45	43 44	sylibr	⊢ ( 𝜑 → ( ( 𝐴 ↑_m { 𝐶 } ) ∖ ( 𝐵 ↑_m { 𝐶 } ) ) ⊆ ( ( 𝐴 ∖ 𝐵 ) ↑_m { 𝐶 } ) )
46	3	snn0d	⊢ ( 𝜑 → { 𝐶 } ≠ ∅ )
47	1 2 39 46	difmap	⊢ ( 𝜑 → ( ( 𝐴 ∖ 𝐵 ) ↑_m { 𝐶 } ) ⊆ ( ( 𝐴 ↑_m { 𝐶 } ) ∖ ( 𝐵 ↑_m { 𝐶 } ) ) )
48	45 47	eqssd	⊢ ( 𝜑 → ( ( 𝐴 ↑_m { 𝐶 } ) ∖ ( 𝐵 ↑_m { 𝐶 } ) ) = ( ( 𝐴 ∖ 𝐵 ) ↑_m { 𝐶 } ) )

Metamath Proof Explorer

Theorem difmapsn

Proof