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

Theorem rntpos 5794
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 2538 . . . . 5 x V
21elrn 4504 . . . 4 (x ran tpos 𝐹y ytpos 𝐹x)
3 vex 2538 . . . . . . . . 9 y V
43, 1breldm 4466 . . . . . . . 8 (ytpos 𝐹xy dom tpos 𝐹)
5 dmtpos 5793 . . . . . . . . 9 (Rel dom 𝐹 → dom tpos 𝐹 = dom 𝐹)
65eleq2d 2089 . . . . . . . 8 (Rel dom 𝐹 → (y dom tpos 𝐹y dom 𝐹))
74, 6syl5ib 143 . . . . . . 7 (Rel dom 𝐹 → (ytpos 𝐹xy dom 𝐹))
8 relcnv 4630 . . . . . . . 8 Rel dom 𝐹
9 elrel 4369 . . . . . . . 8 ((Rel dom 𝐹 y dom 𝐹) → wz y = ⟨w, z⟩)
108, 9mpan 402 . . . . . . 7 (y dom 𝐹wz y = ⟨w, z⟩)
117, 10syl6 29 . . . . . 6 (Rel dom 𝐹 → (ytpos 𝐹xwz y = ⟨w, z⟩))
12 breq1 3741 . . . . . . . . 9 (y = ⟨w, z⟩ → (ytpos 𝐹x ↔ ⟨w, z⟩tpos 𝐹x))
13 vex 2538 . . . . . . . . . 10 w V
14 vex 2538 . . . . . . . . . 10 z V
15 brtposg 5791 . . . . . . . . . 10 ((w V z V x V) → (⟨w, z⟩tpos 𝐹x ↔ ⟨z, w𝐹x))
1613, 14, 1, 15mp3an 1217 . . . . . . . . 9 (⟨w, z⟩tpos 𝐹x ↔ ⟨z, w𝐹x)
1712, 16syl6bb 185 . . . . . . . 8 (y = ⟨w, z⟩ → (ytpos 𝐹x ↔ ⟨z, w𝐹x))
1814, 13opex 3940 . . . . . . . . 9 z, w V
1918, 1brelrn 4494 . . . . . . . 8 (⟨z, w𝐹xx ran 𝐹)
2017, 19syl6bi 152 . . . . . . 7 (y = ⟨w, z⟩ → (ytpos 𝐹xx ran 𝐹))
2120exlimivv 1758 . . . . . 6 (wz y = ⟨w, z⟩ → (ytpos 𝐹xx ran 𝐹))
2211, 21syli 33 . . . . 5 (Rel dom 𝐹 → (ytpos 𝐹xx ran 𝐹))
2322exlimdv 1682 . . . 4 (Rel dom 𝐹 → (y ytpos 𝐹xx ran 𝐹))
242, 23syl5bi 141 . . 3 (Rel dom 𝐹 → (x ran tpos 𝐹x ran 𝐹))
251elrn 4504 . . . 4 (x ran 𝐹y y𝐹x)
263, 1breldm 4466 . . . . . . 7 (y𝐹xy dom 𝐹)
27 elrel 4369 . . . . . . . 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 3741 . . . . . . . . 9 (y = ⟨z, w⟩ → (y𝐹x ↔ ⟨z, w𝐹x))
3130, 16syl6bbr 187 . . . . . . . 8 (y = ⟨z, w⟩ → (y𝐹x ↔ ⟨w, z⟩tpos 𝐹x))
3213, 14opex 3940 . . . . . . . . 9 w, z V
3332, 1brelrn 4494 . . . . . . . 8 (⟨w, z⟩tpos 𝐹xx ran tpos 𝐹)
3431, 33syl6bi 152 . . . . . . 7 (y = ⟨z, w⟩ → (y𝐹xx ran tpos 𝐹))
3534exlimivv 1758 . . . . . 6 (zw y = ⟨z, w⟩ → (y𝐹xx ran tpos 𝐹))
3629, 35syli 33 . . . . 5 (Rel dom 𝐹 → (y𝐹xx ran tpos 𝐹))
3736exlimdv 1682 . . . 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 2020 1 (Rel dom 𝐹 → ran tpos 𝐹 = ran 𝐹)
Colors of variables: wff set class
Syntax hints:  wi 4  wb 98   = wceq 1228  wex 1362   wcel 1374  Vcvv 2535  cop 3353   class class class wbr 3738  ccnv 4271  dom cdm 4272  ran crn 4273  Rel wrel 4277  tpos ctpos 5781
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 532  ax-in2 533  ax-io 617  ax-5 1316  ax-7 1317  ax-gen 1318  ax-ie1 1363  ax-ie2 1364  ax-8 1376  ax-10 1377  ax-11 1378  ax-i12 1379  ax-bnd 1380  ax-4 1381  ax-13 1385  ax-14 1386  ax-17 1400  ax-i9 1404  ax-ial 1409  ax-i5r 1410  ax-ext 2004  ax-sep 3849  ax-nul 3857  ax-pow 3901  ax-pr 3918  ax-un 4120
This theorem depends on definitions:  df-bi 110  df-3an 875  df-tru 1231  df-fal 1234  df-nf 1330  df-sb 1628  df-eu 1885  df-mo 1886  df-clab 2009  df-cleq 2015  df-clel 2018  df-nfc 2149  df-ne 2188  df-ral 2289  df-rex 2290  df-rab 2293  df-v 2537  df-sbc 2742  df-dif 2897  df-un 2899  df-in 2901  df-ss 2908  df-nul 3202  df-pw 3336  df-sn 3356  df-pr 3357  df-op 3359  df-uni 3555  df-br 3739  df-opab 3793  df-mpt 3794  df-id 4004  df-xp 4278  df-rel 4279  df-cnv 4280  df-co 4281  df-dm 4282  df-rn 4283  df-res 4284  df-ima 4285  df-iota 4794  df-fun 4831  df-fn 4832  df-fv 4837  df-tpos 5782
This theorem is referenced by:  tposfo2  5804
  Copyright terms: Public domain W3C validator