Metamath Proof Explorer

Theorem permaxrep

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 ⊢ F : V ⟶ 1-1 onto V
permmodel.2 ⊢ R = F -1 ∘ E
Assertion permaxrep ⊢ ∀ w ∃ y ∀ z ∀ y φ → z = y → ∃ y ∀ z z R y ↔ ∃ w w R x ∧ ∀ y φ

Proof

Step Hyp Ref Expression
1 permmodel.1 ⊢ F : V ⟶ 1-1 onto V
2 permmodel.2 ⊢ R = F -1 ∘ E
3 nfa1 ⊢ Ⅎ y ∀ y φ
4 3 mof ⊢ ∃* z ∀ y φ ↔ ∃ y ∀ z ∀ y φ → z = y
5 4 albii ⊢ ∀ w ∃* z ∀ y φ ↔ ∀ w ∃ y ∀ z ∀ y φ → z = y
6 fvex ⊢ F -1 ⁡ z | ∃ w ∈ F ⁡ x ∀ y φ ∈ V
7 nfmo1 ⊢ Ⅎ z ∃* z ∀ y φ
8 7 nfal ⊢ Ⅎ z ∀ w ∃* z ∀ y φ
9 vex ⊢ z ∈ V
10 1 2 9 6 brpermmodel ⊢ z R F -1 ⁡ z | ∃ w ∈ F ⁡ x ∀ y φ ↔ z ∈ F ⁡ F -1 ⁡ z | ∃ w ∈ F ⁡ x ∀ y φ
11 fvex ⊢ F ⁡ x ∈ V
12 axrep6g ⊢ F ⁡ x ∈ V ∧ ∀ w ∃* z ∀ y φ → z | ∃ w ∈ F ⁡ x ∀ y φ ∈ V
13 11 12 mpan ⊢ ∀ w ∃* z ∀ y φ → z | ∃ w ∈ F ⁡ x ∀ y φ ∈ V
14 f1ocnvfv2 ⊢ F : V ⟶ 1-1 onto V ∧ z | ∃ w ∈ F ⁡ x ∀ y φ ∈ V → F ⁡ F -1 ⁡ z | ∃ w ∈ F ⁡ x ∀ y φ = z | ∃ w ∈ F ⁡ x ∀ y φ
15 1 13 14 sylancr ⊢ ∀ w ∃* z ∀ y φ → F ⁡ F -1 ⁡ z | ∃ w ∈ F ⁡ x ∀ y φ = z | ∃ w ∈ F ⁡ x ∀ y φ
16 15 eleq2d ⊢ ∀ w ∃* z ∀ y φ → z ∈ F ⁡ F -1 ⁡ z | ∃ w ∈ F ⁡ x ∀ y φ ↔ z ∈ z | ∃ w ∈ F ⁡ x ∀ y φ
17 10 16 bitrid ⊢ ∀ w ∃* z ∀ y φ → z R F -1 ⁡ z | ∃ w ∈ F ⁡ x ∀ y φ ↔ z ∈ z | ∃ w ∈ F ⁡ x ∀ y φ
18 df-rex ⊢ ∃ w ∈ F ⁡ x ∀ y φ ↔ ∃ w w ∈ F ⁡ x ∧ ∀ y φ
19 abid ⊢ z ∈ z | ∃ w ∈ F ⁡ x ∀ y φ ↔ ∃ w ∈ F ⁡ x ∀ y φ
20 vex ⊢ w ∈ V
21 vex ⊢ x ∈ V
22 1 2 20 21 brpermmodel ⊢ w R x ↔ w ∈ F ⁡ x
23 22 anbi1i ⊢ w R x ∧ ∀ y φ ↔ w ∈ F ⁡ x ∧ ∀ y φ
24 23 exbii ⊢ ∃ w w R x ∧ ∀ y φ ↔ ∃ w w ∈ F ⁡ x ∧ ∀ y φ
25 18 19 24 3bitr4i ⊢ z ∈ z | ∃ w ∈ F ⁡ x ∀ y φ ↔ ∃ w w R x ∧ ∀ y φ
26 17 25 bitrdi ⊢ ∀ w ∃* z ∀ y φ → z R F -1 ⁡ z | ∃ w ∈ F ⁡ x ∀ y φ ↔ ∃ w w R x ∧ ∀ y φ
27 8 26 alrimi ⊢ ∀ w ∃* z ∀ y φ → ∀ z z R F -1 ⁡ z | ∃ w ∈ F ⁡ x ∀ y φ ↔ ∃ w w R x ∧ ∀ y φ
28 nfcv ⊢ Ⅎ _ y F -1
29 nfcv ⊢ Ⅎ _ y F ⁡ x
30 29 3 nfrexw ⊢ Ⅎ y ∃ w ∈ F ⁡ x ∀ y φ
31 30 nfab ⊢ Ⅎ _ y z | ∃ w ∈ F ⁡ x ∀ y φ
32 28 31 nffv ⊢ Ⅎ _ y F -1 ⁡ z | ∃ w ∈ F ⁡ x ∀ y φ
33 nfcv ⊢ Ⅎ _ y z
34 nfcv ⊢ Ⅎ _ y R
35 33 34 32 nfbr ⊢ Ⅎ y z R F -1 ⁡ z | ∃ w ∈ F ⁡ x ∀ y φ
36 nfv ⊢ Ⅎ y w R x
37 36 3 nfan ⊢ Ⅎ y w R x ∧ ∀ y φ
38 37 nfex ⊢ Ⅎ y ∃ w w R x ∧ ∀ y φ
39 35 38 nfbi ⊢ Ⅎ y z R F -1 ⁡ z | ∃ w ∈ F ⁡ x ∀ y φ ↔ ∃ w w R x ∧ ∀ y φ
40 39 nfal ⊢ Ⅎ y ∀ z z R F -1 ⁡ z | ∃ w ∈ F ⁡ x ∀ y φ ↔ ∃ w w R x ∧ ∀ y φ
41 nfcv ⊢ Ⅎ _ z F -1
42 nfab1 ⊢ Ⅎ _ z z | ∃ w ∈ F ⁡ x ∀ y φ
43 41 42 nffv ⊢ Ⅎ _ z F -1 ⁡ z | ∃ w ∈ F ⁡ x ∀ y φ
44 43 nfeq2 ⊢ Ⅎ z y = F -1 ⁡ z | ∃ w ∈ F ⁡ x ∀ y φ
45 breq2 ⊢ y = F -1 ⁡ z | ∃ w ∈ F ⁡ x ∀ y φ → z R y ↔ z R F -1 ⁡ z | ∃ w ∈ F ⁡ x ∀ y φ
46 45 bibi1d ⊢ y = F -1 ⁡ z | ∃ w ∈ F ⁡ x ∀ y φ → z R y ↔ ∃ w w R x ∧ ∀ y φ ↔ z R F -1 ⁡ z | ∃ w ∈ F ⁡ x ∀ y φ ↔ ∃ w w R x ∧ ∀ y φ
47 44 46 albid ⊢ y = F -1 ⁡ z | ∃ w ∈ F ⁡ x ∀ y φ → ∀ z z R y ↔ ∃ w w R x ∧ ∀ y φ ↔ ∀ z z R F -1 ⁡ z | ∃ w ∈ F ⁡ x ∀ y φ ↔ ∃ w w R x ∧ ∀ y φ
48 32 40 47 spcegf ⊢ F -1 ⁡ z | ∃ w ∈ F ⁡ x ∀ y φ ∈ V → ∀ z z R F -1 ⁡ z | ∃ w ∈ F ⁡ x ∀ y φ ↔ ∃ w w R x ∧ ∀ y φ → ∃ y ∀ z z R y ↔ ∃ w w R x ∧ ∀ y φ
49 6 27 48 mpsyl ⊢ ∀ w ∃* z ∀ y φ → ∃ y ∀ z z R y ↔ ∃ w w R x ∧ ∀ y φ
50 5 49 sylbir ⊢ ∀ w ∃ y ∀ z ∀ y φ → z = y → ∃ y ∀ z z R y ↔ ∃ w w R x ∧ ∀ y φ