Theorem elsetrecs

Description: A set A is an element of setrecs ( F ) iff A is generated by some subset of setrecs ( F ) . The proof requires both setrec1 and setrec2 , but this theorem is not strong enough to uniquely determine setrecs ( F ) . If F respects the subset relation, the theorem still holds if both occurrences of e. are replaced by C_ for a stronger version of the theorem. (Contributed by Emmett Weisz, 12-Jul-2021)

	Ref	Expression
Hypothesis	elsetrecs.1	⊢ 𝐵 = setrecs ( 𝐹 )
Assertion	elsetrecs	⊢ ( 𝐴 ∈ 𝐵 ↔ ∃ 𝑥 ( 𝑥 ⊆ 𝐵 ∧ 𝐴 ∈ ( 𝐹 ‘ 𝑥 ) ) )

Proof

Step	Hyp	Ref	Expression
1		elsetrecs.1	⊢ 𝐵 = setrecs ( 𝐹 )
2	1	elsetrecslem	⊢ ( 𝐴 ∈ 𝐵 → ∃ 𝑥 ( 𝑥 ⊆ 𝐵 ∧ 𝐴 ∈ ( 𝐹 ‘ 𝑥 ) ) )
3		vex	⊢ 𝑥 ∈ V
4	3	a1i	⊢ ( 𝑥 ⊆ 𝐵 → 𝑥 ∈ V )
5		id	⊢ ( 𝑥 ⊆ 𝐵 → 𝑥 ⊆ 𝐵 )
6	1 4 5	setrec1	⊢ ( 𝑥 ⊆ 𝐵 → ( 𝐹 ‘ 𝑥 ) ⊆ 𝐵 )
7	6	sselda	⊢ ( ( 𝑥 ⊆ 𝐵 ∧ 𝐴 ∈ ( 𝐹 ‘ 𝑥 ) ) → 𝐴 ∈ 𝐵 )
8	7	exlimiv	⊢ ( ∃ 𝑥 ( 𝑥 ⊆ 𝐵 ∧ 𝐴 ∈ ( 𝐹 ‘ 𝑥 ) ) → 𝐴 ∈ 𝐵 )
9	2 8	impbii	⊢ ( 𝐴 ∈ 𝐵 ↔ ∃ 𝑥 ( 𝑥 ⊆ 𝐵 ∧ 𝐴 ∈ ( 𝐹 ‘ 𝑥 ) ) )