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