Step | Hyp | Ref
| Expression |
1 | | limelon 5705 |
. . . 4
⊢ ((𝐵 ∈ 𝐶 ∧ Lim 𝐵) → 𝐵 ∈ On) |
2 | | omcl 7503 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ·𝑜
𝐵) ∈
On) |
3 | | eloni 5650 |
. . . . 5
⊢ ((𝐴 ·𝑜
𝐵) ∈ On → Ord
(𝐴
·𝑜 𝐵)) |
4 | 2, 3 | syl 17 |
. . . 4
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → Ord (𝐴 ·𝑜
𝐵)) |
5 | 1, 4 | sylan2 490 |
. . 3
⊢ ((𝐴 ∈ On ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) → Ord (𝐴 ·𝑜 𝐵)) |
6 | 5 | adantr 480 |
. 2
⊢ (((𝐴 ∈ On ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) ∧ ∅ ∈ 𝐴) → Ord (𝐴 ·𝑜 𝐵)) |
7 | | 0ellim 5704 |
. . . . . . . 8
⊢ (Lim
𝐵 → ∅ ∈
𝐵) |
8 | | n0i 3879 |
. . . . . . . 8
⊢ (∅
∈ 𝐵 → ¬ 𝐵 = ∅) |
9 | 7, 8 | syl 17 |
. . . . . . 7
⊢ (Lim
𝐵 → ¬ 𝐵 = ∅) |
10 | | n0i 3879 |
. . . . . . 7
⊢ (∅
∈ 𝐴 → ¬ 𝐴 = ∅) |
11 | 9, 10 | anim12ci 589 |
. . . . . 6
⊢ ((Lim
𝐵 ∧ ∅ ∈
𝐴) → (¬ 𝐴 = ∅ ∧ ¬ 𝐵 = ∅)) |
12 | 11 | adantll 746 |
. . . . 5
⊢ (((𝐵 ∈ 𝐶 ∧ Lim 𝐵) ∧ ∅ ∈ 𝐴) → (¬ 𝐴 = ∅ ∧ ¬ 𝐵 = ∅)) |
13 | 12 | adantll 746 |
. . . 4
⊢ (((𝐴 ∈ On ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) ∧ ∅ ∈ 𝐴) → (¬ 𝐴 = ∅ ∧ ¬ 𝐵 = ∅)) |
14 | | om00 7542 |
. . . . . . . 8
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐴 ·𝑜
𝐵) = ∅ ↔ (𝐴 = ∅ ∨ 𝐵 = ∅))) |
15 | 14 | notbid 307 |
. . . . . . 7
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (¬ (𝐴 ·𝑜
𝐵) = ∅ ↔ ¬
(𝐴 = ∅ ∨ 𝐵 = ∅))) |
16 | | ioran 510 |
. . . . . . 7
⊢ (¬
(𝐴 = ∅ ∨ 𝐵 = ∅) ↔ (¬ 𝐴 = ∅ ∧ ¬ 𝐵 = ∅)) |
17 | 15, 16 | syl6bb 275 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (¬ (𝐴 ·𝑜
𝐵) = ∅ ↔ (¬
𝐴 = ∅ ∧ ¬
𝐵 =
∅))) |
18 | 1, 17 | sylan2 490 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) → (¬ (𝐴 ·𝑜 𝐵) = ∅ ↔ (¬ 𝐴 = ∅ ∧ ¬ 𝐵 = ∅))) |
19 | 18 | adantr 480 |
. . . 4
⊢ (((𝐴 ∈ On ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) ∧ ∅ ∈ 𝐴) → (¬ (𝐴 ·𝑜 𝐵) = ∅ ↔ (¬ 𝐴 = ∅ ∧ ¬ 𝐵 = ∅))) |
20 | 13, 19 | mpbird 246 |
. . 3
⊢ (((𝐴 ∈ On ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) ∧ ∅ ∈ 𝐴) → ¬ (𝐴 ·𝑜 𝐵) = ∅) |
21 | | vex 3176 |
. . . . . . . . . . 11
⊢ 𝑦 ∈ V |
22 | 21 | sucid 5721 |
. . . . . . . . . 10
⊢ 𝑦 ∈ suc 𝑦 |
23 | | omlim 7500 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ On ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) → (𝐴 ·𝑜 𝐵) = ∪ 𝑥 ∈ 𝐵 (𝐴 ·𝑜 𝑥)) |
24 | | eqeq1 2614 |
. . . . . . . . . . . 12
⊢ ((𝐴 ·𝑜
𝐵) = suc 𝑦 → ((𝐴 ·𝑜 𝐵) = ∪ 𝑥 ∈ 𝐵 (𝐴 ·𝑜 𝑥) ↔ suc 𝑦 = ∪ 𝑥 ∈ 𝐵 (𝐴 ·𝑜 𝑥))) |
25 | 24 | biimpac 502 |
. . . . . . . . . . 11
⊢ (((𝐴 ·𝑜
𝐵) = ∪ 𝑥 ∈ 𝐵 (𝐴 ·𝑜 𝑥) ∧ (𝐴 ·𝑜 𝐵) = suc 𝑦) → suc 𝑦 = ∪ 𝑥 ∈ 𝐵 (𝐴 ·𝑜 𝑥)) |
26 | 23, 25 | sylan 487 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ On ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) ∧ (𝐴 ·𝑜 𝐵) = suc 𝑦) → suc 𝑦 = ∪ 𝑥 ∈ 𝐵 (𝐴 ·𝑜 𝑥)) |
27 | 22, 26 | syl5eleq 2694 |
. . . . . . . . 9
⊢ (((𝐴 ∈ On ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) ∧ (𝐴 ·𝑜 𝐵) = suc 𝑦) → 𝑦 ∈ ∪
𝑥 ∈ 𝐵 (𝐴 ·𝑜 𝑥)) |
28 | | eliun 4460 |
. . . . . . . . 9
⊢ (𝑦 ∈ ∪ 𝑥 ∈ 𝐵 (𝐴 ·𝑜 𝑥) ↔ ∃𝑥 ∈ 𝐵 𝑦 ∈ (𝐴 ·𝑜 𝑥)) |
29 | 27, 28 | sylib 207 |
. . . . . . . 8
⊢ (((𝐴 ∈ On ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) ∧ (𝐴 ·𝑜 𝐵) = suc 𝑦) → ∃𝑥 ∈ 𝐵 𝑦 ∈ (𝐴 ·𝑜 𝑥)) |
30 | 29 | adantlr 747 |
. . . . . . 7
⊢ ((((𝐴 ∈ On ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) ∧ ∅ ∈ 𝐴) ∧ (𝐴 ·𝑜 𝐵) = suc 𝑦) → ∃𝑥 ∈ 𝐵 𝑦 ∈ (𝐴 ·𝑜 𝑥)) |
31 | | onelon 5665 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐵 ∈ On ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ On) |
32 | 1, 31 | sylan 487 |
. . . . . . . . . . . . . . 15
⊢ (((𝐵 ∈ 𝐶 ∧ Lim 𝐵) ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ On) |
33 | | onnbtwn 5735 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ On → ¬ (𝑥 ∈ 𝐵 ∧ 𝐵 ∈ suc 𝑥)) |
34 | | imnan 437 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ 𝐵 → ¬ 𝐵 ∈ suc 𝑥) ↔ ¬ (𝑥 ∈ 𝐵 ∧ 𝐵 ∈ suc 𝑥)) |
35 | 33, 34 | sylibr 223 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ On → (𝑥 ∈ 𝐵 → ¬ 𝐵 ∈ suc 𝑥)) |
36 | 35 | com12 32 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ 𝐵 → (𝑥 ∈ On → ¬ 𝐵 ∈ suc 𝑥)) |
37 | 36 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ (((𝐵 ∈ 𝐶 ∧ Lim 𝐵) ∧ 𝑥 ∈ 𝐵) → (𝑥 ∈ On → ¬ 𝐵 ∈ suc 𝑥)) |
38 | 32, 37 | mpd 15 |
. . . . . . . . . . . . . 14
⊢ (((𝐵 ∈ 𝐶 ∧ Lim 𝐵) ∧ 𝑥 ∈ 𝐵) → ¬ 𝐵 ∈ suc 𝑥) |
39 | 38 | adantll 746 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ On ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) ∧ 𝑥 ∈ 𝐵) → ¬ 𝐵 ∈ suc 𝑥) |
40 | 39 | adantlr 747 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ On ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) ∧ ∅ ∈ 𝐴) ∧ 𝑥 ∈ 𝐵) → ¬ 𝐵 ∈ suc 𝑥) |
41 | 40 | adantr 480 |
. . . . . . . . . . 11
⊢
(((((𝐴 ∈ On
∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) ∧ ∅ ∈ 𝐴) ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ (𝐴 ·𝑜 𝑥)) → ¬ 𝐵 ∈ suc 𝑥) |
42 | | simpl 472 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐵 ∈ On ∧ 𝑥 ∈ 𝐵) → 𝐵 ∈ On) |
43 | 42, 31 | jca 553 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐵 ∈ On ∧ 𝑥 ∈ 𝐵) → (𝐵 ∈ On ∧ 𝑥 ∈ On)) |
44 | 1, 43 | sylan 487 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐵 ∈ 𝐶 ∧ Lim 𝐵) ∧ 𝑥 ∈ 𝐵) → (𝐵 ∈ On ∧ 𝑥 ∈ On)) |
45 | 44 | anim2i 591 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ On ∧ ((𝐵 ∈ 𝐶 ∧ Lim 𝐵) ∧ 𝑥 ∈ 𝐵)) → (𝐴 ∈ On ∧ (𝐵 ∈ On ∧ 𝑥 ∈ On))) |
46 | 45 | anassrs 678 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ On ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) ∧ 𝑥 ∈ 𝐵) → (𝐴 ∈ On ∧ (𝐵 ∈ On ∧ 𝑥 ∈ On))) |
47 | | omcl 7503 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ On) → (𝐴 ·𝑜
𝑥) ∈
On) |
48 | | eloni 5650 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐴 ·𝑜
𝑥) ∈ On → Ord
(𝐴
·𝑜 𝑥)) |
49 | | ordsucelsuc 6914 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (Ord
(𝐴
·𝑜 𝑥) → (𝑦 ∈ (𝐴 ·𝑜 𝑥) ↔ suc 𝑦 ∈ suc (𝐴 ·𝑜 𝑥))) |
50 | 48, 49 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐴 ·𝑜
𝑥) ∈ On → (𝑦 ∈ (𝐴 ·𝑜 𝑥) ↔ suc 𝑦 ∈ suc (𝐴 ·𝑜 𝑥))) |
51 | | oa1suc 7498 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐴 ·𝑜
𝑥) ∈ On → ((𝐴 ·𝑜
𝑥) +𝑜
1𝑜) = suc (𝐴 ·𝑜 𝑥)) |
52 | 51 | eleq2d 2673 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐴 ·𝑜
𝑥) ∈ On → (suc
𝑦 ∈ ((𝐴 ·𝑜
𝑥) +𝑜
1𝑜) ↔ suc 𝑦 ∈ suc (𝐴 ·𝑜 𝑥))) |
53 | 50, 52 | bitr4d 270 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐴 ·𝑜
𝑥) ∈ On → (𝑦 ∈ (𝐴 ·𝑜 𝑥) ↔ suc 𝑦 ∈ ((𝐴 ·𝑜 𝑥) +𝑜
1𝑜))) |
54 | 47, 53 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ On) → (𝑦 ∈ (𝐴 ·𝑜 𝑥) ↔ suc 𝑦 ∈ ((𝐴 ·𝑜 𝑥) +𝑜
1𝑜))) |
55 | 54 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴 ∈ On ∧ 𝑥 ∈ On) ∧ ∅ ∈
𝐴) → (𝑦 ∈ (𝐴 ·𝑜 𝑥) ↔ suc 𝑦 ∈ ((𝐴 ·𝑜 𝑥) +𝑜
1𝑜))) |
56 | | eloni 5650 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝐴 ∈ On → Ord 𝐴) |
57 | | ordgt0ge1 7464 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (Ord
𝐴 → (∅ ∈
𝐴 ↔
1𝑜 ⊆ 𝐴)) |
58 | 56, 57 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝐴 ∈ On → (∅
∈ 𝐴 ↔
1𝑜 ⊆ 𝐴)) |
59 | 58 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ On) → (∅
∈ 𝐴 ↔
1𝑜 ⊆ 𝐴)) |
60 | | 1on 7454 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
1𝑜 ∈ On |
61 | | oaword 7516 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((1𝑜 ∈ On ∧ 𝐴 ∈ On ∧ (𝐴 ·𝑜 𝑥) ∈ On) →
(1𝑜 ⊆ 𝐴 ↔ ((𝐴 ·𝑜 𝑥) +𝑜
1𝑜) ⊆ ((𝐴 ·𝑜 𝑥) +𝑜 𝐴))) |
62 | 60, 61 | mp3an1 1403 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐴 ∈ On ∧ (𝐴 ·𝑜
𝑥) ∈ On) →
(1𝑜 ⊆ 𝐴 ↔ ((𝐴 ·𝑜 𝑥) +𝑜
1𝑜) ⊆ ((𝐴 ·𝑜 𝑥) +𝑜 𝐴))) |
63 | 47, 62 | syldan 486 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ On) →
(1𝑜 ⊆ 𝐴 ↔ ((𝐴 ·𝑜 𝑥) +𝑜
1𝑜) ⊆ ((𝐴 ·𝑜 𝑥) +𝑜 𝐴))) |
64 | 59, 63 | bitrd 267 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ On) → (∅
∈ 𝐴 ↔ ((𝐴 ·𝑜
𝑥) +𝑜
1𝑜) ⊆ ((𝐴 ·𝑜 𝑥) +𝑜 𝐴))) |
65 | 64 | biimpa 500 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐴 ∈ On ∧ 𝑥 ∈ On) ∧ ∅ ∈
𝐴) → ((𝐴 ·𝑜
𝑥) +𝑜
1𝑜) ⊆ ((𝐴 ·𝑜 𝑥) +𝑜 𝐴)) |
66 | | omsuc 7493 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ On) → (𝐴 ·𝑜
suc 𝑥) = ((𝐴 ·𝑜
𝑥) +𝑜
𝐴)) |
67 | 66 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐴 ∈ On ∧ 𝑥 ∈ On) ∧ ∅ ∈
𝐴) → (𝐴 ·𝑜
suc 𝑥) = ((𝐴 ·𝑜
𝑥) +𝑜
𝐴)) |
68 | 65, 67 | sseqtr4d 3605 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐴 ∈ On ∧ 𝑥 ∈ On) ∧ ∅ ∈
𝐴) → ((𝐴 ·𝑜
𝑥) +𝑜
1𝑜) ⊆ (𝐴 ·𝑜 suc 𝑥)) |
69 | 68 | sseld 3567 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴 ∈ On ∧ 𝑥 ∈ On) ∧ ∅ ∈
𝐴) → (suc 𝑦 ∈ ((𝐴 ·𝑜 𝑥) +𝑜
1𝑜) → suc 𝑦 ∈ (𝐴 ·𝑜 suc 𝑥))) |
70 | 55, 69 | sylbid 229 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ On ∧ 𝑥 ∈ On) ∧ ∅ ∈
𝐴) → (𝑦 ∈ (𝐴 ·𝑜 𝑥) → suc 𝑦 ∈ (𝐴 ·𝑜 suc 𝑥))) |
71 | | eleq1 2676 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ·𝑜
𝐵) = suc 𝑦 → ((𝐴 ·𝑜 𝐵) ∈ (𝐴 ·𝑜 suc 𝑥) ↔ suc 𝑦 ∈ (𝐴 ·𝑜 suc 𝑥))) |
72 | 71 | biimprd 237 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ·𝑜
𝐵) = suc 𝑦 → (suc 𝑦 ∈ (𝐴 ·𝑜 suc 𝑥) → (𝐴 ·𝑜 𝐵) ∈ (𝐴 ·𝑜 suc 𝑥))) |
73 | 70, 72 | syl9 75 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ On ∧ 𝑥 ∈ On) ∧ ∅ ∈
𝐴) → ((𝐴 ·𝑜
𝐵) = suc 𝑦 → (𝑦 ∈ (𝐴 ·𝑜 𝑥) → (𝐴 ·𝑜 𝐵) ∈ (𝐴 ·𝑜 suc 𝑥)))) |
74 | 73 | com23 84 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ On ∧ 𝑥 ∈ On) ∧ ∅ ∈
𝐴) → (𝑦 ∈ (𝐴 ·𝑜 𝑥) → ((𝐴 ·𝑜 𝐵) = suc 𝑦 → (𝐴 ·𝑜 𝐵) ∈ (𝐴 ·𝑜 suc 𝑥)))) |
75 | 74 | adantlrl 752 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ On ∧ (𝐵 ∈ On ∧ 𝑥 ∈ On)) ∧ ∅
∈ 𝐴) → (𝑦 ∈ (𝐴 ·𝑜 𝑥) → ((𝐴 ·𝑜 𝐵) = suc 𝑦 → (𝐴 ·𝑜 𝐵) ∈ (𝐴 ·𝑜 suc 𝑥)))) |
76 | | sucelon 6909 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ On ↔ suc 𝑥 ∈ On) |
77 | | omord 7535 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐵 ∈ On ∧ suc 𝑥 ∈ On ∧ 𝐴 ∈ On) → ((𝐵 ∈ suc 𝑥 ∧ ∅ ∈ 𝐴) ↔ (𝐴 ·𝑜 𝐵) ∈ (𝐴 ·𝑜 suc 𝑥))) |
78 | | simpl 472 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐵 ∈ suc 𝑥 ∧ ∅ ∈ 𝐴) → 𝐵 ∈ suc 𝑥) |
79 | 77, 78 | syl6bir 243 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐵 ∈ On ∧ suc 𝑥 ∈ On ∧ 𝐴 ∈ On) → ((𝐴 ·𝑜
𝐵) ∈ (𝐴 ·𝑜
suc 𝑥) → 𝐵 ∈ suc 𝑥)) |
80 | 76, 79 | syl3an2b 1355 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐵 ∈ On ∧ 𝑥 ∈ On ∧ 𝐴 ∈ On) → ((𝐴 ·𝑜
𝐵) ∈ (𝐴 ·𝑜
suc 𝑥) → 𝐵 ∈ suc 𝑥)) |
81 | 80 | 3comr 1265 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑥 ∈ On) → ((𝐴 ·𝑜
𝐵) ∈ (𝐴 ·𝑜
suc 𝑥) → 𝐵 ∈ suc 𝑥)) |
82 | 81 | 3expb 1258 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ On ∧ (𝐵 ∈ On ∧ 𝑥 ∈ On)) → ((𝐴 ·𝑜
𝐵) ∈ (𝐴 ·𝑜
suc 𝑥) → 𝐵 ∈ suc 𝑥)) |
83 | 82 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ On ∧ (𝐵 ∈ On ∧ 𝑥 ∈ On)) ∧ ∅
∈ 𝐴) → ((𝐴 ·𝑜
𝐵) ∈ (𝐴 ·𝑜
suc 𝑥) → 𝐵 ∈ suc 𝑥)) |
84 | 75, 83 | syl6d 73 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ On ∧ (𝐵 ∈ On ∧ 𝑥 ∈ On)) ∧ ∅
∈ 𝐴) → (𝑦 ∈ (𝐴 ·𝑜 𝑥) → ((𝐴 ·𝑜 𝐵) = suc 𝑦 → 𝐵 ∈ suc 𝑥))) |
85 | 46, 84 | sylan 487 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ On ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) ∧ 𝑥 ∈ 𝐵) ∧ ∅ ∈ 𝐴) → (𝑦 ∈ (𝐴 ·𝑜 𝑥) → ((𝐴 ·𝑜 𝐵) = suc 𝑦 → 𝐵 ∈ suc 𝑥))) |
86 | 85 | an32s 842 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ On ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) ∧ ∅ ∈ 𝐴) ∧ 𝑥 ∈ 𝐵) → (𝑦 ∈ (𝐴 ·𝑜 𝑥) → ((𝐴 ·𝑜 𝐵) = suc 𝑦 → 𝐵 ∈ suc 𝑥))) |
87 | 86 | imp 444 |
. . . . . . . . . . 11
⊢
(((((𝐴 ∈ On
∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) ∧ ∅ ∈ 𝐴) ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ (𝐴 ·𝑜 𝑥)) → ((𝐴 ·𝑜 𝐵) = suc 𝑦 → 𝐵 ∈ suc 𝑥)) |
88 | 41, 87 | mtod 188 |
. . . . . . . . . 10
⊢
(((((𝐴 ∈ On
∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) ∧ ∅ ∈ 𝐴) ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ (𝐴 ·𝑜 𝑥)) → ¬ (𝐴 ·𝑜
𝐵) = suc 𝑦) |
89 | 88 | exp31 628 |
. . . . . . . . 9
⊢ (((𝐴 ∈ On ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) ∧ ∅ ∈ 𝐴) → (𝑥 ∈ 𝐵 → (𝑦 ∈ (𝐴 ·𝑜 𝑥) → ¬ (𝐴 ·𝑜
𝐵) = suc 𝑦))) |
90 | 89 | rexlimdv 3012 |
. . . . . . . 8
⊢ (((𝐴 ∈ On ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) ∧ ∅ ∈ 𝐴) → (∃𝑥 ∈ 𝐵 𝑦 ∈ (𝐴 ·𝑜 𝑥) → ¬ (𝐴 ·𝑜
𝐵) = suc 𝑦)) |
91 | 90 | adantr 480 |
. . . . . . 7
⊢ ((((𝐴 ∈ On ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) ∧ ∅ ∈ 𝐴) ∧ (𝐴 ·𝑜 𝐵) = suc 𝑦) → (∃𝑥 ∈ 𝐵 𝑦 ∈ (𝐴 ·𝑜 𝑥) → ¬ (𝐴 ·𝑜
𝐵) = suc 𝑦)) |
92 | 30, 91 | mpd 15 |
. . . . . 6
⊢ ((((𝐴 ∈ On ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) ∧ ∅ ∈ 𝐴) ∧ (𝐴 ·𝑜 𝐵) = suc 𝑦) → ¬ (𝐴 ·𝑜 𝐵) = suc 𝑦) |
93 | 92 | pm2.01da 457 |
. . . . 5
⊢ (((𝐴 ∈ On ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) ∧ ∅ ∈ 𝐴) → ¬ (𝐴 ·𝑜 𝐵) = suc 𝑦) |
94 | 93 | adantr 480 |
. . . 4
⊢ ((((𝐴 ∈ On ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) ∧ ∅ ∈ 𝐴) ∧ 𝑦 ∈ On) → ¬ (𝐴 ·𝑜 𝐵) = suc 𝑦) |
95 | 94 | nrexdv 2984 |
. . 3
⊢ (((𝐴 ∈ On ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) ∧ ∅ ∈ 𝐴) → ¬ ∃𝑦 ∈ On (𝐴 ·𝑜 𝐵) = suc 𝑦) |
96 | | ioran 510 |
. . 3
⊢ (¬
((𝐴
·𝑜 𝐵) = ∅ ∨ ∃𝑦 ∈ On (𝐴 ·𝑜 𝐵) = suc 𝑦) ↔ (¬ (𝐴 ·𝑜 𝐵) = ∅ ∧ ¬
∃𝑦 ∈ On (𝐴 ·𝑜
𝐵) = suc 𝑦)) |
97 | 20, 95, 96 | sylanbrc 695 |
. 2
⊢ (((𝐴 ∈ On ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) ∧ ∅ ∈ 𝐴) → ¬ ((𝐴 ·𝑜 𝐵) = ∅ ∨ ∃𝑦 ∈ On (𝐴 ·𝑜 𝐵) = suc 𝑦)) |
98 | | dflim3 6939 |
. 2
⊢ (Lim
(𝐴
·𝑜 𝐵) ↔ (Ord (𝐴 ·𝑜 𝐵) ∧ ¬ ((𝐴 ·𝑜
𝐵) = ∅ ∨
∃𝑦 ∈ On (𝐴 ·𝑜
𝐵) = suc 𝑦))) |
99 | 6, 97, 98 | sylanbrc 695 |
1
⊢ (((𝐴 ∈ On ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) ∧ ∅ ∈ 𝐴) → Lim (𝐴 ·𝑜 𝐵)) |