Proof of Theorem bj-imdiridlem
| Step | Hyp | Ref
| Expression |
| 1 | | bj-imdiridlem.1 |
. . . . . . . 8
⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐴) → (𝜑 ↔ 𝑥 = 𝑦)) |
| 2 | 1 | biimp3a 1471 |
. . . . . . 7
⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ 𝜑) → 𝑥 = 𝑦) |
| 3 | 2 | 3expib 1123 |
. . . . . 6
⊢ (𝑥 ⊆ 𝐴 → ((𝑦 ⊆ 𝐴 ∧ 𝜑) → 𝑥 = 𝑦)) |
| 4 | | equcomi 2016 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → 𝑦 = 𝑥) |
| 5 | 4 | sseq1d 4015 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → (𝑦 ⊆ 𝐴 ↔ 𝑥 ⊆ 𝐴)) |
| 6 | 5 | biimparc 479 |
. . . . . . . 8
⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑥 = 𝑦) → 𝑦 ⊆ 𝐴) |
| 7 | | simpr 484 |
. . . . . . . . 9
⊢ (((𝑥 ⊆ 𝐴 ∧ 𝑥 = 𝑦) ∧ 𝑦 ⊆ 𝐴) → 𝑦 ⊆ 𝐴) |
| 8 | 1 | biimpar 477 |
. . . . . . . . . 10
⊢ (((𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐴) ∧ 𝑥 = 𝑦) → 𝜑) |
| 9 | 8 | an32s 652 |
. . . . . . . . 9
⊢ (((𝑥 ⊆ 𝐴 ∧ 𝑥 = 𝑦) ∧ 𝑦 ⊆ 𝐴) → 𝜑) |
| 10 | 7, 9 | jca 511 |
. . . . . . . 8
⊢ (((𝑥 ⊆ 𝐴 ∧ 𝑥 = 𝑦) ∧ 𝑦 ⊆ 𝐴) → (𝑦 ⊆ 𝐴 ∧ 𝜑)) |
| 11 | 6, 10 | mpdan 687 |
. . . . . . 7
⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑥 = 𝑦) → (𝑦 ⊆ 𝐴 ∧ 𝜑)) |
| 12 | 11 | ex 412 |
. . . . . 6
⊢ (𝑥 ⊆ 𝐴 → (𝑥 = 𝑦 → (𝑦 ⊆ 𝐴 ∧ 𝜑))) |
| 13 | 3, 12 | impbid 212 |
. . . . 5
⊢ (𝑥 ⊆ 𝐴 → ((𝑦 ⊆ 𝐴 ∧ 𝜑) ↔ 𝑥 = 𝑦)) |
| 14 | 13 | pm5.32i 574 |
. . . 4
⊢ ((𝑥 ⊆ 𝐴 ∧ (𝑦 ⊆ 𝐴 ∧ 𝜑)) ↔ (𝑥 ⊆ 𝐴 ∧ 𝑥 = 𝑦)) |
| 15 | | anass 468 |
. . . 4
⊢ (((𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐴) ∧ 𝜑) ↔ (𝑥 ⊆ 𝐴 ∧ (𝑦 ⊆ 𝐴 ∧ 𝜑))) |
| 16 | | velpw 4605 |
. . . . 5
⊢ (𝑥 ∈ 𝒫 𝐴 ↔ 𝑥 ⊆ 𝐴) |
| 17 | | vex 3484 |
. . . . . 6
⊢ 𝑦 ∈ V |
| 18 | 17 | ideq 5863 |
. . . . 5
⊢ (𝑥 I 𝑦 ↔ 𝑥 = 𝑦) |
| 19 | 16, 18 | anbi12i 628 |
. . . 4
⊢ ((𝑥 ∈ 𝒫 𝐴 ∧ 𝑥 I 𝑦) ↔ (𝑥 ⊆ 𝐴 ∧ 𝑥 = 𝑦)) |
| 20 | 14, 15, 19 | 3bitr4i 303 |
. . 3
⊢ (((𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐴) ∧ 𝜑) ↔ (𝑥 ∈ 𝒫 𝐴 ∧ 𝑥 I 𝑦)) |
| 21 | 20 | opabbii 5210 |
. 2
⊢
{〈𝑥, 𝑦〉 ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐴) ∧ 𝜑)} = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝒫 𝐴 ∧ 𝑥 I 𝑦)} |
| 22 | | dfres2 6059 |
. 2
⊢ ( I
↾ 𝒫 𝐴) =
{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝒫 𝐴 ∧ 𝑥 I 𝑦)} |
| 23 | 21, 22 | eqtr4i 2768 |
1
⊢
{〈𝑥, 𝑦〉 ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐴) ∧ 𝜑)} = ( I ↾ 𝒫 𝐴) |