Proof of Theorem omeulem2
Step | Hyp | Ref
| Expression |
1 | | simp3l 1082 |
. . . . . 6
⊢ (((𝐴 ∈ On ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ On ∧ 𝐶 ∈ 𝐴) ∧ (𝐷 ∈ On ∧ 𝐸 ∈ 𝐴)) → 𝐷 ∈ On) |
2 | | eloni 5650 |
. . . . . 6
⊢ (𝐷 ∈ On → Ord 𝐷) |
3 | | ordsucss 6910 |
. . . . . 6
⊢ (Ord
𝐷 → (𝐵 ∈ 𝐷 → suc 𝐵 ⊆ 𝐷)) |
4 | 1, 2, 3 | 3syl 18 |
. . . . 5
⊢ (((𝐴 ∈ On ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ On ∧ 𝐶 ∈ 𝐴) ∧ (𝐷 ∈ On ∧ 𝐸 ∈ 𝐴)) → (𝐵 ∈ 𝐷 → suc 𝐵 ⊆ 𝐷)) |
5 | | simp2l 1080 |
. . . . . . 7
⊢ (((𝐴 ∈ On ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ On ∧ 𝐶 ∈ 𝐴) ∧ (𝐷 ∈ On ∧ 𝐸 ∈ 𝐴)) → 𝐵 ∈ On) |
6 | | suceloni 6905 |
. . . . . . 7
⊢ (𝐵 ∈ On → suc 𝐵 ∈ On) |
7 | 5, 6 | syl 17 |
. . . . . 6
⊢ (((𝐴 ∈ On ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ On ∧ 𝐶 ∈ 𝐴) ∧ (𝐷 ∈ On ∧ 𝐸 ∈ 𝐴)) → suc 𝐵 ∈ On) |
8 | | simp1l 1078 |
. . . . . 6
⊢ (((𝐴 ∈ On ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ On ∧ 𝐶 ∈ 𝐴) ∧ (𝐷 ∈ On ∧ 𝐸 ∈ 𝐴)) → 𝐴 ∈ On) |
9 | | simp1r 1079 |
. . . . . . 7
⊢ (((𝐴 ∈ On ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ On ∧ 𝐶 ∈ 𝐴) ∧ (𝐷 ∈ On ∧ 𝐸 ∈ 𝐴)) → 𝐴 ≠ ∅) |
10 | | on0eln0 5697 |
. . . . . . . 8
⊢ (𝐴 ∈ On → (∅
∈ 𝐴 ↔ 𝐴 ≠ ∅)) |
11 | 8, 10 | syl 17 |
. . . . . . 7
⊢ (((𝐴 ∈ On ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ On ∧ 𝐶 ∈ 𝐴) ∧ (𝐷 ∈ On ∧ 𝐸 ∈ 𝐴)) → (∅ ∈ 𝐴 ↔ 𝐴 ≠ ∅)) |
12 | 9, 11 | mpbird 246 |
. . . . . 6
⊢ (((𝐴 ∈ On ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ On ∧ 𝐶 ∈ 𝐴) ∧ (𝐷 ∈ On ∧ 𝐸 ∈ 𝐴)) → ∅ ∈ 𝐴) |
13 | | omword 7537 |
. . . . . 6
⊢ (((suc
𝐵 ∈ On ∧ 𝐷 ∈ On ∧ 𝐴 ∈ On) ∧ ∅ ∈
𝐴) → (suc 𝐵 ⊆ 𝐷 ↔ (𝐴 ·𝑜 suc 𝐵) ⊆ (𝐴 ·𝑜 𝐷))) |
14 | 7, 1, 8, 12, 13 | syl31anc 1321 |
. . . . 5
⊢ (((𝐴 ∈ On ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ On ∧ 𝐶 ∈ 𝐴) ∧ (𝐷 ∈ On ∧ 𝐸 ∈ 𝐴)) → (suc 𝐵 ⊆ 𝐷 ↔ (𝐴 ·𝑜 suc 𝐵) ⊆ (𝐴 ·𝑜 𝐷))) |
15 | 4, 14 | sylibd 228 |
. . . 4
⊢ (((𝐴 ∈ On ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ On ∧ 𝐶 ∈ 𝐴) ∧ (𝐷 ∈ On ∧ 𝐸 ∈ 𝐴)) → (𝐵 ∈ 𝐷 → (𝐴 ·𝑜 suc 𝐵) ⊆ (𝐴 ·𝑜 𝐷))) |
16 | | omcl 7503 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ 𝐷 ∈ On) → (𝐴 ·𝑜
𝐷) ∈
On) |
17 | 8, 1, 16 | syl2anc 691 |
. . . . 5
⊢ (((𝐴 ∈ On ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ On ∧ 𝐶 ∈ 𝐴) ∧ (𝐷 ∈ On ∧ 𝐸 ∈ 𝐴)) → (𝐴 ·𝑜 𝐷) ∈ On) |
18 | | simp3r 1083 |
. . . . . 6
⊢ (((𝐴 ∈ On ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ On ∧ 𝐶 ∈ 𝐴) ∧ (𝐷 ∈ On ∧ 𝐸 ∈ 𝐴)) → 𝐸 ∈ 𝐴) |
19 | | onelon 5665 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ 𝐸 ∈ 𝐴) → 𝐸 ∈ On) |
20 | 8, 18, 19 | syl2anc 691 |
. . . . 5
⊢ (((𝐴 ∈ On ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ On ∧ 𝐶 ∈ 𝐴) ∧ (𝐷 ∈ On ∧ 𝐸 ∈ 𝐴)) → 𝐸 ∈ On) |
21 | | oaword1 7519 |
. . . . . 6
⊢ (((𝐴 ·𝑜
𝐷) ∈ On ∧ 𝐸 ∈ On) → (𝐴 ·𝑜
𝐷) ⊆ ((𝐴 ·𝑜
𝐷) +𝑜
𝐸)) |
22 | | sstr 3576 |
. . . . . . 7
⊢ (((𝐴 ·𝑜
suc 𝐵) ⊆ (𝐴 ·𝑜
𝐷) ∧ (𝐴 ·𝑜 𝐷) ⊆ ((𝐴 ·𝑜 𝐷) +𝑜 𝐸)) → (𝐴 ·𝑜 suc 𝐵) ⊆ ((𝐴 ·𝑜 𝐷) +𝑜 𝐸)) |
23 | 22 | expcom 450 |
. . . . . 6
⊢ ((𝐴 ·𝑜
𝐷) ⊆ ((𝐴 ·𝑜
𝐷) +𝑜
𝐸) → ((𝐴 ·𝑜
suc 𝐵) ⊆ (𝐴 ·𝑜
𝐷) → (𝐴 ·𝑜
suc 𝐵) ⊆ ((𝐴 ·𝑜
𝐷) +𝑜
𝐸))) |
24 | 21, 23 | syl 17 |
. . . . 5
⊢ (((𝐴 ·𝑜
𝐷) ∈ On ∧ 𝐸 ∈ On) → ((𝐴 ·𝑜
suc 𝐵) ⊆ (𝐴 ·𝑜
𝐷) → (𝐴 ·𝑜
suc 𝐵) ⊆ ((𝐴 ·𝑜
𝐷) +𝑜
𝐸))) |
25 | 17, 20, 24 | syl2anc 691 |
. . . 4
⊢ (((𝐴 ∈ On ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ On ∧ 𝐶 ∈ 𝐴) ∧ (𝐷 ∈ On ∧ 𝐸 ∈ 𝐴)) → ((𝐴 ·𝑜 suc 𝐵) ⊆ (𝐴 ·𝑜 𝐷) → (𝐴 ·𝑜 suc 𝐵) ⊆ ((𝐴 ·𝑜 𝐷) +𝑜 𝐸))) |
26 | 15, 25 | syld 46 |
. . 3
⊢ (((𝐴 ∈ On ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ On ∧ 𝐶 ∈ 𝐴) ∧ (𝐷 ∈ On ∧ 𝐸 ∈ 𝐴)) → (𝐵 ∈ 𝐷 → (𝐴 ·𝑜 suc 𝐵) ⊆ ((𝐴 ·𝑜 𝐷) +𝑜 𝐸))) |
27 | | simp2r 1081 |
. . . . . 6
⊢ (((𝐴 ∈ On ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ On ∧ 𝐶 ∈ 𝐴) ∧ (𝐷 ∈ On ∧ 𝐸 ∈ 𝐴)) → 𝐶 ∈ 𝐴) |
28 | | onelon 5665 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ 𝐶 ∈ 𝐴) → 𝐶 ∈ On) |
29 | 8, 27, 28 | syl2anc 691 |
. . . . 5
⊢ (((𝐴 ∈ On ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ On ∧ 𝐶 ∈ 𝐴) ∧ (𝐷 ∈ On ∧ 𝐸 ∈ 𝐴)) → 𝐶 ∈ On) |
30 | | omcl 7503 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ·𝑜
𝐵) ∈
On) |
31 | 8, 5, 30 | syl2anc 691 |
. . . . 5
⊢ (((𝐴 ∈ On ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ On ∧ 𝐶 ∈ 𝐴) ∧ (𝐷 ∈ On ∧ 𝐸 ∈ 𝐴)) → (𝐴 ·𝑜 𝐵) ∈ On) |
32 | | oaord 7514 |
. . . . . 6
⊢ ((𝐶 ∈ On ∧ 𝐴 ∈ On ∧ (𝐴 ·𝑜
𝐵) ∈ On) → (𝐶 ∈ 𝐴 ↔ ((𝐴 ·𝑜 𝐵) +𝑜 𝐶) ∈ ((𝐴 ·𝑜 𝐵) +𝑜 𝐴))) |
33 | 32 | biimpa 500 |
. . . . 5
⊢ (((𝐶 ∈ On ∧ 𝐴 ∈ On ∧ (𝐴 ·𝑜
𝐵) ∈ On) ∧ 𝐶 ∈ 𝐴) → ((𝐴 ·𝑜 𝐵) +𝑜 𝐶) ∈ ((𝐴 ·𝑜 𝐵) +𝑜 𝐴)) |
34 | 29, 8, 31, 27, 33 | syl31anc 1321 |
. . . 4
⊢ (((𝐴 ∈ On ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ On ∧ 𝐶 ∈ 𝐴) ∧ (𝐷 ∈ On ∧ 𝐸 ∈ 𝐴)) → ((𝐴 ·𝑜 𝐵) +𝑜 𝐶) ∈ ((𝐴 ·𝑜 𝐵) +𝑜 𝐴)) |
35 | | omsuc 7493 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ·𝑜
suc 𝐵) = ((𝐴 ·𝑜
𝐵) +𝑜
𝐴)) |
36 | 8, 5, 35 | syl2anc 691 |
. . . 4
⊢ (((𝐴 ∈ On ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ On ∧ 𝐶 ∈ 𝐴) ∧ (𝐷 ∈ On ∧ 𝐸 ∈ 𝐴)) → (𝐴 ·𝑜 suc 𝐵) = ((𝐴 ·𝑜 𝐵) +𝑜 𝐴)) |
37 | 34, 36 | eleqtrrd 2691 |
. . 3
⊢ (((𝐴 ∈ On ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ On ∧ 𝐶 ∈ 𝐴) ∧ (𝐷 ∈ On ∧ 𝐸 ∈ 𝐴)) → ((𝐴 ·𝑜 𝐵) +𝑜 𝐶) ∈ (𝐴 ·𝑜 suc 𝐵)) |
38 | | ssel 3562 |
. . 3
⊢ ((𝐴 ·𝑜
suc 𝐵) ⊆ ((𝐴 ·𝑜
𝐷) +𝑜
𝐸) → (((𝐴 ·𝑜
𝐵) +𝑜
𝐶) ∈ (𝐴 ·𝑜
suc 𝐵) → ((𝐴 ·𝑜
𝐵) +𝑜
𝐶) ∈ ((𝐴 ·𝑜
𝐷) +𝑜
𝐸))) |
39 | 26, 37, 38 | syl6ci 69 |
. 2
⊢ (((𝐴 ∈ On ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ On ∧ 𝐶 ∈ 𝐴) ∧ (𝐷 ∈ On ∧ 𝐸 ∈ 𝐴)) → (𝐵 ∈ 𝐷 → ((𝐴 ·𝑜 𝐵) +𝑜 𝐶) ∈ ((𝐴 ·𝑜 𝐷) +𝑜 𝐸))) |
40 | | simpr 476 |
. . . . 5
⊢ ((𝐵 = 𝐷 ∧ 𝐶 ∈ 𝐸) → 𝐶 ∈ 𝐸) |
41 | | oaord 7514 |
. . . . 5
⊢ ((𝐶 ∈ On ∧ 𝐸 ∈ On ∧ (𝐴 ·𝑜
𝐵) ∈ On) → (𝐶 ∈ 𝐸 ↔ ((𝐴 ·𝑜 𝐵) +𝑜 𝐶) ∈ ((𝐴 ·𝑜 𝐵) +𝑜 𝐸))) |
42 | 40, 41 | syl5ib 233 |
. . . 4
⊢ ((𝐶 ∈ On ∧ 𝐸 ∈ On ∧ (𝐴 ·𝑜
𝐵) ∈ On) →
((𝐵 = 𝐷 ∧ 𝐶 ∈ 𝐸) → ((𝐴 ·𝑜 𝐵) +𝑜 𝐶) ∈ ((𝐴 ·𝑜 𝐵) +𝑜 𝐸))) |
43 | | oveq2 6557 |
. . . . . . 7
⊢ (𝐵 = 𝐷 → (𝐴 ·𝑜 𝐵) = (𝐴 ·𝑜 𝐷)) |
44 | 43 | oveq1d 6564 |
. . . . . 6
⊢ (𝐵 = 𝐷 → ((𝐴 ·𝑜 𝐵) +𝑜 𝐸) = ((𝐴 ·𝑜 𝐷) +𝑜 𝐸)) |
45 | 44 | adantr 480 |
. . . . 5
⊢ ((𝐵 = 𝐷 ∧ 𝐶 ∈ 𝐸) → ((𝐴 ·𝑜 𝐵) +𝑜 𝐸) = ((𝐴 ·𝑜 𝐷) +𝑜 𝐸)) |
46 | 45 | eleq2d 2673 |
. . . 4
⊢ ((𝐵 = 𝐷 ∧ 𝐶 ∈ 𝐸) → (((𝐴 ·𝑜 𝐵) +𝑜 𝐶) ∈ ((𝐴 ·𝑜 𝐵) +𝑜 𝐸) ↔ ((𝐴 ·𝑜 𝐵) +𝑜 𝐶) ∈ ((𝐴 ·𝑜 𝐷) +𝑜 𝐸))) |
47 | 42, 46 | mpbidi 230 |
. . 3
⊢ ((𝐶 ∈ On ∧ 𝐸 ∈ On ∧ (𝐴 ·𝑜
𝐵) ∈ On) →
((𝐵 = 𝐷 ∧ 𝐶 ∈ 𝐸) → ((𝐴 ·𝑜 𝐵) +𝑜 𝐶) ∈ ((𝐴 ·𝑜 𝐷) +𝑜 𝐸))) |
48 | 29, 20, 31, 47 | syl3anc 1318 |
. 2
⊢ (((𝐴 ∈ On ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ On ∧ 𝐶 ∈ 𝐴) ∧ (𝐷 ∈ On ∧ 𝐸 ∈ 𝐴)) → ((𝐵 = 𝐷 ∧ 𝐶 ∈ 𝐸) → ((𝐴 ·𝑜 𝐵) +𝑜 𝐶) ∈ ((𝐴 ·𝑜 𝐷) +𝑜 𝐸))) |
49 | 39, 48 | jaod 394 |
1
⊢ (((𝐴 ∈ On ∧ 𝐴 ≠ ∅) ∧ (𝐵 ∈ On ∧ 𝐶 ∈ 𝐴) ∧ (𝐷 ∈ On ∧ 𝐸 ∈ 𝐴)) → ((𝐵 ∈ 𝐷 ∨ (𝐵 = 𝐷 ∧ 𝐶 ∈ 𝐸)) → ((𝐴 ·𝑜 𝐵) +𝑜 𝐶) ∈ ((𝐴 ·𝑜 𝐷) +𝑜 𝐸))) |