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

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

Proof of Theorem sbthlemi6
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 simpll 518 . . 3 (((EXMID ∧ ran 𝑓𝐵) ∧ ((dom 𝑔 = 𝐵 ∧ ran 𝑔𝐴) ∧ Fun 𝑔)) → EXMID)
2 simprll 526 . . 3 (((EXMID ∧ ran 𝑓𝐵) ∧ ((dom 𝑔 = 𝐵 ∧ ran 𝑔𝐴) ∧ Fun 𝑔)) → dom 𝑔 = 𝐵)
3 simprlr 527 . . 3 (((EXMID ∧ ran 𝑓𝐵) ∧ ((dom 𝑔 = 𝐵 ∧ ran 𝑔𝐴) ∧ Fun 𝑔)) → ran 𝑔𝐴)
4 simprr 521 . . 3 (((EXMID ∧ ran 𝑓𝐵) ∧ ((dom 𝑔 = 𝐵 ∧ ran 𝑔𝐴) ∧ Fun 𝑔)) → Fun 𝑔)
5 df-ima 4547 . . . . . 6 (𝑔 “ (𝐴 𝐷)) = ran (𝑔 ↾ (𝐴 𝐷))
6 sbthlem.1 . . . . . . 7 𝐴 ∈ V
7 sbthlem.2 . . . . . . 7 𝐷 = {𝑥 ∣ (𝑥𝐴 ∧ (𝑔 “ (𝐵 ∖ (𝑓𝑥))) ⊆ (𝐴𝑥))}
86, 7sbthlemi4 6841 . . . . . 6 ((EXMID ∧ (dom 𝑔 = 𝐵 ∧ ran 𝑔𝐴) ∧ Fun 𝑔) → (𝑔 “ (𝐴 𝐷)) = (𝐵 ∖ (𝑓 𝐷)))
95, 8syl5reqr 2185 . . . . 5 ((EXMID ∧ (dom 𝑔 = 𝐵 ∧ ran 𝑔𝐴) ∧ Fun 𝑔) → (𝐵 ∖ (𝑓 𝐷)) = ran (𝑔 ↾ (𝐴 𝐷)))
109uneq2d 3225 . . . 4 ((EXMID ∧ (dom 𝑔 = 𝐵 ∧ ran 𝑔𝐴) ∧ Fun 𝑔) → ((𝑓 𝐷) ∪ (𝐵 ∖ (𝑓 𝐷))) = ((𝑓 𝐷) ∪ ran (𝑔 ↾ (𝐴 𝐷))))
11 rnun 4942 . . . . 5 ran ((𝑓 𝐷) ∪ (𝑔 ↾ (𝐴 𝐷))) = (ran (𝑓 𝐷) ∪ ran (𝑔 ↾ (𝐴 𝐷)))
12 sbthlem.3 . . . . . 6 𝐻 = ((𝑓 𝐷) ∪ (𝑔 ↾ (𝐴 𝐷)))
1312rneqi 4762 . . . . 5 ran 𝐻 = ran ((𝑓 𝐷) ∪ (𝑔 ↾ (𝐴 𝐷)))
14 df-ima 4547 . . . . . 6 (𝑓 𝐷) = ran (𝑓 𝐷)
1514uneq1i 3221 . . . . 5 ((𝑓 𝐷) ∪ ran (𝑔 ↾ (𝐴 𝐷))) = (ran (𝑓 𝐷) ∪ ran (𝑔 ↾ (𝐴 𝐷)))
1611, 13, 153eqtr4i 2168 . . . 4 ran 𝐻 = ((𝑓 𝐷) ∪ ran (𝑔 ↾ (𝐴 𝐷)))
1710, 16syl6reqr 2189 . . 3 ((EXMID ∧ (dom 𝑔 = 𝐵 ∧ ran 𝑔𝐴) ∧ Fun 𝑔) → ran 𝐻 = ((𝑓 𝐷) ∪ (𝐵 ∖ (𝑓 𝐷))))
181, 2, 3, 4, 17syl121anc 1221 . 2 (((EXMID ∧ ran 𝑓𝐵) ∧ ((dom 𝑔 = 𝐵 ∧ ran 𝑔𝐴) ∧ Fun 𝑔)) → ran 𝐻 = ((𝑓 𝐷) ∪ (𝐵 ∖ (𝑓 𝐷))))
19 imassrn 4887 . . . . . . 7 (𝑓 𝐷) ⊆ ran 𝑓
20 sstr2 3099 . . . . . . 7 ((𝑓 𝐷) ⊆ ran 𝑓 → (ran 𝑓𝐵 → (𝑓 𝐷) ⊆ 𝐵))
2119, 20ax-mp 5 . . . . . 6 (ran 𝑓𝐵 → (𝑓 𝐷) ⊆ 𝐵)
2221adantl 275 . . . . 5 ((EXMID ∧ ran 𝑓𝐵) → (𝑓 𝐷) ⊆ 𝐵)
23 exmidexmid 4115 . . . . . . . . 9 (EXMIDDECID 𝑦 ∈ (𝑓 𝐷))
2423ralrimivw 2504 . . . . . . . 8 (EXMID → ∀𝑦𝐵 DECID 𝑦 ∈ (𝑓 𝐷))
2524biantrud 302 . . . . . . 7 (EXMID → ((𝑓 𝐷) ⊆ 𝐵 ↔ ((𝑓 𝐷) ⊆ 𝐵 ∧ ∀𝑦𝐵 DECID 𝑦 ∈ (𝑓 𝐷))))
26 undifdcss 6804 . . . . . . 7 (𝐵 = ((𝑓 𝐷) ∪ (𝐵 ∖ (𝑓 𝐷))) ↔ ((𝑓 𝐷) ⊆ 𝐵 ∧ ∀𝑦𝐵 DECID 𝑦 ∈ (𝑓 𝐷)))
2725, 26syl6rbbr 198 . . . . . 6 (EXMID → (𝐵 = ((𝑓 𝐷) ∪ (𝐵 ∖ (𝑓 𝐷))) ↔ (𝑓 𝐷) ⊆ 𝐵))
2827adantr 274 . . . . 5 ((EXMID ∧ ran 𝑓𝐵) → (𝐵 = ((𝑓 𝐷) ∪ (𝐵 ∖ (𝑓 𝐷))) ↔ (𝑓 𝐷) ⊆ 𝐵))
2922, 28mpbird 166 . . . 4 ((EXMID ∧ ran 𝑓𝐵) → 𝐵 = ((𝑓 𝐷) ∪ (𝐵 ∖ (𝑓 𝐷))))
3029eqcomd 2143 . . 3 ((EXMID ∧ ran 𝑓𝐵) → ((𝑓 𝐷) ∪ (𝐵 ∖ (𝑓 𝐷))) = 𝐵)
3130adantr 274 . 2 (((EXMID ∧ ran 𝑓𝐵) ∧ ((dom 𝑔 = 𝐵 ∧ ran 𝑔𝐴) ∧ Fun 𝑔)) → ((𝑓 𝐷) ∪ (𝐵 ∖ (𝑓 𝐷))) = 𝐵)
3218, 31eqtrd 2170 1 (((EXMID ∧ ran 𝑓𝐵) ∧ ((dom 𝑔 = 𝐵 ∧ ran 𝑔𝐴) ∧ Fun 𝑔)) → ran 𝐻 = 𝐵)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104  DECID wdc 819   ∧ w3a 962   = wceq 1331   ∈ wcel 1480  {cab 2123  ∀wral 2414  Vcvv 2681   ∖ cdif 3063   ∪ cun 3064   ⊆ wss 3066  ∪ cuni 3731  EXMIDwem 4113  ◡ccnv 4533  dom cdm 4534  ran crn 4535   ↾ cres 4536   “ cima 4537  Fun wfun 5112 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 603  ax-in2 604  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-14 1492  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2119  ax-sep 4041  ax-nul 4049  ax-pow 4093  ax-pr 4126 This theorem depends on definitions:  df-bi 116  df-stab 816  df-dc 820  df-3an 964  df-tru 1334  df-nf 1437  df-sb 1736  df-eu 2000  df-mo 2001  df-clab 2124  df-cleq 2130  df-clel 2133  df-nfc 2268  df-ral 2419  df-rex 2420  df-rab 2423  df-v 2683  df-dif 3068  df-un 3070  df-in 3072  df-ss 3079  df-nul 3359  df-pw 3507  df-sn 3528  df-pr 3529  df-op 3531  df-uni 3732  df-br 3925  df-opab 3985  df-exmid 4114  df-id 4210  df-xp 4540  df-rel 4541  df-cnv 4542  df-co 4543  df-dm 4544  df-rn 4545  df-res 4546  df-ima 4547  df-fun 5120 This theorem is referenced by:  sbthlemi9  6846
 Copyright terms: Public domain W3C validator