Description: Restriction of an element of an infinite Cartesian product. (Contributed by FL, 7-Nov-2011) (Proof shortened by Mario Carneiro, 31-May-2014)
Ref | Expression | ||
---|---|---|---|
Assertion | resixp | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | resexg | |
|
2 | 1 | adantl | |
3 | simpr | |
|
4 | elixp2 | |
|
5 | 3 4 | sylib | |
6 | 5 | simp2d | |
7 | simpl | |
|
8 | fnssres | |
|
9 | 6 7 8 | syl2anc | |
10 | 5 | simp3d | |
11 | ssralv | |
|
12 | 7 10 11 | sylc | |
13 | fvres | |
|
14 | 13 | eleq1d | |
15 | 14 | ralbiia | |
16 | 12 15 | sylibr | |
17 | elixp2 | |
|
18 | 2 9 16 17 | syl3anbrc | |