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

Theorem sbthlemi8 6652
Description: Lemma for isbth 6655. (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 5072 . . . 4 (Fun 𝑓 → Fun (𝑓 𝐷))
21ad2antlr 473 . . 3 (((EXMID ∧ Fun 𝑓) ∧ (((Fun 𝑔 ∧ dom 𝑔 = 𝐵) ∧ ran 𝑔𝐴) ∧ Fun 𝑔)) → Fun (𝑓 𝐷))
3 funcnvcnv 5059 . . . . . 6 (Fun 𝑔 → Fun 𝑔)
4 funres11 5072 . . . . . 6 (Fun 𝑔 → Fun (𝑔 ↾ (𝐴 𝐷)))
53, 4syl 14 . . . . 5 (Fun 𝑔 → Fun (𝑔 ↾ (𝐴 𝐷)))
65ad2antrr 472 . . . 4 (((Fun 𝑔 ∧ dom 𝑔 = 𝐵) ∧ ran 𝑔𝐴) → Fun (𝑔 ↾ (𝐴 𝐷)))
76ad2antrl 474 . . 3 (((EXMID ∧ Fun 𝑓) ∧ (((Fun 𝑔 ∧ dom 𝑔 = 𝐵) ∧ ran 𝑔𝐴) ∧ Fun 𝑔)) → Fun (𝑔 ↾ (𝐴 𝐷)))
8 simpll 496 . . . 4 (((EXMID ∧ Fun 𝑓) ∧ (((Fun 𝑔 ∧ dom 𝑔 = 𝐵) ∧ ran 𝑔𝐴) ∧ Fun 𝑔)) → EXMID)
9 simprll 504 . . . . 5 (((EXMID ∧ Fun 𝑓) ∧ (((Fun 𝑔 ∧ dom 𝑔 = 𝐵) ∧ ran 𝑔𝐴) ∧ Fun 𝑔)) → (Fun 𝑔 ∧ dom 𝑔 = 𝐵))
109simprd 112 . . . 4 (((EXMID ∧ Fun 𝑓) ∧ (((Fun 𝑔 ∧ dom 𝑔 = 𝐵) ∧ ran 𝑔𝐴) ∧ Fun 𝑔)) → dom 𝑔 = 𝐵)
11 simprlr 505 . . . 4 (((EXMID ∧ Fun 𝑓) ∧ (((Fun 𝑔 ∧ dom 𝑔 = 𝐵) ∧ ran 𝑔𝐴) ∧ Fun 𝑔)) → ran 𝑔𝐴)
12 simprr 499 . . . 4 (((EXMID ∧ Fun 𝑓) ∧ (((Fun 𝑔 ∧ dom 𝑔 = 𝐵) ∧ ran 𝑔𝐴) ∧ Fun 𝑔)) → Fun 𝑔)
13 df-ima 4441 . . . . . . 7 (𝑓 𝐷) = ran (𝑓 𝐷)
14 df-rn 4439 . . . . . . 7 ran (𝑓 𝐷) = dom (𝑓 𝐷)
1513, 14eqtr2i 2109 . . . . . 6 dom (𝑓 𝐷) = (𝑓 𝐷)
16 df-ima 4441 . . . . . . . 8 (𝑔 “ (𝐴 𝐷)) = ran (𝑔 ↾ (𝐴 𝐷))
17 df-rn 4439 . . . . . . . 8 ran (𝑔 ↾ (𝐴 𝐷)) = dom (𝑔 ↾ (𝐴 𝐷))
1816, 17eqtri 2108 . . . . . . 7 (𝑔 “ (𝐴 𝐷)) = dom (𝑔 ↾ (𝐴 𝐷))
19 sbthlem.1 . . . . . . . 8 𝐴 ∈ V
20 sbthlem.2 . . . . . . . 8 𝐷 = {𝑥 ∣ (𝑥𝐴 ∧ (𝑔 “ (𝐵 ∖ (𝑓𝑥))) ⊆ (𝐴𝑥))}
2119, 20sbthlemi4 6648 . . . . . . 7 ((EXMID ∧ (dom 𝑔 = 𝐵 ∧ ran 𝑔𝐴) ∧ Fun 𝑔) → (𝑔 “ (𝐴 𝐷)) = (𝐵 ∖ (𝑓 𝐷)))
2218, 21syl5eqr 2134 . . . . . 6 ((EXMID ∧ (dom 𝑔 = 𝐵 ∧ ran 𝑔𝐴) ∧ Fun 𝑔) → dom (𝑔 ↾ (𝐴 𝐷)) = (𝐵 ∖ (𝑓 𝐷)))
23 ineq12 3194 . . . . . 6 ((dom (𝑓 𝐷) = (𝑓 𝐷) ∧ dom (𝑔 ↾ (𝐴 𝐷)) = (𝐵 ∖ (𝑓 𝐷))) → (dom (𝑓 𝐷) ∩ dom (𝑔 ↾ (𝐴 𝐷))) = ((𝑓 𝐷) ∩ (𝐵 ∖ (𝑓 𝐷))))
2415, 22, 23sylancr 405 . . . . 5 ((EXMID ∧ (dom 𝑔 = 𝐵 ∧ ran 𝑔𝐴) ∧ Fun 𝑔) → (dom (𝑓 𝐷) ∩ dom (𝑔 ↾ (𝐴 𝐷))) = ((𝑓 𝐷) ∩ (𝐵 ∖ (𝑓 𝐷))))
25 disjdif 3352 . . . . 5 ((𝑓 𝐷) ∩ (𝐵 ∖ (𝑓 𝐷))) = ∅
2624, 25syl6eq 2136 . . . 4 ((EXMID ∧ (dom 𝑔 = 𝐵 ∧ ran 𝑔𝐴) ∧ Fun 𝑔) → (dom (𝑓 𝐷) ∩ dom (𝑔 ↾ (𝐴 𝐷))) = ∅)
278, 10, 11, 12, 26syl121anc 1179 . . 3 (((EXMID ∧ Fun 𝑓) ∧ (((Fun 𝑔 ∧ dom 𝑔 = 𝐵) ∧ ran 𝑔𝐴) ∧ Fun 𝑔)) → (dom (𝑓 𝐷) ∩ dom (𝑔 ↾ (𝐴 𝐷))) = ∅)
28 funun 5044 . . 3 (((Fun (𝑓 𝐷) ∧ Fun (𝑔 ↾ (𝐴 𝐷))) ∧ (dom (𝑓 𝐷) ∩ dom (𝑔 ↾ (𝐴 𝐷))) = ∅) → Fun ((𝑓 𝐷) ∪ (𝑔 ↾ (𝐴 𝐷))))
292, 7, 27, 28syl21anc 1173 . 2 (((EXMID ∧ Fun 𝑓) ∧ (((Fun 𝑔 ∧ dom 𝑔 = 𝐵) ∧ ran 𝑔𝐴) ∧ Fun 𝑔)) → Fun ((𝑓 𝐷) ∪ (𝑔 ↾ (𝐴 𝐷))))
30 sbthlem.3 . . . . 5 𝐻 = ((𝑓 𝐷) ∪ (𝑔 ↾ (𝐴 𝐷)))
3130cnveqi 4599 . . . 4 𝐻 = ((𝑓 𝐷) ∪ (𝑔 ↾ (𝐴 𝐷)))
32 cnvun 4824 . . . 4 ((𝑓 𝐷) ∪ (𝑔 ↾ (𝐴 𝐷))) = ((𝑓 𝐷) ∪ (𝑔 ↾ (𝐴 𝐷)))
3331, 32eqtri 2108 . . 3 𝐻 = ((𝑓 𝐷) ∪ (𝑔 ↾ (𝐴 𝐷)))
3433funeqi 5022 . 2 (Fun 𝐻 ↔ Fun ((𝑓 𝐷) ∪ (𝑔 ↾ (𝐴 𝐷))))
3529, 34sylibr 132 1 (((EXMID ∧ Fun 𝑓) ∧ (((Fun 𝑔 ∧ dom 𝑔 = 𝐵) ∧ ran 𝑔𝐴) ∧ Fun 𝑔)) → Fun 𝐻)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  w3a 924   = wceq 1289  wcel 1438  {cab 2074  Vcvv 2619  cdif 2994  cun 2995  cin 2996  wss 2997  c0 3284   cuni 3648  EXMIDwem 4020  ccnv 4427  dom cdm 4428  ran crn 4429  cres 4430  cima 4431  Fun wfun 4996
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 579  ax-in2 580  ax-io 665  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-10 1441  ax-11 1442  ax-i12 1443  ax-bndl 1444  ax-4 1445  ax-14 1450  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070  ax-sep 3949  ax-nul 3957  ax-pow 4001  ax-pr 4027
This theorem depends on definitions:  df-bi 115  df-stab 776  df-dc 781  df-3an 926  df-tru 1292  df-nf 1395  df-sb 1693  df-eu 1951  df-mo 1952  df-clab 2075  df-cleq 2081  df-clel 2084  df-nfc 2217  df-ral 2364  df-rex 2365  df-rab 2368  df-v 2621  df-dif 2999  df-un 3001  df-in 3003  df-ss 3010  df-nul 3285  df-pw 3427  df-sn 3447  df-pr 3448  df-op 3450  df-uni 3649  df-br 3838  df-opab 3892  df-exmid 4021  df-id 4111  df-xp 4434  df-rel 4435  df-cnv 4436  df-co 4437  df-dm 4438  df-rn 4439  df-res 4440  df-ima 4441  df-fun 5004
This theorem is referenced by:  sbthlemi9  6653
  Copyright terms: Public domain W3C validator