modelaxreplem2

Description: Lemma for modelaxrep . We define a class F and show that the antecedent of Replacement implies that F is a function. We use Replacement (in the form of funex ) to show that F exists. Then we show that, under our hypotheses, the range of F is a member of M . (Contributed by Eric Schmidt, 29-Sep-2025)

	Ref	Expression
Hypotheses	modelaxreplem.1	$⊢ ψ \to x \subseteq M$
	modelaxreplem.2	$⊢ ψ \to \forall f ((Fun f \land dom f \in M \land ran f \subseteq M) \to ran f \in M)$
	modelaxreplem.3	$⊢ ψ \to \emptyset \in M$
	modelaxreplem.4	$⊢ ψ \to x \in M$
	modelaxreplem2.5	$⊢ Ⅎ w ψ$
	modelaxreplem2.6	$⊢ Ⅎ z ψ$
	modelaxreplem2.7	$⊢ \underline{Ⅎ} z F$
	modelaxreplem2.8	$⊢ F = \{⟨w, z⟩ \| (w \in x \land (z \in M \land \forall y φ))\}$
	modelaxreplem2.9	$⊢ ψ \to (w \in M \to \exists y \in M \forall z \in M (\forall y φ \to z = y))$
Assertion	modelaxreplem2	$⊢ ψ \to ran F \in M$

Proof

Step	Hyp	Ref	Expression
1		modelaxreplem.1	$⊢ ψ \to x \subseteq M$
2		modelaxreplem.2	$⊢ ψ \to \forall f ((Fun f \land dom f \in M \land ran f \subseteq M) \to ran f \in M)$
3		modelaxreplem.3	$⊢ ψ \to \emptyset \in M$
4		modelaxreplem.4	$⊢ ψ \to x \in M$
5		modelaxreplem2.5	$⊢ Ⅎ w ψ$
6		modelaxreplem2.6	$⊢ Ⅎ z ψ$
7		modelaxreplem2.7	$⊢ \underline{Ⅎ} z F$
8		modelaxreplem2.8	$⊢ F = \{⟨w, z⟩ \| (w \in x \land (z \in M \land \forall y φ))\}$
9		modelaxreplem2.9	$⊢ ψ \to (w \in M \to \exists y \in M \forall z \in M (\forall y φ \to z = y))$
10	1	sseld	$⊢ ψ \to (w \in x \to w \in M)$
11		nfa1	$⊢ Ⅎ y \forall y φ$
12	11	rmo2i	$⊢ \exists y \in M \forall z \in M (\forall y φ \to z = y) \to \exists^{*} z \in M \forall y φ$
13		df-rmo	$⊢ \exists^{} z \in M \forall y φ \leftrightarrow \exists^{} z (z \in M \land \forall y φ)$
14	12 13	sylib	$⊢ \exists y \in M \forall z \in M (\forall y φ \to z = y) \to \exists^{*} z (z \in M \land \forall y φ)$
15	9 14	syl6	$⊢ ψ \to (w \in M \to \exists^{*} z (z \in M \land \forall y φ))$
16	10 15	syld	$⊢ ψ \to (w \in x \to \exists^{*} z (z \in M \land \forall y φ))$
17		moanimv	$⊢ \exists^{} z (w \in x \land (z \in M \land \forall y φ)) \leftrightarrow (w \in x \to \exists^{} z (z \in M \land \forall y φ))$
18	16 17	sylibr	$⊢ ψ \to \exists^{*} z (w \in x \land (z \in M \land \forall y φ))$
19	5 18	alrimi	$⊢ ψ \to \forall w \exists^{*} z (w \in x \land (z \in M \land \forall y φ))$
20	8	funeqi	$⊢ Fun F \leftrightarrow Fun \{⟨w, z⟩ \| (w \in x \land (z \in M \land \forall y φ))\}$
21		funopab	$⊢ Fun \{⟨w, z⟩ \| (w \in x \land (z \in M \land \forall y φ))\} \leftrightarrow \forall w \exists^{*} z (w \in x \land (z \in M \land \forall y φ))$
22	20 21	bitri	$⊢ Fun F \leftrightarrow \forall w \exists^{*} z (w \in x \land (z \in M \land \forall y φ))$
23	19 22	sylibr	$⊢ ψ \to Fun F$
24	8	dmeqi	$⊢ dom F = dom \{⟨w, z⟩ \| (w \in x \land (z \in M \land \forall y φ))\}$
25		dmopabss	$⊢ dom \{⟨w, z⟩ \| (w \in x \land (z \in M \land \forall y φ))\} \subseteq x$
26	24 25	eqsstri	$⊢ dom F \subseteq x$
27	1 2 3 4 26	modelaxreplem1	$⊢ ψ \to dom F \in M$
28		an12	$⊢ (w \in x \land (z \in M \land \forall y φ)) \leftrightarrow (z \in M \land (w \in x \land \forall y φ))$
29	28	opabbii	$⊢ \{⟨w, z⟩ \| (w \in x \land (z \in M \land \forall y φ))\} = \{⟨w, z⟩ \| (z \in M \land (w \in x \land \forall y φ))\}$
30	8 29	eqtri	$⊢ F = \{⟨w, z⟩ \| (z \in M \land (w \in x \land \forall y φ))\}$
31	30	rneqi	$⊢ ran F = ran \{⟨w, z⟩ \| (z \in M \land (w \in x \land \forall y φ))\}$
32		rnopabss	$⊢ ran \{⟨w, z⟩ \| (z \in M \land (w \in x \land \forall y φ))\} \subseteq M$
33	31 32	eqsstri	$⊢ ran F \subseteq M$
34	33	a1i	$⊢ ψ \to ran F \subseteq M$
35		funex	$⊢ (Fun F \land dom F \in M) \to F \in V$
36	23 27 35	syl2anc	$⊢ ψ \to F \in V$
37		funeq	$⊢ f = F \to (Fun f \leftrightarrow Fun F)$
38		dmeq	$⊢ f = F \to dom f = dom F$
39	38	eleq1d	$⊢ f = F \to (dom f \in M \leftrightarrow dom F \in M)$
40		rneq	$⊢ f = F \to ran f = ran F$
41	40	sseq1d	$⊢ f = F \to (ran f \subseteq M \leftrightarrow ran F \subseteq M)$
42	37 39 41	3anbi123d	$⊢ f = F \to ((Fun f \land dom f \in M \land ran f \subseteq M) \leftrightarrow (Fun F \land dom F \in M \land ran F \subseteq M))$
43	40	eleq1d	$⊢ f = F \to (ran f \in M \leftrightarrow ran F \in M)$
44	42 43	imbi12d	$⊢ f = F \to (((Fun f \land dom f \in M \land ran f \subseteq M) \to ran f \in M) \leftrightarrow ((Fun F \land dom F \in M \land ran F \subseteq M) \to ran F \in M))$
45	44	spcgv	$⊢ F \in V \to (\forall f ((Fun f \land dom f \in M \land ran f \subseteq M) \to ran f \in M) \to ((Fun F \land dom F \in M \land ran F \subseteq M) \to ran F \in M))$
46	36 2 45	sylc	$⊢ ψ \to ((Fun F \land dom F \in M \land ran F \subseteq M) \to ran F \in M)$
47	23 27 34 46	mp3and	$⊢ ψ \to ran F \in M$

Metamath Proof Explorer

Theorem modelaxreplem2

Proof