| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | eqidd 2737 | . . . . . 6
⊢ ((𝜑 ∧ 𝑅 ∈ V) → (𝑥 ∈ V ↦ ∩ {𝑧
∣ (( I ↾ (dom 𝑥
∪ ran 𝑥)) ⊆ 𝑧 ∧ 𝑥 ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)}) = (𝑥 ∈ V ↦ ∩ {𝑧
∣ (( I ↾ (dom 𝑥
∪ ran 𝑥)) ⊆ 𝑧 ∧ 𝑥 ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)})) | 
| 2 |  | dmeq 5913 | . . . . . . . . . . . . 13
⊢ (𝑥 = 𝑅 → dom 𝑥 = dom 𝑅) | 
| 3 |  | rneq 5946 | . . . . . . . . . . . . 13
⊢ (𝑥 = 𝑅 → ran 𝑥 = ran 𝑅) | 
| 4 | 2, 3 | uneq12d 4168 | . . . . . . . . . . . 12
⊢ (𝑥 = 𝑅 → (dom 𝑥 ∪ ran 𝑥) = (dom 𝑅 ∪ ran 𝑅)) | 
| 5 | 4 | reseq2d 5996 | . . . . . . . . . . 11
⊢ (𝑥 = 𝑅 → ( I ↾ (dom 𝑥 ∪ ran 𝑥)) = ( I ↾ (dom 𝑅 ∪ ran 𝑅))) | 
| 6 | 5 | sseq1d 4014 | . . . . . . . . . 10
⊢ (𝑥 = 𝑅 → (( I ↾ (dom 𝑥 ∪ ran 𝑥)) ⊆ 𝑧 ↔ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑧)) | 
| 7 |  | id 22 | . . . . . . . . . . 11
⊢ (𝑥 = 𝑅 → 𝑥 = 𝑅) | 
| 8 | 7 | sseq1d 4014 | . . . . . . . . . 10
⊢ (𝑥 = 𝑅 → (𝑥 ⊆ 𝑧 ↔ 𝑅 ⊆ 𝑧)) | 
| 9 | 6, 8 | 3anbi12d 1438 | . . . . . . . . 9
⊢ (𝑥 = 𝑅 → ((( I ↾ (dom 𝑥 ∪ ran 𝑥)) ⊆ 𝑧 ∧ 𝑥 ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧) ↔ (( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑧 ∧ 𝑅 ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧))) | 
| 10 | 9 | abbidv 2807 | . . . . . . . 8
⊢ (𝑥 = 𝑅 → {𝑧 ∣ (( I ↾ (dom 𝑥 ∪ ran 𝑥)) ⊆ 𝑧 ∧ 𝑥 ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)} = {𝑧 ∣ (( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑧 ∧ 𝑅 ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)}) | 
| 11 | 10 | inteqd 4950 | . . . . . . 7
⊢ (𝑥 = 𝑅 → ∩ {𝑧 ∣ (( I ↾ (dom 𝑥 ∪ ran 𝑥)) ⊆ 𝑧 ∧ 𝑥 ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)} = ∩ {𝑧 ∣ (( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑧 ∧ 𝑅 ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)}) | 
| 12 | 11 | adantl 481 | . . . . . 6
⊢ (((𝜑 ∧ 𝑅 ∈ V) ∧ 𝑥 = 𝑅) → ∩ {𝑧 ∣ (( I ↾ (dom 𝑥 ∪ ran 𝑥)) ⊆ 𝑧 ∧ 𝑥 ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)} = ∩ {𝑧 ∣ (( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑧 ∧ 𝑅 ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)}) | 
| 13 |  | simpr 484 | . . . . . 6
⊢ ((𝜑 ∧ 𝑅 ∈ V) → 𝑅 ∈ V) | 
| 14 |  | dfrtrcl2.1 | . . . . . . . . . . . . 13
⊢ (𝜑 → Rel 𝑅) | 
| 15 |  | relfld 6294 | . . . . . . . . . . . . 13
⊢ (Rel
𝑅 → ∪ ∪ 𝑅 = (dom 𝑅 ∪ ran 𝑅)) | 
| 16 | 14, 15 | syl 17 | . . . . . . . . . . . 12
⊢ (𝜑 → ∪ ∪ 𝑅 = (dom 𝑅 ∪ ran 𝑅)) | 
| 17 | 16 | eqcomd 2742 | . . . . . . . . . . 11
⊢ (𝜑 → (dom 𝑅 ∪ ran 𝑅) = ∪ ∪ 𝑅) | 
| 18 | 17 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑅 ∈ V) → (dom 𝑅 ∪ ran 𝑅) = ∪ ∪ 𝑅) | 
| 19 | 14 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑅 ∈ V) → Rel 𝑅) | 
| 20 | 19, 13 | rtrclreclem2 15099 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑅 ∈ V) → ( I ↾ ∪ ∪ 𝑅) ⊆ (t*rec‘𝑅)) | 
| 21 |  | id 22 | . . . . . . . . . . . . 13
⊢ ((dom
𝑅 ∪ ran 𝑅) = ∪
∪ 𝑅 → (dom 𝑅 ∪ ran 𝑅) = ∪ ∪ 𝑅) | 
| 22 | 21 | reseq2d 5996 | . . . . . . . . . . . 12
⊢ ((dom
𝑅 ∪ ran 𝑅) = ∪
∪ 𝑅 → ( I ↾ (dom 𝑅 ∪ ran 𝑅)) = ( I ↾ ∪ ∪ 𝑅)) | 
| 23 | 22 | sseq1d 4014 | . . . . . . . . . . 11
⊢ ((dom
𝑅 ∪ ran 𝑅) = ∪
∪ 𝑅 → (( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ (t*rec‘𝑅) ↔ ( I ↾ ∪ ∪ 𝑅) ⊆ (t*rec‘𝑅))) | 
| 24 | 20, 23 | imbitrrid 246 | . . . . . . . . . 10
⊢ ((dom
𝑅 ∪ ran 𝑅) = ∪
∪ 𝑅 → ((𝜑 ∧ 𝑅 ∈ V) → ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ (t*rec‘𝑅))) | 
| 25 | 18, 24 | mpcom 38 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑅 ∈ V) → ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ (t*rec‘𝑅)) | 
| 26 | 13 | rtrclreclem1 15097 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑅 ∈ V) → 𝑅 ⊆ (t*rec‘𝑅)) | 
| 27 | 14 | rtrclreclem3 15100 | . . . . . . . . . 10
⊢ (𝜑 → ((t*rec‘𝑅) ∘ (t*rec‘𝑅)) ⊆ (t*rec‘𝑅)) | 
| 28 | 27 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑅 ∈ V) → ((t*rec‘𝑅) ∘ (t*rec‘𝑅)) ⊆ (t*rec‘𝑅)) | 
| 29 |  | fvex 6918 | . . . . . . . . . . 11
⊢
(t*rec‘𝑅)
∈ V | 
| 30 |  | sseq2 4009 | . . . . . . . . . . . . . 14
⊢ (𝑧 = (t*rec‘𝑅) → (( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑧 ↔ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ (t*rec‘𝑅))) | 
| 31 |  | sseq2 4009 | . . . . . . . . . . . . . 14
⊢ (𝑧 = (t*rec‘𝑅) → (𝑅 ⊆ 𝑧 ↔ 𝑅 ⊆ (t*rec‘𝑅))) | 
| 32 |  | id 22 | . . . . . . . . . . . . . . . 16
⊢ (𝑧 = (t*rec‘𝑅) → 𝑧 = (t*rec‘𝑅)) | 
| 33 | 32, 32 | coeq12d 5874 | . . . . . . . . . . . . . . 15
⊢ (𝑧 = (t*rec‘𝑅) → (𝑧 ∘ 𝑧) = ((t*rec‘𝑅) ∘ (t*rec‘𝑅))) | 
| 34 | 33, 32 | sseq12d 4016 | . . . . . . . . . . . . . 14
⊢ (𝑧 = (t*rec‘𝑅) → ((𝑧 ∘ 𝑧) ⊆ 𝑧 ↔ ((t*rec‘𝑅) ∘ (t*rec‘𝑅)) ⊆ (t*rec‘𝑅))) | 
| 35 | 30, 31, 34 | 3anbi123d 1437 | . . . . . . . . . . . . 13
⊢ (𝑧 = (t*rec‘𝑅) → ((( I ↾ (dom
𝑅 ∪ ran 𝑅)) ⊆ 𝑧 ∧ 𝑅 ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧) ↔ (( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ (t*rec‘𝑅) ∧ 𝑅 ⊆ (t*rec‘𝑅) ∧ ((t*rec‘𝑅) ∘ (t*rec‘𝑅)) ⊆ (t*rec‘𝑅)))) | 
| 36 | 35 | a1i 11 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝑧 = (t*rec‘𝑅) → ((( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑧 ∧ 𝑅 ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧) ↔ (( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ (t*rec‘𝑅) ∧ 𝑅 ⊆ (t*rec‘𝑅) ∧ ((t*rec‘𝑅) ∘ (t*rec‘𝑅)) ⊆ (t*rec‘𝑅))))) | 
| 37 | 36 | alrimiv 1926 | . . . . . . . . . . 11
⊢ (𝜑 → ∀𝑧(𝑧 = (t*rec‘𝑅) → ((( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑧 ∧ 𝑅 ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧) ↔ (( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ (t*rec‘𝑅) ∧ 𝑅 ⊆ (t*rec‘𝑅) ∧ ((t*rec‘𝑅) ∘ (t*rec‘𝑅)) ⊆ (t*rec‘𝑅))))) | 
| 38 |  | elabgt 3671 | . . . . . . . . . . 11
⊢
(((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 587 | . . . . . . . . . 10
⊢ (𝜑 → ((t*rec‘𝑅) ∈ {𝑧 ∣ (( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑧 ∧ 𝑅 ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)} ↔ (( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ (t*rec‘𝑅) ∧ 𝑅 ⊆ (t*rec‘𝑅) ∧ ((t*rec‘𝑅) ∘ (t*rec‘𝑅)) ⊆ (t*rec‘𝑅)))) | 
| 40 | 39 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑅 ∈ 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 1342 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑅 ∈ V) → (t*rec‘𝑅) ∈ {𝑧 ∣ (( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑧 ∧ 𝑅 ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)}) | 
| 42 | 41 | ne0d 4341 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑅 ∈ V) → {𝑧 ∣ (( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑧 ∧ 𝑅 ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)} ≠ ∅) | 
| 43 |  | intex 5343 | . . . . . . 7
⊢ ({𝑧 ∣ (( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑧 ∧ 𝑅 ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)} ≠ ∅ ↔ ∩ {𝑧
∣ (( I ↾ (dom 𝑅
∪ ran 𝑅)) ⊆ 𝑧 ∧ 𝑅 ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)} ∈ V) | 
| 44 | 42, 43 | sylib 218 | . . . . . 6
⊢ ((𝜑 ∧ 𝑅 ∈ V) → ∩ {𝑧
∣ (( I ↾ (dom 𝑅
∪ ran 𝑅)) ⊆ 𝑧 ∧ 𝑅 ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)} ∈ V) | 
| 45 | 1, 12, 13, 44 | fvmptd 7022 | . . . . 5
⊢ ((𝜑 ∧ 𝑅 ∈ V) → ((𝑥 ∈ V ↦ ∩ {𝑧
∣ (( I ↾ (dom 𝑥
∪ ran 𝑥)) ⊆ 𝑧 ∧ 𝑥 ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)})‘𝑅) = ∩ {𝑧 ∣ (( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑧 ∧ 𝑅 ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)}) | 
| 46 |  | intss1 4962 | . . . . . . 7
⊢
((t*rec‘𝑅)
∈ {𝑧 ∣ (( I
↾ (dom 𝑅 ∪ ran
𝑅)) ⊆ 𝑧 ∧ 𝑅 ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)} → ∩ {𝑧 ∣ (( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑧 ∧ 𝑅 ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)} ⊆ (t*rec‘𝑅)) | 
| 47 | 41, 46 | syl 17 | . . . . . 6
⊢ ((𝜑 ∧ 𝑅 ∈ V) → ∩ {𝑧
∣ (( I ↾ (dom 𝑅
∪ ran 𝑅)) ⊆ 𝑧 ∧ 𝑅 ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)} ⊆ (t*rec‘𝑅)) | 
| 48 |  | vex 3483 | . . . . . . . . . . 11
⊢ 𝑠 ∈ V | 
| 49 |  | sseq2 4009 | . . . . . . . . . . . 12
⊢ (𝑧 = 𝑠 → (( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑧 ↔ ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠)) | 
| 50 |  | sseq2 4009 | . . . . . . . . . . . 12
⊢ (𝑧 = 𝑠 → (𝑅 ⊆ 𝑧 ↔ 𝑅 ⊆ 𝑠)) | 
| 51 |  | id 22 | . . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑠 → 𝑧 = 𝑠) | 
| 52 | 51, 51 | coeq12d 5874 | . . . . . . . . . . . . 13
⊢ (𝑧 = 𝑠 → (𝑧 ∘ 𝑧) = (𝑠 ∘ 𝑠)) | 
| 53 | 52, 51 | sseq12d 4016 | . . . . . . . . . . . 12
⊢ (𝑧 = 𝑠 → ((𝑧 ∘ 𝑧) ⊆ 𝑧 ↔ (𝑠 ∘ 𝑠) ⊆ 𝑠)) | 
| 54 | 49, 50, 53 | 3anbi123d 1437 | . . . . . . . . . . 11
⊢ (𝑧 = 𝑠 → ((( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑧 ∧ 𝑅 ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧) ↔ (( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠 ∧ 𝑅 ⊆ 𝑠 ∧ (𝑠 ∘ 𝑠) ⊆ 𝑠))) | 
| 55 | 48, 54 | elab 3678 | . . . . . . . . . 10
⊢ (𝑠 ∈ {𝑧 ∣ (( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑧 ∧ 𝑅 ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)} ↔ (( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠 ∧ 𝑅 ⊆ 𝑠 ∧ (𝑠 ∘ 𝑠) ⊆ 𝑠)) | 
| 56 | 14 | rtrclreclem4 15101 | . . . . . . . . . . 11
⊢ (𝜑 → ∀𝑠((( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠 ∧ 𝑅 ⊆ 𝑠 ∧ (𝑠 ∘ 𝑠) ⊆ 𝑠) → (t*rec‘𝑅) ⊆ 𝑠)) | 
| 57 | 56 | 19.21bi 2188 | . . . . . . . . . 10
⊢ (𝜑 → ((( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠 ∧ 𝑅 ⊆ 𝑠 ∧ (𝑠 ∘ 𝑠) ⊆ 𝑠) → (t*rec‘𝑅) ⊆ 𝑠)) | 
| 58 | 55, 57 | biimtrid 242 | . . . . . . . . 9
⊢ (𝜑 → (𝑠 ∈ {𝑧 ∣ (( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑧 ∧ 𝑅 ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)} → (t*rec‘𝑅) ⊆ 𝑠)) | 
| 59 | 58 | ralrimiv 3144 | . . . . . . . 8
⊢ (𝜑 → ∀𝑠 ∈ {𝑧 ∣ (( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑧 ∧ 𝑅 ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)} (t*rec‘𝑅) ⊆ 𝑠) | 
| 60 |  | ssint 4963 | . . . . . . . 8
⊢
((t*rec‘𝑅)
⊆ ∩ {𝑧 ∣ (( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑧 ∧ 𝑅 ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)} ↔ ∀𝑠 ∈ {𝑧 ∣ (( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑧 ∧ 𝑅 ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)} (t*rec‘𝑅) ⊆ 𝑠) | 
| 61 | 59, 60 | sylibr 234 | . . . . . . 7
⊢ (𝜑 → (t*rec‘𝑅) ⊆ ∩ {𝑧
∣ (( I ↾ (dom 𝑅
∪ ran 𝑅)) ⊆ 𝑧 ∧ 𝑅 ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)}) | 
| 62 | 61 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑅 ∈ V) → (t*rec‘𝑅) ⊆ ∩ {𝑧
∣ (( I ↾ (dom 𝑅
∪ ran 𝑅)) ⊆ 𝑧 ∧ 𝑅 ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)}) | 
| 63 | 47, 62 | eqssd 4000 | . . . . 5
⊢ ((𝜑 ∧ 𝑅 ∈ V) → ∩ {𝑧
∣ (( I ↾ (dom 𝑅
∪ ran 𝑅)) ⊆ 𝑧 ∧ 𝑅 ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)} = (t*rec‘𝑅)) | 
| 64 | 45, 63 | eqtrd 2776 | . . . 4
⊢ ((𝜑 ∧ 𝑅 ∈ V) → ((𝑥 ∈ V ↦ ∩ {𝑧
∣ (( I ↾ (dom 𝑥
∪ ran 𝑥)) ⊆ 𝑧 ∧ 𝑥 ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)})‘𝑅) = (t*rec‘𝑅)) | 
| 65 |  | df-rtrcl 15028 | . . . . 5
⊢ t* =
(𝑥 ∈ V ↦ ∩ {𝑧
∣ (( I ↾ (dom 𝑥
∪ ran 𝑥)) ⊆ 𝑧 ∧ 𝑥 ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)}) | 
| 66 |  | fveq1 6904 | . . . . . . 7
⊢ (t* =
(𝑥 ∈ V ↦ ∩ {𝑧
∣ (( I ↾ (dom 𝑥
∪ ran 𝑥)) ⊆ 𝑧 ∧ 𝑥 ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)}) → (t*‘𝑅) = ((𝑥 ∈ V ↦ ∩ {𝑧
∣ (( I ↾ (dom 𝑥
∪ ran 𝑥)) ⊆ 𝑧 ∧ 𝑥 ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)})‘𝑅)) | 
| 67 | 66 | eqeq1d 2738 | . . . . . 6
⊢ (t* =
(𝑥 ∈ V ↦ ∩ {𝑧
∣ (( I ↾ (dom 𝑥
∪ ran 𝑥)) ⊆ 𝑧 ∧ 𝑥 ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)}) → ((t*‘𝑅) = (t*rec‘𝑅) ↔ ((𝑥 ∈ V ↦ ∩ {𝑧
∣ (( I ↾ (dom 𝑥
∪ ran 𝑥)) ⊆ 𝑧 ∧ 𝑥 ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)})‘𝑅) = (t*rec‘𝑅))) | 
| 68 | 67 | imbi2d 340 | . . . . 5
⊢ (t* =
(𝑥 ∈ V ↦ ∩ {𝑧
∣ (( I ↾ (dom 𝑥
∪ ran 𝑥)) ⊆ 𝑧 ∧ 𝑥 ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)}) → (((𝜑 ∧ 𝑅 ∈ V) → (t*‘𝑅) = (t*rec‘𝑅)) ↔ ((𝜑 ∧ 𝑅 ∈ V) → ((𝑥 ∈ V ↦ ∩ {𝑧
∣ (( I ↾ (dom 𝑥
∪ ran 𝑥)) ⊆ 𝑧 ∧ 𝑥 ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)})‘𝑅) = (t*rec‘𝑅)))) | 
| 69 | 65, 68 | ax-mp 5 | . . . 4
⊢ (((𝜑 ∧ 𝑅 ∈ V) → (t*‘𝑅) = (t*rec‘𝑅)) ↔ ((𝜑 ∧ 𝑅 ∈ V) → ((𝑥 ∈ V ↦ ∩ {𝑧
∣ (( I ↾ (dom 𝑥
∪ ran 𝑥)) ⊆ 𝑧 ∧ 𝑥 ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)})‘𝑅) = (t*rec‘𝑅))) | 
| 70 | 64, 69 | mpbir 231 | . . 3
⊢ ((𝜑 ∧ 𝑅 ∈ V) → (t*‘𝑅) = (t*rec‘𝑅)) | 
| 71 | 70 | ex 412 | . 2
⊢ (𝜑 → (𝑅 ∈ V → (t*‘𝑅) = (t*rec‘𝑅))) | 
| 72 |  | fvprc 6897 | . . 3
⊢ (¬
𝑅 ∈ V →
(t*‘𝑅) =
∅) | 
| 73 |  | fvprc 6897 | . . . 4
⊢ (¬
𝑅 ∈ V →
(t*rec‘𝑅) =
∅) | 
| 74 | 73 | eqcomd 2742 | . . 3
⊢ (¬
𝑅 ∈ V → ∅ =
(t*rec‘𝑅)) | 
| 75 | 72, 74 | eqtrd 2776 | . 2
⊢ (¬
𝑅 ∈ V →
(t*‘𝑅) =
(t*rec‘𝑅)) | 
| 76 | 71, 75 | pm2.61d1 180 | 1
⊢ (𝜑 → (t*‘𝑅) = (t*rec‘𝑅)) |