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 } ) )