MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  cnvresima Structured version   Visualization version   GIF version

Theorem cnvresima 6229
Description: An image under the converse of a restriction. (Contributed by Jeff Hankins, 12-Jul-2009.)
Assertion
Ref Expression
cnvresima ((𝐹𝐴) “ 𝐵) = ((𝐹𝐵) ∩ 𝐴)

Proof of Theorem cnvresima
Dummy variables 𝑡 𝑠 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 19.41v 1953 . . . 4 (∃𝑠((𝑠𝐵 ∧ ⟨𝑠, 𝑡⟩ ∈ 𝐹) ∧ 𝑡𝐴) ↔ (∃𝑠(𝑠𝐵 ∧ ⟨𝑠, 𝑡⟩ ∈ 𝐹) ∧ 𝑡𝐴))
2 vex 3478 . . . . . . . 8 𝑠 ∈ V
32opelresi 5989 . . . . . . 7 (⟨𝑡, 𝑠⟩ ∈ (𝐹𝐴) ↔ (𝑡𝐴 ∧ ⟨𝑡, 𝑠⟩ ∈ 𝐹))
4 vex 3478 . . . . . . . 8 𝑡 ∈ V
52, 4opelcnv 5881 . . . . . . 7 (⟨𝑠, 𝑡⟩ ∈ (𝐹𝐴) ↔ ⟨𝑡, 𝑠⟩ ∈ (𝐹𝐴))
62, 4opelcnv 5881 . . . . . . . 8 (⟨𝑠, 𝑡⟩ ∈ 𝐹 ↔ ⟨𝑡, 𝑠⟩ ∈ 𝐹)
76anbi2ci 625 . . . . . . 7 ((⟨𝑠, 𝑡⟩ ∈ 𝐹𝑡𝐴) ↔ (𝑡𝐴 ∧ ⟨𝑡, 𝑠⟩ ∈ 𝐹))
83, 5, 73bitr4i 302 . . . . . 6 (⟨𝑠, 𝑡⟩ ∈ (𝐹𝐴) ↔ (⟨𝑠, 𝑡⟩ ∈ 𝐹𝑡𝐴))
98bianass 640 . . . . 5 ((𝑠𝐵 ∧ ⟨𝑠, 𝑡⟩ ∈ (𝐹𝐴)) ↔ ((𝑠𝐵 ∧ ⟨𝑠, 𝑡⟩ ∈ 𝐹) ∧ 𝑡𝐴))
109exbii 1850 . . . 4 (∃𝑠(𝑠𝐵 ∧ ⟨𝑠, 𝑡⟩ ∈ (𝐹𝐴)) ↔ ∃𝑠((𝑠𝐵 ∧ ⟨𝑠, 𝑡⟩ ∈ 𝐹) ∧ 𝑡𝐴))
114elima3 6066 . . . . 5 (𝑡 ∈ (𝐹𝐵) ↔ ∃𝑠(𝑠𝐵 ∧ ⟨𝑠, 𝑡⟩ ∈ 𝐹))
1211anbi1i 624 . . . 4 ((𝑡 ∈ (𝐹𝐵) ∧ 𝑡𝐴) ↔ (∃𝑠(𝑠𝐵 ∧ ⟨𝑠, 𝑡⟩ ∈ 𝐹) ∧ 𝑡𝐴))
131, 10, 123bitr4i 302 . . 3 (∃𝑠(𝑠𝐵 ∧ ⟨𝑠, 𝑡⟩ ∈ (𝐹𝐴)) ↔ (𝑡 ∈ (𝐹𝐵) ∧ 𝑡𝐴))
144elima3 6066 . . 3 (𝑡 ∈ ((𝐹𝐴) “ 𝐵) ↔ ∃𝑠(𝑠𝐵 ∧ ⟨𝑠, 𝑡⟩ ∈ (𝐹𝐴)))
15 elin 3964 . . 3 (𝑡 ∈ ((𝐹𝐵) ∩ 𝐴) ↔ (𝑡 ∈ (𝐹𝐵) ∧ 𝑡𝐴))
1613, 14, 153bitr4i 302 . 2 (𝑡 ∈ ((𝐹𝐴) “ 𝐵) ↔ 𝑡 ∈ ((𝐹𝐵) ∩ 𝐴))
1716eqriv 2729 1 ((𝐹𝐴) “ 𝐵) = ((𝐹𝐵) ∩ 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wa 396   = wceq 1541  wex 1781  wcel 2106  cin 3947  cop 4634  ccnv 5675  cres 5678  cima 5679
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pr 5427
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-br 5149  df-opab 5211  df-xp 5682  df-cnv 5684  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689
This theorem is referenced by:  fimacnvinrn  7073  ramub2  16946  ramub1lem2  16959  cnrest  22788  kgencn  23059  kgencn3  23061  xkoptsub  23157  qtopres  23201  qtoprest  23220  mbfid  25151  mbfres  25160  1stpreima  31923  2ndpreima  31924  gsumhashmul  32203  cvmsss2  34260  lmhmlnmsplit  41819
  Copyright terms: Public domain W3C validator