Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > cnvresima | Structured version Visualization version GIF version |
Description: An image under the converse of a restriction. (Contributed by Jeff Hankins, 12-Jul-2009.) |
Ref | Expression |
---|---|
cnvresima | ⊢ (◡(𝐹 ↾ 𝐴) “ 𝐵) = ((◡𝐹 “ 𝐵) ∩ 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 19.41v 1957 | . . . 4 ⊢ (∃𝑠((𝑠 ∈ 𝐵 ∧ 〈𝑠, 𝑡〉 ∈ ◡𝐹) ∧ 𝑡 ∈ 𝐴) ↔ (∃𝑠(𝑠 ∈ 𝐵 ∧ 〈𝑠, 𝑡〉 ∈ ◡𝐹) ∧ 𝑡 ∈ 𝐴)) | |
2 | vex 3402 | . . . . . . . 8 ⊢ 𝑠 ∈ V | |
3 | 2 | opelresi 5833 | . . . . . . 7 ⊢ (〈𝑡, 𝑠〉 ∈ (𝐹 ↾ 𝐴) ↔ (𝑡 ∈ 𝐴 ∧ 〈𝑡, 𝑠〉 ∈ 𝐹)) |
4 | vex 3402 | . . . . . . . 8 ⊢ 𝑡 ∈ V | |
5 | 2, 4 | opelcnv 5724 | . . . . . . 7 ⊢ (〈𝑠, 𝑡〉 ∈ ◡(𝐹 ↾ 𝐴) ↔ 〈𝑡, 𝑠〉 ∈ (𝐹 ↾ 𝐴)) |
6 | 2, 4 | opelcnv 5724 | . . . . . . . 8 ⊢ (〈𝑠, 𝑡〉 ∈ ◡𝐹 ↔ 〈𝑡, 𝑠〉 ∈ 𝐹) |
7 | 6 | anbi2ci 628 | . . . . . . 7 ⊢ ((〈𝑠, 𝑡〉 ∈ ◡𝐹 ∧ 𝑡 ∈ 𝐴) ↔ (𝑡 ∈ 𝐴 ∧ 〈𝑡, 𝑠〉 ∈ 𝐹)) |
8 | 3, 5, 7 | 3bitr4i 306 | . . . . . 6 ⊢ (〈𝑠, 𝑡〉 ∈ ◡(𝐹 ↾ 𝐴) ↔ (〈𝑠, 𝑡〉 ∈ ◡𝐹 ∧ 𝑡 ∈ 𝐴)) |
9 | 8 | bianass 642 | . . . . 5 ⊢ ((𝑠 ∈ 𝐵 ∧ 〈𝑠, 𝑡〉 ∈ ◡(𝐹 ↾ 𝐴)) ↔ ((𝑠 ∈ 𝐵 ∧ 〈𝑠, 𝑡〉 ∈ ◡𝐹) ∧ 𝑡 ∈ 𝐴)) |
10 | 9 | exbii 1854 | . . . 4 ⊢ (∃𝑠(𝑠 ∈ 𝐵 ∧ 〈𝑠, 𝑡〉 ∈ ◡(𝐹 ↾ 𝐴)) ↔ ∃𝑠((𝑠 ∈ 𝐵 ∧ 〈𝑠, 𝑡〉 ∈ ◡𝐹) ∧ 𝑡 ∈ 𝐴)) |
11 | 4 | elima3 5910 | . . . . 5 ⊢ (𝑡 ∈ (◡𝐹 “ 𝐵) ↔ ∃𝑠(𝑠 ∈ 𝐵 ∧ 〈𝑠, 𝑡〉 ∈ ◡𝐹)) |
12 | 11 | anbi1i 627 | . . . 4 ⊢ ((𝑡 ∈ (◡𝐹 “ 𝐵) ∧ 𝑡 ∈ 𝐴) ↔ (∃𝑠(𝑠 ∈ 𝐵 ∧ 〈𝑠, 𝑡〉 ∈ ◡𝐹) ∧ 𝑡 ∈ 𝐴)) |
13 | 1, 10, 12 | 3bitr4i 306 | . . 3 ⊢ (∃𝑠(𝑠 ∈ 𝐵 ∧ 〈𝑠, 𝑡〉 ∈ ◡(𝐹 ↾ 𝐴)) ↔ (𝑡 ∈ (◡𝐹 “ 𝐵) ∧ 𝑡 ∈ 𝐴)) |
14 | 4 | elima3 5910 | . . 3 ⊢ (𝑡 ∈ (◡(𝐹 ↾ 𝐴) “ 𝐵) ↔ ∃𝑠(𝑠 ∈ 𝐵 ∧ 〈𝑠, 𝑡〉 ∈ ◡(𝐹 ↾ 𝐴))) |
15 | elin 3859 | . . 3 ⊢ (𝑡 ∈ ((◡𝐹 “ 𝐵) ∩ 𝐴) ↔ (𝑡 ∈ (◡𝐹 “ 𝐵) ∧ 𝑡 ∈ 𝐴)) | |
16 | 13, 14, 15 | 3bitr4i 306 | . 2 ⊢ (𝑡 ∈ (◡(𝐹 ↾ 𝐴) “ 𝐵) ↔ 𝑡 ∈ ((◡𝐹 “ 𝐵) ∩ 𝐴)) |
17 | 16 | eqriv 2735 | 1 ⊢ (◡(𝐹 ↾ 𝐴) “ 𝐵) = ((◡𝐹 “ 𝐵) ∩ 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: ∧ wa 399 = wceq 1542 ∃wex 1786 ∈ wcel 2114 ∩ cin 3842 〈cop 4522 ◡ccnv 5524 ↾ cres 5527 “ cima 5528 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1975 ax-7 2020 ax-8 2116 ax-9 2124 ax-ext 2710 ax-sep 5167 ax-nul 5174 ax-pr 5296 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1787 df-sb 2075 df-clab 2717 df-cleq 2730 df-clel 2811 df-ral 3058 df-rex 3059 df-v 3400 df-dif 3846 df-un 3848 df-in 3850 df-nul 4212 df-if 4415 df-sn 4517 df-pr 4519 df-op 4523 df-br 5031 df-opab 5093 df-xp 5531 df-cnv 5533 df-dm 5535 df-rn 5536 df-res 5537 df-ima 5538 |
This theorem is referenced by: fimacnvinrn 6849 ramub2 16450 ramub1lem2 16463 cnrest 22036 kgencn 22307 kgencn3 22309 xkoptsub 22405 qtopres 22449 qtoprest 22468 mbfid 24387 mbfres 24396 1stpreima 30614 2ndpreima 30615 gsumhashmul 30893 cvmsss2 32807 lmhmlnmsplit 40484 |
Copyright terms: Public domain | W3C validator |