Theorem setis

Description: Version of setrec2 expressed as an induction schema. This theorem is a generalization of tfis3 . (Contributed by Emmett Weisz, 27-Feb-2022)

	Ref	Expression
Hypotheses	setis.1	|- B = setrecs ( F )
	setis.2	|- ( b = A -> ( ps <-> ch ) )
	setis.3	|- ( ph -> A. a ( A. b e. a ps -> A. b e. ( F ` a ) ps ) )
Assertion	setis	|- ( ph -> ( A e. B -> ch ) )

Proof

Step	Hyp	Ref	Expression
1		setis.1	|- B = setrecs ( F )
2		setis.2	|- ( b = A -> ( ps <-> ch ) )
3		setis.3	|- ( ph -> A. a ( A. b e. a ps -> A. b e. ( F ` a ) ps ) )
4		ssabral	|- ( a C_ { b | ps } <-> A. b e. a ps )
5		ssabral	|- ( ( F ` a ) C_ { b | ps } <-> A. b e. ( F ` a ) ps )
6	4 5	imbi12i	|- ( ( a C_ { b | ps } -> ( F ` a ) C_ { b | ps } ) <-> ( A. b e. a ps -> A. b e. ( F ` a ) ps ) )
7	6	albii	|- ( A. a ( a C_ { b | ps } -> ( F ` a ) C_ { b | ps } ) <-> A. a ( A. b e. a ps -> A. b e. ( F ` a ) ps ) )
8	3 7	sylibr	|- ( ph -> A. a ( a C_ { b | ps } -> ( F ` a ) C_ { b | ps } ) )
9	1 8	setrec2v	|- ( ph -> B C_ { b | ps } )
10	9	sseld	|- ( ph -> ( A e. B -> A e. { b | ps } ) )
11	2	elabg	|- ( A e. B -> ( A e. { b | ps } <-> ch ) )
12	10 11	mpbidi	|- ( ph -> ( A e. B -> ch ) )