Step |
Hyp |
Ref |
Expression |
1 |
|
dffi3.1 |
⊢ 𝑅 = ( 𝑢 ∈ V ↦ ran ( 𝑦 ∈ 𝑢 , 𝑧 ∈ 𝑢 ↦ ( 𝑦 ∩ 𝑧 ) ) ) |
2 |
|
dffi2 |
⊢ ( 𝐴 ∈ 𝑉 → ( fi ‘ 𝐴 ) = ∩ { 𝑥 ∣ ( 𝐴 ⊆ 𝑥 ∧ ∀ 𝑐 ∈ 𝑥 ∀ 𝑑 ∈ 𝑥 ( 𝑐 ∩ 𝑑 ) ∈ 𝑥 ) } ) |
3 |
|
fr0g |
⊢ ( 𝐴 ∈ 𝑉 → ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ∅ ) = 𝐴 ) |
4 |
|
frfnom |
⊢ ( rec ( 𝑅 , 𝐴 ) ↾ ω ) Fn ω |
5 |
|
peano1 |
⊢ ∅ ∈ ω |
6 |
|
fnfvelrn |
⊢ ( ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) Fn ω ∧ ∅ ∈ ω ) → ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ∅ ) ∈ ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ) |
7 |
4 5 6
|
mp2an |
⊢ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ∅ ) ∈ ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) |
8 |
3 7
|
eqeltrrdi |
⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ) |
9 |
|
elssuni |
⊢ ( 𝐴 ∈ ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) → 𝐴 ⊆ ∪ ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ) |
10 |
8 9
|
syl |
⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ⊆ ∪ ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ) |
11 |
|
reeanv |
⊢ ( ∃ 𝑚 ∈ ω ∃ 𝑛 ∈ ω ( 𝑐 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑚 ) ∧ 𝑑 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ) ↔ ( ∃ 𝑚 ∈ ω 𝑐 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑚 ) ∧ ∃ 𝑛 ∈ ω 𝑑 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ) ) |
12 |
|
eliun |
⊢ ( 𝑐 ∈ ∪ 𝑚 ∈ ω ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑚 ) ↔ ∃ 𝑚 ∈ ω 𝑐 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑚 ) ) |
13 |
|
eliun |
⊢ ( 𝑑 ∈ ∪ 𝑛 ∈ ω ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ↔ ∃ 𝑛 ∈ ω 𝑑 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ) |
14 |
12 13
|
anbi12i |
⊢ ( ( 𝑐 ∈ ∪ 𝑚 ∈ ω ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑚 ) ∧ 𝑑 ∈ ∪ 𝑛 ∈ ω ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ) ↔ ( ∃ 𝑚 ∈ ω 𝑐 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑚 ) ∧ ∃ 𝑛 ∈ ω 𝑑 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ) ) |
15 |
|
fniunfv |
⊢ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) Fn ω → ∪ 𝑚 ∈ ω ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑚 ) = ∪ ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ) |
16 |
15
|
eleq2d |
⊢ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) Fn ω → ( 𝑐 ∈ ∪ 𝑚 ∈ ω ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑚 ) ↔ 𝑐 ∈ ∪ ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ) ) |
17 |
|
fniunfv |
⊢ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) Fn ω → ∪ 𝑛 ∈ ω ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) = ∪ ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ) |
18 |
17
|
eleq2d |
⊢ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) Fn ω → ( 𝑑 ∈ ∪ 𝑛 ∈ ω ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ↔ 𝑑 ∈ ∪ ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ) ) |
19 |
16 18
|
anbi12d |
⊢ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) Fn ω → ( ( 𝑐 ∈ ∪ 𝑚 ∈ ω ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑚 ) ∧ 𝑑 ∈ ∪ 𝑛 ∈ ω ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ) ↔ ( 𝑐 ∈ ∪ ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ∧ 𝑑 ∈ ∪ ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ) ) ) |
20 |
4 19
|
ax-mp |
⊢ ( ( 𝑐 ∈ ∪ 𝑚 ∈ ω ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑚 ) ∧ 𝑑 ∈ ∪ 𝑛 ∈ ω ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ) ↔ ( 𝑐 ∈ ∪ ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ∧ 𝑑 ∈ ∪ ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ) ) |
21 |
11 14 20
|
3bitr2i |
⊢ ( ∃ 𝑚 ∈ ω ∃ 𝑛 ∈ ω ( 𝑐 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑚 ) ∧ 𝑑 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ) ↔ ( 𝑐 ∈ ∪ ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ∧ 𝑑 ∈ ∪ ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ) ) |
22 |
|
ordom |
⊢ Ord ω |
23 |
|
ordunel |
⊢ ( ( Ord ω ∧ 𝑚 ∈ ω ∧ 𝑛 ∈ ω ) → ( 𝑚 ∪ 𝑛 ) ∈ ω ) |
24 |
22 23
|
mp3an1 |
⊢ ( ( 𝑚 ∈ ω ∧ 𝑛 ∈ ω ) → ( 𝑚 ∪ 𝑛 ) ∈ ω ) |
25 |
24
|
adantl |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑚 ∈ ω ∧ 𝑛 ∈ ω ) ) → ( 𝑚 ∪ 𝑛 ) ∈ ω ) |
26 |
|
simprl |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑚 ∈ ω ∧ 𝑛 ∈ ω ) ) → 𝑚 ∈ ω ) |
27 |
25 26
|
jca |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑚 ∈ ω ∧ 𝑛 ∈ ω ) ) → ( ( 𝑚 ∪ 𝑛 ) ∈ ω ∧ 𝑚 ∈ ω ) ) |
28 |
|
nnon |
⊢ ( 𝑦 ∈ ω → 𝑦 ∈ On ) |
29 |
|
nnon |
⊢ ( 𝑥 ∈ ω → 𝑥 ∈ On ) |
30 |
29
|
ad2antlr |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑥 ∈ ω ) ∧ 𝑦 ∈ ω ) → 𝑥 ∈ On ) |
31 |
|
onsseleq |
⊢ ( ( 𝑦 ∈ On ∧ 𝑥 ∈ On ) → ( 𝑦 ⊆ 𝑥 ↔ ( 𝑦 ∈ 𝑥 ∨ 𝑦 = 𝑥 ) ) ) |
32 |
28 30 31
|
syl2an2 |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑥 ∈ ω ) ∧ 𝑦 ∈ ω ) → ( 𝑦 ⊆ 𝑥 ↔ ( 𝑦 ∈ 𝑥 ∨ 𝑦 = 𝑥 ) ) ) |
33 |
|
rzal |
⊢ ( 𝑥 = ∅ → ∀ 𝑦 ∈ 𝑥 ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑥 ) ) |
34 |
33
|
biantrud |
⊢ ( 𝑥 = ∅ → ( ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑥 ) ⊆ ( fi ‘ 𝐴 ) ↔ ( ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑥 ) ⊆ ( fi ‘ 𝐴 ) ∧ ∀ 𝑦 ∈ 𝑥 ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑥 ) ) ) ) |
35 |
|
fveq2 |
⊢ ( 𝑥 = ∅ → ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑥 ) = ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ∅ ) ) |
36 |
35
|
sseq1d |
⊢ ( 𝑥 = ∅ → ( ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑥 ) ⊆ ( fi ‘ 𝐴 ) ↔ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ∅ ) ⊆ ( fi ‘ 𝐴 ) ) ) |
37 |
34 36
|
bitr3d |
⊢ ( 𝑥 = ∅ → ( ( ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑥 ) ⊆ ( fi ‘ 𝐴 ) ∧ ∀ 𝑦 ∈ 𝑥 ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑥 ) ) ↔ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ∅ ) ⊆ ( fi ‘ 𝐴 ) ) ) |
38 |
|
fveq2 |
⊢ ( 𝑥 = 𝑛 → ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑥 ) = ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ) |
39 |
38
|
sseq1d |
⊢ ( 𝑥 = 𝑛 → ( ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑥 ) ⊆ ( fi ‘ 𝐴 ) ↔ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ⊆ ( fi ‘ 𝐴 ) ) ) |
40 |
38
|
sseq2d |
⊢ ( 𝑥 = 𝑛 → ( ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑥 ) ↔ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ) ) |
41 |
40
|
raleqbi1dv |
⊢ ( 𝑥 = 𝑛 → ( ∀ 𝑦 ∈ 𝑥 ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑥 ) ↔ ∀ 𝑦 ∈ 𝑛 ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ) ) |
42 |
39 41
|
anbi12d |
⊢ ( 𝑥 = 𝑛 → ( ( ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑥 ) ⊆ ( fi ‘ 𝐴 ) ∧ ∀ 𝑦 ∈ 𝑥 ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑥 ) ) ↔ ( ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ⊆ ( fi ‘ 𝐴 ) ∧ ∀ 𝑦 ∈ 𝑛 ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ) ) ) |
43 |
|
fveq2 |
⊢ ( 𝑥 = suc 𝑛 → ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑥 ) = ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ suc 𝑛 ) ) |
44 |
43
|
sseq1d |
⊢ ( 𝑥 = suc 𝑛 → ( ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑥 ) ⊆ ( fi ‘ 𝐴 ) ↔ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ suc 𝑛 ) ⊆ ( fi ‘ 𝐴 ) ) ) |
45 |
43
|
sseq2d |
⊢ ( 𝑥 = suc 𝑛 → ( ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑥 ) ↔ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ suc 𝑛 ) ) ) |
46 |
45
|
raleqbi1dv |
⊢ ( 𝑥 = suc 𝑛 → ( ∀ 𝑦 ∈ 𝑥 ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑥 ) ↔ ∀ 𝑦 ∈ suc 𝑛 ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ suc 𝑛 ) ) ) |
47 |
44 46
|
anbi12d |
⊢ ( 𝑥 = suc 𝑛 → ( ( ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑥 ) ⊆ ( fi ‘ 𝐴 ) ∧ ∀ 𝑦 ∈ 𝑥 ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑥 ) ) ↔ ( ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ suc 𝑛 ) ⊆ ( fi ‘ 𝐴 ) ∧ ∀ 𝑦 ∈ suc 𝑛 ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ suc 𝑛 ) ) ) ) |
48 |
|
ssfii |
⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ⊆ ( fi ‘ 𝐴 ) ) |
49 |
3 48
|
eqsstrd |
⊢ ( 𝐴 ∈ 𝑉 → ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ∅ ) ⊆ ( fi ‘ 𝐴 ) ) |
50 |
|
id |
⊢ ( 𝑥 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) → 𝑥 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ) |
51 |
|
eqidd |
⊢ ( 𝑥 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) → 𝑥 = 𝑥 ) |
52 |
|
ineq1 |
⊢ ( 𝑎 = 𝑥 → ( 𝑎 ∩ 𝑏 ) = ( 𝑥 ∩ 𝑏 ) ) |
53 |
52
|
eqeq2d |
⊢ ( 𝑎 = 𝑥 → ( 𝑥 = ( 𝑎 ∩ 𝑏 ) ↔ 𝑥 = ( 𝑥 ∩ 𝑏 ) ) ) |
54 |
|
ineq2 |
⊢ ( 𝑏 = 𝑥 → ( 𝑥 ∩ 𝑏 ) = ( 𝑥 ∩ 𝑥 ) ) |
55 |
|
inidm |
⊢ ( 𝑥 ∩ 𝑥 ) = 𝑥 |
56 |
54 55
|
eqtrdi |
⊢ ( 𝑏 = 𝑥 → ( 𝑥 ∩ 𝑏 ) = 𝑥 ) |
57 |
56
|
eqeq2d |
⊢ ( 𝑏 = 𝑥 → ( 𝑥 = ( 𝑥 ∩ 𝑏 ) ↔ 𝑥 = 𝑥 ) ) |
58 |
53 57
|
rspc2ev |
⊢ ( ( 𝑥 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ∧ 𝑥 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ∧ 𝑥 = 𝑥 ) → ∃ 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ∃ 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) 𝑥 = ( 𝑎 ∩ 𝑏 ) ) |
59 |
50 50 51 58
|
syl3anc |
⊢ ( 𝑥 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) → ∃ 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ∃ 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) 𝑥 = ( 𝑎 ∩ 𝑏 ) ) |
60 |
|
eqid |
⊢ ( 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) , 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ↦ ( 𝑎 ∩ 𝑏 ) ) = ( 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) , 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ↦ ( 𝑎 ∩ 𝑏 ) ) |
61 |
60
|
rnmpo |
⊢ ran ( 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) , 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ↦ ( 𝑎 ∩ 𝑏 ) ) = { 𝑥 ∣ ∃ 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ∃ 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) 𝑥 = ( 𝑎 ∩ 𝑏 ) } |
62 |
61
|
abeq2i |
⊢ ( 𝑥 ∈ ran ( 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) , 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ↦ ( 𝑎 ∩ 𝑏 ) ) ↔ ∃ 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ∃ 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) 𝑥 = ( 𝑎 ∩ 𝑏 ) ) |
63 |
59 62
|
sylibr |
⊢ ( 𝑥 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) → 𝑥 ∈ ran ( 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) , 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ↦ ( 𝑎 ∩ 𝑏 ) ) ) |
64 |
63
|
ssriv |
⊢ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ⊆ ran ( 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) , 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ↦ ( 𝑎 ∩ 𝑏 ) ) |
65 |
|
simpl |
⊢ ( ( 𝑛 ∈ ω ∧ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ⊆ ( fi ‘ 𝐴 ) ) → 𝑛 ∈ ω ) |
66 |
|
fvex |
⊢ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ∈ V |
67 |
66
|
uniex |
⊢ ∪ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ∈ V |
68 |
67
|
pwex |
⊢ 𝒫 ∪ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ∈ V |
69 |
|
inss1 |
⊢ ( 𝑎 ∩ 𝑏 ) ⊆ 𝑎 |
70 |
|
elssuni |
⊢ ( 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) → 𝑎 ⊆ ∪ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ) |
71 |
70
|
adantr |
⊢ ( ( 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ∧ 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ) → 𝑎 ⊆ ∪ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ) |
72 |
69 71
|
sstrid |
⊢ ( ( 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ∧ 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ) → ( 𝑎 ∩ 𝑏 ) ⊆ ∪ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ) |
73 |
|
vex |
⊢ 𝑎 ∈ V |
74 |
73
|
inex1 |
⊢ ( 𝑎 ∩ 𝑏 ) ∈ V |
75 |
74
|
elpw |
⊢ ( ( 𝑎 ∩ 𝑏 ) ∈ 𝒫 ∪ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ↔ ( 𝑎 ∩ 𝑏 ) ⊆ ∪ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ) |
76 |
72 75
|
sylibr |
⊢ ( ( 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ∧ 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ) → ( 𝑎 ∩ 𝑏 ) ∈ 𝒫 ∪ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ) |
77 |
76
|
rgen2 |
⊢ ∀ 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ∀ 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ( 𝑎 ∩ 𝑏 ) ∈ 𝒫 ∪ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) |
78 |
60
|
fmpo |
⊢ ( ∀ 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ∀ 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ( 𝑎 ∩ 𝑏 ) ∈ 𝒫 ∪ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ↔ ( 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) , 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ↦ ( 𝑎 ∩ 𝑏 ) ) : ( ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) × ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ) ⟶ 𝒫 ∪ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ) |
79 |
77 78
|
mpbi |
⊢ ( 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) , 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ↦ ( 𝑎 ∩ 𝑏 ) ) : ( ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) × ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ) ⟶ 𝒫 ∪ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) |
80 |
|
frn |
⊢ ( ( 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) , 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ↦ ( 𝑎 ∩ 𝑏 ) ) : ( ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) × ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ) ⟶ 𝒫 ∪ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) → ran ( 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) , 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ↦ ( 𝑎 ∩ 𝑏 ) ) ⊆ 𝒫 ∪ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ) |
81 |
79 80
|
ax-mp |
⊢ ran ( 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) , 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ↦ ( 𝑎 ∩ 𝑏 ) ) ⊆ 𝒫 ∪ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) |
82 |
68 81
|
ssexi |
⊢ ran ( 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) , 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ↦ ( 𝑎 ∩ 𝑏 ) ) ∈ V |
83 |
|
nfcv |
⊢ Ⅎ 𝑣 𝐴 |
84 |
|
nfcv |
⊢ Ⅎ 𝑣 𝑛 |
85 |
|
nfcv |
⊢ Ⅎ 𝑣 ran ( 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) , 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ↦ ( 𝑎 ∩ 𝑏 ) ) |
86 |
|
mpoeq12 |
⊢ ( ( 𝑢 = 𝑣 ∧ 𝑢 = 𝑣 ) → ( 𝑦 ∈ 𝑢 , 𝑧 ∈ 𝑢 ↦ ( 𝑦 ∩ 𝑧 ) ) = ( 𝑦 ∈ 𝑣 , 𝑧 ∈ 𝑣 ↦ ( 𝑦 ∩ 𝑧 ) ) ) |
87 |
86
|
anidms |
⊢ ( 𝑢 = 𝑣 → ( 𝑦 ∈ 𝑢 , 𝑧 ∈ 𝑢 ↦ ( 𝑦 ∩ 𝑧 ) ) = ( 𝑦 ∈ 𝑣 , 𝑧 ∈ 𝑣 ↦ ( 𝑦 ∩ 𝑧 ) ) ) |
88 |
|
ineq1 |
⊢ ( 𝑦 = 𝑎 → ( 𝑦 ∩ 𝑧 ) = ( 𝑎 ∩ 𝑧 ) ) |
89 |
|
ineq2 |
⊢ ( 𝑧 = 𝑏 → ( 𝑎 ∩ 𝑧 ) = ( 𝑎 ∩ 𝑏 ) ) |
90 |
88 89
|
cbvmpov |
⊢ ( 𝑦 ∈ 𝑣 , 𝑧 ∈ 𝑣 ↦ ( 𝑦 ∩ 𝑧 ) ) = ( 𝑎 ∈ 𝑣 , 𝑏 ∈ 𝑣 ↦ ( 𝑎 ∩ 𝑏 ) ) |
91 |
87 90
|
eqtrdi |
⊢ ( 𝑢 = 𝑣 → ( 𝑦 ∈ 𝑢 , 𝑧 ∈ 𝑢 ↦ ( 𝑦 ∩ 𝑧 ) ) = ( 𝑎 ∈ 𝑣 , 𝑏 ∈ 𝑣 ↦ ( 𝑎 ∩ 𝑏 ) ) ) |
92 |
91
|
rneqd |
⊢ ( 𝑢 = 𝑣 → ran ( 𝑦 ∈ 𝑢 , 𝑧 ∈ 𝑢 ↦ ( 𝑦 ∩ 𝑧 ) ) = ran ( 𝑎 ∈ 𝑣 , 𝑏 ∈ 𝑣 ↦ ( 𝑎 ∩ 𝑏 ) ) ) |
93 |
92
|
cbvmptv |
⊢ ( 𝑢 ∈ V ↦ ran ( 𝑦 ∈ 𝑢 , 𝑧 ∈ 𝑢 ↦ ( 𝑦 ∩ 𝑧 ) ) ) = ( 𝑣 ∈ V ↦ ran ( 𝑎 ∈ 𝑣 , 𝑏 ∈ 𝑣 ↦ ( 𝑎 ∩ 𝑏 ) ) ) |
94 |
1 93
|
eqtri |
⊢ 𝑅 = ( 𝑣 ∈ V ↦ ran ( 𝑎 ∈ 𝑣 , 𝑏 ∈ 𝑣 ↦ ( 𝑎 ∩ 𝑏 ) ) ) |
95 |
|
rdgeq1 |
⊢ ( 𝑅 = ( 𝑣 ∈ V ↦ ran ( 𝑎 ∈ 𝑣 , 𝑏 ∈ 𝑣 ↦ ( 𝑎 ∩ 𝑏 ) ) ) → rec ( 𝑅 , 𝐴 ) = rec ( ( 𝑣 ∈ V ↦ ran ( 𝑎 ∈ 𝑣 , 𝑏 ∈ 𝑣 ↦ ( 𝑎 ∩ 𝑏 ) ) ) , 𝐴 ) ) |
96 |
94 95
|
ax-mp |
⊢ rec ( 𝑅 , 𝐴 ) = rec ( ( 𝑣 ∈ V ↦ ran ( 𝑎 ∈ 𝑣 , 𝑏 ∈ 𝑣 ↦ ( 𝑎 ∩ 𝑏 ) ) ) , 𝐴 ) |
97 |
96
|
reseq1i |
⊢ ( rec ( 𝑅 , 𝐴 ) ↾ ω ) = ( rec ( ( 𝑣 ∈ V ↦ ran ( 𝑎 ∈ 𝑣 , 𝑏 ∈ 𝑣 ↦ ( 𝑎 ∩ 𝑏 ) ) ) , 𝐴 ) ↾ ω ) |
98 |
|
mpoeq12 |
⊢ ( ( 𝑣 = ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ∧ 𝑣 = ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ) → ( 𝑎 ∈ 𝑣 , 𝑏 ∈ 𝑣 ↦ ( 𝑎 ∩ 𝑏 ) ) = ( 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) , 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ↦ ( 𝑎 ∩ 𝑏 ) ) ) |
99 |
98
|
anidms |
⊢ ( 𝑣 = ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) → ( 𝑎 ∈ 𝑣 , 𝑏 ∈ 𝑣 ↦ ( 𝑎 ∩ 𝑏 ) ) = ( 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) , 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ↦ ( 𝑎 ∩ 𝑏 ) ) ) |
100 |
99
|
rneqd |
⊢ ( 𝑣 = ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) → ran ( 𝑎 ∈ 𝑣 , 𝑏 ∈ 𝑣 ↦ ( 𝑎 ∩ 𝑏 ) ) = ran ( 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) , 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ↦ ( 𝑎 ∩ 𝑏 ) ) ) |
101 |
83 84 85 97 100
|
frsucmpt |
⊢ ( ( 𝑛 ∈ ω ∧ ran ( 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) , 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ↦ ( 𝑎 ∩ 𝑏 ) ) ∈ V ) → ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ suc 𝑛 ) = ran ( 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) , 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ↦ ( 𝑎 ∩ 𝑏 ) ) ) |
102 |
65 82 101
|
sylancl |
⊢ ( ( 𝑛 ∈ ω ∧ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ⊆ ( fi ‘ 𝐴 ) ) → ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ suc 𝑛 ) = ran ( 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) , 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ↦ ( 𝑎 ∩ 𝑏 ) ) ) |
103 |
64 102
|
sseqtrrid |
⊢ ( ( 𝑛 ∈ ω ∧ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ⊆ ( fi ‘ 𝐴 ) ) → ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ suc 𝑛 ) ) |
104 |
|
sstr2 |
⊢ ( ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) → ( ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ suc 𝑛 ) → ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ suc 𝑛 ) ) ) |
105 |
103 104
|
syl5com |
⊢ ( ( 𝑛 ∈ ω ∧ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ⊆ ( fi ‘ 𝐴 ) ) → ( ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) → ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ suc 𝑛 ) ) ) |
106 |
105
|
ralimdv |
⊢ ( ( 𝑛 ∈ ω ∧ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ⊆ ( fi ‘ 𝐴 ) ) → ( ∀ 𝑦 ∈ 𝑛 ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) → ∀ 𝑦 ∈ 𝑛 ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ suc 𝑛 ) ) ) |
107 |
|
vex |
⊢ 𝑛 ∈ V |
108 |
|
fveq2 |
⊢ ( 𝑦 = 𝑛 → ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) = ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ) |
109 |
108
|
sseq1d |
⊢ ( 𝑦 = 𝑛 → ( ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ suc 𝑛 ) ↔ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ suc 𝑛 ) ) ) |
110 |
107 109
|
ralsn |
⊢ ( ∀ 𝑦 ∈ { 𝑛 } ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ suc 𝑛 ) ↔ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ suc 𝑛 ) ) |
111 |
103 110
|
sylibr |
⊢ ( ( 𝑛 ∈ ω ∧ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ⊆ ( fi ‘ 𝐴 ) ) → ∀ 𝑦 ∈ { 𝑛 } ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ suc 𝑛 ) ) |
112 |
106 111
|
jctird |
⊢ ( ( 𝑛 ∈ ω ∧ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ⊆ ( fi ‘ 𝐴 ) ) → ( ∀ 𝑦 ∈ 𝑛 ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) → ( ∀ 𝑦 ∈ 𝑛 ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ suc 𝑛 ) ∧ ∀ 𝑦 ∈ { 𝑛 } ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ suc 𝑛 ) ) ) ) |
113 |
|
df-suc |
⊢ suc 𝑛 = ( 𝑛 ∪ { 𝑛 } ) |
114 |
113
|
raleqi |
⊢ ( ∀ 𝑦 ∈ suc 𝑛 ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ suc 𝑛 ) ↔ ∀ 𝑦 ∈ ( 𝑛 ∪ { 𝑛 } ) ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ suc 𝑛 ) ) |
115 |
|
ralunb |
⊢ ( ∀ 𝑦 ∈ ( 𝑛 ∪ { 𝑛 } ) ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ suc 𝑛 ) ↔ ( ∀ 𝑦 ∈ 𝑛 ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ suc 𝑛 ) ∧ ∀ 𝑦 ∈ { 𝑛 } ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ suc 𝑛 ) ) ) |
116 |
114 115
|
bitri |
⊢ ( ∀ 𝑦 ∈ suc 𝑛 ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ suc 𝑛 ) ↔ ( ∀ 𝑦 ∈ 𝑛 ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ suc 𝑛 ) ∧ ∀ 𝑦 ∈ { 𝑛 } ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ suc 𝑛 ) ) ) |
117 |
112 116
|
syl6ibr |
⊢ ( ( 𝑛 ∈ ω ∧ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ⊆ ( fi ‘ 𝐴 ) ) → ( ∀ 𝑦 ∈ 𝑛 ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) → ∀ 𝑦 ∈ suc 𝑛 ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ suc 𝑛 ) ) ) |
118 |
|
fiin |
⊢ ( ( 𝑎 ∈ ( fi ‘ 𝐴 ) ∧ 𝑏 ∈ ( fi ‘ 𝐴 ) ) → ( 𝑎 ∩ 𝑏 ) ∈ ( fi ‘ 𝐴 ) ) |
119 |
118
|
rgen2 |
⊢ ∀ 𝑎 ∈ ( fi ‘ 𝐴 ) ∀ 𝑏 ∈ ( fi ‘ 𝐴 ) ( 𝑎 ∩ 𝑏 ) ∈ ( fi ‘ 𝐴 ) |
120 |
|
ss2ralv |
⊢ ( ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ⊆ ( fi ‘ 𝐴 ) → ( ∀ 𝑎 ∈ ( fi ‘ 𝐴 ) ∀ 𝑏 ∈ ( fi ‘ 𝐴 ) ( 𝑎 ∩ 𝑏 ) ∈ ( fi ‘ 𝐴 ) → ∀ 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ∀ 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ( 𝑎 ∩ 𝑏 ) ∈ ( fi ‘ 𝐴 ) ) ) |
121 |
119 120
|
mpi |
⊢ ( ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ⊆ ( fi ‘ 𝐴 ) → ∀ 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ∀ 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ( 𝑎 ∩ 𝑏 ) ∈ ( fi ‘ 𝐴 ) ) |
122 |
60
|
fmpo |
⊢ ( ∀ 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ∀ 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ( 𝑎 ∩ 𝑏 ) ∈ ( fi ‘ 𝐴 ) ↔ ( 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) , 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ↦ ( 𝑎 ∩ 𝑏 ) ) : ( ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) × ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ) ⟶ ( fi ‘ 𝐴 ) ) |
123 |
121 122
|
sylib |
⊢ ( ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ⊆ ( fi ‘ 𝐴 ) → ( 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) , 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ↦ ( 𝑎 ∩ 𝑏 ) ) : ( ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) × ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ) ⟶ ( fi ‘ 𝐴 ) ) |
124 |
123
|
frnd |
⊢ ( ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ⊆ ( fi ‘ 𝐴 ) → ran ( 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) , 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ↦ ( 𝑎 ∩ 𝑏 ) ) ⊆ ( fi ‘ 𝐴 ) ) |
125 |
124
|
adantl |
⊢ ( ( 𝑛 ∈ ω ∧ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ⊆ ( fi ‘ 𝐴 ) ) → ran ( 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) , 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ↦ ( 𝑎 ∩ 𝑏 ) ) ⊆ ( fi ‘ 𝐴 ) ) |
126 |
102 125
|
eqsstrd |
⊢ ( ( 𝑛 ∈ ω ∧ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ⊆ ( fi ‘ 𝐴 ) ) → ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ suc 𝑛 ) ⊆ ( fi ‘ 𝐴 ) ) |
127 |
117 126
|
jctild |
⊢ ( ( 𝑛 ∈ ω ∧ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ⊆ ( fi ‘ 𝐴 ) ) → ( ∀ 𝑦 ∈ 𝑛 ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) → ( ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ suc 𝑛 ) ⊆ ( fi ‘ 𝐴 ) ∧ ∀ 𝑦 ∈ suc 𝑛 ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ suc 𝑛 ) ) ) ) |
128 |
127
|
expimpd |
⊢ ( 𝑛 ∈ ω → ( ( ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ⊆ ( fi ‘ 𝐴 ) ∧ ∀ 𝑦 ∈ 𝑛 ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ) → ( ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ suc 𝑛 ) ⊆ ( fi ‘ 𝐴 ) ∧ ∀ 𝑦 ∈ suc 𝑛 ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ suc 𝑛 ) ) ) ) |
129 |
128
|
a1d |
⊢ ( 𝑛 ∈ ω → ( 𝐴 ∈ 𝑉 → ( ( ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ⊆ ( fi ‘ 𝐴 ) ∧ ∀ 𝑦 ∈ 𝑛 ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ) → ( ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ suc 𝑛 ) ⊆ ( fi ‘ 𝐴 ) ∧ ∀ 𝑦 ∈ suc 𝑛 ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ suc 𝑛 ) ) ) ) ) |
130 |
37 42 47 49 129
|
finds2 |
⊢ ( 𝑥 ∈ ω → ( 𝐴 ∈ 𝑉 → ( ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑥 ) ⊆ ( fi ‘ 𝐴 ) ∧ ∀ 𝑦 ∈ 𝑥 ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑥 ) ) ) ) |
131 |
130
|
impcom |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑥 ∈ ω ) → ( ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑥 ) ⊆ ( fi ‘ 𝐴 ) ∧ ∀ 𝑦 ∈ 𝑥 ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑥 ) ) ) |
132 |
131
|
simprd |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑥 ∈ ω ) → ∀ 𝑦 ∈ 𝑥 ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑥 ) ) |
133 |
132
|
r19.21bi |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑥 ∈ ω ) ∧ 𝑦 ∈ 𝑥 ) → ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑥 ) ) |
134 |
133
|
ex |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑥 ∈ ω ) → ( 𝑦 ∈ 𝑥 → ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑥 ) ) ) |
135 |
134
|
adantr |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑥 ∈ ω ) ∧ 𝑦 ∈ ω ) → ( 𝑦 ∈ 𝑥 → ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑥 ) ) ) |
136 |
|
fveq2 |
⊢ ( 𝑦 = 𝑥 → ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) = ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑥 ) ) |
137 |
|
eqimss |
⊢ ( ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) = ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑥 ) → ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑥 ) ) |
138 |
136 137
|
syl |
⊢ ( 𝑦 = 𝑥 → ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑥 ) ) |
139 |
138
|
a1i |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑥 ∈ ω ) ∧ 𝑦 ∈ ω ) → ( 𝑦 = 𝑥 → ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑥 ) ) ) |
140 |
135 139
|
jaod |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑥 ∈ ω ) ∧ 𝑦 ∈ ω ) → ( ( 𝑦 ∈ 𝑥 ∨ 𝑦 = 𝑥 ) → ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑥 ) ) ) |
141 |
32 140
|
sylbid |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑥 ∈ ω ) ∧ 𝑦 ∈ ω ) → ( 𝑦 ⊆ 𝑥 → ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑥 ) ) ) |
142 |
141
|
ralrimiva |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑥 ∈ ω ) → ∀ 𝑦 ∈ ω ( 𝑦 ⊆ 𝑥 → ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑥 ) ) ) |
143 |
142
|
ralrimiva |
⊢ ( 𝐴 ∈ 𝑉 → ∀ 𝑥 ∈ ω ∀ 𝑦 ∈ ω ( 𝑦 ⊆ 𝑥 → ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑥 ) ) ) |
144 |
143
|
adantr |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑚 ∈ ω ∧ 𝑛 ∈ ω ) ) → ∀ 𝑥 ∈ ω ∀ 𝑦 ∈ ω ( 𝑦 ⊆ 𝑥 → ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑥 ) ) ) |
145 |
|
ssun1 |
⊢ 𝑚 ⊆ ( 𝑚 ∪ 𝑛 ) |
146 |
145
|
a1i |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑚 ∈ ω ∧ 𝑛 ∈ ω ) ) → 𝑚 ⊆ ( 𝑚 ∪ 𝑛 ) ) |
147 |
|
sseq2 |
⊢ ( 𝑥 = ( 𝑚 ∪ 𝑛 ) → ( 𝑦 ⊆ 𝑥 ↔ 𝑦 ⊆ ( 𝑚 ∪ 𝑛 ) ) ) |
148 |
|
fveq2 |
⊢ ( 𝑥 = ( 𝑚 ∪ 𝑛 ) → ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑥 ) = ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) ) |
149 |
148
|
sseq2d |
⊢ ( 𝑥 = ( 𝑚 ∪ 𝑛 ) → ( ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑥 ) ↔ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) ) ) |
150 |
147 149
|
imbi12d |
⊢ ( 𝑥 = ( 𝑚 ∪ 𝑛 ) → ( ( 𝑦 ⊆ 𝑥 → ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑥 ) ) ↔ ( 𝑦 ⊆ ( 𝑚 ∪ 𝑛 ) → ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) ) ) ) |
151 |
|
sseq1 |
⊢ ( 𝑦 = 𝑚 → ( 𝑦 ⊆ ( 𝑚 ∪ 𝑛 ) ↔ 𝑚 ⊆ ( 𝑚 ∪ 𝑛 ) ) ) |
152 |
|
fveq2 |
⊢ ( 𝑦 = 𝑚 → ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) = ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑚 ) ) |
153 |
152
|
sseq1d |
⊢ ( 𝑦 = 𝑚 → ( ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) ↔ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑚 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) ) ) |
154 |
151 153
|
imbi12d |
⊢ ( 𝑦 = 𝑚 → ( ( 𝑦 ⊆ ( 𝑚 ∪ 𝑛 ) → ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) ) ↔ ( 𝑚 ⊆ ( 𝑚 ∪ 𝑛 ) → ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑚 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) ) ) ) |
155 |
150 154
|
rspc2v |
⊢ ( ( ( 𝑚 ∪ 𝑛 ) ∈ ω ∧ 𝑚 ∈ ω ) → ( ∀ 𝑥 ∈ ω ∀ 𝑦 ∈ ω ( 𝑦 ⊆ 𝑥 → ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑥 ) ) → ( 𝑚 ⊆ ( 𝑚 ∪ 𝑛 ) → ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑚 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) ) ) ) |
156 |
27 144 146 155
|
syl3c |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑚 ∈ ω ∧ 𝑛 ∈ ω ) ) → ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑚 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) ) |
157 |
156
|
sseld |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑚 ∈ ω ∧ 𝑛 ∈ ω ) ) → ( 𝑐 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑚 ) → 𝑐 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) ) ) |
158 |
|
simprr |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑚 ∈ ω ∧ 𝑛 ∈ ω ) ) → 𝑛 ∈ ω ) |
159 |
25 158
|
jca |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑚 ∈ ω ∧ 𝑛 ∈ ω ) ) → ( ( 𝑚 ∪ 𝑛 ) ∈ ω ∧ 𝑛 ∈ ω ) ) |
160 |
|
ssun2 |
⊢ 𝑛 ⊆ ( 𝑚 ∪ 𝑛 ) |
161 |
160
|
a1i |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑚 ∈ ω ∧ 𝑛 ∈ ω ) ) → 𝑛 ⊆ ( 𝑚 ∪ 𝑛 ) ) |
162 |
|
sseq1 |
⊢ ( 𝑦 = 𝑛 → ( 𝑦 ⊆ ( 𝑚 ∪ 𝑛 ) ↔ 𝑛 ⊆ ( 𝑚 ∪ 𝑛 ) ) ) |
163 |
108
|
sseq1d |
⊢ ( 𝑦 = 𝑛 → ( ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) ↔ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) ) ) |
164 |
162 163
|
imbi12d |
⊢ ( 𝑦 = 𝑛 → ( ( 𝑦 ⊆ ( 𝑚 ∪ 𝑛 ) → ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) ) ↔ ( 𝑛 ⊆ ( 𝑚 ∪ 𝑛 ) → ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) ) ) ) |
165 |
150 164
|
rspc2v |
⊢ ( ( ( 𝑚 ∪ 𝑛 ) ∈ ω ∧ 𝑛 ∈ ω ) → ( ∀ 𝑥 ∈ ω ∀ 𝑦 ∈ ω ( 𝑦 ⊆ 𝑥 → ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑦 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑥 ) ) → ( 𝑛 ⊆ ( 𝑚 ∪ 𝑛 ) → ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) ) ) ) |
166 |
159 144 161 165
|
syl3c |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑚 ∈ ω ∧ 𝑛 ∈ ω ) ) → ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ⊆ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) ) |
167 |
166
|
sseld |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑚 ∈ ω ∧ 𝑛 ∈ ω ) ) → ( 𝑑 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) → 𝑑 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) ) ) |
168 |
24
|
ad2antlr |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑚 ∈ ω ∧ 𝑛 ∈ ω ) ) ∧ ( 𝑐 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) ∧ 𝑑 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) ) ) → ( 𝑚 ∪ 𝑛 ) ∈ ω ) |
169 |
|
peano2 |
⊢ ( ( 𝑚 ∪ 𝑛 ) ∈ ω → suc ( 𝑚 ∪ 𝑛 ) ∈ ω ) |
170 |
|
fveq2 |
⊢ ( 𝑥 = suc ( 𝑚 ∪ 𝑛 ) → ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑥 ) = ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ suc ( 𝑚 ∪ 𝑛 ) ) ) |
171 |
170
|
ssiun2s |
⊢ ( suc ( 𝑚 ∪ 𝑛 ) ∈ ω → ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ suc ( 𝑚 ∪ 𝑛 ) ) ⊆ ∪ 𝑥 ∈ ω ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑥 ) ) |
172 |
168 169 171
|
3syl |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑚 ∈ ω ∧ 𝑛 ∈ ω ) ) ∧ ( 𝑐 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) ∧ 𝑑 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) ) ) → ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ suc ( 𝑚 ∪ 𝑛 ) ) ⊆ ∪ 𝑥 ∈ ω ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑥 ) ) |
173 |
|
simprl |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑚 ∈ ω ∧ 𝑛 ∈ ω ) ) ∧ ( 𝑐 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) ∧ 𝑑 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) ) ) → 𝑐 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) ) |
174 |
|
simprr |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑚 ∈ ω ∧ 𝑛 ∈ ω ) ) ∧ ( 𝑐 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) ∧ 𝑑 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) ) ) → 𝑑 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) ) |
175 |
|
eqidd |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑚 ∈ ω ∧ 𝑛 ∈ ω ) ) ∧ ( 𝑐 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) ∧ 𝑑 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) ) ) → ( 𝑐 ∩ 𝑑 ) = ( 𝑐 ∩ 𝑑 ) ) |
176 |
|
ineq1 |
⊢ ( 𝑎 = 𝑐 → ( 𝑎 ∩ 𝑏 ) = ( 𝑐 ∩ 𝑏 ) ) |
177 |
176
|
eqeq2d |
⊢ ( 𝑎 = 𝑐 → ( ( 𝑐 ∩ 𝑑 ) = ( 𝑎 ∩ 𝑏 ) ↔ ( 𝑐 ∩ 𝑑 ) = ( 𝑐 ∩ 𝑏 ) ) ) |
178 |
|
ineq2 |
⊢ ( 𝑏 = 𝑑 → ( 𝑐 ∩ 𝑏 ) = ( 𝑐 ∩ 𝑑 ) ) |
179 |
178
|
eqeq2d |
⊢ ( 𝑏 = 𝑑 → ( ( 𝑐 ∩ 𝑑 ) = ( 𝑐 ∩ 𝑏 ) ↔ ( 𝑐 ∩ 𝑑 ) = ( 𝑐 ∩ 𝑑 ) ) ) |
180 |
177 179
|
rspc2ev |
⊢ ( ( 𝑐 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) ∧ 𝑑 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) ∧ ( 𝑐 ∩ 𝑑 ) = ( 𝑐 ∩ 𝑑 ) ) → ∃ 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) ∃ 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) ( 𝑐 ∩ 𝑑 ) = ( 𝑎 ∩ 𝑏 ) ) |
181 |
173 174 175 180
|
syl3anc |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑚 ∈ ω ∧ 𝑛 ∈ ω ) ) ∧ ( 𝑐 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) ∧ 𝑑 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) ) ) → ∃ 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) ∃ 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) ( 𝑐 ∩ 𝑑 ) = ( 𝑎 ∩ 𝑏 ) ) |
182 |
|
vex |
⊢ 𝑐 ∈ V |
183 |
182
|
inex1 |
⊢ ( 𝑐 ∩ 𝑑 ) ∈ V |
184 |
|
eqeq1 |
⊢ ( 𝑥 = ( 𝑐 ∩ 𝑑 ) → ( 𝑥 = ( 𝑎 ∩ 𝑏 ) ↔ ( 𝑐 ∩ 𝑑 ) = ( 𝑎 ∩ 𝑏 ) ) ) |
185 |
184
|
2rexbidv |
⊢ ( 𝑥 = ( 𝑐 ∩ 𝑑 ) → ( ∃ 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) ∃ 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) 𝑥 = ( 𝑎 ∩ 𝑏 ) ↔ ∃ 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) ∃ 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) ( 𝑐 ∩ 𝑑 ) = ( 𝑎 ∩ 𝑏 ) ) ) |
186 |
183 185
|
elab |
⊢ ( ( 𝑐 ∩ 𝑑 ) ∈ { 𝑥 ∣ ∃ 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) ∃ 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) 𝑥 = ( 𝑎 ∩ 𝑏 ) } ↔ ∃ 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) ∃ 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) ( 𝑐 ∩ 𝑑 ) = ( 𝑎 ∩ 𝑏 ) ) |
187 |
181 186
|
sylibr |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑚 ∈ ω ∧ 𝑛 ∈ ω ) ) ∧ ( 𝑐 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) ∧ 𝑑 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) ) ) → ( 𝑐 ∩ 𝑑 ) ∈ { 𝑥 ∣ ∃ 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) ∃ 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) 𝑥 = ( 𝑎 ∩ 𝑏 ) } ) |
188 |
|
eqid |
⊢ ( 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) , 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) ↦ ( 𝑎 ∩ 𝑏 ) ) = ( 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) , 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) ↦ ( 𝑎 ∩ 𝑏 ) ) |
189 |
188
|
rnmpo |
⊢ ran ( 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) , 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) ↦ ( 𝑎 ∩ 𝑏 ) ) = { 𝑥 ∣ ∃ 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) ∃ 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) 𝑥 = ( 𝑎 ∩ 𝑏 ) } |
190 |
187 189
|
eleqtrrdi |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑚 ∈ ω ∧ 𝑛 ∈ ω ) ) ∧ ( 𝑐 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) ∧ 𝑑 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) ) ) → ( 𝑐 ∩ 𝑑 ) ∈ ran ( 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) , 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) ↦ ( 𝑎 ∩ 𝑏 ) ) ) |
191 |
|
fvex |
⊢ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) ∈ V |
192 |
191
|
uniex |
⊢ ∪ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) ∈ V |
193 |
192
|
pwex |
⊢ 𝒫 ∪ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) ∈ V |
194 |
|
elssuni |
⊢ ( 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) → 𝑎 ⊆ ∪ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) ) |
195 |
69 194
|
sstrid |
⊢ ( 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) → ( 𝑎 ∩ 𝑏 ) ⊆ ∪ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) ) |
196 |
74
|
elpw |
⊢ ( ( 𝑎 ∩ 𝑏 ) ∈ 𝒫 ∪ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) ↔ ( 𝑎 ∩ 𝑏 ) ⊆ ∪ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) ) |
197 |
195 196
|
sylibr |
⊢ ( 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) → ( 𝑎 ∩ 𝑏 ) ∈ 𝒫 ∪ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) ) |
198 |
197
|
adantr |
⊢ ( ( 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) ∧ 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) ) → ( 𝑎 ∩ 𝑏 ) ∈ 𝒫 ∪ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) ) |
199 |
198
|
rgen2 |
⊢ ∀ 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) ∀ 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) ( 𝑎 ∩ 𝑏 ) ∈ 𝒫 ∪ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) |
200 |
188
|
fmpo |
⊢ ( ∀ 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) ∀ 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) ( 𝑎 ∩ 𝑏 ) ∈ 𝒫 ∪ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) ↔ ( 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) , 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) ↦ ( 𝑎 ∩ 𝑏 ) ) : ( ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) × ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) ) ⟶ 𝒫 ∪ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) ) |
201 |
199 200
|
mpbi |
⊢ ( 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) , 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) ↦ ( 𝑎 ∩ 𝑏 ) ) : ( ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) × ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) ) ⟶ 𝒫 ∪ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) |
202 |
|
frn |
⊢ ( ( 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) , 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) ↦ ( 𝑎 ∩ 𝑏 ) ) : ( ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) × ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) ) ⟶ 𝒫 ∪ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) → ran ( 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) , 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) ↦ ( 𝑎 ∩ 𝑏 ) ) ⊆ 𝒫 ∪ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) ) |
203 |
201 202
|
ax-mp |
⊢ ran ( 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) , 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) ↦ ( 𝑎 ∩ 𝑏 ) ) ⊆ 𝒫 ∪ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) |
204 |
193 203
|
ssexi |
⊢ ran ( 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) , 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) ↦ ( 𝑎 ∩ 𝑏 ) ) ∈ V |
205 |
|
nfcv |
⊢ Ⅎ 𝑣 ( 𝑚 ∪ 𝑛 ) |
206 |
|
nfcv |
⊢ Ⅎ 𝑣 ran ( 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) , 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) ↦ ( 𝑎 ∩ 𝑏 ) ) |
207 |
|
mpoeq12 |
⊢ ( ( 𝑣 = ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) ∧ 𝑣 = ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) ) → ( 𝑎 ∈ 𝑣 , 𝑏 ∈ 𝑣 ↦ ( 𝑎 ∩ 𝑏 ) ) = ( 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) , 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) ↦ ( 𝑎 ∩ 𝑏 ) ) ) |
208 |
207
|
anidms |
⊢ ( 𝑣 = ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) → ( 𝑎 ∈ 𝑣 , 𝑏 ∈ 𝑣 ↦ ( 𝑎 ∩ 𝑏 ) ) = ( 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) , 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) ↦ ( 𝑎 ∩ 𝑏 ) ) ) |
209 |
208
|
rneqd |
⊢ ( 𝑣 = ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) → ran ( 𝑎 ∈ 𝑣 , 𝑏 ∈ 𝑣 ↦ ( 𝑎 ∩ 𝑏 ) ) = ran ( 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) , 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) ↦ ( 𝑎 ∩ 𝑏 ) ) ) |
210 |
83 205 206 97 209
|
frsucmpt |
⊢ ( ( ( 𝑚 ∪ 𝑛 ) ∈ ω ∧ ran ( 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) , 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) ↦ ( 𝑎 ∩ 𝑏 ) ) ∈ V ) → ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ suc ( 𝑚 ∪ 𝑛 ) ) = ran ( 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) , 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) ↦ ( 𝑎 ∩ 𝑏 ) ) ) |
211 |
168 204 210
|
sylancl |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑚 ∈ ω ∧ 𝑛 ∈ ω ) ) ∧ ( 𝑐 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) ∧ 𝑑 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) ) ) → ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ suc ( 𝑚 ∪ 𝑛 ) ) = ran ( 𝑎 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) , 𝑏 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) ↦ ( 𝑎 ∩ 𝑏 ) ) ) |
212 |
190 211
|
eleqtrrd |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑚 ∈ ω ∧ 𝑛 ∈ ω ) ) ∧ ( 𝑐 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) ∧ 𝑑 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) ) ) → ( 𝑐 ∩ 𝑑 ) ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ suc ( 𝑚 ∪ 𝑛 ) ) ) |
213 |
172 212
|
sseldd |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑚 ∈ ω ∧ 𝑛 ∈ ω ) ) ∧ ( 𝑐 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) ∧ 𝑑 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) ) ) → ( 𝑐 ∩ 𝑑 ) ∈ ∪ 𝑥 ∈ ω ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑥 ) ) |
214 |
|
fniunfv |
⊢ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) Fn ω → ∪ 𝑥 ∈ ω ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑥 ) = ∪ ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ) |
215 |
4 214
|
ax-mp |
⊢ ∪ 𝑥 ∈ ω ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑥 ) = ∪ ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) |
216 |
213 215
|
eleqtrdi |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑚 ∈ ω ∧ 𝑛 ∈ ω ) ) ∧ ( 𝑐 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) ∧ 𝑑 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) ) ) → ( 𝑐 ∩ 𝑑 ) ∈ ∪ ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ) |
217 |
216
|
ex |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑚 ∈ ω ∧ 𝑛 ∈ ω ) ) → ( ( 𝑐 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) ∧ 𝑑 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ ( 𝑚 ∪ 𝑛 ) ) ) → ( 𝑐 ∩ 𝑑 ) ∈ ∪ ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ) ) |
218 |
157 167 217
|
syl2and |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑚 ∈ ω ∧ 𝑛 ∈ ω ) ) → ( ( 𝑐 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑚 ) ∧ 𝑑 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ) → ( 𝑐 ∩ 𝑑 ) ∈ ∪ ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ) ) |
219 |
218
|
rexlimdvva |
⊢ ( 𝐴 ∈ 𝑉 → ( ∃ 𝑚 ∈ ω ∃ 𝑛 ∈ ω ( 𝑐 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑚 ) ∧ 𝑑 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ) → ( 𝑐 ∩ 𝑑 ) ∈ ∪ ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ) ) |
220 |
219
|
imp |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∃ 𝑚 ∈ ω ∃ 𝑛 ∈ ω ( 𝑐 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑚 ) ∧ 𝑑 ∈ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑛 ) ) ) → ( 𝑐 ∩ 𝑑 ) ∈ ∪ ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ) |
221 |
21 220
|
sylan2br |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑐 ∈ ∪ ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ∧ 𝑑 ∈ ∪ ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ) ) → ( 𝑐 ∩ 𝑑 ) ∈ ∪ ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ) |
222 |
221
|
ralrimivva |
⊢ ( 𝐴 ∈ 𝑉 → ∀ 𝑐 ∈ ∪ ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ∀ 𝑑 ∈ ∪ ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ( 𝑐 ∩ 𝑑 ) ∈ ∪ ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ) |
223 |
131
|
simpld |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑥 ∈ ω ) → ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑥 ) ⊆ ( fi ‘ 𝐴 ) ) |
224 |
|
fvex |
⊢ ( fi ‘ 𝐴 ) ∈ V |
225 |
224
|
elpw2 |
⊢ ( ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑥 ) ∈ 𝒫 ( fi ‘ 𝐴 ) ↔ ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑥 ) ⊆ ( fi ‘ 𝐴 ) ) |
226 |
223 225
|
sylibr |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑥 ∈ ω ) → ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑥 ) ∈ 𝒫 ( fi ‘ 𝐴 ) ) |
227 |
226
|
ralrimiva |
⊢ ( 𝐴 ∈ 𝑉 → ∀ 𝑥 ∈ ω ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑥 ) ∈ 𝒫 ( fi ‘ 𝐴 ) ) |
228 |
|
fnfvrnss |
⊢ ( ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) Fn ω ∧ ∀ 𝑥 ∈ ω ( ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ‘ 𝑥 ) ∈ 𝒫 ( fi ‘ 𝐴 ) ) → ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ⊆ 𝒫 ( fi ‘ 𝐴 ) ) |
229 |
4 227 228
|
sylancr |
⊢ ( 𝐴 ∈ 𝑉 → ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ⊆ 𝒫 ( fi ‘ 𝐴 ) ) |
230 |
|
sspwuni |
⊢ ( ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ⊆ 𝒫 ( fi ‘ 𝐴 ) ↔ ∪ ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ⊆ ( fi ‘ 𝐴 ) ) |
231 |
229 230
|
sylib |
⊢ ( 𝐴 ∈ 𝑉 → ∪ ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ⊆ ( fi ‘ 𝐴 ) ) |
232 |
|
ssexg |
⊢ ( ( ∪ ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ⊆ ( fi ‘ 𝐴 ) ∧ ( fi ‘ 𝐴 ) ∈ V ) → ∪ ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ∈ V ) |
233 |
231 224 232
|
sylancl |
⊢ ( 𝐴 ∈ 𝑉 → ∪ ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ∈ V ) |
234 |
|
sseq2 |
⊢ ( 𝑥 = ∪ ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) → ( 𝐴 ⊆ 𝑥 ↔ 𝐴 ⊆ ∪ ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ) ) |
235 |
|
eleq2 |
⊢ ( 𝑥 = ∪ ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) → ( ( 𝑐 ∩ 𝑑 ) ∈ 𝑥 ↔ ( 𝑐 ∩ 𝑑 ) ∈ ∪ ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ) ) |
236 |
235
|
raleqbi1dv |
⊢ ( 𝑥 = ∪ ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) → ( ∀ 𝑑 ∈ 𝑥 ( 𝑐 ∩ 𝑑 ) ∈ 𝑥 ↔ ∀ 𝑑 ∈ ∪ ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ( 𝑐 ∩ 𝑑 ) ∈ ∪ ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ) ) |
237 |
236
|
raleqbi1dv |
⊢ ( 𝑥 = ∪ ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) → ( ∀ 𝑐 ∈ 𝑥 ∀ 𝑑 ∈ 𝑥 ( 𝑐 ∩ 𝑑 ) ∈ 𝑥 ↔ ∀ 𝑐 ∈ ∪ ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ∀ 𝑑 ∈ ∪ ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ( 𝑐 ∩ 𝑑 ) ∈ ∪ ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ) ) |
238 |
234 237
|
anbi12d |
⊢ ( 𝑥 = ∪ ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) → ( ( 𝐴 ⊆ 𝑥 ∧ ∀ 𝑐 ∈ 𝑥 ∀ 𝑑 ∈ 𝑥 ( 𝑐 ∩ 𝑑 ) ∈ 𝑥 ) ↔ ( 𝐴 ⊆ ∪ ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ∧ ∀ 𝑐 ∈ ∪ ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ∀ 𝑑 ∈ ∪ ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ( 𝑐 ∩ 𝑑 ) ∈ ∪ ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ) ) ) |
239 |
238
|
elabg |
⊢ ( ∪ ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ∈ V → ( ∪ ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ∈ { 𝑥 ∣ ( 𝐴 ⊆ 𝑥 ∧ ∀ 𝑐 ∈ 𝑥 ∀ 𝑑 ∈ 𝑥 ( 𝑐 ∩ 𝑑 ) ∈ 𝑥 ) } ↔ ( 𝐴 ⊆ ∪ ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ∧ ∀ 𝑐 ∈ ∪ ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ∀ 𝑑 ∈ ∪ ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ( 𝑐 ∩ 𝑑 ) ∈ ∪ ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ) ) ) |
240 |
233 239
|
syl |
⊢ ( 𝐴 ∈ 𝑉 → ( ∪ ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ∈ { 𝑥 ∣ ( 𝐴 ⊆ 𝑥 ∧ ∀ 𝑐 ∈ 𝑥 ∀ 𝑑 ∈ 𝑥 ( 𝑐 ∩ 𝑑 ) ∈ 𝑥 ) } ↔ ( 𝐴 ⊆ ∪ ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ∧ ∀ 𝑐 ∈ ∪ ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ∀ 𝑑 ∈ ∪ ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ( 𝑐 ∩ 𝑑 ) ∈ ∪ ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ) ) ) |
241 |
10 222 240
|
mpbir2and |
⊢ ( 𝐴 ∈ 𝑉 → ∪ ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ∈ { 𝑥 ∣ ( 𝐴 ⊆ 𝑥 ∧ ∀ 𝑐 ∈ 𝑥 ∀ 𝑑 ∈ 𝑥 ( 𝑐 ∩ 𝑑 ) ∈ 𝑥 ) } ) |
242 |
|
intss1 |
⊢ ( ∪ ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ∈ { 𝑥 ∣ ( 𝐴 ⊆ 𝑥 ∧ ∀ 𝑐 ∈ 𝑥 ∀ 𝑑 ∈ 𝑥 ( 𝑐 ∩ 𝑑 ) ∈ 𝑥 ) } → ∩ { 𝑥 ∣ ( 𝐴 ⊆ 𝑥 ∧ ∀ 𝑐 ∈ 𝑥 ∀ 𝑑 ∈ 𝑥 ( 𝑐 ∩ 𝑑 ) ∈ 𝑥 ) } ⊆ ∪ ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ) |
243 |
241 242
|
syl |
⊢ ( 𝐴 ∈ 𝑉 → ∩ { 𝑥 ∣ ( 𝐴 ⊆ 𝑥 ∧ ∀ 𝑐 ∈ 𝑥 ∀ 𝑑 ∈ 𝑥 ( 𝑐 ∩ 𝑑 ) ∈ 𝑥 ) } ⊆ ∪ ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ) |
244 |
2 243
|
eqsstrd |
⊢ ( 𝐴 ∈ 𝑉 → ( fi ‘ 𝐴 ) ⊆ ∪ ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ) |
245 |
244 231
|
eqssd |
⊢ ( 𝐴 ∈ 𝑉 → ( fi ‘ 𝐴 ) = ∪ ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) ) |
246 |
|
df-ima |
⊢ ( rec ( 𝑅 , 𝐴 ) “ ω ) = ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) |
247 |
246
|
unieqi |
⊢ ∪ ( rec ( 𝑅 , 𝐴 ) “ ω ) = ∪ ran ( rec ( 𝑅 , 𝐴 ) ↾ ω ) |
248 |
245 247
|
eqtr4di |
⊢ ( 𝐴 ∈ 𝑉 → ( fi ‘ 𝐴 ) = ∪ ( rec ( 𝑅 , 𝐴 ) “ ω ) ) |