Proof of Theorem rdglim2
| Step | Hyp | Ref
| Expression |
| 1 | | rdglim 8466 |
. 2
⊢ ((𝐵 ∈ 𝐶 ∧ Lim 𝐵) → (rec(𝐹, 𝐴)‘𝐵) = ∪ (rec(𝐹, 𝐴) “ 𝐵)) |
| 2 | | dfima3 6081 |
. . . . 5
⊢
(rec(𝐹, 𝐴) “ 𝐵) = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐵 ∧ 〈𝑥, 𝑦〉 ∈ rec(𝐹, 𝐴))} |
| 3 | | df-rex 3071 |
. . . . . . 7
⊢
(∃𝑥 ∈
𝐵 𝑦 = (rec(𝐹, 𝐴)‘𝑥) ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑦 = (rec(𝐹, 𝐴)‘𝑥))) |
| 4 | | limord 6444 |
. . . . . . . . . . 11
⊢ (Lim
𝐵 → Ord 𝐵) |
| 5 | | ordelord 6406 |
. . . . . . . . . . . . 13
⊢ ((Ord
𝐵 ∧ 𝑥 ∈ 𝐵) → Ord 𝑥) |
| 6 | 5 | ex 412 |
. . . . . . . . . . . 12
⊢ (Ord
𝐵 → (𝑥 ∈ 𝐵 → Ord 𝑥)) |
| 7 | | vex 3484 |
. . . . . . . . . . . . 13
⊢ 𝑥 ∈ V |
| 8 | 7 | elon 6393 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ On ↔ Ord 𝑥) |
| 9 | 6, 8 | imbitrrdi 252 |
. . . . . . . . . . 11
⊢ (Ord
𝐵 → (𝑥 ∈ 𝐵 → 𝑥 ∈ On)) |
| 10 | 4, 9 | syl 17 |
. . . . . . . . . 10
⊢ (Lim
𝐵 → (𝑥 ∈ 𝐵 → 𝑥 ∈ On)) |
| 11 | | eqcom 2744 |
. . . . . . . . . . 11
⊢ (𝑦 = (rec(𝐹, 𝐴)‘𝑥) ↔ (rec(𝐹, 𝐴)‘𝑥) = 𝑦) |
| 12 | | rdgfnon 8458 |
. . . . . . . . . . . 12
⊢ rec(𝐹, 𝐴) Fn On |
| 13 | | fnopfvb 6960 |
. . . . . . . . . . . 12
⊢
((rec(𝐹, 𝐴) Fn On ∧ 𝑥 ∈ On) → ((rec(𝐹, 𝐴)‘𝑥) = 𝑦 ↔ 〈𝑥, 𝑦〉 ∈ rec(𝐹, 𝐴))) |
| 14 | 12, 13 | mpan 690 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ On → ((rec(𝐹, 𝐴)‘𝑥) = 𝑦 ↔ 〈𝑥, 𝑦〉 ∈ rec(𝐹, 𝐴))) |
| 15 | 11, 14 | bitrid 283 |
. . . . . . . . . 10
⊢ (𝑥 ∈ On → (𝑦 = (rec(𝐹, 𝐴)‘𝑥) ↔ 〈𝑥, 𝑦〉 ∈ rec(𝐹, 𝐴))) |
| 16 | 10, 15 | syl6 35 |
. . . . . . . . 9
⊢ (Lim
𝐵 → (𝑥 ∈ 𝐵 → (𝑦 = (rec(𝐹, 𝐴)‘𝑥) ↔ 〈𝑥, 𝑦〉 ∈ rec(𝐹, 𝐴)))) |
| 17 | 16 | pm5.32d 577 |
. . . . . . . 8
⊢ (Lim
𝐵 → ((𝑥 ∈ 𝐵 ∧ 𝑦 = (rec(𝐹, 𝐴)‘𝑥)) ↔ (𝑥 ∈ 𝐵 ∧ 〈𝑥, 𝑦〉 ∈ rec(𝐹, 𝐴)))) |
| 18 | 17 | exbidv 1921 |
. . . . . . 7
⊢ (Lim
𝐵 → (∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑦 = (rec(𝐹, 𝐴)‘𝑥)) ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 〈𝑥, 𝑦〉 ∈ rec(𝐹, 𝐴)))) |
| 19 | 3, 18 | bitr2id 284 |
. . . . . 6
⊢ (Lim
𝐵 → (∃𝑥(𝑥 ∈ 𝐵 ∧ 〈𝑥, 𝑦〉 ∈ rec(𝐹, 𝐴)) ↔ ∃𝑥 ∈ 𝐵 𝑦 = (rec(𝐹, 𝐴)‘𝑥))) |
| 20 | 19 | abbidv 2808 |
. . . . 5
⊢ (Lim
𝐵 → {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐵 ∧ 〈𝑥, 𝑦〉 ∈ rec(𝐹, 𝐴))} = {𝑦 ∣ ∃𝑥 ∈ 𝐵 𝑦 = (rec(𝐹, 𝐴)‘𝑥)}) |
| 21 | 2, 20 | eqtrid 2789 |
. . . 4
⊢ (Lim
𝐵 → (rec(𝐹, 𝐴) “ 𝐵) = {𝑦 ∣ ∃𝑥 ∈ 𝐵 𝑦 = (rec(𝐹, 𝐴)‘𝑥)}) |
| 22 | 21 | unieqd 4920 |
. . 3
⊢ (Lim
𝐵 → ∪ (rec(𝐹, 𝐴) “ 𝐵) = ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐵 𝑦 = (rec(𝐹, 𝐴)‘𝑥)}) |
| 23 | 22 | adantl 481 |
. 2
⊢ ((𝐵 ∈ 𝐶 ∧ Lim 𝐵) → ∪
(rec(𝐹, 𝐴) “ 𝐵) = ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐵 𝑦 = (rec(𝐹, 𝐴)‘𝑥)}) |
| 24 | 1, 23 | eqtrd 2777 |
1
⊢ ((𝐵 ∈ 𝐶 ∧ Lim 𝐵) → (rec(𝐹, 𝐴)‘𝐵) = ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐵 𝑦 = (rec(𝐹, 𝐴)‘𝑥)}) |