Step | Hyp | Ref
| Expression |
1 | | difsnss 3698 |
. . 3
⊢ (𝐵 ∈ 𝐴 → ((𝐴 ∖ {𝐵}) ∪ {𝐵}) ⊆ 𝐴) |
2 | 1 | adantl 275 |
. 2
⊢
((∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ 𝐴) → ((𝐴 ∖ {𝐵}) ∪ {𝐵}) ⊆ 𝐴) |
3 | | simpr 109 |
. . . . . . 7
⊢
((((∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ 𝐴) ∧ 𝑧 ∈ 𝐴) ∧ 𝑧 = 𝐵) → 𝑧 = 𝐵) |
4 | | velsn 3573 |
. . . . . . 7
⊢ (𝑧 ∈ {𝐵} ↔ 𝑧 = 𝐵) |
5 | 3, 4 | sylibr 133 |
. . . . . 6
⊢
((((∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ 𝐴) ∧ 𝑧 ∈ 𝐴) ∧ 𝑧 = 𝐵) → 𝑧 ∈ {𝐵}) |
6 | | elun2 3271 |
. . . . . 6
⊢ (𝑧 ∈ {𝐵} → 𝑧 ∈ ((𝐴 ∖ {𝐵}) ∪ {𝐵})) |
7 | 5, 6 | syl 14 |
. . . . 5
⊢
((((∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ 𝐴) ∧ 𝑧 ∈ 𝐴) ∧ 𝑧 = 𝐵) → 𝑧 ∈ ((𝐴 ∖ {𝐵}) ∪ {𝐵})) |
8 | | simplr 520 |
. . . . . . 7
⊢
((((∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ 𝐴) ∧ 𝑧 ∈ 𝐴) ∧ ¬ 𝑧 = 𝐵) → 𝑧 ∈ 𝐴) |
9 | | simpr 109 |
. . . . . . . 8
⊢
((((∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ 𝐴) ∧ 𝑧 ∈ 𝐴) ∧ ¬ 𝑧 = 𝐵) → ¬ 𝑧 = 𝐵) |
10 | 9, 4 | sylnibr 667 |
. . . . . . 7
⊢
((((∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ 𝐴) ∧ 𝑧 ∈ 𝐴) ∧ ¬ 𝑧 = 𝐵) → ¬ 𝑧 ∈ {𝐵}) |
11 | 8, 10 | eldifd 3108 |
. . . . . 6
⊢
((((∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ 𝐴) ∧ 𝑧 ∈ 𝐴) ∧ ¬ 𝑧 = 𝐵) → 𝑧 ∈ (𝐴 ∖ {𝐵})) |
12 | | elun1 3270 |
. . . . . 6
⊢ (𝑧 ∈ (𝐴 ∖ {𝐵}) → 𝑧 ∈ ((𝐴 ∖ {𝐵}) ∪ {𝐵})) |
13 | 11, 12 | syl 14 |
. . . . 5
⊢
((((∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ 𝐴) ∧ 𝑧 ∈ 𝐴) ∧ ¬ 𝑧 = 𝐵) → 𝑧 ∈ ((𝐴 ∖ {𝐵}) ∪ {𝐵})) |
14 | | simpll 519 |
. . . . . . 7
⊢
(((∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ 𝐴) ∧ 𝑧 ∈ 𝐴) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦) |
15 | | simpr 109 |
. . . . . . . 8
⊢
(((∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ 𝐴) ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ 𝐴) |
16 | | simplr 520 |
. . . . . . . 8
⊢
(((∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ 𝐴) ∧ 𝑧 ∈ 𝐴) → 𝐵 ∈ 𝐴) |
17 | | equequ1 1689 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑧 → (𝑥 = 𝑦 ↔ 𝑧 = 𝑦)) |
18 | 17 | dcbid 824 |
. . . . . . . . 9
⊢ (𝑥 = 𝑧 → (DECID 𝑥 = 𝑦 ↔ DECID 𝑧 = 𝑦)) |
19 | | eqeq2 2164 |
. . . . . . . . . 10
⊢ (𝑦 = 𝐵 → (𝑧 = 𝑦 ↔ 𝑧 = 𝐵)) |
20 | 19 | dcbid 824 |
. . . . . . . . 9
⊢ (𝑦 = 𝐵 → (DECID 𝑧 = 𝑦 ↔ DECID 𝑧 = 𝐵)) |
21 | 18, 20 | rspc2v 2826 |
. . . . . . . 8
⊢ ((𝑧 ∈ 𝐴 ∧ 𝐵 ∈ 𝐴) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 → DECID 𝑧 = 𝐵)) |
22 | 15, 16, 21 | syl2anc 409 |
. . . . . . 7
⊢
(((∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ 𝐴) ∧ 𝑧 ∈ 𝐴) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 → DECID 𝑧 = 𝐵)) |
23 | 14, 22 | mpd 13 |
. . . . . 6
⊢
(((∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ 𝐴) ∧ 𝑧 ∈ 𝐴) → DECID 𝑧 = 𝐵) |
24 | | exmiddc 822 |
. . . . . 6
⊢
(DECID 𝑧 = 𝐵 → (𝑧 = 𝐵 ∨ ¬ 𝑧 = 𝐵)) |
25 | 23, 24 | syl 14 |
. . . . 5
⊢
(((∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ 𝐴) ∧ 𝑧 ∈ 𝐴) → (𝑧 = 𝐵 ∨ ¬ 𝑧 = 𝐵)) |
26 | 7, 13, 25 | mpjaodan 788 |
. . . 4
⊢
(((∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ 𝐴) ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ ((𝐴 ∖ {𝐵}) ∪ {𝐵})) |
27 | 26 | ex 114 |
. . 3
⊢
((∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ 𝐴) → (𝑧 ∈ 𝐴 → 𝑧 ∈ ((𝐴 ∖ {𝐵}) ∪ {𝐵}))) |
28 | 27 | ssrdv 3130 |
. 2
⊢
((∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ 𝐴) → 𝐴 ⊆ ((𝐴 ∖ {𝐵}) ∪ {𝐵})) |
29 | 2, 28 | eqssd 3141 |
1
⊢
((∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ 𝐴) → ((𝐴 ∖ {𝐵}) ∪ {𝐵}) = 𝐴) |