# Metamath Proof Explorer

Description: For sets, the SSet binary relation is equivalent to the subset relationship. (Contributed by Scott Fenton, 31-Mar-2012)

Ref Expression
Hypothesis brsset.1 ${⊢}{B}\in \mathrm{V}$
Assertion brsset ${⊢}{A}\mathrm{𝖲𝖲𝖾𝗍}{B}↔{A}\subseteq {B}$

### Proof

Step Hyp Ref Expression
1 brsset.1 ${⊢}{B}\in \mathrm{V}$
2 relsset ${⊢}\mathrm{Rel}\mathrm{𝖲𝖲𝖾𝗍}$
3 2 brrelex1i ${⊢}{A}\mathrm{𝖲𝖲𝖾𝗍}{B}\to {A}\in \mathrm{V}$
4 1 ssex ${⊢}{A}\subseteq {B}\to {A}\in \mathrm{V}$
5 breq1 ${⊢}{x}={A}\to \left({x}\mathrm{𝖲𝖲𝖾𝗍}{B}↔{A}\mathrm{𝖲𝖲𝖾𝗍}{B}\right)$
6 sseq1 ${⊢}{x}={A}\to \left({x}\subseteq {B}↔{A}\subseteq {B}\right)$
7 opex ${⊢}⟨{x},{B}⟩\in \mathrm{V}$
8 7 elrn ${⊢}⟨{x},{B}⟩\in \mathrm{ran}\left(\mathrm{E}\otimes \left(\mathrm{V}\setminus \mathrm{E}\right)\right)↔\exists {y}\phantom{\rule{.4em}{0ex}}{y}\left(\mathrm{E}\otimes \left(\mathrm{V}\setminus \mathrm{E}\right)\right)⟨{x},{B}⟩$
9 vex ${⊢}{y}\in \mathrm{V}$
10 vex ${⊢}{x}\in \mathrm{V}$
11 9 10 1 brtxp ${⊢}{y}\left(\mathrm{E}\otimes \left(\mathrm{V}\setminus \mathrm{E}\right)\right)⟨{x},{B}⟩↔\left({y}\mathrm{E}{x}\wedge {y}\left(\mathrm{V}\setminus \mathrm{E}\right){B}\right)$
12 epel ${⊢}{y}\mathrm{E}{x}↔{y}\in {x}$
13 brv ${⊢}{y}\mathrm{V}{B}$
14 brdif ${⊢}{y}\left(\mathrm{V}\setminus \mathrm{E}\right){B}↔\left({y}\mathrm{V}{B}\wedge ¬{y}\mathrm{E}{B}\right)$
15 13 14 mpbiran ${⊢}{y}\left(\mathrm{V}\setminus \mathrm{E}\right){B}↔¬{y}\mathrm{E}{B}$
16 1 epeli ${⊢}{y}\mathrm{E}{B}↔{y}\in {B}$
17 15 16 xchbinx ${⊢}{y}\left(\mathrm{V}\setminus \mathrm{E}\right){B}↔¬{y}\in {B}$
18 12 17 anbi12i ${⊢}\left({y}\mathrm{E}{x}\wedge {y}\left(\mathrm{V}\setminus \mathrm{E}\right){B}\right)↔\left({y}\in {x}\wedge ¬{y}\in {B}\right)$
19 11 18 bitri ${⊢}{y}\left(\mathrm{E}\otimes \left(\mathrm{V}\setminus \mathrm{E}\right)\right)⟨{x},{B}⟩↔\left({y}\in {x}\wedge ¬{y}\in {B}\right)$
20 19 exbii ${⊢}\exists {y}\phantom{\rule{.4em}{0ex}}{y}\left(\mathrm{E}\otimes \left(\mathrm{V}\setminus \mathrm{E}\right)\right)⟨{x},{B}⟩↔\exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\in {x}\wedge ¬{y}\in {B}\right)$
21 exanali ${⊢}\exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\in {x}\wedge ¬{y}\in {B}\right)↔¬\forall {y}\phantom{\rule{.4em}{0ex}}\left({y}\in {x}\to {y}\in {B}\right)$
22 8 20 21 3bitrri ${⊢}¬\forall {y}\phantom{\rule{.4em}{0ex}}\left({y}\in {x}\to {y}\in {B}\right)↔⟨{x},{B}⟩\in \mathrm{ran}\left(\mathrm{E}\otimes \left(\mathrm{V}\setminus \mathrm{E}\right)\right)$
23 22 con1bii ${⊢}¬⟨{x},{B}⟩\in \mathrm{ran}\left(\mathrm{E}\otimes \left(\mathrm{V}\setminus \mathrm{E}\right)\right)↔\forall {y}\phantom{\rule{.4em}{0ex}}\left({y}\in {x}\to {y}\in {B}\right)$
24 df-br ${⊢}{x}\mathrm{𝖲𝖲𝖾𝗍}{B}↔⟨{x},{B}⟩\in \mathrm{𝖲𝖲𝖾𝗍}$
25 df-sset ${⊢}\mathrm{𝖲𝖲𝖾𝗍}=\left(\mathrm{V}×\mathrm{V}\right)\setminus \mathrm{ran}\left(\mathrm{E}\otimes \left(\mathrm{V}\setminus \mathrm{E}\right)\right)$
26 25 eleq2i ${⊢}⟨{x},{B}⟩\in \mathrm{𝖲𝖲𝖾𝗍}↔⟨{x},{B}⟩\in \left(\left(\mathrm{V}×\mathrm{V}\right)\setminus \mathrm{ran}\left(\mathrm{E}\otimes \left(\mathrm{V}\setminus \mathrm{E}\right)\right)\right)$
27 10 1 opelvv ${⊢}⟨{x},{B}⟩\in \left(\mathrm{V}×\mathrm{V}\right)$
28 eldif ${⊢}⟨{x},{B}⟩\in \left(\left(\mathrm{V}×\mathrm{V}\right)\setminus \mathrm{ran}\left(\mathrm{E}\otimes \left(\mathrm{V}\setminus \mathrm{E}\right)\right)\right)↔\left(⟨{x},{B}⟩\in \left(\mathrm{V}×\mathrm{V}\right)\wedge ¬⟨{x},{B}⟩\in \mathrm{ran}\left(\mathrm{E}\otimes \left(\mathrm{V}\setminus \mathrm{E}\right)\right)\right)$
29 27 28 mpbiran ${⊢}⟨{x},{B}⟩\in \left(\left(\mathrm{V}×\mathrm{V}\right)\setminus \mathrm{ran}\left(\mathrm{E}\otimes \left(\mathrm{V}\setminus \mathrm{E}\right)\right)\right)↔¬⟨{x},{B}⟩\in \mathrm{ran}\left(\mathrm{E}\otimes \left(\mathrm{V}\setminus \mathrm{E}\right)\right)$
30 26 29 bitri ${⊢}⟨{x},{B}⟩\in \mathrm{𝖲𝖲𝖾𝗍}↔¬⟨{x},{B}⟩\in \mathrm{ran}\left(\mathrm{E}\otimes \left(\mathrm{V}\setminus \mathrm{E}\right)\right)$
31 24 30 bitri ${⊢}{x}\mathrm{𝖲𝖲𝖾𝗍}{B}↔¬⟨{x},{B}⟩\in \mathrm{ran}\left(\mathrm{E}\otimes \left(\mathrm{V}\setminus \mathrm{E}\right)\right)$
32 dfss2 ${⊢}{x}\subseteq {B}↔\forall {y}\phantom{\rule{.4em}{0ex}}\left({y}\in {x}\to {y}\in {B}\right)$
33 23 31 32 3bitr4i ${⊢}{x}\mathrm{𝖲𝖲𝖾𝗍}{B}↔{x}\subseteq {B}$
34 5 6 33 vtoclbg ${⊢}{A}\in \mathrm{V}\to \left({A}\mathrm{𝖲𝖲𝖾𝗍}{B}↔{A}\subseteq {B}\right)$
35 3 4 34 pm5.21nii ${⊢}{A}\mathrm{𝖲𝖲𝖾𝗍}{B}↔{A}\subseteq {B}$