Step | Hyp | Ref
| Expression |
1 | | elirr 4266 |
. . . . 5
⊢ ¬
𝐵 ∈ 𝐵 |
2 | | elsni 3393 |
. . . . . . . 8
⊢ (𝑥 ∈ {𝐵} → 𝑥 = 𝐵) |
3 | 2 | adantl 262 |
. . . . . . 7
⊢ ((((𝐵 ∈ 𝑉 ∧ (𝐴 ∪ {𝐵}) ∈ On) ∧ 𝑥 ∈ 𝐵) ∧ 𝑥 ∈ {𝐵}) → 𝑥 = 𝐵) |
4 | | simplr 482 |
. . . . . . 7
⊢ ((((𝐵 ∈ 𝑉 ∧ (𝐴 ∪ {𝐵}) ∈ On) ∧ 𝑥 ∈ 𝐵) ∧ 𝑥 ∈ {𝐵}) → 𝑥 ∈ 𝐵) |
5 | 3, 4 | eqeltrrd 2115 |
. . . . . 6
⊢ ((((𝐵 ∈ 𝑉 ∧ (𝐴 ∪ {𝐵}) ∈ On) ∧ 𝑥 ∈ 𝐵) ∧ 𝑥 ∈ {𝐵}) → 𝐵 ∈ 𝐵) |
6 | 5 | ex 108 |
. . . . 5
⊢ (((𝐵 ∈ 𝑉 ∧ (𝐴 ∪ {𝐵}) ∈ On) ∧ 𝑥 ∈ 𝐵) → (𝑥 ∈ {𝐵} → 𝐵 ∈ 𝐵)) |
7 | 1, 6 | mtoi 590 |
. . . 4
⊢ (((𝐵 ∈ 𝑉 ∧ (𝐴 ∪ {𝐵}) ∈ On) ∧ 𝑥 ∈ 𝐵) → ¬ 𝑥 ∈ {𝐵}) |
8 | | snidg 3400 |
. . . . . . . . 9
⊢ (𝐵 ∈ 𝑉 → 𝐵 ∈ {𝐵}) |
9 | | elun2 3111 |
. . . . . . . . 9
⊢ (𝐵 ∈ {𝐵} → 𝐵 ∈ (𝐴 ∪ {𝐵})) |
10 | 8, 9 | syl 14 |
. . . . . . . 8
⊢ (𝐵 ∈ 𝑉 → 𝐵 ∈ (𝐴 ∪ {𝐵})) |
11 | 10 | adantr 261 |
. . . . . . 7
⊢ ((𝐵 ∈ 𝑉 ∧ (𝐴 ∪ {𝐵}) ∈ On) → 𝐵 ∈ (𝐴 ∪ {𝐵})) |
12 | | ontr1 4126 |
. . . . . . . 8
⊢ ((𝐴 ∪ {𝐵}) ∈ On → ((𝑥 ∈ 𝐵 ∧ 𝐵 ∈ (𝐴 ∪ {𝐵})) → 𝑥 ∈ (𝐴 ∪ {𝐵}))) |
13 | 12 | adantl 262 |
. . . . . . 7
⊢ ((𝐵 ∈ 𝑉 ∧ (𝐴 ∪ {𝐵}) ∈ On) → ((𝑥 ∈ 𝐵 ∧ 𝐵 ∈ (𝐴 ∪ {𝐵})) → 𝑥 ∈ (𝐴 ∪ {𝐵}))) |
14 | 11, 13 | mpan2d 404 |
. . . . . 6
⊢ ((𝐵 ∈ 𝑉 ∧ (𝐴 ∪ {𝐵}) ∈ On) → (𝑥 ∈ 𝐵 → 𝑥 ∈ (𝐴 ∪ {𝐵}))) |
15 | 14 | imp 115 |
. . . . 5
⊢ (((𝐵 ∈ 𝑉 ∧ (𝐴 ∪ {𝐵}) ∈ On) ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ (𝐴 ∪ {𝐵})) |
16 | | elun 3084 |
. . . . 5
⊢ (𝑥 ∈ (𝐴 ∪ {𝐵}) ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ {𝐵})) |
17 | 15, 16 | sylib 127 |
. . . 4
⊢ (((𝐵 ∈ 𝑉 ∧ (𝐴 ∪ {𝐵}) ∈ On) ∧ 𝑥 ∈ 𝐵) → (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ {𝐵})) |
18 | 7, 17 | ecased 1239 |
. . 3
⊢ (((𝐵 ∈ 𝑉 ∧ (𝐴 ∪ {𝐵}) ∈ On) ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝐴) |
19 | 18 | ex 108 |
. 2
⊢ ((𝐵 ∈ 𝑉 ∧ (𝐴 ∪ {𝐵}) ∈ On) → (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐴)) |
20 | 19 | ssrdv 2951 |
1
⊢ ((𝐵 ∈ 𝑉 ∧ (𝐴 ∪ {𝐵}) ∈ On) → 𝐵 ⊆ 𝐴) |