Theorem permaxsep

Description: The Axiom of Separation ax-sep holds in permutation models. Part of Exercise II.9.2 of Kunen2 p. 148.

Note that, to prove that an instance of Separation 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 Separation holds. (Contributed by Eric Schmidt, 6-Nov-2025)

	Ref	Expression
Hypotheses	permmodel.1	⊢ 𝐹 : V –1-1-onto→ V
	permmodel.2	⊢ 𝑅 = ( ◡ 𝐹 ∘ E )
Assertion	permaxsep	⊢ ∃ 𝑦 ∀ 𝑥 ( 𝑥 𝑅 𝑦 ↔ ( 𝑥 𝑅 𝑧 ∧ 𝜑 ) )

Proof

Step	Hyp	Ref	Expression
1		permmodel.1	⊢ 𝐹 : V –1-1-onto→ V
2		permmodel.2	⊢ 𝑅 = ( ◡ 𝐹 ∘ E )
3		fvex	⊢ ( ◡ 𝐹 ‘ { 𝑥 ∈ ( 𝐹 ‘ 𝑧 ) ∣ 𝜑 } ) ∈ V
4		nfcv	⊢ Ⅎ 𝑥 ◡ 𝐹
5		nfrab1	⊢ Ⅎ 𝑥 { 𝑥 ∈ ( 𝐹 ‘ 𝑧 ) ∣ 𝜑 }
6	4 5	nffv	⊢ Ⅎ 𝑥 ( ◡ 𝐹 ‘ { 𝑥 ∈ ( 𝐹 ‘ 𝑧 ) ∣ 𝜑 } )
7	6	nfeq2	⊢ Ⅎ 𝑥 𝑦 = ( ◡ 𝐹 ‘ { 𝑥 ∈ ( 𝐹 ‘ 𝑧 ) ∣ 𝜑 } )
8		breq2	⊢ ( 𝑦 = ( ◡ 𝐹 ‘ { 𝑥 ∈ ( 𝐹 ‘ 𝑧 ) ∣ 𝜑 } ) → ( 𝑥 𝑅 𝑦 ↔ 𝑥 𝑅 ( ◡ 𝐹 ‘ { 𝑥 ∈ ( 𝐹 ‘ 𝑧 ) ∣ 𝜑 } ) ) )
9	8	bibi1d	⊢ ( 𝑦 = ( ◡ 𝐹 ‘ { 𝑥 ∈ ( 𝐹 ‘ 𝑧 ) ∣ 𝜑 } ) → ( ( 𝑥 𝑅 𝑦 ↔ ( 𝑥 𝑅 𝑧 ∧ 𝜑 ) ) ↔ ( 𝑥 𝑅 ( ◡ 𝐹 ‘ { 𝑥 ∈ ( 𝐹 ‘ 𝑧 ) ∣ 𝜑 } ) ↔ ( 𝑥 𝑅 𝑧 ∧ 𝜑 ) ) ) )
10	7 9	albid	⊢ ( 𝑦 = ( ◡ 𝐹 ‘ { 𝑥 ∈ ( 𝐹 ‘ 𝑧 ) ∣ 𝜑 } ) → ( ∀ 𝑥 ( 𝑥 𝑅 𝑦 ↔ ( 𝑥 𝑅 𝑧 ∧ 𝜑 ) ) ↔ ∀ 𝑥 ( 𝑥 𝑅 ( ◡ 𝐹 ‘ { 𝑥 ∈ ( 𝐹 ‘ 𝑧 ) ∣ 𝜑 } ) ↔ ( 𝑥 𝑅 𝑧 ∧ 𝜑 ) ) ) )
11		vex	⊢ 𝑥 ∈ V
12		fvex	⊢ ( 𝐹 ‘ 𝑧 ) ∈ V
13	12	rabex	⊢ { 𝑥 ∈ ( 𝐹 ‘ 𝑧 ) ∣ 𝜑 } ∈ V
14	1 2 11 13	brpermmodelcnv	⊢ ( 𝑥 𝑅 ( ◡ 𝐹 ‘ { 𝑥 ∈ ( 𝐹 ‘ 𝑧 ) ∣ 𝜑 } ) ↔ 𝑥 ∈ { 𝑥 ∈ ( 𝐹 ‘ 𝑧 ) ∣ 𝜑 } )
15		rabid	⊢ ( 𝑥 ∈ { 𝑥 ∈ ( 𝐹 ‘ 𝑧 ) ∣ 𝜑 } ↔ ( 𝑥 ∈ ( 𝐹 ‘ 𝑧 ) ∧ 𝜑 ) )
16		vex	⊢ 𝑧 ∈ V
17	1 2 11 16	brpermmodel	⊢ ( 𝑥 𝑅 𝑧 ↔ 𝑥 ∈ ( 𝐹 ‘ 𝑧 ) )
18	17	bicomi	⊢ ( 𝑥 ∈ ( 𝐹 ‘ 𝑧 ) ↔ 𝑥 𝑅 𝑧 )
19	15 18	bianbi	⊢ ( 𝑥 ∈ { 𝑥 ∈ ( 𝐹 ‘ 𝑧 ) ∣ 𝜑 } ↔ ( 𝑥 𝑅 𝑧 ∧ 𝜑 ) )
20	14 19	bitri	⊢ ( 𝑥 𝑅 ( ◡ 𝐹 ‘ { 𝑥 ∈ ( 𝐹 ‘ 𝑧 ) ∣ 𝜑 } ) ↔ ( 𝑥 𝑅 𝑧 ∧ 𝜑 ) )
21	20	ax-gen	⊢ ∀ 𝑥 ( 𝑥 𝑅 ( ◡ 𝐹 ‘ { 𝑥 ∈ ( 𝐹 ‘ 𝑧 ) ∣ 𝜑 } ) ↔ ( 𝑥 𝑅 𝑧 ∧ 𝜑 ) )
22	3 10 21	ceqsexv2d	⊢ ∃ 𝑦 ∀ 𝑥 ( 𝑥 𝑅 𝑦 ↔ ( 𝑥 𝑅 𝑧 ∧ 𝜑 ) )