Metamath Proof Explorer

Theorem brdom4

Description: An equivalence to a dominance relation. (Contributed by NM, 28-Mar-2007) (Revised by NM, 16-Jun-2017)

Ref Expression
Hypothesis brdom3.2 
|- B e. _V
Assertion brdom4 
|- ( A ~<_ B <-> E. f ( A. x e. B E* y e. A 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 mormo 
 |-  ( E* y x f y -> E* y e. A x f y )
4 3 alimi 
 |-  ( A. x E* y x f y -> A. x E* y e. A x f y )
5 alral 
 |-  ( A. x E* y e. A x f y -> A. x e. B E* y e. A x f y )
6 4 5 syl 
 |-  ( A. x E* y x f y -> A. x e. B E* y e. A x f y )
7 6 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 e. A x f y /\ A. x e. A E. y e. B y f x ) )
8 7 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 e. A x f y /\ A. x e. A E. y e. B y f x ) )
9 2 8 sylbi 
 |-  ( A ~<_ B -> E. f ( A. x e. B E* y e. A x f y /\ A. x e. A E. y e. B y f x ) )
10 inss2 
 |-  ( f i^i ( B X. A ) ) C_ ( B X. A )
11 dmss 
 |-  ( ( f i^i ( B X. A ) ) C_ ( B X. A ) -> dom ( f i^i ( B X. A ) ) C_ dom ( B X. A ) )
12 10 11 ax-mp 
 |-  dom ( f i^i ( B X. A ) ) C_ dom ( B X. A )
13 dmxpss 
 |-  dom ( B X. A ) C_ B
14 12 13 sstri 
 |-  dom ( f i^i ( B X. A ) ) C_ B
15 14 sseli 
 |-  ( x e. dom ( f i^i ( B X. A ) ) -> x e. B )
16 10 rnssi 
 |-  ran ( f i^i ( B X. A ) ) C_ ran ( B X. A )
17 rnxpss 
 |-  ran ( B X. A ) C_ A
18 16 17 sstri 
 |-  ran ( f i^i ( B X. A ) ) C_ A
19 18 sseli 
 |-  ( y e. ran ( f i^i ( B X. A ) ) -> y e. A )
20 inss1 
 |-  ( f i^i ( B X. A ) ) C_ f
21 20 ssbri 
 |-  ( x ( f i^i ( B X. A ) ) y -> x f y )
22 19 21 anim12i 
 |-  ( ( y e. ran ( f i^i ( B X. A ) ) /\ x ( f i^i ( B X. A ) ) y ) -> ( y e. A /\ x f y ) )
23 22 moimi 
 |-  ( E* y ( y e. A /\ x f y ) -> E* y ( y e. ran ( f i^i ( B X. A ) ) /\ x ( f i^i ( B X. A ) ) y ) )
24 df-rmo 
 |-  ( E* y e. A x f y <-> E* y ( y e. A /\ x f y ) )
25 df-rmo 
 |-  ( E* y e. ran ( f i^i ( B X. A ) ) x ( f i^i ( B X. A ) ) y <-> E* y ( y e. ran ( f i^i ( B X. A ) ) /\ x ( f i^i ( B X. A ) ) y ) )
26 23 24 25 3imtr4i 
 |-  ( E* y e. A x f y -> E* y e. ran ( f i^i ( B X. A ) ) x ( f i^i ( B X. A ) ) y )
27 15 26 imim12i 
 |-  ( ( x e. B -> E* y e. A x f y ) -> ( x e. dom ( f i^i ( B X. A ) ) -> E* y e. ran ( f i^i ( B X. A ) ) x ( f i^i ( B X. A ) ) y ) )
28 27 ralimi2 
 |-  ( A. x e. B E* y e. A x f y -> A. x e. dom ( f i^i ( B X. A ) ) E* y e. ran ( f i^i ( B X. A ) ) x ( f i^i ( B X. A ) ) y )
29 relinxp 
 |-  Rel ( f i^i ( B X. A ) )
30 28 29 jctil 
 |-  ( A. x e. B E* y e. A x f y -> ( Rel ( f i^i ( B X. A ) ) /\ A. x e. dom ( f i^i ( B X. A ) ) E* y e. ran ( f i^i ( B X. A ) ) x ( f i^i ( B X. A ) ) y ) )
31 dffun9 
 |-  ( 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 e. ran ( f i^i ( B X. A ) ) x ( f i^i ( B X. A ) ) y ) )
32 30 31 sylibr 
 |-  ( A. x e. B E* y e. A x f y -> Fun ( f i^i ( B X. A ) ) )
33 32 funfnd 
 |-  ( A. x e. B E* y e. A x f y -> ( f i^i ( B X. A ) ) Fn dom ( f i^i ( B X. A ) ) )
34 rninxp 
 |-  ( ran ( f i^i ( B X. A ) ) = A <-> A. x e. A E. y e. B y f x )
35 34 biimpri 
 |-  ( A. x e. A E. y e. B y f x -> ran ( f i^i ( B X. A ) ) = A )
36 33 35 anim12i 
 |-  ( ( A. x e. B E* y e. A 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 ) )
37 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 ) )
38 36 37 sylibr 
 |-  ( ( A. x e. B E* y e. A 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 )
39 vex 
 |-  f e. _V
40 39 inex1 
 |-  ( f i^i ( B X. A ) ) e. _V
41 40 dmex 
 |-  dom ( f i^i ( B X. A ) ) e. _V
42 41 fodom 
 |-  ( ( f i^i ( B X. A ) ) : dom ( f i^i ( B X. A ) ) -onto-> A -> A ~<_ dom ( f i^i ( B X. A ) ) )
43 38 42 syl 
 |-  ( ( A. x e. B E* y e. A x f y /\ A. x e. A E. y e. B y f x ) -> A ~<_ dom ( f i^i ( B X. A ) ) )
44 ssdomg 
 |-  ( B e. _V -> ( dom ( f i^i ( B X. A ) ) C_ B -> dom ( f i^i ( B X. A ) ) ~<_ B ) )
45 1 14 44 mp2 
 |-  dom ( f i^i ( B X. A ) ) ~<_ B
46 domtr 
 |-  ( ( A ~<_ dom ( f i^i ( B X. A ) ) /\ dom ( f i^i ( B X. A ) ) ~<_ B ) -> A ~<_ B )
47 43 45 46 sylancl 
 |-  ( ( A. x e. B E* y e. A x f y /\ A. x e. A E. y e. B y f x ) -> A ~<_ B )
48 47 exlimiv 
 |-  ( E. f ( A. x e. B E* y e. A x f y /\ A. x e. A E. y e. B y f x ) -> A ~<_ B )
49 9 48 impbii 
 |-  ( A ~<_ B <-> E. f ( A. x e. B E* y e. A x f y /\ A. x e. A E. y e. B y f x ) )