Theorem ssrel2 4373

Description: A subclass relationship depends only on a relation's ordered pairs. This version of ssrel 4371 is restricted to the relation's domain. (Contributed by Thierry Arnoux, 25-Jan-2018.)

Assertion

Ref	Expression
ssrel2	⊢ (𝑅 ⊆ (A × B) → (𝑅 ⊆ 𝑆 ↔ ∀x ∈ A ∀y ∈ B (⟨x, y⟩ ∈ 𝑅 → ⟨x, y⟩ ∈ 𝑆)))

Distinct variable groups:   x,y,A   x,B,y   x,𝑅,y   x,𝑆,y

Proof of Theorem ssrel2

Dummy variable z is distinct from all other variables.

Step	Hyp	Ref	Expression
1		ssel 2933	. . . 4 ⊢ (𝑅 ⊆ 𝑆 → (⟨x, y⟩ ∈ 𝑅 → ⟨x, y⟩ ∈ 𝑆))
2	1	a1d 22	. . 3 ⊢ (𝑅 ⊆ 𝑆 → ((x ∈ A ∧ y ∈ B) → (⟨x, y⟩ ∈ 𝑅 → ⟨x, y⟩ ∈ 𝑆)))
3	2	ralrimivv 2394	. 2 ⊢ (𝑅 ⊆ 𝑆 → ∀x ∈ A ∀y ∈ B (⟨x, y⟩ ∈ 𝑅 → ⟨x, y⟩ ∈ 𝑆))
4		eleq1 2097	. . . . . . . . . . . 12 ⊢ (z = ⟨x, y⟩ → (z ∈ 𝑅 ↔ ⟨x, y⟩ ∈ 𝑅))
5		eleq1 2097	. . . . . . . . . . . 12 ⊢ (z = ⟨x, y⟩ → (z ∈ 𝑆 ↔ ⟨x, y⟩ ∈ 𝑆))
6	4, 5	imbi12d 223	. . . . . . . . . . 11 ⊢ (z = ⟨x, y⟩ → ((z ∈ 𝑅 → z ∈ 𝑆) ↔ (⟨x, y⟩ ∈ 𝑅 → ⟨x, y⟩ ∈ 𝑆)))
7	6	biimprcd 149	. . . . . . . . . 10 ⊢ ((⟨x, y⟩ ∈ 𝑅 → ⟨x, y⟩ ∈ 𝑆) → (z = ⟨x, y⟩ → (z ∈ 𝑅 → z ∈ 𝑆)))
8	7	ralimi 2378	. . . . . . . . 9 ⊢ (∀y ∈ B (⟨x, y⟩ ∈ 𝑅 → ⟨x, y⟩ ∈ 𝑆) → ∀y ∈ B (z = ⟨x, y⟩ → (z ∈ 𝑅 → z ∈ 𝑆)))
9	8	ralimi 2378	. . . . . . . 8 ⊢ (∀x ∈ A ∀y ∈ B (⟨x, y⟩ ∈ 𝑅 → ⟨x, y⟩ ∈ 𝑆) → ∀x ∈ A ∀y ∈ B (z = ⟨x, y⟩ → (z ∈ 𝑅 → z ∈ 𝑆)))
10		r19.23v 2419	. . . . . . . . . 10 ⊢ (∀y ∈ B (z = ⟨x, y⟩ → (z ∈ 𝑅 → z ∈ 𝑆)) ↔ (∃y ∈ B z = ⟨x, y⟩ → (z ∈ 𝑅 → z ∈ 𝑆)))
11	10	ralbii 2324	. . . . . . . . 9 ⊢ (∀x ∈ A ∀y ∈ B (z = ⟨x, y⟩ → (z ∈ 𝑅 → z ∈ 𝑆)) ↔ ∀x ∈ A (∃y ∈ B z = ⟨x, y⟩ → (z ∈ 𝑅 → z ∈ 𝑆)))
12		r19.23v 2419	. . . . . . . . 9 ⊢ (∀x ∈ A (∃y ∈ B z = ⟨x, y⟩ → (z ∈ 𝑅 → z ∈ 𝑆)) ↔ (∃x ∈ A ∃y ∈ B z = ⟨x, y⟩ → (z ∈ 𝑅 → z ∈ 𝑆)))
13	11, 12	bitri 173	. . . . . . . 8 ⊢ (∀x ∈ A ∀y ∈ B (z = ⟨x, y⟩ → (z ∈ 𝑅 → z ∈ 𝑆)) ↔ (∃x ∈ A ∃y ∈ B z = ⟨x, y⟩ → (z ∈ 𝑅 → z ∈ 𝑆)))
14	9, 13	sylib 127	. . . . . . 7 ⊢ (∀x ∈ A ∀y ∈ B (⟨x, y⟩ ∈ 𝑅 → ⟨x, y⟩ ∈ 𝑆) → (∃x ∈ A ∃y ∈ B z = ⟨x, y⟩ → (z ∈ 𝑅 → z ∈ 𝑆)))
15	14	com23 72	. . . . . 6 ⊢ (∀x ∈ A ∀y ∈ B (⟨x, y⟩ ∈ 𝑅 → ⟨x, y⟩ ∈ 𝑆) → (z ∈ 𝑅 → (∃x ∈ A ∃y ∈ B z = ⟨x, y⟩ → z ∈ 𝑆)))
16	15	a2d 23	. . . . 5 ⊢ (∀x ∈ A ∀y ∈ B (⟨x, y⟩ ∈ 𝑅 → ⟨x, y⟩ ∈ 𝑆) → ((z ∈ 𝑅 → ∃x ∈ A ∃y ∈ B z = ⟨x, y⟩) → (z ∈ 𝑅 → z ∈ 𝑆)))
17	16	alimdv 1756	. . . 4 ⊢ (∀x ∈ A ∀y ∈ B (⟨x, y⟩ ∈ 𝑅 → ⟨x, y⟩ ∈ 𝑆) → (∀z(z ∈ 𝑅 → ∃x ∈ A ∃y ∈ B z = ⟨x, y⟩) → ∀z(z ∈ 𝑅 → z ∈ 𝑆)))
18		dfss2 2928	. . . . 5 ⊢ (𝑅 ⊆ (A × B) ↔ ∀z(z ∈ 𝑅 → z ∈ (A × B)))
19		elxp2 4306	. . . . . . 7 ⊢ (z ∈ (A × B) ↔ ∃x ∈ A ∃y ∈ B z = ⟨x, y⟩)
20	19	imbi2i 215	. . . . . 6 ⊢ ((z ∈ 𝑅 → z ∈ (A × B)) ↔ (z ∈ 𝑅 → ∃x ∈ A ∃y ∈ B z = ⟨x, y⟩))
21	20	albii 1356	. . . . 5 ⊢ (∀z(z ∈ 𝑅 → z ∈ (A × B)) ↔ ∀z(z ∈ 𝑅 → ∃x ∈ A ∃y ∈ B z = ⟨x, y⟩))
22	18, 21	bitri 173	. . . 4 ⊢ (𝑅 ⊆ (A × B) ↔ ∀z(z ∈ 𝑅 → ∃x ∈ A ∃y ∈ B z = ⟨x, y⟩))
23		dfss2 2928	. . . 4 ⊢ (𝑅 ⊆ 𝑆 ↔ ∀z(z ∈ 𝑅 → z ∈ 𝑆))
24	17, 22, 23	3imtr4g 194	. . 3 ⊢ (∀x ∈ A ∀y ∈ B (⟨x, y⟩ ∈ 𝑅 → ⟨x, y⟩ ∈ 𝑆) → (𝑅 ⊆ (A × B) → 𝑅 ⊆ 𝑆))
25	24	com12 27	. 2 ⊢ (𝑅 ⊆ (A × B) → (∀x ∈ A ∀y ∈ B (⟨x, y⟩ ∈ 𝑅 → ⟨x, y⟩ ∈ 𝑆) → 𝑅 ⊆ 𝑆))
26	3, 25	impbid2 131	1 ⊢ (𝑅 ⊆ (A × B) → (𝑅 ⊆ 𝑆 ↔ ∀x ∈ A ∀y ∈ B (⟨x, y⟩ ∈ 𝑅 → ⟨x, y⟩ ∈ 𝑆)))

Syntax hints:   → wi 4   ∧ wa 97   ↔ wb 98  ∀wal 1240   = wceq 1242   ∈ wcel 1390  ∀wral 2300  ∃wrex 2301   ⊆ wss 2911  ⟨cop 3370   × cxp 4286

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bnd 1396  ax-4 1397  ax-14 1402  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-sep 3866  ax-pow 3918  ax-pr 3935

This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-nf 1347  df-sb 1643  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ral 2305  df-rex 2306  df-v 2553  df-un 2916  df-in 2918  df-ss 2925  df-pw 3353  df-sn 3373  df-pr 3374  df-op 3376  df-opab 3810  df-xp 4294

This theorem is referenced by: (None)