Metamath Proof Explorer

Theorem domdifsn

Description: Dominance over a set with one element removed. (Contributed by Stefan O'Rear, 19-Feb-2015) (Revised by Mario Carneiro, 24-Jun-2015)

Ref Expression
Assertion domdifsn 
|- ( A ~< B -> A ~<_ ( B \ { C } ) )

Proof

Step Hyp Ref Expression
1 sdomdom 
 |-  ( A ~< B -> A ~<_ B )
2 relsdom 
 |-  Rel ~<
3 2 brrelex2i 
 |-  ( A ~< B -> B e. _V )
4 brdomg 
 |-  ( B e. _V -> ( A ~<_ B <-> E. f f : A -1-1-> B ) )
5 3 4 syl 
 |-  ( A ~< B -> ( A ~<_ B <-> E. f f : A -1-1-> B ) )
6 1 5 mpbid 
 |-  ( A ~< B -> E. f f : A -1-1-> B )
7 6 adantr 
 |-  ( ( A ~< B /\ C e. B ) -> E. f f : A -1-1-> B )
8 f1f 
 |-  ( f : A -1-1-> B -> f : A --> B )
9 8 frnd 
 |-  ( f : A -1-1-> B -> ran f C_ B )
10 9 adantl 
 |-  ( ( ( A ~< B /\ C e. B ) /\ f : A -1-1-> B ) -> ran f C_ B )
11 sdomnen 
 |-  ( A ~< B -> -. A ~~ B )
12 11 ad2antrr 
 |-  ( ( ( A ~< B /\ C e. B ) /\ f : A -1-1-> B ) -> -. A ~~ B )
13 vex 
 |-  f e. _V
14 dff1o5 
 |-  ( f : A -1-1-onto-> B <-> ( f : A -1-1-> B /\ ran f = B ) )
15 14 biimpri 
 |-  ( ( f : A -1-1-> B /\ ran f = B ) -> f : A -1-1-onto-> B )
16 f1oen3g 
 |-  ( ( f e. _V /\ f : A -1-1-onto-> B ) -> A ~~ B )
17 13 15 16 sylancr 
 |-  ( ( f : A -1-1-> B /\ ran f = B ) -> A ~~ B )
18 17 ex 
 |-  ( f : A -1-1-> B -> ( ran f = B -> A ~~ B ) )
19 18 necon3bd 
 |-  ( f : A -1-1-> B -> ( -. A ~~ B -> ran f =/= B ) )
20 19 adantl 
 |-  ( ( ( A ~< B /\ C e. B ) /\ f : A -1-1-> B ) -> ( -. A ~~ B -> ran f =/= B ) )
21 12 20 mpd 
 |-  ( ( ( A ~< B /\ C e. B ) /\ f : A -1-1-> B ) -> ran f =/= B )
22 pssdifn0 
 |-  ( ( ran f C_ B /\ ran f =/= B ) -> ( B \ ran f ) =/= (/) )
23 10 21 22 syl2anc 
 |-  ( ( ( A ~< B /\ C e. B ) /\ f : A -1-1-> B ) -> ( B \ ran f ) =/= (/) )
24 n0 
 |-  ( ( B \ ran f ) =/= (/) <-> E. x x e. ( B \ ran f ) )
25 23 24 sylib 
 |-  ( ( ( A ~< B /\ C e. B ) /\ f : A -1-1-> B ) -> E. x x e. ( B \ ran f ) )
26 2 brrelex1i 
 |-  ( A ~< B -> A e. _V )
27 26 ad2antrr 
 |-  ( ( ( A ~< B /\ C e. B ) /\ ( f : A -1-1-> B /\ x e. ( B \ ran f ) ) ) -> A e. _V )
28 3 ad2antrr 
 |-  ( ( ( A ~< B /\ C e. B ) /\ ( f : A -1-1-> B /\ x e. ( B \ ran f ) ) ) -> B e. _V )
29 difexg 
 |-  ( B e. _V -> ( B \ { x } ) e. _V )
30 28 29 syl 
 |-  ( ( ( A ~< B /\ C e. B ) /\ ( f : A -1-1-> B /\ x e. ( B \ ran f ) ) ) -> ( B \ { x } ) e. _V )
31 eldifn 
 |-  ( x e. ( B \ ran f ) -> -. x e. ran f )
32 disjsn 
 |-  ( ( ran f i^i { x } ) = (/) <-> -. x e. ran f )
33 31 32 sylibr 
 |-  ( x e. ( B \ ran f ) -> ( ran f i^i { x } ) = (/) )
34 33 adantl 
 |-  ( ( f : A -1-1-> B /\ x e. ( B \ ran f ) ) -> ( ran f i^i { x } ) = (/) )
35 9 adantr 
 |-  ( ( f : A -1-1-> B /\ x e. ( B \ ran f ) ) -> ran f C_ B )
36 reldisj 
 |-  ( ran f C_ B -> ( ( ran f i^i { x } ) = (/) <-> ran f C_ ( B \ { x } ) ) )
37 35 36 syl 
 |-  ( ( f : A -1-1-> B /\ x e. ( B \ ran f ) ) -> ( ( ran f i^i { x } ) = (/) <-> ran f C_ ( B \ { x } ) ) )
38 34 37 mpbid 
 |-  ( ( f : A -1-1-> B /\ x e. ( B \ ran f ) ) -> ran f C_ ( B \ { x } ) )
39 f1ssr 
 |-  ( ( f : A -1-1-> B /\ ran f C_ ( B \ { x } ) ) -> f : A -1-1-> ( B \ { x } ) )
40 38 39 syldan 
 |-  ( ( f : A -1-1-> B /\ x e. ( B \ ran f ) ) -> f : A -1-1-> ( B \ { x } ) )
41 40 adantl 
 |-  ( ( ( A ~< B /\ C e. B ) /\ ( f : A -1-1-> B /\ x e. ( B \ ran f ) ) ) -> f : A -1-1-> ( B \ { x } ) )
42 f1dom2g 
 |-  ( ( A e. _V /\ ( B \ { x } ) e. _V /\ f : A -1-1-> ( B \ { x } ) ) -> A ~<_ ( B \ { x } ) )
43 27 30 41 42 syl3anc 
 |-  ( ( ( A ~< B /\ C e. B ) /\ ( f : A -1-1-> B /\ x e. ( B \ ran f ) ) ) -> A ~<_ ( B \ { x } ) )
44 eldifi 
 |-  ( x e. ( B \ ran f ) -> x e. B )
45 44 ad2antll 
 |-  ( ( ( A ~< B /\ C e. B ) /\ ( f : A -1-1-> B /\ x e. ( B \ ran f ) ) ) -> x e. B )
46 simplr 
 |-  ( ( ( A ~< B /\ C e. B ) /\ ( f : A -1-1-> B /\ x e. ( B \ ran f ) ) ) -> C e. B )
47 difsnen 
 |-  ( ( B e. _V /\ x e. B /\ C e. B ) -> ( B \ { x } ) ~~ ( B \ { C } ) )
48 28 45 46 47 syl3anc 
 |-  ( ( ( A ~< B /\ C e. B ) /\ ( f : A -1-1-> B /\ x e. ( B \ ran f ) ) ) -> ( B \ { x } ) ~~ ( B \ { C } ) )
49 domentr 
 |-  ( ( A ~<_ ( B \ { x } ) /\ ( B \ { x } ) ~~ ( B \ { C } ) ) -> A ~<_ ( B \ { C } ) )
50 43 48 49 syl2anc 
 |-  ( ( ( A ~< B /\ C e. B ) /\ ( f : A -1-1-> B /\ x e. ( B \ ran f ) ) ) -> A ~<_ ( B \ { C } ) )
51 50 expr 
 |-  ( ( ( A ~< B /\ C e. B ) /\ f : A -1-1-> B ) -> ( x e. ( B \ ran f ) -> A ~<_ ( B \ { C } ) ) )
52 51 exlimdv 
 |-  ( ( ( A ~< B /\ C e. B ) /\ f : A -1-1-> B ) -> ( E. x x e. ( B \ ran f ) -> A ~<_ ( B \ { C } ) ) )
53 25 52 mpd 
 |-  ( ( ( A ~< B /\ C e. B ) /\ f : A -1-1-> B ) -> A ~<_ ( B \ { C } ) )
54 7 53 exlimddv 
 |-  ( ( A ~< B /\ C e. B ) -> A ~<_ ( B \ { C } ) )
55 1 adantr 
 |-  ( ( A ~< B /\ -. C e. B ) -> A ~<_ B )
56 difsn 
 |-  ( -. C e. B -> ( B \ { C } ) = B )
57 56 breq2d 
 |-  ( -. C e. B -> ( A ~<_ ( B \ { C } ) <-> A ~<_ B ) )
58 57 adantl 
 |-  ( ( A ~< B /\ -. C e. B ) -> ( A ~<_ ( B \ { C } ) <-> A ~<_ B ) )
59 55 58 mpbird 
 |-  ( ( A ~< B /\ -. C e. B ) -> A ~<_ ( B \ { C } ) )
60 54 59 pm2.61dan 
 |-  ( A ~< B -> A ~<_ ( B \ { C } ) )