Theorem ssrel2 4353

Description: A subclass relationship depends only on a relation's ordered pairs. This version of ssrel 4351 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 2912	. . . 4 ⊢ (𝑅 ⊆ 𝑆 → (⟨x, y⟩ ∈ 𝑅 → ⟨x, y⟩ ∈ 𝑆))
2	1	a1d 22	. . 3 ⊢ (𝑅 ⊆ 𝑆 → ((x ∈ A ∧ y ∈ B) → (⟨x, y⟩ ∈ 𝑅 → ⟨x, y⟩ ∈ 𝑆)))
3	2	ralrimivv 2374	. 2 ⊢ (𝑅 ⊆ 𝑆 → ∀x ∈ A ∀y ∈ B (⟨x, y⟩ ∈ 𝑅 → ⟨x, y⟩ ∈ 𝑆))
4		eleq1 2078	. . . . . . . . . . . 12 ⊢ (z = ⟨x, y⟩ → (z ∈ 𝑅 ↔ ⟨x, y⟩ ∈ 𝑅))
5		eleq1 2078	. . . . . . . . . . . 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 2358	. . . . . . . . 9 ⊢ (∀y ∈ B (⟨x, y⟩ ∈ 𝑅 → ⟨x, y⟩ ∈ 𝑆) → ∀y ∈ B (z = ⟨x, y⟩ → (z ∈ 𝑅 → z ∈ 𝑆)))
9	8	ralimi 2358	. . . . . . . 8 ⊢ (∀x ∈ A ∀y ∈ B (⟨x, y⟩ ∈ 𝑅 → ⟨x, y⟩ ∈ 𝑆) → ∀x ∈ A ∀y ∈ B (z = ⟨x, y⟩ → (z ∈ 𝑅 → z ∈ 𝑆)))
10		r19.23v 2399	. . . . . . . . . 10 ⊢ (∀y ∈ B (z = ⟨x, y⟩ → (z ∈ 𝑅 → z ∈ 𝑆)) ↔ (∃y ∈ B z = ⟨x, y⟩ → (z ∈ 𝑅 → z ∈ 𝑆)))
11	10	ralbii 2304	. . . . . . . . 9 ⊢ (∀x ∈ A ∀y ∈ B (z = ⟨x, y⟩ → (z ∈ 𝑅 → z ∈ 𝑆)) ↔ ∀x ∈ A (∃y ∈ B z = ⟨x, y⟩ → (z ∈ 𝑅 → z ∈ 𝑆)))
12		r19.23v 2399	. . . . . . . . 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 1737	. . . 4 ⊢ (∀x ∈ A ∀y ∈ B (⟨x, y⟩ ∈ 𝑅 → ⟨x, y⟩ ∈ 𝑆) → (∀z(z ∈ 𝑅 → ∃x ∈ A ∃y ∈ B z = ⟨x, y⟩) → ∀z(z ∈ 𝑅 → z ∈ 𝑆)))
18		dfss2 2907	. . . . 5 ⊢ (𝑅 ⊆ (A × B) ↔ ∀z(z ∈ 𝑅 → z ∈ (A × B)))
19		elxp2 4286	. . . . . . 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 1335	. . . . 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 2907	. . . 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 1224   = wceq 1226   ∈ wcel 1370  ∀wral 2280  ∃wrex 2281   ⊆ wss 2890  ⟨cop 3349   × cxp 4266

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 617  ax-5 1312  ax-7 1313  ax-gen 1314  ax-ie1 1359  ax-ie2 1360  ax-8 1372  ax-10 1373  ax-11 1374  ax-i12 1375  ax-bnd 1376  ax-4 1377  ax-14 1382  ax-17 1396  ax-i9 1400  ax-ial 1405  ax-i5r 1406  ax-ext 2000  ax-sep 3845  ax-pow 3897  ax-pr 3914

This theorem depends on definitions:  df-bi 110  df-3an 873  df-tru 1229  df-nf 1326  df-sb 1624  df-clab 2005  df-cleq 2011  df-clel 2014  df-nfc 2145  df-ral 2285  df-rex 2286  df-v 2533  df-un 2895  df-in 2897  df-ss 2904  df-pw 3332  df-sn 3352  df-pr 3353  df-op 3355  df-opab 3789  df-xp 4274

This theorem is referenced by: (None)