This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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