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

Metamath Proof Explorer

Theorem elpreima

Description: Membership in the preimage of a set under a function. (Contributed by Jeff Madsen, 2-Sep-2009)

Ref Expression
Assertion elpreima ( 𝐹 Fn 𝐴 → ( 𝐵 ∈ ( ◡ 𝐹 “ 𝐶 ) ↔ ( 𝐵 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝐵 ) ∈ 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 cnvimass ⊢ ( ◡ 𝐹 “ 𝐶 ) ⊆ dom 𝐹
2 1 sseli ⊢ ( 𝐵 ∈ ( ◡ 𝐹 “ 𝐶 ) → 𝐵 ∈ dom 𝐹 )
3 fndm ⊢ ( 𝐹 Fn 𝐴 → dom 𝐹 = 𝐴 )
4 3 eleq2d ⊢ ( 𝐹 Fn 𝐴 → ( 𝐵 ∈ dom 𝐹 ↔ 𝐵 ∈ 𝐴 ) )
5 2 4 imbitrid ⊢ ( 𝐹 Fn 𝐴 → ( 𝐵 ∈ ( ◡ 𝐹 “ 𝐶 ) → 𝐵 ∈ 𝐴 ) )
6 fnfun ⊢ ( 𝐹 Fn 𝐴 → Fun 𝐹 )
7 fvimacnvi ⊢ ( ( Fun 𝐹 ∧ 𝐵 ∈ ( ◡ 𝐹 “ 𝐶 ) ) → ( 𝐹 ‘ 𝐵 ) ∈ 𝐶 )
8 6 7 sylan ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ∈ ( ◡ 𝐹 “ 𝐶 ) ) → ( 𝐹 ‘ 𝐵 ) ∈ 𝐶 )
9 8 ex ⊢ ( 𝐹 Fn 𝐴 → ( 𝐵 ∈ ( ◡ 𝐹 “ 𝐶 ) → ( 𝐹 ‘ 𝐵 ) ∈ 𝐶 ) )
10 5 9 jcad ⊢ ( 𝐹 Fn 𝐴 → ( 𝐵 ∈ ( ◡ 𝐹 “ 𝐶 ) → ( 𝐵 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝐵 ) ∈ 𝐶 ) ) )
11 fvimacnv ⊢ ( ( Fun 𝐹 ∧ 𝐵 ∈ dom 𝐹 ) → ( ( 𝐹 ‘ 𝐵 ) ∈ 𝐶 ↔ 𝐵 ∈ ( ◡ 𝐹 “ 𝐶 ) ) )
12 11 funfni ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝐵 ) ∈ 𝐶 ↔ 𝐵 ∈ ( ◡ 𝐹 “ 𝐶 ) ) )
13 12 biimpd ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝐵 ) ∈ 𝐶 → 𝐵 ∈ ( ◡ 𝐹 “ 𝐶 ) ) )
14 13 expimpd ⊢ ( 𝐹 Fn 𝐴 → ( ( 𝐵 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝐵 ) ∈ 𝐶 ) → 𝐵 ∈ ( ◡ 𝐹 “ 𝐶 ) ) )
15 10 14 impbid ⊢ ( 𝐹 Fn 𝐴 → ( 𝐵 ∈ ( ◡ 𝐹 “ 𝐶 ) ↔ ( 𝐵 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝐵 ) ∈ 𝐶 ) ) )