| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | dffi2 9464 | . . . 4
⊢ (𝐴 ∈ 𝑉 → (fi‘𝐴) = ∩ {𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ ∀𝑐 ∈ 𝑥 ∀𝑑 ∈ 𝑥 (𝑐 ∩ 𝑑) ∈ 𝑥)}) | 
| 2 |  | fr0g 8477 | . . . . . . . 8
⊢ (𝐴 ∈ 𝑉 → ((rec(𝑅, 𝐴) ↾ ω)‘∅) = 𝐴) | 
| 3 |  | frfnom 8476 | . . . . . . . . 9
⊢
(rec(𝑅, 𝐴) ↾ ω) Fn
ω | 
| 4 |  | peano1 7911 | . . . . . . . . 9
⊢ ∅
∈ ω | 
| 5 |  | fnfvelrn 7099 | . . . . . . . . 9
⊢
(((rec(𝑅, 𝐴) ↾ ω) Fn ω
∧ ∅ ∈ ω) → ((rec(𝑅, 𝐴) ↾ ω)‘∅) ∈ ran
(rec(𝑅, 𝐴) ↾ ω)) | 
| 6 | 3, 4, 5 | mp2an 692 | . . . . . . . 8
⊢
((rec(𝑅, 𝐴) ↾
ω)‘∅) ∈ ran (rec(𝑅, 𝐴) ↾ ω) | 
| 7 | 2, 6 | eqeltrrdi 2849 | . . . . . . 7
⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ ran (rec(𝑅, 𝐴) ↾ ω)) | 
| 8 |  | elssuni 4936 | . . . . . . 7
⊢ (𝐴 ∈ ran (rec(𝑅, 𝐴) ↾ ω) → 𝐴 ⊆ ∪ ran
(rec(𝑅, 𝐴) ↾ ω)) | 
| 9 | 7, 8 | syl 17 | . . . . . 6
⊢ (𝐴 ∈ 𝑉 → 𝐴 ⊆ ∪ ran
(rec(𝑅, 𝐴) ↾ ω)) | 
| 10 |  | reeanv 3228 | . . . . . . . . 9
⊢
(∃𝑚 ∈
ω ∃𝑛 ∈
ω (𝑐 ∈
((rec(𝑅, 𝐴) ↾ ω)‘𝑚) ∧ 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)) ↔ (∃𝑚 ∈ ω 𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑚) ∧ ∃𝑛 ∈ ω 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛))) | 
| 11 |  | eliun 4994 | . . . . . . . . . 10
⊢ (𝑐 ∈ ∪ 𝑚 ∈ ω ((rec(𝑅, 𝐴) ↾ ω)‘𝑚) ↔ ∃𝑚 ∈ ω 𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑚)) | 
| 12 |  | eliun 4994 | . . . . . . . . . 10
⊢ (𝑑 ∈ ∪ 𝑛 ∈ ω ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↔ ∃𝑛 ∈ ω 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)) | 
| 13 | 11, 12 | anbi12i 628 | . . . . . . . . 9
⊢ ((𝑐 ∈ ∪ 𝑚 ∈ ω ((rec(𝑅, 𝐴) ↾ ω)‘𝑚) ∧ 𝑑 ∈ ∪
𝑛 ∈ ω
((rec(𝑅, 𝐴) ↾ ω)‘𝑛)) ↔ (∃𝑚 ∈ ω 𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑚) ∧ ∃𝑛 ∈ ω 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛))) | 
| 14 |  | fniunfv 7268 | . . . . . . . . . . . 12
⊢
((rec(𝑅, 𝐴) ↾ ω) Fn ω
→ ∪ 𝑚 ∈ ω ((rec(𝑅, 𝐴) ↾ ω)‘𝑚) = ∪ ran
(rec(𝑅, 𝐴) ↾ ω)) | 
| 15 | 14 | eleq2d 2826 | . . . . . . . . . . 11
⊢
((rec(𝑅, 𝐴) ↾ ω) Fn ω
→ (𝑐 ∈ ∪ 𝑚 ∈ ω ((rec(𝑅, 𝐴) ↾ ω)‘𝑚) ↔ 𝑐 ∈ ∪ ran
(rec(𝑅, 𝐴) ↾ ω))) | 
| 16 |  | fniunfv 7268 | . . . . . . . . . . . 12
⊢
((rec(𝑅, 𝐴) ↾ ω) Fn ω
→ ∪ 𝑛 ∈ ω ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) = ∪ ran
(rec(𝑅, 𝐴) ↾ ω)) | 
| 17 | 16 | eleq2d 2826 | . . . . . . . . . . 11
⊢
((rec(𝑅, 𝐴) ↾ ω) Fn ω
→ (𝑑 ∈ ∪ 𝑛 ∈ ω ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↔ 𝑑 ∈ ∪ ran
(rec(𝑅, 𝐴) ↾ ω))) | 
| 18 | 15, 17 | anbi12d 632 | . . . . . . . . . 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 299 | . . . . . . . 8
⊢
(∃𝑚 ∈
ω ∃𝑛 ∈
ω (𝑐 ∈
((rec(𝑅, 𝐴) ↾ ω)‘𝑚) ∧ 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)) ↔ (𝑐 ∈ ∪ ran
(rec(𝑅, 𝐴) ↾ ω) ∧ 𝑑 ∈ ∪ ran
(rec(𝑅, 𝐴) ↾ ω))) | 
| 21 |  | ordom 7898 | . . . . . . . . . . . . . . . 16
⊢ Ord
ω | 
| 22 |  | ordunel 7848 | . . . . . . . . . . . . . . . 16
⊢ ((Ord
ω ∧ 𝑚 ∈
ω ∧ 𝑛 ∈
ω) → (𝑚 ∪
𝑛) ∈
ω) | 
| 23 | 21, 22 | mp3an1 1449 | . . . . . . . . . . . . . . 15
⊢ ((𝑚 ∈ ω ∧ 𝑛 ∈ ω) → (𝑚 ∪ 𝑛) ∈ ω) | 
| 24 | 23 | adantl 481 | . . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) → (𝑚 ∪ 𝑛) ∈ ω) | 
| 25 |  | simprl 770 | . . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) → 𝑚 ∈ ω) | 
| 26 | 24, 25 | jca 511 | . . . . . . . . . . . . 13
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) → ((𝑚 ∪ 𝑛) ∈ ω ∧ 𝑚 ∈ ω)) | 
| 27 |  | nnon 7894 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ ω → 𝑦 ∈ On) | 
| 28 |  | nnon 7894 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ ω → 𝑥 ∈ On) | 
| 29 | 28 | ad2antlr 727 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ ω) ∧ 𝑦 ∈ ω) → 𝑥 ∈ On) | 
| 30 |  | onsseleq 6424 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∈ On ∧ 𝑥 ∈ On) → (𝑦 ⊆ 𝑥 ↔ (𝑦 ∈ 𝑥 ∨ 𝑦 = 𝑥))) | 
| 31 | 27, 29, 30 | syl2an2 686 | . . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ ω) ∧ 𝑦 ∈ ω) → (𝑦 ⊆ 𝑥 ↔ (𝑦 ∈ 𝑥 ∨ 𝑦 = 𝑥))) | 
| 32 |  | rzal 4508 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑥 = ∅ → ∀𝑦 ∈ 𝑥 ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥)) | 
| 33 | 32 | biantrud 531 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑥 = ∅ → (((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ⊆ (fi‘𝐴) ↔ (((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ⊆ (fi‘𝐴) ∧ ∀𝑦 ∈ 𝑥 ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥)))) | 
| 34 |  | fveq2 6905 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑥 = ∅ → ((rec(𝑅, 𝐴) ↾ ω)‘𝑥) = ((rec(𝑅, 𝐴) ↾
ω)‘∅)) | 
| 35 | 34 | sseq1d 4014 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑥 = ∅ → (((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ⊆ (fi‘𝐴) ↔ ((rec(𝑅, 𝐴) ↾ ω)‘∅) ⊆
(fi‘𝐴))) | 
| 36 | 33, 35 | bitr3d 281 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 = ∅ → ((((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ⊆ (fi‘𝐴) ∧ ∀𝑦 ∈ 𝑥 ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥)) ↔ ((rec(𝑅, 𝐴) ↾ ω)‘∅) ⊆
(fi‘𝐴))) | 
| 37 |  | fveq2 6905 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑥 = 𝑛 → ((rec(𝑅, 𝐴) ↾ ω)‘𝑥) = ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)) | 
| 38 | 37 | sseq1d 4014 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑥 = 𝑛 → (((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ⊆ (fi‘𝐴) ↔ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ (fi‘𝐴))) | 
| 39 | 37 | sseq2d 4015 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑥 = 𝑛 → (((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ↔ ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛))) | 
| 40 | 39 | raleqbi1dv 3337 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑥 = 𝑛 → (∀𝑦 ∈ 𝑥 ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ↔ ∀𝑦 ∈ 𝑛 ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛))) | 
| 41 | 38, 40 | anbi12d 632 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 = 𝑛 → ((((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ⊆ (fi‘𝐴) ∧ ∀𝑦 ∈ 𝑥 ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥)) ↔ (((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ (fi‘𝐴) ∧ ∀𝑦 ∈ 𝑛 ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)))) | 
| 42 |  | fveq2 6905 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑥 = suc 𝑛 → ((rec(𝑅, 𝐴) ↾ ω)‘𝑥) = ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛)) | 
| 43 | 42 | sseq1d 4014 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑥 = suc 𝑛 → (((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ⊆ (fi‘𝐴) ↔ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛) ⊆ (fi‘𝐴))) | 
| 44 | 42 | sseq2d 4015 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑥 = suc 𝑛 → (((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ↔ ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛))) | 
| 45 | 44 | raleqbi1dv 3337 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑥 = suc 𝑛 → (∀𝑦 ∈ 𝑥 ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ↔ ∀𝑦 ∈ suc 𝑛((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛))) | 
| 46 | 43, 45 | anbi12d 632 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 = suc 𝑛 → ((((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ⊆ (fi‘𝐴) ∧ ∀𝑦 ∈ 𝑥 ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥)) ↔ (((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛) ⊆ (fi‘𝐴) ∧ ∀𝑦 ∈ suc 𝑛((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛)))) | 
| 47 |  | ssfii 9460 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝐴 ∈ 𝑉 → 𝐴 ⊆ (fi‘𝐴)) | 
| 48 | 2, 47 | eqsstrd 4017 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝐴 ∈ 𝑉 → ((rec(𝑅, 𝐴) ↾ ω)‘∅) ⊆
(fi‘𝐴)) | 
| 49 |  | id 22 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑥 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) → 𝑥 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)) | 
| 50 |  | eqidd 2737 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑥 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) → 𝑥 = 𝑥) | 
| 51 |  | ineq1 4212 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝑎 = 𝑥 → (𝑎 ∩ 𝑏) = (𝑥 ∩ 𝑏)) | 
| 52 | 51 | eqeq2d 2747 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑎 = 𝑥 → (𝑥 = (𝑎 ∩ 𝑏) ↔ 𝑥 = (𝑥 ∩ 𝑏))) | 
| 53 |  | ineq2 4213 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (𝑏 = 𝑥 → (𝑥 ∩ 𝑏) = (𝑥 ∩ 𝑥)) | 
| 54 |  | inidm 4226 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (𝑥 ∩ 𝑥) = 𝑥 | 
| 55 | 53, 54 | eqtrdi 2792 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝑏 = 𝑥 → (𝑥 ∩ 𝑏) = 𝑥) | 
| 56 | 55 | eqeq2d 2747 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑏 = 𝑥 → (𝑥 = (𝑥 ∩ 𝑏) ↔ 𝑥 = 𝑥)) | 
| 57 | 52, 56 | rspc2ev 3634 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝑥 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ∧ 𝑥 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ∧ 𝑥 = 𝑥) → ∃𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)∃𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)𝑥 = (𝑎 ∩ 𝑏)) | 
| 58 | 49, 49, 50, 57 | syl3anc 1372 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑥 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) → ∃𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)∃𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)𝑥 = (𝑎 ∩ 𝑏)) | 
| 59 |  | eqid 2736 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎 ∩ 𝑏)) = (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎 ∩ 𝑏)) | 
| 60 | 59 | rnmpo 7567 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ran
(𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎 ∩ 𝑏)) = {𝑥 ∣ ∃𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)∃𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)𝑥 = (𝑎 ∩ 𝑏)} | 
| 61 | 60 | eqabri 2884 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑥 ∈ ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎 ∩ 𝑏)) ↔ ∃𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)∃𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)𝑥 = (𝑎 ∩ 𝑏)) | 
| 62 | 58, 61 | sylibr 234 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑥 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) → 𝑥 ∈ ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎 ∩ 𝑏))) | 
| 63 | 62 | ssriv 3986 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎 ∩ 𝑏)) | 
| 64 |  | simpl 482 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑛 ∈ ω ∧
((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ (fi‘𝐴)) → 𝑛 ∈ ω) | 
| 65 |  | fvex 6918 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢
((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ∈ V | 
| 66 | 65 | uniex 7762 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ∪ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ∈ V | 
| 67 | 66 | pwex 5379 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ 𝒫
∪ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ∈ V | 
| 68 |  | inss1 4236 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (𝑎 ∩ 𝑏) ⊆ 𝑎 | 
| 69 |  | elssuni 4936 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) → 𝑎 ⊆ ∪
((rec(𝑅, 𝐴) ↾ ω)‘𝑛)) | 
| 70 | 69 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ ((𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ∧ 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)) → 𝑎 ⊆ ∪
((rec(𝑅, 𝐴) ↾ ω)‘𝑛)) | 
| 71 | 68, 70 | sstrid 3994 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ∧ 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)) → (𝑎 ∩ 𝑏) ⊆ ∪
((rec(𝑅, 𝐴) ↾ ω)‘𝑛)) | 
| 72 |  | vex 3483 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ 𝑎 ∈ V | 
| 73 | 72 | inex1 5316 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (𝑎 ∩ 𝑏) ∈ V | 
| 74 | 73 | elpw 4603 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((𝑎 ∩ 𝑏) ∈ 𝒫 ∪ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↔ (𝑎 ∩ 𝑏) ⊆ ∪
((rec(𝑅, 𝐴) ↾ ω)‘𝑛)) | 
| 75 | 71, 74 | sylibr 234 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ∧ 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)) → (𝑎 ∩ 𝑏) ∈ 𝒫 ∪ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)) | 
| 76 | 75 | rgen2 3198 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢
∀𝑎 ∈
((rec(𝑅, 𝐴) ↾ ω)‘𝑛)∀𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)(𝑎 ∩ 𝑏) ∈ 𝒫 ∪ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) | 
| 77 | 59 | fmpo 8094 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢
(∀𝑎 ∈
((rec(𝑅, 𝐴) ↾ ω)‘𝑛)∀𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)(𝑎 ∩ 𝑏) ∈ 𝒫 ∪ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↔ (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎 ∩ 𝑏)):(((rec(𝑅, 𝐴) ↾ ω)‘𝑛) × ((rec(𝑅, 𝐴) ↾ ω)‘𝑛))⟶𝒫 ∪ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)) | 
| 78 | 76, 77 | mpbi 230 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎 ∩ 𝑏)):(((rec(𝑅, 𝐴) ↾ ω)‘𝑛) × ((rec(𝑅, 𝐴) ↾ ω)‘𝑛))⟶𝒫 ∪ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) | 
| 79 |  | frn 6742 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎 ∩ 𝑏)):(((rec(𝑅, 𝐴) ↾ ω)‘𝑛) × ((rec(𝑅, 𝐴) ↾ ω)‘𝑛))⟶𝒫 ∪ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) → ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎 ∩ 𝑏)) ⊆ 𝒫 ∪ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)) | 
| 80 | 78, 79 | ax-mp 5 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ran
(𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎 ∩ 𝑏)) ⊆ 𝒫 ∪ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) | 
| 81 | 67, 80 | ssexi 5321 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ran
(𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎 ∩ 𝑏)) ∈ V | 
| 82 |  | nfcv 2904 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
Ⅎ𝑣𝐴 | 
| 83 |  | nfcv 2904 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
Ⅎ𝑣𝑛 | 
| 84 |  | nfcv 2904 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
Ⅎ𝑣ran
(𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎 ∩ 𝑏)) | 
| 85 |  | dffi3.1 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ 𝑅 = (𝑢 ∈ V ↦ ran (𝑦 ∈ 𝑢, 𝑧 ∈ 𝑢 ↦ (𝑦 ∩ 𝑧))) | 
| 86 |  | mpoeq12 7507 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ ((𝑢 = 𝑣 ∧ 𝑢 = 𝑣) → (𝑦 ∈ 𝑢, 𝑧 ∈ 𝑢 ↦ (𝑦 ∩ 𝑧)) = (𝑦 ∈ 𝑣, 𝑧 ∈ 𝑣 ↦ (𝑦 ∩ 𝑧))) | 
| 87 | 86 | anidms 566 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (𝑢 = 𝑣 → (𝑦 ∈ 𝑢, 𝑧 ∈ 𝑢 ↦ (𝑦 ∩ 𝑧)) = (𝑦 ∈ 𝑣, 𝑧 ∈ 𝑣 ↦ (𝑦 ∩ 𝑧))) | 
| 88 |  | ineq1 4212 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (𝑦 = 𝑎 → (𝑦 ∩ 𝑧) = (𝑎 ∩ 𝑧)) | 
| 89 |  | ineq2 4213 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (𝑧 = 𝑏 → (𝑎 ∩ 𝑧) = (𝑎 ∩ 𝑏)) | 
| 90 | 88, 89 | cbvmpov 7529 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (𝑦 ∈ 𝑣, 𝑧 ∈ 𝑣 ↦ (𝑦 ∩ 𝑧)) = (𝑎 ∈ 𝑣, 𝑏 ∈ 𝑣 ↦ (𝑎 ∩ 𝑏)) | 
| 91 | 87, 90 | eqtrdi 2792 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (𝑢 = 𝑣 → (𝑦 ∈ 𝑢, 𝑧 ∈ 𝑢 ↦ (𝑦 ∩ 𝑧)) = (𝑎 ∈ 𝑣, 𝑏 ∈ 𝑣 ↦ (𝑎 ∩ 𝑏))) | 
| 92 | 91 | rneqd 5948 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (𝑢 = 𝑣 → ran (𝑦 ∈ 𝑢, 𝑧 ∈ 𝑢 ↦ (𝑦 ∩ 𝑧)) = ran (𝑎 ∈ 𝑣, 𝑏 ∈ 𝑣 ↦ (𝑎 ∩ 𝑏))) | 
| 93 | 92 | cbvmptv 5254 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝑢 ∈ V ↦ ran (𝑦 ∈ 𝑢, 𝑧 ∈ 𝑢 ↦ (𝑦 ∩ 𝑧))) = (𝑣 ∈ V ↦ ran (𝑎 ∈ 𝑣, 𝑏 ∈ 𝑣 ↦ (𝑎 ∩ 𝑏))) | 
| 94 | 85, 93 | eqtri 2764 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ 𝑅 = (𝑣 ∈ V ↦ ran (𝑎 ∈ 𝑣, 𝑏 ∈ 𝑣 ↦ (𝑎 ∩ 𝑏))) | 
| 95 |  | rdgeq1 8452 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑅 = (𝑣 ∈ V ↦ ran (𝑎 ∈ 𝑣, 𝑏 ∈ 𝑣 ↦ (𝑎 ∩ 𝑏))) → rec(𝑅, 𝐴) = rec((𝑣 ∈ V ↦ ran (𝑎 ∈ 𝑣, 𝑏 ∈ 𝑣 ↦ (𝑎 ∩ 𝑏))), 𝐴)) | 
| 96 | 94, 95 | ax-mp 5 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ rec(𝑅, 𝐴) = rec((𝑣 ∈ V ↦ ran (𝑎 ∈ 𝑣, 𝑏 ∈ 𝑣 ↦ (𝑎 ∩ 𝑏))), 𝐴) | 
| 97 | 96 | reseq1i 5992 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
(rec(𝑅, 𝐴) ↾ ω) = (rec((𝑣 ∈ V ↦ ran (𝑎 ∈ 𝑣, 𝑏 ∈ 𝑣 ↦ (𝑎 ∩ 𝑏))), 𝐴) ↾ ω) | 
| 98 |  | mpoeq12 7507 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝑣 = ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ∧ 𝑣 = ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)) → (𝑎 ∈ 𝑣, 𝑏 ∈ 𝑣 ↦ (𝑎 ∩ 𝑏)) = (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎 ∩ 𝑏))) | 
| 99 | 98 | anidms 566 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑣 = ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) → (𝑎 ∈ 𝑣, 𝑏 ∈ 𝑣 ↦ (𝑎 ∩ 𝑏)) = (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎 ∩ 𝑏))) | 
| 100 | 99 | rneqd 5948 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑣 = ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) → ran (𝑎 ∈ 𝑣, 𝑏 ∈ 𝑣 ↦ (𝑎 ∩ 𝑏)) = ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎 ∩ 𝑏))) | 
| 101 | 82, 83, 84, 97, 100 | frsucmpt 8479 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑛 ∈ ω ∧ ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎 ∩ 𝑏)) ∈ V) → ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛) = ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎 ∩ 𝑏))) | 
| 102 | 64, 81, 101 | sylancl 586 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑛 ∈ ω ∧
((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ (fi‘𝐴)) → ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛) = ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎 ∩ 𝑏))) | 
| 103 | 63, 102 | sseqtrrid 4026 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑛 ∈ ω ∧
((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ (fi‘𝐴)) → ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛)) | 
| 104 |  | sstr2 3989 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) → (((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛) → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛))) | 
| 105 | 103, 104 | syl5com 31 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑛 ∈ ω ∧
((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ (fi‘𝐴)) → (((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛))) | 
| 106 | 105 | ralimdv 3168 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑛 ∈ ω ∧
((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ (fi‘𝐴)) → (∀𝑦 ∈ 𝑛 ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) → ∀𝑦 ∈ 𝑛 ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛))) | 
| 107 |  | vex 3483 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ 𝑛 ∈ V | 
| 108 |  | fveq2 6905 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑦 = 𝑛 → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) = ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)) | 
| 109 | 108 | sseq1d 4014 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑦 = 𝑛 → (((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛) ↔ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛))) | 
| 110 | 107, 109 | ralsn 4680 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(∀𝑦 ∈
{𝑛} ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛) ↔ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛)) | 
| 111 | 103, 110 | sylibr 234 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑛 ∈ ω ∧
((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ (fi‘𝐴)) → ∀𝑦 ∈ {𝑛} ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛)) | 
| 112 | 106, 111 | jctird 526 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑛 ∈ ω ∧
((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ (fi‘𝐴)) → (∀𝑦 ∈ 𝑛 ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) → (∀𝑦 ∈ 𝑛 ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛) ∧ ∀𝑦 ∈ {𝑛} ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛)))) | 
| 113 |  | df-suc 6389 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ suc 𝑛 = (𝑛 ∪ {𝑛}) | 
| 114 | 113 | raleqi 3323 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(∀𝑦 ∈
suc 𝑛((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛) ↔ ∀𝑦 ∈ (𝑛 ∪ {𝑛})((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛)) | 
| 115 |  | ralunb 4196 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(∀𝑦 ∈
(𝑛 ∪ {𝑛})((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛) ↔ (∀𝑦 ∈ 𝑛 ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛) ∧ ∀𝑦 ∈ {𝑛} ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛))) | 
| 116 | 114, 115 | bitri 275 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(∀𝑦 ∈
suc 𝑛((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛) ↔ (∀𝑦 ∈ 𝑛 ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛) ∧ ∀𝑦 ∈ {𝑛} ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛))) | 
| 117 | 112, 116 | imbitrrdi 252 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑛 ∈ ω ∧
((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ (fi‘𝐴)) → (∀𝑦 ∈ 𝑛 ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) → ∀𝑦 ∈ suc 𝑛((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛))) | 
| 118 |  | fiin 9463 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑎 ∈ (fi‘𝐴) ∧ 𝑏 ∈ (fi‘𝐴)) → (𝑎 ∩ 𝑏) ∈ (fi‘𝐴)) | 
| 119 | 118 | rgen2 3198 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
∀𝑎 ∈
(fi‘𝐴)∀𝑏 ∈ (fi‘𝐴)(𝑎 ∩ 𝑏) ∈ (fi‘𝐴) | 
| 120 |  | ss2ralv 4053 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
(((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ (fi‘𝐴) → (∀𝑎 ∈ (fi‘𝐴)∀𝑏 ∈ (fi‘𝐴)(𝑎 ∩ 𝑏) ∈ (fi‘𝐴) → ∀𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)∀𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)(𝑎 ∩ 𝑏) ∈ (fi‘𝐴))) | 
| 121 | 119, 120 | mpi 20 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ (fi‘𝐴) → ∀𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)∀𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)(𝑎 ∩ 𝑏) ∈ (fi‘𝐴)) | 
| 122 | 59 | fmpo 8094 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(∀𝑎 ∈
((rec(𝑅, 𝐴) ↾ ω)‘𝑛)∀𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)(𝑎 ∩ 𝑏) ∈ (fi‘𝐴) ↔ (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎 ∩ 𝑏)):(((rec(𝑅, 𝐴) ↾ ω)‘𝑛) × ((rec(𝑅, 𝐴) ↾ ω)‘𝑛))⟶(fi‘𝐴)) | 
| 123 | 121, 122 | sylib 218 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ (fi‘𝐴) → (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎 ∩ 𝑏)):(((rec(𝑅, 𝐴) ↾ ω)‘𝑛) × ((rec(𝑅, 𝐴) ↾ ω)‘𝑛))⟶(fi‘𝐴)) | 
| 124 | 123 | frnd 6743 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ (fi‘𝐴) → ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎 ∩ 𝑏)) ⊆ (fi‘𝐴)) | 
| 125 | 124 | adantl 481 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑛 ∈ ω ∧
((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ (fi‘𝐴)) → ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ↦ (𝑎 ∩ 𝑏)) ⊆ (fi‘𝐴)) | 
| 126 | 102, 125 | eqsstrd 4017 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑛 ∈ ω ∧
((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ (fi‘𝐴)) → ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛) ⊆ (fi‘𝐴)) | 
| 127 | 117, 126 | jctild 525 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑛 ∈ ω ∧
((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ (fi‘𝐴)) → (∀𝑦 ∈ 𝑛 ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) → (((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛) ⊆ (fi‘𝐴) ∧ ∀𝑦 ∈ suc 𝑛((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛)))) | 
| 128 | 127 | expimpd 453 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑛 ∈ ω →
((((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ (fi‘𝐴) ∧ ∀𝑦 ∈ 𝑛 ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)) → (((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛) ⊆ (fi‘𝐴) ∧ ∀𝑦 ∈ suc 𝑛((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛)))) | 
| 129 | 128 | a1d 25 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑛 ∈ ω → (𝐴 ∈ 𝑉 → ((((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ (fi‘𝐴) ∧ ∀𝑦 ∈ 𝑛 ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)) → (((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛) ⊆ (fi‘𝐴) ∧ ∀𝑦 ∈ suc 𝑛((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘suc 𝑛))))) | 
| 130 | 36, 41, 46, 48, 129 | finds2 7921 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 ∈ ω → (𝐴 ∈ 𝑉 → (((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ⊆ (fi‘𝐴) ∧ ∀𝑦 ∈ 𝑥 ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥)))) | 
| 131 | 130 | impcom 407 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ ω) → (((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ⊆ (fi‘𝐴) ∧ ∀𝑦 ∈ 𝑥 ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥))) | 
| 132 | 131 | simprd 495 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ ω) → ∀𝑦 ∈ 𝑥 ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥)) | 
| 133 | 132 | r19.21bi 3250 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ ω) ∧ 𝑦 ∈ 𝑥) → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥)) | 
| 134 | 133 | ex 412 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ ω) → (𝑦 ∈ 𝑥 → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥))) | 
| 135 | 134 | adantr 480 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ ω) ∧ 𝑦 ∈ ω) → (𝑦 ∈ 𝑥 → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥))) | 
| 136 |  | fveq2 6905 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 = 𝑥 → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) = ((rec(𝑅, 𝐴) ↾ ω)‘𝑥)) | 
| 137 |  | eqimss 4041 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((rec(𝑅, 𝐴) ↾ ω)‘𝑦) = ((rec(𝑅, 𝐴) ↾ ω)‘𝑥) → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥)) | 
| 138 | 136, 137 | syl 17 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = 𝑥 → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥)) | 
| 139 | 138 | a1i 11 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ ω) ∧ 𝑦 ∈ ω) → (𝑦 = 𝑥 → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥))) | 
| 140 | 135, 139 | jaod 859 | . . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ ω) ∧ 𝑦 ∈ ω) → ((𝑦 ∈ 𝑥 ∨ 𝑦 = 𝑥) → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥))) | 
| 141 | 31, 140 | sylbid 240 | . . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ ω) ∧ 𝑦 ∈ ω) → (𝑦 ⊆ 𝑥 → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥))) | 
| 142 | 141 | ralrimiva 3145 | . . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ ω) → ∀𝑦 ∈ ω (𝑦 ⊆ 𝑥 → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥))) | 
| 143 | 142 | ralrimiva 3145 | . . . . . . . . . . . . . 14
⊢ (𝐴 ∈ 𝑉 → ∀𝑥 ∈ ω ∀𝑦 ∈ ω (𝑦 ⊆ 𝑥 → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥))) | 
| 144 | 143 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) → ∀𝑥 ∈ ω ∀𝑦 ∈ ω (𝑦 ⊆ 𝑥 → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥))) | 
| 145 |  | ssun1 4177 | . . . . . . . . . . . . . 14
⊢ 𝑚 ⊆ (𝑚 ∪ 𝑛) | 
| 146 | 145 | a1i 11 | . . . . . . . . . . . . 13
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) → 𝑚 ⊆ (𝑚 ∪ 𝑛)) | 
| 147 |  | sseq2 4009 | . . . . . . . . . . . . . . 15
⊢ (𝑥 = (𝑚 ∪ 𝑛) → (𝑦 ⊆ 𝑥 ↔ 𝑦 ⊆ (𝑚 ∪ 𝑛))) | 
| 148 |  | fveq2 6905 | . . . . . . . . . . . . . . . 16
⊢ (𝑥 = (𝑚 ∪ 𝑛) → ((rec(𝑅, 𝐴) ↾ ω)‘𝑥) = ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛))) | 
| 149 | 148 | sseq2d 4015 | . . . . . . . . . . . . . . 15
⊢ (𝑥 = (𝑚 ∪ 𝑛) → (((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ↔ ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)))) | 
| 150 | 147, 149 | imbi12d 344 | . . . . . . . . . . . . . 14
⊢ (𝑥 = (𝑚 ∪ 𝑛) → ((𝑦 ⊆ 𝑥 → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥)) ↔ (𝑦 ⊆ (𝑚 ∪ 𝑛) → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛))))) | 
| 151 |  | sseq1 4008 | . . . . . . . . . . . . . . 15
⊢ (𝑦 = 𝑚 → (𝑦 ⊆ (𝑚 ∪ 𝑛) ↔ 𝑚 ⊆ (𝑚 ∪ 𝑛))) | 
| 152 |  | fveq2 6905 | . . . . . . . . . . . . . . . 16
⊢ (𝑦 = 𝑚 → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) = ((rec(𝑅, 𝐴) ↾ ω)‘𝑚)) | 
| 153 | 152 | sseq1d 4014 | . . . . . . . . . . . . . . 15
⊢ (𝑦 = 𝑚 → (((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)) ↔ ((rec(𝑅, 𝐴) ↾ ω)‘𝑚) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)))) | 
| 154 | 151, 153 | imbi12d 344 | . . . . . . . . . . . . . 14
⊢ (𝑦 = 𝑚 → ((𝑦 ⊆ (𝑚 ∪ 𝑛) → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛))) ↔ (𝑚 ⊆ (𝑚 ∪ 𝑛) → ((rec(𝑅, 𝐴) ↾ ω)‘𝑚) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛))))) | 
| 155 | 150, 154 | rspc2v 3632 | . . . . . . . . . . . . 13
⊢ (((𝑚 ∪ 𝑛) ∈ ω ∧ 𝑚 ∈ ω) → (∀𝑥 ∈ ω ∀𝑦 ∈ ω (𝑦 ⊆ 𝑥 → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥)) → (𝑚 ⊆ (𝑚 ∪ 𝑛) → ((rec(𝑅, 𝐴) ↾ ω)‘𝑚) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛))))) | 
| 156 | 26, 144, 146, 155 | syl3c 66 | . . . . . . . . . . . 12
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) → ((rec(𝑅, 𝐴) ↾ ω)‘𝑚) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛))) | 
| 157 | 156 | sseld 3981 | . . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) → (𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑚) → 𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)))) | 
| 158 |  | simprr 772 | . . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) → 𝑛 ∈ ω) | 
| 159 | 24, 158 | jca 511 | . . . . . . . . . . . . 13
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) → ((𝑚 ∪ 𝑛) ∈ ω ∧ 𝑛 ∈ ω)) | 
| 160 |  | ssun2 4178 | . . . . . . . . . . . . . 14
⊢ 𝑛 ⊆ (𝑚 ∪ 𝑛) | 
| 161 | 160 | a1i 11 | . . . . . . . . . . . . 13
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) → 𝑛 ⊆ (𝑚 ∪ 𝑛)) | 
| 162 |  | sseq1 4008 | . . . . . . . . . . . . . . 15
⊢ (𝑦 = 𝑛 → (𝑦 ⊆ (𝑚 ∪ 𝑛) ↔ 𝑛 ⊆ (𝑚 ∪ 𝑛))) | 
| 163 | 108 | sseq1d 4014 | . . . . . . . . . . . . . . 15
⊢ (𝑦 = 𝑛 → (((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)) ↔ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)))) | 
| 164 | 162, 163 | imbi12d 344 | . . . . . . . . . . . . . 14
⊢ (𝑦 = 𝑛 → ((𝑦 ⊆ (𝑚 ∪ 𝑛) → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛))) ↔ (𝑛 ⊆ (𝑚 ∪ 𝑛) → ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛))))) | 
| 165 | 150, 164 | rspc2v 3632 | . . . . . . . . . . . . 13
⊢ (((𝑚 ∪ 𝑛) ∈ ω ∧ 𝑛 ∈ ω) → (∀𝑥 ∈ ω ∀𝑦 ∈ ω (𝑦 ⊆ 𝑥 → ((rec(𝑅, 𝐴) ↾ ω)‘𝑦) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘𝑥)) → (𝑛 ⊆ (𝑚 ∪ 𝑛) → ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛))))) | 
| 166 | 159, 144,
161, 165 | syl3c 66 | . . . . . . . . . . . 12
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) → ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) ⊆ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛))) | 
| 167 | 166 | sseld 3981 | . . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) → (𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛) → 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)))) | 
| 168 | 23 | ad2antlr 727 | . . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) ∧ (𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)) ∧ 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)))) → (𝑚 ∪ 𝑛) ∈ ω) | 
| 169 |  | peano2 7913 | . . . . . . . . . . . . . . 15
⊢ ((𝑚 ∪ 𝑛) ∈ ω → suc (𝑚 ∪ 𝑛) ∈ ω) | 
| 170 |  | fveq2 6905 | . . . . . . . . . . . . . . . 16
⊢ (𝑥 = suc (𝑚 ∪ 𝑛) → ((rec(𝑅, 𝐴) ↾ ω)‘𝑥) = ((rec(𝑅, 𝐴) ↾ ω)‘suc (𝑚 ∪ 𝑛))) | 
| 171 | 170 | ssiun2s 5047 | . . . . . . . . . . . . . . 15
⊢ (suc
(𝑚 ∪ 𝑛) ∈ ω → ((rec(𝑅, 𝐴) ↾ ω)‘suc (𝑚 ∪ 𝑛)) ⊆ ∪ 𝑥 ∈ ω ((rec(𝑅, 𝐴) ↾ ω)‘𝑥)) | 
| 172 | 168, 169,
171 | 3syl 18 | . . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) ∧ (𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)) ∧ 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)))) → ((rec(𝑅, 𝐴) ↾ ω)‘suc (𝑚 ∪ 𝑛)) ⊆ ∪ 𝑥 ∈ ω ((rec(𝑅, 𝐴) ↾ ω)‘𝑥)) | 
| 173 |  | simprl 770 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) ∧ (𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)) ∧ 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)))) → 𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛))) | 
| 174 |  | simprr 772 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) ∧ (𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)) ∧ 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)))) → 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛))) | 
| 175 |  | eqidd 2737 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) ∧ (𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)) ∧ 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)))) → (𝑐 ∩ 𝑑) = (𝑐 ∩ 𝑑)) | 
| 176 |  | ineq1 4212 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑎 = 𝑐 → (𝑎 ∩ 𝑏) = (𝑐 ∩ 𝑏)) | 
| 177 | 176 | eqeq2d 2747 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑎 = 𝑐 → ((𝑐 ∩ 𝑑) = (𝑎 ∩ 𝑏) ↔ (𝑐 ∩ 𝑑) = (𝑐 ∩ 𝑏))) | 
| 178 |  | ineq2 4213 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑏 = 𝑑 → (𝑐 ∩ 𝑏) = (𝑐 ∩ 𝑑)) | 
| 179 | 178 | eqeq2d 2747 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑏 = 𝑑 → ((𝑐 ∩ 𝑑) = (𝑐 ∩ 𝑏) ↔ (𝑐 ∩ 𝑑) = (𝑐 ∩ 𝑑))) | 
| 180 | 177, 179 | rspc2ev 3634 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)) ∧ 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)) ∧ (𝑐 ∩ 𝑑) = (𝑐 ∩ 𝑑)) → ∃𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛))∃𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛))(𝑐 ∩ 𝑑) = (𝑎 ∩ 𝑏)) | 
| 181 | 173, 174,
175, 180 | syl3anc 1372 | . . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) ∧ (𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)) ∧ 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)))) → ∃𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛))∃𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛))(𝑐 ∩ 𝑑) = (𝑎 ∩ 𝑏)) | 
| 182 |  | vex 3483 | . . . . . . . . . . . . . . . . . . 19
⊢ 𝑐 ∈ V | 
| 183 | 182 | inex1 5316 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑐 ∩ 𝑑) ∈ V | 
| 184 |  | eqeq1 2740 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = (𝑐 ∩ 𝑑) → (𝑥 = (𝑎 ∩ 𝑏) ↔ (𝑐 ∩ 𝑑) = (𝑎 ∩ 𝑏))) | 
| 185 | 184 | 2rexbidv 3221 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = (𝑐 ∩ 𝑑) → (∃𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛))∃𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛))𝑥 = (𝑎 ∩ 𝑏) ↔ ∃𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛))∃𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛))(𝑐 ∩ 𝑑) = (𝑎 ∩ 𝑏))) | 
| 186 | 183, 185 | elab 3678 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑐 ∩ 𝑑) ∈ {𝑥 ∣ ∃𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛))∃𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛))𝑥 = (𝑎 ∩ 𝑏)} ↔ ∃𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛))∃𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛))(𝑐 ∩ 𝑑) = (𝑎 ∩ 𝑏)) | 
| 187 | 181, 186 | sylibr 234 | . . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) ∧ (𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)) ∧ 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)))) → (𝑐 ∩ 𝑑) ∈ {𝑥 ∣ ∃𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛))∃𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛))𝑥 = (𝑎 ∩ 𝑏)}) | 
| 188 |  | eqid 2736 | . . . . . . . . . . . . . . . . 17
⊢ (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)) ↦ (𝑎 ∩ 𝑏)) = (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)) ↦ (𝑎 ∩ 𝑏)) | 
| 189 | 188 | rnmpo 7567 | . . . . . . . . . . . . . . . 16
⊢ ran
(𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)) ↦ (𝑎 ∩ 𝑏)) = {𝑥 ∣ ∃𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛))∃𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛))𝑥 = (𝑎 ∩ 𝑏)} | 
| 190 | 187, 189 | eleqtrrdi 2851 | . . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) ∧ (𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)) ∧ 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)))) → (𝑐 ∩ 𝑑) ∈ ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)) ↦ (𝑎 ∩ 𝑏))) | 
| 191 |  | fvex 6918 | . . . . . . . . . . . . . . . . . . 19
⊢
((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)) ∈ V | 
| 192 | 191 | uniex 7762 | . . . . . . . . . . . . . . . . . 18
⊢ ∪ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)) ∈ V | 
| 193 | 192 | pwex 5379 | . . . . . . . . . . . . . . . . 17
⊢ 𝒫
∪ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)) ∈ V | 
| 194 |  | elssuni 4936 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)) → 𝑎 ⊆ ∪
((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛))) | 
| 195 | 68, 194 | sstrid 3994 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)) → (𝑎 ∩ 𝑏) ⊆ ∪
((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛))) | 
| 196 | 73 | elpw 4603 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑎 ∩ 𝑏) ∈ 𝒫 ∪ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)) ↔ (𝑎 ∩ 𝑏) ⊆ ∪
((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛))) | 
| 197 | 195, 196 | sylibr 234 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)) → (𝑎 ∩ 𝑏) ∈ 𝒫 ∪ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛))) | 
| 198 | 197 | adantr 480 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)) ∧ 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛))) → (𝑎 ∩ 𝑏) ∈ 𝒫 ∪ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛))) | 
| 199 | 198 | rgen2 3198 | . . . . . . . . . . . . . . . . . . 19
⊢
∀𝑎 ∈
((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛))∀𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛))(𝑎 ∩ 𝑏) ∈ 𝒫 ∪ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)) | 
| 200 | 188 | fmpo 8094 | . . . . . . . . . . . . . . . . . . 19
⊢
(∀𝑎 ∈
((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛))∀𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛))(𝑎 ∩ 𝑏) ∈ 𝒫 ∪ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)) ↔ (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)) ↦ (𝑎 ∩ 𝑏)):(((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)) × ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)))⟶𝒫 ∪ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛))) | 
| 201 | 199, 200 | mpbi 230 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)) ↦ (𝑎 ∩ 𝑏)):(((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)) × ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)))⟶𝒫 ∪ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)) | 
| 202 |  | frn 6742 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)) ↦ (𝑎 ∩ 𝑏)):(((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)) × ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)))⟶𝒫 ∪ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)) → ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)) ↦ (𝑎 ∩ 𝑏)) ⊆ 𝒫 ∪ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛))) | 
| 203 | 201, 202 | ax-mp 5 | . . . . . . . . . . . . . . . . 17
⊢ ran
(𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)) ↦ (𝑎 ∩ 𝑏)) ⊆ 𝒫 ∪ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)) | 
| 204 | 193, 203 | ssexi 5321 | . . . . . . . . . . . . . . . 16
⊢ ran
(𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)) ↦ (𝑎 ∩ 𝑏)) ∈ V | 
| 205 |  | nfcv 2904 | . . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑣(𝑚 ∪ 𝑛) | 
| 206 |  | nfcv 2904 | . . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑣ran
(𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)) ↦ (𝑎 ∩ 𝑏)) | 
| 207 |  | mpoeq12 7507 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑣 = ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)) ∧ 𝑣 = ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛))) → (𝑎 ∈ 𝑣, 𝑏 ∈ 𝑣 ↦ (𝑎 ∩ 𝑏)) = (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)) ↦ (𝑎 ∩ 𝑏))) | 
| 208 | 207 | anidms 566 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑣 = ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)) → (𝑎 ∈ 𝑣, 𝑏 ∈ 𝑣 ↦ (𝑎 ∩ 𝑏)) = (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)) ↦ (𝑎 ∩ 𝑏))) | 
| 209 | 208 | rneqd 5948 | . . . . . . . . . . . . . . . . 17
⊢ (𝑣 = ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)) → ran (𝑎 ∈ 𝑣, 𝑏 ∈ 𝑣 ↦ (𝑎 ∩ 𝑏)) = ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)) ↦ (𝑎 ∩ 𝑏))) | 
| 210 | 82, 205, 206, 97, 209 | frsucmpt 8479 | . . . . . . . . . . . . . . . 16
⊢ (((𝑚 ∪ 𝑛) ∈ ω ∧ ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)) ↦ (𝑎 ∩ 𝑏)) ∈ V) → ((rec(𝑅, 𝐴) ↾ ω)‘suc (𝑚 ∪ 𝑛)) = ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)) ↦ (𝑎 ∩ 𝑏))) | 
| 211 | 168, 204,
210 | sylancl 586 | . . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) ∧ (𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)) ∧ 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)))) → ((rec(𝑅, 𝐴) ↾ ω)‘suc (𝑚 ∪ 𝑛)) = ran (𝑎 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)), 𝑏 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)) ↦ (𝑎 ∩ 𝑏))) | 
| 212 | 190, 211 | eleqtrrd 2843 | . . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) ∧ (𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)) ∧ 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)))) → (𝑐 ∩ 𝑑) ∈ ((rec(𝑅, 𝐴) ↾ ω)‘suc (𝑚 ∪ 𝑛))) | 
| 213 | 172, 212 | sseldd 3983 | . . . . . . . . . . . . 13
⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) ∧ (𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)) ∧ 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)))) → (𝑐 ∩ 𝑑) ∈ ∪
𝑥 ∈ ω
((rec(𝑅, 𝐴) ↾ ω)‘𝑥)) | 
| 214 |  | fniunfv 7268 | . . . . . . . . . . . . . 14
⊢
((rec(𝑅, 𝐴) ↾ ω) Fn ω
→ ∪ 𝑥 ∈ ω ((rec(𝑅, 𝐴) ↾ ω)‘𝑥) = ∪ ran
(rec(𝑅, 𝐴) ↾ ω)) | 
| 215 | 3, 214 | ax-mp 5 | . . . . . . . . . . . . 13
⊢ ∪ 𝑥 ∈ ω ((rec(𝑅, 𝐴) ↾ ω)‘𝑥) = ∪ ran
(rec(𝑅, 𝐴) ↾ ω) | 
| 216 | 213, 215 | eleqtrdi 2850 | . . . . . . . . . . . 12
⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) ∧ (𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)) ∧ 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)))) → (𝑐 ∩ 𝑑) ∈ ∪ ran
(rec(𝑅, 𝐴) ↾ ω)) | 
| 217 | 216 | ex 412 | . . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) → ((𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛)) ∧ 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘(𝑚 ∪ 𝑛))) → (𝑐 ∩ 𝑑) ∈ ∪ ran
(rec(𝑅, 𝐴) ↾ ω))) | 
| 218 | 157, 167,
217 | syl2and 608 | . . . . . . . . . 10
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑛 ∈ ω)) → ((𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑚) ∧ 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)) → (𝑐 ∩ 𝑑) ∈ ∪ ran
(rec(𝑅, 𝐴) ↾ ω))) | 
| 219 | 218 | rexlimdvva 3212 | . . . . . . . . 9
⊢ (𝐴 ∈ 𝑉 → (∃𝑚 ∈ ω ∃𝑛 ∈ ω (𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑚) ∧ 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛)) → (𝑐 ∩ 𝑑) ∈ ∪ ran
(rec(𝑅, 𝐴) ↾ ω))) | 
| 220 | 219 | imp 406 | . . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ ∃𝑚 ∈ ω ∃𝑛 ∈ ω (𝑐 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑚) ∧ 𝑑 ∈ ((rec(𝑅, 𝐴) ↾ ω)‘𝑛))) → (𝑐 ∩ 𝑑) ∈ ∪ ran
(rec(𝑅, 𝐴) ↾ ω)) | 
| 221 | 20, 220 | sylan2br 595 | . . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑐 ∈ ∪ ran
(rec(𝑅, 𝐴) ↾ ω) ∧ 𝑑 ∈ ∪ ran
(rec(𝑅, 𝐴) ↾ ω))) → (𝑐 ∩ 𝑑) ∈ ∪ ran
(rec(𝑅, 𝐴) ↾ ω)) | 
| 222 | 221 | ralrimivva 3201 | . . . . . 6
⊢ (𝐴 ∈ 𝑉 → ∀𝑐 ∈ ∪ ran
(rec(𝑅, 𝐴) ↾ ω)∀𝑑 ∈ ∪ ran
(rec(𝑅, 𝐴) ↾ ω)(𝑐 ∩ 𝑑) ∈ ∪ ran
(rec(𝑅, 𝐴) ↾ ω)) | 
| 223 | 131 | simpld 494 | . . . . . . . . . . . 12
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ ω) → ((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ⊆ (fi‘𝐴)) | 
| 224 |  | fvex 6918 | . . . . . . . . . . . . 13
⊢
(fi‘𝐴) ∈
V | 
| 225 | 224 | elpw2 5333 | . . . . . . . . . . . 12
⊢
(((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ∈ 𝒫
(fi‘𝐴) ↔
((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ⊆ (fi‘𝐴)) | 
| 226 | 223, 225 | sylibr 234 | . . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ ω) → ((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ∈ 𝒫 (fi‘𝐴)) | 
| 227 | 226 | ralrimiva 3145 | . . . . . . . . . 10
⊢ (𝐴 ∈ 𝑉 → ∀𝑥 ∈ ω ((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ∈ 𝒫 (fi‘𝐴)) | 
| 228 |  | fnfvrnss 7140 | . . . . . . . . . 10
⊢
(((rec(𝑅, 𝐴) ↾ ω) Fn ω
∧ ∀𝑥 ∈
ω ((rec(𝑅, 𝐴) ↾ ω)‘𝑥) ∈ 𝒫
(fi‘𝐴)) → ran
(rec(𝑅, 𝐴) ↾ ω) ⊆ 𝒫
(fi‘𝐴)) | 
| 229 | 3, 227, 228 | sylancr 587 | . . . . . . . . 9
⊢ (𝐴 ∈ 𝑉 → ran (rec(𝑅, 𝐴) ↾ ω) ⊆ 𝒫
(fi‘𝐴)) | 
| 230 |  | sspwuni 5099 | . . . . . . . . 9
⊢ (ran
(rec(𝑅, 𝐴) ↾ ω) ⊆ 𝒫
(fi‘𝐴) ↔ ∪ ran (rec(𝑅, 𝐴) ↾ ω) ⊆ (fi‘𝐴)) | 
| 231 | 229, 230 | sylib 218 | . . . . . . . 8
⊢ (𝐴 ∈ 𝑉 → ∪ ran
(rec(𝑅, 𝐴) ↾ ω) ⊆ (fi‘𝐴)) | 
| 232 |  | ssexg 5322 | . . . . . . . 8
⊢ ((∪ ran (rec(𝑅, 𝐴) ↾ ω) ⊆ (fi‘𝐴) ∧ (fi‘𝐴) ∈ V) → ∪ ran (rec(𝑅, 𝐴) ↾ ω) ∈
V) | 
| 233 | 231, 224,
232 | sylancl 586 | . . . . . . 7
⊢ (𝐴 ∈ 𝑉 → ∪ ran
(rec(𝑅, 𝐴) ↾ ω) ∈
V) | 
| 234 |  | sseq2 4009 | . . . . . . . . 9
⊢ (𝑥 = ∪
ran (rec(𝑅, 𝐴) ↾ ω) → (𝐴 ⊆ 𝑥 ↔ 𝐴 ⊆ ∪ ran
(rec(𝑅, 𝐴) ↾ ω))) | 
| 235 |  | eleq2 2829 | . . . . . . . . . . 11
⊢ (𝑥 = ∪
ran (rec(𝑅, 𝐴) ↾ ω) →
((𝑐 ∩ 𝑑) ∈ 𝑥 ↔ (𝑐 ∩ 𝑑) ∈ ∪ ran
(rec(𝑅, 𝐴) ↾ ω))) | 
| 236 | 235 | raleqbi1dv 3337 | . . . . . . . . . 10
⊢ (𝑥 = ∪
ran (rec(𝑅, 𝐴) ↾ ω) →
(∀𝑑 ∈ 𝑥 (𝑐 ∩ 𝑑) ∈ 𝑥 ↔ ∀𝑑 ∈ ∪ ran
(rec(𝑅, 𝐴) ↾ ω)(𝑐 ∩ 𝑑) ∈ ∪ ran
(rec(𝑅, 𝐴) ↾ ω))) | 
| 237 | 236 | raleqbi1dv 3337 | . . . . . . . . 9
⊢ (𝑥 = ∪
ran (rec(𝑅, 𝐴) ↾ ω) →
(∀𝑐 ∈ 𝑥 ∀𝑑 ∈ 𝑥 (𝑐 ∩ 𝑑) ∈ 𝑥 ↔ ∀𝑐 ∈ ∪ ran
(rec(𝑅, 𝐴) ↾ ω)∀𝑑 ∈ ∪ ran
(rec(𝑅, 𝐴) ↾ ω)(𝑐 ∩ 𝑑) ∈ ∪ ran
(rec(𝑅, 𝐴) ↾ ω))) | 
| 238 | 234, 237 | anbi12d 632 | . . . . . . . 8
⊢ (𝑥 = ∪
ran (rec(𝑅, 𝐴) ↾ ω) →
((𝐴 ⊆ 𝑥 ∧ ∀𝑐 ∈ 𝑥 ∀𝑑 ∈ 𝑥 (𝑐 ∩ 𝑑) ∈ 𝑥) ↔ (𝐴 ⊆ ∪ ran
(rec(𝑅, 𝐴) ↾ ω) ∧ ∀𝑐 ∈ ∪ ran (rec(𝑅, 𝐴) ↾ ω)∀𝑑 ∈ ∪ ran
(rec(𝑅, 𝐴) ↾ ω)(𝑐 ∩ 𝑑) ∈ ∪ ran
(rec(𝑅, 𝐴) ↾ ω)))) | 
| 239 | 238 | elabg 3675 | . . . . . . 7
⊢ (∪ ran (rec(𝑅, 𝐴) ↾ ω) ∈ V → (∪ ran (rec(𝑅, 𝐴) ↾ ω) ∈ {𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ ∀𝑐 ∈ 𝑥 ∀𝑑 ∈ 𝑥 (𝑐 ∩ 𝑑) ∈ 𝑥)} ↔ (𝐴 ⊆ ∪ ran
(rec(𝑅, 𝐴) ↾ ω) ∧ ∀𝑐 ∈ ∪ ran (rec(𝑅, 𝐴) ↾ ω)∀𝑑 ∈ ∪ ran
(rec(𝑅, 𝐴) ↾ ω)(𝑐 ∩ 𝑑) ∈ ∪ ran
(rec(𝑅, 𝐴) ↾ ω)))) | 
| 240 | 233, 239 | syl 17 | . . . . . 6
⊢ (𝐴 ∈ 𝑉 → (∪ ran
(rec(𝑅, 𝐴) ↾ ω) ∈ {𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ ∀𝑐 ∈ 𝑥 ∀𝑑 ∈ 𝑥 (𝑐 ∩ 𝑑) ∈ 𝑥)} ↔ (𝐴 ⊆ ∪ ran
(rec(𝑅, 𝐴) ↾ ω) ∧ ∀𝑐 ∈ ∪ ran (rec(𝑅, 𝐴) ↾ ω)∀𝑑 ∈ ∪ ran
(rec(𝑅, 𝐴) ↾ ω)(𝑐 ∩ 𝑑) ∈ ∪ ran
(rec(𝑅, 𝐴) ↾ ω)))) | 
| 241 | 9, 222, 240 | mpbir2and 713 | . . . . 5
⊢ (𝐴 ∈ 𝑉 → ∪ ran
(rec(𝑅, 𝐴) ↾ ω) ∈ {𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ ∀𝑐 ∈ 𝑥 ∀𝑑 ∈ 𝑥 (𝑐 ∩ 𝑑) ∈ 𝑥)}) | 
| 242 |  | intss1 4962 | . . . . 5
⊢ (∪ ran (rec(𝑅, 𝐴) ↾ ω) ∈ {𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ ∀𝑐 ∈ 𝑥 ∀𝑑 ∈ 𝑥 (𝑐 ∩ 𝑑) ∈ 𝑥)} → ∩ {𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ ∀𝑐 ∈ 𝑥 ∀𝑑 ∈ 𝑥 (𝑐 ∩ 𝑑) ∈ 𝑥)} ⊆ ∪ ran
(rec(𝑅, 𝐴) ↾ ω)) | 
| 243 | 241, 242 | syl 17 | . . . 4
⊢ (𝐴 ∈ 𝑉 → ∩ {𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ ∀𝑐 ∈ 𝑥 ∀𝑑 ∈ 𝑥 (𝑐 ∩ 𝑑) ∈ 𝑥)} ⊆ ∪ ran
(rec(𝑅, 𝐴) ↾ ω)) | 
| 244 | 1, 243 | eqsstrd 4017 | . . 3
⊢ (𝐴 ∈ 𝑉 → (fi‘𝐴) ⊆ ∪ ran
(rec(𝑅, 𝐴) ↾ ω)) | 
| 245 | 244, 231 | eqssd 4000 | . 2
⊢ (𝐴 ∈ 𝑉 → (fi‘𝐴) = ∪ ran
(rec(𝑅, 𝐴) ↾ ω)) | 
| 246 |  | df-ima 5697 | . . 3
⊢
(rec(𝑅, 𝐴) “ ω) = ran
(rec(𝑅, 𝐴) ↾ ω) | 
| 247 | 246 | unieqi 4918 | . 2
⊢ ∪ (rec(𝑅, 𝐴) “ ω) = ∪ ran (rec(𝑅, 𝐴) ↾ ω) | 
| 248 | 245, 247 | eqtr4di 2794 | 1
⊢ (𝐴 ∈ 𝑉 → (fi‘𝐴) = ∪ (rec(𝑅, 𝐴) “ ω)) |