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 ( ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) → ( rec ( 𝐹 , 𝐴 ) ‘ 𝐵 ) = ∪ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐵 𝑦 = ( rec ( 𝐹 , 𝐴 ) ‘ 𝑥 ) } )

Proof

Step Hyp Ref Expression
1 rdglim ⊢ ( ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) → ( rec ( 𝐹 , 𝐴 ) ‘ 𝐵 ) = ∪ ( rec ( 𝐹 , 𝐴 ) “ 𝐵 ) )
2 dfima3 ⊢ ( rec ( 𝐹 , 𝐴 ) “ 𝐵 ) = { 𝑦 ∣ ∃ 𝑥 ( 𝑥 ∈ 𝐵 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ rec ( 𝐹 , 𝐴 ) ) }
3 df-rex ⊢ ( ∃ 𝑥 ∈ 𝐵 𝑦 = ( rec ( 𝐹 , 𝐴 ) ‘ 𝑥 ) ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐵 ∧ 𝑦 = ( rec ( 𝐹 , 𝐴 ) ‘ 𝑥 ) ) )
4 limord ⊢ ( Lim 𝐵 → Ord 𝐵 )
5 ordelord ⊢ ( ( Ord 𝐵 ∧ 𝑥 ∈ 𝐵 ) → Ord 𝑥 )
6 5 ex ⊢ ( Ord 𝐵 → ( 𝑥 ∈ 𝐵 → Ord 𝑥 ) )
7 vex ⊢ 𝑥 ∈ V
8 7 elon ⊢ ( 𝑥 ∈ On ↔ Ord 𝑥 )
9 6 8 syl6ibr ⊢ ( Ord 𝐵 → ( 𝑥 ∈ 𝐵 → 𝑥 ∈ On ) )
10 4 9 syl ⊢ ( Lim 𝐵 → ( 𝑥 ∈ 𝐵 → 𝑥 ∈ On ) )
11 eqcom ⊢ ( 𝑦 = ( rec ( 𝐹 , 𝐴 ) ‘ 𝑥 ) ↔ ( rec ( 𝐹 , 𝐴 ) ‘ 𝑥 ) = 𝑦 )
12 rdgfnon ⊢ rec ( 𝐹 , 𝐴 ) Fn On
13 fnopfvb ⊢ ( ( rec ( 𝐹 , 𝐴 ) Fn On ∧ 𝑥 ∈ On ) → ( ( rec ( 𝐹 , 𝐴 ) ‘ 𝑥 ) = 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ rec ( 𝐹 , 𝐴 ) ) )
14 12 13 mpan ⊢ ( 𝑥 ∈ On → ( ( rec ( 𝐹 , 𝐴 ) ‘ 𝑥 ) = 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ rec ( 𝐹 , 𝐴 ) ) )
15 11 14 syl5bb ⊢ ( 𝑥 ∈ On → ( 𝑦 = ( rec ( 𝐹 , 𝐴 ) ‘ 𝑥 ) ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ rec ( 𝐹 , 𝐴 ) ) )
16 10 15 syl6 ⊢ ( Lim 𝐵 → ( 𝑥 ∈ 𝐵 → ( 𝑦 = ( rec ( 𝐹 , 𝐴 ) ‘ 𝑥 ) ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ rec ( 𝐹 , 𝐴 ) ) ) )
17 16 pm5.32d ⊢ ( Lim 𝐵 → ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 = ( rec ( 𝐹 , 𝐴 ) ‘ 𝑥 ) ) ↔ ( 𝑥 ∈ 𝐵 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ rec ( 𝐹 , 𝐴 ) ) ) )
18 17 exbidv ⊢ ( Lim 𝐵 → ( ∃ 𝑥 ( 𝑥 ∈ 𝐵 ∧ 𝑦 = ( rec ( 𝐹 , 𝐴 ) ‘ 𝑥 ) ) ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐵 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ rec ( 𝐹 , 𝐴 ) ) ) )
19 3 18 bitr2id ⊢ ( Lim 𝐵 → ( ∃ 𝑥 ( 𝑥 ∈ 𝐵 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ rec ( 𝐹 , 𝐴 ) ) ↔ ∃ 𝑥 ∈ 𝐵 𝑦 = ( rec ( 𝐹 , 𝐴 ) ‘ 𝑥 ) ) )
20 19 abbidv ⊢ ( Lim 𝐵 → { 𝑦 ∣ ∃ 𝑥 ( 𝑥 ∈ 𝐵 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ rec ( 𝐹 , 𝐴 ) ) } = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐵 𝑦 = ( rec ( 𝐹 , 𝐴 ) ‘ 𝑥 ) } )
21 2 20 eqtrid ⊢ ( Lim 𝐵 → ( rec ( 𝐹 , 𝐴 ) “ 𝐵 ) = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐵 𝑦 = ( rec ( 𝐹 , 𝐴 ) ‘ 𝑥 ) } )
22 21 unieqd ⊢ ( Lim 𝐵 → ∪ ( rec ( 𝐹 , 𝐴 ) “ 𝐵 ) = ∪ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐵 𝑦 = ( rec ( 𝐹 , 𝐴 ) ‘ 𝑥 ) } )
23 22 adantl ⊢ ( ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) → ∪ ( rec ( 𝐹 , 𝐴 ) “ 𝐵 ) = ∪ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐵 𝑦 = ( rec ( 𝐹 , 𝐴 ) ‘ 𝑥 ) } )
24 1 23 eqtrd ⊢ ( ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) → ( rec ( 𝐹 , 𝐴 ) ‘ 𝐵 ) = ∪ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐵 𝑦 = ( rec ( 𝐹 , 𝐴 ) ‘ 𝑥 ) } )