Metamath Proof Explorer

Theorem trpredpred

Description: Assuming it exists, the predecessor class is a subset of the transitive predecessors. (Contributed by Scott Fenton, 18-Feb-2011)

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

Proof

Step	Hyp	Ref	Expression
1		fr0g	$⊢ Pred (R, A, X) \in B \to ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (\emptyset) = Pred (R, A, X)$
2		frfnom	$⊢ ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) Fn ω$
3		peano1	$⊢ \emptyset \in ω$
4		fnbrfvb	$⊢ (({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) Fn ω \land \emptyset \in ω) \to (({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (\emptyset) = Pred (R, A, X) \leftrightarrow \emptyset ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) Pred (R, A, X))$
5	2 3 4	mp2an	$⊢ ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (\emptyset) = Pred (R, A, X) \leftrightarrow \emptyset ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) Pred (R, A, X)$
6	1 5	sylib	$⊢ Pred (R, A, X) \in B \to \emptyset ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) Pred (R, A, X)$
7		0ex	$⊢ \emptyset \in V$
8		breq1	$⊢ z = \emptyset \to (z ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) Pred (R, A, X) \leftrightarrow \emptyset ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) Pred (R, A, X))$
9	7 8	spcev	$⊢ \emptyset ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) Pred (R, A, X) \to \exists z z ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) Pred (R, A, X)$
10	6 9	syl	$⊢ Pred (R, A, X) \in B \to \exists z z ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) Pred (R, A, X)$
11		elrng	$⊢ Pred (R, A, X) \in B \to (Pred (R, A, X) \in ran ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) \leftrightarrow \exists z z ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) Pred (R, A, X))$
12	10 11	mpbird	$⊢ Pred (R, A, X) \in B \to Pred (R, A, X) \in ran ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω})$
13		elssuni	$⊢ Pred (R, A, X) \in ran ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) \to Pred (R, A, X) \subseteq ⋃ ran ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω})$
14	12 13	syl	$⊢ Pred (R, A, X) \in B \to Pred (R, A, X) \subseteq ⋃ ran ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω})$
15		df-trpred	$⊢ TrPred (R, A, X) = ⋃ ran ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω})$
16	14 15	sseqtrrdi	$⊢ Pred (R, A, X) \in B \to Pred (R, A, X) \subseteq TrPred (R, A, X)$