trpredtr

Description: Predecessors of a transitive predecessor are transitive predecessors. (Contributed by Scott Fenton, 20-Feb-2011) (Revised by Mario Carneiro, 26-Jun-2015)

		Ref	Expression
	Assertion	trpredtr	$⊢ (X \in A \land R Se A) \to (Y \in TrPred (R, A, X) \to Pred (R, A, Y) \subseteq TrPred (R, A, X))$

Proof

Step	Hyp	Ref	Expression
1		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)$
2		simplr	$⊢ (((X \in A \land R Se A) \land i \in ω) \land Y \in ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (i)) \to i \in ω$
3		peano2	$⊢ i \in ω \to suc i \in ω$
4	2 3	syl	$⊢ (((X \in A \land R Se A) \land i \in ω) \land Y \in ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (i)) \to suc i \in ω$
5		simpr	$⊢ (((X \in A \land R Se A) \land i \in ω) \land Y \in ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (i)) \to Y \in ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (i)$
6		ssid	$⊢ Pred (R, A, Y) \subseteq Pred (R, A, Y)$
7		predeq3	$⊢ t = Y \to Pred (R, A, t) = Pred (R, A, Y)$
8	7	sseq2d	$⊢ t = Y \to (Pred (R, A, Y) \subseteq Pred (R, A, t) \leftrightarrow Pred (R, A, Y) \subseteq Pred (R, A, Y))$
9	8	rspcev	$⊢ (Y \in ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (i) \land Pred (R, A, Y) \subseteq Pred (R, A, Y)) \to \exists t \in ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (i) Pred (R, A, Y) \subseteq Pred (R, A, t)$
10		ssiun	$⊢ \exists t \in ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (i) Pred (R, A, Y) \subseteq Pred (R, A, t) \to Pred (R, A, Y) \subseteq ⋃_{t \in ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (i)} Pred (R, A, t)$
11	9 10	syl	$⊢ (Y \in ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (i) \land Pred (R, A, Y) \subseteq Pred (R, A, Y)) \to Pred (R, A, Y) \subseteq ⋃_{t \in ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (i)} Pred (R, A, t)$
12	5 6 11	sylancl	$⊢ (((X \in A \land R Se A) \land i \in ω) \land Y \in ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (i)) \to Pred (R, A, Y) \subseteq ⋃_{t \in ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (i)} Pred (R, A, t)$
13		fvex	$⊢ ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (i) \in V$
14		setlikespec	$⊢ (X \in A \land R Se A) \to Pred (R, A, X) \in V$
15		trpredlem1	$⊢ Pred (R, A, X) \in V \to ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (i) \subseteq A$
16	14 15	syl	$⊢ (X \in A \land R Se A) \to ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (i) \subseteq A$
17	16	sseld	$⊢ (X \in A \land R Se A) \to (t \in ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (i) \to t \in A)$
18		setlikespec	$⊢ (t \in A \land R Se A) \to Pred (R, A, t) \in V$
19	18	expcom	$⊢ R Se A \to (t \in A \to Pred (R, A, t) \in V)$
20	19	adantl	$⊢ (X \in A \land R Se A) \to (t \in A \to Pred (R, A, t) \in V)$
21	17 20	syld	$⊢ (X \in A \land R Se A) \to (t \in ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (i) \to Pred (R, A, t) \in V)$
22	21	ralrimiv	$⊢ (X \in A \land R Se A) \to \forall t \in ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (i) Pred (R, A, t) \in V$
23	22	ad2antrr	$⊢ (((X \in A \land R Se A) \land i \in ω) \land Y \in ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (i)) \to \forall t \in ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (i) Pred (R, A, t) \in V$
24		iunexg	$⊢ (({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (i) \in V \land \forall t \in ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (i) Pred (R, A, t) \in V) \to ⋃_{t \in ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (i)} Pred (R, A, t) \in V$
25	13 23 24	sylancr	$⊢ (((X \in A \land R Se A) \land i \in ω) \land Y \in ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (i)) \to ⋃_{t \in ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (i)} Pred (R, A, t) \in V$
26		nfcv	$⊢ \underline{Ⅎ} f Pred (R, A, X)$
27		nfcv	$⊢ \underline{Ⅎ} f i$
28		nfcv	$⊢ \underline{Ⅎ} f ⋃_{t \in ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (i)} Pred (R, A, t)$
29		predeq3	$⊢ y = t \to Pred (R, A, y) = Pred (R, A, t)$
30	29	cbviunv	$⊢ ⋃_{y \in a} Pred (R, A, y) = ⋃_{t \in a} Pred (R, A, t)$
31		iuneq1	$⊢ a = f \to ⋃_{t \in a} Pred (R, A, t) = ⋃_{t \in f} Pred (R, A, t)$
32	30 31	eqtrid	$⊢ a = f \to ⋃_{y \in a} Pred (R, A, y) = ⋃_{t \in f} Pred (R, A, t)$
33	32	cbvmptv	$⊢ (a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)) = (f \in V ⟼ ⋃_{t \in f} Pred (R, A, t))$
34		rdgeq1	$⊢ (a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)) = (f \in V ⟼ ⋃_{t \in f} Pred (R, A, t)) \to rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) = rec ((f \in V ⟼ ⋃_{t \in f} Pred (R, A, t)), Pred (R, A, X))$
35		reseq1	$⊢ rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) = rec ((f \in V ⟼ ⋃_{t \in f} Pred (R, A, t)), Pred (R, A, X)) \to {rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω} = {rec ((f \in V ⟼ ⋃_{t \in f} Pred (R, A, t)), Pred (R, A, X)) ↾}_{ω}$
36	33 34 35	mp2b	$⊢ {rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω} = {rec ((f \in V ⟼ ⋃_{t \in f} Pred (R, A, t)), Pred (R, A, X)) ↾}_{ω}$
37		iuneq1	$⊢ f = ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (i) \to ⋃_{t \in f} Pred (R, A, t) = ⋃_{t \in ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (i)} Pred (R, A, t)$
38	26 27 28 36 37	frsucmpt	$⊢ (i \in ω \land ⋃_{t \in ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (i)} Pred (R, A, t) \in V) \to ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (suc i) = ⋃_{t \in ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (i)} Pred (R, A, t)$
39	2 25 38	syl2anc	$⊢ (((X \in A \land R Se A) \land i \in ω) \land Y \in ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (i)) \to ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (suc i) = ⋃_{t \in ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (i)} Pred (R, A, t)$
40	12 39	sseqtrrd	$⊢ (((X \in A \land R Se A) \land i \in ω) \land Y \in ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (i)) \to Pred (R, A, Y) \subseteq ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (suc i)$
41		fveq2	$⊢ j = suc i \to ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (j) = ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (suc i)$
42	41	sseq2d	$⊢ j = suc i \to (Pred (R, A, Y) \subseteq ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (j) \leftrightarrow Pred (R, A, Y) \subseteq ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (suc i))$
43	42	rspcev	$⊢ (suc i \in ω \land Pred (R, A, Y) \subseteq ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (suc i)) \to \exists j \in ω Pred (R, A, Y) \subseteq ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (j)$
44		ssiun	$⊢ \exists j \in ω Pred (R, A, Y) \subseteq ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (j) \to Pred (R, A, Y) \subseteq ⋃_{j \in ω} ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (j)$
45	43 44	syl	$⊢ (suc i \in ω \land Pred (R, A, Y) \subseteq ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (suc i)) \to Pred (R, A, Y) \subseteq ⋃_{j \in ω} ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (j)$
46		dftrpred2	$⊢ TrPred (R, A, X) = ⋃_{j \in ω} ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (j)$
47	45 46	sseqtrrdi	$⊢ (suc i \in ω \land Pred (R, A, Y) \subseteq ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (suc i)) \to Pred (R, A, Y) \subseteq TrPred (R, A, X)$
48	4 40 47	syl2anc	$⊢ (((X \in A \land R Se A) \land i \in ω) \land Y \in ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (i)) \to Pred (R, A, Y) \subseteq TrPred (R, A, X)$
49	48	rexlimdva2	$⊢ (X \in A \land R Se A) \to (\exists i \in ω Y \in ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (i) \to Pred (R, A, Y) \subseteq TrPred (R, A, X))$
50	1 49	syl5bi	$⊢ (X \in A \land R Se A) \to (Y \in TrPred (R, A, X) \to Pred (R, A, Y) \subseteq TrPred (R, A, X))$

Metamath Proof Explorer

Theorem trpredtr

Proof