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

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

Proof of Theorem sbthlem6
StepHypRef Expression
1 df-ima 5326 . . . . 5 (𝑔 “ (𝐴 𝐷)) = ran (𝑔 ↾ (𝐴 𝐷))
2 sbthlem.1 . . . . . 6 𝐴 ∈ V
3 sbthlem.2 . . . . . 6 𝐷 = {𝑥 ∣ (𝑥𝐴 ∧ (𝑔 “ (𝐵 ∖ (𝑓𝑥))) ⊆ (𝐴𝑥))}
42, 3sbthlem4 8316 . . . . 5 (((dom 𝑔 = 𝐵 ∧ ran 𝑔𝐴) ∧ Fun 𝑔) → (𝑔 “ (𝐴 𝐷)) = (𝐵 ∖ (𝑓 𝐷)))
51, 4syl5reqr 2849 . . . 4 (((dom 𝑔 = 𝐵 ∧ ran 𝑔𝐴) ∧ Fun 𝑔) → (𝐵 ∖ (𝑓 𝐷)) = ran (𝑔 ↾ (𝐴 𝐷)))
65uneq2d 3966 . . 3 (((dom 𝑔 = 𝐵 ∧ ran 𝑔𝐴) ∧ Fun 𝑔) → ((𝑓 𝐷) ∪ (𝐵 ∖ (𝑓 𝐷))) = ((𝑓 𝐷) ∪ ran (𝑔 ↾ (𝐴 𝐷))))
7 rnun 5759 . . . 4 ran ((𝑓 𝐷) ∪ (𝑔 ↾ (𝐴 𝐷))) = (ran (𝑓 𝐷) ∪ ran (𝑔 ↾ (𝐴 𝐷)))
8 sbthlem.3 . . . . 5 𝐻 = ((𝑓 𝐷) ∪ (𝑔 ↾ (𝐴 𝐷)))
98rneqi 5556 . . . 4 ran 𝐻 = ran ((𝑓 𝐷) ∪ (𝑔 ↾ (𝐴 𝐷)))
10 df-ima 5326 . . . . 5 (𝑓 𝐷) = ran (𝑓 𝐷)
1110uneq1i 3962 . . . 4 ((𝑓 𝐷) ∪ ran (𝑔 ↾ (𝐴 𝐷))) = (ran (𝑓 𝐷) ∪ ran (𝑔 ↾ (𝐴 𝐷)))
127, 9, 113eqtr4i 2832 . . 3 ran 𝐻 = ((𝑓 𝐷) ∪ ran (𝑔 ↾ (𝐴 𝐷)))
136, 12syl6reqr 2853 . 2 (((dom 𝑔 = 𝐵 ∧ ran 𝑔𝐴) ∧ Fun 𝑔) → ran 𝐻 = ((𝑓 𝐷) ∪ (𝐵 ∖ (𝑓 𝐷))))
14 imassrn 5695 . . . 4 (𝑓 𝐷) ⊆ ran 𝑓
15 sstr2 3806 . . . 4 ((𝑓 𝐷) ⊆ ran 𝑓 → (ran 𝑓𝐵 → (𝑓 𝐷) ⊆ 𝐵))
1614, 15ax-mp 5 . . 3 (ran 𝑓𝐵 → (𝑓 𝐷) ⊆ 𝐵)
17 undif 4244 . . 3 ((𝑓 𝐷) ⊆ 𝐵 ↔ ((𝑓 𝐷) ∪ (𝐵 ∖ (𝑓 𝐷))) = 𝐵)
1816, 17sylib 210 . 2 (ran 𝑓𝐵 → ((𝑓 𝐷) ∪ (𝐵 ∖ (𝑓 𝐷))) = 𝐵)
1913, 18sylan9eqr 2856 1 ((ran 𝑓𝐵 ∧ ((dom 𝑔 = 𝐵 ∧ ran 𝑔𝐴) ∧ Fun 𝑔)) → ran 𝐻 = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 385   = wceq 1653  wcel 2157  {cab 2786  Vcvv 3386  cdif 3767  cun 3768  wss 3770   cuni 4629  ccnv 5312  dom cdm 5313  ran crn 5314  cres 5315  cima 5316  Fun wfun 6096
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2378  ax-ext 2778  ax-sep 4976  ax-nul 4984  ax-pr 5098
This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-3an 1110  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-mo 2592  df-eu 2610  df-clab 2787  df-cleq 2793  df-clel 2796  df-nfc 2931  df-ral 3095  df-rex 3096  df-rab 3099  df-v 3388  df-dif 3773  df-un 3775  df-in 3777  df-ss 3784  df-nul 4117  df-if 4279  df-sn 4370  df-pr 4372  df-op 4376  df-uni 4630  df-br 4845  df-opab 4907  df-id 5221  df-xp 5319  df-rel 5320  df-cnv 5321  df-co 5322  df-dm 5323  df-rn 5324  df-res 5325  df-ima 5326  df-fun 6104
This theorem is referenced by:  sbthlem9  8321
  Copyright terms: Public domain W3C validator