Metamath Proof Explorer

Theorem omopth2

Description: An ordered pair-like theorem for ordinal multiplication. (Contributed by Mario Carneiro, 29-May-2015)

Ref Expression
Assertion omopth2 ⊢A∈On∧A≠∅∧B∈On∧C∈A∧D∈On∧E∈A→A⋅𝑜B+𝑜C=A⋅𝑜D+𝑜E↔B=D∧C=E

Proof

Step Hyp Ref Expression
1 simpl2l ⊢A∈On∧A≠∅∧B∈On∧C∈A∧D∈On∧E∈A∧A⋅𝑜B+𝑜C=A⋅𝑜D+𝑜E→B∈On
2 eloni ⊢B∈On→Ord⁡B
3 1 2 syl ⊢A∈On∧A≠∅∧B∈On∧C∈A∧D∈On∧E∈A∧A⋅𝑜B+𝑜C=A⋅𝑜D+𝑜E→Ord⁡B
4 simpl3l ⊢A∈On∧A≠∅∧B∈On∧C∈A∧D∈On∧E∈A∧A⋅𝑜B+𝑜C=A⋅𝑜D+𝑜E→D∈On
5 eloni ⊢D∈On→Ord⁡D
6 4 5 syl ⊢A∈On∧A≠∅∧B∈On∧C∈A∧D∈On∧E∈A∧A⋅𝑜B+𝑜C=A⋅𝑜D+𝑜E→Ord⁡D
7 ordtri3or ⊢Ord⁡B∧Ord⁡D→B∈D∨B=D∨D∈B
8 3 6 7 syl2anc ⊢A∈On∧A≠∅∧B∈On∧C∈A∧D∈On∧E∈A∧A⋅𝑜B+𝑜C=A⋅𝑜D+𝑜E→B∈D∨B=D∨D∈B
9 simpr ⊢A∈On∧A≠∅∧B∈On∧C∈A∧D∈On∧E∈A∧A⋅𝑜B+𝑜C=A⋅𝑜D+𝑜E→A⋅𝑜B+𝑜C=A⋅𝑜D+𝑜E
10 simpl1l ⊢A∈On∧A≠∅∧B∈On∧C∈A∧D∈On∧E∈A∧A⋅𝑜B+𝑜C=A⋅𝑜D+𝑜E→A∈On
11 omcl ⊢A∈On∧D∈On→A⋅𝑜D∈On
12 10 4 11 syl2anc ⊢A∈On∧A≠∅∧B∈On∧C∈A∧D∈On∧E∈A∧A⋅𝑜B+𝑜C=A⋅𝑜D+𝑜E→A⋅𝑜D∈On
13 simpl3r ⊢A∈On∧A≠∅∧B∈On∧C∈A∧D∈On∧E∈A∧A⋅𝑜B+𝑜C=A⋅𝑜D+𝑜E→E∈A
14 onelon ⊢A∈On∧E∈A→E∈On
15 10 13 14 syl2anc ⊢A∈On∧A≠∅∧B∈On∧C∈A∧D∈On∧E∈A∧A⋅𝑜B+𝑜C=A⋅𝑜D+𝑜E→E∈On
16 oacl ⊢A⋅𝑜D∈On∧E∈On→A⋅𝑜D+𝑜E∈On
17 12 15 16 syl2anc ⊢A∈On∧A≠∅∧B∈On∧C∈A∧D∈On∧E∈A∧A⋅𝑜B+𝑜C=A⋅𝑜D+𝑜E→A⋅𝑜D+𝑜E∈On
18 eloni ⊢A⋅𝑜D+𝑜E∈On→Ord⁡A⋅𝑜D+𝑜E
19 ordirr ⊢Ord⁡A⋅𝑜D+𝑜E→¬A⋅𝑜D+𝑜E∈A⋅𝑜D+𝑜E
20 17 18 19 3syl ⊢A∈On∧A≠∅∧B∈On∧C∈A∧D∈On∧E∈A∧A⋅𝑜B+𝑜C=A⋅𝑜D+𝑜E→¬A⋅𝑜D+𝑜E∈A⋅𝑜D+𝑜E
21 9 20 eqneltrd ⊢A∈On∧A≠∅∧B∈On∧C∈A∧D∈On∧E∈A∧A⋅𝑜B+𝑜C=A⋅𝑜D+𝑜E→¬A⋅𝑜B+𝑜C∈A⋅𝑜D+𝑜E
22 orc ⊢B∈D→B∈D∨B=D∧C∈E
23 omeulem2 ⊢A∈On∧A≠∅∧B∈On∧C∈A∧D∈On∧E∈A→B∈D∨B=D∧C∈E→A⋅𝑜B+𝑜C∈A⋅𝑜D+𝑜E
24 23 adantr ⊢A∈On∧A≠∅∧B∈On∧C∈A∧D∈On∧E∈A∧A⋅𝑜B+𝑜C=A⋅𝑜D+𝑜E→B∈D∨B=D∧C∈E→A⋅𝑜B+𝑜C∈A⋅𝑜D+𝑜E
25 22 24 syl5 ⊢A∈On∧A≠∅∧B∈On∧C∈A∧D∈On∧E∈A∧A⋅𝑜B+𝑜C=A⋅𝑜D+𝑜E→B∈D→A⋅𝑜B+𝑜C∈A⋅𝑜D+𝑜E
26 21 25 mtod ⊢A∈On∧A≠∅∧B∈On∧C∈A∧D∈On∧E∈A∧A⋅𝑜B+𝑜C=A⋅𝑜D+𝑜E→¬B∈D
27 26 pm2.21d ⊢A∈On∧A≠∅∧B∈On∧C∈A∧D∈On∧E∈A∧A⋅𝑜B+𝑜C=A⋅𝑜D+𝑜E→B∈D→B=D
28 idd ⊢A∈On∧A≠∅∧B∈On∧C∈A∧D∈On∧E∈A∧A⋅𝑜B+𝑜C=A⋅𝑜D+𝑜E→B=D→B=D
29 20 9 neleqtrrd ⊢A∈On∧A≠∅∧B∈On∧C∈A∧D∈On∧E∈A∧A⋅𝑜B+𝑜C=A⋅𝑜D+𝑜E→¬A⋅𝑜D+𝑜E∈A⋅𝑜B+𝑜C
30 orc ⊢D∈B→D∈B∨D=B∧E∈C
31 simpl1r ⊢A∈On∧A≠∅∧B∈On∧C∈A∧D∈On∧E∈A∧A⋅𝑜B+𝑜C=A⋅𝑜D+𝑜E→A≠∅
32 simpl2r ⊢A∈On∧A≠∅∧B∈On∧C∈A∧D∈On∧E∈A∧A⋅𝑜B+𝑜C=A⋅𝑜D+𝑜E→C∈A
33 omeulem2 ⊢A∈On∧A≠∅∧D∈On∧E∈A∧B∈On∧C∈A→D∈B∨D=B∧E∈C→A⋅𝑜D+𝑜E∈A⋅𝑜B+𝑜C
34 10 31 4 13 1 32 33 syl222anc ⊢A∈On∧A≠∅∧B∈On∧C∈A∧D∈On∧E∈A∧A⋅𝑜B+𝑜C=A⋅𝑜D+𝑜E→D∈B∨D=B∧E∈C→A⋅𝑜D+𝑜E∈A⋅𝑜B+𝑜C
35 30 34 syl5 ⊢A∈On∧A≠∅∧B∈On∧C∈A∧D∈On∧E∈A∧A⋅𝑜B+𝑜C=A⋅𝑜D+𝑜E→D∈B→A⋅𝑜D+𝑜E∈A⋅𝑜B+𝑜C
36 29 35 mtod ⊢A∈On∧A≠∅∧B∈On∧C∈A∧D∈On∧E∈A∧A⋅𝑜B+𝑜C=A⋅𝑜D+𝑜E→¬D∈B
37 36 pm2.21d ⊢A∈On∧A≠∅∧B∈On∧C∈A∧D∈On∧E∈A∧A⋅𝑜B+𝑜C=A⋅𝑜D+𝑜E→D∈B→B=D
38 27 28 37 3jaod ⊢A∈On∧A≠∅∧B∈On∧C∈A∧D∈On∧E∈A∧A⋅𝑜B+𝑜C=A⋅𝑜D+𝑜E→B∈D∨B=D∨D∈B→B=D
39 8 38 mpd ⊢A∈On∧A≠∅∧B∈On∧C∈A∧D∈On∧E∈A∧A⋅𝑜B+𝑜C=A⋅𝑜D+𝑜E→B=D
40 onelon ⊢A∈On∧C∈A→C∈On
41 eloni ⊢C∈On→Ord⁡C
42 40 41 syl ⊢A∈On∧C∈A→Ord⁡C
43 10 32 42 syl2anc ⊢A∈On∧A≠∅∧B∈On∧C∈A∧D∈On∧E∈A∧A⋅𝑜B+𝑜C=A⋅𝑜D+𝑜E→Ord⁡C
44 eloni ⊢E∈On→Ord⁡E
45 14 44 syl ⊢A∈On∧E∈A→Ord⁡E
46 10 13 45 syl2anc ⊢A∈On∧A≠∅∧B∈On∧C∈A∧D∈On∧E∈A∧A⋅𝑜B+𝑜C=A⋅𝑜D+𝑜E→Ord⁡E
47 ordtri3or ⊢Ord⁡C∧Ord⁡E→C∈E∨C=E∨E∈C
48 43 46 47 syl2anc ⊢A∈On∧A≠∅∧B∈On∧C∈A∧D∈On∧E∈A∧A⋅𝑜B+𝑜C=A⋅𝑜D+𝑜E→C∈E∨C=E∨E∈C
49 olc ⊢B=D∧C∈E→B∈D∨B=D∧C∈E
50 49 24 syl5 ⊢A∈On∧A≠∅∧B∈On∧C∈A∧D∈On∧E∈A∧A⋅𝑜B+𝑜C=A⋅𝑜D+𝑜E→B=D∧C∈E→A⋅𝑜B+𝑜C∈A⋅𝑜D+𝑜E
51 39 50 mpand ⊢A∈On∧A≠∅∧B∈On∧C∈A∧D∈On∧E∈A∧A⋅𝑜B+𝑜C=A⋅𝑜D+𝑜E→C∈E→A⋅𝑜B+𝑜C∈A⋅𝑜D+𝑜E
52 21 51 mtod ⊢A∈On∧A≠∅∧B∈On∧C∈A∧D∈On∧E∈A∧A⋅𝑜B+𝑜C=A⋅𝑜D+𝑜E→¬C∈E
53 52 pm2.21d ⊢A∈On∧A≠∅∧B∈On∧C∈A∧D∈On∧E∈A∧A⋅𝑜B+𝑜C=A⋅𝑜D+𝑜E→C∈E→C=E
54 idd ⊢A∈On∧A≠∅∧B∈On∧C∈A∧D∈On∧E∈A∧A⋅𝑜B+𝑜C=A⋅𝑜D+𝑜E→C=E→C=E
55 39 eqcomd ⊢A∈On∧A≠∅∧B∈On∧C∈A∧D∈On∧E∈A∧A⋅𝑜B+𝑜C=A⋅𝑜D+𝑜E→D=B
56 olc ⊢D=B∧E∈C→D∈B∨D=B∧E∈C
57 56 34 syl5 ⊢A∈On∧A≠∅∧B∈On∧C∈A∧D∈On∧E∈A∧A⋅𝑜B+𝑜C=A⋅𝑜D+𝑜E→D=B∧E∈C→A⋅𝑜D+𝑜E∈A⋅𝑜B+𝑜C
58 55 57 mpand ⊢A∈On∧A≠∅∧B∈On∧C∈A∧D∈On∧E∈A∧A⋅𝑜B+𝑜C=A⋅𝑜D+𝑜E→E∈C→A⋅𝑜D+𝑜E∈A⋅𝑜B+𝑜C
59 29 58 mtod ⊢A∈On∧A≠∅∧B∈On∧C∈A∧D∈On∧E∈A∧A⋅𝑜B+𝑜C=A⋅𝑜D+𝑜E→¬E∈C
60 59 pm2.21d ⊢A∈On∧A≠∅∧B∈On∧C∈A∧D∈On∧E∈A∧A⋅𝑜B+𝑜C=A⋅𝑜D+𝑜E→E∈C→C=E
61 53 54 60 3jaod ⊢A∈On∧A≠∅∧B∈On∧C∈A∧D∈On∧E∈A∧A⋅𝑜B+𝑜C=A⋅𝑜D+𝑜E→C∈E∨C=E∨E∈C→C=E
62 48 61 mpd ⊢A∈On∧A≠∅∧B∈On∧C∈A∧D∈On∧E∈A∧A⋅𝑜B+𝑜C=A⋅𝑜D+𝑜E→C=E
63 39 62 jca ⊢A∈On∧A≠∅∧B∈On∧C∈A∧D∈On∧E∈A∧A⋅𝑜B+𝑜C=A⋅𝑜D+𝑜E→B=D∧C=E
64 63 ex ⊢A∈On∧A≠∅∧B∈On∧C∈A∧D∈On∧E∈A→A⋅𝑜B+𝑜C=A⋅𝑜D+𝑜E→B=D∧C=E
65 oveq2 ⊢B=D→A⋅𝑜B=A⋅𝑜D
66 id ⊢C=E→C=E
67 65 66 oveqan12d ⊢B=D∧C=E→A⋅𝑜B+𝑜C=A⋅𝑜D+𝑜E
68 64 67 impbid1 ⊢A∈On∧A≠∅∧B∈On∧C∈A∧D∈On∧E∈A→A⋅𝑜B+𝑜C=A⋅𝑜D+𝑜E↔B=D∧C=E