Metamath Proof Explorer

Theorem trpredtr

Description: The transitive predecessors are transitive in R and A (Contributed by Scott Fenton, 20-Feb-2011) (Revised by Mario Carneiro, 26-Jun-2015)

Ref Expression
Assertion trpredtr ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) → ( 𝑌 ∈ TrPred ( 𝑅 , 𝐴 , 𝑋 ) → Pred ( 𝑅 , 𝐴 , 𝑌 ) ⊆ TrPred ( 𝑅 , 𝐴 , 𝑋 ) ) )

Proof

Step Hyp Ref Expression
1 eltrpred ⊢ ( 𝑌 ∈ TrPred ( 𝑅 , 𝐴 , 𝑋 ) ↔ ∃ 𝑖 ∈ ω 𝑌 ∈ ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑖 ) )
2 simplr ⊢ ( ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑖 ∈ ω ) ∧ 𝑌 ∈ ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑖 ) ) → 𝑖 ∈ ω )
3 peano2 ⊢ ( 𝑖 ∈ ω → suc 𝑖 ∈ ω )
4 2 3 syl ⊢ ( ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑖 ∈ ω ) ∧ 𝑌 ∈ ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑖 ) ) → suc 𝑖 ∈ ω )
5 simpr ⊢ ( ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑖 ∈ ω ) ∧ 𝑌 ∈ ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑖 ) ) → 𝑌 ∈ ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑖 ) )
6 ssid ⊢ Pred ( 𝑅 , 𝐴 , 𝑌 ) ⊆ Pred ( 𝑅 , 𝐴 , 𝑌 )
7 predeq3 ⊢ ( 𝑡 = 𝑌 → Pred ( 𝑅 , 𝐴 , 𝑡 ) = Pred ( 𝑅 , 𝐴 , 𝑌 ) )
8 7 sseq2d ⊢ ( 𝑡 = 𝑌 → ( Pred ( 𝑅 , 𝐴 , 𝑌 ) ⊆ Pred ( 𝑅 , 𝐴 , 𝑡 ) ↔ Pred ( 𝑅 , 𝐴 , 𝑌 ) ⊆ Pred ( 𝑅 , 𝐴 , 𝑌 ) ) )
9 8 rspcev ⊢ ( ( 𝑌 ∈ ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑖 ) ∧ Pred ( 𝑅 , 𝐴 , 𝑌 ) ⊆ Pred ( 𝑅 , 𝐴 , 𝑌 ) ) → ∃ 𝑡 ∈ ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑖 ) Pred ( 𝑅 , 𝐴 , 𝑌 ) ⊆ Pred ( 𝑅 , 𝐴 , 𝑡 ) )
10 ssiun ⊢ ( ∃ 𝑡 ∈ ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑖 ) Pred ( 𝑅 , 𝐴 , 𝑌 ) ⊆ Pred ( 𝑅 , 𝐴 , 𝑡 ) → Pred ( 𝑅 , 𝐴 , 𝑌 ) ⊆ ∪ 𝑡 ∈ ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑖 ) Pred ( 𝑅 , 𝐴 , 𝑡 ) )
11 9 10 syl ⊢ ( ( 𝑌 ∈ ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑖 ) ∧ Pred ( 𝑅 , 𝐴 , 𝑌 ) ⊆ Pred ( 𝑅 , 𝐴 , 𝑌 ) ) → Pred ( 𝑅 , 𝐴 , 𝑌 ) ⊆ ∪ 𝑡 ∈ ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑖 ) Pred ( 𝑅 , 𝐴 , 𝑡 ) )
12 5 6 11 sylancl ⊢ ( ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑖 ∈ ω ) ∧ 𝑌 ∈ ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑖 ) ) → Pred ( 𝑅 , 𝐴 , 𝑌 ) ⊆ ∪ 𝑡 ∈ ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑖 ) Pred ( 𝑅 , 𝐴 , 𝑡 ) )
13 fvex ⊢ ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑖 ) ∈ V
14 setlikespec ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) → Pred ( 𝑅 , 𝐴 , 𝑋 ) ∈ V )
15 trpredlem1 ⊢ ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ∈ V → ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑖 ) ⊆ 𝐴 )
16 14 15 syl ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) → ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑖 ) ⊆ 𝐴 )
17 16 sseld ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) → ( 𝑡 ∈ ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑖 ) → 𝑡 ∈ 𝐴 ) )
18 setlikespec ⊢ ( ( 𝑡 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) → Pred ( 𝑅 , 𝐴 , 𝑡 ) ∈ V )
19 18 expcom ⊢ ( 𝑅 Se 𝐴 → ( 𝑡 ∈ 𝐴 → Pred ( 𝑅 , 𝐴 , 𝑡 ) ∈ V ) )
20 19 adantl ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) → ( 𝑡 ∈ 𝐴 → Pred ( 𝑅 , 𝐴 , 𝑡 ) ∈ V ) )
21 17 20 syld ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) → ( 𝑡 ∈ ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑖 ) → Pred ( 𝑅 , 𝐴 , 𝑡 ) ∈ V ) )
22 21 ralrimiv ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) → ∀ 𝑡 ∈ ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑖 ) Pred ( 𝑅 , 𝐴 , 𝑡 ) ∈ V )
23 22 ad2antrr ⊢ ( ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑖 ∈ ω ) ∧ 𝑌 ∈ ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑖 ) ) → ∀ 𝑡 ∈ ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑖 ) Pred ( 𝑅 , 𝐴 , 𝑡 ) ∈ V )
24 iunexg ⊢ ( ( ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑖 ) ∈ V ∧ ∀ 𝑡 ∈ ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑖 ) Pred ( 𝑅 , 𝐴 , 𝑡 ) ∈ V ) → ∪ 𝑡 ∈ ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑖 ) Pred ( 𝑅 , 𝐴 , 𝑡 ) ∈ V )
25 13 23 24 sylancr ⊢ ( ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑖 ∈ ω ) ∧ 𝑌 ∈ ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑖 ) ) → ∪ 𝑡 ∈ ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑖 ) Pred ( 𝑅 , 𝐴 , 𝑡 ) ∈ V )
26 nfcv ⊢ Ⅎ 𝑓 Pred ( 𝑅 , 𝐴 , 𝑋 )
27 nfcv ⊢ Ⅎ 𝑓 𝑖
28 nfcv ⊢ Ⅎ 𝑓 ∪ 𝑡 ∈ ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑖 ) Pred ( 𝑅 , 𝐴 , 𝑡 )
29 predeq3 ⊢ ( 𝑦 = 𝑡 → Pred ( 𝑅 , 𝐴 , 𝑦 ) = Pred ( 𝑅 , 𝐴 , 𝑡 ) )
30 29 cbviunv ⊢ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) = ∪ 𝑡 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑡 )
31 iuneq1 ⊢ ( 𝑎 = 𝑓 → ∪ 𝑡 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑡 ) = ∪ 𝑡 ∈ 𝑓 Pred ( 𝑅 , 𝐴 , 𝑡 ) )
32 30 31 syl5eq ⊢ ( 𝑎 = 𝑓 → ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) = ∪ 𝑡 ∈ 𝑓 Pred ( 𝑅 , 𝐴 , 𝑡 ) )
33 32 cbvmptv ⊢ ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) = ( 𝑓 ∈ V ↦ ∪ 𝑡 ∈ 𝑓 Pred ( 𝑅 , 𝐴 , 𝑡 ) )
34 rdgeq1 ⊢ ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) = ( 𝑓 ∈ V ↦ ∪ 𝑡 ∈ 𝑓 Pred ( 𝑅 , 𝐴 , 𝑡 ) ) → rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) = rec ( ( 𝑓 ∈ V ↦ ∪ 𝑡 ∈ 𝑓 Pred ( 𝑅 , 𝐴 , 𝑡 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) )
35 reseq1 ⊢ ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) = rec ( ( 𝑓 ∈ V ↦ ∪ 𝑡 ∈ 𝑓 Pred ( 𝑅 , 𝐴 , 𝑡 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) → ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) = ( rec ( ( 𝑓 ∈ V ↦ ∪ 𝑡 ∈ 𝑓 Pred ( 𝑅 , 𝐴 , 𝑡 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) )
36 33 34 35 mp2b ⊢ ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) = ( rec ( ( 𝑓 ∈ V ↦ ∪ 𝑡 ∈ 𝑓 Pred ( 𝑅 , 𝐴 , 𝑡 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω )
37 iuneq1 ⊢ ( 𝑓 = ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑖 ) → ∪ 𝑡 ∈ 𝑓 Pred ( 𝑅 , 𝐴 , 𝑡 ) = ∪ 𝑡 ∈ ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑖 ) Pred ( 𝑅 , 𝐴 , 𝑡 ) )
38 26 27 28 36 37 frsucmpt ⊢ ( ( 𝑖 ∈ ω ∧ ∪ 𝑡 ∈ ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑖 ) Pred ( 𝑅 , 𝐴 , 𝑡 ) ∈ V ) → ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ suc 𝑖 ) = ∪ 𝑡 ∈ ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑖 ) Pred ( 𝑅 , 𝐴 , 𝑡 ) )
39 2 25 38 syl2anc ⊢ ( ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑖 ∈ ω ) ∧ 𝑌 ∈ ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑖 ) ) → ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ suc 𝑖 ) = ∪ 𝑡 ∈ ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑖 ) Pred ( 𝑅 , 𝐴 , 𝑡 ) )
40 12 39 sseqtrrd ⊢ ( ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑖 ∈ ω ) ∧ 𝑌 ∈ ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑖 ) ) → Pred ( 𝑅 , 𝐴 , 𝑌 ) ⊆ ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ suc 𝑖 ) )
41 fveq2 ⊢ ( 𝑗 = suc 𝑖 → ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑗 ) = ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ suc 𝑖 ) )
42 41 sseq2d ⊢ ( 𝑗 = suc 𝑖 → ( Pred ( 𝑅 , 𝐴 , 𝑌 ) ⊆ ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑗 ) ↔ Pred ( 𝑅 , 𝐴 , 𝑌 ) ⊆ ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ suc 𝑖 ) ) )
43 42 rspcev ⊢ ( ( suc 𝑖 ∈ ω ∧ Pred ( 𝑅 , 𝐴 , 𝑌 ) ⊆ ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ suc 𝑖 ) ) → ∃ 𝑗 ∈ ω Pred ( 𝑅 , 𝐴 , 𝑌 ) ⊆ ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑗 ) )
44 ssiun ⊢ ( ∃ 𝑗 ∈ ω Pred ( 𝑅 , 𝐴 , 𝑌 ) ⊆ ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑗 ) → Pred ( 𝑅 , 𝐴 , 𝑌 ) ⊆ ∪ 𝑗 ∈ ω ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑗 ) )
45 43 44 syl ⊢ ( ( suc 𝑖 ∈ ω ∧ Pred ( 𝑅 , 𝐴 , 𝑌 ) ⊆ ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ suc 𝑖 ) ) → Pred ( 𝑅 , 𝐴 , 𝑌 ) ⊆ ∪ 𝑗 ∈ ω ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑗 ) )
46 dftrpred2 ⊢ TrPred ( 𝑅 , 𝐴 , 𝑋 ) = ∪ 𝑗 ∈ ω ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑗 )
47 45 46 sseqtrrdi ⊢ ( ( suc 𝑖 ∈ ω ∧ Pred ( 𝑅 , 𝐴 , 𝑌 ) ⊆ ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ suc 𝑖 ) ) → Pred ( 𝑅 , 𝐴 , 𝑌 ) ⊆ TrPred ( 𝑅 , 𝐴 , 𝑋 ) )
48 4 40 47 syl2anc ⊢ ( ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑖 ∈ ω ) ∧ 𝑌 ∈ ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑖 ) ) → Pred ( 𝑅 , 𝐴 , 𝑌 ) ⊆ TrPred ( 𝑅 , 𝐴 , 𝑋 ) )
49 48 rexlimdva2 ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) → ( ∃ 𝑖 ∈ ω 𝑌 ∈ ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑖 ) → Pred ( 𝑅 , 𝐴 , 𝑌 ) ⊆ TrPred ( 𝑅 , 𝐴 , 𝑋 ) ) )
50 1 49 syl5bi ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) → ( 𝑌 ∈ TrPred ( 𝑅 , 𝐴 , 𝑋 ) → Pred ( 𝑅 , 𝐴 , 𝑌 ) ⊆ TrPred ( 𝑅 , 𝐴 , 𝑋 ) ) )