Metamath Proof Explorer


Theorem isof1oopb

Description: A function is a bijection iff it is an isomorphism regarding the universal class of ordered pairs as relations. (Contributed by AV, 9-May-2021)

Ref Expression
Assertion isof1oopb H : A 1-1 onto B H Isom V × V , V × V A B

Proof

Step Hyp Ref Expression
1 fvex H x V
2 fvex H y V
3 1 2 opelvv H x H y V × V
4 df-br H x V × V H y H x H y V × V
5 3 4 mpbir H x V × V H y
6 5 a1i x V × V y H x V × V H y
7 opelvvg x A y A x y V × V
8 df-br x V × V y x y V × V
9 7 8 sylibr x A y A x V × V y
10 9 a1d x A y A H x V × V H y x V × V y
11 6 10 impbid2 x A y A x V × V y H x V × V H y
12 11 adantl H : A 1-1 onto B x A y A x V × V y H x V × V H y
13 12 ralrimivva H : A 1-1 onto B x A y A x V × V y H x V × V H y
14 13 pm4.71i H : A 1-1 onto B H : A 1-1 onto B x A y A x V × V y H x V × V H y
15 df-isom H Isom V × V , V × V A B H : A 1-1 onto B x A y A x V × V y H x V × V H y
16 14 15 bitr4i H : A 1-1 onto B H Isom V × V , V × V A B