modelaxreplem1

Description: Lemma for modelaxrep . We show that M is closed under taking subsets. (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$
	modelaxreplem1.5	$⊢ A \subseteq x$
Assertion	modelaxreplem1	$⊢ ψ \to A \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		modelaxreplem1.5	$⊢ A \subseteq x$
6		eleq1	$⊢ A = \emptyset \to (A \in M \leftrightarrow \emptyset \in M)$
7	3 6	syl5ibrcom	$⊢ ψ \to (A = \emptyset \to A \in M)$
8		vex	$⊢ x \in V$
9	8 5	ssexi	$⊢ A \in V$
10	9	0sdom	$⊢ \emptyset ≺ A \leftrightarrow A \neq \emptyset$
11		ssdomg	$⊢ x \in V \to (A \subseteq x \to A ≼ x)$
12	8 5 11	mp2	$⊢ A ≼ x$
13		fodomr	$⊢ (\emptyset ≺ A \land A ≼ x) \to \exists g g : x \underset{onto}{⟶} A$
14	12 13	mpan2	$⊢ \emptyset ≺ A \to \exists g g : x \underset{onto}{⟶} A$
15	10 14	sylbir	$⊢ A \neq \emptyset \to \exists g g : x \underset{onto}{⟶} A$
16		df-fo	$⊢ g : x \underset{onto}{⟶} A \leftrightarrow (g Fn x \land ran g = A)$
17		df-fn	$⊢ g Fn x \leftrightarrow (Fun g \land dom g = x)$
18		eleq1	$⊢ dom g = x \to (dom g \in M \leftrightarrow x \in M)$
19	4 18	syl5ibrcom	$⊢ ψ \to (dom g = x \to dom g \in M)$
20	19	anim2d	$⊢ ψ \to ((Fun g \land dom g = x) \to (Fun g \land dom g \in M))$
21	17 20	biimtrid	$⊢ ψ \to (g Fn x \to (Fun g \land dom g \in M))$
22	5 1	sstrid	$⊢ ψ \to A \subseteq M$
23		sseq1	$⊢ ran g = A \to (ran g \subseteq M \leftrightarrow A \subseteq M)$
24	22 23	syl5ibrcom	$⊢ ψ \to (ran g = A \to ran g \subseteq M)$
25		df-3an	$⊢ (Fun g \land dom g \in M \land ran g \subseteq M) \leftrightarrow ((Fun g \land dom g \in M) \land ran g \subseteq M)$
26		funeq	$⊢ f = g \to (Fun f \leftrightarrow Fun g)$
27		dmeq	$⊢ f = g \to dom f = dom g$
28	27	eleq1d	$⊢ f = g \to (dom f \in M \leftrightarrow dom g \in M)$
29		rneq	$⊢ f = g \to ran f = ran g$
30	29	sseq1d	$⊢ f = g \to (ran f \subseteq M \leftrightarrow ran g \subseteq M)$
31	26 28 30	3anbi123d	$⊢ f = g \to ((Fun f \land dom f \in M \land ran f \subseteq M) \leftrightarrow (Fun g \land dom g \in M \land ran g \subseteq M))$
32	29	eleq1d	$⊢ f = g \to (ran f \in M \leftrightarrow ran g \in M)$
33	31 32	imbi12d	$⊢ f = g \to (((Fun f \land dom f \in M \land ran f \subseteq M) \to ran f \in M) \leftrightarrow ((Fun g \land dom g \in M \land ran g \subseteq M) \to ran g \in M))$
34	33	spvv	$⊢ \forall f ((Fun f \land dom f \in M \land ran f \subseteq M) \to ran f \in M) \to ((Fun g \land dom g \in M \land ran g \subseteq M) \to ran g \in M)$
35	2 34	syl	$⊢ ψ \to ((Fun g \land dom g \in M \land ran g \subseteq M) \to ran g \in M)$
36	25 35	biimtrrid	$⊢ ψ \to (((Fun g \land dom g \in M) \land ran g \subseteq M) \to ran g \in M)$
37	21 24 36	syl2and	$⊢ ψ \to ((g Fn x \land ran g = A) \to ran g \in M)$
38		eleq1	$⊢ ran g = A \to (ran g \in M \leftrightarrow A \in M)$
39	38	adantl	$⊢ (g Fn x \land ran g = A) \to (ran g \in M \leftrightarrow A \in M)$
40	37 39	mpbidi	$⊢ ψ \to ((g Fn x \land ran g = A) \to A \in M)$
41	16 40	biimtrid	$⊢ ψ \to (g : x \underset{onto}{⟶} A \to A \in M)$
42	41	exlimdv	$⊢ ψ \to (\exists g g : x \underset{onto}{⟶} A \to A \in M)$
43	15 42	syl5	$⊢ ψ \to (A \neq \emptyset \to A \in M)$
44	7 43	pm2.61dne	$⊢ ψ \to A \in M$

Metamath Proof Explorer

Theorem modelaxreplem1

Proof