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	⊢ 𝐹 : V –1-1-onto→ V
	permmodel.2	⊢ 𝑅 = ( ◡ 𝐹 ∘ E )
Assertion	permaxpow	⊢ ∃ 𝑦 ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 𝑅 𝑧 → 𝑤 𝑅 𝑥 ) → 𝑧 𝑅 𝑦 )

Proof

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