Step | Hyp | Ref
| Expression |
1 | | elnn 4271 |
. . . . . 6
⊢
((A ∈ B ∧ B ∈ 𝜔) → A ∈
𝜔) |
2 | 1 | expcom 109 |
. . . . 5
⊢ (B ∈ 𝜔
→ (A ∈ B →
A ∈
𝜔)) |
3 | | eleq2 2098 |
. . . . . . . . . . 11
⊢ (x = B →
(A ∈
x ↔ A ∈ B)) |
4 | | oveq2 5463 |
. . . . . . . . . . . 12
⊢ (x = B →
(𝐶
·𝑜 x) = (𝐶 ·𝑜
B)) |
5 | 4 | eleq2d 2104 |
. . . . . . . . . . 11
⊢ (x = B →
((𝐶
·𝑜 A) ∈ (𝐶 ·𝑜 x) ↔ (𝐶 ·𝑜 A) ∈ (𝐶 ·𝑜
B))) |
6 | 3, 5 | imbi12d 223 |
. . . . . . . . . 10
⊢ (x = B →
((A ∈
x → (𝐶 ·𝑜 A) ∈ (𝐶 ·𝑜
x)) ↔ (A ∈ B → (𝐶 ·𝑜 A) ∈ (𝐶 ·𝑜
B)))) |
7 | 6 | imbi2d 219 |
. . . . . . . . 9
⊢ (x = B →
((((A ∈
𝜔 ∧ 𝐶 ∈
𝜔) ∧ ∅ ∈ 𝐶) → (A ∈ x → (𝐶 ·𝑜 A) ∈ (𝐶 ·𝑜
x))) ↔ (((A ∈ 𝜔
∧ 𝐶 ∈
𝜔) ∧ ∅ ∈ 𝐶) → (A ∈ B → (𝐶 ·𝑜 A) ∈ (𝐶 ·𝑜
B))))) |
8 | | eleq2 2098 |
. . . . . . . . . . 11
⊢ (x = ∅ → (A ∈ x ↔ A ∈ ∅)) |
9 | | oveq2 5463 |
. . . . . . . . . . . 12
⊢ (x = ∅ → (𝐶 ·𝑜 x) = (𝐶 ·𝑜
∅)) |
10 | 9 | eleq2d 2104 |
. . . . . . . . . . 11
⊢ (x = ∅ → ((𝐶 ·𝑜 A) ∈ (𝐶 ·𝑜
x) ↔ (𝐶 ·𝑜 A) ∈ (𝐶 ·𝑜
∅))) |
11 | 8, 10 | imbi12d 223 |
. . . . . . . . . 10
⊢ (x = ∅ → ((A ∈ x → (𝐶 ·𝑜 A) ∈ (𝐶 ·𝑜
x)) ↔ (A ∈ ∅ →
(𝐶
·𝑜 A) ∈ (𝐶 ·𝑜
∅)))) |
12 | | eleq2 2098 |
. . . . . . . . . . 11
⊢ (x = y →
(A ∈
x ↔ A ∈ y)) |
13 | | oveq2 5463 |
. . . . . . . . . . . 12
⊢ (x = y →
(𝐶
·𝑜 x) = (𝐶 ·𝑜
y)) |
14 | 13 | eleq2d 2104 |
. . . . . . . . . . 11
⊢ (x = y →
((𝐶
·𝑜 A) ∈ (𝐶 ·𝑜 x) ↔ (𝐶 ·𝑜 A) ∈ (𝐶 ·𝑜
y))) |
15 | 12, 14 | imbi12d 223 |
. . . . . . . . . 10
⊢ (x = y →
((A ∈
x → (𝐶 ·𝑜 A) ∈ (𝐶 ·𝑜
x)) ↔ (A ∈ y → (𝐶 ·𝑜 A) ∈ (𝐶 ·𝑜
y)))) |
16 | | eleq2 2098 |
. . . . . . . . . . 11
⊢ (x = suc y →
(A ∈
x ↔ A ∈ suc y)) |
17 | | oveq2 5463 |
. . . . . . . . . . . 12
⊢ (x = suc y →
(𝐶
·𝑜 x) = (𝐶 ·𝑜
suc y)) |
18 | 17 | eleq2d 2104 |
. . . . . . . . . . 11
⊢ (x = suc y →
((𝐶
·𝑜 A) ∈ (𝐶 ·𝑜 x) ↔ (𝐶 ·𝑜 A) ∈ (𝐶 ·𝑜
suc y))) |
19 | 16, 18 | imbi12d 223 |
. . . . . . . . . 10
⊢ (x = suc y →
((A ∈
x → (𝐶 ·𝑜 A) ∈ (𝐶 ·𝑜
x)) ↔ (A ∈ suc y → (𝐶 ·𝑜 A) ∈ (𝐶 ·𝑜
suc y)))) |
20 | | noel 3222 |
. . . . . . . . . . . 12
⊢ ¬
A ∈
∅ |
21 | 20 | pm2.21i 574 |
. . . . . . . . . . 11
⊢ (A ∈ ∅ →
(𝐶
·𝑜 A) ∈ (𝐶 ·𝑜
∅)) |
22 | 21 | a1i 9 |
. . . . . . . . . 10
⊢
(((A ∈ 𝜔 ∧
𝐶 ∈ 𝜔) ∧
∅ ∈ 𝐶) → (A ∈ ∅ →
(𝐶
·𝑜 A) ∈ (𝐶 ·𝑜
∅))) |
23 | | elsuci 4106 |
. . . . . . . . . . . . . . . 16
⊢ (A ∈ suc y → (A
∈ y ∨ A = y)) |
24 | | nnmcl 5999 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐶 ∈ 𝜔 ∧
y ∈
𝜔) → (𝐶
·𝑜 y) ∈ 𝜔) |
25 | | simpl 102 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐶 ∈ 𝜔 ∧
y ∈
𝜔) → 𝐶 ∈ 𝜔) |
26 | 24, 25 | jca 290 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐶 ∈ 𝜔 ∧
y ∈
𝜔) → ((𝐶
·𝑜 y) ∈ 𝜔 ∧
𝐶 ∈ 𝜔)) |
27 | | nnaword1 6022 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐶 ·𝑜
y) ∈
𝜔 ∧ 𝐶 ∈
𝜔) → (𝐶
·𝑜 y) ⊆
((𝐶
·𝑜 y)
+𝑜 𝐶)) |
28 | 27 | sseld 2938 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐶 ·𝑜
y) ∈
𝜔 ∧ 𝐶 ∈
𝜔) → ((𝐶
·𝑜 A) ∈ (𝐶 ·𝑜 y) → (𝐶 ·𝑜 A) ∈ ((𝐶 ·𝑜
y) +𝑜 𝐶))) |
29 | 28 | imim2d 48 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐶 ·𝑜
y) ∈
𝜔 ∧ 𝐶 ∈
𝜔) → ((A ∈ y →
(𝐶
·𝑜 A) ∈ (𝐶 ·𝑜 y)) → (A
∈ y
→ (𝐶
·𝑜 A) ∈ ((𝐶 ·𝑜 y) +𝑜 𝐶)))) |
30 | 29 | imp 115 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐶 ·𝑜
y) ∈
𝜔 ∧ 𝐶 ∈
𝜔) ∧ (A ∈ y → (𝐶 ·𝑜 A) ∈ (𝐶 ·𝑜
y))) → (A ∈ y → (𝐶 ·𝑜 A) ∈ ((𝐶 ·𝑜
y) +𝑜 𝐶))) |
31 | 30 | adantrl 447 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐶 ·𝑜
y) ∈
𝜔 ∧ 𝐶 ∈
𝜔) ∧ (∅ ∈ 𝐶 ∧
(A ∈
y → (𝐶 ·𝑜 A) ∈ (𝐶 ·𝑜
y)))) → (A ∈ y → (𝐶 ·𝑜 A) ∈ ((𝐶 ·𝑜
y) +𝑜 𝐶))) |
32 | | nna0 5992 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐶 ·𝑜
y) ∈
𝜔 → ((𝐶
·𝑜 y)
+𝑜 ∅) = (𝐶 ·𝑜 y)) |
33 | 32 | ad2antrr 457 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐶 ·𝑜
y) ∈
𝜔 ∧ 𝐶 ∈
𝜔) ∧ ∅ ∈ 𝐶) → ((𝐶 ·𝑜 y) +𝑜 ∅) = (𝐶 ·𝑜
y)) |
34 | | nnaordi 6017 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐶 ∈ 𝜔 ∧
(𝐶
·𝑜 y) ∈ 𝜔) → (∅ ∈ 𝐶 → ((𝐶 ·𝑜 y) +𝑜 ∅) ∈ ((𝐶 ·𝑜 y) +𝑜 𝐶))) |
35 | 34 | ancoms 255 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐶 ·𝑜
y) ∈
𝜔 ∧ 𝐶 ∈
𝜔) → (∅ ∈ 𝐶 → ((𝐶 ·𝑜 y) +𝑜 ∅) ∈ ((𝐶 ·𝑜 y) +𝑜 𝐶))) |
36 | 35 | imp 115 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐶 ·𝑜
y) ∈
𝜔 ∧ 𝐶 ∈
𝜔) ∧ ∅ ∈ 𝐶) → ((𝐶 ·𝑜 y) +𝑜 ∅) ∈ ((𝐶 ·𝑜 y) +𝑜 𝐶)) |
37 | 33, 36 | eqeltrrd 2112 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐶 ·𝑜
y) ∈
𝜔 ∧ 𝐶 ∈
𝜔) ∧ ∅ ∈ 𝐶) → (𝐶 ·𝑜 y) ∈ ((𝐶 ·𝑜
y) +𝑜 𝐶)) |
38 | | oveq2 5463 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (A = y →
(𝐶
·𝑜 A) = (𝐶 ·𝑜
y)) |
39 | 38 | eleq1d 2103 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (A = y →
((𝐶
·𝑜 A) ∈ ((𝐶 ·𝑜 y) +𝑜 𝐶) ↔ (𝐶 ·𝑜 y) ∈ ((𝐶 ·𝑜
y) +𝑜 𝐶))) |
40 | 37, 39 | syl5ibrcom 146 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐶 ·𝑜
y) ∈
𝜔 ∧ 𝐶 ∈
𝜔) ∧ ∅ ∈ 𝐶) → (A = y →
(𝐶
·𝑜 A) ∈ ((𝐶 ·𝑜 y) +𝑜 𝐶))) |
41 | 40 | adantrr 448 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐶 ·𝑜
y) ∈
𝜔 ∧ 𝐶 ∈
𝜔) ∧ (∅ ∈ 𝐶 ∧
(A ∈
y → (𝐶 ·𝑜 A) ∈ (𝐶 ·𝑜
y)))) → (A = y →
(𝐶
·𝑜 A) ∈ ((𝐶 ·𝑜 y) +𝑜 𝐶))) |
42 | 31, 41 | jaod 636 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐶 ·𝑜
y) ∈
𝜔 ∧ 𝐶 ∈
𝜔) ∧ (∅ ∈ 𝐶 ∧
(A ∈
y → (𝐶 ·𝑜 A) ∈ (𝐶 ·𝑜
y)))) → ((A ∈ y ∨ A = y) →
(𝐶
·𝑜 A) ∈ ((𝐶 ·𝑜 y) +𝑜 𝐶))) |
43 | 26, 42 | sylan 267 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐶 ∈ 𝜔 ∧
y ∈
𝜔) ∧ (∅ ∈ 𝐶 ∧
(A ∈
y → (𝐶 ·𝑜 A) ∈ (𝐶 ·𝑜
y)))) → ((A ∈ y ∨ A = y) →
(𝐶
·𝑜 A) ∈ ((𝐶 ·𝑜 y) +𝑜 𝐶))) |
44 | 23, 43 | syl5 28 |
. . . . . . . . . . . . . . 15
⊢ (((𝐶 ∈ 𝜔 ∧
y ∈
𝜔) ∧ (∅ ∈ 𝐶 ∧
(A ∈
y → (𝐶 ·𝑜 A) ∈ (𝐶 ·𝑜
y)))) → (A ∈ suc y → (𝐶 ·𝑜 A) ∈ ((𝐶 ·𝑜
y) +𝑜 𝐶))) |
45 | | nnmsuc 5995 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐶 ∈ 𝜔 ∧
y ∈
𝜔) → (𝐶
·𝑜 suc y) =
((𝐶
·𝑜 y)
+𝑜 𝐶)) |
46 | 45 | eleq2d 2104 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐶 ∈ 𝜔 ∧
y ∈
𝜔) → ((𝐶
·𝑜 A) ∈ (𝐶 ·𝑜 suc y) ↔ (𝐶 ·𝑜 A) ∈ ((𝐶 ·𝑜
y) +𝑜 𝐶))) |
47 | 46 | adantr 261 |
. . . . . . . . . . . . . . 15
⊢ (((𝐶 ∈ 𝜔 ∧
y ∈
𝜔) ∧ (∅ ∈ 𝐶 ∧
(A ∈
y → (𝐶 ·𝑜 A) ∈ (𝐶 ·𝑜
y)))) → ((𝐶 ·𝑜 A) ∈ (𝐶 ·𝑜
suc y) ↔ (𝐶 ·𝑜 A) ∈ ((𝐶 ·𝑜
y) +𝑜 𝐶))) |
48 | 44, 47 | sylibrd 158 |
. . . . . . . . . . . . . 14
⊢ (((𝐶 ∈ 𝜔 ∧
y ∈
𝜔) ∧ (∅ ∈ 𝐶 ∧
(A ∈
y → (𝐶 ·𝑜 A) ∈ (𝐶 ·𝑜
y)))) → (A ∈ suc y → (𝐶 ·𝑜 A) ∈ (𝐶 ·𝑜
suc y))) |
49 | 48 | exp43 354 |
. . . . . . . . . . . . 13
⊢ (𝐶 ∈ 𝜔 → (y ∈ 𝜔
→ (∅ ∈ 𝐶 → ((A ∈ y → (𝐶 ·𝑜 A) ∈ (𝐶 ·𝑜
y)) → (A ∈ suc y → (𝐶 ·𝑜 A) ∈ (𝐶 ·𝑜
suc y)))))) |
50 | 49 | com12 27 |
. . . . . . . . . . . 12
⊢ (y ∈ 𝜔
→ (𝐶 ∈ 𝜔 → (∅ ∈ 𝐶 → ((A ∈ y → (𝐶 ·𝑜 A) ∈ (𝐶 ·𝑜
y)) → (A ∈ suc y → (𝐶 ·𝑜 A) ∈ (𝐶 ·𝑜
suc y)))))) |
51 | 50 | adantld 263 |
. . . . . . . . . . 11
⊢ (y ∈ 𝜔
→ ((A ∈ 𝜔 ∧
𝐶 ∈ 𝜔) → (∅ ∈ 𝐶 → ((A ∈ y → (𝐶 ·𝑜 A) ∈ (𝐶 ·𝑜
y)) → (A ∈ suc y → (𝐶 ·𝑜 A) ∈ (𝐶 ·𝑜
suc y)))))) |
52 | 51 | impd 242 |
. . . . . . . . . 10
⊢ (y ∈ 𝜔
→ (((A ∈ 𝜔 ∧
𝐶 ∈ 𝜔) ∧
∅ ∈ 𝐶) → ((A ∈ y → (𝐶 ·𝑜 A) ∈ (𝐶 ·𝑜
y)) → (A ∈ suc y → (𝐶 ·𝑜 A) ∈ (𝐶 ·𝑜
suc y))))) |
53 | 11, 15, 19, 22, 52 | finds2 4267 |
. . . . . . . . 9
⊢ (x ∈ 𝜔
→ (((A ∈ 𝜔 ∧
𝐶 ∈ 𝜔) ∧
∅ ∈ 𝐶) → (A ∈ x → (𝐶 ·𝑜 A) ∈ (𝐶 ·𝑜
x)))) |
54 | 7, 53 | vtoclga 2613 |
. . . . . . . 8
⊢ (B ∈ 𝜔
→ (((A ∈ 𝜔 ∧
𝐶 ∈ 𝜔) ∧
∅ ∈ 𝐶) → (A ∈ B → (𝐶 ·𝑜 A) ∈ (𝐶 ·𝑜
B)))) |
55 | 54 | com23 72 |
. . . . . . 7
⊢ (B ∈ 𝜔
→ (A ∈ B →
(((A ∈
𝜔 ∧ 𝐶 ∈
𝜔) ∧ ∅ ∈ 𝐶) → (𝐶 ·𝑜 A) ∈ (𝐶 ·𝑜
B)))) |
56 | 55 | exp4a 348 |
. . . . . 6
⊢ (B ∈ 𝜔
→ (A ∈ B →
((A ∈
𝜔 ∧ 𝐶 ∈
𝜔) → (∅ ∈ 𝐶 → (𝐶 ·𝑜 A) ∈ (𝐶 ·𝑜
B))))) |
57 | 56 | exp4a 348 |
. . . . 5
⊢ (B ∈ 𝜔
→ (A ∈ B →
(A ∈
𝜔 → (𝐶 ∈ 𝜔 → (∅ ∈ 𝐶 → (𝐶 ·𝑜 A) ∈ (𝐶 ·𝑜
B)))))) |
58 | 2, 57 | mpdd 36 |
. . . 4
⊢ (B ∈ 𝜔
→ (A ∈ B →
(𝐶 ∈ 𝜔 → (∅ ∈ 𝐶 → (𝐶 ·𝑜 A) ∈ (𝐶 ·𝑜
B))))) |
59 | 58 | com34 77 |
. . 3
⊢ (B ∈ 𝜔
→ (A ∈ B →
(∅ ∈ 𝐶 → (𝐶 ∈
𝜔 → (𝐶
·𝑜 A) ∈ (𝐶 ·𝑜 B))))) |
60 | 59 | com24 81 |
. 2
⊢ (B ∈ 𝜔
→ (𝐶 ∈ 𝜔 → (∅ ∈ 𝐶 → (A ∈ B → (𝐶 ·𝑜 A) ∈ (𝐶 ·𝑜
B))))) |
61 | 60 | imp31 243 |
1
⊢
(((B ∈ 𝜔 ∧
𝐶 ∈ 𝜔) ∧
∅ ∈ 𝐶) → (A ∈ B → (𝐶 ·𝑜 A) ∈ (𝐶 ·𝑜
B))) |