Metamath Proof Explorer

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 
|- ( ( F '''' A ) = ~P U. ran F <-> ( F '''' A ) e/ ran F )

Proof

Step Hyp Ref Expression
1 pwuninel 
 |-  -. ~P U. ran F e. ran F
2 df-nel 
 |-  ( ( F '''' A ) e/ ran F <-> -. ( F '''' A ) e. ran F )
3 eleq1 
 |-  ( ( F '''' A ) = ~P U. ran F -> ( ( F '''' A ) e. ran F <-> ~P U. ran F e. ran F ) )
4 3 notbid 
 |-  ( ( F '''' A ) = ~P U. ran F -> ( -. ( F '''' A ) e. ran F <-> -. ~P U. ran F e. ran F ) )
5 2 4 syl5bb 
 |-  ( ( F '''' A ) = ~P U. ran F -> ( ( F '''' A ) e/ ran F <-> -. ~P U. ran F e. ran F ) )
6 1 5 mpbiri 
 |-  ( ( F '''' A ) = ~P U. ran F -> ( F '''' A ) e/ ran F )
7 funressndmafv2rn 
 |-  ( F defAt A -> ( F '''' A ) e. ran F )
8 7 con3i 
 |-  ( -. ( F '''' A ) e. ran F -> -. F defAt A )
9 2 8 sylbi 
 |-  ( ( F '''' A ) e/ ran F -> -. F defAt A )
10 ndfatafv2 
 |-  ( -. F defAt A -> ( F '''' A ) = ~P U. ran F )
11 9 10 syl 
 |-  ( ( F '''' A ) e/ ran F -> ( F '''' A ) = ~P U. ran F )
12 6 11 impbii 
 |-  ( ( F '''' A ) = ~P U. ran F <-> ( F '''' A ) e/ ran F )