Theorem permaxpr

Description: The Axiom of Pairing ax-pr 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	permaxpr	⊢ ∃ 𝑧 ∀ 𝑤 ( ( 𝑤 = 𝑥 ∨ 𝑤 = 𝑦 ) → 𝑤 𝑅 𝑧 )

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		prex	⊢ { 𝑥 , 𝑦 } ∈ V
9	1 2 7 8	brpermmodelcnv	⊢ ( 𝑤 𝑅 ( ◡ 𝐹 ‘ { 𝑥 , 𝑦 } ) ↔ 𝑤 ∈ { 𝑥 , 𝑦 } )
10	7	elpr	⊢ ( 𝑤 ∈ { 𝑥 , 𝑦 } ↔ ( 𝑤 = 𝑥 ∨ 𝑤 = 𝑦 ) )
11	9 10	sylbbr	⊢ ( ( 𝑤 = 𝑥 ∨ 𝑤 = 𝑦 ) → 𝑤 𝑅 ( ◡ 𝐹 ‘ { 𝑥 , 𝑦 } ) )
12	11	ax-gen	⊢ ∀ 𝑤 ( ( 𝑤 = 𝑥 ∨ 𝑤 = 𝑦 ) → 𝑤 𝑅 ( ◡ 𝐹 ‘ { 𝑥 , 𝑦 } ) )
13	3 6 12	ceqsexv2d	⊢ ∃ 𝑧 ∀ 𝑤 ( ( 𝑤 = 𝑥 ∨ 𝑤 = 𝑦 ) → 𝑤 𝑅 𝑧 )