Proof of Theorem bj-imdiridlem
Step | Hyp | Ref
| Expression |
1 | | bj-imdiridlem.1 |
. . . . . . . 8
⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐴) → (𝜑 ↔ 𝑥 = 𝑦)) |
2 | 1 | biimp3a 1467 |
. . . . . . 7
⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ 𝜑) → 𝑥 = 𝑦) |
3 | 2 | 3expib 1120 |
. . . . . 6
⊢ (𝑥 ⊆ 𝐴 → ((𝑦 ⊆ 𝐴 ∧ 𝜑) → 𝑥 = 𝑦)) |
4 | | equcomi 2025 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → 𝑦 = 𝑥) |
5 | 4 | sseq1d 3919 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → (𝑦 ⊆ 𝐴 ↔ 𝑥 ⊆ 𝐴)) |
6 | 5 | biimparc 484 |
. . . . . . . 8
⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑥 = 𝑦) → 𝑦 ⊆ 𝐴) |
7 | | simpr 489 |
. . . . . . . . 9
⊢ (((𝑥 ⊆ 𝐴 ∧ 𝑥 = 𝑦) ∧ 𝑦 ⊆ 𝐴) → 𝑦 ⊆ 𝐴) |
8 | 1 | biimpar 482 |
. . . . . . . . . 10
⊢ (((𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐴) ∧ 𝑥 = 𝑦) → 𝜑) |
9 | 8 | an32s 652 |
. . . . . . . . 9
⊢ (((𝑥 ⊆ 𝐴 ∧ 𝑥 = 𝑦) ∧ 𝑦 ⊆ 𝐴) → 𝜑) |
10 | 7, 9 | jca 516 |
. . . . . . . 8
⊢ (((𝑥 ⊆ 𝐴 ∧ 𝑥 = 𝑦) ∧ 𝑦 ⊆ 𝐴) → (𝑦 ⊆ 𝐴 ∧ 𝜑)) |
11 | 6, 10 | mpdan 687 |
. . . . . . 7
⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑥 = 𝑦) → (𝑦 ⊆ 𝐴 ∧ 𝜑)) |
12 | 11 | ex 417 |
. . . . . 6
⊢ (𝑥 ⊆ 𝐴 → (𝑥 = 𝑦 → (𝑦 ⊆ 𝐴 ∧ 𝜑))) |
13 | 3, 12 | impbid 215 |
. . . . 5
⊢ (𝑥 ⊆ 𝐴 → ((𝑦 ⊆ 𝐴 ∧ 𝜑) ↔ 𝑥 = 𝑦)) |
14 | 13 | pm5.32i 579 |
. . . 4
⊢ ((𝑥 ⊆ 𝐴 ∧ (𝑦 ⊆ 𝐴 ∧ 𝜑)) ↔ (𝑥 ⊆ 𝐴 ∧ 𝑥 = 𝑦)) |
15 | | anass 473 |
. . . 4
⊢ (((𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐴) ∧ 𝜑) ↔ (𝑥 ⊆ 𝐴 ∧ (𝑦 ⊆ 𝐴 ∧ 𝜑))) |
16 | | velpw 4492 |
. . . . 5
⊢ (𝑥 ∈ 𝒫 𝐴 ↔ 𝑥 ⊆ 𝐴) |
17 | | vex 3411 |
. . . . . 6
⊢ 𝑦 ∈ V |
18 | 17 | ideq 5685 |
. . . . 5
⊢ (𝑥 I 𝑦 ↔ 𝑥 = 𝑦) |
19 | 16, 18 | anbi12i 630 |
. . . 4
⊢ ((𝑥 ∈ 𝒫 𝐴 ∧ 𝑥 I 𝑦) ↔ (𝑥 ⊆ 𝐴 ∧ 𝑥 = 𝑦)) |
20 | 14, 15, 19 | 3bitr4i 307 |
. . 3
⊢ (((𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐴) ∧ 𝜑) ↔ (𝑥 ∈ 𝒫 𝐴 ∧ 𝑥 I 𝑦)) |
21 | 20 | opabbii 5092 |
. 2
⊢
{〈𝑥, 𝑦〉 ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐴) ∧ 𝜑)} = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝒫 𝐴 ∧ 𝑥 I 𝑦)} |
22 | | dfres2 5874 |
. 2
⊢ ( I
↾ 𝒫 𝐴) =
{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝒫 𝐴 ∧ 𝑥 I 𝑦)} |
23 | 21, 22 | eqtr4i 2785 |
1
⊢
{〈𝑥, 𝑦〉 ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐴) ∧ 𝜑)} = ( I ↾ 𝒫 𝐴) |