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

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

Proof of Theorem sbthlemi4
StepHypRef Expression
1 df-ima 4625 . 2 (𝑔 “ (𝐴 𝐷)) = ran (𝑔 ↾ (𝐴 𝐷))
2 difss 3254 . . . . . . . 8 (𝐵 ∖ (𝑓 𝐷)) ⊆ 𝐵
3 sseq2 3172 . . . . . . . 8 (dom 𝑔 = 𝐵 → ((𝐵 ∖ (𝑓 𝐷)) ⊆ dom 𝑔 ↔ (𝐵 ∖ (𝑓 𝐷)) ⊆ 𝐵))
42, 3mpbiri 167 . . . . . . 7 (dom 𝑔 = 𝐵 → (𝐵 ∖ (𝑓 𝐷)) ⊆ dom 𝑔)
5 ssdmres 4914 . . . . . . 7 ((𝐵 ∖ (𝑓 𝐷)) ⊆ dom 𝑔 ↔ dom (𝑔 ↾ (𝐵 ∖ (𝑓 𝐷))) = (𝐵 ∖ (𝑓 𝐷)))
64, 5sylib 121 . . . . . 6 (dom 𝑔 = 𝐵 → dom (𝑔 ↾ (𝐵 ∖ (𝑓 𝐷))) = (𝐵 ∖ (𝑓 𝐷)))
7 dfdm4 4804 . . . . . 6 dom (𝑔 ↾ (𝐵 ∖ (𝑓 𝐷))) = ran (𝑔 ↾ (𝐵 ∖ (𝑓 𝐷)))
86, 7eqtr3di 2219 . . . . 5 (dom 𝑔 = 𝐵 → (𝐵 ∖ (𝑓 𝐷)) = ran (𝑔 ↾ (𝐵 ∖ (𝑓 𝐷))))
98adantr 274 . . . 4 ((dom 𝑔 = 𝐵 ∧ ran 𝑔𝐴) → (𝐵 ∖ (𝑓 𝐷)) = ran (𝑔 ↾ (𝐵 ∖ (𝑓 𝐷))))
1093ad2ant2 1015 . . 3 ((EXMID ∧ (dom 𝑔 = 𝐵 ∧ ran 𝑔𝐴) ∧ Fun 𝑔) → (𝐵 ∖ (𝑓 𝐷)) = ran (𝑔 ↾ (𝐵 ∖ (𝑓 𝐷))))
11 funcnvres 5273 . . . . . . 7 (Fun 𝑔(𝑔 ↾ (𝐵 ∖ (𝑓 𝐷))) = (𝑔 ↾ (𝑔 “ (𝐵 ∖ (𝑓 𝐷)))))
12113ad2ant3 1016 . . . . . 6 ((EXMID ∧ ran 𝑔𝐴 ∧ Fun 𝑔) → (𝑔 ↾ (𝐵 ∖ (𝑓 𝐷))) = (𝑔 ↾ (𝑔 “ (𝐵 ∖ (𝑓 𝐷)))))
13 sbthlem.1 . . . . . . . . 9 𝐴 ∈ V
14 sbthlem.2 . . . . . . . . 9 𝐷 = {𝑥 ∣ (𝑥𝐴 ∧ (𝑔 “ (𝐵 ∖ (𝑓𝑥))) ⊆ (𝐴𝑥))}
1513, 14sbthlemi3 6940 . . . . . . . 8 ((EXMID ∧ ran 𝑔𝐴) → (𝑔 “ (𝐵 ∖ (𝑓 𝐷))) = (𝐴 𝐷))
1615reseq2d 4892 . . . . . . 7 ((EXMID ∧ ran 𝑔𝐴) → (𝑔 ↾ (𝑔 “ (𝐵 ∖ (𝑓 𝐷)))) = (𝑔 ↾ (𝐴 𝐷)))
17163adant3 1013 . . . . . 6 ((EXMID ∧ ran 𝑔𝐴 ∧ Fun 𝑔) → (𝑔 ↾ (𝑔 “ (𝐵 ∖ (𝑓 𝐷)))) = (𝑔 ↾ (𝐴 𝐷)))
1812, 17eqtrd 2204 . . . . 5 ((EXMID ∧ ran 𝑔𝐴 ∧ Fun 𝑔) → (𝑔 ↾ (𝐵 ∖ (𝑓 𝐷))) = (𝑔 ↾ (𝐴 𝐷)))
1918rneqd 4841 . . . 4 ((EXMID ∧ ran 𝑔𝐴 ∧ Fun 𝑔) → ran (𝑔 ↾ (𝐵 ∖ (𝑓 𝐷))) = ran (𝑔 ↾ (𝐴 𝐷)))
20193adant2l 1228 . . 3 ((EXMID ∧ (dom 𝑔 = 𝐵 ∧ ran 𝑔𝐴) ∧ Fun 𝑔) → ran (𝑔 ↾ (𝐵 ∖ (𝑓 𝐷))) = ran (𝑔 ↾ (𝐴 𝐷)))
2110, 20eqtrd 2204 . 2 ((EXMID ∧ (dom 𝑔 = 𝐵 ∧ ran 𝑔𝐴) ∧ Fun 𝑔) → (𝐵 ∖ (𝑓 𝐷)) = ran (𝑔 ↾ (𝐴 𝐷)))
221, 21eqtr4id 2223 1 ((EXMID ∧ (dom 𝑔 = 𝐵 ∧ ran 𝑔𝐴) ∧ Fun 𝑔) → (𝑔 “ (𝐴 𝐷)) = (𝐵 ∖ (𝑓 𝐷)))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  w3a 974   = wceq 1349  wcel 2142  {cab 2157  Vcvv 2731  cdif 3119  wss 3122   cuni 3797  EXMIDwem 4181  ccnv 4611  dom cdm 4612  ran crn 4613  cres 4614  cima 4615  Fun wfun 5194
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 610  ax-in2 611  ax-io 705  ax-5 1441  ax-7 1442  ax-gen 1443  ax-ie1 1487  ax-ie2 1488  ax-8 1498  ax-10 1499  ax-11 1500  ax-i12 1501  ax-bndl 1503  ax-4 1504  ax-17 1520  ax-i9 1524  ax-ial 1528  ax-i5r 1529  ax-14 2145  ax-ext 2153  ax-sep 4108  ax-nul 4116  ax-pow 4161  ax-pr 4195
This theorem depends on definitions:  df-bi 116  df-stab 827  df-dc 831  df-3an 976  df-tru 1352  df-nf 1455  df-sb 1757  df-eu 2023  df-mo 2024  df-clab 2158  df-cleq 2164  df-clel 2167  df-nfc 2302  df-ral 2454  df-rex 2455  df-rab 2458  df-v 2733  df-dif 3124  df-un 3126  df-in 3128  df-ss 3135  df-nul 3416  df-pw 3569  df-sn 3590  df-pr 3591  df-op 3593  df-uni 3798  df-br 3991  df-opab 4052  df-exmid 4182  df-id 4279  df-xp 4618  df-rel 4619  df-cnv 4620  df-co 4621  df-dm 4622  df-rn 4623  df-res 4624  df-ima 4625  df-fun 5202
This theorem is referenced by:  sbthlemi6  6943  sbthlemi8  6945
  Copyright terms: Public domain W3C validator