MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dffi3 Structured version   Visualization version   GIF version

Theorem dffi3 8493
Description: The set of finite intersections can be "constructed" inductively by iterating binary intersection ω-many times. (Contributed by Mario Carneiro, 21-Mar-2015.)
Hypothesis
Ref Expression
dffi3.1 𝑅 = (𝑢 ∈ V ↦ ran (𝑦𝑢, 𝑧𝑢 ↦ (𝑦𝑧)))
Assertion
Ref Expression
dffi3 (𝐴𝑉 → (fi‘𝐴) = (rec(𝑅, 𝐴) “ ω))
Distinct variable groups:   𝑦,𝐴   𝑦,𝑅   𝑦,𝑉   𝑦,𝑢,𝑧
Allowed substitution hints:   𝐴(𝑧,𝑢)   𝑅(𝑧,𝑢)   𝑉(𝑧,𝑢)

Proof of Theorem dffi3
Dummy variables 𝑎 𝑏 𝑐 𝑑 𝑚 𝑛 𝑣 𝑥 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dffi2 8485 . . . 4 (𝐴𝑉 → (fi‘𝐴) = {𝑥 ∣ (𝐴𝑥 ∧ ∀𝑐𝑥𝑑𝑥 (𝑐𝑑) ∈ 𝑥)})
2 fr0g 7684 . . . . . . . 8 (𝐴𝑉 → ((rec(𝑅, 𝐴) ↾ ω)‘∅) = 𝐴)
3 frfnom 7683 . . . . . . . . 9 (rec(𝑅, 𝐴) ↾ ω) Fn ω
4 peano1 7232 . . . . . . . . 9 ∅ ∈ ω
5 fnfvelrn 6499 . . . . . . . . 9 (((rec(𝑅, 𝐴) ↾ ω) Fn ω ∧ ∅ ∈ ω) → ((rec(𝑅, 𝐴) ↾ ω)‘∅) ∈ ran (rec(𝑅, 𝐴) ↾ ω))
63, 4, 5mp2an 672 . . . . . . . 8 ((rec(𝑅, 𝐴) ↾ ω)‘∅) ∈ ran (rec(𝑅, 𝐴) ↾ ω)
72, 6syl6eqelr 2859 . . . . . . 7 (𝐴𝑉𝐴 ∈ ran (rec(𝑅, 𝐴) ↾ ω))
8 elssuni 4603 . . . . . . 7 (𝐴 ∈ ran (rec(𝑅, 𝐴) ↾ ω) → 𝐴 ran (rec(𝑅, 𝐴) ↾ ω))
97, 8syl 17 . . . . . 6 (𝐴𝑉𝐴 ran (rec(𝑅, 𝐴) ↾ ω))
10 reeanv 3255 . . . . . . . . 9 (∃𝑚 ∈ ω ∃𝑛 ∈ ω (𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑚) ∧ 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)) ↔ (∃𝑚 ∈ ω 𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑚) ∧ ∃𝑛 ∈ ω 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)))
11 eliun 4658 . . . . . . . . . 10 (𝑐 𝑚 ∈ ω ((rec(𝑅, 𝐴) ↾ ω)‘𝑚) ↔ ∃𝑚 ∈ ω 𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑚))
12 eliun 4658 . . . . . . . . . 10 (𝑑 𝑛 ∈ ω ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↔ ∃𝑛 ∈ ω 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛))
1311, 12anbi12i 612 . . . . . . . . 9 ((𝑐 𝑚 ∈ ω ((rec(𝑅, 𝐴) ↾ ω)‘𝑚) ∧ 𝑑 𝑛 ∈ ω ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)) ↔ (∃𝑚 ∈ ω 𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑚) ∧ ∃𝑛 ∈ ω 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)))
14 fniunfv 6648 . . . . . . . . . . . 12 ((rec(𝑅, 𝐴) ↾ ω) Fn ω → 𝑚 ∈ ω ((rec(𝑅, 𝐴) ↾ ω)‘𝑚) = ran (rec(𝑅, 𝐴) ↾ ω))
1514eleq2d 2836 . . . . . . . . . . 11 ((rec(𝑅, 𝐴) ↾ ω) Fn ω → (𝑐 𝑚 ∈ ω ((rec(𝑅, 𝐴) ↾ ω)‘𝑚) ↔ 𝑐 ran (rec(𝑅, 𝐴) ↾ ω)))
16 fniunfv 6648 . . . . . . . . . . . 12 ((rec(𝑅, 𝐴) ↾ ω) Fn ω → 𝑛 ∈ ω ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) = ran (rec(𝑅, 𝐴) ↾ ω))
1716eleq2d 2836 . . . . . . . . . . 11 ((rec(𝑅, 𝐴) ↾ ω) Fn ω → (𝑑 𝑛 ∈ ω ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↔ 𝑑 ran (rec(𝑅, 𝐴) ↾ ω)))
1815, 17anbi12d 616 . . . . . . . . . 10 ((rec(𝑅, 𝐴) ↾ ω) Fn ω → ((𝑐 𝑚 ∈ ω ((rec(𝑅, 𝐴) ↾ ω)‘𝑚) ∧ 𝑑 𝑛 ∈ ω ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)) ↔ (𝑐 ran (rec(𝑅, 𝐴) ↾ ω) ∧ 𝑑 ran (rec(𝑅, 𝐴) ↾ ω))))
193, 18ax-mp 5 . . . . . . . . 9 ((𝑐 𝑚 ∈ ω ((rec(𝑅, 𝐴) ↾ ω)‘𝑚) ∧ 𝑑 𝑛 ∈ ω ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)) ↔ (𝑐 ran (rec(𝑅, 𝐴) ↾ ω) ∧ 𝑑 ran (rec(𝑅, 𝐴) ↾ ω)))
2010, 13, 193bitr2i 288 . . . . . . . 8 (∃𝑚 ∈ ω ∃𝑛 ∈ ω (𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑚) ∧ 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)) ↔ (𝑐 ran (rec(𝑅, 𝐴) ↾ ω) ∧ 𝑑 ran (rec(𝑅, 𝐴) ↾ ω)))
21 ordom 7221 . . . . . . . . . . . . . . . 16 Ord ω
22 ordunel 7174 . . . . . . . . . . . . . . . 16 ((Ord ω ∧ 𝑚 ∈ ω ∧ 𝑛 ∈ ω) → (𝑚𝑛) ∈ ω)
2321, 22mp3an1 1559 . . . . . . . . . . . . . . 15 ((𝑚 ∈ ω ∧ 𝑛 ∈ ω) → (𝑚𝑛) ∈ ω)
2423adantl 467 . . . . . . . . . . . . . 14 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) → (𝑚𝑛) ∈ ω)
25 simprl 754 . . . . . . . . . . . . . 14 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) → 𝑚 ∈ ω)
2624, 25jca 501 . . . . . . . . . . . . 13 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) → ((𝑚𝑛) ∈ ω ∧ 𝑚 ∈ ω))
27 nnon 7218 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ ω → 𝑦 ∈ On)
2827adantl 467 . . . . . . . . . . . . . . . . . 18 (((𝐴𝑉𝑥 ∈ ω) ∧ 𝑦 ∈ ω) → 𝑦 ∈ On)
29 nnon 7218 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ω → 𝑥 ∈ On)
3029ad2antlr 706 . . . . . . . . . . . . . . . . . 18 (((𝐴𝑉𝑥 ∈ ω) ∧ 𝑦 ∈ ω) → 𝑥 ∈ On)
31 onsseleq 5908 . . . . . . . . . . . . . . . . . 18 ((𝑦 ∈ On ∧ 𝑥 ∈ On) → (𝑦𝑥 ↔ (𝑦𝑥𝑦 = 𝑥)))
3228, 30, 31syl2anc 573 . . . . . . . . . . . . . . . . 17 (((𝐴𝑉𝑥 ∈ ω) ∧ 𝑦 ∈ ω) → (𝑦𝑥 ↔ (𝑦𝑥𝑦 = 𝑥)))
33 rzal 4214 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 = ∅ → ∀𝑦𝑥 ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥))
3433biantrud 521 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = ∅ → (((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ⊆ (fi‘𝐴) ↔ (((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ⊆ (fi‘𝐴) ∧ ∀𝑦𝑥 ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥))))
35 fveq2 6332 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 = ∅ → ((rec(𝑅, 𝐴) ↾ ω)‘𝑥) = ((rec(𝑅, 𝐴) ↾ ω)‘∅))
3635sseq1d 3781 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = ∅ → (((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ⊆ (fi‘𝐴) ↔ ((rec(𝑅, 𝐴) ↾ ω)‘∅) ⊆ (fi‘𝐴)))
3734, 36bitr3d 270 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = ∅ → ((((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ⊆ (fi‘𝐴) ∧ ∀𝑦𝑥 ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥)) ↔ ((rec(𝑅, 𝐴) ↾ ω)‘∅) ⊆ (fi‘𝐴)))
38 fveq2 6332 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 = 𝑛 → ((rec(𝑅, 𝐴) ↾ ω)‘𝑥) = ((rec(𝑅, 𝐴) ↾ ω)‘𝑛))
3938sseq1d 3781 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = 𝑛 → (((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ⊆ (fi‘𝐴) ↔ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ (fi‘𝐴)))
4038sseq2d 3782 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 = 𝑛 → (((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ↔ ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)))
4140raleqbi1dv 3295 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = 𝑛 → (∀𝑦𝑥 ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ↔ ∀𝑦𝑛 ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)))
4239, 41anbi12d 616 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = 𝑛 → ((((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ⊆ (fi‘𝐴) ∧ ∀𝑦𝑥 ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥)) ↔ (((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ (fi‘𝐴) ∧ ∀𝑦𝑛 ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛))))
43 fveq2 6332 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 = suc 𝑛 → ((rec(𝑅, 𝐴) ↾ ω)‘𝑥) = ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛))
4443sseq1d 3781 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = suc 𝑛 → (((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ⊆ (fi‘𝐴) ↔ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛) ⊆ (fi‘𝐴)))
4543sseq2d 3782 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 = suc 𝑛 → (((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ↔ ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛)))
4645raleqbi1dv 3295 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = suc 𝑛 → (∀𝑦𝑥 ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ↔ ∀𝑦 ∈ suc 𝑛((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛)))
4744, 46anbi12d 616 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = suc 𝑛 → ((((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ⊆ (fi‘𝐴) ∧ ∀𝑦𝑥 ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥)) ↔ (((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛) ⊆ (fi‘𝐴) ∧ ∀𝑦 ∈ suc 𝑛((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛))))
48 ssfii 8481 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐴𝑉𝐴 ⊆ (fi‘𝐴))
492, 48eqsstrd 3788 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐴𝑉 → ((rec(𝑅, 𝐴) ↾ ω)‘∅) ⊆ (fi‘𝐴))
50 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑥 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) → 𝑥 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛))
51 eqidd 2772 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑥 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) → 𝑥 = 𝑥)
52 ineq1 3958 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑎 = 𝑥 → (𝑎𝑏) = (𝑥𝑏))
5352eqeq2d 2781 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑎 = 𝑥 → (𝑥 = (𝑎𝑏) ↔ 𝑥 = (𝑥𝑏)))
54 ineq2 3959 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑏 = 𝑥 → (𝑥𝑏) = (𝑥𝑥))
55 inidm 3971 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑥𝑥) = 𝑥
5654, 55syl6eq 2821 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑏 = 𝑥 → (𝑥𝑏) = 𝑥)
5756eqeq2d 2781 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑏 = 𝑥 → (𝑥 = (𝑥𝑏) ↔ 𝑥 = 𝑥))
5853, 57rspc2ev 3474 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑥 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ∧ 𝑥 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ∧ 𝑥 = 𝑥) → ∃𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)∃𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)𝑥 = (𝑎𝑏))
5950, 50, 51, 58syl3anc 1476 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑥 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) → ∃𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)∃𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)𝑥 = (𝑎𝑏))
60 eqid 2771 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎𝑏)) = (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎𝑏))
6160rnmpt2 6917 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎𝑏)) = {𝑥 ∣ ∃𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)∃𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)𝑥 = (𝑎𝑏)}
6261abeq2i 2884 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑥 ∈ ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎𝑏)) ↔ ∃𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)∃𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)𝑥 = (𝑎𝑏))
6359, 62sylibr 224 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑥 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) → 𝑥 ∈ ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎𝑏)))
6463ssriv 3756 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎𝑏))
65 simpl 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑛 ∈ ω ∧ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ (fi‘𝐴)) → 𝑛 ∈ ω)
66 fvex 6342 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ∈ V
6766uniex 7100 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ∈ V
6867pwex 4981 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 𝒫 ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ∈ V
69 inss1 3981 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑎𝑏) ⊆ 𝑎
70 elssuni 4603 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) → 𝑎 ((rec(𝑅, 𝐴) ↾ ω)‘𝑛))
7170adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ∧ 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)) → 𝑎 ((rec(𝑅, 𝐴) ↾ ω)‘𝑛))
7269, 71syl5ss 3763 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ∧ 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)) → (𝑎𝑏) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛))
73 vex 3354 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 𝑎 ∈ V
7473inex1 4933 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑎𝑏) ∈ V
7574elpw 4303 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑎𝑏) ∈ 𝒫 ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↔ (𝑎𝑏) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛))
7672, 75sylibr 224 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ∧ 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)) → (𝑎𝑏) ∈ 𝒫 ((rec(𝑅, 𝐴) ↾ ω)‘𝑛))
7776rgen2a 3126 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)∀𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)(𝑎𝑏) ∈ 𝒫 ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)
7860fmpt2 7387 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (∀𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)∀𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)(𝑎𝑏) ∈ 𝒫 ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↔ (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎𝑏)):(((rec(𝑅, 𝐴) ↾ ω)‘𝑛) × ((rec(𝑅, 𝐴) ↾ ω)‘𝑛))⟶𝒫 ((rec(𝑅, 𝐴) ↾ ω)‘𝑛))
7977, 78mpbi 220 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎𝑏)):(((rec(𝑅, 𝐴) ↾ ω)‘𝑛) × ((rec(𝑅, 𝐴) ↾ ω)‘𝑛))⟶𝒫 ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)
80 frn 6193 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎𝑏)):(((rec(𝑅, 𝐴) ↾ ω)‘𝑛) × ((rec(𝑅, 𝐴) ↾ ω)‘𝑛))⟶𝒫 ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) → ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎𝑏)) ⊆ 𝒫 ((rec(𝑅, 𝐴) ↾ ω)‘𝑛))
8179, 80ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎𝑏)) ⊆ 𝒫 ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)
8268, 81ssexi 4937 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎𝑏)) ∈ V
83 nfcv 2913 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 𝑣𝐴
84 nfcv 2913 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 𝑣𝑛
85 nfcv 2913 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 𝑣ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎𝑏))
86 dffi3.1 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 𝑅 = (𝑢 ∈ V ↦ ran (𝑦𝑢, 𝑧𝑢 ↦ (𝑦𝑧)))
87 mpt2eq12 6862 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝑢 = 𝑣𝑢 = 𝑣) → (𝑦𝑢, 𝑧𝑢 ↦ (𝑦𝑧)) = (𝑦𝑣, 𝑧𝑣 ↦ (𝑦𝑧)))
8887anidms 556 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝑢 = 𝑣 → (𝑦𝑢, 𝑧𝑢 ↦ (𝑦𝑧)) = (𝑦𝑣, 𝑧𝑣 ↦ (𝑦𝑧)))
89 ineq1 3958 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝑦 = 𝑎 → (𝑦𝑧) = (𝑎𝑧))
90 ineq2 3959 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝑧 = 𝑏 → (𝑎𝑧) = (𝑎𝑏))
9189, 90cbvmpt2v 6882 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝑦𝑣, 𝑧𝑣 ↦ (𝑦𝑧)) = (𝑎𝑣, 𝑏𝑣 ↦ (𝑎𝑏))
9288, 91syl6eq 2821 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑢 = 𝑣 → (𝑦𝑢, 𝑧𝑢 ↦ (𝑦𝑧)) = (𝑎𝑣, 𝑏𝑣 ↦ (𝑎𝑏)))
9392rneqd 5491 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑢 = 𝑣 → ran (𝑦𝑢, 𝑧𝑢 ↦ (𝑦𝑧)) = ran (𝑎𝑣, 𝑏𝑣 ↦ (𝑎𝑏)))
9493cbvmptv 4884 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑢 ∈ V ↦ ran (𝑦𝑢, 𝑧𝑢 ↦ (𝑦𝑧))) = (𝑣 ∈ V ↦ ran (𝑎𝑣, 𝑏𝑣 ↦ (𝑎𝑏)))
9586, 94eqtri 2793 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 𝑅 = (𝑣 ∈ V ↦ ran (𝑎𝑣, 𝑏𝑣 ↦ (𝑎𝑏)))
96 rdgeq1 7660 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑅 = (𝑣 ∈ V ↦ ran (𝑎𝑣, 𝑏𝑣 ↦ (𝑎𝑏))) → rec(𝑅, 𝐴) = rec((𝑣 ∈ V ↦ ran (𝑎𝑣, 𝑏𝑣 ↦ (𝑎𝑏))), 𝐴))
9795, 96ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 rec(𝑅, 𝐴) = rec((𝑣 ∈ V ↦ ran (𝑎𝑣, 𝑏𝑣 ↦ (𝑎𝑏))), 𝐴)
9897reseq1i 5530 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (rec(𝑅, 𝐴) ↾ ω) = (rec((𝑣 ∈ V ↦ ran (𝑎𝑣, 𝑏𝑣 ↦ (𝑎𝑏))), 𝐴) ↾ ω)
99 mpt2eq12 6862 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑣 = ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ∧ 𝑣 = ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)) → (𝑎𝑣, 𝑏𝑣 ↦ (𝑎𝑏)) = (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎𝑏)))
10099anidms 556 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑣 = ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) → (𝑎𝑣, 𝑏𝑣 ↦ (𝑎𝑏)) = (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎𝑏)))
101100rneqd 5491 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑣 = ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) → ran (𝑎𝑣, 𝑏𝑣 ↦ (𝑎𝑏)) = ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎𝑏)))
10283, 84, 85, 98, 101frsucmpt 7686 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑛 ∈ ω ∧ ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎𝑏)) ∈ V) → ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛) = ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎𝑏)))
10365, 82, 102sylancl 574 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑛 ∈ ω ∧ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ (fi‘𝐴)) → ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛) = ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎𝑏)))
10464, 103syl5sseqr 3803 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑛 ∈ ω ∧ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ (fi‘𝐴)) → ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛))
105 sstr2 3759 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) → (((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛) → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛)))
106104, 105syl5com 31 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑛 ∈ ω ∧ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ (fi‘𝐴)) → (((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛)))
107106ralimdv 3112 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑛 ∈ ω ∧ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ (fi‘𝐴)) → (∀𝑦𝑛 ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) → ∀𝑦𝑛 ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛)))
108 vex 3354 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 𝑛 ∈ V
109 fveq2 6332 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑦 = 𝑛 → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) = ((rec(𝑅, 𝐴) ↾ ω)‘𝑛))
110109sseq1d 3781 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑦 = 𝑛 → (((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛) ↔ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛)))
111108, 110ralsn 4360 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (∀𝑦 ∈ {𝑛} ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛) ↔ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛))
112104, 111sylibr 224 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑛 ∈ ω ∧ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ (fi‘𝐴)) → ∀𝑦 ∈ {𝑛} ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛))
113107, 112jctird 516 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑛 ∈ ω ∧ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ (fi‘𝐴)) → (∀𝑦𝑛 ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) → (∀𝑦𝑛 ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛) ∧ ∀𝑦 ∈ {𝑛} ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛))))
114 df-suc 5872 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 suc 𝑛 = (𝑛 ∪ {𝑛})
115114raleqi 3291 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (∀𝑦 ∈ suc 𝑛((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛) ↔ ∀𝑦 ∈ (𝑛 ∪ {𝑛})((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛))
116 ralunb 3945 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (∀𝑦 ∈ (𝑛 ∪ {𝑛})((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛) ↔ (∀𝑦𝑛 ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛) ∧ ∀𝑦 ∈ {𝑛} ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛)))
117115, 116bitri 264 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (∀𝑦 ∈ suc 𝑛((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛) ↔ (∀𝑦𝑛 ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛) ∧ ∀𝑦 ∈ {𝑛} ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛)))
118113, 117syl6ibr 242 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑛 ∈ ω ∧ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ (fi‘𝐴)) → (∀𝑦𝑛 ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) → ∀𝑦 ∈ suc 𝑛((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛)))
119 fiin 8484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑎 ∈ (fi‘𝐴) ∧ 𝑏 ∈ (fi‘𝐴)) → (𝑎𝑏) ∈ (fi‘𝐴))
120119rgen2a 3126 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 𝑎 ∈ (fi‘𝐴)∀𝑏 ∈ (fi‘𝐴)(𝑎𝑏) ∈ (fi‘𝐴)
121 ssralv 3815 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ (fi‘𝐴) → (∀𝑏 ∈ (fi‘𝐴)(𝑎𝑏) ∈ (fi‘𝐴) → ∀𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)(𝑎𝑏) ∈ (fi‘𝐴)))
122121ralimdv 3112 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ (fi‘𝐴) → (∀𝑎 ∈ (fi‘𝐴)∀𝑏 ∈ (fi‘𝐴)(𝑎𝑏) ∈ (fi‘𝐴) → ∀𝑎 ∈ (fi‘𝐴)∀𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)(𝑎𝑏) ∈ (fi‘𝐴)))
123 ssralv 3815 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ (fi‘𝐴) → (∀𝑎 ∈ (fi‘𝐴)∀𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)(𝑎𝑏) ∈ (fi‘𝐴) → ∀𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)∀𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)(𝑎𝑏) ∈ (fi‘𝐴)))
124122, 123syld 47 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ (fi‘𝐴) → (∀𝑎 ∈ (fi‘𝐴)∀𝑏 ∈ (fi‘𝐴)(𝑎𝑏) ∈ (fi‘𝐴) → ∀𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)∀𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)(𝑎𝑏) ∈ (fi‘𝐴)))
125120, 124mpi 20 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ (fi‘𝐴) → ∀𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)∀𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)(𝑎𝑏) ∈ (fi‘𝐴))
12660fmpt2 7387 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (∀𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)∀𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)(𝑎𝑏) ∈ (fi‘𝐴) ↔ (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎𝑏)):(((rec(𝑅, 𝐴) ↾ ω)‘𝑛) × ((rec(𝑅, 𝐴) ↾ ω)‘𝑛))⟶(fi‘𝐴))
127125, 126sylib 208 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ (fi‘𝐴) → (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎𝑏)):(((rec(𝑅, 𝐴) ↾ ω)‘𝑛) × ((rec(𝑅, 𝐴) ↾ ω)‘𝑛))⟶(fi‘𝐴))
128 frn 6193 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎𝑏)):(((rec(𝑅, 𝐴) ↾ ω)‘𝑛) × ((rec(𝑅, 𝐴) ↾ ω)‘𝑛))⟶(fi‘𝐴) → ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎𝑏)) ⊆ (fi‘𝐴))
129127, 128syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ (fi‘𝐴) → ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎𝑏)) ⊆ (fi‘𝐴))
130129adantl 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑛 ∈ ω ∧ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ (fi‘𝐴)) → ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎𝑏)) ⊆ (fi‘𝐴))
131103, 130eqsstrd 3788 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑛 ∈ ω ∧ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ (fi‘𝐴)) → ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛) ⊆ (fi‘𝐴))
132118, 131jctild 515 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑛 ∈ ω ∧ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ (fi‘𝐴)) → (∀𝑦𝑛 ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) → (((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛) ⊆ (fi‘𝐴) ∧ ∀𝑦 ∈ suc 𝑛((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛))))
133132expimpd 441 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 ∈ ω → ((((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ (fi‘𝐴) ∧ ∀𝑦𝑛 ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)) → (((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛) ⊆ (fi‘𝐴) ∧ ∀𝑦 ∈ suc 𝑛((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛))))
134133a1d 25 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 ∈ ω → (𝐴𝑉 → ((((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ (fi‘𝐴) ∧ ∀𝑦𝑛 ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)) → (((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛) ⊆ (fi‘𝐴) ∧ ∀𝑦 ∈ suc 𝑛((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛)))))
13537, 42, 47, 49, 134finds2 7241 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ∈ ω → (𝐴𝑉 → (((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ⊆ (fi‘𝐴) ∧ ∀𝑦𝑥 ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥))))
136135impcom 394 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐴𝑉𝑥 ∈ ω) → (((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ⊆ (fi‘𝐴) ∧ ∀𝑦𝑥 ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥)))
137136simprd 483 . . . . . . . . . . . . . . . . . . . . 21 ((𝐴𝑉𝑥 ∈ ω) → ∀𝑦𝑥 ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥))
138137r19.21bi 3081 . . . . . . . . . . . . . . . . . . . 20 (((𝐴𝑉𝑥 ∈ ω) ∧ 𝑦𝑥) → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥))
139138ex 397 . . . . . . . . . . . . . . . . . . 19 ((𝐴𝑉𝑥 ∈ ω) → (𝑦𝑥 → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥)))
140139adantr 466 . . . . . . . . . . . . . . . . . 18 (((𝐴𝑉𝑥 ∈ ω) ∧ 𝑦 ∈ ω) → (𝑦𝑥 → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥)))
141 fveq2 6332 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = 𝑥 → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) = ((rec(𝑅, 𝐴) ↾ ω)‘𝑥))
142 eqimss 3806 . . . . . . . . . . . . . . . . . . . 20 (((rec(𝑅, 𝐴) ↾ ω)‘𝑦) = ((rec(𝑅, 𝐴) ↾ ω)‘𝑥) → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥))
143141, 142syl 17 . . . . . . . . . . . . . . . . . . 19 (𝑦 = 𝑥 → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥))
144143a1i 11 . . . . . . . . . . . . . . . . . 18 (((𝐴𝑉𝑥 ∈ ω) ∧ 𝑦 ∈ ω) → (𝑦 = 𝑥 → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥)))
145140, 144jaod 846 . . . . . . . . . . . . . . . . 17 (((𝐴𝑉𝑥 ∈ ω) ∧ 𝑦 ∈ ω) → ((𝑦𝑥𝑦 = 𝑥) → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥)))
14632, 145sylbid 230 . . . . . . . . . . . . . . . 16 (((𝐴𝑉𝑥 ∈ ω) ∧ 𝑦 ∈ ω) → (𝑦𝑥 → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥)))
147146ralrimiva 3115 . . . . . . . . . . . . . . 15 ((𝐴𝑉𝑥 ∈ ω) → ∀𝑦 ∈ ω (𝑦𝑥 → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥)))
148147ralrimiva 3115 . . . . . . . . . . . . . 14 (𝐴𝑉 → ∀𝑥 ∈ ω ∀𝑦 ∈ ω (𝑦𝑥 → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥)))
149148adantr 466 . . . . . . . . . . . . 13 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) → ∀𝑥 ∈ ω ∀𝑦 ∈ ω (𝑦𝑥 → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥)))
150 ssun1 3927 . . . . . . . . . . . . . 14 𝑚 ⊆ (𝑚𝑛)
151150a1i 11 . . . . . . . . . . . . 13 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) → 𝑚 ⊆ (𝑚𝑛))
152 sseq2 3776 . . . . . . . . . . . . . . 15 (𝑥 = (𝑚𝑛) → (𝑦𝑥𝑦 ⊆ (𝑚𝑛)))
153 fveq2 6332 . . . . . . . . . . . . . . . 16 (𝑥 = (𝑚𝑛) → ((rec(𝑅, 𝐴) ↾ ω)‘𝑥) = ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))
154153sseq2d 3782 . . . . . . . . . . . . . . 15 (𝑥 = (𝑚𝑛) → (((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ↔ ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))))
155152, 154imbi12d 333 . . . . . . . . . . . . . 14 (𝑥 = (𝑚𝑛) → ((𝑦𝑥 → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥)) ↔ (𝑦 ⊆ (𝑚𝑛) → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))))
156 sseq1 3775 . . . . . . . . . . . . . . 15 (𝑦 = 𝑚 → (𝑦 ⊆ (𝑚𝑛) ↔ 𝑚 ⊆ (𝑚𝑛)))
157 fveq2 6332 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑚 → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) = ((rec(𝑅, 𝐴) ↾ ω)‘𝑚))
158157sseq1d 3781 . . . . . . . . . . . . . . 15 (𝑦 = 𝑚 → (((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ↔ ((rec(𝑅, 𝐴) ↾ ω)‘𝑚) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))))
159156, 158imbi12d 333 . . . . . . . . . . . . . 14 (𝑦 = 𝑚 → ((𝑦 ⊆ (𝑚𝑛) → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))) ↔ (𝑚 ⊆ (𝑚𝑛) → ((rec(𝑅, 𝐴) ↾ ω)‘𝑚) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))))
160155, 159rspc2v 3472 . . . . . . . . . . . . 13 (((𝑚𝑛) ∈ ω ∧ 𝑚 ∈ ω) → (∀𝑥 ∈ ω ∀𝑦 ∈ ω (𝑦𝑥 → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥)) → (𝑚 ⊆ (𝑚𝑛) → ((rec(𝑅, 𝐴) ↾ ω)‘𝑚) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))))
16126, 149, 151, 160syl3c 66 . . . . . . . . . . . 12 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) → ((rec(𝑅, 𝐴) ↾ ω)‘𝑚) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))
162161sseld 3751 . . . . . . . . . . 11 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) → (𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑚) → 𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))))
163 simprr 756 . . . . . . . . . . . . . 14 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) → 𝑛 ∈ ω)
16424, 163jca 501 . . . . . . . . . . . . 13 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) → ((𝑚𝑛) ∈ ω ∧ 𝑛 ∈ ω))
165 ssun2 3928 . . . . . . . . . . . . . 14 𝑛 ⊆ (𝑚𝑛)
166165a1i 11 . . . . . . . . . . . . 13 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) → 𝑛 ⊆ (𝑚𝑛))
167 sseq1 3775 . . . . . . . . . . . . . . 15 (𝑦 = 𝑛 → (𝑦 ⊆ (𝑚𝑛) ↔ 𝑛 ⊆ (𝑚𝑛)))
168109sseq1d 3781 . . . . . . . . . . . . . . 15 (𝑦 = 𝑛 → (((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ↔ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))))
169167, 168imbi12d 333 . . . . . . . . . . . . . 14 (𝑦 = 𝑛 → ((𝑦 ⊆ (𝑚𝑛) → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))) ↔ (𝑛 ⊆ (𝑚𝑛) → ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))))
170155, 169rspc2v 3472 . . . . . . . . . . . . 13 (((𝑚𝑛) ∈ ω ∧ 𝑛 ∈ ω) → (∀𝑥 ∈ ω ∀𝑦 ∈ ω (𝑦𝑥 → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥)) → (𝑛 ⊆ (𝑚𝑛) → ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))))
171164, 149, 166, 170syl3c 66 . . . . . . . . . . . 12 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) → ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))
172171sseld 3751 . . . . . . . . . . 11 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) → (𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) → 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))))
17323ad2antlr 706 . . . . . . . . . . . . . . 15 (((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) ∧ (𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ∧ 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))) → (𝑚𝑛) ∈ ω)
174 peano2 7233 . . . . . . . . . . . . . . 15 ((𝑚𝑛) ∈ ω → suc (𝑚𝑛) ∈ ω)
175 fveq2 6332 . . . . . . . . . . . . . . . 16 (𝑥 = suc (𝑚𝑛) → ((rec(𝑅, 𝐴) ↾ ω)‘𝑥) = ((rec(𝑅, 𝐴) ↾ ω)‘suc (𝑚𝑛)))
176175ssiun2s 4698 . . . . . . . . . . . . . . 15 (suc (𝑚𝑛) ∈ ω → ((rec(𝑅, 𝐴) ↾ ω)‘suc (𝑚𝑛)) ⊆ 𝑥 ∈ ω ((rec(𝑅, 𝐴) ↾ ω)‘𝑥))
177173, 174, 1763syl 18 . . . . . . . . . . . . . 14 (((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) ∧ (𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ∧ 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))) → ((rec(𝑅, 𝐴) ↾ ω)‘suc (𝑚𝑛)) ⊆ 𝑥 ∈ ω ((rec(𝑅, 𝐴) ↾ ω)‘𝑥))
178 simprl 754 . . . . . . . . . . . . . . . . . 18 (((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) ∧ (𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ∧ 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))) → 𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))
179 simprr 756 . . . . . . . . . . . . . . . . . 18 (((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) ∧ (𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ∧ 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))) → 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))
180 eqidd 2772 . . . . . . . . . . . . . . . . . 18 (((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) ∧ (𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ∧ 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))) → (𝑐𝑑) = (𝑐𝑑))
181 ineq1 3958 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = 𝑐 → (𝑎𝑏) = (𝑐𝑏))
182181eqeq2d 2781 . . . . . . . . . . . . . . . . . . 19 (𝑎 = 𝑐 → ((𝑐𝑑) = (𝑎𝑏) ↔ (𝑐𝑑) = (𝑐𝑏)))
183 ineq2 3959 . . . . . . . . . . . . . . . . . . . 20 (𝑏 = 𝑑 → (𝑐𝑏) = (𝑐𝑑))
184183eqeq2d 2781 . . . . . . . . . . . . . . . . . . 19 (𝑏 = 𝑑 → ((𝑐𝑑) = (𝑐𝑏) ↔ (𝑐𝑑) = (𝑐𝑑)))
185182, 184rspc2ev 3474 . . . . . . . . . . . . . . . . . 18 ((𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ∧ 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ∧ (𝑐𝑑) = (𝑐𝑑)) → ∃𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))∃𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))(𝑐𝑑) = (𝑎𝑏))
186178, 179, 180, 185syl3anc 1476 . . . . . . . . . . . . . . . . 17 (((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) ∧ (𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ∧ 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))) → ∃𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))∃𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))(𝑐𝑑) = (𝑎𝑏))
187 vex 3354 . . . . . . . . . . . . . . . . . . 19 𝑐 ∈ V
188187inex1 4933 . . . . . . . . . . . . . . . . . 18 (𝑐𝑑) ∈ V
189 eqeq1 2775 . . . . . . . . . . . . . . . . . . 19 (𝑥 = (𝑐𝑑) → (𝑥 = (𝑎𝑏) ↔ (𝑐𝑑) = (𝑎𝑏)))
1901892rexbidv 3205 . . . . . . . . . . . . . . . . . 18 (𝑥 = (𝑐𝑑) → (∃𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))∃𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))𝑥 = (𝑎𝑏) ↔ ∃𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))∃𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))(𝑐𝑑) = (𝑎𝑏)))
191188, 190elab 3501 . . . . . . . . . . . . . . . . 17 ((𝑐𝑑) ∈ {𝑥 ∣ ∃𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))∃𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))𝑥 = (𝑎𝑏)} ↔ ∃𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))∃𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))(𝑐𝑑) = (𝑎𝑏))
192186, 191sylibr 224 . . . . . . . . . . . . . . . 16 (((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) ∧ (𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ∧ 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))) → (𝑐𝑑) ∈ {𝑥 ∣ ∃𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))∃𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))𝑥 = (𝑎𝑏)})
193 eqid 2771 . . . . . . . . . . . . . . . . 17 (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ↦ (𝑎𝑏)) = (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ↦ (𝑎𝑏))
194193rnmpt2 6917 . . . . . . . . . . . . . . . 16 ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ↦ (𝑎𝑏)) = {𝑥 ∣ ∃𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))∃𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))𝑥 = (𝑎𝑏)}
195192, 194syl6eleqr 2861 . . . . . . . . . . . . . . 15 (((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) ∧ (𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ∧ 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))) → (𝑐𝑑) ∈ ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ↦ (𝑎𝑏)))
196 fvex 6342 . . . . . . . . . . . . . . . . . . 19 ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ∈ V
197196uniex 7100 . . . . . . . . . . . . . . . . . 18 ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ∈ V
198197pwex 4981 . . . . . . . . . . . . . . . . 17 𝒫 ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ∈ V
199 elssuni 4603 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) → 𝑎 ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))
20069, 199syl5ss 3763 . . . . . . . . . . . . . . . . . . . . . 22 (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) → (𝑎𝑏) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))
20174elpw 4303 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑎𝑏) ∈ 𝒫 ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ↔ (𝑎𝑏) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))
202200, 201sylibr 224 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) → (𝑎𝑏) ∈ 𝒫 ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))
203202adantr 466 . . . . . . . . . . . . . . . . . . . 20 ((𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ∧ 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))) → (𝑎𝑏) ∈ 𝒫 ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))
204203rgen2a 3126 . . . . . . . . . . . . . . . . . . 19 𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))∀𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))(𝑎𝑏) ∈ 𝒫 ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))
205193fmpt2 7387 . . . . . . . . . . . . . . . . . . 19 (∀𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))∀𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))(𝑎𝑏) ∈ 𝒫 ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ↔ (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ↦ (𝑎𝑏)):(((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) × ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))⟶𝒫 ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))
206204, 205mpbi 220 . . . . . . . . . . . . . . . . . 18 (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ↦ (𝑎𝑏)):(((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) × ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))⟶𝒫 ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))
207 frn 6193 . . . . . . . . . . . . . . . . . 18 ((𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ↦ (𝑎𝑏)):(((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) × ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))⟶𝒫 ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) → ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ↦ (𝑎𝑏)) ⊆ 𝒫 ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))
208206, 207ax-mp 5 . . . . . . . . . . . . . . . . 17 ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ↦ (𝑎𝑏)) ⊆ 𝒫 ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))
209198, 208ssexi 4937 . . . . . . . . . . . . . . . 16 ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ↦ (𝑎𝑏)) ∈ V
210 nfcv 2913 . . . . . . . . . . . . . . . . 17 𝑣(𝑚𝑛)
211 nfcv 2913 . . . . . . . . . . . . . . . . 17 𝑣ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ↦ (𝑎𝑏))
212 mpt2eq12 6862 . . . . . . . . . . . . . . . . . . 19 ((𝑣 = ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ∧ 𝑣 = ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))) → (𝑎𝑣, 𝑏𝑣 ↦ (𝑎𝑏)) = (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ↦ (𝑎𝑏)))
213212anidms 556 . . . . . . . . . . . . . . . . . 18 (𝑣 = ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) → (𝑎𝑣, 𝑏𝑣 ↦ (𝑎𝑏)) = (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ↦ (𝑎𝑏)))
214213rneqd 5491 . . . . . . . . . . . . . . . . 17 (𝑣 = ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) → ran (𝑎𝑣, 𝑏𝑣 ↦ (𝑎𝑏)) = ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ↦ (𝑎𝑏)))
21583, 210, 211, 98, 214frsucmpt 7686 . . . . . . . . . . . . . . . 16 (((𝑚𝑛) ∈ ω ∧ ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ↦ (𝑎𝑏)) ∈ V) → ((rec(𝑅, 𝐴) ↾ ω)‘suc (𝑚𝑛)) = ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ↦ (𝑎𝑏)))
216173, 209, 215sylancl 574 . . . . . . . . . . . . . . 15 (((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) ∧ (𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ∧ 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))) → ((rec(𝑅, 𝐴) ↾ ω)‘suc (𝑚𝑛)) = ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ↦ (𝑎𝑏)))
217195, 216eleqtrrd 2853 . . . . . . . . . . . . . 14 (((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) ∧ (𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ∧ 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))) → (𝑐𝑑) ∈ ((rec(𝑅, 𝐴) ↾ ω)‘suc (𝑚𝑛)))
218177, 217sseldd 3753 . . . . . . . . . . . . 13 (((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) ∧ (𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ∧ 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))) → (𝑐𝑑) ∈ 𝑥 ∈ ω ((rec(𝑅, 𝐴) ↾ ω)‘𝑥))
219 fniunfv 6648 . . . . . . . . . . . . . 14 ((rec(𝑅, 𝐴) ↾ ω) Fn ω → 𝑥 ∈ ω ((rec(𝑅, 𝐴) ↾ ω)‘𝑥) = ran (rec(𝑅, 𝐴) ↾ ω))
2203, 219ax-mp 5 . . . . . . . . . . . . 13 𝑥 ∈ ω ((rec(𝑅, 𝐴) ↾ ω)‘𝑥) = ran (rec(𝑅, 𝐴) ↾ ω)
221218, 220syl6eleq 2860 . . . . . . . . . . . 12 (((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) ∧ (𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ∧ 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))) → (𝑐𝑑) ∈ ran (rec(𝑅, 𝐴) ↾ ω))
222221ex 397 . . . . . . . . . . 11 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) → ((𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ∧ 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))) → (𝑐𝑑) ∈ ran (rec(𝑅, 𝐴) ↾ ω)))
223162, 172, 222syl2and 595 . . . . . . . . . 10 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) → ((𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑚) ∧ 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)) → (𝑐𝑑) ∈ ran (rec(𝑅, 𝐴) ↾ ω)))
224223rexlimdvva 3186 . . . . . . . . 9 (𝐴𝑉 → (∃𝑚 ∈ ω ∃𝑛 ∈ ω (𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑚) ∧ 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)) → (𝑐𝑑) ∈ ran (rec(𝑅, 𝐴) ↾ ω)))
225224imp 393 . . . . . . . 8 ((𝐴𝑉 ∧ ∃𝑚 ∈ ω ∃𝑛 ∈ ω (𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑚) ∧ 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛))) → (𝑐𝑑) ∈ ran (rec(𝑅, 𝐴) ↾ ω))
22620, 225sylan2br 582 . . . . . . 7 ((𝐴𝑉 ∧ (𝑐 ran (rec(𝑅, 𝐴) ↾ ω) ∧ 𝑑 ran (rec(𝑅, 𝐴) ↾ ω))) → (𝑐𝑑) ∈ ran (rec(𝑅, 𝐴) ↾ ω))
227226ralrimivva 3120 . . . . . 6 (𝐴𝑉 → ∀𝑐 ran (rec(𝑅, 𝐴) ↾ ω)∀𝑑 ran (rec(𝑅, 𝐴) ↾ ω)(𝑐𝑑) ∈ ran (rec(𝑅, 𝐴) ↾ ω))
228136simpld 482 . . . . . . . . . . . 12 ((𝐴𝑉𝑥 ∈ ω) → ((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ⊆ (fi‘𝐴))
229 fvex 6342 . . . . . . . . . . . . 13 (fi‘𝐴) ∈ V
230229elpw2 4959 . . . . . . . . . . . 12 (((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ∈ 𝒫 (fi‘𝐴) ↔ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ⊆ (fi‘𝐴))
231228, 230sylibr 224 . . . . . . . . . . 11 ((𝐴𝑉𝑥 ∈ ω) → ((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ∈ 𝒫 (fi‘𝐴))
232231ralrimiva 3115 . . . . . . . . . 10 (𝐴𝑉 → ∀𝑥 ∈ ω ((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ∈ 𝒫 (fi‘𝐴))
233 fnfvrnss 6532 . . . . . . . . . 10 (((rec(𝑅, 𝐴) ↾ ω) Fn ω ∧ ∀𝑥 ∈ ω ((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ∈ 𝒫 (fi‘𝐴)) → ran (rec(𝑅, 𝐴) ↾ ω) ⊆ 𝒫 (fi‘𝐴))
2343, 232, 233sylancr 575 . . . . . . . . 9 (𝐴𝑉 → ran (rec(𝑅, 𝐴) ↾ ω) ⊆ 𝒫 (fi‘𝐴))
235 sspwuni 4745 . . . . . . . . 9 (ran (rec(𝑅, 𝐴) ↾ ω) ⊆ 𝒫 (fi‘𝐴) ↔ ran (rec(𝑅, 𝐴) ↾ ω) ⊆ (fi‘𝐴))
236234, 235sylib 208 . . . . . . . 8 (𝐴𝑉 ran (rec(𝑅, 𝐴) ↾ ω) ⊆ (fi‘𝐴))
237 ssexg 4938 . . . . . . . 8 (( ran (rec(𝑅, 𝐴) ↾ ω) ⊆ (fi‘𝐴) ∧ (fi‘𝐴) ∈ V) → ran (rec(𝑅, 𝐴) ↾ ω) ∈ V)
238236, 229, 237sylancl 574 . . . . . . 7 (𝐴𝑉 ran (rec(𝑅, 𝐴) ↾ ω) ∈ V)
239 sseq2 3776 . . . . . . . . 9 (𝑥 = ran (rec(𝑅, 𝐴) ↾ ω) → (𝐴𝑥𝐴 ran (rec(𝑅, 𝐴) ↾ ω)))
240 eleq2 2839 . . . . . . . . . . 11 (𝑥 = ran (rec(𝑅, 𝐴) ↾ ω) → ((𝑐𝑑) ∈ 𝑥 ↔ (𝑐𝑑) ∈ ran (rec(𝑅, 𝐴) ↾ ω)))
241240raleqbi1dv 3295 . . . . . . . . . 10 (𝑥 = ran (rec(𝑅, 𝐴) ↾ ω) → (∀𝑑𝑥 (𝑐𝑑) ∈ 𝑥 ↔ ∀𝑑 ran (rec(𝑅, 𝐴) ↾ ω)(𝑐𝑑) ∈ ran (rec(𝑅, 𝐴) ↾ ω)))
242241raleqbi1dv 3295 . . . . . . . . 9 (𝑥 = ran (rec(𝑅, 𝐴) ↾ ω) → (∀𝑐𝑥𝑑𝑥 (𝑐𝑑) ∈ 𝑥 ↔ ∀𝑐 ran (rec(𝑅, 𝐴) ↾ ω)∀𝑑 ran (rec(𝑅, 𝐴) ↾ ω)(𝑐𝑑) ∈ ran (rec(𝑅, 𝐴) ↾ ω)))
243239, 242anbi12d 616 . . . . . . . 8 (𝑥 = ran (rec(𝑅, 𝐴) ↾ ω) → ((𝐴𝑥 ∧ ∀𝑐𝑥𝑑𝑥 (𝑐𝑑) ∈ 𝑥) ↔ (𝐴 ran (rec(𝑅, 𝐴) ↾ ω) ∧ ∀𝑐 ran (rec(𝑅, 𝐴) ↾ ω)∀𝑑 ran (rec(𝑅, 𝐴) ↾ ω)(𝑐𝑑) ∈ ran (rec(𝑅, 𝐴) ↾ ω))))
244243elabg 3502 . . . . . . 7 ( ran (rec(𝑅, 𝐴) ↾ ω) ∈ V → ( ran (rec(𝑅, 𝐴) ↾ ω) ∈ {𝑥 ∣ (𝐴𝑥 ∧ ∀𝑐𝑥𝑑𝑥 (𝑐𝑑) ∈ 𝑥)} ↔ (𝐴 ran (rec(𝑅, 𝐴) ↾ ω) ∧ ∀𝑐 ran (rec(𝑅, 𝐴) ↾ ω)∀𝑑 ran (rec(𝑅, 𝐴) ↾ ω)(𝑐𝑑) ∈ ran (rec(𝑅, 𝐴) ↾ ω))))
245238, 244syl 17 . . . . . 6 (𝐴𝑉 → ( ran (rec(𝑅, 𝐴) ↾ ω) ∈ {𝑥 ∣ (𝐴𝑥 ∧ ∀𝑐𝑥𝑑𝑥 (𝑐𝑑) ∈ 𝑥)} ↔ (𝐴 ran (rec(𝑅, 𝐴) ↾ ω) ∧ ∀𝑐 ran (rec(𝑅, 𝐴) ↾ ω)∀𝑑 ran (rec(𝑅, 𝐴) ↾ ω)(𝑐𝑑) ∈ ran (rec(𝑅, 𝐴) ↾ ω))))
2469, 227, 245mpbir2and 692 . . . . 5 (𝐴𝑉 ran (rec(𝑅, 𝐴) ↾ ω) ∈ {𝑥 ∣ (𝐴𝑥 ∧ ∀𝑐𝑥𝑑𝑥 (𝑐𝑑) ∈ 𝑥)})
247 intss1 4626 . . . . 5 ( ran (rec(𝑅, 𝐴) ↾ ω) ∈ {𝑥 ∣ (𝐴𝑥 ∧ ∀𝑐𝑥𝑑𝑥 (𝑐𝑑) ∈ 𝑥)} → {𝑥 ∣ (𝐴𝑥 ∧ ∀𝑐𝑥𝑑𝑥 (𝑐𝑑) ∈ 𝑥)} ⊆ ran (rec(𝑅, 𝐴) ↾ ω))
248246, 247syl 17 . . . 4 (𝐴𝑉 {𝑥 ∣ (𝐴𝑥 ∧ ∀𝑐𝑥𝑑𝑥 (𝑐𝑑) ∈ 𝑥)} ⊆ ran (rec(𝑅, 𝐴) ↾ ω))
2491, 248eqsstrd 3788 . . 3 (𝐴𝑉 → (fi‘𝐴) ⊆ ran (rec(𝑅, 𝐴) ↾ ω))
250249, 236eqssd 3769 . 2 (𝐴𝑉 → (fi‘𝐴) = ran (rec(𝑅, 𝐴) ↾ ω))
251 df-ima 5262 . . 3 (rec(𝑅, 𝐴) “ ω) = ran (rec(𝑅, 𝐴) ↾ ω)
252251unieqi 4583 . 2 (rec(𝑅, 𝐴) “ ω) = ran (rec(𝑅, 𝐴) ↾ ω)
253250, 252syl6eqr 2823 1 (𝐴𝑉 → (fi‘𝐴) = (rec(𝑅, 𝐴) “ ω))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 382  wo 834   = wceq 1631  wcel 2145  {cab 2757  wral 3061  wrex 3062  Vcvv 3351  cun 3721  cin 3722  wss 3723  c0 4063  𝒫 cpw 4297  {csn 4316   cuni 4574   cint 4611   ciun 4654  cmpt 4863   × cxp 5247  ran crn 5250  cres 5251  cima 5252  Ord word 5865  Oncon0 5866  suc csuc 5868   Fn wfn 6026  wf 6027  cfv 6031  cmpt2 6795  ωcom 7212  reccrdg 7658  ficfi 8472
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4915  ax-nul 4923  ax-pow 4974  ax-pr 5034  ax-un 7096
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 835  df-3or 1072  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-ral 3066  df-rex 3067  df-reu 3068  df-rab 3070  df-v 3353  df-sbc 3588  df-csb 3683  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-pss 3739  df-nul 4064  df-if 4226  df-pw 4299  df-sn 4317  df-pr 4319  df-tp 4321  df-op 4323  df-uni 4575  df-int 4612  df-iun 4656  df-br 4787  df-opab 4847  df-mpt 4864  df-tr 4887  df-id 5157  df-eprel 5162  df-po 5170  df-so 5171  df-fr 5208  df-we 5210  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-pred 5823  df-ord 5869  df-on 5870  df-lim 5871  df-suc 5872  df-iota 5994  df-fun 6033  df-fn 6034  df-f 6035  df-f1 6036  df-fo 6037  df-f1o 6038  df-fv 6039  df-ov 6796  df-oprab 6797  df-mpt2 6798  df-om 7213  df-1st 7315  df-2nd 7316  df-wrecs 7559  df-recs 7621  df-rdg 7659  df-1o 7713  df-oadd 7717  df-er 7896  df-en 8110  df-fin 8113  df-fi 8473
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator