Description: Closure of the "variable selection" function. (Contributed by SN, 22-Feb-2024)
Ref | Expression | ||
---|---|---|---|
Hypotheses | selvcl.p | |
|
selvcl.b | |
||
selvcl.u | |
||
selvcl.t | |
||
selvcl.e | |
||
selvcl.i | |
||
selvcl.r | |
||
selvcl.j | |
||
selvcl.f | |
||
Assertion | selvcl | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | selvcl.p | |
|
2 | selvcl.b | |
|
3 | selvcl.u | |
|
4 | selvcl.t | |
|
5 | selvcl.e | |
|
6 | selvcl.i | |
|
7 | selvcl.r | |
|
8 | selvcl.j | |
|
9 | selvcl.f | |
|
10 | eqid | |
|
11 | eqid | |
|
12 | 1 2 3 4 10 11 6 7 8 9 | selvval | |
13 | eqid | |
|
14 | eqid | |
|
15 | 6 8 | ssexd | |
16 | 6 | difexd | |
17 | 3 | mplcrng | |
18 | 16 7 17 | syl2anc | |
19 | 4 | mplcrng | |
20 | 15 18 19 | syl2anc | |
21 | ovexd | |
|
22 | eqid | |
|
23 | eqid | |
|
24 | eqid | |
|
25 | 3 4 10 11 22 23 24 13 5 6 7 8 | selvval2lemn | |
26 | eqid | |
|
27 | 26 14 | rhmf | |
28 | 25 27 | syl | |
29 | 1 2 3 4 10 11 24 23 26 6 7 8 9 | selvval2lem4 | |
30 | 28 29 | ffvelrnd | |
31 | 13 5 14 20 21 30 | pwselbas | |
32 | eqid | |
|
33 | 3 4 10 5 32 6 7 8 | selvval2lem5 | |
34 | 31 33 | ffvelrnd | |
35 | 12 34 | eqeltrd | |