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

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

Proof of Theorem sbthlemi9
StepHypRef Expression
1 simp2 944 . . . . . . . . . 10 ((EXMID𝑓:𝐴1-1𝐵𝑔:𝐵1-1𝐴) → 𝑓:𝐴1-1𝐵)
2 df-f1 5007 . . . . . . . . . 10 (𝑓:𝐴1-1𝐵 ↔ (𝑓:𝐴𝐵 ∧ Fun 𝑓))
31, 2sylib 120 . . . . . . . . 9 ((EXMID𝑓:𝐴1-1𝐵𝑔:𝐵1-1𝐴) → (𝑓:𝐴𝐵 ∧ Fun 𝑓))
43simpld 110 . . . . . . . 8 ((EXMID𝑓:𝐴1-1𝐵𝑔:𝐵1-1𝐴) → 𝑓:𝐴𝐵)
5 df-f 5006 . . . . . . . 8 (𝑓:𝐴𝐵 ↔ (𝑓 Fn 𝐴 ∧ ran 𝑓𝐵))
64, 5sylib 120 . . . . . . 7 ((EXMID𝑓:𝐴1-1𝐵𝑔:𝐵1-1𝐴) → (𝑓 Fn 𝐴 ∧ ran 𝑓𝐵))
76simpld 110 . . . . . 6 ((EXMID𝑓:𝐴1-1𝐵𝑔:𝐵1-1𝐴) → 𝑓 Fn 𝐴)
8 df-fn 5005 . . . . . 6 (𝑓 Fn 𝐴 ↔ (Fun 𝑓 ∧ dom 𝑓 = 𝐴))
97, 8sylib 120 . . . . 5 ((EXMID𝑓:𝐴1-1𝐵𝑔:𝐵1-1𝐴) → (Fun 𝑓 ∧ dom 𝑓 = 𝐴))
109simpld 110 . . . 4 ((EXMID𝑓:𝐴1-1𝐵𝑔:𝐵1-1𝐴) → Fun 𝑓)
11 simp3 945 . . . . . 6 ((EXMID𝑓:𝐴1-1𝐵𝑔:𝐵1-1𝐴) → 𝑔:𝐵1-1𝐴)
12 df-f1 5007 . . . . . 6 (𝑔:𝐵1-1𝐴 ↔ (𝑔:𝐵𝐴 ∧ Fun 𝑔))
1311, 12sylib 120 . . . . 5 ((EXMID𝑓:𝐴1-1𝐵𝑔:𝐵1-1𝐴) → (𝑔:𝐵𝐴 ∧ Fun 𝑔))
1413simprd 112 . . . 4 ((EXMID𝑓:𝐴1-1𝐵𝑔:𝐵1-1𝐴) → Fun 𝑔)
15 sbthlem.1 . . . . 5 𝐴 ∈ V
16 sbthlem.2 . . . . 5 𝐷 = {𝑥 ∣ (𝑥𝐴 ∧ (𝑔 “ (𝐵 ∖ (𝑓𝑥))) ⊆ (𝐴𝑥))}
17 sbthlem.3 . . . . 5 𝐻 = ((𝑓 𝐷) ∪ (𝑔 ↾ (𝐴 𝐷)))
1815, 16, 17sbthlem7 6651 . . . 4 ((Fun 𝑓 ∧ Fun 𝑔) → Fun 𝐻)
1910, 14, 18syl2anc 403 . . 3 ((EXMID𝑓:𝐴1-1𝐵𝑔:𝐵1-1𝐴) → Fun 𝐻)
20 simp1 943 . . . 4 ((EXMID𝑓:𝐴1-1𝐵𝑔:𝐵1-1𝐴) → EXMID)
219simprd 112 . . . 4 ((EXMID𝑓:𝐴1-1𝐵𝑔:𝐵1-1𝐴) → dom 𝑓 = 𝐴)
2213simpld 110 . . . . . 6 ((EXMID𝑓:𝐴1-1𝐵𝑔:𝐵1-1𝐴) → 𝑔:𝐵𝐴)
23 df-f 5006 . . . . . 6 (𝑔:𝐵𝐴 ↔ (𝑔 Fn 𝐵 ∧ ran 𝑔𝐴))
2422, 23sylib 120 . . . . 5 ((EXMID𝑓:𝐴1-1𝐵𝑔:𝐵1-1𝐴) → (𝑔 Fn 𝐵 ∧ ran 𝑔𝐴))
2524simprd 112 . . . 4 ((EXMID𝑓:𝐴1-1𝐵𝑔:𝐵1-1𝐴) → ran 𝑔𝐴)
2615, 16, 17sbthlemi5 6649 . . . 4 ((EXMID ∧ (dom 𝑓 = 𝐴 ∧ ran 𝑔𝐴)) → dom 𝐻 = 𝐴)
2720, 21, 25, 26syl12anc 1172 . . 3 ((EXMID𝑓:𝐴1-1𝐵𝑔:𝐵1-1𝐴) → dom 𝐻 = 𝐴)
28 df-fn 5005 . . 3 (𝐻 Fn 𝐴 ↔ (Fun 𝐻 ∧ dom 𝐻 = 𝐴))
2919, 27, 28sylanbrc 408 . 2 ((EXMID𝑓:𝐴1-1𝐵𝑔:𝐵1-1𝐴) → 𝐻 Fn 𝐴)
303simprd 112 . . . 4 ((EXMID𝑓:𝐴1-1𝐵𝑔:𝐵1-1𝐴) → Fun 𝑓)
3124simpld 110 . . . . . 6 ((EXMID𝑓:𝐴1-1𝐵𝑔:𝐵1-1𝐴) → 𝑔 Fn 𝐵)
32 df-fn 5005 . . . . . 6 (𝑔 Fn 𝐵 ↔ (Fun 𝑔 ∧ dom 𝑔 = 𝐵))
3331, 32sylib 120 . . . . 5 ((EXMID𝑓:𝐴1-1𝐵𝑔:𝐵1-1𝐴) → (Fun 𝑔 ∧ dom 𝑔 = 𝐵))
3433, 25jca 300 . . . 4 ((EXMID𝑓:𝐴1-1𝐵𝑔:𝐵1-1𝐴) → ((Fun 𝑔 ∧ dom 𝑔 = 𝐵) ∧ ran 𝑔𝐴))
3515, 16, 17sbthlemi8 6652 . . . 4 (((EXMID ∧ Fun 𝑓) ∧ (((Fun 𝑔 ∧ dom 𝑔 = 𝐵) ∧ ran 𝑔𝐴) ∧ Fun 𝑔)) → Fun 𝐻)
3620, 30, 34, 14, 35syl22anc 1175 . . 3 ((EXMID𝑓:𝐴1-1𝐵𝑔:𝐵1-1𝐴) → Fun 𝐻)
376simprd 112 . . . 4 ((EXMID𝑓:𝐴1-1𝐵𝑔:𝐵1-1𝐴) → ran 𝑓𝐵)
3833simprd 112 . . . . 5 ((EXMID𝑓:𝐴1-1𝐵𝑔:𝐵1-1𝐴) → dom 𝑔 = 𝐵)
3938, 25jca 300 . . . 4 ((EXMID𝑓:𝐴1-1𝐵𝑔:𝐵1-1𝐴) → (dom 𝑔 = 𝐵 ∧ ran 𝑔𝐴))
40 df-rn 4439 . . . . 5 ran 𝐻 = dom 𝐻
4115, 16, 17sbthlemi6 6650 . . . . 5 (((EXMID ∧ ran 𝑓𝐵) ∧ ((dom 𝑔 = 𝐵 ∧ ran 𝑔𝐴) ∧ Fun 𝑔)) → ran 𝐻 = 𝐵)
4240, 41syl5eqr 2134 . . . 4 (((EXMID ∧ ran 𝑓𝐵) ∧ ((dom 𝑔 = 𝐵 ∧ ran 𝑔𝐴) ∧ Fun 𝑔)) → dom 𝐻 = 𝐵)
4320, 37, 39, 14, 42syl22anc 1175 . . 3 ((EXMID𝑓:𝐴1-1𝐵𝑔:𝐵1-1𝐴) → dom 𝐻 = 𝐵)
44 df-fn 5005 . . 3 (𝐻 Fn 𝐵 ↔ (Fun 𝐻 ∧ dom 𝐻 = 𝐵))
4536, 43, 44sylanbrc 408 . 2 ((EXMID𝑓:𝐴1-1𝐵𝑔:𝐵1-1𝐴) → 𝐻 Fn 𝐵)
46 dff1o4 5245 . 2 (𝐻:𝐴1-1-onto𝐵 ↔ (𝐻 Fn 𝐴𝐻 Fn 𝐵))
4729, 45, 46sylanbrc 408 1 ((EXMID𝑓:𝐴1-1𝐵𝑔:𝐵1-1𝐴) → 𝐻:𝐴1-1-onto𝐵)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  w3a 924   = wceq 1289  wcel 1438  {cab 2074  Vcvv 2619  cdif 2994  cun 2995  wss 2997   cuni 3648  EXMIDwem 4020  ccnv 4427  dom cdm 4428  ran crn 4429  cres 4430  cima 4431  Fun wfun 4996   Fn wfn 4997  wf 4998  1-1wf1 4999  1-1-ontowf1o 5001
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-id 4111  df-xp 4434  df-rel 4435  df-cnv 4436  df-co 4437  df-dm 4438  df-rn 4439  df-res 4440  df-ima 4441  df-fun 5004  df-fn 5005  df-f 5006  df-f1 5007  df-fo 5008  df-f1o 5009
This theorem is referenced by:  sbthlemi10  6654
  Copyright terms: Public domain W3C validator