inmap

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

	Ref	Expression
Hypotheses	inmap.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	inmap.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
	inmap.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑍 )
Assertion	inmap	⊢ ( 𝜑 → ( ( 𝐴 ↑_m 𝐶 ) ∩ ( 𝐵 ↑_m 𝐶 ) ) = ( ( 𝐴 ∩ 𝐵 ) ↑_m 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		inmap.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2		inmap.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
3		inmap.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑍 )
4		elinel1	⊢ ( 𝑓 ∈ ( ( 𝐴 ↑_m 𝐶 ) ∩ ( 𝐵 ↑_m 𝐶 ) ) → 𝑓 ∈ ( 𝐴 ↑_m 𝐶 ) )
5		elmapi	⊢ ( 𝑓 ∈ ( 𝐴 ↑_m 𝐶 ) → 𝑓 : 𝐶 ⟶ 𝐴 )
6	4 5	syl	⊢ ( 𝑓 ∈ ( ( 𝐴 ↑_m 𝐶 ) ∩ ( 𝐵 ↑_m 𝐶 ) ) → 𝑓 : 𝐶 ⟶ 𝐴 )
7		elinel2	⊢ ( 𝑓 ∈ ( ( 𝐴 ↑_m 𝐶 ) ∩ ( 𝐵 ↑_m 𝐶 ) ) → 𝑓 ∈ ( 𝐵 ↑_m 𝐶 ) )
8		elmapi	⊢ ( 𝑓 ∈ ( 𝐵 ↑_m 𝐶 ) → 𝑓 : 𝐶 ⟶ 𝐵 )
9	7 8	syl	⊢ ( 𝑓 ∈ ( ( 𝐴 ↑_m 𝐶 ) ∩ ( 𝐵 ↑_m 𝐶 ) ) → 𝑓 : 𝐶 ⟶ 𝐵 )
10	6 9	jca	⊢ ( 𝑓 ∈ ( ( 𝐴 ↑_m 𝐶 ) ∩ ( 𝐵 ↑_m 𝐶 ) ) → ( 𝑓 : 𝐶 ⟶ 𝐴 ∧ 𝑓 : 𝐶 ⟶ 𝐵 ) )
11		fin	⊢ ( 𝑓 : 𝐶 ⟶ ( 𝐴 ∩ 𝐵 ) ↔ ( 𝑓 : 𝐶 ⟶ 𝐴 ∧ 𝑓 : 𝐶 ⟶ 𝐵 ) )
12	10 11	sylibr	⊢ ( 𝑓 ∈ ( ( 𝐴 ↑_m 𝐶 ) ∩ ( 𝐵 ↑_m 𝐶 ) ) → 𝑓 : 𝐶 ⟶ ( 𝐴 ∩ 𝐵 ) )
13	12	adantl	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( ( 𝐴 ↑_m 𝐶 ) ∩ ( 𝐵 ↑_m 𝐶 ) ) ) → 𝑓 : 𝐶 ⟶ ( 𝐴 ∩ 𝐵 ) )
14		inss1	⊢ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐴
15	14	a1i	⊢ ( 𝜑 → ( 𝐴 ∩ 𝐵 ) ⊆ 𝐴 )
16	1 15	ssexd	⊢ ( 𝜑 → ( 𝐴 ∩ 𝐵 ) ∈ V )
17	16 3	elmapd	⊢ ( 𝜑 → ( 𝑓 ∈ ( ( 𝐴 ∩ 𝐵 ) ↑_m 𝐶 ) ↔ 𝑓 : 𝐶 ⟶ ( 𝐴 ∩ 𝐵 ) ) )
18	17	adantr	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( ( 𝐴 ↑_m 𝐶 ) ∩ ( 𝐵 ↑_m 𝐶 ) ) ) → ( 𝑓 ∈ ( ( 𝐴 ∩ 𝐵 ) ↑_m 𝐶 ) ↔ 𝑓 : 𝐶 ⟶ ( 𝐴 ∩ 𝐵 ) ) )
19	13 18	mpbird	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( ( 𝐴 ↑_m 𝐶 ) ∩ ( 𝐵 ↑_m 𝐶 ) ) ) → 𝑓 ∈ ( ( 𝐴 ∩ 𝐵 ) ↑_m 𝐶 ) )
20	19	ralrimiva	⊢ ( 𝜑 → ∀ 𝑓 ∈ ( ( 𝐴 ↑_m 𝐶 ) ∩ ( 𝐵 ↑_m 𝐶 ) ) 𝑓 ∈ ( ( 𝐴 ∩ 𝐵 ) ↑_m 𝐶 ) )
21		dfss3	⊢ ( ( ( 𝐴 ↑_m 𝐶 ) ∩ ( 𝐵 ↑_m 𝐶 ) ) ⊆ ( ( 𝐴 ∩ 𝐵 ) ↑_m 𝐶 ) ↔ ∀ 𝑓 ∈ ( ( 𝐴 ↑_m 𝐶 ) ∩ ( 𝐵 ↑_m 𝐶 ) ) 𝑓 ∈ ( ( 𝐴 ∩ 𝐵 ) ↑_m 𝐶 ) )
22	20 21	sylibr	⊢ ( 𝜑 → ( ( 𝐴 ↑_m 𝐶 ) ∩ ( 𝐵 ↑_m 𝐶 ) ) ⊆ ( ( 𝐴 ∩ 𝐵 ) ↑_m 𝐶 ) )
23		mapss	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐴 ) → ( ( 𝐴 ∩ 𝐵 ) ↑_m 𝐶 ) ⊆ ( 𝐴 ↑_m 𝐶 ) )
24	1 15 23	syl2anc	⊢ ( 𝜑 → ( ( 𝐴 ∩ 𝐵 ) ↑_m 𝐶 ) ⊆ ( 𝐴 ↑_m 𝐶 ) )
25		inss2	⊢ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐵
26	25	a1i	⊢ ( 𝜑 → ( 𝐴 ∩ 𝐵 ) ⊆ 𝐵 )
27		mapss	⊢ ( ( 𝐵 ∈ 𝑊 ∧ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐵 ) → ( ( 𝐴 ∩ 𝐵 ) ↑_m 𝐶 ) ⊆ ( 𝐵 ↑_m 𝐶 ) )
28	2 26 27	syl2anc	⊢ ( 𝜑 → ( ( 𝐴 ∩ 𝐵 ) ↑_m 𝐶 ) ⊆ ( 𝐵 ↑_m 𝐶 ) )
29	24 28	ssind	⊢ ( 𝜑 → ( ( 𝐴 ∩ 𝐵 ) ↑_m 𝐶 ) ⊆ ( ( 𝐴 ↑_m 𝐶 ) ∩ ( 𝐵 ↑_m 𝐶 ) ) )
30	22 29	eqssd	⊢ ( 𝜑 → ( ( 𝐴 ↑_m 𝐶 ) ∩ ( 𝐵 ↑_m 𝐶 ) ) = ( ( 𝐴 ∩ 𝐵 ) ↑_m 𝐶 ) )

Metamath Proof Explorer

Theorem inmap

Proof