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

Theorem afv2ndeffv0 42865
Description: If the alternate function value at an argument is undefined, i.e., not in the range of the function, the function's value at this argument is the empty set. (Contributed by AV, 3-Sep-2022.)
Assertion
Ref Expression
afv2ndeffv0 ((𝐹''''𝐴) ∉ ran 𝐹 → (𝐹𝐴) = ∅)

Proof of Theorem afv2ndeffv0
StepHypRef Expression
1 df-nel 3068 . . 3 ((𝐹''''𝐴) ∉ ran 𝐹 ↔ ¬ (𝐹''''𝐴) ∈ ran 𝐹)
2 dfatafv2rnb 42832 . . . . 5 (𝐹 defAt 𝐴 ↔ (𝐹''''𝐴) ∈ ran 𝐹)
3 df-dfat 42724 . . . . 5 (𝐹 defAt 𝐴 ↔ (𝐴 ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {𝐴})))
42, 3bitr3i 269 . . . 4 ((𝐹''''𝐴) ∈ ran 𝐹 ↔ (𝐴 ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {𝐴})))
54notbii 312 . . 3 (¬ (𝐹''''𝐴) ∈ ran 𝐹 ↔ ¬ (𝐴 ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {𝐴})))
6 ianor 964 . . 3 (¬ (𝐴 ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {𝐴})) ↔ (¬ 𝐴 ∈ dom 𝐹 ∨ ¬ Fun (𝐹 ↾ {𝐴})))
71, 5, 63bitri 289 . 2 ((𝐹''''𝐴) ∉ ran 𝐹 ↔ (¬ 𝐴 ∈ dom 𝐹 ∨ ¬ Fun (𝐹 ↾ {𝐴})))
8 ndmfv 6523 . . 3 𝐴 ∈ dom 𝐹 → (𝐹𝐴) = ∅)
9 nfunsn 6531 . . 3 (¬ Fun (𝐹 ↾ {𝐴}) → (𝐹𝐴) = ∅)
108, 9jaoi 843 . 2 ((¬ 𝐴 ∈ dom 𝐹 ∨ ¬ Fun (𝐹 ↾ {𝐴})) → (𝐹𝐴) = ∅)
117, 10sylbi 209 1 ((𝐹''''𝐴) ∉ ran 𝐹 → (𝐹𝐴) = ∅)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 387  wo 833   = wceq 1507  wcel 2050  wnel 3067  c0 4172  {csn 4435  dom cdm 5401  ran crn 5402  cres 5403  Fun wfun 6176  cfv 6182   defAt wdfat 42721  ''''cafv2 42813
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-13 2301  ax-ext 2744  ax-sep 5054  ax-nul 5061  ax-pow 5113  ax-pr 5180  ax-un 7273
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-mo 2547  df-eu 2584  df-clab 2753  df-cleq 2765  df-clel 2840  df-nfc 2912  df-nel 3068  df-ral 3087  df-rex 3088  df-rab 3091  df-v 3411  df-sbc 3676  df-dif 3826  df-un 3828  df-in 3830  df-ss 3837  df-nul 4173  df-if 4345  df-pw 4418  df-sn 4436  df-pr 4438  df-op 4442  df-uni 4707  df-br 4924  df-opab 4986  df-id 5306  df-xp 5407  df-rel 5408  df-cnv 5409  df-co 5410  df-dm 5411  df-rn 5412  df-res 5413  df-iota 6146  df-fun 6184  df-fv 6190  df-dfat 42724  df-afv2 42814
This theorem is referenced by:  afv2fv0b  42871
  Copyright terms: Public domain W3C validator