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

Theorem dffi3 8378
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 8370 . . . 4 (𝐴𝑉 → (fi‘𝐴) = {𝑥 ∣ (𝐴𝑥 ∧ ∀𝑐𝑥𝑑𝑥 (𝑐𝑑) ∈ 𝑥)})
2 fr0g 7576 . . . . . . . 8 (𝐴𝑉 → ((rec(𝑅, 𝐴) ↾ ω)‘∅) = 𝐴)
3 frfnom 7575 . . . . . . . . 9 (rec(𝑅, 𝐴) ↾ ω) Fn ω
4 peano1 7127 . . . . . . . . 9 ∅ ∈ ω
5 fnfvelrn 6396 . . . . . . . . 9 (((rec(𝑅, 𝐴) ↾ ω) Fn ω ∧ ∅ ∈ ω) → ((rec(𝑅, 𝐴) ↾ ω)‘∅) ∈ ran (rec(𝑅, 𝐴) ↾ ω))
63, 4, 5mp2an 708 . . . . . . . 8 ((rec(𝑅, 𝐴) ↾ ω)‘∅) ∈ ran (rec(𝑅, 𝐴) ↾ ω)
72, 6syl6eqelr 2739 . . . . . . 7 (𝐴𝑉𝐴 ∈ ran (rec(𝑅, 𝐴) ↾ ω))
8 elssuni 4499 . . . . . . 7 (𝐴 ∈ ran (rec(𝑅, 𝐴) ↾ ω) → 𝐴 ran (rec(𝑅, 𝐴) ↾ ω))
97, 8syl 17 . . . . . 6 (𝐴𝑉𝐴 ran (rec(𝑅, 𝐴) ↾ ω))
10 reeanv 3136 . . . . . . . . 9 (∃𝑚 ∈ ω ∃𝑛 ∈ ω (𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑚) ∧ 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)) ↔ (∃𝑚 ∈ ω 𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑚) ∧ ∃𝑛 ∈ ω 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)))
11 eliun 4556 . . . . . . . . . 10 (𝑐 𝑚 ∈ ω ((rec(𝑅, 𝐴) ↾ ω)‘𝑚) ↔ ∃𝑚 ∈ ω 𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑚))
12 eliun 4556 . . . . . . . . . 10 (𝑑 𝑛 ∈ ω ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↔ ∃𝑛 ∈ ω 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛))
1311, 12anbi12i 733 . . . . . . . . 9 ((𝑐 𝑚 ∈ ω ((rec(𝑅, 𝐴) ↾ ω)‘𝑚) ∧ 𝑑 𝑛 ∈ ω ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)) ↔ (∃𝑚 ∈ ω 𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑚) ∧ ∃𝑛 ∈ ω 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)))
14 fniunfv 6545 . . . . . . . . . . . 12 ((rec(𝑅, 𝐴) ↾ ω) Fn ω → 𝑚 ∈ ω ((rec(𝑅, 𝐴) ↾ ω)‘𝑚) = ran (rec(𝑅, 𝐴) ↾ ω))
1514eleq2d 2716 . . . . . . . . . . 11 ((rec(𝑅, 𝐴) ↾ ω) Fn ω → (𝑐 𝑚 ∈ ω ((rec(𝑅, 𝐴) ↾ ω)‘𝑚) ↔ 𝑐 ran (rec(𝑅, 𝐴) ↾ ω)))
16 fniunfv 6545 . . . . . . . . . . . 12 ((rec(𝑅, 𝐴) ↾ ω) Fn ω → 𝑛 ∈ ω ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) = ran (rec(𝑅, 𝐴) ↾ ω))
1716eleq2d 2716 . . . . . . . . . . 11 ((rec(𝑅, 𝐴) ↾ ω) Fn ω → (𝑑 𝑛 ∈ ω ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↔ 𝑑 ran (rec(𝑅, 𝐴) ↾ ω)))
1815, 17anbi12d 747 . . . . . . . . . 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 7116 . . . . . . . . . . . . . . . 16 Ord ω
22 ordunel 7069 . . . . . . . . . . . . . . . 16 ((Ord ω ∧ 𝑚 ∈ ω ∧ 𝑛 ∈ ω) → (𝑚𝑛) ∈ ω)
2321, 22mp3an1 1451 . . . . . . . . . . . . . . 15 ((𝑚 ∈ ω ∧ 𝑛 ∈ ω) → (𝑚𝑛) ∈ ω)
2423adantl 481 . . . . . . . . . . . . . 14 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) → (𝑚𝑛) ∈ ω)
25 simprl 809 . . . . . . . . . . . . . 14 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) → 𝑚 ∈ ω)
2624, 25jca 553 . . . . . . . . . . . . 13 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) → ((𝑚𝑛) ∈ ω ∧ 𝑚 ∈ ω))
27 nnon 7113 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ ω → 𝑦 ∈ On)
2827adantl 481 . . . . . . . . . . . . . . . . . 18 (((𝐴𝑉𝑥 ∈ ω) ∧ 𝑦 ∈ ω) → 𝑦 ∈ On)
29 nnon 7113 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ω → 𝑥 ∈ On)
3029ad2antlr 763 . . . . . . . . . . . . . . . . . 18 (((𝐴𝑉𝑥 ∈ ω) ∧ 𝑦 ∈ ω) → 𝑥 ∈ On)
31 onsseleq 5803 . . . . . . . . . . . . . . . . . 18 ((𝑦 ∈ On ∧ 𝑥 ∈ On) → (𝑦𝑥 ↔ (𝑦𝑥𝑦 = 𝑥)))
3228, 30, 31syl2anc 694 . . . . . . . . . . . . . . . . 17 (((𝐴𝑉𝑥 ∈ ω) ∧ 𝑦 ∈ ω) → (𝑦𝑥 ↔ (𝑦𝑥𝑦 = 𝑥)))
33 rzal 4106 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 = ∅ → ∀𝑦𝑥 ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥))
3433biantrud 527 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = ∅ → (((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ⊆ (fi‘𝐴) ↔ (((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ⊆ (fi‘𝐴) ∧ ∀𝑦𝑥 ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥))))
35 fveq2 6229 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 = ∅ → ((rec(𝑅, 𝐴) ↾ ω)‘𝑥) = ((rec(𝑅, 𝐴) ↾ ω)‘∅))
3635sseq1d 3665 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = ∅ → (((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ⊆ (fi‘𝐴) ↔ ((rec(𝑅, 𝐴) ↾ ω)‘∅) ⊆ (fi‘𝐴)))
3734, 36bitr3d 270 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = ∅ → ((((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ⊆ (fi‘𝐴) ∧ ∀𝑦𝑥 ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥)) ↔ ((rec(𝑅, 𝐴) ↾ ω)‘∅) ⊆ (fi‘𝐴)))
38 fveq2 6229 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 = 𝑛 → ((rec(𝑅, 𝐴) ↾ ω)‘𝑥) = ((rec(𝑅, 𝐴) ↾ ω)‘𝑛))
3938sseq1d 3665 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = 𝑛 → (((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ⊆ (fi‘𝐴) ↔ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ (fi‘𝐴)))
4038sseq2d 3666 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 = 𝑛 → (((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ↔ ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)))
4140raleqbi1dv 3176 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = 𝑛 → (∀𝑦𝑥 ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ↔ ∀𝑦𝑛 ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)))
4239, 41anbi12d 747 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = 𝑛 → ((((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ⊆ (fi‘𝐴) ∧ ∀𝑦𝑥 ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥)) ↔ (((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ (fi‘𝐴) ∧ ∀𝑦𝑛 ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛))))
43 fveq2 6229 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 = suc 𝑛 → ((rec(𝑅, 𝐴) ↾ ω)‘𝑥) = ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛))
4443sseq1d 3665 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = suc 𝑛 → (((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ⊆ (fi‘𝐴) ↔ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛) ⊆ (fi‘𝐴)))
4543sseq2d 3666 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 = suc 𝑛 → (((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ↔ ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛)))
4645raleqbi1dv 3176 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = suc 𝑛 → (∀𝑦𝑥 ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ↔ ∀𝑦 ∈ suc 𝑛((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛)))
4744, 46anbi12d 747 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = suc 𝑛 → ((((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ⊆ (fi‘𝐴) ∧ ∀𝑦𝑥 ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥)) ↔ (((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛) ⊆ (fi‘𝐴) ∧ ∀𝑦 ∈ suc 𝑛((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛))))
48 ssfii 8366 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐴𝑉𝐴 ⊆ (fi‘𝐴))
492, 48eqsstrd 3672 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐴𝑉 → ((rec(𝑅, 𝐴) ↾ ω)‘∅) ⊆ (fi‘𝐴))
50 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑥 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) → 𝑥 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛))
51 eqidd 2652 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑥 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) → 𝑥 = 𝑥)
52 ineq1 3840 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑎 = 𝑥 → (𝑎𝑏) = (𝑥𝑏))
5352eqeq2d 2661 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑎 = 𝑥 → (𝑥 = (𝑎𝑏) ↔ 𝑥 = (𝑥𝑏)))
54 ineq2 3841 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑏 = 𝑥 → (𝑥𝑏) = (𝑥𝑥))
55 inidm 3855 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑥𝑥) = 𝑥
5654, 55syl6eq 2701 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑏 = 𝑥 → (𝑥𝑏) = 𝑥)
5756eqeq2d 2661 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑏 = 𝑥 → (𝑥 = (𝑥𝑏) ↔ 𝑥 = 𝑥))
5853, 57rspc2ev 3355 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑥 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ∧ 𝑥 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ∧ 𝑥 = 𝑥) → ∃𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)∃𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)𝑥 = (𝑎𝑏))
5950, 50, 51, 58syl3anc 1366 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑥 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) → ∃𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)∃𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)𝑥 = (𝑎𝑏))
60 eqid 2651 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎𝑏)) = (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎𝑏))
6160rnmpt2 6812 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎𝑏)) = {𝑥 ∣ ∃𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)∃𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)𝑥 = (𝑎𝑏)}
6261abeq2i 2764 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑥 ∈ ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎𝑏)) ↔ ∃𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)∃𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)𝑥 = (𝑎𝑏))
6359, 62sylibr 224 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑥 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) → 𝑥 ∈ ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎𝑏)))
6463ssriv 3640 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎𝑏))
65 simpl 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑛 ∈ ω ∧ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ (fi‘𝐴)) → 𝑛 ∈ ω)
66 fvex 6239 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ∈ V
6766uniex 6995 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ∈ V
6867pwex 4878 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 𝒫 ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ∈ V
69 inss1 3866 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑎𝑏) ⊆ 𝑎
70 elssuni 4499 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) → 𝑎 ((rec(𝑅, 𝐴) ↾ ω)‘𝑛))
7170adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ∧ 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)) → 𝑎 ((rec(𝑅, 𝐴) ↾ ω)‘𝑛))
7269, 71syl5ss 3647 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ∧ 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)) → (𝑎𝑏) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛))
73 vex 3234 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 𝑎 ∈ V
7473inex1 4832 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑎𝑏) ∈ V
7574elpw 4197 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑎𝑏) ∈ 𝒫 ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↔ (𝑎𝑏) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛))
7672, 75sylibr 224 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ∧ 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)) → (𝑎𝑏) ∈ 𝒫 ((rec(𝑅, 𝐴) ↾ ω)‘𝑛))
7776rgen2a 3006 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)∀𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)(𝑎𝑏) ∈ 𝒫 ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)
7860fmpt2 7282 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (∀𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)∀𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)(𝑎𝑏) ∈ 𝒫 ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↔ (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎𝑏)):(((rec(𝑅, 𝐴) ↾ ω)‘𝑛) × ((rec(𝑅, 𝐴) ↾ ω)‘𝑛))⟶𝒫 ((rec(𝑅, 𝐴) ↾ ω)‘𝑛))
7977, 78mpbi 220 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎𝑏)):(((rec(𝑅, 𝐴) ↾ ω)‘𝑛) × ((rec(𝑅, 𝐴) ↾ ω)‘𝑛))⟶𝒫 ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)
80 frn 6091 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎𝑏)):(((rec(𝑅, 𝐴) ↾ ω)‘𝑛) × ((rec(𝑅, 𝐴) ↾ ω)‘𝑛))⟶𝒫 ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) → ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎𝑏)) ⊆ 𝒫 ((rec(𝑅, 𝐴) ↾ ω)‘𝑛))
8179, 80ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎𝑏)) ⊆ 𝒫 ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)
8268, 81ssexi 4836 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎𝑏)) ∈ V
83 nfcv 2793 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 𝑣𝐴
84 nfcv 2793 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 𝑣𝑛
85 nfcv 2793 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 𝑣ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎𝑏))
86 dffi3.1 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 𝑅 = (𝑢 ∈ V ↦ ran (𝑦𝑢, 𝑧𝑢 ↦ (𝑦𝑧)))
87 mpt2eq12 6757 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝑢 = 𝑣𝑢 = 𝑣) → (𝑦𝑢, 𝑧𝑢 ↦ (𝑦𝑧)) = (𝑦𝑣, 𝑧𝑣 ↦ (𝑦𝑧)))
8887anidms 678 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝑢 = 𝑣 → (𝑦𝑢, 𝑧𝑢 ↦ (𝑦𝑧)) = (𝑦𝑣, 𝑧𝑣 ↦ (𝑦𝑧)))
89 ineq1 3840 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝑦 = 𝑎 → (𝑦𝑧) = (𝑎𝑧))
90 ineq2 3841 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝑧 = 𝑏 → (𝑎𝑧) = (𝑎𝑏))
9189, 90cbvmpt2v 6777 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝑦𝑣, 𝑧𝑣 ↦ (𝑦𝑧)) = (𝑎𝑣, 𝑏𝑣 ↦ (𝑎𝑏))
9288, 91syl6eq 2701 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑢 = 𝑣 → (𝑦𝑢, 𝑧𝑢 ↦ (𝑦𝑧)) = (𝑎𝑣, 𝑏𝑣 ↦ (𝑎𝑏)))
9392rneqd 5385 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑢 = 𝑣 → ran (𝑦𝑢, 𝑧𝑢 ↦ (𝑦𝑧)) = ran (𝑎𝑣, 𝑏𝑣 ↦ (𝑎𝑏)))
9493cbvmptv 4783 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑢 ∈ V ↦ ran (𝑦𝑢, 𝑧𝑢 ↦ (𝑦𝑧))) = (𝑣 ∈ V ↦ ran (𝑎𝑣, 𝑏𝑣 ↦ (𝑎𝑏)))
9586, 94eqtri 2673 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 𝑅 = (𝑣 ∈ V ↦ ran (𝑎𝑣, 𝑏𝑣 ↦ (𝑎𝑏)))
96 rdgeq1 7552 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑅 = (𝑣 ∈ V ↦ ran (𝑎𝑣, 𝑏𝑣 ↦ (𝑎𝑏))) → rec(𝑅, 𝐴) = rec((𝑣 ∈ V ↦ ran (𝑎𝑣, 𝑏𝑣 ↦ (𝑎𝑏))), 𝐴))
9795, 96ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 rec(𝑅, 𝐴) = rec((𝑣 ∈ V ↦ ran (𝑎𝑣, 𝑏𝑣 ↦ (𝑎𝑏))), 𝐴)
9897reseq1i 5424 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (rec(𝑅, 𝐴) ↾ ω) = (rec((𝑣 ∈ V ↦ ran (𝑎𝑣, 𝑏𝑣 ↦ (𝑎𝑏))), 𝐴) ↾ ω)
99 mpt2eq12 6757 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑣 = ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ∧ 𝑣 = ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)) → (𝑎𝑣, 𝑏𝑣 ↦ (𝑎𝑏)) = (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎𝑏)))
10099anidms 678 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑣 = ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) → (𝑎𝑣, 𝑏𝑣 ↦ (𝑎𝑏)) = (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎𝑏)))
101100rneqd 5385 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑣 = ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) → ran (𝑎𝑣, 𝑏𝑣 ↦ (𝑎𝑏)) = ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎𝑏)))
10283, 84, 85, 98, 101frsucmpt 7578 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑛 ∈ ω ∧ ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎𝑏)) ∈ V) → ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛) = ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎𝑏)))
10365, 82, 102sylancl 695 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑛 ∈ ω ∧ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ (fi‘𝐴)) → ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛) = ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎𝑏)))
10464, 103syl5sseqr 3687 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑛 ∈ ω ∧ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ (fi‘𝐴)) → ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛))
105 sstr2 3643 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) → (((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛) → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛)))
106104, 105syl5com 31 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑛 ∈ ω ∧ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ (fi‘𝐴)) → (((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛)))
107106ralimdv 2992 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑛 ∈ ω ∧ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ (fi‘𝐴)) → (∀𝑦𝑛 ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) → ∀𝑦𝑛 ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛)))
108 vex 3234 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 𝑛 ∈ V
109 fveq2 6229 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑦 = 𝑛 → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) = ((rec(𝑅, 𝐴) ↾ ω)‘𝑛))
110109sseq1d 3665 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑦 = 𝑛 → (((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛) ↔ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛)))
111108, 110ralsn 4254 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5767 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 suc 𝑛 = (𝑛 ∪ {𝑛})
115114raleqi 3172 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (∀𝑦 ∈ suc 𝑛((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛) ↔ ∀𝑦 ∈ (𝑛 ∪ {𝑛})((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛))
116 ralunb 3827 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 8369 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑎 ∈ (fi‘𝐴) ∧ 𝑏 ∈ (fi‘𝐴)) → (𝑎𝑏) ∈ (fi‘𝐴))
120119rgen2a 3006 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 𝑎 ∈ (fi‘𝐴)∀𝑏 ∈ (fi‘𝐴)(𝑎𝑏) ∈ (fi‘𝐴)
121 ssralv 3699 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ (fi‘𝐴) → (∀𝑏 ∈ (fi‘𝐴)(𝑎𝑏) ∈ (fi‘𝐴) → ∀𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)(𝑎𝑏) ∈ (fi‘𝐴)))
122121ralimdv 2992 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ (fi‘𝐴) → (∀𝑎 ∈ (fi‘𝐴)∀𝑏 ∈ (fi‘𝐴)(𝑎𝑏) ∈ (fi‘𝐴) → ∀𝑎 ∈ (fi‘𝐴)∀𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)(𝑎𝑏) ∈ (fi‘𝐴)))
123 ssralv 3699 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 7282 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (∀𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)∀𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)(𝑎𝑏) ∈ (fi‘𝐴) ↔ (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎𝑏)):(((rec(𝑅, 𝐴) ↾ ω)‘𝑛) × ((rec(𝑅, 𝐴) ↾ ω)‘𝑛))⟶(fi‘𝐴))
127125, 126sylib 208 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ (fi‘𝐴) → (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎𝑏)):(((rec(𝑅, 𝐴) ↾ ω)‘𝑛) × ((rec(𝑅, 𝐴) ↾ ω)‘𝑛))⟶(fi‘𝐴))
128 frn 6091 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎𝑏)):(((rec(𝑅, 𝐴) ↾ ω)‘𝑛) × ((rec(𝑅, 𝐴) ↾ ω)‘𝑛))⟶(fi‘𝐴) → ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎𝑏)) ⊆ (fi‘𝐴))
129127, 128syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ (fi‘𝐴) → ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎𝑏)) ⊆ (fi‘𝐴))
130129adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑛 ∈ ω ∧ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ (fi‘𝐴)) → ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎𝑏)) ⊆ (fi‘𝐴))
131103, 130eqsstrd 3672 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 7136 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ∈ ω → (𝐴𝑉 → (((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ⊆ (fi‘𝐴) ∧ ∀𝑦𝑥 ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥))))
136135impcom 445 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐴𝑉𝑥 ∈ ω) → (((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ⊆ (fi‘𝐴) ∧ ∀𝑦𝑥 ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥)))
137136simprd 478 . . . . . . . . . . . . . . . . . . . . 21 ((𝐴𝑉𝑥 ∈ ω) → ∀𝑦𝑥 ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥))
138137r19.21bi 2961 . . . . . . . . . . . . . . . . . . . 20 (((𝐴𝑉𝑥 ∈ ω) ∧ 𝑦𝑥) → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥))
139138ex 449 . . . . . . . . . . . . . . . . . . 19 ((𝐴𝑉𝑥 ∈ ω) → (𝑦𝑥 → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥)))
140139adantr 480 . . . . . . . . . . . . . . . . . 18 (((𝐴𝑉𝑥 ∈ ω) ∧ 𝑦 ∈ ω) → (𝑦𝑥 → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥)))
141 fveq2 6229 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = 𝑥 → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) = ((rec(𝑅, 𝐴) ↾ ω)‘𝑥))
142 eqimss 3690 . . . . . . . . . . . . . . . . . . . 20 (((rec(𝑅, 𝐴) ↾ ω)‘𝑦) = ((rec(𝑅, 𝐴) ↾ ω)‘𝑥) → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥))
143141, 142syl 17 . . . . . . . . . . . . . . . . . . 19 (𝑦 = 𝑥 → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥))
144143a1i 11 . . . . . . . . . . . . . . . . . 18 (((𝐴𝑉𝑥 ∈ ω) ∧ 𝑦 ∈ ω) → (𝑦 = 𝑥 → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥)))
145140, 144jaod 394 . . . . . . . . . . . . . . . . 17 (((𝐴𝑉𝑥 ∈ ω) ∧ 𝑦 ∈ ω) → ((𝑦𝑥𝑦 = 𝑥) → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥)))
14632, 145sylbid 230 . . . . . . . . . . . . . . . 16 (((𝐴𝑉𝑥 ∈ ω) ∧ 𝑦 ∈ ω) → (𝑦𝑥 → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥)))
147146ralrimiva 2995 . . . . . . . . . . . . . . 15 ((𝐴𝑉𝑥 ∈ ω) → ∀𝑦 ∈ ω (𝑦𝑥 → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥)))
148147ralrimiva 2995 . . . . . . . . . . . . . 14 (𝐴𝑉 → ∀𝑥 ∈ ω ∀𝑦 ∈ ω (𝑦𝑥 → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥)))
149148adantr 480 . . . . . . . . . . . . 13 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) → ∀𝑥 ∈ ω ∀𝑦 ∈ ω (𝑦𝑥 → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥)))
150 ssun1 3809 . . . . . . . . . . . . . 14 𝑚 ⊆ (𝑚𝑛)
151150a1i 11 . . . . . . . . . . . . 13 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) → 𝑚 ⊆ (𝑚𝑛))
152 sseq2 3660 . . . . . . . . . . . . . . 15 (𝑥 = (𝑚𝑛) → (𝑦𝑥𝑦 ⊆ (𝑚𝑛)))
153 fveq2 6229 . . . . . . . . . . . . . . . 16 (𝑥 = (𝑚𝑛) → ((rec(𝑅, 𝐴) ↾ ω)‘𝑥) = ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))
154153sseq2d 3666 . . . . . . . . . . . . . . 15 (𝑥 = (𝑚𝑛) → (((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ↔ ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))))
155152, 154imbi12d 333 . . . . . . . . . . . . . 14 (𝑥 = (𝑚𝑛) → ((𝑦𝑥 → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥)) ↔ (𝑦 ⊆ (𝑚𝑛) → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))))
156 sseq1 3659 . . . . . . . . . . . . . . 15 (𝑦 = 𝑚 → (𝑦 ⊆ (𝑚𝑛) ↔ 𝑚 ⊆ (𝑚𝑛)))
157 fveq2 6229 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑚 → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) = ((rec(𝑅, 𝐴) ↾ ω)‘𝑚))
158157sseq1d 3665 . . . . . . . . . . . . . . 15 (𝑦 = 𝑚 → (((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ↔ ((rec(𝑅, 𝐴) ↾ ω)‘𝑚) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))))
159156, 158imbi12d 333 . . . . . . . . . . . . . 14 (𝑦 = 𝑚 → ((𝑦 ⊆ (𝑚𝑛) → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))) ↔ (𝑚 ⊆ (𝑚𝑛) → ((rec(𝑅, 𝐴) ↾ ω)‘𝑚) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))))
160155, 159rspc2v 3353 . . . . . . . . . . . . 13 (((𝑚𝑛) ∈ ω ∧ 𝑚 ∈ ω) → (∀𝑥 ∈ ω ∀𝑦 ∈ ω (𝑦𝑥 → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥)) → (𝑚 ⊆ (𝑚𝑛) → ((rec(𝑅, 𝐴) ↾ ω)‘𝑚) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))))
16126, 149, 151, 160syl3c 66 . . . . . . . . . . . 12 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) → ((rec(𝑅, 𝐴) ↾ ω)‘𝑚) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))
162161sseld 3635 . . . . . . . . . . 11 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) → (𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑚) → 𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))))
163 simprr 811 . . . . . . . . . . . . . 14 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) → 𝑛 ∈ ω)
16424, 163jca 553 . . . . . . . . . . . . 13 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) → ((𝑚𝑛) ∈ ω ∧ 𝑛 ∈ ω))
165 ssun2 3810 . . . . . . . . . . . . . 14 𝑛 ⊆ (𝑚𝑛)
166165a1i 11 . . . . . . . . . . . . 13 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) → 𝑛 ⊆ (𝑚𝑛))
167 sseq1 3659 . . . . . . . . . . . . . . 15 (𝑦 = 𝑛 → (𝑦 ⊆ (𝑚𝑛) ↔ 𝑛 ⊆ (𝑚𝑛)))
168109sseq1d 3665 . . . . . . . . . . . . . . 15 (𝑦 = 𝑛 → (((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ↔ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))))
169167, 168imbi12d 333 . . . . . . . . . . . . . 14 (𝑦 = 𝑛 → ((𝑦 ⊆ (𝑚𝑛) → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))) ↔ (𝑛 ⊆ (𝑚𝑛) → ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))))
170155, 169rspc2v 3353 . . . . . . . . . . . . 13 (((𝑚𝑛) ∈ ω ∧ 𝑛 ∈ ω) → (∀𝑥 ∈ ω ∀𝑦 ∈ ω (𝑦𝑥 → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥)) → (𝑛 ⊆ (𝑚𝑛) → ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))))
171164, 149, 166, 170syl3c 66 . . . . . . . . . . . 12 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) → ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))
172171sseld 3635 . . . . . . . . . . 11 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) → (𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) → 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))))
17323ad2antlr 763 . . . . . . . . . . . . . . 15 (((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) ∧ (𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ∧ 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))) → (𝑚𝑛) ∈ ω)
174 peano2 7128 . . . . . . . . . . . . . . 15 ((𝑚𝑛) ∈ ω → suc (𝑚𝑛) ∈ ω)
175 fveq2 6229 . . . . . . . . . . . . . . . 16 (𝑥 = suc (𝑚𝑛) → ((rec(𝑅, 𝐴) ↾ ω)‘𝑥) = ((rec(𝑅, 𝐴) ↾ ω)‘suc (𝑚𝑛)))
176175ssiun2s 4596 . . . . . . . . . . . . . . 15 (suc (𝑚𝑛) ∈ ω → ((rec(𝑅, 𝐴) ↾ ω)‘suc (𝑚𝑛)) ⊆ 𝑥 ∈ ω ((rec(𝑅, 𝐴) ↾ ω)‘𝑥))
177173, 174, 1763syl 18 . . . . . . . . . . . . . 14 (((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) ∧ (𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ∧ 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))) → ((rec(𝑅, 𝐴) ↾ ω)‘suc (𝑚𝑛)) ⊆ 𝑥 ∈ ω ((rec(𝑅, 𝐴) ↾ ω)‘𝑥))
178 simprl 809 . . . . . . . . . . . . . . . . . 18 (((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) ∧ (𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ∧ 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))) → 𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))
179 simprr 811 . . . . . . . . . . . . . . . . . 18 (((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) ∧ (𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ∧ 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))) → 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))
180 eqidd 2652 . . . . . . . . . . . . . . . . . 18 (((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) ∧ (𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ∧ 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))) → (𝑐𝑑) = (𝑐𝑑))
181 ineq1 3840 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = 𝑐 → (𝑎𝑏) = (𝑐𝑏))
182181eqeq2d 2661 . . . . . . . . . . . . . . . . . . 19 (𝑎 = 𝑐 → ((𝑐𝑑) = (𝑎𝑏) ↔ (𝑐𝑑) = (𝑐𝑏)))
183 ineq2 3841 . . . . . . . . . . . . . . . . . . . 20 (𝑏 = 𝑑 → (𝑐𝑏) = (𝑐𝑑))
184183eqeq2d 2661 . . . . . . . . . . . . . . . . . . 19 (𝑏 = 𝑑 → ((𝑐𝑑) = (𝑐𝑏) ↔ (𝑐𝑑) = (𝑐𝑑)))
185182, 184rspc2ev 3355 . . . . . . . . . . . . . . . . . 18 ((𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ∧ 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ∧ (𝑐𝑑) = (𝑐𝑑)) → ∃𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))∃𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))(𝑐𝑑) = (𝑎𝑏))
186178, 179, 180, 185syl3anc 1366 . . . . . . . . . . . . . . . . 17 (((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) ∧ (𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ∧ 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))) → ∃𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))∃𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))(𝑐𝑑) = (𝑎𝑏))
187 vex 3234 . . . . . . . . . . . . . . . . . . 19 𝑐 ∈ V
188187inex1 4832 . . . . . . . . . . . . . . . . . 18 (𝑐𝑑) ∈ V
189 eqeq1 2655 . . . . . . . . . . . . . . . . . . 19 (𝑥 = (𝑐𝑑) → (𝑥 = (𝑎𝑏) ↔ (𝑐𝑑) = (𝑎𝑏)))
1901892rexbidv 3086 . . . . . . . . . . . . . . . . . 18 (𝑥 = (𝑐𝑑) → (∃𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))∃𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))𝑥 = (𝑎𝑏) ↔ ∃𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))∃𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))(𝑐𝑑) = (𝑎𝑏)))
191188, 190elab 3382 . . . . . . . . . . . . . . . . 17 ((𝑐𝑑) ∈ {𝑥 ∣ ∃𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))∃𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))𝑥 = (𝑎𝑏)} ↔ ∃𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))∃𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))(𝑐𝑑) = (𝑎𝑏))
192186, 191sylibr 224 . . . . . . . . . . . . . . . 16 (((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) ∧ (𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ∧ 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))) → (𝑐𝑑) ∈ {𝑥 ∣ ∃𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))∃𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))𝑥 = (𝑎𝑏)})
193 eqid 2651 . . . . . . . . . . . . . . . . 17 (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ↦ (𝑎𝑏)) = (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ↦ (𝑎𝑏))
194193rnmpt2 6812 . . . . . . . . . . . . . . . 16 ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ↦ (𝑎𝑏)) = {𝑥 ∣ ∃𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))∃𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))𝑥 = (𝑎𝑏)}
195192, 194syl6eleqr 2741 . . . . . . . . . . . . . . 15 (((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) ∧ (𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ∧ 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))) → (𝑐𝑑) ∈ ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ↦ (𝑎𝑏)))
196 fvex 6239 . . . . . . . . . . . . . . . . . . 19 ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ∈ V
197196uniex 6995 . . . . . . . . . . . . . . . . . 18 ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ∈ V
198197pwex 4878 . . . . . . . . . . . . . . . . 17 𝒫 ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ∈ V
199 elssuni 4499 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) → 𝑎 ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))
20069, 199syl5ss 3647 . . . . . . . . . . . . . . . . . . . . . 22 (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) → (𝑎𝑏) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))
20174elpw 4197 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑎𝑏) ∈ 𝒫 ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ↔ (𝑎𝑏) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))
202200, 201sylibr 224 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) → (𝑎𝑏) ∈ 𝒫 ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))
203202adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ∧ 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))) → (𝑎𝑏) ∈ 𝒫 ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))
204203rgen2a 3006 . . . . . . . . . . . . . . . . . . 19 𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))∀𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))(𝑎𝑏) ∈ 𝒫 ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))
205193fmpt2 7282 . . . . . . . . . . . . . . . . . . 19 (∀𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))∀𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))(𝑎𝑏) ∈ 𝒫 ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ↔ (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ↦ (𝑎𝑏)):(((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) × ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))⟶𝒫 ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))
206204, 205mpbi 220 . . . . . . . . . . . . . . . . . 18 (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ↦ (𝑎𝑏)):(((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) × ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))⟶𝒫 ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))
207 frn 6091 . . . . . . . . . . . . . . . . . 18 ((𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ↦ (𝑎𝑏)):(((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) × ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))⟶𝒫 ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) → ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ↦ (𝑎𝑏)) ⊆ 𝒫 ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))
208206, 207ax-mp 5 . . . . . . . . . . . . . . . . 17 ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ↦ (𝑎𝑏)) ⊆ 𝒫 ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))
209198, 208ssexi 4836 . . . . . . . . . . . . . . . 16 ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ↦ (𝑎𝑏)) ∈ V
210 nfcv 2793 . . . . . . . . . . . . . . . . 17 𝑣(𝑚𝑛)
211 nfcv 2793 . . . . . . . . . . . . . . . . 17 𝑣ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ↦ (𝑎𝑏))
212 mpt2eq12 6757 . . . . . . . . . . . . . . . . . . 19 ((𝑣 = ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ∧ 𝑣 = ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))) → (𝑎𝑣, 𝑏𝑣 ↦ (𝑎𝑏)) = (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ↦ (𝑎𝑏)))
213212anidms 678 . . . . . . . . . . . . . . . . . 18 (𝑣 = ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) → (𝑎𝑣, 𝑏𝑣 ↦ (𝑎𝑏)) = (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ↦ (𝑎𝑏)))
214213rneqd 5385 . . . . . . . . . . . . . . . . 17 (𝑣 = ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) → ran (𝑎𝑣, 𝑏𝑣 ↦ (𝑎𝑏)) = ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ↦ (𝑎𝑏)))
21583, 210, 211, 98, 214frsucmpt 7578 . . . . . . . . . . . . . . . 16 (((𝑚𝑛) ∈ ω ∧ ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ↦ (𝑎𝑏)) ∈ V) → ((rec(𝑅, 𝐴) ↾ ω)‘suc (𝑚𝑛)) = ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ↦ (𝑎𝑏)))
216173, 209, 215sylancl 695 . . . . . . . . . . . . . . 15 (((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) ∧ (𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ∧ 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))) → ((rec(𝑅, 𝐴) ↾ ω)‘suc (𝑚𝑛)) = ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ↦ (𝑎𝑏)))
217195, 216eleqtrrd 2733 . . . . . . . . . . . . . 14 (((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) ∧ (𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ∧ 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))) → (𝑐𝑑) ∈ ((rec(𝑅, 𝐴) ↾ ω)‘suc (𝑚𝑛)))
218177, 217sseldd 3637 . . . . . . . . . . . . 13 (((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) ∧ (𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ∧ 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))) → (𝑐𝑑) ∈ 𝑥 ∈ ω ((rec(𝑅, 𝐴) ↾ ω)‘𝑥))
219 fniunfv 6545 . . . . . . . . . . . . . 14 ((rec(𝑅, 𝐴) ↾ ω) Fn ω → 𝑥 ∈ ω ((rec(𝑅, 𝐴) ↾ ω)‘𝑥) = ran (rec(𝑅, 𝐴) ↾ ω))
2203, 219ax-mp 5 . . . . . . . . . . . . 13 𝑥 ∈ ω ((rec(𝑅, 𝐴) ↾ ω)‘𝑥) = ran (rec(𝑅, 𝐴) ↾ ω)
221218, 220syl6eleq 2740 . . . . . . . . . . . 12 (((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) ∧ (𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ∧ 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))) → (𝑐𝑑) ∈ ran (rec(𝑅, 𝐴) ↾ ω))
222221ex 449 . . . . . . . . . . 11 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) → ((𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ∧ 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))) → (𝑐𝑑) ∈ ran (rec(𝑅, 𝐴) ↾ ω)))
223162, 172, 222syl2and 499 . . . . . . . . . 10 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) → ((𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑚) ∧ 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)) → (𝑐𝑑) ∈ ran (rec(𝑅, 𝐴) ↾ ω)))
224223rexlimdvva 3067 . . . . . . . . 9 (𝐴𝑉 → (∃𝑚 ∈ ω ∃𝑛 ∈ ω (𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑚) ∧ 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)) → (𝑐𝑑) ∈ ran (rec(𝑅, 𝐴) ↾ ω)))
225224imp 444 . . . . . . . 8 ((𝐴𝑉 ∧ ∃𝑚 ∈ ω ∃𝑛 ∈ ω (𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑚) ∧ 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛))) → (𝑐𝑑) ∈ ran (rec(𝑅, 𝐴) ↾ ω))
22620, 225sylan2br 492 . . . . . . 7 ((𝐴𝑉 ∧ (𝑐 ran (rec(𝑅, 𝐴) ↾ ω) ∧ 𝑑 ran (rec(𝑅, 𝐴) ↾ ω))) → (𝑐𝑑) ∈ ran (rec(𝑅, 𝐴) ↾ ω))
227226ralrimivva 3000 . . . . . 6 (𝐴𝑉 → ∀𝑐 ran (rec(𝑅, 𝐴) ↾ ω)∀𝑑 ran (rec(𝑅, 𝐴) ↾ ω)(𝑐𝑑) ∈ ran (rec(𝑅, 𝐴) ↾ ω))
228136simpld 474 . . . . . . . . . . . 12 ((𝐴𝑉𝑥 ∈ ω) → ((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ⊆ (fi‘𝐴))
229 fvex 6239 . . . . . . . . . . . . 13 (fi‘𝐴) ∈ V
230229elpw2 4858 . . . . . . . . . . . 12 (((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ∈ 𝒫 (fi‘𝐴) ↔ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ⊆ (fi‘𝐴))
231228, 230sylibr 224 . . . . . . . . . . 11 ((𝐴𝑉𝑥 ∈ ω) → ((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ∈ 𝒫 (fi‘𝐴))
232231ralrimiva 2995 . . . . . . . . . 10 (𝐴𝑉 → ∀𝑥 ∈ ω ((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ∈ 𝒫 (fi‘𝐴))
233 fnfvrnss 6430 . . . . . . . . . 10 (((rec(𝑅, 𝐴) ↾ ω) Fn ω ∧ ∀𝑥 ∈ ω ((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ∈ 𝒫 (fi‘𝐴)) → ran (rec(𝑅, 𝐴) ↾ ω) ⊆ 𝒫 (fi‘𝐴))
2343, 232, 233sylancr 696 . . . . . . . . 9 (𝐴𝑉 → ran (rec(𝑅, 𝐴) ↾ ω) ⊆ 𝒫 (fi‘𝐴))
235 sspwuni 4643 . . . . . . . . 9 (ran (rec(𝑅, 𝐴) ↾ ω) ⊆ 𝒫 (fi‘𝐴) ↔ ran (rec(𝑅, 𝐴) ↾ ω) ⊆ (fi‘𝐴))
236234, 235sylib 208 . . . . . . . 8 (𝐴𝑉 ran (rec(𝑅, 𝐴) ↾ ω) ⊆ (fi‘𝐴))
237 ssexg 4837 . . . . . . . 8 (( ran (rec(𝑅, 𝐴) ↾ ω) ⊆ (fi‘𝐴) ∧ (fi‘𝐴) ∈ V) → ran (rec(𝑅, 𝐴) ↾ ω) ∈ V)
238236, 229, 237sylancl 695 . . . . . . 7 (𝐴𝑉 ran (rec(𝑅, 𝐴) ↾ ω) ∈ V)
239 sseq2 3660 . . . . . . . . 9 (𝑥 = ran (rec(𝑅, 𝐴) ↾ ω) → (𝐴𝑥𝐴 ran (rec(𝑅, 𝐴) ↾ ω)))
240 eleq2 2719 . . . . . . . . . . 11 (𝑥 = ran (rec(𝑅, 𝐴) ↾ ω) → ((𝑐𝑑) ∈ 𝑥 ↔ (𝑐𝑑) ∈ ran (rec(𝑅, 𝐴) ↾ ω)))
241240raleqbi1dv 3176 . . . . . . . . . 10 (𝑥 = ran (rec(𝑅, 𝐴) ↾ ω) → (∀𝑑𝑥 (𝑐𝑑) ∈ 𝑥 ↔ ∀𝑑 ran (rec(𝑅, 𝐴) ↾ ω)(𝑐𝑑) ∈ ran (rec(𝑅, 𝐴) ↾ ω)))
242241raleqbi1dv 3176 . . . . . . . . 9 (𝑥 = ran (rec(𝑅, 𝐴) ↾ ω) → (∀𝑐𝑥𝑑𝑥 (𝑐𝑑) ∈ 𝑥 ↔ ∀𝑐 ran (rec(𝑅, 𝐴) ↾ ω)∀𝑑 ran (rec(𝑅, 𝐴) ↾ ω)(𝑐𝑑) ∈ ran (rec(𝑅, 𝐴) ↾ ω)))
243239, 242anbi12d 747 . . . . . . . 8 (𝑥 = ran (rec(𝑅, 𝐴) ↾ ω) → ((𝐴𝑥 ∧ ∀𝑐𝑥𝑑𝑥 (𝑐𝑑) ∈ 𝑥) ↔ (𝐴 ran (rec(𝑅, 𝐴) ↾ ω) ∧ ∀𝑐 ran (rec(𝑅, 𝐴) ↾ ω)∀𝑑 ran (rec(𝑅, 𝐴) ↾ ω)(𝑐𝑑) ∈ ran (rec(𝑅, 𝐴) ↾ ω))))
244243elabg 3383 . . . . . . 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 977 . . . . 5 (𝐴𝑉 ran (rec(𝑅, 𝐴) ↾ ω) ∈ {𝑥 ∣ (𝐴𝑥 ∧ ∀𝑐𝑥𝑑𝑥 (𝑐𝑑) ∈ 𝑥)})
247 intss1 4524 . . . . 5 ( ran (rec(𝑅, 𝐴) ↾ ω) ∈ {𝑥 ∣ (𝐴𝑥 ∧ ∀𝑐𝑥𝑑𝑥 (𝑐𝑑) ∈ 𝑥)} → {𝑥 ∣ (𝐴𝑥 ∧ ∀𝑐𝑥𝑑𝑥 (𝑐𝑑) ∈ 𝑥)} ⊆ ran (rec(𝑅, 𝐴) ↾ ω))
248246, 247syl 17 . . . 4 (𝐴𝑉 {𝑥 ∣ (𝐴𝑥 ∧ ∀𝑐𝑥𝑑𝑥 (𝑐𝑑) ∈ 𝑥)} ⊆ ran (rec(𝑅, 𝐴) ↾ ω))
2491, 248eqsstrd 3672 . . 3 (𝐴𝑉 → (fi‘𝐴) ⊆ ran (rec(𝑅, 𝐴) ↾ ω))
250249, 236eqssd 3653 . 2 (𝐴𝑉 → (fi‘𝐴) = ran (rec(𝑅, 𝐴) ↾ ω))
251 df-ima 5156 . . 3 (rec(𝑅, 𝐴) “ ω) = ran (rec(𝑅, 𝐴) ↾ ω)
252251unieqi 4477 . 2 (rec(𝑅, 𝐴) “ ω) = ran (rec(𝑅, 𝐴) ↾ ω)
253250, 252syl6eqr 2703 1 (𝐴𝑉 → (fi‘𝐴) = (rec(𝑅, 𝐴) “ ω))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wo 382  wa 383   = wceq 1523  wcel 2030  {cab 2637  wral 2941  wrex 2942  Vcvv 3231  cun 3605  cin 3606  wss 3607  c0 3948  𝒫 cpw 4191  {csn 4210   cuni 4468   cint 4507   ciun 4552  cmpt 4762   × cxp 5141  ran crn 5144  cres 5145  cima 5146  Ord word 5760  Oncon0 5761  suc csuc 5763   Fn wfn 5921  wf 5922  cfv 5926  cmpt2 6692  ωcom 7107  reccrdg 7550  ficfi 8357
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-reu 2948  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-oadd 7609  df-er 7787  df-en 7998  df-fin 8001  df-fi 8358
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator