rdgellim

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

		Ref	Expression
	Assertion	rdgellim	$⊢ ((B \in On \land Lim B) \land C \in B) \to (X \in rec (F, A) (C) \to X \in rec (F, A) (B))$

Step	Hyp	Ref	Expression
1		fveq2	$⊢ y = C \to rec (F, A) (y) = rec (F, A) (C)$
2	1	eleq2d	$⊢ y = C \to (X \in rec (F, A) (y) \leftrightarrow X \in rec (F, A) (C))$
3	2	rspcev	$⊢ (C \in B \land X \in rec (F, A) (C)) \to \exists y \in B X \in rec (F, A) (y)$
4	3	ex	$⊢ C \in B \to (X \in rec (F, A) (C) \to \exists y \in B X \in rec (F, A) (y))$
5		eliun	$⊢ X \in ⋃_{y \in B} rec (F, A) (y) \leftrightarrow \exists y \in B X \in rec (F, A) (y)$
6	4 5	imbitrrdi	$⊢ C \in B \to (X \in rec (F, A) (C) \to X \in ⋃_{y \in B} rec (F, A) (y))$
7	6	adantl	$⊢ ((B \in On \land Lim B) \land C \in B) \to (X \in rec (F, A) (C) \to X \in ⋃_{y \in B} rec (F, A) (y))$
8		rdglim2a	$⊢ (B \in On \land Lim B) \to rec (F, A) (B) = ⋃_{y \in B} rec (F, A) (y)$
9	8	eleq2d	$⊢ (B \in On \land Lim B) \to (X \in rec (F, A) (B) \leftrightarrow X \in ⋃_{y \in B} rec (F, A) (y))$
10	9	adantr	$⊢ ((B \in On \land Lim B) \land C \in B) \to (X \in rec (F, A) (B) \leftrightarrow X \in ⋃_{y \in B} rec (F, A) (y))$
11	7 10	sylibrd	$⊢ ((B \in On \land Lim B) \land C \in B) \to (X \in rec (F, A) (C) \to X \in rec (F, A) (B))$

Metamath Proof Explorer