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\leftrightarrow \left(A\left(R{\uparrow }_{r}0\right)B\vee A\left(R{\uparrow }_{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{\uparrow }_{r}n\right)\right)$$
3		0nn0	$$⊢0\in {\mathbb{N}}_0$$
4		1nn0	$$⊢1\in {\mathbb{N}}_0$$
5		prssi	$$⊢\left(0\in {\mathbb{N}}_0\wedge 1\in {\mathbb{N}}_0\right)\to \left\{0,1\right\}\subseteq {\mathbb{N}}_0$$
6	3 4 5	mp2an	$$⊢\left\{0,1\right\}\subseteq {\mathbb{N}}_0$$
7	6	a1i	$$⊢\phi \to \left\{0,1\right\}\subseteq {\mathbb{N}}_0$$
8	2 1 7	brmptiunrelexpd	$$⊢\phi \to \left(A\mathrm{r*}\left(R\right)B\leftrightarrow \exists n\in \left\{0,1\right\}A\left(R{\uparrow }_{r}n\right)B\right)$$
9		oveq2	$$⊢n=0\to R{\uparrow }_{r}n=R{\uparrow }_{r}0$$
10	9	breqd	$$⊢n=0\to \left(A\left(R{\uparrow }_{r}n\right)B\leftrightarrow A\left(R{\uparrow }_{r}0\right)B\right)$$
11		oveq2	$$⊢n=1\to R{\uparrow }_{r}n=R{\uparrow }_{r}1$$
12	11	breqd	$$⊢n=1\to \left(A\left(R{\uparrow }_{r}n\right)B\leftrightarrow A\left(R{\uparrow }_{r}1\right)B\right)$$
13	10 12	rexprg	$$⊢\left(0\in {\mathbb{N}}_0\wedge 1\in {\mathbb{N}}_0\right)\to \left(\exists n\in \left\{0,1\right\}A\left(R{\uparrow }_{r}n\right)B\leftrightarrow \left(A\left(R{\uparrow }_{r}0\right)B\vee A\left(R{\uparrow }_{r}1\right)B\right)\right)$$
14	3 4 13	mp2an	$$⊢\exists n\in \left\{0,1\right\}A\left(R{\uparrow }_{r}n\right)B\leftrightarrow \left(A\left(R{\uparrow }_{r}0\right)B\vee A\left(R{\uparrow }_{r}1\right)B\right)$$
15	8 14	bitrdi	$$⊢\phi \to \left(A\mathrm{r*}\left(R\right)B\leftrightarrow \left(A\left(R{\uparrow }_{r}0\right)B\vee A\left(R{\uparrow }_{r}1\right)B\right)\right)$$