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

Theorem sbthlemi5 6859
 Description: Lemma for isbth 6865. (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.3 . . . . 5 𝐻 = ((𝑓 𝐷) ∪ (𝑔 ↾ (𝐴 𝐷)))
21dmeqi 4749 . . . 4 dom 𝐻 = dom ((𝑓 𝐷) ∪ (𝑔 ↾ (𝐴 𝐷)))
3 dmun 4755 . . . 4 dom ((𝑓 𝐷) ∪ (𝑔 ↾ (𝐴 𝐷))) = (dom (𝑓 𝐷) ∪ dom (𝑔 ↾ (𝐴 𝐷)))
4 dmres 4849 . . . . 5 dom (𝑓 𝐷) = ( 𝐷 ∩ dom 𝑓)
5 dmres 4849 . . . . . 6 dom (𝑔 ↾ (𝐴 𝐷)) = ((𝐴 𝐷) ∩ dom 𝑔)
6 df-rn 4559 . . . . . . . 8 ran 𝑔 = dom 𝑔
76eqcomi 2144 . . . . . . 7 dom 𝑔 = ran 𝑔
87ineq2i 3280 . . . . . 6 ((𝐴 𝐷) ∩ dom 𝑔) = ((𝐴 𝐷) ∩ ran 𝑔)
95, 8eqtri 2161 . . . . 5 dom (𝑔 ↾ (𝐴 𝐷)) = ((𝐴 𝐷) ∩ ran 𝑔)
104, 9uneq12i 3234 . . . 4 (dom (𝑓 𝐷) ∪ dom (𝑔 ↾ (𝐴 𝐷))) = (( 𝐷 ∩ dom 𝑓) ∪ ((𝐴 𝐷) ∩ ran 𝑔))
112, 3, 103eqtri 2165 . . 3 dom 𝐻 = (( 𝐷 ∩ dom 𝑓) ∪ ((𝐴 𝐷) ∩ ran 𝑔))
12 sbthlem.1 . . . . . . . . . 10 𝐴 ∈ V
13 sbthlem.2 . . . . . . . . . 10 𝐷 = {𝑥 ∣ (𝑥𝐴 ∧ (𝑔 “ (𝐵 ∖ (𝑓𝑥))) ⊆ (𝐴𝑥))}
1412, 13sbthlem1 6855 . . . . . . . . 9 𝐷 ⊆ (𝐴 ∖ (𝑔 “ (𝐵 ∖ (𝑓 𝐷))))
15 difss 3208 . . . . . . . . 9 (𝐴 ∖ (𝑔 “ (𝐵 ∖ (𝑓 𝐷)))) ⊆ 𝐴
1614, 15sstri 3112 . . . . . . . 8 𝐷𝐴
17 sseq2 3127 . . . . . . . 8 (dom 𝑓 = 𝐴 → ( 𝐷 ⊆ dom 𝑓 𝐷𝐴))
1816, 17mpbiri 167 . . . . . . 7 (dom 𝑓 = 𝐴 𝐷 ⊆ dom 𝑓)
19 dfss 3091 . . . . . . 7 ( 𝐷 ⊆ dom 𝑓 𝐷 = ( 𝐷 ∩ dom 𝑓))
2018, 19sylib 121 . . . . . 6 (dom 𝑓 = 𝐴 𝐷 = ( 𝐷 ∩ dom 𝑓))
2120uneq1d 3235 . . . . 5 (dom 𝑓 = 𝐴 → ( 𝐷 ∪ (𝐴 𝐷)) = (( 𝐷 ∩ dom 𝑓) ∪ (𝐴 𝐷)))
2212, 13sbthlemi3 6857 . . . . . . . 8 ((EXMID ∧ ran 𝑔𝐴) → (𝑔 “ (𝐵 ∖ (𝑓 𝐷))) = (𝐴 𝐷))
23 imassrn 4901 . . . . . . . 8 (𝑔 “ (𝐵 ∖ (𝑓 𝐷))) ⊆ ran 𝑔
2422, 23eqsstrrdi 3156 . . . . . . 7 ((EXMID ∧ ran 𝑔𝐴) → (𝐴 𝐷) ⊆ ran 𝑔)
25 dfss 3091 . . . . . . 7 ((𝐴 𝐷) ⊆ ran 𝑔 ↔ (𝐴 𝐷) = ((𝐴 𝐷) ∩ ran 𝑔))
2624, 25sylib 121 . . . . . 6 ((EXMID ∧ ran 𝑔𝐴) → (𝐴 𝐷) = ((𝐴 𝐷) ∩ ran 𝑔))
2726uneq2d 3236 . . . . 5 ((EXMID ∧ ran 𝑔𝐴) → (( 𝐷 ∩ dom 𝑓) ∪ (𝐴 𝐷)) = (( 𝐷 ∩ dom 𝑓) ∪ ((𝐴 𝐷) ∩ ran 𝑔)))
2821, 27sylan9eq 2193 . . . 4 ((dom 𝑓 = 𝐴 ∧ (EXMID ∧ ran 𝑔𝐴)) → ( 𝐷 ∪ (𝐴 𝐷)) = (( 𝐷 ∩ dom 𝑓) ∪ ((𝐴 𝐷) ∩ ran 𝑔)))
2928an12s 555 . . 3 ((EXMID ∧ (dom 𝑓 = 𝐴 ∧ ran 𝑔𝐴)) → ( 𝐷 ∪ (𝐴 𝐷)) = (( 𝐷 ∩ dom 𝑓) ∪ ((𝐴 𝐷) ∩ ran 𝑔)))
3011, 29eqtr4id 2192 . 2 ((EXMID ∧ (dom 𝑓 = 𝐴 ∧ ran 𝑔𝐴)) → dom 𝐻 = ( 𝐷 ∪ (𝐴 𝐷)))
31 undifdcss 6821 . . . . 5 (𝐴 = ( 𝐷 ∪ (𝐴 𝐷)) ↔ ( 𝐷𝐴 ∧ ∀𝑦𝐴 DECID 𝑦 𝐷))
32 exmidexmid 4129 . . . . . . 7 (EXMIDDECID 𝑦 𝐷)
3332ralrimivw 2510 . . . . . 6 (EXMID → ∀𝑦𝐴 DECID 𝑦 𝐷)
3433biantrud 302 . . . . 5 (EXMID → ( 𝐷𝐴 ↔ ( 𝐷𝐴 ∧ ∀𝑦𝐴 DECID 𝑦 𝐷)))
3531, 34bitr4id 198 . . . 4 (EXMID → (𝐴 = ( 𝐷 ∪ (𝐴 𝐷)) ↔ 𝐷𝐴))
3616, 35mpbiri 167 . . 3 (EXMID𝐴 = ( 𝐷 ∪ (𝐴 𝐷)))
3736adantr 274 . 2 ((EXMID ∧ (dom 𝑓 = 𝐴 ∧ ran 𝑔𝐴)) → 𝐴 = ( 𝐷 ∪ (𝐴 𝐷)))
3830, 37eqtr4d 2176 1 ((EXMID ∧ (dom 𝑓 = 𝐴 ∧ ran 𝑔𝐴)) → dom 𝐻 = 𝐴)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103  DECID wdc 820   = wceq 1332   ∈ wcel 1481  {cab 2126  ∀wral 2417  Vcvv 2690   ∖ cdif 3074   ∪ cun 3075   ∩ cin 3076   ⊆ wss 3077  ∪ cuni 3745  EXMIDwem 4127  ◡ccnv 4547  dom cdm 4548  ran crn 4549   ↾ cres 4550   “ cima 4551 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-14 1493  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-sep 4055  ax-nul 4063  ax-pow 4107  ax-pr 4140 This theorem depends on definitions:  df-bi 116  df-stab 817  df-dc 821  df-3an 965  df-tru 1335  df-nf 1438  df-sb 1737  df-eu 2003  df-mo 2004  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-ral 2422  df-rex 2423  df-rab 2426  df-v 2692  df-dif 3079  df-un 3081  df-in 3083  df-ss 3090  df-nul 3370  df-pw 3518  df-sn 3539  df-pr 3540  df-op 3542  df-uni 3746  df-br 3939  df-opab 3999  df-exmid 4128  df-xp 4554  df-cnv 4556  df-dm 4558  df-rn 4559  df-res 4560  df-ima 4561 This theorem is referenced by:  sbthlemi9  6863
 Copyright terms: Public domain W3C validator