Step | Hyp | Ref
| Expression |
1 | | bj-imdirid.ex |
. . 3
⊢ (𝜑 → 𝐴 ∈ 𝑈) |
2 | | idssxp 5916 |
. . . 4
⊢ ( I
↾ 𝐴) ⊆ (𝐴 × 𝐴) |
3 | 2 | a1i 11 |
. . 3
⊢ (𝜑 → ( I ↾ 𝐴) ⊆ (𝐴 × 𝐴)) |
4 | 1, 1, 3 | bj-imdirval2 34476 |
. 2
⊢ (𝜑 → ((𝐴𝒫*𝐴)‘( I ↾ 𝐴)) = {〈𝑥, 𝑦〉 ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐴) ∧ (( I ↾ 𝐴) “ 𝑥) = 𝑦)}) |
5 | | resiima 5944 |
. . . . . . . 8
⊢ (𝑥 ⊆ 𝐴 → (( I ↾ 𝐴) “ 𝑥) = 𝑥) |
6 | 5 | ad2antrl 726 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐴)) → (( I ↾ 𝐴) “ 𝑥) = 𝑥) |
7 | 6 | eqeq1d 2823 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐴)) → ((( I ↾ 𝐴) “ 𝑥) = 𝑦 ↔ 𝑥 = 𝑦)) |
8 | 7 | pm5.32da 581 |
. . . . 5
⊢ (𝜑 → (((𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐴) ∧ (( I ↾ 𝐴) “ 𝑥) = 𝑦) ↔ ((𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐴) ∧ 𝑥 = 𝑦))) |
9 | | anass 471 |
. . . . 5
⊢ (((𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐴) ∧ 𝑥 = 𝑦) ↔ (𝑥 ⊆ 𝐴 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑥 = 𝑦))) |
10 | 8, 9 | syl6bb 289 |
. . . 4
⊢ (𝜑 → (((𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐴) ∧ (( I ↾ 𝐴) “ 𝑥) = 𝑦) ↔ (𝑥 ⊆ 𝐴 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑥 = 𝑦)))) |
11 | | simpr 487 |
. . . . . . . 8
⊢ ((𝑦 ⊆ 𝐴 ∧ 𝑥 = 𝑦) → 𝑥 = 𝑦) |
12 | | sseq1 3992 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → (𝑥 ⊆ 𝐴 ↔ 𝑦 ⊆ 𝐴)) |
13 | 12 | biimpcd 251 |
. . . . . . . . 9
⊢ (𝑥 ⊆ 𝐴 → (𝑥 = 𝑦 → 𝑦 ⊆ 𝐴)) |
14 | 13 | ancrd 554 |
. . . . . . . 8
⊢ (𝑥 ⊆ 𝐴 → (𝑥 = 𝑦 → (𝑦 ⊆ 𝐴 ∧ 𝑥 = 𝑦))) |
15 | 11, 14 | impbid2 228 |
. . . . . . 7
⊢ (𝑥 ⊆ 𝐴 → ((𝑦 ⊆ 𝐴 ∧ 𝑥 = 𝑦) ↔ 𝑥 = 𝑦)) |
16 | 15 | pm5.32i 577 |
. . . . . 6
⊢ ((𝑥 ⊆ 𝐴 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑥 = 𝑦)) ↔ (𝑥 ⊆ 𝐴 ∧ 𝑥 = 𝑦)) |
17 | 16 | a1i 11 |
. . . . 5
⊢ (𝜑 → ((𝑥 ⊆ 𝐴 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑥 = 𝑦)) ↔ (𝑥 ⊆ 𝐴 ∧ 𝑥 = 𝑦))) |
18 | | velpw 4544 |
. . . . . 6
⊢ (𝑥 ∈ 𝒫 𝐴 ↔ 𝑥 ⊆ 𝐴) |
19 | | vex 3497 |
. . . . . . 7
⊢ 𝑦 ∈ V |
20 | 19 | ideq 5723 |
. . . . . 6
⊢ (𝑥 I 𝑦 ↔ 𝑥 = 𝑦) |
21 | 18, 20 | anbi12i 628 |
. . . . 5
⊢ ((𝑥 ∈ 𝒫 𝐴 ∧ 𝑥 I 𝑦) ↔ (𝑥 ⊆ 𝐴 ∧ 𝑥 = 𝑦)) |
22 | 17, 21 | syl6bbr 291 |
. . . 4
⊢ (𝜑 → ((𝑥 ⊆ 𝐴 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑥 = 𝑦)) ↔ (𝑥 ∈ 𝒫 𝐴 ∧ 𝑥 I 𝑦))) |
23 | 10, 22 | bitrd 281 |
. . 3
⊢ (𝜑 → (((𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐴) ∧ (( I ↾ 𝐴) “ 𝑥) = 𝑦) ↔ (𝑥 ∈ 𝒫 𝐴 ∧ 𝑥 I 𝑦))) |
24 | 23 | opabbidv 5132 |
. 2
⊢ (𝜑 → {〈𝑥, 𝑦〉 ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐴) ∧ (( I ↾ 𝐴) “ 𝑥) = 𝑦)} = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝒫 𝐴 ∧ 𝑥 I 𝑦)}) |
25 | | dfres2 5909 |
. . 3
⊢ ( I
↾ 𝒫 𝐴) =
{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝒫 𝐴 ∧ 𝑥 I 𝑦)} |
26 | | eqidd 2822 |
. . 3
⊢ (𝜑 → ( I ↾ 𝒫
𝐴) = ( I ↾ 𝒫
𝐴)) |
27 | 25, 26 | syl5eqr 2870 |
. 2
⊢ (𝜑 → {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝒫 𝐴 ∧ 𝑥 I 𝑦)} = ( I ↾ 𝒫 𝐴)) |
28 | 4, 24, 27 | 3eqtrd 2860 |
1
⊢ (𝜑 → ((𝐴𝒫*𝐴)‘( I ↾ 𝐴)) = ( I ↾ 𝒫 𝐴)) |