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 𝐺 → ( 𝐹 ⊊ 𝐺 → dom 𝐹 ⊊ dom 𝐺 ) )

Proof

Step Hyp Ref Expression
1 pssss ⊢ ( 𝐹 ⊊ 𝐺 → 𝐹 ⊆ 𝐺 )
2 dmss ⊢ ( 𝐹 ⊆ 𝐺 → dom 𝐹 ⊆ dom 𝐺 )
3 1 2 syl ⊢ ( 𝐹 ⊊ 𝐺 → dom 𝐹 ⊆ dom 𝐺 )
4 3 a1i ⊢ ( Fun 𝐺 → ( 𝐹 ⊊ 𝐺 → dom 𝐹 ⊆ dom 𝐺 ) )
5 pssdif ⊢ ( 𝐹 ⊊ 𝐺 → ( 𝐺 ∖ 𝐹 ) ≠ ∅ )
6 n0 ⊢ ( ( 𝐺 ∖ 𝐹 ) ≠ ∅ ↔ ∃ 𝑝 𝑝 ∈ ( 𝐺 ∖ 𝐹 ) )
7 5 6 sylib ⊢ ( 𝐹 ⊊ 𝐺 → ∃ 𝑝 𝑝 ∈ ( 𝐺 ∖ 𝐹 ) )
8 7 adantl ⊢ ( ( Fun 𝐺 ∧ 𝐹 ⊊ 𝐺 ) → ∃ 𝑝 𝑝 ∈ ( 𝐺 ∖ 𝐹 ) )
9 funrel ⊢ ( Fun 𝐺 → Rel 𝐺 )
10 reldif ⊢ ( Rel 𝐺 → Rel ( 𝐺 ∖ 𝐹 ) )
11 9 10 syl ⊢ ( Fun 𝐺 → Rel ( 𝐺 ∖ 𝐹 ) )
12 elrel ⊢ ( ( Rel ( 𝐺 ∖ 𝐹 ) ∧ 𝑝 ∈ ( 𝐺 ∖ 𝐹 ) ) → ∃ 𝑥 ∃ 𝑦 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ )
13 eleq1 ⊢ ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑝 ∈ ( 𝐺 ∖ 𝐹 ) ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐺 ∖ 𝐹 ) ) )
14 df-br ⊢ ( 𝑥 ( 𝐺 ∖ 𝐹 ) 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐺 ∖ 𝐹 ) )
15 13 14 bitr4di ⊢ ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑝 ∈ ( 𝐺 ∖ 𝐹 ) ↔ 𝑥 ( 𝐺 ∖ 𝐹 ) 𝑦 ) )
16 15 biimpcd ⊢ ( 𝑝 ∈ ( 𝐺 ∖ 𝐹 ) → ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ → 𝑥 ( 𝐺 ∖ 𝐹 ) 𝑦 ) )
17 16 adantl ⊢ ( ( Rel ( 𝐺 ∖ 𝐹 ) ∧ 𝑝 ∈ ( 𝐺 ∖ 𝐹 ) ) → ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ → 𝑥 ( 𝐺 ∖ 𝐹 ) 𝑦 ) )
18 17 2eximdv ⊢ ( ( Rel ( 𝐺 ∖ 𝐹 ) ∧ 𝑝 ∈ ( 𝐺 ∖ 𝐹 ) ) → ( ∃ 𝑥 ∃ 𝑦 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ → ∃ 𝑥 ∃ 𝑦 𝑥 ( 𝐺 ∖ 𝐹 ) 𝑦 ) )
19 12 18 mpd ⊢ ( ( Rel ( 𝐺 ∖ 𝐹 ) ∧ 𝑝 ∈ ( 𝐺 ∖ 𝐹 ) ) → ∃ 𝑥 ∃ 𝑦 𝑥 ( 𝐺 ∖ 𝐹 ) 𝑦 )
20 19 ex ⊢ ( Rel ( 𝐺 ∖ 𝐹 ) → ( 𝑝 ∈ ( 𝐺 ∖ 𝐹 ) → ∃ 𝑥 ∃ 𝑦 𝑥 ( 𝐺 ∖ 𝐹 ) 𝑦 ) )
21 11 20 syl ⊢ ( Fun 𝐺 → ( 𝑝 ∈ ( 𝐺 ∖ 𝐹 ) → ∃ 𝑥 ∃ 𝑦 𝑥 ( 𝐺 ∖ 𝐹 ) 𝑦 ) )
22 21 adantr ⊢ ( ( Fun 𝐺 ∧ 𝐹 ⊊ 𝐺 ) → ( 𝑝 ∈ ( 𝐺 ∖ 𝐹 ) → ∃ 𝑥 ∃ 𝑦 𝑥 ( 𝐺 ∖ 𝐹 ) 𝑦 ) )
23 difss ⊢ ( 𝐺 ∖ 𝐹 ) ⊆ 𝐺
24 23 ssbri ⊢ ( 𝑥 ( 𝐺 ∖ 𝐹 ) 𝑦 → 𝑥 𝐺 𝑦 )
25 24 eximi ⊢ ( ∃ 𝑦 𝑥 ( 𝐺 ∖ 𝐹 ) 𝑦 → ∃ 𝑦 𝑥 𝐺 𝑦 )
26 25 a1i ⊢ ( ( Fun 𝐺 ∧ 𝐹 ⊊ 𝐺 ) → ( ∃ 𝑦 𝑥 ( 𝐺 ∖ 𝐹 ) 𝑦 → ∃ 𝑦 𝑥 𝐺 𝑦 ) )
27 brdif ⊢ ( 𝑥 ( 𝐺 ∖ 𝐹 ) 𝑦 ↔ ( 𝑥 𝐺 𝑦 ∧ ¬ 𝑥 𝐹 𝑦 ) )
28 27 simprbi ⊢ ( 𝑥 ( 𝐺 ∖ 𝐹 ) 𝑦 → ¬ 𝑥 𝐹 𝑦 )
29 28 adantl ⊢ ( ( ( Fun 𝐺 ∧ 𝐹 ⊊ 𝐺 ) ∧ 𝑥 ( 𝐺 ∖ 𝐹 ) 𝑦 ) → ¬ 𝑥 𝐹 𝑦 )
30 1 ssbrd ⊢ ( 𝐹 ⊊ 𝐺 → ( 𝑥 𝐹 𝑧 → 𝑥 𝐺 𝑧 ) )
31 30 ad2antlr ⊢ ( ( ( Fun 𝐺 ∧ 𝐹 ⊊ 𝐺 ) ∧ 𝑥 ( 𝐺 ∖ 𝐹 ) 𝑦 ) → ( 𝑥 𝐹 𝑧 → 𝑥 𝐺 𝑧 ) )
32 dffun2 ⊢ ( Fun 𝐺 ↔ ( Rel 𝐺 ∧ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 𝐺 𝑦 ∧ 𝑥 𝐺 𝑧 ) → 𝑦 = 𝑧 ) ) )
33 32 simprbi ⊢ ( Fun 𝐺 → ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 𝐺 𝑦 ∧ 𝑥 𝐺 𝑧 ) → 𝑦 = 𝑧 ) )
34 2sp ⊢ ( ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 𝐺 𝑦 ∧ 𝑥 𝐺 𝑧 ) → 𝑦 = 𝑧 ) → ( ( 𝑥 𝐺 𝑦 ∧ 𝑥 𝐺 𝑧 ) → 𝑦 = 𝑧 ) )
35 34 sps ⊢ ( ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 𝐺 𝑦 ∧ 𝑥 𝐺 𝑧 ) → 𝑦 = 𝑧 ) → ( ( 𝑥 𝐺 𝑦 ∧ 𝑥 𝐺 𝑧 ) → 𝑦 = 𝑧 ) )
36 33 35 syl ⊢ ( Fun 𝐺 → ( ( 𝑥 𝐺 𝑦 ∧ 𝑥 𝐺 𝑧 ) → 𝑦 = 𝑧 ) )
37 breq2 ⊢ ( 𝑦 = 𝑧 → ( 𝑥 𝐹 𝑦 ↔ 𝑥 𝐹 𝑧 ) )
38 37 biimprd ⊢ ( 𝑦 = 𝑧 → ( 𝑥 𝐹 𝑧 → 𝑥 𝐹 𝑦 ) )
39 36 38 syl6 ⊢ ( Fun 𝐺 → ( ( 𝑥 𝐺 𝑦 ∧ 𝑥 𝐺 𝑧 ) → ( 𝑥 𝐹 𝑧 → 𝑥 𝐹 𝑦 ) ) )
40 39 expd ⊢ ( Fun 𝐺 → ( 𝑥 𝐺 𝑦 → ( 𝑥 𝐺 𝑧 → ( 𝑥 𝐹 𝑧 → 𝑥 𝐹 𝑦 ) ) ) )
41 27 simplbi ⊢ ( 𝑥 ( 𝐺 ∖ 𝐹 ) 𝑦 → 𝑥 𝐺 𝑦 )
42 40 41 impel ⊢ ( ( Fun 𝐺 ∧ 𝑥 ( 𝐺 ∖ 𝐹 ) 𝑦 ) → ( 𝑥 𝐺 𝑧 → ( 𝑥 𝐹 𝑧 → 𝑥 𝐹 𝑦 ) ) )
43 42 adantlr ⊢ ( ( ( Fun 𝐺 ∧ 𝐹 ⊊ 𝐺 ) ∧ 𝑥 ( 𝐺 ∖ 𝐹 ) 𝑦 ) → ( 𝑥 𝐺 𝑧 → ( 𝑥 𝐹 𝑧 → 𝑥 𝐹 𝑦 ) ) )
44 43 com23 ⊢ ( ( ( Fun 𝐺 ∧ 𝐹 ⊊ 𝐺 ) ∧ 𝑥 ( 𝐺 ∖ 𝐹 ) 𝑦 ) → ( 𝑥 𝐹 𝑧 → ( 𝑥 𝐺 𝑧 → 𝑥 𝐹 𝑦 ) ) )
45 31 44 mpdd ⊢ ( ( ( Fun 𝐺 ∧ 𝐹 ⊊ 𝐺 ) ∧ 𝑥 ( 𝐺 ∖ 𝐹 ) 𝑦 ) → ( 𝑥 𝐹 𝑧 → 𝑥 𝐹 𝑦 ) )
46 45 exlimdv ⊢ ( ( ( Fun 𝐺 ∧ 𝐹 ⊊ 𝐺 ) ∧ 𝑥 ( 𝐺 ∖ 𝐹 ) 𝑦 ) → ( ∃ 𝑧 𝑥 𝐹 𝑧 → 𝑥 𝐹 𝑦 ) )
47 29 46 mtod ⊢ ( ( ( Fun 𝐺 ∧ 𝐹 ⊊ 𝐺 ) ∧ 𝑥 ( 𝐺 ∖ 𝐹 ) 𝑦 ) → ¬ ∃ 𝑧 𝑥 𝐹 𝑧 )
48 47 ex ⊢ ( ( Fun 𝐺 ∧ 𝐹 ⊊ 𝐺 ) → ( 𝑥 ( 𝐺 ∖ 𝐹 ) 𝑦 → ¬ ∃ 𝑧 𝑥 𝐹 𝑧 ) )
49 48 exlimdv ⊢ ( ( Fun 𝐺 ∧ 𝐹 ⊊ 𝐺 ) → ( ∃ 𝑦 𝑥 ( 𝐺 ∖ 𝐹 ) 𝑦 → ¬ ∃ 𝑧 𝑥 𝐹 𝑧 ) )
50 26 49 jcad ⊢ ( ( Fun 𝐺 ∧ 𝐹 ⊊ 𝐺 ) → ( ∃ 𝑦 𝑥 ( 𝐺 ∖ 𝐹 ) 𝑦 → ( ∃ 𝑦 𝑥 𝐺 𝑦 ∧ ¬ ∃ 𝑧 𝑥 𝐹 𝑧 ) ) )
51 50 eximdv ⊢ ( ( Fun 𝐺 ∧ 𝐹 ⊊ 𝐺 ) → ( ∃ 𝑥 ∃ 𝑦 𝑥 ( 𝐺 ∖ 𝐹 ) 𝑦 → ∃ 𝑥 ( ∃ 𝑦 𝑥 𝐺 𝑦 ∧ ¬ ∃ 𝑧 𝑥 𝐹 𝑧 ) ) )
52 22 51 syld ⊢ ( ( Fun 𝐺 ∧ 𝐹 ⊊ 𝐺 ) → ( 𝑝 ∈ ( 𝐺 ∖ 𝐹 ) → ∃ 𝑥 ( ∃ 𝑦 𝑥 𝐺 𝑦 ∧ ¬ ∃ 𝑧 𝑥 𝐹 𝑧 ) ) )
53 52 exlimdv ⊢ ( ( Fun 𝐺 ∧ 𝐹 ⊊ 𝐺 ) → ( ∃ 𝑝 𝑝 ∈ ( 𝐺 ∖ 𝐹 ) → ∃ 𝑥 ( ∃ 𝑦 𝑥 𝐺 𝑦 ∧ ¬ ∃ 𝑧 𝑥 𝐹 𝑧 ) ) )
54 8 53 mpd ⊢ ( ( Fun 𝐺 ∧ 𝐹 ⊊ 𝐺 ) → ∃ 𝑥 ( ∃ 𝑦 𝑥 𝐺 𝑦 ∧ ¬ ∃ 𝑧 𝑥 𝐹 𝑧 ) )
55 nss ⊢ ( ¬ dom 𝐺 ⊆ dom 𝐹 ↔ ∃ 𝑥 ( 𝑥 ∈ dom 𝐺 ∧ ¬ 𝑥 ∈ dom 𝐹 ) )
56 vex ⊢ 𝑥 ∈ V
57 56 eldm ⊢ ( 𝑥 ∈ dom 𝐺 ↔ ∃ 𝑦 𝑥 𝐺 𝑦 )
58 56 eldm ⊢ ( 𝑥 ∈ dom 𝐹 ↔ ∃ 𝑧 𝑥 𝐹 𝑧 )
59 58 notbii ⊢ ( ¬ 𝑥 ∈ dom 𝐹 ↔ ¬ ∃ 𝑧 𝑥 𝐹 𝑧 )
60 57 59 anbi12i ⊢ ( ( 𝑥 ∈ dom 𝐺 ∧ ¬ 𝑥 ∈ dom 𝐹 ) ↔ ( ∃ 𝑦 𝑥 𝐺 𝑦 ∧ ¬ ∃ 𝑧 𝑥 𝐹 𝑧 ) )
61 60 exbii ⊢ ( ∃ 𝑥 ( 𝑥 ∈ dom 𝐺 ∧ ¬ 𝑥 ∈ dom 𝐹 ) ↔ ∃ 𝑥 ( ∃ 𝑦 𝑥 𝐺 𝑦 ∧ ¬ ∃ 𝑧 𝑥 𝐹 𝑧 ) )
62 55 61 bitri ⊢ ( ¬ dom 𝐺 ⊆ dom 𝐹 ↔ ∃ 𝑥 ( ∃ 𝑦 𝑥 𝐺 𝑦 ∧ ¬ ∃ 𝑧 𝑥 𝐹 𝑧 ) )
63 54 62 sylibr ⊢ ( ( Fun 𝐺 ∧ 𝐹 ⊊ 𝐺 ) → ¬ dom 𝐺 ⊆ dom 𝐹 )
64 63 ex ⊢ ( Fun 𝐺 → ( 𝐹 ⊊ 𝐺 → ¬ dom 𝐺 ⊆ dom 𝐹 ) )
65 4 64 jcad ⊢ ( Fun 𝐺 → ( 𝐹 ⊊ 𝐺 → ( dom 𝐹 ⊆ dom 𝐺 ∧ ¬ dom 𝐺 ⊆ dom 𝐹 ) ) )
66 dfpss3 ⊢ ( dom 𝐹 ⊊ dom 𝐺 ↔ ( dom 𝐹 ⊆ dom 𝐺 ∧ ¬ dom 𝐺 ⊆ dom 𝐹 ) )
67 65 66 syl6ibr ⊢ ( Fun 𝐺 → ( 𝐹 ⊊ 𝐺 → dom 𝐹 ⊊ dom 𝐺 ) )