Description: Two ways to say that a join is defined. (Contributed by NM, 9-Sep-2018)
Ref | Expression | ||
---|---|---|---|
Hypotheses | joindef.u | |
|
joindef.j | |
||
joindef.k | |
||
joindef.x | |
||
joindef.y | |
||
Assertion | joindef | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | joindef.u | |
|
2 | joindef.j | |
|
3 | joindef.k | |
|
4 | joindef.x | |
|
5 | joindef.y | |
|
6 | 1 2 | joindm | |
7 | 6 | eleq2d | |
8 | 3 7 | syl | |
9 | preq1 | |
|
10 | 9 | eleq1d | |
11 | preq2 | |
|
12 | 11 | eleq1d | |
13 | 10 12 | opelopabg | |
14 | 4 5 13 | syl2anc | |
15 | 8 14 | bitrd | |