ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  sbthlemi8 GIF version

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

Proof of Theorem sbthlemi8
StepHypRef Expression
1 funres11 5330 . . . 4 (Fun 𝑓 → Fun (𝑓 𝐷))
21ad2antlr 489 . . 3 (((EXMID ∧ Fun 𝑓) ∧ (((Fun 𝑔 ∧ dom 𝑔 = 𝐵) ∧ ran 𝑔𝐴) ∧ Fun 𝑔)) → Fun (𝑓 𝐷))
3 funcnvcnv 5317 . . . . . 6 (Fun 𝑔 → Fun 𝑔)
4 funres11 5330 . . . . . 6 (Fun 𝑔 → Fun (𝑔 ↾ (𝐴 𝐷)))
53, 4syl 14 . . . . 5 (Fun 𝑔 → Fun (𝑔 ↾ (𝐴 𝐷)))
65ad2antrr 488 . . . 4 (((Fun 𝑔 ∧ dom 𝑔 = 𝐵) ∧ ran 𝑔𝐴) → Fun (𝑔 ↾ (𝐴 𝐷)))
76ad2antrl 490 . . 3 (((EXMID ∧ Fun 𝑓) ∧ (((Fun 𝑔 ∧ dom 𝑔 = 𝐵) ∧ ran 𝑔𝐴) ∧ Fun 𝑔)) → Fun (𝑔 ↾ (𝐴 𝐷)))
8 simpll 527 . . . 4 (((EXMID ∧ Fun 𝑓) ∧ (((Fun 𝑔 ∧ dom 𝑔 = 𝐵) ∧ ran 𝑔𝐴) ∧ Fun 𝑔)) → EXMID)
9 simprll 537 . . . . 5 (((EXMID ∧ Fun 𝑓) ∧ (((Fun 𝑔 ∧ dom 𝑔 = 𝐵) ∧ ran 𝑔𝐴) ∧ Fun 𝑔)) → (Fun 𝑔 ∧ dom 𝑔 = 𝐵))
109simprd 114 . . . 4 (((EXMID ∧ Fun 𝑓) ∧ (((Fun 𝑔 ∧ dom 𝑔 = 𝐵) ∧ ran 𝑔𝐴) ∧ Fun 𝑔)) → dom 𝑔 = 𝐵)
11 simprlr 538 . . . 4 (((EXMID ∧ Fun 𝑓) ∧ (((Fun 𝑔 ∧ dom 𝑔 = 𝐵) ∧ ran 𝑔𝐴) ∧ Fun 𝑔)) → ran 𝑔𝐴)
12 simprr 531 . . . 4 (((EXMID ∧ Fun 𝑓) ∧ (((Fun 𝑔 ∧ dom 𝑔 = 𝐵) ∧ ran 𝑔𝐴) ∧ Fun 𝑔)) → Fun 𝑔)
13 df-ima 4676 . . . . . . 7 (𝑓 𝐷) = ran (𝑓 𝐷)
14 df-rn 4674 . . . . . . 7 ran (𝑓 𝐷) = dom (𝑓 𝐷)
1513, 14eqtr2i 2218 . . . . . 6 dom (𝑓 𝐷) = (𝑓 𝐷)
16 df-ima 4676 . . . . . . . 8 (𝑔 “ (𝐴 𝐷)) = ran (𝑔 ↾ (𝐴 𝐷))
17 df-rn 4674 . . . . . . . 8 ran (𝑔 ↾ (𝐴 𝐷)) = dom (𝑔 ↾ (𝐴 𝐷))
1816, 17eqtri 2217 . . . . . . 7 (𝑔 “ (𝐴 𝐷)) = dom (𝑔 ↾ (𝐴 𝐷))
19 sbthlem.1 . . . . . . . 8 𝐴 ∈ V
20 sbthlem.2 . . . . . . . 8 𝐷 = {𝑥 ∣ (𝑥𝐴 ∧ (𝑔 “ (𝐵 ∖ (𝑓𝑥))) ⊆ (𝐴𝑥))}
2119, 20sbthlemi4 7026 . . . . . . 7 ((EXMID ∧ (dom 𝑔 = 𝐵 ∧ ran 𝑔𝐴) ∧ Fun 𝑔) → (𝑔 “ (𝐴 𝐷)) = (𝐵 ∖ (𝑓 𝐷)))
2218, 21eqtr3id 2243 . . . . . 6 ((EXMID ∧ (dom 𝑔 = 𝐵 ∧ ran 𝑔𝐴) ∧ Fun 𝑔) → dom (𝑔 ↾ (𝐴 𝐷)) = (𝐵 ∖ (𝑓 𝐷)))
23 ineq12 3359 . . . . . 6 ((dom (𝑓 𝐷) = (𝑓 𝐷) ∧ dom (𝑔 ↾ (𝐴 𝐷)) = (𝐵 ∖ (𝑓 𝐷))) → (dom (𝑓 𝐷) ∩ dom (𝑔 ↾ (𝐴 𝐷))) = ((𝑓 𝐷) ∩ (𝐵 ∖ (𝑓 𝐷))))
2415, 22, 23sylancr 414 . . . . 5 ((EXMID ∧ (dom 𝑔 = 𝐵 ∧ ran 𝑔𝐴) ∧ Fun 𝑔) → (dom (𝑓 𝐷) ∩ dom (𝑔 ↾ (𝐴 𝐷))) = ((𝑓 𝐷) ∩ (𝐵 ∖ (𝑓 𝐷))))
25 disjdif 3523 . . . . 5 ((𝑓 𝐷) ∩ (𝐵 ∖ (𝑓 𝐷))) = ∅
2624, 25eqtrdi 2245 . . . 4 ((EXMID ∧ (dom 𝑔 = 𝐵 ∧ ran 𝑔𝐴) ∧ Fun 𝑔) → (dom (𝑓 𝐷) ∩ dom (𝑔 ↾ (𝐴 𝐷))) = ∅)
278, 10, 11, 12, 26syl121anc 1254 . . 3 (((EXMID ∧ Fun 𝑓) ∧ (((Fun 𝑔 ∧ dom 𝑔 = 𝐵) ∧ ran 𝑔𝐴) ∧ Fun 𝑔)) → (dom (𝑓 𝐷) ∩ dom (𝑔 ↾ (𝐴 𝐷))) = ∅)
28 funun 5302 . . 3 (((Fun (𝑓 𝐷) ∧ Fun (𝑔 ↾ (𝐴 𝐷))) ∧ (dom (𝑓 𝐷) ∩ dom (𝑔 ↾ (𝐴 𝐷))) = ∅) → Fun ((𝑓 𝐷) ∪ (𝑔 ↾ (𝐴 𝐷))))
292, 7, 27, 28syl21anc 1248 . 2 (((EXMID ∧ Fun 𝑓) ∧ (((Fun 𝑔 ∧ dom 𝑔 = 𝐵) ∧ ran 𝑔𝐴) ∧ Fun 𝑔)) → Fun ((𝑓 𝐷) ∪ (𝑔 ↾ (𝐴 𝐷))))
30 sbthlem.3 . . . . 5 𝐻 = ((𝑓 𝐷) ∪ (𝑔 ↾ (𝐴 𝐷)))
3130cnveqi 4841 . . . 4 𝐻 = ((𝑓 𝐷) ∪ (𝑔 ↾ (𝐴 𝐷)))
32 cnvun 5075 . . . 4 ((𝑓 𝐷) ∪ (𝑔 ↾ (𝐴 𝐷))) = ((𝑓 𝐷) ∪ (𝑔 ↾ (𝐴 𝐷)))
3331, 32eqtri 2217 . . 3 𝐻 = ((𝑓 𝐷) ∪ (𝑔 ↾ (𝐴 𝐷)))
3433funeqi 5279 . 2 (Fun 𝐻 ↔ Fun ((𝑓 𝐷) ∪ (𝑔 ↾ (𝐴 𝐷))))
3529, 34sylibr 134 1 (((EXMID ∧ Fun 𝑓) ∧ (((Fun 𝑔 ∧ dom 𝑔 = 𝐵) ∧ ran 𝑔𝐴) ∧ Fun 𝑔)) → Fun 𝐻)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104  w3a 980   = wceq 1364  wcel 2167  {cab 2182  Vcvv 2763  cdif 3154  cun 3155  cin 3156  wss 3157  c0 3450   cuni 3839  EXMIDwem 4227  ccnv 4662  dom cdm 4663  ran crn 4664  cres 4665  cima 4666  Fun wfun 5252
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-14 2170  ax-ext 2178  ax-sep 4151  ax-nul 4159  ax-pow 4207  ax-pr 4242
This theorem depends on definitions:  df-bi 117  df-stab 832  df-dc 836  df-3an 982  df-tru 1367  df-nf 1475  df-sb 1777  df-eu 2048  df-mo 2049  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-ral 2480  df-rex 2481  df-rab 2484  df-v 2765  df-dif 3159  df-un 3161  df-in 3163  df-ss 3170  df-nul 3451  df-pw 3607  df-sn 3628  df-pr 3629  df-op 3631  df-uni 3840  df-br 4034  df-opab 4095  df-exmid 4228  df-id 4328  df-xp 4669  df-rel 4670  df-cnv 4671  df-co 4672  df-dm 4673  df-rn 4674  df-res 4675  df-ima 4676  df-fun 5260
This theorem is referenced by:  sbthlemi9  7031
  Copyright terms: Public domain W3C validator