Metamath Proof Explorer

Theorem domunsncan

Description: A singleton cancellation law for dominance. (Contributed by Stefan O'Rear, 19-Feb-2015) (Revised by Stefan O'Rear, 5-May-2015)

Ref Expression
Hypotheses domunsncan.a 
|- A e. _V
domunsncan.b 
|- B e. _V
Assertion domunsncan 
|- ( ( -. A e. X /\ -. B e. Y ) -> ( ( { A } u. X ) ~<_ ( { B } u. Y ) <-> X ~<_ Y ) )

Proof

Step Hyp Ref Expression
1 domunsncan.a 
 |-  A e. _V
2 domunsncan.b 
 |-  B e. _V
3 ssun2 
 |-  Y C_ ( { B } u. Y )
4 reldom 
 |-  Rel ~<_
5 4 brrelex2i 
 |-  ( ( { A } u. X ) ~<_ ( { B } u. Y ) -> ( { B } u. Y ) e. _V )
6 5 adantl 
 |-  ( ( ( -. A e. X /\ -. B e. Y ) /\ ( { A } u. X ) ~<_ ( { B } u. Y ) ) -> ( { B } u. Y ) e. _V )
7 ssexg 
 |-  ( ( Y C_ ( { B } u. Y ) /\ ( { B } u. Y ) e. _V ) -> Y e. _V )
8 3 6 7 sylancr 
 |-  ( ( ( -. A e. X /\ -. B e. Y ) /\ ( { A } u. X ) ~<_ ( { B } u. Y ) ) -> Y e. _V )
9 brdomi 
 |-  ( ( { A } u. X ) ~<_ ( { B } u. Y ) -> E. f f : ( { A } u. X ) -1-1-> ( { B } u. Y ) )
10 vex 
 |-  f e. _V
11 10 resex 
 |-  ( f |` ( ( { A } u. X ) \ { A } ) ) e. _V
12 simprr 
 |-  ( ( ( -. A e. X /\ -. B e. Y ) /\ ( Y e. _V /\ f : ( { A } u. X ) -1-1-> ( { B } u. Y ) ) ) -> f : ( { A } u. X ) -1-1-> ( { B } u. Y ) )
13 difss 
 |-  ( ( { A } u. X ) \ { A } ) C_ ( { A } u. X )
14 f1ores 
 |-  ( ( f : ( { A } u. X ) -1-1-> ( { B } u. Y ) /\ ( ( { A } u. X ) \ { A } ) C_ ( { A } u. X ) ) -> ( f |` ( ( { A } u. X ) \ { A } ) ) : ( ( { A } u. X ) \ { A } ) -1-1-onto-> ( f " ( ( { A } u. X ) \ { A } ) ) )
15 12 13 14 sylancl 
 |-  ( ( ( -. A e. X /\ -. B e. Y ) /\ ( Y e. _V /\ f : ( { A } u. X ) -1-1-> ( { B } u. Y ) ) ) -> ( f |` ( ( { A } u. X ) \ { A } ) ) : ( ( { A } u. X ) \ { A } ) -1-1-onto-> ( f " ( ( { A } u. X ) \ { A } ) ) )
16 f1oen3g 
 |-  ( ( ( f |` ( ( { A } u. X ) \ { A } ) ) e. _V /\ ( f |` ( ( { A } u. X ) \ { A } ) ) : ( ( { A } u. X ) \ { A } ) -1-1-onto-> ( f " ( ( { A } u. X ) \ { A } ) ) ) -> ( ( { A } u. X ) \ { A } ) ~~ ( f " ( ( { A } u. X ) \ { A } ) ) )
17 11 15 16 sylancr 
 |-  ( ( ( -. A e. X /\ -. B e. Y ) /\ ( Y e. _V /\ f : ( { A } u. X ) -1-1-> ( { B } u. Y ) ) ) -> ( ( { A } u. X ) \ { A } ) ~~ ( f " ( ( { A } u. X ) \ { A } ) ) )
18 df-f1 
 |-  ( f : ( { A } u. X ) -1-1-> ( { B } u. Y ) <-> ( f : ( { A } u. X ) --> ( { B } u. Y ) /\ Fun `' f ) )
19 imadif 
 |-  ( Fun `' f -> ( f " ( ( { A } u. X ) \ { A } ) ) = ( ( f " ( { A } u. X ) ) \ ( f " { A } ) ) )
20 18 19 simplbiim 
 |-  ( f : ( { A } u. X ) -1-1-> ( { B } u. Y ) -> ( f " ( ( { A } u. X ) \ { A } ) ) = ( ( f " ( { A } u. X ) ) \ ( f " { A } ) ) )
21 20 ad2antll 
 |-  ( ( ( -. A e. X /\ -. B e. Y ) /\ ( Y e. _V /\ f : ( { A } u. X ) -1-1-> ( { B } u. Y ) ) ) -> ( f " ( ( { A } u. X ) \ { A } ) ) = ( ( f " ( { A } u. X ) ) \ ( f " { A } ) ) )
22 snex 
 |-  { B } e. _V
23 simprl 
 |-  ( ( ( -. A e. X /\ -. B e. Y ) /\ ( Y e. _V /\ f : ( { A } u. X ) -1-1-> ( { B } u. Y ) ) ) -> Y e. _V )
24 unexg 
 |-  ( ( { B } e. _V /\ Y e. _V ) -> ( { B } u. Y ) e. _V )
25 22 23 24 sylancr 
 |-  ( ( ( -. A e. X /\ -. B e. Y ) /\ ( Y e. _V /\ f : ( { A } u. X ) -1-1-> ( { B } u. Y ) ) ) -> ( { B } u. Y ) e. _V )
26 25 difexd 
 |-  ( ( ( -. A e. X /\ -. B e. Y ) /\ ( Y e. _V /\ f : ( { A } u. X ) -1-1-> ( { B } u. Y ) ) ) -> ( ( { B } u. Y ) \ { ( f ` A ) } ) e. _V )
