Metamath Proof Explorer


Theorem trpredmintr

Description: The transitive predecessors form the smallest superclass of predecessors closed under taking predecessors. (Contributed by Scott Fenton, 25-Apr-2012) (Revised by Mario Carneiro, 26-Jun-2015)

Ref Expression
Assertion trpredmintr ( ( ( 𝑋𝐴𝑅 Se 𝐴 ) ∧ ( ∀ 𝑦𝐵 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝐵 ∧ Pred ( 𝑅 , 𝐴 , 𝑋 ) ⊆ 𝐵 ) ) → TrPred ( 𝑅 , 𝐴 , 𝑋 ) ⊆ 𝐵 )

Proof

Step Hyp Ref Expression
1 dftrpred2 TrPred ( 𝑅 , 𝐴 , 𝑋 ) = 𝑖 ∈ ω ( ( rec ( ( 𝑎 ∈ V ↦ 𝑦𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑖 )
2 fveq2 ( 𝑗 = ∅ → ( ( rec ( ( 𝑎 ∈ V ↦ 𝑦𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑗 ) = ( ( rec ( ( 𝑎 ∈ V ↦ 𝑦𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ ∅ ) )
3 2 sseq1d ( 𝑗 = ∅ → ( ( ( rec ( ( 𝑎 ∈ V ↦ 𝑦𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑗 ) ⊆ 𝐵 ↔ ( ( rec ( ( 𝑎 ∈ V ↦ 𝑦𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ ∅ ) ⊆ 𝐵 ) )
4 3 imbi2d ( 𝑗 = ∅ → ( ( ( ( 𝑋𝐴𝑅 Se 𝐴 ) ∧ ( ∀ 𝑦𝐵 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝐵 ∧ Pred ( 𝑅 , 𝐴 , 𝑋 ) ⊆ 𝐵 ) ) → ( ( rec ( ( 𝑎 ∈ V ↦ 𝑦𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑗 ) ⊆ 𝐵 ) ↔ ( ( ( 𝑋𝐴𝑅 Se 𝐴 ) ∧ ( ∀ 𝑦𝐵 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝐵 ∧ Pred ( 𝑅 , 𝐴 , 𝑋 ) ⊆ 𝐵 ) ) → ( ( rec ( ( 𝑎 ∈ V ↦ 𝑦𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ ∅ ) ⊆ 𝐵 ) ) )
5 fveq2 ( 𝑗 = 𝑘 → ( ( rec ( ( 𝑎 ∈ V ↦ 𝑦𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑗 ) = ( ( rec ( ( 𝑎 ∈ V ↦ 𝑦𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑘 ) )
6 5 sseq1d ( 𝑗 = 𝑘 → ( ( ( rec ( ( 𝑎 ∈ V ↦ 𝑦𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑗 ) ⊆ 𝐵 ↔ ( ( rec ( ( 𝑎 ∈ V ↦ 𝑦𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑘 ) ⊆ 𝐵 ) )
7 6 imbi2d ( 𝑗 = 𝑘 → ( ( ( ( 𝑋𝐴𝑅 Se 𝐴 ) ∧ ( ∀ 𝑦𝐵 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝐵 ∧ Pred ( 𝑅 , 𝐴 , 𝑋 ) ⊆ 𝐵 ) ) → ( ( rec ( ( 𝑎 ∈ V ↦ 𝑦𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑗 ) ⊆ 𝐵 ) ↔ ( ( ( 𝑋𝐴𝑅 Se 𝐴 ) ∧ ( ∀ 𝑦𝐵 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝐵 ∧ Pred ( 𝑅 , 𝐴 , 𝑋 ) ⊆ 𝐵 ) ) → ( ( rec ( ( 𝑎 ∈ V ↦ 𝑦𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑘 ) ⊆ 𝐵 ) ) )
8 fveq2 ( 𝑗 = suc 𝑘 → ( ( rec ( ( 𝑎 ∈ V ↦ 𝑦𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑗 ) = ( ( rec ( ( 𝑎 ∈ V ↦ 𝑦𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ suc 𝑘 ) )
9 8 sseq1d ( 𝑗 = suc 𝑘 → ( ( ( rec ( ( 𝑎 ∈ V ↦ 𝑦𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑗 ) ⊆ 𝐵 ↔ ( ( rec ( ( 𝑎 ∈ V ↦ 𝑦𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ suc 𝑘 ) ⊆ 𝐵 ) )
10 9 imbi2d ( 𝑗 = suc 𝑘 → ( ( ( ( 𝑋𝐴𝑅 Se 𝐴 ) ∧ ( ∀ 𝑦𝐵 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝐵 ∧ Pred ( 𝑅 , 𝐴 , 𝑋 ) ⊆ 𝐵 ) ) → ( ( rec ( ( 𝑎 ∈ V ↦ 𝑦𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑗 ) ⊆ 𝐵 ) ↔ ( ( ( 𝑋𝐴𝑅 Se 𝐴 ) ∧ ( ∀ 𝑦𝐵 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝐵 ∧ Pred ( 𝑅 , 𝐴 , 𝑋 ) ⊆ 𝐵 ) ) → ( ( rec ( ( 𝑎 ∈ V ↦ 𝑦𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ suc 𝑘 ) ⊆ 𝐵 ) ) )
11 fveq2 ( 𝑗 = 𝑖 → ( ( rec ( ( 𝑎 ∈ V ↦ 𝑦𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑗 ) = ( ( rec ( ( 𝑎 ∈ V ↦ 𝑦𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑖 ) )
12 11 sseq1d ( 𝑗 = 𝑖 → ( ( ( rec ( ( 𝑎 ∈ V ↦ 𝑦𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑗 ) ⊆ 𝐵 ↔ ( ( rec ( ( 𝑎 ∈ V ↦ 𝑦𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑖 ) ⊆ 𝐵 ) )
13 12 imbi2d ( 𝑗 = 𝑖 → ( ( ( ( 𝑋𝐴𝑅 Se 𝐴 ) ∧ ( ∀ 𝑦𝐵 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝐵 ∧ Pred ( 𝑅 , 𝐴 , 𝑋 ) ⊆ 𝐵 ) ) → ( ( rec ( ( 𝑎 ∈ V ↦ 𝑦𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑗 ) ⊆ 𝐵 ) ↔ ( ( ( 𝑋𝐴𝑅 Se 𝐴 ) ∧ ( ∀ 𝑦𝐵 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝐵 ∧ Pred ( 𝑅 , 𝐴 , 𝑋 ) ⊆ 𝐵 ) ) → ( ( rec ( ( 𝑎 ∈ V ↦ 𝑦𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑖 ) ⊆ 𝐵 ) ) )
14 setlikespec ( ( 𝑋𝐴𝑅 Se 𝐴 ) → Pred ( 𝑅 , 𝐴 , 𝑋 ) ∈ V )
15 fr0g ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ∈ V → ( ( rec ( ( 𝑎 ∈ V ↦ 𝑦𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ ∅ ) = Pred ( 𝑅 , 𝐴 , 𝑋 ) )
16 14 15 syl ( ( 𝑋𝐴𝑅 Se 𝐴 ) → ( ( rec ( ( 𝑎 ∈ V ↦ 𝑦𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ ∅ ) = Pred ( 𝑅 , 𝐴 , 𝑋 ) )
17 16 adantr ( ( ( 𝑋𝐴𝑅 Se 𝐴 ) ∧ ( ∀ 𝑦𝐵 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝐵 ∧ Pred ( 𝑅 , 𝐴 , 𝑋 ) ⊆ 𝐵 ) ) → ( ( rec ( ( 𝑎 ∈ V ↦ 𝑦𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ ∅ ) = Pred ( 𝑅 , 𝐴 , 𝑋 ) )
18 simprr ( ( ( 𝑋𝐴𝑅 Se 𝐴 ) ∧ ( ∀ 𝑦𝐵 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝐵 ∧ Pred ( 𝑅 , 𝐴 , 𝑋 ) ⊆ 𝐵 ) ) → Pred ( 𝑅 , 𝐴 , 𝑋 ) ⊆ 𝐵 )
19 17 18 eqsstrd ( ( ( 𝑋𝐴𝑅 Se 𝐴 ) ∧ ( ∀ 𝑦𝐵 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝐵 ∧ Pred ( 𝑅 , 𝐴 , 𝑋 ) ⊆ 𝐵 ) ) → ( ( rec ( ( 𝑎 ∈ V ↦ 𝑦𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ ∅ ) ⊆ 𝐵 )
20 fvex ( ( rec ( ( 𝑐 ∈ V ↦ 𝑑𝑐 Pred ( 𝑅 , 𝐴 , 𝑑 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑘 ) ∈ V
21 trpredlem1 ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ∈ V → ( ( rec ( ( 𝑐 ∈ V ↦ 𝑑𝑐 Pred ( 𝑅 , 𝐴 , 𝑑 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑘 ) ⊆ 𝐴 )
22 14 21 syl ( ( 𝑋𝐴𝑅 Se 𝐴 ) → ( ( rec ( ( 𝑐 ∈ V ↦ 𝑑𝑐 Pred ( 𝑅 , 𝐴 , 𝑑 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑘 ) ⊆ 𝐴 )
23 22 sseld ( ( 𝑋𝐴𝑅 Se 𝐴 ) → ( 𝑦 ∈ ( ( rec ( ( 𝑐 ∈ V ↦ 𝑑𝑐 Pred ( 𝑅 , 𝐴 , 𝑑 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑘 ) → 𝑦𝐴 ) )
24 setlikespec ( ( 𝑦𝐴𝑅 Se 𝐴 ) → Pred ( 𝑅 , 𝐴 , 𝑦 ) ∈ V )
25 24 expcom ( 𝑅 Se 𝐴 → ( 𝑦𝐴 → Pred ( 𝑅 , 𝐴 , 𝑦 ) ∈ V ) )
26 25 adantl ( ( 𝑋𝐴𝑅 Se 𝐴 ) → ( 𝑦𝐴 → Pred ( 𝑅 , 𝐴 , 𝑦 ) ∈ V ) )
27 23 26 syld ( ( 𝑋𝐴𝑅 Se 𝐴 ) → ( 𝑦 ∈ ( ( rec ( ( 𝑐 ∈ V ↦ 𝑑𝑐 Pred ( 𝑅 , 𝐴 , 𝑑 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑘 ) → Pred ( 𝑅 , 𝐴 , 𝑦 ) ∈ V ) )
28 27 ralrimiv ( ( 𝑋𝐴𝑅 Se 𝐴 ) → ∀ 𝑦 ∈ ( ( rec ( ( 𝑐 ∈ V ↦ 𝑑𝑐 Pred ( 𝑅 , 𝐴 , 𝑑 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑘 ) Pred ( 𝑅 , 𝐴 , 𝑦 ) ∈ V )
29 28 ad2antrr ( ( ( ( 𝑋𝐴𝑅 Se 𝐴 ) ∧ ( ∀ 𝑦𝐵 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝐵 ∧ Pred ( 𝑅 , 𝐴 , 𝑋 ) ⊆ 𝐵 ) ) ∧ ( ( rec ( ( 𝑎 ∈ V ↦ 𝑦𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑘 ) ⊆ 𝐵 ) → ∀ 𝑦 ∈ ( ( rec ( ( 𝑐 ∈ V ↦ 𝑑𝑐 Pred ( 𝑅 , 𝐴 , 𝑑 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑘 ) Pred ( 𝑅 , 𝐴 , 𝑦 ) ∈ V )
30 iunexg ( ( ( ( rec ( ( 𝑐 ∈ V ↦ 𝑑𝑐 Pred ( 𝑅 , 𝐴 , 𝑑 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑘 ) ∈ V ∧ ∀ 𝑦 ∈ ( ( rec ( ( 𝑐 ∈ V ↦ 𝑑𝑐 Pred ( 𝑅 , 𝐴 , 𝑑 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑘 ) Pred ( 𝑅 , 𝐴 , 𝑦 ) ∈ V ) → 𝑦 ∈ ( ( rec ( ( 𝑐 ∈ V ↦ 𝑑𝑐 Pred ( 𝑅 , 𝐴 , 𝑑 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑘 ) Pred ( 𝑅 , 𝐴 , 𝑦 ) ∈ V )
31 20 29 30 sylancr ( ( ( ( 𝑋𝐴𝑅 Se 𝐴 ) ∧ ( ∀ 𝑦𝐵 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝐵 ∧ Pred ( 𝑅 , 𝐴 , 𝑋 ) ⊆ 𝐵 ) ) ∧ ( ( rec ( ( 𝑎 ∈ V ↦ 𝑦𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑘 ) ⊆ 𝐵 ) → 𝑦 ∈ ( ( rec ( ( 𝑐 ∈ V ↦ 𝑑𝑐 Pred ( 𝑅 , 𝐴 , 𝑑 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑘 ) Pred ( 𝑅 , 𝐴 , 𝑦 ) ∈ V )
32 nfcv 𝑎 Pred ( 𝑅 , 𝐴 , 𝑋 )
33 nfcv 𝑎 𝑘
34 nfcv 𝑎 𝑦 ∈ ( ( rec ( ( 𝑐 ∈ V ↦ 𝑑𝑐 Pred ( 𝑅 , 𝐴 , 𝑑 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑘 ) Pred ( 𝑅 , 𝐴 , 𝑦 )
35 eqid ( rec ( ( 𝑎 ∈ V ↦ 𝑦𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) = ( rec ( ( 𝑎 ∈ V ↦ 𝑦𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω )
36 predeq3 ( 𝑦 = 𝑑 → Pred ( 𝑅 , 𝐴 , 𝑦 ) = Pred ( 𝑅 , 𝐴 , 𝑑 ) )
37 36 cbviunv 𝑦𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) = 𝑑𝑎 Pred ( 𝑅 , 𝐴 , 𝑑 )
38 iuneq1 ( 𝑎 = 𝑐 𝑑𝑎 Pred ( 𝑅 , 𝐴 , 𝑑 ) = 𝑑𝑐 Pred ( 𝑅 , 𝐴 , 𝑑 ) )
39 37 38 eqtrid ( 𝑎 = 𝑐 𝑦𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) = 𝑑𝑐 Pred ( 𝑅 , 𝐴 , 𝑑 ) )
40 39 cbvmptv ( 𝑎 ∈ V ↦ 𝑦𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) = ( 𝑐 ∈ V ↦ 𝑑𝑐 Pred ( 𝑅 , 𝐴 , 𝑑 ) )
41 rdgeq1 ( ( 𝑎 ∈ V ↦ 𝑦𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) = ( 𝑐 ∈ V ↦ 𝑑𝑐 Pred ( 𝑅 , 𝐴 , 𝑑 ) ) → rec ( ( 𝑎 ∈ V ↦ 𝑦𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) = rec ( ( 𝑐 ∈ V ↦ 𝑑𝑐 Pred ( 𝑅 , 𝐴 , 𝑑 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) )
42 reseq1 ( rec ( ( 𝑎 ∈ V ↦ 𝑦𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) = rec ( ( 𝑐 ∈ V ↦ 𝑑𝑐 Pred ( 𝑅 , 𝐴 , 𝑑 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) → ( rec ( ( 𝑎 ∈ V ↦ 𝑦𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) = ( rec ( ( 𝑐 ∈ V ↦ 𝑑𝑐 Pred ( 𝑅 , 𝐴 , 𝑑 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) )
43 40 41 42 mp2b ( rec ( ( 𝑎 ∈ V ↦ 𝑦𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) = ( rec ( ( 𝑐 ∈ V ↦ 𝑑𝑐 Pred ( 𝑅 , 𝐴 , 𝑑 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω )
44 43 fveq1i ( ( rec ( ( 𝑎 ∈ V ↦ 𝑦𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑘 ) = ( ( rec ( ( 𝑐 ∈ V ↦ 𝑑𝑐 Pred ( 𝑅 , 𝐴 , 𝑑 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑘 )
45 44 eqeq2i ( 𝑎 = ( ( rec ( ( 𝑎 ∈ V ↦ 𝑦𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑘 ) ↔ 𝑎 = ( ( rec ( ( 𝑐 ∈ V ↦ 𝑑𝑐 Pred ( 𝑅 , 𝐴 , 𝑑 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑘 ) )
46 iuneq1 ( 𝑎 = ( ( rec ( ( 𝑐 ∈ V ↦ 𝑑𝑐 Pred ( 𝑅 , 𝐴 , 𝑑 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑘 ) → 𝑦𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) = 𝑦 ∈ ( ( rec ( ( 𝑐 ∈ V ↦ 𝑑𝑐 Pred ( 𝑅 , 𝐴 , 𝑑 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑘 ) Pred ( 𝑅 , 𝐴 , 𝑦 ) )
47 45 46 sylbi ( 𝑎 = ( ( rec ( ( 𝑎 ∈ V ↦ 𝑦𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑘 ) → 𝑦𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) = 𝑦 ∈ ( ( rec ( ( 𝑐 ∈ V ↦ 𝑑𝑐 Pred ( 𝑅 , 𝐴 , 𝑑 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑘 ) Pred ( 𝑅 , 𝐴 , 𝑦 ) )
48 32 33 34 35 47 frsucmpt ( ( 𝑘 ∈ ω ∧ 𝑦 ∈ ( ( rec ( ( 𝑐 ∈ V ↦ 𝑑𝑐 Pred ( 𝑅 , 𝐴 , 𝑑 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑘 ) Pred ( 𝑅 , 𝐴 , 𝑦 ) ∈ V ) → ( ( rec ( ( 𝑎 ∈ V ↦ 𝑦𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ suc 𝑘 ) = 𝑦 ∈ ( ( rec ( ( 𝑐 ∈ V ↦ 𝑑𝑐 Pred ( 𝑅 , 𝐴 , 𝑑 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑘 ) Pred ( 𝑅 , 𝐴 , 𝑦 ) )
49 31 48 sylan2 ( ( 𝑘 ∈ ω ∧ ( ( ( 𝑋𝐴𝑅 Se 𝐴 ) ∧ ( ∀ 𝑦𝐵 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝐵 ∧ Pred ( 𝑅 , 𝐴 , 𝑋 ) ⊆ 𝐵 ) ) ∧ ( ( rec ( ( 𝑎 ∈ V ↦ 𝑦𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑘 ) ⊆ 𝐵 ) ) → ( ( rec ( ( 𝑎 ∈ V ↦ 𝑦𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ suc 𝑘 ) = 𝑦 ∈ ( ( rec ( ( 𝑐 ∈ V ↦ 𝑑𝑐 Pred ( 𝑅 , 𝐴 , 𝑑 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑘 ) Pred ( 𝑅 , 𝐴 , 𝑦 ) )
50 44 sseq1i ( ( ( rec ( ( 𝑎 ∈ V ↦ 𝑦𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑘 ) ⊆ 𝐵 ↔ ( ( rec ( ( 𝑐 ∈ V ↦ 𝑑𝑐 Pred ( 𝑅 , 𝐴 , 𝑑 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑘 ) ⊆ 𝐵 )
51 50 anbi2i ( ( ( ( 𝑋𝐴𝑅 Se 𝐴 ) ∧ ( ∀ 𝑦𝐵 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝐵 ∧ Pred ( 𝑅 , 𝐴 , 𝑋 ) ⊆ 𝐵 ) ) ∧ ( ( rec ( ( 𝑎 ∈ V ↦ 𝑦𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑘 ) ⊆ 𝐵 ) ↔ ( ( ( 𝑋𝐴𝑅 Se 𝐴 ) ∧ ( ∀ 𝑦𝐵 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝐵 ∧ Pred ( 𝑅 , 𝐴 , 𝑋 ) ⊆ 𝐵 ) ) ∧ ( ( rec ( ( 𝑐 ∈ V ↦ 𝑑𝑐 Pred ( 𝑅 , 𝐴 , 𝑑 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑘 ) ⊆ 𝐵 ) )
52 nfv 𝑦 ( 𝑋𝐴𝑅 Se 𝐴 )
53 nfra1 𝑦𝑦𝐵 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝐵
54 nfv 𝑦 Pred ( 𝑅 , 𝐴 , 𝑋 ) ⊆ 𝐵
55 53 54 nfan 𝑦 ( ∀ 𝑦𝐵 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝐵 ∧ Pred ( 𝑅 , 𝐴 , 𝑋 ) ⊆ 𝐵 )
56 52 55 nfan 𝑦 ( ( 𝑋𝐴𝑅 Se 𝐴 ) ∧ ( ∀ 𝑦𝐵 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝐵 ∧ Pred ( 𝑅 , 𝐴 , 𝑋 ) ⊆ 𝐵 ) )
57 nfv 𝑦 ( ( rec ( ( 𝑐 ∈ V ↦ 𝑑𝑐 Pred ( 𝑅 , 𝐴 , 𝑑 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑘 ) ⊆ 𝐵
58 56 57 nfan 𝑦 ( ( ( 𝑋𝐴𝑅 Se 𝐴 ) ∧ ( ∀ 𝑦𝐵 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝐵 ∧ Pred ( 𝑅 , 𝐴 , 𝑋 ) ⊆ 𝐵 ) ) ∧ ( ( rec ( ( 𝑐 ∈ V ↦ 𝑑𝑐 Pred ( 𝑅 , 𝐴 , 𝑑 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑘 ) ⊆ 𝐵 )
59 ssel ( ( ( rec ( ( 𝑐 ∈ V ↦ 𝑑𝑐 Pred ( 𝑅 , 𝐴 , 𝑑 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑘 ) ⊆ 𝐵 → ( 𝑦 ∈ ( ( rec ( ( 𝑐 ∈ V ↦ 𝑑𝑐 Pred ( 𝑅 , 𝐴 , 𝑑 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑘 ) → 𝑦𝐵 ) )
60 rsp ( ∀ 𝑦𝐵 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝐵 → ( 𝑦𝐵 → Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝐵 ) )
61 60 ad2antrl ( ( ( 𝑋𝐴𝑅 Se 𝐴 ) ∧ ( ∀ 𝑦𝐵 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝐵 ∧ Pred ( 𝑅 , 𝐴 , 𝑋 ) ⊆ 𝐵 ) ) → ( 𝑦𝐵 → Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝐵 ) )
62 59 61 sylan9r ( ( ( ( 𝑋𝐴𝑅 Se 𝐴 ) ∧ ( ∀ 𝑦𝐵 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝐵 ∧ Pred ( 𝑅 , 𝐴 , 𝑋 ) ⊆ 𝐵 ) ) ∧ ( ( rec ( ( 𝑐 ∈ V ↦ 𝑑𝑐 Pred ( 𝑅 , 𝐴 , 𝑑 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑘 ) ⊆ 𝐵 ) → ( 𝑦 ∈ ( ( rec ( ( 𝑐 ∈ V ↦ 𝑑𝑐 Pred ( 𝑅 , 𝐴 , 𝑑 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑘 ) → Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝐵 ) )
63 58 62 ralrimi ( ( ( ( 𝑋𝐴𝑅 Se 𝐴 ) ∧ ( ∀ 𝑦𝐵 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝐵 ∧ Pred ( 𝑅 , 𝐴 , 𝑋 ) ⊆ 𝐵 ) ) ∧ ( ( rec ( ( 𝑐 ∈ V ↦ 𝑑𝑐 Pred ( 𝑅 , 𝐴 , 𝑑 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑘 ) ⊆ 𝐵 ) → ∀ 𝑦 ∈ ( ( rec ( ( 𝑐 ∈ V ↦ 𝑑𝑐 Pred ( 𝑅 , 𝐴 , 𝑑 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑘 ) Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝐵 )
64 63 adantl ( ( 𝑘 ∈ ω ∧ ( ( ( 𝑋𝐴𝑅 Se 𝐴 ) ∧ ( ∀ 𝑦𝐵 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝐵 ∧ Pred ( 𝑅 , 𝐴 , 𝑋 ) ⊆ 𝐵 ) ) ∧ ( ( rec ( ( 𝑐 ∈ V ↦ 𝑑𝑐 Pred ( 𝑅 , 𝐴 , 𝑑 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑘 ) ⊆ 𝐵 ) ) → ∀ 𝑦 ∈ ( ( rec ( ( 𝑐 ∈ V ↦ 𝑑𝑐 Pred ( 𝑅 , 𝐴 , 𝑑 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑘 ) Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝐵 )
65 51 64 sylan2b ( ( 𝑘 ∈ ω ∧ ( ( ( 𝑋𝐴𝑅 Se 𝐴 ) ∧ ( ∀ 𝑦𝐵 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝐵 ∧ Pred ( 𝑅 , 𝐴 , 𝑋 ) ⊆ 𝐵 ) ) ∧ ( ( rec ( ( 𝑎 ∈ V ↦ 𝑦𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑘 ) ⊆ 𝐵 ) ) → ∀ 𝑦 ∈ ( ( rec ( ( 𝑐 ∈ V ↦ 𝑑𝑐 Pred ( 𝑅 , 𝐴 , 𝑑 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑘 ) Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝐵 )
66 iunss ( 𝑦 ∈ ( ( rec ( ( 𝑐 ∈ V ↦ 𝑑𝑐 Pred ( 𝑅 , 𝐴 , 𝑑 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑘 ) Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝐵 ↔ ∀ 𝑦 ∈ ( ( rec ( ( 𝑐 ∈ V ↦ 𝑑𝑐 Pred ( 𝑅 , 𝐴 , 𝑑 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑘 ) Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝐵 )
67 65 66 sylibr ( ( 𝑘 ∈ ω ∧ ( ( ( 𝑋𝐴𝑅 Se 𝐴 ) ∧ ( ∀ 𝑦𝐵 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝐵 ∧ Pred ( 𝑅 , 𝐴 , 𝑋 ) ⊆ 𝐵 ) ) ∧ ( ( rec ( ( 𝑎 ∈ V ↦ 𝑦𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑘 ) ⊆ 𝐵 ) ) → 𝑦 ∈ ( ( rec ( ( 𝑐 ∈ V ↦ 𝑑𝑐 Pred ( 𝑅 , 𝐴 , 𝑑 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑘 ) Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝐵 )
68 49 67 eqsstrd ( ( 𝑘 ∈ ω ∧ ( ( ( 𝑋𝐴𝑅 Se 𝐴 ) ∧ ( ∀ 𝑦𝐵 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝐵 ∧ Pred ( 𝑅 , 𝐴 , 𝑋 ) ⊆ 𝐵 ) ) ∧ ( ( rec ( ( 𝑎 ∈ V ↦ 𝑦𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑘 ) ⊆ 𝐵 ) ) → ( ( rec ( ( 𝑎 ∈ V ↦ 𝑦𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ suc 𝑘 ) ⊆ 𝐵 )
69 68 exp32 ( 𝑘 ∈ ω → ( ( ( 𝑋𝐴𝑅 Se 𝐴 ) ∧ ( ∀ 𝑦𝐵 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝐵 ∧ Pred ( 𝑅 , 𝐴 , 𝑋 ) ⊆ 𝐵 ) ) → ( ( ( rec ( ( 𝑎 ∈ V ↦ 𝑦𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑘 ) ⊆ 𝐵 → ( ( rec ( ( 𝑎 ∈ V ↦ 𝑦𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ suc 𝑘 ) ⊆ 𝐵 ) ) )
70 69 a2d ( 𝑘 ∈ ω → ( ( ( ( 𝑋𝐴𝑅 Se 𝐴 ) ∧ ( ∀ 𝑦𝐵 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝐵 ∧ Pred ( 𝑅 , 𝐴 , 𝑋 ) ⊆ 𝐵 ) ) → ( ( rec ( ( 𝑎 ∈ V ↦ 𝑦𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑘 ) ⊆ 𝐵 ) → ( ( ( 𝑋𝐴𝑅 Se 𝐴 ) ∧ ( ∀ 𝑦𝐵 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝐵 ∧ Pred ( 𝑅 , 𝐴 , 𝑋 ) ⊆ 𝐵 ) ) → ( ( rec ( ( 𝑎 ∈ V ↦ 𝑦𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ suc 𝑘 ) ⊆ 𝐵 ) ) )
71 4 7 10 13 19 70 finds ( 𝑖 ∈ ω → ( ( ( 𝑋𝐴𝑅 Se 𝐴 ) ∧ ( ∀ 𝑦𝐵 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝐵 ∧ Pred ( 𝑅 , 𝐴 , 𝑋 ) ⊆ 𝐵 ) ) → ( ( rec ( ( 𝑎 ∈ V ↦ 𝑦𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑖 ) ⊆ 𝐵 ) )
72 71 com12 ( ( ( 𝑋𝐴𝑅 Se 𝐴 ) ∧ ( ∀ 𝑦𝐵 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝐵 ∧ Pred ( 𝑅 , 𝐴 , 𝑋 ) ⊆ 𝐵 ) ) → ( 𝑖 ∈ ω → ( ( rec ( ( 𝑎 ∈ V ↦ 𝑦𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑖 ) ⊆ 𝐵 ) )
73 72 ralrimiv ( ( ( 𝑋𝐴𝑅 Se 𝐴 ) ∧ ( ∀ 𝑦𝐵 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝐵 ∧ Pred ( 𝑅 , 𝐴 , 𝑋 ) ⊆ 𝐵 ) ) → ∀ 𝑖 ∈ ω ( ( rec ( ( 𝑎 ∈ V ↦ 𝑦𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑖 ) ⊆ 𝐵 )
74 iunss ( 𝑖 ∈ ω ( ( rec ( ( 𝑎 ∈ V ↦ 𝑦𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑖 ) ⊆ 𝐵 ↔ ∀ 𝑖 ∈ ω ( ( rec ( ( 𝑎 ∈ V ↦ 𝑦𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑖 ) ⊆ 𝐵 )
75 73 74 sylibr ( ( ( 𝑋𝐴𝑅 Se 𝐴 ) ∧ ( ∀ 𝑦𝐵 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝐵 ∧ Pred ( 𝑅 , 𝐴 , 𝑋 ) ⊆ 𝐵 ) ) → 𝑖 ∈ ω ( ( rec ( ( 𝑎 ∈ V ↦ 𝑦𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑖 ) ⊆ 𝐵 )
76 1 75 eqsstrid ( ( ( 𝑋𝐴𝑅 Se 𝐴 ) ∧ ( ∀ 𝑦𝐵 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝐵 ∧ Pred ( 𝑅 , 𝐴 , 𝑋 ) ⊆ 𝐵 ) ) → TrPred ( 𝑅 , 𝐴 , 𝑋 ) ⊆ 𝐵 )