This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
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 ) ) |
| 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 ) ) |