Metamath Proof Explorer

Theorem funressndmafv2rn

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

Ref Expression
Assertion funressndmafv2rn 
|- ( F defAt A -> ( F '''' A ) e. ran F )

Proof

Step Hyp Ref Expression
1 dfatafv2iota 
 |-  ( F defAt A -> ( F '''' A ) = ( iota y A F y ) )
2 df-dfat 
 |-  ( F defAt A <-> ( A e. dom F /\ Fun ( F |` { A } ) ) )
3 sneq 
 |-  ( x = A -> { x } = { A } )
4 3 reseq2d 
 |-  ( x = A -> ( F |` { x } ) = ( F |` { A } ) )
5 4 funeqd 
 |-  ( x = A -> ( Fun ( F |` { x } ) <-> Fun ( F |` { A } ) ) )
6 eleq1 
 |-  ( x = A -> ( x e. dom F <-> A e. dom F ) )
7 5 6 anbi12d 
 |-  ( x = A -> ( ( Fun ( F |` { x } ) /\ x e. dom F ) <-> ( Fun ( F |` { A } ) /\ A e. dom F ) ) )
8 breq1 
 |-  ( x = A -> ( x F y <-> A F y ) )
9 8 iotabidv 
 |-  ( x = A -> ( iota y x F y ) = ( iota y A F y ) )
10 9 eleq1d 
 |-  ( x = A -> ( ( iota y x F y ) e. ran F <-> ( iota y A F y ) e. ran F ) )
11 7 10 imbi12d 
 |-  ( x = A -> ( ( ( Fun ( F |` { x } ) /\ x e. dom F ) -> ( iota y x F y ) e. ran F ) <-> ( ( Fun ( F |` { A } ) /\ A e. dom F ) -> ( iota y A F y ) e. ran F ) ) )
12 eqid 
 |-  ( iota y x F y ) = ( iota y x F y )
13 iotaex 
 |-  ( iota y x F y ) e. _V
14 eqeq2 
 |-  ( z = ( iota y x F y ) -> ( ( iota y x F y ) = z <-> ( iota y x F y ) = ( iota y x F y ) ) )
15 breq2 
 |-  ( z = ( iota y x F y ) -> ( x F z <-> x F ( iota y x F y ) ) )
16 14 15 bibi12d 
 |-  ( z = ( iota y x F y ) -> ( ( ( iota y x F y ) = z <-> x F z ) <-> ( ( iota y x F y ) = ( iota y x F y ) <-> x F ( iota y x F y ) ) ) )
17 16 imbi2d 
 |-  ( z = ( iota y x F y ) -> ( ( ( Fun ( F |` { x } ) /\ x e. dom F ) -> ( ( iota y x F y ) = z <-> x F z ) ) <-> ( ( Fun ( F |` { x } ) /\ x e. dom F ) -> ( ( iota y x F y ) = ( iota y x F y ) <-> x F ( iota y x F y ) ) ) ) )
18 eldmg 
 |-  ( x e. dom F -> ( x e. dom F <-> E. z x F z ) )
19 18 ibi 
 |-  ( x e. dom F -> E. z x F z )
20 19 adantl 
 |-  ( ( Fun ( F |` { x } ) /\ x e. dom F ) -> E. z x F z )
21 funressnvmo 
 |-  ( Fun ( F |` { x } ) -> E* z x F z )
22 21 adantr 
 |-  ( ( Fun ( F |` { x } ) /\ x e. dom F ) -> E* z x F z )
23 moeu 
 |-  ( E* z x F z <-> ( E. z x F z -> E! z x F z ) )
24 22 23 sylib 
 |-  ( ( Fun ( F |` { x } ) /\ x e. dom F ) -> ( E. z x F z -> E! z x F z ) )
25 20 24 mpd 
 |-  ( ( Fun ( F |` { x } ) /\ x e. dom F ) -> E! z x F z )
26 iota1 
 |-  ( E! z x F z -> ( x F z <-> ( iota z x F z ) = z ) )
27 breq2 
 |-  ( z = y -> ( x F z <-> x F y ) )
28 27 cbviotavw 
 |-  ( iota z x F z ) = ( iota y x F y )
29 28 eqeq1i 
 |-  ( ( iota z x F z ) = z <-> ( iota y x F y ) = z )
30 26 29 bitr2di 
 |-  ( E! z x F z -> ( ( iota y x F y ) = z <-> x F z ) )
31 25 30 syl 
 |-  ( ( Fun ( F |` { x } ) /\ x e. dom F ) -> ( ( iota y x F y ) = z <-> x F z ) )
32 13 17 31 vtocl 
 |-  ( ( Fun ( F |` { x } ) /\ x e. dom F ) -> ( ( iota y x F y ) = ( iota y x F y ) <-> x F ( iota y x F y ) ) )
33 12 32 mpbii 
 |-  ( ( Fun ( F |` { x } ) /\ x e. dom F ) -> x F ( iota y x F y ) )
34 df-br 
 |-  ( x F ( iota y x F y ) <-> <. x , ( iota y x F y ) >. e. F )
35 33 34 sylib 
 |-  ( ( Fun ( F |` { x } ) /\ x e. dom F ) -> <. x , ( iota y x F y ) >. e. F )
36 vex 
 |-  x e. _V
37 opeq1 
 |-  ( z = x -> <. z , ( iota y x F y ) >. = <. x , ( iota y x F y ) >. )
38 37 eleq1d 
 |-  ( z = x -> ( <. z , ( iota y x F y ) >. e. F <-> <. x , ( iota y x F y ) >. e. F ) )
39 36 38 spcev 
 |-  ( <. x , ( iota y x F y ) >. e. F -> E. z <. z , ( iota y x F y ) >. e. F )
40 35 39 syl 
 |-  ( ( Fun ( F |` { x } ) /\ x e. dom F ) -> E. z <. z , ( iota y x F y ) >. e. F )
41 13 elrn2 
 |-  ( ( iota y x F y ) e. ran F <-> E. z <. z , ( iota y x F y ) >. e. F )
42 40 41 sylibr 
 |-  ( ( Fun ( F |` { x } ) /\ x e. dom F ) -> ( iota y x F y ) e. ran F )
43 11 42 vtoclg 
 |-  ( A e. dom F -> ( ( Fun ( F |` { A } ) /\ A e. dom F ) -> ( iota y A F y ) e. ran F ) )
44 43 anabsi6 
 |-  ( ( A e. dom F /\ Fun ( F |` { A } ) ) -> ( iota y A F y ) e. ran F )
45 2 44 sylbi 
 |-  ( F defAt A -> ( iota y A F y ) e. ran F )
46 1 45 eqeltrd 
 |-  ( F defAt A -> ( F '''' A ) e. ran F )