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

Theorem dffi3 8887
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 8879 . . . 4 (𝐴𝑉 → (fi‘𝐴) = {𝑥 ∣ (𝐴𝑥 ∧ ∀𝑐𝑥𝑑𝑥 (𝑐𝑑) ∈ 𝑥)})
2 fr0g 8063 . . . . . . . 8 (𝐴𝑉 → ((rec(𝑅, 𝐴) ↾ ω)‘∅) = 𝐴)
3 frfnom 8062 . . . . . . . . 9 (rec(𝑅, 𝐴) ↾ ω) Fn ω
4 peano1 7593 . . . . . . . . 9 ∅ ∈ ω
5 fnfvelrn 6841 . . . . . . . . 9 (((rec(𝑅, 𝐴) ↾ ω) Fn ω ∧ ∅ ∈ ω) → ((rec(𝑅, 𝐴) ↾ ω)‘∅) ∈ ran (rec(𝑅, 𝐴) ↾ ω))
63, 4, 5mp2an 690 . . . . . . . 8 ((rec(𝑅, 𝐴) ↾ ω)‘∅) ∈ ran (rec(𝑅, 𝐴) ↾ ω)
72, 6eqeltrrdi 2920 . . . . . . 7 (𝐴𝑉𝐴 ∈ ran (rec(𝑅, 𝐴) ↾ ω))
8 elssuni 4859 . . . . . . 7 (𝐴 ∈ ran (rec(𝑅, 𝐴) ↾ ω) → 𝐴 ran (rec(𝑅, 𝐴) ↾ ω))
97, 8syl 17 . . . . . 6 (𝐴𝑉𝐴 ran (rec(𝑅, 𝐴) ↾ ω))
10 reeanv 3366 . . . . . . . . 9 (∃𝑚 ∈ ω ∃𝑛 ∈ ω (𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑚) ∧ 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)) ↔ (∃𝑚 ∈ ω 𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑚) ∧ ∃𝑛 ∈ ω 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)))
11 eliun 4914 . . . . . . . . . 10 (𝑐 𝑚 ∈ ω ((rec(𝑅, 𝐴) ↾ ω)‘𝑚) ↔ ∃𝑚 ∈ ω 𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑚))
12 eliun 4914 . . . . . . . . . 10 (𝑑 𝑛 ∈ ω ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↔ ∃𝑛 ∈ ω 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛))
1311, 12anbi12i 628 . . . . . . . . 9 ((𝑐 𝑚 ∈ ω ((rec(𝑅, 𝐴) ↾ ω)‘𝑚) ∧ 𝑑 𝑛 ∈ ω ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)) ↔ (∃𝑚 ∈ ω 𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑚) ∧ ∃𝑛 ∈ ω 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)))
14 fniunfv 6998 . . . . . . . . . . . 12 ((rec(𝑅, 𝐴) ↾ ω) Fn ω → 𝑚 ∈ ω ((rec(𝑅, 𝐴) ↾ ω)‘𝑚) = ran (rec(𝑅, 𝐴) ↾ ω))
1514eleq2d 2896 . . . . . . . . . . 11 ((rec(𝑅, 𝐴) ↾ ω) Fn ω → (𝑐 𝑚 ∈ ω ((rec(𝑅, 𝐴) ↾ ω)‘𝑚) ↔ 𝑐 ran (rec(𝑅, 𝐴) ↾ ω)))
16 fniunfv 6998 . . . . . . . . . . . 12 ((rec(𝑅, 𝐴) ↾ ω) Fn ω → 𝑛 ∈ ω ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) = ran (rec(𝑅, 𝐴) ↾ ω))
1716eleq2d 2896 . . . . . . . . . . 11 ((rec(𝑅, 𝐴) ↾ ω) Fn ω → (𝑑 𝑛 ∈ ω ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↔ 𝑑 ran (rec(𝑅, 𝐴) ↾ ω)))
1815, 17anbi12d 632 . . . . . . . . . 10 ((rec(𝑅, 𝐴) ↾ ω) Fn ω → ((𝑐 𝑚 ∈ ω ((rec(𝑅, 𝐴) ↾ ω)‘𝑚) ∧ 𝑑 𝑛 ∈ ω ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)) ↔ (𝑐 ran (rec(𝑅, 𝐴) ↾ ω) ∧ 𝑑 ran (rec(𝑅, 𝐴) ↾ ω))))
193, 18ax-mp 5 . . . . . . . . 9 ((𝑐 𝑚 ∈ ω ((rec(𝑅, 𝐴) ↾ ω)‘𝑚) ∧ 𝑑 𝑛 ∈ ω ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)) ↔ (𝑐 ran (rec(𝑅, 𝐴) ↾ ω) ∧ 𝑑 ran (rec(𝑅, 𝐴) ↾ ω)))
2010, 13, 193bitr2i 301 . . . . . . . 8 (∃𝑚 ∈ ω ∃𝑛 ∈ ω (𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑚) ∧ 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)) ↔ (𝑐 ran (rec(𝑅, 𝐴) ↾ ω) ∧ 𝑑 ran (rec(𝑅, 𝐴) ↾ ω)))
21 ordom 7581 . . . . . . . . . . . . . . . 16 Ord ω
22 ordunel 7534 . . . . . . . . . . . . . . . 16 ((Ord ω ∧ 𝑚 ∈ ω ∧ 𝑛 ∈ ω) → (𝑚𝑛) ∈ ω)
2321, 22mp3an1 1441 . . . . . . . . . . . . . . 15 ((𝑚 ∈ ω ∧ 𝑛 ∈ ω) → (𝑚𝑛) ∈ ω)
2423adantl 484 . . . . . . . . . . . . . 14 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) → (𝑚𝑛) ∈ ω)
25 simprl 769 . . . . . . . . . . . . . 14 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) → 𝑚 ∈ ω)
2624, 25jca 514 . . . . . . . . . . . . 13 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) → ((𝑚𝑛) ∈ ω ∧ 𝑚 ∈ ω))
27 nnon 7578 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ ω → 𝑦 ∈ On)
28 nnon 7578 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ω → 𝑥 ∈ On)
2928ad2antlr 725 . . . . . . . . . . . . . . . . . 18 (((𝐴𝑉𝑥 ∈ ω) ∧ 𝑦 ∈ ω) → 𝑥 ∈ On)
30 onsseleq 6225 . . . . . . . . . . . . . . . . . 18 ((𝑦 ∈ On ∧ 𝑥 ∈ On) → (𝑦𝑥 ↔ (𝑦𝑥𝑦 = 𝑥)))
3127, 29, 30syl2an2 684 . . . . . . . . . . . . . . . . 17 (((𝐴𝑉𝑥 ∈ ω) ∧ 𝑦 ∈ ω) → (𝑦𝑥 ↔ (𝑦𝑥𝑦 = 𝑥)))
32 rzal 4451 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 = ∅ → ∀𝑦𝑥 ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥))
3332biantrud 534 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = ∅ → (((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ⊆ (fi‘𝐴) ↔ (((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ⊆ (fi‘𝐴) ∧ ∀𝑦𝑥 ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥))))
34 fveq2 6663 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 = ∅ → ((rec(𝑅, 𝐴) ↾ ω)‘𝑥) = ((rec(𝑅, 𝐴) ↾ ω)‘∅))
3534sseq1d 3996 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = ∅ → (((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ⊆ (fi‘𝐴) ↔ ((rec(𝑅, 𝐴) ↾ ω)‘∅) ⊆ (fi‘𝐴)))
3633, 35bitr3d 283 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = ∅ → ((((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ⊆ (fi‘𝐴) ∧ ∀𝑦𝑥 ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥)) ↔ ((rec(𝑅, 𝐴) ↾ ω)‘∅) ⊆ (fi‘𝐴)))
37 fveq2 6663 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 = 𝑛 → ((rec(𝑅, 𝐴) ↾ ω)‘𝑥) = ((rec(𝑅, 𝐴) ↾ ω)‘𝑛))
3837sseq1d 3996 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = 𝑛 → (((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ⊆ (fi‘𝐴) ↔ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ (fi‘𝐴)))
3937sseq2d 3997 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 = 𝑛 → (((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ↔ ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)))
4039raleqbi1dv 3402 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = 𝑛 → (∀𝑦𝑥 ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ↔ ∀𝑦𝑛 ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)))
4138, 40anbi12d 632 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = 𝑛 → ((((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ⊆ (fi‘𝐴) ∧ ∀𝑦𝑥 ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥)) ↔ (((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ (fi‘𝐴) ∧ ∀𝑦𝑛 ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛))))
42 fveq2 6663 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 = suc 𝑛 → ((rec(𝑅, 𝐴) ↾ ω)‘𝑥) = ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛))
4342sseq1d 3996 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = suc 𝑛 → (((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ⊆ (fi‘𝐴) ↔ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛) ⊆ (fi‘𝐴)))
4442sseq2d 3997 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 = suc 𝑛 → (((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ↔ ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛)))
4544raleqbi1dv 3402 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = suc 𝑛 → (∀𝑦𝑥 ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ↔ ∀𝑦 ∈ suc 𝑛((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛)))
4643, 45anbi12d 632 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = suc 𝑛 → ((((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ⊆ (fi‘𝐴) ∧ ∀𝑦𝑥 ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥)) ↔ (((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛) ⊆ (fi‘𝐴) ∧ ∀𝑦 ∈ suc 𝑛((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛))))
47 ssfii 8875 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐴𝑉𝐴 ⊆ (fi‘𝐴))
482, 47eqsstrd 4003 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐴𝑉 → ((rec(𝑅, 𝐴) ↾ ω)‘∅) ⊆ (fi‘𝐴))
49 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑥 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) → 𝑥 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛))
50 eqidd 2820 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑥 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) → 𝑥 = 𝑥)
51 ineq1 4179 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑎 = 𝑥 → (𝑎𝑏) = (𝑥𝑏))
5251eqeq2d 2830 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑎 = 𝑥 → (𝑥 = (𝑎𝑏) ↔ 𝑥 = (𝑥𝑏)))
53 ineq2 4181 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑏 = 𝑥 → (𝑥𝑏) = (𝑥𝑥))
54 inidm 4193 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑥𝑥) = 𝑥
5553, 54syl6eq 2870 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑏 = 𝑥 → (𝑥𝑏) = 𝑥)
5655eqeq2d 2830 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑏 = 𝑥 → (𝑥 = (𝑥𝑏) ↔ 𝑥 = 𝑥))
5752, 56rspc2ev 3633 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑥 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ∧ 𝑥 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ∧ 𝑥 = 𝑥) → ∃𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)∃𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)𝑥 = (𝑎𝑏))
5849, 49, 50, 57syl3anc 1365 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑥 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) → ∃𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)∃𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)𝑥 = (𝑎𝑏))
59 eqid 2819 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎𝑏)) = (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎𝑏))
6059rnmpo 7276 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎𝑏)) = {𝑥 ∣ ∃𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)∃𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)𝑥 = (𝑎𝑏)}
6160abeq2i 2946 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑥 ∈ ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎𝑏)) ↔ ∃𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)∃𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)𝑥 = (𝑎𝑏))
6258, 61sylibr 236 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑥 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) → 𝑥 ∈ ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎𝑏)))
6362ssriv 3969 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎𝑏))
64 simpl 485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑛 ∈ ω ∧ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ (fi‘𝐴)) → 𝑛 ∈ ω)
65 fvex 6676 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ∈ V
6665uniex 7459 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ∈ V
6766pwex 5272 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 𝒫 ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ∈ V
68 inss1 4203 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑎𝑏) ⊆ 𝑎
69 elssuni 4859 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) → 𝑎 ((rec(𝑅, 𝐴) ↾ ω)‘𝑛))
7069adantr 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ∧ 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)) → 𝑎 ((rec(𝑅, 𝐴) ↾ ω)‘𝑛))
7168, 70sstrid 3976 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ∧ 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)) → (𝑎𝑏) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛))
72 vex 3496 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 𝑎 ∈ V
7372inex1 5212 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑎𝑏) ∈ V
7473elpw 4544 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑎𝑏) ∈ 𝒫 ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↔ (𝑎𝑏) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛))
7571, 74sylibr 236 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ∧ 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)) → (𝑎𝑏) ∈ 𝒫 ((rec(𝑅, 𝐴) ↾ ω)‘𝑛))
7675rgen2 3201 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)∀𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)(𝑎𝑏) ∈ 𝒫 ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)
7759fmpo 7758 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (∀𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)∀𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)(𝑎𝑏) ∈ 𝒫 ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↔ (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎𝑏)):(((rec(𝑅, 𝐴) ↾ ω)‘𝑛) × ((rec(𝑅, 𝐴) ↾ ω)‘𝑛))⟶𝒫 ((rec(𝑅, 𝐴) ↾ ω)‘𝑛))
7876, 77mpbi 232 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎𝑏)):(((rec(𝑅, 𝐴) ↾ ω)‘𝑛) × ((rec(𝑅, 𝐴) ↾ ω)‘𝑛))⟶𝒫 ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)
79 frn 6513 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎𝑏)):(((rec(𝑅, 𝐴) ↾ ω)‘𝑛) × ((rec(𝑅, 𝐴) ↾ ω)‘𝑛))⟶𝒫 ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) → ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎𝑏)) ⊆ 𝒫 ((rec(𝑅, 𝐴) ↾ ω)‘𝑛))
8078, 79ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎𝑏)) ⊆ 𝒫 ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)
8167, 80ssexi 5217 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎𝑏)) ∈ V
82 nfcv 2975 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 𝑣𝐴
83 nfcv 2975 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 𝑣𝑛
84 nfcv 2975 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 𝑣ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎𝑏))
85 dffi3.1 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 𝑅 = (𝑢 ∈ V ↦ ran (𝑦𝑢, 𝑧𝑢 ↦ (𝑦𝑧)))
86 mpoeq12 7219 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝑢 = 𝑣𝑢 = 𝑣) → (𝑦𝑢, 𝑧𝑢 ↦ (𝑦𝑧)) = (𝑦𝑣, 𝑧𝑣 ↦ (𝑦𝑧)))
8786anidms 569 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝑢 = 𝑣 → (𝑦𝑢, 𝑧𝑢 ↦ (𝑦𝑧)) = (𝑦𝑣, 𝑧𝑣 ↦ (𝑦𝑧)))
88 ineq1 4179 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝑦 = 𝑎 → (𝑦𝑧) = (𝑎𝑧))
89 ineq2 4181 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝑧 = 𝑏 → (𝑎𝑧) = (𝑎𝑏))
9088, 89cbvmpov 7241 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝑦𝑣, 𝑧𝑣 ↦ (𝑦𝑧)) = (𝑎𝑣, 𝑏𝑣 ↦ (𝑎𝑏))
9187, 90syl6eq 2870 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑢 = 𝑣 → (𝑦𝑢, 𝑧𝑢 ↦ (𝑦𝑧)) = (𝑎𝑣, 𝑏𝑣 ↦ (𝑎𝑏)))
9291rneqd 5801 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑢 = 𝑣 → ran (𝑦𝑢, 𝑧𝑢 ↦ (𝑦𝑧)) = ran (𝑎𝑣, 𝑏𝑣 ↦ (𝑎𝑏)))
9392cbvmptv 5160 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑢 ∈ V ↦ ran (𝑦𝑢, 𝑧𝑢 ↦ (𝑦𝑧))) = (𝑣 ∈ V ↦ ran (𝑎𝑣, 𝑏𝑣 ↦ (𝑎𝑏)))
9485, 93eqtri 2842 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 𝑅 = (𝑣 ∈ V ↦ ran (𝑎𝑣, 𝑏𝑣 ↦ (𝑎𝑏)))
95 rdgeq1 8039 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑅 = (𝑣 ∈ V ↦ ran (𝑎𝑣, 𝑏𝑣 ↦ (𝑎𝑏))) → rec(𝑅, 𝐴) = rec((𝑣 ∈ V ↦ ran (𝑎𝑣, 𝑏𝑣 ↦ (𝑎𝑏))), 𝐴))
9694, 95ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 rec(𝑅, 𝐴) = rec((𝑣 ∈ V ↦ ran (𝑎𝑣, 𝑏𝑣 ↦ (𝑎𝑏))), 𝐴)
9796reseq1i 5842 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (rec(𝑅, 𝐴) ↾ ω) = (rec((𝑣 ∈ V ↦ ran (𝑎𝑣, 𝑏𝑣 ↦ (𝑎𝑏))), 𝐴) ↾ ω)
98 mpoeq12 7219 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑣 = ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ∧ 𝑣 = ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)) → (𝑎𝑣, 𝑏𝑣 ↦ (𝑎𝑏)) = (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎𝑏)))
9998anidms 569 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑣 = ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) → (𝑎𝑣, 𝑏𝑣 ↦ (𝑎𝑏)) = (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎𝑏)))
10099rneqd 5801 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑣 = ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) → ran (𝑎𝑣, 𝑏𝑣 ↦ (𝑎𝑏)) = ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎𝑏)))
10182, 83, 84, 97, 100frsucmpt 8065 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑛 ∈ ω ∧ ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎𝑏)) ∈ V) → ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛) = ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎𝑏)))
10264, 81, 101sylancl 588 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑛 ∈ ω ∧ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ (fi‘𝐴)) → ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛) = ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎𝑏)))
10363, 102sseqtrrid 4018 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑛 ∈ ω ∧ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ (fi‘𝐴)) → ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛))
104 sstr2 3972 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) → (((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛) → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛)))
105103, 104syl5com 31 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑛 ∈ ω ∧ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ (fi‘𝐴)) → (((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛)))
106105ralimdv 3176 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑛 ∈ ω ∧ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ (fi‘𝐴)) → (∀𝑦𝑛 ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) → ∀𝑦𝑛 ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛)))
107 vex 3496 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 𝑛 ∈ V
108 fveq2 6663 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑦 = 𝑛 → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) = ((rec(𝑅, 𝐴) ↾ ω)‘𝑛))
109108sseq1d 3996 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑦 = 𝑛 → (((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛) ↔ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛)))
110107, 109ralsn 4611 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (∀𝑦 ∈ {𝑛} ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛) ↔ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛))
111103, 110sylibr 236 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑛 ∈ ω ∧ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ (fi‘𝐴)) → ∀𝑦 ∈ {𝑛} ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛))
112106, 111jctird 529 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑛 ∈ ω ∧ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ (fi‘𝐴)) → (∀𝑦𝑛 ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) → (∀𝑦𝑛 ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛) ∧ ∀𝑦 ∈ {𝑛} ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛))))
113 df-suc 6190 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 suc 𝑛 = (𝑛 ∪ {𝑛})
114113raleqi 3412 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (∀𝑦 ∈ suc 𝑛((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛) ↔ ∀𝑦 ∈ (𝑛 ∪ {𝑛})((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛))
115 ralunb 4165 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (∀𝑦 ∈ (𝑛 ∪ {𝑛})((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛) ↔ (∀𝑦𝑛 ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛) ∧ ∀𝑦 ∈ {𝑛} ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛)))
116114, 115bitri 277 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (∀𝑦 ∈ suc 𝑛((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛) ↔ (∀𝑦𝑛 ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛) ∧ ∀𝑦 ∈ {𝑛} ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛)))
117112, 116syl6ibr 254 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑛 ∈ ω ∧ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ (fi‘𝐴)) → (∀𝑦𝑛 ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) → ∀𝑦 ∈ suc 𝑛((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛)))
118 fiin 8878 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑎 ∈ (fi‘𝐴) ∧ 𝑏 ∈ (fi‘𝐴)) → (𝑎𝑏) ∈ (fi‘𝐴))
119118rgen2 3201 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 𝑎 ∈ (fi‘𝐴)∀𝑏 ∈ (fi‘𝐴)(𝑎𝑏) ∈ (fi‘𝐴)
120 ss2ralv 4033 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ (fi‘𝐴) → (∀𝑎 ∈ (fi‘𝐴)∀𝑏 ∈ (fi‘𝐴)(𝑎𝑏) ∈ (fi‘𝐴) → ∀𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)∀𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)(𝑎𝑏) ∈ (fi‘𝐴)))
121119, 120mpi 20 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ (fi‘𝐴) → ∀𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)∀𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)(𝑎𝑏) ∈ (fi‘𝐴))
12259fmpo 7758 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (∀𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)∀𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)(𝑎𝑏) ∈ (fi‘𝐴) ↔ (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎𝑏)):(((rec(𝑅, 𝐴) ↾ ω)‘𝑛) × ((rec(𝑅, 𝐴) ↾ ω)‘𝑛))⟶(fi‘𝐴))
123121, 122sylib 220 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ (fi‘𝐴) → (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎𝑏)):(((rec(𝑅, 𝐴) ↾ ω)‘𝑛) × ((rec(𝑅, 𝐴) ↾ ω)‘𝑛))⟶(fi‘𝐴))
124123frnd 6514 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ (fi‘𝐴) → ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎𝑏)) ⊆ (fi‘𝐴))
125124adantl 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑛 ∈ ω ∧ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ (fi‘𝐴)) → ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎𝑏)) ⊆ (fi‘𝐴))
126102, 125eqsstrd 4003 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑛 ∈ ω ∧ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ (fi‘𝐴)) → ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛) ⊆ (fi‘𝐴))
127117, 126jctild 528 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑛 ∈ ω ∧ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ (fi‘𝐴)) → (∀𝑦𝑛 ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) → (((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛) ⊆ (fi‘𝐴) ∧ ∀𝑦 ∈ suc 𝑛((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛))))
128127expimpd 456 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 ∈ ω → ((((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ (fi‘𝐴) ∧ ∀𝑦𝑛 ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)) → (((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛) ⊆ (fi‘𝐴) ∧ ∀𝑦 ∈ suc 𝑛((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛))))
129128a1d 25 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 ∈ ω → (𝐴𝑉 → ((((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ (fi‘𝐴) ∧ ∀𝑦𝑛 ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)) → (((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛) ⊆ (fi‘𝐴) ∧ ∀𝑦 ∈ suc 𝑛((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛)))))
13036, 41, 46, 48, 129finds2 7602 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ∈ ω → (𝐴𝑉 → (((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ⊆ (fi‘𝐴) ∧ ∀𝑦𝑥 ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥))))
131130impcom 410 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐴𝑉𝑥 ∈ ω) → (((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ⊆ (fi‘𝐴) ∧ ∀𝑦𝑥 ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥)))
132131simprd 498 . . . . . . . . . . . . . . . . . . . . 21 ((𝐴𝑉𝑥 ∈ ω) → ∀𝑦𝑥 ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥))
133132r19.21bi 3206 . . . . . . . . . . . . . . . . . . . 20 (((𝐴𝑉𝑥 ∈ ω) ∧ 𝑦𝑥) → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥))
134133ex 415 . . . . . . . . . . . . . . . . . . 19 ((𝐴𝑉𝑥 ∈ ω) → (𝑦𝑥 → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥)))
135134adantr 483 . . . . . . . . . . . . . . . . . 18 (((𝐴𝑉𝑥 ∈ ω) ∧ 𝑦 ∈ ω) → (𝑦𝑥 → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥)))
136 fveq2 6663 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = 𝑥 → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) = ((rec(𝑅, 𝐴) ↾ ω)‘𝑥))
137 eqimss 4021 . . . . . . . . . . . . . . . . . . . 20 (((rec(𝑅, 𝐴) ↾ ω)‘𝑦) = ((rec(𝑅, 𝐴) ↾ ω)‘𝑥) → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥))
138136, 137syl 17 . . . . . . . . . . . . . . . . . . 19 (𝑦 = 𝑥 → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥))
139138a1i 11 . . . . . . . . . . . . . . . . . 18 (((𝐴𝑉𝑥 ∈ ω) ∧ 𝑦 ∈ ω) → (𝑦 = 𝑥 → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥)))
140135, 139jaod 855 . . . . . . . . . . . . . . . . 17 (((𝐴𝑉𝑥 ∈ ω) ∧ 𝑦 ∈ ω) → ((𝑦𝑥𝑦 = 𝑥) → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥)))
14131, 140sylbid 242 . . . . . . . . . . . . . . . 16 (((𝐴𝑉𝑥 ∈ ω) ∧ 𝑦 ∈ ω) → (𝑦𝑥 → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥)))
142141ralrimiva 3180 . . . . . . . . . . . . . . 15 ((𝐴𝑉𝑥 ∈ ω) → ∀𝑦 ∈ ω (𝑦𝑥 → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥)))
143142ralrimiva 3180 . . . . . . . . . . . . . 14 (𝐴𝑉 → ∀𝑥 ∈ ω ∀𝑦 ∈ ω (𝑦𝑥 → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥)))
144143adantr 483 . . . . . . . . . . . . 13 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) → ∀𝑥 ∈ ω ∀𝑦 ∈ ω (𝑦𝑥 → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥)))
145 ssun1 4146 . . . . . . . . . . . . . 14 𝑚 ⊆ (𝑚𝑛)
146145a1i 11 . . . . . . . . . . . . 13 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) → 𝑚 ⊆ (𝑚𝑛))
147 sseq2 3991 . . . . . . . . . . . . . . 15 (𝑥 = (𝑚𝑛) → (𝑦𝑥𝑦 ⊆ (𝑚𝑛)))
148 fveq2 6663 . . . . . . . . . . . . . . . 16 (𝑥 = (𝑚𝑛) → ((rec(𝑅, 𝐴) ↾ ω)‘𝑥) = ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))
149148sseq2d 3997 . . . . . . . . . . . . . . 15 (𝑥 = (𝑚𝑛) → (((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ↔ ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))))
150147, 149imbi12d 347 . . . . . . . . . . . . . 14 (𝑥 = (𝑚𝑛) → ((𝑦𝑥 → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥)) ↔ (𝑦 ⊆ (𝑚𝑛) → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))))
151 sseq1 3990 . . . . . . . . . . . . . . 15 (𝑦 = 𝑚 → (𝑦 ⊆ (𝑚𝑛) ↔ 𝑚 ⊆ (𝑚𝑛)))
152 fveq2 6663 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑚 → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) = ((rec(𝑅, 𝐴) ↾ ω)‘𝑚))
153152sseq1d 3996 . . . . . . . . . . . . . . 15 (𝑦 = 𝑚 → (((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ↔ ((rec(𝑅, 𝐴) ↾ ω)‘𝑚) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))))
154151, 153imbi12d 347 . . . . . . . . . . . . . 14 (𝑦 = 𝑚 → ((𝑦 ⊆ (𝑚𝑛) → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))) ↔ (𝑚 ⊆ (𝑚𝑛) → ((rec(𝑅, 𝐴) ↾ ω)‘𝑚) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))))
155150, 154rspc2v 3631 . . . . . . . . . . . . 13 (((𝑚𝑛) ∈ ω ∧ 𝑚 ∈ ω) → (∀𝑥 ∈ ω ∀𝑦 ∈ ω (𝑦𝑥 → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥)) → (𝑚 ⊆ (𝑚𝑛) → ((rec(𝑅, 𝐴) ↾ ω)‘𝑚) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))))
15626, 144, 146, 155syl3c 66 . . . . . . . . . . . 12 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) → ((rec(𝑅, 𝐴) ↾ ω)‘𝑚) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))
157156sseld 3964 . . . . . . . . . . 11 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) → (𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑚) → 𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))))
158 simprr 771 . . . . . . . . . . . . . 14 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) → 𝑛 ∈ ω)
15924, 158jca 514 . . . . . . . . . . . . 13 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) → ((𝑚𝑛) ∈ ω ∧ 𝑛 ∈ ω))
160 ssun2 4147 . . . . . . . . . . . . . 14 𝑛 ⊆ (𝑚𝑛)
161160a1i 11 . . . . . . . . . . . . 13 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) → 𝑛 ⊆ (𝑚𝑛))
162 sseq1 3990 . . . . . . . . . . . . . . 15 (𝑦 = 𝑛 → (𝑦 ⊆ (𝑚𝑛) ↔ 𝑛 ⊆ (𝑚𝑛)))
163108sseq1d 3996 . . . . . . . . . . . . . . 15 (𝑦 = 𝑛 → (((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ↔ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))))
164162, 163imbi12d 347 . . . . . . . . . . . . . 14 (𝑦 = 𝑛 → ((𝑦 ⊆ (𝑚𝑛) → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))) ↔ (𝑛 ⊆ (𝑚𝑛) → ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))))
165150, 164rspc2v 3631 . . . . . . . . . . . . 13 (((𝑚𝑛) ∈ ω ∧ 𝑛 ∈ ω) → (∀𝑥 ∈ ω ∀𝑦 ∈ ω (𝑦𝑥 → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥)) → (𝑛 ⊆ (𝑚𝑛) → ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))))
166159, 144, 161, 165syl3c 66 . . . . . . . . . . . 12 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) → ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))
167166sseld 3964 . . . . . . . . . . 11 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) → (𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) → 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))))
16823ad2antlr 725 . . . . . . . . . . . . . . 15 (((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) ∧ (𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ∧ 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))) → (𝑚𝑛) ∈ ω)
169 peano2 7594 . . . . . . . . . . . . . . 15 ((𝑚𝑛) ∈ ω → suc (𝑚𝑛) ∈ ω)
170 fveq2 6663 . . . . . . . . . . . . . . . 16 (𝑥 = suc (𝑚𝑛) → ((rec(𝑅, 𝐴) ↾ ω)‘𝑥) = ((rec(𝑅, 𝐴) ↾ ω)‘suc (𝑚𝑛)))
171170ssiun2s 4963 . . . . . . . . . . . . . . 15 (suc (𝑚𝑛) ∈ ω → ((rec(𝑅, 𝐴) ↾ ω)‘suc (𝑚𝑛)) ⊆ 𝑥 ∈ ω ((rec(𝑅, 𝐴) ↾ ω)‘𝑥))
172168, 169, 1713syl 18 . . . . . . . . . . . . . 14 (((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) ∧ (𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ∧ 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))) → ((rec(𝑅, 𝐴) ↾ ω)‘suc (𝑚𝑛)) ⊆ 𝑥 ∈ ω ((rec(𝑅, 𝐴) ↾ ω)‘𝑥))
173 simprl 769 . . . . . . . . . . . . . . . . . 18 (((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) ∧ (𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ∧ 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))) → 𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))
174 simprr 771 . . . . . . . . . . . . . . . . . 18 (((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) ∧ (𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ∧ 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))) → 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))
175 eqidd 2820 . . . . . . . . . . . . . . . . . 18 (((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) ∧ (𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ∧ 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))) → (𝑐𝑑) = (𝑐𝑑))
176 ineq1 4179 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = 𝑐 → (𝑎𝑏) = (𝑐𝑏))
177176eqeq2d 2830 . . . . . . . . . . . . . . . . . . 19 (𝑎 = 𝑐 → ((𝑐𝑑) = (𝑎𝑏) ↔ (𝑐𝑑) = (𝑐𝑏)))
178 ineq2 4181 . . . . . . . . . . . . . . . . . . . 20 (𝑏 = 𝑑 → (𝑐𝑏) = (𝑐𝑑))
179178eqeq2d 2830 . . . . . . . . . . . . . . . . . . 19 (𝑏 = 𝑑 → ((𝑐𝑑) = (𝑐𝑏) ↔ (𝑐𝑑) = (𝑐𝑑)))
180177, 179rspc2ev 3633 . . . . . . . . . . . . . . . . . 18 ((𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ∧ 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ∧ (𝑐𝑑) = (𝑐𝑑)) → ∃𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))∃𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))(𝑐𝑑) = (𝑎𝑏))
181173, 174, 175, 180syl3anc 1365 . . . . . . . . . . . . . . . . 17 (((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) ∧ (𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ∧ 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))) → ∃𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))∃𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))(𝑐𝑑) = (𝑎𝑏))
182 vex 3496 . . . . . . . . . . . . . . . . . . 19 𝑐 ∈ V
183182inex1 5212 . . . . . . . . . . . . . . . . . 18 (𝑐𝑑) ∈ V
184 eqeq1 2823 . . . . . . . . . . . . . . . . . . 19 (𝑥 = (𝑐𝑑) → (𝑥 = (𝑎𝑏) ↔ (𝑐𝑑) = (𝑎𝑏)))
1851842rexbidv 3298 . . . . . . . . . . . . . . . . . 18 (𝑥 = (𝑐𝑑) → (∃𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))∃𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))𝑥 = (𝑎𝑏) ↔ ∃𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))∃𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))(𝑐𝑑) = (𝑎𝑏)))
186183, 185elab 3665 . . . . . . . . . . . . . . . . 17 ((𝑐𝑑) ∈ {𝑥 ∣ ∃𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))∃𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))𝑥 = (𝑎𝑏)} ↔ ∃𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))∃𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))(𝑐𝑑) = (𝑎𝑏))
187181, 186sylibr 236 . . . . . . . . . . . . . . . 16 (((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) ∧ (𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ∧ 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))) → (𝑐𝑑) ∈ {𝑥 ∣ ∃𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))∃𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))𝑥 = (𝑎𝑏)})
188 eqid 2819 . . . . . . . . . . . . . . . . 17 (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ↦ (𝑎𝑏)) = (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ↦ (𝑎𝑏))
189188rnmpo 7276 . . . . . . . . . . . . . . . 16 ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ↦ (𝑎𝑏)) = {𝑥 ∣ ∃𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))∃𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))𝑥 = (𝑎𝑏)}
190187, 189eleqtrrdi 2922 . . . . . . . . . . . . . . 15 (((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) ∧ (𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ∧ 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))) → (𝑐𝑑) ∈ ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ↦ (𝑎𝑏)))
191 fvex 6676 . . . . . . . . . . . . . . . . . . 19 ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ∈ V
192191uniex 7459 . . . . . . . . . . . . . . . . . 18 ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ∈ V
193192pwex 5272 . . . . . . . . . . . . . . . . 17 𝒫 ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ∈ V
194 elssuni 4859 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) → 𝑎 ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))
19568, 194sstrid 3976 . . . . . . . . . . . . . . . . . . . . . 22 (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) → (𝑎𝑏) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))
19673elpw 4544 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑎𝑏) ∈ 𝒫 ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ↔ (𝑎𝑏) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))
197195, 196sylibr 236 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) → (𝑎𝑏) ∈ 𝒫 ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))
198197adantr 483 . . . . . . . . . . . . . . . . . . . 20 ((𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ∧ 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))) → (𝑎𝑏) ∈ 𝒫 ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))
199198rgen2 3201 . . . . . . . . . . . . . . . . . . 19 𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))∀𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))(𝑎𝑏) ∈ 𝒫 ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))
200188fmpo 7758 . . . . . . . . . . . . . . . . . . 19 (∀𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))∀𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))(𝑎𝑏) ∈ 𝒫 ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ↔ (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ↦ (𝑎𝑏)):(((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) × ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))⟶𝒫 ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))
201199, 200mpbi 232 . . . . . . . . . . . . . . . . . 18 (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ↦ (𝑎𝑏)):(((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) × ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))⟶𝒫 ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))
202 frn 6513 . . . . . . . . . . . . . . . . . 18 ((𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ↦ (𝑎𝑏)):(((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) × ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))⟶𝒫 ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) → ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ↦ (𝑎𝑏)) ⊆ 𝒫 ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))
203201, 202ax-mp 5 . . . . . . . . . . . . . . . . 17 ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ↦ (𝑎𝑏)) ⊆ 𝒫 ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))
204193, 203ssexi 5217 . . . . . . . . . . . . . . . 16 ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ↦ (𝑎𝑏)) ∈ V
205 nfcv 2975 . . . . . . . . . . . . . . . . 17 𝑣(𝑚𝑛)
206 nfcv 2975 . . . . . . . . . . . . . . . . 17 𝑣ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ↦ (𝑎𝑏))
207 mpoeq12 7219 . . . . . . . . . . . . . . . . . . 19 ((𝑣 = ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ∧ 𝑣 = ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))) → (𝑎𝑣, 𝑏𝑣 ↦ (𝑎𝑏)) = (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ↦ (𝑎𝑏)))
208207anidms 569 . . . . . . . . . . . . . . . . . 18 (𝑣 = ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) → (𝑎𝑣, 𝑏𝑣 ↦ (𝑎𝑏)) = (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ↦ (𝑎𝑏)))
209208rneqd 5801 . . . . . . . . . . . . . . . . 17 (𝑣 = ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) → ran (𝑎𝑣, 𝑏𝑣 ↦ (𝑎𝑏)) = ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ↦ (𝑎𝑏)))
21082, 205, 206, 97, 209frsucmpt 8065 . . . . . . . . . . . . . . . 16 (((𝑚𝑛) ∈ ω ∧ ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ↦ (𝑎𝑏)) ∈ V) → ((rec(𝑅, 𝐴) ↾ ω)‘suc (𝑚𝑛)) = ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ↦ (𝑎𝑏)))
211168, 204, 210sylancl 588 . . . . . . . . . . . . . . 15 (((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) ∧ (𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ∧ 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))) → ((rec(𝑅, 𝐴) ↾ ω)‘suc (𝑚𝑛)) = ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ↦ (𝑎𝑏)))
212190, 211eleqtrrd 2914 . . . . . . . . . . . . . 14 (((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) ∧ (𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ∧ 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))) → (𝑐𝑑) ∈ ((rec(𝑅, 𝐴) ↾ ω)‘suc (𝑚𝑛)))
213172, 212sseldd 3966 . . . . . . . . . . . . 13 (((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) ∧ (𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ∧ 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))) → (𝑐𝑑) ∈ 𝑥 ∈ ω ((rec(𝑅, 𝐴) ↾ ω)‘𝑥))
214 fniunfv 6998 . . . . . . . . . . . . . 14 ((rec(𝑅, 𝐴) ↾ ω) Fn ω → 𝑥 ∈ ω ((rec(𝑅, 𝐴) ↾ ω)‘𝑥) = ran (rec(𝑅, 𝐴) ↾ ω))
2153, 214ax-mp 5 . . . . . . . . . . . . 13 𝑥 ∈ ω ((rec(𝑅, 𝐴) ↾ ω)‘𝑥) = ran (rec(𝑅, 𝐴) ↾ ω)
216213, 215eleqtrdi 2921 . . . . . . . . . . . 12 (((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) ∧ (𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ∧ 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)))) → (𝑐𝑑) ∈ ran (rec(𝑅, 𝐴) ↾ ω))
217216ex 415 . . . . . . . . . . 11 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) → ((𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛)) ∧ 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚𝑛))) → (𝑐𝑑) ∈ ran (rec(𝑅, 𝐴) ↾ ω)))
218157, 167, 217syl2and 609 . . . . . . . . . 10 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) → ((𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑚) ∧ 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)) → (𝑐𝑑) ∈ ran (rec(𝑅, 𝐴) ↾ ω)))
219218rexlimdvva 3292 . . . . . . . . 9 (𝐴𝑉 → (∃𝑚 ∈ ω ∃𝑛 ∈ ω (𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑚) ∧ 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)) → (𝑐𝑑) ∈ ran (rec(𝑅, 𝐴) ↾ ω)))
220219imp 409 . . . . . . . 8 ((𝐴𝑉 ∧ ∃𝑚 ∈ ω ∃𝑛 ∈ ω (𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑚) ∧ 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛))) → (𝑐𝑑) ∈ ran (rec(𝑅, 𝐴) ↾ ω))
22120, 220sylan2br 596 . . . . . . 7 ((𝐴𝑉 ∧ (𝑐 ran (rec(𝑅, 𝐴) ↾ ω) ∧ 𝑑 ran (rec(𝑅, 𝐴) ↾ ω))) → (𝑐𝑑) ∈ ran (rec(𝑅, 𝐴) ↾ ω))
222221ralrimivva 3189 . . . . . 6 (𝐴𝑉 → ∀𝑐 ran (rec(𝑅, 𝐴) ↾ ω)∀𝑑 ran (rec(𝑅, 𝐴) ↾ ω)(𝑐𝑑) ∈ ran (rec(𝑅, 𝐴) ↾ ω))
223131simpld 497 . . . . . . . . . . . 12 ((𝐴𝑉𝑥 ∈ ω) → ((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ⊆ (fi‘𝐴))
224 fvex 6676 . . . . . . . . . . . . 13 (fi‘𝐴) ∈ V
225224elpw2 5239 . . . . . . . . . . . 12 (((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ∈ 𝒫 (fi‘𝐴) ↔ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ⊆ (fi‘𝐴))
226223, 225sylibr 236 . . . . . . . . . . 11 ((𝐴𝑉𝑥 ∈ ω) → ((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ∈ 𝒫 (fi‘𝐴))
227226ralrimiva 3180 . . . . . . . . . 10 (𝐴𝑉 → ∀𝑥 ∈ ω ((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ∈ 𝒫 (fi‘𝐴))
228 fnfvrnss 6877 . . . . . . . . . 10 (((rec(𝑅, 𝐴) ↾ ω) Fn ω ∧ ∀𝑥 ∈ ω ((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ∈ 𝒫 (fi‘𝐴)) → ran (rec(𝑅, 𝐴) ↾ ω) ⊆ 𝒫 (fi‘𝐴))
2293, 227, 228sylancr 589 . . . . . . . . 9 (𝐴𝑉 → ran (rec(𝑅, 𝐴) ↾ ω) ⊆ 𝒫 (fi‘𝐴))
230 sspwuni 5013 . . . . . . . . 9 (ran (rec(𝑅, 𝐴) ↾ ω) ⊆ 𝒫 (fi‘𝐴) ↔ ran (rec(𝑅, 𝐴) ↾ ω) ⊆ (fi‘𝐴))
231229, 230sylib 220 . . . . . . . 8 (𝐴𝑉 ran (rec(𝑅, 𝐴) ↾ ω) ⊆ (fi‘𝐴))
232 ssexg 5218 . . . . . . . 8 (( ran (rec(𝑅, 𝐴) ↾ ω) ⊆ (fi‘𝐴) ∧ (fi‘𝐴) ∈ V) → ran (rec(𝑅, 𝐴) ↾ ω) ∈ V)
233231, 224, 232sylancl 588 . . . . . . 7 (𝐴𝑉 ran (rec(𝑅, 𝐴) ↾ ω) ∈ V)
234 sseq2 3991 . . . . . . . . 9 (𝑥 = ran (rec(𝑅, 𝐴) ↾ ω) → (𝐴𝑥𝐴 ran (rec(𝑅, 𝐴) ↾ ω)))
235 eleq2 2899 . . . . . . . . . . 11 (𝑥 = ran (rec(𝑅, 𝐴) ↾ ω) → ((𝑐𝑑) ∈ 𝑥 ↔ (𝑐𝑑) ∈ ran (rec(𝑅, 𝐴) ↾ ω)))
236235raleqbi1dv 3402 . . . . . . . . . 10 (𝑥 = ran (rec(𝑅, 𝐴) ↾ ω) → (∀𝑑𝑥 (𝑐𝑑) ∈ 𝑥 ↔ ∀𝑑 ran (rec(𝑅, 𝐴) ↾ ω)(𝑐𝑑) ∈ ran (rec(𝑅, 𝐴) ↾ ω)))
237236raleqbi1dv 3402 . . . . . . . . 9 (𝑥 = ran (rec(𝑅, 𝐴) ↾ ω) → (∀𝑐𝑥𝑑𝑥 (𝑐𝑑) ∈ 𝑥 ↔ ∀𝑐 ran (rec(𝑅, 𝐴) ↾ ω)∀𝑑 ran (rec(𝑅, 𝐴) ↾ ω)(𝑐𝑑) ∈ ran (rec(𝑅, 𝐴) ↾ ω)))
238234, 237anbi12d 632 . . . . . . . 8 (𝑥 = ran (rec(𝑅, 𝐴) ↾ ω) → ((𝐴𝑥 ∧ ∀𝑐𝑥𝑑𝑥 (𝑐𝑑) ∈ 𝑥) ↔ (𝐴 ran (rec(𝑅, 𝐴) ↾ ω) ∧ ∀𝑐 ran (rec(𝑅, 𝐴) ↾ ω)∀𝑑 ran (rec(𝑅, 𝐴) ↾ ω)(𝑐𝑑) ∈ ran (rec(𝑅, 𝐴) ↾ ω))))
239238elabg 3664 . . . . . . 7 ( ran (rec(𝑅, 𝐴) ↾ ω) ∈ V → ( ran (rec(𝑅, 𝐴) ↾ ω) ∈ {𝑥 ∣ (𝐴𝑥 ∧ ∀𝑐𝑥𝑑𝑥 (𝑐𝑑) ∈ 𝑥)} ↔ (𝐴 ran (rec(𝑅, 𝐴) ↾ ω) ∧ ∀𝑐 ran (rec(𝑅, 𝐴) ↾ ω)∀𝑑 ran (rec(𝑅, 𝐴) ↾ ω)(𝑐𝑑) ∈ ran (rec(𝑅, 𝐴) ↾ ω))))
240233, 239syl 17 . . . . . 6 (𝐴𝑉 → ( ran (rec(𝑅, 𝐴) ↾ ω) ∈ {𝑥 ∣ (𝐴𝑥 ∧ ∀𝑐𝑥𝑑𝑥 (𝑐𝑑) ∈ 𝑥)} ↔ (𝐴 ran (rec(𝑅, 𝐴) ↾ ω) ∧ ∀𝑐 ran (rec(𝑅, 𝐴) ↾ ω)∀𝑑 ran (rec(𝑅, 𝐴) ↾ ω)(𝑐𝑑) ∈ ran (rec(𝑅, 𝐴) ↾ ω))))
2419, 222, 240mpbir2and 711 . . . . 5 (𝐴𝑉 ran (rec(𝑅, 𝐴) ↾ ω) ∈ {𝑥 ∣ (𝐴𝑥 ∧ ∀𝑐𝑥𝑑𝑥 (𝑐𝑑) ∈ 𝑥)})
242 intss1 4882 . . . . 5 ( ran (rec(𝑅, 𝐴) ↾ ω) ∈ {𝑥 ∣ (𝐴𝑥 ∧ ∀𝑐𝑥𝑑𝑥 (𝑐𝑑) ∈ 𝑥)} → {𝑥 ∣ (𝐴𝑥 ∧ ∀𝑐𝑥𝑑𝑥 (𝑐𝑑) ∈ 𝑥)} ⊆ ran (rec(𝑅, 𝐴) ↾ ω))
243241, 242syl 17 . . . 4 (𝐴𝑉 {𝑥 ∣ (𝐴𝑥 ∧ ∀𝑐𝑥𝑑𝑥 (𝑐𝑑) ∈ 𝑥)} ⊆ ran (rec(𝑅, 𝐴) ↾ ω))
2441, 243eqsstrd 4003 . . 3 (𝐴𝑉 → (fi‘𝐴) ⊆ ran (rec(𝑅, 𝐴) ↾ ω))
245244, 231eqssd 3982 . 2 (𝐴𝑉 → (fi‘𝐴) = ran (rec(𝑅, 𝐴) ↾ ω))
246 df-ima 5561 . . 3 (rec(𝑅, 𝐴) “ ω) = ran (rec(𝑅, 𝐴) ↾ ω)
247246unieqi 4839 . 2 (rec(𝑅, 𝐴) “ ω) = ran (rec(𝑅, 𝐴) ↾ ω)
248245, 247syl6eqr 2872 1 (𝐴𝑉 → (fi‘𝐴) = (rec(𝑅, 𝐴) “ ω))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 208  wa 398  wo 843   = wceq 1530  wcel 2107  {cab 2797  wral 3136  wrex 3137  Vcvv 3493  cun 3932  cin 3933  wss 3934  c0 4289  𝒫 cpw 4537  {csn 4559   cuni 4830   cint 4867   ciun 4910  cmpt 5137   × cxp 5546  ran crn 5549  cres 5550  cima 5551  Ord word 6183  Oncon0 6184  suc csuc 6186   Fn wfn 6343  wf 6344  cfv 6348  cmpo 7150  ωcom 7572  reccrdg 8037  ficfi 8866
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2791  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7453
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1082  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2616  df-eu 2648  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ne 3015  df-ral 3141  df-rex 3142  df-reu 3143  df-rab 3145  df-v 3495  df-sbc 3771  df-csb 3882  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-pss 3952  df-nul 4290  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-tp 4564  df-op 4566  df-uni 4831  df-int 4868  df-iun 4912  df-br 5058  df-opab 5120  df-mpt 5138  df-tr 5164  df-id 5453  df-eprel 5458  df-po 5467  df-so 5468  df-fr 5507  df-we 5509  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-pred 6141  df-ord 6187  df-on 6188  df-lim 6189  df-suc 6190  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-ov 7151  df-oprab 7152  df-mpo 7153  df-om 7573  df-1st 7681  df-2nd 7682  df-wrecs 7939  df-recs 8000  df-rdg 8038  df-1o 8094  df-oadd 8098  df-er 8281  df-en 8502  df-fin 8505  df-fi 8867
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator