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

Theorem ssrelrn 5452
 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 5451 . . . . 5 (𝑌 ∈ ran 𝑅 → (𝑌 ∈ ran 𝑅 ↔ ∃𝑎 𝑎𝑅𝑌))
2 ssbr 4831 . . . . . . . . . . 11 (𝑅 ⊆ (𝐴 × 𝐵) → (𝑎𝑅𝑌𝑎(𝐴 × 𝐵)𝑌))
3 brxp 5286 . . . . . . . . . . . 12 (𝑎(𝐴 × 𝐵)𝑌 ↔ (𝑎𝐴𝑌𝐵))
43simplbi 485 . . . . . . . . . . 11 (𝑎(𝐴 × 𝐵)𝑌𝑎𝐴)
52, 4syl6 35 . . . . . . . . . 10 (𝑅 ⊆ (𝐴 × 𝐵) → (𝑎𝑅𝑌𝑎𝐴))
65ancrd 541 . . . . . . . . 9 (𝑅 ⊆ (𝐴 × 𝐵) → (𝑎𝑅𝑌 → (𝑎𝐴𝑎𝑅𝑌)))
76adantl 467 . . . . . . . 8 ((𝑌 ∈ ran 𝑅𝑅 ⊆ (𝐴 × 𝐵)) → (𝑎𝑅𝑌 → (𝑎𝐴𝑎𝑅𝑌)))
87eximdv 1998 . . . . . . 7 ((𝑌 ∈ ran 𝑅𝑅 ⊆ (𝐴 × 𝐵)) → (∃𝑎 𝑎𝑅𝑌 → ∃𝑎(𝑎𝐴𝑎𝑅𝑌)))
98ex 397 . . . . . 6 (𝑌 ∈ ran 𝑅 → (𝑅 ⊆ (𝐴 × 𝐵) → (∃𝑎 𝑎𝑅𝑌 → ∃𝑎(𝑎𝐴𝑎𝑅𝑌))))
109com23 86 . . . . 5 (𝑌 ∈ ran 𝑅 → (∃𝑎 𝑎𝑅𝑌 → (𝑅 ⊆ (𝐴 × 𝐵) → ∃𝑎(𝑎𝐴𝑎𝑅𝑌))))
111, 10sylbid 230 . . . 4 (𝑌 ∈ ran 𝑅 → (𝑌 ∈ ran 𝑅 → (𝑅 ⊆ (𝐴 × 𝐵) → ∃𝑎(𝑎𝐴𝑎𝑅𝑌))))
1211pm2.43i 52 . . 3 (𝑌 ∈ ran 𝑅 → (𝑅 ⊆ (𝐴 × 𝐵) → ∃𝑎(𝑎𝐴𝑎𝑅𝑌)))
1312impcom 394 . 2 ((𝑅 ⊆ (𝐴 × 𝐵) ∧ 𝑌 ∈ ran 𝑅) → ∃𝑎(𝑎𝐴𝑎𝑅𝑌))
14 df-rex 3067 . 2 (∃𝑎𝐴 𝑎𝑅𝑌 ↔ ∃𝑎(𝑎𝐴𝑎𝑅𝑌))
1513, 14sylibr 224 1 ((𝑅 ⊆ (𝐴 × 𝐵) ∧ 𝑌 ∈ ran 𝑅) → ∃𝑎𝐴 𝑎𝑅𝑌)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 382  ∃wex 1852   ∈ wcel 2145  ∃wrex 3062   ⊆ wss 3723   class class class wbr 4787   × cxp 5248  ran crn 5251 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4916  ax-nul 4924  ax-pr 5035 This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3353  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4227  df-sn 4318  df-pr 4320  df-op 4324  df-br 4788  df-opab 4848  df-xp 5256  df-cnv 5258  df-dm 5260  df-rn 5261 This theorem is referenced by:  incistruhgr  26195
 Copyright terms: Public domain W3C validator