Description: The Axiom of Replacement ax-rep holds in permutation models. Part of Exercise II.9.2 of Kunen2 p. 148.
Note that, to prove that an instance of Replacement holds in the model, ph would need have all instances of e. replaced with R . But this still results in an instance of this theorem, so we do establish that Replacement holds. (Contributed by Eric Schmidt, 6-Nov-2025)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | permmodel.1 | ⊢ 𝐹 : V –1-1-onto→ V | |
| permmodel.2 | ⊢ 𝑅 = ( ◡ 𝐹 ∘ E ) | ||
| Assertion | permaxrep | ⊢ ( ∀ 𝑤 ∃ 𝑦 ∀ 𝑧 ( ∀ 𝑦 𝜑 → 𝑧 = 𝑦 ) → ∃ 𝑦 ∀ 𝑧 ( 𝑧 𝑅 𝑦 ↔ ∃ 𝑤 ( 𝑤 𝑅 𝑥 ∧ ∀ 𝑦 𝜑 ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | permmodel.1 | ⊢ 𝐹 : V –1-1-onto→ V | |
| 2 | permmodel.2 | ⊢ 𝑅 = ( ◡ 𝐹 ∘ E ) | |
| 3 | nfa1 | ⊢ Ⅎ 𝑦 ∀ 𝑦 𝜑 | |
| 4 | 3 | mof | ⊢ ( ∃* 𝑧 ∀ 𝑦 𝜑 ↔ ∃ 𝑦 ∀ 𝑧 ( ∀ 𝑦 𝜑 → 𝑧 = 𝑦 ) ) |
| 5 | 4 | albii | ⊢ ( ∀ 𝑤 ∃* 𝑧 ∀ 𝑦 𝜑 ↔ ∀ 𝑤 ∃ 𝑦 ∀ 𝑧 ( ∀ 𝑦 𝜑 → 𝑧 = 𝑦 ) ) |
| 6 | fvex | ⊢ ( ◡ 𝐹 ‘ { 𝑧 ∣ ∃ 𝑤 ∈ ( 𝐹 ‘ 𝑥 ) ∀ 𝑦 𝜑 } ) ∈ V | |
| 7 | nfmo1 | ⊢ Ⅎ 𝑧 ∃* 𝑧 ∀ 𝑦 𝜑 | |
| 8 | 7 | nfal | ⊢ Ⅎ 𝑧 ∀ 𝑤 ∃* 𝑧 ∀ 𝑦 𝜑 |
| 9 | vex | ⊢ 𝑧 ∈ V | |
| 10 | 1 2 9 6 | brpermmodel | ⊢ ( 𝑧 𝑅 ( ◡ 𝐹 ‘ { 𝑧 ∣ ∃ 𝑤 ∈ ( 𝐹 ‘ 𝑥 ) ∀ 𝑦 𝜑 } ) ↔ 𝑧 ∈ ( 𝐹 ‘ ( ◡ 𝐹 ‘ { 𝑧 ∣ ∃ 𝑤 ∈ ( 𝐹 ‘ 𝑥 ) ∀ 𝑦 𝜑 } ) ) ) |
| 11 | fvex | ⊢ ( 𝐹 ‘ 𝑥 ) ∈ V | |
| 12 | axrep6g | ⊢ ( ( ( 𝐹 ‘ 𝑥 ) ∈ V ∧ ∀ 𝑤 ∃* 𝑧 ∀ 𝑦 𝜑 ) → { 𝑧 ∣ ∃ 𝑤 ∈ ( 𝐹 ‘ 𝑥 ) ∀ 𝑦 𝜑 } ∈ V ) | |
| 13 | 11 12 | mpan | ⊢ ( ∀ 𝑤 ∃* 𝑧 ∀ 𝑦 𝜑 → { 𝑧 ∣ ∃ 𝑤 ∈ ( 𝐹 ‘ 𝑥 ) ∀ 𝑦 𝜑 } ∈ V ) |
| 14 | f1ocnvfv2 | ⊢ ( ( 𝐹 : V –1-1-onto→ V ∧ { 𝑧 ∣ ∃ 𝑤 ∈ ( 𝐹 ‘ 𝑥 ) ∀ 𝑦 𝜑 } ∈ V ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ { 𝑧 ∣ ∃ 𝑤 ∈ ( 𝐹 ‘ 𝑥 ) ∀ 𝑦 𝜑 } ) ) = { 𝑧 ∣ ∃ 𝑤 ∈ ( 𝐹 ‘ 𝑥 ) ∀ 𝑦 𝜑 } ) | |
| 15 | 1 13 14 | sylancr | ⊢ ( ∀ 𝑤 ∃* 𝑧 ∀ 𝑦 𝜑 → ( 𝐹 ‘ ( ◡ 𝐹 ‘ { 𝑧 ∣ ∃ 𝑤 ∈ ( 𝐹 ‘ 𝑥 ) ∀ 𝑦 𝜑 } ) ) = { 𝑧 ∣ ∃ 𝑤 ∈ ( 𝐹 ‘ 𝑥 ) ∀ 𝑦 𝜑 } ) |
| 16 | 15 | eleq2d | ⊢ ( ∀ 𝑤 ∃* 𝑧 ∀ 𝑦 𝜑 → ( 𝑧 ∈ ( 𝐹 ‘ ( ◡ 𝐹 ‘ { 𝑧 ∣ ∃ 𝑤 ∈ ( 𝐹 ‘ 𝑥 ) ∀ 𝑦 𝜑 } ) ) ↔ 𝑧 ∈ { 𝑧 ∣ ∃ 𝑤 ∈ ( 𝐹 ‘ 𝑥 ) ∀ 𝑦 𝜑 } ) ) |
| 17 | 10 16 | bitrid | ⊢ ( ∀ 𝑤 ∃* 𝑧 ∀ 𝑦 𝜑 → ( 𝑧 𝑅 ( ◡ 𝐹 ‘ { 𝑧 ∣ ∃ 𝑤 ∈ ( 𝐹 ‘ 𝑥 ) ∀ 𝑦 𝜑 } ) ↔ 𝑧 ∈ { 𝑧 ∣ ∃ 𝑤 ∈ ( 𝐹 ‘ 𝑥 ) ∀ 𝑦 𝜑 } ) ) |
| 18 | df-rex | ⊢ ( ∃ 𝑤 ∈ ( 𝐹 ‘ 𝑥 ) ∀ 𝑦 𝜑 ↔ ∃ 𝑤 ( 𝑤 ∈ ( 𝐹 ‘ 𝑥 ) ∧ ∀ 𝑦 𝜑 ) ) | |
| 19 | abid | ⊢ ( 𝑧 ∈ { 𝑧 ∣ ∃ 𝑤 ∈ ( 𝐹 ‘ 𝑥 ) ∀ 𝑦 𝜑 } ↔ ∃ 𝑤 ∈ ( 𝐹 ‘ 𝑥 ) ∀ 𝑦 𝜑 ) | |
| 20 | vex | ⊢ 𝑤 ∈ V | |
| 21 | vex | ⊢ 𝑥 ∈ V | |
| 22 | 1 2 20 21 | brpermmodel | ⊢ ( 𝑤 𝑅 𝑥 ↔ 𝑤 ∈ ( 𝐹 ‘ 𝑥 ) ) |
| 23 | 22 | anbi1i | ⊢ ( ( 𝑤 𝑅 𝑥 ∧ ∀ 𝑦 𝜑 ) ↔ ( 𝑤 ∈ ( 𝐹 ‘ 𝑥 ) ∧ ∀ 𝑦 𝜑 ) ) |
| 24 | 23 | exbii | ⊢ ( ∃ 𝑤 ( 𝑤 𝑅 𝑥 ∧ ∀ 𝑦 𝜑 ) ↔ ∃ 𝑤 ( 𝑤 ∈ ( 𝐹 ‘ 𝑥 ) ∧ ∀ 𝑦 𝜑 ) ) |
| 25 | 18 19 24 | 3bitr4i | ⊢ ( 𝑧 ∈ { 𝑧 ∣ ∃ 𝑤 ∈ ( 𝐹 ‘ 𝑥 ) ∀ 𝑦 𝜑 } ↔ ∃ 𝑤 ( 𝑤 𝑅 𝑥 ∧ ∀ 𝑦 𝜑 ) ) |
| 26 | 17 25 | bitrdi | ⊢ ( ∀ 𝑤 ∃* 𝑧 ∀ 𝑦 𝜑 → ( 𝑧 𝑅 ( ◡ 𝐹 ‘ { 𝑧 ∣ ∃ 𝑤 ∈ ( 𝐹 ‘ 𝑥 ) ∀ 𝑦 𝜑 } ) ↔ ∃ 𝑤 ( 𝑤 𝑅 𝑥 ∧ ∀ 𝑦 𝜑 ) ) ) |
| 27 | 8 26 | alrimi | ⊢ ( ∀ 𝑤 ∃* 𝑧 ∀ 𝑦 𝜑 → ∀ 𝑧 ( 𝑧 𝑅 ( ◡ 𝐹 ‘ { 𝑧 ∣ ∃ 𝑤 ∈ ( 𝐹 ‘ 𝑥 ) ∀ 𝑦 𝜑 } ) ↔ ∃ 𝑤 ( 𝑤 𝑅 𝑥 ∧ ∀ 𝑦 𝜑 ) ) ) |
| 28 | nfcv | ⊢ Ⅎ 𝑦 ◡ 𝐹 | |
| 29 | nfcv | ⊢ Ⅎ 𝑦 ( 𝐹 ‘ 𝑥 ) | |
| 30 | 29 3 | nfrexw | ⊢ Ⅎ 𝑦 ∃ 𝑤 ∈ ( 𝐹 ‘ 𝑥 ) ∀ 𝑦 𝜑 |
| 31 | 30 | nfab | ⊢ Ⅎ 𝑦 { 𝑧 ∣ ∃ 𝑤 ∈ ( 𝐹 ‘ 𝑥 ) ∀ 𝑦 𝜑 } |
| 32 | 28 31 | nffv | ⊢ Ⅎ 𝑦 ( ◡ 𝐹 ‘ { 𝑧 ∣ ∃ 𝑤 ∈ ( 𝐹 ‘ 𝑥 ) ∀ 𝑦 𝜑 } ) |
| 33 | nfcv | ⊢ Ⅎ 𝑦 𝑧 | |
| 34 | nfcv | ⊢ Ⅎ 𝑦 𝑅 | |
| 35 | 33 34 32 | nfbr | ⊢ Ⅎ 𝑦 𝑧 𝑅 ( ◡ 𝐹 ‘ { 𝑧 ∣ ∃ 𝑤 ∈ ( 𝐹 ‘ 𝑥 ) ∀ 𝑦 𝜑 } ) |
| 36 | nfv | ⊢ Ⅎ 𝑦 𝑤 𝑅 𝑥 | |
| 37 | 36 3 | nfan | ⊢ Ⅎ 𝑦 ( 𝑤 𝑅 𝑥 ∧ ∀ 𝑦 𝜑 ) |
| 38 | 37 | nfex | ⊢ Ⅎ 𝑦 ∃ 𝑤 ( 𝑤 𝑅 𝑥 ∧ ∀ 𝑦 𝜑 ) |
| 39 | 35 38 | nfbi | ⊢ Ⅎ 𝑦 ( 𝑧 𝑅 ( ◡ 𝐹 ‘ { 𝑧 ∣ ∃ 𝑤 ∈ ( 𝐹 ‘ 𝑥 ) ∀ 𝑦 𝜑 } ) ↔ ∃ 𝑤 ( 𝑤 𝑅 𝑥 ∧ ∀ 𝑦 𝜑 ) ) |
| 40 | 39 | nfal | ⊢ Ⅎ 𝑦 ∀ 𝑧 ( 𝑧 𝑅 ( ◡ 𝐹 ‘ { 𝑧 ∣ ∃ 𝑤 ∈ ( 𝐹 ‘ 𝑥 ) ∀ 𝑦 𝜑 } ) ↔ ∃ 𝑤 ( 𝑤 𝑅 𝑥 ∧ ∀ 𝑦 𝜑 ) ) |
| 41 | nfcv | ⊢ Ⅎ 𝑧 ◡ 𝐹 | |
| 42 | nfab1 | ⊢ Ⅎ 𝑧 { 𝑧 ∣ ∃ 𝑤 ∈ ( 𝐹 ‘ 𝑥 ) ∀ 𝑦 𝜑 } | |
| 43 | 41 42 | nffv | ⊢ Ⅎ 𝑧 ( ◡ 𝐹 ‘ { 𝑧 ∣ ∃ 𝑤 ∈ ( 𝐹 ‘ 𝑥 ) ∀ 𝑦 𝜑 } ) |
| 44 | 43 | nfeq2 | ⊢ Ⅎ 𝑧 𝑦 = ( ◡ 𝐹 ‘ { 𝑧 ∣ ∃ 𝑤 ∈ ( 𝐹 ‘ 𝑥 ) ∀ 𝑦 𝜑 } ) |
| 45 | breq2 | ⊢ ( 𝑦 = ( ◡ 𝐹 ‘ { 𝑧 ∣ ∃ 𝑤 ∈ ( 𝐹 ‘ 𝑥 ) ∀ 𝑦 𝜑 } ) → ( 𝑧 𝑅 𝑦 ↔ 𝑧 𝑅 ( ◡ 𝐹 ‘ { 𝑧 ∣ ∃ 𝑤 ∈ ( 𝐹 ‘ 𝑥 ) ∀ 𝑦 𝜑 } ) ) ) | |
| 46 | 45 | bibi1d | ⊢ ( 𝑦 = ( ◡ 𝐹 ‘ { 𝑧 ∣ ∃ 𝑤 ∈ ( 𝐹 ‘ 𝑥 ) ∀ 𝑦 𝜑 } ) → ( ( 𝑧 𝑅 𝑦 ↔ ∃ 𝑤 ( 𝑤 𝑅 𝑥 ∧ ∀ 𝑦 𝜑 ) ) ↔ ( 𝑧 𝑅 ( ◡ 𝐹 ‘ { 𝑧 ∣ ∃ 𝑤 ∈ ( 𝐹 ‘ 𝑥 ) ∀ 𝑦 𝜑 } ) ↔ ∃ 𝑤 ( 𝑤 𝑅 𝑥 ∧ ∀ 𝑦 𝜑 ) ) ) ) |
| 47 | 44 46 | albid | ⊢ ( 𝑦 = ( ◡ 𝐹 ‘ { 𝑧 ∣ ∃ 𝑤 ∈ ( 𝐹 ‘ 𝑥 ) ∀ 𝑦 𝜑 } ) → ( ∀ 𝑧 ( 𝑧 𝑅 𝑦 ↔ ∃ 𝑤 ( 𝑤 𝑅 𝑥 ∧ ∀ 𝑦 𝜑 ) ) ↔ ∀ 𝑧 ( 𝑧 𝑅 ( ◡ 𝐹 ‘ { 𝑧 ∣ ∃ 𝑤 ∈ ( 𝐹 ‘ 𝑥 ) ∀ 𝑦 𝜑 } ) ↔ ∃ 𝑤 ( 𝑤 𝑅 𝑥 ∧ ∀ 𝑦 𝜑 ) ) ) ) |
| 48 | 32 40 47 | spcegf | ⊢ ( ( ◡ 𝐹 ‘ { 𝑧 ∣ ∃ 𝑤 ∈ ( 𝐹 ‘ 𝑥 ) ∀ 𝑦 𝜑 } ) ∈ V → ( ∀ 𝑧 ( 𝑧 𝑅 ( ◡ 𝐹 ‘ { 𝑧 ∣ ∃ 𝑤 ∈ ( 𝐹 ‘ 𝑥 ) ∀ 𝑦 𝜑 } ) ↔ ∃ 𝑤 ( 𝑤 𝑅 𝑥 ∧ ∀ 𝑦 𝜑 ) ) → ∃ 𝑦 ∀ 𝑧 ( 𝑧 𝑅 𝑦 ↔ ∃ 𝑤 ( 𝑤 𝑅 𝑥 ∧ ∀ 𝑦 𝜑 ) ) ) ) |
| 49 | 6 27 48 | mpsyl | ⊢ ( ∀ 𝑤 ∃* 𝑧 ∀ 𝑦 𝜑 → ∃ 𝑦 ∀ 𝑧 ( 𝑧 𝑅 𝑦 ↔ ∃ 𝑤 ( 𝑤 𝑅 𝑥 ∧ ∀ 𝑦 𝜑 ) ) ) |
| 50 | 5 49 | sylbir | ⊢ ( ∀ 𝑤 ∃ 𝑦 ∀ 𝑧 ( ∀ 𝑦 𝜑 → 𝑧 = 𝑦 ) → ∃ 𝑦 ∀ 𝑧 ( 𝑧 𝑅 𝑦 ↔ ∃ 𝑤 ( 𝑤 𝑅 𝑥 ∧ ∀ 𝑦 𝜑 ) ) ) |