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

Theorem dffi3 8322
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 8314 . . . 4 (𝐴𝑉 → (fi‘𝐴) = {𝑥 ∣ (𝐴𝑥 ∧ ∀𝑐𝑥𝑑𝑥 (𝑐𝑑) ∈ 𝑥)})
2 fr0g 7516 . . . . . . . 8 (𝐴𝑉 → ((rec(𝑅, 𝐴) ↾ ω)‘∅) = 𝐴)
3 frfnom 7515 . . . . . . . . 9 (rec(𝑅, 𝐴) ↾ ω) Fn ω
4 peano1 7070 . . . . . . . . 9 ∅ ∈ ω
5 fnfvelrn 6342 . . . . . . . . 9 (((rec(𝑅, 𝐴) ↾ ω) Fn ω ∧ ∅ ∈ ω) → ((rec(𝑅, 𝐴) ↾ ω)‘∅) ∈ ran (rec(𝑅, 𝐴) ↾ ω))
63, 4, 5mp2an 707 . . . . . . . 8 ((rec(𝑅, 𝐴) ↾ ω)‘∅) ∈ ran (rec(𝑅, 𝐴) ↾ ω)
72, 6syl6eqelr 2708 . . . . . . 7 (𝐴𝑉𝐴 ∈ ran (rec(𝑅, 𝐴) ↾ ω))
8 elssuni 4458 . . . . . . 7 (𝐴 ∈ ran (rec(𝑅, 𝐴) ↾ ω) → 𝐴 ran (rec(𝑅, 𝐴) ↾ ω))
97, 8syl 17 . . . . . 6 (𝐴𝑉𝐴 ran (rec(𝑅, 𝐴) ↾ ω))
10 reeanv 3102 . . . . . . . . 9 (∃𝑚 ∈ ω ∃𝑛 ∈ ω (𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑚) ∧ 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)) ↔ (∃𝑚 ∈ ω 𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑚) ∧ ∃𝑛 ∈ ω 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)))
11 eliun 4515 . . . . . . . . . 10 (𝑐 𝑚 ∈ ω ((rec(𝑅, 𝐴) ↾ ω)‘𝑚) ↔ ∃𝑚 ∈ ω 𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑚))
12 eliun 4515 . . . . . . . . . 10 (𝑑 𝑛 ∈ ω ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↔ ∃𝑛 ∈ ω 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛))
1311, 12anbi12i 732 . . . . . . . . 9 ((𝑐 𝑚 ∈ ω ((rec(𝑅, 𝐴) ↾ ω)‘𝑚) ∧ 𝑑 𝑛 ∈ ω ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)) ↔ (∃𝑚 ∈ ω 𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑚) ∧ ∃𝑛 ∈ ω 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)))
14 fniunfv 6490 . . . . . . . . . . . 12 ((rec(𝑅, 𝐴) ↾ ω) Fn ω → 𝑚 ∈ ω ((rec(𝑅, 𝐴) ↾ ω)‘𝑚) = ran (rec(𝑅, 𝐴) ↾ ω))
1514eleq2d 2685 . . . . . . . . . . 11 ((rec(𝑅, 𝐴) ↾ ω) Fn ω → (𝑐 𝑚 ∈ ω ((rec(𝑅, 𝐴) ↾ ω)‘𝑚) ↔ 𝑐 ran (rec(𝑅, 𝐴) ↾ ω)))
16 fniunfv 6490 . . . . . . . . . . . 12 ((rec(𝑅, 𝐴) ↾ ω) Fn ω → 𝑛 ∈ ω ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) = ran (rec(𝑅, 𝐴) ↾ ω))
1716eleq2d 2685 . . . . . . . . . . 11 ((rec(𝑅, 𝐴) ↾ ω) Fn ω → (𝑑 𝑛 ∈ ω ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↔ 𝑑 ran (rec(𝑅, 𝐴) ↾ ω)))
1815, 17anbi12d 746 . . . . . . . . . 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 7059 . . . . . . . . . . . . . . . 16 Ord ω
22 ordunel 7012 . . . . . . . . . . . . . . . 16 ((Ord ω ∧ 𝑚 ∈ ω ∧ 𝑛 ∈ ω) → (𝑚𝑛) ∈ ω)
2321, 22mp3an1 1409 . . . . . . . . . . . . . . 15 ((𝑚 ∈ ω ∧ 𝑛 ∈ ω) → (𝑚𝑛) ∈ ω)
2423adantl 482 . . . . . . . . . . . . . 14 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) → (𝑚𝑛) ∈ ω)
25 simprl 793 . . . . . . . . . . . . . 14 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) → 𝑚 ∈ ω)
2624, 25jca 554 . . . . . . . . . . . . 13 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) → ((𝑚𝑛) ∈ ω ∧ 𝑚 ∈ ω))
27 nnon 7056 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ ω → 𝑦 ∈ On)
2827adantl 482 . . . . . . . . . . . . . . . . . 18 (((𝐴𝑉𝑥 ∈ ω) ∧ 𝑦 ∈ ω) → 𝑦 ∈ On)
29 nnon 7056 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ω → 𝑥 ∈ On)
3029ad2antlr 762 . . . . . . . . . . . . . . . . . 18 (((𝐴𝑉𝑥 ∈ ω) ∧ 𝑦 ∈ ω) → 𝑥 ∈ On)
31 onsseleq 5753 . . . . . . . . . . . . . . . . . 18 ((𝑦 ∈ On ∧ 𝑥 ∈ On) → (𝑦𝑥 ↔ (𝑦𝑥𝑦 = 𝑥)))
3228, 30, 31syl2anc 692 . . . . . . . . . . . . . . . . 17 (((𝐴𝑉𝑥 ∈ ω) ∧ 𝑦 ∈ ω) → (𝑦𝑥 ↔ (𝑦𝑥𝑦 = 𝑥)))
33 rzal 4064 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 = ∅ → ∀𝑦𝑥 ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥))
3433biantrud 528 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = ∅ → (((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ⊆ (fi‘𝐴) ↔ (((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ⊆ (fi‘𝐴) ∧ ∀𝑦𝑥 ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥))))
35 fveq2 6178 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 = ∅ → ((rec(𝑅, 𝐴) ↾ ω)‘𝑥) = ((rec(𝑅, 𝐴) ↾ ω)‘∅))
3635sseq1d 3624 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = ∅ → (((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ⊆ (fi‘𝐴) ↔ ((rec(𝑅, 𝐴) ↾ ω)‘∅) ⊆ (fi‘𝐴)))
3734, 36bitr3d 270 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = ∅ → ((((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ⊆ (fi‘𝐴) ∧ ∀𝑦𝑥 ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥)) ↔ ((rec(𝑅, 𝐴) ↾ ω)‘∅) ⊆ (fi‘𝐴)))
38 fveq2 6178 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 = 𝑛 → ((rec(𝑅, 𝐴) ↾ ω)‘𝑥) = ((rec(𝑅, 𝐴) ↾ ω)‘𝑛))
3938sseq1d 3624 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = 𝑛 → (((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ⊆ (fi‘𝐴) ↔ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ (fi‘𝐴)))
4038sseq2d 3625 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 = 𝑛 → (((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ↔ ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)))
4140raleqbi1dv 3141 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = 𝑛 → (∀𝑦𝑥 ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ↔ ∀𝑦𝑛 ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)))
4239, 41anbi12d 746 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = 𝑛 → ((((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ⊆ (fi‘𝐴) ∧ ∀𝑦𝑥 ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥)) ↔ (((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ (fi‘𝐴) ∧ ∀𝑦𝑛 ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛))))
43 fveq2 6178 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 = suc 𝑛 → ((rec(𝑅, 𝐴) ↾ ω)‘𝑥) = ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛))
4443sseq1d 3624 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = suc 𝑛 → (((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ⊆ (fi‘𝐴) ↔ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛) ⊆ (fi‘𝐴)))
4543sseq2d 3625 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 = suc 𝑛 → (((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ↔ ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛)))
4645raleqbi1dv 3141 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = suc 𝑛 → (∀𝑦𝑥 ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ↔ ∀𝑦 ∈ suc 𝑛((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛)))
4744, 46anbi12d 746 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = suc 𝑛 → ((((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ⊆ (fi‘𝐴) ∧ ∀𝑦𝑥 ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥)) ↔ (((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛) ⊆ (fi‘𝐴) ∧ ∀𝑦 ∈ suc 𝑛((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛))))
48 ssfii 8310 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐴𝑉𝐴 ⊆ (fi‘𝐴))
492, 48eqsstrd 3631 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐴𝑉 → ((rec(𝑅, 𝐴) ↾ ω)‘∅) ⊆ (fi‘𝐴))
50 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑥 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) → 𝑥 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛))
51 eqidd 2621 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑥 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) → 𝑥 = 𝑥)
52 ineq1 3799 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑎 = 𝑥 → (𝑎𝑏) = (𝑥𝑏))
5352eqeq2d 2630 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑎 = 𝑥 → (𝑥 = (𝑎𝑏) ↔ 𝑥 = (𝑥𝑏)))
54 ineq2 3800 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑏 = 𝑥 → (𝑥𝑏) = (𝑥𝑥))
55 inidm 3814 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑥𝑥) = 𝑥
5654, 55syl6eq 2670 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑏 = 𝑥 → (𝑥𝑏) = 𝑥)
5756eqeq2d 2630 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑏 = 𝑥 → (𝑥 = (𝑥𝑏) ↔ 𝑥 = 𝑥))
5853, 57rspc2ev 3319 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑥 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ∧ 𝑥 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ∧ 𝑥 = 𝑥) → ∃𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)∃𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)𝑥 = (𝑎𝑏))
5950, 50, 51, 58syl3anc 1324 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑥 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) → ∃𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)∃𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)𝑥 = (𝑎𝑏))
60 eqid 2620 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎𝑏)) = (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎𝑏))
6160rnmpt2 6755 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎𝑏)) = {𝑥 ∣ ∃𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)∃𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)𝑥 = (𝑎𝑏)}
6261abeq2i 2733 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑥 ∈ ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎𝑏)) ↔ ∃𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)∃𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)𝑥 = (𝑎𝑏))
6359, 62sylibr 224 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑥 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) → 𝑥 ∈ ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎𝑏)))
6463ssriv 3599 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎𝑏))
65 simpl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑛 ∈ ω ∧ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ (fi‘𝐴)) → 𝑛 ∈ ω)
66 fvex 6188 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ∈ V
6766uniex 6938 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ∈ V
6867pwex 4839 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 𝒫 ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ∈ V
69 inss1 3825 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑎𝑏) ⊆ 𝑎
70 elssuni 4458 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) → 𝑎 ((rec(𝑅, 𝐴) ↾ ω)‘𝑛))
7170adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ∧ 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)) → 𝑎 ((rec(𝑅, 𝐴) ↾ ω)‘𝑛))
7269, 71syl5ss 3606 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ∧ 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)) → (𝑎𝑏) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛))
73 vex 3198 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 𝑎 ∈ V
7473inex1 4790 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑎𝑏) ∈ V
7574elpw 4155 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑎𝑏) ∈ 𝒫 ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↔ (𝑎𝑏) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛))
7672, 75sylibr 224 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ∧ 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)) → (𝑎𝑏) ∈ 𝒫 ((rec(𝑅, 𝐴) ↾ ω)‘𝑛))
7776rgen2a 2974 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)∀𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)(𝑎𝑏) ∈ 𝒫 ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)
7860fmpt2 7222 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (∀𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)∀𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)(𝑎𝑏) ∈ 𝒫 ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↔ (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎𝑏)):(((rec(𝑅, 𝐴) ↾ ω)‘𝑛) × ((rec(𝑅, 𝐴) ↾ ω)‘𝑛))⟶𝒫 ((rec(𝑅, 𝐴) ↾ ω)‘𝑛))
7977, 78mpbi 220 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎𝑏)):(((rec(𝑅, 𝐴) ↾ ω)‘𝑛) × ((rec(𝑅, 𝐴) ↾ ω)‘𝑛))⟶𝒫 ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)
80 frn 6040 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎𝑏)):(((rec(𝑅, 𝐴) ↾ ω)‘𝑛) × ((rec(𝑅, 𝐴) ↾ ω)‘𝑛))⟶𝒫 ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) → ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎𝑏)) ⊆ 𝒫 ((rec(𝑅, 𝐴) ↾ ω)‘𝑛))
8179, 80ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎𝑏)) ⊆ 𝒫 ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)
8268, 81ssexi 4794 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎𝑏)) ∈ V
83 nfcv 2762 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 𝑣𝐴
84 nfcv 2762 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 𝑣𝑛
85 nfcv 2762 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 𝑣ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎𝑏))
86 dffi3.1 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 𝑅 = (𝑢 ∈ V ↦ ran (𝑦𝑢, 𝑧𝑢 ↦ (𝑦𝑧)))
87 mpt2eq12 6700 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝑢 = 𝑣𝑢 = 𝑣) → (𝑦𝑢, 𝑧𝑢 ↦ (𝑦𝑧)) = (𝑦𝑣, 𝑧𝑣 ↦ (𝑦𝑧)))
8887anidms 676 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝑢 = 𝑣 → (𝑦𝑢, 𝑧𝑢 ↦ (𝑦𝑧)) = (𝑦𝑣, 𝑧𝑣 ↦ (𝑦𝑧)))
89 ineq1 3799 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝑦 = 𝑎 → (𝑦𝑧) = (𝑎𝑧))
90 ineq2 3800 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝑧 = 𝑏 → (𝑎𝑧) = (𝑎𝑏))
9189, 90cbvmpt2v 6720 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝑦𝑣, 𝑧𝑣 ↦ (𝑦𝑧)) = (𝑎𝑣, 𝑏𝑣 ↦ (𝑎𝑏))
9288, 91syl6eq 2670 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑢 = 𝑣 → (𝑦𝑢, 𝑧𝑢 ↦ (𝑦𝑧)) = (𝑎𝑣, 𝑏𝑣 ↦ (𝑎𝑏)))
9392rneqd 5342 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑢 = 𝑣 → ran (𝑦𝑢, 𝑧𝑢 ↦ (𝑦𝑧)) = ran (𝑎𝑣, 𝑏𝑣 ↦ (𝑎𝑏)))
9493cbvmptv 4741 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑢 ∈ V ↦ ran (𝑦𝑢, 𝑧𝑢 ↦ (𝑦𝑧))) = (𝑣 ∈ V ↦ ran (𝑎𝑣, 𝑏𝑣 ↦ (𝑎𝑏)))
9586, 94eqtri 2642 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 𝑅 = (𝑣 ∈ V ↦ ran (𝑎𝑣, 𝑏𝑣 ↦ (𝑎𝑏)))
96 rdgeq1 7492 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑅 = (𝑣 ∈ V ↦ ran (𝑎𝑣, 𝑏𝑣 ↦ (𝑎𝑏))) → rec(𝑅, 𝐴) = rec((𝑣 ∈ V ↦ ran (𝑎𝑣, 𝑏𝑣 ↦ (𝑎𝑏))), 𝐴))
9795, 96ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 rec(𝑅, 𝐴) = rec((𝑣 ∈ V ↦ ran (𝑎𝑣, 𝑏𝑣 ↦ (𝑎𝑏))), 𝐴)
9897reseq1i 5381 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (rec(𝑅, 𝐴) ↾ ω) = (rec((𝑣 ∈ V ↦ ran (𝑎𝑣, 𝑏𝑣 ↦ (𝑎𝑏))), 𝐴) ↾ ω)
99 mpt2eq12 6700 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑣 = ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ∧ 𝑣 = ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)) → (𝑎𝑣, 𝑏𝑣 ↦ (𝑎𝑏)) = (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎𝑏)))
10099anidms 676 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑣 = ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) → (𝑎𝑣, 𝑏𝑣 ↦ (𝑎𝑏)) = (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎𝑏)))
101100rneqd 5342 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑣 = ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) → ran (𝑎𝑣, 𝑏𝑣 ↦ (𝑎𝑏)) = ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎𝑏)))
10283, 84, 85, 98, 101frsucmpt 7518 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑛 ∈ ω ∧ ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎𝑏)) ∈ V) → ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛) = ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎𝑏)))
10365, 82, 102sylancl 693 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑛 ∈ ω ∧ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ (fi‘𝐴)) → ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛) = ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎𝑏)))
10464, 103syl5sseqr 3646 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑛 ∈ ω ∧ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ (fi‘𝐴)) → ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛))
105 sstr2 3602 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) → (((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛) → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛)))
106104, 105syl5com 31 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑛 ∈ ω ∧ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ (fi‘𝐴)) → (((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛)))
107106ralimdv 2960 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑛 ∈ ω ∧ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ (fi‘𝐴)) → (∀𝑦𝑛 ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) → ∀𝑦𝑛 ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛)))
108 vex 3198 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 𝑛 ∈ V
109 fveq2 6178 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑦 = 𝑛 → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) = ((rec(𝑅, 𝐴) ↾ ω)‘𝑛))
110109sseq1d 3624 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑦 = 𝑛 → (((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛) ↔ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛)))
111108, 110ralsn 4213 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (∀𝑦 ∈ {𝑛} ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛) ↔ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛))
112104, 111sylibr 224 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑛 ∈ ω ∧ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ (fi‘𝐴)) → ∀𝑦 ∈ {𝑛} ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛))
113107, 112jctird 566 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑛 ∈ ω ∧ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ (fi‘𝐴)) → (∀𝑦𝑛 ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) → (∀𝑦𝑛 ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛) ∧ ∀𝑦 ∈ {𝑛} ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛))))
114 df-suc 5717 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 suc 𝑛 = (𝑛 ∪ {𝑛})
115114raleqi 3137 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (∀𝑦 ∈ suc 𝑛((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛) ↔ ∀𝑦 ∈ (𝑛 ∪ {𝑛})((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛))
116 ralunb 3786 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 8313 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑎 ∈ (fi‘𝐴) ∧ 𝑏 ∈ (fi‘𝐴)) → (𝑎𝑏) ∈ (fi‘𝐴))
120119rgen2a 2974 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 𝑎 ∈ (fi‘𝐴)∀𝑏 ∈ (fi‘𝐴)(𝑎𝑏) ∈ (fi‘𝐴)
121 ssralv 3658 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ (fi‘𝐴) → (∀𝑏 ∈ (fi‘𝐴)(𝑎𝑏) ∈ (fi‘𝐴) → ∀𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)(𝑎𝑏) ∈ (fi‘𝐴)))
122121ralimdv 2960 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ (fi‘𝐴) → (∀𝑎 ∈ (fi‘𝐴)∀𝑏 ∈ (fi‘𝐴)(𝑎𝑏) ∈ (fi‘𝐴) → ∀𝑎 ∈ (fi‘𝐴)∀𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)(𝑎𝑏) ∈ (fi‘𝐴)))
123 ssralv 3658 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 7222 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (∀𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)∀𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)(𝑎𝑏) ∈ (fi‘𝐴) ↔ (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎𝑏)):(((rec(𝑅, 𝐴) ↾ ω)‘𝑛) × ((rec(𝑅, 𝐴) ↾ ω)‘𝑛))⟶(fi‘𝐴))
127125, 126sylib 208 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ (fi‘𝐴) → (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎𝑏)):(((rec(𝑅, 𝐴) ↾ ω)‘𝑛) × ((rec(𝑅, 𝐴) ↾ ω)‘𝑛))⟶(fi‘𝐴))
128 frn 6040 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎𝑏)):(((rec(𝑅, 𝐴) ↾ ω)‘𝑛) × ((rec(𝑅, 𝐴) ↾ ω)‘𝑛))⟶(fi‘𝐴) → ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎𝑏)) ⊆ (fi‘𝐴))
129127, 128syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ (fi‘𝐴) → ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎𝑏)) ⊆ (fi‘𝐴))
130129adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑛 ∈ ω ∧ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ (fi‘𝐴)) → ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎𝑏)) ⊆ (fi‘𝐴))
131103, 130eqsstrd 3631 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑛 ∈ ω ∧ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ (fi‘𝐴)) → ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛) ⊆ (fi‘𝐴))
132118, 131jctild 565 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑛 ∈ ω ∧ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ (fi‘𝐴)) → (∀𝑦𝑛 ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) → (((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛) ⊆ (fi‘𝐴) ∧ ∀𝑦 ∈ suc 𝑛((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛))))
133132expimpd 628 . . . . . . . . . . . . . . . . . . . . . . . . 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 7079 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ∈ ω → (𝐴𝑉 → (((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ⊆ (fi‘𝐴) ∧ ∀𝑦𝑥 ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥))))
136135impcom 446 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐴𝑉𝑥 ∈ ω) → (((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ⊆ (fi‘𝐴) ∧ ∀𝑦𝑥 ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥)))
137136simprd 479 . . . . . . . . . . . . . . . . . . . . 21 ((𝐴𝑉𝑥 ∈ ω) → ∀𝑦𝑥 ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥))
138137r19.21bi 2929 . . . . . . . . . . . . . . . . . . . 20 (((𝐴𝑉𝑥 ∈ ω) ∧ 𝑦𝑥) → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥))
139138ex 450 . . . . . . . . . . . . . . . . . . 19 ((𝐴𝑉𝑥 ∈ ω) → (𝑦𝑥 → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥)))
140139adantr 481 . . . . . . . . . . . . . . . . . 18 (((𝐴𝑉𝑥 ∈ ω) ∧ 𝑦 ∈ ω) → (𝑦𝑥 → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥)))
141 fveq2 6178 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = 𝑥 → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) = ((rec(𝑅, 𝐴) ↾ ω)‘𝑥))
142 eqimss 3649 . . . . . . . . . . . . . . . . . . . 20 (((rec(𝑅, 𝐴) ↾ ω)‘𝑦) = ((rec(𝑅, 𝐴) ↾ ω)‘𝑥) → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥))
143141, 142syl 17 . . . . . . . . . . . . . . . . . . 19 (𝑦 = 𝑥 → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥))
144143a1i 11 . . . . . . . . . . . . . . . . . 18 (((𝐴𝑉𝑥 ∈ ω) ∧ 𝑦 ∈ ω) → (𝑦 = 𝑥 → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥)))
145140, 144jaod 395 . . . . . . . . . . . . . . . . 17 (((𝐴𝑉𝑥 ∈ ω) ∧ 𝑦 ∈ ω) → ((𝑦𝑥𝑦 = 𝑥) → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥)))
14632, 145sylbid 230 . . . . . . . . . . . . . . . 16 (((𝐴𝑉𝑥 ∈ ω) ∧ 𝑦 ∈ ω) → (𝑦𝑥 → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥)))
147146ralrimiva 2963 . . . . . . . . . . . . . . 15 ((𝐴𝑉𝑥 ∈ ω) → ∀𝑦 ∈ ω (𝑦𝑥 → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥)))
148147ralrimiva 2963 . . . . . . . . . . . . . 14 (𝐴𝑉 → ∀𝑥 ∈ ω ∀𝑦 ∈ ω (𝑦𝑥 → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥)))
149148adantr 481 . . . . . . . . . . . . 13 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) → ∀𝑥 ∈ ω ∀𝑦 ∈ ω (𝑦𝑥 → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥)))
150 ssun1 3768 . . . . . . . . . . . . . 14 𝑚 ⊆ (𝑚𝑛)
151150a1i 11 . . . . . . . . . . . . 13 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) → 𝑚 ⊆ (𝑚𝑛))
152 sseq2 3619 . . . . . . . . . . . . . . 15 (𝑥 = (𝑚𝑛) → (𝑦𝑥𝑦 ⊆ (𝑚𝑛)))
153 fveq2 6178 . . . . . . . . . . . . . . . 16 (𝑥 = (𝑚𝑛) → ((rec(𝑅, 𝐴) ↾ ω)‘𝑥) = ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))
154153sseq2d 3625 . . . . . . . . . . . . . . 15 (𝑥 = (𝑚𝑛) → (((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ↔ ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))))
155152, 154imbi12d 334 . . . . . . . . . . . . . 14 (𝑥 = (𝑚𝑛) → ((𝑦𝑥 → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥)) ↔ (𝑦 ⊆ (𝑚𝑛) → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))))
156 sseq1 3618 . . . . . . . . . . . . . . 15 (𝑦 = 𝑚 → (𝑦 ⊆ (𝑚𝑛) ↔ 𝑚 ⊆ (𝑚𝑛)))
157 fveq2 6178 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑚 → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) = ((rec(𝑅, 𝐴) ↾ ω)‘𝑚))
158157sseq1d 3624 . . . . . . . . . . . . . . 15 (𝑦 = 𝑚 → (((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ↔ ((rec(𝑅, 𝐴) ↾ ω)‘𝑚) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))))
159156, 158imbi12d 334 . . . . . . . . . . . . . 14 (𝑦 = 𝑚 → ((𝑦 ⊆ (𝑚𝑛) → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))) ↔ (𝑚 ⊆ (𝑚𝑛) → ((rec(𝑅, 𝐴) ↾ ω)‘𝑚) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))))
160155, 159rspc2v 3317 . . . . . . . . . . . . 13 (((𝑚𝑛) ∈ ω ∧ 𝑚 ∈ ω) → (∀𝑥 ∈ ω ∀𝑦 ∈ ω (𝑦𝑥 → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥)) → (𝑚 ⊆ (𝑚𝑛) → ((rec(𝑅, 𝐴) ↾ ω)‘𝑚) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))))
16126, 149, 151, 160syl3c 66 . . . . . . . . . . . 12 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) → ((rec(𝑅, 𝐴) ↾ ω)‘𝑚) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))
162161sseld 3594 . . . . . . . . . . 11 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) → (𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑚) → 𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))))
163 simprr 795 . . . . . . . . . . . . . 14 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) → 𝑛 ∈ ω)
16424, 163jca 554 . . . . . . . . . . . . 13 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) → ((𝑚𝑛) ∈ ω ∧ 𝑛 ∈ ω))
165 ssun2 3769 . . . . . . . . . . . . . 14 𝑛 ⊆ (𝑚𝑛)
166165a1i 11 . . . . . . . . . . . . 13 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) → 𝑛 ⊆ (𝑚𝑛))
167 sseq1 3618 . . . . . . . . . . . . . . 15 (𝑦 = 𝑛 → (𝑦 ⊆ (𝑚𝑛) ↔ 𝑛 ⊆ (𝑚𝑛)))
168109sseq1d 3624 . . . . . . . . . . . . . . 15 (𝑦 = 𝑛 → (((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ↔ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))))
169167, 168imbi12d 334 . . . . . . . . . . . . . 14 (𝑦 = 𝑛 → ((𝑦 ⊆ (𝑚𝑛) → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))) ↔ (𝑛 ⊆ (𝑚𝑛) → ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))))
170155, 169rspc2v 3317 . . . . . . . . . . . . 13 (((𝑚𝑛) ∈ ω ∧ 𝑛 ∈ ω) → (∀𝑥 ∈ ω ∀𝑦 ∈ ω (𝑦𝑥 → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥)) → (𝑛 ⊆ (𝑚𝑛) → ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))))
171164, 149, 166, 170syl3c 66 . . . . . . . . . . . 12 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) → ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))
172171sseld 3594 . . . . . . . . . . 11 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) → (𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) → 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))))
17323ad2antlr 762 . . . . . . . . . . . . . . 15 (((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) ∧ (𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ∧ 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))) → (𝑚𝑛) ∈ ω)
174 peano2 7071 . . . . . . . . . . . . . . 15 ((𝑚𝑛) ∈ ω → suc (𝑚𝑛) ∈ ω)
175 fveq2 6178 . . . . . . . . . . . . . . . 16 (𝑥 = suc (𝑚𝑛) → ((rec(𝑅, 𝐴) ↾ ω)‘𝑥) = ((rec(𝑅, 𝐴) ↾ ω)‘suc (𝑚𝑛)))
176175ssiun2s 4555 . . . . . . . . . . . . . . 15 (suc (𝑚𝑛) ∈ ω → ((rec(𝑅, 𝐴) ↾ ω)‘suc (𝑚𝑛)) ⊆ 𝑥 ∈ ω ((rec(𝑅, 𝐴) ↾ ω)‘𝑥))
177173, 174, 1763syl 18 . . . . . . . . . . . . . 14 (((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) ∧ (𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ∧ 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))) → ((rec(𝑅, 𝐴) ↾ ω)‘suc (𝑚𝑛)) ⊆ 𝑥 ∈ ω ((rec(𝑅, 𝐴) ↾ ω)‘𝑥))
178 simprl 793 . . . . . . . . . . . . . . . . . 18 (((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) ∧ (𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ∧ 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))) → 𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))
179 simprr 795 . . . . . . . . . . . . . . . . . 18 (((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) ∧ (𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ∧ 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))) → 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))
180 eqidd 2621 . . . . . . . . . . . . . . . . . 18 (((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) ∧ (𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ∧ 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))) → (𝑐𝑑) = (𝑐𝑑))
181 ineq1 3799 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = 𝑐 → (𝑎𝑏) = (𝑐𝑏))
182181eqeq2d 2630 . . . . . . . . . . . . . . . . . . 19 (𝑎 = 𝑐 → ((𝑐𝑑) = (𝑎𝑏) ↔ (𝑐𝑑) = (𝑐𝑏)))
183 ineq2 3800 . . . . . . . . . . . . . . . . . . . 20 (𝑏 = 𝑑 → (𝑐𝑏) = (𝑐𝑑))
184183eqeq2d 2630 . . . . . . . . . . . . . . . . . . 19 (𝑏 = 𝑑 → ((𝑐𝑑) = (𝑐𝑏) ↔ (𝑐𝑑) = (𝑐𝑑)))
185182, 184rspc2ev 3319 . . . . . . . . . . . . . . . . . 18 ((𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ∧ 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ∧ (𝑐𝑑) = (𝑐𝑑)) → ∃𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))∃𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))(𝑐𝑑) = (𝑎𝑏))
186178, 179, 180, 185syl3anc 1324 . . . . . . . . . . . . . . . . 17 (((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) ∧ (𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ∧ 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))) → ∃𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))∃𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))(𝑐𝑑) = (𝑎𝑏))
187 vex 3198 . . . . . . . . . . . . . . . . . . 19 𝑐 ∈ V
188187inex1 4790 . . . . . . . . . . . . . . . . . 18 (𝑐𝑑) ∈ V
189 eqeq1 2624 . . . . . . . . . . . . . . . . . . 19 (𝑥 = (𝑐𝑑) → (𝑥 = (𝑎𝑏) ↔ (𝑐𝑑) = (𝑎𝑏)))
1901892rexbidv 3053 . . . . . . . . . . . . . . . . . 18 (𝑥 = (𝑐𝑑) → (∃𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))∃𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))𝑥 = (𝑎𝑏) ↔ ∃𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))∃𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))(𝑐𝑑) = (𝑎𝑏)))
191188, 190elab 3344 . . . . . . . . . . . . . . . . 17 ((𝑐𝑑) ∈ {𝑥 ∣ ∃𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))∃𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))𝑥 = (𝑎𝑏)} ↔ ∃𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))∃𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))(𝑐𝑑) = (𝑎𝑏))
192186, 191sylibr 224 . . . . . . . . . . . . . . . 16 (((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) ∧ (𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ∧ 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))) → (𝑐𝑑) ∈ {𝑥 ∣ ∃𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))∃𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))𝑥 = (𝑎𝑏)})
193 eqid 2620 . . . . . . . . . . . . . . . . 17 (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ↦ (𝑎𝑏)) = (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ↦ (𝑎𝑏))
194193rnmpt2 6755 . . . . . . . . . . . . . . . 16 ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ↦ (𝑎𝑏)) = {𝑥 ∣ ∃𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))∃𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))𝑥 = (𝑎𝑏)}
195192, 194syl6eleqr 2710 . . . . . . . . . . . . . . 15 (((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) ∧ (𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ∧ 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))) → (𝑐𝑑) ∈ ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ↦ (𝑎𝑏)))
196 fvex 6188 . . . . . . . . . . . . . . . . . . 19 ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ∈ V
197196uniex 6938 . . . . . . . . . . . . . . . . . 18 ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ∈ V
198197pwex 4839 . . . . . . . . . . . . . . . . 17 𝒫 ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ∈ V
199 elssuni 4458 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) → 𝑎 ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))
20069, 199syl5ss 3606 . . . . . . . . . . . . . . . . . . . . . 22 (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) → (𝑎𝑏) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))
20174elpw 4155 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑎𝑏) ∈ 𝒫 ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ↔ (𝑎𝑏) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))
202200, 201sylibr 224 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) → (𝑎𝑏) ∈ 𝒫 ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))
203202adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ∧ 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))) → (𝑎𝑏) ∈ 𝒫 ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))
204203rgen2a 2974 . . . . . . . . . . . . . . . . . . 19 𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))∀𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))(𝑎𝑏) ∈ 𝒫 ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))
205193fmpt2 7222 . . . . . . . . . . . . . . . . . . 19 (∀𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))∀𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))(𝑎𝑏) ∈ 𝒫 ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ↔ (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ↦ (𝑎𝑏)):(((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) × ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))⟶𝒫 ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))
206204, 205mpbi 220 . . . . . . . . . . . . . . . . . 18 (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ↦ (𝑎𝑏)):(((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) × ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))⟶𝒫 ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))
207 frn 6040 . . . . . . . . . . . . . . . . . 18 ((𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ↦ (𝑎𝑏)):(((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) × ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))⟶𝒫 ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) → ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ↦ (𝑎𝑏)) ⊆ 𝒫 ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))
208206, 207ax-mp 5 . . . . . . . . . . . . . . . . 17 ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ↦ (𝑎𝑏)) ⊆ 𝒫 ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))
209198, 208ssexi 4794 . . . . . . . . . . . . . . . 16 ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ↦ (𝑎𝑏)) ∈ V
210 nfcv 2762 . . . . . . . . . . . . . . . . 17 𝑣(𝑚𝑛)
211 nfcv 2762 . . . . . . . . . . . . . . . . 17 𝑣ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ↦ (𝑎𝑏))
212 mpt2eq12 6700 . . . . . . . . . . . . . . . . . . 19 ((𝑣 = ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ∧ 𝑣 = ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))) → (𝑎𝑣, 𝑏𝑣 ↦ (𝑎𝑏)) = (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ↦ (𝑎𝑏)))
213212anidms 676 . . . . . . . . . . . . . . . . . 18 (𝑣 = ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) → (𝑎𝑣, 𝑏𝑣 ↦ (𝑎𝑏)) = (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ↦ (𝑎𝑏)))
214213rneqd 5342 . . . . . . . . . . . . . . . . 17 (𝑣 = ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) → ran (𝑎𝑣, 𝑏𝑣 ↦ (𝑎𝑏)) = ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ↦ (𝑎𝑏)))
21583, 210, 211, 98, 214frsucmpt 7518 . . . . . . . . . . . . . . . 16 (((𝑚𝑛) ∈ ω ∧ ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ↦ (𝑎𝑏)) ∈ V) → ((rec(𝑅, 𝐴) ↾ ω)‘suc (𝑚𝑛)) = ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ↦ (𝑎𝑏)))
216173, 209, 215sylancl 693 . . . . . . . . . . . . . . 15 (((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) ∧ (𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ∧ 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))) → ((rec(𝑅, 𝐴) ↾ ω)‘suc (𝑚𝑛)) = ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ↦ (𝑎𝑏)))
217195, 216eleqtrrd 2702 . . . . . . . . . . . . . 14 (((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) ∧ (𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ∧ 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))) → (𝑐𝑑) ∈ ((rec(𝑅, 𝐴) ↾ ω)‘suc (𝑚𝑛)))
218177, 217sseldd 3596 . . . . . . . . . . . . 13 (((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) ∧ (𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ∧ 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))) → (𝑐𝑑) ∈ 𝑥 ∈ ω ((rec(𝑅, 𝐴) ↾ ω)‘𝑥))
219 fniunfv 6490 . . . . . . . . . . . . . 14 ((rec(𝑅, 𝐴) ↾ ω) Fn ω → 𝑥 ∈ ω ((rec(𝑅, 𝐴) ↾ ω)‘𝑥) = ran (rec(𝑅, 𝐴) ↾ ω))
2203, 219ax-mp 5 . . . . . . . . . . . . 13 𝑥 ∈ ω ((rec(𝑅, 𝐴) ↾ ω)‘𝑥) = ran (rec(𝑅, 𝐴) ↾ ω)
221218, 220syl6eleq 2709 . . . . . . . . . . . 12 (((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) ∧ (𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ∧ 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))) → (𝑐𝑑) ∈ ran (rec(𝑅, 𝐴) ↾ ω))
222221ex 450 . . . . . . . . . . 11 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) → ((𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ∧ 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))) → (𝑐𝑑) ∈ ran (rec(𝑅, 𝐴) ↾ ω)))
223162, 172, 222syl2and 500 . . . . . . . . . 10 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) → ((𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑚) ∧ 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)) → (𝑐𝑑) ∈ ran (rec(𝑅, 𝐴) ↾ ω)))
224223rexlimdvva 3034 . . . . . . . . 9 (𝐴𝑉 → (∃𝑚 ∈ ω ∃𝑛 ∈ ω (𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑚) ∧ 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)) → (𝑐𝑑) ∈ ran (rec(𝑅, 𝐴) ↾ ω)))
225224imp 445 . . . . . . . 8 ((𝐴𝑉 ∧ ∃𝑚 ∈ ω ∃𝑛 ∈ ω (𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑚) ∧ 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛))) → (𝑐𝑑) ∈ ran (rec(𝑅, 𝐴) ↾ ω))
22620, 225sylan2br 493 . . . . . . 7 ((𝐴𝑉 ∧ (𝑐 ran (rec(𝑅, 𝐴) ↾ ω) ∧ 𝑑 ran (rec(𝑅, 𝐴) ↾ ω))) → (𝑐𝑑) ∈ ran (rec(𝑅, 𝐴) ↾ ω))
227226ralrimivva 2968 . . . . . 6 (𝐴𝑉 → ∀𝑐 ran (rec(𝑅, 𝐴) ↾ ω)∀𝑑 ran (rec(𝑅, 𝐴) ↾ ω)(𝑐𝑑) ∈ ran (rec(𝑅, 𝐴) ↾ ω))
228136simpld 475 . . . . . . . . . . . 12 ((𝐴𝑉𝑥 ∈ ω) → ((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ⊆ (fi‘𝐴))
229 fvex 6188 . . . . . . . . . . . . 13 (fi‘𝐴) ∈ V
230229elpw2 4819 . . . . . . . . . . . 12 (((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ∈ 𝒫 (fi‘𝐴) ↔ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ⊆ (fi‘𝐴))
231228, 230sylibr 224 . . . . . . . . . . 11 ((𝐴𝑉𝑥 ∈ ω) → ((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ∈ 𝒫 (fi‘𝐴))
232231ralrimiva 2963 . . . . . . . . . 10 (𝐴𝑉 → ∀𝑥 ∈ ω ((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ∈ 𝒫 (fi‘𝐴))
233 fnfvrnss 6376 . . . . . . . . . 10 (((rec(𝑅, 𝐴) ↾ ω) Fn ω ∧ ∀𝑥 ∈ ω ((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ∈ 𝒫 (fi‘𝐴)) → ran (rec(𝑅, 𝐴) ↾ ω) ⊆ 𝒫 (fi‘𝐴))
2343, 232, 233sylancr 694 . . . . . . . . 9 (𝐴𝑉 → ran (rec(𝑅, 𝐴) ↾ ω) ⊆ 𝒫 (fi‘𝐴))
235 sspwuni 4602 . . . . . . . . 9 (ran (rec(𝑅, 𝐴) ↾ ω) ⊆ 𝒫 (fi‘𝐴) ↔ ran (rec(𝑅, 𝐴) ↾ ω) ⊆ (fi‘𝐴))
236234, 235sylib 208 . . . . . . . 8 (𝐴𝑉 ran (rec(𝑅, 𝐴) ↾ ω) ⊆ (fi‘𝐴))
237 ssexg 4795 . . . . . . . 8 (( ran (rec(𝑅, 𝐴) ↾ ω) ⊆ (fi‘𝐴) ∧ (fi‘𝐴) ∈ V) → ran (rec(𝑅, 𝐴) ↾ ω) ∈ V)
238236, 229, 237sylancl 693 . . . . . . 7 (𝐴𝑉 ran (rec(𝑅, 𝐴) ↾ ω) ∈ V)
239 sseq2 3619 . . . . . . . . 9 (𝑥 = ran (rec(𝑅, 𝐴) ↾ ω) → (𝐴𝑥𝐴 ran (rec(𝑅, 𝐴) ↾ ω)))
240 eleq2 2688 . . . . . . . . . . 11 (𝑥 = ran (rec(𝑅, 𝐴) ↾ ω) → ((𝑐𝑑) ∈ 𝑥 ↔ (𝑐𝑑) ∈ ran (rec(𝑅, 𝐴) ↾ ω)))
241240raleqbi1dv 3141 . . . . . . . . . 10 (𝑥 = ran (rec(𝑅, 𝐴) ↾ ω) → (∀𝑑𝑥 (𝑐𝑑) ∈ 𝑥 ↔ ∀𝑑 ran (rec(𝑅, 𝐴) ↾ ω)(𝑐𝑑) ∈ ran (rec(𝑅, 𝐴) ↾ ω)))
242241raleqbi1dv 3141 . . . . . . . . 9 (𝑥 = ran (rec(𝑅, 𝐴) ↾ ω) → (∀𝑐𝑥𝑑𝑥 (𝑐𝑑) ∈ 𝑥 ↔ ∀𝑐 ran (rec(𝑅, 𝐴) ↾ ω)∀𝑑 ran (rec(𝑅, 𝐴) ↾ ω)(𝑐𝑑) ∈ ran (rec(𝑅, 𝐴) ↾ ω)))
243239, 242anbi12d 746 . . . . . . . 8 (𝑥 = ran (rec(𝑅, 𝐴) ↾ ω) → ((𝐴𝑥 ∧ ∀𝑐𝑥𝑑𝑥 (𝑐𝑑) ∈ 𝑥) ↔ (𝐴 ran (rec(𝑅, 𝐴) ↾ ω) ∧ ∀𝑐 ran (rec(𝑅, 𝐴) ↾ ω)∀𝑑 ran (rec(𝑅, 𝐴) ↾ ω)(𝑐𝑑) ∈ ran (rec(𝑅, 𝐴) ↾ ω))))
244243elabg 3345 . . . . . . 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 956 . . . . 5 (𝐴𝑉 ran (rec(𝑅, 𝐴) ↾ ω) ∈ {𝑥 ∣ (𝐴𝑥 ∧ ∀𝑐𝑥𝑑𝑥 (𝑐𝑑) ∈ 𝑥)})
247 intss1 4483 . . . . 5 ( ran (rec(𝑅, 𝐴) ↾ ω) ∈ {𝑥 ∣ (𝐴𝑥 ∧ ∀𝑐𝑥𝑑𝑥 (𝑐𝑑) ∈ 𝑥)} → {𝑥 ∣ (𝐴𝑥 ∧ ∀𝑐𝑥𝑑𝑥 (𝑐𝑑) ∈ 𝑥)} ⊆ ran (rec(𝑅, 𝐴) ↾ ω))
248246, 247syl 17 . . . 4 (𝐴𝑉 {𝑥 ∣ (𝐴𝑥 ∧ ∀𝑐𝑥𝑑𝑥 (𝑐𝑑) ∈ 𝑥)} ⊆ ran (rec(𝑅, 𝐴) ↾ ω))
2491, 248eqsstrd 3631 . . 3 (𝐴𝑉 → (fi‘𝐴) ⊆ ran (rec(𝑅, 𝐴) ↾ ω))
250249, 236eqssd 3612 . 2 (𝐴𝑉 → (fi‘𝐴) = ran (rec(𝑅, 𝐴) ↾ ω))
251 df-ima 5117 . . 3 (rec(𝑅, 𝐴) “ ω) = ran (rec(𝑅, 𝐴) ↾ ω)
252251unieqi 4436 . 2 (rec(𝑅, 𝐴) “ ω) = ran (rec(𝑅, 𝐴) ↾ ω)
253250, 252syl6eqr 2672 1 (𝐴𝑉 → (fi‘𝐴) = (rec(𝑅, 𝐴) “ ω))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wo 383  wa 384   = wceq 1481  wcel 1988  {cab 2606  wral 2909  wrex 2910  Vcvv 3195  cun 3565  cin 3566  wss 3567  c0 3907  𝒫 cpw 4149  {csn 4168   cuni 4427   cint 4466   ciun 4511  cmpt 4720   × cxp 5102  ran crn 5105  cres 5106  cima 5107  Ord word 5710  Oncon0 5711  suc csuc 5713   Fn wfn 5871  wf 5872  cfv 5876  cmpt2 6637  ωcom 7050  reccrdg 7490  ficfi 8301
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-8 1990  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-sep 4772  ax-nul 4780  ax-pow 4834  ax-pr 4897  ax-un 6934
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-eu 2472  df-mo 2473  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ne 2792  df-ral 2914  df-rex 2915  df-reu 2916  df-rab 2918  df-v 3197  df-sbc 3430  df-csb 3527  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-pss 3583  df-nul 3908  df-if 4078  df-pw 4151  df-sn 4169  df-pr 4171  df-tp 4173  df-op 4175  df-uni 4428  df-int 4467  df-iun 4513  df-br 4645  df-opab 4704  df-mpt 4721  df-tr 4744  df-id 5014  df-eprel 5019  df-po 5025  df-so 5026  df-fr 5063  df-we 5065  df-xp 5110  df-rel 5111  df-cnv 5112  df-co 5113  df-dm 5114  df-rn 5115  df-res 5116  df-ima 5117  df-pred 5668  df-ord 5714  df-on 5715  df-lim 5716  df-suc 5717  df-iota 5839  df-fun 5878  df-fn 5879  df-f 5880  df-f1 5881  df-fo 5882  df-f1o 5883  df-fv 5884  df-ov 6638  df-oprab 6639  df-mpt2 6640  df-om 7051  df-1st 7153  df-2nd 7154  df-wrecs 7392  df-recs 7453  df-rdg 7491  df-1o 7545  df-oadd 7549  df-er 7727  df-en 7941  df-fin 7944  df-fi 8302
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator