| Step | Hyp | Ref
| Expression |
| 1 | | oveq1 7438 |
. . 3
⊢ (𝑎 = 𝑏 → (𝑎 +no 1o) = (𝑏 +no 1o)) |
| 2 | | suceq 6450 |
. . 3
⊢ (𝑎 = 𝑏 → suc 𝑎 = suc 𝑏) |
| 3 | 1, 2 | eqeq12d 2753 |
. 2
⊢ (𝑎 = 𝑏 → ((𝑎 +no 1o) = suc 𝑎 ↔ (𝑏 +no 1o) = suc 𝑏)) |
| 4 | | oveq1 7438 |
. . 3
⊢ (𝑎 = 𝐴 → (𝑎 +no 1o) = (𝐴 +no 1o)) |
| 5 | | suceq 6450 |
. . 3
⊢ (𝑎 = 𝐴 → suc 𝑎 = suc 𝐴) |
| 6 | 4, 5 | eqeq12d 2753 |
. 2
⊢ (𝑎 = 𝐴 → ((𝑎 +no 1o) = suc 𝑎 ↔ (𝐴 +no 1o) = suc 𝐴)) |
| 7 | | naddrid 8721 |
. . . . . . . . . 10
⊢ (𝑎 ∈ On → (𝑎 +no ∅) = 𝑎) |
| 8 | 7 | eleq1d 2826 |
. . . . . . . . 9
⊢ (𝑎 ∈ On → ((𝑎 +no ∅) ∈ 𝑥 ↔ 𝑎 ∈ 𝑥)) |
| 9 | 8 | anbi1d 631 |
. . . . . . . 8
⊢ (𝑎 ∈ On → (((𝑎 +no ∅) ∈ 𝑥 ∧ ∀𝑏 ∈ 𝑎 suc 𝑏 ∈ 𝑥) ↔ (𝑎 ∈ 𝑥 ∧ ∀𝑏 ∈ 𝑎 suc 𝑏 ∈ 𝑥))) |
| 10 | 9 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝑎 ∈ On ∧ ∀𝑏 ∈ 𝑎 (𝑏 +no 1o) = suc 𝑏) ∧ 𝑥 ∈ On) → (((𝑎 +no ∅) ∈ 𝑥 ∧ ∀𝑏 ∈ 𝑎 suc 𝑏 ∈ 𝑥) ↔ (𝑎 ∈ 𝑥 ∧ ∀𝑏 ∈ 𝑎 suc 𝑏 ∈ 𝑥))) |
| 11 | | df1o2 8513 |
. . . . . . . . . . . 12
⊢
1o = {∅} |
| 12 | 11 | raleqi 3324 |
. . . . . . . . . . 11
⊢
(∀𝑦 ∈
1o (𝑎 +no 𝑦) ∈ 𝑥 ↔ ∀𝑦 ∈ {∅} (𝑎 +no 𝑦) ∈ 𝑥) |
| 13 | | 0ex 5307 |
. . . . . . . . . . . 12
⊢ ∅
∈ V |
| 14 | | oveq2 7439 |
. . . . . . . . . . . . 13
⊢ (𝑦 = ∅ → (𝑎 +no 𝑦) = (𝑎 +no ∅)) |
| 15 | 14 | eleq1d 2826 |
. . . . . . . . . . . 12
⊢ (𝑦 = ∅ → ((𝑎 +no 𝑦) ∈ 𝑥 ↔ (𝑎 +no ∅) ∈ 𝑥)) |
| 16 | 13, 15 | ralsn 4681 |
. . . . . . . . . . 11
⊢
(∀𝑦 ∈
{∅} (𝑎 +no 𝑦) ∈ 𝑥 ↔ (𝑎 +no ∅) ∈ 𝑥) |
| 17 | 12, 16 | bitri 275 |
. . . . . . . . . 10
⊢
(∀𝑦 ∈
1o (𝑎 +no 𝑦) ∈ 𝑥 ↔ (𝑎 +no ∅) ∈ 𝑥) |
| 18 | 17 | a1i 11 |
. . . . . . . . 9
⊢ ((𝑎 ∈ On ∧ ∀𝑏 ∈ 𝑎 (𝑏 +no 1o) = suc 𝑏) → (∀𝑦 ∈ 1o (𝑎 +no 𝑦) ∈ 𝑥 ↔ (𝑎 +no ∅) ∈ 𝑥)) |
| 19 | | oveq1 7438 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑏 → (𝑦 +no 1o) = (𝑏 +no 1o)) |
| 20 | 19 | eleq1d 2826 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑏 → ((𝑦 +no 1o) ∈ 𝑥 ↔ (𝑏 +no 1o) ∈ 𝑥)) |
| 21 | 20 | cbvralvw 3237 |
. . . . . . . . . 10
⊢
(∀𝑦 ∈
𝑎 (𝑦 +no 1o) ∈ 𝑥 ↔ ∀𝑏 ∈ 𝑎 (𝑏 +no 1o) ∈ 𝑥) |
| 22 | | nfv 1914 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑏 𝑎 ∈ On |
| 23 | | nfra1 3284 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑏∀𝑏 ∈ 𝑎 (𝑏 +no 1o) = suc 𝑏 |
| 24 | 22, 23 | nfan 1899 |
. . . . . . . . . . 11
⊢
Ⅎ𝑏(𝑎 ∈ On ∧ ∀𝑏 ∈ 𝑎 (𝑏 +no 1o) = suc 𝑏) |
| 25 | | simpr 484 |
. . . . . . . . . . . . 13
⊢ ((𝑎 ∈ On ∧ ∀𝑏 ∈ 𝑎 (𝑏 +no 1o) = suc 𝑏) → ∀𝑏 ∈ 𝑎 (𝑏 +no 1o) = suc 𝑏) |
| 26 | 25 | r19.21bi 3251 |
. . . . . . . . . . . 12
⊢ (((𝑎 ∈ On ∧ ∀𝑏 ∈ 𝑎 (𝑏 +no 1o) = suc 𝑏) ∧ 𝑏 ∈ 𝑎) → (𝑏 +no 1o) = suc 𝑏) |
| 27 | 26 | eleq1d 2826 |
. . . . . . . . . . 11
⊢ (((𝑎 ∈ On ∧ ∀𝑏 ∈ 𝑎 (𝑏 +no 1o) = suc 𝑏) ∧ 𝑏 ∈ 𝑎) → ((𝑏 +no 1o) ∈ 𝑥 ↔ suc 𝑏 ∈ 𝑥)) |
| 28 | 24, 27 | ralbida 3270 |
. . . . . . . . . 10
⊢ ((𝑎 ∈ On ∧ ∀𝑏 ∈ 𝑎 (𝑏 +no 1o) = suc 𝑏) → (∀𝑏 ∈ 𝑎 (𝑏 +no 1o) ∈ 𝑥 ↔ ∀𝑏 ∈ 𝑎 suc 𝑏 ∈ 𝑥)) |
| 29 | 21, 28 | bitrid 283 |
. . . . . . . . 9
⊢ ((𝑎 ∈ On ∧ ∀𝑏 ∈ 𝑎 (𝑏 +no 1o) = suc 𝑏) → (∀𝑦 ∈ 𝑎 (𝑦 +no 1o) ∈ 𝑥 ↔ ∀𝑏 ∈ 𝑎 suc 𝑏 ∈ 𝑥)) |
| 30 | 18, 29 | anbi12d 632 |
. . . . . . . 8
⊢ ((𝑎 ∈ On ∧ ∀𝑏 ∈ 𝑎 (𝑏 +no 1o) = suc 𝑏) → ((∀𝑦 ∈ 1o (𝑎 +no 𝑦) ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑎 (𝑦 +no 1o) ∈ 𝑥) ↔ ((𝑎 +no ∅) ∈ 𝑥 ∧ ∀𝑏 ∈ 𝑎 suc 𝑏 ∈ 𝑥))) |
| 31 | 30 | adantr 480 |
. . . . . . 7
⊢ (((𝑎 ∈ On ∧ ∀𝑏 ∈ 𝑎 (𝑏 +no 1o) = suc 𝑏) ∧ 𝑥 ∈ On) → ((∀𝑦 ∈ 1o (𝑎 +no 𝑦) ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑎 (𝑦 +no 1o) ∈ 𝑥) ↔ ((𝑎 +no ∅) ∈ 𝑥 ∧ ∀𝑏 ∈ 𝑎 suc 𝑏 ∈ 𝑥))) |
| 32 | | onelon 6409 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 ∈ On ∧ 𝑏 ∈ 𝑎) → 𝑏 ∈ On) |
| 33 | 32 | ad4ant13 751 |
. . . . . . . . . . . . . 14
⊢ ((((𝑎 ∈ On ∧ 𝑥 ∈ On) ∧ 𝑏 ∈ 𝑎) ∧ 𝑎 ∈ 𝑥) → 𝑏 ∈ On) |
| 34 | | onsuc 7831 |
. . . . . . . . . . . . . 14
⊢ (𝑏 ∈ On → suc 𝑏 ∈ On) |
| 35 | 33, 34 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((((𝑎 ∈ On ∧ 𝑥 ∈ On) ∧ 𝑏 ∈ 𝑎) ∧ 𝑎 ∈ 𝑥) → suc 𝑏 ∈ On) |
| 36 | | simpllr 776 |
. . . . . . . . . . . . 13
⊢ ((((𝑎 ∈ On ∧ 𝑥 ∈ On) ∧ 𝑏 ∈ 𝑎) ∧ 𝑎 ∈ 𝑥) → 𝑥 ∈ On) |
| 37 | 35, 36 | jca 511 |
. . . . . . . . . . . 12
⊢ ((((𝑎 ∈ On ∧ 𝑥 ∈ On) ∧ 𝑏 ∈ 𝑎) ∧ 𝑎 ∈ 𝑥) → (suc 𝑏 ∈ On ∧ 𝑥 ∈ On)) |
| 38 | | eloni 6394 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 ∈ On → Ord 𝑎) |
| 39 | 38 | ad3antrrr 730 |
. . . . . . . . . . . . . 14
⊢ ((((𝑎 ∈ On ∧ 𝑥 ∈ On) ∧ 𝑏 ∈ 𝑎) ∧ 𝑎 ∈ 𝑥) → Ord 𝑎) |
| 40 | | simplr 769 |
. . . . . . . . . . . . . 14
⊢ ((((𝑎 ∈ On ∧ 𝑥 ∈ On) ∧ 𝑏 ∈ 𝑎) ∧ 𝑎 ∈ 𝑥) → 𝑏 ∈ 𝑎) |
| 41 | | ordsucss 7838 |
. . . . . . . . . . . . . 14
⊢ (Ord
𝑎 → (𝑏 ∈ 𝑎 → suc 𝑏 ⊆ 𝑎)) |
| 42 | 39, 40, 41 | sylc 65 |
. . . . . . . . . . . . 13
⊢ ((((𝑎 ∈ On ∧ 𝑥 ∈ On) ∧ 𝑏 ∈ 𝑎) ∧ 𝑎 ∈ 𝑥) → suc 𝑏 ⊆ 𝑎) |
| 43 | | simpr 484 |
. . . . . . . . . . . . 13
⊢ ((((𝑎 ∈ On ∧ 𝑥 ∈ On) ∧ 𝑏 ∈ 𝑎) ∧ 𝑎 ∈ 𝑥) → 𝑎 ∈ 𝑥) |
| 44 | 42, 43 | jca 511 |
. . . . . . . . . . . 12
⊢ ((((𝑎 ∈ On ∧ 𝑥 ∈ On) ∧ 𝑏 ∈ 𝑎) ∧ 𝑎 ∈ 𝑥) → (suc 𝑏 ⊆ 𝑎 ∧ 𝑎 ∈ 𝑥)) |
| 45 | | ontr2 6431 |
. . . . . . . . . . . 12
⊢ ((suc
𝑏 ∈ On ∧ 𝑥 ∈ On) → ((suc 𝑏 ⊆ 𝑎 ∧ 𝑎 ∈ 𝑥) → suc 𝑏 ∈ 𝑥)) |
| 46 | 37, 44, 45 | sylc 65 |
. . . . . . . . . . 11
⊢ ((((𝑎 ∈ On ∧ 𝑥 ∈ On) ∧ 𝑏 ∈ 𝑎) ∧ 𝑎 ∈ 𝑥) → suc 𝑏 ∈ 𝑥) |
| 47 | 46 | ex 412 |
. . . . . . . . . 10
⊢ (((𝑎 ∈ On ∧ 𝑥 ∈ On) ∧ 𝑏 ∈ 𝑎) → (𝑎 ∈ 𝑥 → suc 𝑏 ∈ 𝑥)) |
| 48 | 47 | ralrimdva 3154 |
. . . . . . . . 9
⊢ ((𝑎 ∈ On ∧ 𝑥 ∈ On) → (𝑎 ∈ 𝑥 → ∀𝑏 ∈ 𝑎 suc 𝑏 ∈ 𝑥)) |
| 49 | 48 | pm4.71d 561 |
. . . . . . . 8
⊢ ((𝑎 ∈ On ∧ 𝑥 ∈ On) → (𝑎 ∈ 𝑥 ↔ (𝑎 ∈ 𝑥 ∧ ∀𝑏 ∈ 𝑎 suc 𝑏 ∈ 𝑥))) |
| 50 | 49 | adantlr 715 |
. . . . . . 7
⊢ (((𝑎 ∈ On ∧ ∀𝑏 ∈ 𝑎 (𝑏 +no 1o) = suc 𝑏) ∧ 𝑥 ∈ On) → (𝑎 ∈ 𝑥 ↔ (𝑎 ∈ 𝑥 ∧ ∀𝑏 ∈ 𝑎 suc 𝑏 ∈ 𝑥))) |
| 51 | 10, 31, 50 | 3bitr4d 311 |
. . . . . 6
⊢ (((𝑎 ∈ On ∧ ∀𝑏 ∈ 𝑎 (𝑏 +no 1o) = suc 𝑏) ∧ 𝑥 ∈ On) → ((∀𝑦 ∈ 1o (𝑎 +no 𝑦) ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑎 (𝑦 +no 1o) ∈ 𝑥) ↔ 𝑎 ∈ 𝑥)) |
| 52 | 51 | rabbidva 3443 |
. . . . 5
⊢ ((𝑎 ∈ On ∧ ∀𝑏 ∈ 𝑎 (𝑏 +no 1o) = suc 𝑏) → {𝑥 ∈ On ∣ (∀𝑦 ∈ 1o (𝑎 +no 𝑦) ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑎 (𝑦 +no 1o) ∈ 𝑥)} = {𝑥 ∈ On ∣ 𝑎 ∈ 𝑥}) |
| 53 | 52 | inteqd 4951 |
. . . 4
⊢ ((𝑎 ∈ On ∧ ∀𝑏 ∈ 𝑎 (𝑏 +no 1o) = suc 𝑏) → ∩ {𝑥 ∈ On ∣
(∀𝑦 ∈
1o (𝑎 +no 𝑦) ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑎 (𝑦 +no 1o) ∈ 𝑥)} = ∩ {𝑥 ∈ On ∣ 𝑎 ∈ 𝑥}) |
| 54 | | 1on 8518 |
. . . . . 6
⊢
1o ∈ On |
| 55 | | naddov2 8717 |
. . . . . 6
⊢ ((𝑎 ∈ On ∧ 1o
∈ On) → (𝑎 +no
1o) = ∩ {𝑥 ∈ On ∣ (∀𝑦 ∈ 1o (𝑎 +no 𝑦) ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑎 (𝑦 +no 1o) ∈ 𝑥)}) |
| 56 | 54, 55 | mpan2 691 |
. . . . 5
⊢ (𝑎 ∈ On → (𝑎 +no 1o) = ∩ {𝑥
∈ On ∣ (∀𝑦 ∈ 1o (𝑎 +no 𝑦) ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑎 (𝑦 +no 1o) ∈ 𝑥)}) |
| 57 | 56 | adantr 480 |
. . . 4
⊢ ((𝑎 ∈ On ∧ ∀𝑏 ∈ 𝑎 (𝑏 +no 1o) = suc 𝑏) → (𝑎 +no 1o) = ∩ {𝑥
∈ On ∣ (∀𝑦 ∈ 1o (𝑎 +no 𝑦) ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑎 (𝑦 +no 1o) ∈ 𝑥)}) |
| 58 | | onsucmin 7841 |
. . . . 5
⊢ (𝑎 ∈ On → suc 𝑎 = ∩
{𝑥 ∈ On ∣ 𝑎 ∈ 𝑥}) |
| 59 | 58 | adantr 480 |
. . . 4
⊢ ((𝑎 ∈ On ∧ ∀𝑏 ∈ 𝑎 (𝑏 +no 1o) = suc 𝑏) → suc 𝑎 = ∩ {𝑥 ∈ On ∣ 𝑎 ∈ 𝑥}) |
| 60 | 53, 57, 59 | 3eqtr4d 2787 |
. . 3
⊢ ((𝑎 ∈ On ∧ ∀𝑏 ∈ 𝑎 (𝑏 +no 1o) = suc 𝑏) → (𝑎 +no 1o) = suc 𝑎) |
| 61 | 60 | ex 412 |
. 2
⊢ (𝑎 ∈ On → (∀𝑏 ∈ 𝑎 (𝑏 +no 1o) = suc 𝑏 → (𝑎 +no 1o) = suc 𝑎)) |
| 62 | 3, 6, 61 | tfis3 7879 |
1
⊢ (𝐴 ∈ On → (𝐴 +no 1o) = suc 𝐴) |