| Step | Hyp | Ref
| Expression |
| 1 | | oveq1 7438 |
. . 3
⊢ (𝑎 = 𝑐 → (𝑎 +no suc 𝑏) = (𝑐 +no suc 𝑏)) |
| 2 | | oveq1 7438 |
. . . 4
⊢ (𝑎 = 𝑐 → (𝑎 +no 𝑏) = (𝑐 +no 𝑏)) |
| 3 | | suceq 6450 |
. . . 4
⊢ ((𝑎 +no 𝑏) = (𝑐 +no 𝑏) → suc (𝑎 +no 𝑏) = suc (𝑐 +no 𝑏)) |
| 4 | 2, 3 | syl 17 |
. . 3
⊢ (𝑎 = 𝑐 → suc (𝑎 +no 𝑏) = suc (𝑐 +no 𝑏)) |
| 5 | 1, 4 | eqeq12d 2753 |
. 2
⊢ (𝑎 = 𝑐 → ((𝑎 +no suc 𝑏) = suc (𝑎 +no 𝑏) ↔ (𝑐 +no suc 𝑏) = suc (𝑐 +no 𝑏))) |
| 6 | | suceq 6450 |
. . . 4
⊢ (𝑏 = 𝑑 → suc 𝑏 = suc 𝑑) |
| 7 | 6 | oveq2d 7447 |
. . 3
⊢ (𝑏 = 𝑑 → (𝑐 +no suc 𝑏) = (𝑐 +no suc 𝑑)) |
| 8 | | oveq2 7439 |
. . . 4
⊢ (𝑏 = 𝑑 → (𝑐 +no 𝑏) = (𝑐 +no 𝑑)) |
| 9 | | suceq 6450 |
. . . 4
⊢ ((𝑐 +no 𝑏) = (𝑐 +no 𝑑) → suc (𝑐 +no 𝑏) = suc (𝑐 +no 𝑑)) |
| 10 | 8, 9 | syl 17 |
. . 3
⊢ (𝑏 = 𝑑 → suc (𝑐 +no 𝑏) = suc (𝑐 +no 𝑑)) |
| 11 | 7, 10 | eqeq12d 2753 |
. 2
⊢ (𝑏 = 𝑑 → ((𝑐 +no suc 𝑏) = suc (𝑐 +no 𝑏) ↔ (𝑐 +no suc 𝑑) = suc (𝑐 +no 𝑑))) |
| 12 | | oveq1 7438 |
. . 3
⊢ (𝑎 = 𝑐 → (𝑎 +no suc 𝑑) = (𝑐 +no suc 𝑑)) |
| 13 | | oveq1 7438 |
. . . 4
⊢ (𝑎 = 𝑐 → (𝑎 +no 𝑑) = (𝑐 +no 𝑑)) |
| 14 | | suceq 6450 |
. . . 4
⊢ ((𝑎 +no 𝑑) = (𝑐 +no 𝑑) → suc (𝑎 +no 𝑑) = suc (𝑐 +no 𝑑)) |
| 15 | 13, 14 | syl 17 |
. . 3
⊢ (𝑎 = 𝑐 → suc (𝑎 +no 𝑑) = suc (𝑐 +no 𝑑)) |
| 16 | 12, 15 | eqeq12d 2753 |
. 2
⊢ (𝑎 = 𝑐 → ((𝑎 +no suc 𝑑) = suc (𝑎 +no 𝑑) ↔ (𝑐 +no suc 𝑑) = suc (𝑐 +no 𝑑))) |
| 17 | | oveq1 7438 |
. . 3
⊢ (𝑎 = 𝐴 → (𝑎 +no suc 𝑏) = (𝐴 +no suc 𝑏)) |
| 18 | | oveq1 7438 |
. . . 4
⊢ (𝑎 = 𝐴 → (𝑎 +no 𝑏) = (𝐴 +no 𝑏)) |
| 19 | | suceq 6450 |
. . . 4
⊢ ((𝑎 +no 𝑏) = (𝐴 +no 𝑏) → suc (𝑎 +no 𝑏) = suc (𝐴 +no 𝑏)) |
| 20 | 18, 19 | syl 17 |
. . 3
⊢ (𝑎 = 𝐴 → suc (𝑎 +no 𝑏) = suc (𝐴 +no 𝑏)) |
| 21 | 17, 20 | eqeq12d 2753 |
. 2
⊢ (𝑎 = 𝐴 → ((𝑎 +no suc 𝑏) = suc (𝑎 +no 𝑏) ↔ (𝐴 +no suc 𝑏) = suc (𝐴 +no 𝑏))) |
| 22 | | suceq 6450 |
. . . 4
⊢ (𝑏 = 𝐵 → suc 𝑏 = suc 𝐵) |
| 23 | 22 | oveq2d 7447 |
. . 3
⊢ (𝑏 = 𝐵 → (𝐴 +no suc 𝑏) = (𝐴 +no suc 𝐵)) |
| 24 | | oveq2 7439 |
. . . 4
⊢ (𝑏 = 𝐵 → (𝐴 +no 𝑏) = (𝐴 +no 𝐵)) |
| 25 | | suceq 6450 |
. . . 4
⊢ ((𝐴 +no 𝑏) = (𝐴 +no 𝐵) → suc (𝐴 +no 𝑏) = suc (𝐴 +no 𝐵)) |
| 26 | 24, 25 | syl 17 |
. . 3
⊢ (𝑏 = 𝐵 → suc (𝐴 +no 𝑏) = suc (𝐴 +no 𝐵)) |
| 27 | 23, 26 | eqeq12d 2753 |
. 2
⊢ (𝑏 = 𝐵 → ((𝐴 +no suc 𝑏) = suc (𝐴 +no 𝑏) ↔ (𝐴 +no suc 𝐵) = suc (𝐴 +no 𝐵))) |
| 28 | | simp2 1138 |
. . . 4
⊢
((∀𝑐 ∈
𝑎 ∀𝑑 ∈ 𝑏 (𝑐 +no suc 𝑑) = suc (𝑐 +no 𝑑) ∧ ∀𝑐 ∈ 𝑎 (𝑐 +no suc 𝑏) = suc (𝑐 +no 𝑏) ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no suc 𝑑) = suc (𝑎 +no 𝑑)) → ∀𝑐 ∈ 𝑎 (𝑐 +no suc 𝑏) = suc (𝑐 +no 𝑏)) |
| 29 | 28 | a1i 11 |
. . 3
⊢ ((𝑎 ∈ On ∧ 𝑏 ∈ On) →
((∀𝑐 ∈ 𝑎 ∀𝑑 ∈ 𝑏 (𝑐 +no suc 𝑑) = suc (𝑐 +no 𝑑) ∧ ∀𝑐 ∈ 𝑎 (𝑐 +no suc 𝑏) = suc (𝑐 +no 𝑏) ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no suc 𝑑) = suc (𝑎 +no 𝑑)) → ∀𝑐 ∈ 𝑎 (𝑐 +no suc 𝑏) = suc (𝑐 +no 𝑏))) |
| 30 | | df-suc 6390 |
. . . . . . . . . . . 12
⊢ suc 𝑏 = (𝑏 ∪ {𝑏}) |
| 31 | 30 | a1i 11 |
. . . . . . . . . . 11
⊢ ((((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ ∀𝑐 ∈ 𝑎 (𝑐 +no suc 𝑏) = suc (𝑐 +no 𝑏)) ∧ 𝑥 ∈ On) → suc 𝑏 = (𝑏 ∪ {𝑏})) |
| 32 | 31 | raleqdv 3326 |
. . . . . . . . . 10
⊢ ((((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ ∀𝑐 ∈ 𝑎 (𝑐 +no suc 𝑏) = suc (𝑐 +no 𝑏)) ∧ 𝑥 ∈ On) → (∀𝑑 ∈ suc 𝑏(𝑎 +no 𝑑) ∈ 𝑥 ↔ ∀𝑑 ∈ (𝑏 ∪ {𝑏})(𝑎 +no 𝑑) ∈ 𝑥)) |
| 33 | | vex 3484 |
. . . . . . . . . . . . 13
⊢ 𝑏 ∈ V |
| 34 | 33 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ ∀𝑐 ∈ 𝑎 (𝑐 +no suc 𝑏) = suc (𝑐 +no 𝑏)) ∧ 𝑥 ∈ On) → 𝑏 ∈ V) |
| 35 | | oveq2 7439 |
. . . . . . . . . . . . . 14
⊢ (𝑑 = 𝑏 → (𝑎 +no 𝑑) = (𝑎 +no 𝑏)) |
| 36 | 35 | eleq1d 2826 |
. . . . . . . . . . . . 13
⊢ (𝑑 = 𝑏 → ((𝑎 +no 𝑑) ∈ 𝑥 ↔ (𝑎 +no 𝑏) ∈ 𝑥)) |
| 37 | 36 | ralunsn 4894 |
. . . . . . . . . . . 12
⊢ (𝑏 ∈ V → (∀𝑑 ∈ (𝑏 ∪ {𝑏})(𝑎 +no 𝑑) ∈ 𝑥 ↔ (∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ 𝑥 ∧ (𝑎 +no 𝑏) ∈ 𝑥))) |
| 38 | 34, 37 | syl 17 |
. . . . . . . . . . 11
⊢ ((((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ ∀𝑐 ∈ 𝑎 (𝑐 +no suc 𝑏) = suc (𝑐 +no 𝑏)) ∧ 𝑥 ∈ On) → (∀𝑑 ∈ (𝑏 ∪ {𝑏})(𝑎 +no 𝑑) ∈ 𝑥 ↔ (∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ 𝑥 ∧ (𝑎 +no 𝑏) ∈ 𝑥))) |
| 39 | 38 | biancomd 463 |
. . . . . . . . . 10
⊢ ((((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ ∀𝑐 ∈ 𝑎 (𝑐 +no suc 𝑏) = suc (𝑐 +no 𝑏)) ∧ 𝑥 ∈ On) → (∀𝑑 ∈ (𝑏 ∪ {𝑏})(𝑎 +no 𝑑) ∈ 𝑥 ↔ ((𝑎 +no 𝑏) ∈ 𝑥 ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ 𝑥))) |
| 40 | 32, 39 | bitrd 279 |
. . . . . . . . 9
⊢ ((((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ ∀𝑐 ∈ 𝑎 (𝑐 +no suc 𝑏) = suc (𝑐 +no 𝑏)) ∧ 𝑥 ∈ On) → (∀𝑑 ∈ suc 𝑏(𝑎 +no 𝑑) ∈ 𝑥 ↔ ((𝑎 +no 𝑏) ∈ 𝑥 ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ 𝑥))) |
| 41 | | nfv 1914 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑐(𝑎 ∈ On ∧ 𝑏 ∈ On) |
| 42 | | nfra1 3284 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑐∀𝑐 ∈ 𝑎 (𝑐 +no suc 𝑏) = suc (𝑐 +no 𝑏) |
| 43 | 41, 42 | nfan 1899 |
. . . . . . . . . . 11
⊢
Ⅎ𝑐((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ ∀𝑐 ∈ 𝑎 (𝑐 +no suc 𝑏) = suc (𝑐 +no 𝑏)) |
| 44 | | nfv 1914 |
. . . . . . . . . . 11
⊢
Ⅎ𝑐 𝑥 ∈ On |
| 45 | 43, 44 | nfan 1899 |
. . . . . . . . . 10
⊢
Ⅎ𝑐(((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ ∀𝑐 ∈ 𝑎 (𝑐 +no suc 𝑏) = suc (𝑐 +no 𝑏)) ∧ 𝑥 ∈ On) |
| 46 | | simplr 769 |
. . . . . . . . . . . 12
⊢ ((((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ ∀𝑐 ∈ 𝑎 (𝑐 +no suc 𝑏) = suc (𝑐 +no 𝑏)) ∧ 𝑥 ∈ On) → ∀𝑐 ∈ 𝑎 (𝑐 +no suc 𝑏) = suc (𝑐 +no 𝑏)) |
| 47 | 46 | r19.21bi 3251 |
. . . . . . . . . . 11
⊢
(((((𝑎 ∈ On
∧ 𝑏 ∈ On) ∧
∀𝑐 ∈ 𝑎 (𝑐 +no suc 𝑏) = suc (𝑐 +no 𝑏)) ∧ 𝑥 ∈ On) ∧ 𝑐 ∈ 𝑎) → (𝑐 +no suc 𝑏) = suc (𝑐 +no 𝑏)) |
| 48 | 47 | eleq1d 2826 |
. . . . . . . . . 10
⊢
(((((𝑎 ∈ On
∧ 𝑏 ∈ On) ∧
∀𝑐 ∈ 𝑎 (𝑐 +no suc 𝑏) = suc (𝑐 +no 𝑏)) ∧ 𝑥 ∈ On) ∧ 𝑐 ∈ 𝑎) → ((𝑐 +no suc 𝑏) ∈ 𝑥 ↔ suc (𝑐 +no 𝑏) ∈ 𝑥)) |
| 49 | 45, 48 | ralbida 3270 |
. . . . . . . . 9
⊢ ((((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ ∀𝑐 ∈ 𝑎 (𝑐 +no suc 𝑏) = suc (𝑐 +no 𝑏)) ∧ 𝑥 ∈ On) → (∀𝑐 ∈ 𝑎 (𝑐 +no suc 𝑏) ∈ 𝑥 ↔ ∀𝑐 ∈ 𝑎 suc (𝑐 +no 𝑏) ∈ 𝑥)) |
| 50 | 40, 49 | anbi12d 632 |
. . . . . . . 8
⊢ ((((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ ∀𝑐 ∈ 𝑎 (𝑐 +no suc 𝑏) = suc (𝑐 +no 𝑏)) ∧ 𝑥 ∈ On) → ((∀𝑑 ∈ suc 𝑏(𝑎 +no 𝑑) ∈ 𝑥 ∧ ∀𝑐 ∈ 𝑎 (𝑐 +no suc 𝑏) ∈ 𝑥) ↔ (((𝑎 +no 𝑏) ∈ 𝑥 ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ 𝑥) ∧ ∀𝑐 ∈ 𝑎 suc (𝑐 +no 𝑏) ∈ 𝑥))) |
| 51 | | anass 468 |
. . . . . . . . 9
⊢ ((((𝑎 +no 𝑏) ∈ 𝑥 ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ 𝑥) ∧ ∀𝑐 ∈ 𝑎 suc (𝑐 +no 𝑏) ∈ 𝑥) ↔ ((𝑎 +no 𝑏) ∈ 𝑥 ∧ (∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ 𝑥 ∧ ∀𝑐 ∈ 𝑎 suc (𝑐 +no 𝑏) ∈ 𝑥))) |
| 52 | | simpll3 1215 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑥 ∈ On) ∧ (𝑎 +no 𝑏) ∈ 𝑥) ∧ 𝑑 ∈ 𝑏) → 𝑥 ∈ On) |
| 53 | | simpr 484 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑥 ∈ On) ∧ (𝑎 +no 𝑏) ∈ 𝑥) ∧ 𝑑 ∈ 𝑏) → 𝑑 ∈ 𝑏) |
| 54 | | simpll2 1214 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑥 ∈ On) ∧ (𝑎 +no 𝑏) ∈ 𝑥) ∧ 𝑑 ∈ 𝑏) → 𝑏 ∈ On) |
| 55 | | onelon 6409 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑏 ∈ On ∧ 𝑑 ∈ 𝑏) → 𝑑 ∈ On) |
| 56 | 54, 53, 55 | syl2anc 584 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑥 ∈ On) ∧ (𝑎 +no 𝑏) ∈ 𝑥) ∧ 𝑑 ∈ 𝑏) → 𝑑 ∈ On) |
| 57 | | simpll1 1213 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑥 ∈ On) ∧ (𝑎 +no 𝑏) ∈ 𝑥) ∧ 𝑑 ∈ 𝑏) → 𝑎 ∈ On) |
| 58 | | naddel2 8726 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑑 ∈ On ∧ 𝑏 ∈ On ∧ 𝑎 ∈ On) → (𝑑 ∈ 𝑏 ↔ (𝑎 +no 𝑑) ∈ (𝑎 +no 𝑏))) |
| 59 | 56, 54, 57, 58 | syl3anc 1373 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑥 ∈ On) ∧ (𝑎 +no 𝑏) ∈ 𝑥) ∧ 𝑑 ∈ 𝑏) → (𝑑 ∈ 𝑏 ↔ (𝑎 +no 𝑑) ∈ (𝑎 +no 𝑏))) |
| 60 | 53, 59 | mpbid 232 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑥 ∈ On) ∧ (𝑎 +no 𝑏) ∈ 𝑥) ∧ 𝑑 ∈ 𝑏) → (𝑎 +no 𝑑) ∈ (𝑎 +no 𝑏)) |
| 61 | | simplr 769 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑥 ∈ On) ∧ (𝑎 +no 𝑏) ∈ 𝑥) ∧ 𝑑 ∈ 𝑏) → (𝑎 +no 𝑏) ∈ 𝑥) |
| 62 | 60, 61 | jca 511 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑥 ∈ On) ∧ (𝑎 +no 𝑏) ∈ 𝑥) ∧ 𝑑 ∈ 𝑏) → ((𝑎 +no 𝑑) ∈ (𝑎 +no 𝑏) ∧ (𝑎 +no 𝑏) ∈ 𝑥)) |
| 63 | | ontr1 6430 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ On → (((𝑎 +no 𝑑) ∈ (𝑎 +no 𝑏) ∧ (𝑎 +no 𝑏) ∈ 𝑥) → (𝑎 +no 𝑑) ∈ 𝑥)) |
| 64 | 52, 62, 63 | sylc 65 |
. . . . . . . . . . . . . 14
⊢ ((((𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑥 ∈ On) ∧ (𝑎 +no 𝑏) ∈ 𝑥) ∧ 𝑑 ∈ 𝑏) → (𝑎 +no 𝑑) ∈ 𝑥) |
| 65 | 64 | ralrimiva 3146 |
. . . . . . . . . . . . 13
⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑥 ∈ On) ∧ (𝑎 +no 𝑏) ∈ 𝑥) → ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ 𝑥) |
| 66 | | simpll1 1213 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑥 ∈ On) ∧ (𝑎 +no 𝑏) ∈ 𝑥) ∧ 𝑐 ∈ 𝑎) → 𝑎 ∈ On) |
| 67 | | simpr 484 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑥 ∈ On) ∧ (𝑎 +no 𝑏) ∈ 𝑥) ∧ 𝑐 ∈ 𝑎) → 𝑐 ∈ 𝑎) |
| 68 | | onelon 6409 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑎 ∈ On ∧ 𝑐 ∈ 𝑎) → 𝑐 ∈ On) |
| 69 | 66, 67, 68 | syl2anc 584 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑥 ∈ On) ∧ (𝑎 +no 𝑏) ∈ 𝑥) ∧ 𝑐 ∈ 𝑎) → 𝑐 ∈ On) |
| 70 | | simpll2 1214 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑥 ∈ On) ∧ (𝑎 +no 𝑏) ∈ 𝑥) ∧ 𝑐 ∈ 𝑎) → 𝑏 ∈ On) |
| 71 | 69, 66, 70 | 3jca 1129 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑥 ∈ On) ∧ (𝑎 +no 𝑏) ∈ 𝑥) ∧ 𝑐 ∈ 𝑎) → (𝑐 ∈ On ∧ 𝑎 ∈ On ∧ 𝑏 ∈ On)) |
| 72 | | naddelim 8724 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑐 ∈ On ∧ 𝑎 ∈ On ∧ 𝑏 ∈ On) → (𝑐 ∈ 𝑎 → (𝑐 +no 𝑏) ∈ (𝑎 +no 𝑏))) |
| 73 | 71, 67, 72 | sylc 65 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑥 ∈ On) ∧ (𝑎 +no 𝑏) ∈ 𝑥) ∧ 𝑐 ∈ 𝑎) → (𝑐 +no 𝑏) ∈ (𝑎 +no 𝑏)) |
| 74 | | simplr 769 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑥 ∈ On) ∧ (𝑎 +no 𝑏) ∈ 𝑥) ∧ 𝑐 ∈ 𝑎) → (𝑎 +no 𝑏) ∈ 𝑥) |
| 75 | | elunii 4912 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑐 +no 𝑏) ∈ (𝑎 +no 𝑏) ∧ (𝑎 +no 𝑏) ∈ 𝑥) → (𝑐 +no 𝑏) ∈ ∪ 𝑥) |
| 76 | 73, 74, 75 | syl2anc 584 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑥 ∈ On) ∧ (𝑎 +no 𝑏) ∈ 𝑥) ∧ 𝑐 ∈ 𝑎) → (𝑐 +no 𝑏) ∈ ∪ 𝑥) |
| 77 | | simpll3 1215 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑥 ∈ On) ∧ (𝑎 +no 𝑏) ∈ 𝑥) ∧ 𝑐 ∈ 𝑎) → 𝑥 ∈ On) |
| 78 | | eloni 6394 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ On → Ord 𝑥) |
| 79 | 77, 78 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑥 ∈ On) ∧ (𝑎 +no 𝑏) ∈ 𝑥) ∧ 𝑐 ∈ 𝑎) → Ord 𝑥) |
| 80 | | ordsucuniel 7844 |
. . . . . . . . . . . . . . . 16
⊢ (Ord
𝑥 → ((𝑐 +no 𝑏) ∈ ∪ 𝑥 ↔ suc (𝑐 +no 𝑏) ∈ 𝑥)) |
| 81 | 79, 80 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑥 ∈ On) ∧ (𝑎 +no 𝑏) ∈ 𝑥) ∧ 𝑐 ∈ 𝑎) → ((𝑐 +no 𝑏) ∈ ∪ 𝑥 ↔ suc (𝑐 +no 𝑏) ∈ 𝑥)) |
| 82 | 76, 81 | mpbid 232 |
. . . . . . . . . . . . . 14
⊢ ((((𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑥 ∈ On) ∧ (𝑎 +no 𝑏) ∈ 𝑥) ∧ 𝑐 ∈ 𝑎) → suc (𝑐 +no 𝑏) ∈ 𝑥) |
| 83 | 82 | ralrimiva 3146 |
. . . . . . . . . . . . 13
⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑥 ∈ On) ∧ (𝑎 +no 𝑏) ∈ 𝑥) → ∀𝑐 ∈ 𝑎 suc (𝑐 +no 𝑏) ∈ 𝑥) |
| 84 | 65, 83 | jca 511 |
. . . . . . . . . . . 12
⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑥 ∈ On) ∧ (𝑎 +no 𝑏) ∈ 𝑥) → (∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ 𝑥 ∧ ∀𝑐 ∈ 𝑎 suc (𝑐 +no 𝑏) ∈ 𝑥)) |
| 85 | 84 | ex 412 |
. . . . . . . . . . 11
⊢ ((𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑥 ∈ On) → ((𝑎 +no 𝑏) ∈ 𝑥 → (∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ 𝑥 ∧ ∀𝑐 ∈ 𝑎 suc (𝑐 +no 𝑏) ∈ 𝑥))) |
| 86 | 85 | ad4ant124 1174 |
. . . . . . . . . 10
⊢ ((((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ ∀𝑐 ∈ 𝑎 (𝑐 +no suc 𝑏) = suc (𝑐 +no 𝑏)) ∧ 𝑥 ∈ On) → ((𝑎 +no 𝑏) ∈ 𝑥 → (∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ 𝑥 ∧ ∀𝑐 ∈ 𝑎 suc (𝑐 +no 𝑏) ∈ 𝑥))) |
| 87 | 86 | pm4.71d 561 |
. . . . . . . . 9
⊢ ((((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ ∀𝑐 ∈ 𝑎 (𝑐 +no suc 𝑏) = suc (𝑐 +no 𝑏)) ∧ 𝑥 ∈ On) → ((𝑎 +no 𝑏) ∈ 𝑥 ↔ ((𝑎 +no 𝑏) ∈ 𝑥 ∧ (∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ 𝑥 ∧ ∀𝑐 ∈ 𝑎 suc (𝑐 +no 𝑏) ∈ 𝑥)))) |
| 88 | 51, 87 | bitr4id 290 |
. . . . . . . 8
⊢ ((((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ ∀𝑐 ∈ 𝑎 (𝑐 +no suc 𝑏) = suc (𝑐 +no 𝑏)) ∧ 𝑥 ∈ On) → ((((𝑎 +no 𝑏) ∈ 𝑥 ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ 𝑥) ∧ ∀𝑐 ∈ 𝑎 suc (𝑐 +no 𝑏) ∈ 𝑥) ↔ (𝑎 +no 𝑏) ∈ 𝑥)) |
| 89 | 50, 88 | bitrd 279 |
. . . . . . 7
⊢ ((((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ ∀𝑐 ∈ 𝑎 (𝑐 +no suc 𝑏) = suc (𝑐 +no 𝑏)) ∧ 𝑥 ∈ On) → ((∀𝑑 ∈ suc 𝑏(𝑎 +no 𝑑) ∈ 𝑥 ∧ ∀𝑐 ∈ 𝑎 (𝑐 +no suc 𝑏) ∈ 𝑥) ↔ (𝑎 +no 𝑏) ∈ 𝑥)) |
| 90 | 89 | rabbidva 3443 |
. . . . . 6
⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ ∀𝑐 ∈ 𝑎 (𝑐 +no suc 𝑏) = suc (𝑐 +no 𝑏)) → {𝑥 ∈ On ∣ (∀𝑑 ∈ suc 𝑏(𝑎 +no 𝑑) ∈ 𝑥 ∧ ∀𝑐 ∈ 𝑎 (𝑐 +no suc 𝑏) ∈ 𝑥)} = {𝑥 ∈ On ∣ (𝑎 +no 𝑏) ∈ 𝑥}) |
| 91 | 90 | inteqd 4951 |
. . . . 5
⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ ∀𝑐 ∈ 𝑎 (𝑐 +no suc 𝑏) = suc (𝑐 +no 𝑏)) → ∩ {𝑥 ∈ On ∣
(∀𝑑 ∈ suc 𝑏(𝑎 +no 𝑑) ∈ 𝑥 ∧ ∀𝑐 ∈ 𝑎 (𝑐 +no suc 𝑏) ∈ 𝑥)} = ∩ {𝑥 ∈ On ∣ (𝑎 +no 𝑏) ∈ 𝑥}) |
| 92 | | onsuc 7831 |
. . . . . . 7
⊢ (𝑏 ∈ On → suc 𝑏 ∈ On) |
| 93 | | naddov2 8717 |
. . . . . . 7
⊢ ((𝑎 ∈ On ∧ suc 𝑏 ∈ On) → (𝑎 +no suc 𝑏) = ∩ {𝑥 ∈ On ∣
(∀𝑑 ∈ suc 𝑏(𝑎 +no 𝑑) ∈ 𝑥 ∧ ∀𝑐 ∈ 𝑎 (𝑐 +no suc 𝑏) ∈ 𝑥)}) |
| 94 | 92, 93 | sylan2 593 |
. . . . . 6
⊢ ((𝑎 ∈ On ∧ 𝑏 ∈ On) → (𝑎 +no suc 𝑏) = ∩ {𝑥 ∈ On ∣
(∀𝑑 ∈ suc 𝑏(𝑎 +no 𝑑) ∈ 𝑥 ∧ ∀𝑐 ∈ 𝑎 (𝑐 +no suc 𝑏) ∈ 𝑥)}) |
| 95 | 94 | adantr 480 |
. . . . 5
⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ ∀𝑐 ∈ 𝑎 (𝑐 +no suc 𝑏) = suc (𝑐 +no 𝑏)) → (𝑎 +no suc 𝑏) = ∩ {𝑥 ∈ On ∣
(∀𝑑 ∈ suc 𝑏(𝑎 +no 𝑑) ∈ 𝑥 ∧ ∀𝑐 ∈ 𝑎 (𝑐 +no suc 𝑏) ∈ 𝑥)}) |
| 96 | | naddcl 8715 |
. . . . . . 7
⊢ ((𝑎 ∈ On ∧ 𝑏 ∈ On) → (𝑎 +no 𝑏) ∈ On) |
| 97 | | onsucmin 7841 |
. . . . . . 7
⊢ ((𝑎 +no 𝑏) ∈ On → suc (𝑎 +no 𝑏) = ∩ {𝑥 ∈ On ∣ (𝑎 +no 𝑏) ∈ 𝑥}) |
| 98 | 96, 97 | syl 17 |
. . . . . 6
⊢ ((𝑎 ∈ On ∧ 𝑏 ∈ On) → suc (𝑎 +no 𝑏) = ∩ {𝑥 ∈ On ∣ (𝑎 +no 𝑏) ∈ 𝑥}) |
| 99 | 98 | adantr 480 |
. . . . 5
⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ ∀𝑐 ∈ 𝑎 (𝑐 +no suc 𝑏) = suc (𝑐 +no 𝑏)) → suc (𝑎 +no 𝑏) = ∩ {𝑥 ∈ On ∣ (𝑎 +no 𝑏) ∈ 𝑥}) |
| 100 | 91, 95, 99 | 3eqtr4d 2787 |
. . . 4
⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ ∀𝑐 ∈ 𝑎 (𝑐 +no suc 𝑏) = suc (𝑐 +no 𝑏)) → (𝑎 +no suc 𝑏) = suc (𝑎 +no 𝑏)) |
| 101 | 100 | ex 412 |
. . 3
⊢ ((𝑎 ∈ On ∧ 𝑏 ∈ On) →
(∀𝑐 ∈ 𝑎 (𝑐 +no suc 𝑏) = suc (𝑐 +no 𝑏) → (𝑎 +no suc 𝑏) = suc (𝑎 +no 𝑏))) |
| 102 | 29, 101 | syld 47 |
. 2
⊢ ((𝑎 ∈ On ∧ 𝑏 ∈ On) →
((∀𝑐 ∈ 𝑎 ∀𝑑 ∈ 𝑏 (𝑐 +no suc 𝑑) = suc (𝑐 +no 𝑑) ∧ ∀𝑐 ∈ 𝑎 (𝑐 +no suc 𝑏) = suc (𝑐 +no 𝑏) ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no suc 𝑑) = suc (𝑎 +no 𝑑)) → (𝑎 +no suc 𝑏) = suc (𝑎 +no 𝑏))) |
| 103 | 5, 11, 16, 21, 27, 102 | on2ind 8707 |
1
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 +no suc 𝐵) = suc (𝐴 +no 𝐵)) |