Metamath Proof Explorer

Theorem eltrpred

Description: A class is a transitive predecessor iff it is in some value of the underlying function. This theorem is not meant to be used directly; use trpredpred and trpredmintr instead. (Contributed by Scott Fenton, 28-Apr-2012)

		Ref	Expression
	Assertion	eltrpred	$⊢ Y \in TrPred (R, A, X) \leftrightarrow \exists i \in ω Y \in ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (i)$

Proof

Step	Hyp	Ref	Expression
1		dftrpred2	$⊢ TrPred (R, A, X) = ⋃_{i \in ω} ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (i)$
2	1	eleq2i	$⊢ Y \in TrPred (R, A, X) \leftrightarrow Y \in ⋃_{i \in ω} ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (i)$
3		eliun	$⊢ Y \in ⋃_{i \in ω} ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (i) \leftrightarrow \exists i \in ω Y \in ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (i)$
4	2 3	bitri	$⊢ Y \in TrPred (R, A, X) \leftrightarrow \exists i \in ω Y \in ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (i)$