trpredss

Description: The transitive predecessors form a subclass of the base class. (Contributed by Scott Fenton, 20-Feb-2011)

		Ref	Expression
	Assertion	trpredss	$⊢ Pred (R, A, X) \in B \to TrPred (R, A, X) \subseteq A$

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		trpredlem1	$⊢ Pred (R, A, X) \in B \to ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (i) \subseteq A$
3	2	ralrimivw	$⊢ Pred (R, A, X) \in B \to \forall i \in ω ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (i) \subseteq A$
4		iunss	$⊢ ⋃_{i \in ω} ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (i) \subseteq A \leftrightarrow \forall i \in ω ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (i) \subseteq A$
5	3 4	sylibr	$⊢ Pred (R, A, X) \in B \to ⋃_{i \in ω} ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (i) \subseteq A$
6	1 5	eqsstrid	$⊢ Pred (R, A, X) \in B \to TrPred (R, A, X) \subseteq A$

Metamath Proof Explorer