Theorem rtrclreclem1

Description: The reflexive, transitive closure is indeed a closure. (Contributed by Drahflow, 12-Nov-2015) (Revised by RP, 30-May-2020) (Revised by AV, 12-Jul-2024)

	Ref	Expression
Hypothesis	rtrclreclem1.1	⊢ ( 𝜑 → 𝑅 ∈ 𝑉 )
Assertion	rtrclreclem1	⊢ ( 𝜑 → 𝑅 ⊆ ( t*rec ‘ 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		rtrclreclem1.1	⊢ ( 𝜑 → 𝑅 ∈ 𝑉 )
2		1nn0	⊢ 1 ∈ ℕ0
3		ssidd	⊢ ( 𝜑 → 𝑅 ⊆ 𝑅 )
4	1	relexp1d	⊢ ( 𝜑 → ( 𝑅 ↑𝑟 1 ) = 𝑅 )
5	3 4	sseqtrrd	⊢ ( 𝜑 → 𝑅 ⊆ ( 𝑅 ↑𝑟 1 ) )
6		oveq2	⊢ ( 𝑛 = 1 → ( 𝑅 ↑𝑟 𝑛 ) = ( 𝑅 ↑𝑟 1 ) )
7	6	sseq2d	⊢ ( 𝑛 = 1 → ( 𝑅 ⊆ ( 𝑅 ↑𝑟 𝑛 ) ↔ 𝑅 ⊆ ( 𝑅 ↑𝑟 1 ) ) )
8	7	rspcev	⊢ ( ( 1 ∈ ℕ0 ∧ 𝑅 ⊆ ( 𝑅 ↑𝑟 1 ) ) → ∃ 𝑛 ∈ ℕ0 𝑅 ⊆ ( 𝑅 ↑𝑟 𝑛 ) )
9	2 5 8	sylancr	⊢ ( 𝜑 → ∃ 𝑛 ∈ ℕ0 𝑅 ⊆ ( 𝑅 ↑𝑟 𝑛 ) )
10		ssiun	⊢ ( ∃ 𝑛 ∈ ℕ0 𝑅 ⊆ ( 𝑅 ↑𝑟 𝑛 ) → 𝑅 ⊆ ∪ 𝑛 ∈ ℕ0 ( 𝑅 ↑𝑟 𝑛 ) )
11	9 10	syl	⊢ ( 𝜑 → 𝑅 ⊆ ∪ 𝑛 ∈ ℕ0 ( 𝑅 ↑𝑟 𝑛 ) )
12		eqidd	⊢ ( 𝜑 → ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑟 ↑𝑟 𝑛 ) ) = ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑟 ↑𝑟 𝑛 ) ) )
13		oveq1	⊢ ( 𝑟 = 𝑅 → ( 𝑟 ↑𝑟 𝑛 ) = ( 𝑅 ↑𝑟 𝑛 ) )
14	13	iuneq2d	⊢ ( 𝑟 = 𝑅 → ∪ 𝑛 ∈ ℕ0 ( 𝑟 ↑𝑟 𝑛 ) = ∪ 𝑛 ∈ ℕ0 ( 𝑅 ↑𝑟 𝑛 ) )
15	14	adantl	⊢ ( ( 𝜑 ∧ 𝑟 = 𝑅 ) → ∪ 𝑛 ∈ ℕ0 ( 𝑟 ↑𝑟 𝑛 ) = ∪ 𝑛 ∈ ℕ0 ( 𝑅 ↑𝑟 𝑛 ) )
16	1	elexd	⊢ ( 𝜑 → 𝑅 ∈ V )
17		nn0ex	⊢ ℕ0 ∈ V
18		ovex	⊢ ( 𝑅 ↑𝑟 𝑛 ) ∈ V
19	17 18	iunex	⊢ ∪ 𝑛 ∈ ℕ0 ( 𝑅 ↑𝑟 𝑛 ) ∈ V
20	19	a1i	⊢ ( 𝜑 → ∪ 𝑛 ∈ ℕ0 ( 𝑅 ↑𝑟 𝑛 ) ∈ V )
21	12 15 16 20	fvmptd	⊢ ( 𝜑 → ( ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑟 ↑𝑟 𝑛 ) ) ‘ 𝑅 ) = ∪ 𝑛 ∈ ℕ0 ( 𝑅 ↑𝑟 𝑛 ) )
22	11 21	sseqtrrd	⊢ ( 𝜑 → 𝑅 ⊆ ( ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑟 ↑𝑟 𝑛 ) ) ‘ 𝑅 ) )
23		df-rtrclrec	⊢ t*rec = ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑟 ↑𝑟 𝑛 ) )
24		fveq1	⊢ ( t*rec = ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑟 ↑𝑟 𝑛 ) ) → ( t*rec ‘ 𝑅 ) = ( ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑟 ↑𝑟 𝑛 ) ) ‘ 𝑅 ) )
25	24	sseq2d	⊢ ( t*rec = ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑟 ↑𝑟 𝑛 ) ) → ( 𝑅 ⊆ ( t*rec ‘ 𝑅 ) ↔ 𝑅 ⊆ ( ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑟 ↑𝑟 𝑛 ) ) ‘ 𝑅 ) ) )
26	25	imbi2d	⊢ ( t*rec = ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑟 ↑𝑟 𝑛 ) ) → ( ( 𝜑 → 𝑅 ⊆ ( t*rec ‘ 𝑅 ) ) ↔ ( 𝜑 → 𝑅 ⊆ ( ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑟 ↑𝑟 𝑛 ) ) ‘ 𝑅 ) ) ) )
27	23 26	ax-mp	⊢ ( ( 𝜑 → 𝑅 ⊆ ( t*rec ‘ 𝑅 ) ) ↔ ( 𝜑 → 𝑅 ⊆ ( ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑟 ↑𝑟 𝑛 ) ) ‘ 𝑅 ) ) )
28	22 27	mpbir	⊢ ( 𝜑 → 𝑅 ⊆ ( t*rec ‘ 𝑅 ) )