Theorem brdom2g

Description: Dominance relation. This variation of brdomg does not require the Axiom of Union. (Contributed by BTernaryTau, 29-Nov-2024)

	Ref	Expression
Assertion	brdom2g	|- ( ( A e. V /\ B e. W ) -> ( A ~<_ B <-> E. f f : A -1-1-> B ) )

Proof

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