Step | Hyp | Ref
| Expression |
1 | | elirr 4523 |
. . . . 5
⊢ ¬
𝐵 ∈ 𝐵 |
2 | | elsni 3599 |
. . . . . . . 8
⊢ (𝑥 ∈ {𝐵} → 𝑥 = 𝐵) |
3 | 2 | adantl 275 |
. . . . . . 7
⊢ ((((𝐵 ∈ 𝑉 ∧ (𝐴 ∪ {𝐵}) ∈ On) ∧ 𝑥 ∈ 𝐵) ∧ 𝑥 ∈ {𝐵}) → 𝑥 = 𝐵) |
4 | | simplr 525 |
. . . . . . 7
⊢ ((((𝐵 ∈ 𝑉 ∧ (𝐴 ∪ {𝐵}) ∈ On) ∧ 𝑥 ∈ 𝐵) ∧ 𝑥 ∈ {𝐵}) → 𝑥 ∈ 𝐵) |
5 | 3, 4 | eqeltrrd 2248 |
. . . . . 6
⊢ ((((𝐵 ∈ 𝑉 ∧ (𝐴 ∪ {𝐵}) ∈ On) ∧ 𝑥 ∈ 𝐵) ∧ 𝑥 ∈ {𝐵}) → 𝐵 ∈ 𝐵) |
6 | 5 | ex 114 |
. . . . 5
⊢ (((𝐵 ∈ 𝑉 ∧ (𝐴 ∪ {𝐵}) ∈ On) ∧ 𝑥 ∈ 𝐵) → (𝑥 ∈ {𝐵} → 𝐵 ∈ 𝐵)) |
7 | 1, 6 | mtoi 659 |
. . . 4
⊢ (((𝐵 ∈ 𝑉 ∧ (𝐴 ∪ {𝐵}) ∈ On) ∧ 𝑥 ∈ 𝐵) → ¬ 𝑥 ∈ {𝐵}) |
8 | | snidg 3610 |
. . . . . . . . 9
⊢ (𝐵 ∈ 𝑉 → 𝐵 ∈ {𝐵}) |
9 | | elun2 3295 |
. . . . . . . . 9
⊢ (𝐵 ∈ {𝐵} → 𝐵 ∈ (𝐴 ∪ {𝐵})) |
10 | 8, 9 | syl 14 |
. . . . . . . 8
⊢ (𝐵 ∈ 𝑉 → 𝐵 ∈ (𝐴 ∪ {𝐵})) |
11 | 10 | adantr 274 |
. . . . . . 7
⊢ ((𝐵 ∈ 𝑉 ∧ (𝐴 ∪ {𝐵}) ∈ On) → 𝐵 ∈ (𝐴 ∪ {𝐵})) |
12 | | ontr1 4372 |
. . . . . . . 8
⊢ ((𝐴 ∪ {𝐵}) ∈ On → ((𝑥 ∈ 𝐵 ∧ 𝐵 ∈ (𝐴 ∪ {𝐵})) → 𝑥 ∈ (𝐴 ∪ {𝐵}))) |
13 | 12 | adantl 275 |
. . . . . . 7
⊢ ((𝐵 ∈ 𝑉 ∧ (𝐴 ∪ {𝐵}) ∈ On) → ((𝑥 ∈ 𝐵 ∧ 𝐵 ∈ (𝐴 ∪ {𝐵})) → 𝑥 ∈ (𝐴 ∪ {𝐵}))) |
14 | 11, 13 | mpan2d 426 |
. . . . . 6
⊢ ((𝐵 ∈ 𝑉 ∧ (𝐴 ∪ {𝐵}) ∈ On) → (𝑥 ∈ 𝐵 → 𝑥 ∈ (𝐴 ∪ {𝐵}))) |
15 | 14 | imp 123 |
. . . . 5
⊢ (((𝐵 ∈ 𝑉 ∧ (𝐴 ∪ {𝐵}) ∈ On) ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ (𝐴 ∪ {𝐵})) |
16 | | elun 3268 |
. . . . 5
⊢ (𝑥 ∈ (𝐴 ∪ {𝐵}) ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ {𝐵})) |
17 | 15, 16 | sylib 121 |
. . . 4
⊢ (((𝐵 ∈ 𝑉 ∧ (𝐴 ∪ {𝐵}) ∈ On) ∧ 𝑥 ∈ 𝐵) → (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ {𝐵})) |
18 | 7, 17 | ecased 1344 |
. . 3
⊢ (((𝐵 ∈ 𝑉 ∧ (𝐴 ∪ {𝐵}) ∈ On) ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝐴) |
19 | 18 | ex 114 |
. 2
⊢ ((𝐵 ∈ 𝑉 ∧ (𝐴 ∪ {𝐵}) ∈ On) → (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐴)) |
20 | 19 | ssrdv 3153 |
1
⊢ ((𝐵 ∈ 𝑉 ∧ (𝐴 ∪ {𝐵}) ∈ On) → 𝐵 ⊆ 𝐴) |