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 difexg 
 |-  ( ( { B } u. Y ) e. _V -> ( ( { B } u. Y ) \ { ( f ` A ) } ) e. _V )
27 25 26 syl 
 |-  ( ( ( -. 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 )
28 f1f 
 |-  ( f : ( { A } u. X ) -1-1-> ( { B } u. Y ) -> f : ( { A } u. X ) --> ( { B } u. Y ) )
29 fimass 
 |-  ( f : ( { A } u. X ) --> ( { B } u. Y ) -> ( f " ( { A } u. X ) ) C_ ( { B } u. Y ) )
30 28 29 syl 
 |-  ( f : ( { A } u. X ) -1-1-> ( { B } u. Y ) -> ( f " ( { A } u. X ) ) C_ ( { B } u. Y ) )
31 30 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 ) )
32 31 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 } ) ) )
33 f1fn 
 |-  ( f : ( { A } u. X ) -1-1-> ( { B } u. Y ) -> f Fn ( { A } u. X ) )
34 33 ad2antll 
 |-  ( ( ( -. A e. X /\ -. B e. Y ) /\ ( Y e. _V /\ f : ( { A } u. X ) -1-1-> ( { B } u. Y ) ) ) -> f Fn ( { A } u. X ) )
35 1 snid 
 |-  A e. { A }
36 elun1 
 |-  ( A e. { A } -> A e. ( { A } u. X ) )
37 35 36 ax-mp 
 |-  A e. ( { A } u. X )
38 fnsnfv 
 |-  ( ( f Fn ( { A } u. X ) /\ A e. ( { A } u. X ) ) -> { ( f ` A ) } = ( f " { A } ) )
39 34 37 38 sylancl 
 |-  ( ( ( -. A e. X /\ -. B e. Y ) /\ ( Y e. _V /\ f : ( { A } u. X ) -1-1-> ( { B } u. Y ) ) ) -> { ( f ` A ) } = ( f " { A } ) )
40 39 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 } ) ) )
41 32 40 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 ) } ) )
42 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 ) } ) ) )
43 27 41 42 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 ) } ) )
44 ffvelrn 
 |-  ( ( f : ( { A } u. X ) --> ( { B } u. Y ) /\ A e. ( { A } u. X ) ) -> ( f ` A ) e. ( { B } u. Y ) )
45 28 37 44 sylancl 
 |-  ( f : ( { A } u. X ) -1-1-> ( { B } u. Y ) -> ( f ` A ) e. ( { B } u. Y ) )
46 45 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 ) )
47 2 snid 
 |-  B e. { B }
48 elun1 
 |-  ( B e. { B } -> B e. ( { B } u. Y ) )
49 47 48 mp1i 
 |-  ( ( ( -. A e. X /\ -. B e. Y ) /\ ( Y e. _V /\ f : ( { A } u. X ) -1-1-> ( { B } u. Y ) ) ) -> B e. ( { B } u. Y ) )
50 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 } ) )
51 25 46 49 50 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 } ) )
52 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 } ) )
53 43 51 52 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 } ) )
54 21 53 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 } ) )
55 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 } ) )
56 17 54 55 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 } ) )
57 uncom 
 |-  ( { A } u. X ) = ( X u. { A } )
58 57 difeq1i 
 |-  ( ( { A } u. X ) \ { A } ) = ( ( X u. { A } ) \ { A } )
59 difun2 
 |-  ( ( X u. { A } ) \ { A } ) = ( X \ { A } )
60 58 59 eqtri 
 |-  ( ( { A } u. X ) \ { A } ) = ( X \ { A } )
61 difsn 
 |-  ( -. A e. X -> ( X \ { A } ) = X )
62 60 61 syl5eq 
 |-  ( -. A e. X -> ( ( { A } u. X ) \ { A } ) = X )
63 62 ad2antrr 
 |-  ( ( ( -. A e. X /\ -. B e. Y ) /\ ( Y e. _V /\ f : ( { A } u. X ) -1-1-> ( { B } u. Y ) ) ) -> ( ( { A } u. X ) \ { A } ) = X )
64 uncom 
 |-  ( { B } u. Y ) = ( Y u. { B } )
65 64 difeq1i 
 |-  ( ( { B } u. Y ) \ { B } ) = ( ( Y u. { B } ) \ { B } )
66 difun2 
 |-  ( ( Y u. { B } ) \ { B } ) = ( Y \ { B } )
67 65 66 eqtri 
 |-  ( ( { B } u. Y ) \ { B } ) = ( Y \ { B } )
68 difsn 
 |-  ( -. B e. Y -> ( Y \ { B } ) = Y )
69 67 68 syl5eq 
 |-  ( -. B e. Y -> ( ( { B } u. Y ) \ { B } ) = Y )
70 69 ad2antlr 
 |-  ( ( ( -. A e. X /\ -. B e. Y ) /\ ( Y e. _V /\ f : ( { A } u. X ) -1-1-> ( { B } u. Y ) ) ) -> ( ( { B } u. Y ) \ { B } ) = Y )
71 56 63 70 3brtr3d 
 |-  ( ( ( -. A e. X /\ -. B e. Y ) /\ ( Y e. _V /\ f : ( { A } u. X ) -1-1-> ( { B } u. Y ) ) ) -> X ~<_ Y )
72 71 expr 
 |-  ( ( ( -. A e. X /\ -. B e. Y ) /\ Y e. _V ) -> ( f : ( { A } u. X ) -1-1-> ( { B } u. Y ) -> X ~<_ Y ) )
73 72 exlimdv 
 |-  ( ( ( -. A e. X /\ -. B e. Y ) /\ Y e. _V ) -> ( E. f f : ( { A } u. X ) -1-1-> ( { B } u. Y ) -> X ~<_ Y ) )
74 9 73 syl5 
 |-  ( ( ( -. A e. X /\ -. B e. Y ) /\ Y e. _V ) -> ( ( { A } u. X ) ~<_ ( { B } u. Y ) -> X ~<_ Y ) )
75 74 impancom 
 |-  ( ( ( -. A e. X /\ -. B e. Y ) /\ ( { A } u. X ) ~<_ ( { B } u. Y ) ) -> ( Y e. _V -> X ~<_ Y ) )
76 8 75 mpd 
 |-  ( ( ( -. A e. X /\ -. B e. Y ) /\ ( { A } u. X ) ~<_ ( { B } u. Y ) ) -> X ~<_ Y )
77 en2sn 
 |-  ( ( A e. _V /\ B e. _V ) -> { A } ~~ { B } )
78 1 2 77 mp2an 
 |-  { A } ~~ { B }
79 endom 
 |-  ( { A } ~~ { B } -> { A } ~<_ { B } )
80 78 79 mp1i 
 |-  ( ( ( -. A e. X /\ -. B e. Y ) /\ X ~<_ Y ) -> { A } ~<_ { B } )
81 simpr 
 |-  ( ( ( -. A e. X /\ -. B e. Y ) /\ X ~<_ Y ) -> X ~<_ Y )
82 incom 
 |-  ( { B } i^i Y ) = ( Y i^i { B } )
83 disjsn 
 |-  ( ( Y i^i { B } ) = (/) <-> -. B e. Y )
84 83 biimpri 
 |-  ( -. B e. Y -> ( Y i^i { B } ) = (/) )
85 82 84 syl5eq 
 |-  ( -. B e. Y -> ( { B } i^i Y ) = (/) )
86 85 ad2antlr 
 |-  ( ( ( -. A e. X /\ -. B e. Y ) /\ X ~<_ Y ) -> ( { B } i^i Y ) = (/) )
87 undom 
 |-  ( ( ( { A } ~<_ { B } /\ X ~<_ Y ) /\ ( { B } i^i Y ) = (/) ) -> ( { A } u. X ) ~<_ ( { B } u. Y ) )
88 80 81 86 87 syl21anc 
 |-  ( ( ( -. A e. X /\ -. B e. Y ) /\ X ~<_ Y ) -> ( { A } u. X ) ~<_ ( { B } u. Y ) )
89 76 88 impbida 
 |-  ( ( -. A e. X /\ -. B e. Y ) -> ( ( { A } u. X ) ~<_ ( { B } u. Y ) <-> X ~<_ Y ) )