rdgssun

Description: In a recursive definition where each step expands on the previous one using a union, every previous step is a subset of every later step. (Contributed by ML, 1-Apr-2022)

	Ref	Expression
Hypotheses	rdgssun.1	$⊢ F = (w \in V ⟼ w \cup B)$
	rdgssun.2	$⊢ B \in V$
Assertion	rdgssun	$⊢ (X \in On \land Y \in X) \to rec (F, A) (Y) \subseteq rec (F, A) (X)$

Proof

Step	Hyp	Ref	Expression
1		rdgssun.1	$⊢ F = (w \in V ⟼ w \cup B)$
2		rdgssun.2	$⊢ B \in V$
3		nfsbc1v	$⊢ Ⅎ x \underset{˙}{[} \emptyset / x \underset{˙}{]} \forall y \in x rec (F, A) (y) \subseteq rec (F, A) (x)$
4		0ex	$⊢ \emptyset \in V$
5		rzal	$⊢ x = \emptyset \to \forall y \in x rec (F, A) (y) \subseteq rec (F, A) (x)$
6		sbceq1a	$⊢ x = \emptyset \to (\forall y \in x rec (F, A) (y) \subseteq rec (F, A) (x) \leftrightarrow \underset{˙}{[} \emptyset / x \underset{˙}{]} \forall y \in x rec (F, A) (y) \subseteq rec (F, A) (x))$
7	5 6	mpbid	$⊢ x = \emptyset \to \underset{˙}{[} \emptyset / x \underset{˙}{]} \forall y \in x rec (F, A) (y) \subseteq rec (F, A) (x)$
8	3 4 7	vtoclef	$⊢ \underset{˙}{[} \emptyset / x \underset{˙}{]} \forall y \in x rec (F, A) (y) \subseteq rec (F, A) (x)$
9		vex	$⊢ y \in V$
10	9	elsuc	$⊢ y \in suc x \leftrightarrow (y \in x \lor y = x)$
11		ssun1	$⊢ rec (F, A) (x) \subseteq rec (F, A) (x) \cup ⦋ rec (F, A) (x) / w ⦌ B$
12		fvex	$⊢ rec (F, A) (x) \in V$
13	2	csbex	$⊢ ⦋ rec (F, A) (x) / w ⦌ B \in V$
14	12 13	unex	$⊢ rec (F, A) (x) \cup ⦋ rec (F, A) (x) / w ⦌ B \in V$
15		nfcv	$⊢ \underline{Ⅎ} w A$
16		nfcv	$⊢ \underline{Ⅎ} w x$
17		nfmpt1	$⊢ \underline{Ⅎ} w (w \in V ⟼ w \cup B)$
18	1 17	nfcxfr	$⊢ \underline{Ⅎ} w F$
19	18 15	nfrdg	$⊢ \underline{Ⅎ} w rec (F, A)$
20	19 16	nffv	$⊢ \underline{Ⅎ} w rec (F, A) (x)$
21	20	nfcsb1	$⊢ \underline{Ⅎ} w ⦋ rec (F, A) (x) / w ⦌ B$
22	20 21	nfun	$⊢ \underline{Ⅎ} w (rec (F, A) (x) \cup ⦋ rec (F, A) (x) / w ⦌ B)$
23		rdgeq1	$⊢ F = (w \in V ⟼ w \cup B) \to rec (F, A) = rec ((w \in V ⟼ w \cup B), A)$
24	1 23	ax-mp	$⊢ rec (F, A) = rec ((w \in V ⟼ w \cup B), A)$
25		id	$⊢ w = rec (F, A) (x) \to w = rec (F, A) (x)$
26		csbeq1a	$⊢ w = rec (F, A) (x) \to B = ⦋ rec (F, A) (x) / w ⦌ B$
27	25 26	uneq12d	$⊢ w = rec (F, A) (x) \to w \cup B = rec (F, A) (x) \cup ⦋ rec (F, A) (x) / w ⦌ B$
28	15 16 22 24 27	rdgsucmptf	$⊢ (x \in On \land rec (F, A) (x) \cup ⦋ rec (F, A) (x) / w ⦌ B \in V) \to rec (F, A) (suc x) = rec (F, A) (x) \cup ⦋ rec (F, A) (x) / w ⦌ B$
29	14 28	mpan2	$⊢ x \in On \to rec (F, A) (suc x) = rec (F, A) (x) \cup ⦋ rec (F, A) (x) / w ⦌ B$
30	11 29	sseqtrrid	$⊢ x \in On \to rec (F, A) (x) \subseteq rec (F, A) (suc x)$
31		sstr2	$⊢ rec (F, A) (y) \subseteq rec (F, A) (x) \to (rec (F, A) (x) \subseteq rec (F, A) (suc x) \to rec (F, A) (y) \subseteq rec (F, A) (suc x))$
32	30 31	syl5com	$⊢ x \in On \to (rec (F, A) (y) \subseteq rec (F, A) (x) \to rec (F, A) (y) \subseteq rec (F, A) (suc x))$
33	32	imim2d	$⊢ x \in On \to ((y \in x \to rec (F, A) (y) \subseteq rec (F, A) (x)) \to (y \in x \to rec (F, A) (y) \subseteq rec (F, A) (suc x)))$
34	33	imp	$⊢ (x \in On \land (y \in x \to rec (F, A) (y) \subseteq rec (F, A) (x))) \to (y \in x \to rec (F, A) (y) \subseteq rec (F, A) (suc x))$
35		fveq2	$⊢ y = x \to rec (F, A) (y) = rec (F, A) (x)$
36	35	sseq1d	$⊢ y = x \to (rec (F, A) (y) \subseteq rec (F, A) (suc x) \leftrightarrow rec (F, A) (x) \subseteq rec (F, A) (suc x))$
37	30 36	syl5ibrcom	$⊢ x \in On \to (y = x \to rec (F, A) (y) \subseteq rec (F, A) (suc x))$
38	37	adantr	$⊢ (x \in On \land (y \in x \to rec (F, A) (y) \subseteq rec (F, A) (x))) \to (y = x \to rec (F, A) (y) \subseteq rec (F, A) (suc x))$
39	34 38	jaod	$⊢ (x \in On \land (y \in x \to rec (F, A) (y) \subseteq rec (F, A) (x))) \to ((y \in x \lor y = x) \to rec (F, A) (y) \subseteq rec (F, A) (suc x))$
40	10 39	syl5bi	$⊢ (x \in On \land (y \in x \to rec (F, A) (y) \subseteq rec (F, A) (x))) \to (y \in suc x \to rec (F, A) (y) \subseteq rec (F, A) (suc x))$
41	40	ex	$⊢ x \in On \to ((y \in x \to rec (F, A) (y) \subseteq rec (F, A) (x)) \to (y \in suc x \to rec (F, A) (y) \subseteq rec (F, A) (suc x)))$
42	41	ralimdv2	$⊢ x \in On \to (\forall y \in x rec (F, A) (y) \subseteq rec (F, A) (x) \to \forall y \in suc x rec (F, A) (y) \subseteq rec (F, A) (suc x))$
43		df-sbc	$⊢ \underset{˙}{[} suc x / x \underset{˙}{]} \forall y \in x rec (F, A) (y) \subseteq rec (F, A) (x) \leftrightarrow suc x \in \{x \| \forall y \in x rec (F, A) (y) \subseteq rec (F, A) (x)\}$
44		vex	$⊢ x \in V$
45	44	sucex	$⊢ suc x \in V$
46		fveq2	$⊢ z = suc x \to rec (F, A) (z) = rec (F, A) (suc x)$
47	46	sseq2d	$⊢ z = suc x \to (rec (F, A) (y) \subseteq rec (F, A) (z) \leftrightarrow rec (F, A) (y) \subseteq rec (F, A) (suc x))$
48	47	raleqbi1dv	$⊢ z = suc x \to (\forall y \in z rec (F, A) (y) \subseteq rec (F, A) (z) \leftrightarrow \forall y \in suc x rec (F, A) (y) \subseteq rec (F, A) (suc x))$
49		fveq2	$⊢ x = z \to rec (F, A) (x) = rec (F, A) (z)$
50	49	sseq2d	$⊢ x = z \to (rec (F, A) (y) \subseteq rec (F, A) (x) \leftrightarrow rec (F, A) (y) \subseteq rec (F, A) (z))$
51	50	raleqbi1dv	$⊢ x = z \to (\forall y \in x rec (F, A) (y) \subseteq rec (F, A) (x) \leftrightarrow \forall y \in z rec (F, A) (y) \subseteq rec (F, A) (z))$
52	51	cbvabv	$⊢ \{x \| \forall y \in x rec (F, A) (y) \subseteq rec (F, A) (x)\} = \{z \| \forall y \in z rec (F, A) (y) \subseteq rec (F, A) (z)\}$
53	45 48 52	elab2	$⊢ suc x \in \{x \| \forall y \in x rec (F, A) (y) \subseteq rec (F, A) (x)\} \leftrightarrow \forall y \in suc x rec (F, A) (y) \subseteq rec (F, A) (suc x)$
54	43 53	bitri	$⊢ \underset{˙}{[} suc x / x \underset{˙}{]} \forall y \in x rec (F, A) (y) \subseteq rec (F, A) (x) \leftrightarrow \forall y \in suc x rec (F, A) (y) \subseteq rec (F, A) (suc x)$
55	42 54	syl6ibr	$⊢ x \in On \to (\forall y \in x rec (F, A) (y) \subseteq rec (F, A) (x) \to \underset{˙}{[} suc x / x \underset{˙}{]} \forall y \in x rec (F, A) (y) \subseteq rec (F, A) (x))$
56		ssiun2	$⊢ y \in z \to rec (F, A) (y) \subseteq ⋃_{y \in z} rec (F, A) (y)$
57	56	adantl	$⊢ (Lim z \land y \in z) \to rec (F, A) (y) \subseteq ⋃_{y \in z} rec (F, A) (y)$
58		vex	$⊢ z \in V$
59		rdglim2a	$⊢ (z \in V \land Lim z) \to rec (F, A) (z) = ⋃_{y \in z} rec (F, A) (y)$
60	58 59	mpan	$⊢ Lim z \to rec (F, A) (z) = ⋃_{y \in z} rec (F, A) (y)$
61	60	adantr	$⊢ (Lim z \land y \in z) \to rec (F, A) (z) = ⋃_{y \in z} rec (F, A) (y)$
62	57 61	sseqtrrd	$⊢ (Lim z \land y \in z) \to rec (F, A) (y) \subseteq rec (F, A) (z)$
63	62	ralrimiva	$⊢ Lim z \to \forall y \in z rec (F, A) (y) \subseteq rec (F, A) (z)$
64		df-sbc	$⊢ \underset{˙}{[} z / x \underset{˙}{]} \forall y \in x rec (F, A) (y) \subseteq rec (F, A) (x) \leftrightarrow z \in \{x \| \forall y \in x rec (F, A) (y) \subseteq rec (F, A) (x)\}$
65	52	eleq2i	$⊢ z \in \{x \| \forall y \in x rec (F, A) (y) \subseteq rec (F, A) (x)\} \leftrightarrow z \in \{z \| \forall y \in z rec (F, A) (y) \subseteq rec (F, A) (z)\}$
66	64 65	bitri	$⊢ \underset{˙}{[} z / x \underset{˙}{]} \forall y \in x rec (F, A) (y) \subseteq rec (F, A) (x) \leftrightarrow z \in \{z \| \forall y \in z rec (F, A) (y) \subseteq rec (F, A) (z)\}$
67		abid	$⊢ z \in \{z \| \forall y \in z rec (F, A) (y) \subseteq rec (F, A) (z)\} \leftrightarrow \forall y \in z rec (F, A) (y) \subseteq rec (F, A) (z)$
68	66 67	bitri	$⊢ \underset{˙}{[} z / x \underset{˙}{]} \forall y \in x rec (F, A) (y) \subseteq rec (F, A) (x) \leftrightarrow \forall y \in z rec (F, A) (y) \subseteq rec (F, A) (z)$
69	63 68	sylibr	$⊢ Lim z \to \underset{˙}{[} z / x \underset{˙}{]} \forall y \in x rec (F, A) (y) \subseteq rec (F, A) (x)$
70	69	a1d	$⊢ Lim z \to (\forall x \in z \forall y \in x rec (F, A) (y) \subseteq rec (F, A) (x) \to \underset{˙}{[} z / x \underset{˙}{]} \forall y \in x rec (F, A) (y) \subseteq rec (F, A) (x))$
71	8 55 70	tfindes	$⊢ x \in On \to \forall y \in x rec (F, A) (y) \subseteq rec (F, A) (x)$
72		rsp	$⊢ \forall y \in x rec (F, A) (y) \subseteq rec (F, A) (x) \to (y \in x \to rec (F, A) (y) \subseteq rec (F, A) (x))$
73	71 72	syl	$⊢ x \in On \to (y \in x \to rec (F, A) (y) \subseteq rec (F, A) (x))$
74		eleq1	$⊢ x = X \to (x \in On \leftrightarrow X \in On)$
75	74	adantl	$⊢ (y = Y \land x = X) \to (x \in On \leftrightarrow X \in On)$
76		eleq12	$⊢ (y = Y \land x = X) \to (y \in x \leftrightarrow Y \in X)$
77		fveq2	$⊢ y = Y \to rec (F, A) (y) = rec (F, A) (Y)$
78	77	adantr	$⊢ (y = Y \land x = X) \to rec (F, A) (y) = rec (F, A) (Y)$
79		fveq2	$⊢ x = X \to rec (F, A) (x) = rec (F, A) (X)$
80	79	adantl	$⊢ (y = Y \land x = X) \to rec (F, A) (x) = rec (F, A) (X)$
81	78 80	sseq12d	$⊢ (y = Y \land x = X) \to (rec (F, A) (y) \subseteq rec (F, A) (x) \leftrightarrow rec (F, A) (Y) \subseteq rec (F, A) (X))$
82	76 81	imbi12d	$⊢ (y = Y \land x = X) \to ((y \in x \to rec (F, A) (y) \subseteq rec (F, A) (x)) \leftrightarrow (Y \in X \to rec (F, A) (Y) \subseteq rec (F, A) (X)))$
83	75 82	imbi12d	$⊢ (y = Y \land x = X) \to ((x \in On \to (y \in x \to rec (F, A) (y) \subseteq rec (F, A) (x))) \leftrightarrow (X \in On \to (Y \in X \to rec (F, A) (Y) \subseteq rec (F, A) (X))))$
84	73 83	mpbii	$⊢ (y = Y \land x = X) \to (X \in On \to (Y \in X \to rec (F, A) (Y) \subseteq rec (F, A) (X)))$
85	84	ex	$⊢ y = Y \to (x = X \to (X \in On \to (Y \in X \to rec (F, A) (Y) \subseteq rec (F, A) (X))))$
86	85	vtocleg	$⊢ Y \in X \to (x = X \to (X \in On \to (Y \in X \to rec (F, A) (Y) \subseteq rec (F, A) (X))))$
87	86	com12	$⊢ x = X \to (Y \in X \to (X \in On \to (Y \in X \to rec (F, A) (Y) \subseteq rec (F, A) (X))))$
88	87	vtocleg	$⊢ X \in On \to (Y \in X \to (X \in On \to (Y \in X \to rec (F, A) (Y) \subseteq rec (F, A) (X))))$
89	88	pm2.43b	$⊢ Y \in X \to (X \in On \to (Y \in X \to rec (F, A) (Y) \subseteq rec (F, A) (X)))$
90	89	pm2.43b	$⊢ X \in On \to (Y \in X \to rec (F, A) (Y) \subseteq rec (F, A) (X))$
91	90	imp	$⊢ (X \in On \land Y \in X) \to rec (F, A) (Y) \subseteq rec (F, A) (X)$

Metamath Proof Explorer

Theorem rdgssun

Proof