Step | Hyp | Ref
| Expression |
1 | | relres 5346 |
. 2
⊢ Rel ( I
↾ {𝐴}) |
2 | | relxp 5150 |
. 2
⊢ Rel
({𝐴} × {𝐴}) |
3 | | df-br 4584 |
. . . . . 6
⊢ (𝑥 I 𝑦 ↔ 〈𝑥, 𝑦〉 ∈ I ) |
4 | 3 | bicomi 213 |
. . . . 5
⊢
(〈𝑥, 𝑦〉 ∈ I ↔ 𝑥 I 𝑦) |
5 | 4 | anbi1i 727 |
. . . 4
⊢
((〈𝑥, 𝑦〉 ∈ I ∧ 𝑥 ∈ {𝐴}) ↔ (𝑥 I 𝑦 ∧ 𝑥 ∈ {𝐴})) |
6 | | simpr 476 |
. . . . . 6
⊢ ((𝑥 I 𝑦 ∧ 𝑥 ∈ {𝐴}) → 𝑥 ∈ {𝐴}) |
7 | | velsn 4141 |
. . . . . . . 8
⊢ (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴) |
8 | | vex 3176 |
. . . . . . . . . 10
⊢ 𝑦 ∈ V |
9 | | ideqg 5195 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ V → (𝑥 I 𝑦 ↔ 𝑥 = 𝑦)) |
10 | 9 | biimpd 218 |
. . . . . . . . . 10
⊢ (𝑦 ∈ V → (𝑥 I 𝑦 → 𝑥 = 𝑦)) |
11 | 8, 10 | ax-mp 5 |
. . . . . . . . 9
⊢ (𝑥 I 𝑦 → 𝑥 = 𝑦) |
12 | | eqtr2 2630 |
. . . . . . . . . . 11
⊢ ((𝑥 = 𝑦 ∧ 𝑥 = 𝐴) → 𝑦 = 𝐴) |
13 | 12 | ex 449 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → (𝑥 = 𝐴 → 𝑦 = 𝐴)) |
14 | | velsn 4141 |
. . . . . . . . . 10
⊢ (𝑦 ∈ {𝐴} ↔ 𝑦 = 𝐴) |
15 | 13, 14 | syl6ibr 241 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → (𝑥 = 𝐴 → 𝑦 ∈ {𝐴})) |
16 | 11, 15 | syl 17 |
. . . . . . . 8
⊢ (𝑥 I 𝑦 → (𝑥 = 𝐴 → 𝑦 ∈ {𝐴})) |
17 | 7, 16 | syl5bi 231 |
. . . . . . 7
⊢ (𝑥 I 𝑦 → (𝑥 ∈ {𝐴} → 𝑦 ∈ {𝐴})) |
18 | 17 | imp 444 |
. . . . . 6
⊢ ((𝑥 I 𝑦 ∧ 𝑥 ∈ {𝐴}) → 𝑦 ∈ {𝐴}) |
19 | 6, 18 | jca 553 |
. . . . 5
⊢ ((𝑥 I 𝑦 ∧ 𝑥 ∈ {𝐴}) → (𝑥 ∈ {𝐴} ∧ 𝑦 ∈ {𝐴})) |
20 | | eqtr3 2631 |
. . . . . . . . . . . 12
⊢ ((𝑦 = 𝐴 ∧ 𝑥 = 𝐴) → 𝑦 = 𝑥) |
21 | 8 | ideq 5196 |
. . . . . . . . . . . . 13
⊢ (𝑥 I 𝑦 ↔ 𝑥 = 𝑦) |
22 | | equcom 1932 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑦 ↔ 𝑦 = 𝑥) |
23 | 21, 22 | bitri 263 |
. . . . . . . . . . . 12
⊢ (𝑥 I 𝑦 ↔ 𝑦 = 𝑥) |
24 | 20, 23 | sylibr 223 |
. . . . . . . . . . 11
⊢ ((𝑦 = 𝐴 ∧ 𝑥 = 𝐴) → 𝑥 I 𝑦) |
25 | 24 | ex 449 |
. . . . . . . . . 10
⊢ (𝑦 = 𝐴 → (𝑥 = 𝐴 → 𝑥 I 𝑦)) |
26 | 14, 25 | sylbi 206 |
. . . . . . . . 9
⊢ (𝑦 ∈ {𝐴} → (𝑥 = 𝐴 → 𝑥 I 𝑦)) |
27 | 26 | com12 32 |
. . . . . . . 8
⊢ (𝑥 = 𝐴 → (𝑦 ∈ {𝐴} → 𝑥 I 𝑦)) |
28 | 7, 27 | sylbi 206 |
. . . . . . 7
⊢ (𝑥 ∈ {𝐴} → (𝑦 ∈ {𝐴} → 𝑥 I 𝑦)) |
29 | 28 | imp 444 |
. . . . . 6
⊢ ((𝑥 ∈ {𝐴} ∧ 𝑦 ∈ {𝐴}) → 𝑥 I 𝑦) |
30 | | simpl 472 |
. . . . . 6
⊢ ((𝑥 ∈ {𝐴} ∧ 𝑦 ∈ {𝐴}) → 𝑥 ∈ {𝐴}) |
31 | 29, 30 | jca 553 |
. . . . 5
⊢ ((𝑥 ∈ {𝐴} ∧ 𝑦 ∈ {𝐴}) → (𝑥 I 𝑦 ∧ 𝑥 ∈ {𝐴})) |
32 | 19, 31 | impbii 198 |
. . . 4
⊢ ((𝑥 I 𝑦 ∧ 𝑥 ∈ {𝐴}) ↔ (𝑥 ∈ {𝐴} ∧ 𝑦 ∈ {𝐴})) |
33 | 5, 32 | bitri 263 |
. . 3
⊢
((〈𝑥, 𝑦〉 ∈ I ∧ 𝑥 ∈ {𝐴}) ↔ (𝑥 ∈ {𝐴} ∧ 𝑦 ∈ {𝐴})) |
34 | 8 | opelres 5322 |
. . 3
⊢
(〈𝑥, 𝑦〉 ∈ ( I ↾ {𝐴}) ↔ (〈𝑥, 𝑦〉 ∈ I ∧ 𝑥 ∈ {𝐴})) |
35 | | opelxp 5070 |
. . 3
⊢
(〈𝑥, 𝑦〉 ∈ ({𝐴} × {𝐴}) ↔ (𝑥 ∈ {𝐴} ∧ 𝑦 ∈ {𝐴})) |
36 | 33, 34, 35 | 3bitr4i 291 |
. 2
⊢
(〈𝑥, 𝑦〉 ∈ ( I ↾ {𝐴}) ↔ 〈𝑥, 𝑦〉 ∈ ({𝐴} × {𝐴})) |
37 | 1, 2, 36 | eqrelriiv 5137 |
1
⊢ ( I
↾ {𝐴}) = ({𝐴} × {𝐴}) |