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

Metamath Proof Explorer

Theorem dfimafnf

Description: Alternate definition of the image of a function. (Contributed by Raph Levien, 20-Nov-2006) (Revised by Thierry Arnoux, 24-Apr-2017)

Ref Expression
Hypotheses dfimafnf.1 ⊢ Ⅎ 𝑥 𝐴
dfimafnf.2 ⊢ Ⅎ 𝑥 𝐹
Assertion dfimafnf ( ( Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹 ) → ( 𝐹 “ 𝐴 ) = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑥 ) } )

Proof

Step Hyp Ref Expression
1 dfimafnf.1 ⊢ Ⅎ 𝑥 𝐴
2 dfimafnf.2 ⊢ Ⅎ 𝑥 𝐹
3 dfima2 ⊢ ( 𝐹 “ 𝐴 ) = { 𝑦 ∣ ∃ 𝑧 ∈ 𝐴 𝑧 𝐹 𝑦 }
4 ssel ⊢ ( 𝐴 ⊆ dom 𝐹 → ( 𝑧 ∈ 𝐴 → 𝑧 ∈ dom 𝐹 ) )
5 eqcom ⊢ ( ( 𝐹 ‘ 𝑧 ) = 𝑦 ↔ 𝑦 = ( 𝐹 ‘ 𝑧 ) )
6 funbrfvb ⊢ ( ( Fun 𝐹 ∧ 𝑧 ∈ dom 𝐹 ) → ( ( 𝐹 ‘ 𝑧 ) = 𝑦 ↔ 𝑧 𝐹 𝑦 ) )
7 5 6 bitr3id ⊢ ( ( Fun 𝐹 ∧ 𝑧 ∈ dom 𝐹 ) → ( 𝑦 = ( 𝐹 ‘ 𝑧 ) ↔ 𝑧 𝐹 𝑦 ) )
8 7 ex ⊢ ( Fun 𝐹 → ( 𝑧 ∈ dom 𝐹 → ( 𝑦 = ( 𝐹 ‘ 𝑧 ) ↔ 𝑧 𝐹 𝑦 ) ) )
9 4 8 syl9r ⊢ ( Fun 𝐹 → ( 𝐴 ⊆ dom 𝐹 → ( 𝑧 ∈ 𝐴 → ( 𝑦 = ( 𝐹 ‘ 𝑧 ) ↔ 𝑧 𝐹 𝑦 ) ) ) )
10 9 imp31 ⊢ ( ( ( Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹 ) ∧ 𝑧 ∈ 𝐴 ) → ( 𝑦 = ( 𝐹 ‘ 𝑧 ) ↔ 𝑧 𝐹 𝑦 ) )
11 10 rexbidva ⊢ ( ( Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹 ) → ( ∃ 𝑧 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑧 ) ↔ ∃ 𝑧 ∈ 𝐴 𝑧 𝐹 𝑦 ) )
12 11 abbidv ⊢ ( ( Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹 ) → { 𝑦 ∣ ∃ 𝑧 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑧 ) } = { 𝑦 ∣ ∃ 𝑧 ∈ 𝐴 𝑧 𝐹 𝑦 } )
13 3 12 eqtr4id ⊢ ( ( Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹 ) → ( 𝐹 “ 𝐴 ) = { 𝑦 ∣ ∃ 𝑧 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑧 ) } )
14 nfcv ⊢ Ⅎ 𝑧 𝐴
15 nfcv ⊢ Ⅎ 𝑥 𝑧
16 2 15 nffv ⊢ Ⅎ 𝑥 ( 𝐹 ‘ 𝑧 )
17 16 nfeq2 ⊢ Ⅎ 𝑥 𝑦 = ( 𝐹 ‘ 𝑧 )
18 nfv ⊢ Ⅎ 𝑧 𝑦 = ( 𝐹 ‘ 𝑥 )
19 fveq2 ⊢ ( 𝑧 = 𝑥 → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑥 ) )
20 19 eqeq2d ⊢ ( 𝑧 = 𝑥 → ( 𝑦 = ( 𝐹 ‘ 𝑧 ) ↔ 𝑦 = ( 𝐹 ‘ 𝑥 ) ) )
21 14 1 17 18 20 cbvrexfw ⊢ ( ∃ 𝑧 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑧 ) ↔ ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑥 ) )
22 21 abbii ⊢ { 𝑦 ∣ ∃ 𝑧 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑧 ) } = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑥 ) }
23 13 22 eqtrdi ⊢ ( ( Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹 ) → ( 𝐹 “ 𝐴 ) = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑥 ) } )