Step |
Hyp |
Ref |
Expression |
1 |
|
elex |
|- ( I e. V -> I e. _V ) |
2 |
|
nfcv |
|- F/_ y K |
3 |
|
nfcsb1v |
|- F/_ x [_ y / x ]_ K |
4 |
|
csbeq1a |
|- ( x = y -> K = [_ y / x ]_ K ) |
5 |
2 3 4
|
cbvixp |
|- X_ x e. I K = X_ y e. I [_ y / x ]_ K |
6 |
5
|
eleq2i |
|- ( ( x e. I |-> J ) e. X_ x e. I K <-> ( x e. I |-> J ) e. X_ y e. I [_ y / x ]_ K ) |
7 |
|
elixp2 |
|- ( ( x e. I |-> J ) e. X_ y e. I [_ y / x ]_ K <-> ( ( x e. I |-> J ) e. _V /\ ( x e. I |-> J ) Fn I /\ A. y e. I ( ( x e. I |-> J ) ` y ) e. [_ y / x ]_ K ) ) |
8 |
|
3anass |
|- ( ( ( x e. I |-> J ) e. _V /\ ( x e. I |-> J ) Fn I /\ A. y e. I ( ( x e. I |-> J ) ` y ) e. [_ y / x ]_ K ) <-> ( ( x e. I |-> J ) e. _V /\ ( ( x e. I |-> J ) Fn I /\ A. y e. I ( ( x e. I |-> J ) ` y ) e. [_ y / x ]_ K ) ) ) |
9 |
6 7 8
|
3bitri |
|- ( ( x e. I |-> J ) e. X_ x e. I K <-> ( ( x e. I |-> J ) e. _V /\ ( ( x e. I |-> J ) Fn I /\ A. y e. I ( ( x e. I |-> J ) ` y ) e. [_ y / x ]_ K ) ) ) |
10 |
|
eqid |
|- ( x e. I |-> J ) = ( x e. I |-> J ) |
11 |
10
|
fnmpt |
|- ( A. x e. I J e. K -> ( x e. I |-> J ) Fn I ) |
12 |
10
|
fvmpt2 |
|- ( ( x e. I /\ J e. K ) -> ( ( x e. I |-> J ) ` x ) = J ) |
13 |
|
simpr |
|- ( ( x e. I /\ J e. K ) -> J e. K ) |
14 |
12 13
|
eqeltrd |
|- ( ( x e. I /\ J e. K ) -> ( ( x e. I |-> J ) ` x ) e. K ) |
15 |
14
|
ralimiaa |
|- ( A. x e. I J e. K -> A. x e. I ( ( x e. I |-> J ) ` x ) e. K ) |
16 |
11 15
|
jca |
|- ( A. x e. I J e. K -> ( ( x e. I |-> J ) Fn I /\ A. x e. I ( ( x e. I |-> J ) ` x ) e. K ) ) |
17 |
|
dffn2 |
|- ( ( x e. I |-> J ) Fn I <-> ( x e. I |-> J ) : I --> _V ) |
18 |
10
|
fmpt |
|- ( A. x e. I J e. _V <-> ( x e. I |-> J ) : I --> _V ) |
19 |
10
|
fvmpt2 |
|- ( ( x e. I /\ J e. _V ) -> ( ( x e. I |-> J ) ` x ) = J ) |
20 |
19
|
eleq1d |
|- ( ( x e. I /\ J e. _V ) -> ( ( ( x e. I |-> J ) ` x ) e. K <-> J e. K ) ) |
21 |
20
|
biimpd |
|- ( ( x e. I /\ J e. _V ) -> ( ( ( x e. I |-> J ) ` x ) e. K -> J e. K ) ) |
22 |
21
|
ralimiaa |
|- ( A. x e. I J e. _V -> A. x e. I ( ( ( x e. I |-> J ) ` x ) e. K -> J e. K ) ) |
23 |
|
ralim |
|- ( A. x e. I ( ( ( x e. I |-> J ) ` x ) e. K -> J e. K ) -> ( A. x e. I ( ( x e. I |-> J ) ` x ) e. K -> A. x e. I J e. K ) ) |
24 |
22 23
|
syl |
|- ( A. x e. I J e. _V -> ( A. x e. I ( ( x e. I |-> J ) ` x ) e. K -> A. x e. I J e. K ) ) |
25 |
18 24
|
sylbir |
|- ( ( x e. I |-> J ) : I --> _V -> ( A. x e. I ( ( x e. I |-> J ) ` x ) e. K -> A. x e. I J e. K ) ) |
26 |
17 25
|
sylbi |
|- ( ( x e. I |-> J ) Fn I -> ( A. x e. I ( ( x e. I |-> J ) ` x ) e. K -> A. x e. I J e. K ) ) |
27 |
26
|
imp |
|- ( ( ( x e. I |-> J ) Fn I /\ A. x e. I ( ( x e. I |-> J ) ` x ) e. K ) -> A. x e. I J e. K ) |
28 |
16 27
|
impbii |
|- ( A. x e. I J e. K <-> ( ( x e. I |-> J ) Fn I /\ A. x e. I ( ( x e. I |-> J ) ` x ) e. K ) ) |
29 |
|
nfv |
|- F/ y ( ( x e. I |-> J ) ` x ) e. K |
30 |
|
nffvmpt1 |
|- F/_ x ( ( x e. I |-> J ) ` y ) |
31 |
30 3
|
nfel |
|- F/ x ( ( x e. I |-> J ) ` y ) e. [_ y / x ]_ K |
32 |
|
fveq2 |
|- ( x = y -> ( ( x e. I |-> J ) ` x ) = ( ( x e. I |-> J ) ` y ) ) |
33 |
32 4
|
eleq12d |
|- ( x = y -> ( ( ( x e. I |-> J ) ` x ) e. K <-> ( ( x e. I |-> J ) ` y ) e. [_ y / x ]_ K ) ) |
34 |
29 31 33
|
cbvralw |
|- ( A. x e. I ( ( x e. I |-> J ) ` x ) e. K <-> A. y e. I ( ( x e. I |-> J ) ` y ) e. [_ y / x ]_ K ) |
35 |
34
|
anbi2i |
|- ( ( ( x e. I |-> J ) Fn I /\ A. x e. I ( ( x e. I |-> J ) ` x ) e. K ) <-> ( ( x e. I |-> J ) Fn I /\ A. y e. I ( ( x e. I |-> J ) ` y ) e. [_ y / x ]_ K ) ) |
36 |
28 35
|
bitri |
|- ( A. x e. I J e. K <-> ( ( x e. I |-> J ) Fn I /\ A. y e. I ( ( x e. I |-> J ) ` y ) e. [_ y / x ]_ K ) ) |
37 |
|
mptexg |
|- ( I e. _V -> ( x e. I |-> J ) e. _V ) |
38 |
37
|
biantrurd |
|- ( I e. _V -> ( ( ( x e. I |-> J ) Fn I /\ A. y e. I ( ( x e. I |-> J ) ` y ) e. [_ y / x ]_ K ) <-> ( ( x e. I |-> J ) e. _V /\ ( ( x e. I |-> J ) Fn I /\ A. y e. I ( ( x e. I |-> J ) ` y ) e. [_ y / x ]_ K ) ) ) ) |
39 |
36 38
|
bitr2id |
|- ( I e. _V -> ( ( ( x e. I |-> J ) e. _V /\ ( ( x e. I |-> J ) Fn I /\ A. y e. I ( ( x e. I |-> J ) ` y ) e. [_ y / x ]_ K ) ) <-> A. x e. I J e. K ) ) |
40 |
9 39
|
syl5bb |
|- ( I e. _V -> ( ( x e. I |-> J ) e. X_ x e. I K <-> A. x e. I J e. K ) ) |
41 |
1 40
|
syl |
|- ( I e. V -> ( ( x e. I |-> J ) e. X_ x e. I K <-> A. x e. I J e. K ) ) |