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

Theorem rntpos 5813
Description: The range of tpos 𝐹 when dom 𝐹 is a relation. (Contributed by Mario Carneiro, 10-Sep-2015.)
Assertion
Ref Expression
rntpos (Rel dom 𝐹 → ran tpos 𝐹 = ran 𝐹)

Proof of Theorem rntpos
Dummy variables x y w z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 vex 2554 . . . . 5 x V
21elrn 4520 . . . 4 (x ran tpos 𝐹y ytpos 𝐹x)
3 vex 2554 . . . . . . . . 9 y V
43, 1breldm 4482 . . . . . . . 8 (ytpos 𝐹xy dom tpos 𝐹)
5 dmtpos 5812 . . . . . . . . 9 (Rel dom 𝐹 → dom tpos 𝐹 = dom 𝐹)
65eleq2d 2104 . . . . . . . 8 (Rel dom 𝐹 → (y dom tpos 𝐹y dom 𝐹))
74, 6syl5ib 143 . . . . . . 7 (Rel dom 𝐹 → (ytpos 𝐹xy dom 𝐹))
8 relcnv 4646 . . . . . . . 8 Rel dom 𝐹
9 elrel 4385 . . . . . . . 8 ((Rel dom 𝐹 y dom 𝐹) → wz y = ⟨w, z⟩)
108, 9mpan 400 . . . . . . 7 (y dom 𝐹wz y = ⟨w, z⟩)
117, 10syl6 29 . . . . . 6 (Rel dom 𝐹 → (ytpos 𝐹xwz y = ⟨w, z⟩))
12 breq1 3758 . . . . . . . . 9 (y = ⟨w, z⟩ → (ytpos 𝐹x ↔ ⟨w, z⟩tpos 𝐹x))
13 vex 2554 . . . . . . . . . 10 w V
14 vex 2554 . . . . . . . . . 10 z V
15 brtposg 5810 . . . . . . . . . 10 ((w V z V x V) → (⟨w, z⟩tpos 𝐹x ↔ ⟨z, w𝐹x))
1613, 14, 1, 15mp3an 1231 . . . . . . . . 9 (⟨w, z⟩tpos 𝐹x ↔ ⟨z, w𝐹x)
1712, 16syl6bb 185 . . . . . . . 8 (y = ⟨w, z⟩ → (ytpos 𝐹x ↔ ⟨z, w𝐹x))
1814, 13opex 3957 . . . . . . . . 9 z, w V
1918, 1brelrn 4510 . . . . . . . 8 (⟨z, w𝐹xx ran 𝐹)
2017, 19syl6bi 152 . . . . . . 7 (y = ⟨w, z⟩ → (ytpos 𝐹xx ran 𝐹))
2120exlimivv 1773 . . . . . 6 (wz y = ⟨w, z⟩ → (ytpos 𝐹xx ran 𝐹))
2211, 21syli 33 . . . . 5 (Rel dom 𝐹 → (ytpos 𝐹xx ran 𝐹))
2322exlimdv 1697 . . . 4 (Rel dom 𝐹 → (y ytpos 𝐹xx ran 𝐹))
242, 23syl5bi 141 . . 3 (Rel dom 𝐹 → (x ran tpos 𝐹x ran 𝐹))
251elrn 4520 . . . 4 (x ran 𝐹y y𝐹x)
263, 1breldm 4482 . . . . . . 7 (y𝐹xy dom 𝐹)
27 elrel 4385 . . . . . . . 8 ((Rel dom 𝐹 y dom 𝐹) → zw y = ⟨z, w⟩)
2827ex 108 . . . . . . 7 (Rel dom 𝐹 → (y dom 𝐹zw y = ⟨z, w⟩))
2926, 28syl5 28 . . . . . 6 (Rel dom 𝐹 → (y𝐹xzw y = ⟨z, w⟩))
30 breq1 3758 . . . . . . . . 9 (y = ⟨z, w⟩ → (y𝐹x ↔ ⟨z, w𝐹x))
3130, 16syl6bbr 187 . . . . . . . 8 (y = ⟨z, w⟩ → (y𝐹x ↔ ⟨w, z⟩tpos 𝐹x))
3213, 14opex 3957 . . . . . . . . 9 w, z V
3332, 1brelrn 4510 . . . . . . . 8 (⟨w, z⟩tpos 𝐹xx ran tpos 𝐹)
3431, 33syl6bi 152 . . . . . . 7 (y = ⟨z, w⟩ → (y𝐹xx ran tpos 𝐹))
3534exlimivv 1773 . . . . . 6 (zw y = ⟨z, w⟩ → (y𝐹xx ran tpos 𝐹))
3629, 35syli 33 . . . . 5 (Rel dom 𝐹 → (y𝐹xx ran tpos 𝐹))
3736exlimdv 1697 . . . 4 (Rel dom 𝐹 → (y y𝐹xx ran tpos 𝐹))
3825, 37syl5bi 141 . . 3 (Rel dom 𝐹 → (x ran 𝐹x ran tpos 𝐹))
3924, 38impbid 120 . 2 (Rel dom 𝐹 → (x ran tpos 𝐹x ran 𝐹))
4039eqrdv 2035 1 (Rel dom 𝐹 → ran tpos 𝐹 = ran 𝐹)
Colors of variables: wff set class
Syntax hints:  wi 4  wb 98   = wceq 1242  wex 1378   wcel 1390  Vcvv 2551  cop 3370   class class class wbr 3755  ccnv 4287  dom cdm 4288  ran crn 4289  Rel wrel 4293  tpos ctpos 5800
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 544  ax-in2 545  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bnd 1396  ax-4 1397  ax-13 1401  ax-14 1402  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-sep 3866  ax-nul 3874  ax-pow 3918  ax-pr 3935  ax-un 4136
This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-fal 1248  df-nf 1347  df-sb 1643  df-eu 1900  df-mo 1901  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ne 2203  df-ral 2305  df-rex 2306  df-rab 2309  df-v 2553  df-sbc 2759  df-dif 2914  df-un 2916  df-in 2918  df-ss 2925  df-nul 3219  df-pw 3353  df-sn 3373  df-pr 3374  df-op 3376  df-uni 3572  df-br 3756  df-opab 3810  df-mpt 3811  df-id 4021  df-xp 4294  df-rel 4295  df-cnv 4296  df-co 4297  df-dm 4298  df-rn 4299  df-res 4300  df-ima 4301  df-iota 4810  df-fun 4847  df-fn 4848  df-fv 4853  df-tpos 5801
This theorem is referenced by:  tposfo2  5823
  Copyright terms: Public domain W3C validator