Theorem wfaxrep

Description: The class of well-founded sets models the Axiom of Replacement ax-rep . Actually, our statement is stronger, since it is an instance of Replacement only when all quantifiers in A. y ph are relativized to W . Essentially part of Corollary II.2.5 of Kunen2 p. 112, but note that our Replacement is different from Kunen's. (Contributed by Eric Schmidt, 29-Sep-2025)

	Ref	Expression
Hypothesis	wfax.1	⊢ 𝑊 = ∪ ( 𝑅1 “ On )
Assertion	wfaxrep	⊢ ∀ 𝑥 ∈ 𝑊 ( ∀ 𝑤 ∈ 𝑊 ∃ 𝑦 ∈ 𝑊 ∀ 𝑧 ∈ 𝑊 ( ∀ 𝑦 𝜑 → 𝑧 = 𝑦 ) → ∃ 𝑦 ∈ 𝑊 ∀ 𝑧 ∈ 𝑊 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ 𝑊 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 𝜑 ) ) )

Proof

Step	Hyp	Ref	Expression
1		wfax.1	⊢ 𝑊 = ∪ ( 𝑅1 “ On )
2		trwf	⊢ Tr ∪ ( 𝑅1 “ On )
3		treq	⊢ ( 𝑊 = ∪ ( 𝑅1 “ On ) → ( Tr 𝑊 ↔ Tr ∪ ( 𝑅1 “ On ) ) )
4	2 3	mpbiri	⊢ ( 𝑊 = ∪ ( 𝑅1 “ On ) → Tr 𝑊 )
5		vex	⊢ 𝑓 ∈ V
6	5	rnex	⊢ ran 𝑓 ∈ V
7	6	r1elss	⊢ ( ran 𝑓 ∈ ∪ ( 𝑅1 “ On ) ↔ ran 𝑓 ⊆ ∪ ( 𝑅1 “ On ) )
8	7	biimpri	⊢ ( ran 𝑓 ⊆ ∪ ( 𝑅1 “ On ) → ran 𝑓 ∈ ∪ ( 𝑅1 “ On ) )
9	1	sseq2i	⊢ ( ran 𝑓 ⊆ 𝑊 ↔ ran 𝑓 ⊆ ∪ ( 𝑅1 “ On ) )
10	1	eleq2i	⊢ ( ran 𝑓 ∈ 𝑊 ↔ ran 𝑓 ∈ ∪ ( 𝑅1 “ On ) )
11	8 9 10	3imtr4i	⊢ ( ran 𝑓 ⊆ 𝑊 → ran 𝑓 ∈ 𝑊 )
12	11	3ad2ant3	⊢ ( ( Fun 𝑓 ∧ dom 𝑓 ∈ 𝑊 ∧ ran 𝑓 ⊆ 𝑊 ) → ran 𝑓 ∈ 𝑊 )
13	12	ax-gen	⊢ ∀ 𝑓 ( ( Fun 𝑓 ∧ dom 𝑓 ∈ 𝑊 ∧ ran 𝑓 ⊆ 𝑊 ) → ran 𝑓 ∈ 𝑊 )
14	13	a1i	⊢ ( 𝑊 = ∪ ( 𝑅1 “ On ) → ∀ 𝑓 ( ( Fun 𝑓 ∧ dom 𝑓 ∈ 𝑊 ∧ ran 𝑓 ⊆ 𝑊 ) → ran 𝑓 ∈ 𝑊 ) )
15		onwf	⊢ On ⊆ ∪ ( 𝑅1 “ On )
16		0elon	⊢ ∅ ∈ On
17	15 16	sselii	⊢ ∅ ∈ ∪ ( 𝑅1 “ On )
18		eleq2	⊢ ( 𝑊 = ∪ ( 𝑅1 “ On ) → ( ∅ ∈ 𝑊 ↔ ∅ ∈ ∪ ( 𝑅1 “ On ) ) )
19	17 18	mpbiri	⊢ ( 𝑊 = ∪ ( 𝑅1 “ On ) → ∅ ∈ 𝑊 )
20	4 14 19	modelaxrep	⊢ ( 𝑊 = ∪ ( 𝑅1 “ On ) → ∀ 𝑥 ∈ 𝑊 ( ∀ 𝑤 ∈ 𝑊 ∃ 𝑦 ∈ 𝑊 ∀ 𝑧 ∈ 𝑊 ( ∀ 𝑦 𝜑 → 𝑧 = 𝑦 ) → ∃ 𝑦 ∈ 𝑊 ∀ 𝑧 ∈ 𝑊 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ 𝑊 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 𝜑 ) ) ) )
21	1 20	ax-mp	⊢ ∀ 𝑥 ∈ 𝑊 ( ∀ 𝑤 ∈ 𝑊 ∃ 𝑦 ∈ 𝑊 ∀ 𝑧 ∈ 𝑊 ( ∀ 𝑦 𝜑 → 𝑧 = 𝑦 ) → ∃ 𝑦 ∈ 𝑊 ∀ 𝑧 ∈ 𝑊 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ 𝑊 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 𝜑 ) ) )