Theorem brdomg

Description: Dominance relation. (Contributed by NM, 15-Jun-1998)

	Ref	Expression
Assertion	brdomg	|- ( B e. C -> ( 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. C ) -> ( A ~<_ B <-> E. f f : A -1-1-> B ) )
7	6	ex	|- ( A e. _V -> ( B e. C -> ( A ~<_ B <-> E. f f : A -1-1-> B ) ) )
8		reldom	|- Rel ~<_
9	8	brrelex1i	|- ( A ~<_ B -> A e. _V )
10		f1f	|- ( f : A -1-1-> B -> f : A --> B )
11		fdm	|- ( f : A --> B -> dom f = A )
12		vex	|- f e. _V
13	12	dmex	|- dom f e. _V
14	11 13	eqeltrrdi	|- ( f : A --> B -> A e. _V )
15	10 14	syl	|- ( f : A -1-1-> B -> A e. _V )
16	15	exlimiv	|- ( E. f f : A -1-1-> B -> A e. _V )
17	9 16	pm5.21ni	|- ( -. A e. _V -> ( A ~<_ B <-> E. f f : A -1-1-> B ) )
18	17	a1d	|- ( -. A e. _V -> ( B e. C -> ( A ~<_ B <-> E. f f : A -1-1-> B ) ) )
19	7 18	pm2.61i	|- ( B e. C -> ( A ~<_ B <-> E. f f : A -1-1-> B ) )