Theorem ssrel 5657

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 5203, ax-nul 5210, ax-pr 5330. (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 3961	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵))
2	1	alrimivv 1929	. 2 ⊢ (𝐴 ⊆ 𝐵 → ∀𝑥∀𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵))
3		df-rel 5562	. . . . . . 7 ⊢ (Rel 𝐴 ↔ 𝐴 ⊆ (V × V))
4		dfss2 3955	. . . . . . 7 ⊢ (𝐴 ⊆ (V × V) ↔ ∀𝑧(𝑧 ∈ 𝐴 → 𝑧 ∈ (V × V)))
5	3, 4	sylbb 221	. . . . . 6 ⊢ (Rel 𝐴 → ∀𝑧(𝑧 ∈ 𝐴 → 𝑧 ∈ (V × V)))
6		df-xp 5561	. . . . . . . . . 10 ⊢ (V × V) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ V ∧ 𝑦 ∈ V)}
7		df-opab 5129	. . . . . . . . . 10 ⊢ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ V ∧ 𝑦 ∈ V)} = {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ V ∧ 𝑦 ∈ V))}
8	6, 7	eqtri 2844	. . . . . . . . 9 ⊢ (V × V) = {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ V ∧ 𝑦 ∈ V))}
9	8	abeq2i 2948	. . . . . . . 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 2900	. . . . . . . . . . . 12 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → (𝑧 ∈ 𝐴 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝐴))
16		eleq1 2900	. . . . . . . . . . . 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 3955	. . . 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 2799  Vcvv 3494   ⊆ wss 3936  ⟨cop 4573  {copab 5128   × cxp 5553  Rel wrel 5560

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 2793

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 2800  df-cleq 2814  df-clel 2893  df-in 3943  df-ss 3952  df-opab 5129  df-xp 5561  df-rel 5562

This theorem is referenced by:  eqrel  5658  relssi  5660  relssdv  5661  cotrg  5971  cnvsym  5974  intasym  5975  intirr  5978  codir  5980  qfto  5981  dfso2  32990  dfpo2  32991  dffun10  33375  imagesset  33414  ssrel3  35571  undmrnresiss  39984  cnvssco  39986