Description: If R is set-like over A , then the transitive closure of the restriction of R to A is set-like over A .
This theorem requires the axioms of infinity and replacement for its proof. (Contributed by Scott Fenton, 31-Oct-2024)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | ttrclse | ⊢ ( 𝑅 Se 𝐴 → t++ ( 𝑅 ↾ 𝐴 ) Se 𝐴 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | brttrcl2 | ⊢ ( 𝑦 t++ ( 𝑅 ↾ 𝐴 ) 𝑥 ↔ ∃ 𝑛 ∈ ω ∃ 𝑓 ( 𝑓 Fn suc suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑦 ∧ ( 𝑓 ‘ suc 𝑛 ) = 𝑥 ) ∧ ∀ 𝑎 ∈ suc 𝑛 ( 𝑓 ‘ 𝑎 ) ( 𝑅 ↾ 𝐴 ) ( 𝑓 ‘ suc 𝑎 ) ) ) | |
| 2 | eqid | ⊢ rec ( ( 𝑏 ∈ V ↦ ∪ 𝑤 ∈ 𝑏 Pred ( 𝑅 , 𝐴 , 𝑤 ) ) , Pred ( 𝑅 , 𝐴 , 𝑥 ) ) = rec ( ( 𝑏 ∈ V ↦ ∪ 𝑤 ∈ 𝑏 Pred ( 𝑅 , 𝐴 , 𝑤 ) ) , Pred ( 𝑅 , 𝐴 , 𝑥 ) ) | |
| 3 | 2 | ttrclselem2 | ⊢ ( ( 𝑛 ∈ ω ∧ 𝑅 Se 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( ∃ 𝑓 ( 𝑓 Fn suc suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑦 ∧ ( 𝑓 ‘ suc 𝑛 ) = 𝑥 ) ∧ ∀ 𝑎 ∈ suc 𝑛 ( 𝑓 ‘ 𝑎 ) ( 𝑅 ↾ 𝐴 ) ( 𝑓 ‘ suc 𝑎 ) ) ↔ 𝑦 ∈ ( rec ( ( 𝑏 ∈ V ↦ ∪ 𝑤 ∈ 𝑏 Pred ( 𝑅 , 𝐴 , 𝑤 ) ) , Pred ( 𝑅 , 𝐴 , 𝑥 ) ) ‘ 𝑛 ) ) ) |
| 4 | 3 | 3expb | ⊢ ( ( 𝑛 ∈ ω ∧ ( 𝑅 Se 𝐴 ∧ 𝑥 ∈ 𝐴 ) ) → ( ∃ 𝑓 ( 𝑓 Fn suc suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑦 ∧ ( 𝑓 ‘ suc 𝑛 ) = 𝑥 ) ∧ ∀ 𝑎 ∈ suc 𝑛 ( 𝑓 ‘ 𝑎 ) ( 𝑅 ↾ 𝐴 ) ( 𝑓 ‘ suc 𝑎 ) ) ↔ 𝑦 ∈ ( rec ( ( 𝑏 ∈ V ↦ ∪ 𝑤 ∈ 𝑏 Pred ( 𝑅 , 𝐴 , 𝑤 ) ) , Pred ( 𝑅 , 𝐴 , 𝑥 ) ) ‘ 𝑛 ) ) ) |
| 5 | 4 | ancoms | ⊢ ( ( ( 𝑅 Se 𝐴 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑛 ∈ ω ) → ( ∃ 𝑓 ( 𝑓 Fn suc suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑦 ∧ ( 𝑓 ‘ suc 𝑛 ) = 𝑥 ) ∧ ∀ 𝑎 ∈ suc 𝑛 ( 𝑓 ‘ 𝑎 ) ( 𝑅 ↾ 𝐴 ) ( 𝑓 ‘ suc 𝑎 ) ) ↔ 𝑦 ∈ ( rec ( ( 𝑏 ∈ V ↦ ∪ 𝑤 ∈ 𝑏 Pred ( 𝑅 , 𝐴 , 𝑤 ) ) , Pred ( 𝑅 , 𝐴 , 𝑥 ) ) ‘ 𝑛 ) ) ) |
| 6 | 5 | rexbidva | ⊢ ( ( 𝑅 Se 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( ∃ 𝑛 ∈ ω ∃ 𝑓 ( 𝑓 Fn suc suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑦 ∧ ( 𝑓 ‘ suc 𝑛 ) = 𝑥 ) ∧ ∀ 𝑎 ∈ suc 𝑛 ( 𝑓 ‘ 𝑎 ) ( 𝑅 ↾ 𝐴 ) ( 𝑓 ‘ suc 𝑎 ) ) ↔ ∃ 𝑛 ∈ ω 𝑦 ∈ ( rec ( ( 𝑏 ∈ V ↦ ∪ 𝑤 ∈ 𝑏 Pred ( 𝑅 , 𝐴 , 𝑤 ) ) , Pred ( 𝑅 , 𝐴 , 𝑥 ) ) ‘ 𝑛 ) ) ) |
| 7 | 1 6 | bitrid | ⊢ ( ( 𝑅 Se 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑦 t++ ( 𝑅 ↾ 𝐴 ) 𝑥 ↔ ∃ 𝑛 ∈ ω 𝑦 ∈ ( rec ( ( 𝑏 ∈ V ↦ ∪ 𝑤 ∈ 𝑏 Pred ( 𝑅 , 𝐴 , 𝑤 ) ) , Pred ( 𝑅 , 𝐴 , 𝑥 ) ) ‘ 𝑛 ) ) ) |
| 8 | vex | ⊢ 𝑦 ∈ V | |
| 9 | 8 | elpred | ⊢ ( 𝑥 ∈ V → ( 𝑦 ∈ Pred ( t++ ( 𝑅 ↾ 𝐴 ) , 𝐴 , 𝑥 ) ↔ ( 𝑦 ∈ 𝐴 ∧ 𝑦 t++ ( 𝑅 ↾ 𝐴 ) 𝑥 ) ) ) |
| 10 | 9 | elv | ⊢ ( 𝑦 ∈ Pred ( t++ ( 𝑅 ↾ 𝐴 ) , 𝐴 , 𝑥 ) ↔ ( 𝑦 ∈ 𝐴 ∧ 𝑦 t++ ( 𝑅 ↾ 𝐴 ) 𝑥 ) ) |
| 11 | resdmss | ⊢ dom ( 𝑅 ↾ 𝐴 ) ⊆ 𝐴 | |
| 12 | vex | ⊢ 𝑥 ∈ V | |
| 13 | 8 12 | breldm | ⊢ ( 𝑦 t++ ( 𝑅 ↾ 𝐴 ) 𝑥 → 𝑦 ∈ dom t++ ( 𝑅 ↾ 𝐴 ) ) |
| 14 | dmttrcl | ⊢ dom t++ ( 𝑅 ↾ 𝐴 ) = dom ( 𝑅 ↾ 𝐴 ) | |
| 15 | 13 14 | eleqtrdi | ⊢ ( 𝑦 t++ ( 𝑅 ↾ 𝐴 ) 𝑥 → 𝑦 ∈ dom ( 𝑅 ↾ 𝐴 ) ) |
| 16 | 11 15 | sselid | ⊢ ( 𝑦 t++ ( 𝑅 ↾ 𝐴 ) 𝑥 → 𝑦 ∈ 𝐴 ) |
| 17 | 16 | pm4.71ri | ⊢ ( 𝑦 t++ ( 𝑅 ↾ 𝐴 ) 𝑥 ↔ ( 𝑦 ∈ 𝐴 ∧ 𝑦 t++ ( 𝑅 ↾ 𝐴 ) 𝑥 ) ) |
| 18 | 10 17 | bitr4i | ⊢ ( 𝑦 ∈ Pred ( t++ ( 𝑅 ↾ 𝐴 ) , 𝐴 , 𝑥 ) ↔ 𝑦 t++ ( 𝑅 ↾ 𝐴 ) 𝑥 ) |
| 19 | rdgfun | ⊢ Fun rec ( ( 𝑏 ∈ V ↦ ∪ 𝑤 ∈ 𝑏 Pred ( 𝑅 , 𝐴 , 𝑤 ) ) , Pred ( 𝑅 , 𝐴 , 𝑥 ) ) | |
| 20 | eluniima | ⊢ ( Fun rec ( ( 𝑏 ∈ V ↦ ∪ 𝑤 ∈ 𝑏 Pred ( 𝑅 , 𝐴 , 𝑤 ) ) , Pred ( 𝑅 , 𝐴 , 𝑥 ) ) → ( 𝑦 ∈ ∪ ( rec ( ( 𝑏 ∈ V ↦ ∪ 𝑤 ∈ 𝑏 Pred ( 𝑅 , 𝐴 , 𝑤 ) ) , Pred ( 𝑅 , 𝐴 , 𝑥 ) ) “ ω ) ↔ ∃ 𝑛 ∈ ω 𝑦 ∈ ( rec ( ( 𝑏 ∈ V ↦ ∪ 𝑤 ∈ 𝑏 Pred ( 𝑅 , 𝐴 , 𝑤 ) ) , Pred ( 𝑅 , 𝐴 , 𝑥 ) ) ‘ 𝑛 ) ) ) | |
| 21 | 19 20 | ax-mp | ⊢ ( 𝑦 ∈ ∪ ( rec ( ( 𝑏 ∈ V ↦ ∪ 𝑤 ∈ 𝑏 Pred ( 𝑅 , 𝐴 , 𝑤 ) ) , Pred ( 𝑅 , 𝐴 , 𝑥 ) ) “ ω ) ↔ ∃ 𝑛 ∈ ω 𝑦 ∈ ( rec ( ( 𝑏 ∈ V ↦ ∪ 𝑤 ∈ 𝑏 Pred ( 𝑅 , 𝐴 , 𝑤 ) ) , Pred ( 𝑅 , 𝐴 , 𝑥 ) ) ‘ 𝑛 ) ) |
| 22 | 7 18 21 | 3bitr4g | ⊢ ( ( 𝑅 Se 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑦 ∈ Pred ( t++ ( 𝑅 ↾ 𝐴 ) , 𝐴 , 𝑥 ) ↔ 𝑦 ∈ ∪ ( rec ( ( 𝑏 ∈ V ↦ ∪ 𝑤 ∈ 𝑏 Pred ( 𝑅 , 𝐴 , 𝑤 ) ) , Pred ( 𝑅 , 𝐴 , 𝑥 ) ) “ ω ) ) ) |
| 23 | 22 | eqrdv | ⊢ ( ( 𝑅 Se 𝐴 ∧ 𝑥 ∈ 𝐴 ) → Pred ( t++ ( 𝑅 ↾ 𝐴 ) , 𝐴 , 𝑥 ) = ∪ ( rec ( ( 𝑏 ∈ V ↦ ∪ 𝑤 ∈ 𝑏 Pred ( 𝑅 , 𝐴 , 𝑤 ) ) , Pred ( 𝑅 , 𝐴 , 𝑥 ) ) “ ω ) ) |
| 24 | omex | ⊢ ω ∈ V | |
| 25 | 24 | funimaex | ⊢ ( Fun rec ( ( 𝑏 ∈ V ↦ ∪ 𝑤 ∈ 𝑏 Pred ( 𝑅 , 𝐴 , 𝑤 ) ) , Pred ( 𝑅 , 𝐴 , 𝑥 ) ) → ( rec ( ( 𝑏 ∈ V ↦ ∪ 𝑤 ∈ 𝑏 Pred ( 𝑅 , 𝐴 , 𝑤 ) ) , Pred ( 𝑅 , 𝐴 , 𝑥 ) ) “ ω ) ∈ V ) |
| 26 | 19 25 | ax-mp | ⊢ ( rec ( ( 𝑏 ∈ V ↦ ∪ 𝑤 ∈ 𝑏 Pred ( 𝑅 , 𝐴 , 𝑤 ) ) , Pred ( 𝑅 , 𝐴 , 𝑥 ) ) “ ω ) ∈ V |
| 27 | 26 | uniex | ⊢ ∪ ( rec ( ( 𝑏 ∈ V ↦ ∪ 𝑤 ∈ 𝑏 Pred ( 𝑅 , 𝐴 , 𝑤 ) ) , Pred ( 𝑅 , 𝐴 , 𝑥 ) ) “ ω ) ∈ V |
| 28 | 23 27 | eqeltrdi | ⊢ ( ( 𝑅 Se 𝐴 ∧ 𝑥 ∈ 𝐴 ) → Pred ( t++ ( 𝑅 ↾ 𝐴 ) , 𝐴 , 𝑥 ) ∈ V ) |
| 29 | 28 | ralrimiva | ⊢ ( 𝑅 Se 𝐴 → ∀ 𝑥 ∈ 𝐴 Pred ( t++ ( 𝑅 ↾ 𝐴 ) , 𝐴 , 𝑥 ) ∈ V ) |
| 30 | dfse3 | ⊢ ( t++ ( 𝑅 ↾ 𝐴 ) Se 𝐴 ↔ ∀ 𝑥 ∈ 𝐴 Pred ( t++ ( 𝑅 ↾ 𝐴 ) , 𝐴 , 𝑥 ) ∈ V ) | |
| 31 | 29 30 | sylibr | ⊢ ( 𝑅 Se 𝐴 → t++ ( 𝑅 ↾ 𝐴 ) Se 𝐴 ) |