Step | Hyp | Ref
| Expression |
1 | | elnn 7714 |
. . . . . 6
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ ω) → 𝐴 ∈ ω) |
2 | 1 | expcom 414 |
. . . . 5
⊢ (𝐵 ∈ ω → (𝐴 ∈ 𝐵 → 𝐴 ∈ ω)) |
3 | | eleq2 2827 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝐵 → (𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝐵)) |
4 | | oveq2 7276 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝐵 → (𝐶 ·o 𝑥) = (𝐶 ·o 𝐵)) |
5 | 4 | eleq2d 2824 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝐵 → ((𝐶 ·o 𝐴) ∈ (𝐶 ·o 𝑥) ↔ (𝐶 ·o 𝐴) ∈ (𝐶 ·o 𝐵))) |
6 | 3, 5 | imbi12d 345 |
. . . . . . . . . 10
⊢ (𝑥 = 𝐵 → ((𝐴 ∈ 𝑥 → (𝐶 ·o 𝐴) ∈ (𝐶 ·o 𝑥)) ↔ (𝐴 ∈ 𝐵 → (𝐶 ·o 𝐴) ∈ (𝐶 ·o 𝐵)))) |
7 | 6 | imbi2d 341 |
. . . . . . . . 9
⊢ (𝑥 = 𝐵 → ((((𝐴 ∈ ω ∧ 𝐶 ∈ ω) ∧ ∅ ∈ 𝐶) → (𝐴 ∈ 𝑥 → (𝐶 ·o 𝐴) ∈ (𝐶 ·o 𝑥))) ↔ (((𝐴 ∈ ω ∧ 𝐶 ∈ ω) ∧ ∅ ∈ 𝐶) → (𝐴 ∈ 𝐵 → (𝐶 ·o 𝐴) ∈ (𝐶 ·o 𝐵))))) |
8 | | eleq2 2827 |
. . . . . . . . . . 11
⊢ (𝑥 = ∅ → (𝐴 ∈ 𝑥 ↔ 𝐴 ∈ ∅)) |
9 | | oveq2 7276 |
. . . . . . . . . . . 12
⊢ (𝑥 = ∅ → (𝐶 ·o 𝑥) = (𝐶 ·o
∅)) |
10 | 9 | eleq2d 2824 |
. . . . . . . . . . 11
⊢ (𝑥 = ∅ → ((𝐶 ·o 𝐴) ∈ (𝐶 ·o 𝑥) ↔ (𝐶 ·o 𝐴) ∈ (𝐶 ·o
∅))) |
11 | 8, 10 | imbi12d 345 |
. . . . . . . . . 10
⊢ (𝑥 = ∅ → ((𝐴 ∈ 𝑥 → (𝐶 ·o 𝐴) ∈ (𝐶 ·o 𝑥)) ↔ (𝐴 ∈ ∅ → (𝐶 ·o 𝐴) ∈ (𝐶 ·o
∅)))) |
12 | | eleq2 2827 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → (𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝑦)) |
13 | | oveq2 7276 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 → (𝐶 ·o 𝑥) = (𝐶 ·o 𝑦)) |
14 | 13 | eleq2d 2824 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → ((𝐶 ·o 𝐴) ∈ (𝐶 ·o 𝑥) ↔ (𝐶 ·o 𝐴) ∈ (𝐶 ·o 𝑦))) |
15 | 12, 14 | imbi12d 345 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → ((𝐴 ∈ 𝑥 → (𝐶 ·o 𝐴) ∈ (𝐶 ·o 𝑥)) ↔ (𝐴 ∈ 𝑦 → (𝐶 ·o 𝐴) ∈ (𝐶 ·o 𝑦)))) |
16 | | eleq2 2827 |
. . . . . . . . . . 11
⊢ (𝑥 = suc 𝑦 → (𝐴 ∈ 𝑥 ↔ 𝐴 ∈ suc 𝑦)) |
17 | | oveq2 7276 |
. . . . . . . . . . . 12
⊢ (𝑥 = suc 𝑦 → (𝐶 ·o 𝑥) = (𝐶 ·o suc 𝑦)) |
18 | 17 | eleq2d 2824 |
. . . . . . . . . . 11
⊢ (𝑥 = suc 𝑦 → ((𝐶 ·o 𝐴) ∈ (𝐶 ·o 𝑥) ↔ (𝐶 ·o 𝐴) ∈ (𝐶 ·o suc 𝑦))) |
19 | 16, 18 | imbi12d 345 |
. . . . . . . . . 10
⊢ (𝑥 = suc 𝑦 → ((𝐴 ∈ 𝑥 → (𝐶 ·o 𝐴) ∈ (𝐶 ·o 𝑥)) ↔ (𝐴 ∈ suc 𝑦 → (𝐶 ·o 𝐴) ∈ (𝐶 ·o suc 𝑦)))) |
20 | | noel 4265 |
. . . . . . . . . . . 12
⊢ ¬
𝐴 ∈
∅ |
21 | 20 | pm2.21i 119 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ∅ → (𝐶 ·o 𝐴) ∈ (𝐶 ·o
∅)) |
22 | 21 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ω ∧ 𝐶 ∈ ω) ∧ ∅
∈ 𝐶) → (𝐴 ∈ ∅ → (𝐶 ·o 𝐴) ∈ (𝐶 ·o
∅))) |
23 | | elsuci 6326 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ suc 𝑦 → (𝐴 ∈ 𝑦 ∨ 𝐴 = 𝑦)) |
24 | | nnmcl 8431 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐶 ∈ ω ∧ 𝑦 ∈ ω) → (𝐶 ·o 𝑦) ∈
ω) |
25 | | simpl 483 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐶 ∈ ω ∧ 𝑦 ∈ ω) → 𝐶 ∈
ω) |
26 | 24, 25 | jca 512 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐶 ∈ ω ∧ 𝑦 ∈ ω) → ((𝐶 ·o 𝑦) ∈ ω ∧ 𝐶 ∈
ω)) |
27 | | nnaword1 8448 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐶 ·o 𝑦) ∈ ω ∧ 𝐶 ∈ ω) → (𝐶 ·o 𝑦) ⊆ ((𝐶 ·o 𝑦) +o 𝐶)) |
28 | 27 | sseld 3920 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐶 ·o 𝑦) ∈ ω ∧ 𝐶 ∈ ω) → ((𝐶 ·o 𝐴) ∈ (𝐶 ·o 𝑦) → (𝐶 ·o 𝐴) ∈ ((𝐶 ·o 𝑦) +o 𝐶))) |
29 | 28 | imim2d 57 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐶 ·o 𝑦) ∈ ω ∧ 𝐶 ∈ ω) → ((𝐴 ∈ 𝑦 → (𝐶 ·o 𝐴) ∈ (𝐶 ·o 𝑦)) → (𝐴 ∈ 𝑦 → (𝐶 ·o 𝐴) ∈ ((𝐶 ·o 𝑦) +o 𝐶)))) |
30 | 29 | imp 407 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐶 ·o 𝑦) ∈ ω ∧ 𝐶 ∈ ω) ∧ (𝐴 ∈ 𝑦 → (𝐶 ·o 𝐴) ∈ (𝐶 ·o 𝑦))) → (𝐴 ∈ 𝑦 → (𝐶 ·o 𝐴) ∈ ((𝐶 ·o 𝑦) +o 𝐶))) |
31 | 30 | adantrl 713 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐶 ·o 𝑦) ∈ ω ∧ 𝐶 ∈ ω) ∧ (∅
∈ 𝐶 ∧ (𝐴 ∈ 𝑦 → (𝐶 ·o 𝐴) ∈ (𝐶 ·o 𝑦)))) → (𝐴 ∈ 𝑦 → (𝐶 ·o 𝐴) ∈ ((𝐶 ·o 𝑦) +o 𝐶))) |
32 | | nna0 8423 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐶 ·o 𝑦) ∈ ω → ((𝐶 ·o 𝑦) +o ∅) =
(𝐶 ·o
𝑦)) |
33 | 32 | ad2antrr 723 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐶 ·o 𝑦) ∈ ω ∧ 𝐶 ∈ ω) ∧ ∅
∈ 𝐶) → ((𝐶 ·o 𝑦) +o ∅) =
(𝐶 ·o
𝑦)) |
34 | | nnaordi 8437 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐶 ∈ ω ∧ (𝐶 ·o 𝑦) ∈ ω) →
(∅ ∈ 𝐶 →
((𝐶 ·o
𝑦) +o ∅)
∈ ((𝐶
·o 𝑦)
+o 𝐶))) |
35 | 34 | ancoms 459 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐶 ·o 𝑦) ∈ ω ∧ 𝐶 ∈ ω) → (∅
∈ 𝐶 → ((𝐶 ·o 𝑦) +o ∅) ∈
((𝐶 ·o
𝑦) +o 𝐶))) |
36 | 35 | imp 407 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐶 ·o 𝑦) ∈ ω ∧ 𝐶 ∈ ω) ∧ ∅
∈ 𝐶) → ((𝐶 ·o 𝑦) +o ∅) ∈
((𝐶 ·o
𝑦) +o 𝐶)) |
37 | 33, 36 | eqeltrrd 2840 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐶 ·o 𝑦) ∈ ω ∧ 𝐶 ∈ ω) ∧ ∅
∈ 𝐶) → (𝐶 ·o 𝑦) ∈ ((𝐶 ·o 𝑦) +o 𝐶)) |
38 | | oveq2 7276 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐴 = 𝑦 → (𝐶 ·o 𝐴) = (𝐶 ·o 𝑦)) |
39 | 38 | eleq1d 2823 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐴 = 𝑦 → ((𝐶 ·o 𝐴) ∈ ((𝐶 ·o 𝑦) +o 𝐶) ↔ (𝐶 ·o 𝑦) ∈ ((𝐶 ·o 𝑦) +o 𝐶))) |
40 | 37, 39 | syl5ibrcom 246 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐶 ·o 𝑦) ∈ ω ∧ 𝐶 ∈ ω) ∧ ∅
∈ 𝐶) → (𝐴 = 𝑦 → (𝐶 ·o 𝐴) ∈ ((𝐶 ·o 𝑦) +o 𝐶))) |
41 | 40 | adantrr 714 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐶 ·o 𝑦) ∈ ω ∧ 𝐶 ∈ ω) ∧ (∅
∈ 𝐶 ∧ (𝐴 ∈ 𝑦 → (𝐶 ·o 𝐴) ∈ (𝐶 ·o 𝑦)))) → (𝐴 = 𝑦 → (𝐶 ·o 𝐴) ∈ ((𝐶 ·o 𝑦) +o 𝐶))) |
42 | 31, 41 | jaod 856 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐶 ·o 𝑦) ∈ ω ∧ 𝐶 ∈ ω) ∧ (∅
∈ 𝐶 ∧ (𝐴 ∈ 𝑦 → (𝐶 ·o 𝐴) ∈ (𝐶 ·o 𝑦)))) → ((𝐴 ∈ 𝑦 ∨ 𝐴 = 𝑦) → (𝐶 ·o 𝐴) ∈ ((𝐶 ·o 𝑦) +o 𝐶))) |
43 | 26, 42 | sylan 580 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐶 ∈ ω ∧ 𝑦 ∈ ω) ∧ (∅
∈ 𝐶 ∧ (𝐴 ∈ 𝑦 → (𝐶 ·o 𝐴) ∈ (𝐶 ·o 𝑦)))) → ((𝐴 ∈ 𝑦 ∨ 𝐴 = 𝑦) → (𝐶 ·o 𝐴) ∈ ((𝐶 ·o 𝑦) +o 𝐶))) |
44 | 23, 43 | syl5 34 |
. . . . . . . . . . . . . . 15
⊢ (((𝐶 ∈ ω ∧ 𝑦 ∈ ω) ∧ (∅
∈ 𝐶 ∧ (𝐴 ∈ 𝑦 → (𝐶 ·o 𝐴) ∈ (𝐶 ·o 𝑦)))) → (𝐴 ∈ suc 𝑦 → (𝐶 ·o 𝐴) ∈ ((𝐶 ·o 𝑦) +o 𝐶))) |
45 | | nnmsuc 8426 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐶 ∈ ω ∧ 𝑦 ∈ ω) → (𝐶 ·o suc 𝑦) = ((𝐶 ·o 𝑦) +o 𝐶)) |
46 | 45 | eleq2d 2824 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐶 ∈ ω ∧ 𝑦 ∈ ω) → ((𝐶 ·o 𝐴) ∈ (𝐶 ·o suc 𝑦) ↔ (𝐶 ·o 𝐴) ∈ ((𝐶 ·o 𝑦) +o 𝐶))) |
47 | 46 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ (((𝐶 ∈ ω ∧ 𝑦 ∈ ω) ∧ (∅
∈ 𝐶 ∧ (𝐴 ∈ 𝑦 → (𝐶 ·o 𝐴) ∈ (𝐶 ·o 𝑦)))) → ((𝐶 ·o 𝐴) ∈ (𝐶 ·o suc 𝑦) ↔ (𝐶 ·o 𝐴) ∈ ((𝐶 ·o 𝑦) +o 𝐶))) |
48 | 44, 47 | sylibrd 258 |
. . . . . . . . . . . . . 14
⊢ (((𝐶 ∈ ω ∧ 𝑦 ∈ ω) ∧ (∅
∈ 𝐶 ∧ (𝐴 ∈ 𝑦 → (𝐶 ·o 𝐴) ∈ (𝐶 ·o 𝑦)))) → (𝐴 ∈ suc 𝑦 → (𝐶 ·o 𝐴) ∈ (𝐶 ·o suc 𝑦))) |
49 | 48 | exp43 437 |
. . . . . . . . . . . . 13
⊢ (𝐶 ∈ ω → (𝑦 ∈ ω → (∅
∈ 𝐶 → ((𝐴 ∈ 𝑦 → (𝐶 ·o 𝐴) ∈ (𝐶 ·o 𝑦)) → (𝐴 ∈ suc 𝑦 → (𝐶 ·o 𝐴) ∈ (𝐶 ·o suc 𝑦)))))) |
50 | 49 | com12 32 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ω → (𝐶 ∈ ω → (∅
∈ 𝐶 → ((𝐴 ∈ 𝑦 → (𝐶 ·o 𝐴) ∈ (𝐶 ·o 𝑦)) → (𝐴 ∈ suc 𝑦 → (𝐶 ·o 𝐴) ∈ (𝐶 ·o suc 𝑦)))))) |
51 | 50 | adantld 491 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ω → ((𝐴 ∈ ω ∧ 𝐶 ∈ ω) → (∅
∈ 𝐶 → ((𝐴 ∈ 𝑦 → (𝐶 ·o 𝐴) ∈ (𝐶 ·o 𝑦)) → (𝐴 ∈ suc 𝑦 → (𝐶 ·o 𝐴) ∈ (𝐶 ·o suc 𝑦)))))) |
52 | 51 | impd 411 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ω → (((𝐴 ∈ ω ∧ 𝐶 ∈ ω) ∧ ∅
∈ 𝐶) → ((𝐴 ∈ 𝑦 → (𝐶 ·o 𝐴) ∈ (𝐶 ·o 𝑦)) → (𝐴 ∈ suc 𝑦 → (𝐶 ·o 𝐴) ∈ (𝐶 ·o suc 𝑦))))) |
53 | 11, 15, 19, 22, 52 | finds2 7738 |
. . . . . . . . 9
⊢ (𝑥 ∈ ω → (((𝐴 ∈ ω ∧ 𝐶 ∈ ω) ∧ ∅
∈ 𝐶) → (𝐴 ∈ 𝑥 → (𝐶 ·o 𝐴) ∈ (𝐶 ·o 𝑥)))) |
54 | 7, 53 | vtoclga 3511 |
. . . . . . . 8
⊢ (𝐵 ∈ ω → (((𝐴 ∈ ω ∧ 𝐶 ∈ ω) ∧ ∅
∈ 𝐶) → (𝐴 ∈ 𝐵 → (𝐶 ·o 𝐴) ∈ (𝐶 ·o 𝐵)))) |
55 | 54 | com23 86 |
. . . . . . 7
⊢ (𝐵 ∈ ω → (𝐴 ∈ 𝐵 → (((𝐴 ∈ ω ∧ 𝐶 ∈ ω) ∧ ∅ ∈ 𝐶) → (𝐶 ·o 𝐴) ∈ (𝐶 ·o 𝐵)))) |
56 | 55 | exp4a 432 |
. . . . . 6
⊢ (𝐵 ∈ ω → (𝐴 ∈ 𝐵 → ((𝐴 ∈ ω ∧ 𝐶 ∈ ω) → (∅ ∈
𝐶 → (𝐶 ·o 𝐴) ∈ (𝐶 ·o 𝐵))))) |
57 | 56 | exp4a 432 |
. . . . 5
⊢ (𝐵 ∈ ω → (𝐴 ∈ 𝐵 → (𝐴 ∈ ω → (𝐶 ∈ ω → (∅ ∈ 𝐶 → (𝐶 ·o 𝐴) ∈ (𝐶 ·o 𝐵)))))) |
58 | 2, 57 | mpdd 43 |
. . . 4
⊢ (𝐵 ∈ ω → (𝐴 ∈ 𝐵 → (𝐶 ∈ ω → (∅ ∈ 𝐶 → (𝐶 ·o 𝐴) ∈ (𝐶 ·o 𝐵))))) |
59 | 58 | com34 91 |
. . 3
⊢ (𝐵 ∈ ω → (𝐴 ∈ 𝐵 → (∅ ∈ 𝐶 → (𝐶 ∈ ω → (𝐶 ·o 𝐴) ∈ (𝐶 ·o 𝐵))))) |
60 | 59 | com24 95 |
. 2
⊢ (𝐵 ∈ ω → (𝐶 ∈ ω → (∅
∈ 𝐶 → (𝐴 ∈ 𝐵 → (𝐶 ·o 𝐴) ∈ (𝐶 ·o 𝐵))))) |
61 | 60 | imp31 418 |
1
⊢ (((𝐵 ∈ ω ∧ 𝐶 ∈ ω) ∧ ∅
∈ 𝐶) → (𝐴 ∈ 𝐵 → (𝐶 ·o 𝐴) ∈ (𝐶 ·o 𝐵))) |