Theorem ssrel 5659

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 5205, ax-nul 5212, ax-pr 5332. (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 3963	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵))
2	1	alrimivv 1929	. 2 ⊢ (𝐴 ⊆ 𝐵 → ∀𝑥∀𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵))
3		df-rel 5564	. . . . . . 7 ⊢ (Rel 𝐴 ↔ 𝐴 ⊆ (V × V))
4		dfss2 3957	. . . . . . 7 ⊢ (𝐴 ⊆ (V × V) ↔ ∀𝑧(𝑧 ∈ 𝐴 → 𝑧 ∈ (V × V)))
5	3, 4	sylbb 221	. . . . . 6 ⊢ (Rel 𝐴 → ∀𝑧(𝑧 ∈ 𝐴 → 𝑧 ∈ (V × V)))
6		df-xp 5563	. . . . . . . . . 10 ⊢ (V × V) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ V ∧ 𝑦 ∈ V)}
7		df-opab 5131	. . . . . . . . . 10 ⊢ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ V ∧ 𝑦 ∈ V)} = {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ V ∧ 𝑦 ∈ V))}
8	6, 7	eqtri 2846	. . . . . . . . 9 ⊢ (V × V) = {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ V ∧ 𝑦 ∈ V))}
9	8	abeq2i 2950	. . . . . . . 8 ⊢ (𝑧 ∈ (V × V) ↔ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ V ∧ 𝑦 ∈ V)))
10		simpl 485	. . . . . . . . 9 ⊢ ((𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ V ∧ 𝑦 ∈ V)) → 𝑧 = ⟨𝑥, 𝑦⟩)
11	10	2eximi 1836	. . . . . . . 8 ⊢ (∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ V ∧ 𝑦 ∈ V)) → ∃𝑥∃𝑦 𝑧 = ⟨𝑥, 𝑦⟩)
12	9, 11	sylbi 219	. . . . . . 7 ⊢ (𝑧 ∈ (V × V) → ∃𝑥∃𝑦 𝑧 = ⟨𝑥, 𝑦⟩)
13	12	imim2i 16	. . . . . 6 ⊢ ((𝑧 ∈ 𝐴 → 𝑧 ∈ (V × V)) → (𝑧 ∈ 𝐴 → ∃𝑥∃𝑦 𝑧 = ⟨𝑥, 𝑦⟩))
14	5, 13	sylg 1823	. . . . 5 ⊢ (Rel 𝐴 → ∀𝑧(𝑧 ∈ 𝐴 → ∃𝑥∃𝑦 𝑧 = ⟨𝑥, 𝑦⟩))
15		eleq1 2902	. . . . . . . . . . . 12 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → (𝑧 ∈ 𝐴 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝐴))
16		eleq1 2902	. . . . . . . . . . . 12 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → (𝑧 ∈ 𝐵 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝐵))
17	15, 16	imbi12d 347	. . . . . . . . . . 11 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → ((𝑧 ∈ 𝐴 → 𝑧 ∈ 𝐵) ↔ (⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵)))
18	17	biimprcd 252	. . . . . . . . . 10 ⊢ ((⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵) → (𝑧 = ⟨𝑥, 𝑦⟩ → (𝑧 ∈ 𝐴 → 𝑧 ∈ 𝐵)))
19	18	2alimi 1813	. . . . . . . . 9 ⊢ (∀𝑥∀𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵) → ∀𝑥∀𝑦(𝑧 = ⟨𝑥, 𝑦⟩ → (𝑧 ∈ 𝐴 → 𝑧 ∈ 𝐵)))
20		19.23vv 1944	. . . . . . . . 9 ⊢ (∀𝑥∀𝑦(𝑧 = ⟨𝑥, 𝑦⟩ → (𝑧 ∈ 𝐴 → 𝑧 ∈ 𝐵)) ↔ (∃𝑥∃𝑦 𝑧 = ⟨𝑥, 𝑦⟩ → (𝑧 ∈ 𝐴 → 𝑧 ∈ 𝐵)))
21	19, 20	sylib 220	. . . . . . . 8 ⊢ (∀𝑥∀𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵) → (∃𝑥∃𝑦 𝑧 = ⟨𝑥, 𝑦⟩ → (𝑧 ∈ 𝐴 → 𝑧 ∈ 𝐵)))
22	21	com23 86	. . . . . . 7 ⊢ (∀𝑥∀𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵) → (𝑧 ∈ 𝐴 → (∃𝑥∃𝑦 𝑧 = ⟨𝑥, 𝑦⟩ → 𝑧 ∈ 𝐵)))
23	22	a2d 29	. . . . . 6 ⊢ (∀𝑥∀𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵) → ((𝑧 ∈ 𝐴 → ∃𝑥∃𝑦 𝑧 = ⟨𝑥, 𝑦⟩) → (𝑧 ∈ 𝐴 → 𝑧 ∈ 𝐵)))
24	23	alimdv 1917	. . . . 5 ⊢ (∀𝑥∀𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵) → (∀𝑧(𝑧 ∈ 𝐴 → ∃𝑥∃𝑦 𝑧 = ⟨𝑥, 𝑦⟩) → ∀𝑧(𝑧 ∈ 𝐴 → 𝑧 ∈ 𝐵)))
25	14, 24	syl5 34	. . . 4 ⊢ (∀𝑥∀𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵) → (Rel 𝐴 → ∀𝑧(𝑧 ∈ 𝐴 → 𝑧 ∈ 𝐵)))
26		dfss2 3957	. . . 4 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑧(𝑧 ∈ 𝐴 → 𝑧 ∈ 𝐵))
27	25, 26	syl6ibr 254	. . 3 ⊢ (∀𝑥∀𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵) → (Rel 𝐴 → 𝐴 ⊆ 𝐵))
28	27	com12 32	. 2 ⊢ (Rel 𝐴 → (∀𝑥∀𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵) → 𝐴 ⊆ 𝐵))
29	2, 28	impbid2 228	1 ⊢ (Rel 𝐴 → (𝐴 ⊆ 𝐵 ↔ ∀𝑥∀𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵)))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398  ∀wal 1535   = wceq 1537  ∃wex 1780   ∈ wcel 2114  {cab 2801  Vcvv 3496   ⊆ wss 3938  ⟨cop 4575  {copab 5130   × cxp 5555  Rel wrel 5562

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-in 3945  df-ss 3954  df-opab 5131  df-xp 5563  df-rel 5564

This theorem is referenced by:  eqrel  5660  relssi  5662  relssdv  5663  cotrg  5973  cnvsym  5976  intasym  5977  intirr  5980  codir  5982  qfto  5983  dfso2  32992  dfpo2  32993  dffun10  33377  imagesset  33416  ssrel3  35558  undmrnresiss  39971  cnvssco  39973