27 f1f 
 |-  ( f : ( { A } u. X ) -1-1-> ( { B } u. Y ) -> f : ( { A } u. X ) --> ( { B } u. Y ) )
28 fimass 
 |-  ( f : ( { A } u. X ) --> ( { B } u. Y ) -> ( f " ( { A } u. X ) ) C_ ( { B } u. Y ) )
29 27 28 syl 
 |-  ( f : ( { A } u. X ) -1-1-> ( { B } u. Y ) -> ( f " ( { A } u. X ) ) C_ ( { B } u. Y ) )
30 29 ad2antll 
 |-  ( ( ( -. A e. X /\ -. B e. Y ) /\ ( Y e. _V /\ f : ( { A } u. X ) -1-1-> ( { B } u. Y ) ) ) -> ( f " ( { A } u. X ) ) C_ ( { B } u. Y ) )
31 30 ssdifd 
 |-  ( ( ( -. A e. X /\ -. B e. Y ) /\ ( Y e. _V /\ f : ( { A } u. X ) -1-1-> ( { B } u. Y ) ) ) -> ( ( f " ( { A } u. X ) ) \ ( f " { A } ) ) C_ ( ( { B } u. Y ) \ ( f " { A } ) ) )
32 f1fn 
 |-  ( f : ( { A } u. X ) -1-1-> ( { B } u. Y ) -> f Fn ( { A } u. X ) )
33 32 ad2antll 
 |-  ( ( ( -. A e. X /\ -. B e. Y ) /\ ( Y e. _V /\ f : ( { A } u. X ) -1-1-> ( { B } u. Y ) ) ) -> f Fn ( { A } u. X ) )
34 1 snid 
 |-  A e. { A }
35 elun1 
 |-  ( A e. { A } -> A e. ( { A } u. X ) )
36 34 35 ax-mp 
 |-  A e. ( { A } u. X )
37 fnsnfv 
 |-  ( ( f Fn ( { A } u. X ) /\ A e. ( { A } u. X ) ) -> { ( f ` A ) } = ( f " { A } ) )
38 33 36 37 sylancl 
 |-  ( ( ( -. A e. X /\ -. B e. Y ) /\ ( Y e. _V /\ f : ( { A } u. X ) -1-1-> ( { B } u. Y ) ) ) -> { ( f ` A ) } = ( f " { A } ) )
39 38 difeq2d 
 |-  ( ( ( -. A e. X /\ -. B e. Y ) /\ ( Y e. _V /\ f : ( { A } u. X ) -1-1-> ( { B } u. Y ) ) ) -> ( ( { B } u. Y ) \ { ( f ` A ) } ) = ( ( { B } u. Y ) \ ( f " { A } ) ) )
40 31 39 sseqtrrd 
 |-  ( ( ( -. A e. X /\ -. B e. Y ) /\ ( Y e. _V /\ f : ( { A } u. X ) -1-1-> ( { B } u. Y ) ) ) -> ( ( f " ( { A } u. X ) ) \ ( f " { A } ) ) C_ ( ( { B } u. Y ) \ { ( f ` A ) } ) )
41 ssdomg 
 |-  ( ( ( { B } u. Y ) \ { ( f ` A ) } ) e. _V -> ( ( ( f " ( { A } u. X ) ) \ ( f " { A } ) ) C_ ( ( { B } u. Y ) \ { ( f ` A ) } ) -> ( ( f " ( { A } u. X ) ) \ ( f " { A } ) ) ~<_ ( ( { B } u. Y ) \ { ( f ` A ) } ) ) )
42 26 40 41 sylc 
 |-  ( ( ( -. A e. X /\ -. B e. Y ) /\ ( Y e. _V /\ f : ( { A } u. X ) -1-1-> ( { B } u. Y ) ) ) -> ( ( f " ( { A } u. X ) ) \ ( f " { A } ) ) ~<_ ( ( { B } u. Y ) \ { ( f ` A ) } ) )
43 ffvelrn 
 |-  ( ( f : ( { A } u. X ) --> ( { B } u. Y ) /\ A e. ( { A } u. X ) ) -> ( f ` A ) e. ( { B } u. Y ) )
44 27 36 43 sylancl 
 |-  ( f : ( { A } u. X ) -1-1-> ( { B } u. Y ) -> ( f ` A ) e. ( { B } u. Y ) )
45 44 ad2antll 
 |-  ( ( ( -. A e. X /\ -. B e. Y ) /\ ( Y e. _V /\ f : ( { A } u. X ) -1-1-> ( { B } u. Y ) ) ) -> ( f ` A ) e. ( { B } u. Y ) )
46 2 snid 
 |-  B e. { B }
47 elun1 
 |-  ( B e. { B } -> B e. ( { B } u. Y ) )
48 46 47 mp1i 
 |-  ( ( ( -. A e. X /\ -. B e. Y ) /\ ( Y e. _V /\ f : ( { A } u. X ) -1-1-> ( { B } u. Y ) ) ) -> B e. ( { B } u. Y ) )
49 difsnen 
 |-  ( ( ( { B } u. Y ) e. _V /\ ( f ` A ) e. ( { B } u. Y ) /\ B e. ( { B } u. Y ) ) -> ( ( { B } u. Y ) \ { ( f ` A ) } ) ~~ ( ( { B } u. Y ) \ { B } ) )
50 25 45 48 49 syl3anc 
 |-  ( ( ( -. A e. X /\ -. B e. Y ) /\ ( Y e. _V /\ f : ( { A } u. X ) -1-1-> ( { B } u. Y ) ) ) -> ( ( { B } u. Y ) \ { ( f ` A ) } ) ~~ ( ( { B } u. Y ) \ { B } ) )
51 domentr 
 |-  ( ( ( ( f " ( { A } u. X ) ) \ ( f " { A } ) ) ~<_ ( ( { B } u. Y ) \ { ( f ` A ) } ) /\ ( ( { B } u. Y ) \ { ( f ` A ) } ) ~~ ( ( { B } u. Y ) \ { B } ) ) -> ( ( f " ( { A } u. X ) ) \ ( f " { A } ) ) ~<_ ( ( { B } u. Y ) \ { B } ) )
52 42 50 51 syl2anc 
 |-  ( ( ( -. A e. X /\ -. B e. Y ) /\ ( Y e. _V /\ f : ( { A } u. X ) -1-1-> ( { B } u. Y ) ) ) -> ( ( f " ( { A } u. X ) ) \ ( f " { A } ) ) ~<_ ( ( { B } u. Y ) \ { B } ) )
53 21 52 eqbrtrd 
 |-  ( ( ( -. A e. X /\ -. B e. Y ) /\ ( Y e. _V /\ f : ( { A } u. X ) -1-1-> ( { B } u. Y ) ) ) -> ( f " ( ( { A } u. X ) \ { A } ) ) ~<_ ( ( { B } u. Y ) \ { B } ) )
54 endomtr 
 |-  ( ( ( ( { A } u. X ) \ { A } ) ~~ ( f " ( ( { A } u. X ) \ { A } ) ) /\ ( f " ( ( { A } u. X ) \ { A } ) ) ~<_ ( ( { B } u. Y ) \ { B } ) ) -> ( ( { A } u. X ) \ { A } ) ~<_ ( ( { B } u. Y ) \ { B } ) )
55 17 53 54 syl2anc 
 |-  ( ( ( -. A e. X /\ -. B e. Y ) /\ ( Y e. _V /\ f : ( { A } u. X ) -1-1-> ( { B } u. Y ) ) ) -> ( ( { A } u. X ) \ { A } ) ~<_ ( ( { B } u. Y ) \ { B } ) )
56 uncom 
 |-  ( { A } u. X ) = ( X u. { A } )
57 56 difeq1i 
 |-  ( ( { A } u. X ) \ { A } ) = ( ( X u. { A } ) \ { A } )
58 difun2 
 |-  ( ( X u. { A } ) \ { A } ) = ( X \ { A } )
59 57 58 eqtri 
 |-  ( ( { A } u. X ) \ { A } ) = ( X \ { A } )
60 difsn 
 |-  ( -. A e. X -> ( X \ { A } ) = X )
61 59 60 eqtrid 
 |-  ( -. A e. X -> ( ( { A } u. X ) \ { A } ) = X )
62 61 ad2antrr 
 |-  ( ( ( -. A e. X /\ -. B e. Y ) /\ ( Y e. _V /\ f : ( { A } u. X ) -1-1-> ( { B } u. Y ) ) ) -> ( ( { A } u. X ) \ { A } ) = X )
63 uncom 
 |-  ( { B } u. Y ) = ( Y u. { B } )
64 63 difeq1i 
 |-  ( ( { B } u. Y ) \ { B } ) = ( ( Y u. { B } ) \ { B } )
65 difun2 
 |-  ( ( Y u. { B } ) \ { B } ) = ( Y \ { B } )
66 64 65 eqtri 
 |-  ( ( { B } u. Y ) \ { B } ) = ( Y \ { B } )
67 difsn 
 |-  ( -. B e. Y -> ( Y \ { B } ) = Y )
68 66 67 eqtrid 
 |-  ( -. B e. Y -> ( ( { B } u. Y ) \ { B } ) = Y )
69 68 ad2antlr 
 |-  ( ( ( -. A e. X /\ -. B e. Y ) /\ ( Y e. _V /\ f : ( { A } u. X ) -1-1-> ( { B } u. Y ) ) ) -> ( ( { B } u. Y ) \ { B } ) = Y )
70 55 62 69 3brtr3d 
 |-  ( ( ( -. A e. X /\ -. B e. Y ) /\ ( Y e. _V /\ f : ( { A } u. X ) -1-1-> ( { B } u. Y ) ) ) -> X ~<_ Y )
71 70 expr 
 |-  ( ( ( -. A e. X /\ -. B e. Y ) /\ Y e. _V ) -> ( f : ( { A } u. X ) -1-1-> ( { B } u. Y ) -> X ~<_ Y ) )
72 71 exlimdv 
 |-  ( ( ( -. A e. X /\ -. B e. Y ) /\ Y e. _V ) -> ( E. f f : ( { A } u. X ) -1-1-> ( { B } u. Y ) -> X ~<_ Y ) )
73 9 72 syl5 
 |-  ( ( ( -. A e. X /\ -. B e. Y ) /\ Y e. _V ) -> ( ( { A } u. X ) ~<_ ( { B } u. Y ) -> X ~<_ Y ) )
74 73 impancom 
 |-  ( ( ( -. A e. X /\ -. B e. Y ) /\ ( { A } u. X ) ~<_ ( { B } u. Y ) ) -> ( Y e. _V -> X ~<_ Y ) )
75 8 74 mpd 
 |-  ( ( ( -. A e. X /\ -. B e. Y ) /\ ( { A } u. X ) ~<_ ( { B } u. Y ) ) -> X ~<_ Y )
76 en2sn 
 |-  ( ( A e. _V /\ B e. _V ) -> { A } ~~ { B } )
77 1 2 76 mp2an 
 |-  { A } ~~ { B }
78 endom 
 |-  ( { A } ~~ { B } -> { A } ~<_ { B } )
79 77 78 mp1i 
 |-  ( ( ( -. A e. X /\ -. B e. Y ) /\ X ~<_ Y ) -> { A } ~<_ { B } )
80 simpr 
 |-  ( ( ( -. A e. X /\ -. B e. Y ) /\ X ~<_ Y ) -> X ~<_ Y )
81 incom 
 |-  ( { B } i^i Y ) = ( Y i^i { B } )
82 disjsn 
 |-  ( ( Y i^i { B } ) = (/) <-> -. B e. Y )
83 82 biimpri 
 |-  ( -. B e. Y -> ( Y i^i { B } ) = (/) )
84 81 83 eqtrid 
 |-  ( -. B e. Y -> ( { B } i^i Y ) = (/) )
85 84 ad2antlr 
 |-  ( ( ( -. A e. X /\ -. B e. Y ) /\ X ~<_ Y ) -> ( { B } i^i Y ) = (/) )
86 undom 
 |-  ( ( ( { A } ~<_ { B } /\ X ~<_ Y ) /\ ( { B } i^i Y ) = (/) ) -> ( { A } u. X ) ~<_ ( { B } u. Y ) )
87 79 80 85 86 syl21anc 
 |-  ( ( ( -. A e. X /\ -. B e. Y ) /\ X ~<_ Y ) -> ( { A } u. X ) ~<_ ( { B } u. Y ) )
88 75 87 impbida 
 |-  ( ( -. A e. X /\ -. B e. Y ) -> ( ( { A } u. X ) ~<_ ( { B } u. Y ) <-> X ~<_ Y ) )