Metamath Proof Explorer

Theorem dfrtrcl2

Description: The two definitions t* and t*rec of the reflexive, transitive closure coincide if R is indeed a relation. (Contributed by Drahflow, 12-Nov-2015) (Revised by RP, 30-May-2020) (Revised by AV, 13-Jul-2024)

Ref Expression
Hypothesis dfrtrcl2.1 ⊢ ( 𝜑 → Rel 𝑅 )
Assertion dfrtrcl2 ( 𝜑 → ( t* ‘ 𝑅 ) = ( t*rec ‘ 𝑅 ) )

Proof

Step Hyp Ref Expression
1 dfrtrcl2.1 ⊢ ( 𝜑 → Rel 𝑅 )
2 eqidd ⊢ ( ( 𝜑 ∧ 𝑅 ∈ V ) → ( 𝑥 ∈ V ↦ ∩ { 𝑧 ∣ ( ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ⊆ 𝑧 ∧ 𝑥 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } ) = ( 𝑥 ∈ V ↦ ∩ { 𝑧 ∣ ( ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ⊆ 𝑧 ∧ 𝑥 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } ) )
3 dmeq ⊢ ( 𝑥 = 𝑅 → dom 𝑥 = dom 𝑅 )
4 rneq ⊢ ( 𝑥 = 𝑅 → ran 𝑥 = ran 𝑅 )
5 3 4 uneq12d ⊢ ( 𝑥 = 𝑅 → ( dom 𝑥 ∪ ran 𝑥 ) = ( dom 𝑅 ∪ ran 𝑅 ) )
6 5 reseq2d ⊢ ( 𝑥 = 𝑅 → ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) = ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) )
7 6 sseq1d ⊢ ( 𝑥 = 𝑅 → ( ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ⊆ 𝑧 ↔ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑧 ) )
8 id ⊢ ( 𝑥 = 𝑅 → 𝑥 = 𝑅 )
9 8 sseq1d ⊢ ( 𝑥 = 𝑅 → ( 𝑥 ⊆ 𝑧 ↔ 𝑅 ⊆ 𝑧 ) )
10 7 9 3anbi12d ⊢ ( 𝑥 = 𝑅 → ( ( ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ⊆ 𝑧 ∧ 𝑥 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) ↔ ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑧 ∧ 𝑅 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) ) )
11 10 abbidv ⊢ ( 𝑥 = 𝑅 → { 𝑧 ∣ ( ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ⊆ 𝑧 ∧ 𝑥 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } = { 𝑧 ∣ ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑧 ∧ 𝑅 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } )
12 11 inteqd ⊢ ( 𝑥 = 𝑅 → ∩ { 𝑧 ∣ ( ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ⊆ 𝑧 ∧ 𝑥 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } = ∩ { 𝑧 ∣ ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑧 ∧ 𝑅 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } )
13 12 adantl ⊢ ( ( ( 𝜑 ∧ 𝑅 ∈ V ) ∧ 𝑥 = 𝑅 ) → ∩ { 𝑧 ∣ ( ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ⊆ 𝑧 ∧ 𝑥 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } = ∩ { 𝑧 ∣ ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑧 ∧ 𝑅 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } )
14 simpr ⊢ ( ( 𝜑 ∧ 𝑅 ∈ V ) → 𝑅 ∈ V )
15 relfld ⊢ ( Rel 𝑅 → ∪ ∪ 𝑅 = ( dom 𝑅 ∪ ran 𝑅 ) )
16 1 15 syl ⊢ ( 𝜑 → ∪ ∪ 𝑅 = ( dom 𝑅 ∪ ran 𝑅 ) )
17 16 eqcomd ⊢ ( 𝜑 → ( dom 𝑅 ∪ ran 𝑅 ) = ∪ ∪ 𝑅 )
18 17 adantr ⊢ ( ( 𝜑 ∧ 𝑅 ∈ V ) → ( dom 𝑅 ∪ ran 𝑅 ) = ∪ ∪ 𝑅 )
19 1 adantr ⊢ ( ( 𝜑 ∧ 𝑅 ∈ V ) → Rel 𝑅 )
20 19 14 rtrclreclem2 ⊢ ( ( 𝜑 ∧ 𝑅 ∈ V ) → ( I ↾ ∪ ∪ 𝑅 ) ⊆ ( t*rec ‘ 𝑅 ) )
21 id ⊢ ( ( dom 𝑅 ∪ ran 𝑅 ) = ∪ ∪ 𝑅 → ( dom 𝑅 ∪ ran 𝑅 ) = ∪ ∪ 𝑅 )
22 21 reseq2d ⊢ ( ( dom 𝑅 ∪ ran 𝑅 ) = ∪ ∪ 𝑅 → ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) = ( I ↾ ∪ ∪ 𝑅 ) )
23 22 sseq1d ⊢ ( ( dom 𝑅 ∪ ran 𝑅 ) = ∪ ∪ 𝑅 → ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ ( t*rec ‘ 𝑅 ) ↔ ( I ↾ ∪ ∪ 𝑅 ) ⊆ ( t*rec ‘ 𝑅 ) ) )
24 20 23 imbitrrid ⊢ ( ( dom 𝑅 ∪ ran 𝑅 ) = ∪ ∪ 𝑅 → ( ( 𝜑 ∧ 𝑅 ∈ V ) → ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ ( t*rec ‘ 𝑅 ) ) )
25 18 24 mpcom ⊢ ( ( 𝜑 ∧ 𝑅 ∈ V ) → ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ ( t*rec ‘ 𝑅 ) )
26 14 rtrclreclem1 ⊢ ( ( 𝜑 ∧ 𝑅 ∈ V ) → 𝑅 ⊆ ( t*rec ‘ 𝑅 ) )
27 1 rtrclreclem3 ⊢ ( 𝜑 → ( ( t*rec ‘ 𝑅 ) ∘ ( t*rec ‘ 𝑅 ) ) ⊆ ( t*rec ‘ 𝑅 ) )
28 27 adantr ⊢ ( ( 𝜑 ∧ 𝑅 ∈ V ) → ( ( t*rec ‘ 𝑅 ) ∘ ( t*rec ‘ 𝑅 ) ) ⊆ ( t*rec ‘ 𝑅 ) )
29 fvex ⊢ ( t*rec ‘ 𝑅 ) ∈ V
30 sseq2 ⊢ ( 𝑧 = ( t*rec ‘ 𝑅 ) → ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑧 ↔ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ ( t*rec ‘ 𝑅 ) ) )
31 sseq2 ⊢ ( 𝑧 = ( t*rec ‘ 𝑅 ) → ( 𝑅 ⊆ 𝑧 ↔ 𝑅 ⊆ ( t*rec ‘ 𝑅 ) ) )
32 id ⊢ ( 𝑧 = ( t*rec ‘ 𝑅 ) → 𝑧 = ( t*rec ‘ 𝑅 ) )
33 32 32 coeq12d ⊢ ( 𝑧 = ( t*rec ‘ 𝑅 ) → ( 𝑧 ∘ 𝑧 ) = ( ( t*rec ‘ 𝑅 ) ∘ ( t*rec ‘ 𝑅 ) ) )
34 33 32 sseq12d ⊢ ( 𝑧 = ( t*rec ‘ 𝑅 ) → ( ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ↔ ( ( t*rec ‘ 𝑅 ) ∘ ( t*rec ‘ 𝑅 ) ) ⊆ ( t*rec ‘ 𝑅 ) ) )
35 30 31 34 3anbi123d ⊢ ( 𝑧 = ( t*rec ‘ 𝑅 ) → ( ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑧 ∧ 𝑅 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) ↔ ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ ( t*rec ‘ 𝑅 ) ∧ 𝑅 ⊆ ( t*rec ‘ 𝑅 ) ∧ ( ( t*rec ‘ 𝑅 ) ∘ ( t*rec ‘ 𝑅 ) ) ⊆ ( t*rec ‘ 𝑅 ) ) ) )
36 35 a1i ⊢ ( 𝜑 → ( 𝑧 = ( t*rec ‘ 𝑅 ) → ( ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑧 ∧ 𝑅 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) ↔ ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ ( t*rec ‘ 𝑅 ) ∧ 𝑅 ⊆ ( t*rec ‘ 𝑅 ) ∧ ( ( t*rec ‘ 𝑅 ) ∘ ( t*rec ‘ 𝑅 ) ) ⊆ ( t*rec ‘ 𝑅 ) ) ) ) )
37 36 alrimiv ⊢ ( 𝜑 → ∀ 𝑧 ( 𝑧 = ( t*rec ‘ 𝑅 ) → ( ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑧 ∧ 𝑅 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) ↔ ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ ( t*rec ‘ 𝑅 ) ∧ 𝑅 ⊆ ( t*rec ‘ 𝑅 ) ∧ ( ( t*rec ‘ 𝑅 ) ∘ ( t*rec ‘ 𝑅 ) ) ⊆ ( t*rec ‘ 𝑅 ) ) ) ) )
38 elabgt ⊢ ( ( ( t*rec ‘ 𝑅 ) ∈ V ∧ ∀ 𝑧 ( 𝑧 = ( t*rec ‘ 𝑅 ) → ( ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑧 ∧ 𝑅 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) ↔ ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ ( t*rec ‘ 𝑅 ) ∧ 𝑅 ⊆ ( t*rec ‘ 𝑅 ) ∧ ( ( t*rec ‘ 𝑅 ) ∘ ( t*rec ‘ 𝑅 ) ) ⊆ ( t*rec ‘ 𝑅 ) ) ) ) ) → ( ( t*rec ‘ 𝑅 ) ∈ { 𝑧 ∣ ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑧 ∧ 𝑅 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } ↔ ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ ( t*rec ‘ 𝑅 ) ∧ 𝑅 ⊆ ( t*rec ‘ 𝑅 ) ∧ ( ( t*rec ‘ 𝑅 ) ∘ ( t*rec ‘ 𝑅 ) ) ⊆ ( t*rec ‘ 𝑅 ) ) ) )
39 29 37 38 sylancr ⊢ ( 𝜑 → ( ( t*rec ‘ 𝑅 ) ∈ { 𝑧 ∣ ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑧 ∧ 𝑅 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } ↔ ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ ( t*rec ‘ 𝑅 ) ∧ 𝑅 ⊆ ( t*rec ‘ 𝑅 ) ∧ ( ( t*rec ‘ 𝑅 ) ∘ ( t*rec ‘ 𝑅 ) ) ⊆ ( t*rec ‘ 𝑅 ) ) ) )
40 39 adantr ⊢ ( ( 𝜑 ∧ 𝑅 ∈ V ) → ( ( t*rec ‘ 𝑅 ) ∈ { 𝑧 ∣ ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑧 ∧ 𝑅 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } ↔ ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ ( t*rec ‘ 𝑅 ) ∧ 𝑅 ⊆ ( t*rec ‘ 𝑅 ) ∧ ( ( t*rec ‘ 𝑅 ) ∘ ( t*rec ‘ 𝑅 ) ) ⊆ ( t*rec ‘ 𝑅 ) ) ) )
41 25 26 28 40 mpbir3and ⊢ ( ( 𝜑 ∧ 𝑅 ∈ V ) → ( t*rec ‘ 𝑅 ) ∈ { 𝑧 ∣ ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑧 ∧ 𝑅 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } )
42 41 ne0d ⊢ ( ( 𝜑 ∧ 𝑅 ∈ V ) → { 𝑧 ∣ ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑧 ∧ 𝑅 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } ≠ ∅ )
43 intex ⊢ ( { 𝑧 ∣ ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑧 ∧ 𝑅 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } ≠ ∅ ↔ ∩ { 𝑧 ∣ ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑧 ∧ 𝑅 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } ∈ V )
44 42 43 sylib ⊢ ( ( 𝜑 ∧ 𝑅 ∈ V ) → ∩ { 𝑧 ∣ ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑧 ∧ 𝑅 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } ∈ V )
45 2 13 14 44 fvmptd ⊢ ( ( 𝜑 ∧ 𝑅 ∈ V ) → ( ( 𝑥 ∈ V ↦ ∩ { 𝑧 ∣ ( ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ⊆ 𝑧 ∧ 𝑥 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } ) ‘ 𝑅 ) = ∩ { 𝑧 ∣ ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑧 ∧ 𝑅 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } )
46 intss1 ⊢ ( ( t*rec ‘ 𝑅 ) ∈ { 𝑧 ∣ ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑧 ∧ 𝑅 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } → ∩ { 𝑧 ∣ ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑧 ∧ 𝑅 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } ⊆ ( t*rec ‘ 𝑅 ) )
47 41 46 syl ⊢ ( ( 𝜑 ∧ 𝑅 ∈ V ) → ∩ { 𝑧 ∣ ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑧 ∧ 𝑅 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } ⊆ ( t*rec ‘ 𝑅 ) )
48 vex ⊢ 𝑠 ∈ V
49 sseq2 ⊢ ( 𝑧 = 𝑠 → ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑧 ↔ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ) )
50 sseq2 ⊢ ( 𝑧 = 𝑠 → ( 𝑅 ⊆ 𝑧 ↔ 𝑅 ⊆ 𝑠 ) )
51 id ⊢ ( 𝑧 = 𝑠 → 𝑧 = 𝑠 )
52 51 51 coeq12d ⊢ ( 𝑧 = 𝑠 → ( 𝑧 ∘ 𝑧 ) = ( 𝑠 ∘ 𝑠 ) )
53 52 51 sseq12d ⊢ ( 𝑧 = 𝑠 → ( ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ↔ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) )
54 49 50 53 3anbi123d ⊢ ( 𝑧 = 𝑠 → ( ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑧 ∧ 𝑅 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) ↔ ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ∧ 𝑅 ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) ) )
55 48 54 elab ⊢ ( 𝑠 ∈ { 𝑧 ∣ ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑧 ∧ 𝑅 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } ↔ ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ∧ 𝑅 ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) )
56 1 rtrclreclem4 ⊢ ( 𝜑 → ∀ 𝑠 ( ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ∧ 𝑅 ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) → ( t*rec ‘ 𝑅 ) ⊆ 𝑠 ) )
57 56 19.21bi ⊢ ( 𝜑 → ( ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑠 ∧ 𝑅 ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) → ( t*rec ‘ 𝑅 ) ⊆ 𝑠 ) )
58 55 57 biimtrid ⊢ ( 𝜑 → ( 𝑠 ∈ { 𝑧 ∣ ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑧 ∧ 𝑅 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } → ( t*rec ‘ 𝑅 ) ⊆ 𝑠 ) )
59 58 ralrimiv ⊢ ( 𝜑 → ∀ 𝑠 ∈ { 𝑧 ∣ ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑧 ∧ 𝑅 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } ( t*rec ‘ 𝑅 ) ⊆ 𝑠 )
60 ssint ⊢ ( ( t*rec ‘ 𝑅 ) ⊆ ∩ { 𝑧 ∣ ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑧 ∧ 𝑅 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } ↔ ∀ 𝑠 ∈ { 𝑧 ∣ ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑧 ∧ 𝑅 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } ( t*rec ‘ 𝑅 ) ⊆ 𝑠 )
61 59 60 sylibr ⊢ ( 𝜑 → ( t*rec ‘ 𝑅 ) ⊆ ∩ { 𝑧 ∣ ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑧 ∧ 𝑅 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } )
62 61 adantr ⊢ ( ( 𝜑 ∧ 𝑅 ∈ V ) → ( t*rec ‘ 𝑅 ) ⊆ ∩ { 𝑧 ∣ ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑧 ∧ 𝑅 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } )
63 47 62 eqssd ⊢ ( ( 𝜑 ∧ 𝑅 ∈ V ) → ∩ { 𝑧 ∣ ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑧 ∧ 𝑅 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } = ( t*rec ‘ 𝑅 ) )
64 45 63 eqtrd ⊢ ( ( 𝜑 ∧ 𝑅 ∈ V ) → ( ( 𝑥 ∈ V ↦ ∩ { 𝑧 ∣ ( ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ⊆ 𝑧 ∧ 𝑥 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } ) ‘ 𝑅 ) = ( t*rec ‘ 𝑅 ) )
65 df-rtrcl ⊢ t* = ( 𝑥 ∈ V ↦ ∩ { 𝑧 ∣ ( ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ⊆ 𝑧 ∧ 𝑥 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } )
66 fveq1 ⊢ ( t* = ( 𝑥 ∈ V ↦ ∩ { 𝑧 ∣ ( ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ⊆ 𝑧 ∧ 𝑥 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } ) → ( t* ‘ 𝑅 ) = ( ( 𝑥 ∈ V ↦ ∩ { 𝑧 ∣ ( ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ⊆ 𝑧 ∧ 𝑥 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } ) ‘ 𝑅 ) )
67 66 eqeq1d ⊢ ( t* = ( 𝑥 ∈ V ↦ ∩ { 𝑧 ∣ ( ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ⊆ 𝑧 ∧ 𝑥 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } ) → ( ( t* ‘ 𝑅 ) = ( t*rec ‘ 𝑅 ) ↔ ( ( 𝑥 ∈ V ↦ ∩ { 𝑧 ∣ ( ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ⊆ 𝑧 ∧ 𝑥 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } ) ‘ 𝑅 ) = ( t*rec ‘ 𝑅 ) ) )
68 67 imbi2d ⊢ ( t* = ( 𝑥 ∈ V ↦ ∩ { 𝑧 ∣ ( ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ⊆ 𝑧 ∧ 𝑥 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } ) → ( ( ( 𝜑 ∧ 𝑅 ∈ V ) → ( t* ‘ 𝑅 ) = ( t*rec ‘ 𝑅 ) ) ↔ ( ( 𝜑 ∧ 𝑅 ∈ V ) → ( ( 𝑥 ∈ V ↦ ∩ { 𝑧 ∣ ( ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ⊆ 𝑧 ∧ 𝑥 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } ) ‘ 𝑅 ) = ( t*rec ‘ 𝑅 ) ) ) )
69 65 68 ax-mp ⊢ ( ( ( 𝜑 ∧ 𝑅 ∈ V ) → ( t* ‘ 𝑅 ) = ( t*rec ‘ 𝑅 ) ) ↔ ( ( 𝜑 ∧ 𝑅 ∈ V ) → ( ( 𝑥 ∈ V ↦ ∩ { 𝑧 ∣ ( ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ⊆ 𝑧 ∧ 𝑥 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } ) ‘ 𝑅 ) = ( t*rec ‘ 𝑅 ) ) )
70 64 69 mpbir ⊢ ( ( 𝜑 ∧ 𝑅 ∈ V ) → ( t* ‘ 𝑅 ) = ( t*rec ‘ 𝑅 ) )
71 70 ex ⊢ ( 𝜑 → ( 𝑅 ∈ V → ( t* ‘ 𝑅 ) = ( t*rec ‘ 𝑅 ) ) )
72 fvprc ⊢ ( ¬ 𝑅 ∈ V → ( t* ‘ 𝑅 ) = ∅ )
73 fvprc ⊢ ( ¬ 𝑅 ∈ V → ( t*rec ‘ 𝑅 ) = ∅ )
74 73 eqcomd ⊢ ( ¬ 𝑅 ∈ V → ∅ = ( t*rec ‘ 𝑅 ) )
75 72 74 eqtrd ⊢ ( ¬ 𝑅 ∈ V → ( t* ‘ 𝑅 ) = ( t*rec ‘ 𝑅 ) )
76 71 75 pm2.61d1 ⊢ ( 𝜑 → ( t* ‘ 𝑅 ) = ( t*rec ‘ 𝑅 ) )