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

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

Proof of Theorem sbthlem7
StepHypRef Expression
1 funres 6548 . . 3 (Fun 𝑓 → Fun (𝑓 𝐷))
2 funres 6548 . . 3 (Fun 𝑔 → Fun (𝑔 ↾ (𝐴 𝐷)))
3 dmres 5964 . . . . . . . . 9 dom (𝑓 𝐷) = ( 𝐷 ∩ dom 𝑓)
4 inss1 4193 . . . . . . . . 9 ( 𝐷 ∩ dom 𝑓) ⊆ 𝐷
53, 4eqsstri 3983 . . . . . . . 8 dom (𝑓 𝐷) ⊆ 𝐷
6 ssrin 4198 . . . . . . . 8 (dom (𝑓 𝐷) ⊆ 𝐷 → (dom (𝑓 𝐷) ∩ dom (𝑔 ↾ (𝐴 𝐷))) ⊆ ( 𝐷 ∩ dom (𝑔 ↾ (𝐴 𝐷))))
75, 6ax-mp 5 . . . . . . 7 (dom (𝑓 𝐷) ∩ dom (𝑔 ↾ (𝐴 𝐷))) ⊆ ( 𝐷 ∩ dom (𝑔 ↾ (𝐴 𝐷)))
8 dmres 5964 . . . . . . . . 9 dom (𝑔 ↾ (𝐴 𝐷)) = ((𝐴 𝐷) ∩ dom 𝑔)
9 inss1 4193 . . . . . . . . 9 ((𝐴 𝐷) ∩ dom 𝑔) ⊆ (𝐴 𝐷)
108, 9eqsstri 3983 . . . . . . . 8 dom (𝑔 ↾ (𝐴 𝐷)) ⊆ (𝐴 𝐷)
11 sslin 4199 . . . . . . . 8 (dom (𝑔 ↾ (𝐴 𝐷)) ⊆ (𝐴 𝐷) → ( 𝐷 ∩ dom (𝑔 ↾ (𝐴 𝐷))) ⊆ ( 𝐷 ∩ (𝐴 𝐷)))
1210, 11ax-mp 5 . . . . . . 7 ( 𝐷 ∩ dom (𝑔 ↾ (𝐴 𝐷))) ⊆ ( 𝐷 ∩ (𝐴 𝐷))
137, 12sstri 3958 . . . . . 6 (dom (𝑓 𝐷) ∩ dom (𝑔 ↾ (𝐴 𝐷))) ⊆ ( 𝐷 ∩ (𝐴 𝐷))
14 disjdif 4436 . . . . . 6 ( 𝐷 ∩ (𝐴 𝐷)) = ∅
1513, 14sseqtri 3985 . . . . 5 (dom (𝑓 𝐷) ∩ dom (𝑔 ↾ (𝐴 𝐷))) ⊆ ∅
16 ss0 4363 . . . . 5 ((dom (𝑓 𝐷) ∩ dom (𝑔 ↾ (𝐴 𝐷))) ⊆ ∅ → (dom (𝑓 𝐷) ∩ dom (𝑔 ↾ (𝐴 𝐷))) = ∅)
1715, 16ax-mp 5 . . . 4 (dom (𝑓 𝐷) ∩ dom (𝑔 ↾ (𝐴 𝐷))) = ∅
18 funun 6552 . . . 4 (((Fun (𝑓 𝐷) ∧ Fun (𝑔 ↾ (𝐴 𝐷))) ∧ (dom (𝑓 𝐷) ∩ dom (𝑔 ↾ (𝐴 𝐷))) = ∅) → Fun ((𝑓 𝐷) ∪ (𝑔 ↾ (𝐴 𝐷))))
1917, 18mpan2 690 . . 3 ((Fun (𝑓 𝐷) ∧ Fun (𝑔 ↾ (𝐴 𝐷))) → Fun ((𝑓 𝐷) ∪ (𝑔 ↾ (𝐴 𝐷))))
201, 2, 19syl2an 597 . 2 ((Fun 𝑓 ∧ Fun 𝑔) → Fun ((𝑓 𝐷) ∪ (𝑔 ↾ (𝐴 𝐷))))
21 sbthlem.3 . . 3 𝐻 = ((𝑓 𝐷) ∪ (𝑔 ↾ (𝐴 𝐷)))
2221funeqi 6527 . 2 (Fun 𝐻 ↔ Fun ((𝑓 𝐷) ∪ (𝑔 ↾ (𝐴 𝐷))))
2320, 22sylibr 233 1 ((Fun 𝑓 ∧ 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  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-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-sb 2069  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-br 5111  df-opab 5173  df-id 5536  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-res 5650  df-fun 6503
This theorem is referenced by:  sbthlem9  9042
  Copyright terms: Public domain W3C validator