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

Metamath Proof Explorer

Theorem f1cnvcnv

Description: Two ways to express that a set A (not necessarily a function) is one-to-one. Each side is equivalent to Definition 6.4(3) of TakeutiZaring p. 24, who use the notation "Un_2 (A)" for one-to-one. We do not introduce a separate notation since we rarely use it. (Contributed by NM, 13-Aug-2004)

Ref Expression
Assertion f1cnvcnv ( ◡ ◡ 𝐴 : dom 𝐴 –1-1→ V ↔ ( Fun ◡ 𝐴 ∧ Fun ◡ ◡ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 df-f1 ⊢ ( ◡ ◡ 𝐴 : dom 𝐴 –1-1→ V ↔ ( ◡ ◡ 𝐴 : dom 𝐴 ⟶ V ∧ Fun ◡ ◡ ◡ 𝐴 ) )
2 dffn2 ⊢ ( ◡ ◡ 𝐴 Fn dom 𝐴 ↔ ◡ ◡ 𝐴 : dom 𝐴 ⟶ V )
3 dmcnvcnv ⊢ dom ◡ ◡ 𝐴 = dom 𝐴
4 df-fn ⊢ ( ◡ ◡ 𝐴 Fn dom 𝐴 ↔ ( Fun ◡ ◡ 𝐴 ∧ dom ◡ ◡ 𝐴 = dom 𝐴 ) )
5 3 4 mpbiran2 ⊢ ( ◡ ◡ 𝐴 Fn dom 𝐴 ↔ Fun ◡ ◡ 𝐴 )
6 2 5 bitr3i ⊢ ( ◡ ◡ 𝐴 : dom 𝐴 ⟶ V ↔ Fun ◡ ◡ 𝐴 )
7 relcnv ⊢ Rel ◡ 𝐴
8 dfrel2 ⊢ ( Rel ◡ 𝐴 ↔ ◡ ◡ ◡ 𝐴 = ◡ 𝐴 )
9 7 8 mpbi ⊢ ◡ ◡ ◡ 𝐴 = ◡ 𝐴
10 9 funeqi ⊢ ( Fun ◡ ◡ ◡ 𝐴 ↔ Fun ◡ 𝐴 )
11 6 10 anbi12ci ⊢ ( ( ◡ ◡ 𝐴 : dom 𝐴 ⟶ V ∧ Fun ◡ ◡ ◡ 𝐴 ) ↔ ( Fun ◡ 𝐴 ∧ Fun ◡ ◡ 𝐴 ) )
12 1 11 bitri ⊢ ( ◡ ◡ 𝐴 : dom 𝐴 –1-1→ V ↔ ( Fun ◡ 𝐴 ∧ Fun ◡ ◡ 𝐴 ) )