Theorem dfrcl4

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

	Ref	Expression
Assertion	dfrcl4	⊢ r* = ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ { 0 , 1 } ( 𝑟 ↑𝑟 𝑛 ) )

Proof

Step	Hyp	Ref	Expression
1		dfrcl3	⊢ r* = ( 𝑟 ∈ V ↦ ( ( 𝑟 ↑𝑟 0 ) ∪ ( 𝑟 ↑𝑟 1 ) ) )
2		df-pr	⊢ { 0 , 1 } = ( { 0 } ∪ { 1 } )
3		iuneq1	⊢ ( { 0 , 1 } = ( { 0 } ∪ { 1 } ) → ∪ 𝑛 ∈ { 0 , 1 } ( 𝑟 ↑𝑟 𝑛 ) = ∪ 𝑛 ∈ ( { 0 } ∪ { 1 } ) ( 𝑟 ↑𝑟 𝑛 ) )
4	2 3	ax-mp	⊢ ∪ 𝑛 ∈ { 0 , 1 } ( 𝑟 ↑𝑟 𝑛 ) = ∪ 𝑛 ∈ ( { 0 } ∪ { 1 } ) ( 𝑟 ↑𝑟 𝑛 )
5		iunxun	⊢ ∪ 𝑛 ∈ ( { 0 } ∪ { 1 } ) ( 𝑟 ↑𝑟 𝑛 ) = ( ∪ 𝑛 ∈ { 0 } ( 𝑟 ↑𝑟 𝑛 ) ∪ ∪ 𝑛 ∈ { 1 } ( 𝑟 ↑𝑟 𝑛 ) )
6		c0ex	⊢ 0 ∈ V
7		oveq2	⊢ ( 𝑛 = 0 → ( 𝑟 ↑𝑟 𝑛 ) = ( 𝑟 ↑𝑟 0 ) )
8	6 7	iunxsn	⊢ ∪ 𝑛 ∈ { 0 } ( 𝑟 ↑𝑟 𝑛 ) = ( 𝑟 ↑𝑟 0 )
9		1ex	⊢ 1 ∈ V
10		oveq2	⊢ ( 𝑛 = 1 → ( 𝑟 ↑𝑟 𝑛 ) = ( 𝑟 ↑𝑟 1 ) )
11	9 10	iunxsn	⊢ ∪ 𝑛 ∈ { 1 } ( 𝑟 ↑𝑟 𝑛 ) = ( 𝑟 ↑𝑟 1 )
12	8 11	uneq12i	⊢ ( ∪ 𝑛 ∈ { 0 } ( 𝑟 ↑𝑟 𝑛 ) ∪ ∪ 𝑛 ∈ { 1 } ( 𝑟 ↑𝑟 𝑛 ) ) = ( ( 𝑟 ↑𝑟 0 ) ∪ ( 𝑟 ↑𝑟 1 ) )
13	4 5 12	3eqtri	⊢ ∪ 𝑛 ∈ { 0 , 1 } ( 𝑟 ↑𝑟 𝑛 ) = ( ( 𝑟 ↑𝑟 0 ) ∪ ( 𝑟 ↑𝑟 1 ) )
14	13	mpteq2i	⊢ ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ { 0 , 1 } ( 𝑟 ↑𝑟 𝑛 ) ) = ( 𝑟 ∈ V ↦ ( ( 𝑟 ↑𝑟 0 ) ∪ ( 𝑟 ↑𝑟 1 ) ) )
15	1 14	eqtr4i	⊢ r* = ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ { 0 , 1 } ( 𝑟 ↑𝑟 𝑛 ) )