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

Theorem funpartlem 33517
Description: Lemma for funpartfun 33518. Show membership in the restriction. (Contributed by Scott Fenton, 4-Dec-2017.)
Assertion
Ref Expression
funpartlem (𝐴 ∈ dom ((Image𝐹 ∘ Singleton) ∩ (V × Singletons )) ↔ ∃𝑥(𝐹 “ {𝐴}) = {𝑥})
Distinct variable groups:   𝑥,𝐴   𝑥,𝐹

Proof of Theorem funpartlem
Dummy variables 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elex 3462 . 2 (𝐴 ∈ dom ((Image𝐹 ∘ Singleton) ∩ (V × Singletons )) → 𝐴 ∈ V)
2 vsnid 4565 . . . . 5 𝑥 ∈ {𝑥}
3 eleq2 2881 . . . . 5 ((𝐹 “ {𝐴}) = {𝑥} → (𝑥 ∈ (𝐹 “ {𝐴}) ↔ 𝑥 ∈ {𝑥}))
42, 3mpbiri 261 . . . 4 ((𝐹 “ {𝐴}) = {𝑥} → 𝑥 ∈ (𝐹 “ {𝐴}))
5 n0i 4252 . . . . 5 (𝑥 ∈ (𝐹 “ {𝐴}) → ¬ (𝐹 “ {𝐴}) = ∅)
6 snprc 4616 . . . . . . . 8 𝐴 ∈ V ↔ {𝐴} = ∅)
76biimpi 219 . . . . . . 7 𝐴 ∈ V → {𝐴} = ∅)
87imaeq2d 5900 . . . . . 6 𝐴 ∈ V → (𝐹 “ {𝐴}) = (𝐹 “ ∅))
9 ima0 5916 . . . . . 6 (𝐹 “ ∅) = ∅
108, 9eqtrdi 2852 . . . . 5 𝐴 ∈ V → (𝐹 “ {𝐴}) = ∅)
115, 10nsyl2 143 . . . 4 (𝑥 ∈ (𝐹 “ {𝐴}) → 𝐴 ∈ V)
124, 11syl 17 . . 3 ((𝐹 “ {𝐴}) = {𝑥} → 𝐴 ∈ V)
1312exlimiv 1931 . 2 (∃𝑥(𝐹 “ {𝐴}) = {𝑥} → 𝐴 ∈ V)
14 eleq1 2880 . . 3 (𝑦 = 𝐴 → (𝑦 ∈ dom ((Image𝐹 ∘ Singleton) ∩ (V × Singletons )) ↔ 𝐴 ∈ dom ((Image𝐹 ∘ Singleton) ∩ (V × Singletons ))))
15 sneq 4538 . . . . . 6 (𝑦 = 𝐴 → {𝑦} = {𝐴})
1615imaeq2d 5900 . . . . 5 (𝑦 = 𝐴 → (𝐹 “ {𝑦}) = (𝐹 “ {𝐴}))
1716eqeq1d 2803 . . . 4 (𝑦 = 𝐴 → ((𝐹 “ {𝑦}) = {𝑥} ↔ (𝐹 “ {𝐴}) = {𝑥}))
1817exbidv 1922 . . 3 (𝑦 = 𝐴 → (∃𝑥(𝐹 “ {𝑦}) = {𝑥} ↔ ∃𝑥(𝐹 “ {𝐴}) = {𝑥}))
19 vex 3447 . . . . 5 𝑦 ∈ V
2019eldm 5737 . . . 4 (𝑦 ∈ dom ((Image𝐹 ∘ Singleton) ∩ (V × Singletons )) ↔ ∃𝑧 𝑦((Image𝐹 ∘ Singleton) ∩ (V × Singletons ))𝑧)
21 brxp 5569 . . . . . . . . . 10 (𝑦(V × Singletons )𝑧 ↔ (𝑦 ∈ V ∧ 𝑧 Singletons ))
2219, 21mpbiran 708 . . . . . . . . 9 (𝑦(V × Singletons )𝑧𝑧 Singletons )
23 elsingles 33493 . . . . . . . . 9 (𝑧 Singletons ↔ ∃𝑥 𝑧 = {𝑥})
2422, 23bitri 278 . . . . . . . 8 (𝑦(V × Singletons )𝑧 ↔ ∃𝑥 𝑧 = {𝑥})
2524anbi2i 625 . . . . . . 7 ((𝑦(Image𝐹 ∘ Singleton)𝑧𝑦(V × Singletons )𝑧) ↔ (𝑦(Image𝐹 ∘ Singleton)𝑧 ∧ ∃𝑥 𝑧 = {𝑥}))
26 brin 5085 . . . . . . 7 (𝑦((Image𝐹 ∘ Singleton) ∩ (V × Singletons ))𝑧 ↔ (𝑦(Image𝐹 ∘ Singleton)𝑧𝑦(V × Singletons )𝑧))
27 19.42v 1954 . . . . . . 7 (∃𝑥(𝑦(Image𝐹 ∘ Singleton)𝑧𝑧 = {𝑥}) ↔ (𝑦(Image𝐹 ∘ Singleton)𝑧 ∧ ∃𝑥 𝑧 = {𝑥}))
2825, 26, 273bitr4i 306 . . . . . 6 (𝑦((Image𝐹 ∘ Singleton) ∩ (V × Singletons ))𝑧 ↔ ∃𝑥(𝑦(Image𝐹 ∘ Singleton)𝑧𝑧 = {𝑥}))
2928exbii 1849 . . . . 5 (∃𝑧 𝑦((Image𝐹 ∘ Singleton) ∩ (V × Singletons ))𝑧 ↔ ∃𝑧𝑥(𝑦(Image𝐹 ∘ Singleton)𝑧𝑧 = {𝑥}))
30 excom 2167 . . . . 5 (∃𝑧𝑥(𝑦(Image𝐹 ∘ Singleton)𝑧𝑧 = {𝑥}) ↔ ∃𝑥𝑧(𝑦(Image𝐹 ∘ Singleton)𝑧𝑧 = {𝑥}))
3129, 30bitri 278 . . . 4 (∃𝑧 𝑦((Image𝐹 ∘ Singleton) ∩ (V × Singletons ))𝑧 ↔ ∃𝑥𝑧(𝑦(Image𝐹 ∘ Singleton)𝑧𝑧 = {𝑥}))
32 exancom 1862 . . . . . 6 (∃𝑧(𝑦(Image𝐹 ∘ Singleton)𝑧𝑧 = {𝑥}) ↔ ∃𝑧(𝑧 = {𝑥} ∧ 𝑦(Image𝐹 ∘ Singleton)𝑧))
33 snex 5300 . . . . . . 7 {𝑥} ∈ V
34 breq2 5037 . . . . . . 7 (𝑧 = {𝑥} → (𝑦(Image𝐹 ∘ Singleton)𝑧𝑦(Image𝐹 ∘ Singleton){𝑥}))
3533, 34ceqsexv 3492 . . . . . 6 (∃𝑧(𝑧 = {𝑥} ∧ 𝑦(Image𝐹 ∘ Singleton)𝑧) ↔ 𝑦(Image𝐹 ∘ Singleton){𝑥})
3619, 33brco 5709 . . . . . . 7 (𝑦(Image𝐹 ∘ Singleton){𝑥} ↔ ∃𝑧(𝑦Singleton𝑧𝑧Image𝐹{𝑥}))
37 vex 3447 . . . . . . . . . 10 𝑧 ∈ V
3819, 37brsingle 33492 . . . . . . . . 9 (𝑦Singleton𝑧𝑧 = {𝑦})
3938anbi1i 626 . . . . . . . 8 ((𝑦Singleton𝑧𝑧Image𝐹{𝑥}) ↔ (𝑧 = {𝑦} ∧ 𝑧Image𝐹{𝑥}))
4039exbii 1849 . . . . . . 7 (∃𝑧(𝑦Singleton𝑧𝑧Image𝐹{𝑥}) ↔ ∃𝑧(𝑧 = {𝑦} ∧ 𝑧Image𝐹{𝑥}))
41 snex 5300 . . . . . . . . 9 {𝑦} ∈ V
42 breq1 5036 . . . . . . . . 9 (𝑧 = {𝑦} → (𝑧Image𝐹{𝑥} ↔ {𝑦}Image𝐹{𝑥}))
4341, 42ceqsexv 3492 . . . . . . . 8 (∃𝑧(𝑧 = {𝑦} ∧ 𝑧Image𝐹{𝑥}) ↔ {𝑦}Image𝐹{𝑥})
4441, 33brimage 33501 . . . . . . . 8 ({𝑦}Image𝐹{𝑥} ↔ {𝑥} = (𝐹 “ {𝑦}))
45 eqcom 2808 . . . . . . . 8 ({𝑥} = (𝐹 “ {𝑦}) ↔ (𝐹 “ {𝑦}) = {𝑥})
4643, 44, 453bitri 300 . . . . . . 7 (∃𝑧(𝑧 = {𝑦} ∧ 𝑧Image𝐹{𝑥}) ↔ (𝐹 “ {𝑦}) = {𝑥})
4736, 40, 463bitri 300 . . . . . 6 (𝑦(Image𝐹 ∘ Singleton){𝑥} ↔ (𝐹 “ {𝑦}) = {𝑥})
4832, 35, 473bitri 300 . . . . 5 (∃𝑧(𝑦(Image𝐹 ∘ Singleton)𝑧𝑧 = {𝑥}) ↔ (𝐹 “ {𝑦}) = {𝑥})
4948exbii 1849 . . . 4 (∃𝑥𝑧(𝑦(Image𝐹 ∘ Singleton)𝑧𝑧 = {𝑥}) ↔ ∃𝑥(𝐹 “ {𝑦}) = {𝑥})
5020, 31, 493bitri 300 . . 3 (𝑦 ∈ dom ((Image𝐹 ∘ Singleton) ∩ (V × Singletons )) ↔ ∃𝑥(𝐹 “ {𝑦}) = {𝑥})
5114, 18, 50vtoclbg 3520 . 2 (𝐴 ∈ V → (𝐴 ∈ dom ((Image𝐹 ∘ Singleton) ∩ (V × Singletons )) ↔ ∃𝑥(𝐹 “ {𝐴}) = {𝑥}))
521, 13, 51pm5.21nii 383 1 (𝐴 ∈ dom ((Image𝐹 ∘ Singleton) ∩ (V × Singletons )) ↔ ∃𝑥(𝐹 “ {𝐴}) = {𝑥})
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 209  wa 399   = wceq 1538  wex 1781  wcel 2112  Vcvv 3444  cin 3883  c0 4246  {csn 4528   class class class wbr 5033   × cxp 5521  dom cdm 5523  cima 5526  ccom 5527  Singletoncsingle 33413   Singletons csingles 33414  Imagecimage 33415
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-sep 5170  ax-nul 5177  ax-pow 5234  ax-pr 5298  ax-un 7445
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ne 2991  df-ral 3114  df-rex 3115  df-rab 3118  df-v 3446  df-sbc 3724  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-symdif 4172  df-nul 4247  df-if 4429  df-sn 4529  df-pr 4531  df-op 4535  df-uni 4804  df-br 5034  df-opab 5096  df-mpt 5114  df-id 5428  df-eprel 5433  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-fo 6334  df-fv 6336  df-1st 7675  df-2nd 7676  df-txp 33429  df-singleton 33437  df-singles 33438  df-image 33439
This theorem is referenced by:  funpartfun  33518  funpartfv  33520
  Copyright terms: Public domain W3C validator