Proof of Theorem sbi1ALT
Step | Hyp | Ref
| Expression |
1 | | dfsb1.p5 |
. . . . . 6
⊢ (𝜃 ↔ ((𝑥 = 𝑦 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))) |
2 | 1 | sbequ2ALT 2580 |
. . . . 5
⊢ (𝑥 = 𝑦 → (𝜃 → 𝜑)) |
3 | | dfsb1.im |
. . . . . 6
⊢ (𝜂 ↔ ((𝑥 = 𝑦 → (𝜑 → 𝜓)) ∧ ∃𝑥(𝑥 = 𝑦 ∧ (𝜑 → 𝜓)))) |
4 | 3 | sbequ2ALT 2580 |
. . . . 5
⊢ (𝑥 = 𝑦 → (𝜂 → (𝜑 → 𝜓))) |
5 | 2, 4 | syl5d 73 |
. . . 4
⊢ (𝑥 = 𝑦 → (𝜂 → (𝜃 → 𝜓))) |
6 | | dfsb1.s2 |
. . . . 5
⊢ (𝜏 ↔ ((𝑥 = 𝑦 → 𝜓) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜓))) |
7 | 6 | sbequ1ALT 2579 |
. . . 4
⊢ (𝑥 = 𝑦 → (𝜓 → 𝜏)) |
8 | 5, 7 | syl6d 75 |
. . 3
⊢ (𝑥 = 𝑦 → (𝜂 → (𝜃 → 𝜏))) |
9 | 8 | sps 2184 |
. 2
⊢
(∀𝑥 𝑥 = 𝑦 → (𝜂 → (𝜃 → 𝜏))) |
10 | 1 | sb4ALT 2588 |
. . 3
⊢ (¬
∀𝑥 𝑥 = 𝑦 → (𝜃 → ∀𝑥(𝑥 = 𝑦 → 𝜑))) |
11 | 3 | sb4ALT 2588 |
. . . 4
⊢ (¬
∀𝑥 𝑥 = 𝑦 → (𝜂 → ∀𝑥(𝑥 = 𝑦 → (𝜑 → 𝜓)))) |
12 | | ax-2 7 |
. . . . . 6
⊢ ((𝑥 = 𝑦 → (𝜑 → 𝜓)) → ((𝑥 = 𝑦 → 𝜑) → (𝑥 = 𝑦 → 𝜓))) |
13 | 12 | al2imi 1816 |
. . . . 5
⊢
(∀𝑥(𝑥 = 𝑦 → (𝜑 → 𝜓)) → (∀𝑥(𝑥 = 𝑦 → 𝜑) → ∀𝑥(𝑥 = 𝑦 → 𝜓))) |
14 | 6 | sb2ALT 2587 |
. . . . 5
⊢
(∀𝑥(𝑥 = 𝑦 → 𝜓) → 𝜏) |
15 | 13, 14 | syl6 35 |
. . . 4
⊢
(∀𝑥(𝑥 = 𝑦 → (𝜑 → 𝜓)) → (∀𝑥(𝑥 = 𝑦 → 𝜑) → 𝜏)) |
16 | 11, 15 | syl6 35 |
. . 3
⊢ (¬
∀𝑥 𝑥 = 𝑦 → (𝜂 → (∀𝑥(𝑥 = 𝑦 → 𝜑) → 𝜏))) |
17 | 10, 16 | syl5d 73 |
. 2
⊢ (¬
∀𝑥 𝑥 = 𝑦 → (𝜂 → (𝜃 → 𝜏))) |
18 | 9, 17 | pm2.61i 184 |
1
⊢ (𝜂 → (𝜃 → 𝜏)) |