Theorem fmpt

Description: Functionality of the mapping operation. (Contributed by Mario Carneiro, 26-Jul-2013) (Revised by Mario Carneiro, 31-Aug-2015)

	Ref	Expression
Hypothesis	fmpt.1	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐶 )
Assertion	fmpt	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ↔ 𝐹 : 𝐴 ⟶ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		fmpt.1	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐶 )
2	1	fnmpt	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → 𝐹 Fn 𝐴 )
3	1	rnmpt	⊢ ran 𝐹 = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐶 }
4		r19.29	⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐶 ) → ∃ 𝑥 ∈ 𝐴 ( 𝐶 ∈ 𝐵 ∧ 𝑦 = 𝐶 ) )
5		eleq1	⊢ ( 𝑦 = 𝐶 → ( 𝑦 ∈ 𝐵 ↔ 𝐶 ∈ 𝐵 ) )
6	5	biimparc	⊢ ( ( 𝐶 ∈ 𝐵 ∧ 𝑦 = 𝐶 ) → 𝑦 ∈ 𝐵 )
7	6	rexlimivw	⊢ ( ∃ 𝑥 ∈ 𝐴 ( 𝐶 ∈ 𝐵 ∧ 𝑦 = 𝐶 ) → 𝑦 ∈ 𝐵 )
8	4 7	syl	⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐶 ) → 𝑦 ∈ 𝐵 )
9	8	ex	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → ( ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐶 → 𝑦 ∈ 𝐵 ) )
10	9	abssdv	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐶 } ⊆ 𝐵 )
11	3 10	eqsstrid	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → ran 𝐹 ⊆ 𝐵 )
12		df-f	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 ↔ ( 𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵 ) )
13	2 11 12	sylanbrc	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → 𝐹 : 𝐴 ⟶ 𝐵 )
14	1	mptpreima	⊢ ( ◡ 𝐹 “ 𝐵 ) = { 𝑥 ∈ 𝐴 ∣ 𝐶 ∈ 𝐵 }
15		fimacnv	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( ◡ 𝐹 “ 𝐵 ) = 𝐴 )
16	14 15	syl5reqr	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → 𝐴 = { 𝑥 ∈ 𝐴 ∣ 𝐶 ∈ 𝐵 } )
17		rabid2	⊢ ( 𝐴 = { 𝑥 ∈ 𝐴 ∣ 𝐶 ∈ 𝐵 } ↔ ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 )
18	16 17	sylib	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 )
19	13 18	impbii	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ↔ 𝐹 : 𝐴 ⟶ 𝐵 )