Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  funressndmafv2rn Structured version   Visualization version   GIF version

Theorem funressndmafv2rn 44967
Description: The alternate function value at a class 𝐴 is defined, i.e., in the range of the function if the function is defined at 𝐴. (Contributed by AV, 2-Sep-2022.)
Assertion
Ref Expression
funressndmafv2rn (𝐹 defAt 𝐴 → (𝐹''''𝐴) ∈ ran 𝐹)

Proof of Theorem funressndmafv2rn
Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dfatafv2iota 44954 . 2 (𝐹 defAt 𝐴 → (𝐹''''𝐴) = (℩𝑦𝐴𝐹𝑦))
2 df-dfat 44863 . . 3 (𝐹 defAt 𝐴 ↔ (𝐴 ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {𝐴})))
3 sneq 4581 . . . . . . . . 9 (𝑥 = 𝐴 → {𝑥} = {𝐴})
43reseq2d 5910 . . . . . . . 8 (𝑥 = 𝐴 → (𝐹 ↾ {𝑥}) = (𝐹 ↾ {𝐴}))
54funeqd 6492 . . . . . . 7 (𝑥 = 𝐴 → (Fun (𝐹 ↾ {𝑥}) ↔ Fun (𝐹 ↾ {𝐴})))
6 eleq1 2825 . . . . . . 7 (𝑥 = 𝐴 → (𝑥 ∈ dom 𝐹𝐴 ∈ dom 𝐹))
75, 6anbi12d 631 . . . . . 6 (𝑥 = 𝐴 → ((Fun (𝐹 ↾ {𝑥}) ∧ 𝑥 ∈ dom 𝐹) ↔ (Fun (𝐹 ↾ {𝐴}) ∧ 𝐴 ∈ dom 𝐹)))
8 breq1 5090 . . . . . . . 8 (𝑥 = 𝐴 → (𝑥𝐹𝑦𝐴𝐹𝑦))
98iotabidv 6449 . . . . . . 7 (𝑥 = 𝐴 → (℩𝑦𝑥𝐹𝑦) = (℩𝑦𝐴𝐹𝑦))
109eleq1d 2822 . . . . . 6 (𝑥 = 𝐴 → ((℩𝑦𝑥𝐹𝑦) ∈ ran 𝐹 ↔ (℩𝑦𝐴𝐹𝑦) ∈ ran 𝐹))
117, 10imbi12d 344 . . . . 5 (𝑥 = 𝐴 → (((Fun (𝐹 ↾ {𝑥}) ∧ 𝑥 ∈ dom 𝐹) → (℩𝑦𝑥𝐹𝑦) ∈ ran 𝐹) ↔ ((Fun (𝐹 ↾ {𝐴}) ∧ 𝐴 ∈ dom 𝐹) → (℩𝑦𝐴𝐹𝑦) ∈ ran 𝐹)))
12 eqid 2737 . . . . . . . . 9 (℩𝑦𝑥𝐹𝑦) = (℩𝑦𝑥𝐹𝑦)
13 iotaex 6438 . . . . . . . . . 10 (℩𝑦𝑥𝐹𝑦) ∈ V
14 eqeq2 2749 . . . . . . . . . . . 12 (𝑧 = (℩𝑦𝑥𝐹𝑦) → ((℩𝑦𝑥𝐹𝑦) = 𝑧 ↔ (℩𝑦𝑥𝐹𝑦) = (℩𝑦𝑥𝐹𝑦)))
15 breq2 5091 . . . . . . . . . . . 12 (𝑧 = (℩𝑦𝑥𝐹𝑦) → (𝑥𝐹𝑧𝑥𝐹(℩𝑦𝑥𝐹𝑦)))
1614, 15bibi12d 345 . . . . . . . . . . 11 (𝑧 = (℩𝑦𝑥𝐹𝑦) → (((℩𝑦𝑥𝐹𝑦) = 𝑧𝑥𝐹𝑧) ↔ ((℩𝑦𝑥𝐹𝑦) = (℩𝑦𝑥𝐹𝑦) ↔ 𝑥𝐹(℩𝑦𝑥𝐹𝑦))))
1716imbi2d 340 . . . . . . . . . 10 (𝑧 = (℩𝑦𝑥𝐹𝑦) → (((Fun (𝐹 ↾ {𝑥}) ∧ 𝑥 ∈ dom 𝐹) → ((℩𝑦𝑥𝐹𝑦) = 𝑧𝑥𝐹𝑧)) ↔ ((Fun (𝐹 ↾ {𝑥}) ∧ 𝑥 ∈ dom 𝐹) → ((℩𝑦𝑥𝐹𝑦) = (℩𝑦𝑥𝐹𝑦) ↔ 𝑥𝐹(℩𝑦𝑥𝐹𝑦)))))
18 eldmg 5827 . . . . . . . . . . . . . 14 (𝑥 ∈ dom 𝐹 → (𝑥 ∈ dom 𝐹 ↔ ∃𝑧 𝑥𝐹𝑧))
1918ibi 266 . . . . . . . . . . . . 13 (𝑥 ∈ dom 𝐹 → ∃𝑧 𝑥𝐹𝑧)
2019adantl 482 . . . . . . . . . . . 12 ((Fun (𝐹 ↾ {𝑥}) ∧ 𝑥 ∈ dom 𝐹) → ∃𝑧 𝑥𝐹𝑧)
21 funressnvmo 44791 . . . . . . . . . . . . . 14 (Fun (𝐹 ↾ {𝑥}) → ∃*𝑧 𝑥𝐹𝑧)
2221adantr 481 . . . . . . . . . . . . 13 ((Fun (𝐹 ↾ {𝑥}) ∧ 𝑥 ∈ dom 𝐹) → ∃*𝑧 𝑥𝐹𝑧)
23 moeu 2582 . . . . . . . . . . . . 13 (∃*𝑧 𝑥𝐹𝑧 ↔ (∃𝑧 𝑥𝐹𝑧 → ∃!𝑧 𝑥𝐹𝑧))
2422, 23sylib 217 . . . . . . . . . . . 12 ((Fun (𝐹 ↾ {𝑥}) ∧ 𝑥 ∈ dom 𝐹) → (∃𝑧 𝑥𝐹𝑧 → ∃!𝑧 𝑥𝐹𝑧))
2520, 24mpd 15 . . . . . . . . . . 11 ((Fun (𝐹 ↾ {𝑥}) ∧ 𝑥 ∈ dom 𝐹) → ∃!𝑧 𝑥𝐹𝑧)
26 iota1 6442 . . . . . . . . . . . 12 (∃!𝑧 𝑥𝐹𝑧 → (𝑥𝐹𝑧 ↔ (℩𝑧𝑥𝐹𝑧) = 𝑧))
27 breq2 5091 . . . . . . . . . . . . . 14 (𝑧 = 𝑦 → (𝑥𝐹𝑧𝑥𝐹𝑦))
2827cbviotavw 6425 . . . . . . . . . . . . 13 (℩𝑧𝑥𝐹𝑧) = (℩𝑦𝑥𝐹𝑦)
2928eqeq1i 2742 . . . . . . . . . . . 12 ((℩𝑧𝑥𝐹𝑧) = 𝑧 ↔ (℩𝑦𝑥𝐹𝑦) = 𝑧)
3026, 29bitr2di 287 . . . . . . . . . . 11 (∃!𝑧 𝑥𝐹𝑧 → ((℩𝑦𝑥𝐹𝑦) = 𝑧𝑥𝐹𝑧))
3125, 30syl 17 . . . . . . . . . 10 ((Fun (𝐹 ↾ {𝑥}) ∧ 𝑥 ∈ dom 𝐹) → ((℩𝑦𝑥𝐹𝑦) = 𝑧𝑥𝐹𝑧))
3213, 17, 31vtocl 3507 . . . . . . . . 9 ((Fun (𝐹 ↾ {𝑥}) ∧ 𝑥 ∈ dom 𝐹) → ((℩𝑦𝑥𝐹𝑦) = (℩𝑦𝑥𝐹𝑦) ↔ 𝑥𝐹(℩𝑦𝑥𝐹𝑦)))
3312, 32mpbii 232 . . . . . . . 8 ((Fun (𝐹 ↾ {𝑥}) ∧ 𝑥 ∈ dom 𝐹) → 𝑥𝐹(℩𝑦𝑥𝐹𝑦))
34 df-br 5088 . . . . . . . 8 (𝑥𝐹(℩𝑦𝑥𝐹𝑦) ↔ ⟨𝑥, (℩𝑦𝑥𝐹𝑦)⟩ ∈ 𝐹)
3533, 34sylib 217 . . . . . . 7 ((Fun (𝐹 ↾ {𝑥}) ∧ 𝑥 ∈ dom 𝐹) → ⟨𝑥, (℩𝑦𝑥𝐹𝑦)⟩ ∈ 𝐹)
36 vex 3445 . . . . . . . 8 𝑥 ∈ V
37 opeq1 4815 . . . . . . . . 9 (𝑧 = 𝑥 → ⟨𝑧, (℩𝑦𝑥𝐹𝑦)⟩ = ⟨𝑥, (℩𝑦𝑥𝐹𝑦)⟩)
3837eleq1d 2822 . . . . . . . 8 (𝑧 = 𝑥 → (⟨𝑧, (℩𝑦𝑥𝐹𝑦)⟩ ∈ 𝐹 ↔ ⟨𝑥, (℩𝑦𝑥𝐹𝑦)⟩ ∈ 𝐹))
3936, 38spcev 3554 . . . . . . 7 (⟨𝑥, (℩𝑦𝑥𝐹𝑦)⟩ ∈ 𝐹 → ∃𝑧𝑧, (℩𝑦𝑥𝐹𝑦)⟩ ∈ 𝐹)
4035, 39syl 17 . . . . . 6 ((Fun (𝐹 ↾ {𝑥}) ∧ 𝑥 ∈ dom 𝐹) → ∃𝑧𝑧, (℩𝑦𝑥𝐹𝑦)⟩ ∈ 𝐹)
4113elrn2 5821 . . . . . 6 ((℩𝑦𝑥𝐹𝑦) ∈ ran 𝐹 ↔ ∃𝑧𝑧, (℩𝑦𝑥𝐹𝑦)⟩ ∈ 𝐹)
4240, 41sylibr 233 . . . . 5 ((Fun (𝐹 ↾ {𝑥}) ∧ 𝑥 ∈ dom 𝐹) → (℩𝑦𝑥𝐹𝑦) ∈ ran 𝐹)
4311, 42vtoclg 3514 . . . 4 (𝐴 ∈ dom 𝐹 → ((Fun (𝐹 ↾ {𝐴}) ∧ 𝐴 ∈ dom 𝐹) → (℩𝑦𝐴𝐹𝑦) ∈ ran 𝐹))
4443anabsi6 667 . . 3 ((𝐴 ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {𝐴})) → (℩𝑦𝐴𝐹𝑦) ∈ ran 𝐹)
452, 44sylbi 216 . 2 (𝐹 defAt 𝐴 → (℩𝑦𝐴𝐹𝑦) ∈ ran 𝐹)
461, 45eqeltrd 2838 1 (𝐹 defAt 𝐴 → (𝐹''''𝐴) ∈ ran 𝐹)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396   = wceq 1540  wex 1780  wcel 2105  ∃*wmo 2537  ∃!weu 2567  {csn 4571  cop 4577   class class class wbr 5087  dom cdm 5607  ran crn 5608  cres 5609  cio 6415  Fun wfun 6459   defAt wdfat 44860  ''''cafv2 44952
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-12 2170  ax-ext 2708  ax-sep 5238  ax-nul 5245  ax-pr 5367
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3405  df-v 3443  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4268  df-if 4472  df-sn 4572  df-pr 4574  df-op 4578  df-uni 4851  df-br 5088  df-opab 5150  df-id 5507  df-xp 5613  df-rel 5614  df-cnv 5615  df-co 5616  df-dm 5617  df-rn 5618  df-res 5619  df-iota 6417  df-fun 6467  df-dfat 44863  df-afv2 44953
This theorem is referenced by:  afv2ndefb  44968  dfatafv2rnb  44971
  Copyright terms: Public domain W3C validator