Description: Conditions which guarantee that a class models the Axiom of Replacement ax-rep . Similar to Lemma II.2.4(6) of Kunen2 p. 111. The first two hypotheses are those in Kunen. The reason for the third hypothesis that our version of Replacement is different from Kunen's (which is zfrep6 ). If we assumed Regularity, we could eliminate this extra hypothesis, since under Regularity, the empty set is a member of every non-empty transitive class.
Note that, to obtain the relativization of an instance of Replacement to M , the formula A. y ph would need to be replaced with A. y e. M ch , where ch is ph with all quantifiers relativized to M . However, we can obtain this by using y e. M /\ ch for ph in this theorem, so it does establish that all instances of Replacement hold in M . (Contributed by Eric Schmidt, 29-Sep-2025)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | modelaxrep.1 | ⊢ ( 𝜓 → Tr 𝑀 ) | |
| modelaxrep.2 | ⊢ ( 𝜓 → ∀ 𝑓 ( ( Fun 𝑓 ∧ dom 𝑓 ∈ 𝑀 ∧ ran 𝑓 ⊆ 𝑀 ) → ran 𝑓 ∈ 𝑀 ) ) | ||
| modelaxrep.3 | ⊢ ( 𝜓 → ∅ ∈ 𝑀 ) | ||
| Assertion | modelaxrep | ⊢ ( 𝜓 → ∀ 𝑥 ∈ 𝑀 ( ∀ 𝑤 ∈ 𝑀 ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ∀ 𝑦 𝜑 → 𝑧 = 𝑦 ) → ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 𝜑 ) ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | modelaxrep.1 | ⊢ ( 𝜓 → Tr 𝑀 ) | |
| 2 | modelaxrep.2 | ⊢ ( 𝜓 → ∀ 𝑓 ( ( Fun 𝑓 ∧ dom 𝑓 ∈ 𝑀 ∧ ran 𝑓 ⊆ 𝑀 ) → ran 𝑓 ∈ 𝑀 ) ) | |
| 3 | modelaxrep.3 | ⊢ ( 𝜓 → ∅ ∈ 𝑀 ) | |
| 4 | funeq | ⊢ ( 𝑓 = 𝑔 → ( Fun 𝑓 ↔ Fun 𝑔 ) ) | |
| 5 | dmeq | ⊢ ( 𝑓 = 𝑔 → dom 𝑓 = dom 𝑔 ) | |
| 6 | 5 | eleq1d | ⊢ ( 𝑓 = 𝑔 → ( dom 𝑓 ∈ 𝑀 ↔ dom 𝑔 ∈ 𝑀 ) ) |
| 7 | rneq | ⊢ ( 𝑓 = 𝑔 → ran 𝑓 = ran 𝑔 ) | |
| 8 | 7 | sseq1d | ⊢ ( 𝑓 = 𝑔 → ( ran 𝑓 ⊆ 𝑀 ↔ ran 𝑔 ⊆ 𝑀 ) ) |
| 9 | 4 6 8 | 3anbi123d | ⊢ ( 𝑓 = 𝑔 → ( ( Fun 𝑓 ∧ dom 𝑓 ∈ 𝑀 ∧ ran 𝑓 ⊆ 𝑀 ) ↔ ( Fun 𝑔 ∧ dom 𝑔 ∈ 𝑀 ∧ ran 𝑔 ⊆ 𝑀 ) ) ) |
| 10 | 7 | eleq1d | ⊢ ( 𝑓 = 𝑔 → ( ran 𝑓 ∈ 𝑀 ↔ ran 𝑔 ∈ 𝑀 ) ) |
| 11 | 9 10 | imbi12d | ⊢ ( 𝑓 = 𝑔 → ( ( ( Fun 𝑓 ∧ dom 𝑓 ∈ 𝑀 ∧ ran 𝑓 ⊆ 𝑀 ) → ran 𝑓 ∈ 𝑀 ) ↔ ( ( Fun 𝑔 ∧ dom 𝑔 ∈ 𝑀 ∧ ran 𝑔 ⊆ 𝑀 ) → ran 𝑔 ∈ 𝑀 ) ) ) |
| 12 | 11 | cbvalvw | ⊢ ( ∀ 𝑓 ( ( Fun 𝑓 ∧ dom 𝑓 ∈ 𝑀 ∧ ran 𝑓 ⊆ 𝑀 ) → ran 𝑓 ∈ 𝑀 ) ↔ ∀ 𝑔 ( ( Fun 𝑔 ∧ dom 𝑔 ∈ 𝑀 ∧ ran 𝑔 ⊆ 𝑀 ) → ran 𝑔 ∈ 𝑀 ) ) |
| 13 | 2 12 | sylib | ⊢ ( 𝜓 → ∀ 𝑔 ( ( Fun 𝑔 ∧ dom 𝑔 ∈ 𝑀 ∧ ran 𝑔 ⊆ 𝑀 ) → ran 𝑔 ∈ 𝑀 ) ) |
| 14 | trss | ⊢ ( Tr 𝑀 → ( 𝑥 ∈ 𝑀 → 𝑥 ⊆ 𝑀 ) ) | |
| 15 | 14 | imp | ⊢ ( ( Tr 𝑀 ∧ 𝑥 ∈ 𝑀 ) → 𝑥 ⊆ 𝑀 ) |
| 16 | 15 | ad5ant14 | ⊢ ( ( ( ( ( Tr 𝑀 ∧ ∀ 𝑔 ( ( Fun 𝑔 ∧ dom 𝑔 ∈ 𝑀 ∧ ran 𝑔 ⊆ 𝑀 ) → ran 𝑔 ∈ 𝑀 ) ) ∧ ∅ ∈ 𝑀 ) ∧ 𝑥 ∈ 𝑀 ) ∧ ∀ 𝑤 ∈ 𝑀 ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ∀ 𝑦 𝜑 → 𝑧 = 𝑦 ) ) → 𝑥 ⊆ 𝑀 ) |
| 17 | simp-4r | ⊢ ( ( ( ( ( Tr 𝑀 ∧ ∀ 𝑔 ( ( Fun 𝑔 ∧ dom 𝑔 ∈ 𝑀 ∧ ran 𝑔 ⊆ 𝑀 ) → ran 𝑔 ∈ 𝑀 ) ) ∧ ∅ ∈ 𝑀 ) ∧ 𝑥 ∈ 𝑀 ) ∧ ∀ 𝑤 ∈ 𝑀 ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ∀ 𝑦 𝜑 → 𝑧 = 𝑦 ) ) → ∀ 𝑔 ( ( Fun 𝑔 ∧ dom 𝑔 ∈ 𝑀 ∧ ran 𝑔 ⊆ 𝑀 ) → ran 𝑔 ∈ 𝑀 ) ) | |
| 18 | simpllr | ⊢ ( ( ( ( ( Tr 𝑀 ∧ ∀ 𝑔 ( ( Fun 𝑔 ∧ dom 𝑔 ∈ 𝑀 ∧ ran 𝑔 ⊆ 𝑀 ) → ran 𝑔 ∈ 𝑀 ) ) ∧ ∅ ∈ 𝑀 ) ∧ 𝑥 ∈ 𝑀 ) ∧ ∀ 𝑤 ∈ 𝑀 ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ∀ 𝑦 𝜑 → 𝑧 = 𝑦 ) ) → ∅ ∈ 𝑀 ) | |
| 19 | simplr | ⊢ ( ( ( ( ( Tr 𝑀 ∧ ∀ 𝑔 ( ( Fun 𝑔 ∧ dom 𝑔 ∈ 𝑀 ∧ ran 𝑔 ⊆ 𝑀 ) → ran 𝑔 ∈ 𝑀 ) ) ∧ ∅ ∈ 𝑀 ) ∧ 𝑥 ∈ 𝑀 ) ∧ ∀ 𝑤 ∈ 𝑀 ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ∀ 𝑦 𝜑 → 𝑧 = 𝑦 ) ) → 𝑥 ∈ 𝑀 ) | |
| 20 | nfv | ⊢ Ⅎ 𝑤 ( ( ( Tr 𝑀 ∧ ∀ 𝑔 ( ( Fun 𝑔 ∧ dom 𝑔 ∈ 𝑀 ∧ ran 𝑔 ⊆ 𝑀 ) → ran 𝑔 ∈ 𝑀 ) ) ∧ ∅ ∈ 𝑀 ) ∧ 𝑥 ∈ 𝑀 ) | |
| 21 | nfra1 | ⊢ Ⅎ 𝑤 ∀ 𝑤 ∈ 𝑀 ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ∀ 𝑦 𝜑 → 𝑧 = 𝑦 ) | |
| 22 | 20 21 | nfan | ⊢ Ⅎ 𝑤 ( ( ( ( Tr 𝑀 ∧ ∀ 𝑔 ( ( Fun 𝑔 ∧ dom 𝑔 ∈ 𝑀 ∧ ran 𝑔 ⊆ 𝑀 ) → ran 𝑔 ∈ 𝑀 ) ) ∧ ∅ ∈ 𝑀 ) ∧ 𝑥 ∈ 𝑀 ) ∧ ∀ 𝑤 ∈ 𝑀 ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ∀ 𝑦 𝜑 → 𝑧 = 𝑦 ) ) |
| 23 | nfv | ⊢ Ⅎ 𝑧 ( ( ( Tr 𝑀 ∧ ∀ 𝑔 ( ( Fun 𝑔 ∧ dom 𝑔 ∈ 𝑀 ∧ ran 𝑔 ⊆ 𝑀 ) → ran 𝑔 ∈ 𝑀 ) ) ∧ ∅ ∈ 𝑀 ) ∧ 𝑥 ∈ 𝑀 ) | |
| 24 | nfcv | ⊢ Ⅎ 𝑧 𝑀 | |
| 25 | nfra1 | ⊢ Ⅎ 𝑧 ∀ 𝑧 ∈ 𝑀 ( ∀ 𝑦 𝜑 → 𝑧 = 𝑦 ) | |
| 26 | 24 25 | nfrexw | ⊢ Ⅎ 𝑧 ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ∀ 𝑦 𝜑 → 𝑧 = 𝑦 ) |
| 27 | 24 26 | nfralw | ⊢ Ⅎ 𝑧 ∀ 𝑤 ∈ 𝑀 ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ∀ 𝑦 𝜑 → 𝑧 = 𝑦 ) |
| 28 | 23 27 | nfan | ⊢ Ⅎ 𝑧 ( ( ( ( Tr 𝑀 ∧ ∀ 𝑔 ( ( Fun 𝑔 ∧ dom 𝑔 ∈ 𝑀 ∧ ran 𝑔 ⊆ 𝑀 ) → ran 𝑔 ∈ 𝑀 ) ) ∧ ∅ ∈ 𝑀 ) ∧ 𝑥 ∈ 𝑀 ) ∧ ∀ 𝑤 ∈ 𝑀 ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ∀ 𝑦 𝜑 → 𝑧 = 𝑦 ) ) |
| 29 | nfopab2 | ⊢ Ⅎ 𝑧 { ⟨ 𝑤 , 𝑧 ⟩ ∣ ( 𝑤 ∈ 𝑥 ∧ ( 𝑧 ∈ 𝑀 ∧ ∀ 𝑦 𝜑 ) ) } | |
| 30 | eqid | ⊢ { ⟨ 𝑤 , 𝑧 ⟩ ∣ ( 𝑤 ∈ 𝑥 ∧ ( 𝑧 ∈ 𝑀 ∧ ∀ 𝑦 𝜑 ) ) } = { ⟨ 𝑤 , 𝑧 ⟩ ∣ ( 𝑤 ∈ 𝑥 ∧ ( 𝑧 ∈ 𝑀 ∧ ∀ 𝑦 𝜑 ) ) } | |
| 31 | rsp | ⊢ ( ∀ 𝑤 ∈ 𝑀 ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ∀ 𝑦 𝜑 → 𝑧 = 𝑦 ) → ( 𝑤 ∈ 𝑀 → ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ∀ 𝑦 𝜑 → 𝑧 = 𝑦 ) ) ) | |
| 32 | 31 | adantl | ⊢ ( ( ( ( ( Tr 𝑀 ∧ ∀ 𝑔 ( ( Fun 𝑔 ∧ dom 𝑔 ∈ 𝑀 ∧ ran 𝑔 ⊆ 𝑀 ) → ran 𝑔 ∈ 𝑀 ) ) ∧ ∅ ∈ 𝑀 ) ∧ 𝑥 ∈ 𝑀 ) ∧ ∀ 𝑤 ∈ 𝑀 ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ∀ 𝑦 𝜑 → 𝑧 = 𝑦 ) ) → ( 𝑤 ∈ 𝑀 → ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ∀ 𝑦 𝜑 → 𝑧 = 𝑦 ) ) ) |
| 33 | 16 17 18 19 22 28 29 30 32 | modelaxreplem3 | ⊢ ( ( ( ( ( Tr 𝑀 ∧ ∀ 𝑔 ( ( Fun 𝑔 ∧ dom 𝑔 ∈ 𝑀 ∧ ran 𝑔 ⊆ 𝑀 ) → ran 𝑔 ∈ 𝑀 ) ) ∧ ∅ ∈ 𝑀 ) ∧ 𝑥 ∈ 𝑀 ) ∧ ∀ 𝑤 ∈ 𝑀 ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ∀ 𝑦 𝜑 → 𝑧 = 𝑦 ) ) → ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 𝜑 ) ) ) |
| 34 | 33 | ex | ⊢ ( ( ( ( Tr 𝑀 ∧ ∀ 𝑔 ( ( Fun 𝑔 ∧ dom 𝑔 ∈ 𝑀 ∧ ran 𝑔 ⊆ 𝑀 ) → ran 𝑔 ∈ 𝑀 ) ) ∧ ∅ ∈ 𝑀 ) ∧ 𝑥 ∈ 𝑀 ) → ( ∀ 𝑤 ∈ 𝑀 ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ∀ 𝑦 𝜑 → 𝑧 = 𝑦 ) → ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 𝜑 ) ) ) ) |
| 35 | 34 | ralrimiva | ⊢ ( ( ( Tr 𝑀 ∧ ∀ 𝑔 ( ( Fun 𝑔 ∧ dom 𝑔 ∈ 𝑀 ∧ ran 𝑔 ⊆ 𝑀 ) → ran 𝑔 ∈ 𝑀 ) ) ∧ ∅ ∈ 𝑀 ) → ∀ 𝑥 ∈ 𝑀 ( ∀ 𝑤 ∈ 𝑀 ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ∀ 𝑦 𝜑 → 𝑧 = 𝑦 ) → ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 𝜑 ) ) ) ) |
| 36 | 1 13 3 35 | syl21anc | ⊢ ( 𝜓 → ∀ 𝑥 ∈ 𝑀 ( ∀ 𝑤 ∈ 𝑀 ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ∀ 𝑦 𝜑 → 𝑧 = 𝑦 ) → ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 𝜑 ) ) ) ) |