Theorem setrec2mpt

Description: Version of setrec2 where F is defined using maps-to notation. Deduction form is omitted in the second hypothesis for simplicity. In practice, nothing important is lost since we are only interested in one choice of A , S , and V at a time. However, we are interested in what happens when C varies, so deduction form is used in the third hypothesis. (Contributed by Emmett Weisz, 4-Jun-2024)

	Ref	Expression
Hypotheses	setrec2mpt.1	⊢ 𝐵 = setrecs ( ( 𝑎 ∈ 𝐴 ↦ 𝑆 ) )
	setrec2mpt.2	⊢ ( 𝑎 ∈ 𝐴 → 𝑆 ∈ 𝑉 )
	setrec2mpt.3	⊢ ( 𝜑 → ∀ 𝑎 ( 𝑎 ⊆ 𝐶 → 𝑆 ⊆ 𝐶 ) )
Assertion	setrec2mpt	⊢ ( 𝜑 → 𝐵 ⊆ 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		setrec2mpt.1	⊢ 𝐵 = setrecs ( ( 𝑎 ∈ 𝐴 ↦ 𝑆 ) )
2		setrec2mpt.2	⊢ ( 𝑎 ∈ 𝐴 → 𝑆 ∈ 𝑉 )
3		setrec2mpt.3	⊢ ( 𝜑 → ∀ 𝑎 ( 𝑎 ⊆ 𝐶 → 𝑆 ⊆ 𝐶 ) )
4		nfmpt1	⊢ Ⅎ 𝑎 ( 𝑎 ∈ 𝐴 ↦ 𝑆 )
5		eqid	⊢ ( 𝑎 ∈ 𝐴 ↦ 𝑆 ) = ( 𝑎 ∈ 𝐴 ↦ 𝑆 )
6	5	fvmpt2	⊢ ( ( 𝑎 ∈ 𝐴 ∧ 𝑆 ∈ 𝑉 ) → ( ( 𝑎 ∈ 𝐴 ↦ 𝑆 ) ‘ 𝑎 ) = 𝑆 )
7		eqimss	⊢ ( ( ( 𝑎 ∈ 𝐴 ↦ 𝑆 ) ‘ 𝑎 ) = 𝑆 → ( ( 𝑎 ∈ 𝐴 ↦ 𝑆 ) ‘ 𝑎 ) ⊆ 𝑆 )
8	6 7	syl	⊢ ( ( 𝑎 ∈ 𝐴 ∧ 𝑆 ∈ 𝑉 ) → ( ( 𝑎 ∈ 𝐴 ↦ 𝑆 ) ‘ 𝑎 ) ⊆ 𝑆 )
9	2 8	mpdan	⊢ ( 𝑎 ∈ 𝐴 → ( ( 𝑎 ∈ 𝐴 ↦ 𝑆 ) ‘ 𝑎 ) ⊆ 𝑆 )
10	5	fvmptndm	⊢ ( ¬ 𝑎 ∈ 𝐴 → ( ( 𝑎 ∈ 𝐴 ↦ 𝑆 ) ‘ 𝑎 ) = ∅ )
11		0ss	⊢ ∅ ⊆ 𝑆
12	10 11	eqsstrdi	⊢ ( ¬ 𝑎 ∈ 𝐴 → ( ( 𝑎 ∈ 𝐴 ↦ 𝑆 ) ‘ 𝑎 ) ⊆ 𝑆 )
13	9 12	pm2.61i	⊢ ( ( 𝑎 ∈ 𝐴 ↦ 𝑆 ) ‘ 𝑎 ) ⊆ 𝑆
14		sstr2	⊢ ( ( ( 𝑎 ∈ 𝐴 ↦ 𝑆 ) ‘ 𝑎 ) ⊆ 𝑆 → ( 𝑆 ⊆ 𝐶 → ( ( 𝑎 ∈ 𝐴 ↦ 𝑆 ) ‘ 𝑎 ) ⊆ 𝐶 ) )
15	13 14	ax-mp	⊢ ( 𝑆 ⊆ 𝐶 → ( ( 𝑎 ∈ 𝐴 ↦ 𝑆 ) ‘ 𝑎 ) ⊆ 𝐶 )
16	15	imim2i	⊢ ( ( 𝑎 ⊆ 𝐶 → 𝑆 ⊆ 𝐶 ) → ( 𝑎 ⊆ 𝐶 → ( ( 𝑎 ∈ 𝐴 ↦ 𝑆 ) ‘ 𝑎 ) ⊆ 𝐶 ) )
17	3 16	sylg	⊢ ( 𝜑 → ∀ 𝑎 ( 𝑎 ⊆ 𝐶 → ( ( 𝑎 ∈ 𝐴 ↦ 𝑆 ) ‘ 𝑎 ) ⊆ 𝐶 ) )
18	4 1 17	setrec2	⊢ ( 𝜑 → 𝐵 ⊆ 𝐶 )