Theorem k0004lem2

Description: A mapping with a particular restricted range is also a mapping to that range. (Contributed by RP, 1-Apr-2021)

	Ref	Expression
Assertion	k0004lem2	⊢ ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝐵 ) → ( ( 𝐹 ∈ ( 𝐵 ↑m 𝐴 ) ∧ ( 𝐹 “ 𝐴 ) ⊆ 𝐶 ) ↔ 𝐹 ∈ ( 𝐶 ↑m 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		simp3	⊢ ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝐵 ) → 𝐶 ⊆ 𝐵 )
2		sseqin2	⊢ ( 𝐶 ⊆ 𝐵 ↔ ( 𝐵 ∩ 𝐶 ) = 𝐶 )
3	2	biimpi	⊢ ( 𝐶 ⊆ 𝐵 → ( 𝐵 ∩ 𝐶 ) = 𝐶 )
4	3	eqcomd	⊢ ( 𝐶 ⊆ 𝐵 → 𝐶 = ( 𝐵 ∩ 𝐶 ) )
5		k0004lem1	⊢ ( 𝐶 = ( 𝐵 ∩ 𝐶 ) → ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ( 𝐹 “ 𝐴 ) ⊆ 𝐶 ) ↔ 𝐹 : 𝐴 ⟶ 𝐶 ) )
6	1 4 5	3syl	⊢ ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝐵 ) → ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ( 𝐹 “ 𝐴 ) ⊆ 𝐶 ) ↔ 𝐹 : 𝐴 ⟶ 𝐶 ) )
7		simp2	⊢ ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝐵 ) → 𝐵 ∈ 𝑉 )
8		simp1	⊢ ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝐵 ) → 𝐴 ∈ 𝑈 )
9	7 8	elmapd	⊢ ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝐵 ) → ( 𝐹 ∈ ( 𝐵 ↑m 𝐴 ) ↔ 𝐹 : 𝐴 ⟶ 𝐵 ) )
10	9	anbi1d	⊢ ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝐵 ) → ( ( 𝐹 ∈ ( 𝐵 ↑m 𝐴 ) ∧ ( 𝐹 “ 𝐴 ) ⊆ 𝐶 ) ↔ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ( 𝐹 “ 𝐴 ) ⊆ 𝐶 ) ) )
11	7 1	ssexd	⊢ ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝐵 ) → 𝐶 ∈ V )
12	11 8	elmapd	⊢ ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝐵 ) → ( 𝐹 ∈ ( 𝐶 ↑m 𝐴 ) ↔ 𝐹 : 𝐴 ⟶ 𝐶 ) )
13	6 10 12	3bitr4d	⊢ ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ⊆ 𝐵 ) → ( ( 𝐹 ∈ ( 𝐵 ↑m 𝐴 ) ∧ ( 𝐹 “ 𝐴 ) ⊆ 𝐶 ) ↔ 𝐹 ∈ ( 𝐶 ↑m 𝐴 ) ) )