Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ressupprn Structured version   Visualization version   GIF version

Theorem ressupprn 30453
Description: The range of a function restricted to its support. (Contributed by Thierry Arnoux, 25-Jun-2024.)
Assertion
Ref Expression
ressupprn ((Fun 𝐹𝐹𝑉0𝑊) → ran (𝐹 ↾ (𝐹 supp 0 )) = (ran 𝐹 ∖ { 0 }))

Proof of Theorem ressupprn
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 funfn 6358 . . . . . . . . 9 (Fun 𝐹𝐹 Fn dom 𝐹)
21biimpi 219 . . . . . . . 8 (Fun 𝐹𝐹 Fn dom 𝐹)
323ad2ant1 1130 . . . . . . 7 ((Fun 𝐹𝐹𝑉0𝑊) → 𝐹 Fn dom 𝐹)
4 dmexg 7598 . . . . . . . 8 (𝐹𝑉 → dom 𝐹 ∈ V)
543ad2ant2 1131 . . . . . . 7 ((Fun 𝐹𝐹𝑉0𝑊) → dom 𝐹 ∈ V)
6 simp3 1135 . . . . . . 7 ((Fun 𝐹𝐹𝑉0𝑊) → 0𝑊)
7 elsuppfn 7825 . . . . . . 7 ((𝐹 Fn dom 𝐹 ∧ dom 𝐹 ∈ V ∧ 0𝑊) → (𝑥 ∈ (𝐹 supp 0 ) ↔ (𝑥 ∈ dom 𝐹 ∧ (𝐹𝑥) ≠ 0 )))
83, 5, 6, 7syl3anc 1368 . . . . . 6 ((Fun 𝐹𝐹𝑉0𝑊) → (𝑥 ∈ (𝐹 supp 0 ) ↔ (𝑥 ∈ dom 𝐹 ∧ (𝐹𝑥) ≠ 0 )))
98anbi1d 632 . . . . 5 ((Fun 𝐹𝐹𝑉0𝑊) → ((𝑥 ∈ (𝐹 supp 0 ) ∧ ((𝐹 ↾ (𝐹 supp 0 ))‘𝑥) = 𝑦) ↔ ((𝑥 ∈ dom 𝐹 ∧ (𝐹𝑥) ≠ 0 ) ∧ ((𝐹 ↾ (𝐹 supp 0 ))‘𝑥) = 𝑦)))
10 anass 472 . . . . . 6 (((𝑥 ∈ dom 𝐹 ∧ (𝐹𝑥) ≠ 0 ) ∧ ((𝐹 ↾ (𝐹 supp 0 ))‘𝑥) = 𝑦) ↔ (𝑥 ∈ dom 𝐹 ∧ ((𝐹𝑥) ≠ 0 ∧ ((𝐹 ↾ (𝐹 supp 0 ))‘𝑥) = 𝑦)))
1110a1i 11 . . . . 5 ((Fun 𝐹𝐹𝑉0𝑊) → (((𝑥 ∈ dom 𝐹 ∧ (𝐹𝑥) ≠ 0 ) ∧ ((𝐹 ↾ (𝐹 supp 0 ))‘𝑥) = 𝑦) ↔ (𝑥 ∈ dom 𝐹 ∧ ((𝐹𝑥) ≠ 0 ∧ ((𝐹 ↾ (𝐹 supp 0 ))‘𝑥) = 𝑦))))
128biimprd 251 . . . . . . . . . . 11 ((Fun 𝐹𝐹𝑉0𝑊) → ((𝑥 ∈ dom 𝐹 ∧ (𝐹𝑥) ≠ 0 ) → 𝑥 ∈ (𝐹 supp 0 )))
1312impl 459 . . . . . . . . . 10 ((((Fun 𝐹𝐹𝑉0𝑊) ∧ 𝑥 ∈ dom 𝐹) ∧ (𝐹𝑥) ≠ 0 ) → 𝑥 ∈ (𝐹 supp 0 ))
1413fvresd 6669 . . . . . . . . 9 ((((Fun 𝐹𝐹𝑉0𝑊) ∧ 𝑥 ∈ dom 𝐹) ∧ (𝐹𝑥) ≠ 0 ) → ((𝐹 ↾ (𝐹 supp 0 ))‘𝑥) = (𝐹𝑥))
1514eqeq1d 2803 . . . . . . . 8 ((((Fun 𝐹𝐹𝑉0𝑊) ∧ 𝑥 ∈ dom 𝐹) ∧ (𝐹𝑥) ≠ 0 ) → (((𝐹 ↾ (𝐹 supp 0 ))‘𝑥) = 𝑦 ↔ (𝐹𝑥) = 𝑦))
1615pm5.32da 582 . . . . . . 7 (((Fun 𝐹𝐹𝑉0𝑊) ∧ 𝑥 ∈ dom 𝐹) → (((𝐹𝑥) ≠ 0 ∧ ((𝐹 ↾ (𝐹 supp 0 ))‘𝑥) = 𝑦) ↔ ((𝐹𝑥) ≠ 0 ∧ (𝐹𝑥) = 𝑦)))
17 ancom 464 . . . . . . . 8 (((𝐹𝑥) ≠ 0 ∧ (𝐹𝑥) = 𝑦) ↔ ((𝐹𝑥) = 𝑦 ∧ (𝐹𝑥) ≠ 0 ))
18 simpr 488 . . . . . . . . . 10 ((((Fun 𝐹𝐹𝑉0𝑊) ∧ 𝑥 ∈ dom 𝐹) ∧ (𝐹𝑥) = 𝑦) → (𝐹𝑥) = 𝑦)
1918neeq1d 3049 . . . . . . . . 9 ((((Fun 𝐹𝐹𝑉0𝑊) ∧ 𝑥 ∈ dom 𝐹) ∧ (𝐹𝑥) = 𝑦) → ((𝐹𝑥) ≠ 0𝑦0 ))
2019pm5.32da 582 . . . . . . . 8 (((Fun 𝐹𝐹𝑉0𝑊) ∧ 𝑥 ∈ dom 𝐹) → (((𝐹𝑥) = 𝑦 ∧ (𝐹𝑥) ≠ 0 ) ↔ ((𝐹𝑥) = 𝑦𝑦0 )))
2117, 20syl5bb 286 . . . . . . 7 (((Fun 𝐹𝐹𝑉0𝑊) ∧ 𝑥 ∈ dom 𝐹) → (((𝐹𝑥) ≠ 0 ∧ (𝐹𝑥) = 𝑦) ↔ ((𝐹𝑥) = 𝑦𝑦0 )))
2216, 21bitrd 282 . . . . . 6 (((Fun 𝐹𝐹𝑉0𝑊) ∧ 𝑥 ∈ dom 𝐹) → (((𝐹𝑥) ≠ 0 ∧ ((𝐹 ↾ (𝐹 supp 0 ))‘𝑥) = 𝑦) ↔ ((𝐹𝑥) = 𝑦𝑦0 )))
2322pm5.32da 582 . . . . 5 ((Fun 𝐹𝐹𝑉0𝑊) → ((𝑥 ∈ dom 𝐹 ∧ ((𝐹𝑥) ≠ 0 ∧ ((𝐹 ↾ (𝐹 supp 0 ))‘𝑥) = 𝑦)) ↔ (𝑥 ∈ dom 𝐹 ∧ ((𝐹𝑥) = 𝑦𝑦0 ))))
249, 11, 233bitrd 308 . . . 4 ((Fun 𝐹𝐹𝑉0𝑊) → ((𝑥 ∈ (𝐹 supp 0 ) ∧ ((𝐹 ↾ (𝐹 supp 0 ))‘𝑥) = 𝑦) ↔ (𝑥 ∈ dom 𝐹 ∧ ((𝐹𝑥) = 𝑦𝑦0 ))))
2524rexbidv2 3257 . . 3 ((Fun 𝐹𝐹𝑉0𝑊) → (∃𝑥 ∈ (𝐹 supp 0 )((𝐹 ↾ (𝐹 supp 0 ))‘𝑥) = 𝑦 ↔ ∃𝑥 ∈ dom 𝐹((𝐹𝑥) = 𝑦𝑦0 )))
26 suppssdm 7830 . . . . 5 (𝐹 supp 0 ) ⊆ dom 𝐹
27 fnssres 6446 . . . . 5 ((𝐹 Fn dom 𝐹 ∧ (𝐹 supp 0 ) ⊆ dom 𝐹) → (𝐹 ↾ (𝐹 supp 0 )) Fn (𝐹 supp 0 ))
283, 26, 27sylancl 589 . . . 4 ((Fun 𝐹𝐹𝑉0𝑊) → (𝐹 ↾ (𝐹 supp 0 )) Fn (𝐹 supp 0 ))
29 fvelrnb 6705 . . . 4 ((𝐹 ↾ (𝐹 supp 0 )) Fn (𝐹 supp 0 ) → (𝑦 ∈ ran (𝐹 ↾ (𝐹 supp 0 )) ↔ ∃𝑥 ∈ (𝐹 supp 0 )((𝐹 ↾ (𝐹 supp 0 ))‘𝑥) = 𝑦))
3028, 29syl 17 . . 3 ((Fun 𝐹𝐹𝑉0𝑊) → (𝑦 ∈ ran (𝐹 ↾ (𝐹 supp 0 )) ↔ ∃𝑥 ∈ (𝐹 supp 0 )((𝐹 ↾ (𝐹 supp 0 ))‘𝑥) = 𝑦))
31 fvelrnb 6705 . . . . . 6 (𝐹 Fn dom 𝐹 → (𝑦 ∈ ran 𝐹 ↔ ∃𝑥 ∈ dom 𝐹(𝐹𝑥) = 𝑦))
3231anbi1d 632 . . . . 5 (𝐹 Fn dom 𝐹 → ((𝑦 ∈ ran 𝐹𝑦0 ) ↔ (∃𝑥 ∈ dom 𝐹(𝐹𝑥) = 𝑦𝑦0 )))
33 eldifsn 4683 . . . . 5 (𝑦 ∈ (ran 𝐹 ∖ { 0 }) ↔ (𝑦 ∈ ran 𝐹𝑦0 ))
34 r19.41v 3303 . . . . 5 (∃𝑥 ∈ dom 𝐹((𝐹𝑥) = 𝑦𝑦0 ) ↔ (∃𝑥 ∈ dom 𝐹(𝐹𝑥) = 𝑦𝑦0 ))
3532, 33, 343bitr4g 317 . . . 4 (𝐹 Fn dom 𝐹 → (𝑦 ∈ (ran 𝐹 ∖ { 0 }) ↔ ∃𝑥 ∈ dom 𝐹((𝐹𝑥) = 𝑦𝑦0 )))
363, 35syl 17 . . 3 ((Fun 𝐹𝐹𝑉0𝑊) → (𝑦 ∈ (ran 𝐹 ∖ { 0 }) ↔ ∃𝑥 ∈ dom 𝐹((𝐹𝑥) = 𝑦𝑦0 )))
3725, 30, 363bitr4d 314 . 2 ((Fun 𝐹𝐹𝑉0𝑊) → (𝑦 ∈ ran (𝐹 ↾ (𝐹 supp 0 )) ↔ 𝑦 ∈ (ran 𝐹 ∖ { 0 })))
3837eqrdv 2799 1 ((Fun 𝐹𝐹𝑉0𝑊) → ran (𝐹 ↾ (𝐹 supp 0 )) = (ran 𝐹 ∖ { 0 }))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399  w3a 1084   = wceq 1538  wcel 2112  wne 2990  wrex 3110  Vcvv 3444  cdif 3881  wss 3884  {csn 4528  dom cdm 5523  ran crn 5524  cres 5525  Fun wfun 6322   Fn wfn 6323  cfv 6328  (class class class)co 7139   supp csupp 7817
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-rep 5157  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-reu 3116  df-rab 3118  df-v 3446  df-sbc 3724  df-csb 3832  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-nul 4247  df-if 4429  df-sn 4529  df-pr 4531  df-op 4535  df-uni 4804  df-iun 4886  df-br 5034  df-opab 5096  df-mpt 5114  df-id 5428  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-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-ov 7142  df-oprab 7143  df-mpo 7144  df-supp 7818
This theorem is referenced by:  fsupprnfi  30455
  Copyright terms: Public domain W3C validator