Theorem f1mptrn

Description: Express injection for a mapping operation. (Contributed by Thierry Arnoux, 3-May-2020)

	Ref	Expression
Hypotheses	f1mptrn.1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝐶 )
	f1mptrn.2	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐶 ) → ∃! 𝑥 ∈ 𝐴 𝑦 = 𝐵 )
Assertion	f1mptrn	⊢ ( 𝜑 → Fun ◡ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		f1mptrn.1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝐶 )
2		f1mptrn.2	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐶 ) → ∃! 𝑥 ∈ 𝐴 𝑦 = 𝐵 )
3	1	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 )
4	2	ralrimiva	⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝐶 ∃! 𝑥 ∈ 𝐴 𝑦 = 𝐵 )
5		eqid	⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
6	5	f1ompt	⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 –1-1-onto→ 𝐶 ↔ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 ∧ ∀ 𝑦 ∈ 𝐶 ∃! 𝑥 ∈ 𝐴 𝑦 = 𝐵 ) )
7		dff1o2	⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 –1-1-onto→ 𝐶 ↔ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) Fn 𝐴 ∧ Fun ◡ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∧ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = 𝐶 ) )
8	7	simp2bi	⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 –1-1-onto→ 𝐶 → Fun ◡ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
9	6 8	sylbir	⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 ∧ ∀ 𝑦 ∈ 𝐶 ∃! 𝑥 ∈ 𝐴 𝑦 = 𝐵 ) → Fun ◡ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
10	3 4 9	syl2anc	⊢ ( 𝜑 → Fun ◡ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )