# Metamath Proof Explorer

## Theorem ssrel2

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

Ref Expression
Assertion ssrel2 ${⊢}{R}\subseteq {A}×{B}\to \left({R}\subseteq {S}↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\left(⟨{x},{y}⟩\in {R}\to ⟨{x},{y}⟩\in {S}\right)\right)$

### Proof

Step Hyp Ref Expression
1 ssel ${⊢}{R}\subseteq {S}\to \left(⟨{x},{y}⟩\in {R}\to ⟨{x},{y}⟩\in {S}\right)$
2 1 a1d ${⊢}{R}\subseteq {S}\to \left(\left({x}\in {A}\wedge {y}\in {B}\right)\to \left(⟨{x},{y}⟩\in {R}\to ⟨{x},{y}⟩\in {S}\right)\right)$
3 2 ralrimivv ${⊢}{R}\subseteq {S}\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\left(⟨{x},{y}⟩\in {R}\to ⟨{x},{y}⟩\in {S}\right)$
4 eleq1 ${⊢}{z}=⟨{x},{y}⟩\to \left({z}\in {R}↔⟨{x},{y}⟩\in {R}\right)$
5 eleq1 ${⊢}{z}=⟨{x},{y}⟩\to \left({z}\in {S}↔⟨{x},{y}⟩\in {S}\right)$
6 4 5 imbi12d ${⊢}{z}=⟨{x},{y}⟩\to \left(\left({z}\in {R}\to {z}\in {S}\right)↔\left(⟨{x},{y}⟩\in {R}\to ⟨{x},{y}⟩\in {S}\right)\right)$
7 6 biimprcd ${⊢}\left(⟨{x},{y}⟩\in {R}\to ⟨{x},{y}⟩\in {S}\right)\to \left({z}=⟨{x},{y}⟩\to \left({z}\in {R}\to {z}\in {S}\right)\right)$
8 7 2ralimi ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\left(⟨{x},{y}⟩\in {R}\to ⟨{x},{y}⟩\in {S}\right)\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({z}=⟨{x},{y}⟩\to \left({z}\in {R}\to {z}\in {S}\right)\right)$
9 r19.23v ${⊢}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({z}=⟨{x},{y}⟩\to \left({z}\in {R}\to {z}\in {S}\right)\right)↔\left(\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{z}=⟨{x},{y}⟩\to \left({z}\in {R}\to {z}\in {S}\right)\right)$
10 9 ralbii ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({z}=⟨{x},{y}⟩\to \left({z}\in {R}\to {z}\in {S}\right)\right)↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left(\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{z}=⟨{x},{y}⟩\to \left({z}\in {R}\to {z}\in {S}\right)\right)$
11 r19.23v ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left(\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{z}=⟨{x},{y}⟩\to \left({z}\in {R}\to {z}\in {S}\right)\right)↔\left(\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{z}=⟨{x},{y}⟩\to \left({z}\in {R}\to {z}\in {S}\right)\right)$
12 10 11 bitri ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\left({z}=⟨{x},{y}⟩\to \left({z}\in {R}\to {z}\in {S}\right)\right)↔\left(\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{z}=⟨{x},{y}⟩\to \left({z}\in {R}\to {z}\in {S}\right)\right)$
13 8 12 sylib ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\left(⟨{x},{y}⟩\in {R}\to ⟨{x},{y}⟩\in {S}\right)\to \left(\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{z}=⟨{x},{y}⟩\to \left({z}\in {R}\to {z}\in {S}\right)\right)$
14 13 com23 ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\left(⟨{x},{y}⟩\in {R}\to ⟨{x},{y}⟩\in {S}\right)\to \left({z}\in {R}\to \left(\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{z}=⟨{x},{y}⟩\to {z}\in {S}\right)\right)$
15 14 a2d ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\left(⟨{x},{y}⟩\in {R}\to ⟨{x},{y}⟩\in {S}\right)\to \left(\left({z}\in {R}\to \exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{z}=⟨{x},{y}⟩\right)\to \left({z}\in {R}\to {z}\in {S}\right)\right)$
16 15 alimdv ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\left(⟨{x},{y}⟩\in {R}\to ⟨{x},{y}⟩\in {S}\right)\to \left(\forall {z}\phantom{\rule{.4em}{0ex}}\left({z}\in {R}\to \exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{z}=⟨{x},{y}⟩\right)\to \forall {z}\phantom{\rule{.4em}{0ex}}\left({z}\in {R}\to {z}\in {S}\right)\right)$
17 dfss2 ${⊢}{R}\subseteq {A}×{B}↔\forall {z}\phantom{\rule{.4em}{0ex}}\left({z}\in {R}\to {z}\in \left({A}×{B}\right)\right)$
18 elxp2 ${⊢}{z}\in \left({A}×{B}\right)↔\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{z}=⟨{x},{y}⟩$
19 18 imbi2i ${⊢}\left({z}\in {R}\to {z}\in \left({A}×{B}\right)\right)↔\left({z}\in {R}\to \exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{z}=⟨{x},{y}⟩\right)$
20 19 albii ${⊢}\forall {z}\phantom{\rule{.4em}{0ex}}\left({z}\in {R}\to {z}\in \left({A}×{B}\right)\right)↔\forall {z}\phantom{\rule{.4em}{0ex}}\left({z}\in {R}\to \exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{z}=⟨{x},{y}⟩\right)$
21 17 20 bitri ${⊢}{R}\subseteq {A}×{B}↔\forall {z}\phantom{\rule{.4em}{0ex}}\left({z}\in {R}\to \exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{z}=⟨{x},{y}⟩\right)$
22 dfss2 ${⊢}{R}\subseteq {S}↔\forall {z}\phantom{\rule{.4em}{0ex}}\left({z}\in {R}\to {z}\in {S}\right)$
23 16 21 22 3imtr4g ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\left(⟨{x},{y}⟩\in {R}\to ⟨{x},{y}⟩\in {S}\right)\to \left({R}\subseteq {A}×{B}\to {R}\subseteq {S}\right)$
24 23 com12 ${⊢}{R}\subseteq {A}×{B}\to \left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\left(⟨{x},{y}⟩\in {R}\to ⟨{x},{y}⟩\in {S}\right)\to {R}\subseteq {S}\right)$
25 3 24 impbid2 ${⊢}{R}\subseteq {A}×{B}\to \left({R}\subseteq {S}↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\left(⟨{x},{y}⟩\in {R}\to ⟨{x},{y}⟩\in {S}\right)\right)$