Proof of Theorem bnj1171
Step | Hyp | Ref
| Expression |
1 | | bnj1171.129 |
. 2
⊢
∃𝑧∀𝑤((𝜑 ∧ 𝜓) → (𝑧 ∈ 𝐵 ∧ (𝑤 ∈ 𝐴 → (𝑤𝑅𝑧 → ¬ 𝑤 ∈ 𝐵)))) |
2 | | bnj1171.13 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝜓) → 𝐵 ⊆ 𝐴) |
3 | 2 | sseld 3924 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝜓) → (𝑤 ∈ 𝐵 → 𝑤 ∈ 𝐴)) |
4 | 3 | pm4.71rd 562 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝜓) → (𝑤 ∈ 𝐵 ↔ (𝑤 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵))) |
5 | 4 | imbi1d 341 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝜓) → ((𝑤 ∈ 𝐵 → ¬ 𝑤𝑅𝑧) ↔ ((𝑤 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵) → ¬ 𝑤𝑅𝑧))) |
6 | | impexp 450 |
. . . . . . . 8
⊢ (((𝑤 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵) → ¬ 𝑤𝑅𝑧) ↔ (𝑤 ∈ 𝐴 → (𝑤 ∈ 𝐵 → ¬ 𝑤𝑅𝑧))) |
7 | 5, 6 | bitrdi 286 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝜓) → ((𝑤 ∈ 𝐵 → ¬ 𝑤𝑅𝑧) ↔ (𝑤 ∈ 𝐴 → (𝑤 ∈ 𝐵 → ¬ 𝑤𝑅𝑧)))) |
8 | | con2b 359 |
. . . . . . . 8
⊢ ((𝑤𝑅𝑧 → ¬ 𝑤 ∈ 𝐵) ↔ (𝑤 ∈ 𝐵 → ¬ 𝑤𝑅𝑧)) |
9 | 8 | imbi2i 335 |
. . . . . . 7
⊢ ((𝑤 ∈ 𝐴 → (𝑤𝑅𝑧 → ¬ 𝑤 ∈ 𝐵)) ↔ (𝑤 ∈ 𝐴 → (𝑤 ∈ 𝐵 → ¬ 𝑤𝑅𝑧))) |
10 | 7, 9 | bitr4di 288 |
. . . . . 6
⊢ ((𝜑 ∧ 𝜓) → ((𝑤 ∈ 𝐵 → ¬ 𝑤𝑅𝑧) ↔ (𝑤 ∈ 𝐴 → (𝑤𝑅𝑧 → ¬ 𝑤 ∈ 𝐵)))) |
11 | 10 | anbi2d 628 |
. . . . 5
⊢ ((𝜑 ∧ 𝜓) → ((𝑧 ∈ 𝐵 ∧ (𝑤 ∈ 𝐵 → ¬ 𝑤𝑅𝑧)) ↔ (𝑧 ∈ 𝐵 ∧ (𝑤 ∈ 𝐴 → (𝑤𝑅𝑧 → ¬ 𝑤 ∈ 𝐵))))) |
12 | 11 | pm5.74i 270 |
. . . 4
⊢ (((𝜑 ∧ 𝜓) → (𝑧 ∈ 𝐵 ∧ (𝑤 ∈ 𝐵 → ¬ 𝑤𝑅𝑧))) ↔ ((𝜑 ∧ 𝜓) → (𝑧 ∈ 𝐵 ∧ (𝑤 ∈ 𝐴 → (𝑤𝑅𝑧 → ¬ 𝑤 ∈ 𝐵))))) |
13 | 12 | albii 1825 |
. . 3
⊢
(∀𝑤((𝜑 ∧ 𝜓) → (𝑧 ∈ 𝐵 ∧ (𝑤 ∈ 𝐵 → ¬ 𝑤𝑅𝑧))) ↔ ∀𝑤((𝜑 ∧ 𝜓) → (𝑧 ∈ 𝐵 ∧ (𝑤 ∈ 𝐴 → (𝑤𝑅𝑧 → ¬ 𝑤 ∈ 𝐵))))) |
14 | 13 | exbii 1853 |
. 2
⊢
(∃𝑧∀𝑤((𝜑 ∧ 𝜓) → (𝑧 ∈ 𝐵 ∧ (𝑤 ∈ 𝐵 → ¬ 𝑤𝑅𝑧))) ↔ ∃𝑧∀𝑤((𝜑 ∧ 𝜓) → (𝑧 ∈ 𝐵 ∧ (𝑤 ∈ 𝐴 → (𝑤𝑅𝑧 → ¬ 𝑤 ∈ 𝐵))))) |
15 | 1, 14 | mpbir 230 |
1
⊢
∃𝑧∀𝑤((𝜑 ∧ 𝜓) → (𝑧 ∈ 𝐵 ∧ (𝑤 ∈ 𝐵 → ¬ 𝑤𝑅𝑧))) |