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 ( ( 𝐹 : 𝐴𝐵𝑋𝐴 ) → ( 𝐹𝑋 ) = { 𝑦𝐵 ∣ ∃ 𝑥𝑋 ( 𝐹𝑥 ) = 𝑦 } )