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

Theorem rntpos 5900
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 2575 . . . . 5 𝑥 ∈ V
21elrn 4602 . . . 4 (𝑥 ∈ ran tpos 𝐹 ↔ ∃𝑦 𝑦tpos 𝐹𝑥)
3 vex 2575 . . . . . . . . 9 𝑦 ∈ V
43, 1breldm 4564 . . . . . . . 8 (𝑦tpos 𝐹𝑥𝑦 ∈ dom tpos 𝐹)
5 dmtpos 5899 . . . . . . . . 9 (Rel dom 𝐹 → dom tpos 𝐹 = dom 𝐹)
65eleq2d 2121 . . . . . . . 8 (Rel dom 𝐹 → (𝑦 ∈ dom tpos 𝐹𝑦dom 𝐹))
74, 6syl5ib 147 . . . . . . 7 (Rel dom 𝐹 → (𝑦tpos 𝐹𝑥𝑦dom 𝐹))
8 relcnv 4728 . . . . . . . 8 Rel dom 𝐹
9 elrel 4467 . . . . . . . 8 ((Rel dom 𝐹𝑦dom 𝐹) → ∃𝑤𝑧 𝑦 = ⟨𝑤, 𝑧⟩)
108, 9mpan 408 . . . . . . 7 (𝑦dom 𝐹 → ∃𝑤𝑧 𝑦 = ⟨𝑤, 𝑧⟩)
117, 10syl6 33 . . . . . 6 (Rel dom 𝐹 → (𝑦tpos 𝐹𝑥 → ∃𝑤𝑧 𝑦 = ⟨𝑤, 𝑧⟩))
12 breq1 3792 . . . . . . . . 9 (𝑦 = ⟨𝑤, 𝑧⟩ → (𝑦tpos 𝐹𝑥 ↔ ⟨𝑤, 𝑧⟩tpos 𝐹𝑥))
13 vex 2575 . . . . . . . . . 10 𝑤 ∈ V
14 vex 2575 . . . . . . . . . 10 𝑧 ∈ V
15 brtposg 5897 . . . . . . . . . 10 ((𝑤 ∈ V ∧ 𝑧 ∈ V ∧ 𝑥 ∈ V) → (⟨𝑤, 𝑧⟩tpos 𝐹𝑥 ↔ ⟨𝑧, 𝑤𝐹𝑥))
1613, 14, 1, 15mp3an 1241 . . . . . . . . 9 (⟨𝑤, 𝑧⟩tpos 𝐹𝑥 ↔ ⟨𝑧, 𝑤𝐹𝑥)
1712, 16syl6bb 189 . . . . . . . 8 (𝑦 = ⟨𝑤, 𝑧⟩ → (𝑦tpos 𝐹𝑥 ↔ ⟨𝑧, 𝑤𝐹𝑥))
1814, 13opex 3991 . . . . . . . . 9 𝑧, 𝑤⟩ ∈ V
1918, 1brelrn 4592 . . . . . . . 8 (⟨𝑧, 𝑤𝐹𝑥𝑥 ∈ ran 𝐹)
2017, 19syl6bi 156 . . . . . . 7 (𝑦 = ⟨𝑤, 𝑧⟩ → (𝑦tpos 𝐹𝑥𝑥 ∈ ran 𝐹))
2120exlimivv 1790 . . . . . 6 (∃𝑤𝑧 𝑦 = ⟨𝑤, 𝑧⟩ → (𝑦tpos 𝐹𝑥𝑥 ∈ ran 𝐹))
2211, 21syli 37 . . . . 5 (Rel dom 𝐹 → (𝑦tpos 𝐹𝑥𝑥 ∈ ran 𝐹))
2322exlimdv 1714 . . . 4 (Rel dom 𝐹 → (∃𝑦 𝑦tpos 𝐹𝑥𝑥 ∈ ran 𝐹))
242, 23syl5bi 145 . . 3 (Rel dom 𝐹 → (𝑥 ∈ ran tpos 𝐹𝑥 ∈ ran 𝐹))
251elrn 4602 . . . 4 (𝑥 ∈ ran 𝐹 ↔ ∃𝑦 𝑦𝐹𝑥)
263, 1breldm 4564 . . . . . . 7 (𝑦𝐹𝑥𝑦 ∈ dom 𝐹)
27 elrel 4467 . . . . . . . 8 ((Rel dom 𝐹𝑦 ∈ dom 𝐹) → ∃𝑧𝑤 𝑦 = ⟨𝑧, 𝑤⟩)
2827ex 112 . . . . . . 7 (Rel dom 𝐹 → (𝑦 ∈ dom 𝐹 → ∃𝑧𝑤 𝑦 = ⟨𝑧, 𝑤⟩))
2926, 28syl5 32 . . . . . 6 (Rel dom 𝐹 → (𝑦𝐹𝑥 → ∃𝑧𝑤 𝑦 = ⟨𝑧, 𝑤⟩))
30 breq1 3792 . . . . . . . . 9 (𝑦 = ⟨𝑧, 𝑤⟩ → (𝑦𝐹𝑥 ↔ ⟨𝑧, 𝑤𝐹𝑥))
3130, 16syl6bbr 191 . . . . . . . 8 (𝑦 = ⟨𝑧, 𝑤⟩ → (𝑦𝐹𝑥 ↔ ⟨𝑤, 𝑧⟩tpos 𝐹𝑥))
3213, 14opex 3991 . . . . . . . . 9 𝑤, 𝑧⟩ ∈ V
3332, 1brelrn 4592 . . . . . . . 8 (⟨𝑤, 𝑧⟩tpos 𝐹𝑥𝑥 ∈ ran tpos 𝐹)
3431, 33syl6bi 156 . . . . . . 7 (𝑦 = ⟨𝑧, 𝑤⟩ → (𝑦𝐹𝑥𝑥 ∈ ran tpos 𝐹))
3534exlimivv 1790 . . . . . 6 (∃𝑧𝑤 𝑦 = ⟨𝑧, 𝑤⟩ → (𝑦𝐹𝑥𝑥 ∈ ran tpos 𝐹))
3629, 35syli 37 . . . . 5 (Rel dom 𝐹 → (𝑦𝐹𝑥𝑥 ∈ ran tpos 𝐹))
3736exlimdv 1714 . . . 4 (Rel dom 𝐹 → (∃𝑦 𝑦𝐹𝑥𝑥 ∈ ran tpos 𝐹))
3825, 37syl5bi 145 . . 3 (Rel dom 𝐹 → (𝑥 ∈ ran 𝐹𝑥 ∈ ran tpos 𝐹))
3924, 38impbid 124 . 2 (Rel dom 𝐹 → (𝑥 ∈ ran tpos 𝐹𝑥 ∈ ran 𝐹))
4039eqrdv 2052 1 (Rel dom 𝐹 → ran tpos 𝐹 = ran 𝐹)
Colors of variables: wff set class
Syntax hints:  wi 4  wb 102   = wceq 1257  wex 1395  wcel 1407  Vcvv 2572  cop 3403   class class class wbr 3789  ccnv 4369  dom cdm 4370  ran crn 4371  Rel wrel 4375  tpos ctpos 5887
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-in1 552  ax-in2 553  ax-io 638  ax-5 1350  ax-7 1351  ax-gen 1352  ax-ie1 1396  ax-ie2 1397  ax-8 1409  ax-10 1410  ax-11 1411  ax-i12 1412  ax-bndl 1413  ax-4 1414  ax-13 1418  ax-14 1419  ax-17 1433  ax-i9 1437  ax-ial 1441  ax-i5r 1442  ax-ext 2036  ax-sep 3900  ax-nul 3908  ax-pow 3952  ax-pr 3969  ax-un 4195
This theorem depends on definitions:  df-bi 114  df-3an 896  df-tru 1260  df-fal 1263  df-nf 1364  df-sb 1660  df-eu 1917  df-mo 1918  df-clab 2041  df-cleq 2047  df-clel 2050  df-nfc 2181  df-ne 2219  df-ral 2326  df-rex 2327  df-rab 2330  df-v 2574  df-sbc 2785  df-dif 2945  df-un 2947  df-in 2949  df-ss 2956  df-nul 3250  df-pw 3386  df-sn 3406  df-pr 3407  df-op 3409  df-uni 3606  df-br 3790  df-opab 3844  df-mpt 3845  df-id 4055  df-xp 4376  df-rel 4377  df-cnv 4378  df-co 4379  df-dm 4380  df-rn 4381  df-res 4382  df-ima 4383  df-iota 4892  df-fun 4929  df-fn 4930  df-fv 4935  df-tpos 5888
This theorem is referenced by:  tposfo2  5910
  Copyright terms: Public domain W3C validator