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

Theorem sbthlem8 8875
Description: Lemma for sbth 8878. (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 6513 . . . 4 (Fun 𝑓 → Fun (𝑓 𝐷))
2 funcnvcnv 6503 . . . . . 6 (Fun 𝑔 → Fun 𝑔)
3 funres11 6513 . . . . . 6 (Fun 𝑔 → Fun (𝑔 ↾ (𝐴 𝐷)))
42, 3syl 17 . . . . 5 (Fun 𝑔 → Fun (𝑔 ↾ (𝐴 𝐷)))
54ad3antrrr 727 . . . 4 ((((Fun 𝑔 ∧ dom 𝑔 = 𝐵) ∧ ran 𝑔𝐴) ∧ Fun 𝑔) → Fun (𝑔 ↾ (𝐴 𝐷)))
61, 5anim12i 613 . . 3 ((Fun 𝑓 ∧ (((Fun 𝑔 ∧ dom 𝑔 = 𝐵) ∧ ran 𝑔𝐴) ∧ Fun 𝑔)) → (Fun (𝑓 𝐷) ∧ Fun (𝑔 ↾ (𝐴 𝐷))))
7 df-ima 5604 . . . . . . . 8 (𝑓 𝐷) = ran (𝑓 𝐷)
8 df-rn 5602 . . . . . . . 8 ran (𝑓 𝐷) = dom (𝑓 𝐷)
97, 8eqtr2i 2767 . . . . . . 7 dom (𝑓 𝐷) = (𝑓 𝐷)
10 df-ima 5604 . . . . . . . . 9 (𝑔 “ (𝐴 𝐷)) = ran (𝑔 ↾ (𝐴 𝐷))
11 df-rn 5602 . . . . . . . . 9 ran (𝑔 ↾ (𝐴 𝐷)) = dom (𝑔 ↾ (𝐴 𝐷))
1210, 11eqtri 2766 . . . . . . . 8 (𝑔 “ (𝐴 𝐷)) = dom (𝑔 ↾ (𝐴 𝐷))
13 sbthlem.1 . . . . . . . . 9 𝐴 ∈ V
14 sbthlem.2 . . . . . . . . 9 𝐷 = {𝑥 ∣ (𝑥𝐴 ∧ (𝑔 “ (𝐵 ∖ (𝑓𝑥))) ⊆ (𝐴𝑥))}
1513, 14sbthlem4 8871 . . . . . . . 8 (((dom 𝑔 = 𝐵 ∧ ran 𝑔𝐴) ∧ Fun 𝑔) → (𝑔 “ (𝐴 𝐷)) = (𝐵 ∖ (𝑓 𝐷)))
1612, 15eqtr3id 2792 . . . . . . 7 (((dom 𝑔 = 𝐵 ∧ ran 𝑔𝐴) ∧ Fun 𝑔) → dom (𝑔 ↾ (𝐴 𝐷)) = (𝐵 ∖ (𝑓 𝐷)))
17 ineq12 4143 . . . . . . 7 ((dom (𝑓 𝐷) = (𝑓 𝐷) ∧ dom (𝑔 ↾ (𝐴 𝐷)) = (𝐵 ∖ (𝑓 𝐷))) → (dom (𝑓 𝐷) ∩ dom (𝑔 ↾ (𝐴 𝐷))) = ((𝑓 𝐷) ∩ (𝐵 ∖ (𝑓 𝐷))))
189, 16, 17sylancr 587 . . . . . 6 (((dom 𝑔 = 𝐵 ∧ ran 𝑔𝐴) ∧ Fun 𝑔) → (dom (𝑓 𝐷) ∩ dom (𝑔 ↾ (𝐴 𝐷))) = ((𝑓 𝐷) ∩ (𝐵 ∖ (𝑓 𝐷))))
19 disjdif 4407 . . . . . 6 ((𝑓 𝐷) ∩ (𝐵 ∖ (𝑓 𝐷))) = ∅
2018, 19eqtrdi 2794 . . . . 5 (((dom 𝑔 = 𝐵 ∧ ran 𝑔𝐴) ∧ Fun 𝑔) → (dom (𝑓 𝐷) ∩ dom (𝑔 ↾ (𝐴 𝐷))) = ∅)
2120adantlll 715 . . . 4 ((((Fun 𝑔 ∧ dom 𝑔 = 𝐵) ∧ ran 𝑔𝐴) ∧ Fun 𝑔) → (dom (𝑓 𝐷) ∩ dom (𝑔 ↾ (𝐴 𝐷))) = ∅)
2221adantl 482 . . 3 ((Fun 𝑓 ∧ (((Fun 𝑔 ∧ dom 𝑔 = 𝐵) ∧ ran 𝑔𝐴) ∧ Fun 𝑔)) → (dom (𝑓 𝐷) ∩ dom (𝑔 ↾ (𝐴 𝐷))) = ∅)
23 funun 6482 . . 3 (((Fun (𝑓 𝐷) ∧ Fun (𝑔 ↾ (𝐴 𝐷))) ∧ (dom (𝑓 𝐷) ∩ dom (𝑔 ↾ (𝐴 𝐷))) = ∅) → Fun ((𝑓 𝐷) ∪ (𝑔 ↾ (𝐴 𝐷))))
246, 22, 23syl2anc 584 . 2 ((Fun 𝑓 ∧ (((Fun 𝑔 ∧ dom 𝑔 = 𝐵) ∧ ran 𝑔𝐴) ∧ Fun 𝑔)) → Fun ((𝑓 𝐷) ∪ (𝑔 ↾ (𝐴 𝐷))))
25 sbthlem.3 . . . . 5 𝐻 = ((𝑓 𝐷) ∪ (𝑔 ↾ (𝐴 𝐷)))
2625cnveqi 5785 . . . 4 𝐻 = ((𝑓 𝐷) ∪ (𝑔 ↾ (𝐴 𝐷)))
27 cnvun 6048 . . . 4 ((𝑓 𝐷) ∪ (𝑔 ↾ (𝐴 𝐷))) = ((𝑓 𝐷) ∪ (𝑔 ↾ (𝐴 𝐷)))
2826, 27eqtri 2766 . . 3 𝐻 = ((𝑓 𝐷) ∪ (𝑔 ↾ (𝐴 𝐷)))
2928funeqi 6457 . 2 (Fun 𝐻 ↔ Fun ((𝑓 𝐷) ∪ (𝑔 ↾ (𝐴 𝐷))))
3024, 29sylibr 233 1 ((Fun 𝑓 ∧ (((Fun 𝑔 ∧ dom 𝑔 = 𝐵) ∧ ran 𝑔𝐴) ∧ Fun 𝑔)) → Fun 𝐻)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1539  wcel 2106  {cab 2715  Vcvv 3431  cdif 3885  cun 3886  cin 3887  wss 3888  c0 4258   cuni 4841  ccnv 5590  dom cdm 5591  ran crn 5592  cres 5593  cima 5594  Fun wfun 6429
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-sep 5225  ax-nul 5232  ax-pr 5354
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3433  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4259  df-if 4462  df-sn 4564  df-pr 4566  df-op 4570  df-uni 4842  df-br 5077  df-opab 5139  df-id 5491  df-xp 5597  df-rel 5598  df-cnv 5599  df-co 5600  df-dm 5601  df-rn 5602  df-res 5603  df-ima 5604  df-fun 6437
This theorem is referenced by:  sbthlem9  8876
  Copyright terms: Public domain W3C validator