Proof of Theorem dfrecs3OLD
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | df-recs 8411 | . 2
⊢
recs(𝐹) = wrecs( E ,
On, 𝐹) | 
| 2 |  | dfwrecsOLD 8338 | . 2
⊢ wrecs( E
, On, 𝐹) = ∪ {𝑓
∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ On ∧ ∀𝑦 ∈ 𝑥 Pred( E , On, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ Pred( E , On, 𝑦))))} | 
| 3 |  | 3anass 1095 | . . . . . . 7
⊢ ((𝑓 Fn 𝑥 ∧ (𝑥 ⊆ On ∧ ∀𝑦 ∈ 𝑥 Pred( E , On, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ Pred( E , On, 𝑦)))) ↔ (𝑓 Fn 𝑥 ∧ ((𝑥 ⊆ On ∧ ∀𝑦 ∈ 𝑥 Pred( E , On, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ Pred( E , On, 𝑦)))))) | 
| 4 |  | vex 3484 | . . . . . . . . . . . 12
⊢ 𝑥 ∈ V | 
| 5 | 4 | elon 6393 | . . . . . . . . . . 11
⊢ (𝑥 ∈ On ↔ Ord 𝑥) | 
| 6 |  | ordsson 7803 | . . . . . . . . . . . . 13
⊢ (Ord
𝑥 → 𝑥 ⊆ On) | 
| 7 |  | ordtr 6398 | . . . . . . . . . . . . 13
⊢ (Ord
𝑥 → Tr 𝑥) | 
| 8 | 6, 7 | jca 511 | . . . . . . . . . . . 12
⊢ (Ord
𝑥 → (𝑥 ⊆ On ∧ Tr 𝑥)) | 
| 9 |  | epweon 7795 | . . . . . . . . . . . . . . 15
⊢  E We
On | 
| 10 |  | wess 5671 | . . . . . . . . . . . . . . 15
⊢ (𝑥 ⊆ On → ( E We On
→ E We 𝑥)) | 
| 11 | 9, 10 | mpi 20 | . . . . . . . . . . . . . 14
⊢ (𝑥 ⊆ On → E We 𝑥) | 
| 12 | 11 | anim1ci 616 | . . . . . . . . . . . . 13
⊢ ((𝑥 ⊆ On ∧ Tr 𝑥) → (Tr 𝑥 ∧ E We 𝑥)) | 
| 13 |  | df-ord 6387 | . . . . . . . . . . . . 13
⊢ (Ord
𝑥 ↔ (Tr 𝑥 ∧ E We 𝑥)) | 
| 14 | 12, 13 | sylibr 234 | . . . . . . . . . . . 12
⊢ ((𝑥 ⊆ On ∧ Tr 𝑥) → Ord 𝑥) | 
| 15 | 8, 14 | impbii 209 | . . . . . . . . . . 11
⊢ (Ord
𝑥 ↔ (𝑥 ⊆ On ∧ Tr 𝑥)) | 
| 16 |  | dftr3 5265 | . . . . . . . . . . . . 13
⊢ (Tr 𝑥 ↔ ∀𝑦 ∈ 𝑥 𝑦 ⊆ 𝑥) | 
| 17 |  | ssel2 3978 | . . . . . . . . . . . . . . 15
⊢ ((𝑥 ⊆ On ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ On) | 
| 18 |  | predon 7806 | . . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ On → Pred( E , On,
𝑦) = 𝑦) | 
| 19 | 18 | sseq1d 4015 | . . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ On → (Pred( E , On,
𝑦) ⊆ 𝑥 ↔ 𝑦 ⊆ 𝑥)) | 
| 20 | 17, 19 | syl 17 | . . . . . . . . . . . . . 14
⊢ ((𝑥 ⊆ On ∧ 𝑦 ∈ 𝑥) → (Pred( E , On, 𝑦) ⊆ 𝑥 ↔ 𝑦 ⊆ 𝑥)) | 
| 21 | 20 | ralbidva 3176 | . . . . . . . . . . . . 13
⊢ (𝑥 ⊆ On →
(∀𝑦 ∈ 𝑥 Pred( E , On, 𝑦) ⊆ 𝑥 ↔ ∀𝑦 ∈ 𝑥 𝑦 ⊆ 𝑥)) | 
| 22 | 16, 21 | bitr4id 290 | . . . . . . . . . . . 12
⊢ (𝑥 ⊆ On → (Tr 𝑥 ↔ ∀𝑦 ∈ 𝑥 Pred( E , On, 𝑦) ⊆ 𝑥)) | 
| 23 | 22 | pm5.32i 574 | . . . . . . . . . . 11
⊢ ((𝑥 ⊆ On ∧ Tr 𝑥) ↔ (𝑥 ⊆ On ∧ ∀𝑦 ∈ 𝑥 Pred( E , On, 𝑦) ⊆ 𝑥)) | 
| 24 | 5, 15, 23 | 3bitri 297 | . . . . . . . . . 10
⊢ (𝑥 ∈ On ↔ (𝑥 ⊆ On ∧ ∀𝑦 ∈ 𝑥 Pred( E , On, 𝑦) ⊆ 𝑥)) | 
| 25 | 24 | anbi1i 624 | . . . . . . . . 9
⊢ ((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ Pred( E , On, 𝑦)))) ↔ ((𝑥 ⊆ On ∧ ∀𝑦 ∈ 𝑥 Pred( E , On, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ Pred( E , On, 𝑦))))) | 
| 26 |  | onelon 6409 | . . . . . . . . . . . 12
⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ On) | 
| 27 | 18 | reseq2d 5997 | . . . . . . . . . . . . . 14
⊢ (𝑦 ∈ On → (𝑓 ↾ Pred( E , On, 𝑦)) = (𝑓 ↾ 𝑦)) | 
| 28 | 27 | fveq2d 6910 | . . . . . . . . . . . . 13
⊢ (𝑦 ∈ On → (𝐹‘(𝑓 ↾ Pred( E , On, 𝑦))) = (𝐹‘(𝑓 ↾ 𝑦))) | 
| 29 | 28 | eqeq2d 2748 | . . . . . . . . . . . 12
⊢ (𝑦 ∈ On → ((𝑓‘𝑦) = (𝐹‘(𝑓 ↾ Pred( E , On, 𝑦))) ↔ (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))) | 
| 30 | 26, 29 | syl 17 | . . . . . . . . . . 11
⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ 𝑥) → ((𝑓‘𝑦) = (𝐹‘(𝑓 ↾ Pred( E , On, 𝑦))) ↔ (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))) | 
| 31 | 30 | ralbidva 3176 | . . . . . . . . . 10
⊢ (𝑥 ∈ On → (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ Pred( E , On, 𝑦))) ↔ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))) | 
| 32 | 31 | pm5.32i 574 | . . . . . . . . 9
⊢ ((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ Pred( E , On, 𝑦)))) ↔ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))) | 
| 33 | 25, 32 | bitr3i 277 | . . . . . . . 8
⊢ (((𝑥 ⊆ On ∧ ∀𝑦 ∈ 𝑥 Pred( E , On, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ Pred( E , On, 𝑦)))) ↔ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))) | 
| 34 | 33 | anbi2i 623 | . . . . . . 7
⊢ ((𝑓 Fn 𝑥 ∧ ((𝑥 ⊆ On ∧ ∀𝑦 ∈ 𝑥 Pred( E , On, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ Pred( E , On, 𝑦))))) ↔ (𝑓 Fn 𝑥 ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦))))) | 
| 35 |  | an12 645 | . . . . . . 7
⊢ ((𝑓 Fn 𝑥 ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))) ↔ (𝑥 ∈ On ∧ (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦))))) | 
| 36 | 3, 34, 35 | 3bitri 297 | . . . . . 6
⊢ ((𝑓 Fn 𝑥 ∧ (𝑥 ⊆ On ∧ ∀𝑦 ∈ 𝑥 Pred( E , On, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ Pred( E , On, 𝑦)))) ↔ (𝑥 ∈ On ∧ (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦))))) | 
| 37 | 36 | exbii 1848 | . . . . 5
⊢
(∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ On ∧ ∀𝑦 ∈ 𝑥 Pred( E , On, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ Pred( E , On, 𝑦)))) ↔ ∃𝑥(𝑥 ∈ On ∧ (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦))))) | 
| 38 |  | df-rex 3071 | . . . . 5
⊢
(∃𝑥 ∈ On
(𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦))) ↔ ∃𝑥(𝑥 ∈ On ∧ (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦))))) | 
| 39 | 37, 38 | bitr4i 278 | . . . 4
⊢
(∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ On ∧ ∀𝑦 ∈ 𝑥 Pred( E , On, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ Pred( E , On, 𝑦)))) ↔ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))) | 
| 40 | 39 | abbii 2809 | . . 3
⊢ {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ On ∧ ∀𝑦 ∈ 𝑥 Pred( E , On, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ Pred( E , On, 𝑦))))} = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))} | 
| 41 | 40 | unieqi 4919 | . 2
⊢ ∪ {𝑓
∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ On ∧ ∀𝑦 ∈ 𝑥 Pred( E , On, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ Pred( E , On, 𝑦))))} = ∪ {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))} | 
| 42 | 1, 2, 41 | 3eqtri 2769 | 1
⊢
recs(𝐹) = ∪ {𝑓
∣ ∃𝑥 ∈ On
(𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))} |