Metamath Proof Explorer

Theorem domen

Description: Dominance in terms of equinumerosity. Example 1 of Enderton p. 146. (Contributed by NM, 15-Jun-1998)

Ref Expression
Hypothesis bren.1 
|- B e. _V
Assertion domen 
|- ( A ~<_ B <-> E. x ( A ~~ x /\ x C_ B ) )

Proof

Step Hyp Ref Expression
1 bren.1 
 |-  B e. _V
2 1 brdom 
 |-  ( A ~<_ B <-> E. f f : A -1-1-> B )
3 vex 
 |-  f e. _V
4 3 f11o 
 |-  ( f : A -1-1-> B <-> E. x ( f : A -1-1-onto-> x /\ x C_ B ) )
5 4 exbii 
 |-  ( E. f f : A -1-1-> B <-> E. f E. x ( f : A -1-1-onto-> x /\ x C_ B ) )
6 excom 
 |-  ( E. f E. x ( f : A -1-1-onto-> x /\ x C_ B ) <-> E. x E. f ( f : A -1-1-onto-> x /\ x C_ B ) )
7 5 6 bitri 
 |-  ( E. f f : A -1-1-> B <-> E. x E. f ( f : A -1-1-onto-> x /\ x C_ B ) )
8 bren 
 |-  ( A ~~ x <-> E. f f : A -1-1-onto-> x )
9 8 anbi1i 
 |-  ( ( A ~~ x /\ x C_ B ) <-> ( E. f f : A -1-1-onto-> x /\ x C_ B ) )
10 19.41v 
 |-  ( E. f ( f : A -1-1-onto-> x /\ x C_ B ) <-> ( E. f f : A -1-1-onto-> x /\ x C_ B ) )
11 9 10 bitr4i 
 |-  ( ( A ~~ x /\ x C_ B ) <-> E. f ( f : A -1-1-onto-> x /\ x C_ B ) )
12 11 exbii 
 |-  ( E. x ( A ~~ x /\ x C_ B ) <-> E. x E. f ( f : A -1-1-onto-> x /\ x C_ B ) )
13 7 12 bitr4i 
 |-  ( E. f f : A -1-1-> B <-> E. x ( A ~~ x /\ x C_ B ) )
14 2 13 bitri 
 |-  ( A ~<_ B <-> E. x ( A ~~ x /\ x C_ B ) )