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 bitrid ( 𝑥 ∈ 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 ( 𝐹 , 𝐴 ) ‘ 𝑥 ) } )