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

Theorem ssrelrn 5777
Description: If a relation is a subset of a cartesian product, then for each element of the range of the relation there is an element of the first set of the cartesian product which is related to the element of the range by the relation. (Contributed by AV, 24-Oct-2020.)
Assertion
Ref Expression
ssrelrn ((𝑅 ⊆ (𝐴 × 𝐵) ∧ 𝑌 ∈ ran 𝑅) → ∃𝑎𝐴 𝑎𝑅𝑌)
Distinct variable groups:   𝐴,𝑎   𝐵,𝑎   𝑅,𝑎   𝑌,𝑎

Proof of Theorem ssrelrn
StepHypRef Expression
1 elrng 5774 . . . . 5 (𝑌 ∈ ran 𝑅 → (𝑌 ∈ ran 𝑅 ↔ ∃𝑎 𝑎𝑅𝑌))
2 ssbr 5111 . . . . . . . . . . 11 (𝑅 ⊆ (𝐴 × 𝐵) → (𝑎𝑅𝑌𝑎(𝐴 × 𝐵)𝑌))
3 brxp 5612 . . . . . . . . . . . 12 (𝑎(𝐴 × 𝐵)𝑌 ↔ (𝑎𝐴𝑌𝐵))
43simplbi 501 . . . . . . . . . . 11 (𝑎(𝐴 × 𝐵)𝑌𝑎𝐴)
52, 4syl6 35 . . . . . . . . . 10 (𝑅 ⊆ (𝐴 × 𝐵) → (𝑎𝑅𝑌𝑎𝐴))
65ancrd 555 . . . . . . . . 9 (𝑅 ⊆ (𝐴 × 𝐵) → (𝑎𝑅𝑌 → (𝑎𝐴𝑎𝑅𝑌)))
76adantl 485 . . . . . . . 8 ((𝑌 ∈ ran 𝑅𝑅 ⊆ (𝐴 × 𝐵)) → (𝑎𝑅𝑌 → (𝑎𝐴𝑎𝑅𝑌)))
87eximdv 1925 . . . . . . 7 ((𝑌 ∈ ran 𝑅𝑅 ⊆ (𝐴 × 𝐵)) → (∃𝑎 𝑎𝑅𝑌 → ∃𝑎(𝑎𝐴𝑎𝑅𝑌)))
98ex 416 . . . . . 6 (𝑌 ∈ ran 𝑅 → (𝑅 ⊆ (𝐴 × 𝐵) → (∃𝑎 𝑎𝑅𝑌 → ∃𝑎(𝑎𝐴𝑎𝑅𝑌))))
109com23 86 . . . . 5 (𝑌 ∈ ran 𝑅 → (∃𝑎 𝑎𝑅𝑌 → (𝑅 ⊆ (𝐴 × 𝐵) → ∃𝑎(𝑎𝐴𝑎𝑅𝑌))))
111, 10sylbid 243 . . . 4 (𝑌 ∈ ran 𝑅 → (𝑌 ∈ ran 𝑅 → (𝑅 ⊆ (𝐴 × 𝐵) → ∃𝑎(𝑎𝐴𝑎𝑅𝑌))))
1211pm2.43i 52 . . 3 (𝑌 ∈ ran 𝑅 → (𝑅 ⊆ (𝐴 × 𝐵) → ∃𝑎(𝑎𝐴𝑎𝑅𝑌)))
1312impcom 411 . 2 ((𝑅 ⊆ (𝐴 × 𝐵) ∧ 𝑌 ∈ ran 𝑅) → ∃𝑎(𝑎𝐴𝑎𝑅𝑌))
14 df-rex 3068 . 2 (∃𝑎𝐴 𝑎𝑅𝑌 ↔ ∃𝑎(𝑎𝐴𝑎𝑅𝑌))
1513, 14sylibr 237 1 ((𝑅 ⊆ (𝐴 × 𝐵) ∧ 𝑌 ∈ ran 𝑅) → ∃𝑎𝐴 𝑎𝑅𝑌)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  wex 1787  wcel 2111  wrex 3063  wss 3880   class class class wbr 5067   × cxp 5563  ran crn 5566
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2113  ax-9 2121  ax-ext 2709  ax-sep 5206  ax-nul 5213  ax-pr 5336
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-sb 2072  df-clab 2716  df-cleq 2730  df-clel 2817  df-ral 3067  df-rex 3068  df-rab 3071  df-v 3422  df-dif 3883  df-un 3885  df-in 3887  df-ss 3897  df-nul 4252  df-if 4454  df-sn 4556  df-pr 4558  df-op 4562  df-br 5068  df-opab 5130  df-xp 5571  df-cnv 5573  df-dm 5575  df-rn 5576
This theorem is referenced by:  incistruhgr  27194
  Copyright terms: Public domain W3C validator