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

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

Proof of Theorem sbthlemi3
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 sbthlem.1 . . . . . . 7 𝐴 ∈ V
2 sbthlem.2 . . . . . . 7 𝐷 = {𝑥 ∣ (𝑥𝐴 ∧ (𝑔 “ (𝐵 ∖ (𝑓𝑥))) ⊆ (𝐴𝑥))}
31, 2sbthlem2 6895 . . . . . 6 (ran 𝑔𝐴 → (𝐴 ∖ (𝑔 “ (𝐵 ∖ (𝑓 𝐷)))) ⊆ 𝐷)
41, 2sbthlem1 6894 . . . . . 6 𝐷 ⊆ (𝐴 ∖ (𝑔 “ (𝐵 ∖ (𝑓 𝐷))))
53, 4jctil 310 . . . . 5 (ran 𝑔𝐴 → ( 𝐷 ⊆ (𝐴 ∖ (𝑔 “ (𝐵 ∖ (𝑓 𝐷)))) ∧ (𝐴 ∖ (𝑔 “ (𝐵 ∖ (𝑓 𝐷)))) ⊆ 𝐷))
6 eqss 3143 . . . . 5 ( 𝐷 = (𝐴 ∖ (𝑔 “ (𝐵 ∖ (𝑓 𝐷)))) ↔ ( 𝐷 ⊆ (𝐴 ∖ (𝑔 “ (𝐵 ∖ (𝑓 𝐷)))) ∧ (𝐴 ∖ (𝑔 “ (𝐵 ∖ (𝑓 𝐷)))) ⊆ 𝐷))
75, 6sylibr 133 . . . 4 (ran 𝑔𝐴 𝐷 = (𝐴 ∖ (𝑔 “ (𝐵 ∖ (𝑓 𝐷)))))
87difeq2d 3225 . . 3 (ran 𝑔𝐴 → (𝐴 𝐷) = (𝐴 ∖ (𝐴 ∖ (𝑔 “ (𝐵 ∖ (𝑓 𝐷))))))
98adantl 275 . 2 ((EXMID ∧ ran 𝑔𝐴) → (𝐴 𝐷) = (𝐴 ∖ (𝐴 ∖ (𝑔 “ (𝐵 ∖ (𝑓 𝐷))))))
10 imassrn 4936 . . . . 5 (𝑔 “ (𝐵 ∖ (𝑓 𝐷))) ⊆ ran 𝑔
11 sstr2 3135 . . . . 5 ((𝑔 “ (𝐵 ∖ (𝑓 𝐷))) ⊆ ran 𝑔 → (ran 𝑔𝐴 → (𝑔 “ (𝐵 ∖ (𝑓 𝐷))) ⊆ 𝐴))
1210, 11ax-mp 5 . . . 4 (ran 𝑔𝐴 → (𝑔 “ (𝐵 ∖ (𝑓 𝐷))) ⊆ 𝐴)
13 exmidexmid 4156 . . . . . . 7 (EXMIDDECID 𝑦 ∈ (𝑔 “ (𝐵 ∖ (𝑓 𝐷))))
14 dcstab 830 . . . . . . 7 (DECID 𝑦 ∈ (𝑔 “ (𝐵 ∖ (𝑓 𝐷))) → STAB 𝑦 ∈ (𝑔 “ (𝐵 ∖ (𝑓 𝐷))))
1513, 14syl 14 . . . . . 6 (EXMIDSTAB 𝑦 ∈ (𝑔 “ (𝐵 ∖ (𝑓 𝐷))))
1615alrimiv 1854 . . . . 5 (EXMID → ∀𝑦STAB 𝑦 ∈ (𝑔 “ (𝐵 ∖ (𝑓 𝐷))))
17 dfss4st 3340 . . . . 5 (∀𝑦STAB 𝑦 ∈ (𝑔 “ (𝐵 ∖ (𝑓 𝐷))) → ((𝑔 “ (𝐵 ∖ (𝑓 𝐷))) ⊆ 𝐴 ↔ (𝐴 ∖ (𝐴 ∖ (𝑔 “ (𝐵 ∖ (𝑓 𝐷))))) = (𝑔 “ (𝐵 ∖ (𝑓 𝐷)))))
1816, 17syl 14 . . . 4 (EXMID → ((𝑔 “ (𝐵 ∖ (𝑓 𝐷))) ⊆ 𝐴 ↔ (𝐴 ∖ (𝐴 ∖ (𝑔 “ (𝐵 ∖ (𝑓 𝐷))))) = (𝑔 “ (𝐵 ∖ (𝑓 𝐷)))))
1912, 18syl5ib 153 . . 3 (EXMID → (ran 𝑔𝐴 → (𝐴 ∖ (𝐴 ∖ (𝑔 “ (𝐵 ∖ (𝑓 𝐷))))) = (𝑔 “ (𝐵 ∖ (𝑓 𝐷)))))
2019imp 123 . 2 ((EXMID ∧ ran 𝑔𝐴) → (𝐴 ∖ (𝐴 ∖ (𝑔 “ (𝐵 ∖ (𝑓 𝐷))))) = (𝑔 “ (𝐵 ∖ (𝑓 𝐷))))
219, 20eqtr2d 2191 1 ((EXMID ∧ ran 𝑔𝐴) → (𝑔 “ (𝐵 ∖ (𝑓 𝐷))) = (𝐴 𝐷))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104  STAB wstab 816  DECID wdc 820  ∀wal 1333   = wceq 1335   ∈ wcel 2128  {cab 2143  Vcvv 2712   ∖ cdif 3099   ⊆ wss 3102  ∪ cuni 3772  EXMIDwem 4154  ran crn 4584   “ cima 4586 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 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-14 2131  ax-ext 2139  ax-sep 4082  ax-nul 4090  ax-pow 4134  ax-pr 4168 This theorem depends on definitions:  df-bi 116  df-stab 817  df-dc 821  df-3an 965  df-tru 1338  df-nf 1441  df-sb 1743  df-eu 2009  df-mo 2010  df-clab 2144  df-cleq 2150  df-clel 2153  df-nfc 2288  df-ral 2440  df-rex 2441  df-rab 2444  df-v 2714  df-dif 3104  df-un 3106  df-in 3108  df-ss 3115  df-nul 3395  df-pw 3545  df-sn 3566  df-pr 3567  df-op 3569  df-uni 3773  df-br 3966  df-opab 4026  df-exmid 4155  df-xp 4589  df-cnv 4591  df-dm 4593  df-rn 4594  df-res 4595  df-ima 4596 This theorem is referenced by:  sbthlemi4  6897  sbthlemi5  6898
 Copyright terms: Public domain W3C validator