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	⊢ ( 𝜑 → 𝑅 ∈ V )
Assertion	brfvrcld	⊢ ( 𝜑 → ( 𝐴 ( r* ‘ 𝑅 ) 𝐵 ↔ ( 𝐴 ( 𝑅 ↑𝑟 0 ) 𝐵 ∨ 𝐴 ( 𝑅 ↑𝑟 1 ) 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		brfvrcld.r	⊢ ( 𝜑 → 𝑅 ∈ V )
2		dfrcl4	⊢ r* = ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ { 0 , 1 } ( 𝑟 ↑𝑟 𝑛 ) )
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	⊢ ( 𝜑 → ( 𝐴 ( r* ‘ 𝑅 ) 𝐵 ↔ ∃ 𝑛 ∈ { 0 , 1 } 𝐴 ( 𝑅 ↑𝑟 𝑛 ) 𝐵 ) )
9		oveq2	⊢ ( 𝑛 = 0 → ( 𝑅 ↑𝑟 𝑛 ) = ( 𝑅 ↑𝑟 0 ) )
10	9	breqd	⊢ ( 𝑛 = 0 → ( 𝐴 ( 𝑅 ↑𝑟 𝑛 ) 𝐵 ↔ 𝐴 ( 𝑅 ↑𝑟 0 ) 𝐵 ) )
11		oveq2	⊢ ( 𝑛 = 1 → ( 𝑅 ↑𝑟 𝑛 ) = ( 𝑅 ↑𝑟 1 ) )
12	11	breqd	⊢ ( 𝑛 = 1 → ( 𝐴 ( 𝑅 ↑𝑟 𝑛 ) 𝐵 ↔ 𝐴 ( 𝑅 ↑𝑟 1 ) 𝐵 ) )
13	10 12	rexprg	⊢ ( ( 0 ∈ ℕ0 ∧ 1 ∈ ℕ0 ) → ( ∃ 𝑛 ∈ { 0 , 1 } 𝐴 ( 𝑅 ↑𝑟 𝑛 ) 𝐵 ↔ ( 𝐴 ( 𝑅 ↑𝑟 0 ) 𝐵 ∨ 𝐴 ( 𝑅 ↑𝑟 1 ) 𝐵 ) ) )
14	3 4 13	mp2an	⊢ ( ∃ 𝑛 ∈ { 0 , 1 } 𝐴 ( 𝑅 ↑𝑟 𝑛 ) 𝐵 ↔ ( 𝐴 ( 𝑅 ↑𝑟 0 ) 𝐵 ∨ 𝐴 ( 𝑅 ↑𝑟 1 ) 𝐵 ) )
15	8 14	bitrdi	⊢ ( 𝜑 → ( 𝐴 ( r* ‘ 𝑅 ) 𝐵 ↔ ( 𝐴 ( 𝑅 ↑𝑟 0 ) 𝐵 ∨ 𝐴 ( 𝑅 ↑𝑟 1 ) 𝐵 ) ) )