Description: Dominance relation. This variation of brdomg does not require the Axiom of Union. (Contributed by NM, 15-Jun-1998) Extract from a subproof of brdomg . (Revised by BTernaryTau, 29-Nov-2024)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | brdom2g | |- ( ( A e. V /\ B e. W ) -> ( A ~<_ B <-> E. f f : A -1-1-> B ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | f1eq2 | |- ( x = A -> ( f : x -1-1-> y <-> f : A -1-1-> y ) ) |
|
| 2 | 1 | exbidv | |- ( x = A -> ( E. f f : x -1-1-> y <-> E. f f : A -1-1-> y ) ) |
| 3 | f1eq3 | |- ( y = B -> ( f : A -1-1-> y <-> f : A -1-1-> B ) ) |
|
| 4 | 3 | exbidv | |- ( y = B -> ( E. f f : A -1-1-> y <-> E. f f : A -1-1-> B ) ) |
| 5 | df-dom | |- ~<_ = { <. x , y >. | E. f f : x -1-1-> y } |
|
| 6 | 2 4 5 | brabg | |- ( ( A e. V /\ B e. W ) -> ( A ~<_ B <-> E. f f : A -1-1-> B ) ) |