Step | Hyp | Ref
| Expression |
1 | | ssel 3893 |
. . . . . . . . 9
⊢ (𝐴 ⊆ I → (〈𝑥, 𝑦〉 ∈ 𝐴 → 〈𝑥, 𝑦〉 ∈ I )) |
2 | | vex 3412 |
. . . . . . . . . 10
⊢ 𝑥 ∈ V |
3 | | vex 3412 |
. . . . . . . . . 10
⊢ 𝑦 ∈ V |
4 | 2, 3 | opeldm 5776 |
. . . . . . . . 9
⊢
(〈𝑥, 𝑦〉 ∈ 𝐴 → 𝑥 ∈ dom 𝐴) |
5 | 1, 4 | jca2 517 |
. . . . . . . 8
⊢ (𝐴 ⊆ I → (〈𝑥, 𝑦〉 ∈ 𝐴 → (〈𝑥, 𝑦〉 ∈ I ∧ 𝑥 ∈ dom 𝐴))) |
6 | 2, 3 | opelrn 5812 |
. . . . . . . . 9
⊢
(〈𝑥, 𝑦〉 ∈ 𝐴 → 𝑦 ∈ ran 𝐴) |
7 | 1, 6 | jca2 517 |
. . . . . . . 8
⊢ (𝐴 ⊆ I → (〈𝑥, 𝑦〉 ∈ 𝐴 → (〈𝑥, 𝑦〉 ∈ I ∧ 𝑦 ∈ ran 𝐴))) |
8 | 5, 7 | jcad 516 |
. . . . . . 7
⊢ (𝐴 ⊆ I → (〈𝑥, 𝑦〉 ∈ 𝐴 → ((〈𝑥, 𝑦〉 ∈ I ∧ 𝑥 ∈ dom 𝐴) ∧ (〈𝑥, 𝑦〉 ∈ I ∧ 𝑦 ∈ ran 𝐴)))) |
9 | | anandi 676 |
. . . . . . 7
⊢
((〈𝑥, 𝑦〉 ∈ I ∧ (𝑥 ∈ dom 𝐴 ∧ 𝑦 ∈ ran 𝐴)) ↔ ((〈𝑥, 𝑦〉 ∈ I ∧ 𝑥 ∈ dom 𝐴) ∧ (〈𝑥, 𝑦〉 ∈ I ∧ 𝑦 ∈ ran 𝐴))) |
10 | 8, 9 | syl6ibr 255 |
. . . . . 6
⊢ (𝐴 ⊆ I → (〈𝑥, 𝑦〉 ∈ 𝐴 → (〈𝑥, 𝑦〉 ∈ I ∧ (𝑥 ∈ dom 𝐴 ∧ 𝑦 ∈ ran 𝐴)))) |
11 | | df-br 5054 |
. . . . . . . . 9
⊢ (𝑥 I 𝑦 ↔ 〈𝑥, 𝑦〉 ∈ I ) |
12 | 3 | ideq 5721 |
. . . . . . . . 9
⊢ (𝑥 I 𝑦 ↔ 𝑥 = 𝑦) |
13 | 11, 12 | bitr3i 280 |
. . . . . . . 8
⊢
(〈𝑥, 𝑦〉 ∈ I ↔ 𝑥 = 𝑦) |
14 | 2 | eldm2 5770 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ dom 𝐴 ↔ ∃𝑦〈𝑥, 𝑦〉 ∈ 𝐴) |
15 | | opeq2 4785 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑦 → 〈𝑥, 𝑥〉 = 〈𝑥, 𝑦〉) |
16 | 15 | eleq1d 2822 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑦 → (〈𝑥, 𝑥〉 ∈ 𝐴 ↔ 〈𝑥, 𝑦〉 ∈ 𝐴)) |
17 | 16 | biimprcd 253 |
. . . . . . . . . . . . . . . 16
⊢
(〈𝑥, 𝑦〉 ∈ 𝐴 → (𝑥 = 𝑦 → 〈𝑥, 𝑥〉 ∈ 𝐴)) |
18 | 13, 17 | syl5bi 245 |
. . . . . . . . . . . . . . 15
⊢
(〈𝑥, 𝑦〉 ∈ 𝐴 → (〈𝑥, 𝑦〉 ∈ I → 〈𝑥, 𝑥〉 ∈ 𝐴)) |
19 | 1, 18 | sylcom 30 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ⊆ I → (〈𝑥, 𝑦〉 ∈ 𝐴 → 〈𝑥, 𝑥〉 ∈ 𝐴)) |
20 | 19 | exlimdv 1941 |
. . . . . . . . . . . . 13
⊢ (𝐴 ⊆ I → (∃𝑦〈𝑥, 𝑦〉 ∈ 𝐴 → 〈𝑥, 𝑥〉 ∈ 𝐴)) |
21 | 14, 20 | syl5bi 245 |
. . . . . . . . . . . 12
⊢ (𝐴 ⊆ I → (𝑥 ∈ dom 𝐴 → 〈𝑥, 𝑥〉 ∈ 𝐴)) |
22 | 16 | imbi2d 344 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 → ((𝑥 ∈ dom 𝐴 → 〈𝑥, 𝑥〉 ∈ 𝐴) ↔ (𝑥 ∈ dom 𝐴 → 〈𝑥, 𝑦〉 ∈ 𝐴))) |
23 | 21, 22 | syl5ibcom 248 |
. . . . . . . . . . 11
⊢ (𝐴 ⊆ I → (𝑥 = 𝑦 → (𝑥 ∈ dom 𝐴 → 〈𝑥, 𝑦〉 ∈ 𝐴))) |
24 | 23 | imp 410 |
. . . . . . . . . 10
⊢ ((𝐴 ⊆ I ∧ 𝑥 = 𝑦) → (𝑥 ∈ dom 𝐴 → 〈𝑥, 𝑦〉 ∈ 𝐴)) |
25 | 24 | adantrd 495 |
. . . . . . . . 9
⊢ ((𝐴 ⊆ I ∧ 𝑥 = 𝑦) → ((𝑥 ∈ dom 𝐴 ∧ 𝑦 ∈ ran 𝐴) → 〈𝑥, 𝑦〉 ∈ 𝐴)) |
26 | 25 | ex 416 |
. . . . . . . 8
⊢ (𝐴 ⊆ I → (𝑥 = 𝑦 → ((𝑥 ∈ dom 𝐴 ∧ 𝑦 ∈ ran 𝐴) → 〈𝑥, 𝑦〉 ∈ 𝐴))) |
27 | 13, 26 | syl5bi 245 |
. . . . . . 7
⊢ (𝐴 ⊆ I → (〈𝑥, 𝑦〉 ∈ I → ((𝑥 ∈ dom 𝐴 ∧ 𝑦 ∈ ran 𝐴) → 〈𝑥, 𝑦〉 ∈ 𝐴))) |
28 | 27 | impd 414 |
. . . . . 6
⊢ (𝐴 ⊆ I → ((〈𝑥, 𝑦〉 ∈ I ∧ (𝑥 ∈ dom 𝐴 ∧ 𝑦 ∈ ran 𝐴)) → 〈𝑥, 𝑦〉 ∈ 𝐴)) |
29 | 10, 28 | impbid 215 |
. . . . 5
⊢ (𝐴 ⊆ I → (〈𝑥, 𝑦〉 ∈ 𝐴 ↔ (〈𝑥, 𝑦〉 ∈ I ∧ (𝑥 ∈ dom 𝐴 ∧ 𝑦 ∈ ran 𝐴)))) |
30 | | opelinxp 5628 |
. . . . . 6
⊢
(〈𝑥, 𝑦〉 ∈ ( I ∩ (dom
𝐴 × ran 𝐴)) ↔ ((𝑥 ∈ dom 𝐴 ∧ 𝑦 ∈ ran 𝐴) ∧ 〈𝑥, 𝑦〉 ∈ I )) |
31 | 30 | biancomi 466 |
. . . . 5
⊢
(〈𝑥, 𝑦〉 ∈ ( I ∩ (dom
𝐴 × ran 𝐴)) ↔ (〈𝑥, 𝑦〉 ∈ I ∧ (𝑥 ∈ dom 𝐴 ∧ 𝑦 ∈ ran 𝐴))) |
32 | 29, 31 | bitr4di 292 |
. . . 4
⊢ (𝐴 ⊆ I → (〈𝑥, 𝑦〉 ∈ 𝐴 ↔ 〈𝑥, 𝑦〉 ∈ ( I ∩ (dom 𝐴 × ran 𝐴)))) |
33 | 32 | alrimivv 1936 |
. . 3
⊢ (𝐴 ⊆ I → ∀𝑥∀𝑦(〈𝑥, 𝑦〉 ∈ 𝐴 ↔ 〈𝑥, 𝑦〉 ∈ ( I ∩ (dom 𝐴 × ran 𝐴)))) |
34 | | reli 5696 |
. . . . 5
⊢ Rel
I |
35 | | relss 5653 |
. . . . 5
⊢ (𝐴 ⊆ I → (Rel I →
Rel 𝐴)) |
36 | 34, 35 | mpi 20 |
. . . 4
⊢ (𝐴 ⊆ I → Rel 𝐴) |
37 | | relinxp 5684 |
. . . 4
⊢ Rel ( I
∩ (dom 𝐴 × ran
𝐴)) |
38 | | eqrel 5655 |
. . . 4
⊢ ((Rel
𝐴 ∧ Rel ( I ∩ (dom
𝐴 × ran 𝐴))) → (𝐴 = ( I ∩ (dom 𝐴 × ran 𝐴)) ↔ ∀𝑥∀𝑦(〈𝑥, 𝑦〉 ∈ 𝐴 ↔ 〈𝑥, 𝑦〉 ∈ ( I ∩ (dom 𝐴 × ran 𝐴))))) |
39 | 36, 37, 38 | sylancl 589 |
. . 3
⊢ (𝐴 ⊆ I → (𝐴 = ( I ∩ (dom 𝐴 × ran 𝐴)) ↔ ∀𝑥∀𝑦(〈𝑥, 𝑦〉 ∈ 𝐴 ↔ 〈𝑥, 𝑦〉 ∈ ( I ∩ (dom 𝐴 × ran 𝐴))))) |
40 | 33, 39 | mpbird 260 |
. 2
⊢ (𝐴 ⊆ I → 𝐴 = ( I ∩ (dom 𝐴 × ran 𝐴))) |
41 | | inss1 4143 |
. . 3
⊢ ( I ∩
(dom 𝐴 × ran 𝐴)) ⊆ I |
42 | | sseq1 3926 |
. . 3
⊢ (𝐴 = ( I ∩ (dom 𝐴 × ran 𝐴)) → (𝐴 ⊆ I ↔ ( I ∩ (dom 𝐴 × ran 𝐴)) ⊆ I )) |
43 | 41, 42 | mpbiri 261 |
. 2
⊢ (𝐴 = ( I ∩ (dom 𝐴 × ran 𝐴)) → 𝐴 ⊆ I ) |
44 | 40, 43 | impbii 212 |
1
⊢ (𝐴 ⊆ I ↔ 𝐴 = ( I ∩ (dom 𝐴 × ran 𝐴))) |