ttrclselem1

Description: Lemma for ttrclse . Show that all finite ordinal function values of F are subsets of A . (Contributed by Scott Fenton, 31-Oct-2024)

		Ref	Expression
	Hypothesis	ttrclselem.1	$⊢ F = rec ((b \in V ⟼ ⋃_{w \in b} Pred (R, A, w)), Pred (R, A, X))$
	Assertion	ttrclselem1	$⊢ N \in ω \to F (N) \subseteq A$

Proof

Step	Hyp	Ref	Expression
1		ttrclselem.1	$⊢ F = rec ((b \in V ⟼ ⋃_{w \in b} Pred (R, A, w)), Pred (R, A, X))$
2		nn0suc	$⊢ N \in ω \to (N = \emptyset \lor \exists n \in ω N = suc n)$
3	1	fveq1i	$⊢ F (N) = rec ((b \in V ⟼ ⋃_{w \in b} Pred (R, A, w)), Pred (R, A, X)) (N)$
4		fveq2	$⊢ N = \emptyset \to rec ((b \in V ⟼ ⋃_{w \in b} Pred (R, A, w)), Pred (R, A, X)) (N) = rec ((b \in V ⟼ ⋃_{w \in b} Pred (R, A, w)), Pred (R, A, X)) (\emptyset)$
5	3 4	eqtrid	$⊢ N = \emptyset \to F (N) = rec ((b \in V ⟼ ⋃_{w \in b} Pred (R, A, w)), Pred (R, A, X)) (\emptyset)$
6		rdg0g	$⊢ Pred (R, A, X) \in V \to rec ((b \in V ⟼ ⋃_{w \in b} Pred (R, A, w)), Pred (R, A, X)) (\emptyset) = Pred (R, A, X)$
7		predss	$⊢ Pred (R, A, X) \subseteq A$
8	6 7	eqsstrdi	$⊢ Pred (R, A, X) \in V \to rec ((b \in V ⟼ ⋃_{w \in b} Pred (R, A, w)), Pred (R, A, X)) (\emptyset) \subseteq A$
9		rdg0n	$⊢ \neg Pred (R, A, X) \in V \to rec ((b \in V ⟼ ⋃_{w \in b} Pred (R, A, w)), Pred (R, A, X)) (\emptyset) = \emptyset$
10		0ss	$⊢ \emptyset \subseteq A$
11	9 10	eqsstrdi	$⊢ \neg Pred (R, A, X) \in V \to rec ((b \in V ⟼ ⋃_{w \in b} Pred (R, A, w)), Pred (R, A, X)) (\emptyset) \subseteq A$
12	8 11	pm2.61i	$⊢ rec ((b \in V ⟼ ⋃_{w \in b} Pred (R, A, w)), Pred (R, A, X)) (\emptyset) \subseteq A$
13	5 12	eqsstrdi	$⊢ N = \emptyset \to F (N) \subseteq A$
14		nnon	$⊢ n \in ω \to n \in On$
15		nfcv	$⊢ \underline{Ⅎ} b Pred (R, A, X)$
16		nfcv	$⊢ \underline{Ⅎ} b n$
17		nfmpt1	$⊢ \underline{Ⅎ} b (b \in V ⟼ ⋃_{w \in b} Pred (R, A, w))$
18	17 15	nfrdg	$⊢ \underline{Ⅎ} b rec ((b \in V ⟼ ⋃_{w \in b} Pred (R, A, w)), Pred (R, A, X))$
19	1 18	nfcxfr	$⊢ \underline{Ⅎ} b F$
20	19 16	nffv	$⊢ \underline{Ⅎ} b F (n)$
21		nfcv	$⊢ \underline{Ⅎ} b Pred (R, A, t)$
22	20 21	nfiun	$⊢ \underline{Ⅎ} b ⋃_{t \in F (n)} Pred (R, A, t)$
23		predeq3	$⊢ w = t \to Pred (R, A, w) = Pred (R, A, t)$
24	23	cbviunv	$⊢ ⋃_{w \in b} Pred (R, A, w) = ⋃_{t \in b} Pred (R, A, t)$
25		iuneq1	$⊢ b = F (n) \to ⋃_{t \in b} Pred (R, A, t) = ⋃_{t \in F (n)} Pred (R, A, t)$
26	24 25	eqtrid	$⊢ b = F (n) \to ⋃_{w \in b} Pred (R, A, w) = ⋃_{t \in F (n)} Pred (R, A, t)$
27	15 16 22 1 26	rdgsucmptf	$⊢ (n \in On \land ⋃_{t \in F (n)} Pred (R, A, t) \in V) \to F (suc n) = ⋃_{t \in F (n)} Pred (R, A, t)$
28		iunss	$⊢ ⋃_{t \in F (n)} Pred (R, A, t) \subseteq A \leftrightarrow \forall t \in F (n) Pred (R, A, t) \subseteq A$
29		predss	$⊢ Pred (R, A, t) \subseteq A$
30	29	a1i	$⊢ t \in F (n) \to Pred (R, A, t) \subseteq A$
31	28 30	mprgbir	$⊢ ⋃_{t \in F (n)} Pred (R, A, t) \subseteq A$
32	27 31	eqsstrdi	$⊢ (n \in On \land ⋃_{t \in F (n)} Pred (R, A, t) \in V) \to F (suc n) \subseteq A$
33	14 32	sylan	$⊢ (n \in ω \land ⋃_{t \in F (n)} Pred (R, A, t) \in V) \to F (suc n) \subseteq A$
34	15 16 22 1 26	rdgsucmptnf	$⊢ \neg ⋃_{t \in F (n)} Pred (R, A, t) \in V \to F (suc n) = \emptyset$
35	34 10	eqsstrdi	$⊢ \neg ⋃_{t \in F (n)} Pred (R, A, t) \in V \to F (suc n) \subseteq A$
36	35	adantl	$⊢ (n \in ω \land \neg ⋃_{t \in F (n)} Pred (R, A, t) \in V) \to F (suc n) \subseteq A$
37	33 36	pm2.61dan	$⊢ n \in ω \to F (suc n) \subseteq A$
38		fveq2	$⊢ N = suc n \to F (N) = F (suc n)$
39	38	sseq1d	$⊢ N = suc n \to (F (N) \subseteq A \leftrightarrow F (suc n) \subseteq A)$
40	37 39	syl5ibrcom	$⊢ n \in ω \to (N = suc n \to F (N) \subseteq A)$
41	40	rexlimiv	$⊢ \exists n \in ω N = suc n \to F (N) \subseteq A$
42	13 41	jaoi	$⊢ (N = \emptyset \lor \exists n \in ω N = suc n) \to F (N) \subseteq A$
43	2 42	syl	$⊢ N \in ω \to F (N) \subseteq A$

Metamath Proof Explorer

Theorem ttrclselem1

Proof