Theorem exrecfn

Description: Theorem about the existence of infinite recursive sets. y should usually be free in B . (Contributed by ML, 30-Mar-2022)

	Ref	Expression
Assertion	exrecfn	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑦 𝐵 ∈ 𝑊 ) → ∃ 𝑥 ( 𝐴 ⊆ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 𝐵 ∈ 𝑥 ) )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( 𝑧 ∈ V ↦ ( 𝑧 ∪ ran ( 𝑦 ∈ 𝑧 ↦ 𝐵 ) ) ) = ( 𝑧 ∈ V ↦ ( 𝑧 ∪ ran ( 𝑦 ∈ 𝑧 ↦ 𝐵 ) ) )
2	1	exrecfnlem	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑦 𝐵 ∈ 𝑊 ) → ∃ 𝑥 ( 𝐴 ⊆ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 𝐵 ∈ 𝑥 ) )