Theorem trpredmintr

Description: The transitive predecessors form the smallest class transitive in R and A . That is, if B is another R , A transitive class containing Pred ( R , A , X ) , then TrPred ( R , A , X ) C_ B (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	syl5eq	⊢ ( 𝑎 = 𝑐 → ∪ 𝑦 ∈ 𝑎 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 ( 𝑅 , 𝐴 , 𝑋 ) ⊆ 𝐵 )