Theorem fncnv 5962

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

Assertion

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

Distinct variable groups:   x, y, A   x, B, y   x, R, y

Proof of Theorem fncnv

Step	Hyp	Ref	Expression
1		df-fn 5891	. 2 |- ( `' ( 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 5125	. . . 4 |- ran ( R i^i ( A X. B ) ) = dom `' ( R i^i ( A X. B ) )
3	2	eqeq1i 2627	. . 3 |- ( ran ( R i^i ( A X. B ) ) = B <-> dom `' ( R i^i ( A X. B ) ) = B )
4	3	anbi2i 730	. 2 |- ( ( 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 5573	. . . . 5 |- ( ran ( R i^i ( A X. B ) ) = B <-> A. y e. B E. x e. A x R y )
6	5	anbi1i 731	. . . 4 |- ( ( 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 5958	. . . . . 6 |- ( 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 3138	. . . . . . 7 |- ( 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		biimt 350	. . . . . . . . 9 |- ( y e. B -> ( E* x e. A x R y <-> ( y e. B -> E* x e. A x R y ) ) )
10		moanimv 2531	. . . . . . . . . 10 |- ( E* x ( y e. B /\ ( x e. A /\ x R y ) ) <-> ( y e. B -> E* x ( x e. A /\ x R y ) ) )
11		brinxp2 5180	. . . . . . . . . . . 12 |- ( x ( R i^i ( A X. B ) ) y <-> ( x e. A /\ y e. B /\ x R y ) )
12		3anan12 1051	. . . . . . . . . . . 12 |- ( ( x e. A /\ y e. B /\ x R y ) <-> ( y e. B /\ ( x e. A /\ x R y ) ) )
13	11, 12	bitri 264	. . . . . . . . . . 11 |- ( x ( R i^i ( A X. B ) ) y <-> ( y e. B /\ ( x e. A /\ x R y ) ) )
14	13	mobii 2493	. . . . . . . . . 10 |- ( E* x x ( R i^i ( A X. B ) ) y <-> E* x ( y e. B /\ ( x e. A /\ x R y ) ) )
15		df-rmo 2920	. . . . . . . . . . 11 |- ( E* x e. A x R y <-> E* x ( x e. A /\ x R y ) )
16	15	imbi2i 326	. . . . . . . . . 10 |- ( ( y e. B -> E* x e. A x R y ) <-> ( y e. B -> E* x ( x e. A /\ x R y ) ) )
17	10, 14, 16	3bitr4i 292	. . . . . . . . 9 |- ( E* x x ( R i^i ( A X. B ) ) y <-> ( y e. B -> E* x e. A x R y ) )
18	9, 17	syl6rbbr 279	. . . . . . . 8 |- ( y e. B -> ( E* x x ( R i^i ( A X. B ) ) y <-> E* x e. A x R y ) )
19	18	ralbiia 2979	. . . . . . 7 |- ( 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	syl6bb 276	. . . . . 6 |- ( 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 272	. . . . 5 |- ( 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 669	. . . 4 |- ( ( 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 3064	. . . 4 |- ( 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 292	. . 3 |- ( ( 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 466	. . 3 |- ( ( 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 3159	. . . 4 |- ( E! x e. A x R y <-> ( E. x e. A x R y /\ E* x e. A x R y ) )
27	26	ralbii 2980	. . 3 |- ( 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 292	. 2 |- ( ( 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 288	1 |- ( `' ( R i^i ( A X. B ) ) Fn B <-> A. y e. B E! x e. A x R y )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   /\ w3a 1037   = wceq 1483   e. wcel 1990   E*wmo 2471   A.wral 2912   E.wrex 2913   E!wreu 2914   E*wrmo 2915   i^i cin 3573   class class class wbr 4653   X. cxp 5112   `'ccnv 5113   dom cdm 5114   ran crn 5115   Fun wfun 5882   Fn wfn 5883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pr 4906

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-br 4654  df-opab 4713  df-id 5024  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-fun 5890  df-fn 5891

This theorem is referenced by: (None)