Theorem setrec1lem4

Description: Lemma for setrec1 . If X is recursively generated by F , then so is X u. ( FA ) .

In the proof of setrec1 , the following is substituted for this theorem's ph : ( ph /\ ( A C_ x /\ x e. { y | A. z ( A. w ( w C_ y -> ( w C_ z -> ( Fw ) C_ z ) ) -> y C_ z ) } ) ) Therefore, we cannot declare z to be a distinct variable from ph , since we need it to appear as a bound variable in ph . This theorem can be proven without the hypothesis F/ z ph , but the proof would be harder to read because theorems in deduction form would be interrupted by theorems like eximi , making the antecedent of each line something more complicated than ph . The proof of setrec1lem2 could similarly be made easier to read by adding the hypothesis F/ z ph , but I had already finished the proof and decided to leave it as is. (Contributed by Emmett Weisz, 26-Nov-2020) (New usage is discouraged.)

	Ref	Expression
Hypotheses	setrec1lem4.1	$$⊢Ⅎz\phi$$
	setrec1lem4.2	$$⊢Y=\left\{y|\forall z\left(\forall w\left(w\subseteq y\to \left(w\subseteq z\to F\left(w\right)\subseteq z\right)\right)\to y\subseteq z\right)\right\}$$
	setrec1lem4.3	$$⊢\phi \to A\in \mathrm{V}$$
	setrec1lem4.4	$$⊢\phi \to A\subseteq X$$
	setrec1lem4.5	$$⊢\phi \to X\in Y$$
Assertion	setrec1lem4	$$⊢\phi \to X\cup F\left(A\right)\in Y$$

Proof

