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 ran F

Proof

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