Theorem wfaxun

Description: The class of well-founded sets models the Axiom of Union ax-un . Part of Corollary II.2.5 of Kunen2 p. 112. (Contributed by Eric Schmidt, 19-Oct-2025)

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

Proof

Step	Hyp	Ref	Expression
1		wfax.1	|- W = U. ( R1 " On )
2		uniclaxun	|- ( A. x e. W U. x e. W -> A. x e. W E. y e. W A. z e. W ( E. w e. W ( z e. w /\ w e. x ) -> z e. y ) )
3		uniwf	|- ( x e. U. ( R1 " On ) <-> U. x e. U. ( R1 " On ) )
4	1	eleq2i	|- ( x e. W <-> x e. U. ( R1 " On ) )
5	1	eleq2i	|- ( U. x e. W <-> U. x e. U. ( R1 " On ) )
6	3 4 5	3bitr4i	|- ( x e. W <-> U. x e. W )
7	6	biimpi	|- ( x e. W -> U. x e. W )
8	2 7	mprg	|- A. x e. W E. y e. W A. z e. W ( E. w e. W ( z e. w /\ w e. x ) -> z e. y )