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

Metamath Proof Explorer

Theorem fimarab

Description: Expressing the image of a set as a restricted abstract builder. (Contributed by Thierry Arnoux, 27-Jan-2020)

Ref Expression
Assertion fimarab ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ⊆ 𝐴 ) → ( 𝐹 “ 𝑋 ) = { 𝑦 ∈ 𝐵 ∣ ∃ 𝑥 ∈ 𝑋 ( 𝐹 ‘ 𝑥 ) = 𝑦 } )

Proof

Step Hyp Ref Expression
1 nfv ⊢ Ⅎ 𝑦 ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ⊆ 𝐴 )
2 nfcv ⊢ Ⅎ 𝑦 ( 𝐹 “ 𝑋 )
3 nfrab1 ⊢ Ⅎ 𝑦 { 𝑦 ∈ 𝐵 ∣ ∃ 𝑥 ∈ 𝑋 ( 𝐹 ‘ 𝑥 ) = 𝑦 }
4 ffn ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → 𝐹 Fn 𝐴 )
5 fvelimab ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ⊆ 𝐴 ) → ( 𝑦 ∈ ( 𝐹 “ 𝑋 ) ↔ ∃ 𝑥 ∈ 𝑋 ( 𝐹 ‘ 𝑥 ) = 𝑦 ) )
6 5 anbi2d ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ⊆ 𝐴 ) → ( ( 𝑦 ∈ 𝐵 ∧ 𝑦 ∈ ( 𝐹 “ 𝑋 ) ) ↔ ( 𝑦 ∈ 𝐵 ∧ ∃ 𝑥 ∈ 𝑋 ( 𝐹 ‘ 𝑥 ) = 𝑦 ) ) )
7 4 6 sylan ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ⊆ 𝐴 ) → ( ( 𝑦 ∈ 𝐵 ∧ 𝑦 ∈ ( 𝐹 “ 𝑋 ) ) ↔ ( 𝑦 ∈ 𝐵 ∧ ∃ 𝑥 ∈ 𝑋 ( 𝐹 ‘ 𝑥 ) = 𝑦 ) ) )
8 fimass ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( 𝐹 “ 𝑋 ) ⊆ 𝐵 )
9 8 adantr ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ⊆ 𝐴 ) → ( 𝐹 “ 𝑋 ) ⊆ 𝐵 )
10 9 sseld ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ⊆ 𝐴 ) → ( 𝑦 ∈ ( 𝐹 “ 𝑋 ) → 𝑦 ∈ 𝐵 ) )
11 10 pm4.71rd ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ⊆ 𝐴 ) → ( 𝑦 ∈ ( 𝐹 “ 𝑋 ) ↔ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ∈ ( 𝐹 “ 𝑋 ) ) ) )
12 rabid ⊢ ( 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ ∃ 𝑥 ∈ 𝑋 ( 𝐹 ‘ 𝑥 ) = 𝑦 } ↔ ( 𝑦 ∈ 𝐵 ∧ ∃ 𝑥 ∈ 𝑋 ( 𝐹 ‘ 𝑥 ) = 𝑦 ) )
13 12 a1i ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ⊆ 𝐴 ) → ( 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ ∃ 𝑥 ∈ 𝑋 ( 𝐹 ‘ 𝑥 ) = 𝑦 } ↔ ( 𝑦 ∈ 𝐵 ∧ ∃ 𝑥 ∈ 𝑋 ( 𝐹 ‘ 𝑥 ) = 𝑦 ) ) )
14 7 11 13 3bitr4d ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ⊆ 𝐴 ) → ( 𝑦 ∈ ( 𝐹 “ 𝑋 ) ↔ 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ ∃ 𝑥 ∈ 𝑋 ( 𝐹 ‘ 𝑥 ) = 𝑦 } ) )
15 1 2 3 14 eqrd ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ⊆ 𝐴 ) → ( 𝐹 “ 𝑋 ) = { 𝑦 ∈ 𝐵 ∣ ∃ 𝑥 ∈ 𝑋 ( 𝐹 ‘ 𝑥 ) = 𝑦 } )