Step | Hyp | Ref
| Expression |
1 | | dffi2 8212 |
. . . 4
⊢ (𝐴 ∈ 𝑉 → (fi‘𝐴) = ∩ {𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ ∀𝑐 ∈ 𝑥 ∀𝑑 ∈ 𝑥 (𝑐 ∩ 𝑑) ∈ 𝑥)}) |
2 | | fr0g 7418 |
. . . . . . . 8
⊢ (𝐴 ∈ 𝑉 → ((rec(𝑅, 𝐴) ↾ ω)‘∅) = 𝐴) |
3 | | frfnom 7417 |
. . . . . . . . 9
⊢
(rec(𝑅, 𝐴) ↾ ω) Fn
ω |
4 | | peano1 6977 |
. . . . . . . . 9
⊢ ∅
∈ ω |
5 | | fnfvelrn 6264 |
. . . . . . . . 9
⊢
(((rec(𝑅, 𝐴) ↾ ω) Fn ω
∧ ∅ ∈ ω) → ((rec(𝑅, 𝐴) ↾ ω)‘∅) ∈ ran
(rec(𝑅, 𝐴) ↾ ω)) |
6 | 3, 4, 5 | mp2an 704 |
. . . . . . . 8
⊢
((rec(𝑅, 𝐴) ↾
ω)‘∅) ∈ ran (rec(𝑅, 𝐴) ↾ ω) |
7 | 2, 6 | syl6eqelr 2697 |
. . . . . . 7
⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ ran (rec(𝑅, 𝐴) ↾ ω)) |
8 | | elssuni 4403 |
. . . . . . 7
⊢ (𝐴 ∈ ran (rec(𝑅, 𝐴) ↾ ω) → 𝐴 ⊆ ∪ ran
(rec(𝑅, 𝐴) ↾ ω)) |
9 | 7, 8 | syl 17 |
. . . . . 6
⊢ (𝐴 ∈ 𝑉 → 𝐴 ⊆ ∪ ran
(rec(𝑅, 𝐴) ↾ ω)) |
10 | | reeanv 3086 |
. . . . . . . . 9
⊢
(∃𝑚 ∈
ω ∃𝑛 ∈
ω (𝑐 ∈
((rec(𝑅, 𝐴) ↾ ω)‘𝑚) ∧ 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)) ↔ (∃𝑚 ∈ ω 𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑚) ∧ ∃𝑛 ∈ ω 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛))) |
11 | | eliun 4460 |
. . . . . . . . . 10
⊢ (𝑐 ∈ ∪ 𝑚 ∈ ω ((rec(𝑅, 𝐴) ↾ ω)‘𝑚) ↔ ∃𝑚 ∈ ω 𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑚)) |
12 | | eliun 4460 |
. . . . . . . . . 10
⊢ (𝑑 ∈ ∪ 𝑛 ∈ ω ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↔ ∃𝑛 ∈ ω 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)) |
13 | 11, 12 | anbi12i 729 |
. . . . . . . . 9
⊢ ((𝑐 ∈ ∪ 𝑚 ∈ ω ((rec(𝑅, 𝐴) ↾ ω)‘𝑚) ∧ 𝑑 ∈ ∪
𝑛 ∈ ω
((rec(𝑅, 𝐴) ↾ ω)‘𝑛)) ↔ (∃𝑚 ∈ ω 𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑚) ∧ ∃𝑛 ∈ ω 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛))) |
14 | | fniunfv 6409 |
. . . . . . . . . . . 12
⊢
((rec(𝑅, 𝐴) ↾ ω) Fn ω
→ ∪ 𝑚 ∈ ω ((rec(𝑅, 𝐴) ↾ ω)‘𝑚) = ∪ ran
(rec(𝑅, 𝐴) ↾ ω)) |
15 | 14 | eleq2d 2673 |
. . . . . . . . . . 11
⊢
((rec(𝑅, 𝐴) ↾ ω) Fn ω
→ (𝑐 ∈ ∪ 𝑚 ∈ ω ((rec(𝑅, 𝐴) ↾ ω)‘𝑚) ↔ 𝑐 ∈ ∪ ran
(rec(𝑅, 𝐴) ↾ ω))) |
16 | | fniunfv 6409 |
. . . . . . . . . . . 12
⊢
((rec(𝑅, 𝐴) ↾ ω) Fn ω
→ ∪ 𝑛 ∈ ω ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) = ∪ ran
(rec(𝑅, 𝐴) ↾ ω)) |
17 | 16 | eleq2d 2673 |
. . . . . . . . . . 11
⊢
((rec(𝑅, 𝐴) ↾ ω) Fn ω
→ (𝑑 ∈ ∪ 𝑛 ∈ ω ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↔ 𝑑 ∈ ∪ ran
(rec(𝑅, 𝐴) ↾ ω))) |
18 | 15, 17 | anbi12d 743 |
. . . . . . . . . 10
⊢
((rec(𝑅, 𝐴) ↾ ω) Fn ω
→ ((𝑐 ∈ ∪ 𝑚 ∈ ω ((rec(𝑅, 𝐴) ↾ ω)‘𝑚) ∧ 𝑑 ∈ ∪
𝑛 ∈ ω
((rec(𝑅, 𝐴) ↾ ω)‘𝑛)) ↔ (𝑐 ∈ ∪ ran
(rec(𝑅, 𝐴) ↾ ω) ∧ 𝑑 ∈ ∪ ran
(rec(𝑅, 𝐴) ↾ ω)))) |
19 | 3, 18 | ax-mp 5 |
. . . . . . . . 9
⊢ ((𝑐 ∈ ∪ 𝑚 ∈ ω ((rec(𝑅, 𝐴) ↾ ω)‘𝑚) ∧ 𝑑 ∈ ∪
𝑛 ∈ ω
((rec(𝑅, 𝐴) ↾ ω)‘𝑛)) ↔ (𝑐 ∈ ∪ ran
(rec(𝑅, 𝐴) ↾ ω) ∧ 𝑑 ∈ ∪ ran
(rec(𝑅, 𝐴) ↾ ω))) |
20 | 10, 13, 19 | 3bitr2i 287 |
. . . . . . . 8
⊢
(∃𝑚 ∈
ω ∃𝑛 ∈
ω (𝑐 ∈
((rec(𝑅, 𝐴) ↾ ω)‘𝑚) ∧ 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)) ↔ (𝑐 ∈ ∪ ran
(rec(𝑅, 𝐴) ↾ ω) ∧ 𝑑 ∈ ∪ ran
(rec(𝑅, 𝐴) ↾ ω))) |
21 | | ordom 6966 |
. . . . . . . . . . . . . . . 16
⊢ Ord
ω |
22 | | ordunel 6919 |
. . . . . . . . . . . . . . . 16
⊢ ((Ord
ω ∧ 𝑚 ∈
ω ∧ 𝑛 ∈
ω) → (𝑚 ∪
𝑛) ∈
ω) |
23 | 21, 22 | mp3an1 1403 |
. . . . . . . . . . . . . . 15
⊢ ((𝑚 ∈ ω ∧ 𝑛 ∈ ω) → (𝑚 ∪ 𝑛) ∈ ω) |
24 | 23 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) → (𝑚 ∪ 𝑛) ∈ ω) |
25 | | simprl 790 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) → 𝑚 ∈ ω) |
26 | 24, 25 | jca 553 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) → ((𝑚 ∪ 𝑛) ∈ ω ∧ 𝑚 ∈ ω)) |
27 | | nnon 6963 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ ω → 𝑦 ∈ On) |
28 | 27 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ ω) ∧ 𝑦 ∈ ω) → 𝑦 ∈ On) |
29 | | nnon 6963 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ ω → 𝑥 ∈ On) |
30 | 29 | ad2antlr 759 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ ω) ∧ 𝑦 ∈ ω) → 𝑥 ∈ On) |
31 | | onsseleq 5682 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∈ On ∧ 𝑥 ∈ On) → (𝑦 ⊆ 𝑥 ↔ (𝑦 ∈ 𝑥 ∨ 𝑦 = 𝑥))) |
32 | 28, 30, 31 | syl2anc 691 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ ω) ∧ 𝑦 ∈ ω) → (𝑦 ⊆ 𝑥 ↔ (𝑦 ∈ 𝑥 ∨ 𝑦 = 𝑥))) |
33 | | rzal 4025 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑥 = ∅ → ∀𝑦 ∈ 𝑥 ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥)) |
34 | 33 | biantrud 527 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑥 = ∅ → (((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ⊆ (fi‘𝐴) ↔ (((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ⊆ (fi‘𝐴) ∧ ∀𝑦 ∈ 𝑥 ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥)))) |
35 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑥 = ∅ → ((rec(𝑅, 𝐴) ↾ ω)‘𝑥) = ((rec(𝑅, 𝐴) ↾
ω)‘∅)) |
36 | 35 | sseq1d 3595 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑥 = ∅ → (((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ⊆ (fi‘𝐴) ↔ ((rec(𝑅, 𝐴) ↾ ω)‘∅) ⊆
(fi‘𝐴))) |
37 | 34, 36 | bitr3d 269 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 = ∅ → ((((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ⊆ (fi‘𝐴) ∧ ∀𝑦 ∈ 𝑥 ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥)) ↔ ((rec(𝑅, 𝐴) ↾ ω)‘∅) ⊆
(fi‘𝐴))) |
38 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑥 = 𝑛 → ((rec(𝑅, 𝐴) ↾ ω)‘𝑥) = ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)) |
39 | 38 | sseq1d 3595 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑥 = 𝑛 → (((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ⊆ (fi‘𝐴) ↔ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ (fi‘𝐴))) |
40 | 38 | sseq2d 3596 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑥 = 𝑛 → (((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ↔ ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛))) |
41 | 40 | raleqbi1dv 3123 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑥 = 𝑛 → (∀𝑦 ∈ 𝑥 ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ↔ ∀𝑦 ∈ 𝑛 ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛))) |
42 | 39, 41 | anbi12d 743 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 = 𝑛 → ((((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ⊆ (fi‘𝐴) ∧ ∀𝑦 ∈ 𝑥 ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥)) ↔ (((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ (fi‘𝐴) ∧ ∀𝑦 ∈ 𝑛 ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)))) |
43 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑥 = suc 𝑛 → ((rec(𝑅, 𝐴) ↾ ω)‘𝑥) = ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛)) |
44 | 43 | sseq1d 3595 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑥 = suc 𝑛 → (((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ⊆ (fi‘𝐴) ↔ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛) ⊆ (fi‘𝐴))) |
45 | 43 | sseq2d 3596 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑥 = suc 𝑛 → (((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ↔ ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛))) |
46 | 45 | raleqbi1dv 3123 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑥 = suc 𝑛 → (∀𝑦 ∈ 𝑥 ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ↔ ∀𝑦 ∈ suc 𝑛((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛))) |
47 | 44, 46 | anbi12d 743 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 = suc 𝑛 → ((((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ⊆ (fi‘𝐴) ∧ ∀𝑦 ∈ 𝑥 ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥)) ↔ (((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛) ⊆ (fi‘𝐴) ∧ ∀𝑦 ∈ suc 𝑛((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛)))) |
48 | | ssfii 8208 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝐴 ∈ 𝑉 → 𝐴 ⊆ (fi‘𝐴)) |
49 | 2, 48 | eqsstrd 3602 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝐴 ∈ 𝑉 → ((rec(𝑅, 𝐴) ↾ ω)‘∅) ⊆
(fi‘𝐴)) |
50 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑥 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) → 𝑥 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)) |
51 | | eqidd 2611 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑥 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) → 𝑥 = 𝑥) |
52 | | ineq1 3769 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝑎 = 𝑥 → (𝑎 ∩ 𝑏) = (𝑥 ∩ 𝑏)) |
53 | 52 | eqeq2d 2620 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑎 = 𝑥 → (𝑥 = (𝑎 ∩ 𝑏) ↔ 𝑥 = (𝑥 ∩ 𝑏))) |
54 | | ineq2 3770 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (𝑏 = 𝑥 → (𝑥 ∩ 𝑏) = (𝑥 ∩ 𝑥)) |
55 | | inidm 3784 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (𝑥 ∩ 𝑥) = 𝑥 |
56 | 54, 55 | syl6eq 2660 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝑏 = 𝑥 → (𝑥 ∩ 𝑏) = 𝑥) |
57 | 56 | eqeq2d 2620 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑏 = 𝑥 → (𝑥 = (𝑥 ∩ 𝑏) ↔ 𝑥 = 𝑥)) |
58 | 53, 57 | rspc2ev 3295 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝑥 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ∧ 𝑥 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ∧ 𝑥 = 𝑥) → ∃𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)∃𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)𝑥 = (𝑎 ∩ 𝑏)) |
59 | 50, 50, 51, 58 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑥 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) → ∃𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)∃𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)𝑥 = (𝑎 ∩ 𝑏)) |
60 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎 ∩ 𝑏)) = (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎 ∩ 𝑏)) |
61 | 60 | rnmpt2 6668 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ran
(𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎 ∩ 𝑏)) = {𝑥 ∣ ∃𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)∃𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)𝑥 = (𝑎 ∩ 𝑏)} |
62 | 61 | abeq2i 2722 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑥 ∈ ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎 ∩ 𝑏)) ↔ ∃𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)∃𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)𝑥 = (𝑎 ∩ 𝑏)) |
63 | 59, 62 | sylibr 223 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑥 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) → 𝑥 ∈ ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎 ∩ 𝑏))) |
64 | 63 | ssriv 3572 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎 ∩ 𝑏)) |
65 | | simpl 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑛 ∈ ω ∧
((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ (fi‘𝐴)) → 𝑛 ∈ ω) |
66 | | fvex 6113 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢
((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ∈ V |
67 | 66 | uniex 6851 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ∪ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ∈ V |
68 | 67 | pwex 4774 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ 𝒫
∪ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ∈ V |
69 | | inss1 3795 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (𝑎 ∩ 𝑏) ⊆ 𝑎 |
70 | | elssuni 4403 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) → 𝑎 ⊆ ∪
((rec(𝑅, 𝐴) ↾ ω)‘𝑛)) |
71 | 70 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ ((𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ∧ 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)) → 𝑎 ⊆ ∪
((rec(𝑅, 𝐴) ↾ ω)‘𝑛)) |
72 | 69, 71 | syl5ss 3579 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ∧ 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)) → (𝑎 ∩ 𝑏) ⊆ ∪
((rec(𝑅, 𝐴) ↾ ω)‘𝑛)) |
73 | | vex 3176 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ 𝑎 ∈ V |
74 | 73 | inex1 4727 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (𝑎 ∩ 𝑏) ∈ V |
75 | 74 | elpw 4114 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((𝑎 ∩ 𝑏) ∈ 𝒫 ∪ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↔ (𝑎 ∩ 𝑏) ⊆ ∪
((rec(𝑅, 𝐴) ↾ ω)‘𝑛)) |
76 | 72, 75 | sylibr 223 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ∧ 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)) → (𝑎 ∩ 𝑏) ∈ 𝒫 ∪ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)) |
77 | 76 | rgen2a 2960 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢
∀𝑎 ∈
((rec(𝑅, 𝐴) ↾ ω)‘𝑛)∀𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)(𝑎 ∩ 𝑏) ∈ 𝒫 ∪ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) |
78 | 60 | fmpt2 7126 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢
(∀𝑎 ∈
((rec(𝑅, 𝐴) ↾ ω)‘𝑛)∀𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)(𝑎 ∩ 𝑏) ∈ 𝒫 ∪ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↔ (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎 ∩ 𝑏)):(((rec(𝑅, 𝐴) ↾ ω)‘𝑛) × ((rec(𝑅, 𝐴) ↾ ω)‘𝑛))⟶𝒫 ∪ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)) |
79 | 77, 78 | mpbi 219 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎 ∩ 𝑏)):(((rec(𝑅, 𝐴) ↾ ω)‘𝑛) × ((rec(𝑅, 𝐴) ↾ ω)‘𝑛))⟶𝒫 ∪ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) |
80 | | frn 5966 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎 ∩ 𝑏)):(((rec(𝑅, 𝐴) ↾ ω)‘𝑛) × ((rec(𝑅, 𝐴) ↾ ω)‘𝑛))⟶𝒫 ∪ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) → ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎 ∩ 𝑏)) ⊆ 𝒫 ∪ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)) |
81 | 79, 80 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ran
(𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎 ∩ 𝑏)) ⊆ 𝒫 ∪ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) |
82 | 68, 81 | ssexi 4731 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ran
(𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎 ∩ 𝑏)) ∈ V |
83 | | nfcv 2751 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
Ⅎ𝑣𝐴 |
84 | | nfcv 2751 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
Ⅎ𝑣𝑛 |
85 | | nfcv 2751 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
Ⅎ𝑣ran
(𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎 ∩ 𝑏)) |
86 | | dffi3.1 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ 𝑅 = (𝑢 ∈ V ↦ ran (𝑦 ∈ 𝑢, 𝑧 ∈ 𝑢 ↦ (𝑦 ∩ 𝑧))) |
87 | | mpt2eq12 6613 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ ((𝑢 = 𝑣 ∧ 𝑢 = 𝑣) → (𝑦 ∈ 𝑢, 𝑧 ∈ 𝑢 ↦ (𝑦 ∩ 𝑧)) = (𝑦 ∈ 𝑣, 𝑧 ∈ 𝑣 ↦ (𝑦 ∩ 𝑧))) |
88 | 87 | anidms 675 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (𝑢 = 𝑣 → (𝑦 ∈ 𝑢, 𝑧 ∈ 𝑢 ↦ (𝑦 ∩ 𝑧)) = (𝑦 ∈ 𝑣, 𝑧 ∈ 𝑣 ↦ (𝑦 ∩ 𝑧))) |
89 | | ineq1 3769 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (𝑦 = 𝑎 → (𝑦 ∩ 𝑧) = (𝑎 ∩ 𝑧)) |
90 | | ineq2 3770 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (𝑧 = 𝑏 → (𝑎 ∩ 𝑧) = (𝑎 ∩ 𝑏)) |
91 | 89, 90 | cbvmpt2v 6633 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (𝑦 ∈ 𝑣, 𝑧 ∈ 𝑣 ↦ (𝑦 ∩ 𝑧)) = (𝑎 ∈ 𝑣, 𝑏 ∈ 𝑣 ↦ (𝑎 ∩ 𝑏)) |
92 | 88, 91 | syl6eq 2660 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (𝑢 = 𝑣 → (𝑦 ∈ 𝑢, 𝑧 ∈ 𝑢 ↦ (𝑦 ∩ 𝑧)) = (𝑎 ∈ 𝑣, 𝑏 ∈ 𝑣 ↦ (𝑎 ∩ 𝑏))) |
93 | 92 | rneqd 5274 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (𝑢 = 𝑣 → ran (𝑦 ∈ 𝑢, 𝑧 ∈ 𝑢 ↦ (𝑦 ∩ 𝑧)) = ran (𝑎 ∈ 𝑣, 𝑏 ∈ 𝑣 ↦ (𝑎 ∩ 𝑏))) |
94 | 93 | cbvmptv 4678 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝑢 ∈ V ↦ ran (𝑦 ∈ 𝑢, 𝑧 ∈ 𝑢 ↦ (𝑦 ∩ 𝑧))) = (𝑣 ∈ V ↦ ran (𝑎 ∈ 𝑣, 𝑏 ∈ 𝑣 ↦ (𝑎 ∩ 𝑏))) |
95 | 86, 94 | eqtri 2632 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ 𝑅 = (𝑣 ∈ V ↦ ran (𝑎 ∈ 𝑣, 𝑏 ∈ 𝑣 ↦ (𝑎 ∩ 𝑏))) |
96 | | rdgeq1 7394 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑅 = (𝑣 ∈ V ↦ ran (𝑎 ∈ 𝑣, 𝑏 ∈ 𝑣 ↦ (𝑎 ∩ 𝑏))) → rec(𝑅, 𝐴) = rec((𝑣 ∈ V ↦ ran (𝑎 ∈ 𝑣, 𝑏 ∈ 𝑣 ↦ (𝑎 ∩ 𝑏))), 𝐴)) |
97 | 95, 96 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ rec(𝑅, 𝐴) = rec((𝑣 ∈ V ↦ ran (𝑎 ∈ 𝑣, 𝑏 ∈ 𝑣 ↦ (𝑎 ∩ 𝑏))), 𝐴) |
98 | 97 | reseq1i 5313 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
(rec(𝑅, 𝐴) ↾ ω) = (rec((𝑣 ∈ V ↦ ran (𝑎 ∈ 𝑣, 𝑏 ∈ 𝑣 ↦ (𝑎 ∩ 𝑏))), 𝐴) ↾ ω) |
99 | | mpt2eq12 6613 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝑣 = ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ∧ 𝑣 = ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)) → (𝑎 ∈ 𝑣, 𝑏 ∈ 𝑣 ↦ (𝑎 ∩ 𝑏)) = (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎 ∩ 𝑏))) |
100 | 99 | anidms 675 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑣 = ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) → (𝑎 ∈ 𝑣, 𝑏 ∈ 𝑣 ↦ (𝑎 ∩ 𝑏)) = (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎 ∩ 𝑏))) |
101 | 100 | rneqd 5274 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑣 = ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) → ran (𝑎 ∈ 𝑣, 𝑏 ∈ 𝑣 ↦ (𝑎 ∩ 𝑏)) = ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎 ∩ 𝑏))) |
102 | 83, 84, 85, 98, 101 | frsucmpt 7420 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑛 ∈ ω ∧ ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎 ∩ 𝑏)) ∈ V) → ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛) = ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎 ∩ 𝑏))) |
103 | 65, 82, 102 | sylancl 693 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑛 ∈ ω ∧
((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ (fi‘𝐴)) → ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛) = ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎 ∩ 𝑏))) |
104 | 64, 103 | syl5sseqr 3617 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑛 ∈ ω ∧
((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ (fi‘𝐴)) → ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛)) |
105 | | sstr2 3575 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) → (((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛) → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛))) |
106 | 104, 105 | syl5com 31 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑛 ∈ ω ∧
((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ (fi‘𝐴)) → (((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛))) |
107 | 106 | ralimdv 2946 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑛 ∈ ω ∧
((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ (fi‘𝐴)) → (∀𝑦 ∈ 𝑛 ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) → ∀𝑦 ∈ 𝑛 ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛))) |
108 | | vex 3176 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ 𝑛 ∈ V |
109 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑦 = 𝑛 → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) = ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)) |
110 | 109 | sseq1d 3595 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑦 = 𝑛 → (((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛) ↔ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛))) |
111 | 108, 110 | ralsn 4169 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(∀𝑦 ∈
{𝑛} ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛) ↔ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛)) |
112 | 104, 111 | sylibr 223 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑛 ∈ ω ∧
((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ (fi‘𝐴)) → ∀𝑦 ∈ {𝑛} ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛)) |
113 | 107, 112 | jctird 565 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑛 ∈ ω ∧
((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ (fi‘𝐴)) → (∀𝑦 ∈ 𝑛 ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) → (∀𝑦 ∈ 𝑛 ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛) ∧ ∀𝑦 ∈ {𝑛} ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛)))) |
114 | | df-suc 5646 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ suc 𝑛 = (𝑛 ∪ {𝑛}) |
115 | 114 | raleqi 3119 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(∀𝑦 ∈
suc 𝑛((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛) ↔ ∀𝑦 ∈ (𝑛 ∪ {𝑛})((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛)) |
116 | | ralunb 3756 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(∀𝑦 ∈
(𝑛 ∪ {𝑛})((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛) ↔ (∀𝑦 ∈ 𝑛 ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛) ∧ ∀𝑦 ∈ {𝑛} ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛))) |
117 | 115, 116 | bitri 263 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(∀𝑦 ∈
suc 𝑛((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛) ↔ (∀𝑦 ∈ 𝑛 ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛) ∧ ∀𝑦 ∈ {𝑛} ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛))) |
118 | 113, 117 | syl6ibr 241 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑛 ∈ ω ∧
((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ (fi‘𝐴)) → (∀𝑦 ∈ 𝑛 ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) → ∀𝑦 ∈ suc 𝑛((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛))) |
119 | | fiin 8211 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑎 ∈ (fi‘𝐴) ∧ 𝑏 ∈ (fi‘𝐴)) → (𝑎 ∩ 𝑏) ∈ (fi‘𝐴)) |
120 | 119 | rgen2a 2960 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
∀𝑎 ∈
(fi‘𝐴)∀𝑏 ∈ (fi‘𝐴)(𝑎 ∩ 𝑏) ∈ (fi‘𝐴) |
121 | | ssralv 3629 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
(((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ (fi‘𝐴) → (∀𝑏 ∈ (fi‘𝐴)(𝑎 ∩ 𝑏) ∈ (fi‘𝐴) → ∀𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)(𝑎 ∩ 𝑏) ∈ (fi‘𝐴))) |
122 | 121 | ralimdv 2946 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
(((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ (fi‘𝐴) → (∀𝑎 ∈ (fi‘𝐴)∀𝑏 ∈ (fi‘𝐴)(𝑎 ∩ 𝑏) ∈ (fi‘𝐴) → ∀𝑎 ∈ (fi‘𝐴)∀𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)(𝑎 ∩ 𝑏) ∈ (fi‘𝐴))) |
123 | | ssralv 3629 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
(((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ (fi‘𝐴) → (∀𝑎 ∈ (fi‘𝐴)∀𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)(𝑎 ∩ 𝑏) ∈ (fi‘𝐴) → ∀𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)∀𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)(𝑎 ∩ 𝑏) ∈ (fi‘𝐴))) |
124 | 122, 123 | syld 46 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
(((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ (fi‘𝐴) → (∀𝑎 ∈ (fi‘𝐴)∀𝑏 ∈ (fi‘𝐴)(𝑎 ∩ 𝑏) ∈ (fi‘𝐴) → ∀𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)∀𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)(𝑎 ∩ 𝑏) ∈ (fi‘𝐴))) |
125 | 120, 124 | mpi 20 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ (fi‘𝐴) → ∀𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)∀𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)(𝑎 ∩ 𝑏) ∈ (fi‘𝐴)) |
126 | 60 | fmpt2 7126 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(∀𝑎 ∈
((rec(𝑅, 𝐴) ↾ ω)‘𝑛)∀𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)(𝑎 ∩ 𝑏) ∈ (fi‘𝐴) ↔ (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎 ∩ 𝑏)):(((rec(𝑅, 𝐴) ↾ ω)‘𝑛) × ((rec(𝑅, 𝐴) ↾ ω)‘𝑛))⟶(fi‘𝐴)) |
127 | 125, 126 | sylib 207 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ (fi‘𝐴) → (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎 ∩ 𝑏)):(((rec(𝑅, 𝐴) ↾ ω)‘𝑛) × ((rec(𝑅, 𝐴) ↾ ω)‘𝑛))⟶(fi‘𝐴)) |
128 | | frn 5966 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎 ∩ 𝑏)):(((rec(𝑅, 𝐴) ↾ ω)‘𝑛) × ((rec(𝑅, 𝐴) ↾ ω)‘𝑛))⟶(fi‘𝐴) → ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎 ∩ 𝑏)) ⊆ (fi‘𝐴)) |
129 | 127, 128 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ (fi‘𝐴) → ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎 ∩ 𝑏)) ⊆ (fi‘𝐴)) |
130 | 129 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑛 ∈ ω ∧
((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ (fi‘𝐴)) → ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎 ∩ 𝑏)) ⊆ (fi‘𝐴)) |
131 | 103, 130 | eqsstrd 3602 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑛 ∈ ω ∧
((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ (fi‘𝐴)) → ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛) ⊆ (fi‘𝐴)) |
132 | 118, 131 | jctild 564 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑛 ∈ ω ∧
((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ (fi‘𝐴)) → (∀𝑦 ∈ 𝑛 ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) → (((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛) ⊆ (fi‘𝐴) ∧ ∀𝑦 ∈ suc 𝑛((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛)))) |
133 | 132 | expimpd 627 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑛 ∈ ω →
((((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ (fi‘𝐴) ∧ ∀𝑦 ∈ 𝑛 ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)) → (((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛) ⊆ (fi‘𝐴) ∧ ∀𝑦 ∈ suc 𝑛((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛)))) |
134 | 133 | a1d 25 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑛 ∈ ω → (𝐴 ∈ 𝑉 → ((((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ (fi‘𝐴) ∧ ∀𝑦 ∈ 𝑛 ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)) → (((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛) ⊆ (fi‘𝐴) ∧ ∀𝑦 ∈ suc 𝑛((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛))))) |
135 | 37, 42, 47, 49, 134 | finds2 6986 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 ∈ ω → (𝐴 ∈ 𝑉 → (((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ⊆ (fi‘𝐴) ∧ ∀𝑦 ∈ 𝑥 ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥)))) |
136 | 135 | impcom 445 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ ω) → (((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ⊆ (fi‘𝐴) ∧ ∀𝑦 ∈ 𝑥 ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥))) |
137 | 136 | simprd 478 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ ω) → ∀𝑦 ∈ 𝑥 ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥)) |
138 | 137 | r19.21bi 2916 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ ω) ∧ 𝑦 ∈ 𝑥) → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥)) |
139 | 138 | ex 449 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ ω) → (𝑦 ∈ 𝑥 → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥))) |
140 | 139 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ ω) ∧ 𝑦 ∈ ω) → (𝑦 ∈ 𝑥 → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥))) |
141 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 = 𝑥 → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) = ((rec(𝑅, 𝐴) ↾ ω)‘𝑥)) |
142 | | eqimss 3620 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((rec(𝑅, 𝐴) ↾ ω)‘𝑦) = ((rec(𝑅, 𝐴) ↾ ω)‘𝑥) → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥)) |
143 | 141, 142 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = 𝑥 → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥)) |
144 | 143 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ ω) ∧ 𝑦 ∈ ω) → (𝑦 = 𝑥 → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥))) |
145 | 140, 144 | jaod 394 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ ω) ∧ 𝑦 ∈ ω) → ((𝑦 ∈ 𝑥 ∨ 𝑦 = 𝑥) → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥))) |
146 | 32, 145 | sylbid 229 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ ω) ∧ 𝑦 ∈ ω) → (𝑦 ⊆ 𝑥 → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥))) |
147 | 146 | ralrimiva 2949 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ ω) → ∀𝑦 ∈ ω (𝑦 ⊆ 𝑥 → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥))) |
148 | 147 | ralrimiva 2949 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ 𝑉 → ∀𝑥 ∈ ω ∀𝑦 ∈ ω (𝑦 ⊆ 𝑥 → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥))) |
149 | 148 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) → ∀𝑥 ∈ ω ∀𝑦 ∈ ω (𝑦 ⊆ 𝑥 → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥))) |
150 | | ssun1 3738 |
. . . . . . . . . . . . . 14
⊢ 𝑚 ⊆ (𝑚 ∪ 𝑛) |
151 | 150 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) → 𝑚 ⊆ (𝑚 ∪ 𝑛)) |
152 | | sseq2 3590 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = (𝑚 ∪ 𝑛) → (𝑦 ⊆ 𝑥 ↔ 𝑦 ⊆ (𝑚 ∪ 𝑛))) |
153 | | fveq2 6103 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = (𝑚 ∪ 𝑛) → ((rec(𝑅, 𝐴) ↾ ω)‘𝑥) = ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛))) |
154 | 153 | sseq2d 3596 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = (𝑚 ∪ 𝑛) → (((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ↔ ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)))) |
155 | 152, 154 | imbi12d 333 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = (𝑚 ∪ 𝑛) → ((𝑦 ⊆ 𝑥 → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥)) ↔ (𝑦 ⊆ (𝑚 ∪ 𝑛) → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛))))) |
156 | | sseq1 3589 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 𝑚 → (𝑦 ⊆ (𝑚 ∪ 𝑛) ↔ 𝑚 ⊆ (𝑚 ∪ 𝑛))) |
157 | | fveq2 6103 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = 𝑚 → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) = ((rec(𝑅, 𝐴) ↾ ω)‘𝑚)) |
158 | 157 | sseq1d 3595 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 𝑚 → (((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)) ↔ ((rec(𝑅, 𝐴) ↾ ω)‘𝑚) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)))) |
159 | 156, 158 | imbi12d 333 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 𝑚 → ((𝑦 ⊆ (𝑚 ∪ 𝑛) → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛))) ↔ (𝑚 ⊆ (𝑚 ∪ 𝑛) → ((rec(𝑅, 𝐴) ↾ ω)‘𝑚) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛))))) |
160 | 155, 159 | rspc2v 3293 |
. . . . . . . . . . . . 13
⊢ (((𝑚 ∪ 𝑛) ∈ ω ∧ 𝑚 ∈ ω) → (∀𝑥 ∈ ω ∀𝑦 ∈ ω (𝑦 ⊆ 𝑥 → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥)) → (𝑚 ⊆ (𝑚 ∪ 𝑛) → ((rec(𝑅, 𝐴) ↾ ω)‘𝑚) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛))))) |
161 | 26, 149, 151, 160 | syl3c 64 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) → ((rec(𝑅, 𝐴) ↾ ω)‘𝑚) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛))) |
162 | 161 | sseld 3567 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) → (𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑚) → 𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)))) |
163 | | simprr 792 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) → 𝑛 ∈ ω) |
164 | 24, 163 | jca 553 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) → ((𝑚 ∪ 𝑛) ∈ ω ∧ 𝑛 ∈ ω)) |
165 | | ssun2 3739 |
. . . . . . . . . . . . . 14
⊢ 𝑛 ⊆ (𝑚 ∪ 𝑛) |
166 | 165 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) → 𝑛 ⊆ (𝑚 ∪ 𝑛)) |
167 | | sseq1 3589 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 𝑛 → (𝑦 ⊆ (𝑚 ∪ 𝑛) ↔ 𝑛 ⊆ (𝑚 ∪ 𝑛))) |
168 | 109 | sseq1d 3595 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 𝑛 → (((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)) ↔ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)))) |
169 | 167, 168 | imbi12d 333 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 𝑛 → ((𝑦 ⊆ (𝑚 ∪ 𝑛) → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛))) ↔ (𝑛 ⊆ (𝑚 ∪ 𝑛) → ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛))))) |
170 | 155, 169 | rspc2v 3293 |
. . . . . . . . . . . . 13
⊢ (((𝑚 ∪ 𝑛) ∈ ω ∧ 𝑛 ∈ ω) → (∀𝑥 ∈ ω ∀𝑦 ∈ ω (𝑦 ⊆ 𝑥 → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥)) → (𝑛 ⊆ (𝑚 ∪ 𝑛) → ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛))))) |
171 | 164, 149,
166, 170 | syl3c 64 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) → ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛))) |
172 | 171 | sseld 3567 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) → (𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) → 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)))) |
173 | 23 | ad2antlr 759 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) ∧ (𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)) ∧ 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)))) → (𝑚 ∪ 𝑛) ∈ ω) |
174 | | peano2 6978 |
. . . . . . . . . . . . . . 15
⊢ ((𝑚 ∪ 𝑛) ∈ ω → suc (𝑚 ∪ 𝑛) ∈ ω) |
175 | | fveq2 6103 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = suc (𝑚 ∪ 𝑛) → ((rec(𝑅, 𝐴) ↾ ω)‘𝑥) = ((rec(𝑅, 𝐴) ↾ ω)‘suc (𝑚 ∪ 𝑛))) |
176 | 175 | ssiun2s 4500 |
. . . . . . . . . . . . . . 15
⊢ (suc
(𝑚 ∪ 𝑛) ∈ ω → ((rec(𝑅, 𝐴) ↾ ω)‘suc (𝑚 ∪ 𝑛)) ⊆ ∪ 𝑥 ∈ ω ((rec(𝑅, 𝐴) ↾ ω)‘𝑥)) |
177 | 173, 174,
176 | 3syl 18 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) ∧ (𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)) ∧ 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)))) → ((rec(𝑅, 𝐴) ↾ ω)‘suc (𝑚 ∪ 𝑛)) ⊆ ∪ 𝑥 ∈ ω ((rec(𝑅, 𝐴) ↾ ω)‘𝑥)) |
178 | | simprl 790 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) ∧ (𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)) ∧ 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)))) → 𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛))) |
179 | | simprr 792 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) ∧ (𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)) ∧ 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)))) → 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛))) |
180 | | eqidd 2611 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) ∧ (𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)) ∧ 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)))) → (𝑐 ∩ 𝑑) = (𝑐 ∩ 𝑑)) |
181 | | ineq1 3769 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑎 = 𝑐 → (𝑎 ∩ 𝑏) = (𝑐 ∩ 𝑏)) |
182 | 181 | eqeq2d 2620 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑎 = 𝑐 → ((𝑐 ∩ 𝑑) = (𝑎 ∩ 𝑏) ↔ (𝑐 ∩ 𝑑) = (𝑐 ∩ 𝑏))) |
183 | | ineq2 3770 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑏 = 𝑑 → (𝑐 ∩ 𝑏) = (𝑐 ∩ 𝑑)) |
184 | 183 | eqeq2d 2620 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑏 = 𝑑 → ((𝑐 ∩ 𝑑) = (𝑐 ∩ 𝑏) ↔ (𝑐 ∩ 𝑑) = (𝑐 ∩ 𝑑))) |
185 | 182, 184 | rspc2ev 3295 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)) ∧ 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)) ∧ (𝑐 ∩ 𝑑) = (𝑐 ∩ 𝑑)) → ∃𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛))∃𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛))(𝑐 ∩ 𝑑) = (𝑎 ∩ 𝑏)) |
186 | 178, 179,
180, 185 | syl3anc 1318 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) ∧ (𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)) ∧ 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)))) → ∃𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛))∃𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛))(𝑐 ∩ 𝑑) = (𝑎 ∩ 𝑏)) |
187 | | vex 3176 |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝑐 ∈ V |
188 | 187 | inex1 4727 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑐 ∩ 𝑑) ∈ V |
189 | | eqeq1 2614 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = (𝑐 ∩ 𝑑) → (𝑥 = (𝑎 ∩ 𝑏) ↔ (𝑐 ∩ 𝑑) = (𝑎 ∩ 𝑏))) |
190 | 189 | 2rexbidv 3039 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = (𝑐 ∩ 𝑑) → (∃𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛))∃𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛))𝑥 = (𝑎 ∩ 𝑏) ↔ ∃𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛))∃𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛))(𝑐 ∩ 𝑑) = (𝑎 ∩ 𝑏))) |
191 | 188, 190 | elab 3319 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑐 ∩ 𝑑) ∈ {𝑥 ∣ ∃𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛))∃𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛))𝑥 = (𝑎 ∩ 𝑏)} ↔ ∃𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛))∃𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛))(𝑐 ∩ 𝑑) = (𝑎 ∩ 𝑏)) |
192 | 186, 191 | sylibr 223 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) ∧ (𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)) ∧ 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)))) → (𝑐 ∩ 𝑑) ∈ {𝑥 ∣ ∃𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛))∃𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛))𝑥 = (𝑎 ∩ 𝑏)}) |
193 | | eqid 2610 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)) ↦ (𝑎 ∩ 𝑏)) = (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)) ↦ (𝑎 ∩ 𝑏)) |
194 | 193 | rnmpt2 6668 |
. . . . . . . . . . . . . . . 16
⊢ ran
(𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)) ↦ (𝑎 ∩ 𝑏)) = {𝑥 ∣ ∃𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛))∃𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛))𝑥 = (𝑎 ∩ 𝑏)} |
195 | 192, 194 | syl6eleqr 2699 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) ∧ (𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)) ∧ 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)))) → (𝑐 ∩ 𝑑) ∈ ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)) ↦ (𝑎 ∩ 𝑏))) |
196 | | fvex 6113 |
. . . . . . . . . . . . . . . . . . 19
⊢
((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)) ∈ V |
197 | 196 | uniex 6851 |
. . . . . . . . . . . . . . . . . 18
⊢ ∪ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)) ∈ V |
198 | 197 | pwex 4774 |
. . . . . . . . . . . . . . . . 17
⊢ 𝒫
∪ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)) ∈ V |
199 | | elssuni 4403 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)) → 𝑎 ⊆ ∪
((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛))) |
200 | 69, 199 | syl5ss 3579 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)) → (𝑎 ∩ 𝑏) ⊆ ∪
((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛))) |
201 | 74 | elpw 4114 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑎 ∩ 𝑏) ∈ 𝒫 ∪ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)) ↔ (𝑎 ∩ 𝑏) ⊆ ∪
((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛))) |
202 | 200, 201 | sylibr 223 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)) → (𝑎 ∩ 𝑏) ∈ 𝒫 ∪ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛))) |
203 | 202 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)) ∧ 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛))) → (𝑎 ∩ 𝑏) ∈ 𝒫 ∪ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛))) |
204 | 203 | rgen2a 2960 |
. . . . . . . . . . . . . . . . . . 19
⊢
∀𝑎 ∈
((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛))∀𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛))(𝑎 ∩ 𝑏) ∈ 𝒫 ∪ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)) |
205 | 193 | fmpt2 7126 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∀𝑎 ∈
((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛))∀𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛))(𝑎 ∩ 𝑏) ∈ 𝒫 ∪ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)) ↔ (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)) ↦ (𝑎 ∩ 𝑏)):(((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)) × ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)))⟶𝒫 ∪ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛))) |
206 | 204, 205 | mpbi 219 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)) ↦ (𝑎 ∩ 𝑏)):(((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)) × ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)))⟶𝒫 ∪ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)) |
207 | | frn 5966 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)) ↦ (𝑎 ∩ 𝑏)):(((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)) × ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)))⟶𝒫 ∪ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)) → ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)) ↦ (𝑎 ∩ 𝑏)) ⊆ 𝒫 ∪ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛))) |
208 | 206, 207 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
⊢ ran
(𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)) ↦ (𝑎 ∩ 𝑏)) ⊆ 𝒫 ∪ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)) |
209 | 198, 208 | ssexi 4731 |
. . . . . . . . . . . . . . . 16
⊢ ran
(𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)) ↦ (𝑎 ∩ 𝑏)) ∈ V |
210 | | nfcv 2751 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑣(𝑚 ∪ 𝑛) |
211 | | nfcv 2751 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑣ran
(𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)) ↦ (𝑎 ∩ 𝑏)) |
212 | | mpt2eq12 6613 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑣 = ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)) ∧ 𝑣 = ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛))) → (𝑎 ∈ 𝑣, 𝑏 ∈ 𝑣 ↦ (𝑎 ∩ 𝑏)) = (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)) ↦ (𝑎 ∩ 𝑏))) |
213 | 212 | anidms 675 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑣 = ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)) → (𝑎 ∈ 𝑣, 𝑏 ∈ 𝑣 ↦ (𝑎 ∩ 𝑏)) = (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)) ↦ (𝑎 ∩ 𝑏))) |
214 | 213 | rneqd 5274 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑣 = ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)) → ran (𝑎 ∈ 𝑣, 𝑏 ∈ 𝑣 ↦ (𝑎 ∩ 𝑏)) = ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)) ↦ (𝑎 ∩ 𝑏))) |
215 | 83, 210, 211, 98, 214 | frsucmpt 7420 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑚 ∪ 𝑛) ∈ ω ∧ ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)) ↦ (𝑎 ∩ 𝑏)) ∈ V) → ((rec(𝑅, 𝐴) ↾ ω)‘suc (𝑚 ∪ 𝑛)) = ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)) ↦ (𝑎 ∩ 𝑏))) |
216 | 173, 209,
215 | sylancl 693 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) ∧ (𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)) ∧ 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)))) → ((rec(𝑅, 𝐴) ↾ ω)‘suc (𝑚 ∪ 𝑛)) = ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)) ↦ (𝑎 ∩ 𝑏))) |
217 | 195, 216 | eleqtrrd 2691 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) ∧ (𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)) ∧ 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)))) → (𝑐 ∩ 𝑑) ∈ ((rec(𝑅, 𝐴) ↾ ω)‘suc (𝑚 ∪ 𝑛))) |
218 | 177, 217 | sseldd 3569 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) ∧ (𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)) ∧ 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)))) → (𝑐 ∩ 𝑑) ∈ ∪
𝑥 ∈ ω
((rec(𝑅, 𝐴) ↾ ω)‘𝑥)) |
219 | | fniunfv 6409 |
. . . . . . . . . . . . . 14
⊢
((rec(𝑅, 𝐴) ↾ ω) Fn ω
→ ∪ 𝑥 ∈ ω ((rec(𝑅, 𝐴) ↾ ω)‘𝑥) = ∪ ran
(rec(𝑅, 𝐴) ↾ ω)) |
220 | 3, 219 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ ∪ 𝑥 ∈ ω ((rec(𝑅, 𝐴) ↾ ω)‘𝑥) = ∪ ran
(rec(𝑅, 𝐴) ↾ ω) |
221 | 218, 220 | syl6eleq 2698 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) ∧ (𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)) ∧ 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)))) → (𝑐 ∩ 𝑑) ∈ ∪ ran
(rec(𝑅, 𝐴) ↾ ω)) |
222 | 221 | ex 449 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) → ((𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)) ∧ 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛))) → (𝑐 ∩ 𝑑) ∈ ∪ ran
(rec(𝑅, 𝐴) ↾ ω))) |
223 | 162, 172,
222 | syl2and 499 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) → ((𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑚) ∧ 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)) → (𝑐 ∩ 𝑑) ∈ ∪ ran
(rec(𝑅, 𝐴) ↾ ω))) |
224 | 223 | rexlimdvva 3020 |
. . . . . . . . 9
⊢ (𝐴 ∈ 𝑉 → (∃𝑚 ∈ ω ∃𝑛 ∈ ω (𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑚) ∧ 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)) → (𝑐 ∩ 𝑑) ∈ ∪ ran
(rec(𝑅, 𝐴) ↾ ω))) |
225 | 224 | imp 444 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ ∃𝑚 ∈ ω ∃𝑛 ∈ ω (𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑚) ∧ 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛))) → (𝑐 ∩ 𝑑) ∈ ∪ ran
(rec(𝑅, 𝐴) ↾ ω)) |
226 | 20, 225 | sylan2br 492 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑐 ∈ ∪ ran
(rec(𝑅, 𝐴) ↾ ω) ∧ 𝑑 ∈ ∪ ran
(rec(𝑅, 𝐴) ↾ ω))) → (𝑐 ∩ 𝑑) ∈ ∪ ran
(rec(𝑅, 𝐴) ↾ ω)) |
227 | 226 | ralrimivva 2954 |
. . . . . 6
⊢ (𝐴 ∈ 𝑉 → ∀𝑐 ∈ ∪ ran
(rec(𝑅, 𝐴) ↾ ω)∀𝑑 ∈ ∪ ran
(rec(𝑅, 𝐴) ↾ ω)(𝑐 ∩ 𝑑) ∈ ∪ ran
(rec(𝑅, 𝐴) ↾ ω)) |
228 | 136 | simpld 474 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ ω) → ((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ⊆ (fi‘𝐴)) |
229 | | fvex 6113 |
. . . . . . . . . . . . 13
⊢
(fi‘𝐴) ∈
V |
230 | 229 | elpw2 4755 |
. . . . . . . . . . . 12
⊢
(((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ∈ 𝒫
(fi‘𝐴) ↔
((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ⊆ (fi‘𝐴)) |
231 | 228, 230 | sylibr 223 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ ω) → ((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ∈ 𝒫 (fi‘𝐴)) |
232 | 231 | ralrimiva 2949 |
. . . . . . . . . 10
⊢ (𝐴 ∈ 𝑉 → ∀𝑥 ∈ ω ((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ∈ 𝒫 (fi‘𝐴)) |
233 | | fnfvrnss 6297 |
. . . . . . . . . 10
⊢
(((rec(𝑅, 𝐴) ↾ ω) Fn ω
∧ ∀𝑥 ∈
ω ((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ∈ 𝒫
(fi‘𝐴)) → ran
(rec(𝑅, 𝐴) ↾ ω) ⊆ 𝒫
(fi‘𝐴)) |
234 | 3, 232, 233 | sylancr 694 |
. . . . . . . . 9
⊢ (𝐴 ∈ 𝑉 → ran (rec(𝑅, 𝐴) ↾ ω) ⊆ 𝒫
(fi‘𝐴)) |
235 | | sspwuni 4547 |
. . . . . . . . 9
⊢ (ran
(rec(𝑅, 𝐴) ↾ ω) ⊆ 𝒫
(fi‘𝐴) ↔ ∪ ran (rec(𝑅, 𝐴) ↾ ω) ⊆ (fi‘𝐴)) |
236 | 234, 235 | sylib 207 |
. . . . . . . 8
⊢ (𝐴 ∈ 𝑉 → ∪ ran
(rec(𝑅, 𝐴) ↾ ω) ⊆ (fi‘𝐴)) |
237 | | ssexg 4732 |
. . . . . . . 8
⊢ ((∪ ran (rec(𝑅, 𝐴) ↾ ω) ⊆ (fi‘𝐴) ∧ (fi‘𝐴) ∈ V) → ∪ ran (rec(𝑅, 𝐴) ↾ ω) ∈
V) |
238 | 236, 229,
237 | sylancl 693 |
. . . . . . 7
⊢ (𝐴 ∈ 𝑉 → ∪ ran
(rec(𝑅, 𝐴) ↾ ω) ∈
V) |
239 | | sseq2 3590 |
. . . . . . . . 9
⊢ (𝑥 = ∪
ran (rec(𝑅, 𝐴) ↾ ω) → (𝐴 ⊆ 𝑥 ↔ 𝐴 ⊆ ∪ ran
(rec(𝑅, 𝐴) ↾ ω))) |
240 | | eleq2 2677 |
. . . . . . . . . . 11
⊢ (𝑥 = ∪
ran (rec(𝑅, 𝐴) ↾ ω) →
((𝑐 ∩ 𝑑) ∈ 𝑥 ↔ (𝑐 ∩ 𝑑) ∈ ∪ ran
(rec(𝑅, 𝐴) ↾ ω))) |
241 | 240 | raleqbi1dv 3123 |
. . . . . . . . . 10
⊢ (𝑥 = ∪
ran (rec(𝑅, 𝐴) ↾ ω) →
(∀𝑑 ∈ 𝑥 (𝑐 ∩ 𝑑) ∈ 𝑥 ↔ ∀𝑑 ∈ ∪ ran
(rec(𝑅, 𝐴) ↾ ω)(𝑐 ∩ 𝑑) ∈ ∪ ran
(rec(𝑅, 𝐴) ↾ ω))) |
242 | 241 | raleqbi1dv 3123 |
. . . . . . . . 9
⊢ (𝑥 = ∪
ran (rec(𝑅, 𝐴) ↾ ω) →
(∀𝑐 ∈ 𝑥 ∀𝑑 ∈ 𝑥 (𝑐 ∩ 𝑑) ∈ 𝑥 ↔ ∀𝑐 ∈ ∪ ran
(rec(𝑅, 𝐴) ↾ ω)∀𝑑 ∈ ∪ ran
(rec(𝑅, 𝐴) ↾ ω)(𝑐 ∩ 𝑑) ∈ ∪ ran
(rec(𝑅, 𝐴) ↾ ω))) |
243 | 239, 242 | anbi12d 743 |
. . . . . . . 8
⊢ (𝑥 = ∪
ran (rec(𝑅, 𝐴) ↾ ω) →
((𝐴 ⊆ 𝑥 ∧ ∀𝑐 ∈ 𝑥 ∀𝑑 ∈ 𝑥 (𝑐 ∩ 𝑑) ∈ 𝑥) ↔ (𝐴 ⊆ ∪ ran
(rec(𝑅, 𝐴) ↾ ω) ∧ ∀𝑐 ∈ ∪ ran (rec(𝑅, 𝐴) ↾ ω)∀𝑑 ∈ ∪ ran
(rec(𝑅, 𝐴) ↾ ω)(𝑐 ∩ 𝑑) ∈ ∪ ran
(rec(𝑅, 𝐴) ↾ ω)))) |
244 | 243 | elabg 3320 |
. . . . . . 7
⊢ (∪ ran (rec(𝑅, 𝐴) ↾ ω) ∈ V → (∪ ran (rec(𝑅, 𝐴) ↾ ω) ∈ {𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ ∀𝑐 ∈ 𝑥 ∀𝑑 ∈ 𝑥 (𝑐 ∩ 𝑑) ∈ 𝑥)} ↔ (𝐴 ⊆ ∪ ran
(rec(𝑅, 𝐴) ↾ ω) ∧ ∀𝑐 ∈ ∪ ran (rec(𝑅, 𝐴) ↾ ω)∀𝑑 ∈ ∪ ran
(rec(𝑅, 𝐴) ↾ ω)(𝑐 ∩ 𝑑) ∈ ∪ ran
(rec(𝑅, 𝐴) ↾ ω)))) |
245 | 238, 244 | syl 17 |
. . . . . 6
⊢ (𝐴 ∈ 𝑉 → (∪ ran
(rec(𝑅, 𝐴) ↾ ω) ∈ {𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ ∀𝑐 ∈ 𝑥 ∀𝑑 ∈ 𝑥 (𝑐 ∩ 𝑑) ∈ 𝑥)} ↔ (𝐴 ⊆ ∪ ran
(rec(𝑅, 𝐴) ↾ ω) ∧ ∀𝑐 ∈ ∪ ran (rec(𝑅, 𝐴) ↾ ω)∀𝑑 ∈ ∪ ran
(rec(𝑅, 𝐴) ↾ ω)(𝑐 ∩ 𝑑) ∈ ∪ ran
(rec(𝑅, 𝐴) ↾ ω)))) |
246 | 9, 227, 245 | mpbir2and 959 |
. . . . 5
⊢ (𝐴 ∈ 𝑉 → ∪ ran
(rec(𝑅, 𝐴) ↾ ω) ∈ {𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ ∀𝑐 ∈ 𝑥 ∀𝑑 ∈ 𝑥 (𝑐 ∩ 𝑑) ∈ 𝑥)}) |
247 | | intss1 4427 |
. . . . 5
⊢ (∪ ran (rec(𝑅, 𝐴) ↾ ω) ∈ {𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ ∀𝑐 ∈ 𝑥 ∀𝑑 ∈ 𝑥 (𝑐 ∩ 𝑑) ∈ 𝑥)} → ∩ {𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ ∀𝑐 ∈ 𝑥 ∀𝑑 ∈ 𝑥 (𝑐 ∩ 𝑑) ∈ 𝑥)} ⊆ ∪ ran
(rec(𝑅, 𝐴) ↾ ω)) |
248 | 246, 247 | syl 17 |
. . . 4
⊢ (𝐴 ∈ 𝑉 → ∩ {𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ ∀𝑐 ∈ 𝑥 ∀𝑑 ∈ 𝑥 (𝑐 ∩ 𝑑) ∈ 𝑥)} ⊆ ∪ ran
(rec(𝑅, 𝐴) ↾ ω)) |
249 | 1, 248 | eqsstrd 3602 |
. . 3
⊢ (𝐴 ∈ 𝑉 → (fi‘𝐴) ⊆ ∪ ran
(rec(𝑅, 𝐴) ↾ ω)) |
250 | 249, 236 | eqssd 3585 |
. 2
⊢ (𝐴 ∈ 𝑉 → (fi‘𝐴) = ∪ ran
(rec(𝑅, 𝐴) ↾ ω)) |
251 | | df-ima 5051 |
. . 3
⊢
(rec(𝑅, 𝐴) “ ω) = ran
(rec(𝑅, 𝐴) ↾ ω) |
252 | 251 | unieqi 4381 |
. 2
⊢ ∪ (rec(𝑅, 𝐴) “ ω) = ∪ ran (rec(𝑅, 𝐴) ↾ ω) |
253 | 250, 252 | syl6eqr 2662 |
1
⊢ (𝐴 ∈ 𝑉 → (fi‘𝐴) = ∪ (rec(𝑅, 𝐴) “ ω)) |