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 G dom F dom G

Proof

Step Hyp Ref Expression
1 pssss F G F G
2 dmss F G dom F dom G
3 1 2 syl F G dom F dom G
4 3 a1i Fun G F G dom F dom G
5 pssdif F G G F
6 n0 G F p p G F
7 5 6 sylib F G p p G F
8 7 adantl Fun G F G p p 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 G F x y p = x y
13 eleq1 p = x y p G F x y G F
14 df-br x G F y x y G F
15 13 14 bitr4di p = x y p G F x G F y
16 15 biimpcd p G F p = x y x G F y
17 16 adantl Rel G F p G F p = x y x G F y
18 17 2eximdv Rel G F p G F x y p = x y x y x G F y
19 12 18 mpd Rel G F p G F x y x G F y
20 19 ex Rel G F p G F x y x G F y
21 11 20 syl Fun G p G F x y x G F y
22 21 adantr Fun G F G p G F x y x G F y
23 difss G F G
24 23 ssbri x G F y x G y
25 24 eximi y x G F y y x G y
26 25 a1i Fun G F G y x G F y 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 G x G F y ¬ x F y
30 1 ssbrd F G x F z x G z
31 30 ad2antlr Fun G F G x G F y x F z x G z
32 dffun2 Fun G Rel G x y z x G y x G z y = z
33 32 simprbi Fun G x y z x G y x G z y = z
34 2sp y z x G y x G z y = z x G y x G z y = z
35 34 sps x y 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 G x G F y x G z x F z x F y
44 43 com23 Fun G F G x G F y x F z x G z x F y
45 31 44 mpdd Fun G F G x G F y x F z x F y
46 45 exlimdv Fun G F G x G F y z x F z x F y
47 29 46 mtod Fun G F G x G F y ¬ z x F z
48 47 ex Fun G F G x G F y ¬ z x F z
49 48 exlimdv Fun G F G y x G F y ¬ z x F z
50 26 49 jcad Fun G F G y x G F y y x G y ¬ z x F z
51 50 eximdv Fun G F G x y x G F y x y x G y ¬ z x F z
52 22 51 syld Fun G F G p G F x y x G y ¬ z x F z
53 52 exlimdv Fun G F G p p G F x y x G y ¬ z x F z
54 8 53 mpd Fun G F G x y x G y ¬ z x F z
55 nss ¬ dom G dom F x x dom G ¬ x dom F
56 vex x V
57 56 eldm x dom G y x G y
58 56 eldm x dom F z x F z
59 58 notbii ¬ x dom F ¬ z x F z
60 57 59 anbi12i x dom G ¬ x dom F y x G y ¬ z x F z
61 60 exbii x x dom G ¬ x dom F x y x G y ¬ z x F z
62 55 61 bitri ¬ dom G dom F x y x G y ¬ z x F z
63 54 62 sylibr Fun G F G ¬ dom G dom F
64 63 ex Fun G F G ¬ dom G dom F
65 4 64 jcad Fun G F G dom F dom G ¬ dom G dom F
66 dfpss3 dom F dom G dom F dom G ¬ dom G dom F
67 65 66 syl6ibr Fun G F G dom F dom G