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	|- ( ph -> R e. _V )
Assertion	brfvrcld	|- ( ph -> ( A ( r* ` R ) B <-> ( A ( R ^r 0 ) B \/ A ( R ^r 1 ) B ) ) )

Proof

Step	Hyp	Ref	Expression
1		brfvrcld.r	|- ( ph -> R e. _V )
2		dfrcl4	|- r* = ( r e. _V |-> U_ n e. { 0 , 1 } ( r ^r n ) )
3		0nn0	|- 0 e. NN0
4		1nn0	|- 1 e. NN0
5		prssi	|- ( ( 0 e. NN0 /\ 1 e. NN0 ) -> { 0 , 1 } C_ NN0 )
6	3 4 5	mp2an	|- { 0 , 1 } C_ NN0
7	6	a1i	|- ( ph -> { 0 , 1 } C_ NN0 )
8	2 1 7	brmptiunrelexpd	|- ( ph -> ( A ( r* ` R ) B <-> E. n e. { 0 , 1 } A ( R ^r n ) B ) )
9		oveq2	|- ( n = 0 -> ( R ^r n ) = ( R ^r 0 ) )
10	9	breqd	|- ( n = 0 -> ( A ( R ^r n ) B <-> A ( R ^r 0 ) B ) )
11		oveq2	|- ( n = 1 -> ( R ^r n ) = ( R ^r 1 ) )
12	11	breqd	|- ( n = 1 -> ( A ( R ^r n ) B <-> A ( R ^r 1 ) B ) )
13	10 12	rexprg	|- ( ( 0 e. NN0 /\ 1 e. NN0 ) -> ( E. n e. { 0 , 1 } A ( R ^r n ) B <-> ( A ( R ^r 0 ) B \/ A ( R ^r 1 ) B ) ) )
14	3 4 13	mp2an	|- ( E. n e. { 0 , 1 } A ( R ^r n ) B <-> ( A ( R ^r 0 ) B \/ A ( R ^r 1 ) B ) )
15	8 14	bitrdi	|- ( ph -> ( A ( r* ` R ) B <-> ( A ( R ^r 0 ) B \/ A ( R ^r 1 ) B ) ) )