Theorem 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	⊢ ( 𝜓 → 𝑥 ⊆ 𝑀 )
	modelaxreplem.2	⊢ ( 𝜓 → ∀ 𝑓 ( ( Fun 𝑓 ∧ dom 𝑓 ∈ 𝑀 ∧ ran 𝑓 ⊆ 𝑀 ) → ran 𝑓 ∈ 𝑀 ) )
	modelaxreplem.3	⊢ ( 𝜓 → ∅ ∈ 𝑀 )
	modelaxreplem.4	⊢ ( 𝜓 → 𝑥 ∈ 𝑀 )
	modelaxreplem2.5	⊢ Ⅎ 𝑤 𝜓
	modelaxreplem2.6	⊢ Ⅎ 𝑧 𝜓
	modelaxreplem2.7	⊢ Ⅎ 𝑧 𝐹
	modelaxreplem2.8	⊢ 𝐹 = { ⟨ 𝑤 , 𝑧 ⟩ ∣ ( 𝑤 ∈ 𝑥 ∧ ( 𝑧 ∈ 𝑀 ∧ ∀ 𝑦 𝜑 ) ) }
	modelaxreplem2.9	⊢ ( 𝜓 → ( 𝑤 ∈ 𝑀 → ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ∀ 𝑦 𝜑 → 𝑧 = 𝑦 ) ) )
Assertion	modelaxreplem2	⊢ ( 𝜓 → ran 𝐹 ∈ 𝑀 )

Proof

