Metamath Proof Explorer

Theorem permaxpow

Description: The Axiom of Power Sets ax-pow holds in permutation models. Part of Exercise II.9.2 of Kunen2 p. 148. (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 permaxpow ⊢ ∃ y ∀ z ∀ w w R z → w R x → z R y

Proof

Step Hyp Ref Expression
1 permmodel.1 ⊢ F : V ⟶ 1-1 onto V
2 permmodel.2 ⊢ R = F -1 ∘ E
3 fvex ⊢ F -1 ⁡ F -1 𝒫 F ⁡ x ∈ V
4 breq2 ⊢ y = F -1 ⁡ F -1 𝒫 F ⁡ x → z R y ↔ z R F -1 ⁡ F -1 𝒫 F ⁡ x
5 4 imbi2d ⊢ y = F -1 ⁡ F -1 𝒫 F ⁡ x → ∀ w w R z → w R x → z R y ↔ ∀ w w R z → w R x → z R F -1 ⁡ F -1 𝒫 F ⁡ x
6 5 albidv ⊢ y = F -1 ⁡ F -1 𝒫 F ⁡ x → ∀ z ∀ w w R z → w R x → z R y ↔ ∀ z ∀ w w R z → w R x → z R F -1 ⁡ F -1 𝒫 F ⁡ x
7 vex ⊢ z ∈ V
8 dff1o3 ⊢ F : V ⟶ 1-1 onto V ↔ F : V ⟶ onto V ∧ Fun ⁡ F -1
9 1 8 mpbi ⊢ F : V ⟶ onto V ∧ Fun ⁡ F -1
10 9 simpri ⊢ Fun ⁡ F -1
11 fvex ⊢ F ⁡ x ∈ V
12 11 pwex ⊢ 𝒫 F ⁡ x ∈ V
13 12 funimaex ⊢ Fun ⁡ F -1 → F -1 𝒫 F ⁡ x ∈ V
14 10 13 ax-mp ⊢ F -1 𝒫 F ⁡ x ∈ V
15 1 2 7 14 brpermmodelcnv ⊢ z R F -1 ⁡ F -1 𝒫 F ⁡ x ↔ z ∈ F -1 𝒫 F ⁡ x
16 f1ofn ⊢ F : V ⟶ 1-1 onto V → F Fn V
17 1 16 ax-mp ⊢ F Fn V
18 elpreima ⊢ F Fn V → z ∈ F -1 𝒫 F ⁡ x ↔ z ∈ V ∧ F ⁡ z ∈ 𝒫 F ⁡ x
19 17 18 ax-mp ⊢ z ∈ F -1 𝒫 F ⁡ x ↔ z ∈ V ∧ F ⁡ z ∈ 𝒫 F ⁡ x
20 7 19 mpbiran ⊢ z ∈ F -1 𝒫 F ⁡ x ↔ F ⁡ z ∈ 𝒫 F ⁡ x
21 15 20 bitri ⊢ z R F -1 ⁡ F -1 𝒫 F ⁡ x ↔ F ⁡ z ∈ 𝒫 F ⁡ x
22 df-ss ⊢ F ⁡ z ⊆ F ⁡ x ↔ ∀ w w ∈ F ⁡ z → w ∈ F ⁡ x
23 fvex ⊢ F ⁡ z ∈ V
24 23 elpw ⊢ F ⁡ z ∈ 𝒫 F ⁡ x ↔ F ⁡ z ⊆ F ⁡ x
25 vex ⊢ w ∈ V
26 1 2 25 7 brpermmodel ⊢ w R z ↔ w ∈ F ⁡ z
27 vex ⊢ x ∈ V
28 1 2 25 27 brpermmodel ⊢ w R x ↔ w ∈ F ⁡ x
29 26 28 imbi12i ⊢ w R z → w R x ↔ w ∈ F ⁡ z → w ∈ F ⁡ x
30 29 albii ⊢ ∀ w w R z → w R x ↔ ∀ w w ∈ F ⁡ z → w ∈ F ⁡ x
31 22 24 30 3bitr4i ⊢ F ⁡ z ∈ 𝒫 F ⁡ x ↔ ∀ w w R z → w R x
32 21 31 sylbbr ⊢ ∀ w w R z → w R x → z R F -1 ⁡ F -1 𝒫 F ⁡ x
33 32 ax-gen ⊢ ∀ z ∀ w w R z → w R x → z R F -1 ⁡ F -1 𝒫 F ⁡ x
34 3 6 33 ceqsexv2d ⊢ ∃ y ∀ z ∀ w w R z → w R x → z R y