| Step | Hyp | Ref
| Expression |
| 1 | | oveq1 7438 |
. . 3
⊢ (𝑎 = 𝑏 → (𝑎 +no ∅) = (𝑏 +no ∅)) |
| 2 | | id 22 |
. . 3
⊢ (𝑎 = 𝑏 → 𝑎 = 𝑏) |
| 3 | 1, 2 | eqeq12d 2753 |
. 2
⊢ (𝑎 = 𝑏 → ((𝑎 +no ∅) = 𝑎 ↔ (𝑏 +no ∅) = 𝑏)) |
| 4 | | oveq1 7438 |
. . 3
⊢ (𝑎 = 𝐴 → (𝑎 +no ∅) = (𝐴 +no ∅)) |
| 5 | | id 22 |
. . 3
⊢ (𝑎 = 𝐴 → 𝑎 = 𝐴) |
| 6 | 4, 5 | eqeq12d 2753 |
. 2
⊢ (𝑎 = 𝐴 → ((𝑎 +no ∅) = 𝑎 ↔ (𝐴 +no ∅) = 𝐴)) |
| 7 | | 0elon 6438 |
. . . . . 6
⊢ ∅
∈ On |
| 8 | | naddov2 8717 |
. . . . . 6
⊢ ((𝑎 ∈ On ∧ ∅ ∈
On) → (𝑎 +no ∅)
= ∩ {𝑥 ∈ On ∣ (∀𝑐 ∈ ∅ (𝑎 +no 𝑐) ∈ 𝑥 ∧ ∀𝑏 ∈ 𝑎 (𝑏 +no ∅) ∈ 𝑥)}) |
| 9 | 7, 8 | mpan2 691 |
. . . . 5
⊢ (𝑎 ∈ On → (𝑎 +no ∅) = ∩ {𝑥
∈ On ∣ (∀𝑐 ∈ ∅ (𝑎 +no 𝑐) ∈ 𝑥 ∧ ∀𝑏 ∈ 𝑎 (𝑏 +no ∅) ∈ 𝑥)}) |
| 10 | 9 | adantr 480 |
. . . 4
⊢ ((𝑎 ∈ On ∧ ∀𝑏 ∈ 𝑎 (𝑏 +no ∅) = 𝑏) → (𝑎 +no ∅) = ∩
{𝑥 ∈ On ∣
(∀𝑐 ∈ ∅
(𝑎 +no 𝑐) ∈ 𝑥 ∧ ∀𝑏 ∈ 𝑎 (𝑏 +no ∅) ∈ 𝑥)}) |
| 11 | | ral0 4513 |
. . . . . . . 8
⊢
∀𝑐 ∈
∅ (𝑎 +no 𝑐) ∈ 𝑥 |
| 12 | 11 | biantrur 530 |
. . . . . . 7
⊢
(∀𝑏 ∈
𝑎 (𝑏 +no ∅) ∈ 𝑥 ↔ (∀𝑐 ∈ ∅ (𝑎 +no 𝑐) ∈ 𝑥 ∧ ∀𝑏 ∈ 𝑎 (𝑏 +no ∅) ∈ 𝑥)) |
| 13 | | eleq1 2829 |
. . . . . . . . . . 11
⊢ ((𝑏 +no ∅) = 𝑏 → ((𝑏 +no ∅) ∈ 𝑥 ↔ 𝑏 ∈ 𝑥)) |
| 14 | 13 | ralimi 3083 |
. . . . . . . . . 10
⊢
(∀𝑏 ∈
𝑎 (𝑏 +no ∅) = 𝑏 → ∀𝑏 ∈ 𝑎 ((𝑏 +no ∅) ∈ 𝑥 ↔ 𝑏 ∈ 𝑥)) |
| 15 | | ralbi 3103 |
. . . . . . . . . 10
⊢
(∀𝑏 ∈
𝑎 ((𝑏 +no ∅) ∈ 𝑥 ↔ 𝑏 ∈ 𝑥) → (∀𝑏 ∈ 𝑎 (𝑏 +no ∅) ∈ 𝑥 ↔ ∀𝑏 ∈ 𝑎 𝑏 ∈ 𝑥)) |
| 16 | 14, 15 | syl 17 |
. . . . . . . . 9
⊢
(∀𝑏 ∈
𝑎 (𝑏 +no ∅) = 𝑏 → (∀𝑏 ∈ 𝑎 (𝑏 +no ∅) ∈ 𝑥 ↔ ∀𝑏 ∈ 𝑎 𝑏 ∈ 𝑥)) |
| 17 | 16 | adantl 481 |
. . . . . . . 8
⊢ ((𝑎 ∈ On ∧ ∀𝑏 ∈ 𝑎 (𝑏 +no ∅) = 𝑏) → (∀𝑏 ∈ 𝑎 (𝑏 +no ∅) ∈ 𝑥 ↔ ∀𝑏 ∈ 𝑎 𝑏 ∈ 𝑥)) |
| 18 | | dfss3 3972 |
. . . . . . . 8
⊢ (𝑎 ⊆ 𝑥 ↔ ∀𝑏 ∈ 𝑎 𝑏 ∈ 𝑥) |
| 19 | 17, 18 | bitr4di 289 |
. . . . . . 7
⊢ ((𝑎 ∈ On ∧ ∀𝑏 ∈ 𝑎 (𝑏 +no ∅) = 𝑏) → (∀𝑏 ∈ 𝑎 (𝑏 +no ∅) ∈ 𝑥 ↔ 𝑎 ⊆ 𝑥)) |
| 20 | 12, 19 | bitr3id 285 |
. . . . . 6
⊢ ((𝑎 ∈ On ∧ ∀𝑏 ∈ 𝑎 (𝑏 +no ∅) = 𝑏) → ((∀𝑐 ∈ ∅ (𝑎 +no 𝑐) ∈ 𝑥 ∧ ∀𝑏 ∈ 𝑎 (𝑏 +no ∅) ∈ 𝑥) ↔ 𝑎 ⊆ 𝑥)) |
| 21 | 20 | rabbidv 3444 |
. . . . 5
⊢ ((𝑎 ∈ On ∧ ∀𝑏 ∈ 𝑎 (𝑏 +no ∅) = 𝑏) → {𝑥 ∈ On ∣ (∀𝑐 ∈ ∅ (𝑎 +no 𝑐) ∈ 𝑥 ∧ ∀𝑏 ∈ 𝑎 (𝑏 +no ∅) ∈ 𝑥)} = {𝑥 ∈ On ∣ 𝑎 ⊆ 𝑥}) |
| 22 | 21 | inteqd 4951 |
. . . 4
⊢ ((𝑎 ∈ On ∧ ∀𝑏 ∈ 𝑎 (𝑏 +no ∅) = 𝑏) → ∩ {𝑥 ∈ On ∣
(∀𝑐 ∈ ∅
(𝑎 +no 𝑐) ∈ 𝑥 ∧ ∀𝑏 ∈ 𝑎 (𝑏 +no ∅) ∈ 𝑥)} = ∩ {𝑥 ∈ On ∣ 𝑎 ⊆ 𝑥}) |
| 23 | | intmin 4968 |
. . . . 5
⊢ (𝑎 ∈ On → ∩ {𝑥
∈ On ∣ 𝑎 ⊆
𝑥} = 𝑎) |
| 24 | 23 | adantr 480 |
. . . 4
⊢ ((𝑎 ∈ On ∧ ∀𝑏 ∈ 𝑎 (𝑏 +no ∅) = 𝑏) → ∩ {𝑥 ∈ On ∣ 𝑎 ⊆ 𝑥} = 𝑎) |
| 25 | 10, 22, 24 | 3eqtrd 2781 |
. . 3
⊢ ((𝑎 ∈ On ∧ ∀𝑏 ∈ 𝑎 (𝑏 +no ∅) = 𝑏) → (𝑎 +no ∅) = 𝑎) |
| 26 | 25 | ex 412 |
. 2
⊢ (𝑎 ∈ On → (∀𝑏 ∈ 𝑎 (𝑏 +no ∅) = 𝑏 → (𝑎 +no ∅) = 𝑎)) |
| 27 | 3, 6, 26 | tfis3 7879 |
1
⊢ (𝐴 ∈ On → (𝐴 +no ∅) = 𝐴) |