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	⊢ 𝐵 = setrecs ( 𝐹 )
	setis.2	⊢ ( 𝑏 = 𝐴 → ( 𝜓 ↔ 𝜒 ) )
	setis.3	⊢ ( 𝜑 → ∀ 𝑎 ( ∀ 𝑏 ∈ 𝑎 𝜓 → ∀ 𝑏 ∈ ( 𝐹 ‘ 𝑎 ) 𝜓 ) )
Assertion	setis	⊢ ( 𝜑 → ( 𝐴 ∈ 𝐵 → 𝜒 ) )

Proof

Step	Hyp	Ref	Expression
1		setis.1	⊢ 𝐵 = setrecs ( 𝐹 )
2		setis.2	⊢ ( 𝑏 = 𝐴 → ( 𝜓 ↔ 𝜒 ) )
3		setis.3	⊢ ( 𝜑 → ∀ 𝑎 ( ∀ 𝑏 ∈ 𝑎 𝜓 → ∀ 𝑏 ∈ ( 𝐹 ‘ 𝑎 ) 𝜓 ) )
4		ssabral	⊢ ( 𝑎 ⊆ { 𝑏 ∣ 𝜓 } ↔ ∀ 𝑏 ∈ 𝑎 𝜓 )
5		ssabral	⊢ ( ( 𝐹 ‘ 𝑎 ) ⊆ { 𝑏 ∣ 𝜓 } ↔ ∀ 𝑏 ∈ ( 𝐹 ‘ 𝑎 ) 𝜓 )
6	4 5	imbi12i	⊢ ( ( 𝑎 ⊆ { 𝑏 ∣ 𝜓 } → ( 𝐹 ‘ 𝑎 ) ⊆ { 𝑏 ∣ 𝜓 } ) ↔ ( ∀ 𝑏 ∈ 𝑎 𝜓 → ∀ 𝑏 ∈ ( 𝐹 ‘ 𝑎 ) 𝜓 ) )
7	6	albii	⊢ ( ∀ 𝑎 ( 𝑎 ⊆ { 𝑏 ∣ 𝜓 } → ( 𝐹 ‘ 𝑎 ) ⊆ { 𝑏 ∣ 𝜓 } ) ↔ ∀ 𝑎 ( ∀ 𝑏 ∈ 𝑎 𝜓 → ∀ 𝑏 ∈ ( 𝐹 ‘ 𝑎 ) 𝜓 ) )
8	3 7	sylibr	⊢ ( 𝜑 → ∀ 𝑎 ( 𝑎 ⊆ { 𝑏 ∣ 𝜓 } → ( 𝐹 ‘ 𝑎 ) ⊆ { 𝑏 ∣ 𝜓 } ) )
9	1 8	setrec2v	⊢ ( 𝜑 → 𝐵 ⊆ { 𝑏 ∣ 𝜓 } )
10	9	sseld	⊢ ( 𝜑 → ( 𝐴 ∈ 𝐵 → 𝐴 ∈ { 𝑏 ∣ 𝜓 } ) )
11	2	elabg	⊢ ( 𝐴 ∈ 𝐵 → ( 𝐴 ∈ { 𝑏 ∣ 𝜓 } ↔ 𝜒 ) )
12	10 11	mpbidi	⊢ ( 𝜑 → ( 𝐴 ∈ 𝐵 → 𝜒 ) )