Description: Lemma for joinval2 and joineu . (Contributed by NM, 12-Sep-2018) TODO: combine this through joineu into joinlem ?
Ref | Expression | ||
---|---|---|---|
Hypotheses | joinval2.b | |
|
joinval2.l | |
||
joinval2.j | |
||
joinval2.k | |
||
joinval2.x | |
||
joinval2.y | |
||
Assertion | joinval2lem | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | joinval2.b | |
|
2 | joinval2.l | |
|
3 | joinval2.j | |
|
4 | joinval2.k | |
|
5 | joinval2.x | |
|
6 | joinval2.y | |
|
7 | breq1 | |
|
8 | breq1 | |
|
9 | 7 8 | ralprg | |
10 | breq1 | |
|
11 | breq1 | |
|
12 | 10 11 | ralprg | |
13 | 12 | imbi1d | |
14 | 13 | ralbidv | |
15 | 9 14 | anbi12d | |