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 ⊢ ( 𝜑 → 𝑅 ∈ V )
Assertion brfvrcld2 ( 𝜑 → ( 𝐴 ( r* ‘ 𝑅 ) 𝐵 ↔ ( ( 𝐴 ∈ ( dom 𝑅 ∪ ran 𝑅 ) ∧ 𝐵 ∈ ( dom 𝑅 ∪ ran 𝑅 ) ∧ 𝐴 = 𝐵 ) ∨ 𝐴 𝑅 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 brfvrcld2.r ⊢ ( 𝜑 → 𝑅 ∈ V )
2 1 brfvrcld ⊢ ( 𝜑 → ( 𝐴 ( r* ‘ 𝑅 ) 𝐵 ↔ ( 𝐴 ( 𝑅 ↑𝑟 0 ) 𝐵 ∨ 𝐴 ( 𝑅 ↑𝑟 1 ) 𝐵 ) ) )
3 relexp0g ⊢ ( 𝑅 ∈ V → ( 𝑅 ↑𝑟 0 ) = ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) )
4 1 3 syl ⊢ ( 𝜑 → ( 𝑅 ↑𝑟 0 ) = ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) )
5 4 breqd ⊢ ( 𝜑 → ( 𝐴 ( 𝑅 ↑𝑟 0 ) 𝐵 ↔ 𝐴 ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) 𝐵 ) )
6 relres ⊢ Rel ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) )
7 6 releldmi ⊢ ( 𝐴 ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) 𝐵 → 𝐴 ∈ dom ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) )
8 6 relelrni ⊢ ( 𝐴 ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) 𝐵 → 𝐵 ∈ ran ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) )
9 dmresi ⊢ dom ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) = ( dom 𝑅 ∪ ran 𝑅 )
10 9 eleq2i ⊢ ( 𝐴 ∈ dom ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ↔ 𝐴 ∈ ( dom 𝑅 ∪ ran 𝑅 ) )
11 10 biimpi ⊢ ( 𝐴 ∈ dom ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) → 𝐴 ∈ ( dom 𝑅 ∪ ran 𝑅 ) )
12 rnresi ⊢ ran ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) = ( dom 𝑅 ∪ ran 𝑅 )
13 12 eleq2i ⊢ ( 𝐵 ∈ ran ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ↔ 𝐵 ∈ ( dom 𝑅 ∪ ran 𝑅 ) )
14 13 biimpi ⊢ ( 𝐵 ∈ ran ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) → 𝐵 ∈ ( dom 𝑅 ∪ ran 𝑅 ) )
15 11 14 anim12i ⊢ ( ( 𝐴 ∈ dom ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ∧ 𝐵 ∈ ran ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ) → ( 𝐴 ∈ ( dom 𝑅 ∪ ran 𝑅 ) ∧ 𝐵 ∈ ( dom 𝑅 ∪ ran 𝑅 ) ) )
16 7 8 15 syl2anc ⊢ ( 𝐴 ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) 𝐵 → ( 𝐴 ∈ ( dom 𝑅 ∪ ran 𝑅 ) ∧ 𝐵 ∈ ( dom 𝑅 ∪ ran 𝑅 ) ) )
17 resieq ⊢ ( ( 𝐴 ∈ ( dom 𝑅 ∪ ran 𝑅 ) ∧ 𝐵 ∈ ( dom 𝑅 ∪ ran 𝑅 ) ) → ( 𝐴 ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) 𝐵 ↔ 𝐴 = 𝐵 ) )
18 16 17 biadanii ⊢ ( 𝐴 ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) 𝐵 ↔ ( ( 𝐴 ∈ ( dom 𝑅 ∪ ran 𝑅 ) ∧ 𝐵 ∈ ( dom 𝑅 ∪ ran 𝑅 ) ) ∧ 𝐴 = 𝐵 ) )
19 df-3an ⊢ ( ( 𝐴 ∈ ( dom 𝑅 ∪ ran 𝑅 ) ∧ 𝐵 ∈ ( dom 𝑅 ∪ ran 𝑅 ) ∧ 𝐴 = 𝐵 ) ↔ ( ( 𝐴 ∈ ( dom 𝑅 ∪ ran 𝑅 ) ∧ 𝐵 ∈ ( dom 𝑅 ∪ ran 𝑅 ) ) ∧ 𝐴 = 𝐵 ) )
20 18 19 bitr4i ⊢ ( 𝐴 ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) 𝐵 ↔ ( 𝐴 ∈ ( dom 𝑅 ∪ ran 𝑅 ) ∧ 𝐵 ∈ ( dom 𝑅 ∪ ran 𝑅 ) ∧ 𝐴 = 𝐵 ) )
21 5 20 bitrdi ⊢ ( 𝜑 → ( 𝐴 ( 𝑅 ↑𝑟 0 ) 𝐵 ↔ ( 𝐴 ∈ ( dom 𝑅 ∪ ran 𝑅 ) ∧ 𝐵 ∈ ( dom 𝑅 ∪ ran 𝑅 ) ∧ 𝐴 = 𝐵 ) ) )
22 1 relexp1d ⊢ ( 𝜑 → ( 𝑅 ↑𝑟 1 ) = 𝑅 )
23 22 breqd ⊢ ( 𝜑 → ( 𝐴 ( 𝑅 ↑𝑟 1 ) 𝐵 ↔ 𝐴 𝑅 𝐵 ) )
24 21 23 orbi12d ⊢ ( 𝜑 → ( ( 𝐴 ( 𝑅 ↑𝑟 0 ) 𝐵 ∨ 𝐴 ( 𝑅 ↑𝑟 1 ) 𝐵 ) ↔ ( ( 𝐴 ∈ ( dom 𝑅 ∪ ran 𝑅 ) ∧ 𝐵 ∈ ( dom 𝑅 ∪ ran 𝑅 ) ∧ 𝐴 = 𝐵 ) ∨ 𝐴 𝑅 𝐵 ) ) )
25 2 24 bitrd ⊢ ( 𝜑 → ( 𝐴 ( r* ‘ 𝑅 ) 𝐵 ↔ ( ( 𝐴 ∈ ( dom 𝑅 ∪ ran 𝑅 ) ∧ 𝐵 ∈ ( dom 𝑅 ∪ ran 𝑅 ) ∧ 𝐴 = 𝐵 ) ∨ 𝐴 𝑅 𝐵 ) ) )