Step | Hyp | Ref
| Expression |
1 | | onelon 6290 |
. . . . . 6
⊢ ((𝐵 ∈ On ∧ 𝐴 ∈ 𝐵) → 𝐴 ∈ On) |
2 | 1 | ex 413 |
. . . . 5
⊢ (𝐵 ∈ On → (𝐴 ∈ 𝐵 → 𝐴 ∈ On)) |
3 | | eleq2 2829 |
. . . . . . . . . 10
⊢ (𝑥 = ∅ → (𝐴 ∈ 𝑥 ↔ 𝐴 ∈ ∅)) |
4 | | oveq2 7279 |
. . . . . . . . . . 11
⊢ (𝑥 = ∅ → (𝐶 ·o 𝑥) = (𝐶 ·o
∅)) |
5 | 4 | eleq2d 2826 |
. . . . . . . . . 10
⊢ (𝑥 = ∅ → ((𝐶 ·o 𝐴) ∈ (𝐶 ·o 𝑥) ↔ (𝐶 ·o 𝐴) ∈ (𝐶 ·o
∅))) |
6 | 3, 5 | imbi12d 345 |
. . . . . . . . 9
⊢ (𝑥 = ∅ → ((𝐴 ∈ 𝑥 → (𝐶 ·o 𝐴) ∈ (𝐶 ·o 𝑥)) ↔ (𝐴 ∈ ∅ → (𝐶 ·o 𝐴) ∈ (𝐶 ·o
∅)))) |
7 | | eleq2 2829 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → (𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝑦)) |
8 | | oveq2 7279 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → (𝐶 ·o 𝑥) = (𝐶 ·o 𝑦)) |
9 | 8 | eleq2d 2826 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → ((𝐶 ·o 𝐴) ∈ (𝐶 ·o 𝑥) ↔ (𝐶 ·o 𝐴) ∈ (𝐶 ·o 𝑦))) |
10 | 7, 9 | imbi12d 345 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → ((𝐴 ∈ 𝑥 → (𝐶 ·o 𝐴) ∈ (𝐶 ·o 𝑥)) ↔ (𝐴 ∈ 𝑦 → (𝐶 ·o 𝐴) ∈ (𝐶 ·o 𝑦)))) |
11 | | eleq2 2829 |
. . . . . . . . . 10
⊢ (𝑥 = suc 𝑦 → (𝐴 ∈ 𝑥 ↔ 𝐴 ∈ suc 𝑦)) |
12 | | oveq2 7279 |
. . . . . . . . . . 11
⊢ (𝑥 = suc 𝑦 → (𝐶 ·o 𝑥) = (𝐶 ·o suc 𝑦)) |
13 | 12 | eleq2d 2826 |
. . . . . . . . . 10
⊢ (𝑥 = suc 𝑦 → ((𝐶 ·o 𝐴) ∈ (𝐶 ·o 𝑥) ↔ (𝐶 ·o 𝐴) ∈ (𝐶 ·o suc 𝑦))) |
14 | 11, 13 | imbi12d 345 |
. . . . . . . . 9
⊢ (𝑥 = suc 𝑦 → ((𝐴 ∈ 𝑥 → (𝐶 ·o 𝐴) ∈ (𝐶 ·o 𝑥)) ↔ (𝐴 ∈ suc 𝑦 → (𝐶 ·o 𝐴) ∈ (𝐶 ·o suc 𝑦)))) |
15 | | eleq2 2829 |
. . . . . . . . . 10
⊢ (𝑥 = 𝐵 → (𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝐵)) |
16 | | oveq2 7279 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝐵 → (𝐶 ·o 𝑥) = (𝐶 ·o 𝐵)) |
17 | 16 | eleq2d 2826 |
. . . . . . . . . 10
⊢ (𝑥 = 𝐵 → ((𝐶 ·o 𝐴) ∈ (𝐶 ·o 𝑥) ↔ (𝐶 ·o 𝐴) ∈ (𝐶 ·o 𝐵))) |
18 | 15, 17 | imbi12d 345 |
. . . . . . . . 9
⊢ (𝑥 = 𝐵 → ((𝐴 ∈ 𝑥 → (𝐶 ·o 𝐴) ∈ (𝐶 ·o 𝑥)) ↔ (𝐴 ∈ 𝐵 → (𝐶 ·o 𝐴) ∈ (𝐶 ·o 𝐵)))) |
19 | | noel 4270 |
. . . . . . . . . . 11
⊢ ¬
𝐴 ∈
∅ |
20 | 19 | pm2.21i 119 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ∅ → (𝐶 ·o 𝐴) ∈ (𝐶 ·o
∅)) |
21 | 20 | a1i 11 |
. . . . . . . . 9
⊢ (((𝐴 ∈ On ∧ 𝐶 ∈ On) ∧ ∅ ∈
𝐶) → (𝐴 ∈ ∅ → (𝐶 ·o 𝐴) ∈ (𝐶 ·o
∅))) |
22 | | elsuci 6331 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ suc 𝑦 → (𝐴 ∈ 𝑦 ∨ 𝐴 = 𝑦)) |
23 | | omcl 8351 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐶 ∈ On ∧ 𝑦 ∈ On) → (𝐶 ·o 𝑦) ∈ On) |
24 | | simpl 483 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐶 ∈ On ∧ 𝑦 ∈ On) → 𝐶 ∈ On) |
25 | 23, 24 | jca 512 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐶 ∈ On ∧ 𝑦 ∈ On) → ((𝐶 ·o 𝑦) ∈ On ∧ 𝐶 ∈ On)) |
26 | | oaword1 8368 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐶 ·o 𝑦) ∈ On ∧ 𝐶 ∈ On) → (𝐶 ·o 𝑦) ⊆ ((𝐶 ·o 𝑦) +o 𝐶)) |
27 | 26 | sseld 3925 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐶 ·o 𝑦) ∈ On ∧ 𝐶 ∈ On) → ((𝐶 ·o 𝐴) ∈ (𝐶 ·o 𝑦) → (𝐶 ·o 𝐴) ∈ ((𝐶 ·o 𝑦) +o 𝐶))) |
28 | 27 | imim2d 57 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐶 ·o 𝑦) ∈ On ∧ 𝐶 ∈ On) → ((𝐴 ∈ 𝑦 → (𝐶 ·o 𝐴) ∈ (𝐶 ·o 𝑦)) → (𝐴 ∈ 𝑦 → (𝐶 ·o 𝐴) ∈ ((𝐶 ·o 𝑦) +o 𝐶)))) |
29 | 28 | imp 407 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐶 ·o 𝑦) ∈ On ∧ 𝐶 ∈ On) ∧ (𝐴 ∈ 𝑦 → (𝐶 ·o 𝐴) ∈ (𝐶 ·o 𝑦))) → (𝐴 ∈ 𝑦 → (𝐶 ·o 𝐴) ∈ ((𝐶 ·o 𝑦) +o 𝐶))) |
30 | 29 | adantrl 713 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐶 ·o 𝑦) ∈ On ∧ 𝐶 ∈ On) ∧ (∅
∈ 𝐶 ∧ (𝐴 ∈ 𝑦 → (𝐶 ·o 𝐴) ∈ (𝐶 ·o 𝑦)))) → (𝐴 ∈ 𝑦 → (𝐶 ·o 𝐴) ∈ ((𝐶 ·o 𝑦) +o 𝐶))) |
31 | | oaord1 8367 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐶 ·o 𝑦) ∈ On ∧ 𝐶 ∈ On) → (∅
∈ 𝐶 ↔ (𝐶 ·o 𝑦) ∈ ((𝐶 ·o 𝑦) +o 𝐶))) |
32 | 31 | biimpa 477 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐶 ·o 𝑦) ∈ On ∧ 𝐶 ∈ On) ∧ ∅ ∈
𝐶) → (𝐶 ·o 𝑦) ∈ ((𝐶 ·o 𝑦) +o 𝐶)) |
33 | | oveq2 7279 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐴 = 𝑦 → (𝐶 ·o 𝐴) = (𝐶 ·o 𝑦)) |
34 | 33 | eleq1d 2825 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐴 = 𝑦 → ((𝐶 ·o 𝐴) ∈ ((𝐶 ·o 𝑦) +o 𝐶) ↔ (𝐶 ·o 𝑦) ∈ ((𝐶 ·o 𝑦) +o 𝐶))) |
35 | 32, 34 | syl5ibrcom 246 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐶 ·o 𝑦) ∈ On ∧ 𝐶 ∈ On) ∧ ∅ ∈
𝐶) → (𝐴 = 𝑦 → (𝐶 ·o 𝐴) ∈ ((𝐶 ·o 𝑦) +o 𝐶))) |
36 | 35 | adantrr 714 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐶 ·o 𝑦) ∈ On ∧ 𝐶 ∈ On) ∧ (∅
∈ 𝐶 ∧ (𝐴 ∈ 𝑦 → (𝐶 ·o 𝐴) ∈ (𝐶 ·o 𝑦)))) → (𝐴 = 𝑦 → (𝐶 ·o 𝐴) ∈ ((𝐶 ·o 𝑦) +o 𝐶))) |
37 | 30, 36 | jaod 856 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐶 ·o 𝑦) ∈ On ∧ 𝐶 ∈ On) ∧ (∅
∈ 𝐶 ∧ (𝐴 ∈ 𝑦 → (𝐶 ·o 𝐴) ∈ (𝐶 ·o 𝑦)))) → ((𝐴 ∈ 𝑦 ∨ 𝐴 = 𝑦) → (𝐶 ·o 𝐴) ∈ ((𝐶 ·o 𝑦) +o 𝐶))) |
38 | 25, 37 | sylan 580 |
. . . . . . . . . . . . . . 15
⊢ (((𝐶 ∈ On ∧ 𝑦 ∈ On) ∧ (∅
∈ 𝐶 ∧ (𝐴 ∈ 𝑦 → (𝐶 ·o 𝐴) ∈ (𝐶 ·o 𝑦)))) → ((𝐴 ∈ 𝑦 ∨ 𝐴 = 𝑦) → (𝐶 ·o 𝐴) ∈ ((𝐶 ·o 𝑦) +o 𝐶))) |
39 | 22, 38 | syl5 34 |
. . . . . . . . . . . . . 14
⊢ (((𝐶 ∈ On ∧ 𝑦 ∈ On) ∧ (∅
∈ 𝐶 ∧ (𝐴 ∈ 𝑦 → (𝐶 ·o 𝐴) ∈ (𝐶 ·o 𝑦)))) → (𝐴 ∈ suc 𝑦 → (𝐶 ·o 𝐴) ∈ ((𝐶 ·o 𝑦) +o 𝐶))) |
40 | | omsuc 8341 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐶 ∈ On ∧ 𝑦 ∈ On) → (𝐶 ·o suc 𝑦) = ((𝐶 ·o 𝑦) +o 𝐶)) |
41 | 40 | eleq2d 2826 |
. . . . . . . . . . . . . . 15
⊢ ((𝐶 ∈ On ∧ 𝑦 ∈ On) → ((𝐶 ·o 𝐴) ∈ (𝐶 ·o suc 𝑦) ↔ (𝐶 ·o 𝐴) ∈ ((𝐶 ·o 𝑦) +o 𝐶))) |
42 | 41 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ (((𝐶 ∈ On ∧ 𝑦 ∈ On) ∧ (∅
∈ 𝐶 ∧ (𝐴 ∈ 𝑦 → (𝐶 ·o 𝐴) ∈ (𝐶 ·o 𝑦)))) → ((𝐶 ·o 𝐴) ∈ (𝐶 ·o suc 𝑦) ↔ (𝐶 ·o 𝐴) ∈ ((𝐶 ·o 𝑦) +o 𝐶))) |
43 | 39, 42 | sylibrd 258 |
. . . . . . . . . . . . 13
⊢ (((𝐶 ∈ On ∧ 𝑦 ∈ On) ∧ (∅
∈ 𝐶 ∧ (𝐴 ∈ 𝑦 → (𝐶 ·o 𝐴) ∈ (𝐶 ·o 𝑦)))) → (𝐴 ∈ suc 𝑦 → (𝐶 ·o 𝐴) ∈ (𝐶 ·o suc 𝑦))) |
44 | 43 | exp43 437 |
. . . . . . . . . . . 12
⊢ (𝐶 ∈ On → (𝑦 ∈ On → (∅
∈ 𝐶 → ((𝐴 ∈ 𝑦 → (𝐶 ·o 𝐴) ∈ (𝐶 ·o 𝑦)) → (𝐴 ∈ suc 𝑦 → (𝐶 ·o 𝐴) ∈ (𝐶 ·o suc 𝑦)))))) |
45 | 44 | com12 32 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ On → (𝐶 ∈ On → (∅
∈ 𝐶 → ((𝐴 ∈ 𝑦 → (𝐶 ·o 𝐴) ∈ (𝐶 ·o 𝑦)) → (𝐴 ∈ suc 𝑦 → (𝐶 ·o 𝐴) ∈ (𝐶 ·o suc 𝑦)))))) |
46 | 45 | adantld 491 |
. . . . . . . . . 10
⊢ (𝑦 ∈ On → ((𝐴 ∈ On ∧ 𝐶 ∈ On) → (∅
∈ 𝐶 → ((𝐴 ∈ 𝑦 → (𝐶 ·o 𝐴) ∈ (𝐶 ·o 𝑦)) → (𝐴 ∈ suc 𝑦 → (𝐶 ·o 𝐴) ∈ (𝐶 ·o suc 𝑦)))))) |
47 | 46 | impd 411 |
. . . . . . . . 9
⊢ (𝑦 ∈ On → (((𝐴 ∈ On ∧ 𝐶 ∈ On) ∧ ∅ ∈
𝐶) → ((𝐴 ∈ 𝑦 → (𝐶 ·o 𝐴) ∈ (𝐶 ·o 𝑦)) → (𝐴 ∈ suc 𝑦 → (𝐶 ·o 𝐴) ∈ (𝐶 ·o suc 𝑦))))) |
48 | | id 22 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐶 ∈ On ∧ Lim 𝑥) → (𝐶 ∈ On ∧ Lim 𝑥)) |
49 | 48 | ad2ant2r 744 |
. . . . . . . . . . . . . . 15
⊢ (((𝐶 ∈ On ∧ 𝐴 ∈ On) ∧ (Lim 𝑥 ∧ ∅ ∈ 𝐶)) → (𝐶 ∈ On ∧ Lim 𝑥)) |
50 | | limsuc 7690 |
. . . . . . . . . . . . . . . . . . 19
⊢ (Lim
𝑥 → (𝐴 ∈ 𝑥 ↔ suc 𝐴 ∈ 𝑥)) |
51 | 50 | biimpa 477 |
. . . . . . . . . . . . . . . . . 18
⊢ ((Lim
𝑥 ∧ 𝐴 ∈ 𝑥) → suc 𝐴 ∈ 𝑥) |
52 | | oveq2 7279 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = suc 𝐴 → (𝐶 ·o 𝑦) = (𝐶 ·o suc 𝐴)) |
53 | 52 | ssiun2s 4983 |
. . . . . . . . . . . . . . . . . 18
⊢ (suc
𝐴 ∈ 𝑥 → (𝐶 ·o suc 𝐴) ⊆ ∪ 𝑦 ∈ 𝑥 (𝐶 ·o 𝑦)) |
54 | 51, 53 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((Lim
𝑥 ∧ 𝐴 ∈ 𝑥) → (𝐶 ·o suc 𝐴) ⊆ ∪ 𝑦 ∈ 𝑥 (𝐶 ·o 𝑦)) |
55 | 54 | adantll 711 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐶 ∈ On ∧ Lim 𝑥) ∧ 𝐴 ∈ 𝑥) → (𝐶 ·o suc 𝐴) ⊆ ∪ 𝑦 ∈ 𝑥 (𝐶 ·o 𝑦)) |
56 | | vex 3435 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑥 ∈ V |
57 | | omlim 8348 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐶 ∈ On ∧ (𝑥 ∈ V ∧ Lim 𝑥)) → (𝐶 ·o 𝑥) = ∪ 𝑦 ∈ 𝑥 (𝐶 ·o 𝑦)) |
58 | 56, 57 | mpanr1 700 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐶 ∈ On ∧ Lim 𝑥) → (𝐶 ·o 𝑥) = ∪ 𝑦 ∈ 𝑥 (𝐶 ·o 𝑦)) |
59 | 58 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐶 ∈ On ∧ Lim 𝑥) ∧ 𝐴 ∈ 𝑥) → (𝐶 ·o 𝑥) = ∪ 𝑦 ∈ 𝑥 (𝐶 ·o 𝑦)) |
60 | 55, 59 | sseqtrrd 3967 |
. . . . . . . . . . . . . . 15
⊢ (((𝐶 ∈ On ∧ Lim 𝑥) ∧ 𝐴 ∈ 𝑥) → (𝐶 ·o suc 𝐴) ⊆ (𝐶 ·o 𝑥)) |
61 | 49, 60 | sylan 580 |
. . . . . . . . . . . . . 14
⊢ ((((𝐶 ∈ On ∧ 𝐴 ∈ On) ∧ (Lim 𝑥 ∧ ∅ ∈ 𝐶)) ∧ 𝐴 ∈ 𝑥) → (𝐶 ·o suc 𝐴) ⊆ (𝐶 ·o 𝑥)) |
62 | | omcl 8351 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐶 ∈ On ∧ 𝐴 ∈ On) → (𝐶 ·o 𝐴) ∈ On) |
63 | | oaord1 8367 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐶 ·o 𝐴) ∈ On ∧ 𝐶 ∈ On) → (∅
∈ 𝐶 ↔ (𝐶 ·o 𝐴) ∈ ((𝐶 ·o 𝐴) +o 𝐶))) |
64 | 62, 63 | sylan 580 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐶 ∈ On ∧ 𝐴 ∈ On) ∧ 𝐶 ∈ On) → (∅
∈ 𝐶 ↔ (𝐶 ·o 𝐴) ∈ ((𝐶 ·o 𝐴) +o 𝐶))) |
65 | 64 | anabss1 663 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐶 ∈ On ∧ 𝐴 ∈ On) → (∅
∈ 𝐶 ↔ (𝐶 ·o 𝐴) ∈ ((𝐶 ·o 𝐴) +o 𝐶))) |
66 | 65 | biimpa 477 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐶 ∈ On ∧ 𝐴 ∈ On) ∧ ∅ ∈
𝐶) → (𝐶 ·o 𝐴) ∈ ((𝐶 ·o 𝐴) +o 𝐶)) |
67 | | omsuc 8341 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐶 ∈ On ∧ 𝐴 ∈ On) → (𝐶 ·o suc 𝐴) = ((𝐶 ·o 𝐴) +o 𝐶)) |
68 | 67 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐶 ∈ On ∧ 𝐴 ∈ On) ∧ ∅ ∈
𝐶) → (𝐶 ·o suc 𝐴) = ((𝐶 ·o 𝐴) +o 𝐶)) |
69 | 66, 68 | eleqtrrd 2844 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐶 ∈ On ∧ 𝐴 ∈ On) ∧ ∅ ∈
𝐶) → (𝐶 ·o 𝐴) ∈ (𝐶 ·o suc 𝐴)) |
70 | 69 | adantrl 713 |
. . . . . . . . . . . . . . 15
⊢ (((𝐶 ∈ On ∧ 𝐴 ∈ On) ∧ (Lim 𝑥 ∧ ∅ ∈ 𝐶)) → (𝐶 ·o 𝐴) ∈ (𝐶 ·o suc 𝐴)) |
71 | 70 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((((𝐶 ∈ On ∧ 𝐴 ∈ On) ∧ (Lim 𝑥 ∧ ∅ ∈ 𝐶)) ∧ 𝐴 ∈ 𝑥) → (𝐶 ·o 𝐴) ∈ (𝐶 ·o suc 𝐴)) |
72 | 61, 71 | sseldd 3927 |
. . . . . . . . . . . . 13
⊢ ((((𝐶 ∈ On ∧ 𝐴 ∈ On) ∧ (Lim 𝑥 ∧ ∅ ∈ 𝐶)) ∧ 𝐴 ∈ 𝑥) → (𝐶 ·o 𝐴) ∈ (𝐶 ·o 𝑥)) |
73 | 72 | exp53 448 |
. . . . . . . . . . . 12
⊢ (𝐶 ∈ On → (𝐴 ∈ On → (Lim 𝑥 → (∅ ∈ 𝐶 → (𝐴 ∈ 𝑥 → (𝐶 ·o 𝐴) ∈ (𝐶 ·o 𝑥)))))) |
74 | 73 | com13 88 |
. . . . . . . . . . 11
⊢ (Lim
𝑥 → (𝐴 ∈ On → (𝐶 ∈ On → (∅ ∈ 𝐶 → (𝐴 ∈ 𝑥 → (𝐶 ·o 𝐴) ∈ (𝐶 ·o 𝑥)))))) |
75 | 74 | imp4c 424 |
. . . . . . . . . 10
⊢ (Lim
𝑥 → (((𝐴 ∈ On ∧ 𝐶 ∈ On) ∧ ∅ ∈
𝐶) → (𝐴 ∈ 𝑥 → (𝐶 ·o 𝐴) ∈ (𝐶 ·o 𝑥)))) |
76 | 75 | a1dd 50 |
. . . . . . . . 9
⊢ (Lim
𝑥 → (((𝐴 ∈ On ∧ 𝐶 ∈ On) ∧ ∅ ∈
𝐶) → (∀𝑦 ∈ 𝑥 (𝐴 ∈ 𝑦 → (𝐶 ·o 𝐴) ∈ (𝐶 ·o 𝑦)) → (𝐴 ∈ 𝑥 → (𝐶 ·o 𝐴) ∈ (𝐶 ·o 𝑥))))) |
77 | 6, 10, 14, 18, 21, 47, 76 | tfinds3 7705 |
. . . . . . . 8
⊢ (𝐵 ∈ On → (((𝐴 ∈ On ∧ 𝐶 ∈ On) ∧ ∅ ∈
𝐶) → (𝐴 ∈ 𝐵 → (𝐶 ·o 𝐴) ∈ (𝐶 ·o 𝐵)))) |
78 | 77 | com23 86 |
. . . . . . 7
⊢ (𝐵 ∈ On → (𝐴 ∈ 𝐵 → (((𝐴 ∈ On ∧ 𝐶 ∈ On) ∧ ∅ ∈ 𝐶) → (𝐶 ·o 𝐴) ∈ (𝐶 ·o 𝐵)))) |
79 | 78 | exp4a 432 |
. . . . . 6
⊢ (𝐵 ∈ On → (𝐴 ∈ 𝐵 → ((𝐴 ∈ On ∧ 𝐶 ∈ On) → (∅ ∈ 𝐶 → (𝐶 ·o 𝐴) ∈ (𝐶 ·o 𝐵))))) |
80 | 79 | exp4a 432 |
. . . . 5
⊢ (𝐵 ∈ On → (𝐴 ∈ 𝐵 → (𝐴 ∈ On → (𝐶 ∈ On → (∅ ∈ 𝐶 → (𝐶 ·o 𝐴) ∈ (𝐶 ·o 𝐵)))))) |
81 | 2, 80 | mpdd 43 |
. . . 4
⊢ (𝐵 ∈ On → (𝐴 ∈ 𝐵 → (𝐶 ∈ On → (∅ ∈ 𝐶 → (𝐶 ·o 𝐴) ∈ (𝐶 ·o 𝐵))))) |
82 | 81 | com34 91 |
. . 3
⊢ (𝐵 ∈ On → (𝐴 ∈ 𝐵 → (∅ ∈ 𝐶 → (𝐶 ∈ On → (𝐶 ·o 𝐴) ∈ (𝐶 ·o 𝐵))))) |
83 | 82 | com24 95 |
. 2
⊢ (𝐵 ∈ On → (𝐶 ∈ On → (∅
∈ 𝐶 → (𝐴 ∈ 𝐵 → (𝐶 ·o 𝐴) ∈ (𝐶 ·o 𝐵))))) |
84 | 83 | imp31 418 |
1
⊢ (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ ∅ ∈
𝐶) → (𝐴 ∈ 𝐵 → (𝐶 ·o 𝐴) ∈ (𝐶 ·o 𝐵))) |