Theorem wfaxsep

Description: The class of well-founded sets models the Axiom of Separation ax-sep . Actually, our statement is stronger, since it is an instance of Separation only when all quantifiers in ph are relativized to W . Part of Corollary II.2.5 of Kunen2 p. 112. (Contributed by Eric Schmidt, 29-Sep-2025)

	Ref	Expression
Hypothesis	wfax.1	|- W = U. ( R1 " On )
Assertion	wfaxsep	|- A. z e. W E. y e. W A. x e. W ( x e. y <-> ( x e. z /\ ph ) )

Proof

Step	Hyp	Ref	Expression
1		wfax.1	|- W = U. ( R1 " On )
2		ssclaxsep	|- ( A. z e. W ~P z C_ W -> A. z e. W E. y e. W A. x e. W ( x e. y <-> ( x e. z /\ ph ) ) )
3		pwwf	|- ( z e. U. ( R1 " On ) <-> ~P z e. U. ( R1 " On ) )
4		r1elssi	|- ( ~P z e. U. ( R1 " On ) -> ~P z C_ U. ( R1 " On ) )
5	3 4	sylbi	|- ( z e. U. ( R1 " On ) -> ~P z C_ U. ( R1 " On ) )
6	1	eleq2i	|- ( z e. W <-> z e. U. ( R1 " On ) )
7	1	sseq2i	|- ( ~P z C_ W <-> ~P z C_ U. ( R1 " On ) )
8	5 6 7	3imtr4i	|- ( z e. W -> ~P z C_ W )
9	2 8	mprg	|- A. z e. W E. y e. W A. x e. W ( x e. y <-> ( x e. z /\ ph ) )