Description: Finite product closure lemma. A version of fprodcllem using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 5-Apr-2020)
Ref | Expression | ||
---|---|---|---|
Hypotheses | fprodcllemf.ph | |
|
fprodcllemf.s | |
||
fprodcllemf.xy | |
||
fprodcllemf.a | |
||
fprodcllemf.b | |
||
fprodcllemf.1 | |
||
Assertion | fprodcllemf | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fprodcllemf.ph | |
|
2 | fprodcllemf.s | |
|
3 | fprodcllemf.xy | |
|
4 | fprodcllemf.a | |
|
5 | fprodcllemf.b | |
|
6 | fprodcllemf.1 | |
|
7 | nfcv | |
|
8 | nfcsb1v | |
|
9 | csbeq1a | |
|
10 | 7 8 9 | cbvprodi | |
11 | 5 | ex | |
12 | 1 11 | ralrimi | |
13 | rspsbc | |
|
14 | 12 13 | mpan9 | |
15 | sbcel1g | |
|
16 | 15 | elv | |
17 | 14 16 | sylib | |
18 | 2 3 4 17 6 | fprodcllem | |
19 | 10 18 | eqeltrid | |