Metamath Proof Explorer


Theorem djudom2

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 ABCVC⊔︀AC⊔︀B

Proof

Step Hyp Ref Expression
1 djudom1 ABCVA⊔︀CB⊔︀C
2 reldom Rel
3 2 brrelex1i ABAV
4 djucomen AVCVA⊔︀CC⊔︀A
5 3 4 sylan ABCVA⊔︀CC⊔︀A
6 2 brrelex2i ABBV
7 djucomen BVCVB⊔︀CC⊔︀B
8 6 7 sylan ABCVB⊔︀CC⊔︀B
9 domen1 A⊔︀CC⊔︀AA⊔︀CB⊔︀CC⊔︀AB⊔︀C
10 domen2 B⊔︀CC⊔︀BC⊔︀AB⊔︀CC⊔︀AC⊔︀B
11 9 10 sylan9bb A⊔︀CC⊔︀AB⊔︀CC⊔︀BA⊔︀CB⊔︀CC⊔︀AC⊔︀B
12 5 8 11 syl2anc ABCVA⊔︀CB⊔︀CC⊔︀AC⊔︀B
13 1 12 mpbid ABCVC⊔︀AC⊔︀B