Theorem brdom5

Description: An equivalence to a dominance relation. (Contributed by NM, 29-Mar-2007)

	Ref	Expression
Hypothesis	brdom3.2	|- B e. _V
Assertion	brdom5	|- ( A ~<_ B <-> E. f ( A. x e. B E* y x f y /\ A. x e. A E. y e. B y f x ) )

Proof

Step	Hyp	Ref	Expression
1		brdom3.2	|- B e. _V
2	1	brdom3	|- ( A ~<_ B <-> E. f ( A. x E* y x f y /\ A. x e. A E. y e. B y f x ) )
3		alral	|- ( A. x E* y x f y -> A. x e. B E* y x f y )
4	3	anim1i	|- ( ( A. x E* y x f y /\ A. x e. A E. y e. B y f x ) -> ( A. x e. B E* y x f y /\ A. x e. A E. y e. B y f x ) )
5	4	eximi	|- ( E. f ( A. x E* y x f y /\ A. x e. A E. y e. B y f x ) -> E. f ( A. x e. B E* y x f y /\ A. x e. A E. y e. B y f x ) )
6	2 5	sylbi	|- ( A ~<_ B -> E. f ( A. x e. B E* y x f y /\ A. x e. A E. y e. B y f x ) )
7		inss2	|- ( f i^i ( B X. A ) ) C_ ( B X. A )
8		dmss	|- ( ( f i^i ( B X. A ) ) C_ ( B X. A ) -> dom ( f i^i ( B X. A ) ) C_ dom ( B X. A ) )
9	7 8	ax-mp	|- dom ( f i^i ( B X. A ) ) C_ dom ( B X. A )
10		dmxpss	|- dom ( B X. A ) C_ B
11	9 10	sstri	|- dom ( f i^i ( B X. A ) ) C_ B
12	11	sseli	|- ( x e. dom ( f i^i ( B X. A ) ) -> x e. B )
13		inss1	|- ( f i^i ( B X. A ) ) C_ f
14	13	ssbri	|- ( x ( f i^i ( B X. A ) ) y -> x f y )
15	14	moimi	|- ( E* y x f y -> E* y x ( f i^i ( B X. A ) ) y )
16	12 15	imim12i	|- ( ( x e. B -> E* y x f y ) -> ( x e. dom ( f i^i ( B X. A ) ) -> E* y x ( f i^i ( B X. A ) ) y ) )
17	16	ralimi2	|- ( A. x e. B E* y x f y -> A. x e. dom ( f i^i ( B X. A ) ) E* y x ( f i^i ( B X. A ) ) y )
18		relinxp	|- Rel ( f i^i ( B X. A ) )
19	17 18	jctil	|- ( A. x e. B E* y x f y -> ( Rel ( f i^i ( B X. A ) ) /\ A. x e. dom ( f i^i ( B X. A ) ) E* y x ( f i^i ( B X. A ) ) y ) )
20		dffun7	|- ( Fun ( f i^i ( B X. A ) ) <-> ( Rel ( f i^i ( B X. A ) ) /\ A. x e. dom ( f i^i ( B X. A ) ) E* y x ( f i^i ( B X. A ) ) y ) )
21	19 20	sylibr	|- ( A. x e. B E* y x f y -> Fun ( f i^i ( B X. A ) ) )
22	21	funfnd	|- ( A. x e. B E* y x f y -> ( f i^i ( B X. A ) ) Fn dom ( f i^i ( B X. A ) ) )
23		rninxp	|- ( ran ( f i^i ( B X. A ) ) = A <-> A. x e. A E. y e. B y f x )
24	23	biimpri	|- ( A. x e. A E. y e. B y f x -> ran ( f i^i ( B X. A ) ) = A )
25	22 24	anim12i	|- ( ( A. x e. B E* y x f y /\ A. x e. A E. y e. B y f x ) -> ( ( f i^i ( B X. A ) ) Fn dom ( f i^i ( B X. A ) ) /\ ran ( f i^i ( B X. A ) ) = A ) )
26		df-fo	|- ( ( f i^i ( B X. A ) ) : dom ( f i^i ( B X. A ) ) -onto-> A <-> ( ( f i^i ( B X. A ) ) Fn dom ( f i^i ( B X. A ) ) /\ ran ( f i^i ( B X. A ) ) = A ) )
27	25 26	sylibr	|- ( ( A. x e. B E* y x f y /\ A. x e. A E. y e. B y f x ) -> ( f i^i ( B X. A ) ) : dom ( f i^i ( B X. A ) ) -onto-> A )
28		vex	|- f e. _V
29	28	inex1	|- ( f i^i ( B X. A ) ) e. _V
30	29	dmex	|- dom ( f i^i ( B X. A ) ) e. _V
31	30	fodom	|- ( ( f i^i ( B X. A ) ) : dom ( f i^i ( B X. A ) ) -onto-> A -> A ~<_ dom ( f i^i ( B X. A ) ) )
32		ssdomg	|- ( B e. _V -> ( dom ( f i^i ( B X. A ) ) C_ B -> dom ( f i^i ( B X. A ) ) ~<_ B ) )
33	1 11 32	mp2	|- dom ( f i^i ( B X. A ) ) ~<_ B
34		domtr	|- ( ( A ~<_ dom ( f i^i ( B X. A ) ) /\ dom ( f i^i ( B X. A ) ) ~<_ B ) -> A ~<_ B )
35	33 34	mpan2	|- ( A ~<_ dom ( f i^i ( B X. A ) ) -> A ~<_ B )
36	27 31 35	3syl	|- ( ( A. x e. B E* y x f y /\ A. x e. A E. y e. B y f x ) -> A ~<_ B )
37	36	exlimiv	|- ( E. f ( A. x e. B E* y x f y /\ A. x e. A E. y e. B y f x ) -> A ~<_ B )
38	6 37	impbii	|- ( A ~<_ B <-> E. f ( A. x e. B E* y x f y /\ A. x e. A E. y e. B y f x ) )