Step	Hyp	Ref	Expression
1		modelaxreplem.1	⊢ ( 𝜓 → 𝑥 ⊆ 𝑀 )
2		modelaxreplem.2	⊢ ( 𝜓 → ∀ 𝑓 ( ( Fun 𝑓 ∧ dom 𝑓 ∈ 𝑀 ∧ ran 𝑓 ⊆ 𝑀 ) → ran 𝑓 ∈ 𝑀 ) )
3		modelaxreplem.3	⊢ ( 𝜓 → ∅ ∈ 𝑀 )
4		modelaxreplem.4	⊢ ( 𝜓 → 𝑥 ∈ 𝑀 )
5		modelaxreplem2.5	⊢ Ⅎ 𝑤 𝜓
6		modelaxreplem2.6	⊢ Ⅎ 𝑧 𝜓
7		modelaxreplem2.7	⊢ Ⅎ 𝑧 𝐹
8		modelaxreplem2.8	⊢ 𝐹 = { ⟨ 𝑤 , 𝑧 ⟩ ∣ ( 𝑤 ∈ 𝑥 ∧ ( 𝑧 ∈ 𝑀 ∧ ∀ 𝑦 𝜑 ) ) }
9		modelaxreplem2.9	⊢ ( 𝜓 → ( 𝑤 ∈ 𝑀 → ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ∀ 𝑦 𝜑 → 𝑧 = 𝑦 ) ) )
10	1	sseld	⊢ ( 𝜓 → ( 𝑤 ∈ 𝑥 → 𝑤 ∈ 𝑀 ) )
11		nfa1	⊢ Ⅎ 𝑦 ∀ 𝑦 𝜑
12	11	rmo2i	⊢ ( ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ∀ 𝑦 𝜑 → 𝑧 = 𝑦 ) → ∃* 𝑧 ∈ 𝑀 ∀ 𝑦 𝜑 )
13		df-rmo	⊢ ( ∃* 𝑧 ∈ 𝑀 ∀ 𝑦 𝜑 ↔ ∃* 𝑧 ( 𝑧 ∈ 𝑀 ∧ ∀ 𝑦 𝜑 ) )
14	12 13	sylib	⊢ ( ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ∀ 𝑦 𝜑 → 𝑧 = 𝑦 ) → ∃* 𝑧 ( 𝑧 ∈ 𝑀 ∧ ∀ 𝑦 𝜑 ) )
15	9 14	syl6	⊢ ( 𝜓 → ( 𝑤 ∈ 𝑀 → ∃* 𝑧 ( 𝑧 ∈ 𝑀 ∧ ∀ 𝑦 𝜑 ) ) )
16	10 15	syld	⊢ ( 𝜓 → ( 𝑤 ∈ 𝑥 → ∃* 𝑧 ( 𝑧 ∈ 𝑀 ∧ ∀ 𝑦 𝜑 ) ) )
17		moanimv	⊢ ( ∃* 𝑧 ( 𝑤 ∈ 𝑥 ∧ ( 𝑧 ∈ 𝑀 ∧ ∀ 𝑦 𝜑 ) ) ↔ ( 𝑤 ∈ 𝑥 → ∃* 𝑧 ( 𝑧 ∈ 𝑀 ∧ ∀ 𝑦 𝜑 ) ) )
18	16 17	sylibr	⊢ ( 𝜓 → ∃* 𝑧 ( 𝑤 ∈ 𝑥 ∧ ( 𝑧 ∈ 𝑀 ∧ ∀ 𝑦 𝜑 ) ) )
19	5 18	alrimi	⊢ ( 𝜓 → ∀ 𝑤 ∃* 𝑧 ( 𝑤 ∈ 𝑥 ∧ ( 𝑧 ∈ 𝑀 ∧ ∀ 𝑦 𝜑 ) ) )
20	8	funeqi	⊢ ( Fun 𝐹 ↔ Fun { ⟨ 𝑤 , 𝑧 ⟩ ∣ ( 𝑤 ∈ 𝑥 ∧ ( 𝑧 ∈ 𝑀 ∧ ∀ 𝑦 𝜑 ) ) } )
21		funopab	⊢ ( Fun { ⟨ 𝑤 , 𝑧 ⟩ ∣ ( 𝑤 ∈ 𝑥 ∧ ( 𝑧 ∈ 𝑀 ∧ ∀ 𝑦 𝜑 ) ) } ↔ ∀ 𝑤 ∃* 𝑧 ( 𝑤 ∈ 𝑥 ∧ ( 𝑧 ∈ 𝑀 ∧ ∀ 𝑦 𝜑 ) ) )
22	20 21	bitri	⊢ ( Fun 𝐹 ↔ ∀ 𝑤 ∃* 𝑧 ( 𝑤 ∈ 𝑥 ∧ ( 𝑧 ∈ 𝑀 ∧ ∀ 𝑦 𝜑 ) ) )
23	19 22	sylibr	⊢ ( 𝜓 → Fun 𝐹 )
24	8	dmeqi	⊢ dom 𝐹 = dom { ⟨ 𝑤 , 𝑧 ⟩ ∣ ( 𝑤 ∈ 𝑥 ∧ ( 𝑧 ∈ 𝑀 ∧ ∀ 𝑦 𝜑 ) ) }
25		dmopabss	⊢ dom { ⟨ 𝑤 , 𝑧 ⟩ ∣ ( 𝑤 ∈ 𝑥 ∧ ( 𝑧 ∈ 𝑀 ∧ ∀ 𝑦 𝜑 ) ) } ⊆ 𝑥
26	24 25	eqsstri	⊢ dom 𝐹 ⊆ 𝑥
27	1 2 3 4 26	modelaxreplem1	⊢ ( 𝜓 → dom 𝐹 ∈ 𝑀 )
28		an12	⊢ ( ( 𝑤 ∈ 𝑥 ∧ ( 𝑧 ∈ 𝑀 ∧ ∀ 𝑦 𝜑 ) ) ↔ ( 𝑧 ∈ 𝑀 ∧ ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 𝜑 ) ) )
29	28	opabbii	⊢ { ⟨ 𝑤 , 𝑧 ⟩ ∣ ( 𝑤 ∈ 𝑥 ∧ ( 𝑧 ∈ 𝑀 ∧ ∀ 𝑦 𝜑 ) ) } = { ⟨ 𝑤 , 𝑧 ⟩ ∣ ( 𝑧 ∈ 𝑀 ∧ ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 𝜑 ) ) }
30	8 29	eqtri	⊢ 𝐹 = { ⟨ 𝑤 , 𝑧 ⟩ ∣ ( 𝑧 ∈ 𝑀 ∧ ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 𝜑 ) ) }
31	30	rneqi	⊢ ran 𝐹 = ran { ⟨ 𝑤 , 𝑧 ⟩ ∣ ( 𝑧 ∈ 𝑀 ∧ ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 𝜑 ) ) }
32		rnopabss	⊢ ran { ⟨ 𝑤 , 𝑧 ⟩ ∣ ( 𝑧 ∈ 𝑀 ∧ ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 𝜑 ) ) } ⊆ 𝑀
33	31 32	eqsstri	⊢ ran 𝐹 ⊆ 𝑀
34	33	a1i	⊢ ( 𝜓 → ran 𝐹 ⊆ 𝑀 )
35		funex	⊢ ( ( Fun 𝐹 ∧ dom 𝐹 ∈ 𝑀 ) → 𝐹 ∈ V )
36	23 27 35	syl2anc	⊢ ( 𝜓 → 𝐹 ∈ V )
37		funeq	⊢ ( 𝑓 = 𝐹 → ( Fun 𝑓 ↔ Fun 𝐹 ) )
38		dmeq	⊢ ( 𝑓 = 𝐹 → dom 𝑓 = dom 𝐹 )
39	38	eleq1d	⊢ ( 𝑓 = 𝐹 → ( dom 𝑓 ∈ 𝑀 ↔ dom 𝐹 ∈ 𝑀 ) )
40		rneq	⊢ ( 𝑓 = 𝐹 → ran 𝑓 = ran 𝐹 )
41	40	sseq1d	⊢ ( 𝑓 = 𝐹 → ( ran 𝑓 ⊆ 𝑀 ↔ ran 𝐹 ⊆ 𝑀 ) )
42	37 39 41	3anbi123d	⊢ ( 𝑓 = 𝐹 → ( ( Fun 𝑓 ∧ dom 𝑓 ∈ 𝑀 ∧ ran 𝑓 ⊆ 𝑀 ) ↔ ( Fun 𝐹 ∧ dom 𝐹 ∈ 𝑀 ∧ ran 𝐹 ⊆ 𝑀 ) ) )
43	40	eleq1d	⊢ ( 𝑓 = 𝐹 → ( ran 𝑓 ∈ 𝑀 ↔ ran 𝐹 ∈ 𝑀 ) )
44	42 43	imbi12d	⊢ ( 𝑓 = 𝐹 → ( ( ( Fun 𝑓 ∧ dom 𝑓 ∈ 𝑀 ∧ ran 𝑓 ⊆ 𝑀 ) → ran 𝑓 ∈ 𝑀 ) ↔ ( ( Fun 𝐹 ∧ dom 𝐹 ∈ 𝑀 ∧ ran 𝐹 ⊆ 𝑀 ) → ran 𝐹 ∈ 𝑀 ) ) )
45	44	spcgv	⊢ ( 𝐹 ∈ V → ( ∀ 𝑓 ( ( Fun 𝑓 ∧ dom 𝑓 ∈ 𝑀 ∧ ran 𝑓 ⊆ 𝑀 ) → ran 𝑓 ∈ 𝑀 ) → ( ( Fun 𝐹 ∧ dom 𝐹 ∈ 𝑀 ∧ ran 𝐹 ⊆ 𝑀 ) → ran 𝐹 ∈ 𝑀 ) ) )
46	36 2 45	sylc	⊢ ( 𝜓 → ( ( Fun 𝐹 ∧ dom 𝐹 ∈ 𝑀 ∧ ran 𝐹 ⊆ 𝑀 ) → ran 𝐹 ∈ 𝑀 ) )
47	23 27 34 46	mp3and	⊢ ( 𝜓 → ran 𝐹 ∈ 𝑀 )