Metamath Proof Explorer

Theorem brfvrcld2

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

Ref Expression
Hypothesis brfvrcld2.r ⊢φ→R∈V
Assertion brfvrcld2 ⊢φ→Ar*⁡RB↔A∈dom⁡R∪ran⁡R∧B∈dom⁡R∪ran⁡R∧A=B∨ARB

Proof

Step Hyp Ref Expression
1 brfvrcld2.r ⊢φ→R∈V
2 1 brfvrcld ⊢φ→Ar*⁡RB↔AR↑r0B∨AR↑r1B
3 relexp0g ⊢R∈V→R↑r0=I↾dom⁡R∪ran⁡R
4 1 3 syl ⊢φ→R↑r0=I↾dom⁡R∪ran⁡R
5 4 breqd ⊢φ→AR↑r0B↔AI↾dom⁡R∪ran⁡RB
6 relres ⊢Rel⁡I↾dom⁡R∪ran⁡R
7 6 releldmi ⊢AI↾dom⁡R∪ran⁡RB→A∈dom⁡I↾dom⁡R∪ran⁡R
8 6 relelrni ⊢AI↾dom⁡R∪ran⁡RB→B∈ran⁡I↾dom⁡R∪ran⁡R
9 dmresi ⊢dom⁡I↾dom⁡R∪ran⁡R=dom⁡R∪ran⁡R
10 9 eleq2i ⊢A∈dom⁡I↾dom⁡R∪ran⁡R↔A∈dom⁡R∪ran⁡R
11 10 biimpi ⊢A∈dom⁡I↾dom⁡R∪ran⁡R→A∈dom⁡R∪ran⁡R
12 rnresi ⊢ran⁡I↾dom⁡R∪ran⁡R=dom⁡R∪ran⁡R
13 12 eleq2i ⊢B∈ran⁡I↾dom⁡R∪ran⁡R↔B∈dom⁡R∪ran⁡R
14 13 biimpi ⊢B∈ran⁡I↾dom⁡R∪ran⁡R→B∈dom⁡R∪ran⁡R
15 11 14 anim12i ⊢A∈dom⁡I↾dom⁡R∪ran⁡R∧B∈ran⁡I↾dom⁡R∪ran⁡R→A∈dom⁡R∪ran⁡R∧B∈dom⁡R∪ran⁡R
16 7 8 15 syl2anc ⊢AI↾dom⁡R∪ran⁡RB→A∈dom⁡R∪ran⁡R∧B∈dom⁡R∪ran⁡R
17 resieq ⊢A∈dom⁡R∪ran⁡R∧B∈dom⁡R∪ran⁡R→AI↾dom⁡R∪ran⁡RB↔A=B
18 16 17 biadanii ⊢AI↾dom⁡R∪ran⁡RB↔A∈dom⁡R∪ran⁡R∧B∈dom⁡R∪ran⁡R∧A=B
19 df-3an ⊢A∈dom⁡R∪ran⁡R∧B∈dom⁡R∪ran⁡R∧A=B↔A∈dom⁡R∪ran⁡R∧B∈dom⁡R∪ran⁡R∧A=B
20 18 19 bitr4i ⊢AI↾dom⁡R∪ran⁡RB↔A∈dom⁡R∪ran⁡R∧B∈dom⁡R∪ran⁡R∧A=B
21 5 20 bitrdi ⊢φ→AR↑r0B↔A∈dom⁡R∪ran⁡R∧B∈dom⁡R∪ran⁡R∧A=B
22 1 relexp1d ⊢φ→R↑r1=R
23 22 breqd ⊢φ→AR↑r1B↔ARB
24 21 23 orbi12d ⊢φ→AR↑r0B∨AR↑r1B↔A∈dom⁡R∪ran⁡R∧B∈dom⁡R∪ran⁡R∧A=B∨ARB
25 2 24 bitrd ⊢φ→Ar*⁡RB↔A∈dom⁡R∪ran⁡R∧B∈dom⁡R∪ran⁡R∧A=B∨ARB