Theorem elsetrecslem

Description: Lemma for elsetrecs . Any element of setrecs ( F ) is generated by some subset of setrecs ( F ) . This is much weaker than setrec2v . To see why this lemma also requires setrec1 , consider what would happen if we replaced B with { A } . The antecedent would still hold, but the consequent would fail in general. Consider dispensing with the deduction form. (Contributed by Emmett Weisz, 11-Jul-2021) (New usage is discouraged.)

	Ref	Expression
Hypothesis	elsetrecs.1	|- B = setrecs ( F )
Assertion	elsetrecslem	|- ( A e. B -> E. x ( x C_ B /\ A e. ( F ` x ) ) )

Proof

Step	Hyp	Ref	Expression
1		elsetrecs.1	|- B = setrecs ( F )
2		ssdifsn	|- ( B C_ ( B \ { A } ) <-> ( B C_ B /\ -. A e. B ) )
3	2	simprbi	|- ( B C_ ( B \ { A } ) -> -. A e. B )
4	3	con2i	|- ( A e. B -> -. B C_ ( B \ { A } ) )
5		sseq1	|- ( x = a -> ( x C_ B <-> a C_ B ) )
6		fveq2	|- ( x = a -> ( F ` x ) = ( F ` a ) )
7	6	eleq2d	|- ( x = a -> ( A e. ( F ` x ) <-> A e. ( F ` a ) ) )
8	5 7	anbi12d	|- ( x = a -> ( ( x C_ B /\ A e. ( F ` x ) ) <-> ( a C_ B /\ A e. ( F ` a ) ) ) )
9	8	notbid	|- ( x = a -> ( -. ( x C_ B /\ A e. ( F ` x ) ) <-> -. ( a C_ B /\ A e. ( F ` a ) ) ) )
10	9	spvv	|- ( A. x -. ( x C_ B /\ A e. ( F ` x ) ) -> -. ( a C_ B /\ A e. ( F ` a ) ) )
11		imnan	|- ( ( a C_ B -> -. A e. ( F ` a ) ) <-> -. ( a C_ B /\ A e. ( F ` a ) ) )
12		idd	|- ( a C_ B -> ( -. A e. ( F ` a ) -> -. A e. ( F ` a ) ) )
13		vex	|- a e. _V
14	13	a1i	|- ( a C_ B -> a e. _V )
15		id	|- ( a C_ B -> a C_ B )
16	1 14 15	setrec1	|- ( a C_ B -> ( F ` a ) C_ B )
17	12 16	jctild	|- ( a C_ B -> ( -. A e. ( F ` a ) -> ( ( F ` a ) C_ B /\ -. A e. ( F ` a ) ) ) )
18	17	a2i	|- ( ( a C_ B -> -. A e. ( F ` a ) ) -> ( a C_ B -> ( ( F ` a ) C_ B /\ -. A e. ( F ` a ) ) ) )
19	11 18	sylbir	|- ( -. ( a C_ B /\ A e. ( F ` a ) ) -> ( a C_ B -> ( ( F ` a ) C_ B /\ -. A e. ( F ` a ) ) ) )
20	19	adantrd	|- ( -. ( a C_ B /\ A e. ( F ` a ) ) -> ( ( a C_ B /\ -. A e. a ) -> ( ( F ` a ) C_ B /\ -. A e. ( F ` a ) ) ) )
21		ssdifsn	|- ( a C_ ( B \ { A } ) <-> ( a C_ B /\ -. A e. a ) )
22		ssdifsn	|- ( ( F ` a ) C_ ( B \ { A } ) <-> ( ( F ` a ) C_ B /\ -. A e. ( F ` a ) ) )
23	20 21 22	3imtr4g	|- ( -. ( a C_ B /\ A e. ( F ` a ) ) -> ( a C_ ( B \ { A } ) -> ( F ` a ) C_ ( B \ { A } ) ) )
24	10 23	syl	|- ( A. x -. ( x C_ B /\ A e. ( F ` x ) ) -> ( a C_ ( B \ { A } ) -> ( F ` a ) C_ ( B \ { A } ) ) )
25	24	alrimiv	|- ( A. x -. ( x C_ B /\ A e. ( F ` x ) ) -> A. a ( a C_ ( B \ { A } ) -> ( F ` a ) C_ ( B \ { A } ) ) )
26	1 25	setrec2v	|- ( A. x -. ( x C_ B /\ A e. ( F ` x ) ) -> B C_ ( B \ { A } ) )
27	4 26	nsyl	|- ( A e. B -> -. A. x -. ( x C_ B /\ A e. ( F ` x ) ) )
28		df-ex	|- ( E. x ( x C_ B /\ A e. ( F ` x ) ) <-> -. A. x -. ( x C_ B /\ A e. ( F ` x ) ) )
29	27 28	sylibr	|- ( A e. B -> E. x ( x C_ B /\ A e. ( F ` x ) ) )