Metamath Proof Explorer

Theorem oaord

Description: Ordering property of ordinal addition. Proposition 8.4 of TakeutiZaring p. 58 and its converse. (Contributed by NM, 5-Dec-2004)

Ref Expression
Assertion oaord ⊢A∈On∧B∈On∧C∈On→A∈B↔C+𝑜A∈C+𝑜B

Proof

Step Hyp Ref Expression
1 oaordi ⊢B∈On∧C∈On→A∈B→C+𝑜A∈C+𝑜B
2 1 3adant1 ⊢A∈On∧B∈On∧C∈On→A∈B→C+𝑜A∈C+𝑜B
3 oveq2 ⊢A=B→C+𝑜A=C+𝑜B
4 3 a1i ⊢A∈On∧B∈On∧C∈On→A=B→C+𝑜A=C+𝑜B
5 oaordi ⊢A∈On∧C∈On→B∈A→C+𝑜B∈C+𝑜A
6 5 3adant2 ⊢A∈On∧B∈On∧C∈On→B∈A→C+𝑜B∈C+𝑜A
7 4 6 orim12d ⊢A∈On∧B∈On∧C∈On→A=B∨B∈A→C+𝑜A=C+𝑜B∨C+𝑜B∈C+𝑜A
8 7 con3d ⊢A∈On∧B∈On∧C∈On→¬C+𝑜A=C+𝑜B∨C+𝑜B∈C+𝑜A→¬A=B∨B∈A
9 df-3an ⊢A∈On∧B∈On∧C∈On↔A∈On∧B∈On∧C∈On
10 ancom ⊢A∈On∧B∈On∧C∈On↔C∈On∧A∈On∧B∈On
11 anandi ⊢C∈On∧A∈On∧B∈On↔C∈On∧A∈On∧C∈On∧B∈On
12 9 10 11 3bitri ⊢A∈On∧B∈On∧C∈On↔C∈On∧A∈On∧C∈On∧B∈On
13 oacl ⊢C∈On∧A∈On→C+𝑜A∈On
14 eloni ⊢C+𝑜A∈On→Ord⁡C+𝑜A
15 13 14 syl ⊢C∈On∧A∈On→Ord⁡C+𝑜A
16 oacl ⊢C∈On∧B∈On→C+𝑜B∈On
17 eloni ⊢C+𝑜B∈On→Ord⁡C+𝑜B
18 16 17 syl ⊢C∈On∧B∈On→Ord⁡C+𝑜B
19 15 18 anim12i ⊢C∈On∧A∈On∧C∈On∧B∈On→Ord⁡C+𝑜A∧Ord⁡C+𝑜B
20 12 19 sylbi ⊢A∈On∧B∈On∧C∈On→Ord⁡C+𝑜A∧Ord⁡C+𝑜B
21 ordtri2 ⊢Ord⁡C+𝑜A∧Ord⁡C+𝑜B→C+𝑜A∈C+𝑜B↔¬C+𝑜A=C+𝑜B∨C+𝑜B∈C+𝑜A
22 20 21 syl ⊢A∈On∧B∈On∧C∈On→C+𝑜A∈C+𝑜B↔¬C+𝑜A=C+𝑜B∨C+𝑜B∈C+𝑜A
23 eloni ⊢A∈On→Ord⁡A
24 eloni ⊢B∈On→Ord⁡B
25 23 24 anim12i ⊢A∈On∧B∈On→Ord⁡A∧Ord⁡B
26 25 3adant3 ⊢A∈On∧B∈On∧C∈On→Ord⁡A∧Ord⁡B
27 ordtri2 ⊢Ord⁡A∧Ord⁡B→A∈B↔¬A=B∨B∈A
28 26 27 syl ⊢A∈On∧B∈On∧C∈On→A∈B↔¬A=B∨B∈A
29 8 22 28 3imtr4d ⊢A∈On∧B∈On∧C∈On→C+𝑜A∈C+𝑜B→A∈B
30 2 29 impbid ⊢A∈On∧B∈On∧C∈On→A∈B↔C+𝑜A∈C+𝑜B