Theorem ssrel 5130

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 4709, ax-nul 4717, ax-pr 4833. (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.

Step	Hyp	Ref	Expression
1		ssel 3562	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵))
2	1	alrimivv 1843	. 2 ⊢ (𝐴 ⊆ 𝐵 → ∀𝑥∀𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵))
3		df-rel 5045	. . . . . . 7 ⊢ (Rel 𝐴 ↔ 𝐴 ⊆ (V × V))
4		dfss2 3557	. . . . . . 7 ⊢ (𝐴 ⊆ (V × V) ↔ ∀𝑧(𝑧 ∈ 𝐴 → 𝑧 ∈ (V × V)))
5	3, 4	sylbb 208	. . . . . 6 ⊢ (Rel 𝐴 → ∀𝑧(𝑧 ∈ 𝐴 → 𝑧 ∈ (V × V)))
6		df-xp 5044	. . . . . . . . . 10 ⊢ (V × V) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ V ∧ 𝑦 ∈ V)}
7		df-opab 4644	. . . . . . . . . 10 ⊢ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ V ∧ 𝑦 ∈ V)} = {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ V ∧ 𝑦 ∈ V))}
8	6, 7	eqtri 2632	. . . . . . . . 9 ⊢ (V × V) = {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ V ∧ 𝑦 ∈ V))}
9	8	abeq2i 2722	. . . . . . . 8 ⊢ (𝑧 ∈ (V × V) ↔ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ V ∧ 𝑦 ∈ V)))
10		simpl 472	. . . . . . . . 9 ⊢ ((𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ V ∧ 𝑦 ∈ V)) → 𝑧 = ⟨𝑥, 𝑦⟩)
11	10	2eximi 1753	. . . . . . . 8 ⊢ (∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ V ∧ 𝑦 ∈ V)) → ∃𝑥∃𝑦 𝑧 = ⟨𝑥, 𝑦⟩)
12	9, 11	sylbi 206	. . . . . . 7 ⊢ (𝑧 ∈ (V × V) → ∃𝑥∃𝑦 𝑧 = ⟨𝑥, 𝑦⟩)
13	12	imim2i 16	. . . . . 6 ⊢ ((𝑧 ∈ 𝐴 → 𝑧 ∈ (V × V)) → (𝑧 ∈ 𝐴 → ∃𝑥∃𝑦 𝑧 = ⟨𝑥, 𝑦⟩))
14	5, 13	sylg 1740	. . . . 5 ⊢ (Rel 𝐴 → ∀𝑧(𝑧 ∈ 𝐴 → ∃𝑥∃𝑦 𝑧 = ⟨𝑥, 𝑦⟩))
15		eleq1 2676	. . . . . . . . . . . 12 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → (𝑧 ∈ 𝐴 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝐴))
16		eleq1 2676	. . . . . . . . . . . 12 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → (𝑧 ∈ 𝐵 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝐵))
17	15, 16	imbi12d 333	. . . . . . . . . . 11 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → ((𝑧 ∈ 𝐴 → 𝑧 ∈ 𝐵) ↔ (⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵)))
18	17	biimprcd 239	. . . . . . . . . 10 ⊢ ((⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵) → (𝑧 = ⟨𝑥, 𝑦⟩ → (𝑧 ∈ 𝐴 → 𝑧 ∈ 𝐵)))
19	18	2alimi 1731	. . . . . . . . 9 ⊢ (∀𝑥∀𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵) → ∀𝑥∀𝑦(𝑧 = ⟨𝑥, 𝑦⟩ → (𝑧 ∈ 𝐴 → 𝑧 ∈ 𝐵)))
20		19.23vv 1890	. . . . . . . . 9 ⊢ (∀𝑥∀𝑦(𝑧 = ⟨𝑥, 𝑦⟩ → (𝑧 ∈ 𝐴 → 𝑧 ∈ 𝐵)) ↔ (∃𝑥∃𝑦 𝑧 = ⟨𝑥, 𝑦⟩ → (𝑧 ∈ 𝐴 → 𝑧 ∈ 𝐵)))
21	19, 20	sylib 207	. . . . . . . 8 ⊢ (∀𝑥∀𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵) → (∃𝑥∃𝑦 𝑧 = ⟨𝑥, 𝑦⟩ → (𝑧 ∈ 𝐴 → 𝑧 ∈ 𝐵)))
22	21	com23 84	. . . . . . 7 ⊢ (∀𝑥∀𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵) → (𝑧 ∈ 𝐴 → (∃𝑥∃𝑦 𝑧 = ⟨𝑥, 𝑦⟩ → 𝑧 ∈ 𝐵)))
23	22	a2d 29	. . . . . 6 ⊢ (∀𝑥∀𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵) → ((𝑧 ∈ 𝐴 → ∃𝑥∃𝑦 𝑧 = ⟨𝑥, 𝑦⟩) → (𝑧 ∈ 𝐴 → 𝑧 ∈ 𝐵)))
24	23	alimdv 1832	. . . . 5 ⊢ (∀𝑥∀𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵) → (∀𝑧(𝑧 ∈ 𝐴 → ∃𝑥∃𝑦 𝑧 = ⟨𝑥, 𝑦⟩) → ∀𝑧(𝑧 ∈ 𝐴 → 𝑧 ∈ 𝐵)))
25	14, 24	syl5 33	. . . 4 ⊢ (∀𝑥∀𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵) → (Rel 𝐴 → ∀𝑧(𝑧 ∈ 𝐴 → 𝑧 ∈ 𝐵)))
26		dfss2 3557	. . . 4 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑧(𝑧 ∈ 𝐴 → 𝑧 ∈ 𝐵))
27	25, 26	syl6ibr 241	. . 3 ⊢ (∀𝑥∀𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵) → (Rel 𝐴 → 𝐴 ⊆ 𝐵))
28	27	com12 32	. 2 ⊢ (Rel 𝐴 → (∀𝑥∀𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵) → 𝐴 ⊆ 𝐵))
29	2, 28	impbid2 215	1 ⊢ (Rel 𝐴 → (𝐴 ⊆ 𝐵 ↔ ∀𝑥∀𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵)))

Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383  ∀wal 1473   = wceq 1475  ∃wex 1695   ∈ wcel 1977  {cab 2596  Vcvv 3173   ⊆ wss 3540  ⟨cop 4131  {copab 4642   × cxp 5036  Rel wrel 5043

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-in 3547  df-ss 3554  df-opab 4644  df-xp 5044  df-rel 5045

This theorem is referenced by:  eqrel  5132  relssi  5134  relssdv  5135  cotrg  5426  cnvsym  5429  intasym  5430  intirr  5433  codir  5435  qfto  5436  dfso2  30897  dfpo2  30898  dffun10  31191  imagesset  31230  undmrnresiss  36929  cnvssco  36931