Metamath Proof Explorer

Theorem rtrclreclem2

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

Ref Expression
Hypotheses rtrclreclem2.1 ⊢ ( 𝜑 → Rel 𝑅 )
rtrclreclem2.2 ⊢ ( 𝜑 → 𝑅 ∈ 𝑉 )
Assertion rtrclreclem2 ( 𝜑 → ( I ↾ ∪ ∪ 𝑅 ) ⊆ ( t*rec ‘ 𝑅 ) )

Proof

Step Hyp Ref Expression
1 rtrclreclem2.1 ⊢ ( 𝜑 → Rel 𝑅 )
2 rtrclreclem2.2 ⊢ ( 𝜑 → 𝑅 ∈ 𝑉 )
3 0nn0 ⊢ 0 ∈ ℕ0
4 ssid ⊢ ( I ↾ ∪ ∪ 𝑅 ) ⊆ ( I ↾ ∪ ∪ 𝑅 )
5 1 2 relexp0d ⊢ ( 𝜑 → ( 𝑅 ↑𝑟 0 ) = ( I ↾ ∪ ∪ 𝑅 ) )
6 4 5 sseqtrrid ⊢ ( 𝜑 → ( I ↾ ∪ ∪ 𝑅 ) ⊆ ( 𝑅 ↑𝑟 0 ) )
7 oveq2 ⊢ ( 𝑛 = 0 → ( 𝑅 ↑𝑟 𝑛 ) = ( 𝑅 ↑𝑟 0 ) )
8 7 sseq2d ⊢ ( 𝑛 = 0 → ( ( I ↾ ∪ ∪ 𝑅 ) ⊆ ( 𝑅 ↑𝑟 𝑛 ) ↔ ( I ↾ ∪ ∪ 𝑅 ) ⊆ ( 𝑅 ↑𝑟 0 ) ) )
9 8 rspcev ⊢ ( ( 0 ∈ ℕ0 ∧ ( I ↾ ∪ ∪ 𝑅 ) ⊆ ( 𝑅 ↑𝑟 0 ) ) → ∃ 𝑛 ∈ ℕ0 ( I ↾ ∪ ∪ 𝑅 ) ⊆ ( 𝑅 ↑𝑟 𝑛 ) )
10 3 6 9 sylancr ⊢ ( 𝜑 → ∃ 𝑛 ∈ ℕ0 ( I ↾ ∪ ∪ 𝑅 ) ⊆ ( 𝑅 ↑𝑟 𝑛 ) )
11 ssiun ⊢ ( ∃ 𝑛 ∈ ℕ0 ( I ↾ ∪ ∪ 𝑅 ) ⊆ ( 𝑅 ↑𝑟 𝑛 ) → ( I ↾ ∪ ∪ 𝑅 ) ⊆ ∪ 𝑛 ∈ ℕ0 ( 𝑅 ↑𝑟 𝑛 ) )
12 10 11 syl ⊢ ( 𝜑 → ( I ↾ ∪ ∪ 𝑅 ) ⊆ ∪ 𝑛 ∈ ℕ0 ( 𝑅 ↑𝑟 𝑛 ) )
13 2 elexd ⊢ ( 𝜑 → 𝑅 ∈ V )
14 nn0ex ⊢ ℕ0 ∈ V
15 ovex ⊢ ( 𝑅 ↑𝑟 𝑛 ) ∈ V
16 14 15 iunex ⊢ ∪ 𝑛 ∈ ℕ0 ( 𝑅 ↑𝑟 𝑛 ) ∈ V
17 oveq1 ⊢ ( 𝑟 = 𝑅 → ( 𝑟 ↑𝑟 𝑛 ) = ( 𝑅 ↑𝑟 𝑛 ) )
18 17 iuneq2d ⊢ ( 𝑟 = 𝑅 → ∪ 𝑛 ∈ ℕ0 ( 𝑟 ↑𝑟 𝑛 ) = ∪ 𝑛 ∈ ℕ0 ( 𝑅 ↑𝑟 𝑛 ) )
19 eqid ⊢ ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑟 ↑𝑟 𝑛 ) ) = ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑟 ↑𝑟 𝑛 ) )
20 18 19 fvmptg ⊢ ( ( 𝑅 ∈ V ∧ ∪ 𝑛 ∈ ℕ0 ( 𝑅 ↑𝑟 𝑛 ) ∈ V ) → ( ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑟 ↑𝑟 𝑛 ) ) ‘ 𝑅 ) = ∪ 𝑛 ∈ ℕ0 ( 𝑅 ↑𝑟 𝑛 ) )
21 13 16 20 sylancl ⊢ ( 𝜑 → ( ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑟 ↑𝑟 𝑛 ) ) ‘ 𝑅 ) = ∪ 𝑛 ∈ ℕ0 ( 𝑅 ↑𝑟 𝑛 ) )
22 12 21 sseqtrrd ⊢ ( 𝜑 → ( I ↾ ∪ ∪ 𝑅 ) ⊆ ( ( 𝑟 ∈ 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 ( 𝑟 ↑𝑟 𝑛 ) ) → ( ( I ↾ ∪ ∪ 𝑅 ) ⊆ ( t*rec ‘ 𝑅 ) ↔ ( I ↾ ∪ ∪ 𝑅 ) ⊆ ( ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑟 ↑𝑟 𝑛 ) ) ‘ 𝑅 ) ) )
26 25 imbi2d ⊢ ( t*rec = ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑟 ↑𝑟 𝑛 ) ) → ( ( 𝜑 → ( I ↾ ∪ ∪ 𝑅 ) ⊆ ( t*rec ‘ 𝑅 ) ) ↔ ( 𝜑 → ( I ↾ ∪ ∪ 𝑅 ) ⊆ ( ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑟 ↑𝑟 𝑛 ) ) ‘ 𝑅 ) ) ) )
27 23 26 ax-mp ⊢ ( ( 𝜑 → ( I ↾ ∪ ∪ 𝑅 ) ⊆ ( t*rec ‘ 𝑅 ) ) ↔ ( 𝜑 → ( I ↾ ∪ ∪ 𝑅 ) ⊆ ( ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑟 ↑𝑟 𝑛 ) ) ‘ 𝑅 ) ) )
28 22 27 mpbir ⊢ ( 𝜑 → ( I ↾ ∪ ∪ 𝑅 ) ⊆ ( t*rec ‘ 𝑅 ) )