Metamath Proof Explorer


Theorem fncnv

Description: Single-rootedness (see funcnv ) of a class cut down by a Cartesian product. (Contributed by NM, 5-Mar-2007)

Ref Expression
Assertion fncnv
|- ( `' ( R i^i ( A X. B ) ) Fn B <-> A. y e. B E! x e. A x R y )

Proof

Step Hyp Ref Expression
1 df-fn
 |-  ( `' ( R i^i ( A X. B ) ) Fn B <-> ( Fun `' ( R i^i ( A X. B ) ) /\ dom `' ( R i^i ( A X. B ) ) = B ) )
2 df-rn
 |-  ran ( R i^i ( A X. B ) ) = dom `' ( R i^i ( A X. B ) )
3 2 eqeq1i
 |-  ( ran ( R i^i ( A X. B ) ) = B <-> dom `' ( R i^i ( A X. B ) ) = B )
4 3 anbi2i
 |-  ( ( Fun `' ( R i^i ( A X. B ) ) /\ ran ( R i^i ( A X. B ) ) = B ) <-> ( Fun `' ( R i^i ( A X. B ) ) /\ dom `' ( R i^i ( A X. B ) ) = B ) )
5 rninxp
 |-  ( ran ( R i^i ( A X. B ) ) = B <-> A. y e. B E. x e. A x R y )
6 5 anbi1i
 |-  ( ( ran ( R i^i ( A X. B ) ) = B /\ A. y e. B E* x e. A x R y ) <-> ( A. y e. B E. x e. A x R y /\ A. y e. B E* x e. A x R y ) )
7 funcnv
 |-  ( Fun `' ( R i^i ( A X. B ) ) <-> A. y e. ran ( R i^i ( A X. B ) ) E* x x ( R i^i ( A X. B ) ) y )
8 raleq
 |-  ( ran ( R i^i ( A X. B ) ) = B -> ( A. y e. ran ( R i^i ( A X. B ) ) E* x x ( R i^i ( A X. B ) ) y <-> A. y e. B E* x x ( R i^i ( A X. B ) ) y ) )
9 moanimv
 |-  ( E* x ( y e. B /\ ( x e. A /\ x R y ) ) <-> ( y e. B -> E* x ( x e. A /\ x R y ) ) )
10 brinxp2
 |-  ( x ( R i^i ( A X. B ) ) y <-> ( ( x e. A /\ y e. B ) /\ x R y ) )
11 an21
 |-  ( ( ( x e. A /\ y e. B ) /\ x R y ) <-> ( y e. B /\ ( x e. A /\ x R y ) ) )
12 10 11 bitri
 |-  ( x ( R i^i ( A X. B ) ) y <-> ( y e. B /\ ( x e. A /\ x R y ) ) )
13 12 mobii
 |-  ( E* x x ( R i^i ( A X. B ) ) y <-> E* x ( y e. B /\ ( x e. A /\ x R y ) ) )
14 df-rmo
 |-  ( E* x e. A x R y <-> E* x ( x e. A /\ x R y ) )
15 14 imbi2i
 |-  ( ( y e. B -> E* x e. A x R y ) <-> ( y e. B -> E* x ( x e. A /\ x R y ) ) )
16 9 13 15 3bitr4i
 |-  ( E* x x ( R i^i ( A X. B ) ) y <-> ( y e. B -> E* x e. A x R y ) )
17 biimt
 |-  ( y e. B -> ( E* x e. A x R y <-> ( y e. B -> E* x e. A x R y ) ) )
18 16 17 bitr4id
 |-  ( y e. B -> ( E* x x ( R i^i ( A X. B ) ) y <-> E* x e. A x R y ) )
19 18 ralbiia
 |-  ( A. y e. B E* x x ( R i^i ( A X. B ) ) y <-> A. y e. B E* x e. A x R y )
20 8 19 bitrdi
 |-  ( ran ( R i^i ( A X. B ) ) = B -> ( A. y e. ran ( R i^i ( A X. B ) ) E* x x ( R i^i ( A X. B ) ) y <-> A. y e. B E* x e. A x R y ) )
21 7 20 syl5bb
 |-  ( ran ( R i^i ( A X. B ) ) = B -> ( Fun `' ( R i^i ( A X. B ) ) <-> A. y e. B E* x e. A x R y ) )
22 21 pm5.32i
 |-  ( ( ran ( R i^i ( A X. B ) ) = B /\ Fun `' ( R i^i ( A X. B ) ) ) <-> ( ran ( R i^i ( A X. B ) ) = B /\ A. y e. B E* x e. A x R y ) )
23 r19.26
 |-  ( A. y e. B ( E. x e. A x R y /\ E* x e. A x R y ) <-> ( A. y e. B E. x e. A x R y /\ A. y e. B E* x e. A x R y ) )
24 6 22 23 3bitr4i
 |-  ( ( ran ( R i^i ( A X. B ) ) = B /\ Fun `' ( R i^i ( A X. B ) ) ) <-> A. y e. B ( E. x e. A x R y /\ E* x e. A x R y ) )
25 ancom
 |-  ( ( Fun `' ( R i^i ( A X. B ) ) /\ ran ( R i^i ( A X. B ) ) = B ) <-> ( ran ( R i^i ( A X. B ) ) = B /\ Fun `' ( R i^i ( A X. B ) ) ) )
26 reu5
 |-  ( E! x e. A x R y <-> ( E. x e. A x R y /\ E* x e. A x R y ) )
27 26 ralbii
 |-  ( A. y e. B E! x e. A x R y <-> A. y e. B ( E. x e. A x R y /\ E* x e. A x R y ) )
28 24 25 27 3bitr4i
 |-  ( ( Fun `' ( R i^i ( A X. B ) ) /\ ran ( R i^i ( A X. B ) ) = B ) <-> A. y e. B E! x e. A x R y )
29 1 4 28 3bitr2i
 |-  ( `' ( R i^i ( A X. B ) ) Fn B <-> A. y e. B E! x e. A x R y )