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 28 difexd 
 |-  ( ( ( A ~< B /\ C e. B ) /\ ( f : A -1-1-> B /\ x e. ( B \ ran f ) ) ) -> ( B \ { x } ) e. _V )
30 eldifn 
 |-  ( x e. ( B \ ran f ) -> -. x e. ran f )
31 disjsn 
 |-  ( ( ran f i^i { x } ) = (/) <-> -. x e. ran f )
32 30 31 sylibr 
 |-  ( x e. ( B \ ran f ) -> ( ran f i^i { x } ) = (/) )
33 32 adantl 
 |-  ( ( f : A -1-1-> B /\ x e. ( B \ ran f ) ) -> ( ran f i^i { x } ) = (/) )
34 9 adantr 
 |-  ( ( f : A -1-1-> B /\ x e. ( B \ ran f ) ) -> ran f C_ B )
35 reldisj 
 |-  ( ran f C_ B -> ( ( ran f i^i { x } ) = (/) <-> ran f C_ ( B \ { x } ) ) )
36 34 35 syl 
 |-  ( ( f : A -1-1-> B /\ x e. ( B \ ran f ) ) -> ( ( ran f i^i { x } ) = (/) <-> ran f C_ ( B \ { x } ) ) )
37 33 36 mpbid 
 |-  ( ( f : A -1-1-> B /\ x e. ( B \ ran f ) ) -> ran f C_ ( B \ { x } ) )
38 f1ssr 
 |-  ( ( f : A -1-1-> B /\ ran f C_ ( B \ { x } ) ) -> f : A -1-1-> ( B \ { x } ) )
39 37 38 syldan 
 |-  ( ( f : A -1-1-> B /\ x e. ( B \ ran f ) ) -> f : A -1-1-> ( B \ { x } ) )
40 39 adantl 
 |-  ( ( ( A ~< B /\ C e. B ) /\ ( f : A -1-1-> B /\ x e. ( B \ ran f ) ) ) -> f : A -1-1-> ( B \ { x } ) )
41 f1dom2g 
 |-  ( ( A e. _V /\ ( B \ { x } ) e. _V /\ f : A -1-1-> ( B \ { x } ) ) -> A ~<_ ( B \ { x } ) )
42 27 29 40 41 syl3anc 
 |-  ( ( ( A ~< B /\ C e. B ) /\ ( f : A -1-1-> B /\ x e. ( B \ ran f ) ) ) -> A ~<_ ( B \ { x } ) )
43 eldifi 
 |-  ( x e. ( B \ ran f ) -> x e. B )
44 43 ad2antll 
 |-  ( ( ( A ~< B /\ C e. B ) /\ ( f : A -1-1-> B /\ x e. ( B \ ran f ) ) ) -> x e. B )
45 simplr 
 |-  ( ( ( A ~< B /\ C e. B ) /\ ( f : A -1-1-> B /\ x e. ( B \ ran f ) ) ) -> C e. B )
46 difsnen 
 |-  ( ( B e. _V /\ x e. B /\ C e. B ) -> ( B \ { x } ) ~~ ( B \ { C } ) )
47 28 44 45 46 syl3anc 
 |-  ( ( ( A ~< B /\ C e. B ) /\ ( f : A -1-1-> B /\ x e. ( B \ ran f ) ) ) -> ( B \ { x } ) ~~ ( B \ { C } ) )
48 domentr 
 |-  ( ( A ~<_ ( B \ { x } ) /\ ( B \ { x } ) ~~ ( B \ { C } ) ) -> A ~<_ ( B \ { C } ) )
49 42 47 48 syl2anc 
 |-  ( ( ( A ~< B /\ C e. B ) /\ ( f : A -1-1-> B /\ x e. ( B \ ran f ) ) ) -> A ~<_ ( B \ { C } ) )
50 49 expr 
 |-  ( ( ( A ~< B /\ C e. B ) /\ f : A -1-1-> B ) -> ( x e. ( B \ ran f ) -> A ~<_ ( B \ { C } ) ) )
51 50 exlimdv 
 |-  ( ( ( A ~< B /\ C e. B ) /\ f : A -1-1-> B ) -> ( E. x x e. ( B \ ran f ) -> A ~<_ ( B \ { C } ) ) )
52 25 51 mpd 
 |-  ( ( ( A ~< B /\ C e. B ) /\ f : A -1-1-> B ) -> A ~<_ ( B \ { C } ) )
53 7 52 exlimddv 
 |-  ( ( A ~< B /\ C e. B ) -> A ~<_ ( B \ { C } ) )
54 1 adantr 
 |-  ( ( A ~< B /\ -. C e. B ) -> A ~<_ B )
55 difsn 
 |-  ( -. C e. B -> ( B \ { C } ) = B )
56 55 breq2d 
 |-  ( -. C e. B -> ( A ~<_ ( B \ { C } ) <-> A ~<_ B ) )
57 56 adantl 
 |-  ( ( A ~< B /\ -. C e. B ) -> ( A ~<_ ( B \ { C } ) <-> A ~<_ B ) )
58 54 57 mpbird 
 |-  ( ( A ~< B /\ -. C e. B ) -> A ~<_ ( B \ { C } ) )
59 53 58 pm2.61dan 
 |-  ( A ~< B -> A ~<_ ( B \ { C } ) )