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 φ R V
Assertion brfvrcld φ A r* R B A R r 0 B A R r 1 B

Proof

Step Hyp Ref Expression
1 brfvrcld.r φ R V
2 dfrcl4 r* = r V n 0 1 r r n
3 0nn0 0 0
4 1nn0 1 0
5 prssi 0 0 1 0 0 1 0
6 3 4 5 mp2an 0 1 0
7 6 a1i φ 0 1 0
8 2 1 7 brmptiunrelexpd φ A r* R B n 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 0 1 0 n 0 1 A R r n B A R r 0 B A R r 1 B
14 3 4 13 mp2an n 0 1 A R r n B A R r 0 B A R r 1 B
15 8 14 bitrdi φ A r* R B A R r 0 B A R r 1 B