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

Metamath Proof Explorer

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 fimacnv ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( ◡ 𝐹 “ 𝐵 ) = 𝐴 )
15 1 mptpreima ⊢ ( ◡ 𝐹 “ 𝐵 ) = { 𝑥 ∈ 𝐴 ∣ 𝐶 ∈ 𝐵 }
16 14 15 eqtr3di ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → 𝐴 = { 𝑥 ∈ 𝐴 ∣ 𝐶 ∈ 𝐵 } )
17 rabid2 ⊢ ( 𝐴 = { 𝑥 ∈ 𝐴 ∣ 𝐶 ∈ 𝐵 } ↔ ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 )
18 16 17 sylib ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 )
19 13 18 impbii ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ↔ 𝐹 : 𝐴 ⟶ 𝐵 )