Theorem maprnin

Description: Restricting the range of the mapping operator. (Contributed by Thierry Arnoux, 30-Aug-2017)

	Ref	Expression
Hypotheses	maprnin.1	⊢ 𝐴 ∈ V
	maprnin.2	⊢ 𝐵 ∈ V
Assertion	maprnin	⊢ ( ( 𝐵 ∩ 𝐶 ) ↑m 𝐴 ) = { 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) ∣ ran 𝑓 ⊆ 𝐶 }

Proof

Step	Hyp	Ref	Expression
1		maprnin.1	⊢ 𝐴 ∈ V
2		maprnin.2	⊢ 𝐵 ∈ V
3		ffn	⊢ ( 𝑓 : 𝐴 ⟶ 𝐵 → 𝑓 Fn 𝐴 )
4		df-f	⊢ ( 𝑓 : 𝐴 ⟶ 𝐶 ↔ ( 𝑓 Fn 𝐴 ∧ ran 𝑓 ⊆ 𝐶 ) )
5	4	baibr	⊢ ( 𝑓 Fn 𝐴 → ( ran 𝑓 ⊆ 𝐶 ↔ 𝑓 : 𝐴 ⟶ 𝐶 ) )
6	3 5	syl	⊢ ( 𝑓 : 𝐴 ⟶ 𝐵 → ( ran 𝑓 ⊆ 𝐶 ↔ 𝑓 : 𝐴 ⟶ 𝐶 ) )
7	6	pm5.32i	⊢ ( ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ran 𝑓 ⊆ 𝐶 ) ↔ ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ 𝑓 : 𝐴 ⟶ 𝐶 ) )
8	2 1	elmap	⊢ ( 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) ↔ 𝑓 : 𝐴 ⟶ 𝐵 )
9	8	anbi1i	⊢ ( ( 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) ∧ ran 𝑓 ⊆ 𝐶 ) ↔ ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ran 𝑓 ⊆ 𝐶 ) )
10		fin	⊢ ( 𝑓 : 𝐴 ⟶ ( 𝐵 ∩ 𝐶 ) ↔ ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ 𝑓 : 𝐴 ⟶ 𝐶 ) )
11	7 9 10	3bitr4ri	⊢ ( 𝑓 : 𝐴 ⟶ ( 𝐵 ∩ 𝐶 ) ↔ ( 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) ∧ ran 𝑓 ⊆ 𝐶 ) )
12	11	abbii	⊢ { 𝑓 ∣ 𝑓 : 𝐴 ⟶ ( 𝐵 ∩ 𝐶 ) } = { 𝑓 ∣ ( 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) ∧ ran 𝑓 ⊆ 𝐶 ) }
13	2	inex1	⊢ ( 𝐵 ∩ 𝐶 ) ∈ V
14	13 1	mapval	⊢ ( ( 𝐵 ∩ 𝐶 ) ↑m 𝐴 ) = { 𝑓 ∣ 𝑓 : 𝐴 ⟶ ( 𝐵 ∩ 𝐶 ) }
15		df-rab	⊢ { 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) ∣ ran 𝑓 ⊆ 𝐶 } = { 𝑓 ∣ ( 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) ∧ ran 𝑓 ⊆ 𝐶 ) }
16	12 14 15	3eqtr4i	⊢ ( ( 𝐵 ∩ 𝐶 ) ↑m 𝐴 ) = { 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) ∣ ran 𝑓 ⊆ 𝐶 }