Metamath Proof Explorer

Theorem brdom3

Description: Equivalence to a dominance relation. (Contributed by NM, 27-Mar-2007)

Ref Expression
Hypothesis brdom3.2 
|- B e. _V
Assertion brdom3 
|- ( A ~<_ B <-> E. f ( A. x 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 reldom 
 |-  Rel ~<_
3 2 brrelex1i 
 |-  ( A ~<_ B -> A e. _V )
4 0sdomg 
 |-  ( A e. _V -> ( (/) ~< A <-> A =/= (/) ) )
5 3 4 syl 
 |-  ( A ~<_ B -> ( (/) ~< A <-> A =/= (/) ) )
6 df-ne 
 |-  ( A =/= (/) <-> -. A = (/) )
7 5 6 bitrdi 
 |-  ( A ~<_ B -> ( (/) ~< A <-> -. A = (/) ) )
8 7 biimpar 
 |-  ( ( A ~<_ B /\ -. A = (/) ) -> (/) ~< A )
9 fodomr 
 |-  ( ( (/) ~< A /\ A ~<_ B ) -> E. f f : B -onto-> A )
10 9 ancoms 
 |-  ( ( A ~<_ B /\ (/) ~< A ) -> E. f f : B -onto-> A )
11 8 10 syldan 
 |-  ( ( A ~<_ B /\ -. A = (/) ) -> E. f f : B -onto-> A )
12 pm5.6 
 |-  ( ( ( A ~<_ B /\ -. A = (/) ) -> E. f f : B -onto-> A ) <-> ( A ~<_ B -> ( A = (/) \/ E. f f : B -onto-> A ) ) )
13 11 12 mpbi 
 |-  ( A ~<_ B -> ( A = (/) \/ E. f f : B -onto-> A ) )
14 br0 
 |-  -. x (/) y
15 14 nex 
 |-  -. E. y x (/) y
16 exmo 
 |-  ( E. y x (/) y \/ E* y x (/) y )
17 15 16 mtpor 
 |-  E* y x (/) y
18 17 ax-gen 
 |-  A. x E* y x (/) y
19 rzal 
 |-  ( A = (/) -> A. x e. A E. y e. B y (/) x )
20 0ex 
 |-  (/) e. _V
21 breq 
 |-  ( f = (/) -> ( x f y <-> x (/) y ) )
22 21 mobidv 
 |-  ( f = (/) -> ( E* y x f y <-> E* y x (/) y ) )
23 22 albidv 
 |-  ( f = (/) -> ( A. x E* y x f y <-> A. x E* y x (/) y ) )
24 breq 
 |-  ( f = (/) -> ( y f x <-> y (/) x ) )
25 24 rexbidv 
 |-  ( f = (/) -> ( E. y e. B y f x <-> E. y e. B y (/) x ) )
26 25 ralbidv 
 |-  ( f = (/) -> ( A. x e. A E. y e. B y f x <-> A. x e. A E. y e. B y (/) x ) )
27 23 26 anbi12d 
 |-  ( f = (/) -> ( ( A. x E* y x f y /\ A. x e. A E. y e. B y f x ) <-> ( A. x E* y x (/) y /\ A. x e. A E. y e. B y (/) x ) ) )
28 20 27 spcev 
 |-  ( ( A. x E* y x (/) y /\ A. x e. A E. y e. B y (/) x ) -> E. f ( A. x E* y x f y /\ A. x e. A E. y e. B y f x ) )
29 18 19 28 sylancr 
 |-  ( A = (/) -> E. f ( A. x E* y x f y /\ A. x e. A E. y e. B y f x ) )
30 fofun 
 |-  ( f : B -onto-> A -> Fun f )
31 dffun6 
 |-  ( Fun f <-> ( Rel f /\ A. x E* y x f y ) )
32 31 simprbi 
 |-  ( Fun f -> A. x E* y x f y )
33 30 32 syl 
 |-  ( f : B -onto-> A -> A. x E* y x f y )
34 dffo4 
 |-  ( f : B -onto-> A <-> ( f : B --> A /\ A. x e. A E. y e. B y f x ) )
35 34 simprbi 
 |-  ( f : B -onto-> A -> A. x e. A E. y e. B y f x )
36 33 35 jca 
 |-  ( f : B -onto-> A -> ( A. x E* y x f y /\ A. x e. A E. y e. B y f x ) )
37 36 eximi 
 |-  ( E. f f : B -onto-> A -> E. f ( A. x E* y x f y /\ A. x e. A E. y e. B y f x ) )
38 29 37 jaoi 
 |-  ( ( A = (/) \/ E. f f : B -onto-> A ) -> E. f ( A. x E* y x f y /\ A. x e. A E. y e. B y f x ) )
39 13 38 syl 
 |-  ( A ~<_ B -> E. f ( A. x E* y x f y /\ A. x e. A E. y e. B y f x ) )
40 inss1 
 |-  ( f i^i ( B X. A ) ) C_ f
41 40 ssbri 
 |-  ( x ( f i^i ( B X. A ) ) y -> x f y )
42 41 moimi 
 |-  ( E* y x f y -> E* y x ( f i^i ( B X. A ) ) y )
43 42 alimi 
 |-  ( A. x E* y x f y -> A. x E* y x ( f i^i ( B X. A ) ) y )
44 relinxp 
 |-  Rel ( f i^i ( B X. A ) )
45 dffun6 
 |-  ( Fun ( f i^i ( B X. A ) ) <-> ( Rel ( f i^i ( B X. A ) ) /\ A. x E* y x ( f i^i ( B X. A ) ) y ) )
46 44 45 mpbiran 
 |-  ( Fun ( f i^i ( B X. A ) ) <-> A. x E* y x ( f i^i ( B X. A ) ) y )
47 43 46 sylibr 
 |-  ( A. x E* y x f y -> Fun ( f i^i ( B X. A ) ) )
48 47 funfnd 
 |-  ( A. x E* y x f y -> ( f i^i ( B X. A ) ) Fn dom ( f i^i ( B X. A ) ) )
49 rninxp 
 |-  ( ran ( f i^i ( B X. A ) ) = A <-> A. x e. A E. y e. B y f x )
50 49 biimpri 
 |-  ( A. x e. A E. y e. B y f x -> ran ( f i^i ( B X. A ) ) = A )
51 48 50 anim12i 
 |-  ( ( A. x 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 ) )
52 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 ) )
53 51 52 sylibr 
 |-  ( ( A. x 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 )
54 vex 
 |-  f e. _V
55 54 inex1 
 |-  ( f i^i ( B X. A ) ) e. _V
56 55 dmex 
 |-  dom ( f i^i ( B X. A ) ) e. _V
57 56 fodom 
 |-  ( ( f i^i ( B X. A ) ) : dom ( f i^i ( B X. A ) ) -onto-> A -> A ~<_ dom ( f i^i ( B X. A ) ) )
58 inss2 
 |-  ( f i^i ( B X. A ) ) C_ ( B X. A )
59 dmss 
 |-  ( ( f i^i ( B X. A ) ) C_ ( B X. A ) -> dom ( f i^i ( B X. A ) ) C_ dom ( B X. A ) )
60 58 59 ax-mp 
 |-  dom ( f i^i ( B X. A ) ) C_ dom ( B X. A )
61 dmxpss 
 |-  dom ( B X. A ) C_ B
62 60 61 sstri 
 |-  dom ( f i^i ( B X. A ) ) C_ B
63 ssdomg 
 |-  ( B e. _V -> ( dom ( f i^i ( B X. A ) ) C_ B -> dom ( f i^i ( B X. A ) ) ~<_ B ) )
64 1 62 63 mp2 
 |-  dom ( f i^i ( B X. A ) ) ~<_ B
65 domtr 
 |-  ( ( A ~<_ dom ( f i^i ( B X. A ) ) /\ dom ( f i^i ( B X. A ) ) ~<_ B ) -> A ~<_ B )
66 64 65 mpan2 
 |-  ( A ~<_ dom ( f i^i ( B X. A ) ) -> A ~<_ B )
67 53 57 66 3syl 
 |-  ( ( A. x E* y x f y /\ A. x e. A E. y e. B y f x ) -> A ~<_ B )
68 67 exlimiv 
 |-  ( E. f ( A. x E* y x f y /\ A. x e. A E. y e. B y f x ) -> A ~<_ B )
69 39 68 impbii 
 |-  ( A ~<_ B <-> E. f ( A. x E* y x f y /\ A. x e. A E. y e. B y f x ) )