trpredlem1

Description: Technical lemma for transitive predecessors properties. All values of the transitive predecessors' underlying function are subclasses of the base class. (Contributed by Scott Fenton, 28-Apr-2012)

		Ref	Expression
	Assertion	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$

Proof

Step	Hyp	Ref	Expression
1		nn0suc	$⊢ i \in ω \to (i = \emptyset \lor \exists j \in ω i = suc j)$
2		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)$
3		predss	$⊢ Pred (R, A, X) \subseteq A$
4	2 3	eqsstrdi	$⊢ Pred (R, A, X) \in B \to ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (\emptyset) \subseteq A$
5		fveq2	$⊢ i = \emptyset \to ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (i) = ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (\emptyset)$
6	5	sseq1d	$⊢ i = \emptyset \to (({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (i) \subseteq A \leftrightarrow ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (\emptyset) \subseteq A)$
7	4 6	syl5ibr	$⊢ i = \emptyset \to (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)$
8		nfcv	$⊢ \underline{Ⅎ} a Pred (R, A, X)$
9		nfcv	$⊢ \underline{Ⅎ} a j$
10		nfmpt1	$⊢ \underline{Ⅎ} a (a \in V ⟼ ⋃_{y \in a} Pred (R, A, y))$
11	10 8	nfrdg	$⊢ \underline{Ⅎ} a rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X))$
12		nfcv	$⊢ \underline{Ⅎ} a ω$
13	11 12	nfres	$⊢ \underline{Ⅎ} a ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω})$
14	13 9	nffv	$⊢ \underline{Ⅎ} a ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (j)$
15		nfcv	$⊢ \underline{Ⅎ} a Pred (R, A, e)$
16	14 15	nfiun	$⊢ \underline{Ⅎ} a ⋃_{e \in ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (j)} Pred (R, A, e)$
17		predeq3	$⊢ y = e \to Pred (R, A, y) = Pred (R, A, e)$
18	17	cbviunv	$⊢ ⋃_{y \in a} Pred (R, A, y) = ⋃_{e \in a} Pred (R, A, e)$
19	18	mpteq2i	$⊢ (a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)) = (a \in V ⟼ ⋃_{e \in a} Pred (R, A, e))$
20		rdgeq1	$⊢ (a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)) = (a \in V ⟼ ⋃_{e \in a} Pred (R, A, e)) \to rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) = rec ((a \in V ⟼ ⋃_{e \in a} Pred (R, A, e)), Pred (R, A, X))$
21		reseq1	$⊢ rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) = rec ((a \in V ⟼ ⋃_{e \in a} Pred (R, A, e)), Pred (R, A, X)) \to {rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω} = {rec ((a \in V ⟼ ⋃_{e \in a} Pred (R, A, e)), Pred (R, A, X)) ↾}_{ω}$
22	19 20 21	mp2b	$⊢ {rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω} = {rec ((a \in V ⟼ ⋃_{e \in a} Pred (R, A, e)), Pred (R, A, X)) ↾}_{ω}$
23		iuneq1	$⊢ a = ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (j) \to ⋃_{e \in a} Pred (R, A, e) = ⋃_{e \in ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (j)} Pred (R, A, e)$
24	8 9 16 22 23	frsucmpt	$⊢ (j \in ω \land ⋃_{e \in ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (j)} Pred (R, A, e) \in V) \to ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (suc j) = ⋃_{e \in ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (j)} Pred (R, A, e)$
25		iunss	$⊢ ⋃_{e \in ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (j)} Pred (R, A, e) \subseteq A \leftrightarrow \forall e \in ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (j) Pred (R, A, e) \subseteq A$
26		predss	$⊢ Pred (R, A, e) \subseteq A$
27	26	a1i	$⊢ e \in ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (j) \to Pred (R, A, e) \subseteq A$
28	25 27	mprgbir	$⊢ ⋃_{e \in ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (j)} Pred (R, A, e) \subseteq A$
29	24 28	eqsstrdi	$⊢ (j \in ω \land ⋃_{e \in ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (j)} Pred (R, A, e) \in V) \to ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (suc j) \subseteq A$
30	8 9 16 22 23	frsucmptn	$⊢ \neg ⋃_{e \in ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (j)} Pred (R, A, e) \in V \to ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (suc j) = \emptyset$
31	30	adantl	$⊢ (j \in ω \land \neg ⋃_{e \in ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (j)} Pred (R, A, e) \in V) \to ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (suc j) = \emptyset$
32		0ss	$⊢ \emptyset \subseteq A$
33	31 32	eqsstrdi	$⊢ (j \in ω \land \neg ⋃_{e \in ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (j)} Pred (R, A, e) \in V) \to ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (suc j) \subseteq A$
34	29 33	pm2.61dan	$⊢ j \in ω \to ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (suc j) \subseteq A$
35	34	adantr	$⊢ (j \in ω \land i = suc j) \to ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (suc j) \subseteq A$
36		fveq2	$⊢ i = suc j \to ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (i) = ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (suc j)$
37	36	sseq1d	$⊢ i = suc j \to (({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (i) \subseteq A \leftrightarrow ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (suc j) \subseteq A)$
38	37	adantl	$⊢ (j \in ω \land i = suc j) \to (({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (i) \subseteq A \leftrightarrow ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (suc j) \subseteq A)$
39	35 38	mpbird	$⊢ (j \in ω \land i = suc j) \to ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (i) \subseteq A$
40	39	rexlimiva	$⊢ \exists j \in ω i = suc j \to ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (i) \subseteq A$
41	40	a1d	$⊢ \exists j \in ω i = suc j \to (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)$
42	7 41	jaoi	$⊢ (i = \emptyset \lor \exists j \in ω i = suc j) \to (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)$
43	1 42	syl	$⊢ i \in ω \to (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)$
44		nfvres	$⊢ \neg i \in ω \to ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (i) = \emptyset$
45	44 32	eqsstrdi	$⊢ \neg i \in ω \to ({rec ((a \in V ⟼ ⋃_{y \in a} Pred (R, A, y)), Pred (R, A, X)) ↾}_{ω}) (i) \subseteq A$
46	45	a1d	$⊢ \neg i \in ω \to (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)$
47	43 46	pm2.61i	$⊢ 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$

Metamath Proof Explorer

Theorem trpredlem1

Proof