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

Theorem sbthlem4 9037
Description: Lemma for sbth 9044. (Contributed by NM, 27-Mar-1998.)
Hypotheses
Ref Expression
sbthlem.1 𝐴 ∈ V
sbthlem.2 𝐷 = {𝑥 ∣ (𝑥𝐴 ∧ (𝑔 “ (𝐵 ∖ (𝑓𝑥))) ⊆ (𝐴𝑥))}
Assertion
Ref Expression
sbthlem4 (((dom 𝑔 = 𝐵 ∧ ran 𝑔𝐴) ∧ Fun 𝑔) → (𝑔 “ (𝐴 𝐷)) = (𝐵 ∖ (𝑓 𝐷)))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝑥,𝐷   𝑥,𝑓   𝑥,𝑔
Allowed substitution hints:   𝐴(𝑓,𝑔)   𝐵(𝑓,𝑔)   𝐷(𝑓,𝑔)

Proof of Theorem sbthlem4
StepHypRef Expression
1 df-ima 5651 . 2 (𝑔 “ (𝐴 𝐷)) = ran (𝑔 ↾ (𝐴 𝐷))
2 difss 4096 . . . . . . 7 (𝐵 ∖ (𝑓 𝐷)) ⊆ 𝐵
3 sseq2 3975 . . . . . . 7 (dom 𝑔 = 𝐵 → ((𝐵 ∖ (𝑓 𝐷)) ⊆ dom 𝑔 ↔ (𝐵 ∖ (𝑓 𝐷)) ⊆ 𝐵))
42, 3mpbiri 258 . . . . . 6 (dom 𝑔 = 𝐵 → (𝐵 ∖ (𝑓 𝐷)) ⊆ dom 𝑔)
5 ssdmres 5965 . . . . . 6 ((𝐵 ∖ (𝑓 𝐷)) ⊆ dom 𝑔 ↔ dom (𝑔 ↾ (𝐵 ∖ (𝑓 𝐷))) = (𝐵 ∖ (𝑓 𝐷)))
64, 5sylib 217 . . . . 5 (dom 𝑔 = 𝐵 → dom (𝑔 ↾ (𝐵 ∖ (𝑓 𝐷))) = (𝐵 ∖ (𝑓 𝐷)))
7 dfdm4 5856 . . . . 5 dom (𝑔 ↾ (𝐵 ∖ (𝑓 𝐷))) = ran (𝑔 ↾ (𝐵 ∖ (𝑓 𝐷)))
86, 7eqtr3di 2792 . . . 4 (dom 𝑔 = 𝐵 → (𝐵 ∖ (𝑓 𝐷)) = ran (𝑔 ↾ (𝐵 ∖ (𝑓 𝐷))))
9 funcnvres 6584 . . . . . 6 (Fun 𝑔(𝑔 ↾ (𝐵 ∖ (𝑓 𝐷))) = (𝑔 ↾ (𝑔 “ (𝐵 ∖ (𝑓 𝐷)))))
10 sbthlem.1 . . . . . . . 8 𝐴 ∈ V
11 sbthlem.2 . . . . . . . 8 𝐷 = {𝑥 ∣ (𝑥𝐴 ∧ (𝑔 “ (𝐵 ∖ (𝑓𝑥))) ⊆ (𝐴𝑥))}
1210, 11sbthlem3 9036 . . . . . . 7 (ran 𝑔𝐴 → (𝑔 “ (𝐵 ∖ (𝑓 𝐷))) = (𝐴 𝐷))
1312reseq2d 5942 . . . . . 6 (ran 𝑔𝐴 → (𝑔 ↾ (𝑔 “ (𝐵 ∖ (𝑓 𝐷)))) = (𝑔 ↾ (𝐴 𝐷)))
149, 13sylan9eqr 2799 . . . . 5 ((ran 𝑔𝐴 ∧ Fun 𝑔) → (𝑔 ↾ (𝐵 ∖ (𝑓 𝐷))) = (𝑔 ↾ (𝐴 𝐷)))
1514rneqd 5898 . . . 4 ((ran 𝑔𝐴 ∧ Fun 𝑔) → ran (𝑔 ↾ (𝐵 ∖ (𝑓 𝐷))) = ran (𝑔 ↾ (𝐴 𝐷)))
168, 15sylan9eq 2797 . . 3 ((dom 𝑔 = 𝐵 ∧ (ran 𝑔𝐴 ∧ Fun 𝑔)) → (𝐵 ∖ (𝑓 𝐷)) = ran (𝑔 ↾ (𝐴 𝐷)))
1716anassrs 469 . 2 (((dom 𝑔 = 𝐵 ∧ ran 𝑔𝐴) ∧ Fun 𝑔) → (𝐵 ∖ (𝑓 𝐷)) = ran (𝑔 ↾ (𝐴 𝐷)))
181, 17eqtr4id 2796 1 (((dom 𝑔 = 𝐵 ∧ ran 𝑔𝐴) ∧ Fun 𝑔) → (𝑔 “ (𝐴 𝐷)) = (𝐵 ∖ (𝑓 𝐷)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397   = wceq 1542  wcel 2107  {cab 2714  Vcvv 3448  cdif 3912  wss 3915   cuni 4870  ccnv 5637  dom cdm 5638  ran crn 5639  cres 5640  cima 5641  Fun wfun 6495
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-12 2172  ax-ext 2708  ax-sep 5261  ax-nul 5268  ax-pr 5389
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-ral 3066  df-rex 3075  df-rab 3411  df-v 3450  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-nul 4288  df-if 4492  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-br 5111  df-opab 5173  df-id 5536  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-fun 6503
This theorem is referenced by:  sbthlem6  9039  sbthlem8  9041
  Copyright terms: Public domain W3C validator