Metamath Proof Explorer

Theorem rdglim2

Description: The value of the recursive definition generator at a limit ordinal, in terms of the union of all smaller values. (Contributed by NM, 23-Apr-1995)

Ref Expression
Assertion rdglim2 ⊢ B ∈ C ∧ Lim ⁡ B → rec ⁡ F A ⁡ B = ⋃ y | ∃ x ∈ B y = rec ⁡ F A ⁡ x

Proof

Step Hyp Ref Expression
1 rdglim ⊢ B ∈ C ∧ Lim ⁡ B → rec ⁡ F A ⁡ B = ⋃ rec ⁡ F A B
2 dfima3 ⊢ rec ⁡ F A B = y | ∃ x x ∈ B ∧ x y ∈ rec ⁡ F A
3 df-rex ⊢ ∃ x ∈ B y = rec ⁡ F A ⁡ x ↔ ∃ x x ∈ B ∧ y = rec ⁡ F A ⁡ x
4 limord ⊢ Lim ⁡ B → Ord ⁡ B
5 ordelord ⊢ Ord ⁡ B ∧ x ∈ B → Ord ⁡ x
6 5 ex ⊢ Ord ⁡ B → x ∈ B → Ord ⁡ x
7 vex ⊢ x ∈ V
8 7 elon ⊢ x ∈ On ↔ Ord ⁡ x
9 6 8 syl6ibr ⊢ Ord ⁡ B → x ∈ B → x ∈ On
10 4 9 syl ⊢ Lim ⁡ B → x ∈ B → x ∈ On
11 eqcom ⊢ y = rec ⁡ F A ⁡ x ↔ rec ⁡ F A ⁡ x = y
12 rdgfnon ⊢ rec ⁡ F A Fn On
13 fnopfvb ⊢ rec ⁡ F A Fn On ∧ x ∈ On → rec ⁡ F A ⁡ x = y ↔ x y ∈ rec ⁡ F A
14 12 13 mpan ⊢ x ∈ On → rec ⁡ F A ⁡ x = y ↔ x y ∈ rec ⁡ F A
15 11 14 syl5bb ⊢ x ∈ On → y = rec ⁡ F A ⁡ x ↔ x y ∈ rec ⁡ F A
16 10 15 syl6 ⊢ Lim ⁡ B → x ∈ B → y = rec ⁡ F A ⁡ x ↔ x y ∈ rec ⁡ F A
17 16 pm5.32d ⊢ Lim ⁡ B → x ∈ B ∧ y = rec ⁡ F A ⁡ x ↔ x ∈ B ∧ x y ∈ rec ⁡ F A
18 17 exbidv ⊢ Lim ⁡ B → ∃ x x ∈ B ∧ y = rec ⁡ F A ⁡ x ↔ ∃ x x ∈ B ∧ x y ∈ rec ⁡ F A
19 3 18 bitr2id ⊢ Lim ⁡ B → ∃ x x ∈ B ∧ x y ∈ rec ⁡ F A ↔ ∃ x ∈ B y = rec ⁡ F A ⁡ x
20 19 abbidv ⊢ Lim ⁡ B → y | ∃ x x ∈ B ∧ x y ∈ rec ⁡ F A = y | ∃ x ∈ B y = rec ⁡ F A ⁡ x
21 2 20 eqtrid ⊢ Lim ⁡ B → rec ⁡ F A B = y | ∃ x ∈ B y = rec ⁡ F A ⁡ x
22 21 unieqd ⊢ Lim ⁡ B → ⋃ rec ⁡ F A B = ⋃ y | ∃ x ∈ B y = rec ⁡ F A ⁡ x
23 22 adantl ⊢ B ∈ C ∧ Lim ⁡ B → ⋃ rec ⁡ F A B = ⋃ y | ∃ x ∈ B y = rec ⁡ F A ⁡ x
24 1 23 eqtrd ⊢ B ∈ C ∧ Lim ⁡ B → rec ⁡ F A ⁡ B = ⋃ y | ∃ x ∈ B y = rec ⁡ F A ⁡ x