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	$⊢ B = setrecs ((a \in A ⟼ S))$
	setrec2mpt.2	$⊢ a \in A \to S \in V$
	setrec2mpt.3	$⊢ φ \to \forall a (a \subseteq C \to S \subseteq C)$
Assertion	setrec2mpt	$⊢ φ \to B \subseteq C$

Proof

Step	Hyp	Ref	Expression
1		setrec2mpt.1	$⊢ B = setrecs ((a \in A ⟼ S))$
2		setrec2mpt.2	$⊢ a \in A \to S \in V$
3		setrec2mpt.3	$⊢ φ \to \forall a (a \subseteq C \to S \subseteq C)$
4		nfmpt1	$⊢ \underline{Ⅎ} a (a \in A ⟼ S)$
5		eqid	$⊢ (a \in A ⟼ S) = (a \in A ⟼ S)$
6	5	fvmpt2	$⊢ (a \in A \land S \in V) \to (a \in A ⟼ S) (a) = S$
7		eqimss	$⊢ (a \in A ⟼ S) (a) = S \to (a \in A ⟼ S) (a) \subseteq S$
8	6 7	syl	$⊢ (a \in A \land S \in V) \to (a \in A ⟼ S) (a) \subseteq S$
9	2 8	mpdan	$⊢ a \in A \to (a \in A ⟼ S) (a) \subseteq S$
10	5	fvmptndm	$⊢ \neg a \in A \to (a \in A ⟼ S) (a) = \emptyset$
11		0ss	$⊢ \emptyset \subseteq S$
12	10 11	eqsstrdi	$⊢ \neg a \in A \to (a \in A ⟼ S) (a) \subseteq S$
13	9 12	pm2.61i	$⊢ (a \in A ⟼ S) (a) \subseteq S$
14		sstr2	$⊢ (a \in A ⟼ S) (a) \subseteq S \to (S \subseteq C \to (a \in A ⟼ S) (a) \subseteq C)$
15	13 14	ax-mp	$⊢ S \subseteq C \to (a \in A ⟼ S) (a) \subseteq C$
16	15	imim2i	$⊢ (a \subseteq C \to S \subseteq C) \to (a \subseteq C \to (a \in A ⟼ S) (a) \subseteq C)$
17	3 16	sylg	$⊢ φ \to \forall a (a \subseteq C \to (a \in A ⟼ S) (a) \subseteq C)$
18	4 1 17	setrec2	$⊢ φ \to B \subseteq C$

Metamath Proof Explorer

Theorem setrec2mpt

Proof