| Step | Hyp | Ref
| Expression |
| 1 | | ssel 3977 |
. . . . . . . . 9
⊢ (𝐴 ⊆ I → (〈𝑥, 𝑦〉 ∈ 𝐴 → 〈𝑥, 𝑦〉 ∈ I )) |
| 2 | | vex 3484 |
. . . . . . . . . 10
⊢ 𝑥 ∈ V |
| 3 | | vex 3484 |
. . . . . . . . . 10
⊢ 𝑦 ∈ V |
| 4 | 2, 3 | opeldm 5918 |
. . . . . . . . 9
⊢
(〈𝑥, 𝑦〉 ∈ 𝐴 → 𝑥 ∈ dom 𝐴) |
| 5 | 1, 4 | jca2 513 |
. . . . . . . 8
⊢ (𝐴 ⊆ I → (〈𝑥, 𝑦〉 ∈ 𝐴 → (〈𝑥, 𝑦〉 ∈ I ∧ 𝑥 ∈ dom 𝐴))) |
| 6 | 2, 3 | opelrn 5954 |
. . . . . . . . 9
⊢
(〈𝑥, 𝑦〉 ∈ 𝐴 → 𝑦 ∈ ran 𝐴) |
| 7 | 1, 6 | jca2 513 |
. . . . . . . 8
⊢ (𝐴 ⊆ I → (〈𝑥, 𝑦〉 ∈ 𝐴 → (〈𝑥, 𝑦〉 ∈ I ∧ 𝑦 ∈ ran 𝐴))) |
| 8 | 5, 7 | jcad 512 |
. . . . . . 7
⊢ (𝐴 ⊆ I → (〈𝑥, 𝑦〉 ∈ 𝐴 → ((〈𝑥, 𝑦〉 ∈ I ∧ 𝑥 ∈ dom 𝐴) ∧ (〈𝑥, 𝑦〉 ∈ I ∧ 𝑦 ∈ ran 𝐴)))) |
| 9 | | anandi 676 |
. . . . . . 7
⊢
((〈𝑥, 𝑦〉 ∈ I ∧ (𝑥 ∈ dom 𝐴 ∧ 𝑦 ∈ ran 𝐴)) ↔ ((〈𝑥, 𝑦〉 ∈ I ∧ 𝑥 ∈ dom 𝐴) ∧ (〈𝑥, 𝑦〉 ∈ I ∧ 𝑦 ∈ ran 𝐴))) |
| 10 | 8, 9 | imbitrrdi 252 |
. . . . . 6
⊢ (𝐴 ⊆ I → (〈𝑥, 𝑦〉 ∈ 𝐴 → (〈𝑥, 𝑦〉 ∈ I ∧ (𝑥 ∈ dom 𝐴 ∧ 𝑦 ∈ ran 𝐴)))) |
| 11 | | df-br 5144 |
. . . . . . . . 9
⊢ (𝑥 I 𝑦 ↔ 〈𝑥, 𝑦〉 ∈ I ) |
| 12 | 3 | ideq 5863 |
. . . . . . . . 9
⊢ (𝑥 I 𝑦 ↔ 𝑥 = 𝑦) |
| 13 | 11, 12 | bitr3i 277 |
. . . . . . . 8
⊢
(〈𝑥, 𝑦〉 ∈ I ↔ 𝑥 = 𝑦) |
| 14 | 2 | eldm2 5912 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ dom 𝐴 ↔ ∃𝑦〈𝑥, 𝑦〉 ∈ 𝐴) |
| 15 | | opeq2 4874 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑦 → 〈𝑥, 𝑥〉 = 〈𝑥, 𝑦〉) |
| 16 | 15 | eleq1d 2826 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑦 → (〈𝑥, 𝑥〉 ∈ 𝐴 ↔ 〈𝑥, 𝑦〉 ∈ 𝐴)) |
| 17 | 16 | biimprcd 250 |
. . . . . . . . . . . . . . . 16
⊢
(〈𝑥, 𝑦〉 ∈ 𝐴 → (𝑥 = 𝑦 → 〈𝑥, 𝑥〉 ∈ 𝐴)) |
| 18 | 13, 17 | biimtrid 242 |
. . . . . . . . . . . . . . 15
⊢
(〈𝑥, 𝑦〉 ∈ 𝐴 → (〈𝑥, 𝑦〉 ∈ I → 〈𝑥, 𝑥〉 ∈ 𝐴)) |
| 19 | 1, 18 | sylcom 30 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ⊆ I → (〈𝑥, 𝑦〉 ∈ 𝐴 → 〈𝑥, 𝑥〉 ∈ 𝐴)) |
| 20 | 19 | exlimdv 1933 |
. . . . . . . . . . . . 13
⊢ (𝐴 ⊆ I → (∃𝑦〈𝑥, 𝑦〉 ∈ 𝐴 → 〈𝑥, 𝑥〉 ∈ 𝐴)) |
| 21 | 14, 20 | biimtrid 242 |
. . . . . . . . . . . 12
⊢ (𝐴 ⊆ I → (𝑥 ∈ dom 𝐴 → 〈𝑥, 𝑥〉 ∈ 𝐴)) |
| 22 | 16 | imbi2d 340 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 → ((𝑥 ∈ dom 𝐴 → 〈𝑥, 𝑥〉 ∈ 𝐴) ↔ (𝑥 ∈ dom 𝐴 → 〈𝑥, 𝑦〉 ∈ 𝐴))) |
| 23 | 21, 22 | syl5ibcom 245 |
. . . . . . . . . . 11
⊢ (𝐴 ⊆ I → (𝑥 = 𝑦 → (𝑥 ∈ dom 𝐴 → 〈𝑥, 𝑦〉 ∈ 𝐴))) |
| 24 | 23 | imp 406 |
. . . . . . . . . 10
⊢ ((𝐴 ⊆ I ∧ 𝑥 = 𝑦) → (𝑥 ∈ dom 𝐴 → 〈𝑥, 𝑦〉 ∈ 𝐴)) |
| 25 | 24 | adantrd 491 |
. . . . . . . . 9
⊢ ((𝐴 ⊆ I ∧ 𝑥 = 𝑦) → ((𝑥 ∈ dom 𝐴 ∧ 𝑦 ∈ ran 𝐴) → 〈𝑥, 𝑦〉 ∈ 𝐴)) |
| 26 | 25 | ex 412 |
. . . . . . . 8
⊢ (𝐴 ⊆ I → (𝑥 = 𝑦 → ((𝑥 ∈ dom 𝐴 ∧ 𝑦 ∈ ran 𝐴) → 〈𝑥, 𝑦〉 ∈ 𝐴))) |
| 27 | 13, 26 | biimtrid 242 |
. . . . . . 7
⊢ (𝐴 ⊆ I → (〈𝑥, 𝑦〉 ∈ I → ((𝑥 ∈ dom 𝐴 ∧ 𝑦 ∈ ran 𝐴) → 〈𝑥, 𝑦〉 ∈ 𝐴))) |
| 28 | 27 | impd 410 |
. . . . . 6
⊢ (𝐴 ⊆ I → ((〈𝑥, 𝑦〉 ∈ I ∧ (𝑥 ∈ dom 𝐴 ∧ 𝑦 ∈ ran 𝐴)) → 〈𝑥, 𝑦〉 ∈ 𝐴)) |
| 29 | 10, 28 | impbid 212 |
. . . . 5
⊢ (𝐴 ⊆ I → (〈𝑥, 𝑦〉 ∈ 𝐴 ↔ (〈𝑥, 𝑦〉 ∈ I ∧ (𝑥 ∈ dom 𝐴 ∧ 𝑦 ∈ ran 𝐴)))) |
| 30 | | opelinxp 5765 |
. . . . . 6
⊢
(〈𝑥, 𝑦〉 ∈ ( I ∩ (dom
𝐴 × ran 𝐴)) ↔ ((𝑥 ∈ dom 𝐴 ∧ 𝑦 ∈ ran 𝐴) ∧ 〈𝑥, 𝑦〉 ∈ I )) |
| 31 | 30 | biancomi 462 |
. . . . 5
⊢
(〈𝑥, 𝑦〉 ∈ ( I ∩ (dom
𝐴 × ran 𝐴)) ↔ (〈𝑥, 𝑦〉 ∈ I ∧ (𝑥 ∈ dom 𝐴 ∧ 𝑦 ∈ ran 𝐴))) |
| 32 | 29, 31 | bitr4di 289 |
. . . 4
⊢ (𝐴 ⊆ I → (〈𝑥, 𝑦〉 ∈ 𝐴 ↔ 〈𝑥, 𝑦〉 ∈ ( I ∩ (dom 𝐴 × ran 𝐴)))) |
| 33 | 32 | alrimivv 1928 |
. . 3
⊢ (𝐴 ⊆ I → ∀𝑥∀𝑦(〈𝑥, 𝑦〉 ∈ 𝐴 ↔ 〈𝑥, 𝑦〉 ∈ ( I ∩ (dom 𝐴 × ran 𝐴)))) |
| 34 | | reli 5836 |
. . . . 5
⊢ Rel
I |
| 35 | | relss 5791 |
. . . . 5
⊢ (𝐴 ⊆ I → (Rel I →
Rel 𝐴)) |
| 36 | 34, 35 | mpi 20 |
. . . 4
⊢ (𝐴 ⊆ I → Rel 𝐴) |
| 37 | | relinxp 5824 |
. . . 4
⊢ Rel ( I
∩ (dom 𝐴 × ran
𝐴)) |
| 38 | | eqrel 5794 |
. . . 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 257 |
. 2
⊢ (𝐴 ⊆ I → 𝐴 = ( I ∩ (dom 𝐴 × ran 𝐴))) |
| 41 | | inss1 4237 |
. . 3
⊢ ( I ∩
(dom 𝐴 × ran 𝐴)) ⊆ I |
| 42 | | sseq1 4009 |
. . 3
⊢ (𝐴 = ( I ∩ (dom 𝐴 × ran 𝐴)) → (𝐴 ⊆ I ↔ ( I ∩ (dom 𝐴 × ran 𝐴)) ⊆ I )) |
| 43 | 41, 42 | mpbiri 258 |
. 2
⊢ (𝐴 = ( I ∩ (dom 𝐴 × ran 𝐴)) → 𝐴 ⊆ I ) |
| 44 | 40, 43 | impbii 209 |
1
⊢ (𝐴 ⊆ I ↔ 𝐴 = ( I ∩ (dom 𝐴 × ran 𝐴))) |