Step |
Hyp |
Ref |
Expression |
1 |
|
efgval.w |
|- W = ( _I ` Word ( I X. 2o ) ) |
2 |
|
efgval.r |
|- .~ = ( ~FG ` I ) |
3 |
|
vex |
|- i e. _V |
4 |
|
2on |
|- 2o e. On |
5 |
4
|
elexi |
|- 2o e. _V |
6 |
3 5
|
xpex |
|- ( i X. 2o ) e. _V |
7 |
|
wrdexg |
|- ( ( i X. 2o ) e. _V -> Word ( i X. 2o ) e. _V ) |
8 |
|
fvi |
|- ( Word ( i X. 2o ) e. _V -> ( _I ` Word ( i X. 2o ) ) = Word ( i X. 2o ) ) |
9 |
6 7 8
|
mp2b |
|- ( _I ` Word ( i X. 2o ) ) = Word ( i X. 2o ) |
10 |
|
xpeq1 |
|- ( i = I -> ( i X. 2o ) = ( I X. 2o ) ) |
11 |
|
wrdeq |
|- ( ( i X. 2o ) = ( I X. 2o ) -> Word ( i X. 2o ) = Word ( I X. 2o ) ) |
12 |
10 11
|
syl |
|- ( i = I -> Word ( i X. 2o ) = Word ( I X. 2o ) ) |
13 |
12
|
fveq2d |
|- ( i = I -> ( _I ` Word ( i X. 2o ) ) = ( _I ` Word ( I X. 2o ) ) ) |
14 |
9 13
|
eqtr3id |
|- ( i = I -> Word ( i X. 2o ) = ( _I ` Word ( I X. 2o ) ) ) |
15 |
14 1
|
eqtr4di |
|- ( i = I -> Word ( i X. 2o ) = W ) |
16 |
|
ereq2 |
|- ( Word ( i X. 2o ) = W -> ( r Er Word ( i X. 2o ) <-> r Er W ) ) |
17 |
15 16
|
syl |
|- ( i = I -> ( r Er Word ( i X. 2o ) <-> r Er W ) ) |
18 |
|
raleq |
|- ( i = I -> ( A. y e. i A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) <-> A. y e. I A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) ) ) |
19 |
18
|
ralbidv |
|- ( i = I -> ( A. n e. ( 0 ... ( # ` x ) ) A. y e. i A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) <-> A. n e. ( 0 ... ( # ` x ) ) A. y e. I A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) ) ) |
20 |
15 19
|
raleqbidv |
|- ( i = I -> ( A. x e. Word ( i X. 2o ) A. n e. ( 0 ... ( # ` x ) ) A. y e. i A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) <-> A. x e. W A. n e. ( 0 ... ( # ` x ) ) A. y e. I A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) ) ) |
21 |
17 20
|
anbi12d |
|- ( i = I -> ( ( r Er Word ( i X. 2o ) /\ A. x e. Word ( i X. 2o ) A. n e. ( 0 ... ( # ` x ) ) A. y e. i A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) ) <-> ( r Er W /\ A. x e. W A. n e. ( 0 ... ( # ` x ) ) A. y e. I A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) ) ) ) |
22 |
21
|
abbidv |
|- ( i = I -> { r | ( r Er Word ( i X. 2o ) /\ A. x e. Word ( i X. 2o ) A. n e. ( 0 ... ( # ` x ) ) A. y e. i A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) ) } = { r | ( r Er W /\ A. x e. W A. n e. ( 0 ... ( # ` x ) ) A. y e. I A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) ) } ) |
23 |
22
|
inteqd |
|- ( i = I -> |^| { r | ( r Er Word ( i X. 2o ) /\ A. x e. Word ( i X. 2o ) A. n e. ( 0 ... ( # ` x ) ) A. y e. i A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) ) } = |^| { r | ( r Er W /\ A. x e. W A. n e. ( 0 ... ( # ` x ) ) A. y e. I A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) ) } ) |
24 |
|
df-efg |
|- ~FG = ( i e. _V |-> |^| { r | ( r Er Word ( i X. 2o ) /\ A. x e. Word ( i X. 2o ) A. n e. ( 0 ... ( # ` x ) ) A. y e. i A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) ) } ) |
25 |
1
|
efglem |
|- E. r ( r Er W /\ A. x e. W A. n e. ( 0 ... ( # ` x ) ) A. y e. I A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) ) |
26 |
|
intexab |
|- ( E. r ( r Er W /\ A. x e. W A. n e. ( 0 ... ( # ` x ) ) A. y e. I A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) ) <-> |^| { r | ( r Er W /\ A. x e. W A. n e. ( 0 ... ( # ` x ) ) A. y e. I A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) ) } e. _V ) |
27 |
25 26
|
mpbi |
|- |^| { r | ( r Er W /\ A. x e. W A. n e. ( 0 ... ( # ` x ) ) A. y e. I A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) ) } e. _V |
28 |
23 24 27
|
fvmpt |
|- ( I e. _V -> ( ~FG ` I ) = |^| { r | ( r Er W /\ A. x e. W A. n e. ( 0 ... ( # ` x ) ) A. y e. I A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) ) } ) |
29 |
|
fvprc |
|- ( -. I e. _V -> ( ~FG ` I ) = (/) ) |
30 |
|
abn0 |
|- ( { r | ( r Er W /\ A. x e. W A. n e. ( 0 ... ( # ` x ) ) A. y e. I A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) ) } =/= (/) <-> E. r ( r Er W /\ A. x e. W A. n e. ( 0 ... ( # ` x ) ) A. y e. I A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) ) ) |
31 |
25 30
|
mpbir |
|- { r | ( r Er W /\ A. x e. W A. n e. ( 0 ... ( # ` x ) ) A. y e. I A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) ) } =/= (/) |
32 |
|
intssuni |
|- ( { r | ( r Er W /\ A. x e. W A. n e. ( 0 ... ( # ` x ) ) A. y e. I A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) ) } =/= (/) -> |^| { r | ( r Er W /\ A. x e. W A. n e. ( 0 ... ( # ` x ) ) A. y e. I A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) ) } C_ U. { r | ( r Er W /\ A. x e. W A. n e. ( 0 ... ( # ` x ) ) A. y e. I A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) ) } ) |
33 |
31 32
|
ax-mp |
|- |^| { r | ( r Er W /\ A. x e. W A. n e. ( 0 ... ( # ` x ) ) A. y e. I A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) ) } C_ U. { r | ( r Er W /\ A. x e. W A. n e. ( 0 ... ( # ` x ) ) A. y e. I A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) ) } |
34 |
|
erssxp |
|- ( r Er W -> r C_ ( W X. W ) ) |
35 |
1
|
efgrcl |
|- ( x e. W -> ( I e. _V /\ W = Word ( I X. 2o ) ) ) |
36 |
35
|
simpld |
|- ( x e. W -> I e. _V ) |
37 |
36
|
con3i |
|- ( -. I e. _V -> -. x e. W ) |
38 |
37
|
eq0rdv |
|- ( -. I e. _V -> W = (/) ) |
39 |
38
|
xpeq2d |
|- ( -. I e. _V -> ( W X. W ) = ( W X. (/) ) ) |
40 |
|
xp0 |
|- ( W X. (/) ) = (/) |
41 |
39 40
|
eqtrdi |
|- ( -. I e. _V -> ( W X. W ) = (/) ) |
42 |
|
ss0b |
|- ( ( W X. W ) C_ (/) <-> ( W X. W ) = (/) ) |
43 |
41 42
|
sylibr |
|- ( -. I e. _V -> ( W X. W ) C_ (/) ) |
44 |
34 43
|
sylan9ssr |
|- ( ( -. I e. _V /\ r Er W ) -> r C_ (/) ) |
45 |
44
|
ex |
|- ( -. I e. _V -> ( r Er W -> r C_ (/) ) ) |
46 |
45
|
adantrd |
|- ( -. I e. _V -> ( ( r Er W /\ A. x e. W A. n e. ( 0 ... ( # ` x ) ) A. y e. I A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) ) -> r C_ (/) ) ) |
47 |
46
|
alrimiv |
|- ( -. I e. _V -> A. r ( ( r Er W /\ A. x e. W A. n e. ( 0 ... ( # ` x ) ) A. y e. I A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) ) -> r C_ (/) ) ) |
48 |
|
sseq1 |
|- ( w = r -> ( w C_ (/) <-> r C_ (/) ) ) |
49 |
48
|
ralab2 |
|- ( A. w e. { r | ( r Er W /\ A. x e. W A. n e. ( 0 ... ( # ` x ) ) A. y e. I A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) ) } w C_ (/) <-> A. r ( ( r Er W /\ A. x e. W A. n e. ( 0 ... ( # ` x ) ) A. y e. I A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) ) -> r C_ (/) ) ) |
50 |
47 49
|
sylibr |
|- ( -. I e. _V -> A. w e. { r | ( r Er W /\ A. x e. W A. n e. ( 0 ... ( # ` x ) ) A. y e. I A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) ) } w C_ (/) ) |
51 |
|
unissb |
|- ( U. { r | ( r Er W /\ A. x e. W A. n e. ( 0 ... ( # ` x ) ) A. y e. I A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) ) } C_ (/) <-> A. w e. { r | ( r Er W /\ A. x e. W A. n e. ( 0 ... ( # ` x ) ) A. y e. I A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) ) } w C_ (/) ) |
52 |
50 51
|
sylibr |
|- ( -. I e. _V -> U. { r | ( r Er W /\ A. x e. W A. n e. ( 0 ... ( # ` x ) ) A. y e. I A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) ) } C_ (/) ) |
53 |
33 52
|
sstrid |
|- ( -. I e. _V -> |^| { r | ( r Er W /\ A. x e. W A. n e. ( 0 ... ( # ` x ) ) A. y e. I A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) ) } C_ (/) ) |
54 |
|
ss0 |
|- ( |^| { r | ( r Er W /\ A. x e. W A. n e. ( 0 ... ( # ` x ) ) A. y e. I A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) ) } C_ (/) -> |^| { r | ( r Er W /\ A. x e. W A. n e. ( 0 ... ( # ` x ) ) A. y e. I A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) ) } = (/) ) |
55 |
53 54
|
syl |
|- ( -. I e. _V -> |^| { r | ( r Er W /\ A. x e. W A. n e. ( 0 ... ( # ` x ) ) A. y e. I A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) ) } = (/) ) |
56 |
29 55
|
eqtr4d |
|- ( -. I e. _V -> ( ~FG ` I ) = |^| { r | ( r Er W /\ A. x e. W A. n e. ( 0 ... ( # ` x ) ) A. y e. I A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) ) } ) |
57 |
28 56
|
pm2.61i |
|- ( ~FG ` I ) = |^| { r | ( r Er W /\ A. x e. W A. n e. ( 0 ... ( # ` x ) ) A. y e. I A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) ) } |
58 |
2 57
|
eqtri |
|- .~ = |^| { r | ( r Er W /\ A. x e. W A. n e. ( 0 ... ( # ` x ) ) A. y e. I A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) ) } |