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	|- F/ z ph
	setrec1lem4.2	|- Y = { y | A. z ( A. w ( w C_ y -> ( w C_ z -> ( F ` w ) C_ z ) ) -> y C_ z ) }
	setrec1lem4.3	|- ( ph -> A e. _V )
	setrec1lem4.4	|- ( ph -> A C_ X )
	setrec1lem4.5	|- ( ph -> X e. Y )
Assertion	setrec1lem4	|- ( ph -> ( X u. ( F ` A ) ) e. Y )

Proof

Step	Hyp	Ref	Expression
1		setrec1lem4.1	|- F/ z ph
2		setrec1lem4.2	|- Y = { y | A. z ( A. w ( w C_ y -> ( w C_ z -> ( F ` w ) C_ z ) ) -> y C_ z ) }
3		setrec1lem4.3	|- ( ph -> A e. _V )
4		setrec1lem4.4	|- ( ph -> A C_ X )
5		setrec1lem4.5	|- ( ph -> X e. Y )
6		id	|- ( w C_ X -> w C_ X )
7		ssun1	|- X C_ ( X u. ( F ` A ) )
8	6 7	sstrdi	|- ( w C_ X -> w C_ ( X u. ( F ` A ) ) )
9	8	imim1i	|- ( ( w C_ ( X u. ( F ` A ) ) -> ( w C_ z -> ( F ` w ) C_ z ) ) -> ( w C_ X -> ( w C_ z -> ( F ` w ) C_ z ) ) )
10	9	alimi	|- ( A. w ( w C_ ( X u. ( F ` A ) ) -> ( w C_ z -> ( F ` w ) C_ z ) ) -> A. w ( w C_ X -> ( w C_ z -> ( F ` w ) C_ z ) ) )
11	2 5	setrec1lem1	|- ( ph -> ( X e. Y <-> A. z ( A. w ( w C_ X -> ( w C_ z -> ( F ` w ) C_ z ) ) -> X C_ z ) ) )
12	5 11	mpbid	|- ( ph -> A. z ( A. w ( w C_ X -> ( w C_ z -> ( F ` w ) C_ z ) ) -> X C_ z ) )
13		sp	|- ( A. z ( A. w ( w C_ X -> ( w C_ z -> ( F ` w ) C_ z ) ) -> X C_ z ) -> ( A. w ( w C_ X -> ( w C_ z -> ( F ` w ) C_ z ) ) -> X C_ z ) )
14	12 13	syl	|- ( ph -> ( A. w ( w C_ X -> ( w C_ z -> ( F ` w ) C_ z ) ) -> X C_ z ) )
15		sstr2	|- ( A C_ X -> ( X C_ z -> A C_ z ) )
16	4 15	syl	|- ( ph -> ( X C_ z -> A C_ z ) )
17	14 16	syld	|- ( ph -> ( A. w ( w C_ X -> ( w C_ z -> ( F ` w ) C_ z ) ) -> A C_ z ) )
18		sseq1	|- ( w = A -> ( w C_ X <-> A C_ X ) )
19		sseq1	|- ( w = A -> ( w C_ z <-> A C_ z ) )
20		fveq2	|- ( w = A -> ( F ` w ) = ( F ` A ) )
21	20	sseq1d	|- ( w = A -> ( ( F ` w ) C_ z <-> ( F ` A ) C_ z ) )
22	19 21	imbi12d	|- ( w = A -> ( ( w C_ z -> ( F ` w ) C_ z ) <-> ( A C_ z -> ( F ` A ) C_ z ) ) )
23	18 22	imbi12d	|- ( w = A -> ( ( w C_ X -> ( w C_ z -> ( F ` w ) C_ z ) ) <-> ( A C_ X -> ( A C_ z -> ( F ` A ) C_ z ) ) ) )
24	3 23	spcdvw	|- ( ph -> ( A. w ( w C_ X -> ( w C_ z -> ( F ` w ) C_ z ) ) -> ( A C_ X -> ( A C_ z -> ( F ` A ) C_ z ) ) ) )
25	4 24	mpid	|- ( ph -> ( A. w ( w C_ X -> ( w C_ z -> ( F ` w ) C_ z ) ) -> ( A C_ z -> ( F ` A ) C_ z ) ) )
26	17 25	mpdd	|- ( ph -> ( A. w ( w C_ X -> ( w C_ z -> ( F ` w ) C_ z ) ) -> ( F ` A ) C_ z ) )
27	14 26	jcad	|- ( ph -> ( A. w ( w C_ X -> ( w C_ z -> ( F ` w ) C_ z ) ) -> ( X C_ z /\ ( F ` A ) C_ z ) ) )
28	10 27	syl5	|- ( ph -> ( A. w ( w C_ ( X u. ( F ` A ) ) -> ( w C_ z -> ( F ` w ) C_ z ) ) -> ( X C_ z /\ ( F ` A ) C_ z ) ) )
29		unss	|- ( ( X C_ z /\ ( F ` A ) C_ z ) <-> ( X u. ( F ` A ) ) C_ z )
30	28 29	syl6ib	|- ( ph -> ( A. w ( w C_ ( X u. ( F ` A ) ) -> ( w C_ z -> ( F ` w ) C_ z ) ) -> ( X u. ( F ` A ) ) C_ z ) )
31	1 30	alrimi	|- ( ph -> A. z ( A. w ( w C_ ( X u. ( F ` A ) ) -> ( w C_ z -> ( F ` w ) C_ z ) ) -> ( X u. ( F ` A ) ) C_ z ) )
32		fvex	|- ( F ` A ) e. _V
33		unexg	|- ( ( X e. Y /\ ( F ` A ) e. _V ) -> ( X u. ( F ` A ) ) e. _V )
34	5 32 33	sylancl	|- ( ph -> ( X u. ( F ` A ) ) e. _V )
35	2 34	setrec1lem1	|- ( ph -> ( ( X u. ( F ` A ) ) e. Y <-> A. z ( A. w ( w C_ ( X u. ( F ` A ) ) -> ( w C_ z -> ( F ` w ) C_ z ) ) -> ( X u. ( F ` A ) ) C_ z ) ) )
36	31 35	mpbird	|- ( ph -> ( X u. ( F ` A ) ) e. Y )