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

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

Proof of Theorem sbthlemi5
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 sbthlem.1 . . . . . . . . . 10 𝐴 ∈ V
2 sbthlem.2 . . . . . . . . . 10 𝐷 = {𝑥 ∣ (𝑥𝐴 ∧ (𝑔 “ (𝐵 ∖ (𝑓𝑥))) ⊆ (𝐴𝑥))}
31, 2sbthlem1 6645 . . . . . . . . 9 𝐷 ⊆ (𝐴 ∖ (𝑔 “ (𝐵 ∖ (𝑓 𝐷))))
4 difss 3124 . . . . . . . . 9 (𝐴 ∖ (𝑔 “ (𝐵 ∖ (𝑓 𝐷)))) ⊆ 𝐴
53, 4sstri 3032 . . . . . . . 8 𝐷𝐴
6 sseq2 3046 . . . . . . . 8 (dom 𝑓 = 𝐴 → ( 𝐷 ⊆ dom 𝑓 𝐷𝐴))
75, 6mpbiri 166 . . . . . . 7 (dom 𝑓 = 𝐴 𝐷 ⊆ dom 𝑓)
8 dfss 3011 . . . . . . 7 ( 𝐷 ⊆ dom 𝑓 𝐷 = ( 𝐷 ∩ dom 𝑓))
97, 8sylib 120 . . . . . 6 (dom 𝑓 = 𝐴 𝐷 = ( 𝐷 ∩ dom 𝑓))
109uneq1d 3151 . . . . 5 (dom 𝑓 = 𝐴 → ( 𝐷 ∪ (𝐴 𝐷)) = (( 𝐷 ∩ dom 𝑓) ∪ (𝐴 𝐷)))
111, 2sbthlemi3 6647 . . . . . . . 8 ((EXMID ∧ ran 𝑔𝐴) → (𝑔 “ (𝐵 ∖ (𝑓 𝐷))) = (𝐴 𝐷))
12 imassrn 4772 . . . . . . . 8 (𝑔 “ (𝐵 ∖ (𝑓 𝐷))) ⊆ ran 𝑔
1311, 12syl6eqssr 3075 . . . . . . 7 ((EXMID ∧ ran 𝑔𝐴) → (𝐴 𝐷) ⊆ ran 𝑔)
14 dfss 3011 . . . . . . 7 ((𝐴 𝐷) ⊆ ran 𝑔 ↔ (𝐴 𝐷) = ((𝐴 𝐷) ∩ ran 𝑔))
1513, 14sylib 120 . . . . . 6 ((EXMID ∧ ran 𝑔𝐴) → (𝐴 𝐷) = ((𝐴 𝐷) ∩ ran 𝑔))
1615uneq2d 3152 . . . . 5 ((EXMID ∧ ran 𝑔𝐴) → (( 𝐷 ∩ dom 𝑓) ∪ (𝐴 𝐷)) = (( 𝐷 ∩ dom 𝑓) ∪ ((𝐴 𝐷) ∩ ran 𝑔)))
1710, 16sylan9eq 2140 . . . 4 ((dom 𝑓 = 𝐴 ∧ (EXMID ∧ ran 𝑔𝐴)) → ( 𝐷 ∪ (𝐴 𝐷)) = (( 𝐷 ∩ dom 𝑓) ∪ ((𝐴 𝐷) ∩ ran 𝑔)))
1817an12s 532 . . 3 ((EXMID ∧ (dom 𝑓 = 𝐴 ∧ ran 𝑔𝐴)) → ( 𝐷 ∪ (𝐴 𝐷)) = (( 𝐷 ∩ dom 𝑓) ∪ ((𝐴 𝐷) ∩ ran 𝑔)))
19 sbthlem.3 . . . . 5 𝐻 = ((𝑓 𝐷) ∪ (𝑔 ↾ (𝐴 𝐷)))
2019dmeqi 4625 . . . 4 dom 𝐻 = dom ((𝑓 𝐷) ∪ (𝑔 ↾ (𝐴 𝐷)))
21 dmun 4631 . . . 4 dom ((𝑓 𝐷) ∪ (𝑔 ↾ (𝐴 𝐷))) = (dom (𝑓 𝐷) ∪ dom (𝑔 ↾ (𝐴 𝐷)))
22 dmres 4721 . . . . 5 dom (𝑓 𝐷) = ( 𝐷 ∩ dom 𝑓)
23 dmres 4721 . . . . . 6 dom (𝑔 ↾ (𝐴 𝐷)) = ((𝐴 𝐷) ∩ dom 𝑔)
24 df-rn 4439 . . . . . . . 8 ran 𝑔 = dom 𝑔
2524eqcomi 2092 . . . . . . 7 dom 𝑔 = ran 𝑔
2625ineq2i 3196 . . . . . 6 ((𝐴 𝐷) ∩ dom 𝑔) = ((𝐴 𝐷) ∩ ran 𝑔)
2723, 26eqtri 2108 . . . . 5 dom (𝑔 ↾ (𝐴 𝐷)) = ((𝐴 𝐷) ∩ ran 𝑔)
2822, 27uneq12i 3150 . . . 4 (dom (𝑓 𝐷) ∪ dom (𝑔 ↾ (𝐴 𝐷))) = (( 𝐷 ∩ dom 𝑓) ∪ ((𝐴 𝐷) ∩ ran 𝑔))
2920, 21, 283eqtri 2112 . . 3 dom 𝐻 = (( 𝐷 ∩ dom 𝑓) ∪ ((𝐴 𝐷) ∩ ran 𝑔))
3018, 29syl6reqr 2139 . 2 ((EXMID ∧ (dom 𝑓 = 𝐴 ∧ ran 𝑔𝐴)) → dom 𝐻 = ( 𝐷 ∪ (𝐴 𝐷)))
31 exmidexmid 4022 . . . . . . 7 (EXMIDDECID 𝑦 𝐷)
3231ralrimivw 2447 . . . . . 6 (EXMID → ∀𝑦𝐴 DECID 𝑦 𝐷)
3332biantrud 298 . . . . 5 (EXMID → ( 𝐷𝐴 ↔ ( 𝐷𝐴 ∧ ∀𝑦𝐴 DECID 𝑦 𝐷)))
34 undifdcss 6613 . . . . 5 (𝐴 = ( 𝐷 ∪ (𝐴 𝐷)) ↔ ( 𝐷𝐴 ∧ ∀𝑦𝐴 DECID 𝑦 𝐷))
3533, 34syl6rbbr 197 . . . 4 (EXMID → (𝐴 = ( 𝐷 ∪ (𝐴 𝐷)) ↔ 𝐷𝐴))
365, 35mpbiri 166 . . 3 (EXMID𝐴 = ( 𝐷 ∪ (𝐴 𝐷)))
3736adantr 270 . 2 ((EXMID ∧ (dom 𝑓 = 𝐴 ∧ ran 𝑔𝐴)) → 𝐴 = ( 𝐷 ∪ (𝐴 𝐷)))
3830, 37eqtr4d 2123 1 ((EXMID ∧ (dom 𝑓 = 𝐴 ∧ ran 𝑔𝐴)) → dom 𝐻 = 𝐴)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  DECID wdc 780   = wceq 1289  wcel 1438  {cab 2074  wral 2359  Vcvv 2619  cdif 2994  cun 2995  cin 2996  wss 2997   cuni 3648  EXMIDwem 4020  ccnv 4427  dom cdm 4428  ran crn 4429  cres 4430  cima 4431
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-xp 4434  df-cnv 4436  df-dm 4438  df-rn 4439  df-res 4440  df-ima 4441
This theorem is referenced by:  sbthlemi9  6653
  Copyright terms: Public domain W3C validator