dftrpred3g

Description: The transitive predecessors of X are equal to the predecessors of X together with their transitive predecessors. (Contributed by Scott Fenton, 26-Apr-2012) (Revised by Mario Carneiro, 26-Jun-2015)

		Ref	Expression
	Assertion	dftrpred3g	$⊢ (X \in A \land R Se A) \to TrPred (R, A, X) = Pred (R, A, X) \cup ⋃_{y \in Pred (R, A, X)} TrPred (R, A, y)$

Proof

Step	Hyp	Ref	Expression
1		elun	$⊢ z \in (Pred (R, A, X) \cup ⋃_{y \in Pred (R, A, X)} TrPred (R, A, y)) \leftrightarrow (z \in Pred (R, A, X) \lor z \in ⋃_{y \in Pred (R, A, X)} TrPred (R, A, y))$
2		predel	$⊢ z \in Pred (R, A, X) \to z \in A$
3		setlikespec	$⊢ (z \in A \land R Se A) \to Pred (R, A, z) \in V$
4		trpredpred	$⊢ Pred (R, A, z) \in V \to Pred (R, A, z) \subseteq TrPred (R, A, z)$
5	3 4	syl	$⊢ (z \in A \land R Se A) \to Pred (R, A, z) \subseteq TrPred (R, A, z)$
6	5	expcom	$⊢ R Se A \to (z \in A \to Pred (R, A, z) \subseteq TrPred (R, A, z))$
7	6	adantl	$⊢ (X \in A \land R Se A) \to (z \in A \to Pred (R, A, z) \subseteq TrPred (R, A, z))$
8	2 7	syl5	$⊢ (X \in A \land R Se A) \to (z \in Pred (R, A, X) \to Pred (R, A, z) \subseteq TrPred (R, A, z))$
9	8	ancld	$⊢ (X \in A \land R Se A) \to (z \in Pred (R, A, X) \to (z \in Pred (R, A, X) \land Pred (R, A, z) \subseteq TrPred (R, A, z)))$
10		trpredeq3	$⊢ y = z \to TrPred (R, A, y) = TrPred (R, A, z)$
11	10	sseq2d	$⊢ y = z \to (Pred (R, A, z) \subseteq TrPred (R, A, y) \leftrightarrow Pred (R, A, z) \subseteq TrPred (R, A, z))$
12	11	rspcev	$⊢ (z \in Pred (R, A, X) \land Pred (R, A, z) \subseteq TrPred (R, A, z)) \to \exists y \in Pred (R, A, X) Pred (R, A, z) \subseteq TrPred (R, A, y)$
13		ssiun	$⊢ \exists y \in Pred (R, A, X) Pred (R, A, z) \subseteq TrPred (R, A, y) \to Pred (R, A, z) \subseteq ⋃_{y \in Pred (R, A, X)} TrPred (R, A, y)$
14	12 13	syl	$⊢ (z \in Pred (R, A, X) \land Pred (R, A, z) \subseteq TrPred (R, A, z)) \to Pred (R, A, z) \subseteq ⋃_{y \in Pred (R, A, X)} TrPred (R, A, y)$
15	9 14	syl6	$⊢ (X \in A \land R Se A) \to (z \in Pred (R, A, X) \to Pred (R, A, z) \subseteq ⋃_{y \in Pred (R, A, X)} TrPred (R, A, y))$
16		eliun	$⊢ z \in ⋃_{y \in Pred (R, A, X)} TrPred (R, A, y) \leftrightarrow \exists y \in Pred (R, A, X) z \in TrPred (R, A, y)$
17		predel	$⊢ y \in Pred (R, A, X) \to y \in A$
18		setlikespec	$⊢ (y \in A \land R Se A) \to Pred (R, A, y) \in V$
19	18	ancoms	$⊢ (R Se A \land y \in A) \to Pred (R, A, y) \in V$
20	19	adantll	$⊢ ((X \in A \land R Se A) \land y \in A) \to Pred (R, A, y) \in V$
21		trpredss	$⊢ Pred (R, A, y) \in V \to TrPred (R, A, y) \subseteq A$
22	20 21	syl	$⊢ ((X \in A \land R Se A) \land y \in A) \to TrPred (R, A, y) \subseteq A$
23	22	sseld	$⊢ ((X \in A \land R Se A) \land y \in A) \to (z \in TrPred (R, A, y) \to z \in A)$
24	3	expcom	$⊢ R Se A \to (z \in A \to Pred (R, A, z) \in V)$
25	24	ad2antlr	$⊢ ((X \in A \land R Se A) \land y \in A) \to (z \in A \to Pred (R, A, z) \in V)$
26	23 25	syld	$⊢ ((X \in A \land R Se A) \land y \in A) \to (z \in TrPred (R, A, y) \to Pred (R, A, z) \in V)$
27	26	imp	$⊢ (((X \in A \land R Se A) \land y \in A) \land z \in TrPred (R, A, y)) \to Pred (R, A, z) \in V$
28	27 4	syl	$⊢ (((X \in A \land R Se A) \land y \in A) \land z \in TrPred (R, A, y)) \to Pred (R, A, z) \subseteq TrPred (R, A, z)$
29		simpr	$⊢ ((X \in A \land R Se A) \land y \in A) \to y \in A$
30		simplr	$⊢ ((X \in A \land R Se A) \land y \in A) \to R Se A$
31		trpredelss	$⊢ (y \in A \land R Se A) \to (z \in TrPred (R, A, y) \to TrPred (R, A, z) \subseteq TrPred (R, A, y))$
32	29 30 31	syl2anc	$⊢ ((X \in A \land R Se A) \land y \in A) \to (z \in TrPred (R, A, y) \to TrPred (R, A, z) \subseteq TrPred (R, A, y))$
33	32	imp	$⊢ (((X \in A \land R Se A) \land y \in A) \land z \in TrPred (R, A, y)) \to TrPred (R, A, z) \subseteq TrPred (R, A, y)$
34	28 33	sstrd	$⊢ (((X \in A \land R Se A) \land y \in A) \land z \in TrPred (R, A, y)) \to Pred (R, A, z) \subseteq TrPred (R, A, y)$
35	34	exp31	$⊢ (X \in A \land R Se A) \to (y \in A \to (z \in TrPred (R, A, y) \to Pred (R, A, z) \subseteq TrPred (R, A, y)))$
36	17 35	syl5	$⊢ (X \in A \land R Se A) \to (y \in Pred (R, A, X) \to (z \in TrPred (R, A, y) \to Pred (R, A, z) \subseteq TrPred (R, A, y)))$
37	36	reximdvai	$⊢ (X \in A \land R Se A) \to (\exists y \in Pred (R, A, X) z \in TrPred (R, A, y) \to \exists y \in Pred (R, A, X) Pred (R, A, z) \subseteq TrPred (R, A, y))$
38	37 13	syl6	$⊢ (X \in A \land R Se A) \to (\exists y \in Pred (R, A, X) z \in TrPred (R, A, y) \to Pred (R, A, z) \subseteq ⋃_{y \in Pred (R, A, X)} TrPred (R, A, y))$
39	16 38	syl5bi	$⊢ (X \in A \land R Se A) \to (z \in ⋃_{y \in Pred (R, A, X)} TrPred (R, A, y) \to Pred (R, A, z) \subseteq ⋃_{y \in Pred (R, A, X)} TrPred (R, A, y))$
40	15 39	jaod	$⊢ (X \in A \land R Se A) \to ((z \in Pred (R, A, X) \lor z \in ⋃_{y \in Pred (R, A, X)} TrPred (R, A, y)) \to Pred (R, A, z) \subseteq ⋃_{y \in Pred (R, A, X)} TrPred (R, A, y))$
41		ssun4	$⊢ Pred (R, A, z) \subseteq ⋃_{y \in Pred (R, A, X)} TrPred (R, A, y) \to Pred (R, A, z) \subseteq Pred (R, A, X) \cup ⋃_{y \in Pred (R, A, X)} TrPred (R, A, y)$
42	40 41	syl6	$⊢ (X \in A \land R Se A) \to ((z \in Pred (R, A, X) \lor z \in ⋃_{y \in Pred (R, A, X)} TrPred (R, A, y)) \to Pred (R, A, z) \subseteq Pred (R, A, X) \cup ⋃_{y \in Pred (R, A, X)} TrPred (R, A, y))$
43	1 42	syl5bi	$⊢ (X \in A \land R Se A) \to (z \in (Pred (R, A, X) \cup ⋃_{y \in Pred (R, A, X)} TrPred (R, A, y)) \to Pred (R, A, z) \subseteq Pred (R, A, X) \cup ⋃_{y \in Pred (R, A, X)} TrPred (R, A, y))$
44	43	ralrimiv	$⊢ (X \in A \land R Se A) \to \forall z \in (Pred (R, A, X) \cup ⋃_{y \in Pred (R, A, X)} TrPred (R, A, y)) Pred (R, A, z) \subseteq Pred (R, A, X) \cup ⋃_{y \in Pred (R, A, X)} TrPred (R, A, y)$
45		ssun1	$⊢ Pred (R, A, X) \subseteq Pred (R, A, X) \cup ⋃_{y \in Pred (R, A, X)} TrPred (R, A, y)$
46	44 45	jctir	$⊢ (X \in A \land R Se A) \to (\forall z \in (Pred (R, A, X) \cup ⋃_{y \in Pred (R, A, X)} TrPred (R, A, y)) Pred (R, A, z) \subseteq Pred (R, A, X) \cup ⋃_{y \in Pred (R, A, X)} TrPred (R, A, y) \land Pred (R, A, X) \subseteq Pred (R, A, X) \cup ⋃_{y \in Pred (R, A, X)} TrPred (R, A, y))$
47		trpredmintr	$⊢ ((X \in A \land R Se A) \land (\forall z \in (Pred (R, A, X) \cup ⋃_{y \in Pred (R, A, X)} TrPred (R, A, y)) Pred (R, A, z) \subseteq Pred (R, A, X) \cup ⋃_{y \in Pred (R, A, X)} TrPred (R, A, y) \land Pred (R, A, X) \subseteq Pred (R, A, X) \cup ⋃_{y \in Pred (R, A, X)} TrPred (R, A, y))) \to TrPred (R, A, X) \subseteq Pred (R, A, X) \cup ⋃_{y \in Pred (R, A, X)} TrPred (R, A, y)$
48	46 47	mpdan	$⊢ (X \in A \land R Se A) \to TrPred (R, A, X) \subseteq Pred (R, A, X) \cup ⋃_{y \in Pred (R, A, X)} TrPred (R, A, y)$
49		setlikespec	$⊢ (X \in A \land R Se A) \to Pred (R, A, X) \in V$
50		trpredpred	$⊢ Pred (R, A, X) \in V \to Pred (R, A, X) \subseteq TrPred (R, A, X)$
51	49 50	syl	$⊢ (X \in A \land R Se A) \to Pred (R, A, X) \subseteq TrPred (R, A, X)$
52	51	sseld	$⊢ (X \in A \land R Se A) \to (y \in Pred (R, A, X) \to y \in TrPred (R, A, X))$
53		trpredelss	$⊢ (X \in A \land R Se A) \to (y \in TrPred (R, A, X) \to TrPred (R, A, y) \subseteq TrPred (R, A, X))$
54	52 53	syld	$⊢ (X \in A \land R Se A) \to (y \in Pred (R, A, X) \to TrPred (R, A, y) \subseteq TrPred (R, A, X))$
55	54	ralrimiv	$⊢ (X \in A \land R Se A) \to \forall y \in Pred (R, A, X) TrPred (R, A, y) \subseteq TrPred (R, A, X)$
56		iunss	$⊢ ⋃_{y \in Pred (R, A, X)} TrPred (R, A, y) \subseteq TrPred (R, A, X) \leftrightarrow \forall y \in Pred (R, A, X) TrPred (R, A, y) \subseteq TrPred (R, A, X)$
57	55 56	sylibr	$⊢ (X \in A \land R Se A) \to ⋃_{y \in Pred (R, A, X)} TrPred (R, A, y) \subseteq TrPred (R, A, X)$
58	51 57	unssd	$⊢ (X \in A \land R Se A) \to Pred (R, A, X) \cup ⋃_{y \in Pred (R, A, X)} TrPred (R, A, y) \subseteq TrPred (R, A, X)$
59	48 58	eqssd	$⊢ (X \in A \land R Se A) \to TrPred (R, A, X) = Pred (R, A, X) \cup ⋃_{y \in Pred (R, A, X)} TrPred (R, A, y)$

Metamath Proof Explorer

Theorem dftrpred3g

Proof