Description: Ordering law for cardinal addition. Theorem 6L(a) of Enderton p. 149. (Contributed by NM, 28-Sep-2004) (Revised by Mario Carneiro, 29-Apr-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | djudom2 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | djudom1 | |
|
2 | reldom | |
|
3 | 2 | brrelex1i | |
4 | djucomen | |
|
5 | 3 4 | sylan | |
6 | 2 | brrelex2i | |
7 | djucomen | |
|
8 | 6 7 | sylan | |
9 | domen1 | |
|
10 | domen2 | |
|
11 | 9 10 | sylan9bb | |
12 | 5 8 11 | syl2anc | |
13 | 1 12 | mpbid | |