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 )