Step | Hyp | Ref
| Expression |
1 | | ssel 3975 |
. . . . . . . . 9
⊢ (𝐴 ⊆ I → (⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ I )) |
2 | | vex 3478 |
. . . . . . . . . 10
⊢ 𝑥 ∈ V |
3 | | vex 3478 |
. . . . . . . . . 10
⊢ 𝑦 ∈ V |
4 | 2, 3 | opeldm 5907 |
. . . . . . . . 9
⊢
(⟨𝑥, 𝑦⟩ ∈ 𝐴 → 𝑥 ∈ dom 𝐴) |
5 | 1, 4 | jca2 514 |
. . . . . . . 8
⊢ (𝐴 ⊆ I → (⟨𝑥, 𝑦⟩ ∈ 𝐴 → (⟨𝑥, 𝑦⟩ ∈ I ∧ 𝑥 ∈ dom 𝐴))) |
6 | 2, 3 | opelrn 5942 |
. . . . . . . . 9
⊢
(⟨𝑥, 𝑦⟩ ∈ 𝐴 → 𝑦 ∈ ran 𝐴) |
7 | 1, 6 | jca2 514 |
. . . . . . . 8
⊢ (𝐴 ⊆ I → (⟨𝑥, 𝑦⟩ ∈ 𝐴 → (⟨𝑥, 𝑦⟩ ∈ I ∧ 𝑦 ∈ ran 𝐴))) |
8 | 5, 7 | jcad 513 |
. . . . . . 7
⊢ (𝐴 ⊆ I → (⟨𝑥, 𝑦⟩ ∈ 𝐴 → ((⟨𝑥, 𝑦⟩ ∈ I ∧ 𝑥 ∈ dom 𝐴) ∧ (⟨𝑥, 𝑦⟩ ∈ I ∧ 𝑦 ∈ ran 𝐴)))) |
9 | | anandi 674 |
. . . . . . 7
⊢
((⟨𝑥, 𝑦⟩ ∈ I ∧ (𝑥 ∈ dom 𝐴 ∧ 𝑦 ∈ ran 𝐴)) ↔ ((⟨𝑥, 𝑦⟩ ∈ I ∧ 𝑥 ∈ dom 𝐴) ∧ (⟨𝑥, 𝑦⟩ ∈ I ∧ 𝑦 ∈ ran 𝐴))) |
10 | 8, 9 | syl6ibr 251 |
. . . . . 6
⊢ (𝐴 ⊆ I → (⟨𝑥, 𝑦⟩ ∈ 𝐴 → (⟨𝑥, 𝑦⟩ ∈ I ∧ (𝑥 ∈ dom 𝐴 ∧ 𝑦 ∈ ran 𝐴)))) |
11 | | df-br 5149 |
. . . . . . . . 9
⊢ (𝑥 I 𝑦 ↔ ⟨𝑥, 𝑦⟩ ∈ I ) |
12 | 3 | ideq 5852 |
. . . . . . . . 9
⊢ (𝑥 I 𝑦 ↔ 𝑥 = 𝑦) |
13 | 11, 12 | bitr3i 276 |
. . . . . . . 8
⊢
(⟨𝑥, 𝑦⟩ ∈ I ↔ 𝑥 = 𝑦) |
14 | 2 | eldm2 5901 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ dom 𝐴 ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴) |
15 | | opeq2 4874 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑦 → ⟨𝑥, 𝑥⟩ = ⟨𝑥, 𝑦⟩) |
16 | 15 | eleq1d 2818 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑦 → (⟨𝑥, 𝑥⟩ ∈ 𝐴 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝐴)) |
17 | 16 | biimprcd 249 |
. . . . . . . . . . . . . . . 16
⊢
(⟨𝑥, 𝑦⟩ ∈ 𝐴 → (𝑥 = 𝑦 → ⟨𝑥, 𝑥⟩ ∈ 𝐴)) |
18 | 13, 17 | biimtrid 241 |
. . . . . . . . . . . . . . 15
⊢
(⟨𝑥, 𝑦⟩ ∈ 𝐴 → (⟨𝑥, 𝑦⟩ ∈ I → ⟨𝑥, 𝑥⟩ ∈ 𝐴)) |
19 | 1, 18 | sylcom 30 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ⊆ I → (⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑥⟩ ∈ 𝐴)) |
20 | 19 | exlimdv 1936 |
. . . . . . . . . . . . 13
⊢ (𝐴 ⊆ I → (∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑥⟩ ∈ 𝐴)) |
21 | 14, 20 | biimtrid 241 |
. . . . . . . . . . . 12
⊢ (𝐴 ⊆ I → (𝑥 ∈ dom 𝐴 → ⟨𝑥, 𝑥⟩ ∈ 𝐴)) |
22 | 16 | imbi2d 340 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 → ((𝑥 ∈ dom 𝐴 → ⟨𝑥, 𝑥⟩ ∈ 𝐴) ↔ (𝑥 ∈ dom 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐴))) |
23 | 21, 22 | syl5ibcom 244 |
. . . . . . . . . . 11
⊢ (𝐴 ⊆ I → (𝑥 = 𝑦 → (𝑥 ∈ dom 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐴))) |
24 | 23 | imp 407 |
. . . . . . . . . 10
⊢ ((𝐴 ⊆ I ∧ 𝑥 = 𝑦) → (𝑥 ∈ dom 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐴)) |
25 | 24 | adantrd 492 |
. . . . . . . . 9
⊢ ((𝐴 ⊆ I ∧ 𝑥 = 𝑦) → ((𝑥 ∈ dom 𝐴 ∧ 𝑦 ∈ ran 𝐴) → ⟨𝑥, 𝑦⟩ ∈ 𝐴)) |
26 | 25 | ex 413 |
. . . . . . . 8
⊢ (𝐴 ⊆ I → (𝑥 = 𝑦 → ((𝑥 ∈ dom 𝐴 ∧ 𝑦 ∈ ran 𝐴) → ⟨𝑥, 𝑦⟩ ∈ 𝐴))) |
27 | 13, 26 | biimtrid 241 |
. . . . . . 7
⊢ (𝐴 ⊆ I → (⟨𝑥, 𝑦⟩ ∈ I → ((𝑥 ∈ dom 𝐴 ∧ 𝑦 ∈ ran 𝐴) → ⟨𝑥, 𝑦⟩ ∈ 𝐴))) |
28 | 27 | impd 411 |
. . . . . 6
⊢ (𝐴 ⊆ I → ((⟨𝑥, 𝑦⟩ ∈ I ∧ (𝑥 ∈ dom 𝐴 ∧ 𝑦 ∈ ran 𝐴)) → ⟨𝑥, 𝑦⟩ ∈ 𝐴)) |
29 | 10, 28 | impbid 211 |
. . . . 5
⊢ (𝐴 ⊆ I → (⟨𝑥, 𝑦⟩ ∈ 𝐴 ↔ (⟨𝑥, 𝑦⟩ ∈ I ∧ (𝑥 ∈ dom 𝐴 ∧ 𝑦 ∈ ran 𝐴)))) |
30 | | opelinxp 5755 |
. . . . . 6
⊢
(⟨𝑥, 𝑦⟩ ∈ ( I ∩ (dom
𝐴 × ran 𝐴)) ↔ ((𝑥 ∈ dom 𝐴 ∧ 𝑦 ∈ ran 𝐴) ∧ ⟨𝑥, 𝑦⟩ ∈ I )) |
31 | 30 | biancomi 463 |
. . . . 5
⊢
(⟨𝑥, 𝑦⟩ ∈ ( I ∩ (dom
𝐴 × ran 𝐴)) ↔ (⟨𝑥, 𝑦⟩ ∈ I ∧ (𝑥 ∈ dom 𝐴 ∧ 𝑦 ∈ ran 𝐴))) |
32 | 29, 31 | bitr4di 288 |
. . . 4
⊢ (𝐴 ⊆ I → (⟨𝑥, 𝑦⟩ ∈ 𝐴 ↔ ⟨𝑥, 𝑦⟩ ∈ ( I ∩ (dom 𝐴 × ran 𝐴)))) |
33 | 32 | alrimivv 1931 |
. . 3
⊢ (𝐴 ⊆ I → ∀𝑥∀𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 ↔ ⟨𝑥, 𝑦⟩ ∈ ( I ∩ (dom 𝐴 × ran 𝐴)))) |
34 | | reli 5826 |
. . . . 5
⊢ Rel
I |
35 | | relss 5781 |
. . . . 5
⊢ (𝐴 ⊆ I → (Rel I →
Rel 𝐴)) |
36 | 34, 35 | mpi 20 |
. . . 4
⊢ (𝐴 ⊆ I → Rel 𝐴) |
37 | | relinxp 5814 |
. . . 4
⊢ Rel ( I
∩ (dom 𝐴 × ran
𝐴)) |
38 | | eqrel 5784 |
. . . 4
⊢ ((Rel
𝐴 ∧ Rel ( I ∩ (dom
𝐴 × ran 𝐴))) → (𝐴 = ( I ∩ (dom 𝐴 × ran 𝐴)) ↔ ∀𝑥∀𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 ↔ ⟨𝑥, 𝑦⟩ ∈ ( I ∩ (dom 𝐴 × ran 𝐴))))) |
39 | 36, 37, 38 | sylancl 586 |
. . 3
⊢ (𝐴 ⊆ I → (𝐴 = ( I ∩ (dom 𝐴 × ran 𝐴)) ↔ ∀𝑥∀𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 ↔ ⟨𝑥, 𝑦⟩ ∈ ( I ∩ (dom 𝐴 × ran 𝐴))))) |
40 | 33, 39 | mpbird 256 |
. 2
⊢ (𝐴 ⊆ I → 𝐴 = ( I ∩ (dom 𝐴 × ran 𝐴))) |
41 | | inss1 4228 |
. . 3
⊢ ( I ∩
(dom 𝐴 × ran 𝐴)) ⊆ I |
42 | | sseq1 4007 |
. . 3
⊢ (𝐴 = ( I ∩ (dom 𝐴 × ran 𝐴)) → (𝐴 ⊆ I ↔ ( I ∩ (dom 𝐴 × ran 𝐴)) ⊆ I )) |
43 | 41, 42 | mpbiri 257 |
. 2
⊢ (𝐴 = ( I ∩ (dom 𝐴 × ran 𝐴)) → 𝐴 ⊆ I ) |
44 | 40, 43 | impbii 208 |
1
⊢ (𝐴 ⊆ I ↔ 𝐴 = ( I ∩ (dom 𝐴 × ran 𝐴))) |