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 eqabri ⊢ ( 𝑥 ∈ 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 imbitrrdi ⊢ ( ( 𝑛 ∈ ω ∧ ( ( 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 ( 𝑅 , 𝐴 ) “ ω ) )