Step	Hyp	Ref	Expression
1		setrec1lem4.1	$$⊢Ⅎz\phi$$
2		setrec1lem4.2	$$⊢Y=\left\{y|\forall z\left(\forall w\left(w\subseteq y\to \left(w\subseteq z\to F\left(w\right)\subseteq z\right)\right)\to y\subseteq z\right)\right\}$$
3		setrec1lem4.3	$$⊢\phi \to A\in \mathrm{V}$$
4		setrec1lem4.4	$$⊢\phi \to A\subseteq X$$
5		setrec1lem4.5	$$⊢\phi \to X\in Y$$
6		id	$$⊢w\subseteq X\to w\subseteq X$$
7		ssun1	$$⊢X\subseteq X\cup F\left(A\right)$$
8	6 7	sstrdi	$$⊢w\subseteq X\to w\subseteq X\cup F\left(A\right)$$
9	8	imim1i	$$⊢\left(w\subseteq X\cup F\left(A\right)\to \left(w\subseteq z\to F\left(w\right)\subseteq z\right)\right)\to \left(w\subseteq X\to \left(w\subseteq z\to F\left(w\right)\subseteq z\right)\right)$$
10	9	alimi	$$⊢\forall w\left(w\subseteq X\cup F\left(A\right)\to \left(w\subseteq z\to F\left(w\right)\subseteq z\right)\right)\to \forall w\left(w\subseteq X\to \left(w\subseteq z\to F\left(w\right)\subseteq z\right)\right)$$
11	2 5	setrec1lem1	$$⊢\phi \to \left(X\in Y\leftrightarrow \forall z\left(\forall w\left(w\subseteq X\to \left(w\subseteq z\to F\left(w\right)\subseteq z\right)\right)\to X\subseteq z\right)\right)$$
12	5 11	mpbid	$$⊢\phi \to \forall z\left(\forall w\left(w\subseteq X\to \left(w\subseteq z\to F\left(w\right)\subseteq z\right)\right)\to X\subseteq z\right)$$
13		sp	$$⊢\forall z\left(\forall w\left(w\subseteq X\to \left(w\subseteq z\to F\left(w\right)\subseteq z\right)\right)\to X\subseteq z\right)\to \left(\forall w\left(w\subseteq X\to \left(w\subseteq z\to F\left(w\right)\subseteq z\right)\right)\to X\subseteq z\right)$$
14	12 13	syl	$$⊢\phi \to \left(\forall w\left(w\subseteq X\to \left(w\subseteq z\to F\left(w\right)\subseteq z\right)\right)\to X\subseteq z\right)$$
15		sstr2	$$⊢A\subseteq X\to \left(X\subseteq z\to A\subseteq z\right)$$
16	4 15	syl	$$⊢\phi \to \left(X\subseteq z\to A\subseteq z\right)$$
17	14 16	syld	$$⊢\phi \to \left(\forall w\left(w\subseteq X\to \left(w\subseteq z\to F\left(w\right)\subseteq z\right)\right)\to A\subseteq z\right)$$
18		sseq1	$$⊢w=A\to \left(w\subseteq X\leftrightarrow A\subseteq X\right)$$
19		sseq1	$$⊢w=A\to \left(w\subseteq z\leftrightarrow A\subseteq z\right)$$
20		fveq2	$$⊢w=A\to F\left(w\right)=F\left(A\right)$$
21	20	sseq1d	$$⊢w=A\to \left(F\left(w\right)\subseteq z\leftrightarrow F\left(A\right)\subseteq z\right)$$
22	19 21	imbi12d	$$⊢w=A\to \left(\left(w\subseteq z\to F\left(w\right)\subseteq z\right)\leftrightarrow \left(A\subseteq z\to F\left(A\right)\subseteq z\right)\right)$$
23	18 22	imbi12d	$$⊢w=A\to \left(\left(w\subseteq X\to \left(w\subseteq z\to F\left(w\right)\subseteq z\right)\right)\leftrightarrow \left(A\subseteq X\to \left(A\subseteq z\to F\left(A\right)\subseteq z\right)\right)\right)$$
24	3 23	spcdvw	$$⊢\phi \to \left(\forall w\left(w\subseteq X\to \left(w\subseteq z\to F\left(w\right)\subseteq z\right)\right)\to \left(A\subseteq X\to \left(A\subseteq z\to F\left(A\right)\subseteq z\right)\right)\right)$$
25	4 24	mpid	$$⊢\phi \to \left(\forall w\left(w\subseteq X\to \left(w\subseteq z\to F\left(w\right)\subseteq z\right)\right)\to \left(A\subseteq z\to F\left(A\right)\subseteq z\right)\right)$$
26	17 25	mpdd	$$⊢\phi \to \left(\forall w\left(w\subseteq X\to \left(w\subseteq z\to F\left(w\right)\subseteq z\right)\right)\to F\left(A\right)\subseteq z\right)$$
27	14 26	jcad	$$⊢\phi \to \left(\forall w\left(w\subseteq X\to \left(w\subseteq z\to F\left(w\right)\subseteq z\right)\right)\to \left(X\subseteq z\wedge F\left(A\right)\subseteq z\right)\right)$$
28	10 27	syl5	$$⊢\phi \to \left(\forall w\left(w\subseteq X\cup F\left(A\right)\to \left(w\subseteq z\to F\left(w\right)\subseteq z\right)\right)\to \left(X\subseteq z\wedge F\left(A\right)\subseteq z\right)\right)$$
29		unss	$$⊢\left(X\subseteq z\wedge F\left(A\right)\subseteq z\right)\leftrightarrow X\cup F\left(A\right)\subseteq z$$
30	28 29	imbitrdi	$$⊢\phi \to \left(\forall w\left(w\subseteq X\cup F\left(A\right)\to \left(w\subseteq z\to F\left(w\right)\subseteq z\right)\right)\to X\cup F\left(A\right)\subseteq z\right)$$
31	1 30	alrimi	$$⊢\phi \to \forall z\left(\forall w\left(w\subseteq X\cup F\left(A\right)\to \left(w\subseteq z\to F\left(w\right)\subseteq z\right)\right)\to X\cup F\left(A\right)\subseteq z\right)$$
32		fvex	$$⊢F\left(A\right)\in \mathrm{V}$$
33		unexg	$$⊢\left(X\in Y\wedge F\left(A\right)\in \mathrm{V}\right)\to X\cup F\left(A\right)\in \mathrm{V}$$
34	5 32 33	sylancl	$$⊢\phi \to X\cup F\left(A\right)\in \mathrm{V}$$
35	2 34	setrec1lem1	$$⊢\phi \to \left(X\cup F\left(A\right)\in Y\leftrightarrow \forall z\left(\forall w\left(w\subseteq X\cup F\left(A\right)\to \left(w\subseteq z\to F\left(w\right)\subseteq z\right)\right)\to X\cup F\left(A\right)\subseteq z\right)\right)$$
36	31 35	mpbird	$$⊢\phi \to X\cup F\left(A\right)\in Y$$