MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sbthlem9 Structured version   Visualization version   GIF version

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

Proof of Theorem sbthlem9
StepHypRef Expression
1 sbthlem.1 . . . . . . . 8 𝐴 ∈ V
2 sbthlem.2 . . . . . . . 8 𝐷 = {𝑥 ∣ (𝑥𝐴 ∧ (𝑔 “ (𝐵 ∖ (𝑓𝑥))) ⊆ (𝐴𝑥))}
3 sbthlem.3 . . . . . . . 8 𝐻 = ((𝑓 𝐷) ∪ (𝑔 ↾ (𝐴 𝐷)))
41, 2, 3sbthlem7 9091 . . . . . . 7 ((Fun 𝑓 ∧ Fun 𝑔) → Fun 𝐻)
51, 2, 3sbthlem5 9089 . . . . . . . 8 ((dom 𝑓 = 𝐴 ∧ ran 𝑔𝐴) → dom 𝐻 = 𝐴)
65adantrl 714 . . . . . . 7 ((dom 𝑓 = 𝐴 ∧ ((Fun 𝑔 ∧ dom 𝑔 = 𝐵) ∧ ran 𝑔𝐴)) → dom 𝐻 = 𝐴)
74, 6anim12i 613 . . . . . 6 (((Fun 𝑓 ∧ Fun 𝑔) ∧ (dom 𝑓 = 𝐴 ∧ ((Fun 𝑔 ∧ dom 𝑔 = 𝐵) ∧ ran 𝑔𝐴))) → (Fun 𝐻 ∧ dom 𝐻 = 𝐴))
87an42s 659 . . . . 5 (((Fun 𝑓 ∧ dom 𝑓 = 𝐴) ∧ (((Fun 𝑔 ∧ dom 𝑔 = 𝐵) ∧ ran 𝑔𝐴) ∧ Fun 𝑔)) → (Fun 𝐻 ∧ dom 𝐻 = 𝐴))
98adantlr 713 . . . 4 ((((Fun 𝑓 ∧ dom 𝑓 = 𝐴) ∧ ran 𝑓𝐵) ∧ (((Fun 𝑔 ∧ dom 𝑔 = 𝐵) ∧ ran 𝑔𝐴) ∧ Fun 𝑔)) → (Fun 𝐻 ∧ dom 𝐻 = 𝐴))
109adantlr 713 . . 3 (((((Fun 𝑓 ∧ dom 𝑓 = 𝐴) ∧ ran 𝑓𝐵) ∧ Fun 𝑓) ∧ (((Fun 𝑔 ∧ dom 𝑔 = 𝐵) ∧ ran 𝑔𝐴) ∧ Fun 𝑔)) → (Fun 𝐻 ∧ dom 𝐻 = 𝐴))
111, 2, 3sbthlem8 9092 . . . 4 ((Fun 𝑓 ∧ (((Fun 𝑔 ∧ dom 𝑔 = 𝐵) ∧ ran 𝑔𝐴) ∧ Fun 𝑔)) → Fun 𝐻)
1211adantll 712 . . 3 (((((Fun 𝑓 ∧ dom 𝑓 = 𝐴) ∧ ran 𝑓𝐵) ∧ Fun 𝑓) ∧ (((Fun 𝑔 ∧ dom 𝑔 = 𝐵) ∧ ran 𝑔𝐴) ∧ Fun 𝑔)) → Fun 𝐻)
13 simpr 485 . . . . . . 7 ((Fun 𝑔 ∧ dom 𝑔 = 𝐵) → dom 𝑔 = 𝐵)
1413anim1i 615 . . . . . 6 (((Fun 𝑔 ∧ dom 𝑔 = 𝐵) ∧ ran 𝑔𝐴) → (dom 𝑔 = 𝐵 ∧ ran 𝑔𝐴))
15 df-rn 5687 . . . . . . 7 ran 𝐻 = dom 𝐻
161, 2, 3sbthlem6 9090 . . . . . . 7 ((ran 𝑓𝐵 ∧ ((dom 𝑔 = 𝐵 ∧ ran 𝑔𝐴) ∧ Fun 𝑔)) → ran 𝐻 = 𝐵)
1715, 16eqtr3id 2786 . . . . . 6 ((ran 𝑓𝐵 ∧ ((dom 𝑔 = 𝐵 ∧ ran 𝑔𝐴) ∧ Fun 𝑔)) → dom 𝐻 = 𝐵)
1814, 17sylanr1 680 . . . . 5 ((ran 𝑓𝐵 ∧ (((Fun 𝑔 ∧ dom 𝑔 = 𝐵) ∧ ran 𝑔𝐴) ∧ Fun 𝑔)) → dom 𝐻 = 𝐵)
1918adantll 712 . . . 4 ((((Fun 𝑓 ∧ dom 𝑓 = 𝐴) ∧ ran 𝑓𝐵) ∧ (((Fun 𝑔 ∧ dom 𝑔 = 𝐵) ∧ ran 𝑔𝐴) ∧ Fun 𝑔)) → dom 𝐻 = 𝐵)
2019adantlr 713 . . 3 (((((Fun 𝑓 ∧ dom 𝑓 = 𝐴) ∧ ran 𝑓𝐵) ∧ Fun 𝑓) ∧ (((Fun 𝑔 ∧ dom 𝑔 = 𝐵) ∧ ran 𝑔𝐴) ∧ Fun 𝑔)) → dom 𝐻 = 𝐵)
2110, 12, 20jca32 516 . 2 (((((Fun 𝑓 ∧ dom 𝑓 = 𝐴) ∧ ran 𝑓𝐵) ∧ Fun 𝑓) ∧ (((Fun 𝑔 ∧ dom 𝑔 = 𝐵) ∧ ran 𝑔𝐴) ∧ Fun 𝑔)) → ((Fun 𝐻 ∧ dom 𝐻 = 𝐴) ∧ (Fun 𝐻 ∧ dom 𝐻 = 𝐵)))
22 df-f1 6548 . . . 4 (𝑓:𝐴1-1𝐵 ↔ (𝑓:𝐴𝐵 ∧ Fun 𝑓))
23 df-f 6547 . . . . . 6 (𝑓:𝐴𝐵 ↔ (𝑓 Fn 𝐴 ∧ ran 𝑓𝐵))
24 df-fn 6546 . . . . . . 7 (𝑓 Fn 𝐴 ↔ (Fun 𝑓 ∧ dom 𝑓 = 𝐴))
2524anbi1i 624 . . . . . 6 ((𝑓 Fn 𝐴 ∧ ran 𝑓𝐵) ↔ ((Fun 𝑓 ∧ dom 𝑓 = 𝐴) ∧ ran 𝑓𝐵))
2623, 25bitri 274 . . . . 5 (𝑓:𝐴𝐵 ↔ ((Fun 𝑓 ∧ dom 𝑓 = 𝐴) ∧ ran 𝑓𝐵))
2726anbi1i 624 . . . 4 ((𝑓:𝐴𝐵 ∧ Fun 𝑓) ↔ (((Fun 𝑓 ∧ dom 𝑓 = 𝐴) ∧ ran 𝑓𝐵) ∧ Fun 𝑓))
2822, 27bitri 274 . . 3 (𝑓:𝐴1-1𝐵 ↔ (((Fun 𝑓 ∧ dom 𝑓 = 𝐴) ∧ ran 𝑓𝐵) ∧ Fun 𝑓))
29 df-f1 6548 . . . 4 (𝑔:𝐵1-1𝐴 ↔ (𝑔:𝐵𝐴 ∧ Fun 𝑔))
30 df-f 6547 . . . . . 6 (𝑔:𝐵𝐴 ↔ (𝑔 Fn 𝐵 ∧ ran 𝑔𝐴))
31 df-fn 6546 . . . . . . 7 (𝑔 Fn 𝐵 ↔ (Fun 𝑔 ∧ dom 𝑔 = 𝐵))
3231anbi1i 624 . . . . . 6 ((𝑔 Fn 𝐵 ∧ ran 𝑔𝐴) ↔ ((Fun 𝑔 ∧ dom 𝑔 = 𝐵) ∧ ran 𝑔𝐴))
3330, 32bitri 274 . . . . 5 (𝑔:𝐵𝐴 ↔ ((Fun 𝑔 ∧ dom 𝑔 = 𝐵) ∧ ran 𝑔𝐴))
3433anbi1i 624 . . . 4 ((𝑔:𝐵𝐴 ∧ Fun 𝑔) ↔ (((Fun 𝑔 ∧ dom 𝑔 = 𝐵) ∧ ran 𝑔𝐴) ∧ Fun 𝑔))
3529, 34bitri 274 . . 3 (𝑔:𝐵1-1𝐴 ↔ (((Fun 𝑔 ∧ dom 𝑔 = 𝐵) ∧ ran 𝑔𝐴) ∧ Fun 𝑔))
3628, 35anbi12i 627 . 2 ((𝑓:𝐴1-1𝐵𝑔:𝐵1-1𝐴) ↔ ((((Fun 𝑓 ∧ dom 𝑓 = 𝐴) ∧ ran 𝑓𝐵) ∧ Fun 𝑓) ∧ (((Fun 𝑔 ∧ dom 𝑔 = 𝐵) ∧ ran 𝑔𝐴) ∧ Fun 𝑔)))
37 dff1o4 6841 . . 3 (𝐻:𝐴1-1-onto𝐵 ↔ (𝐻 Fn 𝐴𝐻 Fn 𝐵))
38 df-fn 6546 . . . 4 (𝐻 Fn 𝐴 ↔ (Fun 𝐻 ∧ dom 𝐻 = 𝐴))
39 df-fn 6546 . . . 4 (𝐻 Fn 𝐵 ↔ (Fun 𝐻 ∧ dom 𝐻 = 𝐵))
4038, 39anbi12i 627 . . 3 ((𝐻 Fn 𝐴𝐻 Fn 𝐵) ↔ ((Fun 𝐻 ∧ dom 𝐻 = 𝐴) ∧ (Fun 𝐻 ∧ dom 𝐻 = 𝐵)))
4137, 40bitri 274 . 2 (𝐻:𝐴1-1-onto𝐵 ↔ ((Fun 𝐻 ∧ dom 𝐻 = 𝐴) ∧ (Fun 𝐻 ∧ dom 𝐻 = 𝐵)))
4221, 36, 413imtr4i 291 1 ((𝑓:𝐴1-1𝐵𝑔:𝐵1-1𝐴) → 𝐻:𝐴1-1-onto𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1541  wcel 2106  {cab 2709  Vcvv 3474  cdif 3945  cun 3946  wss 3948   cuni 4908  ccnv 5675  dom cdm 5676  ran crn 5677  cres 5678  cima 5679  Fun wfun 6537   Fn wfn 6538  wf 6539  1-1wf1 6540  1-1-ontowf1o 6542
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-12 2171  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pr 5427
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550
This theorem is referenced by:  sbthlem10  9094  sbthfilem  9203
  Copyright terms: Public domain W3C validator