Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  fundmpss Structured version   Visualization version   GIF version

Theorem fundmpss 31996
Description: If a class 𝐹 is a proper subset of a function 𝐺, then dom 𝐹 ⊊ dom 𝐺. (Contributed by Scott Fenton, 20-Apr-2011.)
Assertion
Ref Expression
fundmpss (Fun 𝐺 → (𝐹𝐺 → dom 𝐹 ⊊ dom 𝐺))

Proof of Theorem fundmpss
Dummy variables 𝑝 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 pssss 3850 . . . . 5 (𝐹𝐺𝐹𝐺)
2 dmss 5461 . . . . 5 (𝐹𝐺 → dom 𝐹 ⊆ dom 𝐺)
31, 2syl 17 . . . 4 (𝐹𝐺 → dom 𝐹 ⊆ dom 𝐺)
43a1i 11 . . 3 (Fun 𝐺 → (𝐹𝐺 → dom 𝐹 ⊆ dom 𝐺))
5 pssdif 4090 . . . . . . . 8 (𝐹𝐺 → (𝐺𝐹) ≠ ∅)
6 n0 4076 . . . . . . . 8 ((𝐺𝐹) ≠ ∅ ↔ ∃𝑝 𝑝 ∈ (𝐺𝐹))
75, 6sylib 208 . . . . . . 7 (𝐹𝐺 → ∃𝑝 𝑝 ∈ (𝐺𝐹))
87adantl 467 . . . . . 6 ((Fun 𝐺𝐹𝐺) → ∃𝑝 𝑝 ∈ (𝐺𝐹))
9 funrel 6048 . . . . . . . . . . 11 (Fun 𝐺 → Rel 𝐺)
10 reldif 5377 . . . . . . . . . . 11 (Rel 𝐺 → Rel (𝐺𝐹))
119, 10syl 17 . . . . . . . . . 10 (Fun 𝐺 → Rel (𝐺𝐹))
12 elrel 5362 . . . . . . . . . . . 12 ((Rel (𝐺𝐹) ∧ 𝑝 ∈ (𝐺𝐹)) → ∃𝑥𝑦 𝑝 = ⟨𝑥, 𝑦⟩)
13 eleq1 2837 . . . . . . . . . . . . . . . 16 (𝑝 = ⟨𝑥, 𝑦⟩ → (𝑝 ∈ (𝐺𝐹) ↔ ⟨𝑥, 𝑦⟩ ∈ (𝐺𝐹)))
14 df-br 4785 . . . . . . . . . . . . . . . 16 (𝑥(𝐺𝐹)𝑦 ↔ ⟨𝑥, 𝑦⟩ ∈ (𝐺𝐹))
1513, 14syl6bbr 278 . . . . . . . . . . . . . . 15 (𝑝 = ⟨𝑥, 𝑦⟩ → (𝑝 ∈ (𝐺𝐹) ↔ 𝑥(𝐺𝐹)𝑦))
1615biimpcd 239 . . . . . . . . . . . . . 14 (𝑝 ∈ (𝐺𝐹) → (𝑝 = ⟨𝑥, 𝑦⟩ → 𝑥(𝐺𝐹)𝑦))
1716adantl 467 . . . . . . . . . . . . 13 ((Rel (𝐺𝐹) ∧ 𝑝 ∈ (𝐺𝐹)) → (𝑝 = ⟨𝑥, 𝑦⟩ → 𝑥(𝐺𝐹)𝑦))
18172eximdv 1999 . . . . . . . . . . . 12 ((Rel (𝐺𝐹) ∧ 𝑝 ∈ (𝐺𝐹)) → (∃𝑥𝑦 𝑝 = ⟨𝑥, 𝑦⟩ → ∃𝑥𝑦 𝑥(𝐺𝐹)𝑦))
1912, 18mpd 15 . . . . . . . . . . 11 ((Rel (𝐺𝐹) ∧ 𝑝 ∈ (𝐺𝐹)) → ∃𝑥𝑦 𝑥(𝐺𝐹)𝑦)
2019ex 397 . . . . . . . . . 10 (Rel (𝐺𝐹) → (𝑝 ∈ (𝐺𝐹) → ∃𝑥𝑦 𝑥(𝐺𝐹)𝑦))
2111, 20syl 17 . . . . . . . . 9 (Fun 𝐺 → (𝑝 ∈ (𝐺𝐹) → ∃𝑥𝑦 𝑥(𝐺𝐹)𝑦))
2221adantr 466 . . . . . . . 8 ((Fun 𝐺𝐹𝐺) → (𝑝 ∈ (𝐺𝐹) → ∃𝑥𝑦 𝑥(𝐺𝐹)𝑦))
23 difss 3886 . . . . . . . . . . . . 13 (𝐺𝐹) ⊆ 𝐺
2423ssbri 4829 . . . . . . . . . . . 12 (𝑥(𝐺𝐹)𝑦𝑥𝐺𝑦)
2524eximi 1909 . . . . . . . . . . 11 (∃𝑦 𝑥(𝐺𝐹)𝑦 → ∃𝑦 𝑥𝐺𝑦)
2625a1i 11 . . . . . . . . . 10 ((Fun 𝐺𝐹𝐺) → (∃𝑦 𝑥(𝐺𝐹)𝑦 → ∃𝑦 𝑥𝐺𝑦))
27 brdif 4837 . . . . . . . . . . . . . . 15 (𝑥(𝐺𝐹)𝑦 ↔ (𝑥𝐺𝑦 ∧ ¬ 𝑥𝐹𝑦))
2827simprbi 478 . . . . . . . . . . . . . 14 (𝑥(𝐺𝐹)𝑦 → ¬ 𝑥𝐹𝑦)
2928adantl 467 . . . . . . . . . . . . 13 (((Fun 𝐺𝐹𝐺) ∧ 𝑥(𝐺𝐹)𝑦) → ¬ 𝑥𝐹𝑦)
301ssbrd 4827 . . . . . . . . . . . . . . . 16 (𝐹𝐺 → (𝑥𝐹𝑧𝑥𝐺𝑧))
3130ad2antlr 698 . . . . . . . . . . . . . . 15 (((Fun 𝐺𝐹𝐺) ∧ 𝑥(𝐺𝐹)𝑦) → (𝑥𝐹𝑧𝑥𝐺𝑧))
3227simplbi 479 . . . . . . . . . . . . . . . . . . 19 (𝑥(𝐺𝐹)𝑦𝑥𝐺𝑦)
33 dffun2 6041 . . . . . . . . . . . . . . . . . . . . . . 23 (Fun 𝐺 ↔ (Rel 𝐺 ∧ ∀𝑥𝑦𝑧((𝑥𝐺𝑦𝑥𝐺𝑧) → 𝑦 = 𝑧)))
3433simprbi 478 . . . . . . . . . . . . . . . . . . . . . 22 (Fun 𝐺 → ∀𝑥𝑦𝑧((𝑥𝐺𝑦𝑥𝐺𝑧) → 𝑦 = 𝑧))
35 2sp 2209 . . . . . . . . . . . . . . . . . . . . . . 23 (∀𝑦𝑧((𝑥𝐺𝑦𝑥𝐺𝑧) → 𝑦 = 𝑧) → ((𝑥𝐺𝑦𝑥𝐺𝑧) → 𝑦 = 𝑧))
3635sps 2208 . . . . . . . . . . . . . . . . . . . . . 22 (∀𝑥𝑦𝑧((𝑥𝐺𝑦𝑥𝐺𝑧) → 𝑦 = 𝑧) → ((𝑥𝐺𝑦𝑥𝐺𝑧) → 𝑦 = 𝑧))
3734, 36syl 17 . . . . . . . . . . . . . . . . . . . . 21 (Fun 𝐺 → ((𝑥𝐺𝑦𝑥𝐺𝑧) → 𝑦 = 𝑧))
38 breq2 4788 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 = 𝑧 → (𝑥𝐹𝑦𝑥𝐹𝑧))
3938biimprd 238 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 = 𝑧 → (𝑥𝐹𝑧𝑥𝐹𝑦))
4037, 39syl6 35 . . . . . . . . . . . . . . . . . . . 20 (Fun 𝐺 → ((𝑥𝐺𝑦𝑥𝐺𝑧) → (𝑥𝐹𝑧𝑥𝐹𝑦)))
4140expd 400 . . . . . . . . . . . . . . . . . . 19 (Fun 𝐺 → (𝑥𝐺𝑦 → (𝑥𝐺𝑧 → (𝑥𝐹𝑧𝑥𝐹𝑦))))
4232, 41syl5 34 . . . . . . . . . . . . . . . . . 18 (Fun 𝐺 → (𝑥(𝐺𝐹)𝑦 → (𝑥𝐺𝑧 → (𝑥𝐹𝑧𝑥𝐹𝑦))))
4342imp 393 . . . . . . . . . . . . . . . . 17 ((Fun 𝐺𝑥(𝐺𝐹)𝑦) → (𝑥𝐺𝑧 → (𝑥𝐹𝑧𝑥𝐹𝑦)))
4443adantlr 686 . . . . . . . . . . . . . . . 16 (((Fun 𝐺𝐹𝐺) ∧ 𝑥(𝐺𝐹)𝑦) → (𝑥𝐺𝑧 → (𝑥𝐹𝑧𝑥𝐹𝑦)))
4544com23 86 . . . . . . . . . . . . . . 15 (((Fun 𝐺𝐹𝐺) ∧ 𝑥(𝐺𝐹)𝑦) → (𝑥𝐹𝑧 → (𝑥𝐺𝑧𝑥𝐹𝑦)))
4631, 45mpdd 43 . . . . . . . . . . . . . 14 (((Fun 𝐺𝐹𝐺) ∧ 𝑥(𝐺𝐹)𝑦) → (𝑥𝐹𝑧𝑥𝐹𝑦))
4746exlimdv 2012 . . . . . . . . . . . . 13 (((Fun 𝐺𝐹𝐺) ∧ 𝑥(𝐺𝐹)𝑦) → (∃𝑧 𝑥𝐹𝑧𝑥𝐹𝑦))
4829, 47mtod 189 . . . . . . . . . . . 12 (((Fun 𝐺𝐹𝐺) ∧ 𝑥(𝐺𝐹)𝑦) → ¬ ∃𝑧 𝑥𝐹𝑧)
4948ex 397 . . . . . . . . . . 11 ((Fun 𝐺𝐹𝐺) → (𝑥(𝐺𝐹)𝑦 → ¬ ∃𝑧 𝑥𝐹𝑧))
5049exlimdv 2012 . . . . . . . . . 10 ((Fun 𝐺𝐹𝐺) → (∃𝑦 𝑥(𝐺𝐹)𝑦 → ¬ ∃𝑧 𝑥𝐹𝑧))
5126, 50jcad 496 . . . . . . . . 9 ((Fun 𝐺𝐹𝐺) → (∃𝑦 𝑥(𝐺𝐹)𝑦 → (∃𝑦 𝑥𝐺𝑦 ∧ ¬ ∃𝑧 𝑥𝐹𝑧)))
5251eximdv 1997 . . . . . . . 8 ((Fun 𝐺𝐹𝐺) → (∃𝑥𝑦 𝑥(𝐺𝐹)𝑦 → ∃𝑥(∃𝑦 𝑥𝐺𝑦 ∧ ¬ ∃𝑧 𝑥𝐹𝑧)))
5322, 52syld 47 . . . . . . 7 ((Fun 𝐺𝐹𝐺) → (𝑝 ∈ (𝐺𝐹) → ∃𝑥(∃𝑦 𝑥𝐺𝑦 ∧ ¬ ∃𝑧 𝑥𝐹𝑧)))
5453exlimdv 2012 . . . . . 6 ((Fun 𝐺𝐹𝐺) → (∃𝑝 𝑝 ∈ (𝐺𝐹) → ∃𝑥(∃𝑦 𝑥𝐺𝑦 ∧ ¬ ∃𝑧 𝑥𝐹𝑧)))
558, 54mpd 15 . . . . 5 ((Fun 𝐺𝐹𝐺) → ∃𝑥(∃𝑦 𝑥𝐺𝑦 ∧ ¬ ∃𝑧 𝑥𝐹𝑧))
56 nss 3810 . . . . . 6 (¬ dom 𝐺 ⊆ dom 𝐹 ↔ ∃𝑥(𝑥 ∈ dom 𝐺 ∧ ¬ 𝑥 ∈ dom 𝐹))
57 vex 3352 . . . . . . . . 9 𝑥 ∈ V
5857eldm 5459 . . . . . . . 8 (𝑥 ∈ dom 𝐺 ↔ ∃𝑦 𝑥𝐺𝑦)
5957eldm 5459 . . . . . . . . 9 (𝑥 ∈ dom 𝐹 ↔ ∃𝑧 𝑥𝐹𝑧)
6059notbii 309 . . . . . . . 8 𝑥 ∈ dom 𝐹 ↔ ¬ ∃𝑧 𝑥𝐹𝑧)
6158, 60anbi12i 604 . . . . . . 7 ((𝑥 ∈ dom 𝐺 ∧ ¬ 𝑥 ∈ dom 𝐹) ↔ (∃𝑦 𝑥𝐺𝑦 ∧ ¬ ∃𝑧 𝑥𝐹𝑧))
6261exbii 1923 . . . . . 6 (∃𝑥(𝑥 ∈ dom 𝐺 ∧ ¬ 𝑥 ∈ dom 𝐹) ↔ ∃𝑥(∃𝑦 𝑥𝐺𝑦 ∧ ¬ ∃𝑧 𝑥𝐹𝑧))
6356, 62bitri 264 . . . . 5 (¬ dom 𝐺 ⊆ dom 𝐹 ↔ ∃𝑥(∃𝑦 𝑥𝐺𝑦 ∧ ¬ ∃𝑧 𝑥𝐹𝑧))
6455, 63sylibr 224 . . . 4 ((Fun 𝐺𝐹𝐺) → ¬ dom 𝐺 ⊆ dom 𝐹)
6564ex 397 . . 3 (Fun 𝐺 → (𝐹𝐺 → ¬ dom 𝐺 ⊆ dom 𝐹))
664, 65jcad 496 . 2 (Fun 𝐺 → (𝐹𝐺 → (dom 𝐹 ⊆ dom 𝐺 ∧ ¬ dom 𝐺 ⊆ dom 𝐹)))
67 dfpss3 3841 . 2 (dom 𝐹 ⊊ dom 𝐺 ↔ (dom 𝐹 ⊆ dom 𝐺 ∧ ¬ dom 𝐺 ⊆ dom 𝐹))
6866, 67syl6ibr 242 1 (Fun 𝐺 → (𝐹𝐺 → dom 𝐹 ⊊ dom 𝐺))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 382  wal 1628   = wceq 1630  wex 1851  wcel 2144  wne 2942  cdif 3718  wss 3721  wpss 3722  c0 4061  cop 4320   class class class wbr 4784  dom cdm 5249  Rel wrel 5254  Fun wfun 6025
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1990  ax-6 2056  ax-7 2092  ax-9 2153  ax-10 2173  ax-11 2189  ax-12 2202  ax-13 2407  ax-ext 2750  ax-sep 4912  ax-nul 4920  ax-pr 5034
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-3an 1072  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2049  df-eu 2621  df-mo 2622  df-clab 2757  df-cleq 2763  df-clel 2766  df-nfc 2901  df-ne 2943  df-ral 3065  df-rab 3069  df-v 3351  df-dif 3724  df-un 3726  df-in 3728  df-ss 3735  df-pss 3737  df-nul 4062  df-if 4224  df-sn 4315  df-pr 4317  df-op 4321  df-br 4785  df-opab 4845  df-id 5157  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-fun 6033
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator