Theorem dfrcl3

Description: Reflexive closure of a relation as union of powers of the relation. (Contributed by RP, 6-Jun-2020)

	Ref	Expression
Assertion	dfrcl3	⊢ r* = ( 𝑥 ∈ V ↦ ( ( 𝑥 ↑𝑟 0 ) ∪ ( 𝑥 ↑𝑟 1 ) ) )

Proof

Step	Hyp	Ref	Expression
1		dfrcl2	⊢ r* = ( 𝑥 ∈ V ↦ ( ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ∪ 𝑥 ) )
2		relexp0g	⊢ ( 𝑥 ∈ V → ( 𝑥 ↑𝑟 0 ) = ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) )
3		relexp1g	⊢ ( 𝑥 ∈ V → ( 𝑥 ↑𝑟 1 ) = 𝑥 )
4	2 3	uneq12d	⊢ ( 𝑥 ∈ V → ( ( 𝑥 ↑𝑟 0 ) ∪ ( 𝑥 ↑𝑟 1 ) ) = ( ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ∪ 𝑥 ) )
5	4	mpteq2ia	⊢ ( 𝑥 ∈ V ↦ ( ( 𝑥 ↑𝑟 0 ) ∪ ( 𝑥 ↑𝑟 1 ) ) ) = ( 𝑥 ∈ V ↦ ( ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ∪ 𝑥 ) )
6	1 5	eqtr4i	⊢ r* = ( 𝑥 ∈ V ↦ ( ( 𝑥 ↑𝑟 0 ) ∪ ( 𝑥 ↑𝑟 1 ) ) )