Step | Hyp | Ref
| Expression |
1 | | raleq 2659 |
. . 3
⊢ (𝑤 = ∅ → (∀𝑥 ∈ 𝑤 𝜑 ↔ ∀𝑥 ∈ ∅ 𝜑)) |
2 | 1 | dcbid 828 |
. 2
⊢ (𝑤 = ∅ →
(DECID ∀𝑥 ∈ 𝑤 𝜑 ↔ DECID ∀𝑥 ∈ ∅ 𝜑)) |
3 | | raleq 2659 |
. . 3
⊢ (𝑤 = 𝑦 → (∀𝑥 ∈ 𝑤 𝜑 ↔ ∀𝑥 ∈ 𝑦 𝜑)) |
4 | 3 | dcbid 828 |
. 2
⊢ (𝑤 = 𝑦 → (DECID ∀𝑥 ∈ 𝑤 𝜑 ↔ DECID ∀𝑥 ∈ 𝑦 𝜑)) |
5 | | raleq 2659 |
. . 3
⊢ (𝑤 = (𝑦 ∪ {𝑧}) → (∀𝑥 ∈ 𝑤 𝜑 ↔ ∀𝑥 ∈ (𝑦 ∪ {𝑧})𝜑)) |
6 | 5 | dcbid 828 |
. 2
⊢ (𝑤 = (𝑦 ∪ {𝑧}) → (DECID ∀𝑥 ∈ 𝑤 𝜑 ↔ DECID ∀𝑥 ∈ (𝑦 ∪ {𝑧})𝜑)) |
7 | | raleq 2659 |
. . 3
⊢ (𝑤 = 𝐴 → (∀𝑥 ∈ 𝑤 𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜑)) |
8 | 7 | dcbid 828 |
. 2
⊢ (𝑤 = 𝐴 → (DECID ∀𝑥 ∈ 𝑤 𝜑 ↔ DECID ∀𝑥 ∈ 𝐴 𝜑)) |
9 | | ral0 3508 |
. . . . 5
⊢
∀𝑥 ∈
∅ 𝜑 |
10 | 9 | orci 721 |
. . . 4
⊢
(∀𝑥 ∈
∅ 𝜑 ∨ ¬
∀𝑥 ∈ ∅
𝜑) |
11 | | df-dc 825 |
. . . 4
⊢
(DECID ∀𝑥 ∈ ∅ 𝜑 ↔ (∀𝑥 ∈ ∅ 𝜑 ∨ ¬ ∀𝑥 ∈ ∅ 𝜑)) |
12 | 10, 11 | mpbir 145 |
. . 3
⊢
DECID ∀𝑥 ∈ ∅ 𝜑 |
13 | 12 | a1i 9 |
. 2
⊢ ((𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 DECID 𝜑) → DECID ∀𝑥 ∈ ∅ 𝜑) |
14 | | simpr 109 |
. . . . 5
⊢
(((((𝐴 ∈ Fin
∧ ∀𝑥 ∈
𝐴 DECID
𝜑) ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ DECID ∀𝑥 ∈ 𝑦 𝜑) → DECID ∀𝑥 ∈ 𝑦 𝜑) |
15 | | simplrr 526 |
. . . . . . . 8
⊢
(((((𝐴 ∈ Fin
∧ ∀𝑥 ∈
𝐴 DECID
𝜑) ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ DECID ∀𝑥 ∈ 𝑦 𝜑) → 𝑧 ∈ (𝐴 ∖ 𝑦)) |
16 | 15 | eldifad 3125 |
. . . . . . 7
⊢
(((((𝐴 ∈ Fin
∧ ∀𝑥 ∈
𝐴 DECID
𝜑) ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ DECID ∀𝑥 ∈ 𝑦 𝜑) → 𝑧 ∈ 𝐴) |
17 | | simp-4r 532 |
. . . . . . 7
⊢
(((((𝐴 ∈ Fin
∧ ∀𝑥 ∈
𝐴 DECID
𝜑) ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ DECID ∀𝑥 ∈ 𝑦 𝜑) → ∀𝑥 ∈ 𝐴 DECID 𝜑) |
18 | | nfsbc1v 2967 |
. . . . . . . . 9
⊢
Ⅎ𝑥[𝑧 / 𝑥]𝜑 |
19 | 18 | nfdc 1646 |
. . . . . . . 8
⊢
Ⅎ𝑥DECID [𝑧 / 𝑥]𝜑 |
20 | | sbceq1a 2958 |
. . . . . . . . 9
⊢ (𝑥 = 𝑧 → (𝜑 ↔ [𝑧 / 𝑥]𝜑)) |
21 | 20 | dcbid 828 |
. . . . . . . 8
⊢ (𝑥 = 𝑧 → (DECID 𝜑 ↔ DECID [𝑧 / 𝑥]𝜑)) |
22 | 19, 21 | rspc 2822 |
. . . . . . 7
⊢ (𝑧 ∈ 𝐴 → (∀𝑥 ∈ 𝐴 DECID 𝜑 → DECID [𝑧 / 𝑥]𝜑)) |
23 | 16, 17, 22 | sylc 62 |
. . . . . 6
⊢
(((((𝐴 ∈ Fin
∧ ∀𝑥 ∈
𝐴 DECID
𝜑) ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ DECID ∀𝑥 ∈ 𝑦 𝜑) → DECID [𝑧 / 𝑥]𝜑) |
24 | | ralsnsg 3610 |
. . . . . . . 8
⊢ (𝑧 ∈ V → (∀𝑥 ∈ {𝑧}𝜑 ↔ [𝑧 / 𝑥]𝜑)) |
25 | 24 | elv 2728 |
. . . . . . 7
⊢
(∀𝑥 ∈
{𝑧}𝜑 ↔ [𝑧 / 𝑥]𝜑) |
26 | 25 | dcbii 830 |
. . . . . 6
⊢
(DECID ∀𝑥 ∈ {𝑧}𝜑 ↔ DECID [𝑧 / 𝑥]𝜑) |
27 | 23, 26 | sylibr 133 |
. . . . 5
⊢
(((((𝐴 ∈ Fin
∧ ∀𝑥 ∈
𝐴 DECID
𝜑) ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ DECID ∀𝑥 ∈ 𝑦 𝜑) → DECID ∀𝑥 ∈ {𝑧}𝜑) |
28 | | dcan 923 |
. . . . 5
⊢
(DECID ∀𝑥 ∈ 𝑦 𝜑 → (DECID ∀𝑥 ∈ {𝑧}𝜑 → DECID (∀𝑥 ∈ 𝑦 𝜑 ∧ ∀𝑥 ∈ {𝑧}𝜑))) |
29 | 14, 27, 28 | sylc 62 |
. . . 4
⊢
(((((𝐴 ∈ Fin
∧ ∀𝑥 ∈
𝐴 DECID
𝜑) ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ DECID ∀𝑥 ∈ 𝑦 𝜑) → DECID (∀𝑥 ∈ 𝑦 𝜑 ∧ ∀𝑥 ∈ {𝑧}𝜑)) |
30 | | ralunb 3301 |
. . . . 5
⊢
(∀𝑥 ∈
(𝑦 ∪ {𝑧})𝜑 ↔ (∀𝑥 ∈ 𝑦 𝜑 ∧ ∀𝑥 ∈ {𝑧}𝜑)) |
31 | 30 | dcbii 830 |
. . . 4
⊢
(DECID ∀𝑥 ∈ (𝑦 ∪ {𝑧})𝜑 ↔ DECID (∀𝑥 ∈ 𝑦 𝜑 ∧ ∀𝑥 ∈ {𝑧}𝜑)) |
32 | 29, 31 | sylibr 133 |
. . 3
⊢
(((((𝐴 ∈ Fin
∧ ∀𝑥 ∈
𝐴 DECID
𝜑) ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ DECID ∀𝑥 ∈ 𝑦 𝜑) → DECID ∀𝑥 ∈ (𝑦 ∪ {𝑧})𝜑) |
33 | 32 | ex 114 |
. 2
⊢ ((((𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 DECID 𝜑) ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → (DECID
∀𝑥 ∈ 𝑦 𝜑 → DECID ∀𝑥 ∈ (𝑦 ∪ {𝑧})𝜑)) |
34 | | simpl 108 |
. 2
⊢ ((𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 DECID 𝜑) → 𝐴 ∈ Fin) |
35 | 2, 4, 6, 8, 13, 33, 34 | findcard2sd 6852 |
1
⊢ ((𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 DECID 𝜑) → DECID ∀𝑥 ∈ 𝐴 𝜑) |