Metamath Proof Explorer

Theorem dftrpred3g

Description: The transitive predecessors of X are equal to the predecessors of X together with their transitive predecessors. (Contributed by Scott Fenton, 26-Apr-2012) (Revised by Mario Carneiro, 26-Jun-2015)

Ref Expression
Assertion dftrpred3g ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) → TrPred ( 𝑅 , 𝐴 , 𝑋 ) = ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ∪ ∪ 𝑦 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) TrPred ( 𝑅 , 𝐴 , 𝑦 ) ) )

Proof

Step Hyp Ref Expression
1 elun ⊢ ( 𝑧 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ∪ ∪ 𝑦 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) TrPred ( 𝑅 , 𝐴 , 𝑦 ) ) ↔ ( 𝑧 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) ∨ 𝑧 ∈ ∪ 𝑦 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) TrPred ( 𝑅 , 𝐴 , 𝑦 ) ) )
2 predel ⊢ ( 𝑧 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) → 𝑧 ∈ 𝐴 )
3 setlikespec ⊢ ( ( 𝑧 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) → Pred ( 𝑅 , 𝐴 , 𝑧 ) ∈ V )
4 trpredpred ⊢ ( Pred ( 𝑅 , 𝐴 , 𝑧 ) ∈ V → Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ TrPred ( 𝑅 , 𝐴 , 𝑧 ) )
5 3 4 syl ⊢ ( ( 𝑧 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) → Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ TrPred ( 𝑅 , 𝐴 , 𝑧 ) )
6 5 expcom ⊢ ( 𝑅 Se 𝐴 → ( 𝑧 ∈ 𝐴 → Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ TrPred ( 𝑅 , 𝐴 , 𝑧 ) ) )
7 6 adantl ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) → ( 𝑧 ∈ 𝐴 → Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ TrPred ( 𝑅 , 𝐴 , 𝑧 ) ) )
8 2 7 syl5 ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) → ( 𝑧 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) → Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ TrPred ( 𝑅 , 𝐴 , 𝑧 ) ) )
9 8 ancld ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) → ( 𝑧 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) → ( 𝑧 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) ∧ Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ TrPred ( 𝑅 , 𝐴 , 𝑧 ) ) ) )
10 trpredeq3 ⊢ ( 𝑦 = 𝑧 → TrPred ( 𝑅 , 𝐴 , 𝑦 ) = TrPred ( 𝑅 , 𝐴 , 𝑧 ) )
11 10 sseq2d ⊢ ( 𝑦 = 𝑧 → ( Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ TrPred ( 𝑅 , 𝐴 , 𝑦 ) ↔ Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ TrPred ( 𝑅 , 𝐴 , 𝑧 ) ) )
12 11 rspcev ⊢ ( ( 𝑧 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) ∧ Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ TrPred ( 𝑅 , 𝐴 , 𝑧 ) ) → ∃ 𝑦 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ TrPred ( 𝑅 , 𝐴 , 𝑦 ) )
13 ssiun ⊢ ( ∃ 𝑦 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ TrPred ( 𝑅 , 𝐴 , 𝑦 ) → Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ ∪ 𝑦 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) TrPred ( 𝑅 , 𝐴 , 𝑦 ) )
14 12 13 syl ⊢ ( ( 𝑧 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) ∧ Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ TrPred ( 𝑅 , 𝐴 , 𝑧 ) ) → Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ ∪ 𝑦 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) TrPred ( 𝑅 , 𝐴 , 𝑦 ) )
15 9 14 syl6 ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) → ( 𝑧 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) → Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ ∪ 𝑦 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) TrPred ( 𝑅 , 𝐴 , 𝑦 ) ) )
16 eliun ⊢ ( 𝑧 ∈ ∪ 𝑦 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) TrPred ( 𝑅 , 𝐴 , 𝑦 ) ↔ ∃ 𝑦 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) 𝑧 ∈ TrPred ( 𝑅 , 𝐴 , 𝑦 ) )
17 predel ⊢ ( 𝑦 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) → 𝑦 ∈ 𝐴 )
18 setlikespec ⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) → Pred ( 𝑅 , 𝐴 , 𝑦 ) ∈ V )
19 18 ancoms ⊢ ( ( 𝑅 Se 𝐴 ∧ 𝑦 ∈ 𝐴 ) → Pred ( 𝑅 , 𝐴 , 𝑦 ) ∈ V )
20 19 adantll ⊢ ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) → Pred ( 𝑅 , 𝐴 , 𝑦 ) ∈ V )
21 trpredss ⊢ ( Pred ( 𝑅 , 𝐴 , 𝑦 ) ∈ V → TrPred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝐴 )
22 20 21 syl ⊢ ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) → TrPred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝐴 )
23 22 sseld ⊢ ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) → ( 𝑧 ∈ TrPred ( 𝑅 , 𝐴 , 𝑦 ) → 𝑧 ∈ 𝐴 ) )
24 3 expcom ⊢ ( 𝑅 Se 𝐴 → ( 𝑧 ∈ 𝐴 → Pred ( 𝑅 , 𝐴 , 𝑧 ) ∈ V ) )
25 24 ad2antlr ⊢ ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) → ( 𝑧 ∈ 𝐴 → Pred ( 𝑅 , 𝐴 , 𝑧 ) ∈ V ) )
26 23 25 syld ⊢ ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) → ( 𝑧 ∈ TrPred ( 𝑅 , 𝐴 , 𝑦 ) → Pred ( 𝑅 , 𝐴 , 𝑧 ) ∈ V ) )
27 26 imp ⊢ ( ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑧 ∈ TrPred ( 𝑅 , 𝐴 , 𝑦 ) ) → Pred ( 𝑅 , 𝐴 , 𝑧 ) ∈ V )
28 27 4 syl ⊢ ( ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑧 ∈ TrPred ( 𝑅 , 𝐴 , 𝑦 ) ) → Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ TrPred ( 𝑅 , 𝐴 , 𝑧 ) )
29 simpr ⊢ ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ∈ 𝐴 )
30 simplr ⊢ ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) → 𝑅 Se 𝐴 )
31 trpredelss ⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) → ( 𝑧 ∈ TrPred ( 𝑅 , 𝐴 , 𝑦 ) → TrPred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ TrPred ( 𝑅 , 𝐴 , 𝑦 ) ) )
32 29 30 31 syl2anc ⊢ ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) → ( 𝑧 ∈ TrPred ( 𝑅 , 𝐴 , 𝑦 ) → TrPred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ TrPred ( 𝑅 , 𝐴 , 𝑦 ) ) )
33 32 imp ⊢ ( ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑧 ∈ TrPred ( 𝑅 , 𝐴 , 𝑦 ) ) → TrPred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ TrPred ( 𝑅 , 𝐴 , 𝑦 ) )
34 28 33 sstrd ⊢ ( ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑧 ∈ TrPred ( 𝑅 , 𝐴 , 𝑦 ) ) → Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ TrPred ( 𝑅 , 𝐴 , 𝑦 ) )
35 34 exp31 ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) → ( 𝑦 ∈ 𝐴 → ( 𝑧 ∈ TrPred ( 𝑅 , 𝐴 , 𝑦 ) → Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ TrPred ( 𝑅 , 𝐴 , 𝑦 ) ) ) )
36 17 35 syl5 ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) → ( 𝑦 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) → ( 𝑧 ∈ TrPred ( 𝑅 , 𝐴 , 𝑦 ) → Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ TrPred ( 𝑅 , 𝐴 , 𝑦 ) ) ) )
37 36 reximdvai ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) → ( ∃ 𝑦 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) 𝑧 ∈ TrPred ( 𝑅 , 𝐴 , 𝑦 ) → ∃ 𝑦 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ TrPred ( 𝑅 , 𝐴 , 𝑦 ) ) )
38 37 13 syl6 ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) → ( ∃ 𝑦 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) 𝑧 ∈ TrPred ( 𝑅 , 𝐴 , 𝑦 ) → Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ ∪ 𝑦 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) TrPred ( 𝑅 , 𝐴 , 𝑦 ) ) )
39 16 38 syl5bi ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) → ( 𝑧 ∈ ∪ 𝑦 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) TrPred ( 𝑅 , 𝐴 , 𝑦 ) → Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ ∪ 𝑦 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) TrPred ( 𝑅 , 𝐴 , 𝑦 ) ) )
40 15 39 jaod ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) → ( ( 𝑧 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) ∨ 𝑧 ∈ ∪ 𝑦 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) TrPred ( 𝑅 , 𝐴 , 𝑦 ) ) → Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ ∪ 𝑦 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) TrPred ( 𝑅 , 𝐴 , 𝑦 ) ) )
41 ssun4 ⊢ ( Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ ∪ 𝑦 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) TrPred ( 𝑅 , 𝐴 , 𝑦 ) → Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ∪ ∪ 𝑦 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) TrPred ( 𝑅 , 𝐴 , 𝑦 ) ) )
42 40 41 syl6 ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) → ( ( 𝑧 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) ∨ 𝑧 ∈ ∪ 𝑦 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) TrPred ( 𝑅 , 𝐴 , 𝑦 ) ) → Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ∪ ∪ 𝑦 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) TrPred ( 𝑅 , 𝐴 , 𝑦 ) ) ) )
43 1 42 syl5bi ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) → ( 𝑧 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ∪ ∪ 𝑦 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) TrPred ( 𝑅 , 𝐴 , 𝑦 ) ) → Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ∪ ∪ 𝑦 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) TrPred ( 𝑅 , 𝐴 , 𝑦 ) ) ) )
44 43 ralrimiv ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) → ∀ 𝑧 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ∪ ∪ 𝑦 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) TrPred ( 𝑅 , 𝐴 , 𝑦 ) ) Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ∪ ∪ 𝑦 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) TrPred ( 𝑅 , 𝐴 , 𝑦 ) ) )
45 ssun1 ⊢ Pred ( 𝑅 , 𝐴 , 𝑋 ) ⊆ ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ∪ ∪ 𝑦 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) TrPred ( 𝑅 , 𝐴 , 𝑦 ) )
46 44 45 jctir ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) → ( ∀ 𝑧 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ∪ ∪ 𝑦 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) TrPred ( 𝑅 , 𝐴 , 𝑦 ) ) Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ∪ ∪ 𝑦 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) TrPred ( 𝑅 , 𝐴 , 𝑦 ) ) ∧ Pred ( 𝑅 , 𝐴 , 𝑋 ) ⊆ ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ∪ ∪ 𝑦 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) TrPred ( 𝑅 , 𝐴 , 𝑦 ) ) ) )
47 trpredmintr ⊢ ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( ∀ 𝑧 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ∪ ∪ 𝑦 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) TrPred ( 𝑅 , 𝐴 , 𝑦 ) ) Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ∪ ∪ 𝑦 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) TrPred ( 𝑅 , 𝐴 , 𝑦 ) ) ∧ Pred ( 𝑅 , 𝐴 , 𝑋 ) ⊆ ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ∪ ∪ 𝑦 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) TrPred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) → TrPred ( 𝑅 , 𝐴 , 𝑋 ) ⊆ ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ∪ ∪ 𝑦 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) TrPred ( 𝑅 , 𝐴 , 𝑦 ) ) )
48 46 47 mpdan ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) → TrPred ( 𝑅 , 𝐴 , 𝑋 ) ⊆ ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ∪ ∪ 𝑦 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) TrPred ( 𝑅 , 𝐴 , 𝑦 ) ) )
49 setlikespec ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) → Pred ( 𝑅 , 𝐴 , 𝑋 ) ∈ V )
50 trpredpred ⊢ ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ∈ V → Pred ( 𝑅 , 𝐴 , 𝑋 ) ⊆ TrPred ( 𝑅 , 𝐴 , 𝑋 ) )
51 49 50 syl ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) → Pred ( 𝑅 , 𝐴 , 𝑋 ) ⊆ TrPred ( 𝑅 , 𝐴 , 𝑋 ) )
52 51 sseld ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) → ( 𝑦 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) → 𝑦 ∈ TrPred ( 𝑅 , 𝐴 , 𝑋 ) ) )
53 trpredelss ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) → ( 𝑦 ∈ TrPred ( 𝑅 , 𝐴 , 𝑋 ) → TrPred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ TrPred ( 𝑅 , 𝐴 , 𝑋 ) ) )
54 52 53 syld ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) → ( 𝑦 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) → TrPred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ TrPred ( 𝑅 , 𝐴 , 𝑋 ) ) )
55 54 ralrimiv ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) → ∀ 𝑦 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) TrPred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ TrPred ( 𝑅 , 𝐴 , 𝑋 ) )
56 iunss ⊢ ( ∪ 𝑦 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) TrPred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ TrPred ( 𝑅 , 𝐴 , 𝑋 ) ↔ ∀ 𝑦 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) TrPred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ TrPred ( 𝑅 , 𝐴 , 𝑋 ) )
57 55 56 sylibr ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) → ∪ 𝑦 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) TrPred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ TrPred ( 𝑅 , 𝐴 , 𝑋 ) )
58 51 57 unssd ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) → ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ∪ ∪ 𝑦 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) TrPred ( 𝑅 , 𝐴 , 𝑦 ) ) ⊆ TrPred ( 𝑅 , 𝐴 , 𝑋 ) )
59 48 58 eqssd ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴 ) → TrPred ( 𝑅 , 𝐴 , 𝑋 ) = ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ∪ ∪ 𝑦 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) TrPred ( 𝑅 , 𝐴 , 𝑦 ) ) )