Proof of Theorem omcl3g
Step | Hyp | Ref
| Expression |
1 | | eltpi 4684 |
. . . . 5
⊢ (𝐶 ∈ {∅, 1o,
2o} → (𝐶 =
∅ ∨ 𝐶 =
1o ∨ 𝐶 =
2o)) |
2 | | df-3o 8450 |
. . . . . 6
⊢
3o = suc 2o |
3 | | df2o3 8456 |
. . . . . . . 8
⊢
2o = {∅, 1o} |
4 | 3 | uneq1i 4155 |
. . . . . . 7
⊢
(2o ∪ {2o}) = ({∅, 1o} ∪
{2o}) |
5 | | df-suc 6359 |
. . . . . . 7
⊢ suc
2o = (2o ∪ {2o}) |
6 | | df-tp 4627 |
. . . . . . 7
⊢ {∅,
1o, 2o} = ({∅, 1o} ∪
{2o}) |
7 | 4, 5, 6 | 3eqtr4i 2769 |
. . . . . 6
⊢ suc
2o = {∅, 1o, 2o} |
8 | 2, 7 | eqtri 2759 |
. . . . 5
⊢
3o = {∅, 1o, 2o} |
9 | 1, 8 | eleq2s 2850 |
. . . 4
⊢ (𝐶 ∈ 3o →
(𝐶 = ∅ ∨ 𝐶 = 1o ∨ 𝐶 =
2o)) |
10 | | orc 865 |
. . . . . . 7
⊢ (𝐶 = ∅ → (𝐶 = ∅ ∨ (𝐶 = (ω ↑o
(ω ↑o 𝐶)) ∧ 𝐶 ∈ On))) |
11 | | omcl2 41854 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) ∧ (𝐶 = ∅ ∨ (𝐶 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On))) →
(𝐴 ·o
𝐵) ∈ 𝐶) |
12 | 10, 11 | sylan2 593 |
. . . . . 6
⊢ (((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) ∧ 𝐶 = ∅) → (𝐴 ·o 𝐵) ∈ 𝐶) |
13 | 12 | ex 413 |
. . . . 5
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → (𝐶 = ∅ → (𝐴 ·o 𝐵) ∈ 𝐶)) |
14 | | el1o 8477 |
. . . . . . . . 9
⊢ (𝐴 ∈ 1o ↔
𝐴 =
∅) |
15 | | el1o 8477 |
. . . . . . . . 9
⊢ (𝐵 ∈ 1o ↔
𝐵 =
∅) |
16 | | oveq12 7402 |
. . . . . . . . . 10
⊢ ((𝐴 = ∅ ∧ 𝐵 = ∅) → (𝐴 ·o 𝐵) = (∅
·o ∅)) |
17 | | 0elon 6407 |
. . . . . . . . . . . 12
⊢ ∅
∈ On |
18 | | om0 8499 |
. . . . . . . . . . . 12
⊢ (∅
∈ On → (∅ ·o ∅) =
∅) |
19 | 17, 18 | ax-mp 5 |
. . . . . . . . . . 11
⊢ (∅
·o ∅) = ∅ |
20 | | 0lt1o 8486 |
. . . . . . . . . . 11
⊢ ∅
∈ 1o |
21 | 19, 20 | eqeltri 2828 |
. . . . . . . . . 10
⊢ (∅
·o ∅) ∈ 1o |
22 | 16, 21 | eqeltrdi 2840 |
. . . . . . . . 9
⊢ ((𝐴 = ∅ ∧ 𝐵 = ∅) → (𝐴 ·o 𝐵) ∈
1o) |
23 | 14, 15, 22 | syl2anb 598 |
. . . . . . . 8
⊢ ((𝐴 ∈ 1o ∧
𝐵 ∈ 1o)
→ (𝐴
·o 𝐵)
∈ 1o) |
24 | 23 | a1i 11 |
. . . . . . 7
⊢ (𝐶 = 1o → ((𝐴 ∈ 1o ∧
𝐵 ∈ 1o)
→ (𝐴
·o 𝐵)
∈ 1o)) |
25 | | eleq2 2821 |
. . . . . . . 8
⊢ (𝐶 = 1o → (𝐴 ∈ 𝐶 ↔ 𝐴 ∈ 1o)) |
26 | | eleq2 2821 |
. . . . . . . 8
⊢ (𝐶 = 1o → (𝐵 ∈ 𝐶 ↔ 𝐵 ∈ 1o)) |
27 | 25, 26 | anbi12d 631 |
. . . . . . 7
⊢ (𝐶 = 1o → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) ↔ (𝐴 ∈ 1o ∧ 𝐵 ∈
1o))) |
28 | | eleq2 2821 |
. . . . . . 7
⊢ (𝐶 = 1o → ((𝐴 ·o 𝐵) ∈ 𝐶 ↔ (𝐴 ·o 𝐵) ∈ 1o)) |
29 | 24, 27, 28 | 3imtr4d 293 |
. . . . . 6
⊢ (𝐶 = 1o → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → (𝐴 ·o 𝐵) ∈ 𝐶)) |
30 | 29 | com12 32 |
. . . . 5
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → (𝐶 = 1o → (𝐴 ·o 𝐵) ∈ 𝐶)) |
31 | | elpri 4644 |
. . . . . . . . . 10
⊢ (𝐴 ∈ {∅, 1o}
→ (𝐴 = ∅ ∨
𝐴 =
1o)) |
32 | 31, 3 | eleq2s 2850 |
. . . . . . . . 9
⊢ (𝐴 ∈ 2o →
(𝐴 = ∅ ∨ 𝐴 =
1o)) |
33 | | elpri 4644 |
. . . . . . . . . 10
⊢ (𝐵 ∈ {∅, 1o}
→ (𝐵 = ∅ ∨
𝐵 =
1o)) |
34 | 33, 3 | eleq2s 2850 |
. . . . . . . . 9
⊢ (𝐵 ∈ 2o →
(𝐵 = ∅ ∨ 𝐵 =
1o)) |
35 | | 0ex 5300 |
. . . . . . . . . . . . 13
⊢ ∅
∈ V |
36 | 35 | prid1 4759 |
. . . . . . . . . . . 12
⊢ ∅
∈ {∅, 1o} |
37 | 36, 19, 3 | 3eltr4i 2845 |
. . . . . . . . . . 11
⊢ (∅
·o ∅) ∈ 2o |
38 | 16, 37 | eqeltrdi 2840 |
. . . . . . . . . 10
⊢ ((𝐴 = ∅ ∧ 𝐵 = ∅) → (𝐴 ·o 𝐵) ∈
2o) |
39 | | oveq12 7402 |
. . . . . . . . . . 11
⊢ ((𝐴 = 1o ∧ 𝐵 = ∅) → (𝐴 ·o 𝐵) = (1o
·o ∅)) |
40 | | 1on 8460 |
. . . . . . . . . . . . 13
⊢
1o ∈ On |
41 | | om0 8499 |
. . . . . . . . . . . . 13
⊢
(1o ∈ On → (1o ·o
∅) = ∅) |
42 | 40, 41 | ax-mp 5 |
. . . . . . . . . . . 12
⊢
(1o ·o ∅) = ∅ |
43 | 36, 42, 3 | 3eltr4i 2845 |
. . . . . . . . . . 11
⊢
(1o ·o ∅) ∈
2o |
44 | 39, 43 | eqeltrdi 2840 |
. . . . . . . . . 10
⊢ ((𝐴 = 1o ∧ 𝐵 = ∅) → (𝐴 ·o 𝐵) ∈
2o) |
45 | | oveq12 7402 |
. . . . . . . . . . 11
⊢ ((𝐴 = ∅ ∧ 𝐵 = 1o) → (𝐴 ·o 𝐵) = (∅
·o 1o)) |
46 | | om0r 8521 |
. . . . . . . . . . . . 13
⊢
(1o ∈ On → (∅ ·o
1o) = ∅) |
47 | 40, 46 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ (∅
·o 1o) = ∅ |
48 | 36, 47, 3 | 3eltr4i 2845 |
. . . . . . . . . . 11
⊢ (∅
·o 1o) ∈ 2o |
49 | 45, 48 | eqeltrdi 2840 |
. . . . . . . . . 10
⊢ ((𝐴 = ∅ ∧ 𝐵 = 1o) → (𝐴 ·o 𝐵) ∈
2o) |
50 | | oveq12 7402 |
. . . . . . . . . . 11
⊢ ((𝐴 = 1o ∧ 𝐵 = 1o) → (𝐴 ·o 𝐵) = (1o
·o 1o)) |
51 | | 1oex 8458 |
. . . . . . . . . . . . 13
⊢
1o ∈ V |
52 | 51 | prid2 4760 |
. . . . . . . . . . . 12
⊢
1o ∈ {∅, 1o} |
53 | | om1 8525 |
. . . . . . . . . . . . 13
⊢
(1o ∈ On → (1o ·o
1o) = 1o) |
54 | 40, 53 | ax-mp 5 |
. . . . . . . . . . . 12
⊢
(1o ·o 1o) =
1o |
55 | 52, 54, 3 | 3eltr4i 2845 |
. . . . . . . . . . 11
⊢
(1o ·o 1o) ∈
2o |
56 | 50, 55 | eqeltrdi 2840 |
. . . . . . . . . 10
⊢ ((𝐴 = 1o ∧ 𝐵 = 1o) → (𝐴 ·o 𝐵) ∈
2o) |
57 | 38, 44, 49, 56 | ccase 1036 |
. . . . . . . . 9
⊢ (((𝐴 = ∅ ∨ 𝐴 = 1o) ∧ (𝐵 = ∅ ∨ 𝐵 = 1o)) → (𝐴 ·o 𝐵) ∈
2o) |
58 | 32, 34, 57 | syl2an 596 |
. . . . . . . 8
⊢ ((𝐴 ∈ 2o ∧
𝐵 ∈ 2o)
→ (𝐴
·o 𝐵)
∈ 2o) |
59 | 58 | a1i 11 |
. . . . . . 7
⊢ (𝐶 = 2o → ((𝐴 ∈ 2o ∧
𝐵 ∈ 2o)
→ (𝐴
·o 𝐵)
∈ 2o)) |
60 | | eleq2 2821 |
. . . . . . . 8
⊢ (𝐶 = 2o → (𝐴 ∈ 𝐶 ↔ 𝐴 ∈ 2o)) |
61 | | eleq2 2821 |
. . . . . . . 8
⊢ (𝐶 = 2o → (𝐵 ∈ 𝐶 ↔ 𝐵 ∈ 2o)) |
62 | 60, 61 | anbi12d 631 |
. . . . . . 7
⊢ (𝐶 = 2o → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) ↔ (𝐴 ∈ 2o ∧ 𝐵 ∈
2o))) |
63 | | eleq2 2821 |
. . . . . . 7
⊢ (𝐶 = 2o → ((𝐴 ·o 𝐵) ∈ 𝐶 ↔ (𝐴 ·o 𝐵) ∈ 2o)) |
64 | 59, 62, 63 | 3imtr4d 293 |
. . . . . 6
⊢ (𝐶 = 2o → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → (𝐴 ·o 𝐵) ∈ 𝐶)) |
65 | 64 | com12 32 |
. . . . 5
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → (𝐶 = 2o → (𝐴 ·o 𝐵) ∈ 𝐶)) |
66 | 13, 30, 65 | 3jaod 1428 |
. . . 4
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → ((𝐶 = ∅ ∨ 𝐶 = 1o ∨ 𝐶 = 2o) → (𝐴 ·o 𝐵) ∈ 𝐶)) |
67 | 9, 66 | syl5 34 |
. . 3
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → (𝐶 ∈ 3o → (𝐴 ·o 𝐵) ∈ 𝐶)) |
68 | | olc 866 |
. . . . 5
⊢ ((𝐶 = (ω ↑o
(ω ↑o 𝐷)) ∧ 𝐷 ∈ On) → (𝐶 = ∅ ∨ (𝐶 = (ω ↑o (ω
↑o 𝐷))
∧ 𝐷 ∈
On))) |
69 | | omcl2 41854 |
. . . . 5
⊢ (((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) ∧ (𝐶 = ∅ ∨ (𝐶 = (ω ↑o (ω
↑o 𝐷))
∧ 𝐷 ∈ On))) →
(𝐴 ·o
𝐵) ∈ 𝐶) |
70 | 68, 69 | sylan2 593 |
. . . 4
⊢ (((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) ∧ (𝐶 = (ω ↑o (ω
↑o 𝐷))
∧ 𝐷 ∈ On)) →
(𝐴 ·o
𝐵) ∈ 𝐶) |
71 | 70 | ex 413 |
. . 3
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → ((𝐶 = (ω ↑o (ω
↑o 𝐷))
∧ 𝐷 ∈ On) →
(𝐴 ·o
𝐵) ∈ 𝐶)) |
72 | 67, 71 | jaod 857 |
. 2
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → ((𝐶 ∈ 3o ∨ (𝐶 = (ω ↑o
(ω ↑o 𝐷)) ∧ 𝐷 ∈ On)) → (𝐴 ·o 𝐵) ∈ 𝐶)) |
73 | 72 | imp 407 |
1
⊢ (((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) ∧ (𝐶 ∈ 3o ∨ (𝐶 = (ω ↑o
(ω ↑o 𝐷)) ∧ 𝐷 ∈ On))) → (𝐴 ·o 𝐵) ∈ 𝐶) |