Theorem permaxrep

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

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

	Ref	Expression
Hypotheses	permmodel.1	|- F : _V -1-1-onto-> _V
	permmodel.2	|- R = ( `' F o. _E )
Assertion	permaxrep	|- ( A. w E. y A. z ( A. y ph -> z = y ) -> E. y A. z ( z R y <-> E. w ( w R x /\ A. y ph ) ) )

Proof

Step	Hyp	Ref	Expression
1		permmodel.1	|- F : _V -1-1-onto-> _V
2		permmodel.2	|- R = ( `' F o. _E )
3		nfa1	|- F/ y A. y ph
4	3	mof	|- ( E* z A. y ph <-> E. y A. z ( A. y ph -> z = y ) )
5	4	albii	|- ( A. w E* z A. y ph <-> A. w E. y A. z ( A. y ph -> z = y ) )
6		fvex	|- ( `' F ` { z | E. w e. ( F ` x ) A. y ph } ) e. _V
7		nfmo1	|- F/ z E* z A. y ph
8	7	nfal	|- F/ z A. w E* z A. y ph
9		vex	|- z e. _V
10	1 2 9 6	brpermmodel	|- ( z R ( `' F ` { z | E. w e. ( F ` x ) A. y ph } ) <-> z e. ( F ` ( `' F ` { z | E. w e. ( F ` x ) A. y ph } ) ) )
11		fvex	|- ( F ` x ) e. _V
12		axrep6g	|- ( ( ( F ` x ) e. _V /\ A. w E* z A. y ph ) -> { z | E. w e. ( F ` x ) A. y ph } e. _V )
13	11 12	mpan	|- ( A. w E* z A. y ph -> { z | E. w e. ( F ` x ) A. y ph } e. _V )
14		f1ocnvfv2	|- ( ( F : _V -1-1-onto-> _V /\ { z | E. w e. ( F ` x ) A. y ph } e. _V ) -> ( F ` ( `' F ` { z | E. w e. ( F ` x ) A. y ph } ) ) = { z | E. w e. ( F ` x ) A. y ph } )
15	1 13 14	sylancr	|- ( A. w E* z A. y ph -> ( F ` ( `' F ` { z | E. w e. ( F ` x ) A. y ph } ) ) = { z | E. w e. ( F ` x ) A. y ph } )
16	15	eleq2d	|- ( A. w E* z A. y ph -> ( z e. ( F ` ( `' F ` { z | E. w e. ( F ` x ) A. y ph } ) ) <-> z e. { z | E. w e. ( F ` x ) A. y ph } ) )
17	10 16	bitrid	|- ( A. w E* z A. y ph -> ( z R ( `' F ` { z | E. w e. ( F ` x ) A. y ph } ) <-> z e. { z | E. w e. ( F ` x ) A. y ph } ) )
18		df-rex	|- ( E. w e. ( F ` x ) A. y ph <-> E. w ( w e. ( F ` x ) /\ A. y ph ) )
19		abid	|- ( z e. { z | E. w e. ( F ` x ) A. y ph } <-> E. w e. ( F ` x ) A. y ph )
20		vex	|- w e. _V
21		vex	|- x e. _V
22	1 2 20 21	brpermmodel	|- ( w R x <-> w e. ( F ` x ) )
23	22	anbi1i	|- ( ( w R x /\ A. y ph ) <-> ( w e. ( F ` x ) /\ A. y ph ) )
24	23	exbii	|- ( E. w ( w R x /\ A. y ph ) <-> E. w ( w e. ( F ` x ) /\ A. y ph ) )
25	18 19 24	3bitr4i	|- ( z e. { z | E. w e. ( F ` x ) A. y ph } <-> E. w ( w R x /\ A. y ph ) )
26	17 25	bitrdi	|- ( A. w E* z A. y ph -> ( z R ( `' F ` { z | E. w e. ( F ` x ) A. y ph } ) <-> E. w ( w R x /\ A. y ph ) ) )
27	8 26	alrimi	|- ( A. w E* z A. y ph -> A. z ( z R ( `' F ` { z | E. w e. ( F ` x ) A. y ph } ) <-> E. w ( w R x /\ A. y ph ) ) )
28		nfcv	|- F/_ y `' F
29		nfcv	|- F/_ y ( F ` x )
30	29 3	nfrexw	|- F/ y E. w e. ( F ` x ) A. y ph
31	30	nfab	|- F/_ y { z | E. w e. ( F ` x ) A. y ph }
32	28 31	nffv	|- F/_ y ( `' F ` { z | E. w e. ( F ` x ) A. y ph } )
33		nfcv	|- F/_ y z
34		nfcv	|- F/_ y R
35	33 34 32	nfbr	|- F/ y z R ( `' F ` { z | E. w e. ( F ` x ) A. y ph } )
36		nfv	|- F/ y w R x
37	36 3	nfan	|- F/ y ( w R x /\ A. y ph )
38	37	nfex	|- F/ y E. w ( w R x /\ A. y ph )
39	35 38	nfbi	|- F/ y ( z R ( `' F ` { z | E. w e. ( F ` x ) A. y ph } ) <-> E. w ( w R x /\ A. y ph ) )
40	39	nfal	|- F/ y A. z ( z R ( `' F ` { z | E. w e. ( F ` x ) A. y ph } ) <-> E. w ( w R x /\ A. y ph ) )
41		nfcv	|- F/_ z `' F
42		nfab1	|- F/_ z { z | E. w e. ( F ` x ) A. y ph }
43	41 42	nffv	|- F/_ z ( `' F ` { z | E. w e. ( F ` x ) A. y ph } )
44	43	nfeq2	|- F/ z y = ( `' F ` { z | E. w e. ( F ` x ) A. y ph } )
45		breq2	|- ( y = ( `' F ` { z | E. w e. ( F ` x ) A. y ph } ) -> ( z R y <-> z R ( `' F ` { z | E. w e. ( F ` x ) A. y ph } ) ) )
46	45	bibi1d	|- ( y = ( `' F ` { z | E. w e. ( F ` x ) A. y ph } ) -> ( ( z R y <-> E. w ( w R x /\ A. y ph ) ) <-> ( z R ( `' F ` { z | E. w e. ( F ` x ) A. y ph } ) <-> E. w ( w R x /\ A. y ph ) ) ) )
47	44 46	albid	|- ( y = ( `' F ` { z | E. w e. ( F ` x ) A. y ph } ) -> ( A. z ( z R y <-> E. w ( w R x /\ A. y ph ) ) <-> A. z ( z R ( `' F ` { z | E. w e. ( F ` x ) A. y ph } ) <-> E. w ( w R x /\ A. y ph ) ) ) )
48	32 40 47	spcegf	|- ( ( `' F ` { z | E. w e. ( F ` x ) A. y ph } ) e. _V -> ( A. z ( z R ( `' F ` { z | E. w e. ( F ` x ) A. y ph } ) <-> E. w ( w R x /\ A. y ph ) ) -> E. y A. z ( z R y <-> E. w ( w R x /\ A. y ph ) ) ) )
49	6 27 48	mpsyl	|- ( A. w E* z A. y ph -> E. y A. z ( z R y <-> E. w ( w R x /\ A. y ph ) ) )
50	5 49	sylbir	|- ( A. w E. y A. z ( A. y ph -> z = y ) -> E. y A. z ( z R y <-> E. w ( w R x /\ A. y ph ) ) )