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

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

Proof of Theorem sbthlem8
StepHypRef Expression
1 funres11 6583 . . . 4 (Fun 𝑓 → Fun (𝑓 𝐷))
2 funcnvcnv 6573 . . . . . 6 (Fun 𝑔 → Fun 𝑔)
3 funres11 6583 . . . . . 6 (Fun 𝑔 → Fun (𝑔 ↾ (𝐴 𝐷)))
42, 3syl 17 . . . . 5 (Fun 𝑔 → Fun (𝑔 ↾ (𝐴 𝐷)))
54ad3antrrr 729 . . . 4 ((((Fun 𝑔 ∧ dom 𝑔 = 𝐵) ∧ ran 𝑔𝐴) ∧ Fun 𝑔) → Fun (𝑔 ↾ (𝐴 𝐷)))
61, 5anim12i 614 . . 3 ((Fun 𝑓 ∧ (((Fun 𝑔 ∧ dom 𝑔 = 𝐵) ∧ ran 𝑔𝐴) ∧ Fun 𝑔)) → (Fun (𝑓 𝐷) ∧ Fun (𝑔 ↾ (𝐴 𝐷))))
7 df-ima 5651 . . . . . . . 8 (𝑓 𝐷) = ran (𝑓 𝐷)
8 df-rn 5649 . . . . . . . 8 ran (𝑓 𝐷) = dom (𝑓 𝐷)
97, 8eqtr2i 2766 . . . . . . 7 dom (𝑓 𝐷) = (𝑓 𝐷)
10 df-ima 5651 . . . . . . . . 9 (𝑔 “ (𝐴 𝐷)) = ran (𝑔 ↾ (𝐴 𝐷))
11 df-rn 5649 . . . . . . . . 9 ran (𝑔 ↾ (𝐴 𝐷)) = dom (𝑔 ↾ (𝐴 𝐷))
1210, 11eqtri 2765 . . . . . . . 8 (𝑔 “ (𝐴 𝐷)) = dom (𝑔 ↾ (𝐴 𝐷))
13 sbthlem.1 . . . . . . . . 9 𝐴 ∈ V
14 sbthlem.2 . . . . . . . . 9 𝐷 = {𝑥 ∣ (𝑥𝐴 ∧ (𝑔 “ (𝐵 ∖ (𝑓𝑥))) ⊆ (𝐴𝑥))}
1513, 14sbthlem4 9037 . . . . . . . 8 (((dom 𝑔 = 𝐵 ∧ ran 𝑔𝐴) ∧ Fun 𝑔) → (𝑔 “ (𝐴 𝐷)) = (𝐵 ∖ (𝑓 𝐷)))
1612, 15eqtr3id 2791 . . . . . . 7 (((dom 𝑔 = 𝐵 ∧ ran 𝑔𝐴) ∧ Fun 𝑔) → dom (𝑔 ↾ (𝐴 𝐷)) = (𝐵 ∖ (𝑓 𝐷)))
17 ineq12 4172 . . . . . . 7 ((dom (𝑓 𝐷) = (𝑓 𝐷) ∧ dom (𝑔 ↾ (𝐴 𝐷)) = (𝐵 ∖ (𝑓 𝐷))) → (dom (𝑓 𝐷) ∩ dom (𝑔 ↾ (𝐴 𝐷))) = ((𝑓 𝐷) ∩ (𝐵 ∖ (𝑓 𝐷))))
189, 16, 17sylancr 588 . . . . . 6 (((dom 𝑔 = 𝐵 ∧ ran 𝑔𝐴) ∧ Fun 𝑔) → (dom (𝑓 𝐷) ∩ dom (𝑔 ↾ (𝐴 𝐷))) = ((𝑓 𝐷) ∩ (𝐵 ∖ (𝑓 𝐷))))
19 disjdif 4436 . . . . . 6 ((𝑓 𝐷) ∩ (𝐵 ∖ (𝑓 𝐷))) = ∅
2018, 19eqtrdi 2793 . . . . 5 (((dom 𝑔 = 𝐵 ∧ ran 𝑔𝐴) ∧ Fun 𝑔) → (dom (𝑓 𝐷) ∩ dom (𝑔 ↾ (𝐴 𝐷))) = ∅)
2120adantlll 717 . . . 4 ((((Fun 𝑔 ∧ dom 𝑔 = 𝐵) ∧ ran 𝑔𝐴) ∧ Fun 𝑔) → (dom (𝑓 𝐷) ∩ dom (𝑔 ↾ (𝐴 𝐷))) = ∅)
2221adantl 483 . . 3 ((Fun 𝑓 ∧ (((Fun 𝑔 ∧ dom 𝑔 = 𝐵) ∧ ran 𝑔𝐴) ∧ Fun 𝑔)) → (dom (𝑓 𝐷) ∩ dom (𝑔 ↾ (𝐴 𝐷))) = ∅)
23 funun 6552 . . 3 (((Fun (𝑓 𝐷) ∧ Fun (𝑔 ↾ (𝐴 𝐷))) ∧ (dom (𝑓 𝐷) ∩ dom (𝑔 ↾ (𝐴 𝐷))) = ∅) → Fun ((𝑓 𝐷) ∪ (𝑔 ↾ (𝐴 𝐷))))
246, 22, 23syl2anc 585 . 2 ((Fun 𝑓 ∧ (((Fun 𝑔 ∧ dom 𝑔 = 𝐵) ∧ ran 𝑔𝐴) ∧ Fun 𝑔)) → Fun ((𝑓 𝐷) ∪ (𝑔 ↾ (𝐴 𝐷))))
25 sbthlem.3 . . . . 5 𝐻 = ((𝑓 𝐷) ∪ (𝑔 ↾ (𝐴 𝐷)))
2625cnveqi 5835 . . . 4 𝐻 = ((𝑓 𝐷) ∪ (𝑔 ↾ (𝐴 𝐷)))
27 cnvun 6100 . . . 4 ((𝑓 𝐷) ∪ (𝑔 ↾ (𝐴 𝐷))) = ((𝑓 𝐷) ∪ (𝑔 ↾ (𝐴 𝐷)))
2826, 27eqtri 2765 . . 3 𝐻 = ((𝑓 𝐷) ∪ (𝑔 ↾ (𝐴 𝐷)))
2928funeqi 6527 . 2 (Fun 𝐻 ↔ Fun ((𝑓 𝐷) ∪ (𝑔 ↾ (𝐴 𝐷))))
3024, 29sylibr 233 1 ((Fun 𝑓 ∧ (((Fun 𝑔 ∧ dom 𝑔 = 𝐵) ∧ ran 𝑔𝐴) ∧ Fun 𝑔)) → Fun 𝐻)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397   = wceq 1542  wcel 2107  {cab 2714  Vcvv 3448  cdif 3912  cun 3913  cin 3914  wss 3915  c0 4287   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:  sbthlem9  9042
  Copyright terms: Public domain W3C validator