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

Theorem rntpos 5926
 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 𝑥 𝑦 𝑤 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 vex 2613 . . . . 5 𝑥 ∈ V
21elrn 4625 . . . 4 (𝑥 ∈ ran tpos 𝐹 ↔ ∃𝑦 𝑦tpos 𝐹𝑥)
3 vex 2613 . . . . . . . . 9 𝑦 ∈ V
43, 1breldm 4587 . . . . . . . 8 (𝑦tpos 𝐹𝑥𝑦 ∈ dom tpos 𝐹)
5 dmtpos 5925 . . . . . . . . 9 (Rel dom 𝐹 → dom tpos 𝐹 = dom 𝐹)
65eleq2d 2152 . . . . . . . 8 (Rel dom 𝐹 → (𝑦 ∈ dom tpos 𝐹𝑦dom 𝐹))
74, 6syl5ib 152 . . . . . . 7 (Rel dom 𝐹 → (𝑦tpos 𝐹𝑥𝑦dom 𝐹))
8 relcnv 4753 . . . . . . . 8 Rel dom 𝐹
9 elrel 4488 . . . . . . . 8 ((Rel dom 𝐹𝑦dom 𝐹) → ∃𝑤𝑧 𝑦 = ⟨𝑤, 𝑧⟩)
108, 9mpan 415 . . . . . . 7 (𝑦dom 𝐹 → ∃𝑤𝑧 𝑦 = ⟨𝑤, 𝑧⟩)
117, 10syl6 33 . . . . . 6 (Rel dom 𝐹 → (𝑦tpos 𝐹𝑥 → ∃𝑤𝑧 𝑦 = ⟨𝑤, 𝑧⟩))
12 breq1 3808 . . . . . . . . 9 (𝑦 = ⟨𝑤, 𝑧⟩ → (𝑦tpos 𝐹𝑥 ↔ ⟨𝑤, 𝑧⟩tpos 𝐹𝑥))
13 vex 2613 . . . . . . . . . 10 𝑤 ∈ V
14 vex 2613 . . . . . . . . . 10 𝑧 ∈ V
15 brtposg 5923 . . . . . . . . . 10 ((𝑤 ∈ V ∧ 𝑧 ∈ V ∧ 𝑥 ∈ V) → (⟨𝑤, 𝑧⟩tpos 𝐹𝑥 ↔ ⟨𝑧, 𝑤𝐹𝑥))
1613, 14, 1, 15mp3an 1269 . . . . . . . . 9 (⟨𝑤, 𝑧⟩tpos 𝐹𝑥 ↔ ⟨𝑧, 𝑤𝐹𝑥)
1712, 16syl6bb 194 . . . . . . . 8 (𝑦 = ⟨𝑤, 𝑧⟩ → (𝑦tpos 𝐹𝑥 ↔ ⟨𝑧, 𝑤𝐹𝑥))
1814, 13opex 4012 . . . . . . . . 9 𝑧, 𝑤⟩ ∈ V
1918, 1brelrn 4615 . . . . . . . 8 (⟨𝑧, 𝑤𝐹𝑥𝑥 ∈ ran 𝐹)
2017, 19syl6bi 161 . . . . . . 7 (𝑦 = ⟨𝑤, 𝑧⟩ → (𝑦tpos 𝐹𝑥𝑥 ∈ ran 𝐹))
2120exlimivv 1819 . . . . . 6 (∃𝑤𝑧 𝑦 = ⟨𝑤, 𝑧⟩ → (𝑦tpos 𝐹𝑥𝑥 ∈ ran 𝐹))
2211, 21syli 37 . . . . 5 (Rel dom 𝐹 → (𝑦tpos 𝐹𝑥𝑥 ∈ ran 𝐹))
2322exlimdv 1742 . . . 4 (Rel dom 𝐹 → (∃𝑦 𝑦tpos 𝐹𝑥𝑥 ∈ ran 𝐹))
242, 23syl5bi 150 . . 3 (Rel dom 𝐹 → (𝑥 ∈ ran tpos 𝐹𝑥 ∈ ran 𝐹))
251elrn 4625 . . . 4 (𝑥 ∈ ran 𝐹 ↔ ∃𝑦 𝑦𝐹𝑥)
263, 1breldm 4587 . . . . . . 7 (𝑦𝐹𝑥𝑦 ∈ dom 𝐹)
27 elrel 4488 . . . . . . . 8 ((Rel dom 𝐹𝑦 ∈ dom 𝐹) → ∃𝑧𝑤 𝑦 = ⟨𝑧, 𝑤⟩)
2827ex 113 . . . . . . 7 (Rel dom 𝐹 → (𝑦 ∈ dom 𝐹 → ∃𝑧𝑤 𝑦 = ⟨𝑧, 𝑤⟩))
2926, 28syl5 32 . . . . . 6 (Rel dom 𝐹 → (𝑦𝐹𝑥 → ∃𝑧𝑤 𝑦 = ⟨𝑧, 𝑤⟩))
30 breq1 3808 . . . . . . . . 9 (𝑦 = ⟨𝑧, 𝑤⟩ → (𝑦𝐹𝑥 ↔ ⟨𝑧, 𝑤𝐹𝑥))
3130, 16syl6bbr 196 . . . . . . . 8 (𝑦 = ⟨𝑧, 𝑤⟩ → (𝑦𝐹𝑥 ↔ ⟨𝑤, 𝑧⟩tpos 𝐹𝑥))
3213, 14opex 4012 . . . . . . . . 9 𝑤, 𝑧⟩ ∈ V
3332, 1brelrn 4615 . . . . . . . 8 (⟨𝑤, 𝑧⟩tpos 𝐹𝑥𝑥 ∈ ran tpos 𝐹)
3431, 33syl6bi 161 . . . . . . 7 (𝑦 = ⟨𝑧, 𝑤⟩ → (𝑦𝐹𝑥𝑥 ∈ ran tpos 𝐹))
3534exlimivv 1819 . . . . . 6 (∃𝑧𝑤 𝑦 = ⟨𝑧, 𝑤⟩ → (𝑦𝐹𝑥𝑥 ∈ ran tpos 𝐹))
3629, 35syli 37 . . . . 5 (Rel dom 𝐹 → (𝑦𝐹𝑥𝑥 ∈ ran tpos 𝐹))
3736exlimdv 1742 . . . 4 (Rel dom 𝐹 → (∃𝑦 𝑦𝐹𝑥𝑥 ∈ ran tpos 𝐹))
3825, 37syl5bi 150 . . 3 (Rel dom 𝐹 → (𝑥 ∈ ran 𝐹𝑥 ∈ ran tpos 𝐹))
3924, 38impbid 127 . 2 (Rel dom 𝐹 → (𝑥 ∈ ran tpos 𝐹𝑥 ∈ ran 𝐹))
4039eqrdv 2081 1 (Rel dom 𝐹 → ran tpos 𝐹 = ran 𝐹)
 Colors of variables: wff set class Syntax hints:   → wi 4   ↔ wb 103   = wceq 1285  ∃wex 1422   ∈ wcel 1434  Vcvv 2610  ⟨cop 3419   class class class wbr 3805  ◡ccnv 4390  dom cdm 4391  ran crn 4392  Rel wrel 4396  tpos ctpos 5913 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 577  ax-in2 578  ax-io 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-13 1445  ax-14 1446  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2065  ax-sep 3916  ax-nul 3924  ax-pow 3968  ax-pr 3992  ax-un 4216 This theorem depends on definitions:  df-bi 115  df-3an 922  df-tru 1288  df-fal 1291  df-nf 1391  df-sb 1688  df-eu 1946  df-mo 1947  df-clab 2070  df-cleq 2076  df-clel 2079  df-nfc 2212  df-ne 2250  df-ral 2358  df-rex 2359  df-rab 2362  df-v 2612  df-sbc 2825  df-dif 2984  df-un 2986  df-in 2988  df-ss 2995  df-nul 3268  df-pw 3402  df-sn 3422  df-pr 3423  df-op 3425  df-uni 3622  df-br 3806  df-opab 3860  df-mpt 3861  df-id 4076  df-xp 4397  df-rel 4398  df-cnv 4399  df-co 4400  df-dm 4401  df-rn 4402  df-res 4403  df-ima 4404  df-iota 4917  df-fun 4954  df-fn 4955  df-fv 4960  df-tpos 5914 This theorem is referenced by:  tposfo2  5936
 Copyright terms: Public domain W3C validator