Description: Hypothesis builder for function operation. (Contributed by Mario Carneiro, 20-Jul-2014)
Ref | Expression | ||
---|---|---|---|
Hypothesis | nfof.1 | |- F/_ x R |
|
Assertion | nfof | |- F/_ x oF R |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfof.1 | |- F/_ x R |
|
2 | df-of | |- oF R = ( u e. _V , v e. _V |-> ( w e. ( dom u i^i dom v ) |-> ( ( u ` w ) R ( v ` w ) ) ) ) |
|
3 | nfcv | |- F/_ x _V |
|
4 | nfcv | |- F/_ x ( dom u i^i dom v ) |
|
5 | nfcv | |- F/_ x ( u ` w ) |
|
6 | nfcv | |- F/_ x ( v ` w ) |
|
7 | 5 1 6 | nfov | |- F/_ x ( ( u ` w ) R ( v ` w ) ) |
8 | 4 7 | nfmpt | |- F/_ x ( w e. ( dom u i^i dom v ) |-> ( ( u ` w ) R ( v ` w ) ) ) |
9 | 3 3 8 | nfmpo | |- F/_ x ( u e. _V , v e. _V |-> ( w e. ( dom u i^i dom v ) |-> ( ( u ` w ) R ( v ` w ) ) ) ) |
10 | 2 9 | nfcxfr | |- F/_ x oF R |