trpredmintr

Description: The transitive predecessors form the smallest class transitive in R and A . That is, if B is another R , A transitive class containing Pred ( R , A , X ) , then TrPred ( R , A , X ) C_ B (Contributed by Scott Fenton, 25-Apr-2012) (Revised by Mario Carneiro, 26-Jun-2015)

		Ref	Expression
	Assertion	trpredmintr	$⊢ ((X \in A \land R Se A) \land (\forall y \in B Pred (R, A, y) \subseteq B \land Pred (R, A, X) \subseteq B)) \to TrPred (R, A, X) \subseteq B$

Proof

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		fveq2	$⊢ j = \emptyset \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)) ↾}_{ω}) (\emptyset)$
3	2	sseq1d	$⊢ j = \emptyset \to (({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (j) \subseteq B \leftrightarrow ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (\emptyset) \subseteq B)$
4	3	imbi2d	$⊢ j = \emptyset \to ((((X \in A \land R Se A) \land (\forall y \in B Pred (R, A, y) \subseteq B \land Pred (R, A, X) \subseteq B)) \to ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (j) \subseteq B) \leftrightarrow (((X \in A \land R Se A) \land (\forall y \in B Pred (R, A, y) \subseteq B \land Pred (R, A, X) \subseteq B)) \to ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (\emptyset) \subseteq B))$
5		fveq2	$⊢ j = k \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)) ↾}_{ω}) (k)$
6	5	sseq1d	$⊢ j = k \to (({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (j) \subseteq B \leftrightarrow ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (k) \subseteq B)$
7	6	imbi2d	$⊢ j = k \to ((((X \in A \land R Se A) \land (\forall y \in B Pred (R, A, y) \subseteq B \land Pred (R, A, X) \subseteq B)) \to ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (j) \subseteq B) \leftrightarrow (((X \in A \land R Se A) \land (\forall y \in B Pred (R, A, y) \subseteq B \land Pred (R, A, X) \subseteq B)) \to ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (k) \subseteq B))$
8		fveq2	$⊢ j = suc k \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 k)$
9	8	sseq1d	$⊢ j = suc k \to (({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (j) \subseteq B \leftrightarrow ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (suc k) \subseteq B)$
10	9	imbi2d	$⊢ j = suc k \to ((((X \in A \land R Se A) \land (\forall y \in B Pred (R, A, y) \subseteq B \land Pred (R, A, X) \subseteq B)) \to ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (j) \subseteq B) \leftrightarrow (((X \in A \land R Se A) \land (\forall y \in B Pred (R, A, y) \subseteq B \land Pred (R, A, X) \subseteq B)) \to ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (suc k) \subseteq B))$
11		fveq2	$⊢ j = 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)) ↾}_{ω}) (i)$
12	11	sseq1d	$⊢ j = i \to (({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (j) \subseteq B \leftrightarrow ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (i) \subseteq B)$
13	12	imbi2d	$⊢ j = i \to ((((X \in A \land R Se A) \land (\forall y \in B Pred (R, A, y) \subseteq B \land Pred (R, A, X) \subseteq B)) \to ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (j) \subseteq B) \leftrightarrow (((X \in A \land R Se A) \land (\forall y \in B Pred (R, A, y) \subseteq B \land Pred (R, A, X) \subseteq B)) \to ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (i) \subseteq B))$
14		setlikespec	$⊢ (X \in A \land R Se A) \to Pred (R, A, X) \in V$
15		fr0g	$⊢ Pred (R, A, X) \in V \to ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (\emptyset) = Pred (R, A, X)$
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)) ↾}_{ω}) (\emptyset) = Pred (R, A, X)$
17	16	adantr	$⊢ ((X \in A \land R Se A) \land (\forall y \in B Pred (R, A, y) \subseteq B \land Pred (R, A, X) \subseteq B)) \to ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (\emptyset) = Pred (R, A, X)$
18		simprr	$⊢ ((X \in A \land R Se A) \land (\forall y \in B Pred (R, A, y) \subseteq B \land Pred (R, A, X) \subseteq B)) \to Pred (R, A, X) \subseteq B$
19	17 18	eqsstrd	$⊢ ((X \in A \land R Se A) \land (\forall y \in B Pred (R, A, y) \subseteq B \land Pred (R, A, X) \subseteq B)) \to ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (\emptyset) \subseteq B$
20		fvex	$⊢ ({rec ((c \in V ⟼ ⋃_{d \in c} Pred (R, A, d)), Pred (R, A, X)) ↾}_{ω}) (k) \in V$
21		trpredlem1	$⊢ Pred (R, A, X) \in V \to ({rec ((c \in V ⟼ ⋃_{d \in c} Pred (R, A, d)), Pred (R, A, X)) ↾}_{ω}) (k) \subseteq A$
22	14 21	syl	$⊢ (X \in A \land R Se A) \to ({rec ((c \in V ⟼ ⋃_{d \in c} Pred (R, A, d)), Pred (R, A, X)) ↾}_{ω}) (k) \subseteq A$
23	22	sseld	$⊢ (X \in A \land R Se A) \to (y \in ({rec ((c \in V ⟼ ⋃_{d \in c} Pred (R, A, d)), Pred (R, A, X)) ↾}_{ω}) (k) \to y \in A)$
24		setlikespec	$⊢ (y \in A \land R Se A) \to Pred (R, A, y) \in V$
25	24	expcom	$⊢ R Se A \to (y \in A \to Pred (R, A, y) \in V)$
26	25	adantl	$⊢ (X \in A \land R Se A) \to (y \in A \to Pred (R, A, y) \in V)$
27	23 26	syld	$⊢ (X \in A \land R Se A) \to (y \in ({rec ((c \in V ⟼ ⋃_{d \in c} Pred (R, A, d)), Pred (R, A, X)) ↾}_{ω}) (k) \to Pred (R, A, y) \in V)$
28	27	ralrimiv	$⊢ (X \in A \land R Se A) \to \forall y \in ({rec ((c \in V ⟼ ⋃_{d \in c} Pred (R, A, d)), Pred (R, A, X)) ↾}_{ω}) (k) Pred (R, A, y) \in V$
29	28	ad2antrr	$⊢ (((X \in A \land R Se A) \land (\forall y \in B Pred (R, A, y) \subseteq B \land Pred (R, A, X) \subseteq B)) \land ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (k) \subseteq B) \to \forall y \in ({rec ((c \in V ⟼ ⋃_{d \in c} Pred (R, A, d)), Pred (R, A, X)) ↾}_{ω}) (k) Pred (R, A, y) \in V$
30		iunexg	$⊢ (({rec ((c \in V ⟼ ⋃_{d \in c} Pred (R, A, d)), Pred (R, A, X)) ↾}_{ω}) (k) \in V \land \forall y \in ({rec ((c \in V ⟼ ⋃_{d \in c} Pred (R, A, d)), Pred (R, A, X)) ↾}_{ω}) (k) Pred (R, A, y) \in V) \to ⋃_{y \in ({rec ((c \in V ⟼ ⋃_{d \in c} Pred (R, A, d)), Pred (R, A, X)) ↾}_{ω}) (k)} Pred (R, A, y) \in V$
31	20 29 30	sylancr	$⊢ (((X \in A \land R Se A) \land (\forall y \in B Pred (R, A, y) \subseteq B \land Pred (R, A, X) \subseteq B)) \land ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (k) \subseteq B) \to ⋃_{y \in ({rec ((c \in V ⟼ ⋃_{d \in c} Pred (R, A, d)), Pred (R, A, X)) ↾}_{ω}) (k)} Pred (R, A, y) \in V$
32		nfcv	$⊢ \underline{Ⅎ} a Pred (R, A, X)$
33		nfcv	$⊢ \underline{Ⅎ} a k$
34		nfcv	$⊢ \underline{Ⅎ} a ⋃_{y \in ({rec ((c \in V ⟼ ⋃_{d \in c} Pred (R, A, d)), Pred (R, A, X)) ↾}_{ω}) (k)} Pred (R, A, y)$
35		eqid	$⊢ {rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω} = {rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}$
36		predeq3	$⊢ y = d \to Pred (R, A, y) = Pred (R, A, d)$
37	36	cbviunv	$⊢ ⋃_{y \in a} Pred (R, A, y) = ⋃_{d \in a} Pred (R, A, d)$
38		iuneq1	$⊢ a = c \to ⋃_{d \in a} Pred (R, A, d) = ⋃_{d \in c} Pred (R, A, d)$
39	37 38	syl5eq	$⊢ a = c \to ⋃_{y \in a} Pred (R, A, y) = ⋃_{d \in c} Pred (R, A, d)$
40	39	cbvmptv	$⊢ (a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)) = (c \in V ⟼ ⋃_{d \in c} Pred (R, A, d))$
41		rdgeq1	$⊢ (a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)) = (c \in V ⟼ ⋃_{d \in c} Pred (R, A, d)) \to rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) = rec ((c \in V ⟼ ⋃_{d \in c} Pred (R, A, d)), Pred (R, A, X))$
42		reseq1	$⊢ rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) = rec ((c \in V ⟼ ⋃_{d \in c} Pred (R, A, d)), Pred (R, A, X)) \to {rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω} = {rec ((c \in V ⟼ ⋃_{d \in c} Pred (R, A, d)), Pred (R, A, X)) ↾}_{ω}$
43	40 41 42	mp2b	$⊢ {rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω} = {rec ((c \in V ⟼ ⋃_{d \in c} Pred (R, A, d)), Pred (R, A, X)) ↾}_{ω}$
44	43	fveq1i	$⊢ ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (k) = ({rec ((c \in V ⟼ ⋃_{d \in c} Pred (R, A, d)), Pred (R, A, X)) ↾}_{ω}) (k)$
45	44	eqeq2i	$⊢ a = ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (k) \leftrightarrow a = ({rec ((c \in V ⟼ ⋃_{d \in c} Pred (R, A, d)), Pred (R, A, X)) ↾}_{ω}) (k)$
46		iuneq1	$⊢ a = ({rec ((c \in V ⟼ ⋃_{d \in c} Pred (R, A, d)), Pred (R, A, X)) ↾}_{ω}) (k) \to ⋃_{y \in a} Pred (R, A, y) = ⋃_{y \in ({rec ((c \in V ⟼ ⋃_{d \in c} Pred (R, A, d)), Pred (R, A, X)) ↾}_{ω}) (k)} Pred (R, A, y)$
47	45 46	sylbi	$⊢ a = ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (k) \to ⋃_{y \in a} Pred (R, A, y) = ⋃_{y \in ({rec ((c \in V ⟼ ⋃_{d \in c} Pred (R, A, d)), Pred (R, A, X)) ↾}_{ω}) (k)} Pred (R, A, y)$
48	32 33 34 35 47	frsucmpt	$⊢ (k \in ω \land ⋃_{y \in ({rec ((c \in V ⟼ ⋃_{d \in c} Pred (R, A, d)), Pred (R, A, X)) ↾}_{ω}) (k)} Pred (R, A, y) \in V) \to ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (suc k) = ⋃_{y \in ({rec ((c \in V ⟼ ⋃_{d \in c} Pred (R, A, d)), Pred (R, A, X)) ↾}_{ω}) (k)} Pred (R, A, y)$
49	31 48	sylan2	$⊢ (k \in ω \land (((X \in A \land R Se A) \land (\forall y \in B Pred (R, A, y) \subseteq B \land Pred (R, A, X) \subseteq B)) \land ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (k) \subseteq B)) \to ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (suc k) = ⋃_{y \in ({rec ((c \in V ⟼ ⋃_{d \in c} Pred (R, A, d)), Pred (R, A, X)) ↾}_{ω}) (k)} Pred (R, A, y)$
50	44	sseq1i	$⊢ ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (k) \subseteq B \leftrightarrow ({rec ((c \in V ⟼ ⋃_{d \in c} Pred (R, A, d)), Pred (R, A, X)) ↾}_{ω}) (k) \subseteq B$
51	50	anbi2i	$⊢ (((X \in A \land R Se A) \land (\forall y \in B Pred (R, A, y) \subseteq B \land Pred (R, A, X) \subseteq B)) \land ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (k) \subseteq B) \leftrightarrow (((X \in A \land R Se A) \land (\forall y \in B Pred (R, A, y) \subseteq B \land Pred (R, A, X) \subseteq B)) \land ({rec ((c \in V ⟼ ⋃_{d \in c} Pred (R, A, d)), Pred (R, A, X)) ↾}_{ω}) (k) \subseteq B)$
52		nfv	$⊢ Ⅎ y (X \in A \land R Se A)$
53		nfra1	$⊢ Ⅎ y \forall y \in B Pred (R, A, y) \subseteq B$
54		nfv	$⊢ Ⅎ y Pred (R, A, X) \subseteq B$
55	53 54	nfan	$⊢ Ⅎ y (\forall y \in B Pred (R, A, y) \subseteq B \land Pred (R, A, X) \subseteq B)$
56	52 55	nfan	$⊢ Ⅎ y ((X \in A \land R Se A) \land (\forall y \in B Pred (R, A, y) \subseteq B \land Pred (R, A, X) \subseteq B))$
57		nfv	$⊢ Ⅎ y ({rec ((c \in V ⟼ ⋃_{d \in c} Pred (R, A, d)), Pred (R, A, X)) ↾}_{ω}) (k) \subseteq B$
58	56 57	nfan	$⊢ Ⅎ y (((X \in A \land R Se A) \land (\forall y \in B Pred (R, A, y) \subseteq B \land Pred (R, A, X) \subseteq B)) \land ({rec ((c \in V ⟼ ⋃_{d \in c} Pred (R, A, d)), Pred (R, A, X)) ↾}_{ω}) (k) \subseteq B)$
59		ssel	$⊢ ({rec ((c \in V ⟼ ⋃_{d \in c} Pred (R, A, d)), Pred (R, A, X)) ↾}_{ω}) (k) \subseteq B \to (y \in ({rec ((c \in V ⟼ ⋃_{d \in c} Pred (R, A, d)), Pred (R, A, X)) ↾}_{ω}) (k) \to y \in B)$
60		rsp	$⊢ \forall y \in B Pred (R, A, y) \subseteq B \to (y \in B \to Pred (R, A, y) \subseteq B)$
61	60	ad2antrl	$⊢ ((X \in A \land R Se A) \land (\forall y \in B Pred (R, A, y) \subseteq B \land Pred (R, A, X) \subseteq B)) \to (y \in B \to Pred (R, A, y) \subseteq B)$
62	59 61	sylan9r	$⊢ (((X \in A \land R Se A) \land (\forall y \in B Pred (R, A, y) \subseteq B \land Pred (R, A, X) \subseteq B)) \land ({rec ((c \in V ⟼ ⋃_{d \in c} Pred (R, A, d)), Pred (R, A, X)) ↾}_{ω}) (k) \subseteq B) \to (y \in ({rec ((c \in V ⟼ ⋃_{d \in c} Pred (R, A, d)), Pred (R, A, X)) ↾}_{ω}) (k) \to Pred (R, A, y) \subseteq B)$
63	58 62	ralrimi	$⊢ (((X \in A \land R Se A) \land (\forall y \in B Pred (R, A, y) \subseteq B \land Pred (R, A, X) \subseteq B)) \land ({rec ((c \in V ⟼ ⋃_{d \in c} Pred (R, A, d)), Pred (R, A, X)) ↾}_{ω}) (k) \subseteq B) \to \forall y \in ({rec ((c \in V ⟼ ⋃_{d \in c} Pred (R, A, d)), Pred (R, A, X)) ↾}_{ω}) (k) Pred (R, A, y) \subseteq B$
64	63	adantl	$⊢ (k \in ω \land (((X \in A \land R Se A) \land (\forall y \in B Pred (R, A, y) \subseteq B \land Pred (R, A, X) \subseteq B)) \land ({rec ((c \in V ⟼ ⋃_{d \in c} Pred (R, A, d)), Pred (R, A, X)) ↾}_{ω}) (k) \subseteq B)) \to \forall y \in ({rec ((c \in V ⟼ ⋃_{d \in c} Pred (R, A, d)), Pred (R, A, X)) ↾}_{ω}) (k) Pred (R, A, y) \subseteq B$
65	51 64	sylan2b	$⊢ (k \in ω \land (((X \in A \land R Se A) \land (\forall y \in B Pred (R, A, y) \subseteq B \land Pred (R, A, X) \subseteq B)) \land ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (k) \subseteq B)) \to \forall y \in ({rec ((c \in V ⟼ ⋃_{d \in c} Pred (R, A, d)), Pred (R, A, X)) ↾}_{ω}) (k) Pred (R, A, y) \subseteq B$
66		iunss	$⊢ ⋃_{y \in ({rec ((c \in V ⟼ ⋃_{d \in c} Pred (R, A, d)), Pred (R, A, X)) ↾}_{ω}) (k)} Pred (R, A, y) \subseteq B \leftrightarrow \forall y \in ({rec ((c \in V ⟼ ⋃_{d \in c} Pred (R, A, d)), Pred (R, A, X)) ↾}_{ω}) (k) Pred (R, A, y) \subseteq B$
67	65 66	sylibr	$⊢ (k \in ω \land (((X \in A \land R Se A) \land (\forall y \in B Pred (R, A, y) \subseteq B \land Pred (R, A, X) \subseteq B)) \land ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (k) \subseteq B)) \to ⋃_{y \in ({rec ((c \in V ⟼ ⋃_{d \in c} Pred (R, A, d)), Pred (R, A, X)) ↾}_{ω}) (k)} Pred (R, A, y) \subseteq B$
68	49 67	eqsstrd	$⊢ (k \in ω \land (((X \in A \land R Se A) \land (\forall y \in B Pred (R, A, y) \subseteq B \land Pred (R, A, X) \subseteq B)) \land ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (k) \subseteq B)) \to ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (suc k) \subseteq B$
69	68	exp32	$⊢ k \in ω \to (((X \in A \land R Se A) \land (\forall y \in B Pred (R, A, y) \subseteq B \land Pred (R, A, X) \subseteq B)) \to (({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (k) \subseteq B \to ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (suc k) \subseteq B))$
70	69	a2d	$⊢ k \in ω \to ((((X \in A \land R Se A) \land (\forall y \in B Pred (R, A, y) \subseteq B \land Pred (R, A, X) \subseteq B)) \to ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (k) \subseteq B) \to (((X \in A \land R Se A) \land (\forall y \in B Pred (R, A, y) \subseteq B \land Pred (R, A, X) \subseteq B)) \to ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (suc k) \subseteq B))$
71	4 7 10 13 19 70	finds	$⊢ i \in ω \to (((X \in A \land R Se A) \land (\forall y \in B Pred (R, A, y) \subseteq B \land Pred (R, A, X) \subseteq B)) \to ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (i) \subseteq B)$
72	71	com12	$⊢ ((X \in A \land R Se A) \land (\forall y \in B Pred (R, A, y) \subseteq B \land Pred (R, A, X) \subseteq B)) \to (i \in ω \to ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (i) \subseteq B)$
73	72	ralrimiv	$⊢ ((X \in A \land R Se A) \land (\forall y \in B Pred (R, A, y) \subseteq B \land Pred (R, A, X) \subseteq B)) \to \forall i \in ω ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (i) \subseteq B$
74		iunss	$⊢ ⋃_{i \in ω} ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (i) \subseteq B \leftrightarrow \forall i \in ω ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (i) \subseteq B$
75	73 74	sylibr	$⊢ ((X \in A \land R Se A) \land (\forall y \in B Pred (R, A, y) \subseteq B \land Pred (R, A, X) \subseteq B)) \to ⋃_{i \in ω} ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (i) \subseteq B$
76	1 75	eqsstrid	$⊢ ((X \in A \land R Se A) \land (\forall y \in B Pred (R, A, y) \subseteq B \land Pred (R, A, X) \subseteq B)) \to TrPred (R, A, X) \subseteq B$

Metamath Proof Explorer

Theorem trpredmintr

Proof