Proof of Theorem dfrecs3
Step | Hyp | Ref
| Expression |
1 | | df-recs 7355 |
. 2
⊢
recs(𝐹) = wrecs( E ,
On, 𝐹) |
2 | | df-wrecs 7294 |
. 2
⊢ wrecs( E
, On, 𝐹) = ∪ {𝑓
∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ On ∧ ∀𝑦 ∈ 𝑥 Pred( E , On, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ Pred( E , On, 𝑦))))} |
3 | | 3anass 1035 |
. . . . . . 7
⊢ ((𝑓 Fn 𝑥 ∧ (𝑥 ⊆ On ∧ ∀𝑦 ∈ 𝑥 Pred( E , On, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ Pred( E , On, 𝑦)))) ↔ (𝑓 Fn 𝑥 ∧ ((𝑥 ⊆ On ∧ ∀𝑦 ∈ 𝑥 Pred( E , On, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ Pred( E , On, 𝑦)))))) |
4 | | vex 3176 |
. . . . . . . . . . . 12
⊢ 𝑥 ∈ V |
5 | 4 | elon 5649 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ On ↔ Ord 𝑥) |
6 | | ordsson 6881 |
. . . . . . . . . . . . 13
⊢ (Ord
𝑥 → 𝑥 ⊆ On) |
7 | | ordtr 5654 |
. . . . . . . . . . . . 13
⊢ (Ord
𝑥 → Tr 𝑥) |
8 | 6, 7 | jca 553 |
. . . . . . . . . . . 12
⊢ (Ord
𝑥 → (𝑥 ⊆ On ∧ Tr 𝑥)) |
9 | | epweon 6875 |
. . . . . . . . . . . . . . . 16
⊢ E We
On |
10 | | wess 5025 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ⊆ On → ( E We On
→ E We 𝑥)) |
11 | 9, 10 | mpi 20 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ⊆ On → E We 𝑥) |
12 | 11 | anim2i 591 |
. . . . . . . . . . . . . 14
⊢ ((Tr
𝑥 ∧ 𝑥 ⊆ On) → (Tr 𝑥 ∧ E We 𝑥)) |
13 | 12 | ancoms 468 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ⊆ On ∧ Tr 𝑥) → (Tr 𝑥 ∧ E We 𝑥)) |
14 | | df-ord 5643 |
. . . . . . . . . . . . 13
⊢ (Ord
𝑥 ↔ (Tr 𝑥 ∧ E We 𝑥)) |
15 | 13, 14 | sylibr 223 |
. . . . . . . . . . . 12
⊢ ((𝑥 ⊆ On ∧ Tr 𝑥) → Ord 𝑥) |
16 | 8, 15 | impbii 198 |
. . . . . . . . . . 11
⊢ (Ord
𝑥 ↔ (𝑥 ⊆ On ∧ Tr 𝑥)) |
17 | | ssel2 3563 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ⊆ On ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ On) |
18 | | predon 6883 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ On → Pred( E , On,
𝑦) = 𝑦) |
19 | 18 | sseq1d 3595 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ On → (Pred( E , On,
𝑦) ⊆ 𝑥 ↔ 𝑦 ⊆ 𝑥)) |
20 | 17, 19 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ⊆ On ∧ 𝑦 ∈ 𝑥) → (Pred( E , On, 𝑦) ⊆ 𝑥 ↔ 𝑦 ⊆ 𝑥)) |
21 | 20 | ralbidva 2968 |
. . . . . . . . . . . . 13
⊢ (𝑥 ⊆ On →
(∀𝑦 ∈ 𝑥 Pred( E , On, 𝑦) ⊆ 𝑥 ↔ ∀𝑦 ∈ 𝑥 𝑦 ⊆ 𝑥)) |
22 | | dftr3 4684 |
. . . . . . . . . . . . 13
⊢ (Tr 𝑥 ↔ ∀𝑦 ∈ 𝑥 𝑦 ⊆ 𝑥) |
23 | 21, 22 | syl6rbbr 278 |
. . . . . . . . . . . 12
⊢ (𝑥 ⊆ On → (Tr 𝑥 ↔ ∀𝑦 ∈ 𝑥 Pred( E , On, 𝑦) ⊆ 𝑥)) |
24 | 23 | pm5.32i 667 |
. . . . . . . . . . 11
⊢ ((𝑥 ⊆ On ∧ Tr 𝑥) ↔ (𝑥 ⊆ On ∧ ∀𝑦 ∈ 𝑥 Pred( E , On, 𝑦) ⊆ 𝑥)) |
25 | 5, 16, 24 | 3bitri 285 |
. . . . . . . . . 10
⊢ (𝑥 ∈ On ↔ (𝑥 ⊆ On ∧ ∀𝑦 ∈ 𝑥 Pred( E , On, 𝑦) ⊆ 𝑥)) |
26 | 25 | anbi1i 727 |
. . . . . . . . 9
⊢ ((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ Pred( E , On, 𝑦)))) ↔ ((𝑥 ⊆ On ∧ ∀𝑦 ∈ 𝑥 Pred( E , On, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ Pred( E , On, 𝑦))))) |
27 | | onelon 5665 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ On) |
28 | 18 | reseq2d 5317 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ On → (𝑓 ↾ Pred( E , On, 𝑦)) = (𝑓 ↾ 𝑦)) |
29 | 28 | fveq2d 6107 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ On → (𝐹‘(𝑓 ↾ Pred( E , On, 𝑦))) = (𝐹‘(𝑓 ↾ 𝑦))) |
30 | 29 | eqeq2d 2620 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ On → ((𝑓‘𝑦) = (𝐹‘(𝑓 ↾ Pred( E , On, 𝑦))) ↔ (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))) |
31 | 27, 30 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ 𝑥) → ((𝑓‘𝑦) = (𝐹‘(𝑓 ↾ Pred( E , On, 𝑦))) ↔ (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))) |
32 | 31 | ralbidva 2968 |
. . . . . . . . . 10
⊢ (𝑥 ∈ On → (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ Pred( E , On, 𝑦))) ↔ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))) |
33 | 32 | pm5.32i 667 |
. . . . . . . . 9
⊢ ((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ Pred( E , On, 𝑦)))) ↔ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))) |
34 | 26, 33 | bitr3i 265 |
. . . . . . . 8
⊢ (((𝑥 ⊆ On ∧ ∀𝑦 ∈ 𝑥 Pred( E , On, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ Pred( E , On, 𝑦)))) ↔ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))) |
35 | 34 | anbi2i 726 |
. . . . . . 7
⊢ ((𝑓 Fn 𝑥 ∧ ((𝑥 ⊆ On ∧ ∀𝑦 ∈ 𝑥 Pred( E , On, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ Pred( E , On, 𝑦))))) ↔ (𝑓 Fn 𝑥 ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦))))) |
36 | | an12 834 |
. . . . . . 7
⊢ ((𝑓 Fn 𝑥 ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))) ↔ (𝑥 ∈ On ∧ (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦))))) |
37 | 3, 35, 36 | 3bitri 285 |
. . . . . 6
⊢ ((𝑓 Fn 𝑥 ∧ (𝑥 ⊆ On ∧ ∀𝑦 ∈ 𝑥 Pred( E , On, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ Pred( E , On, 𝑦)))) ↔ (𝑥 ∈ On ∧ (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦))))) |
38 | 37 | exbii 1764 |
. . . . 5
⊢
(∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ On ∧ ∀𝑦 ∈ 𝑥 Pred( E , On, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ Pred( E , On, 𝑦)))) ↔ ∃𝑥(𝑥 ∈ On ∧ (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦))))) |
39 | | df-rex 2902 |
. . . . 5
⊢
(∃𝑥 ∈ On
(𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦))) ↔ ∃𝑥(𝑥 ∈ On ∧ (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦))))) |
40 | 38, 39 | bitr4i 266 |
. . . 4
⊢
(∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ On ∧ ∀𝑦 ∈ 𝑥 Pred( E , On, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ Pred( E , On, 𝑦)))) ↔ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))) |
41 | 40 | abbii 2726 |
. . 3
⊢ {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ On ∧ ∀𝑦 ∈ 𝑥 Pred( E , On, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ Pred( E , On, 𝑦))))} = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))} |
42 | 41 | unieqi 4381 |
. 2
⊢ ∪ {𝑓
∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ On ∧ ∀𝑦 ∈ 𝑥 Pred( E , On, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ Pred( E , On, 𝑦))))} = ∪ {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))} |
43 | 1, 2, 42 | 3eqtri 2636 |
1
⊢
recs(𝐹) = ∪ {𝑓
∣ ∃𝑥 ∈ On
(𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))} |