Metamath Proof Explorer

Theorem trpredex

Description: The transitive predecessors of a relation form a set (NOTE: this is the first theorem in the transitive predecessor series that requires infinity). (Contributed by Scott Fenton, 18-Feb-2011)

		Ref	Expression
	Assertion	trpredex	$⊢ TrPred (R, A, X) \in V$

Proof

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		omex	$⊢ ω \in V$
4		fnex	$⊢ (({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) Fn ω \land ω \in V) \to {rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω} \in V$
5	2 3 4	mp2an	$⊢ {rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω} \in V$
6	5	rnex	$⊢ ran ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) \in V$
7	6	uniex	$⊢ ⋃ ran ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) \in V$
8	1 7	eqeltri	$⊢ TrPred (R, A, X) \in V$