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 -1 -1 : dom ⁡ A ⟶ 1-1 V ↔ Fun ⁡ A -1 ∧ Fun ⁡ A -1 -1

Proof

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