Theorem dfrtrcl4

Description: Reflexive-transitive closure of a relation, expressed as the union of the zeroth power and the transitive closure. (Contributed by RP, 5-Jun-2020)

	Ref	Expression
Assertion	dfrtrcl4	⊢ t* = ( 𝑟 ∈ V ↦ ( ( 𝑟 ↑𝑟 0 ) ∪ ( t+ ‘ 𝑟 ) ) )

Proof

Step	Hyp	Ref	Expression
1		dfrtrcl3	⊢ t* = ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑟 ↑𝑟 𝑛 ) )
2		df-n0	⊢ ℕ0 = ( ℕ ∪ { 0 } )
3	2	equncomi	⊢ ℕ0 = ( { 0 } ∪ ℕ )
4		iuneq1	⊢ ( ℕ0 = ( { 0 } ∪ ℕ ) → ∪ 𝑛 ∈ ℕ0 ( 𝑟 ↑𝑟 𝑛 ) = ∪ 𝑛 ∈ ( { 0 } ∪ ℕ ) ( 𝑟 ↑𝑟 𝑛 ) )
5	3 4	ax-mp	⊢ ∪ 𝑛 ∈ ℕ0 ( 𝑟 ↑𝑟 𝑛 ) = ∪ 𝑛 ∈ ( { 0 } ∪ ℕ ) ( 𝑟 ↑𝑟 𝑛 )
6		iunxun	⊢ ∪ 𝑛 ∈ ( { 0 } ∪ ℕ ) ( 𝑟 ↑𝑟 𝑛 ) = ( ∪ 𝑛 ∈ { 0 } ( 𝑟 ↑𝑟 𝑛 ) ∪ ∪ 𝑛 ∈ ℕ ( 𝑟 ↑𝑟 𝑛 ) )
7	5 6	eqtri	⊢ ∪ 𝑛 ∈ ℕ0 ( 𝑟 ↑𝑟 𝑛 ) = ( ∪ 𝑛 ∈ { 0 } ( 𝑟 ↑𝑟 𝑛 ) ∪ ∪ 𝑛 ∈ ℕ ( 𝑟 ↑𝑟 𝑛 ) )
8		c0ex	⊢ 0 ∈ V
9		oveq2	⊢ ( 𝑛 = 0 → ( 𝑟 ↑𝑟 𝑛 ) = ( 𝑟 ↑𝑟 0 ) )
10	8 9	iunxsn	⊢ ∪ 𝑛 ∈ { 0 } ( 𝑟 ↑𝑟 𝑛 ) = ( 𝑟 ↑𝑟 0 )
11	10	a1i	⊢ ( 𝑟 ∈ V → ∪ 𝑛 ∈ { 0 } ( 𝑟 ↑𝑟 𝑛 ) = ( 𝑟 ↑𝑟 0 ) )
12		oveq1	⊢ ( 𝑥 = 𝑟 → ( 𝑥 ↑𝑟 𝑛 ) = ( 𝑟 ↑𝑟 𝑛 ) )
13	12	iuneq2d	⊢ ( 𝑥 = 𝑟 → ∪ 𝑛 ∈ ℕ ( 𝑥 ↑𝑟 𝑛 ) = ∪ 𝑛 ∈ ℕ ( 𝑟 ↑𝑟 𝑛 ) )
14		dftrcl3	⊢ t+ = ( 𝑥 ∈ V ↦ ∪ 𝑛 ∈ ℕ ( 𝑥 ↑𝑟 𝑛 ) )
15		nnex	⊢ ℕ ∈ V
16		ovex	⊢ ( 𝑟 ↑𝑟 𝑛 ) ∈ V
17	15 16	iunex	⊢ ∪ 𝑛 ∈ ℕ ( 𝑟 ↑𝑟 𝑛 ) ∈ V
18	13 14 17	fvmpt	⊢ ( 𝑟 ∈ V → ( t+ ‘ 𝑟 ) = ∪ 𝑛 ∈ ℕ ( 𝑟 ↑𝑟 𝑛 ) )
19	18	eqcomd	⊢ ( 𝑟 ∈ V → ∪ 𝑛 ∈ ℕ ( 𝑟 ↑𝑟 𝑛 ) = ( t+ ‘ 𝑟 ) )
20	11 19	uneq12d	⊢ ( 𝑟 ∈ V → ( ∪ 𝑛 ∈ { 0 } ( 𝑟 ↑𝑟 𝑛 ) ∪ ∪ 𝑛 ∈ ℕ ( 𝑟 ↑𝑟 𝑛 ) ) = ( ( 𝑟 ↑𝑟 0 ) ∪ ( t+ ‘ 𝑟 ) ) )
21	7 20	syl5eq	⊢ ( 𝑟 ∈ V → ∪ 𝑛 ∈ ℕ0 ( 𝑟 ↑𝑟 𝑛 ) = ( ( 𝑟 ↑𝑟 0 ) ∪ ( t+ ‘ 𝑟 ) ) )
22	21	mpteq2ia	⊢ ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑟 ↑𝑟 𝑛 ) ) = ( 𝑟 ∈ V ↦ ( ( 𝑟 ↑𝑟 0 ) ∪ ( t+ ‘ 𝑟 ) ) )
23	1 22	eqtri	⊢ t* = ( 𝑟 ∈ V ↦ ( ( 𝑟 ↑𝑟 0 ) ∪ ( t+ ‘ 𝑟 ) ) )