Step |
Hyp |
Ref |
Expression |
1 |
|
eqeq1 |
|- ( y = A -> ( y = (/) <-> A = (/) ) ) |
2 |
|
oveq2 |
|- ( y = A -> ( x .o y ) = ( x .o A ) ) |
3 |
2
|
mpteq2dv |
|- ( y = A -> ( x e. _V |-> ( x .o y ) ) = ( x e. _V |-> ( x .o A ) ) ) |
4 |
|
rdgeq1 |
|- ( ( x e. _V |-> ( x .o y ) ) = ( x e. _V |-> ( x .o A ) ) -> rec ( ( x e. _V |-> ( x .o y ) ) , 1o ) = rec ( ( x e. _V |-> ( x .o A ) ) , 1o ) ) |
5 |
3 4
|
syl |
|- ( y = A -> rec ( ( x e. _V |-> ( x .o y ) ) , 1o ) = rec ( ( x e. _V |-> ( x .o A ) ) , 1o ) ) |
6 |
5
|
fveq1d |
|- ( y = A -> ( rec ( ( x e. _V |-> ( x .o y ) ) , 1o ) ` z ) = ( rec ( ( x e. _V |-> ( x .o A ) ) , 1o ) ` z ) ) |
7 |
1 6
|
ifbieq2d |
|- ( y = A -> if ( y = (/) , ( 1o \ z ) , ( rec ( ( x e. _V |-> ( x .o y ) ) , 1o ) ` z ) ) = if ( A = (/) , ( 1o \ z ) , ( rec ( ( x e. _V |-> ( x .o A ) ) , 1o ) ` z ) ) ) |
8 |
|
difeq2 |
|- ( z = B -> ( 1o \ z ) = ( 1o \ B ) ) |
9 |
|
fveq2 |
|- ( z = B -> ( rec ( ( x e. _V |-> ( x .o A ) ) , 1o ) ` z ) = ( rec ( ( x e. _V |-> ( x .o A ) ) , 1o ) ` B ) ) |
10 |
8 9
|
ifeq12d |
|- ( z = B -> if ( A = (/) , ( 1o \ z ) , ( rec ( ( x e. _V |-> ( x .o A ) ) , 1o ) ` z ) ) = if ( A = (/) , ( 1o \ B ) , ( rec ( ( x e. _V |-> ( x .o A ) ) , 1o ) ` B ) ) ) |
11 |
|
df-oexp |
|- ^o = ( y e. On , z e. On |-> if ( y = (/) , ( 1o \ z ) , ( rec ( ( x e. _V |-> ( x .o y ) ) , 1o ) ` z ) ) ) |
12 |
|
1oex |
|- 1o e. _V |
13 |
12
|
difexi |
|- ( 1o \ B ) e. _V |
14 |
|
fvex |
|- ( rec ( ( x e. _V |-> ( x .o A ) ) , 1o ) ` B ) e. _V |
15 |
13 14
|
ifex |
|- if ( A = (/) , ( 1o \ B ) , ( rec ( ( x e. _V |-> ( x .o A ) ) , 1o ) ` B ) ) e. _V |
16 |
7 10 11 15
|
ovmpo |
|- ( ( A e. On /\ B e. On ) -> ( A ^o B ) = if ( A = (/) , ( 1o \ B ) , ( rec ( ( x e. _V |-> ( x .o A ) ) , 1o ) ` B ) ) ) |