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

Theorem ssrel 5625
 Description: A subclass relationship depends only on a relation's ordered pairs. Theorem 3.2(i) of [Monk1] p. 33. (Contributed by NM, 2-Aug-1994.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) Remove dependency on ax-sep 5170, ax-nul 5177, ax-pr 5298. (Revised by KP, 25-Oct-2021.)
Assertion
Ref Expression
ssrel (Rel 𝐴 → (𝐴𝐵 ↔ ∀𝑥𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵)))
Distinct variable groups:   𝑥,𝑦,𝐴   𝑥,𝐵,𝑦

Proof of Theorem ssrel
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 ssel 3911 . . 3 (𝐴𝐵 → (⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵))
21alrimivv 1929 . 2 (𝐴𝐵 → ∀𝑥𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵))
3 df-rel 5530 . . . . . . 7 (Rel 𝐴𝐴 ⊆ (V × V))
4 dfss2 3904 . . . . . . 7 (𝐴 ⊆ (V × V) ↔ ∀𝑧(𝑧𝐴𝑧 ∈ (V × V)))
53, 4sylbb 222 . . . . . 6 (Rel 𝐴 → ∀𝑧(𝑧𝐴𝑧 ∈ (V × V)))
6 df-xp 5529 . . . . . . . . . 10 (V × V) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ V ∧ 𝑦 ∈ V)}
7 df-opab 5096 . . . . . . . . . 10 {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ V ∧ 𝑦 ∈ V)} = {𝑧 ∣ ∃𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ V ∧ 𝑦 ∈ V))}
86, 7eqtri 2824 . . . . . . . . 9 (V × V) = {𝑧 ∣ ∃𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ V ∧ 𝑦 ∈ V))}
98abeq2i 2928 . . . . . . . 8 (𝑧 ∈ (V × V) ↔ ∃𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ V ∧ 𝑦 ∈ V)))
10 simpl 486 . . . . . . . . 9 ((𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ V ∧ 𝑦 ∈ V)) → 𝑧 = ⟨𝑥, 𝑦⟩)
11102eximi 1837 . . . . . . . 8 (∃𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ V ∧ 𝑦 ∈ V)) → ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩)
129, 11sylbi 220 . . . . . . 7 (𝑧 ∈ (V × V) → ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩)
1312imim2i 16 . . . . . 6 ((𝑧𝐴𝑧 ∈ (V × V)) → (𝑧𝐴 → ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩))
145, 13sylg 1824 . . . . 5 (Rel 𝐴 → ∀𝑧(𝑧𝐴 → ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩))
15 eleq1 2880 . . . . . . . . . . . 12 (𝑧 = ⟨𝑥, 𝑦⟩ → (𝑧𝐴 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝐴))
16 eleq1 2880 . . . . . . . . . . . 12 (𝑧 = ⟨𝑥, 𝑦⟩ → (𝑧𝐵 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝐵))
1715, 16imbi12d 348 . . . . . . . . . . 11 (𝑧 = ⟨𝑥, 𝑦⟩ → ((𝑧𝐴𝑧𝐵) ↔ (⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵)))
1817biimprcd 253 . . . . . . . . . 10 ((⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵) → (𝑧 = ⟨𝑥, 𝑦⟩ → (𝑧𝐴𝑧𝐵)))
19182alimi 1814 . . . . . . . . 9 (∀𝑥𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵) → ∀𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ → (𝑧𝐴𝑧𝐵)))
20 19.23vv 1944 . . . . . . . . 9 (∀𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ → (𝑧𝐴𝑧𝐵)) ↔ (∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩ → (𝑧𝐴𝑧𝐵)))
2119, 20sylib 221 . . . . . . . 8 (∀𝑥𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵) → (∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩ → (𝑧𝐴𝑧𝐵)))
2221com23 86 . . . . . . 7 (∀𝑥𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵) → (𝑧𝐴 → (∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩ → 𝑧𝐵)))
2322a2d 29 . . . . . 6 (∀𝑥𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵) → ((𝑧𝐴 → ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩) → (𝑧𝐴𝑧𝐵)))
2423alimdv 1917 . . . . 5 (∀𝑥𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵) → (∀𝑧(𝑧𝐴 → ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩) → ∀𝑧(𝑧𝐴𝑧𝐵)))
2514, 24syl5 34 . . . 4 (∀𝑥𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵) → (Rel 𝐴 → ∀𝑧(𝑧𝐴𝑧𝐵)))
26 dfss2 3904 . . . 4 (𝐴𝐵 ↔ ∀𝑧(𝑧𝐴𝑧𝐵))
2725, 26syl6ibr 255 . . 3 (∀𝑥𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵) → (Rel 𝐴𝐴𝐵))
2827com12 32 . 2 (Rel 𝐴 → (∀𝑥𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵) → 𝐴𝐵))
292, 28impbid2 229 1 (Rel 𝐴 → (𝐴𝐵 ↔ ∀𝑥𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399  ∀wal 1536   = wceq 1538  ∃wex 1781   ∈ wcel 2112  {cab 2779  Vcvv 3444   ⊆ wss 3884  ⟨cop 4534  {copab 5095   × cxp 5521  Rel wrel 5528 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-12 2176  ax-ext 2773 This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-v 3446  df-in 3891  df-ss 3901  df-opab 5096  df-xp 5529  df-rel 5530 This theorem is referenced by:  eqrel  5626  relssi  5628  relssdv  5629  cotrg  5942  cnvsym  5945  intasym  5946  intirr  5949  codir  5951  qfto  5952  dfso2  33104  dfpo2  33105  dffun10  33489  imagesset  33528  ssrel3  35715  undmrnresiss  40301  cnvssco  40303
 Copyright terms: Public domain W3C validator