Proof of Theorem bnj1533
Step | Hyp | Ref
| Expression |
1 | | bnj1533.1 |
. . . 4
⊢ (𝜃 → ∀𝑧 ∈ 𝐵 ¬ 𝑧 ∈ 𝐷) |
2 | 1 | bnj1211 30122 |
. . 3
⊢ (𝜃 → ∀𝑧(𝑧 ∈ 𝐵 → ¬ 𝑧 ∈ 𝐷)) |
3 | | bnj1533.3 |
. . . . . . . . 9
⊢ 𝐷 = {𝑧 ∈ 𝐴 ∣ 𝐶 ≠ 𝐸} |
4 | 3 | rabeq2i 3170 |
. . . . . . . 8
⊢ (𝑧 ∈ 𝐷 ↔ (𝑧 ∈ 𝐴 ∧ 𝐶 ≠ 𝐸)) |
5 | 4 | notbii 309 |
. . . . . . 7
⊢ (¬
𝑧 ∈ 𝐷 ↔ ¬ (𝑧 ∈ 𝐴 ∧ 𝐶 ≠ 𝐸)) |
6 | | imnan 437 |
. . . . . . 7
⊢ ((𝑧 ∈ 𝐴 → ¬ 𝐶 ≠ 𝐸) ↔ ¬ (𝑧 ∈ 𝐴 ∧ 𝐶 ≠ 𝐸)) |
7 | | nne 2786 |
. . . . . . . 8
⊢ (¬
𝐶 ≠ 𝐸 ↔ 𝐶 = 𝐸) |
8 | 7 | imbi2i 325 |
. . . . . . 7
⊢ ((𝑧 ∈ 𝐴 → ¬ 𝐶 ≠ 𝐸) ↔ (𝑧 ∈ 𝐴 → 𝐶 = 𝐸)) |
9 | 5, 6, 8 | 3bitr2i 287 |
. . . . . 6
⊢ (¬
𝑧 ∈ 𝐷 ↔ (𝑧 ∈ 𝐴 → 𝐶 = 𝐸)) |
10 | 9 | imbi2i 325 |
. . . . 5
⊢ ((𝑧 ∈ 𝐵 → ¬ 𝑧 ∈ 𝐷) ↔ (𝑧 ∈ 𝐵 → (𝑧 ∈ 𝐴 → 𝐶 = 𝐸))) |
11 | | bnj1533.2 |
. . . . . . . 8
⊢ 𝐵 ⊆ 𝐴 |
12 | 11 | sseli 3564 |
. . . . . . 7
⊢ (𝑧 ∈ 𝐵 → 𝑧 ∈ 𝐴) |
13 | 12 | imim1i 61 |
. . . . . 6
⊢ ((𝑧 ∈ 𝐴 → 𝐶 = 𝐸) → (𝑧 ∈ 𝐵 → 𝐶 = 𝐸)) |
14 | | ax-1 6 |
. . . . . . . . . 10
⊢ ((𝑧 ∈ 𝐴 → 𝐶 = 𝐸) → (𝑧 ∈ 𝐵 → (𝑧 ∈ 𝐴 → 𝐶 = 𝐸))) |
15 | 14 | anim1i 590 |
. . . . . . . . 9
⊢ (((𝑧 ∈ 𝐴 → 𝐶 = 𝐸) ∧ 𝑧 ∈ 𝐵) → ((𝑧 ∈ 𝐵 → (𝑧 ∈ 𝐴 → 𝐶 = 𝐸)) ∧ 𝑧 ∈ 𝐵)) |
16 | | simpr 476 |
. . . . . . . . . . 11
⊢ (((𝑧 ∈ 𝐵 → (𝑧 ∈ 𝐴 → 𝐶 = 𝐸)) ∧ 𝑧 ∈ 𝐵) → 𝑧 ∈ 𝐵) |
17 | | simpl 472 |
. . . . . . . . . . 11
⊢ (((𝑧 ∈ 𝐵 → (𝑧 ∈ 𝐴 → 𝐶 = 𝐸)) ∧ 𝑧 ∈ 𝐵) → (𝑧 ∈ 𝐵 → (𝑧 ∈ 𝐴 → 𝐶 = 𝐸))) |
18 | 16, 17 | mpd 15 |
. . . . . . . . . 10
⊢ (((𝑧 ∈ 𝐵 → (𝑧 ∈ 𝐴 → 𝐶 = 𝐸)) ∧ 𝑧 ∈ 𝐵) → (𝑧 ∈ 𝐴 → 𝐶 = 𝐸)) |
19 | 18, 16 | jca 553 |
. . . . . . . . 9
⊢ (((𝑧 ∈ 𝐵 → (𝑧 ∈ 𝐴 → 𝐶 = 𝐸)) ∧ 𝑧 ∈ 𝐵) → ((𝑧 ∈ 𝐴 → 𝐶 = 𝐸) ∧ 𝑧 ∈ 𝐵)) |
20 | 15, 19 | impbii 198 |
. . . . . . . 8
⊢ (((𝑧 ∈ 𝐴 → 𝐶 = 𝐸) ∧ 𝑧 ∈ 𝐵) ↔ ((𝑧 ∈ 𝐵 → (𝑧 ∈ 𝐴 → 𝐶 = 𝐸)) ∧ 𝑧 ∈ 𝐵)) |
21 | 20 | imbi1i 338 |
. . . . . . 7
⊢ ((((𝑧 ∈ 𝐴 → 𝐶 = 𝐸) ∧ 𝑧 ∈ 𝐵) → 𝐶 = 𝐸) ↔ (((𝑧 ∈ 𝐵 → (𝑧 ∈ 𝐴 → 𝐶 = 𝐸)) ∧ 𝑧 ∈ 𝐵) → 𝐶 = 𝐸)) |
22 | | impexp 461 |
. . . . . . 7
⊢ ((((𝑧 ∈ 𝐴 → 𝐶 = 𝐸) ∧ 𝑧 ∈ 𝐵) → 𝐶 = 𝐸) ↔ ((𝑧 ∈ 𝐴 → 𝐶 = 𝐸) → (𝑧 ∈ 𝐵 → 𝐶 = 𝐸))) |
23 | | impexp 461 |
. . . . . . 7
⊢ ((((𝑧 ∈ 𝐵 → (𝑧 ∈ 𝐴 → 𝐶 = 𝐸)) ∧ 𝑧 ∈ 𝐵) → 𝐶 = 𝐸) ↔ ((𝑧 ∈ 𝐵 → (𝑧 ∈ 𝐴 → 𝐶 = 𝐸)) → (𝑧 ∈ 𝐵 → 𝐶 = 𝐸))) |
24 | 21, 22, 23 | 3bitr3i 289 |
. . . . . 6
⊢ (((𝑧 ∈ 𝐴 → 𝐶 = 𝐸) → (𝑧 ∈ 𝐵 → 𝐶 = 𝐸)) ↔ ((𝑧 ∈ 𝐵 → (𝑧 ∈ 𝐴 → 𝐶 = 𝐸)) → (𝑧 ∈ 𝐵 → 𝐶 = 𝐸))) |
25 | 13, 24 | mpbi 219 |
. . . . 5
⊢ ((𝑧 ∈ 𝐵 → (𝑧 ∈ 𝐴 → 𝐶 = 𝐸)) → (𝑧 ∈ 𝐵 → 𝐶 = 𝐸)) |
26 | 10, 25 | sylbi 206 |
. . . 4
⊢ ((𝑧 ∈ 𝐵 → ¬ 𝑧 ∈ 𝐷) → (𝑧 ∈ 𝐵 → 𝐶 = 𝐸)) |
27 | 26 | alimi 1730 |
. . 3
⊢
(∀𝑧(𝑧 ∈ 𝐵 → ¬ 𝑧 ∈ 𝐷) → ∀𝑧(𝑧 ∈ 𝐵 → 𝐶 = 𝐸)) |
28 | 2, 27 | syl 17 |
. 2
⊢ (𝜃 → ∀𝑧(𝑧 ∈ 𝐵 → 𝐶 = 𝐸)) |
29 | 28 | bnj1142 30114 |
1
⊢ (𝜃 → ∀𝑧 ∈ 𝐵 𝐶 = 𝐸) |