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=\mathrm{setrecs}\left(F\right)$$
	setis.2	$$⊢b=A\to \left(\psi \leftrightarrow \chi \right)$$
	setis.3	$$⊢\phi \to \forall a\left(\forall b\in a\psi \to \forall b\in F\left(a\right)\psi \right)$$
Assertion	setis	$$⊢\phi \to \left(A\in B\to \chi \right)$$

Proof

Step	Hyp	Ref	Expression
1		setis.1	$$⊢B=\mathrm{setrecs}\left(F\right)$$
2		setis.2	$$⊢b=A\to \left(\psi \leftrightarrow \chi \right)$$
3		setis.3	$$⊢\phi \to \forall a\left(\forall b\in a\psi \to \forall b\in F\left(a\right)\psi \right)$$
4		ssabral	$$⊢a\subseteq \left\{b|\psi \right\}\leftrightarrow \forall b\in a\psi$$
5		ssabral	$$⊢F\left(a\right)\subseteq \left\{b|\psi \right\}\leftrightarrow \forall b\in F\left(a\right)\psi$$
6	4 5	imbi12i	$$⊢\left(a\subseteq \left\{b|\psi \right\}\to F\left(a\right)\subseteq \left\{b|\psi \right\}\right)\leftrightarrow \left(\forall b\in a\psi \to \forall b\in F\left(a\right)\psi \right)$$
7	6	albii	$$⊢\forall a\left(a\subseteq \left\{b|\psi \right\}\to F\left(a\right)\subseteq \left\{b|\psi \right\}\right)\leftrightarrow \forall a\left(\forall b\in a\psi \to \forall b\in F\left(a\right)\psi \right)$$
8	3 7	sylibr	$$⊢\phi \to \forall a\left(a\subseteq \left\{b|\psi \right\}\to F\left(a\right)\subseteq \left\{b|\psi \right\}\right)$$
9	1 8	setrec2v	$$⊢\phi \to B\subseteq \left\{b|\psi \right\}$$
10	9	sseld	$$⊢\phi \to \left(A\in B\to A\in \left\{b|\psi \right\}\right)$$
11	2	elabg	$$⊢A\in B\to \left(A\in \left\{b|\psi \right\}\leftrightarrow \chi \right)$$
12	10 11	mpbidi	$$⊢\phi \to \left(A\in B\to \chi \right)$$