Metamath Proof Explorer

Theorem nvof1ob

Description: A class equal to its converse is a function on a class if and only if it is a bijection from that class onto itself (the reverse implication holds without the hypothesis, see f1ofn ). (Contributed by BJ, 8-Nov-2026) Can shorten nvof1o using biimpac .

Ref Expression
Assertion nvof1ob ⊢ F -1 = F → F Fn A ↔ F : A ⟶ 1-1 onto A

Proof

Step Hyp Ref Expression
1 dff1o4 ⊢ F : A ⟶ 1-1 onto A ↔ F Fn A ∧ F -1 Fn A
2 fneq1 ⊢ F -1 = F → F -1 Fn A ↔ F Fn A
3 2 anbi2d ⊢ F -1 = F → F Fn A ∧ F -1 Fn A ↔ F Fn A ∧ F Fn A
4 1 3 bitrid ⊢ F -1 = F → F : A ⟶ 1-1 onto A ↔ F Fn A ∧ F Fn A
5 anidm ⊢ F Fn A ∧ F Fn A ↔ F Fn A
6 4 5 bitr2di ⊢ F -1 = F → F Fn A ↔ F : A ⟶ 1-1 onto A