Theorem ndfatafv2nrn 47348

Description: The alternate function value at a class 𝐴 at which the function is not defined is undefined, i.e., not in the range of the function. (Contributed by AV, 2-Sep-2022.)

Assertion

Ref	Expression
ndfatafv2nrn	⊢ (¬ 𝐹 defAt 𝐴 → (𝐹''''𝐴) ∉ ran 𝐹)

Proof of Theorem ndfatafv2nrn

Step	Hyp	Ref	Expression
1		ndfatafv2 47338	. 2 ⊢ (¬ 𝐹 defAt 𝐴 → (𝐹''''𝐴) = 𝒫 ∪ ran 𝐹)
2		pwuninel 8213	. . 3 ⊢ ¬ 𝒫 ∪ ran 𝐹 ∈ ran 𝐹
3		df-nel 3034	. . . 4 ⊢ ((𝐹''''𝐴) ∉ ran 𝐹 ↔ ¬ (𝐹''''𝐴) ∈ ran 𝐹)
4		eleq1 2821	. . . . 5 ⊢ ((𝐹''''𝐴) = 𝒫 ∪ ran 𝐹 → ((𝐹''''𝐴) ∈ ran 𝐹 ↔ 𝒫 ∪ ran 𝐹 ∈ ran 𝐹))
5	4	notbid 318	. . . 4 ⊢ ((𝐹''''𝐴) = 𝒫 ∪ ran 𝐹 → (¬ (𝐹''''𝐴) ∈ ran 𝐹 ↔ ¬ 𝒫 ∪ ran 𝐹 ∈ ran 𝐹))
6	3, 5	bitrid 283	. . 3 ⊢ ((𝐹''''𝐴) = 𝒫 ∪ ran 𝐹 → ((𝐹''''𝐴) ∉ ran 𝐹 ↔ ¬ 𝒫 ∪ ran 𝐹 ∈ ran 𝐹))
7	2, 6	mpbiri 258	. 2 ⊢ ((𝐹''''𝐴) = 𝒫 ∪ ran 𝐹 → (𝐹''''𝐴) ∉ ran 𝐹)
8	1, 7	syl 17	1 ⊢ (¬ 𝐹 defAt 𝐴 → (𝐹''''𝐴) ∉ ran 𝐹)

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1541   ∈ wcel 2113   ∉ wnel 3033  𝒫 cpw 4551  ∪ cuni 4860  ran crn 5622   defAt wdfat 47243  ''''cafv2 47335

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 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705  ax-sep 5238  ax-pr 5374  ax-un 7676

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-nel 3034  df-rab 3397  df-v 3439  df-un 3903  df-in 3905  df-ss 3915  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-uni 4861  df-afv2 47336

This theorem is referenced by:  ndmafv2nrn  47349  nfunsnafv2  47352  dfatafv2rnb  47354  tz6.12-2-afv2  47364