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

Theorem sbthlem6 8243
Description: Lemma for sbth 8248. (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 5280 . . . . 5 (𝑔 “ (𝐴 𝐷)) = ran (𝑔 ↾ (𝐴 𝐷))
2 sbthlem.1 . . . . . 6 𝐴 ∈ V
3 sbthlem.2 . . . . . 6 𝐷 = {𝑥 ∣ (𝑥𝐴 ∧ (𝑔 “ (𝐵 ∖ (𝑓𝑥))) ⊆ (𝐴𝑥))}
42, 3sbthlem4 8241 . . . . 5 (((dom 𝑔 = 𝐵 ∧ ran 𝑔𝐴) ∧ Fun 𝑔) → (𝑔 “ (𝐴 𝐷)) = (𝐵 ∖ (𝑓 𝐷)))
51, 4syl5reqr 2810 . . . 4 (((dom 𝑔 = 𝐵 ∧ ran 𝑔𝐴) ∧ Fun 𝑔) → (𝐵 ∖ (𝑓 𝐷)) = ran (𝑔 ↾ (𝐴 𝐷)))
65uneq2d 3911 . . 3 (((dom 𝑔 = 𝐵 ∧ ran 𝑔𝐴) ∧ Fun 𝑔) → ((𝑓 𝐷) ∪ (𝐵 ∖ (𝑓 𝐷))) = ((𝑓 𝐷) ∪ ran (𝑔 ↾ (𝐴 𝐷))))
7 rnun 5700 . . . 4 ran ((𝑓 𝐷) ∪ (𝑔 ↾ (𝐴 𝐷))) = (ran (𝑓 𝐷) ∪ ran (𝑔 ↾ (𝐴 𝐷)))
8 sbthlem.3 . . . . 5 𝐻 = ((𝑓 𝐷) ∪ (𝑔 ↾ (𝐴 𝐷)))
98rneqi 5508 . . . 4 ran 𝐻 = ran ((𝑓 𝐷) ∪ (𝑔 ↾ (𝐴 𝐷)))
10 df-ima 5280 . . . . 5 (𝑓 𝐷) = ran (𝑓 𝐷)
1110uneq1i 3907 . . . 4 ((𝑓 𝐷) ∪ ran (𝑔 ↾ (𝐴 𝐷))) = (ran (𝑓 𝐷) ∪ ran (𝑔 ↾ (𝐴 𝐷)))
127, 9, 113eqtr4i 2793 . . 3 ran 𝐻 = ((𝑓 𝐷) ∪ ran (𝑔 ↾ (𝐴 𝐷)))
136, 12syl6reqr 2814 . 2 (((dom 𝑔 = 𝐵 ∧ ran 𝑔𝐴) ∧ Fun 𝑔) → ran 𝐻 = ((𝑓 𝐷) ∪ (𝐵 ∖ (𝑓 𝐷))))
14 imassrn 5636 . . . 4 (𝑓 𝐷) ⊆ ran 𝑓
15 sstr2 3752 . . . 4 ((𝑓 𝐷) ⊆ ran 𝑓 → (ran 𝑓𝐵 → (𝑓 𝐷) ⊆ 𝐵))
1614, 15ax-mp 5 . . 3 (ran 𝑓𝐵 → (𝑓 𝐷) ⊆ 𝐵)
17 undif 4194 . . 3 ((𝑓 𝐷) ⊆ 𝐵 ↔ ((𝑓 𝐷) ∪ (𝐵 ∖ (𝑓 𝐷))) = 𝐵)
1816, 17sylib 208 . 2 (ran 𝑓𝐵 → ((𝑓 𝐷) ∪ (𝐵 ∖ (𝑓 𝐷))) = 𝐵)
1913, 18sylan9eqr 2817 1 ((ran 𝑓𝐵 ∧ ((dom 𝑔 = 𝐵 ∧ ran 𝑔𝐴) ∧ Fun 𝑔)) → ran 𝐻 = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383   = wceq 1632  wcel 2140  {cab 2747  Vcvv 3341  cdif 3713  cun 3714  wss 3716   cuni 4589  ccnv 5266  dom cdm 5267  ran crn 5268  cres 5269  cima 5270  Fun wfun 6044
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1989  ax-6 2055  ax-7 2091  ax-9 2149  ax-10 2169  ax-11 2184  ax-12 2197  ax-13 2392  ax-ext 2741  ax-sep 4934  ax-nul 4942  ax-pr 5056
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2048  df-eu 2612  df-mo 2613  df-clab 2748  df-cleq 2754  df-clel 2757  df-nfc 2892  df-ral 3056  df-rex 3057  df-rab 3060  df-v 3343  df-dif 3719  df-un 3721  df-in 3723  df-ss 3730  df-nul 4060  df-if 4232  df-sn 4323  df-pr 4325  df-op 4329  df-uni 4590  df-br 4806  df-opab 4866  df-id 5175  df-xp 5273  df-rel 5274  df-cnv 5275  df-co 5276  df-dm 5277  df-rn 5278  df-res 5279  df-ima 5280  df-fun 6052
This theorem is referenced by:  sbthlem9  8246
  Copyright terms: Public domain W3C validator