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	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ⊆ 𝐴 ) → ( 𝐹 “ 𝑋 ) = { 𝑦 ∈ 𝐵 ∣ ∃ 𝑥 ∈ 𝑋 ( 𝐹 ‘ 𝑥 ) = 𝑦 } )