Metamath Proof Explorer

Theorem fundmpss

Description: If a class F is a proper subset of a function G , then dom F C. dom G . (Contributed by Scott Fenton, 20-Apr-2011)

Ref Expression
Assertion fundmpss 
|- ( Fun G -> ( F C. G -> dom F C. dom G ) )

Proof

Step Hyp Ref Expression
1 pssss 
 |-  ( F C. G -> F C_ G )
2 dmss 
 |-  ( F C_ G -> dom F C_ dom G )
3 1 2 syl 
 |-  ( F C. G -> dom F C_ dom G )
4 3 a1i 
 |-  ( Fun G -> ( F C. G -> dom F C_ dom G ) )
5 pssdif 
 |-  ( F C. G -> ( G \ F ) =/= (/) )
6 n0 
 |-  ( ( G \ F ) =/= (/) <-> E. p p e. ( G \ F ) )
7 5 6 sylib 
 |-  ( F C. G -> E. p p e. ( G \ F ) )
8 7 adantl 
 |-  ( ( Fun G /\ F C. G ) -> E. p p e. ( G \ F ) )
9 funrel 
 |-  ( Fun G -> Rel G )
10 reldif 
 |-  ( Rel G -> Rel ( G \ F ) )
11 9 10 syl 
 |-  ( Fun G -> Rel ( G \ F ) )
12 elrel 
 |-  ( ( Rel ( G \ F ) /\ p e. ( G \ F ) ) -> E. x E. y p = <. x , y >. )
13 eleq1 
 |-  ( p = <. x , y >. -> ( p e. ( G \ F ) <-> <. x , y >. e. ( G \ F ) ) )
14 df-br 
 |-  ( x ( G \ F ) y <-> <. x , y >. e. ( G \ F ) )
15 13 14 bitr4di 
 |-  ( p = <. x , y >. -> ( p e. ( G \ F ) <-> x ( G \ F ) y ) )
16 15 biimpcd 
 |-  ( p e. ( G \ F ) -> ( p = <. x , y >. -> x ( G \ F ) y ) )
17 16 adantl 
 |-  ( ( Rel ( G \ F ) /\ p e. ( G \ F ) ) -> ( p = <. x , y >. -> x ( G \ F ) y ) )
18 17 2eximdv 
 |-  ( ( Rel ( G \ F ) /\ p e. ( G \ F ) ) -> ( E. x E. y p = <. x , y >. -> E. x E. y x ( G \ F ) y ) )
19 12 18 mpd 
 |-  ( ( Rel ( G \ F ) /\ p e. ( G \ F ) ) -> E. x E. y x ( G \ F ) y )
20 19 ex 
 |-  ( Rel ( G \ F ) -> ( p e. ( G \ F ) -> E. x E. y x ( G \ F ) y ) )
21 11 20 syl 
 |-  ( Fun G -> ( p e. ( G \ F ) -> E. x E. y x ( G \ F ) y ) )
22 21 adantr 
 |-  ( ( Fun G /\ F C. G ) -> ( p e. ( G \ F ) -> E. x E. y x ( G \ F ) y ) )
23 difss 
 |-  ( G \ F ) C_ G
24 23 ssbri 
 |-  ( x ( G \ F ) y -> x G y )
25 24 eximi 
 |-  ( E. y x ( G \ F ) y -> E. y x G y )
26 25 a1i 
 |-  ( ( Fun G /\ F C. G ) -> ( E. y x ( G \ F ) y -> E. y x G y ) )
27 brdif 
 |-  ( x ( G \ F ) y <-> ( x G y /\ -. x F y ) )
28 27 simprbi 
 |-  ( x ( G \ F ) y -> -. x F y )
29 28 adantl 
 |-  ( ( ( Fun G /\ F C. G ) /\ x ( G \ F ) y ) -> -. x F y )
30 1 ssbrd 
 |-  ( F C. G -> ( x F z -> x G z ) )
31 30 ad2antlr 
 |-  ( ( ( Fun G /\ F C. G ) /\ x ( G \ F ) y ) -> ( x F z -> x G z ) )
32 dffun2 
 |-  ( Fun G <-> ( Rel G /\ A. x A. y A. z ( ( x G y /\ x G z ) -> y = z ) ) )
33 32 simprbi 
 |-  ( Fun G -> A. x A. y A. z ( ( x G y /\ x G z ) -> y = z ) )
34 2sp 
 |-  ( A. y A. z ( ( x G y /\ x G z ) -> y = z ) -> ( ( x G y /\ x G z ) -> y = z ) )
