Metamath Proof Explorer

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 ⊢ W = ⋃ R1 On
Assertion wfaxrep ⊢ ∀ x ∈ W ∀ w ∈ W ∃ y ∈ W ∀ z ∈ W ∀ y φ → z = y → ∃ y ∈ W ∀ z ∈ W z ∈ y ↔ ∃ w ∈ W w ∈ x ∧ ∀ y φ

Proof

Step Hyp Ref Expression
1 wfax.1 ⊢ W = ⋃ R1 On
2 trwf ⊢ Tr ⁡ ⋃ R1 On
3 treq ⊢ W = ⋃ R1 On → Tr ⁡ W ↔ Tr ⁡ ⋃ R1 On
4 2 3 mpbiri ⊢ W = ⋃ R1 On → Tr ⁡ W
5 vex ⊢ f ∈ V
6 5 rnex ⊢ ran ⁡ f ∈ V
7 6 r1elss ⊢ ran ⁡ f ∈ ⋃ R1 On ↔ ran ⁡ f ⊆ ⋃ R1 On
8 7 biimpri ⊢ ran ⁡ f ⊆ ⋃ R1 On → ran ⁡ f ∈ ⋃ R1 On
9 1 sseq2i ⊢ ran ⁡ f ⊆ W ↔ ran ⁡ f ⊆ ⋃ R1 On
10 1 eleq2i ⊢ ran ⁡ f ∈ W ↔ ran ⁡ f ∈ ⋃ R1 On
11 8 9 10 3imtr4i ⊢ ran ⁡ f ⊆ W → ran ⁡ f ∈ W
12 11 3ad2ant3 ⊢ Fun ⁡ f ∧ dom ⁡ f ∈ W ∧ ran ⁡ f ⊆ W → ran ⁡ f ∈ W
13 12 ax-gen ⊢ ∀ f Fun ⁡ f ∧ dom ⁡ f ∈ W ∧ ran ⁡ f ⊆ W → ran ⁡ f ∈ W
14 13 a1i ⊢ W = ⋃ R1 On → ∀ f Fun ⁡ f ∧ dom ⁡ f ∈ W ∧ ran ⁡ f ⊆ W → ran ⁡ f ∈ W
15 onwf ⊢ On ⊆ ⋃ R1 On
16 0elon ⊢ ∅ ∈ On
17 15 16 sselii ⊢ ∅ ∈ ⋃ R1 On
18 eleq2 ⊢ W = ⋃ R1 On → ∅ ∈ W ↔ ∅ ∈ ⋃ R1 On
19 17 18 mpbiri ⊢ W = ⋃ R1 On → ∅ ∈ W
20 4 14 19 modelaxrep ⊢ W = ⋃ R1 On → ∀ x ∈ W ∀ w ∈ W ∃ y ∈ W ∀ z ∈ W ∀ y φ → z = y → ∃ y ∈ W ∀ z ∈ W z ∈ y ↔ ∃ w ∈ W w ∈ x ∧ ∀ y φ
21 1 20 ax-mp ⊢ ∀ x ∈ W ∀ w ∈ W ∃ y ∈ W ∀ z ∈ W ∀ y φ → z = y → ∃ y ∈ W ∀ z ∈ W z ∈ y ↔ ∃ w ∈ W w ∈ x ∧ ∀ y φ