Theorem rdgellim

Description: Elementhood in a recursive definition at a limit ordinal. (Contributed by ML, 30-Mar-2022)

	Ref	Expression
Assertion	rdgellim	⊢ ( ( ( 𝐵 ∈ On ∧ Lim 𝐵 ) ∧ 𝐶 ∈ 𝐵 ) → ( 𝑋 ∈ ( rec ( 𝐹 , 𝐴 ) ‘ 𝐶 ) → 𝑋 ∈ ( rec ( 𝐹 , 𝐴 ) ‘ 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		fveq2	⊢ ( 𝑦 = 𝐶 → ( rec ( 𝐹 , 𝐴 ) ‘ 𝑦 ) = ( rec ( 𝐹 , 𝐴 ) ‘ 𝐶 ) )
2	1	eleq2d	⊢ ( 𝑦 = 𝐶 → ( 𝑋 ∈ ( rec ( 𝐹 , 𝐴 ) ‘ 𝑦 ) ↔ 𝑋 ∈ ( rec ( 𝐹 , 𝐴 ) ‘ 𝐶 ) ) )
3	2	rspcev	⊢ ( ( 𝐶 ∈ 𝐵 ∧ 𝑋 ∈ ( rec ( 𝐹 , 𝐴 ) ‘ 𝐶 ) ) → ∃ 𝑦 ∈ 𝐵 𝑋 ∈ ( rec ( 𝐹 , 𝐴 ) ‘ 𝑦 ) )
4	3	ex	⊢ ( 𝐶 ∈ 𝐵 → ( 𝑋 ∈ ( rec ( 𝐹 , 𝐴 ) ‘ 𝐶 ) → ∃ 𝑦 ∈ 𝐵 𝑋 ∈ ( rec ( 𝐹 , 𝐴 ) ‘ 𝑦 ) ) )
5		eliun	⊢ ( 𝑋 ∈ ∪ 𝑦 ∈ 𝐵 ( rec ( 𝐹 , 𝐴 ) ‘ 𝑦 ) ↔ ∃ 𝑦 ∈ 𝐵 𝑋 ∈ ( rec ( 𝐹 , 𝐴 ) ‘ 𝑦 ) )
6	4 5	imbitrrdi	⊢ ( 𝐶 ∈ 𝐵 → ( 𝑋 ∈ ( rec ( 𝐹 , 𝐴 ) ‘ 𝐶 ) → 𝑋 ∈ ∪ 𝑦 ∈ 𝐵 ( rec ( 𝐹 , 𝐴 ) ‘ 𝑦 ) ) )
7	6	adantl	⊢ ( ( ( 𝐵 ∈ On ∧ Lim 𝐵 ) ∧ 𝐶 ∈ 𝐵 ) → ( 𝑋 ∈ ( rec ( 𝐹 , 𝐴 ) ‘ 𝐶 ) → 𝑋 ∈ ∪ 𝑦 ∈ 𝐵 ( rec ( 𝐹 , 𝐴 ) ‘ 𝑦 ) ) )
8		rdglim2a	⊢ ( ( 𝐵 ∈ On ∧ Lim 𝐵 ) → ( rec ( 𝐹 , 𝐴 ) ‘ 𝐵 ) = ∪ 𝑦 ∈ 𝐵 ( rec ( 𝐹 , 𝐴 ) ‘ 𝑦 ) )
9	8	eleq2d	⊢ ( ( 𝐵 ∈ On ∧ Lim 𝐵 ) → ( 𝑋 ∈ ( rec ( 𝐹 , 𝐴 ) ‘ 𝐵 ) ↔ 𝑋 ∈ ∪ 𝑦 ∈ 𝐵 ( rec ( 𝐹 , 𝐴 ) ‘ 𝑦 ) ) )
10	9	adantr	⊢ ( ( ( 𝐵 ∈ On ∧ Lim 𝐵 ) ∧ 𝐶 ∈ 𝐵 ) → ( 𝑋 ∈ ( rec ( 𝐹 , 𝐴 ) ‘ 𝐵 ) ↔ 𝑋 ∈ ∪ 𝑦 ∈ 𝐵 ( rec ( 𝐹 , 𝐴 ) ‘ 𝑦 ) ) )
11	7 10	sylibrd	⊢ ( ( ( 𝐵 ∈ On ∧ Lim 𝐵 ) ∧ 𝐶 ∈ 𝐵 ) → ( 𝑋 ∈ ( rec ( 𝐹 , 𝐴 ) ‘ 𝐶 ) → 𝑋 ∈ ( rec ( 𝐹 , 𝐴 ) ‘ 𝐵 ) ) )