Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ssrelf Structured version   Visualization version   GIF version

Theorem ssrelf 28607
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.) (Revised by Thierry Arnoux, 6-Nov-2017.)
Hypotheses
Ref Expression
eqrelrd2.1 𝑥𝜑
eqrelrd2.2 𝑦𝜑
eqrelrd2.3 𝑥𝐴
eqrelrd2.4 𝑦𝐴
eqrelrd2.5 𝑥𝐵
eqrelrd2.6 𝑦𝐵
Assertion
Ref Expression
ssrelf (Rel 𝐴 → (𝐴𝐵 ↔ ∀𝑥𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵)))
Distinct variable group:   𝑥,𝑦
Allowed substitution hints:   𝜑(𝑥,𝑦)   𝐴(𝑥,𝑦)   𝐵(𝑥,𝑦)

Proof of Theorem ssrelf
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 eqrelrd2.3 . . . 4 𝑥𝐴
2 eqrelrd2.5 . . . 4 𝑥𝐵
31, 2nfss 3556 . . 3 𝑥 𝐴𝐵
4 eqrelrd2.4 . . . . 5 𝑦𝐴
5 eqrelrd2.6 . . . . 5 𝑦𝐵
64, 5nfss 3556 . . . 4 𝑦 𝐴𝐵
7 ssel 3557 . . . 4 (𝐴𝐵 → (⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵))
86, 7alrimi 2066 . . 3 (𝐴𝐵 → ∀𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵))
93, 8alrimi 2066 . 2 (𝐴𝐵 → ∀𝑥𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵))
10 eleq1 2671 . . . . . . . . . . 11 (𝑧 = ⟨𝑥, 𝑦⟩ → (𝑧𝐴 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝐴))
11 eleq1 2671 . . . . . . . . . . 11 (𝑧 = ⟨𝑥, 𝑦⟩ → (𝑧𝐵 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝐵))
1210, 11imbi12d 332 . . . . . . . . . 10 (𝑧 = ⟨𝑥, 𝑦⟩ → ((𝑧𝐴𝑧𝐵) ↔ (⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵)))
1312biimprcd 238 . . . . . . . . 9 ((⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵) → (𝑧 = ⟨𝑥, 𝑦⟩ → (𝑧𝐴𝑧𝐵)))
14132alimi 1729 . . . . . . . 8 (∀𝑥𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵) → ∀𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ → (𝑧𝐴𝑧𝐵)))
154nfcri 2740 . . . . . . . . . . . 12 𝑦 𝑧𝐴
165nfcri 2740 . . . . . . . . . . . 12 𝑦 𝑧𝐵
1715, 16nfim 1811 . . . . . . . . . . 11 𝑦(𝑧𝐴𝑧𝐵)
181719.23 2064 . . . . . . . . . 10 (∀𝑦(𝑧 = ⟨𝑥, 𝑦⟩ → (𝑧𝐴𝑧𝐵)) ↔ (∃𝑦 𝑧 = ⟨𝑥, 𝑦⟩ → (𝑧𝐴𝑧𝐵)))
1918albii 1735 . . . . . . . . 9 (∀𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ → (𝑧𝐴𝑧𝐵)) ↔ ∀𝑥(∃𝑦 𝑧 = ⟨𝑥, 𝑦⟩ → (𝑧𝐴𝑧𝐵)))
201nfcri 2740 . . . . . . . . . . 11 𝑥 𝑧𝐴
212nfcri 2740 . . . . . . . . . . 11 𝑥 𝑧𝐵
2220, 21nfim 1811 . . . . . . . . . 10 𝑥(𝑧𝐴𝑧𝐵)
232219.23 2064 . . . . . . . . 9 (∀𝑥(∃𝑦 𝑧 = ⟨𝑥, 𝑦⟩ → (𝑧𝐴𝑧𝐵)) ↔ (∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩ → (𝑧𝐴𝑧𝐵)))
2419, 23bitri 262 . . . . . . . 8 (∀𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ → (𝑧𝐴𝑧𝐵)) ↔ (∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩ → (𝑧𝐴𝑧𝐵)))
2514, 24sylib 206 . . . . . . 7 (∀𝑥𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵) → (∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩ → (𝑧𝐴𝑧𝐵)))
2625com23 83 . . . . . 6 (∀𝑥𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵) → (𝑧𝐴 → (∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩ → 𝑧𝐵)))
2726a2d 29 . . . . 5 (∀𝑥𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵) → ((𝑧𝐴 → ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩) → (𝑧𝐴𝑧𝐵)))
2827alimdv 1830 . . . 4 (∀𝑥𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵) → (∀𝑧(𝑧𝐴 → ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩) → ∀𝑧(𝑧𝐴𝑧𝐵)))
29 df-rel 5031 . . . . 5 (Rel 𝐴𝐴 ⊆ (V × V))
30 dfss2 3552 . . . . 5 (𝐴 ⊆ (V × V) ↔ ∀𝑧(𝑧𝐴𝑧 ∈ (V × V)))
31 elvv 5086 . . . . . . 7 (𝑧 ∈ (V × V) ↔ ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩)
3231imbi2i 324 . . . . . 6 ((𝑧𝐴𝑧 ∈ (V × V)) ↔ (𝑧𝐴 → ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩))
3332albii 1735 . . . . 5 (∀𝑧(𝑧𝐴𝑧 ∈ (V × V)) ↔ ∀𝑧(𝑧𝐴 → ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩))
3429, 30, 333bitri 284 . . . 4 (Rel 𝐴 ↔ ∀𝑧(𝑧𝐴 → ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩))
35 dfss2 3552 . . . 4 (𝐴𝐵 ↔ ∀𝑧(𝑧𝐴𝑧𝐵))
3628, 34, 353imtr4g 283 . . 3 (∀𝑥𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵) → (Rel 𝐴𝐴𝐵))
3736com12 32 . 2 (Rel 𝐴 → (∀𝑥𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵) → 𝐴𝐵))
389, 37impbid2 214 1 (Rel 𝐴 → (𝐴𝐵 ↔ ∀𝑥𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wal 1472   = wceq 1474  wex 1694  wnf 1698  wcel 1975  wnfc 2733  Vcvv 3168  wss 3535  cop 4126   × cxp 5022  Rel wrel 5029
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-9 1984  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2228  ax-ext 2585  ax-sep 4699  ax-nul 4708  ax-pr 4824
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1866  df-clab 2592  df-cleq 2598  df-clel 2601  df-nfc 2735  df-ral 2896  df-v 3170  df-dif 3538  df-un 3540  df-in 3542  df-ss 3549  df-nul 3870  df-if 4032  df-sn 4121  df-pr 4123  df-op 4127  df-opab 4634  df-xp 5030  df-rel 5031
This theorem is referenced by:  eqrelrd2  28608
  Copyright terms: Public domain W3C validator