Metamath Proof Explorer


Theorem dffi3

Description: The set of finite intersections can be "constructed" inductively by iterating binary intersection _om -many times. (Contributed by Mario Carneiro, 21-Mar-2015)

Ref Expression
Hypothesis dffi3.1 𝑅 = ( 𝑢 ∈ V ↦ ran ( 𝑦𝑢 , 𝑧𝑢 ↦ ( 𝑦𝑧 ) ) )
Assertion dffi3 ( 𝐴𝑉 → ( fi ‘ 𝐴 ) = ( rec ( 𝑅 , 𝐴 ) “ ω ) )

Proof

Step Hyp Ref Expression
1 dffi3.1 𝑅 = ( 𝑢 ∈ V ↦ ran ( 𝑦𝑢 , 𝑧𝑢 ↦ ( 𝑦𝑧 ) ) )
2 dffi2 ( 𝐴𝑉 → ( fi ‘ 𝐴 ) = { 𝑥 ∣ ( 𝐴𝑥 ∧ ∀ 𝑐𝑥𝑑𝑥 ( 𝑐𝑑 ) ∈ 𝑥 ) } )
3 fr0g ( 𝐴𝑉 → ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ∅ ) = 𝐴 )
4 frfnom ( rec ( 𝑅 , 𝐴 ) ↾ ω ) Fn ω
5 peano1 ∅ ∈ ω
6 fnfvelrn ( ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) Fn ω ∧ ∅ ∈ ω ) → ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ∅ ) ∈ ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) )
7 4 5 6 mp2an ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ∅ ) ∈ ran ( rec ( 𝑅 , 𝐴 ) ↾ ω )
8 3 7 eqeltrrdi ( 𝐴𝑉𝐴 ∈ ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) )
9 elssuni ( 𝐴 ∈ ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) → 𝐴 ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) )
10 8 9 syl ( 𝐴𝑉𝐴 ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) )
11 reeanv ( ∃ 𝑚 ∈ ω ∃ 𝑛 ∈ ω ( 𝑐 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑚 ) ∧ 𝑑 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ) ↔ ( ∃ 𝑚 ∈ ω 𝑐 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑚 ) ∧ ∃ 𝑛 ∈ ω 𝑑 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ) )
12 eliun ( 𝑐 𝑚 ∈ ω ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑚 ) ↔ ∃ 𝑚 ∈ ω 𝑐 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑚 ) )
13 eliun ( 𝑑 𝑛 ∈ ω ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ↔ ∃ 𝑛 ∈ ω 𝑑 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) )
14 12 13 anbi12i ( ( 𝑐 𝑚 ∈ ω ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑚 ) ∧ 𝑑 𝑛 ∈ ω ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ) ↔ ( ∃ 𝑚 ∈ ω 𝑐 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑚 ) ∧ ∃ 𝑛 ∈ ω 𝑑 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ) )
15 fniunfv ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) Fn ω → 𝑚 ∈ ω ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑚 ) = ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) )
16 15 eleq2d ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) Fn ω → ( 𝑐 𝑚 ∈ ω ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑚 ) ↔ 𝑐 ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ) )
17 fniunfv ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) Fn ω → 𝑛 ∈ ω ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) = ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) )
18 17 eleq2d ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) Fn ω → ( 𝑑 𝑛 ∈ ω ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ↔ 𝑑 ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ) )
19 16 18 anbi12d ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) Fn ω → ( ( 𝑐 𝑚 ∈ ω ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑚 ) ∧ 𝑑 𝑛 ∈ ω ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ) ↔ ( 𝑐 ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ∧ 𝑑 ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ) ) )
20 4 19 ax-mp ( ( 𝑐 𝑚 ∈ ω ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑚 ) ∧ 𝑑 𝑛 ∈ ω ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ) ↔ ( 𝑐 ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ∧ 𝑑 ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ) )
21 11 14 20 3bitr2i ( ∃ 𝑚 ∈ ω ∃ 𝑛 ∈ ω ( 𝑐 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑚 ) ∧ 𝑑 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ) ↔ ( 𝑐 ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ∧ 𝑑 ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ) )
22 ordom Ord ω
23 ordunel ( ( Ord ω ∧ 𝑚 ∈ ω ∧ 𝑛 ∈ ω ) → ( 𝑚𝑛 ) ∈ ω )
24 22 23 mp3an1 ( ( 𝑚 ∈ ω ∧ 𝑛 ∈ ω ) → ( 𝑚𝑛 ) ∈ ω )
25 24 adantl ( ( 𝐴𝑉 ∧ ( 𝑚 ∈ ω ∧ 𝑛 ∈ ω ) ) → ( 𝑚𝑛 ) ∈ ω )
26 simprl ( ( 𝐴𝑉 ∧ ( 𝑚 ∈ ω ∧ 𝑛 ∈ ω ) ) → 𝑚 ∈ ω )
27 25 26 jca ( ( 𝐴𝑉 ∧ ( 𝑚 ∈ ω ∧ 𝑛 ∈ ω ) ) → ( ( 𝑚𝑛 ) ∈ ω ∧ 𝑚 ∈ ω ) )
28 nnon ( 𝑦 ∈ ω → 𝑦 ∈ On )
29 nnon ( 𝑥 ∈ ω → 𝑥 ∈ On )
30 29 ad2antlr ( ( ( 𝐴𝑉𝑥 ∈ ω ) ∧ 𝑦 ∈ ω ) → 𝑥 ∈ On )
31 onsseleq ( ( 𝑦 ∈ On ∧ 𝑥 ∈ On ) → ( 𝑦𝑥 ↔ ( 𝑦𝑥𝑦 = 𝑥 ) ) )
32 28 30 31 syl2an2 ( ( ( 𝐴𝑉𝑥 ∈ ω ) ∧ 𝑦 ∈ ω ) → ( 𝑦𝑥 ↔ ( 𝑦𝑥𝑦 = 𝑥 ) ) )
33 rzal ( 𝑥 = ∅ → ∀ 𝑦𝑥 ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑥 ) )
34 33 biantrud ( 𝑥 = ∅ → ( ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑥 ) ⊆ ( fi ‘ 𝐴 ) ↔ ( ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑥 ) ⊆ ( fi ‘ 𝐴 ) ∧ ∀ 𝑦𝑥 ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑥 ) ) ) )
35 fveq2 ( 𝑥 = ∅ → ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑥 ) = ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ∅ ) )
36 35 sseq1d ( 𝑥 = ∅ → ( ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑥 ) ⊆ ( fi ‘ 𝐴 ) ↔ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ∅ ) ⊆ ( fi ‘ 𝐴 ) ) )
37 34 36 bitr3d ( 𝑥 = ∅ → ( ( ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑥 ) ⊆ ( fi ‘ 𝐴 ) ∧ ∀ 𝑦𝑥 ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑥 ) ) ↔ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ∅ ) ⊆ ( fi ‘ 𝐴 ) ) )
38 fveq2 ( 𝑥 = 𝑛 → ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑥 ) = ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) )
39 38 sseq1d ( 𝑥 = 𝑛 → ( ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑥 ) ⊆ ( fi ‘ 𝐴 ) ↔ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ⊆ ( fi ‘ 𝐴 ) ) )
40 38 sseq2d ( 𝑥 = 𝑛 → ( ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑥 ) ↔ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ) )
41 40 raleqbi1dv ( 𝑥 = 𝑛 → ( ∀ 𝑦𝑥 ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑥 ) ↔ ∀ 𝑦𝑛 ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ) )
42 39 41 anbi12d ( 𝑥 = 𝑛 → ( ( ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑥 ) ⊆ ( fi ‘ 𝐴 ) ∧ ∀ 𝑦𝑥 ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑥 ) ) ↔ ( ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ⊆ ( fi ‘ 𝐴 ) ∧ ∀ 𝑦𝑛 ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ) ) )
43 fveq2 ( 𝑥 = suc 𝑛 → ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑥 ) = ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ suc 𝑛 ) )
44 43 sseq1d ( 𝑥 = suc 𝑛 → ( ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑥 ) ⊆ ( fi ‘ 𝐴 ) ↔ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ suc 𝑛 ) ⊆ ( fi ‘ 𝐴 ) ) )
45 43 sseq2d ( 𝑥 = suc 𝑛 → ( ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑥 ) ↔ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ suc 𝑛 ) ) )
46 45 raleqbi1dv ( 𝑥 = suc 𝑛 → ( ∀ 𝑦𝑥 ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑥 ) ↔ ∀ 𝑦 ∈ suc 𝑛 ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ suc 𝑛 ) ) )
47 44 46 anbi12d ( 𝑥 = suc 𝑛 → ( ( ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑥 ) ⊆ ( fi ‘ 𝐴 ) ∧ ∀ 𝑦𝑥 ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑥 ) ) ↔ ( ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ suc 𝑛 ) ⊆ ( fi ‘ 𝐴 ) ∧ ∀ 𝑦 ∈ suc 𝑛 ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ suc 𝑛 ) ) ) )
48 ssfii ( 𝐴𝑉𝐴 ⊆ ( fi ‘ 𝐴 ) )
49 3 48 eqsstrd ( 𝐴𝑉 → ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ∅ ) ⊆ ( fi ‘ 𝐴 ) )
50 id ( 𝑥 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) → 𝑥 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) )
51 eqidd ( 𝑥 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) → 𝑥 = 𝑥 )
52 ineq1 ( 𝑎 = 𝑥 → ( 𝑎𝑏 ) = ( 𝑥𝑏 ) )
53 52 eqeq2d ( 𝑎 = 𝑥 → ( 𝑥 = ( 𝑎𝑏 ) ↔ 𝑥 = ( 𝑥𝑏 ) ) )
54 ineq2 ( 𝑏 = 𝑥 → ( 𝑥𝑏 ) = ( 𝑥𝑥 ) )
55 inidm ( 𝑥𝑥 ) = 𝑥
56 54 55 eqtrdi ( 𝑏 = 𝑥 → ( 𝑥𝑏 ) = 𝑥 )
57 56 eqeq2d ( 𝑏 = 𝑥 → ( 𝑥 = ( 𝑥𝑏 ) ↔ 𝑥 = 𝑥 ) )
58 53 57 rspc2ev ( ( 𝑥 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ∧ 𝑥 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ∧ 𝑥 = 𝑥 ) → ∃ 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ∃ 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) 𝑥 = ( 𝑎𝑏 ) )
59 50 50 51 58 syl3anc ( 𝑥 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) → ∃ 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ∃ 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) 𝑥 = ( 𝑎𝑏 ) )
60 eqid ( 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) , 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ↦ ( 𝑎𝑏 ) ) = ( 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) , 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ↦ ( 𝑎𝑏 ) )
61 60 rnmpo ran ( 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) , 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ↦ ( 𝑎𝑏 ) ) = { 𝑥 ∣ ∃ 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ∃ 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) 𝑥 = ( 𝑎𝑏 ) }
62 61 abeq2i ( 𝑥 ∈ ran ( 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) , 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ↦ ( 𝑎𝑏 ) ) ↔ ∃ 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ∃ 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) 𝑥 = ( 𝑎𝑏 ) )
63 59 62 sylibr ( 𝑥 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) → 𝑥 ∈ ran ( 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) , 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ↦ ( 𝑎𝑏 ) ) )
64 63 ssriv ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ⊆ ran ( 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) , 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ↦ ( 𝑎𝑏 ) )
65 simpl ( ( 𝑛 ∈ ω ∧ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ⊆ ( fi ‘ 𝐴 ) ) → 𝑛 ∈ ω )
66 fvex ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ∈ V
67 66 uniex ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ∈ V
68 67 pwex 𝒫 ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ∈ V
69 inss1 ( 𝑎𝑏 ) ⊆ 𝑎
70 elssuni ( 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) → 𝑎 ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) )
71 70 adantr ( ( 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ∧ 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ) → 𝑎 ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) )
72 69 71 sstrid ( ( 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ∧ 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ) → ( 𝑎𝑏 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) )
73 vex 𝑎 ∈ V
74 73 inex1 ( 𝑎𝑏 ) ∈ V
75 74 elpw ( ( 𝑎𝑏 ) ∈ 𝒫 ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ↔ ( 𝑎𝑏 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) )
76 72 75 sylibr ( ( 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ∧ 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ) → ( 𝑎𝑏 ) ∈ 𝒫 ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) )
77 76 rgen2 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ∀ 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ( 𝑎𝑏 ) ∈ 𝒫 ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 )
78 60 fmpo ( ∀ 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ∀ 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ( 𝑎𝑏 ) ∈ 𝒫 ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ↔ ( 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) , 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ↦ ( 𝑎𝑏 ) ) : ( ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) × ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ) ⟶ 𝒫 ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) )
79 77 78 mpbi ( 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) , 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ↦ ( 𝑎𝑏 ) ) : ( ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) × ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ) ⟶ 𝒫 ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 )
80 frn ( ( 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) , 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ↦ ( 𝑎𝑏 ) ) : ( ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) × ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ) ⟶ 𝒫 ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) → ran ( 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) , 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ↦ ( 𝑎𝑏 ) ) ⊆ 𝒫 ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) )
81 79 80 ax-mp ran ( 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) , 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ↦ ( 𝑎𝑏 ) ) ⊆ 𝒫 ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 )
82 68 81 ssexi ran ( 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) , 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ↦ ( 𝑎𝑏 ) ) ∈ V
83 nfcv 𝑣 𝐴
84 nfcv 𝑣 𝑛
85 nfcv 𝑣 ran ( 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) , 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ↦ ( 𝑎𝑏 ) )
86 mpoeq12 ( ( 𝑢 = 𝑣𝑢 = 𝑣 ) → ( 𝑦𝑢 , 𝑧𝑢 ↦ ( 𝑦𝑧 ) ) = ( 𝑦𝑣 , 𝑧𝑣 ↦ ( 𝑦𝑧 ) ) )
87 86 anidms ( 𝑢 = 𝑣 → ( 𝑦𝑢 , 𝑧𝑢 ↦ ( 𝑦𝑧 ) ) = ( 𝑦𝑣 , 𝑧𝑣 ↦ ( 𝑦𝑧 ) ) )
88 ineq1 ( 𝑦 = 𝑎 → ( 𝑦𝑧 ) = ( 𝑎𝑧 ) )
89 ineq2 ( 𝑧 = 𝑏 → ( 𝑎𝑧 ) = ( 𝑎𝑏 ) )
90 88 89 cbvmpov ( 𝑦𝑣 , 𝑧𝑣 ↦ ( 𝑦𝑧 ) ) = ( 𝑎𝑣 , 𝑏𝑣 ↦ ( 𝑎𝑏 ) )
91 87 90 eqtrdi ( 𝑢 = 𝑣 → ( 𝑦𝑢 , 𝑧𝑢 ↦ ( 𝑦𝑧 ) ) = ( 𝑎𝑣 , 𝑏𝑣 ↦ ( 𝑎𝑏 ) ) )
92 91 rneqd ( 𝑢 = 𝑣 → ran ( 𝑦𝑢 , 𝑧𝑢 ↦ ( 𝑦𝑧 ) ) = ran ( 𝑎𝑣 , 𝑏𝑣 ↦ ( 𝑎𝑏 ) ) )
93 92 cbvmptv ( 𝑢 ∈ V ↦ ran ( 𝑦𝑢 , 𝑧𝑢 ↦ ( 𝑦𝑧 ) ) ) = ( 𝑣 ∈ V ↦ ran ( 𝑎𝑣 , 𝑏𝑣 ↦ ( 𝑎𝑏 ) ) )
94 1 93 eqtri 𝑅 = ( 𝑣 ∈ V ↦ ran ( 𝑎𝑣 , 𝑏𝑣 ↦ ( 𝑎𝑏 ) ) )
95 rdgeq1 ( 𝑅 = ( 𝑣 ∈ V ↦ ran ( 𝑎𝑣 , 𝑏𝑣 ↦ ( 𝑎𝑏 ) ) ) → rec ( 𝑅 , 𝐴 ) = rec ( ( 𝑣 ∈ V ↦ ran ( 𝑎𝑣 , 𝑏𝑣 ↦ ( 𝑎𝑏 ) ) ) , 𝐴 ) )
96 94 95 ax-mp rec ( 𝑅 , 𝐴 ) = rec ( ( 𝑣 ∈ V ↦ ran ( 𝑎𝑣 , 𝑏𝑣 ↦ ( 𝑎𝑏 ) ) ) , 𝐴 )
97 96 reseq1i ( rec ( 𝑅 , 𝐴 ) ↾ ω ) = ( rec ( ( 𝑣 ∈ V ↦ ran ( 𝑎𝑣 , 𝑏𝑣 ↦ ( 𝑎𝑏 ) ) ) , 𝐴 ) ↾ ω )
98 mpoeq12 ( ( 𝑣 = ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ∧ 𝑣 = ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ) → ( 𝑎𝑣 , 𝑏𝑣 ↦ ( 𝑎𝑏 ) ) = ( 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) , 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ↦ ( 𝑎𝑏 ) ) )
99 98 anidms ( 𝑣 = ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) → ( 𝑎𝑣 , 𝑏𝑣 ↦ ( 𝑎𝑏 ) ) = ( 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) , 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ↦ ( 𝑎𝑏 ) ) )
100 99 rneqd ( 𝑣 = ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) → ran ( 𝑎𝑣 , 𝑏𝑣 ↦ ( 𝑎𝑏 ) ) = ran ( 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) , 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ↦ ( 𝑎𝑏 ) ) )
101 83 84 85 97 100 frsucmpt ( ( 𝑛 ∈ ω ∧ ran ( 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) , 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ↦ ( 𝑎𝑏 ) ) ∈ V ) → ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ suc 𝑛 ) = ran ( 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) , 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ↦ ( 𝑎𝑏 ) ) )
102 65 82 101 sylancl ( ( 𝑛 ∈ ω ∧ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ⊆ ( fi ‘ 𝐴 ) ) → ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ suc 𝑛 ) = ran ( 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) , 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ↦ ( 𝑎𝑏 ) ) )
103 64 102 sseqtrrid ( ( 𝑛 ∈ ω ∧ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ⊆ ( fi ‘ 𝐴 ) ) → ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ suc 𝑛 ) )
104 sstr2 ( ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) → ( ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ suc 𝑛 ) → ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ suc 𝑛 ) ) )
105 103 104 syl5com ( ( 𝑛 ∈ ω ∧ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ⊆ ( fi ‘ 𝐴 ) ) → ( ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) → ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ suc 𝑛 ) ) )
106 105 ralimdv ( ( 𝑛 ∈ ω ∧ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ⊆ ( fi ‘ 𝐴 ) ) → ( ∀ 𝑦𝑛 ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) → ∀ 𝑦𝑛 ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ suc 𝑛 ) ) )
107 vex 𝑛 ∈ V
108 fveq2 ( 𝑦 = 𝑛 → ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) = ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) )
109 108 sseq1d ( 𝑦 = 𝑛 → ( ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ suc 𝑛 ) ↔ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ suc 𝑛 ) ) )
110 107 109 ralsn ( ∀ 𝑦 ∈ { 𝑛 } ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ suc 𝑛 ) ↔ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ suc 𝑛 ) )
111 103 110 sylibr ( ( 𝑛 ∈ ω ∧ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ⊆ ( fi ‘ 𝐴 ) ) → ∀ 𝑦 ∈ { 𝑛 } ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ suc 𝑛 ) )
112 106 111 jctird ( ( 𝑛 ∈ ω ∧ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ⊆ ( fi ‘ 𝐴 ) ) → ( ∀ 𝑦𝑛 ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) → ( ∀ 𝑦𝑛 ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ suc 𝑛 ) ∧ ∀ 𝑦 ∈ { 𝑛 } ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ suc 𝑛 ) ) ) )
113 df-suc suc 𝑛 = ( 𝑛 ∪ { 𝑛 } )
114 113 raleqi ( ∀ 𝑦 ∈ suc 𝑛 ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ suc 𝑛 ) ↔ ∀ 𝑦 ∈ ( 𝑛 ∪ { 𝑛 } ) ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ suc 𝑛 ) )
115 ralunb ( ∀ 𝑦 ∈ ( 𝑛 ∪ { 𝑛 } ) ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ suc 𝑛 ) ↔ ( ∀ 𝑦𝑛 ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ suc 𝑛 ) ∧ ∀ 𝑦 ∈ { 𝑛 } ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ suc 𝑛 ) ) )
116 114 115 bitri ( ∀ 𝑦 ∈ suc 𝑛 ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ suc 𝑛 ) ↔ ( ∀ 𝑦𝑛 ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ suc 𝑛 ) ∧ ∀ 𝑦 ∈ { 𝑛 } ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ suc 𝑛 ) ) )
117 112 116 syl6ibr ( ( 𝑛 ∈ ω ∧ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ⊆ ( fi ‘ 𝐴 ) ) → ( ∀ 𝑦𝑛 ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) → ∀ 𝑦 ∈ suc 𝑛 ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ suc 𝑛 ) ) )
118 fiin ( ( 𝑎 ∈ ( fi ‘ 𝐴 ) ∧ 𝑏 ∈ ( fi ‘ 𝐴 ) ) → ( 𝑎𝑏 ) ∈ ( fi ‘ 𝐴 ) )
119 118 rgen2 𝑎 ∈ ( fi ‘ 𝐴 ) ∀ 𝑏 ∈ ( fi ‘ 𝐴 ) ( 𝑎𝑏 ) ∈ ( fi ‘ 𝐴 )
120 ss2ralv ( ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ⊆ ( fi ‘ 𝐴 ) → ( ∀ 𝑎 ∈ ( fi ‘ 𝐴 ) ∀ 𝑏 ∈ ( fi ‘ 𝐴 ) ( 𝑎𝑏 ) ∈ ( fi ‘ 𝐴 ) → ∀ 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ∀ 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ( 𝑎𝑏 ) ∈ ( fi ‘ 𝐴 ) ) )
121 119 120 mpi ( ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ⊆ ( fi ‘ 𝐴 ) → ∀ 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ∀ 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ( 𝑎𝑏 ) ∈ ( fi ‘ 𝐴 ) )
122 60 fmpo ( ∀ 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ∀ 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ( 𝑎𝑏 ) ∈ ( fi ‘ 𝐴 ) ↔ ( 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) , 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ↦ ( 𝑎𝑏 ) ) : ( ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) × ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ) ⟶ ( fi ‘ 𝐴 ) )
123 121 122 sylib ( ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ⊆ ( fi ‘ 𝐴 ) → ( 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) , 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ↦ ( 𝑎𝑏 ) ) : ( ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) × ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ) ⟶ ( fi ‘ 𝐴 ) )
124 123 frnd ( ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ⊆ ( fi ‘ 𝐴 ) → ran ( 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) , 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ↦ ( 𝑎𝑏 ) ) ⊆ ( fi ‘ 𝐴 ) )
125 124 adantl ( ( 𝑛 ∈ ω ∧ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ⊆ ( fi ‘ 𝐴 ) ) → ran ( 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) , 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ↦ ( 𝑎𝑏 ) ) ⊆ ( fi ‘ 𝐴 ) )
126 102 125 eqsstrd ( ( 𝑛 ∈ ω ∧ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ⊆ ( fi ‘ 𝐴 ) ) → ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ suc 𝑛 ) ⊆ ( fi ‘ 𝐴 ) )
127 117 126 jctild ( ( 𝑛 ∈ ω ∧ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ⊆ ( fi ‘ 𝐴 ) ) → ( ∀ 𝑦𝑛 ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) → ( ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ suc 𝑛 ) ⊆ ( fi ‘ 𝐴 ) ∧ ∀ 𝑦 ∈ suc 𝑛 ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ suc 𝑛 ) ) ) )
128 127 expimpd ( 𝑛 ∈ ω → ( ( ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ⊆ ( fi ‘ 𝐴 ) ∧ ∀ 𝑦𝑛 ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ) → ( ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ suc 𝑛 ) ⊆ ( fi ‘ 𝐴 ) ∧ ∀ 𝑦 ∈ suc 𝑛 ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ suc 𝑛 ) ) ) )
129 128 a1d ( 𝑛 ∈ ω → ( 𝐴𝑉 → ( ( ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ⊆ ( fi ‘ 𝐴 ) ∧ ∀ 𝑦𝑛 ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ) → ( ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ suc 𝑛 ) ⊆ ( fi ‘ 𝐴 ) ∧ ∀ 𝑦 ∈ suc 𝑛 ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ suc 𝑛 ) ) ) ) )
130 37 42 47 49 129 finds2 ( 𝑥 ∈ ω → ( 𝐴𝑉 → ( ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑥 ) ⊆ ( fi ‘ 𝐴 ) ∧ ∀ 𝑦𝑥 ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑥 ) ) ) )
131 130 impcom ( ( 𝐴𝑉𝑥 ∈ ω ) → ( ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑥 ) ⊆ ( fi ‘ 𝐴 ) ∧ ∀ 𝑦𝑥 ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑥 ) ) )
132 131 simprd ( ( 𝐴𝑉𝑥 ∈ ω ) → ∀ 𝑦𝑥 ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑥 ) )
133 132 r19.21bi ( ( ( 𝐴𝑉𝑥 ∈ ω ) ∧ 𝑦𝑥 ) → ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑥 ) )
134 133 ex ( ( 𝐴𝑉𝑥 ∈ ω ) → ( 𝑦𝑥 → ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑥 ) ) )
135 134 adantr ( ( ( 𝐴𝑉𝑥 ∈ ω ) ∧ 𝑦 ∈ ω ) → ( 𝑦𝑥 → ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑥 ) ) )
136 fveq2 ( 𝑦 = 𝑥 → ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) = ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑥 ) )
137 eqimss ( ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) = ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑥 ) → ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑥 ) )
138 136 137 syl ( 𝑦 = 𝑥 → ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑥 ) )
139 138 a1i ( ( ( 𝐴𝑉𝑥 ∈ ω ) ∧ 𝑦 ∈ ω ) → ( 𝑦 = 𝑥 → ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑥 ) ) )
140 135 139 jaod ( ( ( 𝐴𝑉𝑥 ∈ ω ) ∧ 𝑦 ∈ ω ) → ( ( 𝑦𝑥𝑦 = 𝑥 ) → ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑥 ) ) )
141 32 140 sylbid ( ( ( 𝐴𝑉𝑥 ∈ ω ) ∧ 𝑦 ∈ ω ) → ( 𝑦𝑥 → ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑥 ) ) )
142 141 ralrimiva ( ( 𝐴𝑉𝑥 ∈ ω ) → ∀ 𝑦 ∈ ω ( 𝑦𝑥 → ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑥 ) ) )
143 142 ralrimiva ( 𝐴𝑉 → ∀ 𝑥 ∈ ω ∀ 𝑦 ∈ ω ( 𝑦𝑥 → ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑥 ) ) )
144 143 adantr ( ( 𝐴𝑉 ∧ ( 𝑚 ∈ ω ∧ 𝑛 ∈ ω ) ) → ∀ 𝑥 ∈ ω ∀ 𝑦 ∈ ω ( 𝑦𝑥 → ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑥 ) ) )
145 ssun1 𝑚 ⊆ ( 𝑚𝑛 )
146 145 a1i ( ( 𝐴𝑉 ∧ ( 𝑚 ∈ ω ∧ 𝑛 ∈ ω ) ) → 𝑚 ⊆ ( 𝑚𝑛 ) )
147 sseq2 ( 𝑥 = ( 𝑚𝑛 ) → ( 𝑦𝑥𝑦 ⊆ ( 𝑚𝑛 ) ) )
148 fveq2 ( 𝑥 = ( 𝑚𝑛 ) → ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑥 ) = ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) )
149 148 sseq2d ( 𝑥 = ( 𝑚𝑛 ) → ( ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑥 ) ↔ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) ) )
150 147 149 imbi12d ( 𝑥 = ( 𝑚𝑛 ) → ( ( 𝑦𝑥 → ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑥 ) ) ↔ ( 𝑦 ⊆ ( 𝑚𝑛 ) → ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) ) ) )
151 sseq1 ( 𝑦 = 𝑚 → ( 𝑦 ⊆ ( 𝑚𝑛 ) ↔ 𝑚 ⊆ ( 𝑚𝑛 ) ) )
152 fveq2 ( 𝑦 = 𝑚 → ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) = ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑚 ) )
153 152 sseq1d ( 𝑦 = 𝑚 → ( ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) ↔ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑚 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) ) )
154 151 153 imbi12d ( 𝑦 = 𝑚 → ( ( 𝑦 ⊆ ( 𝑚𝑛 ) → ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) ) ↔ ( 𝑚 ⊆ ( 𝑚𝑛 ) → ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑚 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) ) ) )
155 150 154 rspc2v ( ( ( 𝑚𝑛 ) ∈ ω ∧ 𝑚 ∈ ω ) → ( ∀ 𝑥 ∈ ω ∀ 𝑦 ∈ ω ( 𝑦𝑥 → ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑥 ) ) → ( 𝑚 ⊆ ( 𝑚𝑛 ) → ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑚 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) ) ) )
156 27 144 146 155 syl3c ( ( 𝐴𝑉 ∧ ( 𝑚 ∈ ω ∧ 𝑛 ∈ ω ) ) → ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑚 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) )
157 156 sseld ( ( 𝐴𝑉 ∧ ( 𝑚 ∈ ω ∧ 𝑛 ∈ ω ) ) → ( 𝑐 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑚 ) → 𝑐 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) ) )
158 simprr ( ( 𝐴𝑉 ∧ ( 𝑚 ∈ ω ∧ 𝑛 ∈ ω ) ) → 𝑛 ∈ ω )
159 25 158 jca ( ( 𝐴𝑉 ∧ ( 𝑚 ∈ ω ∧ 𝑛 ∈ ω ) ) → ( ( 𝑚𝑛 ) ∈ ω ∧ 𝑛 ∈ ω ) )
160 ssun2 𝑛 ⊆ ( 𝑚𝑛 )
161 160 a1i ( ( 𝐴𝑉 ∧ ( 𝑚 ∈ ω ∧ 𝑛 ∈ ω ) ) → 𝑛 ⊆ ( 𝑚𝑛 ) )
162 sseq1 ( 𝑦 = 𝑛 → ( 𝑦 ⊆ ( 𝑚𝑛 ) ↔ 𝑛 ⊆ ( 𝑚𝑛 ) ) )
163 108 sseq1d ( 𝑦 = 𝑛 → ( ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) ↔ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) ) )
164 162 163 imbi12d ( 𝑦 = 𝑛 → ( ( 𝑦 ⊆ ( 𝑚𝑛 ) → ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) ) ↔ ( 𝑛 ⊆ ( 𝑚𝑛 ) → ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) ) ) )
165 150 164 rspc2v ( ( ( 𝑚𝑛 ) ∈ ω ∧ 𝑛 ∈ ω ) → ( ∀ 𝑥 ∈ ω ∀ 𝑦 ∈ ω ( 𝑦𝑥 → ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑥 ) ) → ( 𝑛 ⊆ ( 𝑚𝑛 ) → ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) ) ) )
166 159 144 161 165 syl3c ( ( 𝐴𝑉 ∧ ( 𝑚 ∈ ω ∧ 𝑛 ∈ ω ) ) → ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) )
167 166 sseld ( ( 𝐴𝑉 ∧ ( 𝑚 ∈ ω ∧ 𝑛 ∈ ω ) ) → ( 𝑑 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) → 𝑑 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) ) )
168 24 ad2antlr ( ( ( 𝐴𝑉 ∧ ( 𝑚 ∈ ω ∧ 𝑛 ∈ ω ) ) ∧ ( 𝑐 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) ∧ 𝑑 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) ) ) → ( 𝑚𝑛 ) ∈ ω )
169 peano2 ( ( 𝑚𝑛 ) ∈ ω → suc ( 𝑚𝑛 ) ∈ ω )
170 fveq2 ( 𝑥 = suc ( 𝑚𝑛 ) → ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑥 ) = ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ suc ( 𝑚𝑛 ) ) )
171 170 ssiun2s ( suc ( 𝑚𝑛 ) ∈ ω → ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ suc ( 𝑚𝑛 ) ) ⊆ 𝑥 ∈ ω ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑥 ) )
172 168 169 171 3syl ( ( ( 𝐴𝑉 ∧ ( 𝑚 ∈ ω ∧ 𝑛 ∈ ω ) ) ∧ ( 𝑐 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) ∧ 𝑑 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) ) ) → ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ suc ( 𝑚𝑛 ) ) ⊆ 𝑥 ∈ ω ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑥 ) )
173 simprl ( ( ( 𝐴𝑉 ∧ ( 𝑚 ∈ ω ∧ 𝑛 ∈ ω ) ) ∧ ( 𝑐 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) ∧ 𝑑 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) ) ) → 𝑐 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) )
174 simprr ( ( ( 𝐴𝑉 ∧ ( 𝑚 ∈ ω ∧ 𝑛 ∈ ω ) ) ∧ ( 𝑐 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) ∧ 𝑑 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) ) ) → 𝑑 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) )
175 eqidd ( ( ( 𝐴𝑉 ∧ ( 𝑚 ∈ ω ∧ 𝑛 ∈ ω ) ) ∧ ( 𝑐 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) ∧ 𝑑 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) ) ) → ( 𝑐𝑑 ) = ( 𝑐𝑑 ) )
176 ineq1 ( 𝑎 = 𝑐 → ( 𝑎𝑏 ) = ( 𝑐𝑏 ) )
177 176 eqeq2d ( 𝑎 = 𝑐 → ( ( 𝑐𝑑 ) = ( 𝑎𝑏 ) ↔ ( 𝑐𝑑 ) = ( 𝑐𝑏 ) ) )
178 ineq2 ( 𝑏 = 𝑑 → ( 𝑐𝑏 ) = ( 𝑐𝑑 ) )
179 178 eqeq2d ( 𝑏 = 𝑑 → ( ( 𝑐𝑑 ) = ( 𝑐𝑏 ) ↔ ( 𝑐𝑑 ) = ( 𝑐𝑑 ) ) )
180 177 179 rspc2ev ( ( 𝑐 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) ∧ 𝑑 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) ∧ ( 𝑐𝑑 ) = ( 𝑐𝑑 ) ) → ∃ 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) ∃ 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) ( 𝑐𝑑 ) = ( 𝑎𝑏 ) )
181 173 174 175 180 syl3anc ( ( ( 𝐴𝑉 ∧ ( 𝑚 ∈ ω ∧ 𝑛 ∈ ω ) ) ∧ ( 𝑐 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) ∧ 𝑑 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) ) ) → ∃ 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) ∃ 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) ( 𝑐𝑑 ) = ( 𝑎𝑏 ) )
182 vex 𝑐 ∈ V
183 182 inex1 ( 𝑐𝑑 ) ∈ V
184 eqeq1 ( 𝑥 = ( 𝑐𝑑 ) → ( 𝑥 = ( 𝑎𝑏 ) ↔ ( 𝑐𝑑 ) = ( 𝑎𝑏 ) ) )
185 184 2rexbidv ( 𝑥 = ( 𝑐𝑑 ) → ( ∃ 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) ∃ 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) 𝑥 = ( 𝑎𝑏 ) ↔ ∃ 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) ∃ 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) ( 𝑐𝑑 ) = ( 𝑎𝑏 ) ) )
186 183 185 elab ( ( 𝑐𝑑 ) ∈ { 𝑥 ∣ ∃ 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) ∃ 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) 𝑥 = ( 𝑎𝑏 ) } ↔ ∃ 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) ∃ 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) ( 𝑐𝑑 ) = ( 𝑎𝑏 ) )
187 181 186 sylibr ( ( ( 𝐴𝑉 ∧ ( 𝑚 ∈ ω ∧ 𝑛 ∈ ω ) ) ∧ ( 𝑐 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) ∧ 𝑑 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) ) ) → ( 𝑐𝑑 ) ∈ { 𝑥 ∣ ∃ 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) ∃ 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) 𝑥 = ( 𝑎𝑏 ) } )
188 eqid ( 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) , 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) ↦ ( 𝑎𝑏 ) ) = ( 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) , 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) ↦ ( 𝑎𝑏 ) )
189 188 rnmpo ran ( 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) , 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) ↦ ( 𝑎𝑏 ) ) = { 𝑥 ∣ ∃ 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) ∃ 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) 𝑥 = ( 𝑎𝑏 ) }
190 187 189 eleqtrrdi ( ( ( 𝐴𝑉 ∧ ( 𝑚 ∈ ω ∧ 𝑛 ∈ ω ) ) ∧ ( 𝑐 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) ∧ 𝑑 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) ) ) → ( 𝑐𝑑 ) ∈ ran ( 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) , 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) ↦ ( 𝑎𝑏 ) ) )
191 fvex ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) ∈ V
192 191 uniex ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) ∈ V
193 192 pwex 𝒫 ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) ∈ V
194 elssuni ( 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) → 𝑎 ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) )
195 69 194 sstrid ( 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) → ( 𝑎𝑏 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) )
196 74 elpw ( ( 𝑎𝑏 ) ∈ 𝒫 ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) ↔ ( 𝑎𝑏 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) )
197 195 196 sylibr ( 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) → ( 𝑎𝑏 ) ∈ 𝒫 ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) )
198 197 adantr ( ( 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) ∧ 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) ) → ( 𝑎𝑏 ) ∈ 𝒫 ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) )
199 198 rgen2 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) ∀ 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) ( 𝑎𝑏 ) ∈ 𝒫 ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) )
200 188 fmpo ( ∀ 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) ∀ 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) ( 𝑎𝑏 ) ∈ 𝒫 ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) ↔ ( 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) , 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) ↦ ( 𝑎𝑏 ) ) : ( ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) × ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) ) ⟶ 𝒫 ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) )
201 199 200 mpbi ( 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) , 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) ↦ ( 𝑎𝑏 ) ) : ( ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) × ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) ) ⟶ 𝒫 ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) )
202 frn ( ( 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) , 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) ↦ ( 𝑎𝑏 ) ) : ( ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) × ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) ) ⟶ 𝒫 ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) → ran ( 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) , 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) ↦ ( 𝑎𝑏 ) ) ⊆ 𝒫 ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) )
203 201 202 ax-mp ran ( 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) , 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) ↦ ( 𝑎𝑏 ) ) ⊆ 𝒫 ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) )
204 193 203 ssexi ran ( 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) , 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) ↦ ( 𝑎𝑏 ) ) ∈ V
205 nfcv 𝑣 ( 𝑚𝑛 )
206 nfcv 𝑣 ran ( 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) , 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) ↦ ( 𝑎𝑏 ) )
207 mpoeq12 ( ( 𝑣 = ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) ∧ 𝑣 = ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) ) → ( 𝑎𝑣 , 𝑏𝑣 ↦ ( 𝑎𝑏 ) ) = ( 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) , 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) ↦ ( 𝑎𝑏 ) ) )
208 207 anidms ( 𝑣 = ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) → ( 𝑎𝑣 , 𝑏𝑣 ↦ ( 𝑎𝑏 ) ) = ( 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) , 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) ↦ ( 𝑎𝑏 ) ) )
209 208 rneqd ( 𝑣 = ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) → ran ( 𝑎𝑣 , 𝑏𝑣 ↦ ( 𝑎𝑏 ) ) = ran ( 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) , 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) ↦ ( 𝑎𝑏 ) ) )
210 83 205 206 97 209 frsucmpt ( ( ( 𝑚𝑛 ) ∈ ω ∧ ran ( 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) , 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) ↦ ( 𝑎𝑏 ) ) ∈ V ) → ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ suc ( 𝑚𝑛 ) ) = ran ( 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) , 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) ↦ ( 𝑎𝑏 ) ) )
211 168 204 210 sylancl ( ( ( 𝐴𝑉 ∧ ( 𝑚 ∈ ω ∧ 𝑛 ∈ ω ) ) ∧ ( 𝑐 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) ∧ 𝑑 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) ) ) → ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ suc ( 𝑚𝑛 ) ) = ran ( 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) , 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) ↦ ( 𝑎𝑏 ) ) )
212 190 211 eleqtrrd ( ( ( 𝐴𝑉 ∧ ( 𝑚 ∈ ω ∧ 𝑛 ∈ ω ) ) ∧ ( 𝑐 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) ∧ 𝑑 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) ) ) → ( 𝑐𝑑 ) ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ suc ( 𝑚𝑛 ) ) )
213 172 212 sseldd ( ( ( 𝐴𝑉 ∧ ( 𝑚 ∈ ω ∧ 𝑛 ∈ ω ) ) ∧ ( 𝑐 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) ∧ 𝑑 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) ) ) → ( 𝑐𝑑 ) ∈ 𝑥 ∈ ω ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑥 ) )
214 fniunfv ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) Fn ω → 𝑥 ∈ ω ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑥 ) = ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) )
215 4 214 ax-mp 𝑥 ∈ ω ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑥 ) = ran ( rec ( 𝑅 , 𝐴 ) ↾ ω )
216 213 215 eleqtrdi ( ( ( 𝐴𝑉 ∧ ( 𝑚 ∈ ω ∧ 𝑛 ∈ ω ) ) ∧ ( 𝑐 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) ∧ 𝑑 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) ) ) → ( 𝑐𝑑 ) ∈ ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) )
217 216 ex ( ( 𝐴𝑉 ∧ ( 𝑚 ∈ ω ∧ 𝑛 ∈ ω ) ) → ( ( 𝑐 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) ∧ 𝑑 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚𝑛 ) ) ) → ( 𝑐𝑑 ) ∈ ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ) )
218 157 167 217 syl2and ( ( 𝐴𝑉 ∧ ( 𝑚 ∈ ω ∧ 𝑛 ∈ ω ) ) → ( ( 𝑐 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑚 ) ∧ 𝑑 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ) → ( 𝑐𝑑 ) ∈ ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ) )
219 218 rexlimdvva ( 𝐴𝑉 → ( ∃ 𝑚 ∈ ω ∃ 𝑛 ∈ ω ( 𝑐 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑚 ) ∧ 𝑑 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ) → ( 𝑐𝑑 ) ∈ ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ) )
220 219 imp ( ( 𝐴𝑉 ∧ ∃ 𝑚 ∈ ω ∃ 𝑛 ∈ ω ( 𝑐 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑚 ) ∧ 𝑑 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ) ) → ( 𝑐𝑑 ) ∈ ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) )
221 21 220 sylan2br ( ( 𝐴𝑉 ∧ ( 𝑐 ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ∧ 𝑑 ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ) ) → ( 𝑐𝑑 ) ∈ ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) )
222 221 ralrimivva ( 𝐴𝑉 → ∀ 𝑐 ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ∀ 𝑑 ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ( 𝑐𝑑 ) ∈ ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) )
223 131 simpld ( ( 𝐴𝑉𝑥 ∈ ω ) → ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑥 ) ⊆ ( fi ‘ 𝐴 ) )
224 fvex ( fi ‘ 𝐴 ) ∈ V
225 224 elpw2 ( ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑥 ) ∈ 𝒫 ( fi ‘ 𝐴 ) ↔ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑥 ) ⊆ ( fi ‘ 𝐴 ) )
226 223 225 sylibr ( ( 𝐴𝑉𝑥 ∈ ω ) → ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑥 ) ∈ 𝒫 ( fi ‘ 𝐴 ) )
227 226 ralrimiva ( 𝐴𝑉 → ∀ 𝑥 ∈ ω ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑥 ) ∈ 𝒫 ( fi ‘ 𝐴 ) )
228 fnfvrnss ( ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) Fn ω ∧ ∀ 𝑥 ∈ ω ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑥 ) ∈ 𝒫 ( fi ‘ 𝐴 ) ) → ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ⊆ 𝒫 ( fi ‘ 𝐴 ) )
229 4 227 228 sylancr ( 𝐴𝑉 → ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ⊆ 𝒫 ( fi ‘ 𝐴 ) )
230 sspwuni ( ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ⊆ 𝒫 ( fi ‘ 𝐴 ) ↔ ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ⊆ ( fi ‘ 𝐴 ) )
231 229 230 sylib ( 𝐴𝑉 ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ⊆ ( fi ‘ 𝐴 ) )
232 ssexg ( ( ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ⊆ ( fi ‘ 𝐴 ) ∧ ( fi ‘ 𝐴 ) ∈ V ) → ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ∈ V )
233 231 224 232 sylancl ( 𝐴𝑉 ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ∈ V )
234 sseq2 ( 𝑥 = ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) → ( 𝐴𝑥𝐴 ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ) )
235 eleq2 ( 𝑥 = ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) → ( ( 𝑐𝑑 ) ∈ 𝑥 ↔ ( 𝑐𝑑 ) ∈ ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ) )
236 235 raleqbi1dv ( 𝑥 = ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) → ( ∀ 𝑑𝑥 ( 𝑐𝑑 ) ∈ 𝑥 ↔ ∀ 𝑑 ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ( 𝑐𝑑 ) ∈ ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ) )
237 236 raleqbi1dv ( 𝑥 = ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) → ( ∀ 𝑐𝑥𝑑𝑥 ( 𝑐𝑑 ) ∈ 𝑥 ↔ ∀ 𝑐 ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ∀ 𝑑 ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ( 𝑐𝑑 ) ∈ ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ) )
238 234 237 anbi12d ( 𝑥 = ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) → ( ( 𝐴𝑥 ∧ ∀ 𝑐𝑥𝑑𝑥 ( 𝑐𝑑 ) ∈ 𝑥 ) ↔ ( 𝐴 ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ∧ ∀ 𝑐 ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ∀ 𝑑 ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ( 𝑐𝑑 ) ∈ ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ) ) )
239 238 elabg ( ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ∈ V → ( ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ∈ { 𝑥 ∣ ( 𝐴𝑥 ∧ ∀ 𝑐𝑥𝑑𝑥 ( 𝑐𝑑 ) ∈ 𝑥 ) } ↔ ( 𝐴 ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ∧ ∀ 𝑐 ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ∀ 𝑑 ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ( 𝑐𝑑 ) ∈ ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ) ) )
240 233 239 syl ( 𝐴𝑉 → ( ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ∈ { 𝑥 ∣ ( 𝐴𝑥 ∧ ∀ 𝑐𝑥𝑑𝑥 ( 𝑐𝑑 ) ∈ 𝑥 ) } ↔ ( 𝐴 ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ∧ ∀ 𝑐 ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ∀ 𝑑 ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ( 𝑐𝑑 ) ∈ ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ) ) )
241 10 222 240 mpbir2and ( 𝐴𝑉 ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ∈ { 𝑥 ∣ ( 𝐴𝑥 ∧ ∀ 𝑐𝑥𝑑𝑥 ( 𝑐𝑑 ) ∈ 𝑥 ) } )
242 intss1 ( ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ∈ { 𝑥 ∣ ( 𝐴𝑥 ∧ ∀ 𝑐𝑥𝑑𝑥 ( 𝑐𝑑 ) ∈ 𝑥 ) } → { 𝑥 ∣ ( 𝐴𝑥 ∧ ∀ 𝑐𝑥𝑑𝑥 ( 𝑐𝑑 ) ∈ 𝑥 ) } ⊆ ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) )
243 241 242 syl ( 𝐴𝑉 { 𝑥 ∣ ( 𝐴𝑥 ∧ ∀ 𝑐𝑥𝑑𝑥 ( 𝑐𝑑 ) ∈ 𝑥 ) } ⊆ ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) )
244 2 243 eqsstrd ( 𝐴𝑉 → ( fi ‘ 𝐴 ) ⊆ ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) )
245 244 231 eqssd ( 𝐴𝑉 → ( fi ‘ 𝐴 ) = ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) )
246 df-ima ( rec ( 𝑅 , 𝐴 ) “ ω ) = ran ( rec ( 𝑅 , 𝐴 ) ↾ ω )
247 246 unieqi ( rec ( 𝑅 , 𝐴 ) “ ω ) = ran ( rec ( 𝑅 , 𝐴 ) ↾ ω )
248 245 247 eqtr4di ( 𝐴𝑉 → ( fi ‘ 𝐴 ) = ( rec ( 𝑅 , 𝐴 ) “ ω ) )