# Metamath Proof Explorer

## Theorem brfvrcld

Description: If two elements are connected by the reflexive closure of a relation, then they are connected via zero or one instances the relation. (Contributed by RP, 21-Jul-2020)

Ref Expression
Hypothesis brfvrcld.r ${⊢}{\phi }\to {R}\in \mathrm{V}$
Assertion brfvrcld ${⊢}{\phi }\to \left({A}\mathrm{r*}\left({R}\right){B}↔\left({A}\left({R}{↑}_{r}0\right){B}\vee {A}\left({R}{↑}_{r}1\right){B}\right)\right)$

### Proof

Step Hyp Ref Expression
1 brfvrcld.r ${⊢}{\phi }\to {R}\in \mathrm{V}$
2 dfrcl4 ${⊢}\mathrm{r*}=\left({r}\in \mathrm{V}⟼\bigcup _{{n}\in \left\{0,1\right\}}\left({r}{↑}_{r}{n}\right)\right)$
3 0nn0 ${⊢}0\in {ℕ}_{0}$
4 1nn0 ${⊢}1\in {ℕ}_{0}$
5 prssi ${⊢}\left(0\in {ℕ}_{0}\wedge 1\in {ℕ}_{0}\right)\to \left\{0,1\right\}\subseteq {ℕ}_{0}$
6 3 4 5 mp2an ${⊢}\left\{0,1\right\}\subseteq {ℕ}_{0}$
7 6 a1i ${⊢}{\phi }\to \left\{0,1\right\}\subseteq {ℕ}_{0}$
8 2 1 7 brmptiunrelexpd ${⊢}{\phi }\to \left({A}\mathrm{r*}\left({R}\right){B}↔\exists {n}\in \left\{0,1\right\}\phantom{\rule{.4em}{0ex}}{A}\left({R}{↑}_{r}{n}\right){B}\right)$
9 oveq2 ${⊢}{n}=0\to {R}{↑}_{r}{n}={R}{↑}_{r}0$
10 9 breqd ${⊢}{n}=0\to \left({A}\left({R}{↑}_{r}{n}\right){B}↔{A}\left({R}{↑}_{r}0\right){B}\right)$
11 oveq2 ${⊢}{n}=1\to {R}{↑}_{r}{n}={R}{↑}_{r}1$
12 11 breqd ${⊢}{n}=1\to \left({A}\left({R}{↑}_{r}{n}\right){B}↔{A}\left({R}{↑}_{r}1\right){B}\right)$
13 10 12 rexprg ${⊢}\left(0\in {ℕ}_{0}\wedge 1\in {ℕ}_{0}\right)\to \left(\exists {n}\in \left\{0,1\right\}\phantom{\rule{.4em}{0ex}}{A}\left({R}{↑}_{r}{n}\right){B}↔\left({A}\left({R}{↑}_{r}0\right){B}\vee {A}\left({R}{↑}_{r}1\right){B}\right)\right)$
14 3 4 13 mp2an ${⊢}\exists {n}\in \left\{0,1\right\}\phantom{\rule{.4em}{0ex}}{A}\left({R}{↑}_{r}{n}\right){B}↔\left({A}\left({R}{↑}_{r}0\right){B}\vee {A}\left({R}{↑}_{r}1\right){B}\right)$
15 8 14 syl6bb ${⊢}{\phi }\to \left({A}\mathrm{r*}\left({R}\right){B}↔\left({A}\left({R}{↑}_{r}0\right){B}\vee {A}\left({R}{↑}_{r}1\right){B}\right)\right)$