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 
|- ( `' `' A : dom A -1-1-> _V <-> ( Fun `' A /\ Fun `' `' A ) )

Proof

Step Hyp Ref Expression
1 df-f1 
 |-  ( `' `' A : dom A -1-1-> _V <-> ( `' `' A : dom A --> _V /\ Fun `' `' `' A ) )
2 dffn2 
 |-  ( `' `' A Fn dom A <-> `' `' A : dom A --> _V )
3 dmcnvcnv 
 |-  dom `' `' A = dom A
4 df-fn 
 |-  ( `' `' A Fn dom A <-> ( Fun `' `' A /\ dom `' `' A = dom A ) )
5 3 4 mpbiran2 
 |-  ( `' `' A Fn dom A <-> Fun `' `' A )
6 2 5 bitr3i 
 |-  ( `' `' A : dom A --> _V <-> Fun `' `' A )
7 relcnv 
 |-  Rel `' A
8 dfrel2 
 |-  ( Rel `' A <-> `' `' `' A = `' A )
9 7 8 mpbi 
 |-  `' `' `' A = `' A
10 9 funeqi 
 |-  ( Fun `' `' `' A <-> Fun `' A )
11 6 10 anbi12ci 
 |-  ( ( `' `' A : dom A --> _V /\ Fun `' `' `' A ) <-> ( Fun `' A /\ Fun `' `' A ) )
12 1 11 bitri 
 |-  ( `' `' A : dom A -1-1-> _V <-> ( Fun `' A /\ Fun `' `' A ) )