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 ⊢ A ∈ V
brimage.2 ⊢ B ∈ V
Assertion brimage ⊢ A 𝖨𝗆𝖺𝗀𝖾 R B ↔ B = R A

Proof

Step Hyp Ref Expression
1 brimage.1 ⊢ A ∈ V
2 brimage.2 ⊢ B ∈ V
3 df-image ⊢ 𝖨𝗆𝖺𝗀𝖾 R = V × V ∖ ran ⁡ V ⊗ E ∆ E ∘ R -1 ⊗ V
4 brxp ⊢ A V × V B ↔ A ∈ V ∧ B ∈ V
5 1 2 4 mpbir2an ⊢ A V × V B
6 vex ⊢ x ∈ V
7 vex ⊢ y ∈ V
8 6 7 brcnv ⊢ x R -1 y ↔ y R x
9 8 rexbii ⊢ ∃ y ∈ A x R -1 y ↔ ∃ y ∈ A y R x
10 6 1 coep ⊢ x E ∘ R -1 A ↔ ∃ y ∈ A x R -1 y
11 6 elima ⊢ x ∈ R A ↔ ∃ y ∈ A y R x
12 9 10 11 3bitr4ri ⊢ x ∈ R A ↔ x E ∘ R -1 A
13 1 2 3 5 12 brtxpsd3 ⊢ A 𝖨𝗆𝖺𝗀𝖾 R B ↔ B = R A