Theorem afv2ndefb

Description: Two ways to say that an alternate function value is not defined. (Contributed by AV, 5-Sep-2022)

	Ref	Expression
Assertion	afv2ndefb	⊢ ( ( 𝐹 '''' 𝐴 ) = 𝒫 ∪ ran 𝐹 ↔ ( 𝐹 '''' 𝐴 ) ∉ ran 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		pwuninel	⊢ ¬ 𝒫 ∪ ran 𝐹 ∈ ran 𝐹
2		df-nel	⊢ ( ( 𝐹 '''' 𝐴 ) ∉ ran 𝐹 ↔ ¬ ( 𝐹 '''' 𝐴 ) ∈ ran 𝐹 )
3		eleq1	⊢ ( ( 𝐹 '''' 𝐴 ) = 𝒫 ∪ ran 𝐹 → ( ( 𝐹 '''' 𝐴 ) ∈ ran 𝐹 ↔ 𝒫 ∪ ran 𝐹 ∈ ran 𝐹 ) )
4	3	notbid	⊢ ( ( 𝐹 '''' 𝐴 ) = 𝒫 ∪ ran 𝐹 → ( ¬ ( 𝐹 '''' 𝐴 ) ∈ ran 𝐹 ↔ ¬ 𝒫 ∪ ran 𝐹 ∈ ran 𝐹 ) )
5	2 4	bitrid	⊢ ( ( 𝐹 '''' 𝐴 ) = 𝒫 ∪ ran 𝐹 → ( ( 𝐹 '''' 𝐴 ) ∉ ran 𝐹 ↔ ¬ 𝒫 ∪ ran 𝐹 ∈ ran 𝐹 ) )
6	1 5	mpbiri	⊢ ( ( 𝐹 '''' 𝐴 ) = 𝒫 ∪ ran 𝐹 → ( 𝐹 '''' 𝐴 ) ∉ ran 𝐹 )
7		funressndmafv2rn	⊢ ( 𝐹 defAt 𝐴 → ( 𝐹 '''' 𝐴 ) ∈ ran 𝐹 )
8	7	con3i	⊢ ( ¬ ( 𝐹 '''' 𝐴 ) ∈ ran 𝐹 → ¬ 𝐹 defAt 𝐴 )
9	2 8	sylbi	⊢ ( ( 𝐹 '''' 𝐴 ) ∉ ran 𝐹 → ¬ 𝐹 defAt 𝐴 )
10		ndfatafv2	⊢ ( ¬ 𝐹 defAt 𝐴 → ( 𝐹 '''' 𝐴 ) = 𝒫 ∪ ran 𝐹 )
11	9 10	syl	⊢ ( ( 𝐹 '''' 𝐴 ) ∉ ran 𝐹 → ( 𝐹 '''' 𝐴 ) = 𝒫 ∪ ran 𝐹 )
12	6 11	impbii	⊢ ( ( 𝐹 '''' 𝐴 ) = 𝒫 ∪ ran 𝐹 ↔ ( 𝐹 '''' 𝐴 ) ∉ ran 𝐹 )