dftrpred2

Description: A definition of the transitive predecessors of a class in terms of indexed union. (Contributed by Scott Fenton, 28-Apr-2012)

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

Step	Hyp	Ref	Expression
1		df-trpred	$⊢ TrPred (R, A, X) = ⋃ ran ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω})$
2		frfnom	$⊢ ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) Fn ω$
3		fniunfv	$⊢ ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) Fn ω \to ⋃_{i \in ω} ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (i) = ⋃ ran ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω})$
4	2 3	ax-mp	$⊢ ⋃_{i \in ω} ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (i) = ⋃ ran ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω})$
5	1 4	eqtr4i	$⊢ TrPred (R, A, X) = ⋃_{i \in ω} ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (i)$

Metamath Proof Explorer