35 34 sps 
 |-  ( A. x A. y A. z ( ( x G y /\ x G z ) -> y = z ) -> ( ( x G y /\ x G z ) -> y = z ) )
36 33 35 syl 
 |-  ( Fun G -> ( ( x G y /\ x G z ) -> y = z ) )
37 breq2 
 |-  ( y = z -> ( x F y <-> x F z ) )
38 37 biimprd 
 |-  ( y = z -> ( x F z -> x F y ) )
39 36 38 syl6 
 |-  ( Fun G -> ( ( x G y /\ x G z ) -> ( x F z -> x F y ) ) )
40 39 expd 
 |-  ( Fun G -> ( x G y -> ( x G z -> ( x F z -> x F y ) ) ) )
41 27 simplbi 
 |-  ( x ( G \ F ) y -> x G y )
42 40 41 impel 
 |-  ( ( Fun G /\ x ( G \ F ) y ) -> ( x G z -> ( x F z -> x F y ) ) )
43 42 adantlr 
 |-  ( ( ( Fun G /\ F C. G ) /\ x ( G \ F ) y ) -> ( x G z -> ( x F z -> x F y ) ) )
44 43 com23 
 |-  ( ( ( Fun G /\ F C. G ) /\ x ( G \ F ) y ) -> ( x F z -> ( x G z -> x F y ) ) )
45 31 44 mpdd 
 |-  ( ( ( Fun G /\ F C. G ) /\ x ( G \ F ) y ) -> ( x F z -> x F y ) )
46 45 exlimdv 
 |-  ( ( ( Fun G /\ F C. G ) /\ x ( G \ F ) y ) -> ( E. z x F z -> x F y ) )
47 29 46 mtod 
 |-  ( ( ( Fun G /\ F C. G ) /\ x ( G \ F ) y ) -> -. E. z x F z )
48 47 ex 
 |-  ( ( Fun G /\ F C. G ) -> ( x ( G \ F ) y -> -. E. z x F z ) )
49 48 exlimdv 
 |-  ( ( Fun G /\ F C. G ) -> ( E. y x ( G \ F ) y -> -. E. z x F z ) )
50 26 49 jcad 
 |-  ( ( Fun G /\ F C. G ) -> ( E. y x ( G \ F ) y -> ( E. y x G y /\ -. E. z x F z ) ) )
51 50 eximdv 
 |-  ( ( Fun G /\ F C. G ) -> ( E. x E. y x ( G \ F ) y -> E. x ( E. y x G y /\ -. E. z x F z ) ) )
52 22 51 syld 
 |-  ( ( Fun G /\ F C. G ) -> ( p e. ( G \ F ) -> E. x ( E. y x G y /\ -. E. z x F z ) ) )
53 52 exlimdv 
 |-  ( ( Fun G /\ F C. G ) -> ( E. p p e. ( G \ F ) -> E. x ( E. y x G y /\ -. E. z x F z ) ) )
54 8 53 mpd 
 |-  ( ( Fun G /\ F C. G ) -> E. x ( E. y x G y /\ -. E. z x F z ) )
55 nss 
 |-  ( -. dom G C_ dom F <-> E. x ( x e. dom G /\ -. x e. dom F ) )
56 vex 
 |-  x e. _V
57 56 eldm 
 |-  ( x e. dom G <-> E. y x G y )
58 56 eldm 
 |-  ( x e. dom F <-> E. z x F z )
59 58 notbii 
 |-  ( -. x e. dom F <-> -. E. z x F z )
60 57 59 anbi12i 
 |-  ( ( x e. dom G /\ -. x e. dom F ) <-> ( E. y x G y /\ -. E. z x F z ) )
61 60 exbii 
 |-  ( E. x ( x e. dom G /\ -. x e. dom F ) <-> E. x ( E. y x G y /\ -. E. z x F z ) )
62 55 61 bitri 
 |-  ( -. dom G C_ dom F <-> E. x ( E. y x G y /\ -. E. z x F z ) )
63 54 62 sylibr 
 |-  ( ( Fun G /\ F C. G ) -> -. dom G C_ dom F )
64 63 ex 
 |-  ( Fun G -> ( F C. G -> -. dom G C_ dom F ) )
65 4 64 jcad 
 |-  ( Fun G -> ( F C. G -> ( dom F C_ dom G /\ -. dom G C_ dom F ) ) )
66 dfpss3 
 |-  ( dom F C. dom G <-> ( dom F C_ dom G /\ -. dom G C_ dom F ) )
67 65 66 syl6ibr 
 |-  ( Fun G -> ( F C. G -> dom F C. dom G ) )