Step | Hyp | Ref
| Expression |
1 | | eldifi 4017 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐴 ∈ (On ∖
2o) → 𝐴
∈ On) |
2 | 1 | adantr 484 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) → 𝐴 ∈ On) |
3 | 2 | ad2antrr 726 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → 𝐴 ∈ On) |
4 | | simprl 771 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → 𝐶 ∈ On) |
5 | | oecl 8193 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ On ∧ 𝐶 ∈ On) → (𝐴 ↑o 𝐶) ∈ On) |
6 | 3, 4, 5 | syl2anc 587 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → (𝐴 ↑o 𝐶) ∈ On) |
7 | | om1 8199 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ↑o 𝐶) ∈ On → ((𝐴 ↑o 𝐶) ·o
1o) = (𝐴
↑o 𝐶)) |
8 | 6, 7 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → ((𝐴 ↑o 𝐶) ·o
1o) = (𝐴
↑o 𝐶)) |
9 | | df1o2 8143 |
. . . . . . . . . . . . . . . 16
⊢
1o = {∅} |
10 | | dif1o 8156 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐷 ∈ (𝐴 ∖ 1o) ↔ (𝐷 ∈ 𝐴 ∧ 𝐷 ≠ ∅)) |
11 | 10 | simprbi 500 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐷 ∈ (𝐴 ∖ 1o) → 𝐷 ≠ ∅) |
12 | 11 | ad2antll 729 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → 𝐷 ≠ ∅) |
13 | | eldifi 4017 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐷 ∈ (𝐴 ∖ 1o) → 𝐷 ∈ 𝐴) |
14 | 13 | ad2antll 729 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → 𝐷 ∈ 𝐴) |
15 | | onelon 6197 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐴 ∈ On ∧ 𝐷 ∈ 𝐴) → 𝐷 ∈ On) |
16 | 3, 14, 15 | syl2anc 587 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → 𝐷 ∈ On) |
17 | | on0eln0 6227 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐷 ∈ On → (∅
∈ 𝐷 ↔ 𝐷 ≠ ∅)) |
18 | 16, 17 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → (∅
∈ 𝐷 ↔ 𝐷 ≠ ∅)) |
19 | 12, 18 | mpbird 260 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → ∅
∈ 𝐷) |
20 | 19 | snssd 4697 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → {∅}
⊆ 𝐷) |
21 | 9, 20 | eqsstrid 3925 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) →
1o ⊆ 𝐷) |
22 | | 1on 8138 |
. . . . . . . . . . . . . . . . 17
⊢
1o ∈ On |
23 | 22 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) →
1o ∈ On) |
24 | | omwordi 8228 |
. . . . . . . . . . . . . . . 16
⊢
((1o ∈ On ∧ 𝐷 ∈ On ∧ (𝐴 ↑o 𝐶) ∈ On) → (1o ⊆
𝐷 → ((𝐴 ↑o 𝐶) ·o
1o) ⊆ ((𝐴
↑o 𝐶)
·o 𝐷))) |
25 | 23, 16, 6, 24 | syl3anc 1372 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) →
(1o ⊆ 𝐷
→ ((𝐴
↑o 𝐶)
·o 1o) ⊆ ((𝐴 ↑o 𝐶) ·o 𝐷))) |
26 | 21, 25 | mpd 15 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → ((𝐴 ↑o 𝐶) ·o
1o) ⊆ ((𝐴
↑o 𝐶)
·o 𝐷)) |
27 | 8, 26 | eqsstrrd 3916 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → (𝐴 ↑o 𝐶) ⊆ ((𝐴 ↑o 𝐶) ·o 𝐷)) |
28 | | omcl 8192 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ↑o 𝐶) ∈ On ∧ 𝐷 ∈ On) → ((𝐴 ↑o 𝐶) ·o 𝐷) ∈ On) |
29 | 6, 16, 28 | syl2anc 587 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → ((𝐴 ↑o 𝐶) ·o 𝐷) ∈ On) |
30 | | simplrl 777 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → 𝐸 ∈ (𝐴 ↑o 𝐶)) |
31 | | onelon 6197 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ↑o 𝐶) ∈ On ∧ 𝐸 ∈ (𝐴 ↑o 𝐶)) → 𝐸 ∈ On) |
32 | 6, 30, 31 | syl2anc 587 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → 𝐸 ∈ On) |
33 | | oaword1 8209 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ↑o 𝐶) ·o 𝐷) ∈ On ∧ 𝐸 ∈ On) → ((𝐴 ↑o 𝐶) ·o 𝐷) ⊆ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸)) |
34 | 29, 32, 33 | syl2anc 587 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → ((𝐴 ↑o 𝐶) ·o 𝐷) ⊆ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸)) |
35 | | simplrr 778 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵) |
36 | 34, 35 | sseqtrd 3917 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → ((𝐴 ↑o 𝐶) ·o 𝐷) ⊆ 𝐵) |
37 | 27, 36 | sstrd 3887 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → (𝐴 ↑o 𝐶) ⊆ 𝐵) |
38 | | oeeu.1 |
. . . . . . . . . . . . . . 15
⊢ 𝑋 = ∪
∩ {𝑥 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑥)} |
39 | 38 | oeeulem 8258 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) → (𝑋 ∈ On ∧ (𝐴 ↑o 𝑋) ⊆ 𝐵 ∧ 𝐵 ∈ (𝐴 ↑o suc 𝑋))) |
40 | 39 | simp3d 1145 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) → 𝐵 ∈ (𝐴 ↑o suc 𝑋)) |
41 | 40 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → 𝐵 ∈ (𝐴 ↑o suc 𝑋)) |
42 | 39 | simp1d 1143 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) → 𝑋 ∈ On) |
43 | 42 | ad2antrr 726 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → 𝑋 ∈ On) |
44 | | suceloni 7547 |
. . . . . . . . . . . . . . 15
⊢ (𝑋 ∈ On → suc 𝑋 ∈ On) |
45 | 43, 44 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → suc 𝑋 ∈ On) |
46 | | oecl 8193 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ On ∧ suc 𝑋 ∈ On) → (𝐴 ↑o suc 𝑋) ∈ On) |
47 | 3, 45, 46 | syl2anc 587 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → (𝐴 ↑o suc 𝑋) ∈ On) |
48 | | ontr2 6219 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ↑o 𝐶) ∈ On ∧ (𝐴 ↑o suc 𝑋) ∈ On) → (((𝐴 ↑o 𝐶) ⊆ 𝐵 ∧ 𝐵 ∈ (𝐴 ↑o suc 𝑋)) → (𝐴 ↑o 𝐶) ∈ (𝐴 ↑o suc 𝑋))) |
49 | 6, 47, 48 | syl2anc 587 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → (((𝐴 ↑o 𝐶) ⊆ 𝐵 ∧ 𝐵 ∈ (𝐴 ↑o suc 𝑋)) → (𝐴 ↑o 𝐶) ∈ (𝐴 ↑o suc 𝑋))) |
50 | 37, 41, 49 | mp2and 699 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → (𝐴 ↑o 𝐶) ∈ (𝐴 ↑o suc 𝑋)) |
51 | | simplll 775 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → 𝐴 ∈ (On ∖
2o)) |
52 | | oeord 8245 |
. . . . . . . . . . . 12
⊢ ((𝐶 ∈ On ∧ suc 𝑋 ∈ On ∧ 𝐴 ∈ (On ∖
2o)) → (𝐶
∈ suc 𝑋 ↔ (𝐴 ↑o 𝐶) ∈ (𝐴 ↑o suc 𝑋))) |
53 | 4, 45, 51, 52 | syl3anc 1372 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → (𝐶 ∈ suc 𝑋 ↔ (𝐴 ↑o 𝐶) ∈ (𝐴 ↑o suc 𝑋))) |
54 | 50, 53 | mpbird 260 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → 𝐶 ∈ suc 𝑋) |
55 | | onsssuc 6259 |
. . . . . . . . . . 11
⊢ ((𝐶 ∈ On ∧ 𝑋 ∈ On) → (𝐶 ⊆ 𝑋 ↔ 𝐶 ∈ suc 𝑋)) |
56 | 4, 43, 55 | syl2anc 587 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → (𝐶 ⊆ 𝑋 ↔ 𝐶 ∈ suc 𝑋)) |
57 | 54, 56 | mpbird 260 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → 𝐶 ⊆ 𝑋) |
58 | 39 | simp2d 1144 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) → (𝐴 ↑o 𝑋) ⊆ 𝐵) |
59 | 58 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → (𝐴 ↑o 𝑋) ⊆ 𝐵) |
60 | | eloni 6182 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ On → Ord 𝐴) |
61 | 3, 60 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → Ord 𝐴) |
62 | | ordsucss 7552 |
. . . . . . . . . . . . . . . 16
⊢ (Ord
𝐴 → (𝐷 ∈ 𝐴 → suc 𝐷 ⊆ 𝐴)) |
63 | 61, 14, 62 | sylc 65 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → suc 𝐷 ⊆ 𝐴) |
64 | | suceloni 7547 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐷 ∈ On → suc 𝐷 ∈ On) |
65 | 16, 64 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → suc 𝐷 ∈ On) |
66 | | dif20el 8161 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐴 ∈ (On ∖
2o) → ∅ ∈ 𝐴) |
67 | 51, 66 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → ∅
∈ 𝐴) |
68 | | oen0 8243 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ On ∧ 𝐶 ∈ On) ∧ ∅ ∈
𝐴) → ∅ ∈
(𝐴 ↑o 𝐶)) |
69 | 3, 4, 67, 68 | syl21anc 837 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → ∅
∈ (𝐴
↑o 𝐶)) |
70 | | omword 8227 |
. . . . . . . . . . . . . . . 16
⊢ (((suc
𝐷 ∈ On ∧ 𝐴 ∈ On ∧ (𝐴 ↑o 𝐶) ∈ On) ∧ ∅
∈ (𝐴
↑o 𝐶))
→ (suc 𝐷 ⊆ 𝐴 ↔ ((𝐴 ↑o 𝐶) ·o suc 𝐷) ⊆ ((𝐴 ↑o 𝐶) ·o 𝐴))) |
71 | 65, 3, 6, 69, 70 | syl31anc 1374 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → (suc 𝐷 ⊆ 𝐴 ↔ ((𝐴 ↑o 𝐶) ·o suc 𝐷) ⊆ ((𝐴 ↑o 𝐶) ·o 𝐴))) |
72 | 63, 71 | mpbid 235 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → ((𝐴 ↑o 𝐶) ·o suc 𝐷) ⊆ ((𝐴 ↑o 𝐶) ·o 𝐴)) |
73 | | oaord 8204 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐸 ∈ On ∧ (𝐴 ↑o 𝐶) ∈ On ∧ ((𝐴 ↑o 𝐶) ·o 𝐷) ∈ On) → (𝐸 ∈ (𝐴 ↑o 𝐶) ↔ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) ∈ (((𝐴 ↑o 𝐶) ·o 𝐷) +o (𝐴 ↑o 𝐶)))) |
74 | 32, 6, 29, 73 | syl3anc 1372 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → (𝐸 ∈ (𝐴 ↑o 𝐶) ↔ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) ∈ (((𝐴 ↑o 𝐶) ·o 𝐷) +o (𝐴 ↑o 𝐶)))) |
75 | 30, 74 | mpbid 235 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) ∈ (((𝐴 ↑o 𝐶) ·o 𝐷) +o (𝐴 ↑o 𝐶))) |
76 | 35, 75 | eqeltrrd 2834 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → 𝐵 ∈ (((𝐴 ↑o 𝐶) ·o 𝐷) +o (𝐴 ↑o 𝐶))) |
77 | | odi 8236 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ↑o 𝐶) ∈ On ∧ 𝐷 ∈ On ∧ 1o
∈ On) → ((𝐴
↑o 𝐶)
·o (𝐷
+o 1o)) = (((𝐴 ↑o 𝐶) ·o 𝐷) +o ((𝐴 ↑o 𝐶) ·o
1o))) |
78 | 6, 16, 23, 77 | syl3anc 1372 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → ((𝐴 ↑o 𝐶) ·o (𝐷 +o 1o)) =
(((𝐴 ↑o
𝐶) ·o
𝐷) +o ((𝐴 ↑o 𝐶) ·o
1o))) |
79 | | oa1suc 8187 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐷 ∈ On → (𝐷 +o 1o) =
suc 𝐷) |
80 | 16, 79 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → (𝐷 +o 1o) =
suc 𝐷) |
81 | 80 | oveq2d 7186 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → ((𝐴 ↑o 𝐶) ·o (𝐷 +o 1o)) =
((𝐴 ↑o
𝐶) ·o suc
𝐷)) |
82 | 8 | oveq2d 7186 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → (((𝐴 ↑o 𝐶) ·o 𝐷) +o ((𝐴 ↑o 𝐶) ·o
1o)) = (((𝐴
↑o 𝐶)
·o 𝐷)
+o (𝐴
↑o 𝐶))) |
83 | 78, 81, 82 | 3eqtr3d 2781 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → ((𝐴 ↑o 𝐶) ·o suc 𝐷) = (((𝐴 ↑o 𝐶) ·o 𝐷) +o (𝐴 ↑o 𝐶))) |
84 | 76, 83 | eleqtrrd 2836 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → 𝐵 ∈ ((𝐴 ↑o 𝐶) ·o suc 𝐷)) |
85 | 72, 84 | sseldd 3878 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → 𝐵 ∈ ((𝐴 ↑o 𝐶) ·o 𝐴)) |
86 | | oesuc 8183 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ On ∧ 𝐶 ∈ On) → (𝐴 ↑o suc 𝐶) = ((𝐴 ↑o 𝐶) ·o 𝐴)) |
87 | 3, 4, 86 | syl2anc 587 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → (𝐴 ↑o suc 𝐶) = ((𝐴 ↑o 𝐶) ·o 𝐴)) |
88 | 85, 87 | eleqtrrd 2836 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → 𝐵 ∈ (𝐴 ↑o suc 𝐶)) |
89 | | oecl 8193 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ On ∧ 𝑋 ∈ On) → (𝐴 ↑o 𝑋) ∈ On) |
90 | 3, 43, 89 | syl2anc 587 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → (𝐴 ↑o 𝑋) ∈ On) |
91 | | suceloni 7547 |
. . . . . . . . . . . . . . 15
⊢ (𝐶 ∈ On → suc 𝐶 ∈ On) |
92 | 91 | ad2antrl 728 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → suc 𝐶 ∈ On) |
93 | | oecl 8193 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ On ∧ suc 𝐶 ∈ On) → (𝐴 ↑o suc 𝐶) ∈ On) |
94 | 3, 92, 93 | syl2anc 587 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → (𝐴 ↑o suc 𝐶) ∈ On) |
95 | | ontr2 6219 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ↑o 𝑋) ∈ On ∧ (𝐴 ↑o suc 𝐶) ∈ On) → (((𝐴 ↑o 𝑋) ⊆ 𝐵 ∧ 𝐵 ∈ (𝐴 ↑o suc 𝐶)) → (𝐴 ↑o 𝑋) ∈ (𝐴 ↑o suc 𝐶))) |
96 | 90, 94, 95 | syl2anc 587 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → (((𝐴 ↑o 𝑋) ⊆ 𝐵 ∧ 𝐵 ∈ (𝐴 ↑o suc 𝐶)) → (𝐴 ↑o 𝑋) ∈ (𝐴 ↑o suc 𝐶))) |
97 | 59, 88, 96 | mp2and 699 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → (𝐴 ↑o 𝑋) ∈ (𝐴 ↑o suc 𝐶)) |
98 | | oeord 8245 |
. . . . . . . . . . . 12
⊢ ((𝑋 ∈ On ∧ suc 𝐶 ∈ On ∧ 𝐴 ∈ (On ∖
2o)) → (𝑋
∈ suc 𝐶 ↔ (𝐴 ↑o 𝑋) ∈ (𝐴 ↑o suc 𝐶))) |
99 | 43, 92, 51, 98 | syl3anc 1372 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → (𝑋 ∈ suc 𝐶 ↔ (𝐴 ↑o 𝑋) ∈ (𝐴 ↑o suc 𝐶))) |
100 | 97, 99 | mpbird 260 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → 𝑋 ∈ suc 𝐶) |
101 | | onsssuc 6259 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ On ∧ 𝐶 ∈ On) → (𝑋 ⊆ 𝐶 ↔ 𝑋 ∈ suc 𝐶)) |
102 | 43, 4, 101 | syl2anc 587 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → (𝑋 ⊆ 𝐶 ↔ 𝑋 ∈ suc 𝐶)) |
103 | 100, 102 | mpbird 260 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → 𝑋 ⊆ 𝐶) |
104 | 57, 103 | eqssd 3894 |
. . . . . . . 8
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → 𝐶 = 𝑋) |
105 | 104, 16 | jca 515 |
. . . . . . 7
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) → (𝐶 = 𝑋 ∧ 𝐷 ∈ On)) |
106 | | simprl 771 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋 ∧ 𝐷 ∈ On)) → 𝐶 = 𝑋) |
107 | 42 | ad2antrr 726 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋 ∧ 𝐷 ∈ On)) → 𝑋 ∈ On) |
108 | 106, 107 | eqeltrd 2833 |
. . . . . . . 8
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋 ∧ 𝐷 ∈ On)) → 𝐶 ∈ On) |
109 | 2 | ad2antrr 726 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋 ∧ 𝐷 ∈ On)) → 𝐴 ∈ On) |
110 | 109, 108,
5 | syl2anc 587 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋 ∧ 𝐷 ∈ On)) → (𝐴 ↑o 𝐶) ∈ On) |
111 | | simprr 773 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋 ∧ 𝐷 ∈ On)) → 𝐷 ∈ On) |
112 | 110, 111,
28 | syl2anc 587 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋 ∧ 𝐷 ∈ On)) → ((𝐴 ↑o 𝐶) ·o 𝐷) ∈ On) |
113 | | simplrl 777 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋 ∧ 𝐷 ∈ On)) → 𝐸 ∈ (𝐴 ↑o 𝐶)) |
114 | 110, 113,
31 | syl2anc 587 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋 ∧ 𝐷 ∈ On)) → 𝐸 ∈ On) |
115 | 112, 114,
33 | syl2anc 587 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋 ∧ 𝐷 ∈ On)) → ((𝐴 ↑o 𝐶) ·o 𝐷) ⊆ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸)) |
116 | | simplrr 778 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋 ∧ 𝐷 ∈ On)) → (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵) |
117 | 115, 116 | sseqtrd 3917 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋 ∧ 𝐷 ∈ On)) → ((𝐴 ↑o 𝐶) ·o 𝐷) ⊆ 𝐵) |
118 | 40 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋 ∧ 𝐷 ∈ On)) → 𝐵 ∈ (𝐴 ↑o suc 𝑋)) |
119 | | suceq 6237 |
. . . . . . . . . . . . . . 15
⊢ (𝐶 = 𝑋 → suc 𝐶 = suc 𝑋) |
120 | 119 | ad2antrl 728 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋 ∧ 𝐷 ∈ On)) → suc 𝐶 = suc 𝑋) |
121 | 120 | oveq2d 7186 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋 ∧ 𝐷 ∈ On)) → (𝐴 ↑o suc 𝐶) = (𝐴 ↑o suc 𝑋)) |
122 | 109, 108,
86 | syl2anc 587 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋 ∧ 𝐷 ∈ On)) → (𝐴 ↑o suc 𝐶) = ((𝐴 ↑o 𝐶) ·o 𝐴)) |
123 | 121, 122 | eqtr3d 2775 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋 ∧ 𝐷 ∈ On)) → (𝐴 ↑o suc 𝑋) = ((𝐴 ↑o 𝐶) ·o 𝐴)) |
124 | 118, 123 | eleqtrd 2835 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋 ∧ 𝐷 ∈ On)) → 𝐵 ∈ ((𝐴 ↑o 𝐶) ·o 𝐴)) |
125 | | omcl 8192 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ↑o 𝐶) ∈ On ∧ 𝐴 ∈ On) → ((𝐴 ↑o 𝐶) ·o 𝐴) ∈ On) |
126 | 110, 109,
125 | syl2anc 587 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋 ∧ 𝐷 ∈ On)) → ((𝐴 ↑o 𝐶) ·o 𝐴) ∈ On) |
127 | | ontr2 6219 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ↑o 𝐶) ·o 𝐷) ∈ On ∧ ((𝐴 ↑o 𝐶) ·o 𝐴) ∈ On) → ((((𝐴 ↑o 𝐶) ·o 𝐷) ⊆ 𝐵 ∧ 𝐵 ∈ ((𝐴 ↑o 𝐶) ·o 𝐴)) → ((𝐴 ↑o 𝐶) ·o 𝐷) ∈ ((𝐴 ↑o 𝐶) ·o 𝐴))) |
128 | 112, 126,
127 | syl2anc 587 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋 ∧ 𝐷 ∈ On)) → ((((𝐴 ↑o 𝐶) ·o 𝐷) ⊆ 𝐵 ∧ 𝐵 ∈ ((𝐴 ↑o 𝐶) ·o 𝐴)) → ((𝐴 ↑o 𝐶) ·o 𝐷) ∈ ((𝐴 ↑o 𝐶) ·o 𝐴))) |
129 | 117, 124,
128 | mp2and 699 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋 ∧ 𝐷 ∈ On)) → ((𝐴 ↑o 𝐶) ·o 𝐷) ∈ ((𝐴 ↑o 𝐶) ·o 𝐴)) |
130 | 66 | adantr 484 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) → ∅ ∈ 𝐴) |
131 | 130 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋 ∧ 𝐷 ∈ On)) → ∅ ∈ 𝐴) |
132 | 109, 108,
131, 68 | syl21anc 837 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋 ∧ 𝐷 ∈ On)) → ∅ ∈ (𝐴 ↑o 𝐶)) |
133 | | omord2 8224 |
. . . . . . . . . . 11
⊢ (((𝐷 ∈ On ∧ 𝐴 ∈ On ∧ (𝐴 ↑o 𝐶) ∈ On) ∧ ∅
∈ (𝐴
↑o 𝐶))
→ (𝐷 ∈ 𝐴 ↔ ((𝐴 ↑o 𝐶) ·o 𝐷) ∈ ((𝐴 ↑o 𝐶) ·o 𝐴))) |
134 | 111, 109,
110, 132, 133 | syl31anc 1374 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋 ∧ 𝐷 ∈ On)) → (𝐷 ∈ 𝐴 ↔ ((𝐴 ↑o 𝐶) ·o 𝐷) ∈ ((𝐴 ↑o 𝐶) ·o 𝐴))) |
135 | 129, 134 | mpbird 260 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋 ∧ 𝐷 ∈ On)) → 𝐷 ∈ 𝐴) |
136 | 106 | oveq2d 7186 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋 ∧ 𝐷 ∈ On)) → (𝐴 ↑o 𝐶) = (𝐴 ↑o 𝑋)) |
137 | 58 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋 ∧ 𝐷 ∈ On)) → (𝐴 ↑o 𝑋) ⊆ 𝐵) |
138 | 136, 137 | eqsstrd 3915 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋 ∧ 𝐷 ∈ On)) → (𝐴 ↑o 𝐶) ⊆ 𝐵) |
139 | | eldifi 4017 |
. . . . . . . . . . . . . 14
⊢ (𝐵 ∈ (On ∖
1o) → 𝐵
∈ On) |
140 | 139 | adantl 485 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) → 𝐵 ∈ On) |
141 | 140 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋 ∧ 𝐷 ∈ On)) → 𝐵 ∈ On) |
142 | | ontri1 6206 |
. . . . . . . . . . . 12
⊢ (((𝐴 ↑o 𝐶) ∈ On ∧ 𝐵 ∈ On) → ((𝐴 ↑o 𝐶) ⊆ 𝐵 ↔ ¬ 𝐵 ∈ (𝐴 ↑o 𝐶))) |
143 | 110, 141,
142 | syl2anc 587 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋 ∧ 𝐷 ∈ On)) → ((𝐴 ↑o 𝐶) ⊆ 𝐵 ↔ ¬ 𝐵 ∈ (𝐴 ↑o 𝐶))) |
144 | 138, 143 | mpbid 235 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋 ∧ 𝐷 ∈ On)) → ¬ 𝐵 ∈ (𝐴 ↑o 𝐶)) |
145 | | om0 8173 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ↑o 𝐶) ∈ On → ((𝐴 ↑o 𝐶) ·o ∅)
= ∅) |
146 | 110, 145 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋 ∧ 𝐷 ∈ On)) → ((𝐴 ↑o 𝐶) ·o ∅) =
∅) |
147 | 146 | oveq1d 7185 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋 ∧ 𝐷 ∈ On)) → (((𝐴 ↑o 𝐶) ·o ∅)
+o 𝐸) = (∅
+o 𝐸)) |
148 | | oa0r 8194 |
. . . . . . . . . . . . . . . 16
⊢ (𝐸 ∈ On → (∅
+o 𝐸) = 𝐸) |
149 | 114, 148 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋 ∧ 𝐷 ∈ On)) → (∅ +o
𝐸) = 𝐸) |
150 | 147, 149 | eqtrd 2773 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋 ∧ 𝐷 ∈ On)) → (((𝐴 ↑o 𝐶) ·o ∅)
+o 𝐸) = 𝐸) |
151 | 150, 113 | eqeltrd 2833 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋 ∧ 𝐷 ∈ On)) → (((𝐴 ↑o 𝐶) ·o ∅)
+o 𝐸) ∈
(𝐴 ↑o 𝐶)) |
152 | | oveq2 7178 |
. . . . . . . . . . . . . . 15
⊢ (𝐷 = ∅ → ((𝐴 ↑o 𝐶) ·o 𝐷) = ((𝐴 ↑o 𝐶) ·o
∅)) |
153 | 152 | oveq1d 7185 |
. . . . . . . . . . . . . 14
⊢ (𝐷 = ∅ → (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = (((𝐴 ↑o 𝐶) ·o ∅)
+o 𝐸)) |
154 | 153 | eleq1d 2817 |
. . . . . . . . . . . . 13
⊢ (𝐷 = ∅ → ((((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) ∈ (𝐴 ↑o 𝐶) ↔ (((𝐴 ↑o 𝐶) ·o ∅)
+o 𝐸) ∈
(𝐴 ↑o 𝐶))) |
155 | 151, 154 | syl5ibrcom 250 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋 ∧ 𝐷 ∈ On)) → (𝐷 = ∅ → (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) ∈ (𝐴 ↑o 𝐶))) |
156 | 116 | eleq1d 2817 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋 ∧ 𝐷 ∈ On)) → ((((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) ∈ (𝐴 ↑o 𝐶) ↔ 𝐵 ∈ (𝐴 ↑o 𝐶))) |
157 | 155, 156 | sylibd 242 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋 ∧ 𝐷 ∈ On)) → (𝐷 = ∅ → 𝐵 ∈ (𝐴 ↑o 𝐶))) |
158 | 157 | necon3bd 2948 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋 ∧ 𝐷 ∈ On)) → (¬ 𝐵 ∈ (𝐴 ↑o 𝐶) → 𝐷 ≠ ∅)) |
159 | 144, 158 | mpd 15 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋 ∧ 𝐷 ∈ On)) → 𝐷 ≠ ∅) |
160 | 135, 159,
10 | sylanbrc 586 |
. . . . . . . 8
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋 ∧ 𝐷 ∈ On)) → 𝐷 ∈ (𝐴 ∖ 1o)) |
161 | 108, 160 | jca 515 |
. . . . . . 7
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ∧ (𝐶 = 𝑋 ∧ 𝐷 ∈ On)) → (𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o))) |
162 | 105, 161 | impbida 801 |
. . . . . 6
⊢ (((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ (𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) → ((𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o)) ↔ (𝐶 = 𝑋 ∧ 𝐷 ∈ On))) |
163 | 162 | ex 416 |
. . . . 5
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) → ((𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵) → ((𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o)) ↔ (𝐶 = 𝑋 ∧ 𝐷 ∈ On)))) |
164 | 163 | pm5.32rd 581 |
. . . 4
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) → (((𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o)) ∧ (𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ↔ ((𝐶 = 𝑋 ∧ 𝐷 ∈ On) ∧ (𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)))) |
165 | | anass 472 |
. . . 4
⊢ (((𝐶 = 𝑋 ∧ 𝐷 ∈ On) ∧ (𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ↔ (𝐶 = 𝑋 ∧ (𝐷 ∈ On ∧ (𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)))) |
166 | 164, 165 | bitrdi 290 |
. . 3
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) → (((𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o)) ∧ (𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ↔ (𝐶 = 𝑋 ∧ (𝐷 ∈ On ∧ (𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵))))) |
167 | | 3anass 1096 |
. . . . . 6
⊢ ((𝐷 ∈ On ∧ 𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵) ↔ (𝐷 ∈ On ∧ (𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵))) |
168 | | oveq2 7178 |
. . . . . . . 8
⊢ (𝐶 = 𝑋 → (𝐴 ↑o 𝐶) = (𝐴 ↑o 𝑋)) |
169 | 168 | eleq2d 2818 |
. . . . . . 7
⊢ (𝐶 = 𝑋 → (𝐸 ∈ (𝐴 ↑o 𝐶) ↔ 𝐸 ∈ (𝐴 ↑o 𝑋))) |
170 | 168 | oveq1d 7185 |
. . . . . . . . 9
⊢ (𝐶 = 𝑋 → ((𝐴 ↑o 𝐶) ·o 𝐷) = ((𝐴 ↑o 𝑋) ·o 𝐷)) |
171 | 170 | oveq1d 7185 |
. . . . . . . 8
⊢ (𝐶 = 𝑋 → (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = (((𝐴 ↑o 𝑋) ·o 𝐷) +o 𝐸)) |
172 | 171 | eqeq1d 2740 |
. . . . . . 7
⊢ (𝐶 = 𝑋 → ((((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵 ↔ (((𝐴 ↑o 𝑋) ·o 𝐷) +o 𝐸) = 𝐵)) |
173 | 169, 172 | 3anbi23d 1440 |
. . . . . 6
⊢ (𝐶 = 𝑋 → ((𝐷 ∈ On ∧ 𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵) ↔ (𝐷 ∈ On ∧ 𝐸 ∈ (𝐴 ↑o 𝑋) ∧ (((𝐴 ↑o 𝑋) ·o 𝐷) +o 𝐸) = 𝐵))) |
174 | 167, 173 | bitr3id 288 |
. . . . 5
⊢ (𝐶 = 𝑋 → ((𝐷 ∈ On ∧ (𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ↔ (𝐷 ∈ On ∧ 𝐸 ∈ (𝐴 ↑o 𝑋) ∧ (((𝐴 ↑o 𝑋) ·o 𝐷) +o 𝐸) = 𝐵))) |
175 | 2, 42, 89 | syl2anc 587 |
. . . . . 6
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) → (𝐴 ↑o 𝑋) ∈ On) |
176 | | oen0 8243 |
. . . . . . . 8
⊢ (((𝐴 ∈ On ∧ 𝑋 ∈ On) ∧ ∅ ∈
𝐴) → ∅ ∈
(𝐴 ↑o 𝑋)) |
177 | 2, 42, 130, 176 | syl21anc 837 |
. . . . . . 7
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) → ∅ ∈ (𝐴 ↑o 𝑋)) |
178 | 177 | ne0d 4224 |
. . . . . 6
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) → (𝐴 ↑o 𝑋) ≠ ∅) |
179 | | omeu 8242 |
. . . . . . 7
⊢ (((𝐴 ↑o 𝑋) ∈ On ∧ 𝐵 ∈ On ∧ (𝐴 ↑o 𝑋) ≠ ∅) →
∃!𝑎∃𝑑 ∈ On ∃𝑒 ∈ (𝐴 ↑o 𝑋)(𝑎 = 〈𝑑, 𝑒〉 ∧ (((𝐴 ↑o 𝑋) ·o 𝑑) +o 𝑒) = 𝐵)) |
180 | | oeeu.2 |
. . . . . . . . 9
⊢ 𝑃 = (℩𝑤∃𝑦 ∈ On ∃𝑧 ∈ (𝐴 ↑o 𝑋)(𝑤 = 〈𝑦, 𝑧〉 ∧ (((𝐴 ↑o 𝑋) ·o 𝑦) +o 𝑧) = 𝐵)) |
181 | | opeq1 4759 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 𝑑 → 〈𝑦, 𝑧〉 = 〈𝑑, 𝑧〉) |
182 | 181 | eqeq2d 2749 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝑑 → (𝑤 = 〈𝑦, 𝑧〉 ↔ 𝑤 = 〈𝑑, 𝑧〉)) |
183 | | oveq2 7178 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 𝑑 → ((𝐴 ↑o 𝑋) ·o 𝑦) = ((𝐴 ↑o 𝑋) ·o 𝑑)) |
184 | 183 | oveq1d 7185 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 𝑑 → (((𝐴 ↑o 𝑋) ·o 𝑦) +o 𝑧) = (((𝐴 ↑o 𝑋) ·o 𝑑) +o 𝑧)) |
185 | 184 | eqeq1d 2740 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝑑 → ((((𝐴 ↑o 𝑋) ·o 𝑦) +o 𝑧) = 𝐵 ↔ (((𝐴 ↑o 𝑋) ·o 𝑑) +o 𝑧) = 𝐵)) |
186 | 182, 185 | anbi12d 634 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑑 → ((𝑤 = 〈𝑦, 𝑧〉 ∧ (((𝐴 ↑o 𝑋) ·o 𝑦) +o 𝑧) = 𝐵) ↔ (𝑤 = 〈𝑑, 𝑧〉 ∧ (((𝐴 ↑o 𝑋) ·o 𝑑) +o 𝑧) = 𝐵))) |
187 | | opeq2 4761 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑒 → 〈𝑑, 𝑧〉 = 〈𝑑, 𝑒〉) |
188 | 187 | eqeq2d 2749 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 𝑒 → (𝑤 = 〈𝑑, 𝑧〉 ↔ 𝑤 = 〈𝑑, 𝑒〉)) |
189 | | oveq2 7178 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑒 → (((𝐴 ↑o 𝑋) ·o 𝑑) +o 𝑧) = (((𝐴 ↑o 𝑋) ·o 𝑑) +o 𝑒)) |
190 | 189 | eqeq1d 2740 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 𝑒 → ((((𝐴 ↑o 𝑋) ·o 𝑑) +o 𝑧) = 𝐵 ↔ (((𝐴 ↑o 𝑋) ·o 𝑑) +o 𝑒) = 𝐵)) |
191 | 188, 190 | anbi12d 634 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑒 → ((𝑤 = 〈𝑑, 𝑧〉 ∧ (((𝐴 ↑o 𝑋) ·o 𝑑) +o 𝑧) = 𝐵) ↔ (𝑤 = 〈𝑑, 𝑒〉 ∧ (((𝐴 ↑o 𝑋) ·o 𝑑) +o 𝑒) = 𝐵))) |
192 | 186, 191 | cbvrex2vw 3363 |
. . . . . . . . . . 11
⊢
(∃𝑦 ∈ On
∃𝑧 ∈ (𝐴 ↑o 𝑋)(𝑤 = 〈𝑦, 𝑧〉 ∧ (((𝐴 ↑o 𝑋) ·o 𝑦) +o 𝑧) = 𝐵) ↔ ∃𝑑 ∈ On ∃𝑒 ∈ (𝐴 ↑o 𝑋)(𝑤 = 〈𝑑, 𝑒〉 ∧ (((𝐴 ↑o 𝑋) ·o 𝑑) +o 𝑒) = 𝐵)) |
193 | | eqeq1 2742 |
. . . . . . . . . . . . 13
⊢ (𝑤 = 𝑎 → (𝑤 = 〈𝑑, 𝑒〉 ↔ 𝑎 = 〈𝑑, 𝑒〉)) |
194 | 193 | anbi1d 633 |
. . . . . . . . . . . 12
⊢ (𝑤 = 𝑎 → ((𝑤 = 〈𝑑, 𝑒〉 ∧ (((𝐴 ↑o 𝑋) ·o 𝑑) +o 𝑒) = 𝐵) ↔ (𝑎 = 〈𝑑, 𝑒〉 ∧ (((𝐴 ↑o 𝑋) ·o 𝑑) +o 𝑒) = 𝐵))) |
195 | 194 | 2rexbidv 3210 |
. . . . . . . . . . 11
⊢ (𝑤 = 𝑎 → (∃𝑑 ∈ On ∃𝑒 ∈ (𝐴 ↑o 𝑋)(𝑤 = 〈𝑑, 𝑒〉 ∧ (((𝐴 ↑o 𝑋) ·o 𝑑) +o 𝑒) = 𝐵) ↔ ∃𝑑 ∈ On ∃𝑒 ∈ (𝐴 ↑o 𝑋)(𝑎 = 〈𝑑, 𝑒〉 ∧ (((𝐴 ↑o 𝑋) ·o 𝑑) +o 𝑒) = 𝐵))) |
196 | 192, 195 | syl5bb 286 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑎 → (∃𝑦 ∈ On ∃𝑧 ∈ (𝐴 ↑o 𝑋)(𝑤 = 〈𝑦, 𝑧〉 ∧ (((𝐴 ↑o 𝑋) ·o 𝑦) +o 𝑧) = 𝐵) ↔ ∃𝑑 ∈ On ∃𝑒 ∈ (𝐴 ↑o 𝑋)(𝑎 = 〈𝑑, 𝑒〉 ∧ (((𝐴 ↑o 𝑋) ·o 𝑑) +o 𝑒) = 𝐵))) |
197 | 196 | cbviotavw 6305 |
. . . . . . . . 9
⊢
(℩𝑤∃𝑦 ∈ On ∃𝑧 ∈ (𝐴 ↑o 𝑋)(𝑤 = 〈𝑦, 𝑧〉 ∧ (((𝐴 ↑o 𝑋) ·o 𝑦) +o 𝑧) = 𝐵)) = (℩𝑎∃𝑑 ∈ On ∃𝑒 ∈ (𝐴 ↑o 𝑋)(𝑎 = 〈𝑑, 𝑒〉 ∧ (((𝐴 ↑o 𝑋) ·o 𝑑) +o 𝑒) = 𝐵)) |
198 | 180, 197 | eqtri 2761 |
. . . . . . . 8
⊢ 𝑃 = (℩𝑎∃𝑑 ∈ On ∃𝑒 ∈ (𝐴 ↑o 𝑋)(𝑎 = 〈𝑑, 𝑒〉 ∧ (((𝐴 ↑o 𝑋) ·o 𝑑) +o 𝑒) = 𝐵)) |
199 | | oeeu.3 |
. . . . . . . 8
⊢ 𝑌 = (1st ‘𝑃) |
200 | | oeeu.4 |
. . . . . . . 8
⊢ 𝑍 = (2nd ‘𝑃) |
201 | | oveq2 7178 |
. . . . . . . . . 10
⊢ (𝑑 = 𝐷 → ((𝐴 ↑o 𝑋) ·o 𝑑) = ((𝐴 ↑o 𝑋) ·o 𝐷)) |
202 | 201 | oveq1d 7185 |
. . . . . . . . 9
⊢ (𝑑 = 𝐷 → (((𝐴 ↑o 𝑋) ·o 𝑑) +o 𝑒) = (((𝐴 ↑o 𝑋) ·o 𝐷) +o 𝑒)) |
203 | 202 | eqeq1d 2740 |
. . . . . . . 8
⊢ (𝑑 = 𝐷 → ((((𝐴 ↑o 𝑋) ·o 𝑑) +o 𝑒) = 𝐵 ↔ (((𝐴 ↑o 𝑋) ·o 𝐷) +o 𝑒) = 𝐵)) |
204 | | oveq2 7178 |
. . . . . . . . 9
⊢ (𝑒 = 𝐸 → (((𝐴 ↑o 𝑋) ·o 𝐷) +o 𝑒) = (((𝐴 ↑o 𝑋) ·o 𝐷) +o 𝐸)) |
205 | 204 | eqeq1d 2740 |
. . . . . . . 8
⊢ (𝑒 = 𝐸 → ((((𝐴 ↑o 𝑋) ·o 𝐷) +o 𝑒) = 𝐵 ↔ (((𝐴 ↑o 𝑋) ·o 𝐷) +o 𝐸) = 𝐵)) |
206 | 198, 199,
200, 203, 205 | opiota 7782 |
. . . . . . 7
⊢
(∃!𝑎∃𝑑 ∈ On ∃𝑒 ∈ (𝐴 ↑o 𝑋)(𝑎 = 〈𝑑, 𝑒〉 ∧ (((𝐴 ↑o 𝑋) ·o 𝑑) +o 𝑒) = 𝐵) → ((𝐷 ∈ On ∧ 𝐸 ∈ (𝐴 ↑o 𝑋) ∧ (((𝐴 ↑o 𝑋) ·o 𝐷) +o 𝐸) = 𝐵) ↔ (𝐷 = 𝑌 ∧ 𝐸 = 𝑍))) |
207 | 179, 206 | syl 17 |
. . . . . 6
⊢ (((𝐴 ↑o 𝑋) ∈ On ∧ 𝐵 ∈ On ∧ (𝐴 ↑o 𝑋) ≠ ∅) → ((𝐷 ∈ On ∧ 𝐸 ∈ (𝐴 ↑o 𝑋) ∧ (((𝐴 ↑o 𝑋) ·o 𝐷) +o 𝐸) = 𝐵) ↔ (𝐷 = 𝑌 ∧ 𝐸 = 𝑍))) |
208 | 175, 140,
178, 207 | syl3anc 1372 |
. . . . 5
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) → ((𝐷 ∈ On ∧ 𝐸 ∈ (𝐴 ↑o 𝑋) ∧ (((𝐴 ↑o 𝑋) ·o 𝐷) +o 𝐸) = 𝐵) ↔ (𝐷 = 𝑌 ∧ 𝐸 = 𝑍))) |
209 | 174, 208 | sylan9bbr 514 |
. . . 4
⊢ (((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) ∧ 𝐶 = 𝑋) → ((𝐷 ∈ On ∧ (𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ↔ (𝐷 = 𝑌 ∧ 𝐸 = 𝑍))) |
210 | 209 | pm5.32da 582 |
. . 3
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) → ((𝐶 = 𝑋 ∧ (𝐷 ∈ On ∧ (𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵))) ↔ (𝐶 = 𝑋 ∧ (𝐷 = 𝑌 ∧ 𝐸 = 𝑍)))) |
211 | 166, 210 | bitrd 282 |
. 2
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) → (((𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o)) ∧ (𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵)) ↔ (𝐶 = 𝑋 ∧ (𝐷 = 𝑌 ∧ 𝐸 = 𝑍)))) |
212 | | 3an4anass 1106 |
. 2
⊢ (((𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o) ∧ 𝐸 ∈ (𝐴 ↑o 𝐶)) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵) ↔ ((𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o)) ∧ (𝐸 ∈ (𝐴 ↑o 𝐶) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵))) |
213 | | 3anass 1096 |
. 2
⊢ ((𝐶 = 𝑋 ∧ 𝐷 = 𝑌 ∧ 𝐸 = 𝑍) ↔ (𝐶 = 𝑋 ∧ (𝐷 = 𝑌 ∧ 𝐸 = 𝑍))) |
214 | 211, 212,
213 | 3bitr4g 317 |
1
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) → (((𝐶 ∈ On ∧ 𝐷 ∈ (𝐴 ∖ 1o) ∧ 𝐸 ∈ (𝐴 ↑o 𝐶)) ∧ (((𝐴 ↑o 𝐶) ·o 𝐷) +o 𝐸) = 𝐵) ↔ (𝐶 = 𝑋 ∧ 𝐷 = 𝑌 ∧ 𝐸 = 𝑍))) |