This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝑓 ⊆ 𝐶 }