Theorem modelaxreplem3

Description: Lemma for modelaxrep . We show that the consequent of Replacement is satisfied with ran F as the value of y . (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	modelaxreplem3	⊢ ( 𝜓 → ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 𝜑 ) ) )

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 2 3 4 5 6 7 8 9	modelaxreplem2	⊢ ( 𝜓 → ran 𝐹 ∈ 𝑀 )
11	1	sseld	⊢ ( 𝜓 → ( 𝑤 ∈ 𝑥 → 𝑤 ∈ 𝑀 ) )
12	11	pm4.71rd	⊢ ( 𝜓 → ( 𝑤 ∈ 𝑥 ↔ ( 𝑤 ∈ 𝑀 ∧ 𝑤 ∈ 𝑥 ) ) )
13	12	anbi1d	⊢ ( 𝜓 → ( ( 𝑤 ∈ 𝑥 ∧ ( 𝑧 ∈ 𝑀 ∧ ∀ 𝑦 𝜑 ) ) ↔ ( ( 𝑤 ∈ 𝑀 ∧ 𝑤 ∈ 𝑥 ) ∧ ( 𝑧 ∈ 𝑀 ∧ ∀ 𝑦 𝜑 ) ) ) )
14		an12	⊢ ( ( ( 𝑤 ∈ 𝑀 ∧ 𝑤 ∈ 𝑥 ) ∧ ( 𝑧 ∈ 𝑀 ∧ ∀ 𝑦 𝜑 ) ) ↔ ( 𝑧 ∈ 𝑀 ∧ ( ( 𝑤 ∈ 𝑀 ∧ 𝑤 ∈ 𝑥 ) ∧ ∀ 𝑦 𝜑 ) ) )
15		anass	⊢ ( ( ( 𝑤 ∈ 𝑀 ∧ 𝑤 ∈ 𝑥 ) ∧ ∀ 𝑦 𝜑 ) ↔ ( 𝑤 ∈ 𝑀 ∧ ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 𝜑 ) ) )
16	15	anbi2i	⊢ ( ( 𝑧 ∈ 𝑀 ∧ ( ( 𝑤 ∈ 𝑀 ∧ 𝑤 ∈ 𝑥 ) ∧ ∀ 𝑦 𝜑 ) ) ↔ ( 𝑧 ∈ 𝑀 ∧ ( 𝑤 ∈ 𝑀 ∧ ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 𝜑 ) ) ) )
17	14 16	bitri	⊢ ( ( ( 𝑤 ∈ 𝑀 ∧ 𝑤 ∈ 𝑥 ) ∧ ( 𝑧 ∈ 𝑀 ∧ ∀ 𝑦 𝜑 ) ) ↔ ( 𝑧 ∈ 𝑀 ∧ ( 𝑤 ∈ 𝑀 ∧ ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 𝜑 ) ) ) )
18	13 17	bitrdi	⊢ ( 𝜓 → ( ( 𝑤 ∈ 𝑥 ∧ ( 𝑧 ∈ 𝑀 ∧ ∀ 𝑦 𝜑 ) ) ↔ ( 𝑧 ∈ 𝑀 ∧ ( 𝑤 ∈ 𝑀 ∧ ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 𝜑 ) ) ) ) )
19	5 18	exbid	⊢ ( 𝜓 → ( ∃ 𝑤 ( 𝑤 ∈ 𝑥 ∧ ( 𝑧 ∈ 𝑀 ∧ ∀ 𝑦 𝜑 ) ) ↔ ∃ 𝑤 ( 𝑧 ∈ 𝑀 ∧ ( 𝑤 ∈ 𝑀 ∧ ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 𝜑 ) ) ) ) )
20	8	rneqi	⊢ ran 𝐹 = ran { ⟨ 𝑤 , 𝑧 ⟩ ∣ ( 𝑤 ∈ 𝑥 ∧ ( 𝑧 ∈ 𝑀 ∧ ∀ 𝑦 𝜑 ) ) }
21		rnopab	⊢ ran { ⟨ 𝑤 , 𝑧 ⟩ ∣ ( 𝑤 ∈ 𝑥 ∧ ( 𝑧 ∈ 𝑀 ∧ ∀ 𝑦 𝜑 ) ) } = { 𝑧 ∣ ∃ 𝑤 ( 𝑤 ∈ 𝑥 ∧ ( 𝑧 ∈ 𝑀 ∧ ∀ 𝑦 𝜑 ) ) }
22	20 21	eqtri	⊢ ran 𝐹 = { 𝑧 ∣ ∃ 𝑤 ( 𝑤 ∈ 𝑥 ∧ ( 𝑧 ∈ 𝑀 ∧ ∀ 𝑦 𝜑 ) ) }
23	22	eqabri	⊢ ( 𝑧 ∈ ran 𝐹 ↔ ∃ 𝑤 ( 𝑤 ∈ 𝑥 ∧ ( 𝑧 ∈ 𝑀 ∧ ∀ 𝑦 𝜑 ) ) )
24		df-rex	⊢ ( ∃ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 𝜑 ) ↔ ∃ 𝑤 ( 𝑤 ∈ 𝑀 ∧ ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 𝜑 ) ) )
25	24	anbi2i	⊢ ( ( 𝑧 ∈ 𝑀 ∧ ∃ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 𝜑 ) ) ↔ ( 𝑧 ∈ 𝑀 ∧ ∃ 𝑤 ( 𝑤 ∈ 𝑀 ∧ ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 𝜑 ) ) ) )
26		19.42v	⊢ ( ∃ 𝑤 ( 𝑧 ∈ 𝑀 ∧ ( 𝑤 ∈ 𝑀 ∧ ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 𝜑 ) ) ) ↔ ( 𝑧 ∈ 𝑀 ∧ ∃ 𝑤 ( 𝑤 ∈ 𝑀 ∧ ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 𝜑 ) ) ) )
27	25 26	bitr4i	⊢ ( ( 𝑧 ∈ 𝑀 ∧ ∃ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 𝜑 ) ) ↔ ∃ 𝑤 ( 𝑧 ∈ 𝑀 ∧ ( 𝑤 ∈ 𝑀 ∧ ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 𝜑 ) ) ) )
28	19 23 27	3bitr4g	⊢ ( 𝜓 → ( 𝑧 ∈ ran 𝐹 ↔ ( 𝑧 ∈ 𝑀 ∧ ∃ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 𝜑 ) ) ) )
29	28	baibd	⊢ ( ( 𝜓 ∧ 𝑧 ∈ 𝑀 ) → ( 𝑧 ∈ ran 𝐹 ↔ ∃ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 𝜑 ) ) )
30	6 29	ralrimia	⊢ ( 𝜓 → ∀ 𝑧 ∈ 𝑀 ( 𝑧 ∈ ran 𝐹 ↔ ∃ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 𝜑 ) ) )
31	7	nfrn	⊢ Ⅎ 𝑧 ran 𝐹
32		sbcralt	⊢ ( ( ran 𝐹 ∈ 𝑀 ∧ Ⅎ 𝑧 ran 𝐹 ) → ( [ ran 𝐹 / 𝑦 ] ∀ 𝑧 ∈ 𝑀 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 𝜑 ) ) ↔ ∀ 𝑧 ∈ 𝑀 [ ran 𝐹 / 𝑦 ] ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 𝜑 ) ) ) )
33	31 32	mpan2	⊢ ( ran 𝐹 ∈ 𝑀 → ( [ ran 𝐹 / 𝑦 ] ∀ 𝑧 ∈ 𝑀 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 𝜑 ) ) ↔ ∀ 𝑧 ∈ 𝑀 [ ran 𝐹 / 𝑦 ] ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 𝜑 ) ) ) )
34	31	nfel1	⊢ Ⅎ 𝑧 ran 𝐹 ∈ 𝑀
35		sbcbig	⊢ ( ran 𝐹 ∈ 𝑀 → ( [ ran 𝐹 / 𝑦 ] ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 𝜑 ) ) ↔ ( [ ran 𝐹 / 𝑦 ] 𝑧 ∈ 𝑦 ↔ [ ran 𝐹 / 𝑦 ] ∃ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 𝜑 ) ) ) )
36		sbcel2gv	⊢ ( ran 𝐹 ∈ 𝑀 → ( [ ran 𝐹 / 𝑦 ] 𝑧 ∈ 𝑦 ↔ 𝑧 ∈ ran 𝐹 ) )
37		nfcv	⊢ Ⅎ 𝑦 𝑀
38		nfv	⊢ Ⅎ 𝑦 𝑤 ∈ 𝑥
39		nfa1	⊢ Ⅎ 𝑦 ∀ 𝑦 𝜑
40	38 39	nfan	⊢ Ⅎ 𝑦 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 𝜑 )
41	37 40	nfrexw	⊢ Ⅎ 𝑦 ∃ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 𝜑 )
42	41	sbcgf	⊢ ( ran 𝐹 ∈ 𝑀 → ( [ ran 𝐹 / 𝑦 ] ∃ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 𝜑 ) ↔ ∃ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 𝜑 ) ) )
43	36 42	bibi12d	⊢ ( ran 𝐹 ∈ 𝑀 → ( ( [ ran 𝐹 / 𝑦 ] 𝑧 ∈ 𝑦 ↔ [ ran 𝐹 / 𝑦 ] ∃ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 𝜑 ) ) ↔ ( 𝑧 ∈ ran 𝐹 ↔ ∃ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 𝜑 ) ) ) )
44	35 43	bitrd	⊢ ( ran 𝐹 ∈ 𝑀 → ( [ ran 𝐹 / 𝑦 ] ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 𝜑 ) ) ↔ ( 𝑧 ∈ ran 𝐹 ↔ ∃ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 𝜑 ) ) ) )
45	34 44	ralbid	⊢ ( ran 𝐹 ∈ 𝑀 → ( ∀ 𝑧 ∈ 𝑀 [ ran 𝐹 / 𝑦 ] ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 𝜑 ) ) ↔ ∀ 𝑧 ∈ 𝑀 ( 𝑧 ∈ ran 𝐹 ↔ ∃ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 𝜑 ) ) ) )
46	33 45	bitrd	⊢ ( ran 𝐹 ∈ 𝑀 → ( [ ran 𝐹 / 𝑦 ] ∀ 𝑧 ∈ 𝑀 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 𝜑 ) ) ↔ ∀ 𝑧 ∈ 𝑀 ( 𝑧 ∈ ran 𝐹 ↔ ∃ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 𝜑 ) ) ) )
47	10 46	syl	⊢ ( 𝜓 → ( [ ran 𝐹 / 𝑦 ] ∀ 𝑧 ∈ 𝑀 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 𝜑 ) ) ↔ ∀ 𝑧 ∈ 𝑀 ( 𝑧 ∈ ran 𝐹 ↔ ∃ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 𝜑 ) ) ) )
48	30 47	mpbird	⊢ ( 𝜓 → [ ran 𝐹 / 𝑦 ] ∀ 𝑧 ∈ 𝑀 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 𝜑 ) ) )
49	10 48	rspesbcd	⊢ ( 𝜓 → ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 𝜑 ) ) )