Theorem permaxinf2lem

Description: Lemma for permaxinf2 . (Contributed by Eric Schmidt, 6-Nov-2025)

	Ref	Expression
Hypotheses	permmodel.1	$$⊢F:\mathrm{V}\underset{1-1\; onto}{⟶}\mathrm{V}$$
	permmodel.2	$$⊢R=F^{-1}\circ \mathrm{E}$$
	permaxinf2lem.3	$$⊢Z=\mathrm{rec}\left(\left(v\in \mathrm{V}⟼F^{-1}\left(F\left(v\right)\cup \left\{v\right\}\right)\right),F^{-1}\left(\varnothing \right)\right)\left[\mathrm{\omega }\right]$$
Assertion	permaxinf2lem	$$⊢\exists x\left(\exists y\left(yRx\wedge \forall z\neg zRy\right)\wedge \forall y\left(yRx\to \exists z\left(zRx\wedge \forall w\left(wRz\leftrightarrow \left(wRy\vee w=y\right)\right)\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		permmodel.1	$$⊢F:\mathrm{V}\underset{1-1\; onto}{⟶}\mathrm{V}$$
2		permmodel.2	$$⊢R=F^{-1}\circ \mathrm{E}$$
3		permaxinf2lem.3	$$⊢Z=\mathrm{rec}\left(\left(v\in \mathrm{V}⟼F^{-1}\left(F\left(v\right)\cup \left\{v\right\}\right)\right),F^{-1}\left(\varnothing \right)\right)\left[\mathrm{\omega }\right]$$
4		fvex	$$⊢F^{-1}\left(Z\right)\in \mathrm{V}$$
5		breq2	$$⊢x=F^{-1}\left(Z\right)\to \left(yRx\leftrightarrow yR{F}^{-1}\left(Z\right)\right)$$
6	5	anbi1d	$$⊢x=F^{-1}\left(Z\right)\to \left(\left(yRx\wedge \forall z\neg zRy\right)\leftrightarrow \left(yR{F}^{-1}\left(Z\right)\wedge \forall z\neg zRy\right)\right)$$
7	6	exbidv	$$⊢x=F^{-1}\left(Z\right)\to \left(\exists y\left(yRx\wedge \forall z\neg zRy\right)\leftrightarrow \exists y\left(yR{F}^{-1}\left(Z\right)\wedge \forall z\neg zRy\right)\right)$$
8		breq2	$$⊢x=F^{-1}\left(Z\right)\to \left(zRx\leftrightarrow zR{F}^{-1}\left(Z\right)\right)$$
9	8	anbi1d	$$⊢x=F^{-1}\left(Z\right)\to \left(\left(zRx\wedge \forall w\left(wRz\leftrightarrow \left(wRy\vee w=y\right)\right)\right)\leftrightarrow \left(zR{F}^{-1}\left(Z\right)\wedge \forall w\left(wRz\leftrightarrow \left(wRy\vee w=y\right)\right)\right)\right)$$
10	9	exbidv	$$⊢x=F^{-1}\left(Z\right)\to \left(\exists z\left(zRx\wedge \forall w\left(wRz\leftrightarrow \left(wRy\vee w=y\right)\right)\right)\leftrightarrow \exists z\left(zR{F}^{-1}\left(Z\right)\wedge \forall w\left(wRz\leftrightarrow \left(wRy\vee w=y\right)\right)\right)\right)$$
11	5 10	imbi12d	$$⊢x=F^{-1}\left(Z\right)\to \left(\left(yRx\to \exists z\left(zRx\wedge \forall w\left(wRz\leftrightarrow \left(wRy\vee w=y\right)\right)\right)\right)\leftrightarrow \left(yR{F}^{-1}\left(Z\right)\to \exists z\left(zR{F}^{-1}\left(Z\right)\wedge \forall w\left(wRz\leftrightarrow \left(wRy\vee w=y\right)\right)\right)\right)\right)$$
12	11	albidv	$$⊢x=F^{-1}\left(Z\right)\to \left(\forall y\left(yRx\to \exists z\left(zRx\wedge \forall w\left(wRz\leftrightarrow \left(wRy\vee w=y\right)\right)\right)\right)\leftrightarrow \forall y\left(yR{F}^{-1}\left(Z\right)\to \exists z\left(zR{F}^{-1}\left(Z\right)\wedge \forall w\left(wRz\leftrightarrow \left(wRy\vee w=y\right)\right)\right)\right)\right)$$
13	7 12	anbi12d	$$⊢x=F^{-1}\left(Z\right)\to \left(\left(\exists y\left(yRx\wedge \forall z\neg zRy\right)\wedge \forall y\left(yRx\to \exists z\left(zRx\wedge \forall w\left(wRz\leftrightarrow \left(wRy\vee w=y\right)\right)\right)\right)\right)\leftrightarrow \left(\exists y\left(yR{F}^{-1}\left(Z\right)\wedge \forall z\neg zRy\right)\wedge \forall y\left(yR{F}^{-1}\left(Z\right)\to \exists z\left(zR{F}^{-1}\left(Z\right)\wedge \forall w\left(wRz\leftrightarrow \left(wRy\vee w=y\right)\right)\right)\right)\right)\right)$$
14		fvex	$$⊢F^{-1}\left(\varnothing \right)\in \mathrm{V}$$
15		breq1	$$⊢y=F^{-1}\left(\varnothing \right)\to \left(yR{F}^{-1}\left(Z\right)\leftrightarrow F^{-1}\left(\varnothing \right)R{F}^{-1}\left(Z\right)\right)$$
16		breq2	$$⊢y=F^{-1}\left(\varnothing \right)\to \left(zRy\leftrightarrow zR{F}^{-1}\left(\varnothing \right)\right)$$
17	16	notbid	$$⊢y=F^{-1}\left(\varnothing \right)\to \left(\neg zRy\leftrightarrow \neg zR{F}^{-1}\left(\varnothing \right)\right)$$
18	17	albidv	$$⊢y=F^{-1}\left(\varnothing \right)\to \left(\forall z\neg zRy\leftrightarrow \forall z\neg zR{F}^{-1}\left(\varnothing \right)\right)$$
19	15 18	anbi12d	$$⊢y=F^{-1}\left(\varnothing \right)\to \left(\left(yR{F}^{-1}\left(Z\right)\wedge \forall z\neg zRy\right)\leftrightarrow \left(F^{-1}\left(\varnothing \right)R{F}^{-1}\left(Z\right)\wedge \forall z\neg zR{F}^{-1}\left(\varnothing \right)\right)\right)$$
20		orbitinit	$$⊢F^{-1}\left(\varnothing \right)\in \mathrm{V}\to F^{-1}\left(\varnothing \right)\in \mathrm{rec}\left(\left(v\in \mathrm{V}⟼F^{-1}\left(F\left(v\right)\cup \left\{v\right\}\right)\right),F^{-1}\left(\varnothing \right)\right)\left[\mathrm{\omega }\right]$$
21	20 3	eleqtrrdi	$$⊢F^{-1}\left(\varnothing \right)\in \mathrm{V}\to F^{-1}\left(\varnothing \right)\in Z$$
22	14 21	ax-mp	$$⊢F^{-1}\left(\varnothing \right)\in Z$$
23		orbitex	$$⊢\mathrm{rec}\left(\left(v\in \mathrm{V}⟼F^{-1}\left(F\left(v\right)\cup \left\{v\right\}\right)\right),F^{-1}\left(\varnothing \right)\right)\left[\mathrm{\omega }\right]\in \mathrm{V}$$
24	3 23	eqeltri	$$⊢Z\in \mathrm{V}$$
25	1 2 14 24	brpermmodelcnv	$$⊢F^{-1}\left(\varnothing \right)R{F}^{-1}\left(Z\right)\leftrightarrow F^{-1}\left(\varnothing \right)\in Z$$
26	22 25	mpbir	$$⊢F^{-1}\left(\varnothing \right)R{F}^{-1}\left(Z\right)$$
27		noel	$$⊢\neg z\in \varnothing$$
28		vex	$$⊢z\in \mathrm{V}$$
29		0ex	$$⊢\varnothing \in \mathrm{V}$$
30	1 2 28 29	brpermmodelcnv	$$⊢zR{F}^{-1}\left(\varnothing \right)\leftrightarrow z\in \varnothing$$
31	27 30	mtbir	$$⊢\neg zR{F}^{-1}\left(\varnothing \right)$$
32	31	ax-gen	$$⊢\forall z\neg zR{F}^{-1}\left(\varnothing \right)$$
33	26 32	pm3.2i	$$⊢\left(F^{-1}\left(\varnothing \right)R{F}^{-1}\left(Z\right)\wedge \forall z\neg zR{F}^{-1}\left(\varnothing \right)\right)$$
34	14 19 33	ceqsexv2d	$$⊢\exists y\left(yR{F}^{-1}\left(Z\right)\wedge \forall z\neg zRy\right)$$
35		fvex	$$⊢F^{-1}\left(F\left(y\right)\cup \left\{y\right\}\right)\in \mathrm{V}$$
36		nfcv	$$⊢\underset{\_}{Ⅎ}vy$$
37		nfcv	$$⊢\underset{\_}{Ⅎ}v{F}^{-1}\left(F\left(y\right)\cup \left\{y\right\}\right)$$
38		fveq2	$$⊢v=y\to F\left(v\right)=F\left(y\right)$$
39		sneq	$$⊢v=y\to \left\{v\right\}=\left\{y\right\}$$
40	38 39	uneq12d	$$⊢v=y\to F\left(v\right)\cup \left\{v\right\}=F\left(y\right)\cup \left\{y\right\}$$
41	40	fveq2d	$$⊢v=y\to F^{-1}\left(F\left(v\right)\cup \left\{v\right\}\right)=F^{-1}\left(F\left(y\right)\cup \left\{y\right\}\right)$$
42	36 37 3 41	orbitclmpt	$$⊢\left(y\in Z\wedge F^{-1}\left(F\left(y\right)\cup \left\{y\right\}\right)\in \mathrm{V}\right)\to F^{-1}\left(F\left(y\right)\cup \left\{y\right\}\right)\in Z$$
43	35 42	mpan2	$$⊢y\in Z\to F^{-1}\left(F\left(y\right)\cup \left\{y\right\}\right)\in Z$$
44		vex	$$⊢y\in \mathrm{V}$$
45	1 2 44 24	brpermmodelcnv	$$⊢yR{F}^{-1}\left(Z\right)\leftrightarrow y\in Z$$
46	1 2 35 24	brpermmodelcnv	$$⊢F^{-1}\left(F\left(y\right)\cup \left\{y\right\}\right)R{F}^{-1}\left(Z\right)\leftrightarrow F^{-1}\left(F\left(y\right)\cup \left\{y\right\}\right)\in Z$$
47	43 45 46	3imtr4i	$$⊢yR{F}^{-1}\left(Z\right)\to F^{-1}\left(F\left(y\right)\cup \left\{y\right\}\right)R{F}^{-1}\left(Z\right)$$
48		vex	$$⊢w\in \mathrm{V}$$
49		fvex	$$⊢F\left(y\right)\in \mathrm{V}$$
50		vsnex	$$⊢\left\{y\right\}\in \mathrm{V}$$
51	49 50	unex	$$⊢F\left(y\right)\cup \left\{y\right\}\in \mathrm{V}$$
52	1 2 48 51	brpermmodelcnv	$$⊢wR{F}^{-1}\left(F\left(y\right)\cup \left\{y\right\}\right)\leftrightarrow w\in \left(F\left(y\right)\cup \left\{y\right\}\right)$$
53		elun	$$⊢w\in \left(F\left(y\right)\cup \left\{y\right\}\right)\leftrightarrow \left(w\in F\left(y\right)\vee w\in \left\{y\right\}\right)$$
54	1 2 48 44	brpermmodel	$$⊢wRy\leftrightarrow w\in F\left(y\right)$$
55	54	bicomi	$$⊢w\in F\left(y\right)\leftrightarrow wRy$$
56		velsn	$$⊢w\in \left\{y\right\}\leftrightarrow w=y$$
57	55 56	orbi12i	$$⊢\left(w\in F\left(y\right)\vee w\in \left\{y\right\}\right)\leftrightarrow \left(wRy\vee w=y\right)$$
58	52 53 57	3bitri	$$⊢wR{F}^{-1}\left(F\left(y\right)\cup \left\{y\right\}\right)\leftrightarrow \left(wRy\vee w=y\right)$$
59	58	ax-gen	$$⊢\forall w\left(wR{F}^{-1}\left(F\left(y\right)\cup \left\{y\right\}\right)\leftrightarrow \left(wRy\vee w=y\right)\right)$$
60		breq1	$$⊢z=F^{-1}\left(F\left(y\right)\cup \left\{y\right\}\right)\to \left(zR{F}^{-1}\left(Z\right)\leftrightarrow F^{-1}\left(F\left(y\right)\cup \left\{y\right\}\right)R{F}^{-1}\left(Z\right)\right)$$
61		breq2	$$⊢z=F^{-1}\left(F\left(y\right)\cup \left\{y\right\}\right)\to \left(wRz\leftrightarrow wR{F}^{-1}\left(F\left(y\right)\cup \left\{y\right\}\right)\right)$$
62	61	bibi1d	$$⊢z=F^{-1}\left(F\left(y\right)\cup \left\{y\right\}\right)\to \left(\left(wRz\leftrightarrow \left(wRy\vee w=y\right)\right)\leftrightarrow \left(wR{F}^{-1}\left(F\left(y\right)\cup \left\{y\right\}\right)\leftrightarrow \left(wRy\vee w=y\right)\right)\right)$$
63	62	albidv	$$⊢z=F^{-1}\left(F\left(y\right)\cup \left\{y\right\}\right)\to \left(\forall w\left(wRz\leftrightarrow \left(wRy\vee w=y\right)\right)\leftrightarrow \forall w\left(wR{F}^{-1}\left(F\left(y\right)\cup \left\{y\right\}\right)\leftrightarrow \left(wRy\vee w=y\right)\right)\right)$$
64	60 63	anbi12d	$$⊢z=F^{-1}\left(F\left(y\right)\cup \left\{y\right\}\right)\to \left(\left(zR{F}^{-1}\left(Z\right)\wedge \forall w\left(wRz\leftrightarrow \left(wRy\vee w=y\right)\right)\right)\leftrightarrow \left(F^{-1}\left(F\left(y\right)\cup \left\{y\right\}\right)R{F}^{-1}\left(Z\right)\wedge \forall w\left(wR{F}^{-1}\left(F\left(y\right)\cup \left\{y\right\}\right)\leftrightarrow \left(wRy\vee w=y\right)\right)\right)\right)$$
65	35 64	spcev	$$⊢\left(F^{-1}\left(F\left(y\right)\cup \left\{y\right\}\right)R{F}^{-1}\left(Z\right)\wedge \forall w\left(wR{F}^{-1}\left(F\left(y\right)\cup \left\{y\right\}\right)\leftrightarrow \left(wRy\vee w=y\right)\right)\right)\to \exists z\left(zR{F}^{-1}\left(Z\right)\wedge \forall w\left(wRz\leftrightarrow \left(wRy\vee w=y\right)\right)\right)$$
66	47 59 65	sylancl	$$⊢yR{F}^{-1}\left(Z\right)\to \exists z\left(zR{F}^{-1}\left(Z\right)\wedge \forall w\left(wRz\leftrightarrow \left(wRy\vee w=y\right)\right)\right)$$
67	66	ax-gen	$$⊢\forall y\left(yR{F}^{-1}\left(Z\right)\to \exists z\left(zR{F}^{-1}\left(Z\right)\wedge \forall w\left(wRz\leftrightarrow \left(wRy\vee w=y\right)\right)\right)\right)$$
68	34 67	pm3.2i	$$⊢\left(\exists y\left(yR{F}^{-1}\left(Z\right)\wedge \forall z\neg zRy\right)\wedge \forall y\left(yR{F}^{-1}\left(Z\right)\to \exists z\left(zR{F}^{-1}\left(Z\right)\wedge \forall w\left(wRz\leftrightarrow \left(wRy\vee w=y\right)\right)\right)\right)\right)$$
69	4 13 68	ceqsexv2d	$$⊢\exists x\left(\exists y\left(yRx\wedge \forall z\neg zRy\right)\wedge \forall y\left(yRx\to \exists z\left(zRx\wedge \forall w\left(wRz\leftrightarrow \left(wRy\vee w=y\right)\right)\right)\right)\right)$$