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

Metamath Proof Explorer

Theorem brimage

Description: Binary relation form of the Image functor. (Contributed by Scott Fenton, 4-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Hypotheses brimage.1 ⊢ 𝐴 ∈ V
brimage.2 ⊢ 𝐵 ∈ V
Assertion brimage ( 𝐴 Image 𝑅 𝐵 ↔ 𝐵 = ( 𝑅 “ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 brimage.1 ⊢ 𝐴 ∈ V
2 brimage.2 ⊢ 𝐵 ∈ V
3 df-image ⊢ Image 𝑅 = ( ( V × V ) ∖ ran ( ( V ⊗ E ) △ ( ( E ∘ ◡ 𝑅 ) ⊗ V ) ) )
4 brxp ⊢ ( 𝐴 ( V × V ) 𝐵 ↔ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )
5 1 2 4 mpbir2an ⊢ 𝐴 ( V × V ) 𝐵
6 vex ⊢ 𝑥 ∈ V
7 vex ⊢ 𝑦 ∈ V
8 6 7 brcnv ⊢ ( 𝑥 ◡ 𝑅 𝑦 ↔ 𝑦 𝑅 𝑥 )
9 8 rexbii ⊢ ( ∃ 𝑦 ∈ 𝐴 𝑥 ◡ 𝑅 𝑦 ↔ ∃ 𝑦 ∈ 𝐴 𝑦 𝑅 𝑥 )
10 6 1 coep ⊢ ( 𝑥 ( E ∘ ◡ 𝑅 ) 𝐴 ↔ ∃ 𝑦 ∈ 𝐴 𝑥 ◡ 𝑅 𝑦 )
11 6 elima ⊢ ( 𝑥 ∈ ( 𝑅 “ 𝐴 ) ↔ ∃ 𝑦 ∈ 𝐴 𝑦 𝑅 𝑥 )
12 9 10 11 3bitr4ri ⊢ ( 𝑥 ∈ ( 𝑅 “ 𝐴 ) ↔ 𝑥 ( E ∘ ◡ 𝑅 ) 𝐴 )
13 1 2 3 5 12 brtxpsd3 ⊢ ( 𝐴 Image 𝑅 𝐵 ↔ 𝐵 = ( 𝑅 “ 𝐴 ) )