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 ) )