MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  domunsncan Structured version   Visualization version   Unicode version
Theorem domunsncan 8060
Description: A singleton cancellation law for dominance. (Contributed by Stefan O'Rear, 19-Feb-2015.) (Revised by Stefan O'Rear, 5-May-2015.)
Hypotheses
Ref Expression
domunsncan.a |- A e. _V
domunsncan.b |- B e. _V
Assertion
Ref Expression
domunsncan |- ( ( -. A e. X /\ -. B e. Y ) -> ( ( { A } u. X ) ~<_ ( { B } u. Y ) <-> X ~<_ Y ) )
Proof of Theorem domunsncan
Dummy variable f is distinct from all other variables.
StepHypRef Expression
1 ssun2 3777 . . . 4 |- Y C_ ( { B } u. Y )
2 reldom 7961 . . . . . 6 |- Rel ~<_
32brrelex2i 5159 . . . . 5 |- ( ( { A } u. X ) ~<_ ( { B } u. Y ) -> ( { B } u. Y ) e. _V )
43adantl 482 . . . 4 |- ( ( ( -. A e. X /\ -. B e. Y ) /\ ( { A } u. X ) ~<_ ( { B } u. Y ) ) -> ( { B } u. Y ) e. _V )
5 ssexg 4804 . . . 4 |- ( ( Y C_ ( { B } u. Y ) /\ ( { B } u. Y ) e. _V ) -> Y e. _V )
61, 4, 5sylancr 695 . . 3 |- ( ( ( -. A e. X /\ -. B e. Y ) /\ ( { A } u. X ) ~<_ ( { B } u. Y ) ) -> Y e. _V )
7 brdomi 7966 . . . . 5 |- ( ( { A } u. X ) ~<_ ( { B } u. Y ) -> E. f f : ( { A } u. X ) -1-1-> ( { B } u. Y ) )
8 vex 3203 . . . . . . . . . . 11 |- f e. _V
98resex 5443 . . . . . . . . . 10 |- ( f |` ( ( { A } u. X ) \ { A } ) ) e. _V
10 simprr 796 . . . . . . . . . . 11 |- ( ( ( -. 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 ) )
11 difss 3737 . . . . . . . . . . 11 |- ( ( { A } u. X ) \ { A } ) C_ ( { A } u. X )
12 f1ores 6151 . . . . . . . . . . 11 |- ( ( 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 } ) ) )
1310, 11, 12sylancl 694 . . . . . . . . . 10 |- ( ( ( -. 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 } ) ) )
14 f1oen3g 7971 . . . . . . . . . 10 |- ( ( ( 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 } ) ) )
159, 13, 14sylancr 695 . . . . . . . . 9 |- ( ( ( -. 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 } ) ) )
16 df-f1 5893 . . . . . . . . . . . . 13 |- ( f : ( { A } u. X ) -1-1-> ( { B } u. Y ) <-> ( f : ( { A } u. X ) --> ( { B } u. Y ) /\ Fun `' f ) )
1716simprbi 480 . . . . . . . . . . . 12 |- ( f : ( { A } u. X ) -1-1-> ( { B } u. Y ) -> Fun `' f )
18 imadif 5973 . . . . . . . . . . . 12 |- ( Fun `' f -> ( f " ( ( { A } u. X ) \ { A } ) ) = ( ( f " ( { A } u. X ) ) \ ( f " { A } ) ) )
1917, 18syl 17 . . . . . . . . . . 11 |- ( f : ( { A } u. X ) -1-1-> ( { B } u. Y ) -> ( f " ( ( { A } u. X ) \ { A } ) ) = ( ( f " ( { A } u. X ) ) \ ( f " { A } ) ) )
2019ad2antll 765 . . . . . . . . . 10 |- ( ( ( -. 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 } ) ) )
21 snex 4908 . . . . . . . . . . . . . 14 |- { B } e. _V
22 simprl 794 . . . . . . . . . . . . . 14 |- ( ( ( -. A e. X /\ -. B e. Y ) /\ ( Y e. _V /\ f : ( { A } u. X ) -1-1-> ( { B } u. Y ) ) ) -> Y e. _V )
23 unexg 6959 . . . . . . . . . . . . . 14 |- ( ( { B } e. _V /\ Y e. _V ) -> ( { B } u. Y ) e. _V )
2421, 22, 23sylancr 695 . . . . . . . . . . . . 13 |- ( ( ( -. A e. X /\ -. B e. Y ) /\ ( Y e. _V /\ f : ( { A } u. X ) -1-1-> ( { B } u. Y ) ) ) -> ( { B } u. Y ) e. _V )
25 difexg 4808 . . . . . . . . . . . . 13 |- ( ( { B } u. Y ) e. _V -> ( ( { B } u. Y ) \ { ( f ` A ) } ) e. _V )
2624, 25syl 17 . . . . . . . . . . . 12 |- ( ( ( -. 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 6101 . . . . . . . . . . . . . . . 16 |- ( f : ( { A } u. X ) -1-1-> ( { B } u. Y ) -> f : ( { A } u. X ) --> ( { B } u. Y ) )
28 imassrn 5477 . . . . . . . . . . . . . . . . 17 |- ( f " ( { A } u. X ) ) C_ ran f
29 frn 6053 . . . . . . . . . . . . . . . . 17 |- ( f : ( { A } u. X ) --> ( { B } u. Y ) -> ran f C_ ( { B } u. Y ) )
3028, 29syl5ss 3614 . . . . . . . . . . . . . . . 16 |- ( f : ( { A } u. X ) --> ( { B } u. Y ) -> ( f " ( { A } u. X ) ) C_ ( { B } u. Y ) )
3127, 30syl 17 . . . . . . . . . . . . . . 15 |- ( f : ( { A } u. X ) -1-1-> ( { B } u. Y ) -> ( f " ( { A } u. X ) ) C_ ( { B } u. Y ) )
3231ad2antll 765 . . . . . . . . . . . . . 14 |- ( ( ( -. 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 ) )
3332ssdifd 3746 . . . . . . . . . . . . 13 |- ( ( ( -. 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 } ) ) )
34 f1fn 6102 . . . . . . . . . . . . . . . 16 |- ( f : ( { A } u. X ) -1-1-> ( { B } u. Y ) -> f Fn ( { A } u. X ) )
3534ad2antll 765 . . . . . . . . . . . . . . 15 |- ( ( ( -. A e. X /\ -. B e. Y ) /\ ( Y e. _V /\ f : ( { A } u. X ) -1-1-> ( { B } u. Y ) ) ) -> f Fn ( { A } u. X ) )
36 domunsncan.a . . . . . . . . . . . . . . . . 17 |- A e. _V
3736snid 4208 . . . . . . . . . . . . . . . 16 |- A e. { A }
38 elun1 3780 . . . . . . . . . . . . . . . 16 |- ( A e. { A } -> A e. ( { A } u. X ) )
3937, 38ax-mp 5 . . . . . . . . . . . . . . 15 |- A e. ( { A } u. X )
40 fnsnfv 6258 . . . . . . . . . . . . . . 15 |- ( ( f Fn ( { A } u. X ) /\ A e. ( { A } u. X ) ) -> { ( f ` A ) } = ( f " { A } ) )
4135, 39, 40sylancl 694 . . . . . . . . . . . . . 14 |- ( ( ( -. A e. X /\ -. B e. Y ) /\ ( Y e. _V /\ f : ( { A } u. X ) -1-1-> ( { B } u. Y ) ) ) -> { ( f ` A ) } = ( f " { A } ) )
4241difeq2d 3728 . . . . . . . . . . . . 13 |- ( ( ( -. 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 } ) ) )
4333, 42sseqtr4d 3642 . . . . . . . . . . . 12 |- ( ( ( -. 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 ) } ) )
44 ssdomg 8001 . . . . . . . . . . . 12 |- ( ( ( { 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 ) } ) ) )
4526, 43, 44sylc 65 . . . . . . . . . . 11 |- ( ( ( -. 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 ) } ) )
46 ffvelrn 6357 . . . . . . . . . . . . . 14 |- ( ( f : ( { A } u. X ) --> ( { B } u. Y ) /\ A e. ( { A } u. X ) ) -> ( f ` A ) e. ( { B } u. Y ) )
4727, 39, 46sylancl 694 . . . . . . . . . . . . 13 |- ( f : ( { A } u. X ) -1-1-> ( { B } u. Y ) -> ( f ` A ) e. ( { B } u. Y ) )
4847ad2antll 765 . . . . . . . . . . . 12 |- ( ( ( -. A e. X /\ -. B e. Y ) /\ ( Y e. _V /\ f : ( { A } u. X ) -1-1-> ( { B } u. Y ) ) ) -> ( f ` A ) e. ( { B } u. Y ) )
49 domunsncan.b . . . . . . . . . . . . . 14 |- B e. _V
5049snid 4208 . . . . . . . . . . . . 13 |- B e. { B }
51 elun1 3780 . . . . . . . . . . . . 13 |- ( B e. { B } -> B e. ( { B } u. Y ) )
5250, 51mp1i 13 . . . . . . . . . . . 12 |- ( ( ( -. A e. X /\ -. B e. Y ) /\ ( Y e. _V /\ f : ( { A } u. X ) -1-1-> ( { B } u. Y ) ) ) -> B e. ( { B } u. Y ) )
53 difsnen 8042 . . . . . . . . . . . 12 |- ( ( ( { 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 } ) )
5424, 48, 52, 53syl3anc 1326 . . . . . . . . . . 11 |- ( ( ( -. 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 } ) )
55 domentr 8015 . . . . . . . . . . 11 |- ( ( ( ( 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 } ) )
5645, 54, 55syl2anc 693 . . . . . . . . . 10 |- ( ( ( -. 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 } ) )
5720, 56eqbrtrd 4675 . . . . . . . . 9 |- ( ( ( -. 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 } ) )
58 endomtr 8014 . . . . . . . . 9 |- ( ( ( ( { 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 } ) )
5915, 57, 58syl2anc 693 . . . . . . . 8 |- ( ( ( -. 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 } ) )
60 uncom 3757 . . . . . . . . . . . 12 |- ( { A } u. X ) = ( X u. { A } )
6160difeq1i 3724 . . . . . . . . . . 11 |- ( ( { A } u. X ) \ { A } ) = ( ( X u. { A } ) \ { A } )
62 difun2 4048 . . . . . . . . . . 11 |- ( ( X u. { A } ) \ { A } ) = ( X \ { A } )
6361, 62eqtri 2644 . . . . . . . . . 10 |- ( ( { A } u. X ) \ { A } ) = ( X \ { A } )
64 difsn 4328 . . . . . . . . . 10 |- ( -. A e. X -> ( X \ { A } ) = X )
6563, 64syl5eq 2668 . . . . . . . . 9 |- ( -. A e. X -> ( ( { A } u. X ) \ { A } ) = X )
6665ad2antrr 762 . . . . . . . 8 |- ( ( ( -. A e. X /\ -. B e. Y ) /\ ( Y e. _V /\ f : ( { A } u. X ) -1-1-> ( { B } u. Y ) ) ) -> ( ( { A } u. X ) \ { A } ) = X )
67 uncom 3757 . . . . . . . . . . . 12 |- ( { B } u. Y ) = ( Y u. { B } )
6867difeq1i 3724 . . . . . . . . . . 11 |- ( ( { B } u. Y ) \ { B } ) = ( ( Y u. { B } ) \ { B } )
69 difun2 4048 . . . . . . . . . . 11 |- ( ( Y u. { B } ) \ { B } ) = ( Y \ { B } )
7068, 69eqtri 2644 . . . . . . . . . 10 |- ( ( { B } u. Y ) \ { B } ) = ( Y \ { B } )
71 difsn 4328 . . . . . . . . . 10 |- ( -. B e. Y -> ( Y \ { B } ) = Y )
7270, 71syl5eq 2668 . . . . . . . . 9 |- ( -. B e. Y -> ( ( { B } u. Y ) \ { B } ) = Y )
7372ad2antlr 763 . . . . . . . 8 |- ( ( ( -. A e. X /\ -. B e. Y ) /\ ( Y e. _V /\ f : ( { A } u. X ) -1-1-> ( { B } u. Y ) ) ) -> ( ( { B } u. Y ) \ { B } ) = Y )
7459, 66, 733brtr3d 4684 . . . . . . 7 |- ( ( ( -. A e. X /\ -. B e. Y ) /\ ( Y e. _V /\ f : ( { A } u. X ) -1-1-> ( { B } u. Y ) ) ) -> X ~<_ Y )
7574expr 643 . . . . . 6 |- ( ( ( -. A e. X /\ -. B e. Y ) /\ Y e. _V ) -> ( f : ( { A } u. X ) -1-1-> ( { B } u. Y ) -> X ~<_ Y ) )
7675exlimdv 1861 . . . . 5 |- ( ( ( -. A e. X /\ -. B e. Y ) /\ Y e. _V ) -> ( E. f f : ( { A } u. X ) -1-1-> ( { B } u. Y ) -> X ~<_ Y ) )
777, 76syl5 34 . . . 4 |- ( ( ( -. A e. X /\ -. B e. Y ) /\ Y e. _V ) -> ( ( { A } u. X ) ~<_ ( { B } u. Y ) -> X ~<_ Y ) )
7877impancom 456 . . 3 |- ( ( ( -. A e. X /\ -. B e. Y ) /\ ( { A } u. X ) ~<_ ( { B } u. Y ) ) -> ( Y e. _V -> X ~<_ Y ) )
796, 78mpd 15 . 2 |- ( ( ( -. A e. X /\ -. B e. Y ) /\ ( { A } u. X ) ~<_ ( { B } u. Y ) ) -> X ~<_ Y )
80 en2sn 8037 . . . . 5 |- ( ( A e. _V /\ B e. _V ) -> { A } ~~ { B } )
8136, 49, 80mp2an 708 . . . 4 |- { A } ~~ { B }
82 endom 7982 . . . 4 |- ( { A } ~~ { B } -> { A } ~<_ { B } )
8381, 82mp1i 13 . . 3 |- ( ( ( -. A e. X /\ -. B e. Y ) /\ X ~<_ Y ) -> { A } ~<_ { B } )
84 simpr 477 . . 3 |- ( ( ( -. A e. X /\ -. B e. Y ) /\ X ~<_ Y ) -> X ~<_ Y )
85 incom 3805 . . . . 5 |- ( { B } i^i Y ) = ( Y i^i { B } )
86 disjsn 4246 . . . . . 6 |- ( ( Y i^i { B } ) = (/) <-> -. B e. Y )
8786biimpri 218 . . . . 5 |- ( -. B e. Y -> ( Y i^i { B } ) = (/) )
8885, 87syl5eq 2668 . . . 4 |- ( -. B e. Y -> ( { B } i^i Y ) = (/) )
8988ad2antlr 763 . . 3 |- ( ( ( -. A e. X /\ -. B e. Y ) /\ X ~<_ Y ) -> ( { B } i^i Y ) = (/) )
90 undom 8048 . . 3 |- ( ( ( { A } ~<_ { B } /\ X ~<_ Y ) /\ ( { B } i^i Y ) = (/) ) -> ( { A } u. X ) ~<_ ( { B } u. Y ) )
9183, 84, 89, 90syl21anc 1325 . 2 |- ( ( ( -. A e. X /\ -. B e. Y ) /\ X ~<_ Y ) -> ( { A } u. X ) ~<_ ( { B } u. Y ) )
9279, 91impbida 877 1 |- ( ( -. A e. X /\ -. B e. Y ) -> ( ( { A } u. X ) ~<_ ( { B } u. Y ) <-> X ~<_ Y ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   /\ wa 384   = wceq 1483   E.wex 1704   e. wcel 1990   _Vcvv 3200   \ cdif 3571   u. cun 3572   i^i cin 3573   C_ wss 3574   (/)c0 3915   {csn 4177   class class class wbr 4653   `'ccnv 5113   ran crn 5115   |` cres 5116   "cima 5117   Fun wfun 5882   Fn wfn 5883   -->wf 5884   -1-1->wf1 5885   -1-1-onto->wf1o 5887   ` cfv 5888   ~~ cen 7952   ~<_ cdom 7953
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-id 5024  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-1o 7560  df-er 7742  df-en 7956  df-dom 7957
This theorem is referenced by:  domunfican  8233
  Copyright terms: Public domain W3C validator